aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/zify.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/zify.ml')
-rw-r--r--plugins/micromega/zify.ml234
1 files changed, 147 insertions, 87 deletions
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 61966b60c0..b780c1833e 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -23,6 +23,19 @@ let zify str =
(UnivGen.constr_of_monomorphic_global
(Coqlib.lib_ref ("ZifyClasses." ^ str)))
+(** classes *)
+let coq_InjTyp = lazy (Coqlib.lib_ref "ZifyClasses.InjTyp")
+
+let coq_BinOp = lazy (Coqlib.lib_ref "ZifyClasses.BinOp")
+let coq_UnOp = lazy (Coqlib.lib_ref "ZifyClasses.UnOp")
+let coq_CstOp = lazy (Coqlib.lib_ref "ZifyClasses.CstOp")
+let coq_BinRel = lazy (Coqlib.lib_ref "ZifyClasses.BinRel")
+let coq_PropBinOp = lazy (Coqlib.lib_ref "ZifyClasses.PropBinOp")
+let coq_PropUOp = lazy (Coqlib.lib_ref "ZifyClasses.PropUOp")
+let coq_BinOpSpec = lazy (Coqlib.lib_ref "ZifyClasses.BinOpSpec")
+let coq_UnOpSpec = lazy (Coqlib.lib_ref "ZifyClasses.UnOpSpec")
+let coq_Saturate = lazy (Coqlib.lib_ref "ZifyClasses.Saturate")
+
(* morphism like lemma *)
let mkapp2 = lazy (zify "mkapp2")
@@ -46,7 +59,7 @@ let op_iff_morph = lazy (zify "iff_morph")
let op_not = lazy (zify "not")
let op_not_morph = lazy (zify "not_morph")
let op_True = lazy (zify "True")
-let whd = Reductionops.clos_whd_flags CClosure.all
+let op_I = lazy (zify "I")
(** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map.
This is useful for calling Constr.hash *)
@@ -59,6 +72,7 @@ let gl_pr_constr e =
let evd = Evd.from_env genv in
pr_constr genv evd e
+let whd = Reductionops.clos_whd_flags CClosure.all
let is_convertible env evd t1 t2 = Reductionops.(is_conv env evd t1 t2)
(** [get_type_of] performs beta reduction ;
@@ -66,14 +80,36 @@ let is_convertible env evd t1 t2 = Reductionops.(is_conv env evd t1 t2)
let get_type_of env evd e =
Tacred.cbv_beta env evd (Retyping.get_type_of env evd e)
+(* arguments are dealt with in a second step *)
+
let rec find_option pred l =
match l with
| [] -> raise Not_found
| e :: l -> ( match pred e with Some r -> r | None -> find_option pred l )
-(** [HConstr] is a map indexed by EConstr.t.
- It should only be used using closed terms.
- *)
+module ConstrMap = struct
+ open Names.GlobRef
+
+ type 'a t = 'a list Map.t
+
+ let add gr e m =
+ Map.update gr (function None -> Some [e] | Some l -> Some (e :: l)) m
+
+ let empty = Map.empty
+
+ let find evd h m =
+ match Map.find (fst (EConstr.destRef evd h)) m with
+ | e :: _ -> e
+ | [] -> assert false
+
+ let find_all evd h m = Map.find (fst (EConstr.destRef evd h)) m
+
+ let fold f m acc =
+ Map.fold
+ (fun k l acc -> List.fold_left (fun acc e -> f k e acc) acc l)
+ m acc
+end
+
module HConstr = struct
module M = Map.Make (struct
type t = EConstr.t
@@ -81,20 +117,11 @@ module HConstr = struct
let compare c c' = Constr.compare (unsafe_to_constr c) (unsafe_to_constr c')
end)
- type 'a t = 'a list M.t
-
- let lfind h m = try M.find h m with Not_found -> []
-
- let add h e m =
- let l = lfind h m in
- M.add h (e :: l) m
+ type 'a t = 'a M.t
+ let add h e m = M.add h e m
let empty = M.empty
- let find h m = match lfind h m with e :: _ -> e | [] -> raise Not_found
- let find_all = lfind
-
- let fold f m acc =
- M.fold (fun k l acc -> List.fold_left (fun acc e -> f k e acc) acc l) m acc
+ let find = M.find
end
(** [get_projections_from_constant (evd,c) ]
@@ -331,7 +358,8 @@ module type Elt = sig
(** name *)
val name : string
- val table : (term_kind * decl_kind) HConstr.t ref
+ val gref : GlobRef.t Lazy.t
+ val table : (term_kind * decl_kind) ConstrMap.t ref
val cast : elt decl -> decl_kind
val dest : decl_kind -> elt decl option
@@ -346,12 +374,12 @@ module type Elt = sig
(* val arity : int*)
end
-let table = Summary.ref ~name:"zify_table" HConstr.empty
-let saturate = Summary.ref ~name:"zify_saturate" HConstr.empty
-let specs = Summary.ref ~name:"zify_specs" HConstr.empty
-let table_cache = ref HConstr.empty
-let saturate_cache = ref HConstr.empty
-let specs_cache = ref HConstr.empty
+let table = Summary.ref ~name:"zify_table" ConstrMap.empty
+let saturate = Summary.ref ~name:"zify_saturate" ConstrMap.empty
+let specs = Summary.ref ~name:"zify_specs" ConstrMap.empty
+let table_cache = ref ConstrMap.empty
+let saturate_cache = ref ConstrMap.empty
+let specs_cache = ref ConstrMap.empty
(** Each type-class gives rise to a different table.
They only differ on how projections are extracted. *)
@@ -362,6 +390,7 @@ module EInj = struct
type elt = EInjT.t
let name = "EInj"
+ let gref = coq_InjTyp
let table = table
let cast x = InjTyp x
let dest = function InjTyp x -> Some x | _ -> None
@@ -419,6 +448,7 @@ module EBinOp = struct
open EBinOpT
let name = "BinOp"
+ let gref = coq_BinOp
let table = table
let mk_elt evd i a =
@@ -460,6 +490,7 @@ module ECstOp = struct
open ECstOpT
let name = "CstOp"
+ let gref = coq_CstOp
let table = table
let cast x = CstOp x
let dest = function CstOp x -> Some x | _ -> None
@@ -486,6 +517,7 @@ module EUnOp = struct
open EUnOpT
let name = "UnOp"
+ let gref = coq_UnOp
let table = table
let cast x = UnOp x
let dest = function UnOp x -> Some x | _ -> None
@@ -518,6 +550,7 @@ module EBinRel = struct
open EBinRelT
let name = "BinRel"
+ let gref = coq_BinRel
let table = table
let cast x = BinRel x
let dest = function BinRel x -> Some x | _ -> None
@@ -544,6 +577,7 @@ module EPropBinOp = struct
open EPropBinOpT
let name = "PropBinOp"
+ let gref = coq_PropBinOp
let table = table
let cast x = PropOp x
let dest = function PropOp x -> Some x | _ -> None
@@ -556,7 +590,8 @@ module EPropUnOp = struct
open EPropUnOpT
- let name = "PropUnOp"
+ let name = "PropUOp"
+ let gref = coq_PropUOp
let table = table
let cast x = PropUnOp x
let dest = function PropUnOp x -> Some x | _ -> None
@@ -567,7 +602,7 @@ end
let constr_of_term_kind = function Application c -> c | OtherTerm c -> c
module type S = sig
- val register : Constrexpr.constr_expr -> unit
+ val register : Libnames.qualid -> unit
val print : unit -> unit
end
@@ -589,14 +624,17 @@ module MakeTable (E : Elt) = struct
let register_hint evd t elt =
match EConstr.kind evd t with
| App (c, _) ->
- E.table := HConstr.add c (Application t, E.cast elt) !E.table
- | _ -> E.table := HConstr.add t (OtherTerm t, E.cast elt) !E.table
+ let gr = fst (EConstr.destRef evd c) in
+ E.table := ConstrMap.add gr (Application t, E.cast elt) !E.table
+ | _ ->
+ let gr = fst (EConstr.destRef evd t) in
+ E.table := ConstrMap.add gr (OtherTerm t, E.cast elt) !E.table
let register_constr env evd c =
let c = EConstr.of_constr c in
let t = get_type_of env evd c in
match EConstr.kind evd t with
- | App (intyp, args) ->
+ | App (intyp, args) when EConstr.isRefX evd (Lazy.force E.gref) intyp ->
let styp = args.(E.get_key) in
let elt = {decl = c; deriv = make_elt (evd, c)} in
register_hint evd styp elt
@@ -605,10 +643,11 @@ module MakeTable (E : Elt) = struct
raise
(CErrors.user_err
Pp.(
- str ": Cannot register term "
- ++ pr_constr env evd c ++ str ". It has type "
- ++ pr_constr env evd t
- ++ str " which should be of the form [F X1 .. Xn]"))
+ str "Cannot register " ++ pr_constr env evd c
+ ++ str ". It has type " ++ pr_constr env evd t
+ ++ str " instead of type "
+ ++ Printer.pr_global (Lazy.force E.gref)
+ ++ str " X1 ... Xn"))
let register_obj : Constr.constr -> Libobject.obj =
let cache_constr (_, c) =
@@ -622,22 +661,24 @@ module MakeTable (E : Elt) = struct
("register-zify-" ^ E.name)
~cache:cache_constr ~subst:(Some subst_constr)
- (** [register c] is called from the VERNACULAR ADD [name] constr(t).
+ (** [register c] is called from the VERNACULAR ADD [name] reference(t).
The term [c] is interpreted and
registered as a [superglobal_object_nodischarge].
TODO: pre-compute [get_type_of] - [cache_constr] is using another environment.
*)
let register c =
- let env = Global.env () in
- let evd = Evd.from_env env in
- let evd, c = Constrintern.interp_open_constr env evd c in
- let _ = Lib.add_anonymous_leaf (register_obj (EConstr.to_constr evd c)) in
- ()
+ try
+ let c = UnivGen.constr_of_monomorphic_global (Nametab.locate c) in
+ let _ = Lib.add_anonymous_leaf (register_obj c) in
+ ()
+ with Not_found ->
+ raise
+ (CErrors.user_err Pp.(Libnames.pr_qualid c ++ str " does not exist."))
let pp_keys () =
let env = Global.env () in
let evd = Evd.from_env env in
- HConstr.fold
+ ConstrMap.fold
(fun _ (k, d) acc ->
match E.dest d with
| None -> acc
@@ -656,6 +697,7 @@ module ESat = struct
open ESatT
let name = "Saturate"
+ let gref = coq_Saturate
let table = saturate
let cast x = Saturate x
let dest = function Saturate x -> Some x | _ -> None
@@ -669,6 +711,7 @@ module EUnopSpec = struct
type elt = ESpecT.t
let name = "UnopSpec"
+ let gref = coq_UnOpSpec
let table = specs
let cast x = UnOpSpec x
let dest = function UnOpSpec x -> Some x | _ -> None
@@ -682,6 +725,7 @@ module EBinOpSpec = struct
type elt = ESpecT.t
let name = "BinOpSpec"
+ let gref = coq_BinOpSpec
let table = specs
let cast x = BinOpSpec x
let dest = function BinOpSpec x -> Some x | _ -> None
@@ -947,9 +991,11 @@ let app_binop evd src binop arg1 prf1 arg2 prf2 =
type typed_constr = {constr : EConstr.t; typ : EConstr.t; inj : EInjT.t}
let get_injection env evd t =
- match snd (HConstr.find t !table_cache) with
- | InjTyp i -> i
- | _ -> raise Not_found
+ try
+ match snd (ConstrMap.find evd t !table_cache) with
+ | InjTyp i -> i
+ | _ -> raise Not_found
+ with DestKO -> raise Not_found
(* [arrow] is the term (fun (x:Prop) (y : Prop) => x -> y) *)
let arrow =
@@ -1087,7 +1133,7 @@ let declared_term env evd hd args =
| PropUnOp _ -> decomp t 1
| _ -> None )
in
- find_option match_operator (HConstr.find_all hd !table)
+ find_option match_operator (ConstrMap.find_all evd hd !table)
let rec trans_expr env evd e =
let inj = e.inj in
@@ -1099,7 +1145,7 @@ let rec trans_expr env evd e =
let k, t =
find_option
(match_operator env evd c a)
- (HConstr.find_all c !table_cache)
+ (ConstrMap.find_all evd c !table_cache)
in
let n = Array.length a in
match k with
@@ -1243,7 +1289,7 @@ let rec trans_prop env evd e =
let k, t =
find_option
(match_operator env evd c a)
- (HConstr.find_all c !table_cache)
+ (ConstrMap.find_all evd c !table_cache)
in
let n = Array.length a in
match k with
@@ -1262,7 +1308,7 @@ let rec trans_prop env evd e =
in
trans_binrel evd e rop a.(n - 2) a1 a.(n - 1) a2
| _ -> IProof
- with Not_found -> IProof )
+ with Not_found | DestKO -> IProof )
let trans_check_prop env evd t =
if is_prop env evd t then Some (trans_prop env evd t) else None
@@ -1359,7 +1405,7 @@ let do_let tac (h : Constr.named_declaration) =
find_option
(match_operator env evd eq
[|EConstr.of_constr ty; EConstr.mkVar x; EConstr.of_constr t|])
- (HConstr.find_all eq !table_cache));
+ (ConstrMap.find_all evd eq !table_cache));
tac x (EConstr.of_constr t) (EConstr.of_constr ty)
with Not_found -> Tacticals.New.tclIDTAC)
@@ -1453,12 +1499,12 @@ let rec spec_of_term env evd (senv : spec_env) t =
try (EConstr.mkVar (HConstr.find t' senv'.map), senv')
with Not_found -> (
try
- match snd (HConstr.find c !specs_cache) with
+ match snd (ConstrMap.find evd c !specs_cache) with
| UnOpSpec s | BinOpSpec s ->
let thm = EConstr.mkApp (s.deriv.ESpecT.spec, a') in
register_constr senv' t' thm
| _ -> (get_name t' senv', senv')
- with Not_found -> (t', senv') )
+ with Not_found | DestKO -> (t', senv') )
let interp_pscript s =
match s with
@@ -1493,47 +1539,58 @@ let spec_of_hyps =
let iter_specs = spec_of_hyps
let find_hyp evd t l =
- try Some (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l))
+ try
+ Some
+ (EConstr.mkVar
+ (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l)))
with Not_found -> None
-let sat_constr c d =
- Proofview.Goal.enter (fun gl ->
- let evd = Tacmach.New.project gl in
- let env = Tacmach.New.pf_env gl in
- let hyps = Tacmach.New.pf_hyps_types gl in
- match EConstr.kind evd c with
- | App (c, args) ->
- if Array.length args = 2 then
- let h1 =
- Tacred.cbv_beta env evd
- (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|]))
- in
- let h2 =
- Tacred.cbv_beta env evd
- (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|]))
- in
- match (find_hyp evd h1 hyps, find_hyp evd h2 hyps) with
- | Some h1, Some h2 ->
- let n =
- Tactics.fresh_id_in_env Id.Set.empty
- (Names.Id.of_string "__sat")
- env
- in
- let trm =
- EConstr.mkApp
- ( d.ESatT.satOK
- , [|args.(0); args.(1); EConstr.mkVar h1; EConstr.mkVar h2|] )
- in
- Tactics.pose_proof (Names.Name n) trm
- | _, _ -> Tacticals.New.tclIDTAC
- else Tacticals.New.tclIDTAC
- | _ -> Tacticals.New.tclIDTAC)
+let find_proof evd t l =
+ if EConstr.eq_constr evd t (Lazy.force op_True) then Some (Lazy.force op_I)
+ else find_hyp evd t l
+
+(** [sat_constr env evd sub taclist hyps c d]= (sub',taclist',hyps') where
+ - sub' is a fresh subscript obtained from sub
+ - taclist' is obtained from taclist by posing the lemma 'd' applied to 'c'
+ - hyps' is obtained from hyps'
+ taclist and hyps are threaded to avoid adding duplicates
+ *)
+let sat_constr env evd (sub,taclist, hyps) c d =
+ match EConstr.kind evd c with
+ | App (c, args) ->
+ if Array.length args = 2 then
+ let h1 =
+ Tacred.cbv_beta env evd
+ (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|]))
+ in
+ let h2 =
+ Tacred.cbv_beta env evd
+ (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|]))
+ in
+ let n = Nameops.add_subscript (Names.Id.of_string "__sat") sub in
+ let trm =
+ match (find_proof evd h1 hyps, find_proof evd h2 hyps) with
+ | Some h1, Some h2 ->
+ (EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1); h1; h2|]))
+ | Some h1, _ ->
+ EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1); h1|])
+ | _, _ -> EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1)|])
+ in
+ let rtrm = Tacred.cbv_beta env evd trm in
+ let typ = Retyping.get_type_of env evd rtrm in
+ match find_hyp evd typ hyps with
+ | None -> (Nameops.Subscript.succ sub, (Tactics.pose_proof (Names.Name n) rtrm :: taclist) , (n,typ)::hyps)
+ | Some _ -> (sub, taclist, hyps)
+ else (sub,taclist,hyps)
+ | _ -> (sub,taclist,hyps)
+
let get_all_sat env evd c =
List.fold_left
(fun acc e -> match e with _, Saturate s -> s :: acc | _ -> acc)
[]
- (HConstr.find_all c !saturate_cache)
+ ( try ConstrMap.find_all evd c !saturate_cache
+ with DestKO | Not_found -> [] )
let saturate =
Proofview.Goal.enter (fun gl ->
@@ -1550,8 +1607,10 @@ let saturate =
Array.iter sat args;
if Array.length args = 2 then
let ds = get_all_sat env evd c in
- if ds = [] then ()
- else List.iter (fun x -> CstrTable.HConstr.add table t x.deriv) ds
+ if ds = [] || CstrTable.HConstr.mem table t
+ then ()
+ else List.iter (fun x ->
+ CstrTable.HConstr.add table t x.deriv) ds
else ()
| Prod (a, t1, t2) when a.Context.binder_name = Names.Anonymous ->
sat t1; sat t2
@@ -1560,5 +1619,6 @@ let saturate =
(* Collect all the potential saturation lemma *)
sat concl;
List.iter (fun (_, t) -> sat t) hyps;
- Tacticals.New.tclTHENLIST
- (CstrTable.HConstr.fold (fun c d acc -> sat_constr c d :: acc) table []))
+ let s0 = fresh_subscript env in
+ let (_,tacs,_) = CstrTable.HConstr.fold (fun c d acc -> sat_constr env evd acc c d) table (s0,[],hyps) in
+ Tacticals.New.tclTHENLIST tacs)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:00:40 +0000