Refactor IL to AL preprocess

spectec/src/backend-prose/gen.ml

@@ -289,7 +289,7 @@ let rec group_vrules = function
       let same_rules, diff_rules =
         List.partition (fun (_, rule) -> name_of_rule rule = rule_name) t in
       let same_rules = List.map snd same_rules in
-      let group = (rule_name, rel_id, List.map pack_pair_rule (rule :: same_rules |> Il2al.Il2il.unify_rules)) in
+      let group = (rule_name, rel_id, List.map pack_pair_rule (rule :: same_rules |> Il2al.Unify.unify_rules)) in
       group :: group_vrules diff_rules
 
 (* TODO: The codes below are too repetitive. Should be factored. *)
@@ -320,7 +320,7 @@ let prose_of_valid_rules rel_id rules =
 
 let prose_of_valid_rel def =
   match def.it with
-  | Ast.RelD (rel_id, _, _, rules) -> prose_of_valid_rules rel_id (Il2al.Il2il.unify_rules rules)
+  | Ast.RelD (rel_id, _, _, rules) -> prose_of_valid_rules rel_id (Il2al.Unify.unify_rules rules)
   | _ -> assert false
 
 (** 2. C |- instr : type **)
@@ -356,7 +356,7 @@ let prose_of_valid_with_rules rel_id rules =
 
 let prose_of_valid_with_rel def =
   match def.it with
-  | Ast.RelD (rel_id, _, _, rules) -> prose_of_valid_with_rules rel_id (Il2al.Il2il.unify_rules rules)
+  | Ast.RelD (rel_id, _, _, rules) -> prose_of_valid_with_rules rel_id (Il2al.Unify.unify_rules rules)
   | _ -> assert false
 
 (** 4. C |- type <: type **)
@@ -385,7 +385,7 @@ let prose_of_match_rules rel_id rules =
 
 let prose_of_match_rel def =
   match def.it with
-  | Ast.RelD (rel_id, _, _, rules) -> prose_of_match_rules rel_id (Il2al.Il2il.unify_rules rules)
+  | Ast.RelD (rel_id, _, _, rules) -> prose_of_match_rules rel_id (Il2al.Unify.unify_rules rules)
   | _ -> assert false
 
 
@@ -415,7 +415,7 @@ let prose_of_const_rules rel_id rules =
 
 let prose_of_const_rel def =
   match def.it with
-  | Ast.RelD (rel_id, _, _, rules) -> prose_of_const_rules rel_id (Il2al.Il2il.unify_rules rules)
+  | Ast.RelD (rel_id, _, _, rules) -> prose_of_const_rules rel_id (Il2al.Unify.unify_rules rules)
   | _ -> assert false
 
 (** 6. C |- e : e CONST **)
@@ -447,7 +447,7 @@ let prose_of_valid_with2_rules rel_id rules =
 
 let prose_of_valid_with2_rel def =
   match def.it with
-  | Ast.RelD (rel_id, _, _, rules) -> prose_of_valid_with2_rules rel_id (Il2al.Il2il.unify_rules rules)
+  | Ast.RelD (rel_id, _, _, rules) -> prose_of_valid_with2_rules rel_id (Il2al.Unify.unify_rules rules)
   | _ -> assert false
 
 (** 8. Others **)

spectec/src/il2al/def.ml

@@ -0,0 +1,10 @@
+open Il.Ast
+open Util.Source
+
+type partial = Partial | Total
+type helper_clause = clause
+type helper_def' = id * helper_clause list * partial
+type helper_def = helper_def' phrase
+type rule_clause = exp * exp * (prem list)
+type rule_def' = string * id * rule_clause list
+type rule_def = rule_def' phrase

spectec/src/il2al/dune

@@ -3,12 +3,14 @@
   (libraries middlend util il al)
   (modules
     animate
-    il2il
+    unify
     manual
     translate
     transpile
     free
     preprocess
     encode
+    def
+    il2al_util
   )
 )

spectec/src/il2al/il2al_util.ml

