DSL for module semantics

spectec/src/backend-latex/render.ml

@@ -327,7 +327,7 @@ exception Arity_mismatch
 let rec expand_iter args iter =
   match iter with
   | Opt | List | List1 -> iter
-  | ListN (e, opt) -> ListN (expand_exp args e, opt)
+  | ListN (e, id_opt) -> ListN (expand_exp args e, id_opt)
 
 and expand_exp args e = expand_exp' args e.it $ e.at
 and expand_exp' args e' =
@@ -442,9 +442,9 @@ and render_iter env = function
   | List -> "^\\ast"
   | List1 -> "^{+}"
   | ListN ({it = ParenE (e, _); _}, None) | ListN (e, None) ->
-      "^{" ^ render_exp env e ^ "}"
+    "^{" ^ render_exp env e ^ "}"
   | ListN (e, Some id) ->
-      "^(" ^ id.it ^ "<" ^ render_exp env e ^ ")"
+    "^(" ^ id.it ^ "<" ^ render_exp env e ^ ")"
 
 
 (* Types *)
@@ -687,7 +687,7 @@ let render_ruledef env d =
     render_rule_deco env " \\, " id1 id2 ""
   | _ -> failwith "render_ruledef"
 
-let render_condition env tabs = function
+let render_conditions env tabs = function
   | [] -> " & "
   | [Elem {it = ElsePr; _}] -> " &\\quad\n  " ^ word "otherwise"
   | (Elem {it = ElsePr; _})::prems ->
@@ -708,14 +708,14 @@ let render_reddef env d =
     in
     render_rule_deco env "" id1 id2 " \\quad " ^ "& " ^
       render_exp env e1 ^ " &" ^ render_atom env SqArrow ^ "& " ^
-        render_exp env e2 ^ render_condition env "&&&&" prems
+        render_exp env e2 ^ render_conditions env "&&&&" prems
   | _ -> failwith "render_reddef"
 
 let render_funcdef env d =
   match d.it with
   | DefD (id1, e1, e2, prems) ->
     render_exp env (CallE (id1, e1) $ d.at) ^ " &=& " ^
-      render_exp env e2 ^ render_condition env "&&&" prems
+      render_exp env e2 ^ render_conditions env "&&&" prems
   | _ -> failwith "render_funcdef"
 
 let rec render_sep_defs ?(sep = " \\\\\n") ?(br = " \\\\[0.8ex]\n") f = function

spectec/src/el/eq.ml

@@ -22,7 +22,7 @@ let rec eq_iter iter1 iter2 =
   match iter1, iter2 with
   | ListN (e1, None), ListN (e2, None) -> eq_exp e1 e2
   | ListN (e1, Some id1), ListN (e2, Some id2) ->
-      eq_exp e1 e2 && id1.it = id2.it
+    eq_exp e1 e2 && id1.it = id2.it
   | _, _ -> false
 
 

spectec/src/el/free.ml

@@ -18,6 +18,7 @@ let union sets1 sets2 =
     defid = Set.union sets1.defid sets2.defid;
   }
 
+let free_opt free_x xo = Option.(value (map free_x xo) ~default:empty)
 let free_list free_x xs = List.(fold_left union empty (map free_x xs))
 
 let free_nl_elem free_x = function Nl -> empty | Elem x -> free_x x
@@ -37,7 +38,7 @@ let free_defid id = {empty with defid = Set.singleton id.it}
 let rec free_iter iter =
   match iter with
   | Opt | List | List1 -> empty
-  | ListN (e, _) -> free_exp e
+  | ListN (e, id_opt) -> union (free_exp e) (free_opt free_varid id_opt)
 
 
 (* Types *)

spectec/src/el/print.ml

@@ -71,8 +71,7 @@ let rec string_of_iter iter =
   | List -> "*"
   | List1 -> "+"
   | ListN (e, None) -> "^" ^ string_of_exp e
-  | ListN (e, Some (id)) ->
-      "^(" ^ id.it ^ "<" ^ string_of_exp e ^ ")"
+  | ListN (e, Some (id)) -> "^(" ^ id.it ^ "<" ^ string_of_exp e ^ ")"
 
 
 (* Types *)

spectec/src/frontend/elab.ml

@@ -336,7 +336,7 @@ let rec elab_iter env iter : Il.iter =
   | Opt -> Il.Opt
   | List -> Il.List
   | List1 -> Il.List1
-  | ListN (e, opt) -> Il.ListN (elab_exp env e (NatT $ e.at), opt)
+  | ListN (e, id_opt) -> Il.ListN (elab_exp env e (NatT $ e.at), id_opt)
 
 
 (* Types *)

spectec/src/frontend/multiplicity.ml

@@ -68,7 +68,8 @@ let iter_nl_list f xs = List.iter (function Nl -> () | Elem x -> f x) xs
 let rec check_iter env ctx iter =
   match iter with
   | Opt | List | List1 -> ()
-  | ListN (e, _) ->
+  | ListN (e, opt) ->
+      Option.iter (fun id -> check_id env (iter::ctx) id) opt;
       check_exp env ctx e
 
 and check_exp env ctx e =
@@ -162,9 +163,13 @@ let union = Env.union (fun _ ctx1 ctx2 -> assert (ctx1 = ctx2); Some ctx1)
 let rec annot_iter env iter : Il.Ast.iter * occur =
   match iter with
   | Opt | List | List1 -> iter, Env.empty
