diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/main.ml | 3 | ||||
| -rw-r--r-- | src/type_internal.ml | 10 | ||||
| -rw-r--r-- | src/type_internal.mli | 2 |
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 |