diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/constraint.ml | 82 | ||||
| -rw-r--r-- | src/constraint.mli | 9 | ||||
| -rw-r--r-- | src/initial_check.ml | 2 | ||||
| -rw-r--r-- | src/parser2.mly | 7 | ||||
| -rw-r--r-- | src/pretty_print_sail2.ml | 139 | ||||
| -rw-r--r-- | src/process_file.ml | 23 | ||||
| -rw-r--r-- | src/reporting_basic.ml | 18 | ||||
| -rw-r--r-- | src/sail.ml | 8 | ||||
| -rw-r--r-- | src/type_check.ml | 12 |
9 files changed, 223 insertions, 77 deletions
diff --git a/src/constraint.ml b/src/constraint.ml index e8252f2a..37d1fae9 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -212,7 +212,44 @@ let smtlib_of_constraint constr : string = type t = nexp constraint_bool -type smt_result = Unknown of t list | Unsat of t +type smt_result = Unknown | Sat | Unsat + +module DigestMap = Map.Make(Digest) + +let known_problems = ref (DigestMap.empty) + +let load_digests_err () = + let in_chan = open_in_bin "z3_problems" in + let rec load () = + let digest = Digest.input in_chan in + let result = input_byte in_chan in + begin + match result with + | 0 -> known_problems := DigestMap.add digest Unknown !known_problems + | 1 -> known_problems := DigestMap.add digest Sat !known_problems + | 2 -> known_problems := DigestMap.add digest Unsat !known_problems + | _ -> assert false + end; + load () + in + try load () with + | End_of_file -> close_in in_chan + +let load_digests () = + try load_digests_err () with + | Sys_error _ -> () + +let save_digests () = + let out_chan = open_out_bin "z3_problems" in + let output digest result = + Digest.output out_chan digest; + match result with + | Unknown -> output_byte out_chan 0 + | Sat -> output_byte out_chan 1 + | Unsat -> output_byte out_chan 2 + in + DigestMap.iter output !known_problems; + close_out out_chan let rec call_z3 constraints : smt_result = let problems = unbranch constraints in @@ -235,24 +272,31 @@ let rec call_z3 constraints : smt_result = end in - begin - let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in - output_string tmp_chan z3_file; - close_out tmp_chan; - let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in - let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in - let _ = Unix.close_process_in z3_chan in - Sys.remove input_file; - try - let (problem, _) = List.find (fun (_, result) -> result = "unsat") z3_output in - Unsat problem - with - | Not_found -> - z3_output - |> List.filter (fun (_, result) -> result = "unknown") - |> List.map fst - |> (fun unsolved -> Unknown unsolved) - end + let digest = Digest.string z3_file in + try + let result = DigestMap.find digest !known_problems in + result + with + | Not_found -> + begin + let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in + output_string tmp_chan z3_file; + close_out tmp_chan; + let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in + let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in + let _ = Unix.close_process_in z3_chan in + Sys.remove input_file; + try + let (problem, _) = List.find (fun (_, result) -> result = "unsat") z3_output in + known_problems := DigestMap.add digest Unsat !known_problems; + Unsat + with + | Not_found -> + let unsolved = List.filter (fun (_, result) -> result = "unknown") z3_output in + if unsolved == [] + then (known_problems := DigestMap.add digest Sat !known_problems; Sat) + else (known_problems := DigestMap.add digest Unknown !known_problems; Unknown) + end let string_of constr = constr diff --git a/src/constraint.mli b/src/constraint.mli index 3fb3d2f6..ad75f453 100644 --- a/src/constraint.mli +++ b/src/constraint.mli @@ -1,12 +1,15 @@ type nexp type t -type smt_result = Unknown of t list | Unsat of t - +type smt_result = Unknown | Sat | Unsat + +val load_digests : unit -> unit +val save_digests : unit -> unit + val call_z3 : t -> smt_result val string_of : t -> string - + val implies : t -> t -> t val conj : t -> t -> t val disj : t -> t -> t diff --git a/src/initial_check.ml b/src/initial_check.ml index b7505391..efda0da1 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -958,6 +958,8 @@ let generate_undefineds vs_ids (Defs defs) = gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}"; gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}"; gen_vs (mk_id "undefined_int") "unit -> int effect {undef}"; + gen_vs (mk_id "undefined_nat") "unit -> nat effect {undef}"; + gen_vs (mk_id "undefined_real") "unit -> real effect {undef}"; gen_vs (mk_id "undefined_string") "unit -> string effect {undef}"; gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}"; (* FIXME: How to handle inc/dec order correctly? *) diff --git a/src/parser2.mly b/src/parser2.mly index 16e93a59..59db84a1 100644 --- a/src/parser2.mly +++ b/src/parser2.mly @@ -46,9 +46,9 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *) open Parse_ast -let loc n m = Range (m, n) +let loc n m = Range (n, m) -let mk_id i n m = Id_aux (i, loc m n) +let mk_id i n m = Id_aux (i, loc n m) let mk_kid str n m = Kid_aux (Var str, loc n m) let id_of_kid = function @@ -434,16 +434,19 @@ typ8: | typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } | typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos } + | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos} | typ9 { $1 } typ8l: | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } | typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos } + | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos} | typ9 { $1 } typ8r: | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } | typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos } + | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos} | typ9 { $1 } typ9: diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml index d9bc0c7c..bb7aa3b4 100644 --- a/src/pretty_print_sail2.ml +++ b/src/pretty_print_sail2.ml @@ -19,24 +19,56 @@ let doc_ord (Ord_aux(o,_)) = match o with | Ord_inc -> string "inc" | Ord_dec -> string "dec" -let rec doc_nexp (Nexp_aux (n_aux, _)) = - match n_aux with - | Nexp_constant c -> string (string_of_int c) - | Nexp_id id -> doc_id id - | Nexp_var kid -> doc_kid kid - | _ -> string "NEXP" +let rec doc_nexp = + let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) = + match n_aux with + | Nexp_constant c -> string (string_of_int c) + | Nexp_id id -> doc_id id + | Nexp_var kid -> doc_kid kid + | _ -> parens (nexp0 nexp) + and nexp0 (Nexp_aux (n_aux, _) as nexp) = + match n_aux with + | Nexp_sum (n1, Nexp_aux (Nexp_neg n2, _)) | Nexp_minus (n1, n2) -> + separate space [nexp0 n1; string "-"; nexp1 n2] + | Nexp_sum (n1, Nexp_aux (Nexp_constant c, _)) when c < 0 -> + separate space [nexp0 n1; string "-"; doc_int (abs c)] + | Nexp_sum (n1, n2) -> separate space [nexp0 n1; string "+"; nexp1 n2] + | _ -> nexp1 nexp + and nexp1 (Nexp_aux (n_aux, _) as nexp) = + match n_aux with + | Nexp_times (n1, n2) -> separate space [nexp1 n1; string "*"; nexp2 n2] + | _ -> nexp2 nexp + and nexp2 (Nexp_aux (n_aux, _) as nexp) = + match n_aux with + | Nexp_neg n -> separate space [string "-"; atomic_nexp n] + | Nexp_exp n -> separate space [string "2"; string "^"; atomic_nexp n] + | _ -> atomic_nexp nexp + in + nexp0 let doc_nc = + let nc_op op n1 n2 = separate space [doc_nexp n1; string op; doc_nexp n2] in let rec atomic_nc (NC_aux (nc_aux, _) as nc) = match nc_aux with | NC_true -> string "true" | NC_false -> string "false" + | NC_equal (n1, n2) -> nc_op "=" n1 n2 + | NC_not_equal (n1, n2) -> nc_op "!=" n1 n2 + | NC_bounded_ge (n1, n2) -> nc_op ">=" n1 n2 + | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2 | NC_set (kid, ints) -> separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)] | _ -> parens (nc0 nc) - and nc0 (NC_aux (nc_aux, _)) = string "NC0" + and nc0 (NC_aux (nc_aux, _) as nc) = + match nc_aux with + | NC_or (c1, c2) -> separate space [nc0 c1; string "|"; nc1 c2] + | _ -> nc1 nc + and nc1 (NC_aux (nc_aux, _) as nc) = + match nc_aux with + | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2] + | _ -> atomic_nc nc in - atomic_nc + nc0 let rec doc_typ (Typ_aux (typ_aux, _)) = match typ_aux with @@ -49,8 +81,8 @@ let rec doc_typ (Typ_aux (typ_aux, _)) = | Typ_var kid -> doc_kid kid | Typ_wild -> assert false (* Resugar set types like {|1, 2, 3|} *) - | Typ_exist ([kid1], NC_aux (NC_set (kid2, ints), _), Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_var kid3, _)), _)]), _)) - when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 -> + | Typ_exist ([kid1], NC_aux (NC_set (kid2, ints), _), Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _)) + when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 && Id.compare (mk_id "atom") id == 0 -> enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints) | Typ_exist (kids, nc, typ) -> braces (separate_map space doc_kid kids ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ) @@ -62,14 +94,42 @@ and doc_typ_arg (Typ_arg_aux (ta_aux, _)) = | Typ_arg_nexp nexp -> doc_nexp nexp | Typ_arg_order o -> doc_ord o +let doc_quants quants = + let doc_qi_kopt (QI_aux (qi_aux, _)) = + match qi_aux with + | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid] + | QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])] + | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])] + | QI_id kopt when is_order_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])] + | QI_const nc -> [] + in + let qi_nc (QI_aux (qi_aux, _)) = + match qi_aux with + | QI_const nc -> [nc] + | _ -> [] + in + let kdoc = separate space (List.concat (List.map doc_qi_kopt quants)) in + let ncs = List.concat (List.map qi_nc quants) in + match ncs with + | [] -> kdoc + | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc + | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs) + let doc_typschm (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = match tq_aux with | TypQ_no_forall -> doc_typ typ | TypQ_tq [] -> doc_typ typ - | TypQ_tq qs -> string "QI" ^^ dot ^^ space ^^ doc_typ typ + | TypQ_tq qs -> + string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ typ let doc_typschm_typ (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = doc_typ typ +let doc_typschm_quants (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = + match tq_aux with + | TypQ_no_forall -> None + | TypQ_tq [] -> None + | TypQ_tq qs -> Some (doc_quants qs) + let doc_lit (L_aux(l,_)) = utf8string (match l with | L_unit -> "()" @@ -111,26 +171,27 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = | E_app (id, [E_aux (E_lit (L_aux (L_unit, _)), _)]) -> doc_id id ^^ string "()" | E_app (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps) | E_app_infix (x, id, y) -> doc_op (doc_id id) (doc_exp x) (doc_exp y) - | E_tuple exps -> assert false - | E_if (if_exp, then_exp, else_exp) -> assert false - | E_for (id, exp1, exp2, exp3, order, exp4) -> assert false - | E_vector exps -> assert false - | E_vector_access (exp1, exp2) -> assert false + | E_tuple exps -> parens (separate_map (comma ^^ space) doc_exp exps) + | E_if (if_exp, then_exp, else_exp) -> string "E_if" + | E_for (id, exp1, exp2, exp3, order, exp4) -> string "E_for" + | E_vector exps -> string "E_vector" + | E_vector_access (exp1, exp2) -> string "E_vector_access" | E_vector_subrange (exp1, exp2, exp3) -> doc_exp exp1 ^^ brackets (separate space [doc_exp exp2; string ".."; doc_exp exp3]) - | E_vector_update (exp1, exp2, exp3) -> assert false - | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> assert false - | E_list exps -> assert false - | E_cons (exp1, exp2) -> assert false - | E_record fexps -> assert false - | E_record_update (exp, fexps) -> assert false - | E_field (exp, id) -> assert false + | E_vector_update (exp1, exp2, exp3) -> string "E_vector_update" + | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> string "E_vector_update_subrange" + | E_list exps -> string "E_list" + | E_cons (exp1, exp2) -> string "E_cons" + | E_record fexps -> string "E_record" + | E_record_update (exp, fexps) -> string "E_record_update" + | E_field (exp, id) -> string "E_field" | E_case (exp, pexps) -> separate space [string "match"; doc_exp exp; doc_pexps pexps] | E_let (LB_aux (LB_val (pat, binding), _), exp) -> separate space [string "let"; doc_pat pat; equals; doc_exp binding; string "in"; doc_exp exp] | E_assign (lexp, exp) -> separate space [doc_lexp lexp; equals; doc_exp exp] - | E_sizeof nexp -> assert false + | E_sizeof (Nexp_aux (Nexp_var kid, _)) -> doc_kid kid + | E_sizeof nexp -> string "sizeof" ^^ parens (doc_nexp nexp) | E_constraint nc -> string "constraint" ^^ parens (doc_nc nc) | E_exit exp -> assert false (* Resugar an assert with an empty message *) @@ -138,7 +199,7 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = | E_assert (exp1, exp2) -> string "assert" ^^ parens (doc_exp exp1 ^^ comma ^^ space ^^ doc_exp exp2) | E_throw exp -> assert false | E_try (exp, pexps) -> assert false - | E_return exp -> assert false + | E_return exp -> string "return" ^^ parens (doc_exp exp) and doc_block = function | [] -> assert false | [E_aux (E_let (LB_aux (LB_val (pat, binding), _), E_aux (E_block exps, _)), _)] -> @@ -187,13 +248,29 @@ let doc_dec (DEC_aux (reg,_)) = let doc_typdef (TD_aux(td,_)) = match td with | TD_abbrev(id, _, typschm) -> - doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm) + begin + match doc_typschm_quants typschm with + | Some qdoc -> + doc_op equals (concat [string "type"; space; doc_id id; space; qdoc]) (doc_typschm_typ typschm) + | None -> + doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm) + end | _ -> string "TYPEDEF" -let doc_spec (VS_aux(v,_)) = match v with - | VS_val_spec(ts,id,_,_) -> - separate space [string "val"; doc_id id; colon; doc_typschm ts] - | _ -> string "VS?" +let doc_spec (VS_aux(v,_)) = + let doc_extern = function + | Some s -> equals ^^ space ^^ utf8string ("\"" ^ String.escaped s ^ "\"") ^^ space + | None -> empty + in + match v with + | VS_val_spec(ts,id,ext,is_cast) -> + string "val" ^^ space + ^^ (if is_cast then (string "cast" ^^ space) else empty) + ^^ doc_id id ^^ space + ^^ doc_extern ext + ^^ colon ^^ space + ^^ doc_typschm ts + (* | VS_cast_spec (ts, id) -> separate space [string "val"; string "cast"; doc_typscm ts; doc_id id] @@ -212,7 +289,7 @@ let rec doc_def def = group (match def with | DEF_reg_dec dec -> doc_dec dec | DEF_scattered sdef -> string "TOPLEVEL" | DEF_overload (id, ids) -> - string "TOPLEVEL" + separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (semi ^^ break 1) doc_id ids) rbrace] | DEF_comm (DC_comm s) -> string "TOPLEVEL" | DEF_comm (DC_comm_struct d) -> string "TOPLEVEL" ) ^^ hardline diff --git a/src/process_file.ml b/src/process_file.ml index 0f789c9d..1749bc03 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -82,13 +82,16 @@ let parse_file (f : string) : Parse_ast.defs = in close_in in_chan; ast with - | Parsing.Parse_error -> - let pos = Lexing.lexeme_start_p lexbuf in - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main"))) - | Parse_ast.Parse_error_locn(l,m) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))) - | Lexer.LexError(s,p) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) + | Parser2.Error -> + let pos = Lexing.lexeme_start_p lexbuf in + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "no information"))) + | Parsing.Parse_error -> + let pos = Lexing.lexeme_start_p lexbuf in + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main"))) + | Parse_ast.Parse_error_locn(l,m) -> + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))) + | Lexer.LexError(s,p) -> + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) let convert_ast (order : Ast.order) (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast order defs @@ -237,7 +240,11 @@ let rewrite_step defs rewriter = | _ -> () in defs -let rewrite rewriters defs = List.fold_left rewrite_step defs rewriters +let rewrite rewriters defs = + try List.fold_left rewrite_step defs rewriters with + | Type_check.Type_error (_, err) -> + prerr_endline (Type_check.string_of_type_error err); + exit 1 let rewrite_ast = rewrite [Rewriter.rewrite_defs] let rewrite_ast_lem = rewrite Rewriter.rewrite_defs_lem diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml index e552dca4..a47ee8ae 100644 --- a/src/reporting_basic.ml +++ b/src/reporting_basic.ml @@ -87,14 +87,6 @@ (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (**************************************************************************) -let format_pos ff p = - let open Lexing in - begin - Format.fprintf ff "file \"%s\", line %d, character %d:\n" - p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol); - Format.pp_print_flush ff () - end - let rec skip_lines in_chan = function | n when n <= 0 -> () | n -> input_line in_chan; skip_lines in_chan (n - 1) @@ -126,6 +118,16 @@ let print_code1 ff fname lnum1 cnum1 cnum2 = end with _ -> () +let format_pos ff p = + let open Lexing in + begin + Format.fprintf ff "file \"%s\", line %d, character %d:\n\n" + p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol); + print_code1 ff p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) (p.pos_cnum - p.pos_bol + 1); + Format.fprintf ff "\n\n"; + Format.pp_print_flush ff () + end + let print_code2 ff fname lnum1 cnum1 lnum2 cnum2 = try let in_chan = open_in fname in diff --git a/src/sail.ml b/src/sail.ml index 8083b26c..e5a5071f 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -51,6 +51,7 @@ let opt_print_lem_ast = ref false let opt_print_lem = ref false let opt_print_ocaml = ref false let opt_convert = ref false +let opt_memo_z3 = ref false let opt_libs_lem = ref ([]:string list) let opt_libs_ocaml = ref ([]:string list) let opt_file_arguments = ref ([]:string list) @@ -104,6 +105,9 @@ let options = Arg.align ([ ( "-convert", Arg.Set opt_convert, " Convert sail to new syntax"); + ( "-memo_z3", + Arg.Set opt_memo_z3, + " Memoize calls to z3"); ( "-ddump_tc_ast", Arg.Set opt_ddump_tc_ast, " (debug) dump the typechecked ast to stdout"); @@ -143,6 +147,7 @@ let main() = if !(opt_print_version) then Printf.printf "Sail private release \n" else + if !opt_memo_z3 then Constraint.load_digests () else (); let parsed = (List.map (fun f -> (f,(parse_file f))) !opt_file_arguments) in let ast = @@ -166,6 +171,9 @@ let main() = let out_name = match !opt_file_out with | None -> fst (List.hd parsed) | Some f -> f ^ ".sail" in + + if !opt_memo_z3 then Constraint.save_digests () else (); + (*let _ = Printf.eprintf "Type checked, next to pretty print" in*) begin (if !(opt_print_verbose) diff --git a/src/type_check.ml b/src/type_check.ml index 76bc0d2a..06083211 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1105,9 +1105,9 @@ let prove_z3 env nc = in let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env)) (Constraint.negate (nc_constraint env var_of nc)) in match Constraint.call_z3 constr with - | Constraint.Unsat _ -> typ_debug "unsat"; true - | Constraint.Unknown [] -> typ_debug "sat"; false - | Constraint.Unknown _ -> typ_debug "unknown"; false + | Constraint.Unsat -> typ_debug "unsat"; true + | Constraint.Sat -> typ_debug "sat"; false + | Constraint.Unknown -> typ_debug "unknown"; false let prove env (NC_aux (nc_aux, _) as nc) = let compare_const f (Nexp_aux (n1, _)) (Nexp_aux (n2, _)) = @@ -1171,9 +1171,9 @@ let rec subtyp_tnf env tnf1 tnf2 = let (prop1, prop2) = props_subst kid1 (Nexp_var kid3) prop1, props_subst kid2 (Nexp_var kid3) prop2 in let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env)) (Constraint.conj (pos_props prop1) (neg_props prop2)) in match Constraint.call_z3 constr with - | Constraint.Unsat _ -> typ_debug "unsat"; true - | Constraint.Unknown [] -> typ_debug "sat"; false - | Constraint.Unknown _ -> typ_debug "unknown"; false + | Constraint.Unsat -> typ_debug "unsat"; true + | Constraint.Sat -> typ_debug "sat"; false + | Constraint.Unknown -> typ_debug "unknown"; false end | _, _ -> false |