diff options
Diffstat (limited to 'src/trace')
-rw-r--r-- | src/trace/smtAtom.ml | 145 | ||||
-rw-r--r-- | src/trace/smtAtom.mli | 43 | ||||
-rw-r--r-- | src/trace/smtBtype.ml | 113 | ||||
-rw-r--r-- | src/trace/smtBtype.mli | 16 | ||||
-rw-r--r-- | src/trace/smtCommands.ml | 2 | ||||
-rw-r--r-- | src/trace/smtCommands.mli | 18 |
6 files changed, 158 insertions, 179 deletions
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 72e7ed3..ed0402c 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -16,120 +16,7 @@ open SmtMisc open CoqTerms - -(** Syntaxified version of Coq type *) -type indexed_type = Term.constr gen_hashed - -let dummy_indexed_type i = {index = i; hval = Term.mkProp} -let indexed_type_index i = i.index - -type btype = - | TZ - | Tbool - | Tpositive - | Tindex of indexed_type - -module Btype = - struct - - let index_tbl = Hashtbl.create 17 - - let index_to_coq i = - let i = i.index in - try Hashtbl.find index_tbl i - with Not_found -> - let interp = mklApp cTindex [|mkInt i|] in - Hashtbl.add index_tbl i interp; - interp - - let equal t1 t2 = - match t1,t2 with - | Tindex i, Tindex j -> i.index == j.index - | _ -> t1 == t2 - - let to_coq = function - | TZ -> Lazy.force cTZ - | Tbool -> Lazy.force cTbool - | Tpositive -> Lazy.force cTpositive - | Tindex i -> index_to_coq i - - let to_smt fmt = function - | TZ -> Format.fprintf fmt "Int" - | Tbool -> Format.fprintf fmt "Bool" - | Tpositive -> Format.fprintf fmt "Int" - | Tindex i -> Format.fprintf fmt "Tindex_%i" i.index - - (* reify table *) - type reify_tbl = - { mutable count : int; - tbl : (Term.constr, btype) Hashtbl.t; - mutable cuts : (Structures.names_id_t * Term.types) list - } - - let create () = - let htbl = Hashtbl.create 17 in - Hashtbl.add htbl (Lazy.force cZ) TZ; - Hashtbl.add htbl (Lazy.force cbool) Tbool; - (* Hashtbl.add htbl (Lazy.force cpositive) Tpositive; *) - { count = 0; - tbl = htbl; - cuts = [] } - - let get_cuts reify = reify.cuts - - let declare reify t typ_eqb = - (* TODO: allows to have only typ_eqb *) - assert (not (Hashtbl.mem reify.tbl t)); - let res = Tindex {index = reify.count; hval = typ_eqb} in - Hashtbl.add reify.tbl t res; - reify.count <- reify.count + 1; - res - - let of_coq reify t = - try - Hashtbl.find reify.tbl t - with | Not_found -> - let n = string_of_int (List.length reify.cuts) in - let eq_name = Names.id_of_string ("eq"^n) in - let eq_var = Term.mkVar eq_name in - - let eq_ty = Term.mkArrow t (Term.mkArrow t (Lazy.force cbool)) in - - let eq = mkName "eq" in - let x = mkName "x" in - let y = mkName "y" in - let req = Term.mkRel 3 in - let rx = Term.mkRel 2 in - let ry = Term.mkRel 1 in - let refl_ty = Term.mkLambda (eq, eq_ty, Term.mkProd (x,t,Term.mkProd (y,t,mklApp creflect [|mklApp ceq [|t;rx;ry|]; Term.mkApp (req, [|rx;ry|])|]))) in - - let pair_ty = mklApp csigT [|eq_ty; refl_ty|] in - - reify.cuts <- (eq_name, pair_ty)::reify.cuts; - let ce = mklApp ctyp_eqb_of_typ_eqb_param [|t; eq_var|] in - declare reify t ce - - let interp_tbl reify = - let t = Array.make (reify.count + 1) (Lazy.force cunit_typ_eqb) in - let set _ = function - | Tindex it -> t.(it.index) <- it.hval - | _ -> () in - Hashtbl.iter set reify.tbl; - Structures.mkArray (Lazy.force ctyp_eqb, t) - - let to_list reify = - let set _ t acc = match t with - | Tindex it -> (it.index,it)::acc - | _ -> acc in - Hashtbl.fold set reify.tbl [] - - let interp_to_coq reify = function - | TZ -> Lazy.force cZ - | Tbool -> Lazy.force cbool - | Tpositive -> Lazy.force cpositive - | Tindex c -> mklApp cte_carrier [|c.hval|] - - end +open SmtBtype (** Operators *) @@ -215,7 +102,7 @@ module Op = let eq_to_coq t = try Hashtbl.find eq_tbl t with Not_found -> - let op = mklApp cBO_eq [|Btype.to_coq t|] in + let op = mklApp cBO_eq [|SmtBtype.to_coq t|] in Hashtbl.add eq_tbl t op; op @@ -242,7 +129,7 @@ module Op = | TZ -> Lazy.force ceqbZ | Tbool -> Lazy.force ceqb | Tpositive -> Lazy.force ceqbP - | Tindex i -> mklApp cte_eqb [|i.hval|] + | Tindex i -> mklApp cte_eqb [|indexed_type_hval i|] let interp_bop = function | BO_Zplus -> Lazy.force cadd @@ -255,7 +142,7 @@ module Op = | BO_eq t -> interp_eq t let n_to_coq = function - | NO_distinct t -> mklApp cNO_distinct [|Btype.to_coq t|] + | NO_distinct t -> mklApp cNO_distinct [|SmtBtype.to_coq t|] let n_type_of = function | NO_distinct _ -> Tbool @@ -267,7 +154,7 @@ module Op = | TZ -> Lazy.force cZ | Tbool -> Lazy.force cbool | Tpositive -> Lazy.force cpositive - | Tindex i -> mklApp cte_carrier [|i.hval|] + | Tindex i -> mklApp cte_carrier [|indexed_type_hval i|] let interp_nop = function | NO_distinct ty -> mklApp cdistinct [|interp_distinct ty;interp_eq ty|] @@ -320,12 +207,12 @@ module Op = let b_equal op1 op2 = match op1,op2 with - | BO_eq t1, BO_eq t2 -> Btype.equal t1 t2 + | BO_eq t1, BO_eq t2 -> SmtBtype.equal t1 t2 | _ -> op1 == op2 let n_equal op1 op2 = match op1,op2 with - | NO_distinct t1, NO_distinct t2 -> Btype.equal t1 t2 + | NO_distinct t1, NO_distinct t2 -> SmtBtype.equal t1 t2 let i_equal op1 op2 = op1.index == op2.index @@ -437,7 +324,7 @@ module Atom = | Anop (op,_) -> Op.n_type_of op | Aapp (op,_) -> Op.i_type_of op - let is_bool_type h = Btype.equal (type_of h) Tbool + let is_bool_type h = SmtBtype.equal (type_of h) Tbool let rec compute_int = function @@ -513,19 +400,19 @@ module Atom = match a with | Acop _ -> () | Auop(op,h) -> - if not (Btype.equal (Op.u_type_arg op) (type_of 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 (Btype.equal t1 (type_of h1) && Btype.equal t2 (type_of h2)) + if not (SmtBtype.equal t1 (type_of h1) && SmtBtype.equal t2 (type_of h2)) then raise (NotWellTyped a) | Anop(op,ha) -> let ty = Op.n_type_args op in - Array.iter (fun h -> if not (Btype.equal ty (type_of h)) then raise (NotWellTyped a)) ha + 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 (Btype.equal t (type_of args.(i))) then + if not (SmtBtype.equal t (type_of args.(i))) then raise (NotWellTyped a)) tparams type reify_tbl = @@ -632,7 +519,7 @@ module Atom = let op = try Op.of_coq ro c with Not_found -> let targs = Array.map type_of hargs in - let tres = Btype.of_coq rt ty in + let tres = SmtBtype.of_coq rt ty in Op.declare ro c targs tres in get reify (Aapp (op,hargs)) in @@ -768,9 +655,9 @@ module Trace = SmtTrace.MakeOpt(Form) let mk_ftype cod dom = let typeb = Lazy.force ctype in let typea = mklApp clist [|typeb|] in - let a = Array.fold_right (fun bt acc -> mklApp ccons [|typeb; Btype.to_coq bt; acc|]) cod (mklApp cnil [|typeb|]) in - let b = Btype.to_coq dom in + let a = Array.fold_right (fun bt acc -> mklApp ccons [|typeb; SmtBtype.to_coq bt; acc|]) cod (mklApp cnil [|typeb|]) in + let b = SmtBtype.to_coq dom in mklApp cpair [|typea;typeb;a;b|] -let make_t_i rt = Btype.interp_tbl rt +let make_t_i rt = SmtBtype.interp_tbl rt let make_t_func ro t_i = Op.interp_tbl (mklApp ctval [|t_i|]) (fun cod dom value -> mklApp cTval [|t_i; mk_ftype cod dom; value|]) ro diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index e6a3c47..8e69265 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -13,44 +13,7 @@ (* *) (**************************************************************************) - -type indexed_type - -val dummy_indexed_type: int -> indexed_type -val indexed_type_index : indexed_type -> int - -type btype = - | TZ - | Tbool - | Tpositive - | Tindex of indexed_type - -module Btype : - sig - - val equal : btype -> btype -> bool - - val to_coq : btype -> Term.constr - - val to_smt : Format.formatter -> btype -> unit - - type reify_tbl - - val create : unit -> reify_tbl - - val declare : reify_tbl -> Term.constr -> Term.constr -> btype - - val of_coq : reify_tbl -> Term.constr -> btype - - val interp_tbl : reify_tbl -> Term.constr - - val to_list : reify_tbl -> (int * indexed_type) list - - val interp_to_coq : reify_tbl -> btype -> Term.constr - - val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list - - end +open SmtBtype (** Operators *) @@ -142,7 +105,7 @@ module Atom : val get : reify_tbl -> atom -> hatom (** Given a coq term, build the corresponding atom *) - val of_coq : Btype.reify_tbl -> Op.reify_tbl -> + val of_coq : SmtBtype.reify_tbl -> Op.reify_tbl -> reify_tbl -> Environ.env -> Evd.evar_map -> Term.constr -> t val to_coq : hatom -> Term.constr @@ -178,5 +141,5 @@ module Trace : sig end -val make_t_i : Btype.reify_tbl -> Term.constr +val make_t_i : SmtBtype.reify_tbl -> Term.constr val make_t_func : Op.reify_tbl -> Term.constr -> Term.constr diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml new file mode 100644 index 0000000..92b8ad7 --- /dev/null +++ b/src/trace/smtBtype.ml @@ -0,0 +1,113 @@ +open SmtMisc +open CoqTerms + +(** Syntaxified version of Coq type *) + +type indexed_type = Term.constr gen_hashed + +let dummy_indexed_type i = {index = i; hval = Term.mkProp} +let indexed_type_index i = i.index +let indexed_type_hval i = i.hval + +type btype = + | TZ + | Tbool + | Tpositive + | Tindex of indexed_type + +let index_tbl = Hashtbl.create 17 + +let index_to_coq i = + let i = i.index in + try Hashtbl.find index_tbl i + with Not_found -> + let interp = mklApp cTindex [|mkInt i|] in + Hashtbl.add index_tbl i interp; + interp + +let equal t1 t2 = + match t1,t2 with + | Tindex i, Tindex j -> i.index == j.index + | _ -> t1 == t2 + +let to_coq = function + | TZ -> Lazy.force cTZ + | Tbool -> Lazy.force cTbool + | Tpositive -> Lazy.force cTpositive + | Tindex i -> index_to_coq i + +let to_smt fmt = function + | TZ -> Format.fprintf fmt "Int" + | Tbool -> Format.fprintf fmt "Bool" + | Tpositive -> Format.fprintf fmt "Int" + | Tindex i -> Format.fprintf fmt "Tindex_%i" i.index + +(* reify table *) +type reify_tbl = + { mutable count : int; + tbl : (Term.constr, btype) Hashtbl.t; + mutable cuts : (Structures.names_id_t * Term.types) list + } + +let create () = + let htbl = Hashtbl.create 17 in + Hashtbl.add htbl (Lazy.force cZ) TZ; + Hashtbl.add htbl (Lazy.force cbool) Tbool; + (* Hashtbl.add htbl (Lazy.force cpositive) Tpositive; *) + { count = 0; + tbl = htbl; + cuts = [] } + +let get_cuts reify = reify.cuts + +let declare reify t typ_eqb = + (* TODO: allows to have only typ_eqb *) + assert (not (Hashtbl.mem reify.tbl t)); + let res = Tindex {index = reify.count; hval = typ_eqb} in + Hashtbl.add reify.tbl t res; + reify.count <- reify.count + 1; + res + +let of_coq reify t = + try + Hashtbl.find reify.tbl t + with | Not_found -> + let n = string_of_int (List.length reify.cuts) in + let eq_name = Names.id_of_string ("eq"^n) in + let eq_var = Term.mkVar eq_name in + + let eq_ty = Term.mkArrow t (Term.mkArrow t (Lazy.force cbool)) in + + let eq = mkName "eq" in + let x = mkName "x" in + let y = mkName "y" in + let req = Term.mkRel 3 in + let rx = Term.mkRel 2 in + let ry = Term.mkRel 1 in + let refl_ty = Term.mkLambda (eq, eq_ty, Term.mkProd (x,t,Term.mkProd (y,t,mklApp creflect [|mklApp ceq [|t;rx;ry|]; Term.mkApp (req, [|rx;ry|])|]))) in + + let pair_ty = mklApp csigT [|eq_ty; refl_ty|] in + + reify.cuts <- (eq_name, pair_ty)::reify.cuts; + let ce = mklApp ctyp_eqb_of_typ_eqb_param [|t; eq_var|] in + declare reify t ce + +let interp_tbl reify = + let t = Array.make (reify.count + 1) (Lazy.force cunit_typ_eqb) in + let set _ = function + | Tindex it -> t.(it.index) <- it.hval + | _ -> () in + Hashtbl.iter set reify.tbl; + Structures.mkArray (Lazy.force ctyp_eqb, t) + +let to_list reify = + let set _ t acc = match t with + | Tindex it -> (it.index,it)::acc + | _ -> acc in + Hashtbl.fold set reify.tbl [] + +let interp_to_coq reify = function + | TZ -> Lazy.force cZ + | Tbool -> Lazy.force cbool + | Tpositive -> Lazy.force cpositive + | Tindex c -> mklApp cte_carrier [|c.hval|] diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli new file mode 100644 index 0000000..11d596f --- /dev/null +++ b/src/trace/smtBtype.mli @@ -0,0 +1,16 @@ +type indexed_type +val dummy_indexed_type : int -> indexed_type +val indexed_type_index : indexed_type -> int +val indexed_type_hval : indexed_type -> Term.constr +type btype = TZ | Tbool | Tpositive | Tindex of indexed_type +val equal : btype -> btype -> bool +val to_coq : btype -> Term.constr +val to_smt : Format.formatter -> btype -> unit +type reify_tbl +val create : unit -> reify_tbl +val declare : reify_tbl -> Term.constr -> Term.constr -> btype +val of_coq : reify_tbl -> Term.constr -> btype +val interp_tbl : reify_tbl -> Term.constr +val to_list : reify_tbl -> (int * indexed_type) list +val interp_to_coq : reify_tbl -> btype -> Term.constr +val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index 8950022..ba86a5b 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -383,7 +383,7 @@ let core_tactic call_solver rt ro ra rf env sigma concl = let max_id_confl = make_proof call_solver rt ro rf l in build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl in - let cuts = (Btype.get_cuts rt)@cuts in + let cuts = SmtBtype.get_cuts rt @ cuts in List.fold_right (fun (eqn, eqt) tac -> Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac) diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli index d6fa756..3cac245 100644 --- a/src/trace/smtCommands.mli +++ b/src/trace/smtCommands.mli @@ -32,21 +32,21 @@ val parse_certif : Names.identifier -> Names.identifier -> Names.identifier -> - SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * + SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify * SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> unit val interp_roots : SmtAtom.Form.t list -> Term.constr val theorem : Names.identifier -> - SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * + SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify * SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> unit val checker : - SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * + SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify * SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> unit val build_body : - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> @@ -55,7 +55,7 @@ val build_body : int * SmtAtom.Form.t SmtCertif.clause -> Term.constr * Term.constr * (Names.identifier * Term.types) list val build_body_eq : - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> @@ -71,22 +71,22 @@ val make_proof : SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> 'c) -> 'a -> 'b -> SmtAtom.Form.reify -> SmtAtom.Form.t -> 'c val core_tactic : - (SmtAtom.Btype.reify_tbl -> + (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> int * SmtAtom.Form.t SmtCertif.clause) -> - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Environ.env -> Evd.evar_map -> Term.constr -> Structures.tactic val tactic : - (SmtAtom.Btype.reify_tbl -> + (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> int * SmtAtom.Form.t SmtCertif.clause) -> - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Structures.tactic |