aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace
diff options
context:
space:
mode:
Diffstat (limited to 'src/trace')
-rw-r--r--src/trace/coqTerms.ml65
-rw-r--r--src/trace/smtAtom.ml132
-rw-r--r--src/trace/smtAtom.mli2
-rw-r--r--src/trace/smtCommands.ml2
-rw-r--r--src/trace/smtForm.ml18
-rw-r--r--src/trace/smtForm.mli8
-rw-r--r--src/trace/smtMisc.ml2
-rw-r--r--src/trace/smtTrace.ml4
8 files changed, 125 insertions, 108 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index ad5ec1d..a1b6765 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -10,7 +10,6 @@
(**************************************************************************)
-open Coqlib
open SmtMisc
@@ -25,9 +24,9 @@ let ceq63 = gen_constant Structures.int63_modules "eqb"
let carray = gen_constant Structures.parray_modules "array"
(* nat *)
-let cnat = gen_constant init_modules "nat"
-let cO = gen_constant init_modules "O"
-let cS = gen_constant init_modules "S"
+let cnat = gen_constant Structures.init_modules "nat"
+let cO = gen_constant Structures.init_modules "O"
+let cS = gen_constant Structures.init_modules "S"
(* Positive *)
let positive_modules = [["Coq";"Numbers";"BinNums"];
@@ -72,49 +71,49 @@ let ceqbZ = gen_constant z_modules "eqb"
(* Booleans *)
let bool_modules = [["Coq";"Bool";"Bool"]]
-let cbool = gen_constant init_modules "bool"
-let ctrue = gen_constant init_modules "true"
-let cfalse = gen_constant init_modules "false"
-let candb = gen_constant init_modules "andb"
-let corb = gen_constant init_modules "orb"
-let cxorb = gen_constant init_modules "xorb"
-let cnegb = gen_constant init_modules "negb"
-let cimplb = gen_constant init_modules "implb"
+let cbool = gen_constant Structures.init_modules "bool"
+let ctrue = gen_constant Structures.init_modules "true"
+let cfalse = gen_constant Structures.init_modules "false"
+let candb = gen_constant Structures.init_modules "andb"
+let corb = gen_constant Structures.init_modules "orb"
+let cxorb = gen_constant Structures.init_modules "xorb"
+let cnegb = gen_constant Structures.init_modules "negb"
+let cimplb = gen_constant Structures.init_modules "implb"
let ceqb = gen_constant bool_modules "eqb"
let cifb = gen_constant bool_modules "ifb"
-let ciff = gen_constant init_modules "iff"
+let ciff = gen_constant Structures.init_modules "iff"
let creflect = gen_constant bool_modules "reflect"
(* Lists *)
-let clist = gen_constant init_modules "list"
-let cnil = gen_constant init_modules "nil"
-let ccons = gen_constant init_modules "cons"
-let clength = gen_constant init_modules "length"
+let clist = gen_constant Structures.init_modules "list"
+let cnil = gen_constant Structures.init_modules "nil"
+let ccons = gen_constant Structures.init_modules "cons"
+let clength = gen_constant Structures.init_modules "length"
(* Option *)
-let coption = gen_constant init_modules "option"
-let cSome = gen_constant init_modules "Some"
-let cNone = gen_constant init_modules "None"
+let coption = gen_constant Structures.init_modules "option"
+let cSome = gen_constant Structures.init_modules "Some"
+let cNone = gen_constant Structures.init_modules "None"
(* Pairs *)
-let cpair = gen_constant init_modules "pair"
-let cprod = gen_constant init_modules "prod"
+let cpair = gen_constant Structures.init_modules "pair"
+let cprod = gen_constant Structures.init_modules "prod"
(* Dependent pairs *)
-let csigT = gen_constant init_modules "sigT"
-(* let cprojT1 = gen_constant init_modules "projT1" *)
-(* let cprojT2 = gen_constant init_modules "projT2" *)
-(* let cprojT3 = gen_constant init_modules "projT3" *)
+let csigT = gen_constant Structures.init_modules "sigT"
+(* let cprojT1 = gen_constant Structures.init_modules "projT1" *)
+(* let cprojT2 = gen_constant Structures.init_modules "projT2" *)
+(* let cprojT3 = gen_constant Structures.init_modules "projT3" *)
-(* let csigT2 = gen_constant init_modules "sigT2" *)
-(* let csigT_of_sigT2 = gen_constant init_modules "sigT_of_sigT2" *)
+(* let csigT2 = gen_constant Structures.init_modules "sigT2" *)
+(* let csigT_of_sigT2 = gen_constant Structures.init_modules "sigT_of_sigT2" *)
(* Logical Operators *)
-let cnot = gen_constant init_modules "not"
-let ceq = gen_constant init_modules "eq"
-let crefl_equal = gen_constant init_modules "eq_refl"
-let cconj = gen_constant init_modules "conj"
-let cand = gen_constant init_modules "and"
+let cnot = gen_constant Structures.init_modules "not"
+let ceq = gen_constant Structures.init_modules "eq"
+let crefl_equal = gen_constant Structures.init_modules "eq_refl"
+let cconj = gen_constant Structures.init_modules "conj"
+let cand = gen_constant Structures.init_modules "and"
(* Bit vectors *)
let bv_modules = [["SMTCoq";"bva";"BVList";"BITVECTOR_LIST"]]
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 16d9bdb..ae44b8d 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -649,25 +649,9 @@ module Atom =
to_smt_atom (atom h)
and to_smt_atom = function
- | Acop (CO_BV bv) -> Format.fprintf fmt "#b%a" bv_to_smt bv
+ | Acop (CO_BV bv) -> if List.length bv = 0 then Structures.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv
| Acop _ as a -> to_smt_int fmt (compute_int a)
- | Auop (UO_Zopp,h) ->
- Format.fprintf fmt "(- ";
- to_smt fmt h;
- Format.fprintf fmt ")"
- | Auop (UO_BVbitOf (_, i), h) ->
- Format.fprintf fmt "(bitof %d %a)" i to_smt h
- | Auop (UO_BVnot _, h) ->
- Format.fprintf fmt "(bvnot %a)" to_smt h
- | Auop (UO_BVneg _, h) ->
- Format.fprintf fmt "(bvneg %a)" to_smt h
- | Auop (UO_BVextr (i, n, _), h) ->
- Format.fprintf fmt "((_ extract %d %d) %a)" (i+n-1) i to_smt h
- | Auop (UO_BVzextn (_, n), h) ->
- Format.fprintf fmt "((_ zero_extend %d) %a)" n to_smt h
- | Auop (UO_BVsextn (_, n), h) ->
- Format.fprintf fmt "((_ sign_extend %d) %a)" n to_smt h
- | Auop _ as a -> to_smt_int fmt (compute_int a)
+ | Auop (op,h) -> to_smt_uop op h
| Abop (op,h1,h2) -> to_smt_bop op h1 h2
| Atop (op,h1,h2,h3) -> to_smt_top op h1 h2 h3
| Anop (op,a) -> to_smt_nop op a
@@ -694,6 +678,28 @@ module Atom =
SmtBtype.to_smt fmt bt;
Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (Structures.pr_constr t))
+ and to_smt_uop op h =
+ match op with
+ | UO_Zpos ->
+ Format.fprintf fmt "%a" to_smt h
+ | UO_Zneg ->
+ Format.fprintf fmt "(- %a)" to_smt h
+ | UO_Zopp ->
+ Format.fprintf fmt "(- %a)" to_smt h
+ | UO_BVbitOf (_, i) ->
+ Format.fprintf fmt "(bitof %d %a)" i to_smt h
+ | UO_BVnot _ ->
+ Format.fprintf fmt "(bvnot %a)" to_smt h
+ | UO_BVneg _ ->
+ Format.fprintf fmt "(bvneg %a)" to_smt h
+ | UO_BVextr (i, n, _) ->
+ Format.fprintf fmt "((_ extract %d %d) %a)" (i+n-1) i to_smt h
+ | UO_BVzextn (_, n) ->
+ Format.fprintf fmt "((_ zero_extend %d) %a)" n to_smt h
+ | UO_BVsextn (_, n) ->
+ Format.fprintf fmt "((_ sign_extend %d) %a)" n to_smt h
+ | _ -> to_smt_int fmt (compute_int (Auop (op, h)))
+
and to_smt_bop op h1 h2 =
let s = match op with
| BO_Zplus -> "+"
@@ -738,41 +744,6 @@ module Atom =
let to_smt (fmt:Format.formatter) h = to_smt_named fmt h
- exception NotWellTyped of atom
-
- let check a =
- (* Format.eprintf "Checking %a @." to_smt_atom a; *)
- match a with
- | Acop _ -> ()
- | Auop(op,h) ->
- if not (SmtBtype.equal (Op.u_type_arg op) (type_of h)) then
- raise (NotWellTyped a)
- | Abop(op,h1,h2) ->
- let (t1,t2) = Op.b_type_args op in
- if not (SmtBtype.equal t1 (type_of h1) && SmtBtype.equal t2 (type_of h2))
- then (Format.eprintf "1. Wanted %a, got %a@.2. Wanted %a, got %a@."
- SmtBtype.to_smt t1 SmtBtype.to_smt (type_of h1)
- SmtBtype.to_smt t2 SmtBtype.to_smt (type_of h2);
- raise (NotWellTyped a))
- | Atop(op,h1,h2,h3) ->
- let (t1,t2,t3) = Op.t_type_args op in
- if not (SmtBtype.equal t1 (type_of h1) &&
- SmtBtype.equal t2 (type_of h2) &&
- SmtBtype.equal t3 (type_of h3))
- then raise (NotWellTyped a)
- | Anop(op,ha) ->
- let ty = Op.n_type_args op in
- Array.iter
- (fun h -> if not (SmtBtype.equal ty (type_of h)) then
- raise (NotWellTyped a)) ha
- | Aapp(op,args) ->
- let tparams = Op.i_type_args op in
- Array.iteri (fun i t ->
- if not (SmtBtype.equal t (type_of args.(i))) then
- (Format.eprintf "Wanted %a, got %a@."
- SmtBtype.to_smt t SmtBtype.to_smt (type_of args.(i));
- raise (NotWellTyped a))) tparams
-
type reify_tbl =
{ mutable count : int;
tbl : hatom HashAtom.t
@@ -789,19 +760,68 @@ module Atom =
reify.count <- 0;
HashAtom.clear reify.tbl
+
let declare reify a =
- check a;
let res = {index = reify.count; hval = a} in
HashAtom.add reify.tbl a res;
reify.count <- reify.count + 1;
res
- let get ?declare:(decl=true) reify a =
+ let rec get ?declare:(decl=true) reify a =
if decl
then try HashAtom.find reify.tbl a
- with Not_found -> declare reify a
+ with Not_found ->
+ (let a = check reify a in
+ try HashAtom.find reify.tbl a
+ with Not_found ->
+ declare reify a)
else {index = -1; hval = a}
+ and check reify a =
+ (* Format.eprintf "Checking %a @." to_smt_atom a; *)
+
+ let check_one t h =
+ let th = type_of h in
+ if SmtBtype.equal t th then
+ h
+ else if t == TZ && th == Tpositive then
+ (* Special case: the SMT solver cannot distinguish Z from
+ positive, we have to add the injection back *)
+ get reify (Auop(UO_Zpos, h))
+ else (
+ Format.eprintf "Incorrect type: wanted %a, got %a@."
+ SmtBtype.to_smt t SmtBtype.to_smt th;
+ failwith (Format.asprintf "Atom %a is not of the expected type" to_smt h)
+ )
+ in
+
+ let a =
+ match a with
+ | Acop _ -> a
+ | Auop(op,h) ->
+ let t = Op.u_type_arg op in
+ Auop(op, check_one t h)
+ | Abop(op,h1,h2) ->
+ let (t1,t2) = Op.b_type_args op in
+ let h1 = check_one t1 h1 in
+ let h2 = check_one t2 h2 in
+ Abop(op, h1, h2)
+ | Atop(op,h1,h2,h3) ->
+ let (t1,t2,t3) = Op.t_type_args op in
+ let h1 = check_one t1 h1 in
+ let h2 = check_one t2 h2 in
+ let h3 = check_one t3 h3 in
+ Atop(op, h1, h2, h3)
+ | Anop(op,ha) ->
+ let ty = Op.n_type_args op in
+ Anop(op, Array.map (check_one ty) ha)
+ | Aapp(op,args) ->
+ let tparams = Op.i_type_args op in
+ Aapp(op, Array.mapi (fun i -> check_one tparams.(i)) args)
+ in
+ a
+
+
let mk_eq reify ?declare:(decl=true) ty h1 h2 =
let op = BO_eq ty in
try
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index a6a1761..f076cb8 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -121,8 +121,6 @@ module Atom :
val to_smt : Format.formatter -> t -> unit
- exception NotWellTyped of atom
-
type reify_tbl
val create : unit -> reify_tbl
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index e64a131..b1f2666 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -115,7 +115,7 @@ let interp_conseq_uf t_i (prem, concl) =
let tf = Hashtbl.create 17 in
let rec interp = function
| [] -> mklApp cis_true [|interp_uf t_i ta tf concl|]
- | c::prem -> Term.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in
+ | c::prem -> Structures.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in
interp prem
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 12aef5a..044ff4c 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -80,11 +80,11 @@ module type FORM =
val clear : reify -> unit
val get : ?declare:bool -> reify -> pform -> t
- (** Give a coq term, build the corresponding formula *)
+ (** Given a coq term, build the corresponding formula *)
val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t
val hash_hform : (hatom -> hatom) -> reify -> t -> t
- (** Flattening of [Fand] and [For], removing of [Fnot2] *)
+ (* Flattening of [Fand] and [For], removing of [Fnot2] *)
val flatten : reify -> t -> t
(** Turn n-ary [Fand] and [For] into their right-associative
@@ -100,10 +100,10 @@ module type FORM =
val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
val interp_tbl : reify -> Structures.constr * Structures.constr
val nvars : reify -> int
- (** Producing a Coq term corresponding to the interpretation
- of a formula *)
- (** [interp_atom] map [hatom] to coq term, it is better if it produce
- shared terms. *)
+ (* Producing a Coq term corresponding to the interpretation
+ of a formula *)
+ (* [interp_atom] map [hatom] to coq term, it is better if it produce
+ shared terms. *)
val interp_to_coq :
(hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
t -> Structures.constr
@@ -589,9 +589,9 @@ module Make (Atom:ATOM) =
(mkInt i, Structures.mkArray (Lazy.force cform, t))
let nvars reify = reify.count
- (** Producing a Coq term corresponding to the interpretation of a formula *)
- (** [interp_atom] map [Atom.t] to coq term, it is better if it produce
- shared terms. *)
+ (* Producing a Coq term corresponding to the interpretation of a formula *)
+ (* [interp_atom] map [Atom.t] to coq term, it is better if it produce
+ shared terms. *)
let interp_to_coq interp_atom form_tbl f =
let rec interp_form f =
let l = to_lit f in
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
index ad7d2ca..fead657 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -97,10 +97,10 @@ module type FORM =
val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
val interp_tbl : reify -> Structures.constr * Structures.constr
val nvars : reify -> int
- (** Producing a Coq term corresponding to the interpretation
- of a formula *)
- (** [interp_atom] map [hatom] to coq term, it is better if it produce
- shared terms. *)
+ (* Producing a Coq term corresponding to the interpretation
+ of a formula *)
+ (* [interp_atom] map [hatom] to coq term, it is better if it produce
+ shared terms. *)
val interp_to_coq :
(hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
t -> Structures.constr
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 92f0f09..607ebe7 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -46,7 +46,7 @@ type logic_item =
module SL = Set.Make (struct
type t = logic_item
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end)
type logic = SL.t
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index f397826..ef017a7 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -159,7 +159,7 @@ let order_roots init_index first =
r := n
| _ -> failwith "root value has unexpected form" end
done;
- let _, lr = List.sort (fun (i1, _) (i2, _) -> Pervasives.compare i1 i2) !acc
+ let _, lr = List.sort (fun (i1, _) (i2, _) -> Stdlib.compare i1 i2) !acc
|> List.split in
let link_to c1 c2 =
let curr_id = c2.id -1 in
@@ -476,7 +476,7 @@ let to_coq to_lit interp (cstep,
let concl' = out_cl [concl] in
let app_name = Structures.mkId ("app" ^ (string_of_int (Hashtbl.hash concl))) in
let app_var = Structures.mkVar app_name in
- let app_ty = Term.mkArrow clemma (interp ([], [concl])) in
+ let app_ty = Structures.mkArrow clemma (interp ([], [concl])) in
cuts := (app_name, app_ty)::!cuts;
mklApp cForallInst [|out_c c; clemma; cplemma; concl'; app_var|]
end
generated by cgit (git 2.34.1) at 2024-07-05 20:21:57 +0000