@@ -0,0 +1,94 @@
+open Il.Ast
+open Def
+open Util
+open Source
+
+let error at msg = Error.error at "prose translation" msg
+
+let name_of_rule rule =
+  match rule.it with
+  | RuleD (id, _, _, _, _) ->
+    String.split_on_char '-' id.it |> List.hd
+
+let lhs_of_prem pr =
+  match pr.it with
+  | LetPr (lhs, _, _) -> lhs
+  | _ -> error pr.at "expected a LetPr"
+let rhs_of_prem pr =
+  match pr.it with
+  | LetPr (_, rhs, _) -> rhs
+  | _ -> error pr.at "expected a LetPr"
+let replace_lhs lhs pr =
+  let open Il.Free in
+  match pr.it with
+  | LetPr (lhs', rhs, _) ->
+    if Il.Eq.eq_exp lhs lhs' then
+      pr
+    else
+      { pr with it = LetPr (lhs, rhs, (free_exp lhs).varid |> Set.elements) }
+  | _ -> error pr.at "expected a LetPr"
+
+let case_of_case e =
+  match e.it with
+  | CaseE (mixop, _) -> mixop
+  | _ -> error e.at
+    (Printf.sprintf "cannot get case of case expression `%s`" (Il.Print.string_of_exp e))
+
+let is_let_prem_with_rhs_type t prem =
+  match prem.it with
+  | LetPr (_, e, _) ->
+    (match e.note.it with
+    | VarT (id, []) -> id.it = t
+    | _ -> false
+    )
+  | _ -> false
+let is_pop : prem -> bool = is_let_prem_with_rhs_type "stackT"
+let is_ctxt_prem : prem -> bool = is_let_prem_with_rhs_type "contextT"
+
+let extract_context r =
+  let _, _, prems = r in
+  prems
+  |> List.find_opt is_ctxt_prem
+  |> Option.map lhs_of_prem (* TODO: Collect helper functions into one place *)
+
+let extract_pops rgroup =
+  (* Helpers *)
+  let rec extract_pops' acc prems premss =
+    match prems with
+    | hd :: tl when is_pop hd ->
+      let partitions = List.map (List.partition (Il.Eq.eq_prem hd)) premss in
+      let fsts = List.map fst partitions in
+      let snds = List.map snd partitions in
+
+      if List.for_all (fun l -> List.length l = 1) fsts then
+        extract_pops' (hd :: acc) tl snds
+      else
+        List.rev acc, prems :: premss
+    | _ -> List.rev acc, prems :: premss
+  in
+
+  let get_prems r = let _, _, prems = r in prems in
+  let set_prems r prems =
+    let lhs, rhs, _ = r in
+    lhs, rhs, prems
+  in
+  (* End of helpers *)
+
+  let hd = List.hd rgroup in
+  let tl = List.tl rgroup in
+
+  let extracted, new_premss = extract_pops' [] (get_prems hd) (List.map get_prems tl) in
+  extracted, List.map2 set_prems rgroup new_premss
+
+let rec add eq k v = function (* add a (k,v) to an assoc list *)
+  | [] -> [(k, [v])]
+  | (k', vs) :: tl ->
+    if eq k k' then
+      (k', vs @ [v]) :: tl
+    else
+      (k', vs) :: add eq k v tl
+
+let group_by_context (rs: rule_clause list): ('a option * rule_clause list) list =
+  let eq_context = Option.equal (fun c1 c2 -> Il.Mixop.eq (case_of_case c1) (case_of_case c2)) in
+  List.fold_left (fun acc r -> add eq_context (extract_context r) r acc) [] rs
+

spectec/src/il2al/preprocess.ml

@@ -2,6 +2,8 @@ open Il
 open Ast
 open Util.Source
 open El.Atom
+open Def
+open Il2al_util
 
 
 (* Remove or *)
@@ -156,19 +158,57 @@ let preprocess_clause (clause: clause) : clause =
   let DefD (binds, args, exp, prems) = clause.it in
   DefD (binds, args, exp, List.concat_map preprocess_prem prems) $ clause.at
 
-let rec preprocess_def (def: def) : def =
+let preprocess_def (def: def) : def =
   let def' =
     def
     |> remove_or
     |> remove_block_context
   in
 
   match def'.it with
-  | RelD (id, mixop, typ, rules) ->
-    RelD (id, mixop, typ, List.map preprocess_rule rules) $ def.at
-  | DecD (id, params, typ, clauses) ->
-    DecD (id, params, typ, List.map preprocess_clause clauses) $ def.at
-  | RecD defs -> RecD (List.map preprocess_def defs) $ def.at
-  | _ -> def
+  | TypD (id, ps, insts) ->
+    Al.Valid.env := Env.bind_typ !Al.Valid.env id (ps, insts); def'
+  | RelD (id, mixop, t, rules) ->
+    Al.Valid.env := Env.bind_rel !Al.Valid.env id (mixop, t, rules);
+    RelD (id, mixop, t, List.map preprocess_rule rules) $ def.at
+  | DecD (id, ps, t, clauses) ->
+    Al.Valid.env := Env.bind_def !Al.Valid.env id (ps, t, clauses);
+    DecD (id, ps, t, List.map preprocess_clause clauses) $ def.at
+  | GramD (id, ps, t, prods) ->
+    Al.Valid.env := Env.bind_gram !Al.Valid.env id (ps, t, prods); def'
+  | RecD _ -> assert (false);
+  | HintD _ -> def'
+
+let flatten_rec def =
+  match def.it with
+  | RecD defs -> defs
+  | _ -> [ def ]
+
+
+let preprocess (il: script) : rule_def list * helper_def list =
+
+  let not_translate = ["typing.watsup"] in
+  let is_al_target def =
+    let f = fun name -> String.ends_with ~suffix:name def.at.left.file in
+    match def.it with
+    | _ when List.exists f not_translate -> None
+    | DecD (id, _, _, _) when id.it = "utf8" -> None
+    | RelD (id, mixop, t, rules) when List.mem id.it [ "Step"; "Step_read"; "Step_pure" ] ->
+      (* HARDCODE: Exclude administrative rules *)
+      let filter_rule rule =
+        ["pure"; "read"; "trap"; "ctxt"]
+        |> List.mem (name_of_rule rule)
+        |> not
+      in
+      Some (RelD (id, mixop, t, List.filter filter_rule rules) $ def.at)
+    | RelD _ -> None
+    | _ -> Some def
+  in
 
-let preprocess: script -> script = List.map preprocess_def
+  il
+  |> List.concat_map flatten_rec
+  |> List.filter_map is_al_target
+  |> List.map preprocess_def
+  |> Encode.transform
+  |> Animate.transform
+  |> Unify.unify

spectec/src/il2al/preprocess.mli

@@ -1,3 +1,4 @@
 open Il.Ast
+open Def
 
-val preprocess: script -> script
+val preprocess: script -> rule_def list * helper_def list