-  | ListN (e, opt) ->
+  | ListN (e, None) ->
     let e', occur = annot_exp env e in
-    ListN (e', opt), occur
+    ListN (e', None), occur
+  | ListN (e, Some id) ->
+    let e', occur1 = annot_exp env e in
+    let occur2 = Env.singleton id.it [] in
+    ListN (e', Some id), union occur1 occur2
 
 and annot_exp env e : Il.Ast.exp * occur =
   let it, occur =

spectec/src/frontend/parser.mly

@@ -141,8 +141,8 @@ iter :
   | STAR { List }
   | UP arith_prim
     { match $2.it with
-      | ParenE ({ it = CmpE({ it = VarE id; _ }, LtOp, e); _}, false) ->
-          ListN (e, Some id)
+      | ParenE ({it = CmpE({it = VarE id; _}, LtOp, e); _}, false) ->
+        ListN (e, Some id)
       | _ -> ListN ($2, None)
     }
 

spectec/src/il/eq.ml

@@ -26,7 +26,7 @@ let rec eq_iter iter1 iter2 =
   match iter1, iter2 with
   | ListN (e1, None), ListN (e2, None) -> eq_exp e1 e2
   | ListN (e1, Some id1), ListN (e2, Some id2) ->
-      eq_exp e1 e2 && id1.it = id2.it
+    eq_exp e1 e2 && id1.it = id2.it
   | _, _ -> false
 
 

spectec/src/il/free.ml

@@ -55,7 +55,7 @@ let free_defid id = {empty with defid = Set.singleton id.it}
 let rec free_iter iter =
   match iter with
   | Opt | List | List1 -> empty
-  | ListN (e, _) -> free_exp e
+  | ListN (e, id_opt) -> union (free_exp e) (free_opt free_varid id_opt)
 
 
 (* Types *)

spectec/src/il/validation.ml

@@ -241,7 +241,15 @@ let valid_list valid_x_y env xs ys at =
 let rec valid_iter env iter =
   match iter with
   | Opt | List | List1 -> ()
-  | ListN (e, _) -> valid_exp env e (NatT $ e.at)
+  | ListN (e, None) -> valid_exp env e (NatT $ e.at)
+  | ListN (e, Some id) ->
+    valid_exp env e (NatT $ e.at);
+    let t', dim = find "variable" env.vars id in
+    equiv_typ env t' (NatT $ e.at) e.at;
+    if dim <> [iter] then
+      error e.at ("use of iterated variable `" ^
+        id.it ^ String.concat "" (List.map string_of_iter dim) ^
+        "` outside suitable iteraton context")
 
 
 (* Types *)
@@ -314,11 +322,7 @@ and infer_exp env e : typ =
   | CallE (id, _) -> snd (find "function" env.defs id)
   | MixE _ -> error e.at "cannot infer type of mixin notation"
   | IterE (e1, iter) ->
-    let iter' =
-      match fst iter with
-      | ListN _ -> List
-      | iter' -> iter'
-    in
+    let iter' = match fst iter with ListN _ -> List | iter' -> iter' in
     IterT (infer_exp env e1, iter') $ e.at
   | OptE _ -> error e.at "cannot infer type of option"
   | TheE e1 -> as_iter_typ Opt "option" env Check (infer_exp env e1) e1.at

spectec/src/middlend/sub.ml

@@ -119,7 +119,7 @@ and t_exp' env = function
   | SubE (e, t1, t2) -> SubE (e, t1, t2)
 
 and t_iter env = function
-  | ListN (e, id) -> ListN (t_exp env e, id)
+  | ListN (e, id_opt) -> ListN (t_exp env e, id_opt)
   | i -> i
 
 and t_iterexp env (iter, vs) = (t_iter env iter, vs)

spectec/src/middlend/totalize.ml

@@ -78,7 +78,7 @@ and t_exp' env = function
   | SubE (e, t1, t2) -> SubE (e, t1, t2)
 
 and t_iter env = function
-  | ListN (e, id) -> ListN (t_exp env e, id)
+  | ListN (e, id_opt) -> ListN (t_exp env e, id_opt)
   | i -> i
 
 and t_iterexp env (iter, vs) = (t_iter env iter, vs)

spectec/src/middlend/unthe.ml

@@ -156,7 +156,7 @@ and t_iterexp n (iter, vs) =
   unary t_iter n iter (fun iter' -> (iter', vs))
 
 and t_iter n iter = match iter with
-  | ListN (e, id) -> unary t_exp n e (fun e' -> ListN (e', id))
+  | ListN (e, id_opt) -> unary t_exp n e (fun e' -> ListN (e', id_opt))
   | _ -> [], iter
 
 and t_path n = phrase t_path' n

spectec/src/middlend/wild.ml

@@ -180,7 +180,7 @@ and t_iterexp env (iter, vs) =
   unary t_iter env iter (fun iter' -> (iter', vs))
 
 and t_iter env iter = match iter with
-  | ListN (e, id) -> unary t_exp env e (fun e' -> ListN (e', id))
+  | ListN (e, id_opt) -> unary t_exp env e (fun e' -> ListN (e', id_opt))
   | _ -> [], iter
 
 and t_path env = phrase t_path' env