aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder/instances.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/instances.ml')
-rw-r--r--plugins/firstorder/instances.ml126
1 files changed, 63 insertions, 63 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index eff0db5bf4..e131cad7da 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -26,13 +26,13 @@ open Context.Rel.Declaration
let compare_instance inst1 inst2=
let cmp c1 c2 = Constr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
- match inst1,inst2 with
- Phantom(d1),Phantom(d2)->
- (cmp d1 d2)
- | Real((m1,c1),n1),Real((m2,c2),n2)->
- ((-) =? (-) ==? cmp) m2 m1 n1 n2 c1 c2
- | Phantom(_),Real((m,_),_)-> if Int.equal m 0 then -1 else 1
- | Real((m,_),_),Phantom(_)-> if Int.equal m 0 then 1 else -1
+ match inst1,inst2 with
+ Phantom(d1),Phantom(d2)->
+ (cmp d1 d2)
+ | Real((m1,c1),n1),Real((m2,c2),n2)->
+ ((-) =? (-) ==? cmp) m2 m1 n1 n2 c1 c2
+ | Phantom(_),Real((m,_),_)-> if Int.equal m 0 then -1 else 1
+ | Real((m,_),_),Phantom(_)-> if Int.equal m 0 then 1 else -1
let compare_gr id1 id2 =
if id1==id2 then 0 else
@@ -53,7 +53,7 @@ module IS=Set.Make(OrderedInstance)
let make_simple_atoms seq=
let ratoms=
match seq.glatom with
- Some t->[t]
+ Some t->[t]
| None->[]
in {negative=seq.latoms;positive=ratoms}
@@ -63,9 +63,9 @@ let do_sequent sigma setref triv id seq i dom atoms=
let do_atoms a1 a2 =
let do_pair t1 t2 =
match unif_atoms sigma i dom t1 t2 with
- None->()
- | Some (Phantom _) ->phref:=true
- | Some c ->flag:=false;setref:=IS.add (c,id) !setref in
+ None->()
+ | Some (Phantom _) ->phref:=true
+ | Some c ->flag:=false;setref:=IS.add (c,id) !setref in
List.iter (fun t->List.iter (do_pair t) a2.negative) a1.positive;
List.iter (fun t->List.iter (do_pair t) a2.positive) a1.negative in
HP.iter (fun lf->do_atoms atoms lf.atoms) seq.redexes;
@@ -75,8 +75,8 @@ let do_sequent sigma setref triv id seq i dom atoms=
let match_one_quantified_hyp sigma setref seq lf=
match lf.pat with
Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
- if do_sequent sigma setref triv lf.id seq i dom lf.atoms then
- setref:=IS.add ((Phantom dom),lf.id) !setref
+ if do_sequent sigma setref triv lf.id seq i dom lf.atoms then
+ setref:=IS.add ((Phantom dom),lf.id) !setref
| _ -> anomaly (Pp.str "can't happen.")
let give_instances sigma lf seq=
@@ -90,10 +90,10 @@ let rec collect_quantified sigma seq=
try
let hd,seq1=take_formula sigma seq in
(match hd.pat with
- Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) ->
- let (q,seq2)=collect_quantified sigma seq1 in
- ((hd::q),seq2)
- | _->[],seq)
+ Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) ->
+ let (q,seq2)=collect_quantified sigma seq1 in
+ ((hd::q),seq2)
+ | _->[],seq)
with Heap.EmptyHeap -> [],seq
(* open instances processor *)
@@ -104,19 +104,19 @@ let mk_open_instance env evmap id idc m t =
let var_id=
if id==dummy_id then dummy_bvid else
let typ=Typing.unsafe_type_of env evmap idc in
- (* since we know we will get a product,
- reduction is not too expensive *)
+ (* since we know we will get a product,
+ reduction is not too expensive *)
let (nam,_,_)=destProd evmap (whd_all env evmap typ) in
match nam.Context.binder_name with
- Name id -> id
- | Anonymous -> dummy_bvid in
+ Name id -> id
+ | Anonymous -> dummy_bvid in
let revt=substl (List.init m (fun i->mkRel (m-i))) t in
let rec aux n avoid env evmap decls =
if Int.equal n 0 then evmap, decls else
let nid=(fresh_id_in_env avoid var_id env) in
let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
let decl = LocalAssum (Context.make_annot (Name nid) Sorts.Relevant, c) in
- aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
+ aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
let evmap, decls = aux m Id.Set.empty env evmap [] in
(evmap, decls, revt)
@@ -128,49 +128,49 @@ let left_instance_tac (inst,id) continue seq=
let sigma = project gl in
match inst with
Phantom dom->
- if lookup sigma (id,None) seq then
- tclFAIL 0 (Pp.str "already done")
- else
- tclTHENS (cut dom)
- [tclTHENLIST
- [introf;
+ if lookup sigma (id,None) seq then
+ tclFAIL 0 (Pp.str "already done")
+ else
+ tclTHENS (cut dom)
+ [tclTHENLIST
+ [introf;
(pf_constr_of_global id >>= fun idc ->
Proofview.Goal.enter begin fun gl ->
let id0 = List.nth (pf_ids_of_hyps gl) 0 in
generalize [mkApp(idc, [|mkVar id0|])]
end);
- introf;
- tclSOLVE [wrap 1 false continue
- (deepen (record (id,None) seq))]];
- tclTRY assumption]
+ introf;
+ tclSOLVE [wrap 1 false continue
+ (deepen (record (id,None) seq))]];
+ tclTRY assumption]
| Real((m,t),_)->
let c = (m, EConstr.to_constr sigma t) in
- if lookup sigma (id,Some c) seq then
- tclFAIL 0 (Pp.str "already done")
- else
- let special_generalize=
- if m>0 then
- (pf_constr_of_global id >>= fun idc ->
- Proofview.Goal.enter begin fun gl->
- let (evmap, rc, ot) = mk_open_instance (pf_env gl) (project gl) id idc m t in
- let gt=
- it_mkLambda_or_LetIn
- (mkApp(idc,[|ot|])) rc in
- let evmap, _ =
- try Typing.type_of (pf_env gl) evmap gt
- with e when CErrors.noncritical e ->
- user_err Pp.(str "Untypable instance, maybe higher-order non-prenex quantification") in
+ if lookup sigma (id,Some c) seq then
+ tclFAIL 0 (Pp.str "already done")
+ else
+ let special_generalize=
+ if m>0 then
+ (pf_constr_of_global id >>= fun idc ->
+ Proofview.Goal.enter begin fun gl->
+ let (evmap, rc, ot) = mk_open_instance (pf_env gl) (project gl) id idc m t in
+ let gt=
+ it_mkLambda_or_LetIn
+ (mkApp(idc,[|ot|])) rc in
+ let evmap, _ =
+ try Typing.type_of (pf_env gl) evmap gt
+ with e when CErrors.noncritical e ->
+ user_err Pp.(str "Untypable instance, maybe higher-order non-prenex quantification") in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evmap)
- (generalize [gt])
+ (generalize [gt])
end)
- else
- pf_constr_of_global id >>= fun idc -> generalize [mkApp(idc,[|t|])]
- in
- tclTHENLIST
- [special_generalize;
- introf;
- tclSOLVE
- [wrap 1 false continue (deepen (record (id,Some c) seq))]]
+ else
+ pf_constr_of_global id >>= fun idc -> generalize [mkApp(idc,[|t|])]
+ in
+ tclTHENLIST
+ [special_generalize;
+ introf;
+ tclSOLVE
+ [wrap 1 false continue (deepen (record (id,Some c) seq))]]
end
let right_instance_tac inst continue seq=
@@ -178,20 +178,20 @@ let right_instance_tac inst continue seq=
Proofview.Goal.enter begin fun gl ->
match inst with
Phantom dom ->
- tclTHENS (cut dom)
- [tclTHENLIST
- [introf;
+ tclTHENS (cut dom)
+ [tclTHENLIST
+ [introf;
Proofview.Goal.enter begin fun gl ->
let id0 = List.nth (pf_ids_of_hyps gl) 0 in
split (Tactypes.ImplicitBindings [mkVar id0])
end;
- tclSOLVE [wrap 0 true continue (deepen seq)]];
- tclTRY assumption]
+ tclSOLVE [wrap 0 true continue (deepen seq)]];
+ tclTRY assumption]
| Real ((0,t),_) ->
(tclTHEN (split (Tactypes.ImplicitBindings [t]))
- (tclSOLVE [wrap 0 true continue (deepen seq)]))
+ (tclSOLVE [wrap 0 true continue (deepen seq)]))
| Real ((m,t),_) ->
- tclFAIL 0 (Pp.str "not implemented ... yet")
+ tclFAIL 0 (Pp.str "not implemented ... yet")
end
let instance_tac inst=
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:45:04 +0000