diff options
| author | Alasdair Armstrong | 2017-08-04 18:45:46 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-08-04 18:45:46 +0100 |
| commit | 6a68833bbd28044feeb3f2863021e4f5d6dbd951 (patch) | |
| tree | 87ce90e0468dcf095c10d3638e337c0aace1eab9 /src | |
| parent | 0e27492d76cf5ac1abdde6a45a4c05652ba74c2a (diff) | |
Various improvements for ASL generation
Fixed a bug where existential constraint's weren't used to solve function quantifiers correctly
Diffstat (limited to 'src')
| -rw-r--r-- | src/reporting_basic.ml | 5 | ||||
| -rw-r--r-- | src/reporting_basic.mli | 1 | ||||
| -rw-r--r-- | src/type_check.ml | 8 |
3 files changed, 9 insertions, 5 deletions
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml index 5ff43208..69c5c084 100644 --- a/src/reporting_basic.ml +++ b/src/reporting_basic.ml @@ -220,5 +220,6 @@ let report_error e = let (m1, verb_pos, pos_l, m2) = dest_err e in (print_err_internal verb_pos false pos_l m1 m2; exit 1) - - +let print_error e = + let (m1, verb_pos, pos_l, m2) = dest_err e in + print_err_internal verb_pos false pos_l m1 m2 diff --git a/src/reporting_basic.mli b/src/reporting_basic.mli index 559be9d4..3d1cbe13 100644 --- a/src/reporting_basic.mli +++ b/src/reporting_basic.mli @@ -104,3 +104,4 @@ val err_typ_dual : Parse_ast.l -> Parse_ast.l -> string -> exn raising a [Fatal_error] exception is recommended. *) val report_error : error -> 'a +val print_error : error -> unit diff --git a/src/type_check.ml b/src/type_check.ml index 5e7febaa..bf907e41 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -559,7 +559,7 @@ end = struct | Typ_arg_effect _ -> () (* Check: is this ever used? *) and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l)) = match nexp_aux with - | Nexp_id _ -> typ_error l "Unimplemented: Nexp_id" + | Nexp_id _ -> () | Nexp_var kid when KidSet.mem kid exs -> () | Nexp_var kid -> begin @@ -1652,6 +1652,8 @@ let rec assert_constraint (E_aux (exp_aux, l)) = nc_and (assert_constraint x) (assert_constraint y) | E_app_infix (x, op, y) when string_of_id op = "==" -> nc_eq (assert_nexp x) (assert_nexp y) + | E_app_infix (x, op, y) when string_of_id op = ">=" -> + nc_gteq (assert_nexp x) (assert_nexp y) | _ -> nc_true type flow_constraint = @@ -2455,7 +2457,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = | [] -> [] | (x :: xs) -> (n, x) :: number (n + 1) xs in - let solve_quant = function + let solve_quant env = function | QI_aux (QI_id _, _) -> false | QI_aux (QI_const nc, _) -> prove env nc in @@ -2464,7 +2466,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = | (utyps, []), (uargs, []) -> begin typ_debug ("Got unresolved args: " ^ string_of_list ", " (fun (_, exp) -> string_of_exp exp) uargs); - if List.for_all solve_quant quants + if List.for_all (solve_quant env) quants then let iuargs = List.map2 (fun utyp (n, uarg) -> (n, crule check_exp env uarg utyp)) utyps uargs in (iuargs, ret_typ, env) |