Add mli files under il2al

spectec/src/il2al/il2il.ml

@@ -6,14 +6,18 @@ open Il.Ast
 open Il.Eq
 open Util.Source
 
+type reduction_group = (exp * exp * (premise list)) list
+
 (** Helpers **)
+
 let take_prefix n str =
   if String.length str < n then
     str
   else
     String.sub str 0 n
 
 (** Walker-based transformer **)
+
 let rec transform_expr f e =
   let new_ = transform_expr f in
   { e with it = match (f e).it with

spectec/src/il2al/il2il.mli

@@ -0,0 +1,9 @@
+open Il.Ast
+
+type reduction_group = (exp * exp * (premise list)) list
+
+val transform_expr : (exp -> exp) -> exp -> exp
+val is_unified_id : string -> bool
+
+val unify_lhs : string * reduction_group -> string * reduction_group
+val unify_defs : clause list -> clause list

spectec/src/il2al/translate.ml

@@ -961,7 +961,6 @@ let translate_helpers il =
 
 (** Translating reduction rules **)
 let translate_rules il =
-
   (* Extract rules *)
   List.concat_map extract_rules il
   (* Group rules that have the same names *)
@@ -981,4 +980,4 @@ let translate il =
 
   (* Transpile *)
   (* Can be turned off *)
-  List.map Transpile.state_remover algos
+  List.map Transpile.remove_state algos

spectec/src/il2al/translate.mli

@@ -0,0 +1,6 @@
+val name_of_rule : Il.Ast.rule -> string
+val name2kwd : string -> Il.Ast.typ -> string * string
+val get_params : Il.Ast.exp -> Il.Ast.exp list
+val exp2expr : Il.Ast.exp -> Al.Ast.expr
+val exp2args : Il.Ast.exp -> Al.Ast.expr list
+val translate : Il.Ast.script -> Al.Ast.algorithm list

spectec/src/il2al/transpile.ml

@@ -95,17 +95,6 @@ let unify_tail l1 l2 =
 let intersect_list xs ys = List.filter (fun x -> List.mem x ys) xs
 let diff_list xs ys = Lib.List.filter_not (fun x -> List.mem x ys) xs
 
-let dedup l =
-  let rec aux acc = function
-    | [] -> List.rev acc
-    | x :: xs ->
-      if List.mem x acc then
-        aux acc xs
-      else
-        aux (x :: acc) xs
-  in
-  aux [] l
-
 (** AL -> AL transpilers *)
 
 (* Recursively append else block to every empty if *)
@@ -485,7 +474,7 @@ let hide_state instr =
     [ replaceI (mk_access hs f, t, e) ~at:at ]
   | _ -> [ instr ]
 
-let state_remover algo =
+let remove_state algo =
   let walk_config =
       {
         Walk.default_config with

spectec/src/il2al/transpile.mli

@@ -0,0 +1,9 @@
+open Al.Ast
+
+val merge : instr list -> instr list -> instr list
+val push_either :instr -> instr list
+val simplify_record_concat : expr -> expr
+val enhance_readability : instr list -> instr list
+val remove_state : algorithm -> algorithm
+val infer_assert : instr list -> instr list
+val enforce_return :  instr list -> instr list