[spectec] extend IterPr AST in IL

spectec/src/backend-ast/print.ml

@@ -167,7 +167,7 @@ and prem pr =
   | IfPr e -> Node ("if", [exp e])
   | LetPr (e1, e2, _xs) -> Node ("let", [exp e1; exp e2])
   | ElsePr -> Atom "else"
-  | IterPr (pr1, it) -> Node ("iter", [prem pr1] @ iterexp it)
+  | IterPr (prs, it) -> Node ("iter", List.map prem prs @ iterexp it)
   | NegPr pr1 -> Node ("neg", [prem pr1])
 
 

spectec/src/backend-prose/gen.ml

@@ -324,7 +324,7 @@ let rec prem_to_instrs prem =
       | OtherRel,       _             -> print_yet_prem prem "prem_to_instrs"; [ YetS "TODO: prem_to_instrs for RulePr" ]
       | _,              _             -> assert false )
     )
-  | Ast.IterPr (prem, iter) ->
+  | Ast.IterPr ([prem], iter) ->
     (match iter with
     | Ast.Opt, [(id, _)] -> [ IfS (isDefinedE (varE id.it ~note:no_note) ~note:no_note, prem_to_instrs prem) ]
     | Ast.(List | ListN _), vars ->

spectec/src/frontend/dim.ml

@@ -596,10 +596,11 @@ and annot_prem env prem : Il.Ast.prem * occur =
       LetPr (e1', e2', ids), union occur1 occur2
     | ElsePr ->
       ElsePr, Env.empty
-    | IterPr (prem1, iter) ->
+    | IterPr ([prem1], iter) ->
       let prem1', occur1 = annot_prem env prem1 in
       let iter', occur' = annot_iterexp env occur1 iter prem.at in
-      IterPr (prem1', iter'), occur'
+      IterPr ([prem1'], iter'), occur'
+    | IterPr (_, _) -> assert false
     | NegPr prem1 ->
       let prem1', occur1 = annot_prem env prem1 in
       NegPr prem1', occur1

spectec/src/frontend/elab.ml

@@ -1824,7 +1824,7 @@ and elab_prem env prem : Il.prem list =
   | IterPr (prem1, iter) ->
     let iter' = elab_iterexp env iter in
     let prem1' = List.hd (elab_prem env prem1) in
-    [Il.IterPr (prem1', iter') $ prem.at]
+    [Il.IterPr ([prem1'], iter') $ prem.at]
 
 
 (* Grammars *)

spectec/src/il/ast.ml

@@ -163,7 +163,7 @@ and prem' =
   | IfPr of exp                                       (* side condition *)
   | LetPr of exp * exp * string list                  (* binding *)
   | ElsePr                                            (* otherwise *)
-  | IterPr of prem * iterexp                          (* iteration *)
+  | IterPr of prem list * iterexp                     (* iteration *)
   | NegPr of prem                                     (* negated premise *)
 
 and hintdef = hintdef' phrase

spectec/src/il/eq.ml

@@ -139,8 +139,8 @@ and eq_prem prem1 prem2 =
   | RulePr (id1, op1, e1), RulePr (id2, op2, e2) ->
     eq_id id1 id2 && eq_mixop op1 op2 && eq_exp e1 e2
   | IfPr e1, IfPr e2 -> eq_exp e1 e2
-  | IterPr (prem1, e1), IterPr (prem2, e2) ->
-    eq_prem prem1 prem2 && eq_iterexp e1 e2
+  | IterPr (prems1, e1), IterPr (prems2, e2) ->
+    eq_list eq_prem prems1 prems2 && eq_iterexp e1 e2
   | LetPr (e1, e1', ids1), LetPr (e2, e2', ids2) ->
     eq_exp e1 e2 && eq_exp e1' e2' && ids1 = ids2
   | _, _ -> prem1.it = prem2.it

spectec/src/il/eval.ml

@@ -502,7 +502,7 @@ and reduce_prem env prem : bool option =
     | None -> None
     | exception Irred -> None
     )
-  | IterPr (_prem, _iter) -> None  (* TODO(3, rossberg): reduce? *)
+  | IterPr (_prems, _iter) -> None  (* TODO(3, rossberg): reduce? *)
   | NegPr prem -> 
     let* b = reduce_prem env prem in
     Some (not b)

spectec/src/il/free.ml

@@ -175,7 +175,7 @@ and free_prem prem =
   | IfPr e -> free_exp e
   | LetPr (e1, e2, _) -> free_exp e1 + free_exp e2
   | ElsePr -> empty
-  | IterPr (prem1, iter) -> (free_prem prem1 - bound_iterexp iter) + free_iterexp iter
+  | IterPr (prems, iter) -> (free_list free_prem prems - bound_iterexp iter) + free_iterexp iter
   | NegPr prem' -> free_prem prem'
 
 and free_prems prems = free_list free_prem prems

spectec/src/il/iter.ml

@@ -177,7 +177,7 @@ and prem pr =
   | RulePr (x, op, e) -> relid x; mixop op; exp e
   | IfPr e -> exp e
   | ElsePr -> ()
-  | IterPr (pr1, it) -> prem pr1; iterexp it
+  | IterPr (pr1, it) -> list prem pr1; iterexp it
   | LetPr (e1, e2, _) -> exp e1; exp e2
   | NegPr pr1 -> prem pr1
 

spectec/src/il/print.ml

@@ -196,7 +196,7 @@ and string_of_sym g =
 
 (* Premises *)
 
-and string_of_prem prem =
+and string_of_prem' lv prem =
   match prem.it with
   | RulePr (id, mixop, e) ->
     string_of_id id ^ ": " ^ string_of_mixop mixop ^ string_of_exp_args e
@@ -206,12 +206,20 @@ and string_of_prem prem =
     "where " ^ string_of_exp e1 ^ " = " ^ string_of_exp e2 ^
     " {" ^ (String.concat ", " (List.map string_of_id ids')) ^ "}"
   | ElsePr -> "otherwise"
-  | IterPr ({it = IterPr _; _} as prem', iter) ->
-    string_of_prem prem' ^ string_of_iterexp iter
-  | IterPr (prem', iter) ->
-    "(" ^ string_of_prem prem' ^ ")" ^ string_of_iterexp iter
+  | IterPr ([{it = IterPr _; _} as prem'], iter) ->
+    string_of_prem' (lv+1) prem' ^ string_of_iterexp iter
+  | IterPr ([prem'], iter) ->
+    "(" ^ string_of_prem' (lv+1) prem' ^ ")" ^ string_of_iterexp iter
+  | IterPr (prems', iter) ->
+    let spaces = String.make (2*(lv+1)) ' ' in
+    let pre = "\n" ^ spaces ^ "-- " in
+    "(" ^
+    concat "" (List.map (prefix pre string_of_prem) prems') ^
+    "\n" ^ spaces ^ ")" ^ string_of_iterexp iter
   | NegPr prem' -> "~ " ^ string_of_prem prem'
 
+and string_of_prem prem = string_of_prem' 2 prem
+
 
 (* Definitions *)
 

spectec/src/il/subst.ml

@@ -213,9 +213,9 @@ and subst_prem s prem =
   | RulePr (id, op, e) -> RulePr (id, op, subst_exp s e)
   | IfPr e -> IfPr (subst_exp s e)
   | ElsePr -> ElsePr
-  | IterPr (prem1, iterexp) ->
+  | IterPr (prems, iterexp) ->
     let it', s' = subst_iterexp s iterexp in
-    IterPr (subst_prem s' prem1, it')
+    IterPr (subst_list subst_prem s' prems, it')
   | LetPr (e1, e2, ids) -> LetPr (subst_exp s e1, subst_exp s e2, ids)
   | NegPr prem' -> NegPr (subst_prem s prem')
   ) $ prem.at

spectec/src/il/valid.ml

@@ -600,9 +600,9 @@ and valid_prem env prem =
         " do not occur in left-hand side expression")
   | ElsePr ->
     ()
-  | IterPr (prem', iterexp) ->
+  | IterPr (prems, iterexp) ->
     let _iter, env' = valid_iterexp env iterexp prem.at in
-    valid_prem env' prem'
+    List.iter (valid_prem env') prems
   | NegPr prem' -> valid_prem env prem'
 
 

spectec/src/il2al/animate.ml

@@ -78,7 +78,8 @@ let rec rewrite_iterexp' iterexp pr =
     let new_ids = List.map (rewrite_id iterexp) ids in
     LetPr (new_ e1, new_ e2, new_ids)
   | ElsePr -> ElsePr
-  | IterPr (pr, (iter, xes)) -> IterPr (rewrite_iterexp iterexp pr, (iter, xes |> List.map (fun (x, e) -> (x, new_ e))))
+  | IterPr (prs, (iter, xes)) -> IterPr (List.map (rewrite_iterexp iterexp) prs,
+                                         (iter, xes |> List.map (fun (x, e) -> (x, new_ e))))
   | NegPr pr' -> NegPr (rewrite_iterexp iterexp pr')
 and rewrite_iterexp iterexp pr = Source.map (rewrite_iterexp' iterexp) pr
 
@@ -109,7 +110,7 @@ let rec recover_iterexp' iterexp pr =
     let new_ids = List.map (recover_id iterexp) ids in
     LetPr (new_ e1, new_ e2, new_ids)
   | ElsePr -> ElsePr
-  | IterPr (pr, (iter, xes)) -> IterPr (recover_iterexp iterexp pr, (iter, xes |> List.map (fun (x, e) -> (x, new_ e))))
+  | IterPr (prs, (iter, xes)) -> IterPr (List.map (recover_iterexp iterexp) prs, (iter, xes |> List.map (fun (x, e) -> (x, new_ e))))
   | NegPr prem -> NegPr (recover_iterexp iterexp prem)
 and recover_iterexp iterexp pr = Source.map (recover_iterexp' iterexp) pr
 
@@ -302,10 +303,11 @@ let rec rows_of_prem vars len i p =
       Condition, p, [i];
       Assign frees, p, [i] @ List.filter_map (index_of len vars) (free_exp_list l)
     ]
-  | IterPr (p', iterexp) ->
+  | IterPr ([p'], iterexp) ->
     let p_r = rewrite_iterexp iterexp p' in
-    let to_iter (tag, p, coverings) = tag, IterPr (recover_iterexp iterexp p, iterexp) $ p.at, coverings in
+    let to_iter (tag, p, coverings) = tag, IterPr ([recover_iterexp iterexp p], iterexp) $ p.at, coverings in
     List.map to_iter (rows_of_prem vars len i p_r)
+  | IterPr (_, _) -> assert false
   | _ -> [ Condition, p, [i] ]
 
 let build_matrix prems known_vars =

spectec/src/il2al/free.ml

@@ -85,8 +85,8 @@ let rec free_prem ignore_listN prem =
   | IfPr e -> f e
   | LetPr (e1, e2, _ids) -> f e1 + f e2
   | ElsePr -> empty
-  | IterPr (prem', iter) ->
-    let free1 = fp prem' in
+  | IterPr (prems, iter) ->
+    let free1 = free_list fp prems in
     let bound, free2 = fi iter in
     diff (free1 + free2) bound
   | NegPr prem' -> fp prem'

spectec/src/il2al/il_walk.ml

@@ -74,7 +74,7 @@ and transform_prem t p =
     | IfPr e -> IfPr (transform_exp t e)
     | LetPr (e1, e2, ss) -> LetPr (transform_exp t e1, transform_exp t e2, ss)
     | ElsePr -> ElsePr
-    | IterPr (p, ie) -> IterPr (transform_prem t p, transform_iterexp t ie)
+    | IterPr (ps, ie) -> IterPr (List.map (transform_prem t) ps, transform_iterexp t ie)
     | NegPr p -> NegPr (transform_prem t p)
   in
   f { p with it }

spectec/src/il2al/preprocess.ml

@@ -8,10 +8,11 @@ let typing_functions = ref []
 
 let rec transform_rulepr_prem prem =
   match prem.it with
-  | IterPr (prem, iterexp) ->
+  | IterPr ([prem], iterexp) ->
     prem
     |> transform_rulepr_prem
-    |> (fun new_prem -> IterPr (new_prem, iterexp) $ prem.at)
+    |> (fun new_prem -> IterPr ([new_prem], iterexp) $ prem.at)
+  | IterPr (_, _) -> assert false
   | IfPr ({ it = CmpE (`EqOp, _, { it = CallE (id, args); note; at }, rhs); _ })
   when List.mem id.it !typing_functions ->
     IfPr (CallE (id, args @ [ExpA rhs $ rhs.at]) $$ at % note) $ prem.at
@@ -44,10 +45,11 @@ let remove_or_exp e =
 let rec remove_or_prem prem =
   match prem.it with
   | IfPr e -> e |> remove_or_exp |> List.map (fun e' -> IfPr e' $ prem.at)
-  | IterPr (prem, iterexp) ->
+  | IterPr ([prem], iterexp) ->
     prem
     |> remove_or_prem
-    |> List.map (fun new_prem -> IterPr (new_prem, iterexp) $ prem.at)
+    |> List.map (fun new_prem -> IterPr ([new_prem], iterexp) $ prem.at)
+  | IterPr (_, _) -> assert false
   | _ -> [ prem ]
 
 let remove_or_rule rule =
@@ -124,10 +126,11 @@ let remove_block_context def =
 (* Pre-process a premise *)
 let rec preprocess_prem prem =
   match prem.it with
-  | IterPr (prem, iterexp) ->
+  | IterPr ([prem], iterexp) ->
     prem
     |> preprocess_prem
-    |> List.map (fun new_prem -> IterPr (new_prem, iterexp) $ prem.at)
+    |> List.map (fun new_prem -> IterPr ([new_prem], iterexp) $ prem.at)
+  | IterPr (_, _) -> assert false
   | RulePr (id, mixop, exp) ->
     let lhs_rhs_opt = 
       match mixop, exp.it with

spectec/src/il2al/translate.ml

@@ -969,7 +969,8 @@ and translate_prem prem =
     init_lhs_id ();
     translate_letpr exp1 exp2 ids
   | Il.RulePr (id, _, exp) -> translate_rulepr id exp
-  | Il.IterPr (pr, iterexp) -> translate_iterpr pr iterexp
+  | Il.IterPr ([pr], iterexp) -> translate_iterpr pr iterexp
+  | Il.IterPr (_, _) -> assert false
   | Il.NegPr _ -> error at "encountered a negated premise"
 
 

spectec/src/middlend/aliasDemut.ml

@@ -141,7 +141,7 @@ and t_prem' env = function
   | IfPr e -> IfPr (t_exp env e)
   | LetPr (e1, e2, ids) -> LetPr (t_exp env e1, t_exp env e2, ids)
   | ElsePr -> ElsePr
-  | IterPr (prem, iterexp) -> IterPr (t_prem env prem, t_iterexp env iterexp)
+  | IterPr (prems, iterexp) -> IterPr (t_prems env prems, t_iterexp env iterexp)
 
 and t_prem env x = { x with it = t_prem' env x.it }
 

spectec/src/middlend/sideconditions.ml

@@ -27,14 +27,14 @@ let lenE e = match e.it with
 | _ -> LenE e $$ e.at % (NumT `NatT $ e.at)
 
 (* Smart constructor for IterPr that removes dead iter-variables *)
-let iterPr (pr, (iter, vars)) =
-  let frees = free_prem pr in
+let iterPr (prs, (iter, vars)) =
+  let frees = free_list free_prem prs in
   let vars' = List.filter (fun (id, _) ->
     Set.mem id.it frees.varid
   ) vars in
   (* Must keep at least one variable to keep the iteration well-formed *)
   let vars'' = if vars' <> [] then vars' else [List.hd vars] in
-  IterPr (pr, (iter, vars''))
+  IterPr (prs, (iter, vars''))
 
 let is_null e = CmpE (`EqOp, `BoolT, e, OptE None $$ e.at % e.note) $$ e.at % (BoolT $ e.at)
 let iffE e1 e2 = IfPr (BinE (`EquivOp, `BoolT, e1, e2) $$ e1.at % (BoolT $ e1.at)) $ e1.at
@@ -107,7 +107,7 @@ let rec t_exp env e : prem list =
   ->
     t_iterexp env iterexp @
     let env' = env_under_iter env iterexp in
-    List.map (fun pr -> iterPr (pr, iterexp) $ e.at) (t_exp env' e1)
+    List.map (fun pr -> iterPr ([pr], iterexp) $ e.at) (t_exp env' e1)
 
 and t_iterexp env (iter, _) = t_iter env iter
 
@@ -134,11 +134,12 @@ let rec t_prem env prem =
   | IfPr e -> t_exp env e
   | LetPr (e1, e2, _) -> t_exp env e1 @ t_exp env e2
   | ElsePr -> []
-  | IterPr (prem, iterexp)
+  | IterPr ([prem'], iterexp)
   -> iter_side_conditions env iterexp @
      t_iterexp env iterexp @
      let env' = env_under_iter env iterexp in
-     List.map (fun pr -> iterPr (pr, iterexp) $ prem.at) (t_prem env' prem)
+     List.map (fun pr -> iterPr ([pr], iterexp) $ prem'.at) (t_prem env' prem')
+  | IterPr (_, _) -> assert false
   | NegPr _prem' -> 
     (* We do not want to infer anything from NegPr *)
     []
@@ -162,7 +163,8 @@ let is_true prem = match prem.it with
 (* Does prem1 obviously imply prem2? *)
 let rec implies prem1 prem2 = Il.Eq.eq_prem prem1 prem2 ||
   match prem2.it with
-  | IterPr (prem2', _) -> implies prem1 prem2'
+  | IterPr ([prem2'], _) -> implies prem1 prem2'
+  | IterPr (_, _) -> assert false
   | _ -> false
 
 let reduce_prems prems = prems

spectec/src/middlend/sub.ml

@@ -235,7 +235,7 @@ and t_prem' env = function
   | IfPr e -> IfPr (t_exp env e)
   | LetPr (e1, e2, ids) -> LetPr (t_exp env e1, t_exp env e2, ids)
   | ElsePr -> ElsePr
-  | IterPr (prem, iterexp) -> IterPr (t_prem env prem, t_iterexp env iterexp)
+  | IterPr (prems, iterexp) -> IterPr (List.map (t_prem env) prems, t_iterexp env iterexp)
 
 and t_prem env x = { x with it = t_prem' env x.it }
 

spectec/src/middlend/totalize.ml

@@ -165,7 +165,7 @@ and t_prem' env = function
   | IfPr e -> IfPr (t_exp env e)
   | LetPr (e1, e2, ids) -> LetPr (t_exp env e1, t_exp env e2, ids)
   | ElsePr -> ElsePr
-  | IterPr (prem, iterexp) -> IterPr (t_prem env prem, t_iterexp env iterexp)
+  | IterPr (prems, iterexp) -> IterPr (List.map (t_prem env) prems, t_iterexp env iterexp)
   | NegPr prem -> NegPr (t_prem env prem)
 
 and t_prem env x = { x with it = t_prem' env x.it }

spectec/src/middlend/typefamilyremoval.ml

@@ -526,9 +526,9 @@ let rec transform_prem bind_map env prem =
   | IfPr e -> IfPr (transform_exp bind_map env e)
   | LetPr (e1, e2, ids) -> LetPr (transform_exp bind_map env e1, transform_exp bind_map env e2, ids)
   | ElsePr -> ElsePr
-  | IterPr (prem1, (iter, id_exp_pairs)) -> 
+  | IterPr (prems1, (iter, id_exp_pairs)) ->
     let new_bind_map = add_iter_ids_to_map env id_exp_pairs bind_map in
-    IterPr (transform_prem new_bind_map env prem1, 
+    IterPr (List.map (transform_prem new_bind_map env) prems1,
       (transform_iter new_bind_map env iter, List.map (fun (id, exp) -> (id, transform_exp new_bind_map env exp)) id_exp_pairs)
     )
   | NegPr prem1 -> NegPr (transform_prem bind_map env prem1)

spectec/src/middlend/undep.ml

@@ -142,9 +142,9 @@ and collect_userdef_prem iterexps p =
   match p.it with
   | IfPr e | RulePr (_, _, e) -> collect_userdef_exp iterexps e
   | LetPr (e1, e2, _) -> collect_userdef_exp iterexps e1 @ collect_userdef_exp iterexps e2
-  | IterPr (p', ((_, id_exp_pairs) as iterexp)) -> collect_userdef_prem (iterexp :: iterexps) p' @
+  | IterPr (ps, ((_, id_exp_pairs) as iterexp)) -> List.concat_map (collect_userdef_prem (iterexp :: iterexps)) ps @
     List.concat_map (fun (_, exp) -> collect_userdef_exp iterexps exp) id_exp_pairs
-  | _ -> [] 
+  | _ -> []
 
 and collect_userdef_path iterexps p =
   match p.it with
@@ -251,7 +251,7 @@ let rec transform_prem env prem =
   | IfPr e -> IfPr (transform_exp env e)
   | LetPr (e1, e2, ids) -> LetPr (transform_exp env e1, transform_exp env e2, ids)
   | ElsePr -> ElsePr
-  | IterPr (prem1, (iter, id_exp_pairs)) -> IterPr (transform_prem env prem1, 
+  | IterPr (prems1, (iter, id_exp_pairs)) -> IterPr (List.map (transform_prem env) prems1, 
       (transform_iter env iter, List.map (fun (id, exp) -> (id, transform_exp env exp)) id_exp_pairs)
     )
   | NegPr p -> NegPr p
@@ -311,7 +311,7 @@ let rec get_wf_pred env (exp, t) =
       let name = get_id exp' in
       let name' = remove_last_char name.it $ name.at in 
       let prems = get_wf_pred env (VarE name' $$ name.at % typ, typ) in
-      List.map (fun prem -> IterPr (prem, (iter, [(name', exp')])) $ name.at) prems
+      List.map (fun prem -> IterPr ([prem], (iter, [(name', exp')])) $ name.at) prems
     | TupT exp_typ_pairs -> 
       let prems = 
         List.mapi (fun idx (_, typ) -> 
@@ -416,7 +416,7 @@ let get_extra_prems env binds exp prems =
 
   let more_prems = List.concat_map (fun (pair, iterexps) -> 
     List.map (fun prem' -> List.fold_left (fun acc iterexp ->
-      IterPr (acc, iterexp) $ acc.at   
+      IterPr ([acc], iterexp) $ acc.at
     ) prem' iterexps) (get_wf_pred env pair) 
   ) unique_terms in