Print error message on cyclic binding

spectec/src/il2al/animate.ml

@@ -261,24 +261,31 @@ let animate_prems known_vars prems =
   let is_other = function {it = ElsePr; _} -> true | _ -> false in
   let (other, non_other) = List.partition is_other pp_prems in
   let rows, cols = build_matrix non_other known_vars in
+
+  (* 1. Run knuth *)
   best := (List.length cols + 1, []);
-  let candidates = match knuth rows cols [] with
-    | [] -> [ snd !best ]
-    | xs -> List.map List.rev xs in
+  let (candidates, k_fail) =
+    match knuth rows cols [] with
+    | [] -> [ snd !best ], true
+    | xs -> List.map List.rev xs, false
+  in
+
+  (* 2. Reorder *)
   let best' = ref (-1, []) in
   match List.find_map (fun cand -> select_tight cand other known_vars best') candidates with
-  | None -> snd !best'
+  | None ->
+    if (not k_fail) then
+      let unhandled_prems = Lib.List.drop (fst !best') (snd !best') in
+      Error.error (over_region (List.map at unhandled_prems)) "prose translation" "There might be a cyclic binding"
+    else
+      snd !best'
   | Some x -> x
 
 (* Animate rule *)
 let animate_rule r = match r.it with
   | RuleD(id, _ , _, _, _) when id.it = "pure" || id.it = "read" -> r (* TODO: remove this line *)
   | RuleD(id, binds, mixop, args, prems) -> (
     match (mixop, args.it) with
-    (* c |- e : t *)
-    | ([ [] ; [{it = Turnstile; _}] ; [{it = Colon; _}] ; []] , TupE ([c; e; _t])) ->
-      let new_prems = animate_prems (union (free_exp false c) (free_exp false e)) prems in
-      RuleD(id, binds, mixop, args, new_prems) $ r.at
     (* lhs ~> rhs *)
     | ([ [] ; [{it = SqArrow; _}] ; []] , TupE ([lhs; _rhs])) ->
       let new_prems = animate_prems (free_exp true lhs) prems in

spectec/src/il2al/il2il.ml

@@ -210,8 +210,8 @@ let rec collect_unified template e = if eq_exp template e then [], [] else
     | VarE id, _
     | IterE ({ it = VarE id; _}, _) , _
       when is_unified_id id.it ->
-      [ IfPr (CmpE (EqOp, template, e) $$ no_region % (BoolT $ no_region)) $ no_region ],
-      [ ExpB (id, template.note, []) $ no_region ]
+      [ IfPr (CmpE (EqOp, template, e) $$ e.at % (BoolT $ e.at)) $ e.at ],
+      [ ExpB (id, template.note, []) $ e.at ]
     | UnE (_, e1), UnE (_, e2)
     | DotE (e1, _), DotE (e2, _)
     | LenE e1, LenE e2
@@ -276,12 +276,11 @@ let unify_rules rules =
 
 
 (** 2. Reduction rules **)
-
 let apply_template_to_rgroup template (lhs, rhs, prems) =
   let new_prems, _ = collect_unified template lhs in
   (* TODO: Remove this depedency on animation. Perhaps this should be moved as a middle end before animation path *)
-  let animated_prems = Animate.animate_prems (Il.Free.free_exp template) (new_prems @ prems) in
-  template, rhs, prioritize_else animated_prems
+  let animated_prems = Animate.animate_prems (Il.Free.free_exp template) new_prems in
+  template, rhs, prioritize_else (animated_prems @ prems)
 
 let unify_lhs' rgroup =
   init_unified_idx();