Deftorel pass

spectec/src/exe-spectec/main.ml

@@ -27,6 +27,7 @@ type pass =
   | AliasDemut
   | ImproveIds
   | Ite
+  | DefToRel
 
 (* This list declares the intended order of passes.
 
@@ -42,9 +43,10 @@ let all_passes = [
   Totalize;
   Else;
   Uncaseremoval;
-  Sideconditions;
   SubExpansion;
   Sub;
+  DefToRel;
+  Sideconditions;
   AliasDemut;
   ImproveIds
 ]
@@ -112,6 +114,7 @@ let pass_flag = function
   | Uncaseremoval -> "uncase-removal"
   | ImproveIds -> "improve-ids"
   | Ite -> "ite"
+  | DefToRel -> "definition-to-relation"
 
 let pass_desc = function
   | Sub -> "Synthesize explicit subtype coercions"
@@ -126,6 +129,7 @@ let pass_desc = function
   | AliasDemut -> "Lifts type aliases out of mutual groups"
   | ImproveIds -> "Disambiguates ids used from each other"
   | Ite -> "If-then-else introduction"
+  | DefToRel -> "Transform specific function definitions into relations"
 
 
 let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function
@@ -141,6 +145,7 @@ let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function
   | AliasDemut -> Middlend.AliasDemut.transform
   | ImproveIds -> Middlend.Improveids.transform
   | Ite -> Middlend.Ite.transform
+  | DefToRel -> Middlend.Deftorel.transform
 
 
 (* Argument parsing *)

spectec/src/il/iter.ml

@@ -19,6 +19,7 @@ sig
   val visit_typ : typ -> unit
   val visit_deftyp : deftyp -> unit
   val visit_exp : exp -> unit
+  val visit_arg : arg -> unit
   val visit_path : path -> unit
   val visit_sym : sym -> unit
   val visit_prem : prem -> unit
@@ -46,6 +47,7 @@ struct
   let visit_typ _ = ()
   let visit_deftyp _ = ()
   let visit_exp _ = ()
+  let visit_arg _ = ()
   let visit_path _ = ()
   let visit_sym _ = ()
   let visit_prem _ = ()
@@ -219,6 +221,7 @@ and prems prs = list prem prs
 (* Definitions *)
 
 and arg a =
+  visit_arg a;
   match a.it with
   | ExpA e -> exp e
   | TypA t -> typ t