aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/formula.ml23
-rw-r--r--plugins/firstorder/instances.ml15
-rw-r--r--plugins/firstorder/rules.ml25
-rw-r--r--plugins/firstorder/sequent.ml6
-rw-r--r--plugins/firstorder/unify.ml18
5 files changed, 54 insertions, 33 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index b34a36492..87bac2fe3 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -54,7 +54,7 @@ let construct_nhyps ind gls =
let ind_hyps nevar ind largs gls=
let types= Inductiveops.arities_of_constructors (pf_env gls) ind in
let myhyps t =
- let t1=prod_applist t largs in
+ let t1=Term.prod_applist t largs in
let t2=snd (decompose_prod_n_assum nevar t1) in
fst (decompose_prod_assum t2) in
Array.map myhyps types
@@ -76,18 +76,21 @@ type kind_of_formula=
| Forall of constr*constr
| Atom of constr
+let pop t = Vars.lift (-1) t
+
let kind_of_formula gl term =
let normalize=special_nf gl in
let cciterm=special_whd gl term in
- match match_with_imp_term cciterm with
- Some (a,b)-> Arrow(a,(pop b))
+ match match_with_imp_term (project gl) (EConstr.of_constr cciterm) with
+ Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop (EConstr.Unsafe.to_constr b)))
|_->
- match match_with_forall_term cciterm with
- Some (_,a,b)-> Forall(a,b)
+ match match_with_forall_term (project gl) (EConstr.of_constr cciterm) with
+ Some (_,a,b)-> Forall(EConstr.Unsafe.to_constr a,EConstr.Unsafe.to_constr b)
|_->
- match match_with_nodep_ind cciterm with
+ match match_with_nodep_ind (project gl) (EConstr.of_constr cciterm) with
Some (i,l,n)->
- let ind,u=destInd i in
+ let l = List.map EConstr.Unsafe.to_constr l in
+ let ind,u=EConstr.destInd (project gl) i in
let (mib,mip) = Global.lookup_inductive ind in
let nconstr=Array.length mip.mind_consnames in
if Int.equal nconstr 0 then
@@ -96,7 +99,7 @@ let kind_of_formula gl term =
let has_realargs=(n>0) in
let is_trivial=
let is_constant c =
- Int.equal (nb_prod c) mib.mind_nparams in
+ Int.equal (nb_prod (project gl) (EConstr.of_constr c)) mib.mind_nparams in
Array.exists is_constant mip.mind_nf_lc in
if Inductiveops.mis_is_recursive (ind,mib,mip) ||
(has_realargs && not is_trivial)
@@ -108,8 +111,8 @@ let kind_of_formula gl term =
else
Or((ind,u),l,is_trivial)
| _ ->
- match match_with_sigma_type cciterm with
- Some (i,l)-> Exists((destInd i),l)
+ match match_with_sigma_type (project gl) (EConstr.of_constr cciterm) with
+ Some (i,l)-> Exists((EConstr.destInd (project gl) i),List.map EConstr.Unsafe.to_constr l)
|_-> Atom (normalize cciterm)
type atoms = {positive:constr list;negative:constr list}
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index eebd974ea..9dc2a51a6 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t=
let typ=pf_unsafe_type_of gl idc in
(* since we know we will get a product,
reduction is not too expensive *)
- let (nam,_,_)=destProd (whd_all env evmap typ) in
+ let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap typ)) in
match nam with
Name id -> id
| Anonymous -> dummy_bvid in
@@ -119,19 +119,20 @@ let mk_open_instance id idc gl m t=
let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
let evmap = Sigma.to_evar_map evmap in
let decl = LocalAssum (Name nid, c) in
- aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
+ aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
let evmap, decls = aux m [] env evmap [] in
evmap, decls, revt
(* tactics *)
let left_instance_tac (inst,id) continue seq=
+ let open EConstr in
match inst with
Phantom dom->
if lookup (id,None) seq then
tclFAIL 0 (Pp.str "already done")
else
- tclTHENS (Proofview.V82.of_tactic (cut dom))
+ tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom)))
[tclTHENLIST
[Proofview.V82.of_tactic introf;
pf_constr_of_global id (fun idc ->
@@ -151,6 +152,7 @@ let left_instance_tac (inst,id) continue seq=
pf_constr_of_global id (fun idc ->
fun gl->
let evmap,rc,ot = mk_open_instance id idc gl m t in
+ let ot = EConstr.of_constr ot in
let gt=
it_mkLambda_or_LetIn
(mkApp(idc,[|ot|])) rc in
@@ -160,6 +162,7 @@ let left_instance_tac (inst,id) continue seq=
error "Untypable instance, maybe higher-order non-prenex quantification" in
tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
else
+ let t = EConstr.of_constr t in
pf_constr_of_global id (fun idc ->
Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])]))
in
@@ -172,16 +175,16 @@ let left_instance_tac (inst,id) continue seq=
let right_instance_tac inst continue seq=
match inst with
Phantom dom ->
- tclTHENS (Proofview.V82.of_tactic (cut dom))
+ tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom)))
[tclTHENLIST
[Proofview.V82.of_tactic introf;
(fun gls->
Proofview.V82.of_tactic (split (ImplicitBindings
- [mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls);
+ [EConstr.mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls);
tclSOLVE [wrap 0 true continue (deepen seq)]];
tclTRY (Proofview.V82.of_tactic assumption)]
| Real ((0,t),_) ->
- (tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [t])))
+ (tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr t])))
(tclSOLVE [wrap 0 true continue (deepen seq)]))
| Real ((m,t),_) ->
tclFAIL 0 (Pp.str "not implemented ... yet")
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 7ffc78928..a60fd4d8f 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -38,14 +38,14 @@ let wrap n b continue seq gls=
[]->anomaly (Pp.str "Not the expected number of hyps")
| nd::q->
let id = NamedDecl.get_id nd in
- if occur_var env id (pf_concl gls) ||
- List.exists (occur_var_in_decl env id) ctx then
+ if occur_var env (project gls) id (pf_concl gls) ||
+ List.exists (occur_var_in_decl env (project gls) id) ctx then
(aux (i-1) q (nd::ctx))
else
- add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in
+ add_formula Hyp (VarRef id) (EConstr.Unsafe.to_constr (NamedDecl.get_type nd)) (aux (i-1) q (nd::ctx)) gls in
let seq1=aux n nc [] in
let seq2=if b then
- add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
+ add_formula Concl dummy_id (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in
continue seq2 gls
let basename_of_global=function
@@ -63,12 +63,13 @@ let axiom_tac t seq=
with Not_found->tclFAIL 0 (Pp.str "No axiom link")
let ll_atom_tac a backtrack id continue seq=
+ let open EConstr in
tclIFTHENELSE
(try
tclTHENLIST
[pf_constr_of_global (find_left a seq) (fun left ->
pf_constr_of_global id (fun id ->
- Proofview.V82.of_tactic (generalize [mkApp(id, [|left|])])));
+ Proofview.V82.of_tactic (generalize [(mkApp(id, [|left|]))])));
clear_global id;
Proofview.V82.of_tactic intro]
with Not_found->tclFAIL 0 (Pp.str "No link"))
@@ -131,9 +132,9 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
let vars=Array.init p (fun j->mkRel (p-j)) in
let capply=mkApp ((lift p cstr),vars) in
let head=mkApp ((lift p idc),[|capply|]) in
- it_mkLambda_or_LetIn head rc in
+ EConstr.of_constr (it_mkLambda_or_LetIn head rc) in
let lp=Array.length rcs in
- let newhyps idc =List.init lp (myterm idc) in
+ let newhyps idc =List.init lp (myterm (EConstr.Unsafe.to_constr idc)) in
tclIFTHENELSE
(tclTHENLIST
[pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc)));
@@ -142,8 +143,13 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
(wrap lp false continue seq) backtrack gl
let ll_arrow_tac a b c backtrack id continue seq=
+ let open EConstr in
+ let open Vars in
+ let a = EConstr.of_constr a in
+ let b = EConstr.of_constr b in
+ let c = EConstr.of_constr c in
let cc=mkProd(Anonymous,a,(lift 1 b)) in
- let d idc =mkLambda (Anonymous,b,
+ let d idc = mkLambda (Anonymous,b,
mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
tclORELSE
(tclTHENS (Proofview.V82.of_tactic (cut c))
@@ -186,11 +192,12 @@ let left_exists_tac ind backtrack id continue seq gls=
let ll_forall_tac prod backtrack id continue seq=
tclORELSE
- (tclTHENS (Proofview.V82.of_tactic (cut prod))
+ (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr prod)))
[tclTHENLIST
[Proofview.V82.of_tactic intro;
pf_constr_of_global id (fun idc ->
(fun gls->
+ let open EConstr in
let id0=pf_nth_hyp_id gls 1 in
let term=mkApp(idc,[|mkVar(id0)|]) in
tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls));
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 1248b60a7..fb0c22c2b 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -200,7 +200,8 @@ let extend_with_ref_list l seq gl =
let l = expand_constructor_hints l in
let f gr (seq,gl) =
let gl, c = pf_eapply Evd.fresh_global gl gr in
- let typ=(pf_unsafe_type_of gl c) in
+ let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
+ let typ = EConstr.Unsafe.to_constr typ in
(add_formula Hyp gr typ seq gl,gl) in
List.fold_right f l (seq,gl)
@@ -214,8 +215,9 @@ let extend_with_auto_hints l seq gl=
| Res_pf_THEN_trivial_fail (c,_) ->
let (c, _, _) = c in
(try
- let gr = global_of_constr c in
+ let (gr, _) = Termops.global_of_constr (project gl) c in
let typ=(pf_unsafe_type_of gl c) in
+ let typ = EConstr.Unsafe.to_constr typ in
seqref:=add_formula Hint gr typ !seqref gl
with Not_found->())
| _-> () in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index d9ab36ad6..7cbfb8e7d 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -21,7 +21,13 @@ exception UFAIL of constr*constr
to the equation set. Raises UFAIL with a pair of terms
*)
+let strip_outer_cast t =
+ EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *)
+
+let pop t = Vars.lift (-1) t
+
let unif t1 t2=
+ let evd = Evd.empty in (** FIXME *)
let bige=Queue.create ()
and sigma=ref [] in
let bind i t=
@@ -38,8 +44,8 @@ let unif t1 t2=
Queue.add (t1,t2) bige;
try while true do
let t1,t2=Queue.take bige in
- let nt1=head_reduce (whd_betaiotazeta Evd.empty t1)
- and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in
+ let nt1=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t1)))
+ and nt2=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t2))) in
match (kind_of_term nt1),(kind_of_term nt2) with
Meta i,Meta j->
if not (Int.equal i j) then
@@ -47,13 +53,13 @@ let unif t1 t2=
else bind i nt2
| Meta i,_ ->
let t=subst_meta !sigma nt2 in
- if Int.Set.is_empty (free_rels t) &&
- not (occur_term (mkMeta i) t) then
+ if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) &&
+ not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then
bind i t else raise (UFAIL(nt1,nt2))
| _,Meta i ->
let t=subst_meta !sigma nt1 in
- if Int.Set.is_empty (free_rels t) &&
- not (occur_term (mkMeta i) t) then
+ if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) &&
+ not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then
bind i t else raise (UFAIL(nt1,nt2))
| Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
| _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 09:08:29 +0000