diff options
author | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
commit | 72b9a7df489ea47b3e5470741fd39f6100d31676 (patch) | |
tree | 60108a573d2a80d2dd4e3833649890e32427ff8d /contrib | |
parent | 55ce117e8083477593cf1ff2e51a3641c7973830 (diff) |
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'contrib')
46 files changed, 2339 insertions, 1704 deletions
diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml index 1ffa347a..d336f599 100644 --- a/contrib/cc/ccproof.ml +++ b/contrib/cc/ccproof.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccproof.ml 9151 2006-09-19 13:32:22Z corbinea $ *) +(* $Id: ccproof.ml 9856 2007-05-24 14:05:40Z corbinea $ *) (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) @@ -16,58 +16,107 @@ open Names open Term open Ccalgo -type proof= +type rule= Ax of constr | SymAx of constr | Refl of term | Trans of proof*proof | Congr of proof*proof | Inject of proof*constructor*int*int - -let pcongr=function - Refl t1, Refl t2 -> Refl (Appli (t1,t2)) - | p1, p2 -> Congr (p1,p2) - -let rec ptrans=function - Refl _, p ->p - | p, Refl _ ->p - | Trans(p1,p2), p3 ->ptrans(p1,ptrans (p2,p3)) - | Congr(p1,p2), Congr(p3,p4) ->pcongr(ptrans(p1,p3),ptrans(p2,p4)) - | Congr(p1,p2), Trans(Congr(p3,p4),p5) -> - ptrans(pcongr(ptrans(p1,p3),ptrans(p2,p4)),p5) - | p1, p2 ->Trans (p1,p2) - -let rec psym=function - Refl p->Refl p - | SymAx s->Ax s - | Ax s-> SymAx s - | Inject (p,c,n,a)-> Inject (psym p,c,n,a) - | Trans (p1,p2)-> ptrans (psym p2,psym p1) - | Congr (p1,p2)-> pcongr (psym p1,psym p2) +and proof = + {p_lhs:term;p_rhs:term;p_rule:rule} + +let prefl t = {p_lhs=t;p_rhs=t;p_rule=Refl t} + +let pcongr p1 p2 = + match p1.p_rule,p2.p_rule with + Refl t1, Refl t2 -> prefl (Appli (t1,t2)) + | _, _ -> + {p_lhs=Appli (p1.p_lhs,p2.p_lhs); + p_rhs=Appli (p1.p_rhs,p2.p_rhs); + p_rule=Congr (p1,p2)} + +let rec ptrans p1 p3= + match p1.p_rule,p3.p_rule with + Refl _, _ ->p3 + | _, Refl _ ->p1 + | Trans(p1,p2), _ ->ptrans p1 (ptrans p2 p3) + | Congr(p1,p2), Congr(p3,p4) ->pcongr (ptrans p1 p3) (ptrans p2 p4) + | Congr(p1,p2), Trans({p_rule=Congr(p3,p4)},p5) -> + ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5 + | _, _ -> + if p1.p_rhs = p3.p_lhs then + {p_lhs=p1.p_lhs; + p_rhs=p3.p_rhs; + p_rule=Trans (p1,p3)} + else anomaly "invalid cc transitivity" -let pcongr=function - Refl t1, Refl t2 ->Refl (Appli (t1,t2)) - | p1, p2 -> Congr (p1,p2) +let rec psym p = + match p.p_rule with + Refl _ -> p + | SymAx s -> + {p_lhs=p.p_rhs; + p_rhs=p.p_lhs; + p_rule=Ax s} + | Ax s-> + {p_lhs=p.p_rhs; + p_rhs=p.p_lhs; + p_rule=SymAx s} + | Inject (p0,c,n,a)-> + {p_lhs=p.p_rhs; + p_rhs=p.p_lhs; + p_rule=Inject (psym p0,c,n,a)} + | Trans (p1,p2)-> ptrans (psym p2) (psym p1) + | Congr (p1,p2)-> pcongr (psym p1) (psym p2) + +let pax axioms s = + let l,r = Hashtbl.find axioms s in + {p_lhs=l; + p_rhs=r; + p_rule=Ax s} + +let psymax axioms s = + let l,r = Hashtbl.find axioms s in + {p_lhs=r; + p_rhs=l; + p_rule=SymAx s} + +let rec nth_arg t n= + match t with + Appli (t1,t2)-> + if n>0 then + nth_arg t1 (n-1) + else t2 + | _ -> anomaly "nth_arg: not enough args" + +let pinject p c n a = + {p_lhs=nth_arg p.p_lhs (n-a); + p_rhs=nth_arg p.p_rhs (n-a); + p_rule=Inject(p,c,n,a)} let build_proof uf= - + + let axioms = axioms uf in + let rec equal_proof i j= - if i=j then Refl (term uf i) else + if i=j then prefl (term uf i) else let (li,lj)=join_path uf i j in - ptrans (path_proof i li,psym (path_proof j lj)) + ptrans (path_proof i li) (psym (path_proof j lj)) and edge_proof ((i,j),eq)= let pi=equal_proof i eq.lhs in let pj=psym (equal_proof j eq.rhs) in let pij= match eq.rule with - Axiom (s,reversed)->if reversed then SymAx s else Ax s + Axiom (s,reversed)-> + if reversed then psymax axioms s + else pax axioms s | Congruence ->congr_proof eq.lhs eq.rhs | Injection (ti,ipac,tj,jpac,k) -> let p=ind_proof ti ipac tj jpac in let cinfo= get_constructor_info uf ipac.cnode in - Inject(p,cinfo.ci_constr,cinfo.ci_nhyps,k) - in ptrans(ptrans (pi,pij),pj) + pinject p cinfo.ci_constr cinfo.ci_nhyps k + in ptrans (ptrans pi pij) pj and constr_proof i t ipac= if ipac.args=[] then @@ -79,49 +128,26 @@ let build_proof uf= let rj=find uf j in let u=find_pac uf rj npac in let p=constr_proof j u npac in - ptrans (equal_proof i t, pcongr (p,Refl targ)) + ptrans (equal_proof i t) (pcongr p (prefl targ)) and path_proof i=function - [] -> Refl (term uf i) - | x::q->ptrans (path_proof (snd (fst x)) q,edge_proof x) + [] -> prefl (term uf i) + | x::q->ptrans (path_proof (snd (fst x)) q) (edge_proof x) and congr_proof i j= let (i1,i2) = subterms uf i and (j1,j2) = subterms uf j in - pcongr (equal_proof i1 j1, equal_proof i2 j2) + pcongr (equal_proof i1 j1) (equal_proof i2 j2) and ind_proof i ipac j jpac= let p=equal_proof i j and p1=constr_proof i i ipac and p2=constr_proof j j jpac in - ptrans(psym p1,ptrans(p,p2)) + ptrans (psym p1) (ptrans p p2) in function `Prove (i,j) -> equal_proof i j | `Discr (i,ci,j,cj)-> ind_proof i ci j cj -let rec nth_arg t n= - match t with - Appli (t1,t2)-> - if n>0 then - nth_arg t1 (n-1) - else t2 - | _ -> anomaly "nth_arg: not enough args" -let rec type_proof axioms p= - match p with - Ax s->Hashtbl.find axioms s - | SymAx s-> let (t1,t2)=Hashtbl.find axioms s in (t2,t1) - | Refl t-> t,t - | Trans (p1,p2)-> - let (s1,t1)=type_proof axioms p1 - and (t2,s2)=type_proof axioms p2 in - if t1=t2 then (s1,s2) else anomaly "invalid cc transitivity" - | Congr (p1,p2)-> - let (i1,j1)=type_proof axioms p1 - and (i2,j2)=type_proof axioms p2 in - Appli (i1,i2),Appli (j1,j2) - | Inject (p,c,n,a)-> - let (ti,tj)=type_proof axioms p in - nth_arg ti (n-a),nth_arg tj (n-a) diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli index abdd6fea..572b2c53 100644 --- a/contrib/cc/ccproof.mli +++ b/contrib/cc/ccproof.mli @@ -6,26 +6,26 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccproof.mli 9151 2006-09-19 13:32:22Z corbinea $ *) +(* $Id: ccproof.mli 9856 2007-05-24 14:05:40Z corbinea $ *) open Ccalgo open Names open Term -type proof = +type rule= Ax of constr | SymAx of constr | Refl of term - | Trans of proof * proof - | Congr of proof * proof - | Inject of proof * constructor * int * int + | Trans of proof*proof + | Congr of proof*proof + | Inject of proof*constructor*int*int +and proof = + private {p_lhs:term;p_rhs:term;p_rule:rule} val build_proof : forest -> [ `Discr of int * pa_constructor * int * pa_constructor | `Prove of int * int ] -> proof -val type_proof : - (constr, (term * term)) Hashtbl.t -> proof -> term * term diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml index ea8aceeb..86251254 100644 --- a/contrib/cc/cctac.ml +++ b/contrib/cc/cctac.ml @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: cctac.ml 9151 2006-09-19 13:32:22Z corbinea $ *) +(* $Id: cctac.ml 9856 2007-05-24 14:05:40Z corbinea $ *) (* This file is the interface between the c-c algorithm and Coq *) @@ -37,6 +37,12 @@ let _f_equal = constant ["Init";"Logic"] "f_equal" let _eq_rect = constant ["Init";"Logic"] "eq_rect" +let _refl_equal = constant ["Init";"Logic"] "refl_equal" + +let _sym_eq = constant ["Init";"Logic"] "sym_eq" + +let _trans_eq = constant ["Init";"Logic"] "trans_eq" + let _eq = constant ["Init";"Logic"] "eq" let _False = constant ["Init";"Logic"] "False" @@ -210,54 +216,73 @@ let build_projection intype outtype (cstr:constructor) special default gls= (* generate an adhoc tactic following the proof tree *) -let rec proof_tac axioms=function - Ax c -> exact_check c - | SymAx c -> tclTHEN symmetry (exact_check c) - | Refl t -> reflexivity - | Trans (p1,p2)->let t=(constr_of_term (snd (type_proof axioms p1))) in - (tclTHENS (transitivity t) - [(proof_tac axioms p1);(proof_tac axioms p2)]) - | Congr (p1,p2)-> - fun gls-> - let (f1,f2)=(type_proof axioms p1) - and (x1,x2)=(type_proof axioms p2) in - let tf1=constr_of_term f1 and tx1=constr_of_term x1 - and tf2=constr_of_term f2 and tx2=constr_of_term x2 in - let typf=pf_type_of gls tf1 and typx=pf_type_of gls tx1 - and typfx=pf_type_of gls (mkApp(tf1,[|tx1|])) in - let id=pf_get_new_id (id_of_string "f") gls in - let appx1=mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in - let lemma1= - mkApp(Lazy.force _f_equal,[|typf;typfx;appx1;tf1;tf2|]) - and lemma2= - mkApp(Lazy.force _f_equal,[|typx;typfx;tf2;tx1;tx2|]) in - (tclTHENS (transitivity (mkApp(tf2,[|tx1|]))) - [tclTHEN (apply lemma1) (proof_tac axioms p1); - tclFIRST - [tclTHEN (apply lemma2) (proof_tac axioms p2); - reflexivity; - fun gls -> - errorlabstrm "Congruence" - (Pp.str - "I don't know how to handle dependent equality")]] - gls) - | Inject (prf,cstr,nargs,argind) as gprf-> - (fun gls -> - let ti,tj=type_proof axioms prf in - let ai,aj=type_proof axioms gprf in - let cti=constr_of_term ti in - let ctj=constr_of_term tj in - let cai=constr_of_term ai in - let intype=pf_type_of gls cti in - let outtype=pf_type_of gls cai in +let _M =mkMeta + +let rec proof_tac p gls = + match p.p_rule with + Ax c -> exact_check c gls + | SymAx c -> + let l=constr_of_term p.p_lhs and + r=constr_of_term p.p_rhs in + let typ = pf_type_of gls l in + exact_check + (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls + | Refl t -> + let lr = constr_of_term t in + let typ = pf_type_of gls lr in + exact_check + (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls + | Trans (p1,p2)-> + let t1 = constr_of_term p1.p_lhs and + t2 = constr_of_term p1.p_rhs and + t3 = constr_of_term p2.p_rhs in + let typ = pf_type_of gls t2 in + let prf = + mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in + tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls + | Congr (p1,p2)-> + let tf1=constr_of_term p1.p_lhs + and tx1=constr_of_term p2.p_lhs + and tf2=constr_of_term p1.p_rhs + and tx2=constr_of_term p2.p_rhs in + let typf = pf_type_of gls tf1 in + let typx = pf_type_of gls tx1 in + let typfx = prod_applist typf [tx1] in + let id = pf_get_new_id (id_of_string "f") gls in + let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in + let lemma1 = + mkApp(Lazy.force _f_equal, + [|typf;typfx;appx1;tf1;tf2;_M 1|]) in + let lemma2= + mkApp(Lazy.force _f_equal,[|typx;typfx;tf2;tx1;tx2;_M 1|]) in + let prf = + mkApp(Lazy.force _trans_eq, + [|typfx; + mkApp(tf1,[|tx1|]); + mkApp(tf2,[|tx1|]); + mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in + tclTHENS (refine prf) + [tclTHEN (refine lemma1) (proof_tac p1); + tclFIRST + [tclTHEN (refine lemma2) (proof_tac p2); + reflexivity; + fun gls -> + errorlabstrm "Congruence" + (Pp.str + "I don't know how to handle dependent equality")]] gls + | Inject (prf,cstr,nargs,argind) -> + let ti=constr_of_term prf.p_lhs in + let tj=constr_of_term prf.p_rhs in + let default=constr_of_term p.p_lhs in + let intype=pf_type_of gls ti in + let outtype=pf_type_of gls default in let special=mkRel (1+nargs-argind) in - let default=constr_of_term ai in let proj=build_projection intype outtype cstr special default gls in let injt= - mkApp (Lazy.force _f_equal,[|intype;outtype;proj;cti;ctj|]) in - tclTHEN (apply injt) (proof_tac axioms prf) gls) + mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in + tclTHEN (refine injt) (proof_tac prf) gls -let refute_tac axioms c t1 t2 p gls = +let refute_tac c t1 t2 p gls = let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let intype=pf_type_of gls tt1 in let neweq= @@ -266,9 +291,9 @@ let refute_tac axioms c t1 t2 p gls = let hid=pf_get_new_id (id_of_string "Heq") gls in let false_t=mkApp (c,[|mkVar hid|]) in tclTHENS (true_cut (Name hid) neweq) - [proof_tac axioms p; simplest_elim false_t] gls + [proof_tac p; simplest_elim false_t] gls -let convert_to_goal_tac axioms c t1 t2 p gls = +let convert_to_goal_tac c t1 t2 p gls = let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let sort=pf_type_of gls tt2 in let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in @@ -278,20 +303,19 @@ let convert_to_goal_tac axioms c t1 t2 p gls = let endt=mkApp (Lazy.force _eq_rect, [|sort;tt1;identity;c;tt2;mkVar e|]) in tclTHENS (true_cut (Name e) neweq) - [proof_tac axioms p;exact_check endt] gls + [proof_tac p;exact_check endt] gls -let convert_to_hyp_tac axioms c1 t1 c2 t2 p gls = +let convert_to_hyp_tac c1 t1 c2 t2 p gls = let tt2=constr_of_term t2 in let h=pf_get_new_id (id_of_string "H") gls in let false_t=mkApp (c2,[|mkVar h|]) in tclTHENS (true_cut (Name h) tt2) - [convert_to_goal_tac axioms c1 t1 t2 p; + [convert_to_goal_tac c1 t1 t2 p; simplest_elim false_t] gls -let discriminate_tac axioms cstr p gls = - let t1,t2=type_proof axioms p in - let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let intype=pf_type_of gls tt1 in +let discriminate_tac cstr p gls = + let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in + let intype=pf_type_of gls t1 in let concl=pf_concl gls in let outsort=mkType (new_univ ()) in let xid=pf_get_new_id (id_of_string "X") gls in @@ -303,12 +327,12 @@ let discriminate_tac axioms cstr p gls = let hid=pf_get_new_id (id_of_string "Heq") gls in let proj=build_projection intype outtype cstr trivial concl gls in let injt=mkApp (Lazy.force _f_equal, - [|intype;outtype;proj;tt1;tt2;mkVar hid|]) in + [|intype;outtype;proj;t1;t2;mkVar hid|]) in let endt=mkApp (Lazy.force _eq_rect, [|outtype;trivial;pred;identity;concl;injt|]) in - let neweq=mkApp(Lazy.force _eq,[|intype;tt1;tt2|]) in + let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in tclTHENS (true_cut (Name hid) neweq) - [proof_tac axioms p;exact_check endt] gls + [proof_tac p;exact_check endt] gls (* wrap everything *) @@ -333,12 +357,12 @@ let cc_tactic depth additionnal_terms gls= debug Pp.msgnl (Pp.str "Goal solved, generating proof ..."); match reason with Discrimination (i,ipac,j,jpac) -> - let p=build_proof uf (`Discr (i,ipac,j,jpac)) in + let p=build_proof uf (`Discr (i,ipac,j,jpac)) in let cstr=(get_constructor_info uf ipac.cnode).ci_constr in - discriminate_tac (axioms uf) cstr p gls + discriminate_tac cstr p gls | Incomplete -> let metacnt = ref 0 in - let newmeta _ = incr metacnt; mkMeta !metacnt in + let newmeta _ = incr metacnt; _M !metacnt in let terms_to_complete = List.map (build_term_to_complete uf newmeta) @@ -363,14 +387,13 @@ let cc_tactic depth additionnal_terms gls= | Contradiction dis -> let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in let ta=term uf dis.lhs and tb=term uf dis.rhs in - let axioms = axioms uf in match dis.rule with - Goal -> proof_tac axioms p gls - | Hyp id -> refute_tac axioms id ta tb p gls + Goal -> proof_tac p gls + | Hyp id -> refute_tac id ta tb p gls | HeqG id -> - convert_to_goal_tac axioms id ta tb p gls + convert_to_goal_tac id ta tb p gls | HeqnH (ida,idb) -> - convert_to_hyp_tac axioms ida ta idb tb p gls + convert_to_hyp_tac ida ta idb tb p gls let cc_fail gls = diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index ff4f7499..dec7273b 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -621,33 +621,39 @@ let build_proof fun g -> (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) - match kind_of_term dyn_infos.info with - | Case(_,_,t,_) -> - let g_nb_prod = nb_prod (pf_concl g) in - let type_of_term = pf_type_of g t in - let term_eq = - make_refl_eq type_of_term t + match kind_of_term dyn_infos.info with | Case(ci,ct,t,cb) -> + let do_finalize_t dyn_info' = + fun g -> + let t = dyn_info'.info in + let dyn_infos = {dyn_info' with info = + mkCase(ci,ct,t,cb)} in + let g_nb_prod = nb_prod (pf_concl g) in + let type_of_term = pf_type_of g t in + let term_eq = + make_refl_eq type_of_term t + in + tclTHENSEQ + [ + h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); + thin dyn_infos.rec_hyps; + pattern_option [[-1],t] None; + h_simplest_case t; + (fun g' -> + let g'_nb_prod = nb_prod (pf_concl g') in + let nb_instanciate_partial = g'_nb_prod - g_nb_prod in + observe_tac "treat_new_case" + (treat_new_case + ptes_infos + nb_instanciate_partial + (build_proof do_finalize) + t + dyn_infos) + g' + ) + + ] g in - tclTHENSEQ - [ - h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); - thin dyn_infos.rec_hyps; - pattern_option [[-1],t] None; - h_simplest_case t; - (fun g' -> - let g'_nb_prod = nb_prod (pf_concl g') in - let nb_instanciate_partial = g'_nb_prod - g_nb_prod in - observe_tac "treat_new_case" - (treat_new_case - ptes_infos - nb_instanciate_partial - (build_proof do_finalize) - t - dyn_infos) - g' - ) - - ] g + build_proof do_finalize_t {dyn_infos with info = t} g | Lambda(n,t,b) -> begin match kind_of_term( pf_concl g) with @@ -1474,7 +1480,7 @@ let prove_principle_for_gen (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) ); observe_tac "reverting" (revert (List.rev (acc_rec_arg_id::args_ids))); - observe_tac "h_fix" (h_fix (Some fix_id) (npost_rec_arg + 1)); + observe_tac "h_fix" (h_fix (Some fix_id) (List.length args_ids + 1)); h_intros (List.rev (acc_rec_arg_id::args_ids)); Equality.rewriteLR (mkConst eq_ref); observe_tac "finish" (fun gl' -> diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 6e2af224..82bee01f 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -209,7 +209,7 @@ let rec is_rec names = let rec lookup names = function | RVar(_,id) -> check_id id names | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false - | RCast(_,b,_,_) -> lookup names b + | RCast(_,b,_) -> lookup names b | RRec _ -> error "RRec not handled" | RIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) @@ -270,7 +270,30 @@ let derive_inversion fix_names = if do_observe () then Cerrors.explain_exn e else mt ()) with _ -> () -let generate_principle +let warning_error names e = + match e with + | Building_graph e -> + Pp.msg_warning + (str "Cannot define graph(s) for " ++ + h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ + if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()) + | Defining_principle e -> + Pp.msg_warning + (str "Cannot define principle(s) for "++ + h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ + if do_observe () then Cerrors.explain_exn e else mt ()) + | _ -> anomaly "" + +let error_error names e = + match e with + | Building_graph e -> + errorlabstrm "" + (str "Cannot define graph(s) for " ++ + h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ + if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()) + | _ -> anomaly "" + +let generate_principle on_error is_general do_built fix_rec_l recdefs interactive_proof (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit = @@ -324,18 +347,7 @@ let generate_principle () end with e -> - match e with - | Building_graph e -> - Pp.msg_warning - (str "Cannot define graph(s) for " ++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ - if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()) - | Defining_principle e -> - Pp.msg_warning - (str "Cannot define principle(s) for "++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ - if do_observe () then Cerrors.explain_exn e else mt ()) - | _ -> anomaly "" + on_error names e let register_struct is_rec fixpoint_exprl = match fixpoint_exprl with @@ -459,13 +471,14 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b using_lemmas args ret_type body -let do_generate_principle register_built interactive_proof fixpoint_exprl = +let do_generate_principle on_error register_built interactive_proof fixpoint_exprl = let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let _is_struct = match fixpoint_exprl with | [((name,Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> let pre_hook = generate_principle + on_error true register_built fixpoint_exprl @@ -478,6 +491,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl = | [((name,Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> let pre_hook = generate_principle + on_error true register_built fixpoint_exprl @@ -530,6 +544,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl = let is_rec = List.exists (is_rec fix_names) recdefs in if register_built then register_struct is_rec old_fixpoint_exprl; generate_principle + on_error false register_built fixpoint_exprl @@ -596,8 +611,10 @@ let rec add_args id new_args b = | CPatVar _ -> b | CEvar _ -> b | CSort _ -> b - | CCast(loc,b1,ck,b2) -> - CCast(loc,add_args id new_args b1,ck,add_args id new_args b2) + | CCast(loc,b1,CastConv(ck,b2)) -> + CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2)) + | CCast(loc,b1,CastCoerce) -> + CCast(loc,add_args id new_args b1,CastCoerce) | CNotation _ -> anomaly "add_args : CNotation" | CPrim _ -> b | CDelimiters _ -> anomaly "add_args : CDelimiters" @@ -732,7 +749,7 @@ let make_graph (f_ref:global_reference) = let id = id_of_label (con_label c) in [(id,None,nal_tas,t,b)] in - do_generate_principle false false expr_list; + do_generate_principle error_error false false expr_list; (* We register the infos *) let mp,dp,_ = repr_con c in List.iter @@ -742,6 +759,6 @@ let make_graph (f_ref:global_reference) = (* let make_graph _ = assert false *) -let do_generate_principle = do_generate_principle true +let do_generate_principle = do_generate_principle warning_error true diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index 26a1066c..9cee9edc 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -203,7 +203,10 @@ VERNAC COMMAND EXTEND NewFunctionalScheme match fas with | (_,fun_name,_)::_ -> begin - make_graph (Nametab.global fun_name); + begin + make_graph (Nametab.global fun_name) + end + ; try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> Util.error ("Cannot generate induction principle(s)") diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 04110ea9..9ec02d4c 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -478,7 +478,72 @@ let generalize_depedent_of x hyp g = - + (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis + (unfolding, substituting, destructing cases \ldots) + *) +let rec intros_with_rewrite g = + observe_tac "intros_with_rewrite" intros_with_rewrite_aux g +and intros_with_rewrite_aux : tactic = + fun g -> + let eq_ind = Coqlib.build_coq_eq () in + match kind_of_term (pf_concl g) with + | Prod(_,t,t') -> + begin + match kind_of_term t with + | App(eq,args) when (eq_constr eq eq_ind) -> + if isVar args.(1) + then + let id = pf_get_new_id (id_of_string "y") g in + tclTHENSEQ [ h_intro id; + generalize_depedent_of (destVar args.(1)) id; + tclTRY (Equality.rewriteLR (mkVar id)); + intros_with_rewrite + ] + g + else + begin + let id = pf_get_new_id (id_of_string "y") g in + tclTHENSEQ[ + h_intro id; + tclTRY (Equality.rewriteLR (mkVar id)); + intros_with_rewrite + ] g + end + | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> + Tauto.tauto g + | Case(_,_,v,_) -> + tclTHENSEQ[ + h_case (v,Rawterm.NoBindings); + intros_with_rewrite + ] g + | LetIn _ -> + tclTHENSEQ[ + h_reduce + (Rawterm.Cbv + {Rawterm.all_flags + with Rawterm.rDelta = false; + }) + onConcl + ; + intros_with_rewrite + ] g + | _ -> + let id = pf_get_new_id (id_of_string "y") g in + tclTHENSEQ [ h_intro id;intros_with_rewrite] g + end + | LetIn _ -> + tclTHENSEQ[ + h_reduce + (Rawterm.Cbv + {Rawterm.all_flags + with Rawterm.rDelta = false; + }) + onConcl + ; + intros_with_rewrite + ] g + | _ -> tclIDTAC g + let rec reflexivity_with_destruct_cases g = let destruct_case () = try @@ -492,10 +557,34 @@ let rec reflexivity_with_destruct_cases g = | _ -> reflexivity with _ -> reflexivity in - tclFIRST + let eq_ind = Coqlib.build_coq_eq () in + let discr_inject = + Tacticals.onAllClauses ( + fun sc g -> + match sc with + None -> tclIDTAC g + | Some ((_,id),_) -> + match kind_of_term (pf_type_of g (mkVar id)) with + | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> + if Equality.discriminable (pf_env g) (project g) t1 t2 + then Equality.discr id g + else if Equality.injectable (pf_env g) (project g) t1 t2 + then tclTHEN (Equality.inj [] id) intros_with_rewrite g + else tclIDTAC g + | _ -> tclIDTAC g + ) + in + (tclFIRST [ reflexivity; - destruct_case () - ] + destruct_case (); + (* We reach this point ONLY if + the same value is matched (at least) two times + along binding path. + In this case, either we have a discriminable hypothesis and we are done, + either at least an injectable one and we do the injection before continuing + *) + tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases + ]) g @@ -566,7 +655,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = ) branches in - let eq_ind = Coqlib.build_coq_eq () in (* We will need to change the function by its body using [f_equation] if it is recursive (that is the graph is infinite or unfold if the graph is finite @@ -596,71 +684,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = ] else unfold_in_concl [([],Names.EvalConstRef (destConst f))] in - (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis - (unfolding, substituting, destructing cases \ldots) - *) - let rec intros_with_rewrite_aux : tactic = - fun g -> - match kind_of_term (pf_concl g) with - | Prod(_,t,t') -> - begin - match kind_of_term t with - | App(eq,args) when (eq_constr eq eq_ind) -> - if isVar args.(1) - then - let id = pf_get_new_id (id_of_string "y") g in - tclTHENSEQ [ h_intro id; - generalize_depedent_of (destVar args.(1)) id; - tclTRY (Equality.rewriteLR (mkVar id)); - intros_with_rewrite - ] - g - else - begin - let id = pf_get_new_id (id_of_string "y") g in - tclTHENSEQ[ - h_intro id; - tclTRY (Equality.rewriteLR (mkVar id)); - intros_with_rewrite - ] g - end - | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> - Tauto.tauto g - | Case(_,_,v,_) -> - tclTHENSEQ[ - h_case (v,Rawterm.NoBindings); - intros_with_rewrite - ] g - | LetIn _ -> - tclTHENSEQ[ - h_reduce - (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; - }) - onConcl - ; - intros_with_rewrite - ] g - | _ -> - let id = pf_get_new_id (id_of_string "y") g in - tclTHENSEQ [ h_intro id;intros_with_rewrite] g - end - | LetIn _ -> - tclTHENSEQ[ - h_reduce - (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; - }) - onConcl - ; - intros_with_rewrite - ] g - | _ -> tclIDTAC g - and intros_with_rewrite g = - observe_tac "intros_with_rewrite" intros_with_rewrite_aux g - in (* The proof of each branche itself *) let ind_number = ref 0 in let min_constr_number = ref 0 in @@ -698,7 +721,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = h_intro graph_principle_id; observe_tac "" (tclTHEN_i (observe_tac "elim" ((elim (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings))))) - (fun i g -> prove_branche i g )) + (fun i g -> observe_tac "prove_branche" (prove_branche i) g )) ] g diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index aca84f06..b34a1097 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -351,7 +351,7 @@ let rec find_type_of nb b = then raise (Invalid_argument "find_type_of : not a valid inductive"); ind_type end - | RCast(_,b,_,_) -> find_type_of nb b + | RCast(_,b,_) -> find_type_of nb b | RApp _ -> assert false (* we have decomposed any application via raw_decompose_app *) | _ -> raise (Invalid_argument "not a ref") @@ -575,7 +575,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = let f_res = build_entry_lc env funnames args_res.to_avoid f in combine_results combine_app f_res args_res | RDynamic _ ->error "Not handled RDynamic" - | RCast(_,b,_,_) -> + | RCast(_,b,_) -> (* for an applied cast we just trash the cast part and restart the work. @@ -685,7 +685,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = end | RRec _ -> error "Not handled RRec" - | RCast(_,b,_,_) -> + | RCast(_,b,_) -> build_entry_lc env funnames avoid b | RDynamic _ -> error "Not handled RDynamic" and build_entry_lc_from_case env funname make_discr diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index ba5c2bbd..113ddd8b 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -18,7 +18,7 @@ let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b) let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl) let mkRSort s = RSort(dummy_loc,s) let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous) -let mkRCast(b,t) = RCast(dummy_loc,b,CastCoerce,t) +let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) (* Some basic functions to decompose rawconstrs @@ -145,8 +145,10 @@ let change_vars = | RRec _ -> error "Local (co)fixes are not supported" | RSort _ -> rt | RHole _ -> rt - | RCast(loc,b,k,t) -> - RCast(loc,change_vars mapping b,k,change_vars mapping t) + | RCast(loc,b,CastConv (k,t)) -> + RCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) + | RCast(loc,b,CastCoerce) -> + RCast(loc,change_vars mapping b,CastCoerce) | RDynamic _ -> error "Not handled RDynamic" and change_vars_br mapping ((loc,idl,patl,res) as br) = let new_mapping = List.fold_right Idmap.remove idl mapping in @@ -324,8 +326,10 @@ let rec alpha_rt excluded rt = | RRec _ -> error "Not handled RRec" | RSort _ -> rt | RHole _ -> rt - | RCast (loc,b,k,t) -> - RCast(loc,alpha_rt excluded b,k,alpha_rt excluded t) + | RCast (loc,b,CastConv (k,t)) -> + RCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) + | RCast (loc,b,CastCoerce) -> + RCast(loc,alpha_rt excluded b,CastCoerce) | RDynamic _ -> error "Not handled RDynamic" | RApp(loc,f,args) -> RApp(loc, @@ -375,7 +379,8 @@ let is_free_in id = | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> false | RHole _ -> false - | RCast (_,b,_,t) -> is_free_in b || is_free_in t + | RCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t + | RCast (_,b,CastCoerce) -> is_free_in b | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) and is_free_in_br (_,ids,_,rt) = (not (List.mem id ids)) && is_free_in rt @@ -469,8 +474,10 @@ let replace_var_by_term x_id term = | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> rt | RHole _ -> rt - | RCast(loc,b,k,t) -> - RCast(loc,replace_var_by_pattern b,k,replace_var_by_pattern t) + | RCast(loc,b,CastConv(k,t)) -> + RCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) + | RCast(loc,b,CastCoerce) -> + RCast(loc,replace_var_by_pattern b,CastCoerce) | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = if List.exists (fun id -> id_ord id x_id == 0) idl @@ -554,7 +561,8 @@ let ids_of_rawterm c = | RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc | RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | RCast (loc,c,k,t) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc + | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc + | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc | RLetTuple (_,nal,(na,po),b,c) -> List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc @@ -619,8 +627,10 @@ let zeta_normalize = | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> rt | RHole _ -> rt - | RCast(loc,b,k,t) -> - RCast(loc,zeta_normalize_term b,k,zeta_normalize_term t) + | RCast(loc,b,CastConv(k,t)) -> + RCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) + | RCast(loc,b,CastCoerce) -> + RCast(loc,zeta_normalize_term b,CastCoerce) | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) and zeta_normalize_br (loc,idl,patl,res) = (loc,idl,patl,zeta_normalize_term res) @@ -660,7 +670,8 @@ let expand_as = expand_as map br1, expand_as map br2) | RRec _ -> error "Not handled RRec" | RDynamic _ -> error "Not handled RDynamic" - | RCast(loc,b,kind,t) -> RCast(loc,expand_as map b,kind,expand_as map t) + | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t)) + | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce) | RCases(loc,po,el,brl) -> RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 60195229..df03a579 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -408,9 +408,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function | CDynamic (_, _) -> assert false | CDelimiters (_, key, num) -> CT_num_encapsulator(CT_num_type key , xlate_formula num) - | CCast (_, e,_, t) -> + | CCast (_, e, CastConv (_, t)) -> CT_coerce_TYPED_FORMULA_to_FORMULA (CT_typed_formula(xlate_formula e, xlate_formula t)) + | CCast (_, e, CastCoerce) -> assert false | CPatVar (_, (_,i)) when is_int_meta i -> CT_coerce_ID_to_FORMULA(CT_metac (CT_int (int_of_meta i))) | CPatVar (_, (false, s)) -> diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index da0817d1..be9ea5ae 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -13,7 +13,7 @@ (* *) (**************************************************************************) -(* $Id: coq_omega.ml 8934 2006-06-09 14:30:12Z herbelin $ *) +(* $Id: coq_omega.ml 9963 2007-07-09 14:02:20Z letouzey $ *) open Util open Pp @@ -302,6 +302,7 @@ let coq_eq_ind_r = lazy (constant "eq_ind_r") let coq_dec_or = lazy (constant "dec_or") let coq_dec_and = lazy (constant "dec_and") let coq_dec_imp = lazy (constant "dec_imp") +let coq_dec_iff = lazy (constant "dec_iff") let coq_dec_not = lazy (constant "dec_not") let coq_dec_False = lazy (constant "dec_False") let coq_dec_not_not = lazy (constant "dec_not_not") @@ -312,6 +313,7 @@ let coq_not_and = lazy (constant "not_and") let coq_not_imp = lazy (constant "not_imp") let coq_not_not = lazy (constant "not_not") let coq_imp_simp = lazy (constant "imp_simp") +let coq_iff = lazy (constant "iff") (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) @@ -388,6 +390,8 @@ let destructurate_prop t = | _, [_;_] when c = Lazy.force coq_Zgt -> Kapp (Zgt,args) | _, [_;_] when c = build_coq_and () -> Kapp (And,args) | _, [_;_] when c = build_coq_or () -> Kapp (Or,args) + | _, [t1;t2] when c = Lazy.force coq_iff -> + Kapp (And,[mkArrow t1 t2;mkArrow t2 t1]) | _, [_] when c = build_coq_not () -> Kapp (Not,args) | _, [] when c = build_coq_False () -> Kapp (False,args) | _, [] when c = build_coq_True () -> Kapp (True,args) diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 353fcdb3..a4acd9a9 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -46,6 +46,9 @@ open Eauto open Genarg +let compute_renamed_type gls c = + rename_bound_var (pf_env gls) [] (pf_type_of gls c) + let qed () = Command.save_named true let defined () = Command.save_named false @@ -388,32 +391,57 @@ let rec compute_le_proofs = function | a::tl -> tclORELSE assumption (tclTHENS - (apply_with_bindings - (delayed_force le_trans, - ExplicitBindings[dummy_loc,NamedHyp(id_of_string "m"),a])) + (fun g -> + let le_trans = delayed_force le_trans in + let t_le_trans = compute_renamed_type g le_trans in + let m_id = + let _,_,t = destProd t_le_trans in + let na,_,_ = destProd t in + Nameops.out_name na + in + apply_with_bindings + (le_trans, + ExplicitBindings[dummy_loc,NamedHyp m_id,a]) + g + ) [compute_le_proofs tl; tclORELSE (apply (delayed_force le_n)) assumption]) let make_lt_proof pmax le_proof = tclTHENS - (apply_with_bindings - (delayed_force le_lt_trans, - ExplicitBindings[dummy_loc,NamedHyp(id_of_string "m"), pmax])) - [compute_le_proofs le_proof; - tclTHENLIST[apply (delayed_force lt_S_n); default_full_auto]];; + (fun g -> + let le_lt_trans = delayed_force le_lt_trans in + let t_le_lt_trans = compute_renamed_type g le_lt_trans in + let m_id = + let _,_,t = destProd t_le_lt_trans in + let na,_,_ = destProd t in + Nameops.out_name na + in + apply_with_bindings + (le_lt_trans, + ExplicitBindings[dummy_loc,NamedHyp m_id, pmax]) g) + [observe_tac "compute_le_proofs" (compute_le_proofs le_proof); + tclTHENLIST[observe_tac "lt_S_n" (apply (delayed_force lt_S_n)); default_full_auto]];; let rec list_cond_rewrite k def pmax cond_eqs le_proofs = match cond_eqs with [] -> tclIDTAC | eq::eqs -> (fun g -> + let t_eq = compute_renamed_type g (mkVar eq) in + let k_id,def_id = + let k_na,_,t = destProd t_eq in + let _,_,t = destProd t in + let def_na,_,_ = destProd t in + Nameops.out_name k_na,Nameops.out_name def_na + in tclTHENS (general_rewrite_bindings false (mkVar eq, ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k; dummy_loc, NamedHyp def_id, mkVar def])) [list_cond_rewrite k def pmax eqs le_proofs; - make_lt_proof pmax le_proofs] g + observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g ) let rec introduce_all_equalities func eqs values specs bound le_proofs @@ -1023,12 +1051,20 @@ let rec introduce_all_values_eq cont_tac functional termine [] -> tclTHENLIST [tclTHENS - (general_rewrite_bindings false + (fun gls -> + let t_eq = compute_renamed_type gls (mkVar heq1) in + let k_id,def_id = + let k_na,_,t = destProd t_eq in + let _,_,t = destProd t in + let def_na,_,_ = destProd t in + Nameops.out_name k_na,Nameops.out_name def_na + in + general_rewrite_bindings false (mkVar heq1, ExplicitBindings[dummy_loc,NamedHyp k_id, f_S(f_S(mkVar pmax)); dummy_loc,NamedHyp def_id, - f])) + f]) gls ) [tclTHENLIST [simpl_iter(); unfold_constr (reference_of_constr functional); @@ -1067,12 +1103,22 @@ let rec introduce_all_values_eq cont_tac functional termine h_intros [heq;heq2]; rewriteLR (mkVar heq2); tclTHENS - (general_rewrite_bindings false - (mkVar heq, - ExplicitBindings - [dummy_loc, NamedHyp k_id, - f_S(mkVar pmax'); - dummy_loc, NamedHyp def_id, f])) + ( fun g -> + let t_eq = compute_renamed_type g (mkVar heq) in + let k_id,def_id = + let k_na,_,t = destProd t_eq in + let _,_,t = destProd t in + let def_na,_,_ = destProd t in + Nameops.out_name k_na,Nameops.out_name def_na + in + general_rewrite_bindings false + (mkVar heq, + ExplicitBindings + [dummy_loc, NamedHyp k_id, + f_S(mkVar pmax'); + dummy_loc, NamedHyp def_id, f]) + g + ) [tclIDTAC; tclTHENLIST [apply (delayed_force le_lt_n_Sm); @@ -1132,9 +1178,9 @@ let rec prove_eq (termine:constr) (f:constr)(functional:global_reference) | fn,args -> fun g -> let ids = ids_of_named_context (pf_hyps g) in - rec_leaf_eq + observe_tac "rec_leaf_eq" (rec_leaf_eq termine f ids (constr_of_reference functional) - eqs expr fn args g));; + eqs expr fn args) g));; let (com_eqn : identifier -> global_reference -> global_reference -> global_reference @@ -1159,10 +1205,19 @@ let (com_eqn : identifier -> ) ) ); +(* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); + Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); +*) Options.silently defined (); );; +let nf_zeta env = + Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + env + Evd.empty + + let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : unit = let function_type = interp_constr Evd.empty (Global.env()) type_of_f in @@ -1171,10 +1226,12 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:([],rec_impls) eq in (* Pp.msgnl (Printer.pr_lconstr equation_lemma_type); *) let res_vars,eq' = decompose_prod equation_lemma_type in + let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in + let eq' = nf_zeta env_eq' eq' in let res = (* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) (* Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *) -(* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *) +(* Pp.msgnl (str "eq' := " ++ Printer.pr_lconstr_env env eq' ++ fnl () ++str (string_of_int rec_arg_num)); *) match kind_of_term eq' with | App(e,[|_;_;eq_fix|]) -> mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars eq_fix)) @@ -1201,16 +1258,19 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let term_ref = Nametab.locate (make_short_qualid term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in (* message "start second proof"; *) + let continue = ref true in begin try com_eqn equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type) with e -> begin if Tacinterp.get_debug () <> Tactic_debug.DebugOff - then anomalylabstrm "" (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e); - ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); - anomaly "Cannot create equation Lemma" + then (Pp.msgnl (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e); continue := false) + else (ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); + anomaly "Cannot create equation Lemma") end end; + if !continue + then let eq_ref = Nametab.locate (make_short_qualid equation_id ) in let f_ref = destConst (constr_of_reference f_ref) and functional_ref = destConst (constr_of_reference functional_ref) diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index 83ea5b63..d20cafc1 100644 --- a/contrib/romega/ReflOmegaCore.v +++ b/contrib/romega/ReflOmegaCore.v @@ -1848,6 +1848,15 @@ Definition exact_divide (k : Z) (body : term) (t : nat) end | false => TrueTerm end + | NeqTerm (Tint Z0) b => + match eq_term (scalar_norm t (body * Tint k)%term) b with + | true => + match eq_Z k 0 with + | true => FalseTerm + | false => NeqTerm (Tint 0) body + end + | false => TrueTerm + end | _ => TrueTerm end. @@ -1858,18 +1867,24 @@ Theorem exact_divide_valid : unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; Simplify; simpl in |- *; auto; elim_eq_term (scalar_norm t (k2 * Tint k1)%term) t1; simpl in |- *; auto; elim_eq_Z k1 0; simpl in |- *; - auto; intros H1 H2; elim H2; elim scalar_norm_stable; - simpl in |- *; generalize H1; case (interp_term e k2); + auto; intros H1 H2; elim H2; elim scalar_norm_stable; + simpl in |- *; + [ + generalize H1; case (interp_term e k2); try trivial; (case k1; simpl in |- *; [ intros; absurd (0 = 0); assumption | intros p2 p3 H3 H4; discriminate H4 - | intros p2 p3 H3 H4; discriminate H4 ]). - + | intros p2 p3 H3 H4; discriminate H4 ]) + | + subst k1; rewrite Zmult_comm; simpl in *; intros; absurd (0=0); trivial + | + generalize H1; case (interp_term e k2); + try trivial; intros p2 p3 H3 H4; discriminate H4 + ]. Qed. - (* \paragraph{[O_DIV_APPROX]} La preuve reprend le schéma de la précédente mais on est sur une opération de type valid1 et non sur une opération terminale. *) @@ -1954,7 +1969,7 @@ Definition state (m : Z) (s : step) (prop1 prop2 : proposition) := match prop1 with | EqTerm (Tint Z0) b1 => match prop2 with - | EqTerm (Tint Z0) (b2 + - b3)%term => + | EqTerm b2 b3 => EqTerm (Tint 0) (rewrite s (b1 + (- b3 + b2) * Tint m)%term) | _ => TrueTerm end @@ -1965,10 +1980,8 @@ Theorem state_valid : forall (m : Z) (s : step), valid2 (state m s). unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify; simpl in |- *; auto; elim (rewrite_stable s e); simpl in |- *; - intros H1 H2; elim H1; - rewrite (Zplus_comm (- interp_term e t5) (interp_term e t3)); - elim H2; simpl in |- *; reflexivity. - + intros H1 H2; elim H1. + rewrite H2; rewrite Zplus_opp_l; simpl; reflexivity. Qed. (* \subsubsection{Tactiques générant plusieurs but} diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml index 285fc0ca..e7e7b3c5 100644 --- a/contrib/romega/refl_omega.ml +++ b/contrib/romega/refl_omega.ml @@ -6,6 +6,10 @@ *************************************************************************) +(* The addition on int, since it while be hidden soon by the one on BigInt *) + +let (+.) = (+) + open Const_omega module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -792,6 +796,9 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = | Kimp(t1,t2) -> binprop env ctxt (not negated) (not negated) gl (fun i x y -> Pimp(i,x,y)) t1 t2 + | Kapp("iff",[t1;t2]) -> + binprop env ctxt negated negated gl + (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1) | _ -> Pprop c with e when Logic.catchable_exception e -> Pprop c @@ -995,10 +1002,10 @@ let rec equas_of_solution_tree = function list_union (equas_of_solution_tree t1) (equas_of_solution_tree t2) | Leaf s -> s.s_equa_deps - -(* Because of really_useful_prop, decidable formulas such as Pfalse - and Ptrue are moved to Pprop, thus breaking the decidability check - in ReflOmegaCore.concl_to_hyp... *) +(* [really_useful_prop] pushes useless props in a new Pprop variable *) +(* Things get shorter, but may also get wrong, since a Prop is considered + to be undecidable in ReflOmegaCore.concl_to_hyp, whereas for instance + Pfalse is decidable. So should not be used on conclusion (??) *) let really_useful_prop l_equa c = let rec real_of = function @@ -1034,6 +1041,14 @@ let really_useful_prop l_equa c = None -> Pprop (real_of c) | Some t -> t +let rec vars_of_prop = function + | Pequa(_,e) -> vars_of_equations [e] + | Pnot p -> vars_of_prop p + | Por(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2) + | Pand(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2) + | Pimp(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2) + | _ -> [] + let rec display_solution_tree ch = function Leaf t -> output_string ch @@ -1160,10 +1175,15 @@ let replay_history env env_hyp = | CONSTANT_NUL e :: l -> mkApp (Lazy.force coq_s_constant_nul, [| mk_nat (get_hyp env_hyp e) |]) - | NEGATE_CONTRADICT(e1,e2,b) :: l -> + | NEGATE_CONTRADICT(e1,e2,true) :: l -> mkApp (Lazy.force coq_s_negate_contradict, [| mk_nat (get_hyp env_hyp e1.id); mk_nat (get_hyp env_hyp e2.id) |]) + | NEGATE_CONTRADICT(e1,e2,false) :: l -> + mkApp (Lazy.force coq_s_negate_contradict_inv, + [| mk_nat (List.length e2.body); + mk_nat (get_hyp env_hyp e1.id); + mk_nat (get_hyp env_hyp e2.id) |]) | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l -> let i = get_hyp env_hyp e.id in let r1 = loop (CCEqua e1 :: env_hyp) l1 in @@ -1254,14 +1274,18 @@ let resolution env full_reified_goal systems_list = let l_hyps = id_concl :: list_remove id_concl l_hyps' in let useful_hyps = List.map (fun id -> List.assoc id full_reified_goal) l_hyps in - let useful_vars = vars_of_equations equations in + let useful_vars = + let really_useful_vars = vars_of_equations equations in + let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in + list_uniq (List.sort compare (really_useful_vars @ concl_vars)) + in (* variables a introduire *) let to_introduce = add_stated_equations env solution_tree in let stated_vars = List.map (fun (v,_,_,_) -> v) to_introduce in let l_generalize_arg = List.map (fun (_,t,_,_) -> t) to_introduce in let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in (* L'environnement de base se construit en deux morceaux : - - les variables des équations utiles + - les variables des équations utiles (et de la conclusion) - les nouvelles variables declarées durant les preuves *) let all_vars_env = useful_vars @ stated_vars in let basic_env = @@ -1280,8 +1304,7 @@ let resolution env full_reified_goal systems_list = to_introduce in let reified_concl = match useful_hyps with - (Pnot p) :: _ -> - reified_of_proposition env (really_useful_prop useful_equa_id p) + (Pnot p) :: _ -> reified_of_proposition env p | _ -> reified_of_proposition env Pfalse in let l_reified_terms = (List.map @@ -1301,9 +1324,13 @@ let resolution env full_reified_goal systems_list = [| e.e_trace |] | ((O_left | O_mono) :: l) -> app coq_p_left [| loop l |] | (O_right :: l) -> app coq_p_right [| loop l |] in - app coq_pair_step - [| mk_nat (list_index e.e_origin.o_hyp l_hyps) ; - loop e.e_origin.o_path |] in + let correct_index = + let i = list_index e.e_origin.o_hyp l_hyps in + (* PL: it seems that additionnally introduced hyps are in the way during + normalization, hence this index shifting... *) + if i=0 then 0 else i +. List.length to_introduce + in + app coq_pair_step [| mk_nat correct_index; loop e.e_origin.o_path |] in let normalization_trace = mk_list (Lazy.force coq_h_step) (List.map normalize_equation equations) in diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v index bbdcd443..f5f845c2 100644 --- a/contrib/setoid_ring/InitialRing.v +++ b/contrib/setoid_ring/InitialRing.v @@ -13,6 +13,7 @@ Require Import BinNat. Require Import Setoid. Require Import Ring_theory. Require Import Ring_polynom. +Import List. Set Implicit Arguments. @@ -172,7 +173,7 @@ Section ZMORPHISM. Lemma gen_Zeqb_ok : forall x y, Zeq_bool x y = true -> [x] == [y]. Proof. - intros x y H; repeat rewrite same_genZ. + intros x y H. assert (H1 := Zeqb_ok x y H);unfold IDphi in H1. rewrite H1;rrefl. Qed. @@ -365,9 +366,236 @@ Section NMORPHISM. End NMORPHISM. +(* Words on N : initial structure for almost-rings. *) +Definition Nword := list N. +Definition NwO : Nword := nil. +Definition NwI : Nword := 1%N :: nil. + +Definition Nwcons n (w : Nword) : Nword := + match w, n with + | nil, 0%N => nil + | _, _ => n :: w + end. + +Fixpoint Nwadd (w1 w2 : Nword) {struct w1} : Nword := + match w1, w2 with + | n1::w1', n2:: w2' => (n1+n2)%N :: Nwadd w1' w2' + | nil, _ => w2 + | _, nil => w1 + end. + +Definition Nwopp (w:Nword) : Nword := Nwcons 0%N w. + +Definition Nwsub w1 w2 := Nwadd w1 (Nwopp w2). + +Fixpoint Nwscal (n : N) (w : Nword) {struct w} : Nword := + match w with + | m :: w' => (n*m)%N :: Nwscal n w' + | nil => nil + end. + +Fixpoint Nwmul (w1 w2 : Nword) {struct w1} : Nword := + match w1 with + | 0%N::w1' => Nwopp (Nwmul w1' w2) + | n1::w1' => Nwsub (Nwscal n1 w2) (Nwmul w1' w2) + | nil => nil + end. +Fixpoint Nw_is0 (w : Nword) : bool := + match w with + | nil => true + | 0%N :: w' => Nw_is0 w' + | _ => false + end. + +Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool := + match w1, w2 with + | n1::w1', n2::w2' => + if Neq_bool n1 n2 then Nweq_bool w1' w2' else false + | nil, _ => Nw_is0 w2 + | _, nil => Nw_is0 w1 + end. + +Section NWORDMORPHISM. + Variable R : Type. + Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). + Variable req : R -> R -> Prop. + Notation "0" := rO. Notation "1" := rI. + Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). + Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). + Notation "x == y" := (req x y). + Variable Rsth : Setoid_Theory R req. + Add Setoid R req Rsth as R_setoid5. + Ltac rrefl := gen_reflexivity Rsth. + Variable Reqe : ring_eq_ext radd rmul ropp req. + Add Morphism radd : radd_ext5. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext5. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext5. exact (Ropp_ext Reqe). Qed. + + Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. + Add Morphism rsub : rsub_ext7. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth. + Ltac add_push := gen_add_push radd Rsth Reqe ARth. + + Fixpoint gen_phiNword (w : Nword) : R := + match w with + | nil => 0 + | n :: nil => gen_phiN rO rI radd rmul n + | N0 :: w' => - gen_phiNword w' + | n::w' => gen_phiN rO rI radd rmul n - gen_phiNword w' + end. + + Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0. +Proof. +induction w; simpl in |- *; intros; auto. + reflexivity. + + destruct a. + destruct w. + reflexivity. + + rewrite IHw in |- *; trivial. + apply (ARopp_zero Rsth Reqe ARth). + + discriminate. +Qed. + + Lemma gen_phiNword_cons : forall w n, + gen_phiNword (n::w) == gen_phiN rO rI radd rmul n - gen_phiNword w. +induction w. + destruct n; simpl in |- *; norm. + + intros. + destruct n; norm. +Qed. + + Lemma gen_phiNword_Nwcons : forall w n, + gen_phiNword (Nwcons n w) == gen_phiN rO rI radd rmul n - gen_phiNword w. +destruct w; intros. + destruct n; norm. + + unfold Nwcons in |- *. + rewrite gen_phiNword_cons in |- *. + reflexivity. +Qed. + + Lemma gen_phiNword_ok : forall w1 w2, + Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2. +induction w1; intros. + simpl in |- *. + rewrite (gen_phiNword0_ok _ H) in |- *. + reflexivity. + + rewrite gen_phiNword_cons in |- *. + destruct w2. + simpl in H. + destruct a; try discriminate. + rewrite (gen_phiNword0_ok _ H) in |- *. + norm. + + simpl in H. + rewrite gen_phiNword_cons in |- *. + case_eq (Neq_bool a n); intros. + rewrite H0 in H. + rewrite <- (Neq_bool_ok _ _ H0) in |- *. + rewrite (IHw1 _ H) in |- *. + reflexivity. + + rewrite H0 in H; discriminate H. +Qed. + + +Lemma Nwadd_ok : forall x y, + gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y. +induction x; intros. + simpl in |- *. + norm. + + destruct y. + simpl Nwadd; norm. + + simpl Nwadd in |- *. + repeat rewrite gen_phiNword_cons in |- *. + rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- *. + destruct Reqe; constructor; trivial. + + rewrite IHx in |- *. + norm. + add_push (- gen_phiNword x); reflexivity. +Qed. + +Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x. +simpl in |- *. +unfold Nwopp in |- *; simpl in |- *. +intros. +rewrite gen_phiNword_Nwcons in |- *; norm. +Qed. + +Lemma Nwscal_ok : forall n x, + gen_phiNword (Nwscal n x) == gen_phiN rO rI radd rmul n * gen_phiNword x. +induction x; intros. + norm. + + simpl Nwscal in |- *. + repeat rewrite gen_phiNword_cons in |- *. + rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- *. + destruct Reqe; constructor; trivial. + + rewrite IHx in |- *. + norm. +Qed. + +Lemma Nwmul_ok : forall x y, + gen_phiNword (Nwmul x y) == gen_phiNword x * gen_phiNword y. +induction x; intros. + norm. + + destruct a. + simpl Nwmul in |- *. + rewrite Nwopp_ok in |- *. + rewrite IHx in |- *. + rewrite gen_phiNword_cons in |- *. + norm. + + simpl Nwmul in |- *. + unfold Nwsub in |- *. + rewrite Nwadd_ok in |- *. + rewrite Nwscal_ok in |- *. + rewrite Nwopp_ok in |- *. + rewrite IHx in |- *. + rewrite gen_phiNword_cons in |- *. + norm. +Qed. + +(* Proof that [.] satisfies morphism specifications *) + Lemma gen_phiNword_morph : + ring_morph 0 1 radd rmul rsub ropp req + NwO NwI Nwadd Nwmul Nwsub Nwopp Nweq_bool gen_phiNword. +constructor. + reflexivity. + + reflexivity. + + exact Nwadd_ok. + + intros. + unfold Nwsub in |- *. + rewrite Nwadd_ok in |- *. + rewrite Nwopp_ok in |- *. + norm. + + exact Nwmul_ok. + + exact Nwopp_ok. + + exact gen_phiNword_ok. +Qed. + +End NWORDMORPHISM. + + + (* syntaxification of constants in an abstract ring: - the inverse of gen_phiPOS - Why we do not reconnize only rI ?????? *) + the inverse of gen_phiPOS *) Ltac inv_gen_phi_pos rI add mul t := let rec inv_cst t := match t with @@ -390,6 +618,18 @@ End NMORPHISM. end in inv_cst t. +(* The (partial) inverse of gen_phiNword *) + Ltac inv_gen_phiNword rO rI add mul opp t := + match t with + rO => constr:NwO + | _ => + match inv_gen_phi_pos rI add mul t with + NotConstant => NotConstant + | ?p => constr:(Npos p::nil) + end + end. + + (* The inverse of gen_phiN *) Ltac inv_gen_phiN rO rI add mul t := match t with @@ -417,9 +657,18 @@ End NMORPHISM. end end. -(* A simpl tactic reconninzing nothing *) - Ltac inv_morph_nothing t := constr:(NotConstant). +(* A simple tactic recognizing only 0 and 1. The inv_gen_phiX above + are only optimisations that directly returns the reifid constant + instead of resorting to the constant propagation of the simplification + algorithm. *) +Ltac inv_gen_phi rO rI cO cI t := + match t with + | rO => cO + | rI => cI + end. +(* A simple tactic recognizing no constant *) + Ltac inv_morph_nothing t := constr:(NotConstant). Ltac coerce_to_almost_ring set ext rspec := match type of rspec with @@ -441,7 +690,7 @@ Ltac abstract_ring_morphism set ext rspec := | ring_theory _ _ _ _ _ _ _ => constr:(gen_phiZ_morph set ext rspec) | semi_ring_theory _ _ _ _ _ => constr:(gen_phiN_morph set ext rspec) | almost_ring_theory _ _ _ _ _ _ _ => - fail 1 "an almost ring cannot be abstract" + constr:(gen_phiNword_morph set ext rspec) | _ => fail 1 "bad ring structure" end. @@ -502,7 +751,7 @@ Ltac ring_elements set ext rspec pspec sspec rk := | ring_morph _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => m | @semi_morph _ _ _ _ _ _ _ _ _ _ _ _ _ => constr:(SRmorph_Rmorph set m) - | _ => fail 2 " ici" + | _ => fail 2 "ring anomaly" end | _ => fail 1 "ill-formed ring kind" end in diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index 7419f184..b55c5443 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -108,31 +108,37 @@ Ltac FV Cst CstPow add mul sub opp pow t fv := (* syntaxification of ring expressions *) Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := let rec mkP t := + let f := match Cst t with | InitialRing.NotConstant => match t with | (radd ?t1 ?t2) => + fun _ => let e1 := mkP t1 in let e2 := mkP t2 in constr:(PEadd e1 e2) | (rmul ?t1 ?t2) => + fun _ => let e1 := mkP t1 in let e2 := mkP t2 in constr:(PEmul e1 e2) | (rsub ?t1 ?t2) => + fun _ => let e1 := mkP t1 in let e2 := mkP t2 in constr:(PEsub e1 e2) | (ropp ?t1) => + fun _ => let e1 := mkP t1 in constr:(PEopp e1) | (rpow ?t1 ?n) => match CstPow n with | InitialRing.NotConstant => - let p := Find_at t fv in constr:(PEX C p) - | ?c => let e1 := mkP t1 in constr:(PEpow e1 c) + fun _ => let p := Find_at t fv in constr:(PEX C p) + | ?c => fun _ => let e1 := mkP t1 in constr:(PEpow e1 c) end | _ => - let p := Find_at t fv in constr:(PEX C p) + fun _ => let p := Find_at t fv in constr:(PEX C p) end - | ?c => constr:(PEc c) - end + | ?c => fun _ => constr:(@PEc C c) + end in + f () in mkP t. Ltac ParseRingComponents lemma := diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 8b2ce26b..f963fc9c 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: newring.ml4 9603 2007-02-07 00:41:16Z barras $ i*) +(*i $Id: newring.ml4 9968 2007-07-11 15:49:07Z barras $ i*) open Pp open Util @@ -166,8 +166,10 @@ let decl_constant na c = const_entry_boxed = true}, IsProof Lemma)) -let ltac_call tac args = +let ltac_call tac (args:glob_tactic_arg list) = TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)) +let ltac_acall tac (args:glob_tactic_arg list) = + TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args) let ltac_lcall tac args = TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args)) @@ -276,12 +278,18 @@ let coq_mk_reqe = my_constant "mk_reqe" let coq_semi_ring_theory = my_constant "semi_ring_theory" let coq_mk_seqe = my_constant "mk_seqe" +let ltac_inv_morph_gen = zltac"inv_gen_phi" let ltac_inv_morphZ = zltac"inv_gen_phiZ" let ltac_inv_morphN = zltac"inv_gen_phiN" +let ltac_inv_morphNword = zltac"inv_gen_phiNword" let coq_abstract = my_constant"Abstract" let coq_comp = my_constant"Computational" let coq_morph = my_constant"Morphism" +(* morphism *) +let coq_ring_morph = my_constant "ring_morph" +let coq_semi_morph = my_constant "semi_morph" + (* power function *) let ltac_inv_morph_nothing = zltac"inv_morph_nothing" let coq_pow_N_pow_N = my_constant "pow_N_pow_N" @@ -527,6 +535,18 @@ let dest_ring env sigma th_spec = | _ -> error "bad ring structure" +let dest_morph env sigma m_spec = + let m_typ = Retyping.get_type_of env sigma m_spec in + match kind_of_term m_typ with + App(f,[|r;zero;one;add;mul;sub;opp;req; + c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) + when f = Lazy.force coq_ring_morph -> + (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi) + | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|]) + when f = Lazy.force coq_semi_morph -> + (c,czero,cone,cadd,cmul,None,None,ceqb,phi) + | _ -> error "bad morphism structure" + type coeff_spec = Computational of constr (* equality test *) @@ -545,22 +565,34 @@ type cst_tac_spec = CstTac of raw_tactic_expr | Closed of reference list -let interp_cst_tac kind (zero,one,add,mul,opp) cst_tac = +let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = match cst_tac with Some (CstTac t) -> Tacinterp.glob_tactic t | Some (Closed lc) -> closed_term_ast (List.map Nametab.global lc) | None -> - (match opp, kind with - None, _ -> + (match rk, opp, kind with + Abstract, None, _ -> let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul])) - | Some opp, Some _ -> + | Abstract, Some opp, Some _ -> let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) - | _ -> error"a tactic must be specified for an almost_ring") + | Abstract, Some opp, None -> + let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in + TacArg + (TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) + | Computational _,_,_ -> + let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in + TacArg + (TacCall(dummy_loc,t,List.map carg [zero;one;zero;one])) + | Morphism mth,_,_ -> + let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in + let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in + TacArg + (TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone]))) let make_hyp env c = - let t = (Typeops.typing env c).uj_type in + let t = Retyping.get_type_of env Evd.empty c in lapp coq_mkhypo [|t;c|] let make_hyp_list env lH = @@ -608,7 +640,8 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign = let lemma1 = decl_constant (string_of_id name^"_ring_lemma1") lemma1 in let lemma2 = decl_constant (string_of_id name^"_ring_lemma2") lemma2 in - let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in + let cst_tac = + interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = match pre with Some t -> Tacinterp.glob_tactic t @@ -980,7 +1013,8 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign = let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in let lemma4 = decl_constant (string_of_id name^"_field_lemma4") lemma4 in let cond_lemma = decl_constant (string_of_id name^"_lemma5") cond_lemma in - let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in + let cst_tac = + interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = match pre with Some t -> Tacinterp.glob_tactic t diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v index 46121ff1..f047b729 100644 --- a/contrib/subtac/FixSub.v +++ b/contrib/subtac/FixSub.v @@ -1,6 +1,8 @@ Require Import Wf. Require Import Coq.subtac.Utils. +(** Reformulation of the Wellfounded module using subsets where possible. *) + Section Well_founded. Variable A : Type. Variable R : A -> A -> Prop. @@ -75,23 +77,70 @@ Require Import Wf_nat. Require Import Lt. Section Well_founded_measure. -Variable A : Type. -Variable f : A -> nat. -Definition R := fun x y => f x < f y. + Variable A : Type. + Variable m : A -> nat. + + Section Acc. + + Variable P : A -> Type. + + Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x. + + Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x := + F_sub x (fun y: { y : A | m y < m x} => Fix_measure_F_sub (proj1_sig y) + (Acc_inv r (m (proj1_sig y)) (proj2_sig y))). + + Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)). + + End Acc. -Section FixPoint. + Section FixPoint. + Variable P : A -> Type. + + Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x. + + Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *) + + Definition Fix_measure (x:A) := Fix_measure_F_sub P F_sub x (lt_wf (m x)). + + Hypothesis + F_ext : + forall (x:A) (f g:forall y:{y:A | m y < m x}, P (`y)), + (forall y:{ y:A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g. -Variable P : A -> Type. + Lemma Fix_measure_F_eq : + forall (x:A) (r:Acc lt (m x)), + F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (proj2_sig y))) = Fix_F x r. + Proof. + intros x. + set (y := m x). + unfold Fix_measure_F_sub. + intros r ; case r ; auto. + Qed. + + Lemma Fix_measure_F_inv : forall (x:A) (r s:Acc lt (m x)), Fix_F x r = Fix_F x s. + Proof. + intros x r s. + rewrite (proof_irrelevance (Acc lt (m x)) r s) ; auto. + Qed. -Variable F_sub : forall x:A, (forall y: { y : A | f y < f x }, P (proj1_sig y)) -> P x. - -Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (f x)) {struct r} : P x := - F_sub x (fun y: { y : A | f y < f x} => Fix_measure_F_sub (proj1_sig y) - (Acc_inv r (f (proj1_sig y)) (proj2_sig y))). + Lemma Fix_measure_eq : forall x:A, Fix_measure x = F_sub x (fun (y:{y:A| m y < m x}) => Fix_measure (proj1_sig y)). + Proof. + intro x; unfold Fix_measure in |- *. + rewrite <- (Fix_measure_F_eq ). + apply F_ext; intros. + apply Fix_measure_F_inv. + Qed. -Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (f x)). + Lemma fix_measure_sub_eq : + forall x : A, + Fix_measure_sub P F_sub x = + let f_sub := F_sub in + f_sub x (fun {y : A | m y < m x}=> Fix_measure (`y)). + exact Fix_measure_eq. + Qed. -End FixPoint. + End FixPoint. End Well_founded_measure. diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v index 1a12ac82..4610f346 100644 --- a/contrib/subtac/FunctionalExtensionality.v +++ b/contrib/subtac/FunctionalExtensionality.v @@ -1,3 +1,11 @@ +Lemma equal_f : forall A B : Type, forall (f g : A -> B), + f = g -> forall x, f x = g x. +Proof. + intros. + rewrite H. + auto. +Qed. + Axiom fun_extensionality : forall A B (f g : A -> B), (forall x, f x = g x) -> f = g. @@ -23,3 +31,17 @@ Proof. apply (fun_extensionality_dep _ _ _ _ H). rewrite H0 ; auto. Qed. + +Lemma fix_sub_measure_eq_ext : + forall (A : Type) (f : A -> nat) (P : A -> Type) + (F_sub : forall x : A, (forall {y : A | f y < f x}, P (`y)) -> P x), + forall x : A, + Fix_measure_sub A f P F_sub x = + F_sub x (fun {y : A | f y < f x}=> Fix_measure_sub A f P F_sub (`y)). +Proof. + intros ; apply Fix_measure_eq ; auto. + intros. + assert(f0 = g). + apply (fun_extensionality_dep _ _ _ _ H). + rewrite H0 ; auto. +Qed. diff --git a/contrib/subtac/Heq.v b/contrib/subtac/Heq.v new file mode 100644 index 00000000..f2b216d9 --- /dev/null +++ b/contrib/subtac/Heq.v @@ -0,0 +1,34 @@ +Require Export JMeq. + +(** Notation for heterogenous equality. *) + +Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level). + +(** Do something on an heterogeneous equality appearing in the context. *) + +Ltac on_JMeq tac := + match goal with + | [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H + end. + +(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *) + +Ltac simpl_one_JMeq := + on_JMeq + ltac:(fun H => let H' := fresh "H" in + assert (H' := JMeq_eq H) ; clear H ; rename H' into H). + +(** Repeat it for every possible hypothesis. *) + +Ltac simpl_JMeq := repeat simpl_one_JMeq. + +(** Just simplify an h.eq. without clearing it. *) + +Ltac simpl_one_dep_JMeq := + on_JMeq + ltac:(fun H => let H' := fresh "H" in + assert (H' := JMeq_eq H)). + + + + diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v new file mode 100644 index 00000000..a00234dd --- /dev/null +++ b/contrib/subtac/SubtacTactics.v @@ -0,0 +1,158 @@ +Ltac induction_with_subterm c H := + let x := fresh "x" in + let y := fresh "y" in + (remember c as x ; rewrite <- y in H ; induction H ; subst). + +Ltac induction_on_subterm c := + let x := fresh "x" in + let y := fresh "y" in + (set(x := c) ; assert(y:x = c) by reflexivity ; clearbody x ; induction x ; inversion y ; try subst ; + clear y). + +Ltac induction_with_subterms c c' H := + let x := fresh "x" in + let y := fresh "y" in + let z := fresh "z" in + let w := fresh "w" in + (set(x := c) ; assert(y:x = c) by reflexivity ; + set(z := c') ; assert(w:z = c') by reflexivity ; + rewrite <- y in H ; rewrite <- w in H ; + induction H ; subst). + + +Ltac destruct_one_pair := + match goal with + | [H : (_ /\ _) |- _] => destruct H + | [H : prod _ _ |- _] => destruct H + end. + +Ltac destruct_pairs := repeat (destruct_one_pair). + +Ltac destruct_one_ex := + let tac H := let ph := fresh "H" in destruct H as [H ph] in + match goal with + | [H : (ex _) |- _] => tac H + | [H : (sig ?P) |- _ ] => tac H + | [H : (ex2 _) |- _] => tac H + end. + +Ltac destruct_exists := repeat (destruct_one_ex). + +Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht]. + +Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H]. + +Tactic Notation "contradiction" "by" constr(t) := + let H := fresh in assert t as H by auto with * ; contradiction. + +Ltac discriminates := + match goal with + | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity + | _ => discriminate + end. + +Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex). + +Ltac on_last_hyp tac := + match goal with + [ H : _ |- _ ] => tac H + end. + +Tactic Notation "on_last_hyp" tactic(t) := on_last_hyp t. + +Ltac revert_last := + match goal with + [ H : _ |- _ ] => revert H + end. + +Ltac reverse := repeat revert_last. + +Ltac on_call f tac := + match goal with + | H : ?T |- _ => + match T with + | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u) + | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v) + | context [f ?x ?y ?z ?w] => tac (f x y z w) + | context [f ?x ?y ?z] => tac (f x y z) + | context [f ?x ?y] => tac (f x y) + | context [f ?x] => tac (f x) + end + | |- ?T => + match T with + | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u) + | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v) + | context [f ?x ?y ?z ?w] => tac (f x y z w) + | context [f ?x ?y ?z] => tac (f x y z) + | context [f ?x ?y] => tac (f x y) + | context [f ?x] => tac (f x) + end + end. + +(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *) +Ltac destruct_call f := + let tac t := destruct t in on_call f tac. + +Ltac destruct_call_as f l := + let tac t := destruct t as l in on_call f tac. + +Tactic Notation "destruct_call" constr(f) := destruct_call f. +Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := destruct_call_as f l. + +Ltac myinjection := + let tac H := inversion H ; subst ; clear H in + match goal with + | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H + | [ H : ?f ?a ?b = ?f' ?a' ?b' |- _ ] => tac H + | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H + | _ => idtac + end. + +Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0. + +Ltac bang := + match goal with + | |- ?x => + match x with + | context [False_rect _ ?p] => elim p + end + end. + +Require Import Eqdep. + +Ltac elim_eq_rect := + match goal with + | [ |- ?t ] => + match t with + | context [ @eq_rect _ _ _ _ _ ?p ] => + let P := fresh "P" in + set (P := p); simpl in P ; + try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) + | context [ @eq_rect _ _ _ _ _ ?p _ ] => + let P := fresh "P" in + set (P := p); simpl in P ; + try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) + end + end. + +Ltac real_elim_eq_rect := + match goal with + | [ |- ?t ] => + match t with + | context [ @eq_rect _ _ _ _ _ ?p ] => + let P := fresh "P" in + set (P := p); simpl in P ; + ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) + | context [ @eq_rect _ _ _ _ _ ?p _ ] => + let P := fresh "P" in + set (P := p); simpl in P ; + ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) + end + end. +
\ No newline at end of file diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index 4a2208ce..76f49dd3 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -1,75 +1,65 @@ +Require Export Coq.subtac.SubtacTactics. + Set Implicit Arguments. -Notation "'fun' { x : A | P } => Q" := - (fun x:{x:A|P} => Q) - (at level 200, x ident, right associativity). +(** Wrap a proposition inside a subset. *) -Notation "( x & ? )" := (@exist _ _ x _) : core_scope. +Notation " {{ x }} " := (tt : { y : unit | x }). + +(** A simpler notation for subsets defined on a cartesian product. *) + +Notation "{ ( x , y ) : A | P }" := + (sig (fun anonymous : A => let (x,y) := anonymous in P)) + (x ident, y ident) : type_scope. + +(** Generates an obligation to prove False. *) Notation " ! " := (False_rect _ _). -Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A. -intros. -induction t. -exact x. -Defined. +(** Abbreviation for first projection and hiding of proofs of subset objects. *) + +Notation " ` t " := (proj1_sig t) (at level 10) : core_scope. +Notation "( x & ? )" := (@exist _ _ x _) : core_scope. + +(** Coerces objects to their support before comparing them. *) -Lemma ex_pi2 : forall (A : Prop) (P : A -> Prop) (t : ex P), - P (ex_pi1 t). -intros A P. -dependent inversion t. -simpl. -exact p. -Defined. +Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70). +(** Quantifying over subsets. *) + +Notation "'fun' { x : A | P } => Q" := + (fun x:{x:A|P} => Q) + (at level 200, x ident, right associativity). -Notation "` t" := (proj1_sig t) (at level 100) : core_scope. Notation "'forall' { x : A | P } , Q" := (forall x:{x:A|P}, Q) (at level 200, x ident, right associativity). -Lemma subset_simpl : forall (A : Set) (P : A -> Prop) - (t : sig P), P (` t). -Proof. -intros. -induction t. - simpl ; auto. -Qed. - -Ltac destruct_one_pair := - match goal with - | [H : (ex _) |- _] => destruct H - | [H : (ex2 _) |- _] => destruct H - | [H : (sig _) |- _] => destruct H - | [H : (_ /\ _) |- _] => destruct H -end. - -Ltac destruct_exists := repeat (destruct_one_pair) . - -Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; auto with arith. - -(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *) -Ltac destruct_call f := - match goal with - | H : ?T |- _ => - match T with - context [f ?x ?y ?z] => destruct (f x y z) - | context [f ?x ?y] => destruct (f x y) - | context [f ?x] => destruct (f x) - end - | |- ?T => - match T with - context [f ?x ?y ?z] => let n := fresh "H" in set (n:=f x y z); destruct n - | context [f ?x ?y] => let n := fresh "H" in set (n:=f x y); destruct n - | context [f ?x] => let n := fresh "H" in set (n:=f x); destruct n - end - end. +Require Import Coq.Bool.Sumbool. + +(** Construct a dependent disjunction from a boolean. *) + +Notation "'dec'" := (sumbool_of_bool) (at level 0). +(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *) + +Notation in_right := (@right _ _ _). +Notation in_left := (@left _ _ _). + +(** Default simplification tactic. *) + +Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; + try (solve [ red ; intros ; discriminate ]) ; auto with *. + +(** Extraction directives *) Extraction Inline proj1_sig. Extract Inductive unit => "unit" [ "()" ]. Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. -Extract Inductive prod => "pair" [ "" ]. -Extract Inductive sigT => "pair" [ "" ]. +(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) +(* Extract Inductive sigT => "prod" [ "" ]. *) Require Export ProofIrrelevance. +Require Export Coq.subtac.Heq. + +Delimit Scope program_scope with program. diff --git a/contrib/subtac/context.ml b/contrib/subtac/context.ml deleted file mode 100644 index 236b0ea5..00000000 --- a/contrib/subtac/context.ml +++ /dev/null @@ -1,35 +0,0 @@ -open Term -open Names - -type t = rel_declaration list (* name, optional coq interp, algorithmic type *) - -let assoc n t = - let _, term, typ = List.find (fun (x, _, _) -> x = n) t in - term, typ - -let assoc_and_index x l = - let rec aux i = function - (y, term, typ) :: tl -> if x = y then i, term, typ else aux (succ i) tl - | [] -> raise Not_found - in aux 0 l - -let id_of_name = function - Name id -> id - | Anonymous -> raise (Invalid_argument "id_of_name") -(* - -let subst_ctx ctx c = - let rec aux ((ctx, n, c) as acc) = function - (name, None, typ) :: tl -> - aux (((id_of_name name, None, rel_to_vars ctx typ) :: ctx), - pred n, c) tl - | (name, Some term, typ) :: tl -> - let t' = Term.substnl [term] n c in - aux (ctx, n, t') tl - | [] -> acc - in - let (x, _, z) = aux ([], pred (List.length ctx), c) (List.rev ctx) in - (x, rel_to_vars x z) -*) - -let subst_env env c = (env, c) diff --git a/contrib/subtac/context.mli b/contrib/subtac/context.mli deleted file mode 100644 index 671d6f36..00000000 --- a/contrib/subtac/context.mli +++ /dev/null @@ -1,5 +0,0 @@ -type t = Term.rel_declaration list -val assoc : 'a -> ('a * 'b * 'c) list -> 'b * 'c -val assoc_and_index : 'a -> ('a * 'b * 'c) list -> int * 'b * 'c -val id_of_name : Names.name -> Names.identifier -val subst_env : 'a -> 'b -> 'a * 'b diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 1844fea5..2a84fdd0 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -11,52 +11,33 @@ open Evd open List open Pp open Util +open Subtac_utils -let reverse_array arr = - Array.of_list (List.rev (Array.to_list arr)) - let trace s = if !Options.debug then (msgnl s; msgerr s) else () -(** Utilities to find indices in lists *) -let list_index x l = - let rec aux i = function - k :: tl -> if k = x then i else aux (succ i) tl - | [] -> raise Not_found - in aux 0 l - -let list_assoc_index x l = - let rec aux i = function - (k, _, v) :: tl -> if k = x then i else aux (succ i) tl - | [] -> raise Not_found - in aux 0 l - - (** Substitute evar references in t using De Bruijn indices, where n binders were passed through. *) let subst_evar_constr evs n t = let seen = ref Intset.empty in - let evar_info id = - let rec aux i = function - (k, x) :: tl -> - if k = id then x else aux (succ i) tl - | [] -> raise Not_found - in aux 0 evs - in + let evar_info id = List.assoc id evs in let rec substrec depth c = match kind_of_term c with | Evar (k, args) -> - let (id, idstr), hyps, _, _ = + let (id, idstr), hyps, chop, _, _ = try evar_info k with Not_found -> anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") in seen := Intset.add id !seen; -(* (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++ *) -(* int (List.length hyps) ++ str " hypotheses"); with _ -> () ); *) (* Evar arguments are created in inverse order, and we must not apply to defined ones (i.e. LetIn's) *) + let args = + let n = match chop with None -> 0 | Some c -> c in + let (l, r) = list_chop n (List.rev (Array.to_list args)) in + List.rev r + in let args = let rec aux hyps args acc = match hyps, args with @@ -66,9 +47,13 @@ let subst_evar_constr evs n t = aux tlh tla acc | [], [] -> acc | _, _ -> acc (*failwith "subst_evars: invalid argument"*) - in aux hyps (Array.to_list args) [] - in - mkApp (mkVar idstr, Array.of_list args) + in aux hyps args [] + in + (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (List.length args) ++ str "arguments," ++ + int (List.length hyps) ++ str " hypotheses" ++ spc () ++ + pp_list (fun x -> my_print_constr (Global.env ()) x) args); + with _ -> ()); + mkApp (mkVar idstr, Array.of_list args) | _ -> map_constr_with_binders succ substrec depth c in let t' = substrec 0 t in @@ -78,10 +63,7 @@ let subst_evar_constr evs n t = (** Substitute variable references in t using De Bruijn indices, where n binders were passed through. *) let subst_vars acc n t = - let var_index id = - let idx = list_index id acc in - idx + 1 - in + let var_index id = Util.list_index id acc in let rec substrec depth c = match kind_of_term c with | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c) | _ -> map_constr_with_binders succ substrec depth c @@ -89,47 +71,58 @@ let subst_vars acc n t = substrec 0 t (** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ]) - to a product : forall H1 : t1, ..., forall Hn : tn, concl. + to a product : forall H1 : t1, ..., forall Hn : tn, concl. Changes evars and hypothesis references to variable references. + A little optimization: don't include unnecessary let-ins and their dependencies. *) -let etype_of_evar evs ev hyps = +let etype_of_evar evs hyps concl = let rec aux acc n = function (id, copt, t) :: tl -> let t', s = subst_evar_constr evs n t in let t'' = subst_vars acc 0 t' in - let copt', s = - match copt with + let rest, s' = aux (id :: acc) (succ n) tl in + let s' = Intset.union s s' in + (match copt with Some c -> - let c', s' = subst_evar_constr evs n c in - Some c', Intset.union s s' - | None -> None, s - in - let copt' = option_map (subst_vars acc 0) copt' in - let rest, s' = aux (id :: acc) (succ n) tl in - mkNamedProd_or_LetIn (id, copt', t'') rest, Intset.union s' s + if noccurn 1 rest then lift (-1) rest, s' + else + let c', s'' = subst_evar_constr evs n c in + let c' = subst_vars acc 0 c' in + mkNamedProd_or_LetIn (id, Some c', t'') rest, Intset.union s'' s' + | None -> + mkNamedProd_or_LetIn (id, None, t'') rest, s') | [] -> - let t', s = subst_evar_constr evs n ev.evar_concl in + let t', s = subst_evar_constr evs n concl in subst_vars acc 0 t', s in aux [] 0 (rev hyps) open Tacticals -let rec take n l = - if n = 0 then [] else List.hd l :: take (pred n) (List.tl l) - let trunc_named_context n ctx = let len = List.length ctx in - take (len - n) ctx + list_firstn (len - n) ctx -let eterm_obligations name nclen evm t tycon = +let rec chop_product n t = + if n = 0 then Some t + else + match kind_of_term t with + | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None + | _ -> None + +let eterm_obligations name nclen isevars evm fs t tycon = (* 'Serialize' the evars, we assume that the types of the existentials refer to previous existentials in the list only *) + trace (str " In eterm: isevars: " ++ my_print_evardefs isevars); + trace (str "Term given to eterm" ++ spc () ++ + Termops.print_constr_env (Global.env ()) t); let evl = List.rev (to_list evm) in let evn = let i = ref (-1) in List.rev_map (fun (id, ev) -> incr i; - (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), ev)) evl + (id, (!i, id_of_string + (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), + ev)) evl in let evts = (* Remove existential variables in types and build the corresponding products *) @@ -137,8 +130,22 @@ let eterm_obligations name nclen evm t tycon = (fun (id, (n, nstr), ev) l -> let hyps = Environ.named_context_of_val ev.evar_hyps in let hyps = trunc_named_context nclen hyps in - let evtyp, deps = etype_of_evar l ev hyps in - let y' = (id, ((n, nstr), hyps, evtyp, deps)) in + let evtyp, deps = etype_of_evar l hyps ev.evar_concl in + let evtyp, hyps, chop = + match chop_product fs evtyp with + Some t -> + (try + trace (str "Choped a product: " ++ spc () ++ + Termops.print_constr_env (Global.env ()) evtyp ++ str " to " ++ spc () ++ + Termops.print_constr_env (Global.env ()) t); + with _ -> ()); + t, trunc_named_context fs hyps, fs + | None -> evtyp, hyps, 0 + in + let loc, k = evar_source id isevars in + let opacity = match k with QuestionMark o -> o | _ -> true in + let opaque = if not opacity || chop <> fs then None else Some chop in + let y' = (id, ((n, nstr), hyps, opaque, evtyp, deps)) in y' :: l) evn [] in @@ -146,26 +153,20 @@ let eterm_obligations name nclen evm t tycon = subst_evar_constr evts 0 t in let evars = - List.map (fun (_, ((_, name), _, typ, deps)) -> name, typ, deps) evts + List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None), deps) evts in -(* (try *) -(* trace (str "Term given to eterm" ++ spc () ++ *) -(* Termops.print_constr_env (Global.env ()) t); *) -(* trace (str "Term constructed in eterm" ++ spc () ++ *) -(* Termops.print_constr_env (Global.env ()) t'); *) -(* ignore(iter *) -(* (fun (name, typ, deps) -> *) -(* trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++ *) -(* Termops.print_constr_env (Global.env ()) typ)) *) -(* evars); *) -(* with _ -> ()); *) + (try + trace (str "Term constructed in eterm" ++ spc () ++ + Termops.print_constr_env (Global.env ()) t'); + ignore(iter + (fun (name, typ, _, deps) -> + trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++ + Termops.print_constr_env (Global.env ()) typ)) + evars); + with _ -> ()); Array.of_list (List.rev evars), t' -let mkMetas n = - let rec aux i acc = - if i > 0 then aux (pred i) (Evarutil.mk_new_meta () :: acc) - else acc - in aux n [] +let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n (* let eterm evm t (tycon : types option) = *) (* let t, tycon, evs = eterm_term evm t tycon in *) diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli index 3a571ee1..76994c06 100644 --- a/contrib/subtac/eterm.mli +++ b/contrib/subtac/eterm.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: eterm.mli 9326 2006-10-31 12:57:26Z msozeau $ i*) +(*i $Id: eterm.mli 9976 2007-07-12 11:58:30Z msozeau $ i*) open Tacmach open Term @@ -18,7 +18,10 @@ val mkMetas : int -> constr list (* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *) -val eterm_obligations : identifier -> int -> evar_map -> constr -> types option -> - (identifier * types * Intset.t) array * constr (* Obl. name, type as product and dependencies as indexes into the array *) +(* id, named context length, evars, number of + function prototypes to try to clear from evars contexts, object and optional type *) +val eterm_obligations : identifier -> int -> evar_defs -> evar_map -> int -> constr -> types option -> + (identifier * types * bool * Intset.t) array * constr + (* Obl. name, type as product, opacity (true = opaque) and dependencies as indexes into the array *) val etermtac : open_constr -> tactic diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index e31326e9..43a3bec4 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -10,7 +10,7 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) -(* $Id: g_subtac.ml4 9588 2007-02-02 16:17:13Z herbelin $ *) +(* $Id: g_subtac.ml4 9976 2007-07-12 11:58:30Z msozeau $ *) (*i camlp4deps: "parsing/grammar.cma" i*) @@ -104,15 +104,36 @@ VERNAC COMMAND EXTEND Subtac_Obligations | [ "Next" "Obligation" ] -> [ Subtac_obligations.next_obligation None ] END +VERNAC COMMAND EXTEND Subtac_Solve_Obligation +| [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> + [ Subtac_obligations.try_solve_obligation num (Some name) (Tacinterp.interp t) ] +| [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> + [ Subtac_obligations.try_solve_obligation num None (Tacinterp.interp t) ] + END + VERNAC COMMAND EXTEND Subtac_Solve_Obligations -| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations (Some name) (Tacinterp.interp t) ] -| [ "Solve" "Obligations" "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations None (Tacinterp.interp t) ] +| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> + [ Subtac_obligations.try_solve_obligations (Some name) (Tacinterp.interp t) ] +| [ "Solve" "Obligations" "using" tactic(t) ] -> + [ Subtac_obligations.try_solve_obligations None (Tacinterp.interp t) ] +| [ "Solve" "Obligations" ] -> + [ Subtac_obligations.try_solve_obligations None (Subtac_obligations.default_tactic ()) ] + END + +VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations +| [ "Solve" "All" "Obligations" "using" tactic(t) ] -> + [ Subtac_obligations.solve_all_obligations (Tacinterp.interp t) ] +| [ "Solve" "All" "Obligations" ] -> + [ Subtac_obligations.solve_all_obligations (Subtac_obligations.default_tactic ()) ] + END + +VERNAC COMMAND EXTEND Subtac_Admit_Obligations | [ "Admit" "Obligations" "of" ident(name) ] -> [ Subtac_obligations.admit_obligations (Some name) ] | [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ] END VERNAC COMMAND EXTEND Subtac_Set_Solver -| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.interp t) ] +| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.glob_tactic t) ] END VERNAC COMMAND EXTEND Subtac_Show_Obligations diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 5e46bead..8bc310d5 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac.ml 9563 2007-01-31 09:37:18Z msozeau $ *) +(* $Id: subtac.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Global open Pp @@ -37,85 +37,11 @@ open Subtac_utils open Coqlib open Printer open Subtac_errors -open Context open Eterm let require_library dirpath = let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in Library.require_library [qualid] None -(* -let subtac_one_fixpoint env isevars (f, decl) = - let ((id, n, bl, typ, body), decl) = - Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl) - in - let _ = - try trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++ - Ppconstr.pr_constr_expr body) - with _ -> () - in ((id, n, bl, typ, body), decl) -*) - -let subtac_fixpoint isevars l = - (* TODO: Copy command.build_recursive *) - () -(* -let save id const (locality,kind) hook = - let {const_entry_body = pft; - const_entry_type = tpo; - const_entry_opaque = opacity } = const in - let l,r = match locality with - | Local when Lib.sections_are_opened () -> - let k = logical_kind_of_goal_kind kind in - let c = SectionLocalDef (pft, tpo, opacity) in - let _ = declare_variable id (Lib.cwd(), c, k) in - (Local, VarRef id) - | Local -> - let k = logical_kind_of_goal_kind kind in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global, ConstRef kn) - | Global -> - let k = logical_kind_of_goal_kind kind in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global, ConstRef kn) in - Pfedit.delete_current_proof (); - hook l r; - definition_message id - -let save_named opacity = - let id,(const,persistence,hook) = Pfedit.cook_proof () in - let const = { const with const_entry_opaque = opacity } in - save id const persistence hook - -let check_anonymity id save_ident = - if atompart_of_id id <> "Unnamed_thm" then - error "This command can only be used for unnamed theorem" -(* - message("Overriding name "^(string_of_id id)^" and using "^save_ident) -*) - -let save_anonymous opacity save_ident = - let id,(const,persistence,hook) = Pfedit.cook_proof () in - let const = { const with const_entry_opaque = opacity } in - check_anonymity id save_ident; - save save_ident const persistence hook - -let save_anonymous_with_strength kind opacity save_ident = - let id,(const,_,hook) = Pfedit.cook_proof () in - let const = { const with const_entry_opaque = opacity } in - check_anonymity id save_ident; - (* we consider that non opaque behaves as local for discharge *) - save save_ident const (Global, Proof kind) hook - -let subtac_end_proof = function - | Admitted -> admit () - | Proved (is_opaque,idopt) -> - if_verbose show_script (); - match idopt with - | None -> save_named is_opaque - | Some ((_,id),None) -> save_anonymous is_opaque id - | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id - - *) open Pp open Ppconstr @@ -142,48 +68,45 @@ let start_proof_com env isevars sopt kind (bl,t) hook = let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () -let subtac_utils_path = - make_dirpath (List.map id_of_string ["Utils";contrib_name;"Coq"]) -let utils_tac s = - lazy(make_kn (MPfile subtac_utils_path) (make_dirpath []) (mk_label s)) - -let utils_call tac args = - TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args)) - let start_proof_and_print env isevars idopt k t hook = start_proof_com env isevars idopt k t hook; print_subgoals () - (*if !pcoq <> None then (out_some !pcoq).start_proof ()*) + +let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n))) + +let assumption_message id = + Options.if_verbose message ((string_of_id id) ^ " is assumed") -let _ = Subtac_obligations.set_default_tactic - (Tacinterp.eval_tactic (utils_call "subtac_simpl" [])) +let declare_assumption env isevars idl is_coe k bl c = + if not (Pfedit.refining ()) then + let evm, c, typ = + Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None + in + List.iter (Command.declare_one_assumption is_coe k c) idl + else + errorlabstrm "Command.Assumption" + (str "Cannot declare an assumption while in proof editing mode.") + +let vernac_assumption env isevars kind l = + List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c) l let subtac (loc, command) = check_required_library ["Coq";"Init";"Datatypes"]; check_required_library ["Coq";"Init";"Specif"]; - (* check_required_library ["Coq";"Logic";"JMeq"]; *) +(* check_required_library ["Coq";"Logic";"JMeq"]; *) require_library "Coq.subtac.FixSub"; require_library "Coq.subtac.Utils"; + require_library "Coq.Logic.JMeq"; let env = Global.env () in let isevars = ref (create_evar_defs Evd.empty) in try - match command with + match command with VernacDefinition (defkind, (locid, id), expr, hook) -> (match expr with ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None -(* let evm, c, ctyp = in *) -(* trace (str "Starting proof"); *) -(* Command.start_proof id goal_kind c hook; *) -(* trace (str "Started proof"); *) - | DefineBody (bl, _, c, tycon) -> - Subtac_pretyping.subtac_proof env isevars id bl c tycon - (* let tac = Eterm.etermtac (evm, c) in *) - (* trace (str "Starting proof"); *) - (* Command.start_proof id goal_kind ctyp hook; *) - (* trace (str "Started proof"); *) - (* Pfedit.by tac) *)) + Subtac_pretyping.subtac_proof env isevars id bl c tycon) | VernacFixpoint (l, b) -> let _ = trace (str "Building fixpoint") in ignore(Subtac_command.build_recursive l b) @@ -199,6 +122,8 @@ let subtac (loc, command) = start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook + | VernacAssumption (stre,l) -> + vernac_assumption env isevars stre l (*| VernacEndProof e -> subtac_end_proof e*) @@ -237,6 +162,10 @@ let subtac (loc, command) = str "Uncoercible terms:" ++ spc () ++ x ++ spc () ++ str "and" ++ spc () ++ y in msg_warning cmds + + | Cases.PatternMatchingError (env, exn) as e -> + debug 2 (Himsg.explain_pattern_matching_error env exn); + raise e | Type_errors.TypeError (env, exn) as e -> debug 2 (Himsg.explain_type_error env exn); diff --git a/contrib/subtac/subtac.mli b/contrib/subtac/subtac.mli index 25922782..b51150aa 100644 --- a/contrib/subtac/subtac.mli +++ b/contrib/subtac/subtac.mli @@ -1,3 +1,2 @@ val require_library : string -> unit -val subtac_fixpoint : 'a -> 'b -> unit val subtac : Util.loc * Vernacexpr.vernac_expr -> unit diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index fbe1ac37..04cad7c0 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -8,6 +8,7 @@ (* $Id: cases.ml 9399 2006-11-22 16:11:53Z herbelin $ *) +open Cases open Util open Names open Nameops @@ -29,52 +30,6 @@ open Evarconv open Subtac_utils -(* Pattern-matching errors *) - -type pattern_matching_error = - | BadPattern of constructor * constr - | BadConstructor of constructor * inductive - | WrongNumargConstructor of constructor * int - | WrongNumargInductive of inductive * int - | WrongPredicateArity of constr * constr * constr - | NeedsInversion of constr * constr - | UnusedClause of cases_pattern list - | NonExhaustive of cases_pattern list - | CannotInferPredicate of (constr * types) array - -exception PatternMatchingError of env * pattern_matching_error - -let raise_pattern_matching_error (loc,ctx,te) = - Stdpp.raise_with_loc loc (PatternMatchingError(ctx,te)) - -let error_bad_pattern_loc loc cstr ind = - raise_pattern_matching_error (loc, Global.env(), BadPattern (cstr,ind)) - -let error_bad_constructor_loc loc cstr ind = - raise_pattern_matching_error (loc, Global.env(), BadConstructor (cstr,ind)) - -let error_wrong_numarg_constructor_loc loc env c n = - raise_pattern_matching_error (loc, env, WrongNumargConstructor(c,n)) - -let error_wrong_numarg_inductive_loc loc env c n = - raise_pattern_matching_error (loc, env, WrongNumargInductive(c,n)) - -let error_wrong_predicate_arity_loc loc env c n1 n2 = - raise_pattern_matching_error (loc, env, WrongPredicateArity (c,n1,n2)) - -let error_needs_inversion env x t = - raise (PatternMatchingError (env, NeedsInversion (x,t))) - -module type S = sig - val compile_cases : - loc -> - (type_constraint -> env -> rawconstr -> unsafe_judgment) * - Evd.evar_defs ref -> - type_constraint -> - env -> rawconstr option * tomatch_tuple * cases_clauses -> - unsafe_judgment -end - (************************************************************************) (* Pattern-matching compilation (Cases) *) (************************************************************************) @@ -1500,7 +1455,7 @@ let set_arity_signature dep n arsign tomatchl pred x = in decomp_block [] pred (tomatchl,arsign) -let prepare_predicate_from_tycon loc dep env isevars tomatchs sign c = +let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c = let cook (n, l, env, signs) = function | c,IsInd (_,IndType(indf,realargs)) -> let indf' = lift_inductive_family n indf in @@ -1587,6 +1542,39 @@ let extract_arity_signature env0 tomatchl tmsign = | _ -> assert false in List.rev (buildrec 0 (tomatchl,tmsign)) +let extract_arity_signatures env0 tomatchl tmsign = + let get_one_sign tm (na,t) = + match tm with + | NotInd (bo,typ) -> + (match t with + | None -> [na,bo,typ] + | Some (loc,_,_,_) -> + user_err_loc (loc,"", + str "Unexpected type annotation for a term of non inductive type")) + | IsInd (_,IndType(indf,realargs)) -> + let (ind,params) = dest_ind_family indf in + let nrealargs = List.length realargs in + let realnal = + match t with + | Some (loc,ind',nparams,realnal) -> + if ind <> ind' then + user_err_loc (loc,"",str "Wrong inductive type"); + if List.length params <> nparams + or nrealargs <> List.length realnal then + anomaly "Ill-formed 'in' clause in cases"; + List.rev realnal + | None -> list_tabulate (fun _ -> Anonymous) nrealargs in + let arsign = fst (get_arity env0 indf) in + (na,None,build_dependent_inductive env0 indf) + ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign with _ -> assert false) in + let rec buildrec = function + | [],[] -> [] + | (_,tm)::ltm, x::tmsign -> + let l = get_one_sign tm x in + l :: buildrec (ltm,tmsign) + | _ -> assert false + in List.rev (buildrec (tomatchl,tmsign)) + let inh_conv_coerce_to_tycon loc env isevars j tycon = match tycon with | Some p -> @@ -1596,44 +1584,80 @@ let inh_conv_coerce_to_tycon loc env isevars j tycon = | None -> j let out_ind = function IsInd (_, IndType(x, y)) -> (x, y) | _ -> assert(false) - -let list_mapi f l = - let rec aux n = function - [] -> [] - | hd :: tl -> f n hd :: aux (succ n) tl - in aux 0 l - -let constr_of_pat env isevars ty pat idents = - let rec typ env ty pat idents = + +let string_of_name name = + match name with + | Anonymous -> "anonymous" + | Name n -> string_of_id n + +let id_of_name n = id_of_string (string_of_name n) + +let make_prime_id name = + let str = string_of_name name in + id_of_string str, id_of_string (str ^ "'") + +let prime avoid name = + let previd, id = make_prime_id name in + previd, next_ident_away_from id avoid + +let make_prime avoid prevname = + let previd, id = prime !avoid prevname in + avoid := id :: !avoid; + previd, id + +let eq_id avoid id = + let hid = id_of_string ("Heq_" ^ string_of_id id) in + let hid' = next_ident_away_from hid avoid in + hid' + +let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |]) +let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |]) +let mk_JMeq typ x typ' y = mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |]) +let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |]) + +let hole = RHole (dummy_loc, Evd.QuestionMark true) + +let context_of_arsign l = + let (x, _) = List.fold_right + (fun c (x, n) -> + (lift_rel_context n c @ x, List.length c + n)) + l ([], 0) + in x + +let constr_of_pat env isevars arsign pat avoid = + let rec typ env (ty, realargs) pat avoid = trace (str "Typing pattern " ++ Printer.pr_cases_pattern pat ++ str " in env " ++ print_env env ++ str" should have type: " ++ my_print_constr env ty); match pat with | PatVar (l,name) -> - let name, idents' = match name with - Name n -> name, idents + trace (str "Treating pattern variable " ++ str (string_of_id (id_of_name name))); + let name, avoid = match name with + Name n -> name, avoid | Anonymous -> - let n' = next_ident_away_from (id_of_string "wildcard") idents in - Name n', n' :: idents + let previd, id = prime avoid (Name (id_of_string "wildcard")) in + Name id, id :: avoid in -(* trace (str "Treating pattern variable " ++ str (string_of_id (id_of_name name))); *) - PatVar (l, name), [name, None, ty], mkRel 1, 1, idents' + trace (str "Treated pattern variable " ++ str (string_of_id (id_of_name name))); + PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid | PatCstr (l,((_, i) as cstr),args,alias) -> - let _ind = inductive_of_constructor cstr in - let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) ty in + let cind = inductive_of_constructor cstr in + let IndType (indf, _) = find_rectype env (Evd.evars_of !isevars) (lift (-(List.length realargs)) ty) in let ind, params = dest_ind_family indf in + if ind <> cind then error_bad_constructor_loc l cstr ind; let cstrs = get_constructors env indf in let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in assert(nb_args_constr = List.length args); - let idents' = idents in - let patargs, args, sign, env, n, m, idents' = + let patargs, args, sign, env, n, m, avoid = List.fold_right2 - (fun (na, c, t) ua (patargs, args, sign, env, n, m, idents) -> - let pat', sign', arg', n', idents' = typ env (lift (n - m) t) ua idents in + (fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid) -> + let pat', sign', arg', typ', argtypargs, n', avoid = + typ env (lift (n - m) t, []) ua avoid + in let args' = arg' :: List.map (lift n') args in let env' = push_rels sign' env in - (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, idents')) - ci.cs_args (List.rev args) ([], [], [], env, 0, 0, idents') + (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, avoid)) + ci.cs_args (List.rev args) ([], [], [], env, 0, 0, avoid) in let args = List.rev args in let patargs = List.rev patargs in @@ -1641,120 +1665,244 @@ let constr_of_pat env isevars ty pat idents = let cstr = mkConstruct ci.cs_cstr in let app = applistc cstr (List.map (lift (List.length sign)) params) in let app = applistc app args in -(* trace (str "New pattern: " ++ Printer.pr_cases_pattern pat'); *) -(* let alname = if alias <> Anonymous then alias else Name (id_of_string "anon") in *) -(* let al = alname, Some (mkRel 1), lift 1 ty in *) - if alias <> Anonymous then - pat', (alias, Some app, ty) :: sign, lift 1 app, n + 1, idents' - else pat', sign, app, n, idents' + trace (str "Getting type of app: " ++ my_print_constr env app); + let apptype = Retyping.get_type_of env (Evd.evars_of !isevars) app in + trace (str "Family and args of apptype: " ++ my_print_constr env apptype); + let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) apptype in + trace (str "Got Family and args of apptype: " ++ my_print_constr env apptype); + match alias with + Anonymous -> + pat', sign, app, apptype, realargs, n, avoid + | Name id -> + let sign = (alias, None, lift m ty) :: sign in + let avoid = id :: avoid in + let sign, i, avoid = + try + let env = push_rels sign env in + isevars := the_conv_x_leq (push_rels sign env) (lift (succ m) ty) (lift 1 apptype) !isevars; + trace (str "convertible types for alias : " ++ my_print_constr env (lift (succ m) ty) + ++ my_print_constr env (lift 1 apptype)); + let eq_t = mk_eq (lift (succ m) ty) + (mkRel 1) (* alias *) + (lift 1 app) (* aliased term *) + in + let neq = eq_id avoid id in + (Name neq, Some (mkRel 0), eq_t) :: sign, 2, neq :: avoid + with Reduction.NotConvertible -> sign, 1, avoid + in + (* Mark the equality as a hole *) + pat', sign, lift i app, lift i apptype, realargs, n + i, avoid in - let pat', sign, y, z, idents = typ env ty pat idents in - let c = it_mkProd_or_LetIn y sign in - trace (str "Constr_of_pat gives: " ++ my_print_constr env c); - pat', (sign, y), idents - -let mk_refl typ a = mkApp (Lazy.force eq_refl, [| typ; a |]) - -let vars_of_ctx = - List.rev_map (fun (na, _, t) -> - match na with - Anonymous -> raise (Invalid_argument "vars_of_ctx") - | Name n -> RVar (dummy_loc, n)) - -(*let build_ineqs eqns pats = - List.fold_left - (fun (sign, c) eqn -> - let acc = fold_left3 - (fun acc prevpat (ppat_sign, ppat_c, ppat_ty) (pat, pat_c) -> - match acc with - None -> None - | Some (sign,len, c) -> - if is_included pat prevpat then - let lens = List.length ppat_sign in - let acc = - (lift_rels lens ppat_sign @ sign, - lens + len, - mkApp (Lazy.force eq_ind, - [| ppat_ty ; ppat_c ; - lift (lens + len) pat_c |]) :: c) - in Some acc - else None) - (sign, c) eqn.patterns eqn.c_patterns pats - in match acc with - None -> (sign, c) - | Some (sign, len, c) -> - it_mkProd_or_LetIn c sign - - ) - ([], []) eqns*) - -let constrs_of_pats typing_fun tycon env isevars eqns tomatchs = +(* let tycon, arity = mk_tycon_from_sign env isevars arsign arity in *) + let pat', sign, patc, patty, args, z, avoid = typ env (pi3 (List.hd arsign), List.tl arsign) pat avoid in + let c = it_mkProd_or_LetIn patc sign in + trace (str "arity signature is : " ++ my_print_rel_context env arsign); + trace (str "signature is : " ++ my_print_rel_context env sign); + trace (str "patty, args are : " ++ my_print_constr env (applistc patty args)); + trace (str "Constr_of_pat gives: " ++ my_print_constr env c); + trace (str "with args: " ++ pp_list (my_print_constr (push_rels sign env)) args); + pat', (sign, patc, (pi3 (List.hd arsign), args), pat'), avoid + + +(* shadows functional version *) +let eq_id avoid id = + let hid = id_of_string ("Heq_" ^ string_of_id id) in + let hid' = next_ident_away_from hid !avoid in + avoid := hid' :: !avoid; + hid' + +let rels_of_patsign = + List.map (fun ((na, b, t) as x) -> + match b with + | Some t' when kind_of_term t' = Rel 0 -> (na, None, t) + | _ -> x) + +let vars_of_ctx ctx = + let _, y = + List.fold_right (fun (na, b, t) (prev, vars) -> + match b with + | Some t' when kind_of_term t' = Rel 0 -> + prev, + (RApp (dummy_loc, + (RRef (dummy_loc, Lazy.force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars + | _ -> + match na with + Anonymous -> raise (Invalid_argument "vars_of_ctx") + | Name n -> n, RVar (dummy_loc, n) :: vars) + ctx (id_of_string "vars_of_ctx: error", []) + in List.rev y + +let rec is_included x y = + match x, y with + | PatVar _, _ -> true + | _, PatVar _ -> true + | PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias') -> + if i = i' then List.for_all2 is_included args args' + else false + +(* liftsign is the current pattern's signature length *) +let build_ineqs prevpatterns pats liftsign = + let _tomatchs = List.length pats in + let diffs = + List.fold_left + (fun c eqnpats -> + let acc = List.fold_left2 + (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat) + (curpat_sign, curpat_c, (curpat_ty, curpat_tyargs), curpat) -> + match acc with + None -> None + | Some (sign, len, n, c) -> (* FixMe: do not work with ppat_args *) + if is_included curpat ppat then + (* Length of previous pattern's signature *) + let lens = List.length ppat_sign in + (* Accumulated length of previous pattern's signatures *) + let len' = lens + len in + trace (str "Lifting " ++ my_print_constr Environ.empty_env curpat_c ++ str " by " + ++ int len'); + let acc = + ((* Jump over previous prevpat signs *) + lift_rel_context len ppat_sign @ sign, + len', + succ n, (* nth pattern *) + mkApp (Lazy.force eq_ind, + [| lift (lens + liftsign) ppat_ty ; + liftn liftsign (succ lens) ppat_c ; + lift len' curpat_c |]) :: + List.map + (fun t -> + liftn (List.length curpat_sign) (succ len') (* Jump over the curpat signature *) + (lift lens t (* Jump over this prevpat signature *))) c) + in Some acc + else None) + (Some ([], 0, 0, [])) eqnpats pats + in match acc with + None -> c + | Some (sign, len, _, c') -> + let conj = it_mkProd_or_LetIn (mk_not (mk_conj c')) + (lift_rel_context liftsign sign) + in + conj :: c) + [] prevpatterns + in match diffs with [] -> None + | _ -> Some (mk_conj diffs) + +let subst_rel_context k ctx subst = + let (_, ctx') = + List.fold_right + (fun (n, b, t) (k, acc) -> + (succ k, (n, option_map (substnl subst k) b, substnl subst k t) :: acc)) + ctx (k, []) + in ctx' + +let lift_rel_contextn n k sign = + let rec liftrec k = function + | (na,c,t)::sign -> + (na,option_map (liftn n k) c,type_app (liftn n k) t) + ::(liftrec (k-1) sign) + | [] -> [] + in + liftrec (rel_context_length sign + k) sign + +let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs arity = let i = ref 0 in - List.fold_left - (fun (branches, eqns) eqn -> - let _, newpatterns, pats = - List.fold_right2 (fun pat (_, ty) (idents, newpatterns, pats) -> - let x, y, z = constr_of_pat env isevars (type_of_tomatch ty) pat idents in - (z, x :: newpatterns, y :: pats)) - eqn.patterns tomatchs ([], [], []) - in - let rhs_rels, signlen = - List.fold_left (fun (renv, n) (sign,_) -> - ((lift_rel_context n sign) @ renv, List.length sign + n)) - ([], 0) pats in - let eqs, _, _ = List.fold_left2 - (fun (eqs, n, slen) (sign, c) (tm, ty) -> - let len = n + signlen in (* Number of already defined equations + signature *) - let csignlen = List.length sign in - let slen' = slen - csignlen in (* Lift to get pattern variables signature *) - let c = liftn (signlen - slen) signlen c in (* Lift to jump over previous ind signatures for pattern variables outside sign - in c (e.g. type arguments of constructors instanciated by variables ) *) - let cstr = lift (slen' + n) c in -(* trace (str "lift " ++ my_print_constr (push_rels sign env) c ++ *) -(* str " by " ++ int ++ str " to get " ++ *) -(* my_print_constr (push_rels sign env) cstr); *) - let app = - mkApp (Lazy.force eq_ind, - [| lift len (type_of_tomatch ty); cstr; lift len tm |]) - in app :: eqs, succ n, slen') - ([], 0, signlen) pats tomatchs - in - let eqs_rels = List.map (fun eq -> Name (id_of_string "H"), None, eq) eqs in -(* let ineqs = build_ineqs eqns newpatterns in *) - let rhs_rels' = eqs_rels @ rhs_rels in - let rhs_env = push_rels rhs_rels' env in -(* (try trace (str "branch env: " ++ print_env rhs_env) *) -(* with _ -> trace (str "error in print branch env")); *) - let tycon = lift_tycon (List.length eqs + signlen) tycon in - - let j = typing_fun tycon rhs_env eqn.rhs.it in -(* (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++ *) -(* str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); *) -(* with _ -> *) -(* trace (str "Error in typed branch pretty printing")); *) + let (x, y, z) = + List.fold_left + (fun (branches, eqns, prevpatterns) eqn -> + let _, newpatterns, pats = + List.fold_left2 + (fun (idents, newpatterns, pats) pat arsign -> + let pat', cpat, idents = constr_of_pat env isevars arsign pat idents in + (idents, pat' :: newpatterns, cpat :: pats)) + ([], [], []) eqn.patterns sign + in + let newpatterns = List.rev newpatterns and pats = List.rev pats in + let rhs_rels, pats, signlen = + List.fold_left + (fun (renv, pats, n) (sign,c, (s, args), p) -> + (* Recombine signatures and terms of all of the row's patterns *) +(* trace (str "treating pattern:" ++ my_print_constr Environ.empty_env c); *) + let sign' = lift_rel_context n sign in + let len = List.length sign' in + (sign' @ renv, + (* lift to get outside of previous pattern's signatures. *) + (sign', liftn n (succ len) c, (s, List.map (liftn n (succ len)) args), p) :: pats, + len + n)) + ([], [], 0) pats in + let pats, _ = List.fold_left + (* lift to get outside of past patterns to get terms in the combined environment. *) + (fun (pats, n) (sign, c, (s, args), p) -> + let len = List.length sign in + ((rels_of_patsign sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n)) + ([], 0) pats + in + let rhs_rels' = rels_of_patsign rhs_rels in + let _signenv = push_rel_context rhs_rels' env in +(* trace (str "Env with signature is: " ++ my_print_env _signenv); *) + let ineqs = build_ineqs prevpatterns pats signlen in + let eqs_rels = + let eqs = (*List.concat (List.rev eqs)*) context_of_arsign eqs in + let args, nargs = + List.fold_right (fun (sign, c, (_, args), _) (allargs,n) -> +(* trace (str "treating arg:" ++ my_print_constr Environ.empty_env c); *) + (args @ c :: allargs, List.length args + succ n)) + pats ([], 0) + in + let args = List.rev args in +(* trace (str " equalities " ++ my_print_rel_context Environ.empty_env eqs); *) +(* trace (str " args " ++ pp_list (my_print_constr _signenv) args); *) + (* Make room for substitution of prime arguments by constr patterns *) + let eqs' = lift_rel_contextn signlen nargs eqs in + let eqs'' = subst_rel_context 0 eqs' args in +(* trace (str " new equalities " ++ my_print_rel_context Environ.empty_env eqs'); *) +(* trace (str " subtituted equalities " ++ my_print_rel_context _signenv eqs''); *) + eqs'' + in + let rhs_rels', lift_ineqs = + match ineqs with + None -> eqs_rels @ rhs_rels', 0 + | Some ineqs -> + (* let _ = trace (str"Generated inequalities: " ++ my_print_constr env ineqs) in *) + lift_rel_context 1 eqs_rels @ ((Anonymous, None, ineqs) :: rhs_rels'), 1 + in + let rhs_env = push_rels rhs_rels' env in +(* (try trace (str "branch env: " ++ print_env rhs_env) *) +(* with _ -> trace (str "error in print branch env")); *) + let tycon = lift_tycon (List.length eqs_rels + lift_ineqs + signlen) tycon in + + let j = typing_fun tycon rhs_env eqn.rhs.it in +(* (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++ *) +(* str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); *) +(* with _ -> *) +(* trace (str "Error in typed branch pretty printing")); *) let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in -(* (try trace (str "Branch decl: " ++ pr_rel_decl env (Name branch_name, Some bbody, btype)) *) -(* with _ -> trace (str "Error in branch decl pp")); *) + (* (try trace (str "Branch decl: " ++ pr_rel_decl env (Name branch_name, Some bbody, btype)) *) + (* with _ -> trace (str "Error in branch decl pp")); *) let branch = let bref = RVar (dummy_loc, branch_name) in - match vars_of_ctx rhs_rels with - [] -> bref - | l -> RApp (dummy_loc, bref, l) + match vars_of_ctx rhs_rels with + [] -> bref + | l -> RApp (dummy_loc, bref, l) in -(* let branch = *) -(* List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels *) -(* in *) -(* (try trace (str "New branch: " ++ Printer.pr_rawconstr branch) *) -(* with _ -> trace (str "Error in new branch pp")); *) - incr i; - let rhs = { eqn.rhs with it = branch } in - (branch_decl :: branches, - { eqn with patterns = newpatterns; rhs = rhs } :: eqns)) - ([], []) eqns - + let branch = match ineqs with + Some _ -> RApp (dummy_loc, branch, [ hole ]) + | None -> branch + in + (* let branch = *) + (* List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels *) + (* in *) + (* (try trace (str "New branch: " ++ Printer.pr_rawconstr branch) *) + (* with _ -> trace (str "Error in new branch pp")); *) + incr i; + let rhs = { eqn.rhs with it = branch } in + (branch_decl :: branches, + { eqn with patterns = newpatterns; rhs = rhs } :: eqns, + pats :: prevpatterns)) + ([], [], []) eqns + in x, y + (* liftn_rel_declaration *) @@ -1769,52 +1917,28 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs = * A type constraint but no annotation case: it is assumed non dependent. *) -let prepare_predicate_from_tycon loc typing_fun isevars env tomatchs arsign tycon = - (* We extract the signature of the arity *) -(* List.iter *) -(* (fun arsign -> *) -(* trace (str "arity signature: " ++ my_print_rel_context env arsign)) *) -(* arsign; *) -(* let env = List.fold_right push_rels arsign env in *) - let allnames = List.rev (List.map (List.map pi1) arsign) in - let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in - let pred = out_some (valcon_of_tycon tycon) in - let predcclj, pred, neqs = - let _, _, eqs = - List.fold_left2 - (fun (neqs, slift, eqs) ctx (tm,ty) -> - let len = List.length ctx in - let _name, _, _typ' = List.hd ctx in (* FixMe: Ignoring dependent inductives *) - let eq = mkApp (Lazy.force eq_ind, - [| lift (neqs + nar) (type_of_tomatch ty); - mkRel (neqs + slift); - lift (neqs + nar) tm|]) - in - (succ neqs, slift - len, (Anonymous, None, eq) :: eqs)) - (0, nar, []) (List.rev arsign) tomatchs - in - let len = List.length eqs in - it_mkProd_wo_LetIn (lift (nar + len) pred) eqs, pred, len - in - let predccl = nf_isevar !isevars predcclj in -(* let env' = List.fold_right push_rel_context arsign env in *) -(* trace (str " Env:" ++ my_print_env env' ++ str" Predicate: " ++ my_print_constr env' predccl); *) - build_initial_predicate true allnames predccl, pred - let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp = (* We extract the signature of the arity *) let arsign = extract_arity_signature env tomatchs sign in +(* (try List.iter *) +(* (fun arsign -> *) +(* trace (str "arity signature: " ++ my_print_rel_context env arsign)) *) +(* arsign; *) +(* with _ -> trace (str "error in arity signature printing")); *) let env = List.fold_right push_rels arsign env in let allnames = List.rev (List.map (List.map pi1) arsign) in - let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in -(* let _ = *) -(* option_map (fun tycon -> *) -(* isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val *) -(* (lift_tycon_type (List.length arsign) tycon)) *) -(* tycon *) -(* in *) - let predccl = (j_nf_isevar !isevars predcclj).uj_val in - Some (build_initial_predicate true allnames predccl) + match rtntyp with + | Some rtntyp -> + let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in + let predccl = (j_nf_isevar !isevars predcclj).uj_val in + Some (build_initial_predicate true allnames predccl) + | None -> + match valcon_of_tycon tycon with + | Some ty -> + let names,pred = + oldprepare_predicate_from_tycon loc false env isevars tomatchs sign ty + in Some (build_initial_predicate true names pred) + | None -> None let lift_ctx n ctx = let ctx', _ = @@ -1837,70 +1961,240 @@ let abstract_tomatch env tomatchs = ([], [], []) tomatchs in List.rev prev, ctx +let is_dependent_ind = function + IsInd (_, IndType (indf, args)) when List.length args > 0 -> true + | _ -> false + +let build_dependent_signature env evars avoid tomatchs arsign = + let avoid = ref avoid in + let arsign = List.rev arsign in + let allnames = List.rev (List.map (List.map pi1) arsign) in + let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in + let eqs, neqs, refls, slift, arsign' = + List.fold_left2 + (fun (eqs, neqs, refl_args, slift, arsigns) (tm, ty) arsign -> + (* The accumulator: + previous eqs, + number of previous eqs, + lift to get outside eqs and in the introduced variables ('as' and 'in'), + new arity signatures + *) + match ty with + IsInd (ty, IndType (indf, args)) when List.length args > 0 -> + (* Build the arity signature following the names in matched terms as much as possible *) + let argsign = List.tl arsign in (* arguments in inverse application order *) + let (appn, appb, appt) as _appsign = List.hd arsign in (* The matched argument *) +(* let _ = trace (str "Working on dependent arg: " ++ my_print_rel_context *) +(* (push_rel_context argsign env) [_appsign]) *) +(* in *) + let argsign = List.rev argsign in (* arguments in application order *) + let env', nargeqs, argeqs, refl_args, slift, argsign' = + List.fold_left2 + (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) -> +(* trace (str "Matching indexes: " ++ my_print_constr env arg ++ *) +(* str " and " ++ my_print_rel_context env [(name,b,t)]); *) + let argt = Retyping.get_type_of env evars arg in + let eq, refl_arg = + if Reductionops.is_conv env evars argt t then + (mk_eq (lift (nargeqs + slift) argt) + (mkRel (nargeqs + slift)) + (lift (nargeqs + nar) arg), + mk_eq_refl argt arg) + else + (mk_JMeq (lift (nargeqs + slift) appt) + (mkRel (nargeqs + slift)) + (lift (nargeqs + nar) argt) + (lift (nargeqs + nar) arg), + mk_JMeq_refl argt arg) + in + let previd, id = + let name = + match kind_of_term arg with + Rel n -> pi1 (lookup_rel n (rel_context env)) + | _ -> name + in + make_prime avoid name + in + (env, succ nargeqs, + (Name (eq_id avoid previd), None, eq) :: argeqs, + refl_arg :: refl_args, + pred slift, + (Name id, b, t) :: argsign')) + (env, 0, [], [], slift, []) args argsign + in +(* trace (str "neqs: " ++ int neqs ++ spc () ++ *) +(* str "nargeqs: " ++ int nargeqs ++spc () ++ *) +(* str "slift: " ++ int slift ++spc () ++ *) +(* str "nar: " ++ int nar); *) + let eq = mk_JMeq + (lift (nargeqs + slift) appt) + (mkRel (nargeqs + slift)) + (lift (nargeqs + nar) ty) + (lift (nargeqs + nar) tm) + in + let refl_eq = mk_JMeq_refl ty tm in + let previd, id = make_prime avoid appn in + (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs, + succ nargeqs, + refl_eq :: refl_args, + pred slift, + (((Name id, appb, appt) :: argsign') :: arsigns)) + + | _ -> + (* Non dependent inductive or not inductive, just use a regular equality *) + let (name, b, typ) = match arsign with [x] -> x | _ -> assert(false) in + let previd, id = make_prime avoid name in + let arsign' = (Name id, b, typ) in +(* let _ = trace (str "Working on arg: " ++ my_print_rel_context *) +(* env [arsign']) *) +(* in *) + let tomatch_ty = type_of_tomatch ty in + let eq = + mk_eq (lift nar tomatch_ty) + (mkRel slift) (lift nar tm) +(* mk_eq (lift (neqs + nar) tomatch_ty) *) +(* (mkRel (neqs + slift)) (lift (neqs + nar) tm) *) + in + ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs, + (mk_eq_refl tomatch_ty tm) :: refl_args, + pred slift, (arsign' :: []) :: arsigns)) + ([], 0, [], nar, []) tomatchs arsign + in + let arsign'' = List.rev arsign' in + assert(slift = 0); (* we must have folded over all elements of the arity signature *) +(* begin try *) +(* List.iter *) +(* (fun arsign -> *) +(* trace (str "old arity signature: " ++ my_print_rel_context env arsign)) *) +(* arsign; *) + List.iter + (fun c -> + trace (str "new arity signature: " ++ my_print_rel_context env c)) + (arsign''); +(* with _ -> trace (str "error in arity signature printing") *) +(* end; *) + let env' = push_rel_context (context_of_arsign arsign') env in + let _eqsenv = push_rel_context (context_of_arsign eqs) env' in + (try trace (str "Where env with eqs is: " ++ my_print_env _eqsenv); + trace (str "args: " ++ List.fold_left (fun acc x -> acc ++ my_print_constr env x) + (mt()) refls) + with _ -> trace (str "error in equalities signature printing")); + arsign'', allnames, nar, eqs, neqs, refls + +(* let len = List.length eqs in *) +(* it_mkProd_wo_LetIn (lift (nar + len) pred) eqs, pred, len *) + + (**************************************************************************) (* Main entry of the matching compilation *) -let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)= - let tycon0 = tycon in +let liftn_rel_context n k sign = + let rec liftrec k = function + | (na,c,t)::sign -> + (na,option_map (liftn n k) c,type_app (liftn n k) t) + ::(liftrec (k-1) sign) + | [] -> [] + in + liftrec (k + rel_context_length sign) sign + +let nf_evars_env evar_defs (env : env) : env = + let nf t = nf_isevar evar_defs t in + let env0 : env = reset_context env in + let f e (na, b, t) e' : env = + Environ.push_named (na, option_map nf b, nf t) e' + in + let env' = Environ.fold_named_context f ~init:env0 env in + Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, option_map nf b, nf t) e') + ~init:env' env + +let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) = (* We build the matrix of patterns and right-hand-side *) let matx = matx_of_eqns env eqns in (* We build the vector of terms to match consistently with the *) (* constructors found in patterns *) let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in +(* isevars := nf_evar_defs !isevars; *) +(* let env = nf_evars_env !isevars (env : env) in *) +(* trace (str "Evars : " ++ my_print_evardefs !isevars); *) +(* trace (str "Env : " ++ my_print_env env); *) + let tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in let tomatchs_len = List.length tomatchs_lets in let tycon = lift_tycon tomatchs_len tycon in let env = push_rel_context tomatchs_lets env in - match predopt with - None -> - let lets, matx = constrs_of_pats typing_fun tycon env isevars matx tomatchs in - let matx = List.rev matx in - let len = List.length lets in - let sign = - let arsign = extract_arity_signature env tomatchs (List.map snd tomatchl) in - List.map (lift_rel_context len) arsign - in - let env = push_rels lets env in - let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in - let tycon = lift_tycon len tycon in - let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in - let args = List.map (fun (tm,ty) -> mk_refl (type_of_tomatch ty) tm) tomatchs in - - (* We build the elimination predicate if any and check its consistency *) - (* with the type of arguments to match *) - let pred, opred = prepare_predicate_from_tycon loc typing_fun isevars env tomatchs sign tycon in - (* We push the initial terms to match and push their alias to rhs' envs *) - (* names of aliases will be recovered from patterns (hence Anonymous here) *) - let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in - - let pb = - { env = env; - isevars = isevars; - pred = Some pred; - tomatch = initial_pushed; - history = start_history (List.length initial_pushed); - mat = matx; - caseloc = loc; - typing_function = typing_fun } in - - let _, j = compile pb in - (* We check for unused patterns *) - List.iter (check_unused_pattern env) matx; - let ty = out_some (valcon_of_tycon tycon0) in - let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in - let j = - { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; - uj_type = ty; } - in - inh_conv_coerce_to_tycon loc env isevars j tycon0 - - | Some rtntyp -> - (* We build the elimination predicate if any and check its consistency *) - (* with the type of arguments to match *) - let tmsign = List.map snd tomatchl in - let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon rtntyp in - + let _isdep = List.exists (fun (x, y) -> is_dependent_ind y) tomatchs in + if predopt = None then + let len = List.length eqns in + let sign, allnames, signlen, eqs, neqs, args = + (* The arity signature *) + let arsign = extract_arity_signatures env tomatchs (List.map snd tomatchl) in + (* Build the dependent arity signature, the equalities which makes + the first part of the predicate and their instantiations. *) + trace (str "Arity signatures : " ++ my_print_rel_context env (context_of_arsign arsign)); + let avoid = [] in + build_dependent_signature env (Evd.evars_of !isevars) avoid tomatchs arsign + + in + let tycon_constr = + match valcon_of_tycon tycon with + | None -> mkExistential env isevars + | Some t -> t + in + let lets, matx = + (* Type the rhs under the assumption of equations *) + constrs_of_pats typing_fun tycon env isevars matx tomatchs sign neqs + (eqs : rel_context list) (lift (signlen + neqs) tycon_constr) in + + let matx = List.rev matx in + let _ = assert(len = List.length lets) in + let env = push_rels lets env in + let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in + let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in + let args = List.rev_map (lift len) args in + let sign = List.map (lift_rel_context len) sign in + let pred = it_mkProd_wo_LetIn (lift (signlen + neqs) tycon_constr) + (context_of_arsign eqs) in + + let pred = liftn len (succ signlen) pred in +(* it_mkProd_wo_LetIn (lift (len + signlen + neqs) tycon_constr) (liftn_rel_context len signlen eqs) in*) + (* We build the elimination predicate if any and check its consistency *) + (* with the type of arguments to match *) + let _signenv = List.fold_right push_rels sign env in +(* trace (str "Using predicate: " ++ my_print_constr signenv pred ++ str " in env: " ++ my_print_env signenv ++ str " len is " ++ int len); *) + + let pred = + (* prepare_predicate_from_tycon loc typing_fun isevars env tomatchs eqs allnames signlen sign tycon in *) + build_initial_predicate true allnames pred in + (* We push the initial terms to match and push their alias to rhs' envs *) + (* names of aliases will be recovered from patterns (hence Anonymous here) *) + let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in + + let pb = + { env = env; + isevars = isevars; + pred = Some pred; + tomatch = initial_pushed; + history = start_history (List.length initial_pushed); + mat = matx; + caseloc = loc; + typing_function = typing_fun } in + + let _, j = compile pb in + (* We check for unused patterns *) + List.iter (check_unused_pattern env) matx; + let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in + let j = + { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; + uj_type = lift (-tomatchs_len) (nf_isevar !isevars tycon_constr); } + in j +(* inh_conv_coerce_to_tycon loc env isevars j tycon0 *) + else + (* We build the elimination predicate if any and check its consistency *) + (* with the type of arguments to match *) + let tmsign = List.map snd tomatchl in + let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon predopt in + (* We push the initial terms to match and push their alias to rhs' envs *) (* names of aliases will be recovered from patterns (hence Anonymous here) *) let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in diff --git a/contrib/subtac/subtac_cases.mli b/contrib/subtac/subtac_cases.mli index 9e902126..02fe016d 100644 --- a/contrib/subtac/subtac_cases.mli +++ b/contrib/subtac/subtac_cases.mli @@ -19,32 +19,5 @@ open Rawterm open Evarutil (*i*) -type pattern_matching_error = - | BadPattern of constructor * constr - | BadConstructor of constructor * inductive - | WrongNumargConstructor of constructor * int - | WrongNumargInductive of inductive * int - | WrongPredicateArity of constr * constr * constr - | NeedsInversion of constr * constr - | UnusedClause of cases_pattern list - | NonExhaustive of cases_pattern list - | CannotInferPredicate of (constr * types) array - -exception PatternMatchingError of env * pattern_matching_error - -val error_wrong_numarg_constructor_loc : loc -> env -> constructor -> int -> 'a - -val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a - -(*s Compilation of pattern-matching. *) - -module type S = sig - val compile_cases : - loc -> - (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref -> - type_constraint -> - env -> rawconstr option * tomatch_tuple * cases_clauses -> - unsafe_judgment -end - -module Cases_F(C : Coercion.S) : S +(*s Compilation of pattern-matching, subtac style. *) +module Cases_F(C : Coercion.S) : Cases.S diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 3613ec4f..c764443f 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_coercion.ml 9563 2007-01-31 09:37:18Z msozeau $ *) +(* $Id: subtac_coercion.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Util open Names @@ -26,7 +26,6 @@ open Subtac_utils open Coqlib open Printer open Subtac_errors -open Context open Eterm open Pp @@ -86,6 +85,13 @@ module Coercion = struct let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c + let lift_args n sign = + let rec liftrec k = function + | t::sign -> liftn n k t :: (liftrec (k-1) sign) + | [] -> [] + in + liftrec (List.length sign) sign + let rec mu env isevars t = let isevars = ref isevars in let rec aux v = @@ -113,15 +119,41 @@ module Coercion = struct (* (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++ *) (* str " to "++ my_print_constr env y) *) (* with _ -> ()); *) - try - isevars := the_conv_x_leq env x y !isevars; -(* (try debug 1 (str "Unified " ++ (my_print_constr env x) ++ *) -(* str " and "++ my_print_constr env y); *) -(* with _ -> ()); *) - None - with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y) + let x = hnf env isevars x and y = hnf env isevars y in + try + isevars := the_conv_x_leq env x y !isevars; + (* (try debug 1 (str "Unified " ++ (my_print_constr env x) ++ *) + (* str " and "++ my_print_constr env y); *) + (* with _ -> ()); *) + None + with Reduction.NotConvertible -> coerce' env x y and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env isevars x y in + let rec coerce_application typ c c' l l' = + let len = Array.length l in + let rec aux tele typ i co = + if i < len then + let hdx = l.(i) and hdy = l'.(i) in + try isevars := the_conv_x_leq env hdx hdy !isevars; + let (n, eqT, restT) = destProd typ in + aux (hdx :: tele) (subst1 hdy restT) (succ i) co + with Reduction.NotConvertible -> + let (n, eqT, restT) = destProd typ in + let restargs = lift_args 1 + (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i))))) + in + let args = List.rev (restargs @ mkRel 1 :: lift_args 1 tele) in + let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in + let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in +(* let jmeq = mkApp (Lazy.force jmeq_ind, [| eqT; hdx; eqT; hdy |]) in *) + let evar = make_existential dummy_loc env isevars eq in + let eq_app x = mkApp (Lazy.force eq_rect, + [| eqT; hdx; pred; x; hdy; evar|]) in + trace (str"Inserting coercion at application"); + aux (hdy :: tele) (subst1 hdy restT) (succ i) (fun x -> eq_app (co x)) + else co + in aux [] typ 0 (fun x -> x) + in (* (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++ *) (* str " to "++ my_print_constr env y); *) (* with _ -> ()); *) @@ -214,40 +246,25 @@ module Coercion = struct mkApp (prod.intro, [| a'; b'; x ; y |])) end else - (* if len = 1 && len = Array.length l' && i = i' then *) -(* let argx, argy = l.(0), l'.(0) in *) -(* let indtyp = Inductiveops.type_of_inductive env i in *) -(* let argname, argtype, _ = destProd indtyp in *) -(* let eq = *) -(* mkApp (Lazy.force eqind, [| argtype; argx; argy |]) *) -(* in *) -(* let pred = mkLambda (argname, argtype, *) -(* mkApp (mkInd i, [| mkRel 1 |])) *) -(* in *) -(* let evar = make_existential dummy_loc env isevars eq in *) -(* Some (fun x -> *) -(* mkApp (Lazy.force eqrec, *) -(* [| argtype; argx; pred; x; argy; evar |])) *) -(* else *)subco () + if i = i' && len = Array.length l' then + let evm = evars_of !isevars in + let typ = Typing.type_of env evm c in + (try subco () + with NoSubtacCoercion -> + +(* if not (is_arity env evm typ) then *) + Some (coerce_application typ c c' l l')) +(* else subco () *) + else + subco () | x, y when x = y -> - let lam_type = Typing.type_of env (evars_of !isevars) c in - let rec coerce typ i co = - if i < Array.length l then - let hdx = l.(i) and hdy = l'.(i) in - let (n, eqT, restT) = destProd typ in - let pred = mkLambda (n, eqT, mkApp (lift 1 c, [| mkRel 1 |])) in - let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in - let evar = make_existential dummy_loc env isevars eq in - let eq_app x = mkApp (Lazy.force eq_rect, - [| eqT; hdx; pred; x; hdy; evar|]) - in - coerce (subst1 hdy restT) (succ i) (fun x -> eq_app (co x)) - else co - in - if Array.length l = Array.length l' then ( - trace (str"Inserting coercion at application"); - Some (coerce lam_type 0 (fun x -> x)) - ) else subco () + if Array.length l = Array.length l' then + let evm = evars_of !isevars in + let lam_type = Typing.type_of env evm c in +(* if not (is_arity env evm lam_type) then ( *) + Some (coerce_application lam_type c c' l l') +(* ) else subco () *) + else subco () | _ -> subco ()) | _, _ -> subco () diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 68ab8c46..86139039 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -56,7 +56,6 @@ let interp_gen kind isevars env ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in - let c' = Subtac_utils.rewrite_cases env c' in (* (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *) let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in evar_nf isevars c' @@ -178,10 +177,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let env = Global.env() in let nc = named_context env in let nc_len = named_context_length nc in -(* let pr c = my_print_constr env c in *) -(* let prr = Printer.pr_rel_context env in *) -(* let prn = Printer.pr_named_context env in *) -(* let pr_rel env = Printer.pr_rel_context env in *) + let pr c = my_print_constr env c in + let prr = Printer.pr_rel_context env in + let _prn = Printer.pr_named_context env in + let _pr_rel env = Printer.pr_rel_context env in (* let _ = *) (* try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ *) (* Ppconstr.pr_binders bl ++ str " : " ++ *) @@ -193,40 +192,42 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in let before_length, after_length = List.length before, List.length after in let argid = match argname with Name n -> n | _ -> assert(false) in - let _liftafter = lift_binders 1 after_length after in + let liftafter = lift_binders 1 after_length after in let envwf = push_rel_context before env in let wf_rel, wf_rel_fun, measure_fn = let rconstr_body, rconstr = let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in let env = push_rel_context [arg] envwf in let capp = interp_constr isevars env app in - capp, mkLambda (argname, argtyp, capp) + capp, mkLambda (argname, argtyp, capp) in + trace (str"rconstr_body: " ++ pr rconstr_body); if measure then let lt_rel = constr_of_global (Lazy.force lt_ref) in let name s = Name (id_of_string s) in - let wf_rel_fun = - (fun x y -> - mkApp (lt_rel, [| subst1 x rconstr_body; - subst1 y rconstr_body |])) - in + let wf_rel_fun lift x y = (* lift to before_env *) + trace (str"lifter rconstr_body:" ++ pr (liftn lift 2 rconstr_body)); + mkApp (lt_rel, [| subst1 x (liftn lift 2 rconstr_body); + subst1 y (liftn lift 2 rconstr_body) |]) + in let wf_rel = mkLambda (name "x", argtyp, mkLambda (name "y", lift 1 argtyp, - wf_rel_fun (mkRel 2) (mkRel 1))) + wf_rel_fun 0 (mkRel 2) (mkRel 1))) in wf_rel, wf_rel_fun , Some rconstr - else rconstr, (fun x y -> mkApp (rconstr, [|x; y|])), None + else rconstr, (fun lift x y -> mkApp (rconstr, [|x; y|])), None in let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) in let argid' = id_of_string (string_of_id argid ^ "'") in - let wfarg len = (Name argid', None, + let wfarg len = (Name argid', None, mkSubset (Name argid') (lift len argtyp) - (wf_rel_fun (mkRel 1) (mkRel (len + 1)))) + (wf_rel_fun (succ len) (mkRel 1) (mkRel (len + 1)))) in let top_bl = after @ (arg :: before) in - let intern_bl = after @ (wfarg 1 :: arg :: before) in + let intern_bl = liftafter @ (wfarg 1 :: arg :: before) in + (try trace (str "Intern bl: " ++ prr intern_bl) with _ -> ()); let top_env = push_rel_context top_bl env in let _intern_env = push_rel_context intern_bl env in let top_arity = interp_type isevars top_env arityc in @@ -234,36 +235,45 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let projection = mkApp (proj, [| argtyp ; (mkLambda (Name argid', argtyp, - (wf_rel_fun (mkRel 1) (mkRel 3)))) ; + (wf_rel_fun 1 (mkRel 1) (mkRel 3)))) ; mkRel 1 |]) in - (* (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ()); *) - let intern_arity = substnl [projection] after_length top_arity in -(* (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ()); *) + let intern_arity = it_mkProd_or_LetIn top_arity after in + (try trace (str "After length: " ++ int after_length ++ str "Top env: " ++ prr top_bl ++ spc () ++ str "Top arity: " ++ my_print_constr top_env top_arity); + trace (str "Before lifting arity: " ++ my_print_constr env top_arity) with _ -> ()); + (* Top arity is in top_env = after :: arg :: before *) +(* let intern_arity' = liftn 1 (succ after_length) top_arity in (\* arity in after :: wfarg :: arg :: before *\) *) +(* (try trace (str "projection: " "After lifting arity: " ++ my_print_constr env intern_arity' ++ spc ()); *) +(* trace (str "Intern env: " ++ prr intern_bl ++ str "intern_arity': " ++ my_print_constr _intern_env intern_arity') with _ -> ()); *) + let intern_arity = substl [projection] intern_arity in (* substitute the projection of wfarg for arg *) + (try trace (str "Top arity after subst: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); +(* let intern_arity = liftn 1 (succ after_length) intern_arity in (\* back in after :: wfarg :: arg :: before (ie, jump over arg) *\) *) +(* (try trace (str "Top arity after subst and lift: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); *) let intern_before_env = push_rel_context before env in - let intern_fun_bl = after @ [wfarg 1] in +(* let intern_fun_bl = liftafter @ [wfarg 1] in (\* FixMe dependencies *\) *) (* (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ()); *) - let intern_fun_arity = intern_arity in -(* (try debug 2 (str "Intern fun arity: " ++ *) -(* my_print_constr intern_env intern_fun_arity) with _ -> ()); *) - let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in + (try trace (str "Intern arity: " ++ + my_print_constr _intern_env intern_arity) with _ -> ()); + let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in + (try trace (str "Intern fun arity product: " ++ + my_print_constr (push_rel_context [arg] intern_before_env) intern_fun_arity_prod) with _ -> ()); let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in - let fun_bl = after @ (intern_fun_binder :: [arg]) in + let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in (* (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ()); *) let fun_env = push_rel_context fun_bl intern_before_env in let fun_arity = interp_type isevars fun_env arityc in let intern_body = interp_casted_constr isevars fun_env body fun_arity in let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in -(* let _ = *) -(* try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++ *) -(* str "Intern bl" ++ prr intern_bl ++ spc () ++ *) -(* str "Top bl" ++ prr top_bl ++ spc () ++ *) -(* str "Intern arity: " ++ pr intern_arity ++ *) -(* str "Top arity: " ++ pr top_arity ++ spc () ++ *) + let _ = + try trace ((* str "Fun bl: " ++ prr fun_bl ++ spc () ++ *) + str "Intern bl" ++ prr intern_bl ++ spc ()) +(* str "Top bl" ++ prr top_bl ++ spc () ++ *) +(* str "Intern arity: " ++ pr intern_arity ++ *) +(* str "Top arity: " ++ pr top_arity ++ spc () ++ *) (* str "Intern body " ++ pr intern_body_lam) *) -(* with _ -> () *) -(* in *) + with _ -> () + in let _impl = if Impargs.is_implicit_args() then Impargs.compute_implicits top_env top_arity @@ -276,13 +286,16 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = mkApp (constr_of_reference (Lazy.force fix_sub_ref), [| argtyp ; wf_rel ; - make_existential dummy_loc intern_before_env isevars wf_proof ; + make_existential dummy_loc ~opaque:false intern_before_env isevars wf_proof ; prop ; intern_body_lam |]) | Some f -> - mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), - [| argtyp ; f ; prop ; - intern_body_lam |]) + lift (succ after_length) + (mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), + [| argtyp ; + f ; + prop ; + intern_body_lam |])) in let def_appl = applist (fix_def, gen_rels (after_length + 1)) in let def = it_mkLambda_or_LetIn def_appl binders_rel in @@ -294,15 +307,22 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = (* ++ str "Coq type: " ++ my_print_constr env fullctyp) *) (* with _ -> () *) (* in *) - let evm = non_instanciated_map env isevars in + let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in + let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in + let evm = non_instanciated_map env isevars evm in + (* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *) - let evars, evars_def = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in + let evars, evars_def = Eterm.eterm_obligations recname nc_len !isevars evm 0 fullcoqc (Some fullctyp) in (* (try trace (str "Generated obligations : "); *) (* Array.iter *) (* (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *) (* evars; *) (* with _ -> ()); *) Subtac_obligations.add_definition recname evars_def fullctyp evars + +let nf_evar_context isevars ctx = + List.map (fun (n, b, t) -> + (n, option_map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx let build_mutrec l boxed = let sigma = Evd.empty and env = Global.env () in @@ -368,10 +388,13 @@ let build_mutrec l boxed = let (isevars, info, def) = defrec.(i) in (* let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in *) let def = evar_nf isevars def in + let x, y, typ = arrec.(i) in + let typ = evar_nf isevars typ in + arrec.(i) <- (x, y, typ); + let rec_sign = nf_evar_context !isevars rec_sign in let isevars = Evd.undefined_evars !isevars in (* let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in *) let evm = Evd.evars_of isevars in - let _, _, typ = arrec.(i) in let id = namerec.(i) in (* Generalize by the recursive prototypes *) let def = @@ -379,7 +402,7 @@ let build_mutrec l boxed = and typ = Termops.it_mkNamedProd_or_LetIn typ rec_sign in - let evars, def = Eterm.eterm_obligations id nc_len evm def (Some typ) in + let evars, def = Eterm.eterm_obligations id nc_len isevars evm recdefs def (Some typ) in collect_evars (succ i) ((id, def, typ, evars) :: acc) else acc in diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml deleted file mode 100644 index bb35833f..00000000 --- a/contrib/subtac/subtac_interp_fixpoint.ml +++ /dev/null @@ -1,154 +0,0 @@ -open Global -open Pp -open Util -open Names -open Sign -open Evd -open Term -open Termops -open Reductionops -open Environ -open Type_errors -open Typeops -open Libnames -open Classops -open List -open Recordops -open Evarutil -open Pretype_errors -open Rawterm -open Evarconv -open Pattern -open Dyn -open Topconstr - -open Subtac_coercion -open Subtac_utils -open Coqlib -open Printer -open Subtac_errors -open Context -open Eterm - - -let mkAppExplC (f, args) = CAppExpl (dummy_loc, (None, f), args) - -let mkSubset name typ prop = - mkAppExplC (sig_ref, - [ typ; mkLambdaC ([name], typ, prop) ]) - -let mkProj1 u p x = - mkAppExplC (proj1_sig_ref, [ u; p; x ]) - -let mkProj2 u p x = - mkAppExplC (proj2_sig_ref, [ u; p; x ]) - -let list_of_local_binders l = - let rec aux acc = function - Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, c) :: acc) tl - | Topconstr.LocalRawAssum (nl, c) :: tl -> - aux (List.fold_left (fun acc n -> (n, c) :: acc) acc nl) tl - | [] -> List.rev acc - in aux [] l - -let abstract_constr_expr_bl abs c bl = - List.fold_right (fun (n, t) c -> abs ([n], t, c)) bl c - -let pr_binder_list b = - List.fold_right (fun ((loc, name), t) acc -> Nameops.pr_name name ++ str " : " ++ - Ppconstr.pr_constr_expr t ++ spc () ++ acc) b (mt ()) - - -let rec rewrite_rec_calls l c = c -(* -let rewrite_fixpoint env l (f, decl) = - let (id, (n, ro), bl, typ, body) = f in - let body = rewrite_rec_calls l body in - match ro with - CStructRec -> ((id, (n, ro), bl, typ, body), decl) - | CWfRec wfrel -> - let bls = list_of_local_binders bl in - let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id id ++ - Ppconstr.pr_binders bl ++ str " : " ++ - Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++ - Ppconstr.pr_constr_expr body) - in - let before, after = list_chop n bls in - let _ = trace (str "Binders before the recursion arg: " ++ spc () ++ - pr_binder_list before ++ str "; after the recursion arg: " ++ - pr_binder_list after) - in - let ((locn, name) as lnid, ntyp), after = match after with - hd :: tl -> hd, tl - | _ -> assert(false) (* Rec arg must be in after *) - in - let nid = match name with - Name id -> id - | Anonymous -> assert(false) (* Rec arg _must_ be named *) - in - let _wfproof = - let _wf_rel = mkAppExplC (well_founded_ref, [ntyp; wfrel]) in - (*make_existential_expr dummy_loc before wf_rel*) - mkRefC lt_wf_ref - in - let nid', accproofid = - let nid = string_of_id nid in - id_of_string (nid ^ "'"), id_of_string ("Acc_" ^ nid) - in - let lnid', laccproofid = (dummy_loc, Name nid'), (dummy_loc, Name accproofid) in - let wf_prop = (mkAppC (wfrel, [ mkIdentC nid'; mkIdentC nid ])) in - let lam_wf_prop = mkLambdaC ([lnid'], ntyp, wf_prop) in - let typnid' = mkSubset lnid' ntyp wf_prop in - let internal_type = - abstract_constr_expr_bl mkProdC - (mkProdC ([lnid'], typnid', - mkLetInC (lnid, mkProj1 ntyp lam_wf_prop (mkIdentC nid'), - abstract_constr_expr_bl mkProdC typ after))) - before - in - let body' = - let body = - (* cast or we will loose some info at pretyping time as body - is a function *) - CCast (dummy_loc, body, CastConv DEFAULTcast, typ) - in - let body' = (* body abstracted by rec call *) - mkLambdaC ([(dummy_loc, Name id)], internal_type, body) - in - mkAppC (body', - [mkLambdaC - ([lnid'], typnid', - mkAppC (mkIdentC id, - [mkProj1 ntyp lam_wf_prop (mkIdentC nid'); - (mkAppExplC (acc_inv_ref, - [ ntyp; wfrel; - mkIdentC nid; - mkIdentC accproofid; - mkProj1 ntyp lam_wf_prop (mkIdentC nid'); - mkProj2 ntyp lam_wf_prop (mkIdentC nid') ])) ]))]) - in - let acctyp = mkAppExplC (acc_ref, [ ntyp; wfrel; mkIdentC nid ]) in - let bl' = - let rec aux acc = function - Topconstr.LocalRawDef _ as x :: tl -> - aux (x :: acc) tl - | Topconstr.LocalRawAssum (bl, typ) as assum :: tl -> - let rec aux' bl' = function - ((loc, name') as x) :: tl -> - if name' = name then - (if tl = [] then [] else [LocalRawAssum (tl, typ)]) @ - LocalRawAssum ([(dummy_loc, Name accproofid)], acctyp) :: - [LocalRawAssum (List.rev (x :: bl'), typ)] - else aux' (x :: bl') tl - | [] -> [assum] - in aux (aux' [] bl @ acc) tl - | [] -> List.rev acc - in aux [] bl - in - let _ = trace (str "Rewrote fixpoint: " ++ Ppconstr.pr_id id ++ - Ppconstr.pr_binders bl' ++ str " : " ++ - Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++ - Ppconstr.pr_constr_expr body') - in (id, (succ n, ro), bl', typ, body'), decl - -*) diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli deleted file mode 100644 index 149e7580..00000000 --- a/contrib/subtac/subtac_interp_fixpoint.mli +++ /dev/null @@ -1,17 +0,0 @@ -val mkAppExplC : - Libnames.reference * Topconstr.constr_expr list -> Topconstr.constr_expr -val mkSubset : - Names.name Util.located -> - Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr -val mkProj1 : - Topconstr.constr_expr -> - Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr -val mkProj2 : - Topconstr.constr_expr -> - Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr -val list_of_local_binders : - Topconstr.local_binder list -> - (Names.name Util.located * Topconstr.constr_expr) list -val pr_binder_list : - (('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds -val rewrite_rec_calls : 'a -> 'b -> 'b diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index d6c1772f..d182f7cd 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -1,3 +1,4 @@ +(* -*- default-directory: "~/research/coq/trunk/" -*- *) open Printf open Pp open Subtac_utils @@ -12,12 +13,22 @@ open Decl_kinds open Util open Evd -type obligation_info = (Names.identifier * Term.types * Intset.t) array +let pperror cmd = Util.errorlabstrm "Subtac" cmd +let error s = pperror (str s) + +exception NoObligations of identifier option + +let explain_no_obligations = function + Some ident -> str "No obligations for program " ++ str (string_of_id ident) + | None -> str "No obligations remaining" + +type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array type obligation = { obl_name : identifier; obl_type : types; obl_body : constr option; + obl_opaque : bool; obl_deps : Intset.t; } @@ -36,8 +47,9 @@ let assumption_message id = Options.if_verbose message ((string_of_id id) ^ " is assumed") let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC +let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ()) -let set_default_tactic t = default_tactic := t +let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t let evar_of_obligation o = { evar_hyps = Global.named_context_val () ; evar_concl = o.obl_type ; @@ -81,26 +93,35 @@ let map_first m = let from_prg : program_info ProgMap.t ref = ref ProgMap.empty +let freeze () = !from_prg, !default_tactic_expr +let unfreeze (v, t) = from_prg := v; set_default_tactic t +let init () = + from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.utils_call "subtac_simpl" []) + let _ = Summary.declare_summary "program-tcc-table" - { Summary.freeze_function = (fun () -> !from_prg); - Summary.unfreeze_function = - (fun v -> from_prg := v); - Summary.init_function = - (fun () -> from_prg := ProgMap.empty); + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; Summary.survive_module = false; Summary.survive_section = false } -open Evd +let progmap_union = ProgMap.fold ProgMap.add -let terms_of_evar ev = - match ev.evar_body with - Evar_defined b -> - let nc = Environ.named_context_of_val ev.evar_hyps in - let body = Termops.it_mkNamedLambda_or_LetIn b nc in - let typ = Termops.it_mkNamedProd_or_LetIn ev.evar_concl nc in - body, typ - | _ -> assert(false) +let cache (_, (infos, tac)) = + from_prg := infos; + default_tactic_expr := tac + +let (input,output) = + declare_object + { (default_object "Program state") with + cache_function = cache; + load_function = (fun _ -> cache); + open_function = (fun _ -> cache); + classify_function = (fun _ -> Dispose); + export_function = (fun x -> Some x) } + +open Evd let rec intset_to = function -1 -> Intset.empty @@ -113,7 +134,8 @@ let subst_body prg = let declare_definition prg = let body = subst_body prg in (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++ - my_print_constr (Global.env()) body); + my_print_constr (Global.env()) body ++ str " : " ++ + my_print_constr (Global.env()) prg.prg_type); with _ -> ()); let ce = { const_entry_body = body; @@ -163,7 +185,7 @@ let declare_obligation obl body = let ce = { const_entry_body = body; const_entry_type = Some obl.obl_type; - const_entry_opaque = false; + const_entry_opaque = obl.obl_opaque; const_entry_boxed = false} in let constant = Declare.declare_constant obl.obl_name @@ -190,42 +212,53 @@ let red = Reductionops.nf_betaiota let init_prog_info n b t deps nvrec obls = let obls' = Array.mapi - (fun i (n, t, d) -> + (fun i (n, t, o, d) -> debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d)); { obl_name = n ; obl_body = None; - obl_type = red t; + obl_type = red t; obl_opaque = o; obl_deps = d }) obls in { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_nvrec = nvrec; } -let pperror cmd = Util.errorlabstrm "Subtac" cmd -let error s = pperror (str s) - let get_prog name = let prg_infos = !from_prg in match name with Some n -> (try ProgMap.find n prg_infos - with Not_found -> error ("No obligations for program " ^ string_of_id n)) + with Not_found -> raise (NoObligations (Some n))) | None -> (let n = map_cardinal prg_infos in match n with - 0 -> error "No obligations remaining" + 0 -> raise (NoObligations None) | 1 -> map_first prg_infos | _ -> error "More than one program with unsolved obligations") +let get_prog_err n = + try get_prog n with NoObligations id -> pperror (explain_no_obligations id) + let obligations_solved prg = (snd prg.prg_obligations) = 0 +let update_state s = +(* msgnl (str "Updating obligations info"); *) + Lib.add_anonymous_leaf (input s) + +let obligations_message rem = + if rem > 0 then + if rem = 1 then + Options.if_verbose msgnl (int rem ++ str " obligation remaining") + else + Options.if_verbose msgnl (int rem ++ str " obligations remaining") + else + Options.if_verbose msgnl (str "No more obligations remaining") + let update_obls prg obls rem = let prg' = { prg with prg_obligations = (obls, rem) } in from_prg := map_replace prg.prg_name prg' !from_prg; - if rem > 0 then ( - Options.if_verbose msgnl (int rem ++ str " obligation(s) remaining"); - ) + obligations_message rem; + if rem > 0 then () else ( - Options.if_verbose msgnl (str "No more obligations remaining"); match prg'.prg_deps with [] -> declare_definition prg'; @@ -235,7 +268,10 @@ let update_obls prg obls rem = if List.for_all (fun x -> obligations_solved x) progs then (declare_mutual_definition progs; from_prg := List.fold_left - (fun acc x -> ProgMap.remove x.prg_name acc) !from_prg progs)) + (fun acc x -> + ProgMap.remove x.prg_name acc) !from_prg progs)); + update_state (!from_prg, !default_tactic_expr); + rem let is_defined obls x = obls.(x).obl_body <> None @@ -246,7 +282,24 @@ let deps_remaining obls deps = else x :: acc) deps [] -let solve_obligation prg num = +let kind_of_opacity o = + if o then Subtac_utils.goal_proof_kind + else Subtac_utils.goal_kind + +let obligations_of_evars evars = + let arr = + Array.of_list + (List.map + (fun (n, t) -> + { obl_name = n; + obl_type = t; + obl_body = None; + obl_opaque = false; + obl_deps = Intset.empty; + }) evars) + in arr, Array.length arr + +let rec solve_obligation prg num = let user_num = succ num in let obls, rem = prg.prg_obligations in let obl = obls.(num) in @@ -256,22 +309,23 @@ let solve_obligation prg num = match deps_remaining obls obl.obl_deps with [] -> let obl = subst_deps_obl obls obl in - Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type + Command.start_proof obl.obl_name (kind_of_opacity obl.obl_opaque) obl.obl_type (fun strength gr -> debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished"); let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in let obls = Array.copy obls in let _ = obls.(num) <- obl in - update_obls prg obls (pred rem)); + if update_obls prg obls (pred rem) <> 0 then + auto_solve_obligations (Some prg.prg_name)); trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); Pfedit.by !default_tactic | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) -let subtac_obligation (user_num, name, typ) = +and subtac_obligation (user_num, name, typ) = let num = pred user_num in - let prg = get_prog name in + let prg = get_prog_err name in let obls, rem = prg.prg_obligations in if num < Array.length obls then let obl = obls.(num) in @@ -280,20 +334,8 @@ let subtac_obligation (user_num, name, typ) = | Some r -> error "Obligation already solved" else error (sprintf "Unknown obligation number %i" (succ num)) - -let obligations_of_evars evars = - let arr = - Array.of_list - (List.map - (fun (n, t) -> - { obl_name = n; - obl_type = t; - obl_body = None; - obl_deps = Intset.empty; - }) evars) - in arr, Array.length arr - -let solve_obligation_by_tac prg obls i tac = + +and solve_obligation_by_tac prg obls i tac = let obl = obls.(i) in match obl.obl_body with Some _ -> false @@ -302,13 +344,15 @@ let solve_obligation_by_tac prg obls i tac = if deps_remaining obls obl.obl_deps = [] then let obl = subst_deps_obl obls obl in let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in - obls.(i) <- { obl with obl_body = Some t }; + if obl.obl_opaque then + obls.(i) <- declare_obligation obl t + else + obls.(i) <- { obl with obl_body = Some t }; true else false with _ -> false) -let solve_obligations n tac = - let prg = get_prog n in +and solve_prg_obligations prg tac = let obls, rem = prg.prg_obligations in let rem = ref rem in let obls' = Array.copy obls in @@ -320,6 +364,27 @@ let solve_obligations n tac = in update_obls prg obls' !rem +and solve_obligations n tac = + let prg = get_prog_err n in + solve_prg_obligations prg tac + +and solve_all_obligations tac = + ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg + +and try_solve_obligation n prg tac = + let prg = get_prog prg in + let obls, rem = prg.prg_obligations in + let obls' = Array.copy obls in + if solve_obligation_by_tac prg obls' n tac then + ignore(update_obls prg obls' (pred rem)); + +and try_solve_obligations n tac = + try ignore (solve_obligations n tac) with NoObligations _ -> () + +and auto_solve_obligations n : unit = + Options.if_verbose msgnl (str "Solving obligations automatically..."); + try_solve_obligations n !default_tactic + let add_definition n b t obls = Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); let prg = init_prog_info n b t [] (Array.make 0 0) obls in @@ -332,7 +397,7 @@ let add_definition n b t obls = let len = Array.length obls in let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in from_prg := ProgMap.add n prg !from_prg; - solve_obligations (Some n) !default_tactic) + auto_solve_obligations (Some n)) let add_mutual_definitions l nvrec = let deps = List.map (fun (n, b, t, obls) -> n) l in @@ -343,22 +408,21 @@ let add_mutual_definitions l nvrec = !from_prg l in from_prg := upd; - List.iter (fun x -> solve_obligations (Some x) !default_tactic) deps + List.iter (fun x -> auto_solve_obligations (Some x)) deps let admit_obligations n = - let prg = get_prog n in + let prg = get_prog_err n in let obls, rem = prg.prg_obligations in - let obls' = - Array.mapi (fun i x -> + Array.iteri (fun i x -> match x.obl_body with None -> - let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in - assumption_message x.obl_name; - { x with obl_body = Some (mkConst kn) } - | Some _ -> x) - obls - in - update_obls prg obls' 0 + let x = subst_deps_obl obls x in + let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in + assumption_message x.obl_name; + obls.(i) <- { x with obl_body = Some (mkConst kn) } + | Some _ -> ()) + obls; + ignore(update_obls prg obls 0) exception Found of int @@ -367,21 +431,17 @@ let array_find f arr = raise Not_found with Found i -> i -let rec next_obligation n = - let prg = get_prog n in +let next_obligation n = + let prg = get_prog_err n in let obls, rem = prg.prg_obligations in let i = array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls - in - if solve_obligation_by_tac prg obls i !default_tactic then ( - update_obls prg obls (pred rem); - next_obligation n - ) else solve_obligation prg i + in solve_obligation prg i open Pp let show_obligations n = - let prg = get_prog n in + let prg = get_prog_err n in let n = prg.prg_name in let obls, rem = prg.prg_obligations in msgnl (int rem ++ str " obligation(s) remaining: "); @@ -392,3 +452,4 @@ let show_obligations n = | Some _ -> ()) obls +let default_tactic () = !default_tactic diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 3981d4c6..f015b80b 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -1,8 +1,10 @@ open Util -type obligation_info = (Names.identifier * Term.types * Intset.t) array +type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array + (* ident, type, opaque or transparent, dependencies *) -val set_default_tactic : Proof_type.tactic -> unit +val set_default_tactic : Tacexpr.glob_tactic_expr -> unit +val default_tactic : unit -> Proof_type.tactic val add_definition : Names.identifier -> Term.constr -> Term.types -> obligation_info -> unit @@ -14,8 +16,20 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op val next_obligation : Names.identifier option -> unit -val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit +val solve_obligations : Names.identifier option -> Proof_type.tactic -> int +(* Number of remaining obligations to be solved for this program *) + +val solve_all_obligations : Proof_type.tactic -> unit + +val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic -> unit + +val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit val show_obligations : Names.identifier option -> unit val admit_obligations : Names.identifier option -> unit + +exception NoObligations of Names.identifier option + +val explain_no_obligations : Names.identifier option -> Pp.std_ppcmds + diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 4d1ac731..cce9a358 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping.ml 9563 2007-01-31 09:37:18Z msozeau $ *) +(* $Id: subtac_pretyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Global open Pp @@ -36,7 +36,6 @@ open Subtac_utils open Coqlib open Printer open Subtac_errors -open Context open Eterm module Pretyping = Subtac_pretyping_F.SubtacPretyping_F(Subtac_coercion.Coercion) @@ -89,18 +88,18 @@ let list_split_at index l = open Vernacexpr -let coqintern evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env -let coqinterp evd env : Topconstr.constr_expr -> Term.constr = Constrintern.interp_constr (evars_of evd) env +let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env +let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type (evars_of evd) env let env_with_binders env isevars l = let rec aux ((env, rels) as acc) = function Topconstr.LocalRawDef ((loc, name), def) :: tl -> - let rawdef = coqintern !isevars env def in + let rawdef = coqintern_constr !isevars env def in let coqdef, deftyp = interp env isevars rawdef empty_tycon in let reldecl = (name, Some coqdef, deftyp) in aux (push_rel reldecl env, reldecl :: rels) tl | Topconstr.LocalRawAssum (bl, typ) :: tl -> - let rawtyp = coqintern !isevars env typ in + let rawtyp = coqintern_type !isevars env typ in let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in let acc = List.fold_left (fun (env, rels) (loc, name) -> @@ -113,36 +112,37 @@ let env_with_binders env isevars l = in aux (env, []) l let subtac_process env isevars id l c tycon = - let env_binders, binders_rel = env_with_binders env isevars l in + let c = Command.abstract_constr_expr c l in +(* let env_binders, binders_rel = env_with_binders env isevars l in *) let tycon = match tycon with None -> empty_tycon | Some t -> - let t = coqintern !isevars env_binders t in - let coqt, ttyp = interp env_binders isevars t empty_tycon in + let t = Command.generalize_constr_expr t l in + let t = coqintern_type !isevars env t in + let coqt, ttyp = interp env isevars t empty_tycon in mk_tycon coqt in - let c = coqintern !isevars env_binders c in - let c = Subtac_utils.rewrite_cases env c in - let coqc, ctyp = interp env_binders isevars c tycon in -(* let _ = try trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++ *) -(* str "Coq type: " ++ my_print_constr env_binders ctyp) *) -(* with _ -> () *) + let c = coqintern_constr !isevars env c in + let coqc, ctyp = interp env isevars c tycon in +(* let _ = try trace (str "Interpreted term: " ++ my_print_constr env coqc ++ spc () ++ *) +(* str "Coq type: " ++ my_print_constr env ctyp) *) +(* with _ -> () *) (* in *) -(* let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) with _ -> () in *) +(* let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !isevars)) with _ -> () in *) - let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel - and fullctyp = it_mkProd_or_LetIn ctyp binders_rel - in - let fullcoqc = Evarutil.nf_evar (evars_of !isevars) fullcoqc in - let fullctyp = Evarutil.nf_evar (evars_of !isevars) fullctyp in - -(* let _ = try trace (str "After evar normalization: " ++ spc () ++ *) -(* str "Coq term: " ++ my_print_constr env fullcoqc ++ spc () *) -(* ++ str "Coq type: " ++ my_print_constr env fullctyp) *) -(* with _ -> () *) +(* let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel *) +(* and fullctyp = it_mkProd_or_LetIn ctyp binders_rel *) (* in *) - let evm = non_instanciated_map env isevars in + let fullcoqc = Evarutil.nf_evar (evars_of !isevars) coqc in + let fullctyp = Evarutil.nf_evar (evars_of !isevars) ctyp in +(* let evm = evars_of_term (evars_of !isevars) Evd.empty fullctyp in *) +(* let evm = evars_of_term (evars_of !isevars) evm fullcoqc in *) +(* let _ = try trace (str "After evar normalization remain: " ++ spc () ++ *) +(* Evd.pr_evar_map evm) *) +(* with _ -> () *) +(* in *) + let evm = non_instanciated_map env isevars (evars_of !isevars) in (* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *) evm, fullcoqc, fullctyp @@ -152,5 +152,5 @@ let subtac_proof env isevars id l c tycon = let nc = named_context env in let nc_len = named_context_length nc in let evm, coqc, coqt = subtac_process env isevars id l c tycon in - let evars, def = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in + let evars, def = Eterm.eterm_obligations id nc_len !isevars evm 0 coqc (Some coqt) in add_definition id def coqt evars diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 6244aef3..53eec0b6 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping_F.ml 9563 2007-01-31 09:37:18Z msozeau $ *) +(* $Id: subtac_pretyping_F.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Pp open Util @@ -93,7 +93,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* coerce to tycon if any *) let inh_conv_coerce_to_tycon loc env isevars j = function - | None -> j + | None -> j_nf_isevar !isevars j | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t let push_rels vars env = List.fold_right push_rel vars env @@ -364,21 +364,21 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct error_case_not_inductive_loc cloc env (evars_of !isevars) cj in let cstrs = get_constructors env indf in - if Array.length cstrs <> 1 then - user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor"); - let cs = cstrs.(0) in - if List.length nal <> cs.cs_nargs then - user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables"); - let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) - (List.rev nal) cs.cs_args in - let env_f = push_rels fsign env in - (* Make dependencies from arity signature impossible *) - let arsgn = - let arsgn,_ = get_arity env indf in - if not !allow_anonymous_refs then - List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn - else arsgn - in + if Array.length cstrs <> 1 then + user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor"); + let cs = cstrs.(0) in + if List.length nal <> cs.cs_nargs then + user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables"); + let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) + (List.rev nal) cs.cs_args in + let env_f = push_rels fsign env in + (* Make dependencies from arity signature impossible *) + let arsgn = + let arsgn,_ = get_arity env indf in + if not !allow_anonymous_refs then + List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn + else arsgn + in let psign = (na,None,build_dependent_inductive env indf)::arsgn in let nar = List.length arsgn in (match po with @@ -495,13 +495,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct ((fun vtyc env -> pretype vtyc env isevars lvar),isevars) tycon env (* loc *) (po,tml,eqns) - | RCast(loc,c,k,t) -> + | RCast(loc,c,k) -> let cj = match k with CastCoerce -> let cj = pretype empty_tycon env isevars lvar c in evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj - | CastConv k -> + | CastConv (k,t) -> let tj = pretype_type empty_valcon env isevars lvar t in let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in (* User Casts are for helping pretyping, experimentally not to be kept*) diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index 01dee3e9..28fe6352 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -32,6 +32,7 @@ let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub" let fix_measure_sub_ref = make_ref ["subtac";"FixSub"] "Fix_measure_sub" let lt_ref = make_ref ["Init";"Peano"] "lt" let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf" +let refl_ref = make_ref ["Init";"Logic"] "refl_equal" let make_ref s = Qualid (dummy_loc, qualid_of_string s) let sig_ref = make_ref "Init.Specif.sig" @@ -54,6 +55,10 @@ let eq_refl = lazy (init_constant ["Init"; "Logic"] "refl_equal") let eq_ind_ref = lazy (init_reference ["Init"; "Logic"] "eq") let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal") +let not_ref = lazy (init_constant ["Init"; "Logic"] "not") + +let and_typ = lazy (Coqlib.build_coq_and ()) + let eqdep_ind = lazy (init_constant [ "Logic";"Eqdep"] "eq_dep") let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec") let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep") @@ -61,8 +66,7 @@ let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro") let jmeq_ind = lazy (init_constant ["Logic";"JMeq"] "JMeq") let jmeq_rec = lazy (init_constant ["Logic";"JMeq"] "JMeq_rec") -let jmeq_ind_ref = lazy (init_reference ["Logic";"JMeq"] "JMeq") -let jmeq_refl_ref = lazy (init_reference ["Logic";"JMeq"] "JMeq_refl") +let jmeq_refl = lazy (init_constant ["Logic";"JMeq"] "JMeq_refl") let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex") let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro") @@ -126,6 +130,10 @@ let trace s = else () else () +let rec pp_list f = function + [] -> mt() + | x :: y -> f x ++ spc () ++ pp_list f y + let wf_relations = Hashtbl.create 10 let std_relations () = @@ -145,8 +153,8 @@ let app_opt c e = let print_args env args = Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "") -let make_existential loc env isevars c = - let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in +let make_existential loc ?(opaque = true) env isevars c = + let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in let (key, args) = destEvar evar in (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++ print_args env args ++ str " for type: "++ @@ -162,25 +170,33 @@ let make_existential_expr loc env c = let string_of_hole_kind = function | ImplicitArg _ -> "ImplicitArg" | BinderType _ -> "BinderType" - | QuestionMark -> "QuestionMark" + | QuestionMark _ -> "QuestionMark" | CasesType -> "CasesType" | InternalHole -> "InternalHole" | TomatchTypeParameter _ -> "TomatchTypeParameter" - -let non_instanciated_map env evd = - let evm = evars_of !evd in - List.fold_left - (fun evm (key, evi) -> - let (loc,k) = evar_source key !evd in - debug 2 (str "evar " ++ int key ++ str " has kind " ++ - str (string_of_hole_kind k)); - match k with - QuestionMark -> Evd.add evm key evi - | _ -> + +let evars_of_term evc init c = + let rec evrec acc c = + match kind_of_term c with + | Evar (n, _) when Evd.mem evc n -> Evd.add acc n (Evd.find evc n) + | Evar (n, _) -> assert(false) + | _ -> fold_constr evrec acc c + in + evrec init c + +let non_instanciated_map env evd evm = + List.fold_left + (fun evm (key, evi) -> + let (loc,k) = evar_source key !evd in + debug 2 (str "evar " ++ int key ++ str " has kind " ++ + str (string_of_hole_kind k)); + match k with + QuestionMark _ -> Evd.add evm key evi + | _ -> debug 2 (str " and is an implicit"); Pretype_errors.error_unsolvable_implicit loc env evm k) - Evd.empty (Evarutil.non_instantiated evm) - + Evd.empty (Evarutil.non_instantiated evm) + let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition @@ -247,11 +263,30 @@ let mk_ex_pi1 a b c = let mk_ex_pi2 a b c = mkApp (Lazy.force ex_pi2, [| a; b; c |]) - let mkSubset name typ prop = mkApp ((Lazy.force sig_).typ, [| typ; mkLambda (name, typ, prop) |]) +let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |]) +let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |]) +let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |]) +let mk_JMeq_refl typ x = mkApp (Lazy.force jmeq_refl, [| typ; x |]) + +let unsafe_fold_right f = function + hd :: tl -> List.fold_right f tl hd + | [] -> raise (Invalid_argument "unsafe_fold_right") + +let mk_conj l = + let conj_typ = Lazy.force and_typ in + unsafe_fold_right + (fun c conj -> + mkApp (conj_typ, [| c ; conj |])) + l + +let mk_not c = + let notc = Lazy.force not_ref in + mkApp (notc, [| c |]) + let and_tac l hook = let andc = Coqlib.build_coq_and () in let rec aux ((accid, goal, tac, extract) as acc) = function @@ -301,291 +336,7 @@ let destruct_ex ext ex = in aux ex ext open Rawterm - -let rec concatMap f l = - match l with - hd :: tl -> f hd @ concatMap f tl - | [] -> [] -let list_mapi f = - let rec aux i = function - hd :: tl -> f i hd :: aux (succ i) tl - | [] -> [] - in aux 0 - -(* -let make_discr (loc, po, tml, eqns) = - let mkHole = RHole (dummy_loc, InternalHole) in - - let rec vars_of_pat = function - RPatVar (loc, n) -> (match n with Anonymous -> [] | Name n -> [n]) - | RPatCstr (loc, csrt, pats, _) -> - concatMap vars_of_pat pats - in - let rec constr_of_pat l = function - RPatVar (loc, n) -> - (match n with - Anonymous -> - let n = next_name_away_from "x" l in - RVar n, (n :: l) - | Name n -> RVar n, l) - | RPatCstr (loc, csrt, pats, _) -> - let (args, vars) = - List.fold_left - (fun (args, vars) x -> - let c, vars = constr_of_pat vars x in - c :: args, vars) - ([], l) pats - in - RApp ((RRef (dummy_loc, ConstructRef cstr)), args), vars - in - let rec constr_of_pat l = function - RPatVar (loc, n) -> - (match n with - Anonymous -> - let n = next_name_away_from "x" l in - RVar n, (n :: l) - | Name n -> RVar n, l) - | RPatCstr (loc, csrt, pats, _) -> - let (args, vars) = - List.fold_left - (fun (args, vars) x -> - let c, vars = constr_of_pat vars x in - c :: args, vars) - ([], l) pats - in - RApp ((RRef (dummy_loc, ConstructRef cstr)), args), vars - in - let constrs_of_pats v l = - List.fold_left - (fun (v, acc) x -> - let x', v' = constr_of_pat v x in - (l', v' :: acc)) - (v, []) l - in - let rec pat_of_pat l = function - RPatVar (loc, n) -> - let n', l = match n with - Anonymous -> - let n = next_name_away_from "x" l in - n, n :: l - | Name n -> n, n :: l - in - RPatVar (loc, Name n'), l - | RPatCstr (loc, cstr, pats, (loc, alias)) -> - let args, vars, s = - List.fold_left (fun (args, vars) x -> - let pat', vars = pat_of_pat vars pat in - pat' :: args, vars) - ([], alias :: l) pats - in RPatCstr (loc, cstr, args, (loc, alias)), vars - in - let pats_of_pats l = - List.fold_left - (fun (v, acc) x -> - let x', v' = pat_of_pat v x in - (v', x' :: acc)) - ([], []) l - in - let eq_of_pat p used c = - let constr, vars' = constr_of_pat used p in - let eq = RApp (dummy_loc, RRef (dummy_loc, Lazy.force eqind_ref), [mkHole; constr; c]) in - vars', eq - in - let eqs_of_pats ps used cstrs = - List.fold_left2 - (fun (vars, eqs) pat c -> - let (vars', eq) = eq_of_pat pat c in - match eqs with - None -> Some eq - | Some eqs -> - Some (RApp (dummy_loc, RRef (dummy_loc, Lazy.force and_ref), [eq, eqs]))) - (used, None) ps cstrs - in - let quantify c l = - List.fold_left - (fun acc name -> RProd (dummy_loc, name, mkHole, acc)) - c l - in - let quantpats = - List.fold_left - (fun (acc, pats) ((loc, idl, cpl, c) as x) -> - let vars, cpl = pats_of_pats cpl in - let l', constrs = constrs_of_pats vars cpl in - let discrs = - List.map (fun (_, _, cpl', _) -> - let qvars, eqs = eqs_of_pats cpl' l' constrs in - let neg = RApp (dummy_loc, RRef (dummy_loc, Lazy.force not_ref), [out_some eqs]) in - let pat_ineq = quantify qvars neg in - - ) - pats in - - - - - - - - (x, pat_ineq)) - in - List.fold_left - (fun acc ((loc, idl, cpl, c0) pat) -> - - - let c' = - List.fold_left - (fun acc (n, t) -> - RLambda (dummy_loc, n, mkHole, acc)) - c eqs_types - in (loc, idl, cpl, c')) - eqns - i -*) -(* let rewrite_cases_aux (loc, po, tml, eqns) = *) -(* let tml = list_mapi (fun i (c, (n, opt)) -> c, *) -(* ((match n with *) -(* Name id -> (match c with *) -(* | RVar (_, id') when id = id' -> *) -(* Name (id_of_string (string_of_id id ^ "'")) *) -(* | _ -> n) *) -(* | Anonymous -> Name (id_of_string ("x" ^ string_of_int i))), *) -(* opt)) tml *) -(* in *) -(* let mkHole = RHole (dummy_loc, InternalHole) in *) -(* (\* let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)), *\) *) -(* (\* [mkHole; c; n]) *\) *) -(* (\* in *\) *) -(* let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqdep_ind_ref)), *) -(* [mkHole; c; mkHole; n]) *) -(* in *) -(* let eqs_types = *) -(* List.map *) -(* (fun (c, (n, _)) -> *) -(* let id = match n with Name id -> id | _ -> assert false in *) -(* let heqid = id_of_string ("Heq" ^ string_of_id id) in *) -(* Name heqid, mkeq c (RVar (dummy_loc, id))) *) -(* tml *) -(* in *) -(* let po = *) -(* List.fold_right *) -(* (fun (n,t) acc -> *) -(* RProd (dummy_loc, Anonymous, t, acc)) *) -(* eqs_types (match po with *) -(* Some e -> e *) -(* | None -> mkHole) *) -(* in *) -(* let eqns = *) -(* List.map (fun (loc, idl, cpl, c) -> *) -(* let c' = *) -(* List.fold_left *) -(* (fun acc (n, t) -> *) -(* RLambda (dummy_loc, n, mkHole, acc)) *) -(* c eqs_types *) -(* in (loc, idl, cpl, c')) *) -(* eqns *) -(* in *) -(* let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref), *) -(* [mkHole; c]) *) -(* in *) -(* (\*let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref), *) -(* [mkHole; c]) *) -(* in*\) *) -(* let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in *) -(* let case = RCases (loc,Some po,tml,eqns) in *) -(* let app = RApp (dummy_loc, case, refls) in *) -(* app *) - -(* let rec rewrite_cases c = *) -(* match c with *) -(* RCases _ -> let c' = map_rawconstr rewrite_cases c in *) -(* (match c' with *) -(* | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w) *) -(* | _ -> assert(false)) *) -(* | _ -> map_rawconstr rewrite_cases c *) - -(* let rewrite_cases env c = *) -(* let c' = rewrite_cases c in *) -(* let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in *) -(* c' *) - -let list_mapi f = - let rec aux i = function - hd :: tl -> f i hd :: aux (succ i) tl - | [] -> [] - in aux 0 - -open Rawterm - -let rewrite_cases_aux (loc, po, tml, eqns) = - let tml' = list_mapi (fun i (c, (n, opt)) -> c, - ((match n with - Name id -> (match c with - | RVar (_, id') when id = id' -> - id, (id_of_string (string_of_id id ^ "Heq_id")) - | RVar (_, id') -> - id', id - | _ -> id_of_string (string_of_id id ^ "Heq_id"), id) - | Anonymous -> - let str = "Heq_id" ^ string_of_int i in - id_of_string str, id_of_string (str ^ "'")), - opt)) tml - in - let mkHole = RHole (dummy_loc, InternalHole) in - let mkCoerceCast c = RCast (dummy_loc, c, CastCoerce, mkHole) in - let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eq_ind_ref)), - [mkHole; c; n]) - in - let eqs_types = - List.map - (fun (c, ((id, id'), _)) -> - let heqid = id_of_string ("Heq" ^ string_of_id id) in - Name heqid, mkeq (RVar (dummy_loc, id')) c) - tml' - in - let po = - List.fold_right - (fun (n,t) acc -> - RProd (dummy_loc, Anonymous, t, acc)) - eqs_types (match po with - Some e -> e - | None -> mkHole) - in - let eqns = - List.map (fun (loc, idl, cpl, c) -> - let c' = - List.fold_left - (fun acc (n, t) -> - RLambda (dummy_loc, n, mkHole, acc)) - c eqs_types - in (loc, idl, cpl, c')) - eqns - in - let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref), - [mkHole; c]) - in - let refls = List.map (fun (c, ((id, _), _)) -> mk_refl_equal (mkCoerceCast c)) tml' in - let tml'' = List.map (fun (c, ((id, id'), opt)) -> c, (Name id', opt)) tml' in - let case = RCases (loc,Some po,tml'',eqns) in - let app = RApp (dummy_loc, case, refls) in -(* let letapp = List.fold_left (fun acc (c, ((id, id'), opt)) -> RLetIn (dummy_loc, Name id, c, acc)) *) -(* app tml' *) -(* in *) - app - -let rec rewrite_cases c = - match c with - RCases _ -> let c' = map_rawconstr rewrite_cases c in - (match c' with - | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w) - | _ -> assert(false)) - | _ -> map_rawconstr rewrite_cases c - -let rewrite_cases env c = c -(* let c' = rewrite_cases c in *) -(* let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in *) -(* c' *) - let id_of_name = function Name n -> n | Anonymous -> raise (Invalid_argument "id_of_name") @@ -601,23 +352,6 @@ let recursive_message v = spc () ++ str "are recursively defined") (* Solve an obligation using tactics, return the corresponding proof term *) -(* -let solve_by_tac ev t = - debug 1 (str "Solving goal using tactics: " ++ Evd.pr_evar_info ev); - let goal = Proof_trees.mk_goal ev.evar_hyps ev.evar_concl None in - debug 1 (str "Goal created"); - let ts = Tacmach.mk_pftreestate goal in - debug 1 (str "Got pftreestate"); - let solved_state = Tacmach.solve_pftreestate t ts in - debug 1 (str "Solved goal"); - let _, l = Tacmach.extract_open_pftreestate solved_state in - List.iter (fun (_, x) -> debug 1 (str "left hole of type " ++ my_print_constr (Global.env()) x)) l; - let c = Tacmach.extract_pftreestate solved_state in - debug 1 (str "Extracted term"); - debug 1 (str "Term constructed in solve by tac: " ++ my_print_constr (Global.env ()) c); - c - *) - let solve_by_tac evi t = debug 2 (str "Solving goal using tactics: " ++ Evd.pr_evar_info evi); let id = id_of_string "H" in @@ -705,3 +439,12 @@ let pr_evar_defs evd = if meta_list evd = [] then mt() else str"METAS:"++brk(0,1)++pr_meta_map evd in v 0 (pp_evm ++ pp_met) + +let subtac_utils_path = + make_dirpath (List.map id_of_string ["Utils";contrib_name;"Coq"]) +let utils_tac s = + lazy(make_kn (MPfile subtac_utils_path) (make_dirpath []) (mk_label s)) + +let utils_call tac args = + TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args)) + diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 482640f9..5a5dd427 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -27,6 +27,7 @@ val fix_sub_ref : global_reference lazy_t val fix_measure_sub_ref : global_reference lazy_t val lt_ref : global_reference lazy_t val lt_wf_ref : global_reference lazy_t +val refl_ref : global_reference lazy_t val sig_ref : reference val proj1_sig_ref : reference val proj2_sig_ref : reference @@ -37,13 +38,16 @@ val eq_ind : constr lazy_t val eq_rec : constr lazy_t val eq_rect : constr lazy_t val eq_refl : constr lazy_t -val eq_ind_ref : global_reference lazy_t -val refl_equal_ref : global_reference lazy_t + +val not_ref : constr lazy_t +val and_typ : constr lazy_t val eqdep_ind : constr lazy_t val eqdep_rec : constr lazy_t -val eqdep_ind_ref : global_reference lazy_t -val eqdep_intro_ref : global_reference lazy_t + +val jmeq_ind : constr lazy_t +val jmeq_rec : constr lazy_t +val jmeq_refl : constr lazy_t val boolind : constr lazy_t val sumboolind : constr lazy_t @@ -79,10 +83,11 @@ val wf_relations : (constr, constr lazy_t) Hashtbl.t type binders = local_binder list val app_opt : ('a -> 'a) option -> 'a -> 'a val print_args : env -> constr array -> std_ppcmds -val make_existential : loc -> env -> evar_defs ref -> types -> constr +val make_existential : loc -> ?opaque:bool -> env -> evar_defs ref -> types -> constr val make_existential_expr : loc -> 'a -> 'b -> constr_expr val string_of_hole_kind : hole_kind -> string -val non_instanciated_map : env -> evar_defs ref -> evar_map +val evars_of_term : evar_map -> evar_map -> constr -> evar_map +val non_instanciated_map : env -> evar_defs ref -> evar_map -> evar_map val global_kind : logical_kind val goal_kind : locality_flag * goal_object_kind val global_proof_kind : logical_kind @@ -95,6 +100,12 @@ val mkProj1 : constr -> constr -> constr -> constr val mkProj1 : constr -> constr -> constr -> constr val mk_ex_pi1 : constr -> constr -> constr -> constr val mk_ex_pi1 : constr -> constr -> constr -> constr +val mk_eq : types -> constr -> constr -> types +val mk_eq_refl : types -> constr -> constr +val mk_JMeq : types -> constr-> types -> constr -> types +val mk_JMeq_refl : types -> constr -> constr +val mk_conj : types list -> types +val mk_not : types -> types val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types val and_tac : (identifier * 'a * constr * Proof_type.tactic) list -> @@ -102,7 +113,6 @@ val and_tac : (identifier * 'a * constr * Proof_type.tactic) list -> val destruct_ex : constr -> constr -> constr list -val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr val id_of_name : name -> identifier val definition_message : identifier -> unit @@ -114,3 +124,7 @@ val string_of_list : string -> ('a -> string) -> 'a list -> string val string_of_intset : Intset.t -> string val pr_evar_defs : evar_defs -> Pp.std_ppcmds + +val utils_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr + +val pp_list : ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds diff --git a/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v index 7ab720f6..97cef9a5 100644 --- a/contrib/subtac/test/ListDep.v +++ b/contrib/subtac/test/ListDep.v @@ -1,3 +1,4 @@ +(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) Require Import List. Require Import Coq.subtac.Utils. @@ -21,63 +22,25 @@ Section Map_DependentRecursor. Variable l : list U. Variable f : { x : U | In x l } -> V. + Obligations Tactic := unfold sub_list in * ; + subtac_simpl ; intuition. + Program Fixpoint map_rec ( l' : list U | sub_list l' l ) - { measure l' length } : { r : list V | length r = length l' } := + { measure length l' } : { r : list V | length r = length l' } := match l' with nil => nil | cons x tl => let tl' := map_rec tl in f x :: tl' end. - Obligation 1. - intros. - destruct tl' ; simpl ; simpl in e. - subst x0 tl0. - rewrite <- Heql'. - rewrite e. - auto. - Qed. - - Obligation 2. - simpl. - intros. - destruct l'. - simpl in Heql'. - destruct x0 ; simpl ; try discriminate. - inversion Heql'. - inversion s. - apply H. - auto with datatypes. - Qed. - - - Obligation 3 of map_rec. - simpl. - intros. - rewrite <- Heql'. + Next Obligation. + destruct_call map_rec. + simpl in *. + subst l'. simpl ; auto with arith. - Qed. - - Obligation 4. - simpl. - intros. - destruct l'. - simpl in Heql'. - destruct x0 ; simpl ; try discriminate. - inversion Heql'. - subst x tl. - apply sub_list_tl with u ; auto. - Qed. - - Obligation 5. - intros. - rewrite <- Heql' ; auto. - Qed. - - Program Definition map : list V := map_rec l. - Obligation 1. - split ; auto. - Qed. + Qed. + + Program Definition map : list V := map_rec l. End Map_DependentRecursor. diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v index b8d13fe6..3ceea173 100644 --- a/contrib/subtac/test/ListsTest.v +++ b/contrib/subtac/test/ListsTest.v @@ -70,7 +70,22 @@ Section Nth. Next Obligation. Proof. - inversion l0. + intros. + inversion H. Defined. + + Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := + match l, n with + | hd :: _, 0 => hd + | _ :: tl, S n' => nth' tl n' + | nil, _ => ! + end. + + Next Obligation. + Proof. + intros. + inversion H. + Defined. + End Nth. diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index ff07c3c4..8a5967a2 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -22,8 +22,13 @@ let get_module_path_of_section_path path = List.filter (function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules with - [modul] -> modul - | _ -> raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther + [] -> + Pp.warning ("Modules not supported: reference to "^ + Libnames.string_of_path path^" will be wrong"); + dirpath + | [modul] -> modul + | _ -> + raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther ;; (*CSC: Problem: here we are using the wrong (???) hypothesis that there do *) @@ -652,11 +657,13 @@ print_endline "PASSATO" ; flush stdout ; A.ALambdas (new_passed_lambdas, t') ) | T.LetIn (n,s,t,d) -> - let n' = + let id = match n with - N.Anonymous -> N.Anonymous - | _ -> - N.Name (Nameops.next_name_away n (Termops.ids_of_context env)) + N.Anonymous -> N.id_of_string "_X" + | N.Name id -> id + in + let n' = + N.Name (Nameops.next_ident_away id (Termops.ids_of_context env)) in Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; let sourcesort = diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index c7d3b4ff..cce78891 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -26,31 +26,13 @@ let cprop = (N.mk_label "CProp") ;; -let whd_betadeltaiotacprop env evar_map ty = +let whd_betadeltaiotacprop env _evar_map ty = let module R = Rawterm in - let red_exp = - R.Hnf (*** Instead CProp is made Opaque ***) -(* - R.Cbv - {R.rBeta = true ; R.rIota = true ; R.rDelta = true; R.rZeta=true ; - R.rConst = [Names.EvalConstRef cprop] - } -*) - in -Conv_oracle.set_opaque_const cprop; -prerr_endline "###whd_betadeltaiotacprop:" ; -let xxx = -(*Pp.msgerr (Printer.pr_lconstr_env env ty);*) -prerr_endline ""; - (fst (Redexpr.reduction_of_red_expr red_exp)) env evar_map ty -in -prerr_endline "###FINE" ; -(* -Pp.msgerr (Printer.pr_lconstr_env env xxx); -*) -prerr_endline ""; -Conv_oracle.set_transparent_const cprop; -xxx + let module C = Closure in + let module CR = C.RedFlags in + (*** CProp is made Opaque ***) + let flags = CR.red_sub C.betadeltaiota (CR.fCONST cprop) in + C.whd_val (C.create_clos_infos flags env) (C.inject ty) ;; diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index f286d2c8..01271323 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -461,11 +461,42 @@ let kind_of_constant kn = match Declare.constant_kind (Nametab.sp_of_global(Libnames.ConstRef kn)) with | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration" | DK.IsAssumption DK.Logical -> "AXIOM","Axiom" - | DK.IsAssumption DK.Conjectural -> "AXIOM","Conjecture" + | DK.IsAssumption DK.Conjectural -> + Pp.warning "Conjecture not supported in dtd (used Declaration instead)"; + "AXIOM","Declaration" | DK.IsDefinition DK.Definition -> "DEFINITION","Definition" - | DK.IsDefinition DK.Example -> "DEFINITION","Example" - | DK.IsDefinition _ -> Util.anomaly "Unsupported constant kind" - | DK.IsProof thm -> "THEOREM",DK.string_of_theorem_kind thm + | DK.IsDefinition DK.Example -> + Pp.warning "Example not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.Coercion -> + Pp.warning "Coercion not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.SubClass -> + Pp.warning "SubClass not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.CanonicalStructure -> + Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.Fixpoint -> + Pp.warning "Fixpoint not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.CoFixpoint -> + Pp.warning "CoFixpoint not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.Scheme -> + Pp.warning "Scheme not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.StructureComponent -> + Pp.warning "StructureComponent not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsDefinition DK.IdentityCoercion -> + Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> + "THEOREM",DK.string_of_theorem_kind thm + | DK.IsProof _ -> + Pp.warning "Unsupported theorem kind (used Theorem instead)"; + "THEOREM",DK.string_of_theorem_kind DK.Theorem ;; let kind_of_global r = |