diff options
Diffstat (limited to 'src/lfsc')
| -rw-r--r-- | src/lfsc/ast.ml | 4 | ||||
| -rw-r--r-- | src/lfsc/builtin.ml | 2 | ||||
| -rw-r--r-- | src/lfsc/lfsc.ml | 22 | ||||
| -rw-r--r-- | src/lfsc/shashcons.mli | 2 |
4 files changed, 16 insertions, 14 deletions
diff --git a/src/lfsc/ast.ml b/src/lfsc/ast.ml index 7c2cd8f..d231dc6 100644 --- a/src/lfsc/ast.ml +++ b/src/lfsc/ast.ml @@ -198,7 +198,7 @@ let compare_symbol s1 s2 = match s1.sname, s2.sname with | Name n1, Name n2 -> Hstring.compare n1 n2 | Name _, _ -> -1 | _, Name _ -> 1 - | S_Hole i1, S_Hole i2 -> Pervasives.compare i1 i2 + | S_Hole i1, S_Hole i2 -> Stdlib.compare i1 i2 let rec compare_term ?(mod_eq=false) t1 t2 = match t1.value, t2.value with @@ -250,7 +250,7 @@ let rec compare_term ?(mod_eq=false) t1 t2 = match t1.value, t2.value with | SideCond (_, _, _, t), _ -> compare_term ~mod_eq t t2 | _, SideCond (_, _, _, t) -> compare_term ~mod_eq t1 t - | Hole i1, Hole i2 -> Pervasives.compare i1 i2 + | Hole i1, Hole i2 -> Stdlib.compare i1 i2 and compare_term_list ?(mod_eq=false) l1 l2 = match l1, l2 with diff --git a/src/lfsc/builtin.ml b/src/lfsc/builtin.ml index e528db3..3ee5f33 100644 --- a/src/lfsc/builtin.ml +++ b/src/lfsc/builtin.ml @@ -616,7 +616,7 @@ let cong s1 s2 a1 b1 a2 b2 u1 u2 = module MInt = Map.Make (struct type t = int - let compare = Pervasives.compare + let compare = Stdlib.compare end) module STerm = Set.Make (Term) diff --git a/src/lfsc/lfsc.ml b/src/lfsc/lfsc.ml index 906340d..10e40ed 100644 --- a/src/lfsc/lfsc.ml +++ b/src/lfsc/lfsc.ml @@ -57,7 +57,7 @@ let process_signatures_once = ) signatures with | Ast.TypingError (t1, t2) -> - Structures.error + CoqInterface.error (asprintf "@[<hov>LFSC typing error: expected %a, got %a@]@." Ast.print_term t1 Ast.print_term t2) @@ -116,7 +116,7 @@ let import_trace first parse lexbuf = with | Ast.TypingError (t1, t2) -> - Structures.error + CoqInterface.error (asprintf "@[<hov>LFSC typing error: expected %a, got %a@]@." Ast.print_term t1 Ast.print_term t2) @@ -386,13 +386,13 @@ let call_cvc4 env rt ro ra rf root _ = begin try get_proof cvc4 (import_trace (Some root) lfsc_parse_one) with - | Ast.CVC4Sat -> Structures.error "CVC4 returned SAT" - | No_proof -> Structures.error "CVC4 did not generate a proof" - | Failure s -> Structures.error ("Importing of proof failed: " ^ s) + | Ast.CVC4Sat -> CoqInterface.error "CVC4 returned SAT" + | No_proof -> CoqInterface.error "CVC4 did not generate a proof" + | Failure s -> CoqInterface.error ("Importing of proof failed: " ^ s) end | Sat -> let smodel = get_model cvc4 in - Structures.error + CoqInterface.error ("CVC4 returned sat. Here is the model:\n\n" ^ SmtCommands.model_string env rt ro ra rf smodel) (* (asprintf "CVC4 returned sat. Here is the model:\n%a" SExpr.print smodel) *) @@ -435,7 +435,7 @@ let get_model_from_file filename = let lexbuf = Lexing.from_channel chan in match SExprParser.sexps SExprLexer.main lexbuf with | [SExpr.Atom "sat"; m] -> m - | _ -> Structures.error "CVC4 returned SAT but no model" + | _ -> CoqInterface.error "CVC4 returned SAT but no model" let call_cvc4_file env rt ro ra rf root = @@ -467,17 +467,17 @@ let call_cvc4_file env rt ro ra rf root = eprintf "CVC4 = %.5f@." (t1-.t0); if exit_code <> 0 then - Structures.error ("CVC4 crashed: return code "^string_of_int exit_code); + CoqInterface.error ("CVC4 crashed: return code "^string_of_int exit_code); (* ignore (Sys.command clean_cmd); *) try import_trace_from_file (Some root) prooffilename with - | No_proof -> Structures.error "CVC4 did not generate a proof" - | Failure s -> Structures.error ("Importing of proof failed: " ^ s) + | No_proof -> CoqInterface.error "CVC4 did not generate a proof" + | Failure s -> CoqInterface.error ("Importing of proof failed: " ^ s) | Ast.CVC4Sat -> let smodel = get_model_from_file prooffilename in - Structures.error + CoqInterface.error ("CVC4 returned sat. Here is the model:\n\n" ^ SmtCommands.model_string env rt ro ra rf smodel) diff --git a/src/lfsc/shashcons.mli b/src/lfsc/shashcons.mli index 6787322..e9ba5fb 100644 --- a/src/lfsc/shashcons.mli +++ b/src/lfsc/shashcons.mli @@ -47,6 +47,7 @@ module type S = val iter : (t -> unit) -> unit (** [iter f] iterates [f] over all elements of the table . *) + val stats : unit -> int * int * int * int * int * int (** Return statistics on the table. The numbers are, in order: table length, number of entries, sum of bucket lengths, @@ -83,6 +84,7 @@ module type S_consed = val iter : (key hash_consed -> unit) -> unit (** [iter f] iterates [f] over all elements of the table . *) + val stats : unit -> int * int * int * int * int * int (** Return statistics on the table. The numbers are, in order: table length, number of entries, sum of bucket lengths, |