Add -skip_constraints to type-check without constraints

3 files changed, 13 insertions, 2 deletions

diff --git a/src/main.ml b/src/main.ml
index 639da7d7..b0957f91 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -372,6 +372,9 @@ let options = Arg.align ([
   ( "-lem_ast",
     Arg.Unit (fun b -> opt_print_lem := true),
     " pretty-print a Lem AST representation of the file");
+  ( "-skip_constraints",
+    Arg.Clear Type_internal.do_resolve_constraints,
+    " skip constraint resolution in type-checking");
   ( "-v",
     Arg.Unit (fun b -> opt_print_version := true),
     " print version");
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 08ba4c88..e4e3b1bd 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1008,9 +1008,15 @@ let rec simple_constraint_check cs =
       | _,_ -> LtEq(l,n1',n2')::(simple_constraint_check cs))
   | x::cs -> x::(simple_constraint_check cs)
     
+let do_resolve_constraints = ref true
+
 let resolve_constraints cs = 
-  let complex_constraints = simple_constraint_check cs in
-  complex_constraints (*cs*)
+  if not !do_resolve_constraints
+  then cs
+  else begin
+    let complex_constraints = simple_constraint_check cs in
+    complex_constraints (*cs*)
+  end
 
 
 let check_tannot l annot constraints efs = 
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 71b72856..fb10f83f 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -122,6 +122,8 @@ val get_index : nexp -> int (*TEMPORARILY expose nindex through this for debuggi
 
 (*May raise an exception if a contradiction is found*)
 val resolve_constraints : nexp_range list -> nexp_range list
+(* whether to actually perform constraint resolution or not *)
+val do_resolve_constraints : bool ref
 
 (*May raise an exception if effects do not match tannot effects, will lift unification variables to fresh type variables *)
 val check_tannot : Parse_ast.l -> tannot -> nexp_range list -> effect -> tannot