diff options
Diffstat (limited to 'plugins/decl_mode')
-rw-r--r-- | plugins/decl_mode/decl_expr.mli | 103 | ||||
-rw-r--r-- | plugins/decl_mode/decl_interp.ml | 471 | ||||
-rw-r--r-- | plugins/decl_mode/decl_interp.mli | 16 | ||||
-rw-r--r-- | plugins/decl_mode/decl_mode.ml | 123 | ||||
-rw-r--r-- | plugins/decl_mode/decl_mode.mli | 78 | ||||
-rw-r--r-- | plugins/decl_mode/decl_mode_plugin.mllib | 6 | ||||
-rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 1504 | ||||
-rw-r--r-- | plugins/decl_mode/decl_proof_instr.mli | 109 | ||||
-rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 409 | ||||
-rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 188 | ||||
-rw-r--r-- | plugins/decl_mode/ppdecl_proof.mli | 2 |
11 files changed, 3009 insertions, 0 deletions
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli new file mode 100644 index 00000000..69b0a0e3 --- /dev/null +++ b/plugins/decl_mode/decl_expr.mli @@ -0,0 +1,103 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Util +open Tacexpr + +type 'it statement = + {st_label:name; + st_it:'it} + +type thesis_kind = + Plain + | For of identifier + +type 'this or_thesis = + This of 'this + | Thesis of thesis_kind + +type side = Lhs | Rhs + +type elim_type = + ET_Case_analysis + | ET_Induction + +type block_type = + B_proof + | B_claim + | B_focus + | B_elim of elim_type + +type ('it,'constr,'tac) cut = + {cut_stat: 'it; + cut_by: 'constr list option; + cut_using: 'tac option} + +type ('var,'constr) hyp = + Hvar of 'var + | Hprop of 'constr statement + +type ('constr,'tac) casee = + Real of 'constr + | Virtual of ('constr statement,'constr,'tac) cut + +type ('hyp,'constr,'pat,'tac) bare_proof_instr = + | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr + | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr + | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr + | Pcut of ('constr or_thesis statement,'constr,'tac) cut + | Prew of side * ('constr statement,'constr,'tac) cut + | Psuffices of ((('hyp,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut + | Passume of ('hyp,'constr) hyp list + | Plet of ('hyp,'constr) hyp list + | Pgiven of ('hyp,'constr) hyp list + | Pconsider of 'constr*('hyp,'constr) hyp list + | Pclaim of 'constr statement + | Pfocus of 'constr statement + | Pdefine of identifier * 'hyp list * 'constr + | Pcast of identifier or_thesis * 'constr + | Psuppose of ('hyp,'constr) hyp list + | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list) + | Ptake of 'constr list + | Pper of elim_type * ('constr,'tac) casee + | Pend of block_type + | Pescape + +type emphasis = int + +type ('hyp,'constr,'pat,'tac) gen_proof_instr= + {emph: emphasis; + instr: ('hyp,'constr,'pat,'tac) bare_proof_instr } + + +type raw_proof_instr = + ((identifier*(Topconstr.constr_expr option)) located, + Topconstr.constr_expr, + Topconstr.cases_pattern_expr, + raw_tactic_expr) gen_proof_instr + +type glob_proof_instr = + ((identifier*(Genarg.glob_constr_and_expr option)) located, + Genarg.glob_constr_and_expr, + Topconstr.cases_pattern_expr, + Tacexpr.glob_tactic_expr) gen_proof_instr + +type proof_pattern = + {pat_vars: Term.types statement list; + pat_aliases: (Term.constr*Term.types) statement list; + pat_constr: Term.constr; + pat_typ: Term.types; + pat_pat: Glob_term.cases_pattern; + pat_expr: Topconstr.cases_pattern_expr} + +type proof_instr = + (Term.constr statement, + Term.constr, + proof_pattern, + Tacexpr.glob_tactic_expr) gen_proof_instr diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml new file mode 100644 index 00000000..7637fed2 --- /dev/null +++ b/plugins/decl_mode/decl_interp.ml @@ -0,0 +1,471 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Names +open Topconstr +open Tacinterp +open Tacmach +open Decl_expr +open Decl_mode +open Pretyping.Default +open Glob_term +open Term +open Pp +open Compat + +(* INTERN *) + +let glob_app (loc,hd,args) = if args =[] then hd else GApp(loc,hd,args) + +let intern_justification_items globs = + Option.map (List.map (intern_constr globs)) + +let intern_justification_method globs = + Option.map (intern_pure_tactic globs) + +let intern_statement intern_it globs st = + {st_label=st.st_label; + st_it=intern_it globs st.st_it} + +let intern_no_bind intern_it globs x = + globs,intern_it globs x + +let intern_constr_or_thesis globs = function + Thesis n -> Thesis n + | This c -> This (intern_constr globs c) + +let add_var id globs= + let l1,l2=globs.ltacvars in + {globs with ltacvars= (id::l1),(id::l2)} + +let add_name nam globs= + match nam with + Anonymous -> globs + | Name id -> add_var id globs + +let intern_hyp iconstr globs = function + Hvar (loc,(id,topt)) -> add_var id globs, + Hvar (loc,(id,Option.map (intern_constr globs) topt)) + | Hprop st -> add_name st.st_label globs, + Hprop (intern_statement iconstr globs st) + +let intern_hyps iconstr globs hyps = + snd (list_fold_map (intern_hyp iconstr) globs hyps) + +let intern_cut intern_it globs cut= + let nglobs,nstat=intern_it globs cut.cut_stat in + {cut_stat=nstat; + cut_by=intern_justification_items nglobs cut.cut_by; + cut_using=intern_justification_method nglobs cut.cut_using} + +let intern_casee globs = function + Real c -> Real (intern_constr globs c) + | Virtual cut -> Virtual + (intern_cut (intern_no_bind (intern_statement intern_constr)) globs cut) + +let intern_hyp_list args globs = + let intern_one globs (loc,(id,opttyp)) = + (add_var id globs), + (loc,(id,Option.map (intern_constr globs) opttyp)) in + list_fold_map intern_one globs args + +let intern_suffices_clause globs (hyps,c) = + let nglobs,nhyps = list_fold_map (intern_hyp intern_constr) globs hyps in + nglobs,(nhyps,intern_constr_or_thesis nglobs c) + +let intern_fundecl args body globs= + let nglobs,nargs = intern_hyp_list args globs in + nargs,intern_constr nglobs body + +let rec add_vars_of_simple_pattern globs = function + CPatAlias (loc,p,id) -> + add_vars_of_simple_pattern (add_var id globs) p +(* Loc.raise loc + (UserError ("simple_pattern",str "\"as\" is not allowed here"))*) + | CPatOr (loc, _)-> + Loc.raise loc + (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) + | CPatDelimiters (_,_,p) -> + add_vars_of_simple_pattern globs p + | CPatCstr (_,_,pl) | CPatCstrExpl (_,_,pl) -> + List.fold_left add_vars_of_simple_pattern globs pl + | CPatNotation(_,_,(pl,pll)) -> + List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pll)) + | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs + | _ -> globs + +let rec intern_bare_proof_instr globs = function + Pthus i -> Pthus (intern_bare_proof_instr globs i) + | Pthen i -> Pthen (intern_bare_proof_instr globs i) + | Phence i -> Phence (intern_bare_proof_instr globs i) + | Pcut c -> Pcut + (intern_cut + (intern_no_bind (intern_statement intern_constr_or_thesis)) globs c) + | Psuffices c -> + Psuffices (intern_cut intern_suffices_clause globs c) + | Prew (s,c) -> Prew + (s,intern_cut + (intern_no_bind (intern_statement intern_constr)) globs c) + | Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps) + | Pcase (params,pat,hyps) -> + let nglobs,nparams = intern_hyp_list params globs in + let nnglobs= add_vars_of_simple_pattern nglobs pat in + let nhyps = intern_hyps intern_constr_or_thesis nnglobs hyps in + Pcase (nparams,pat,nhyps) + | Ptake witl -> Ptake (List.map (intern_constr globs) witl) + | Pconsider (c,hyps) -> Pconsider (intern_constr globs c, + intern_hyps intern_constr globs hyps) + | Pper (et,c) -> Pper (et,intern_casee globs c) + | Pend bt -> Pend bt + | Pescape -> Pescape + | Passume hyps -> Passume (intern_hyps intern_constr globs hyps) + | Pgiven hyps -> Pgiven (intern_hyps intern_constr globs hyps) + | Plet hyps -> Plet (intern_hyps intern_constr globs hyps) + | Pclaim st -> Pclaim (intern_statement intern_constr globs st) + | Pfocus st -> Pfocus (intern_statement intern_constr globs st) + | Pdefine (id,args,body) -> + let nargs,nbody = intern_fundecl args body globs in + Pdefine (id,nargs,nbody) + | Pcast (id,typ) -> + Pcast (id,intern_constr globs typ) + +let rec intern_proof_instr globs instr= + {emph = instr.emph; + instr = intern_bare_proof_instr globs instr.instr} + +(* INTERP *) + +let interp_justification_items sigma env = + Option.map (List.map (fun c ->understand sigma env (fst c))) + +let interp_constr check_sort sigma env c = + if check_sort then + understand_type sigma env (fst c) + else + understand sigma env (fst c) + +let special_whd env = + let infos=Closure.create_clos_infos Closure.betadeltaiota env in + (fun t -> Closure.whd_val infos (Closure.inject t)) + +let _eq = Libnames.constr_of_global (Coqlib.glob_eq) + +let decompose_eq env id = + let typ = Environ.named_type id env in + let whd = special_whd env typ in + match kind_of_term whd with + App (f,args)-> + if eq_constr f _eq && (Array.length args)=3 + then args.(0) + else error "Previous step is not an equality." + | _ -> error "Previous step is not an equality." + +let get_eq_typ info env = + let typ = decompose_eq env (get_last env) in + typ + +let interp_constr_in_type typ sigma env c = + understand sigma env (fst c) ~expected_type:typ + +let interp_statement interp_it sigma env st = + {st_label=st.st_label; + st_it=interp_it sigma env st.st_it} + +let interp_constr_or_thesis check_sort sigma env = function + Thesis n -> Thesis n + | This c -> This (interp_constr check_sort sigma env c) + +let abstract_one_hyp inject h glob = + match h with + Hvar (loc,(id,None)) -> + GProd (dummy_loc,Name id, Explicit, GHole (loc,Evd.BinderType (Name id)), glob) + | Hvar (loc,(id,Some typ)) -> + GProd (dummy_loc,Name id, Explicit, fst typ, glob) + | Hprop st -> + GProd (dummy_loc,st.st_label, Explicit, inject st.st_it, glob) + +let glob_constr_of_hyps inject hyps head = + List.fold_right (abstract_one_hyp inject) hyps head + +let glob_prop = GSort (dummy_loc,GProp Null) + +let rec match_hyps blend names constr = function + [] -> [],substl names constr + | hyp::q -> + let (name,typ,body)=destProd constr in + let st= {st_label=name;st_it=substl names typ} in + let qnames= + match name with + Anonymous -> mkMeta 0 :: names + | Name id -> mkVar id :: names in + let qhyp = match hyp with + Hprop st' -> Hprop (blend st st') + | Hvar _ -> Hvar st in + let rhyps,head = match_hyps blend qnames body q in + qhyp::rhyps,head + +let interp_hyps_gen inject blend sigma env hyps head = + let constr=understand sigma env (glob_constr_of_hyps inject hyps head) in + match_hyps blend [] constr hyps + +let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps glob_prop) + +let dummy_prefix= id_of_string "__" + +let rec deanonymize ids = + function + PatVar (loc,Anonymous) -> + let (found,known) = !ids in + let new_id=Namegen.next_ident_away dummy_prefix known in + let _= ids:= (loc,new_id) :: found , new_id :: known in + PatVar (loc,Name new_id) + | PatVar (loc,Name id) as pat -> + let (found,known) = !ids in + let _= ids:= (loc,id) :: found , known in + pat + | PatCstr(loc,cstr,lpat,nam) -> + PatCstr(loc,cstr,List.map (deanonymize ids) lpat,nam) + +let rec glob_of_pat = + function + PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable" + | PatVar (loc,Name id) -> + GVar (loc,id) + | PatCstr(loc,((ind,_) as cstr),lpat,_) -> + let mind= fst (Global.lookup_inductive ind) in + let rec add_params n q = + if n<=0 then q else + add_params (pred n) (GHole(dummy_loc, + Evd.TomatchTypeParameter(ind,n))::q) in + let args = List.map glob_of_pat lpat in + glob_app(loc,GRef(dummy_loc,Libnames.ConstructRef cstr), + add_params mind.Declarations.mind_nparams args) + +let prod_one_hyp = function + (loc,(id,None)) -> + (fun glob -> + GProd (dummy_loc,Name id, Explicit, + GHole (loc,Evd.BinderType (Name id)), glob)) + | (loc,(id,Some typ)) -> + (fun glob -> + GProd (dummy_loc,Name id, Explicit, fst typ, glob)) + +let prod_one_id (loc,id) glob = + GProd (dummy_loc,Name id, Explicit, + GHole (loc,Evd.BinderType (Name id)), glob) + +let let_in_one_alias (id,pat) glob = + GLetIn (dummy_loc,Name id, glob_of_pat pat, glob) + +let rec bind_primary_aliases map pat = + match pat with + PatVar (_,_) -> map + | PatCstr(loc,_,lpat,nam) -> + let map1 = + match nam with + Anonymous -> map + | Name id -> (id,pat)::map + in + List.fold_left bind_primary_aliases map1 lpat + +let bind_secondary_aliases map subst = + List.fold_left (fun map (ids,idp) -> (ids,List.assoc idp map)::map) map subst + +let bind_aliases patvars subst patt = + let map = bind_primary_aliases [] patt in + let map1 = bind_secondary_aliases map subst in + List.rev map1 + +let interp_pattern env pat_expr = + let patvars,pats = Constrintern.intern_pattern env pat_expr in + match pats with + [] -> anomaly "empty pattern list" + | [subst,patt] -> + (patvars,bind_aliases patvars subst patt,patt) + | _ -> anomaly "undetected disjunctive pattern" + +let rec match_args dest names constr = function + [] -> [],names,substl names constr + | _::q -> + let (name,typ,body)=dest constr in + let st={st_label=name;st_it=substl names typ} in + let qnames= + match name with + Anonymous -> assert false + | Name id -> mkVar id :: names in + let args,bnames,body = match_args dest qnames body q in + st::args,bnames,body + +let rec match_aliases names constr = function + [] -> [],names,substl names constr + | _::q -> + let (name,c,typ,body)=destLetIn constr in + let st={st_label=name;st_it=(substl names c,substl names typ)} in + let qnames= + match name with + Anonymous -> assert false + | Name id -> mkVar id :: names in + let args,bnames,body = match_aliases qnames body q in + st::args,bnames,body + +let detype_ground c = Detyping.detype false [] [] c + +let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = + let et,pinfo = + match info.pm_stack with + Per(et,pi,_,_)::_ -> et,pi + | _ -> error "No proof per cases/induction/inversion in progress." in + let mib,oib=Global.lookup_inductive pinfo.per_ind in + let num_params = pinfo.per_nparams in + let _ = + let expected = mib.Declarations.mind_nparams - num_params in + if List.length params <> expected then + errorlabstrm "suppose it is" + (str "Wrong number of extra arguments: " ++ + (if expected = 0 then str "none" else int expected) ++ spc () ++ + str "expected.") in + let app_ind = + let rind = GRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in + let rparams = List.map detype_ground pinfo.per_params in + let rparams_rec = + List.map + (fun (loc,(id,_)) -> + GVar (loc,id)) params in + let dum_args= + list_tabulate (fun _ -> GHole (dummy_loc,Evd.QuestionMark (Evd.Define false))) + oib.Declarations.mind_nrealargs in + glob_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in + let pat_vars,aliases,patt = interp_pattern env pat in + let inject = function + Thesis (Plain) -> Glob_term.GSort(dummy_loc,GProp Null) + | Thesis (For rec_occ) -> + if not (List.mem rec_occ pat_vars) then + errorlabstrm "suppose it is" + (str "Variable " ++ Nameops.pr_id rec_occ ++ + str " does not occur in pattern."); + Glob_term.GSort(dummy_loc,GProp Null) + | This (c,_) -> c in + let term1 = glob_constr_of_hyps inject hyps glob_prop in + let loc_ids,npatt = + let rids=ref ([],pat_vars) in + let npatt= deanonymize rids patt in + List.rev (fst !rids),npatt in + let term2 = + GLetIn(dummy_loc,Anonymous, + GCast(dummy_loc,glob_of_pat npatt, + CastConv (DEFAULTcast,app_ind)),term1) in + let term3=List.fold_right let_in_one_alias aliases term2 in + let term4=List.fold_right prod_one_id loc_ids term3 in + let term5=List.fold_right prod_one_hyp params term4 in + let constr = understand sigma env term5 in + let tparams,nam4,rest4 = match_args destProd [] constr params in + let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in + let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in + let (_,pat_pat,pat_typ,rest1) = destLetIn rest2 in + let blend st st' = + match st'.st_it with + Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label} + | This _ -> {st_it = This st.st_it;st_label=st.st_label} in + let thyps = fst (match_hyps blend nam2 (Termops.pop rest1) hyps) in + tparams,{pat_vars=tpatvars; + pat_aliases=taliases; + pat_constr=pat_pat; + pat_typ=pat_typ; + pat_pat=patt; + pat_expr=pat},thyps + +let interp_cut interp_it sigma env cut= + let nenv,nstat = interp_it sigma env cut.cut_stat in + {cut with + cut_stat=nstat; + cut_by=interp_justification_items sigma nenv cut.cut_by} + +let interp_no_bind interp_it sigma env x = + env,interp_it sigma env x + +let interp_suffices_clause sigma env (hyps,cot)= + let (locvars,_) as res = + match cot with + This (c,_) -> + let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in + nhyps,This nc + | Thesis Plain as th -> interp_hyps sigma env hyps,th + | Thesis (For n) -> error "\"thesis for\" is not applicable here." in + let push_one hyp env0 = + match hyp with + (Hprop st | Hvar st) -> + match st.st_label with + Name id -> Environ.push_named (id,None,st.st_it) env0 + | _ -> env in + let nenv = List.fold_right push_one locvars env in + nenv,res + +let interp_casee sigma env = function + Real c -> Real (understand sigma env (fst c)) + | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) sigma env cut) + +let abstract_one_arg = function + (loc,(id,None)) -> + (fun glob -> + GLambda (dummy_loc,Name id, Explicit, + GHole (loc,Evd.BinderType (Name id)), glob)) + | (loc,(id,Some typ)) -> + (fun glob -> + GLambda (dummy_loc,Name id, Explicit, fst typ, glob)) + +let glob_constr_of_fun args body = + List.fold_right abstract_one_arg args (fst body) + +let interp_fun sigma env args body = + let constr=understand sigma env (glob_constr_of_fun args body) in + match_args destLambda [] constr args + +let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = function + Pthus i -> Pthus (interp_bare_proof_instr info sigma env i) + | Pthen i -> Pthen (interp_bare_proof_instr info sigma env i) + | Phence i -> Phence (interp_bare_proof_instr info sigma env i) + | Pcut c -> Pcut (interp_cut + (interp_no_bind (interp_statement + (interp_constr_or_thesis true))) + sigma env c) + | Psuffices c -> + Psuffices (interp_cut interp_suffices_clause sigma env c) + | Prew (s,c) -> Prew (s,interp_cut + (interp_no_bind (interp_statement + (interp_constr_in_type (get_eq_typ info env)))) + sigma env c) + + | Psuppose hyps -> Psuppose (interp_hyps sigma env hyps) + | Pcase (params,pat,hyps) -> + let tparams,tpat,thyps = interp_cases info sigma env params pat hyps in + Pcase (tparams,tpat,thyps) + | Ptake witl -> + Ptake (List.map (fun c -> understand sigma env (fst c)) witl) + | Pconsider (c,hyps) -> Pconsider (interp_constr false sigma env c, + interp_hyps sigma env hyps) + | Pper (et,c) -> Pper (et,interp_casee sigma env c) + | Pend bt -> Pend bt + | Pescape -> Pescape + | Passume hyps -> Passume (interp_hyps sigma env hyps) + | Pgiven hyps -> Pgiven (interp_hyps sigma env hyps) + | Plet hyps -> Plet (interp_hyps sigma env hyps) + | Pclaim st -> Pclaim (interp_statement (interp_constr true) sigma env st) + | Pfocus st -> Pfocus (interp_statement (interp_constr true) sigma env st) + | Pdefine (id,args,body) -> + let nargs,_,nbody = interp_fun sigma env args body in + Pdefine (id,nargs,nbody) + | Pcast (id,typ) -> + Pcast(id,interp_constr true sigma env typ) + +let rec interp_proof_instr info sigma env instr= + {emph = instr.emph; + instr = interp_bare_proof_instr info sigma env instr.instr} + + + diff --git a/plugins/decl_mode/decl_interp.mli b/plugins/decl_mode/decl_interp.mli new file mode 100644 index 00000000..bd6ed064 --- /dev/null +++ b/plugins/decl_mode/decl_interp.mli @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Tacinterp +open Decl_expr +open Mod_subst + + +val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr +val interp_proof_instr : Decl_mode.pm_info -> + Evd.evar_map -> Environ.env -> glob_proof_instr -> proof_instr diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml new file mode 100644 index 00000000..da88d48d --- /dev/null +++ b/plugins/decl_mode/decl_mode.ml @@ -0,0 +1,123 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Term +open Evd +open Util + + +let daimon_flag = ref false + +let set_daimon_flag () = daimon_flag:=true +let clear_daimon_flag () = daimon_flag:=false +let get_daimon_flag () = !daimon_flag + + + +(* Information associated to goals. *) +open Store.Field + +type split_tree= + Skip_patt of Idset.t * split_tree + | Split_patt of Idset.t * inductive * + (bool array * (Idset.t * split_tree) option) array + | Close_patt of split_tree + | End_patt of (identifier * (int * int)) + +type elim_kind = + EK_dep of split_tree + | EK_nodep + | EK_unknown + +type recpath = int option*Declarations.wf_paths + +type per_info = + {per_casee:constr; + per_ctype:types; + per_ind:inductive; + per_pred:constr; + per_args:constr list; + per_params:constr list; + per_nparams:int; + per_wf:recpath} + +type stack_info = + Per of Decl_expr.elim_type * per_info * elim_kind * identifier list + | Suppose_case + | Claim + | Focus_claim + +type pm_info = + { pm_stack : stack_info list} +let info = Store.field () + + +(* Current proof mode *) + +type command_mode = + Mode_tactic + | Mode_proof + | Mode_none + +let mode_of_pftreestate pts = + (* spiwack: it used to be "top_goal_..." but this should be fine *) + let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in + let goal = List.hd goals in + if info.get (Goal.V82.extra sigma goal) = None then + Mode_tactic + else + Mode_proof + +let get_current_mode () = + try + mode_of_pftreestate (Pfedit.get_pftreestate ()) + with e when Errors.noncritical e -> Mode_none + +let check_not_proof_mode str = + if get_current_mode () = Mode_proof then + error str + +let get_info sigma gl= + match info.get (Goal.V82.extra sigma gl) with + | None -> invalid_arg "get_info" + | Some pm -> pm + +let try_get_info sigma gl = + info.get (Goal.V82.extra sigma gl) + +let get_stack pts = + let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in + let info = get_info sigma (List.hd goals) in + info.pm_stack + + +let proof_focus = Proof.new_focus_kind () +let proof_cond = Proof.no_cond proof_focus + +let focus p = + let inf = get_stack p in + Proof.focus proof_cond inf 1 p + +let unfocus = Proof.unfocus proof_focus + +let maximal_unfocus = Proof_global.maximal_unfocus proof_focus + +let get_top_stack pts = + try + Proof.get_at_focus proof_focus pts + with Proof.NoSuchFocus -> + let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in + let info = get_info sigma gl in + info.pm_stack + +let get_last env = + try + let (id,_,_) = List.hd (Environ.named_context env) in id + with Invalid_argument _ -> error "no previous statement to use" + diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli new file mode 100644 index 00000000..f23a97b4 --- /dev/null +++ b/plugins/decl_mode/decl_mode.mli @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Term +open Evd +open Tacmach + +val set_daimon_flag : unit -> unit +val clear_daimon_flag : unit -> unit +val get_daimon_flag : unit -> bool + +type command_mode = + Mode_tactic + | Mode_proof + | Mode_none + +val mode_of_pftreestate : Proof.proof -> command_mode + +val get_current_mode : unit -> command_mode + +val check_not_proof_mode : string -> unit + +type split_tree= + Skip_patt of Idset.t * split_tree + | Split_patt of Idset.t * inductive * + (bool array * (Idset.t * split_tree) option) array + | Close_patt of split_tree + | End_patt of (identifier * (int * int)) + +type elim_kind = + EK_dep of split_tree + | EK_nodep + | EK_unknown + +type recpath = int option*Declarations.wf_paths + +type per_info = + {per_casee:constr; + per_ctype:types; + per_ind:inductive; + per_pred:constr; + per_args:constr list; + per_params:constr list; + per_nparams:int; + per_wf:recpath} + +type stack_info = + Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list + | Suppose_case + | Claim + | Focus_claim + +type pm_info = + {pm_stack : stack_info list } + +val info : pm_info Store.Field.t + +val get_info : Evd.evar_map -> Proof_type.goal -> pm_info + +val try_get_info : Evd.evar_map -> Proof_type.goal -> pm_info option + +val get_stack : Proof.proof -> stack_info list + +val get_top_stack : Proof.proof -> stack_info list + +val get_last: Environ.env -> identifier + +val focus : Proof.proof -> unit + +val unfocus : Proof.proof -> unit + +val maximal_unfocus : Proof.proof -> unit diff --git a/plugins/decl_mode/decl_mode_plugin.mllib b/plugins/decl_mode/decl_mode_plugin.mllib new file mode 100644 index 00000000..39342dbd --- /dev/null +++ b/plugins/decl_mode/decl_mode_plugin.mllib @@ -0,0 +1,6 @@ +Decl_mode +Decl_interp +Decl_proof_instr +Ppdecl_proof +G_decl_mode +Decl_mode_plugin_mod diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml new file mode 100644 index 00000000..ab161b35 --- /dev/null +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -0,0 +1,1504 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Pp +open Evd + +open Refiner +open Proof_type +open Tacmach +open Tacinterp +open Decl_expr +open Decl_mode +open Decl_interp +open Glob_term +open Names +open Nameops +open Declarations +open Tactics +open Tacticals +open Term +open Termops +open Namegen +open Reductionops +open Goptions + + +(* Strictness option *) + +let get_its_info gls = get_info gls.sigma gls.it + +let get_strictness,set_strictness = + let strictness = ref false in + (fun () -> (!strictness)),(fun b -> strictness:=b) + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "strict mode"; + optkey = ["Strict";"Proofs"]; + optread = get_strictness; + optwrite = set_strictness } + +let tcl_change_info_gen info_gen = + (fun gls -> + let concl = pf_concl gls in + let hyps = Goal.V82.hyps (project gls) (sig_it gls) in + let extra = Goal.V82.extra (project gls) (sig_it gls) in + let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in + let sigma = Goal.V82.partial_solution sigma (sig_it gls) ev in + { it = [gl] ; sigma= sigma } ) + +open Store.Field + +let tcl_change_info info gls = + let info_gen = Decl_mode.info.set info in + tcl_change_info_gen info_gen gls + +let tcl_erase_info gls = tcl_change_info_gen (Decl_mode.info.remove) gls + +let special_whd gl= + let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in + (fun t -> Closure.whd_val infos (Closure.inject t)) + +let special_nf gl= + let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in + (fun t -> Closure.norm_val infos (Closure.inject t)) + +let is_good_inductive env ind = + let mib,oib = Inductive.lookup_mind_specif env ind in + oib.mind_nrealargs = 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib)) + +let check_not_per pts = + if not (Proof.is_done pts) then + match get_stack pts with + Per (_,_,_,_)::_ -> + error "You are inside a proof per cases/induction.\n\ +Please \"suppose\" something or \"end\" it now." + | _ -> () + +let mk_evd metalist gls = + let evd0= create_goal_evar_defs (sig_sig gls) in + let add_one (meta,typ) evd = + meta_declare meta typ evd in + List.fold_right add_one metalist evd0 + +let is_tmp id = (string_of_id id).[0] = '_' + +let tmp_ids gls = + let ctx = pf_hyps gls in + match ctx with + [] -> [] + | _::q -> List.filter is_tmp (ids_of_named_context q) + +let clean_tmp gls = + let clean_id id0 gls0 = + tclTRY (clear [id0]) gls0 in + let rec clean_all = function + [] -> tclIDTAC + | id :: rest -> tclTHEN (clean_id id) (clean_all rest) + in + clean_all (tmp_ids gls) gls + +let assert_postpone id t = + assert_tac (Name id) t + +(* start a proof *) + + +let start_proof_tac gls= + let info={pm_stack=[]} in + tcl_change_info info gls + +let go_to_proof_mode () = + Pfedit.by start_proof_tac; + let p = Proof_global.give_me_the_proof () in + Decl_mode.focus p + +(* closing gaps *) + +let daimon_tac gls = + set_daimon_flag (); + {it=[];sigma=sig_sig gls} + + +(* marking closed blocks *) + +let rec is_focussing_instr = function + Pthus i | Pthen i | Phence i -> is_focussing_instr i + | Pescape | Pper _ | Pclaim _ | Pfocus _ + | Psuppose _ | Pcase (_,_,_) -> true + | _ -> false + +let mark_rule_as_done = function + Decl_proof true -> Decl_proof false + | Decl_proof false -> + anomaly "already marked as done" + | _ -> anomaly "mark_rule_as_done" + + +(* post-instruction focus management *) + +(* spiwack: This used to fail if there was no focusing command + above, but I don't think it ever happened. I hope it doesn't mess + things up*) +let goto_current_focus pts = + Decl_mode.maximal_unfocus pts + +let goto_current_focus_or_top pts = + goto_current_focus pts + +(* return *) + +let close_tactic_mode pts = + try goto_current_focus pts + with Not_found -> + error "\"return\" cannot be used outside of Declarative Proof Mode." + +let return_from_tactic_mode () = + close_tactic_mode (Proof_global.give_me_the_proof ()) + +(* end proof/claim *) + +let close_block bt pts = + if Proof.no_focused_goal pts then + goto_current_focus pts + else + let stack = + if Proof.is_done pts then + get_top_stack pts + else + get_stack pts + in + match bt,stack with + B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> + (goto_current_focus pts) + | _, Claim::_ -> + error "\"end claim\" expected." + | _, Focus_claim::_ -> + error "\"end focus\" expected." + | _, [] -> + error "\"end proof\" expected." + | _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) -> + begin + match et with + ET_Case_analysis -> error "\"end cases\" expected." + | ET_Induction -> error "\"end induction\" expected." + end + | _,_ -> anomaly "Lonely suppose on stack." + + +(* utility for suppose / suppose it is *) + +let close_previous_case pts = + if + Proof.is_done pts + then + match get_top_stack pts with + Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..." + | Suppose_case :: Per (et,_,_,_) :: _ -> + goto_current_focus (pts) + | _ -> error "Not inside a proof per cases or induction." + else + match get_stack pts with + Per (et,_,_,_) :: _ -> () + | Suppose_case :: Per (et,_,_,_) :: _ -> + goto_current_focus ((pts)) + | _ -> error "Not inside a proof per cases or induction." + +(* Proof instructions *) + +(* automation *) + +let filter_hyps f gls = + let filter_aux (id,_,_) = + if f id then + tclIDTAC + else + tclTRY (clear [id]) in + tclMAP filter_aux (pf_hyps gls) gls + +let local_hyp_prefix = id_of_string "___" + +let add_justification_hyps keep items gls = + let add_aux c gls= + match kind_of_term c with + Var id -> + keep:=Idset.add id !keep; + tclIDTAC gls + | _ -> + let id=pf_get_new_id local_hyp_prefix gls in + keep:=Idset.add id !keep; + tclTHEN (letin_tac None (Names.Name id) c None Tacexpr.nowhere) + (thin_body [id]) gls in + tclMAP add_aux items gls + +let prepare_goal items gls = + let tokeep = ref Idset.empty in + let auxres = add_justification_hyps tokeep items gls in + tclTHENLIST + [ (fun _ -> auxres); + filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep)] gls + +let my_automation_tac = ref + (fun gls -> anomaly "No automation registered") + +let register_automation_tac tac = my_automation_tac:= tac + +let automation_tac gls = !my_automation_tac gls + +let justification tac gls= + tclORELSE + (tclSOLVE [tclTHEN tac assumption]) + (fun gls -> + if get_strictness () then + error "Insufficient justification." + else + begin + msg_warning (str "Insufficient justification."); + daimon_tac gls + end) gls + +let default_justification elems gls= + justification (tclTHEN (prepare_goal elems) automation_tac) gls + +(* code for conclusion refining *) + +let constant dir s = lazy (Coqlib.gen_constant "Declarative" dir s) + +let _and = constant ["Init";"Logic"] "and" + +let _and_rect = constant ["Init";"Logic"] "and_rect" + +let _prod = constant ["Init";"Datatypes"] "prod" + +let _prod_rect = constant ["Init";"Datatypes"] "prod_rect" + +let _ex = constant ["Init";"Logic"] "ex" + +let _ex_ind = constant ["Init";"Logic"] "ex_ind" + +let _sig = constant ["Init";"Specif"] "sig" + +let _sig_rect = constant ["Init";"Specif"] "sig_rect" + +let _sigT = constant ["Init";"Specif"] "sigT" + +let _sigT_rect = constant ["Init";"Specif"] "sigT_rect" + +type stackd_elt = +{se_meta:metavariable; + se_type:types; + se_last_meta:metavariable; + se_meta_list:(metavariable*types) list; + se_evd: evar_map} + +let rec replace_in_list m l = function + [] -> raise Not_found + | c::q -> if m=fst c then l@q else c::replace_in_list m l q + +let enstack_subsubgoals env se stack gls= + let hd,params = decompose_app (special_whd gls se.se_type) in + match kind_of_term hd with + Ind ind when is_good_inductive env ind -> + let mib,oib= + Inductive.lookup_mind_specif env ind in + let gentypes= + Inductive.arities_of_constructors ind (mib,oib) in + let process i gentyp = + let constructor = mkConstruct(ind,succ i) + (* constructors numbering*) in + let appterm = applist (constructor,params) in + let apptype = Term.prod_applist gentyp params in + let rc,_ = Reduction.dest_prod env apptype in + let rec meta_aux last lenv = function + [] -> (last,lenv,[]) + | (nam,_,typ)::q -> + let nlast=succ last in + let (llast,holes,metas) = + meta_aux nlast (mkMeta nlast :: lenv) q in + (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in + let (nlast,holes,nmetas) = + meta_aux se.se_last_meta [] (List.rev rc) in + let refiner = applist (appterm,List.rev holes) in + let evd = meta_assign se.se_meta + (refiner,(Conv,TypeProcessed (* ? *))) se.se_evd in + let ncreated = replace_in_list + se.se_meta nmetas se.se_meta_list in + let evd0 = List.fold_left + (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in + List.iter (fun (m,typ) -> + Stack.push + {se_meta=m; + se_type=typ; + se_evd=evd0; + se_meta_list=ncreated; + se_last_meta=nlast} stack) (List.rev nmetas) + in + Array.iteri process gentypes + | _ -> () + +let rec nf_list evd = + function + [] -> [] + | (m,typ)::others -> + if meta_defined evd m then + nf_list evd others + else + (m,nf_meta evd typ)::nf_list evd others + +let find_subsubgoal c ctyp skip submetas gls = + let env= pf_env gls in + let concl = pf_concl gls in + let evd = mk_evd ((0,concl)::submetas) gls in + let stack = Stack.create () in + let max_meta = + List.fold_left (fun a (m,_) -> max a m) 0 submetas in + let _ = Stack.push + {se_meta=0; + se_type=concl; + se_last_meta=max_meta; + se_meta_list=[0,concl]; + se_evd=evd} stack in + let rec dfs n = + let se = Stack.pop stack in + try + let unifier = + Unification.w_unify env se.se_evd Reduction.CUMUL + ~flags:Unification.elim_flags ctyp se.se_type in + if n <= 0 then + {se with + se_evd=meta_assign se.se_meta + (c,(Conv,TypeNotProcessed (* ?? *))) unifier; + se_meta_list=replace_in_list + se.se_meta submetas se.se_meta_list} + else + dfs (pred n) + with e when Errors.noncritical e -> + begin + enstack_subsubgoals env se stack gls; + dfs n + end in + let nse= try dfs skip with Stack.Empty -> raise Not_found in + nf_list nse.se_evd nse.se_meta_list,nf_meta nse.se_evd (mkMeta 0) + +let concl_refiner metas body gls = + let concl = pf_concl gls in + let evd = sig_sig gls in + let env = pf_env gls in + let sort = family_of_sort (Typing.sort_of env evd concl) in + let rec aux env avoid subst = function + [] -> anomaly "concl_refiner: cannot happen" + | (n,typ)::rest -> + let _A = subst_meta subst typ in + let x = id_of_name_using_hdchar env _A Anonymous in + let _x = fresh_id avoid x gls in + let nenv = Environ.push_named (_x,None,_A) env in + let asort = family_of_sort (Typing.sort_of nenv evd _A) in + let nsubst = (n,mkVar _x)::subst in + if rest = [] then + asort,_A,mkNamedLambda _x _A (subst_meta nsubst body) + else + let bsort,_B,nbody = + aux nenv (_x::avoid) ((n,mkVar _x)::subst) rest in + let body = mkNamedLambda _x _A nbody in + if occur_term (mkVar _x) _B then + begin + let _P = mkNamedLambda _x _A _B in + match bsort,sort with + InProp,InProp -> + let _AxB = mkApp(Lazy.force _ex,[|_A;_P|]) in + InProp,_AxB, + mkApp(Lazy.force _ex_ind,[|_A;_P;concl;body|]) + | InProp,_ -> + let _AxB = mkApp(Lazy.force _sig,[|_A;_P|]) in + let _P0 = mkLambda(Anonymous,_AxB,concl) in + InType,_AxB, + mkApp(Lazy.force _sig_rect,[|_A;_P;_P0;body|]) + | _,_ -> + let _AxB = mkApp(Lazy.force _sigT,[|_A;_P|]) in + let _P0 = mkLambda(Anonymous,_AxB,concl) in + InType,_AxB, + mkApp(Lazy.force _sigT_rect,[|_A;_P;_P0;body|]) + end + else + begin + match asort,bsort with + InProp,InProp -> + let _AxB = mkApp(Lazy.force _and,[|_A;_B|]) in + InProp,_AxB, + mkApp(Lazy.force _and_rect,[|_A;_B;concl;body|]) + |_,_ -> + let _AxB = mkApp(Lazy.force _prod,[|_A;_B|]) in + let _P0 = mkLambda(Anonymous,_AxB,concl) in + InType,_AxB, + mkApp(Lazy.force _prod_rect,[|_A;_B;_P0;body|]) + end + in + let (_,_,prf) = aux env [] [] metas in + mkApp(prf,[|mkMeta 1|]) + +let thus_tac c ctyp submetas gls = + let list,proof = + try + find_subsubgoal c ctyp 0 submetas gls + with Not_found -> + error "I could not relate this statement to the thesis." in + if list = [] then + exact_check proof gls + else + let refiner = concl_refiner list proof gls in + Tactics.refine refiner gls + +(* general forward step *) + +let mk_stat_or_thesis info gls = function + This c -> c + | Thesis (For _ ) -> + error "\"thesis for ...\" is not applicable here." + | Thesis Plain -> pf_concl gls + +let just_tac _then cut info gls0 = + let last_item = if _then then + let last_id = try get_last (pf_env gls0) with Failure _ -> + error "\"then\" and \"hence\" require at least one previous fact" in + [mkVar last_id] + else [] + in + let items_tac gls = + match cut.cut_by with + None -> tclIDTAC gls + | Some items -> prepare_goal (last_item@items) gls in + let method_tac gls = + match cut.cut_using with + None -> + automation_tac gls + | Some tac -> + (Tacinterp.eval_tactic tac) gls in + justification (tclTHEN items_tac method_tac) gls0 + +let instr_cut mkstat _thus _then cut gls0 = + let info = get_its_info gls0 in + let stat = cut.cut_stat in + let (c_id,_) = match stat.st_label with + Anonymous -> + pf_get_new_id (id_of_string "_fact") gls0,false + | Name id -> id,true in + let c_stat = mkstat info gls0 stat.st_it in + let thus_tac gls= + if _thus then + thus_tac (mkVar c_id) c_stat [] gls + else tclIDTAC gls in + tclTHENS (assert_postpone c_id c_stat) + [tclTHEN tcl_erase_info (just_tac _then cut info); + thus_tac] gls0 + + + +(* iterated equality *) +let _eq = Libnames.constr_of_global (Coqlib.glob_eq) + +let decompose_eq id gls = + let typ = pf_get_hyp_typ gls id in + let whd = (special_whd gls typ) in + match kind_of_term whd with + App (f,args)-> + if eq_constr f _eq && (Array.length args)=3 + then (args.(0), + args.(1), + args.(2)) + else error "Previous step is not an equality." + | _ -> error "Previous step is not an equality." + +let instr_rew _thus rew_side cut gls0 = + let last_id = + try get_last (pf_env gls0) + with e when Errors.noncritical e -> + error "No previous equality." + in + let typ,lhs,rhs = decompose_eq last_id gls0 in + let items_tac gls = + match cut.cut_by with + None -> tclIDTAC gls + | Some items -> prepare_goal items gls in + let method_tac gls = + match cut.cut_using with + None -> + automation_tac gls + | Some tac -> + (Tacinterp.eval_tactic tac) gls in + let just_tac gls = + justification (tclTHEN items_tac method_tac) gls in + let (c_id,_) = match cut.cut_stat.st_label with + Anonymous -> + pf_get_new_id (id_of_string "_eq") gls0,false + | Name id -> id,true in + let thus_tac new_eq gls= + if _thus then + thus_tac (mkVar c_id) new_eq [] gls + else tclIDTAC gls in + match rew_side with + Lhs -> + let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in + tclTHENS (assert_postpone c_id new_eq) + [tclTHEN tcl_erase_info + (tclTHENS (transitivity lhs) + [just_tac;exact_check (mkVar last_id)]); + thus_tac new_eq] gls0 + | Rhs -> + let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in + tclTHENS (assert_postpone c_id new_eq) + [tclTHEN tcl_erase_info + (tclTHENS (transitivity rhs) + [exact_check (mkVar last_id);just_tac]); + thus_tac new_eq] gls0 + + + +(* tactics for claim/focus *) + +let instr_claim _thus st gls0 = + let info = get_its_info gls0 in + let (id,_) = match st.st_label with + Anonymous -> pf_get_new_id (id_of_string "_claim") gls0,false + | Name id -> id,true in + let thus_tac gls= + if _thus then + thus_tac (mkVar id) st.st_it [] gls + else tclIDTAC gls in + let ninfo1 = {pm_stack= + (if _thus then Focus_claim else Claim)::info.pm_stack} in + tclTHENS (assert_postpone id st.st_it) + [thus_tac; + tcl_change_info ninfo1] gls0 + +(* tactics for assume *) + +let push_intro_tac coerce nam gls = + let (hid,_) = + match nam with + Anonymous -> pf_get_new_id (id_of_string "_hyp") gls,false + | Name id -> id,true in + tclTHENLIST + [intro_mustbe_force hid; + coerce hid] + gls + +let assume_tac hyps gls = + List.fold_right + (fun (Hvar st | Hprop st) -> + tclTHEN + (push_intro_tac + (fun id -> + convert_hyp (id,None,st.st_it)) st.st_label)) + hyps tclIDTAC gls + +let assume_hyps_or_theses hyps gls = + List.fold_right + (function + (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) -> + tclTHEN + (push_intro_tac + (fun id -> + convert_hyp (id,None,c)) nam) + | Hprop {st_label=nam;st_it=Thesis (tk)} -> + tclTHEN + (push_intro_tac + (fun id -> tclIDTAC) nam)) + hyps tclIDTAC gls + +let assume_st hyps gls = + List.fold_right + (fun st -> + tclTHEN + (push_intro_tac + (fun id -> convert_hyp (id,None,st.st_it)) st.st_label)) + hyps tclIDTAC gls + +let assume_st_letin hyps gls = + List.fold_right + (fun st -> + tclTHEN + (push_intro_tac + (fun id -> + convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label)) + hyps tclIDTAC gls + +(* suffices *) + +let rec metas_from n hyps = + match hyps with + _ :: q -> n :: metas_from (succ n) q + | [] -> [] + +let rec build_product args body = + match args with + (Hprop st| Hvar st )::rest -> + let pprod= lift 1 (build_product rest body) in + let lbody = + match st.st_label with + Anonymous -> pprod + | Name id -> subst_term (mkVar id) pprod in + mkProd (st.st_label, st.st_it, lbody) + | [] -> body + +let rec build_applist prod = function + [] -> [],prod + | n::q -> + let (_,typ,_) = destProd prod in + let ctx,head = build_applist (Term.prod_applist prod [mkMeta n]) q in + (n,typ)::ctx,head + +let instr_suffices _then cut gls0 = + let info = get_its_info gls0 in + let c_id = pf_get_new_id (id_of_string "_cofact") gls0 in + let ctx,hd = cut.cut_stat in + let c_stat = build_product ctx (mk_stat_or_thesis info gls0 hd) in + let metas = metas_from 1 ctx in + let c_ctx,c_head = build_applist c_stat metas in + let c_term = applist (mkVar c_id,List.map mkMeta metas) in + let thus_tac gls= + thus_tac c_term c_head c_ctx gls in + tclTHENS (assert_postpone c_id c_stat) + [tclTHENLIST + [ assume_tac ctx; + tcl_erase_info; + just_tac _then cut info]; + thus_tac] gls0 + +(* tactics for consider/given *) + +let conjunction_arity id gls = + let typ = pf_get_hyp_typ gls id in + let hd,params = decompose_app (special_whd gls typ) in + let env =pf_env gls in + match kind_of_term hd with + Ind ind when is_good_inductive env ind -> + let mib,oib= + Inductive.lookup_mind_specif env ind in + let gentypes= + Inductive.arities_of_constructors ind (mib,oib) in + let _ = if Array.length gentypes <> 1 then raise Not_found in + let apptype = Term.prod_applist gentypes.(0) params in + let rc,_ = Reduction.dest_prod env apptype in + List.length rc + | _ -> raise Not_found + +let rec intron_then n ids ltac gls = + if n<=0 then + ltac ids gls + else + let id = pf_get_new_id (id_of_string "_tmp") gls in + tclTHEN + (intro_mustbe_force id) + (intron_then (pred n) (id::ids) ltac) gls + + +let rec consider_match may_intro introduced available expected gls = + match available,expected with + [],[] -> + tclIDTAC gls + | _,[] -> error "Last statements do not match a complete hypothesis." + (* should tell which ones *) + | [],hyps -> + if may_intro then + begin + let id = pf_get_new_id (id_of_string "_tmp") gls in + tclIFTHENELSE + (intro_mustbe_force id) + (consider_match true [] [id] hyps) + (fun _ -> + error "Not enough sub-hypotheses to match statements.") + gls + end + else + error "Not enough sub-hypotheses to match statements." + (* should tell which ones *) + | id::rest_ids,(Hvar st | Hprop st)::rest -> + tclIFTHENELSE (convert_hyp (id,None,st.st_it)) + begin + match st.st_label with + Anonymous -> + consider_match may_intro ((id,false)::introduced) rest_ids rest + | Name hid -> + tclTHENLIST + [rename_hyp [id,hid]; + consider_match may_intro ((hid,true)::introduced) rest_ids rest] + end + begin + (fun gls -> + let nhyps = + try conjunction_arity id gls with + Not_found -> error "Matching hypothesis not found." in + tclTHENLIST + [general_case_analysis false (mkVar id,NoBindings); + intron_then nhyps [] + (fun l -> consider_match may_intro introduced + (List.rev_append l rest_ids) expected)] gls) + end + gls + +let consider_tac c hyps gls = + match kind_of_term (strip_outer_cast c) with + Var id -> + consider_match false [] [id] hyps gls + | _ -> + let id = pf_get_new_id (id_of_string "_tmp") gls in + tclTHEN + (forward None (Some (dummy_loc, Genarg.IntroIdentifier id)) c) + (consider_match false [] [id] hyps) gls + + +let given_tac hyps gls = + consider_match true [] [] hyps gls + +(* tactics for take *) + +let rec take_tac wits gls = + match wits with + [] -> tclIDTAC gls + | wit::rest -> + let typ = pf_type_of gls wit in + tclTHEN (thus_tac wit typ []) (take_tac rest) gls + + +(* tactics for define *) + +let rec build_function args body = + match args with + st::rest -> + let pfun= lift 1 (build_function rest body) in + let id = match st.st_label with + Anonymous -> assert false + | Name id -> id in + mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun) + | [] -> body + +let define_tac id args body gls = + let t = build_function args body in + letin_tac None (Name id) t None Tacexpr.nowhere gls + +(* tactics for reconsider *) + +let cast_tac id_or_thesis typ gls = + match id_or_thesis with + This id -> + let (_,body,_) = pf_get_hyp gls id in + convert_hyp (id,body,typ) gls + | Thesis (For _ ) -> + error "\"thesis for ...\" is not applicable here." + | Thesis Plain -> + convert_concl typ DEFAULTcast gls + +(* per cases *) + +let is_rec_pos (main_ind,wft) = + match main_ind with + None -> false + | Some index -> + match fst (Rtree.dest_node wft) with + Mrec (_,i) when i = index -> true + | _ -> false + +let rec constr_trees (main_ind,wft) ind = + match Rtree.dest_node wft with + Norec,_ -> + let itree = + (snd (Global.lookup_inductive ind)).mind_recargs in + constr_trees (None,itree) ind + | _,constrs -> main_ind,constrs + +let ind_args rp ind = + let main_ind,constrs = constr_trees rp ind in + let args ctree = + Array.map (fun t -> main_ind,t) (snd (Rtree.dest_node ctree)) in + Array.map args constrs + +let init_tree ids ind rp nexti = + let indargs = ind_args rp ind in + let do_i i arp = (Array.map is_rec_pos arp),nexti i arp in + Split_patt (ids,ind,Array.mapi do_i indargs) + +let map_tree_rp rp id_fun mapi = function + Split_patt (ids,ind,branches) -> + let indargs = ind_args rp ind in + let do_i i (recargs,bri) = recargs,mapi i indargs.(i) bri in + Split_patt (id_fun ids,ind,Array.mapi do_i branches) + | _ -> failwith "map_tree_rp: not a splitting node" + +let map_tree id_fun mapi = function + Split_patt (ids,ind,branches) -> + let do_i i (recargs,bri) = recargs,mapi i bri in + Split_patt (id_fun ids,ind,Array.mapi do_i branches) + | _ -> failwith "map_tree: not a splitting node" + + +let start_tree env ind rp = + init_tree Idset.empty ind rp (fun _ _ -> None) + +let build_per_info etype casee gls = + let concl=pf_concl gls in + let env=pf_env gls in + let ctyp=pf_type_of gls casee in + let is_dep = dependent casee concl in + let hd,args = decompose_app (special_whd gls ctyp) in + let ind = + try + destInd hd + with e when Errors.noncritical e -> + error "Case analysis must be done on an inductive object." in + let mind,oind = Global.lookup_inductive ind in + let nparams,index = + match etype with + ET_Induction -> mind.mind_nparams_rec,Some (snd ind) + | _ -> mind.mind_nparams,None in + let params,real_args = list_chop nparams args in + let abstract_obj c body = + let typ=pf_type_of gls c in + lambda_create env (typ,subst_term c body) in + let pred= List.fold_right abstract_obj + real_args (lambda_create env (ctyp,subst_term casee concl)) in + is_dep, + {per_casee=casee; + per_ctype=ctyp; + per_ind=ind; + per_pred=pred; + per_args=real_args; + per_params=params; + per_nparams=nparams; + per_wf=index,oind.mind_recargs} + +let per_tac etype casee gls= + let env=pf_env gls in + let info = get_its_info gls in + match casee with + Real c -> + let is_dep,per_info = build_per_info etype c gls in + let ek = + if is_dep then + EK_dep (start_tree env per_info.per_ind per_info.per_wf) + else EK_unknown in + tcl_change_info + {pm_stack= + Per(etype,per_info,ek,[])::info.pm_stack} gls + | Virtual cut -> + assert (cut.cut_stat.st_label=Anonymous); + let id = pf_get_new_id (id_of_string "anonymous_matched") gls in + let c = mkVar id in + let modified_cut = + {cut with cut_stat={cut.cut_stat with st_label=Name id}} in + tclTHEN + (instr_cut (fun _ _ c -> c) false false modified_cut) + (fun gls0 -> + let is_dep,per_info = build_per_info etype c gls0 in + assert (not is_dep); + tcl_change_info + {pm_stack= + Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0) + gls + +(* suppose *) + +let register_nodep_subcase id= function + Per(et,pi,ek,clauses)::s -> + begin + match ek with + EK_unknown -> clauses,Per(et,pi,EK_nodep,id::clauses)::s + | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s + | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"." + end + | _ -> anomaly "wrong stack state" + +let suppose_tac hyps gls0 = + let info = get_its_info gls0 in + let thesis = pf_concl gls0 in + let id = pf_get_new_id (id_of_string "subcase_") gls0 in + let clause = build_product hyps thesis in + let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in + let old_clauses,stack = register_nodep_subcase id info.pm_stack in + let ninfo2 = {pm_stack=stack} in + tclTHENS (assert_postpone id clause) + [tclTHENLIST [tcl_change_info ninfo1; + assume_tac hyps; + clear old_clauses]; + tcl_change_info ninfo2] gls0 + +(* suppose it is ... *) + +(* pattern matching compiling *) + +let rec skip_args rest ids n = + if n <= 0 then + Close_patt rest + else + Skip_patt (ids,skip_args rest ids (pred n)) + +let rec tree_of_pats ((id,_) as cpl) pats = + match pats with + [] -> End_patt cpl + | args::stack -> + match args with + [] -> Close_patt (tree_of_pats cpl stack) + | (patt,rp) :: rest_args -> + match patt with + PatVar (_,v) -> + Skip_patt (Idset.singleton id, + tree_of_pats cpl (rest_args::stack)) + | PatCstr (_,(ind,cnum),args,nam) -> + let nexti i ati = + if i = pred cnum then + let nargs = + list_map_i (fun j a -> (a,ati.(j))) 0 args in + Some (Idset.singleton id, + tree_of_pats cpl (nargs::rest_args::stack)) + else None + in init_tree Idset.empty ind rp nexti + +let rec add_branch ((id,_) as cpl) pats tree= + match pats with + [] -> + begin + match tree with + End_patt cpl0 -> End_patt cpl0 + (* this ensures precedence for overlapping patterns *) + | _ -> anomaly "tree is expected to end here" + end + | args::stack -> + match args with + [] -> + begin + match tree with + Close_patt t -> + Close_patt (add_branch cpl stack t) + | _ -> anomaly "we should pop here" + end + | (patt,rp) :: rest_args -> + match patt with + PatVar (_,v) -> + begin + match tree with + Skip_patt (ids,t) -> + Skip_patt (Idset.add id ids, + add_branch cpl (rest_args::stack) t) + | Split_patt (_,_,_) -> + map_tree (Idset.add id) + (fun i bri -> + append_branch cpl 1 (rest_args::stack) bri) + tree + | _ -> anomaly "No pop/stop expected here" + end + | PatCstr (_,(ind,cnum),args,nam) -> + match tree with + Skip_patt (ids,t) -> + let nexti i ati = + if i = pred cnum then + let nargs = + list_map_i (fun j a -> (a,ati.(j))) 0 args in + Some (Idset.add id ids, + add_branch cpl (nargs::rest_args::stack) + (skip_args t ids (Array.length ati))) + else + Some (ids, + skip_args t ids (Array.length ati)) + in init_tree ids ind rp nexti + | Split_patt (_,ind0,_) -> + if (ind <> ind0) then error + (* this can happen with coercions *) + "Case pattern belongs to wrong inductive type."; + let mapi i ati bri = + if i = pred cnum then + let nargs = + list_map_i (fun j a -> (a,ati.(j))) 0 args in + append_branch cpl 0 + (nargs::rest_args::stack) bri + else bri in + map_tree_rp rp (fun ids -> ids) mapi tree + | _ -> anomaly "No pop/stop expected here" +and append_branch ((id,_) as cpl) depth pats = function + Some (ids,tree) -> + Some (Idset.add id ids,append_tree cpl depth pats tree) + | None -> + Some (Idset.singleton id,tree_of_pats cpl pats) +and append_tree ((id,_) as cpl) depth pats tree = + if depth<=0 then add_branch cpl pats tree + else match tree with + Close_patt t -> + Close_patt (append_tree cpl (pred depth) pats t) + | Skip_patt (ids,t) -> + Skip_patt (Idset.add id ids,append_tree cpl depth pats t) + | End_patt _ -> anomaly "Premature end of branch" + | Split_patt (_,_,_) -> + map_tree (Idset.add id) + (fun i bri -> append_branch cpl (succ depth) pats bri) tree + +(* suppose it is *) + +let rec st_assoc id = function + [] -> raise Not_found + | st::_ when st.st_label = id -> st.st_it + | _ :: rest -> st_assoc id rest + +let thesis_for obj typ per_info env= + let rc,hd1=decompose_prod typ in + let cind,all_args=decompose_app typ in + let ind = destInd cind in + let _ = if ind <> per_info.per_ind then + errorlabstrm "thesis_for" + ((Printer.pr_constr_env env obj) ++ spc () ++ + str"cannot give an induction hypothesis (wrong inductive type).") in + let params,args = list_chop per_info.per_nparams all_args in + let _ = if not (List.for_all2 eq_constr params per_info.per_params) then + errorlabstrm "thesis_for" + ((Printer.pr_constr_env env obj) ++ spc () ++ + str "cannot give an induction hypothesis (wrong parameters).") in + let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in + compose_prod rc (whd_beta Evd.empty hd2) + +let rec build_product_dep pat_info per_info args body gls = + match args with + (Hprop {st_label=nam;st_it=This c} + | Hvar {st_label=nam;st_it=c})::rest -> + let pprod= + lift 1 (build_product_dep pat_info per_info rest body gls) in + let lbody = + match nam with + Anonymous -> body + | Name id -> subst_var id pprod in + mkProd (nam,c,lbody) + | Hprop ({st_it=Thesis tk} as st)::rest -> + let pprod= + lift 1 (build_product_dep pat_info per_info rest body gls) in + let lbody = + match st.st_label with + Anonymous -> body + | Name id -> subst_var id pprod in + let ptyp = + match tk with + For id -> + let obj = mkVar id in + let typ = + try st_assoc (Name id) pat_info.pat_vars + with Not_found -> + snd (st_assoc (Name id) pat_info.pat_aliases) in + thesis_for obj typ per_info (pf_env gls) + | Plain -> pf_concl gls in + mkProd (st.st_label,ptyp,lbody) + | [] -> body + +let build_dep_clause params pat_info per_info hyps gls = + let concl= + thesis_for pat_info.pat_constr pat_info.pat_typ per_info (pf_env gls) in + let open_clause = + build_product_dep pat_info per_info hyps concl gls in + let prod_one st body = + match st.st_label with + Anonymous -> mkProd(Anonymous,st.st_it,lift 1 body) + | Name id -> mkNamedProd id st.st_it (lift 1 body) in + let let_one_in st body = + match st.st_label with + Anonymous -> mkLetIn(Anonymous,fst st.st_it,snd st.st_it,lift 1 body) + | Name id -> + mkNamedLetIn id (fst st.st_it) (snd st.st_it) (lift 1 body) in + let aliased_clause = + List.fold_right let_one_in pat_info.pat_aliases open_clause in + List.fold_right prod_one (params@pat_info.pat_vars) aliased_clause + +let rec register_dep_subcase id env per_info pat = function + EK_nodep -> error "Only \"suppose it is\" can be used here." + | EK_unknown -> + register_dep_subcase id env per_info pat + (EK_dep (start_tree env per_info.per_ind per_info.per_wf)) + | EK_dep tree -> EK_dep (add_branch id [[pat,per_info.per_wf]] tree) + +let case_tac params pat_info hyps gls0 = + let info = get_its_info gls0 in + let id = pf_get_new_id (id_of_string "subcase_") gls0 in + let et,per_info,ek,old_clauses,rest = + match info.pm_stack with + Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) + | _ -> anomaly "wrong place for cases" in + let clause = build_dep_clause params pat_info per_info hyps gls0 in + let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in + let nek = + register_dep_subcase (id,(List.length params,List.length hyps)) + (pf_env gls0) per_info pat_info.pat_pat ek in + let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in + tclTHENS (assert_postpone id clause) + [tclTHENLIST + [tcl_change_info ninfo1; + assume_st (params@pat_info.pat_vars); + assume_st_letin pat_info.pat_aliases; + assume_hyps_or_theses hyps; + clear old_clauses]; + tcl_change_info ninfo2] gls0 + +(* end cases *) + +type instance_stack = + (constr option*(constr list) list) list + +let initial_instance_stack ids = + List.map (fun id -> id,[None,[]]) ids + +let push_one_arg arg = function + [] -> anomaly "impossible" + | (head,args) :: ctx -> + ((head,(arg::args)) :: ctx) + +let push_arg arg stacks = + List.map (fun (id,stack) -> (id,push_one_arg arg stack)) stacks + + +let push_one_head c ids (id,stack) = + let head = if Idset.mem id ids then Some c else None in + id,(head,[]) :: stack + +let push_head c ids stacks = + List.map (push_one_head c ids) stacks + +let pop_one (id,stack) = + let nstack= + match stack with + [] -> anomaly "impossible" + | [c] as l -> l + | (Some head,args)::(head0,args0)::ctx -> + let arg = applist (head,(List.rev args)) in + (head0,(arg::args0))::ctx + | (None,args)::(head0,args0)::ctx -> + (head0,(args@args0))::ctx + in id,nstack + +let pop_stacks stacks = + List.map pop_one stacks + +let hrec_for fix_id per_info gls obj_id = + let obj=mkVar obj_id in + let typ=pf_get_hyp_typ gls obj_id in + let rc,hd1=decompose_prod typ in + let cind,all_args=decompose_app typ in + let ind = destInd cind in assert (ind=per_info.per_ind); + let params,args= list_chop per_info.per_nparams all_args in + assert begin + try List.for_all2 eq_constr params per_info.per_params with + Invalid_argument _ -> false end; + let hd2 = applist (mkVar fix_id,args@[obj]) in + compose_lam rc (whd_beta gls.sigma hd2) + + +let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = + match tree, objs with + Close_patt t,_ -> + let args0 = pop_stacks args in + execute_cases fix_name per_info tacnext args0 objs nhrec t gls + | Skip_patt (_,t),skipped::next_objs -> + let args0 = push_arg skipped args in + execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls + | End_patt (id,(nparams,nhyps)),[] -> + begin + match List.assoc id args with + [None,br_args] -> + let all_metas = + list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in + let param_metas,hyp_metas = list_chop nparams all_metas in + tclTHEN + (tclDO nhrec introf) + (tacnext + (applist (mkVar id, + List.append param_metas + (List.rev_append br_args hyp_metas)))) gls + | _ -> anomaly "wrong stack size" + end + | Split_patt (ids,ind,br), casee::next_objs -> + let (mind,oind) as spec = Global.lookup_inductive ind in + let nparams = mind.mind_nparams in + let concl=pf_concl gls in + let env=pf_env gls in + let ctyp=pf_type_of gls casee in + let hd,all_args = decompose_app (special_whd gls ctyp) in + let _ = assert (destInd hd = ind) in (* just in case *) + let params,real_args = list_chop nparams all_args in + let abstract_obj c body = + let typ=pf_type_of gls c in + lambda_create env (typ,subst_term c body) in + let elim_pred = List.fold_right abstract_obj + real_args (lambda_create env (ctyp,subst_term casee concl)) in + let case_info = Inductiveops.make_case_info env ind RegularStyle in + let gen_arities = Inductive.arities_of_constructors ind spec in + let f_ids typ = + let sign = + (prod_assum (Term.prod_applist typ params)) in + find_intro_names sign gls in + let constr_args_ids = Array.map f_ids gen_arities in + let case_term = + mkCase(case_info,elim_pred,casee, + Array.mapi (fun i _ -> mkMeta (succ i)) constr_args_ids) in + let branch_tac i (recargs,bro) gls0 = + let args_ids = constr_args_ids.(i) in + let rec aux n = function + [] -> + assert (n=Array.length recargs); + next_objs,[],nhrec + | id :: q -> + let objs,recs,nrec = aux (succ n) q in + if recargs.(n) + then (mkVar id::objs),(id::recs),succ nrec + else (mkVar id::objs),recs,nrec in + let objs,recs,nhrec = aux 0 args_ids in + tclTHENLIST + [tclMAP intro_mustbe_force args_ids; + begin + fun gls1 -> + let hrecs = + List.map + (fun id -> + hrec_for (out_name fix_name) per_info gls1 id) + recs in + generalize hrecs gls1 + end; + match bro with + None -> + msg_warning (str "missing case"); + tacnext (mkMeta 1) + | Some (sub_ids,tree) -> + let br_args = + List.filter + (fun (id,_) -> Idset.mem id sub_ids) args in + let construct = + applist (mkConstruct(ind,succ i),params) in + let p_args = + push_head construct ids br_args in + execute_cases fix_name per_info tacnext + p_args objs nhrec tree] gls0 in + tclTHENSV + (refine case_term) + (Array.mapi branch_tac br) gls + | Split_patt (_, _, _) , [] -> + anomaly "execute_cases : Nothing to split" + | Skip_patt _ , [] -> + anomaly "execute_cases : Nothing to skip" + | End_patt (_,_) , _ :: _ -> + anomaly "execute_cases : End of branch with garbage left" + +let understand_my_constr c gls = + let env = pf_env gls in + let nc = names_of_rel_context env in + let rawc = Detyping.detype false [] nc c in + let rec frob = function GEvar _ -> GHole (dummy_loc,QuestionMark Expand) | rc -> map_glob_constr frob rc in + Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) + +let my_refine c gls = + let oc = understand_my_constr c gls in + Refine.refine oc gls + +(* end focus/claim *) + +let end_tac et2 gls = + let info = get_its_info gls in + let et1,pi,ek,clauses = + match info.pm_stack with + Suppose_case::_ -> + anomaly "This case should already be trapped" + | Claim::_ -> + error "\"end claim\" expected." + | Focus_claim::_ -> + error "\"end focus\" expected." + | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) + | [] -> + anomaly "This case should already be trapped" in + let et = + if et1 <> et2 then + match et1 with + ET_Case_analysis -> + error "\"end cases\" expected." + | ET_Induction -> + error "\"end induction\" expected." + else et1 in + tclTHEN + tcl_erase_info + begin + match et,ek with + _,EK_unknown -> + tclSOLVE [simplest_elim pi.per_casee] + | ET_Case_analysis,EK_nodep -> + tclTHEN + (general_case_analysis false (pi.per_casee,NoBindings)) + (default_justification (List.map mkVar clauses)) + | ET_Induction,EK_nodep -> + tclTHENLIST + [generalize (pi.per_args@[pi.per_casee]); + simple_induct (AnonHyp (succ (List.length pi.per_args))); + default_justification (List.map mkVar clauses)] + | ET_Case_analysis,EK_dep tree -> + execute_cases Anonymous pi + (fun c -> tclTHENLIST + [my_refine c; + clear clauses; + justification assumption]) + (initial_instance_stack clauses) [pi.per_casee] 0 tree + | ET_Induction,EK_dep tree -> + let nargs = (List.length pi.per_args) in + tclTHEN (generalize (pi.per_args@[pi.per_casee])) + begin + fun gls0 -> + let fix_id = + pf_get_new_id (id_of_string "_fix") gls0 in + let c_id = + pf_get_new_id (id_of_string "_main_arg") gls0 in + tclTHENLIST + [fix (Some fix_id) (succ nargs); + tclDO nargs introf; + intro_mustbe_force c_id; + execute_cases (Name fix_id) pi + (fun c -> + tclTHENLIST + [clear [fix_id]; + my_refine c; + clear clauses; + justification assumption]) + (initial_instance_stack clauses) + [mkVar c_id] 0 tree] gls0 + end + end gls + +(* escape *) + +let escape_tac gls = + (* spiwack: sets an empty info stack to avoid interferences. + We could erase the info altogether, but that doesn't play + well with the Decl_mode.focus (used in post_processing). *) + let info={pm_stack=[]} in + tcl_change_info info gls + +(* General instruction engine *) + +let rec do_proof_instr_gen _thus _then instr = + match instr with + Pthus i -> + assert (not _thus); + do_proof_instr_gen true _then i + | Pthen i -> + assert (not _then); + do_proof_instr_gen _thus true i + | Phence i -> + assert (not (_then || _thus)); + do_proof_instr_gen true true i + | Pcut c -> + instr_cut mk_stat_or_thesis _thus _then c + | Psuffices c -> + instr_suffices _then c + | Prew (s,c) -> + assert (not _then); + instr_rew _thus s c + | Pconsider (c,hyps) -> consider_tac c hyps + | Pgiven hyps -> given_tac hyps + | Passume hyps -> assume_tac hyps + | Plet hyps -> assume_tac hyps + | Pclaim st -> instr_claim false st + | Pfocus st -> instr_claim true st + | Ptake witl -> take_tac witl + | Pdefine (id,args,body) -> define_tac id args body + | Pcast (id,typ) -> cast_tac id typ + | Pper (et,cs) -> per_tac et cs + | Psuppose hyps -> suppose_tac hyps + | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps + | Pend (B_elim et) -> end_tac et + | Pend _ -> anomaly "Not applicable" + | Pescape -> escape_tac + +let eval_instr {instr=instr} = + do_proof_instr_gen false false instr + +let rec preprocess pts instr = + match instr with + Phence i |Pthus i | Pthen i -> preprocess pts i + | Psuffices _ | Pcut _ | Passume _ | Plet _ | Pclaim _ | Pfocus _ + | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ + | Pdefine (_,_,_) | Pper _ | Prew _ -> + check_not_per pts; + true + | Pescape -> + check_not_per pts; + true + | Pcase _ | Psuppose _ | Pend (B_elim _) -> + close_previous_case pts ; + true + | Pend bt -> + close_block bt pts ; + false + +let rec postprocess pts instr = + match instr with + Phence i | Pthus i | Pthen i -> postprocess pts i + | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_) + | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> () + | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> + Decl_mode.focus pts + | Pescape -> + Decl_mode.focus pts; + Proof_global.set_proof_mode "Classic" + | Pend (B_elim ET_Induction) -> + begin + let pfterm = List.hd (Proof.partial_proof pts) in + let { it = gls ; sigma = sigma } = Proof.V82.subgoals pts in + let env = try + Goal.V82.env sigma (List.hd gls) + with Failure "hd" -> + Global.env () + in + try + Inductiveops.control_only_guard env pfterm; + goto_current_focus_or_top pts + with + Type_errors.TypeError(env, + Type_errors.IllFormedRecBody(_,_,_,_,_)) -> + anomaly "\"end induction\" generated an ill-formed fixpoint" + end + | Pend _ -> + goto_current_focus_or_top (pts) + +let do_instr raw_instr pts = + let has_tactic = preprocess pts raw_instr.instr in + begin + if has_tactic then + let { it=gls ; sigma=sigma } = Proof.V82.subgoals pts in + let gl = { it=List.hd gls ; sigma=sigma } in + let env= pf_env gl in + let ist = {ltacvars = ([],[]); ltacrecvars = []; + gsigma = sigma; genv = env} in + let glob_instr = intern_proof_instr ist raw_instr in + let instr = + interp_proof_instr (get_its_info gl) sigma env glob_instr in + Pfedit.by (tclTHEN (eval_instr instr) clean_tmp) + else () end; + postprocess pts raw_instr.instr; + (* spiwack: this should restore a compatible semantics with + v8.3 where we never stayed focused on 0 goal. *) + Decl_mode.maximal_unfocus pts + +let proof_instr raw_instr = + let p = Proof_global.give_me_the_proof () in + do_instr raw_instr p + +(* + +(* STUFF FOR ITERATED RELATIONS *) +let decompose_bin_app t= + let hd,args = destApp + +let identify_transitivity_lemma c = + let varx,tx,c1 = destProd c in + let vary,ty,c2 = destProd (pop c1) in + let varz,tz,c3 = destProd (pop c2) in + let _,p1,c4 = destProd (pop c3) in + let _,lp2,lp3 = destProd (pop c4) in + let p2=pop lp2 in + let p3=pop lp3 in +*) + diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli new file mode 100644 index 00000000..775d2f53 --- /dev/null +++ b/plugins/decl_mode/decl_proof_instr.mli @@ -0,0 +1,109 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Refiner +open Names +open Term +open Tacmach +open Decl_mode + +val go_to_proof_mode: unit -> unit +val return_from_tactic_mode: unit -> unit + +val register_automation_tac: tactic -> unit + +val automation_tac : tactic + +val concl_refiner: + Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr + +val do_instr: Decl_expr.raw_proof_instr -> Proof.proof -> unit +val proof_instr: Decl_expr.raw_proof_instr -> unit + +val tcl_change_info : Decl_mode.pm_info -> tactic + +val execute_cases : + Names.name -> + Decl_mode.per_info -> + (Term.constr -> Proof_type.tactic) -> + (Names.Idset.elt * (Term.constr option * Term.constr list) list) list -> + Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic + +val tree_of_pats : + identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> + split_tree + +val add_branch : + identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> + split_tree -> split_tree + +val append_branch : + identifier *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> + (Names.Idset.t * Decl_mode.split_tree) option -> + (Names.Idset.t * Decl_mode.split_tree) option + +val append_tree : + identifier * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> + split_tree -> split_tree + +val build_dep_clause : Term.types Decl_expr.statement list -> + Decl_expr.proof_pattern -> + Decl_mode.per_info -> + (Term.types Decl_expr.statement, Term.types Decl_expr.or_thesis) + Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types + +val register_dep_subcase : + Names.identifier * (int * int) -> + Environ.env -> + Decl_mode.per_info -> + Glob_term.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind + +val thesis_for : Term.constr -> + Term.constr -> Decl_mode.per_info -> Environ.env -> Term.constr + +val close_previous_case : Proof.proof -> unit + +val pop_stacks : + (Names.identifier * + (Term.constr option * Term.constr list) list) list -> + (Names.identifier * + (Term.constr option * Term.constr list) list) list + +val push_head : Term.constr -> + Names.Idset.t -> + (Names.identifier * + (Term.constr option * Term.constr list) list) list -> + (Names.identifier * + (Term.constr option * Term.constr list) list) list + +val push_arg : Term.constr -> + (Names.identifier * + (Term.constr option * Term.constr list) list) list -> + (Names.identifier * + (Term.constr option * Term.constr list) list) list + +val hrec_for: + Names.identifier -> + Decl_mode.per_info -> Proof_type.goal Tacmach.sigma -> + Names.identifier -> Term.constr + +val consider_match : + bool -> + (Names.Idset.elt*bool) list -> + Names.Idset.elt list -> + (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list -> + Proof_type.tactic + +val init_tree: + Names.Idset.t -> + Names.inductive -> + int option * Declarations.wf_paths -> + (int -> + (int option * Declarations.recarg Rtree.t) array -> + (Names.Idset.t * Decl_mode.split_tree) option) -> + Decl_mode.split_tree diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 new file mode 100644 index 00000000..5699c1bf --- /dev/null +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -0,0 +1,409 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* arnaud: veiller à l'aspect tutorial des commentaires *) + +open Pp +open Tok +open Decl_expr +open Names +open Term +open Genarg +open Pcoq + +open Pcoq.Constr +open Pcoq.Tactic +open Pcoq.Vernac_ + +let pr_goal gs = + let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in + let env = Goal.V82.unfiltered_env sigma g in + let preamb,thesis,penv,pc = + (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), + (str "thesis := " ++ fnl ()), + Printer.pr_context_of env, + Printer.pr_goal_concl_style_env env (Goal.V82.concl sigma g) + in + preamb ++ + str" " ++ hv 0 (penv ++ fnl () ++ + str (Printer.emacs_str "") ++ + str "============================" ++ fnl () ++ + thesis ++ str " " ++ pc) ++ fnl () + +(* arnaud: rebrancher ça +let pr_open_subgoals () = + let p = Proof_global.give_me_the_proof () in + let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in + let close_cmd = Decl_mode.get_end_command p in + pr_subgoals close_cmd sigma goals +*) + +let pr_proof_instr instr = + Util.anomaly "Cannot print a proof_instr" + (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller + dans cette direction + Ppdecl_proof.pr_proof_instr (Global.env()) instr + *) +let pr_raw_proof_instr instr = + Util.anomaly "Cannot print a raw proof_instr" +let pr_glob_proof_instr instr = + Util.anomaly "Cannot print a non-interpreted proof_instr" + +let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= + Decl_interp.interp_proof_instr + (Decl_mode.get_info sigma gl) + (sigma) + (Goal.V82.env sigma gl) + +let vernac_decl_proof () = + let pf = Proof_global.give_me_the_proof () in + if Proof.is_done pf then + Util.error "Nothing left to prove here." + else + Proof.transaction pf begin fun () -> + Decl_proof_instr.go_to_proof_mode () ; + Proof_global.set_proof_mode "Declarative" ; + Vernacentries.print_subgoals () + end + +(* spiwack: some bureaucracy is not performed here *) +let vernac_return () = + Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + Decl_proof_instr.return_from_tactic_mode () ; + Proof_global.set_proof_mode "Declarative" ; + Vernacentries.print_subgoals () + end + +let vernac_proof_instr instr = + Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + Decl_proof_instr.proof_instr instr; + Vernacentries.print_subgoals () + end + +(* We create a new parser entry [proof_mode]. The Declarative proof mode + will replace the normal parser entry for tactics with this one. *) +let proof_mode = Gram.entry_create "vernac:proof_command" +(* Auxiliary grammar entry. *) +let proof_instr = Gram.entry_create "proofmode:instr" + +(* Before we can write an new toplevel command (see below) + which takes a [proof_instr] as argument, we need to declare + how to parse it, print it, globalise it and interprete it. + Normally we could do that easily through ARGUMENT EXTEND, + but as the parsing is fairly complicated we will do it manually to + indirect through the [proof_instr] grammar entry. *) +(* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *) + +(* [Genarg.create_arg] creates a new embedding into Genarg. *) +let (wit_proof_instr,globwit_proof_instr,rawwit_proof_instr) = + Genarg.create_arg None "proof_instr" +let _ = Tacinterp.add_interp_genarg "proof_instr" + begin + begin fun e x -> (* declares the globalisation function *) + Genarg.in_gen globwit_proof_instr + (Decl_interp.intern_proof_instr e (Genarg.out_gen rawwit_proof_instr x)) + end, + begin fun ist gl x -> (* declares the interpretation function *) + Tacmach.project gl , + Genarg.in_gen wit_proof_instr + (interp_proof_instr ist gl (Genarg.out_gen globwit_proof_instr x)) + end, + begin fun _ x -> x end (* declares the substitution function, irrelevant in our case *) + end + +let _ = Pptactic.declare_extra_genarg_pprule + (rawwit_proof_instr, pr_raw_proof_instr) + (globwit_proof_instr, pr_glob_proof_instr) + (wit_proof_instr, pr_proof_instr) + +(* We use the VERNAC EXTEND facility with a custom non-terminal + to populate [proof_mode] with a new toplevel interpreter. + The "-" indicates that the rule does not start with a distinguished + string. *) +VERNAC proof_mode EXTEND ProofInstr + [ - proof_instr(instr) ] -> [ vernac_proof_instr instr ] +END + +(* It is useful to use GEXTEND directly to call grammar entries that have been + defined previously VERNAC EXTEND. In this case we allow, in proof mode, + the use of commands like Check or Print. VERNAC EXTEND does quite a bit of + bureaucracy for us, but it is not needed in this sort of case, and it would require + to have an ARGUMENT EXTEND version of the "proof_mode" grammar entry. *) +GEXTEND Gram + GLOBAL: proof_mode ; + + proof_mode: LAST + [ [ c=G_vernac.subgoal_command -> c (Some 1) ] ] + ; +END + +(* We register a new proof mode here *) + +let _ = + Proof_global.register_proof_mode { Proof_global. + name = "Declarative" ; (* name for identifying and printing *) + (* function [set] goes from No Proof Mode to + Declarative Proof Mode performing side effects *) + set = begin fun () -> + (* We set the command non terminal to + [proof_mode] (which we just defined). *) + G_vernac.set_command_entry proof_mode ; + (* We substitute the goal printer, by the one we built + for the proof mode. *) + Printer.set_printer_pr { Printer.default_printer_pr with + Printer.pr_goal = pr_goal } + end ; + (* function [reset] goes back to No Proof Mode from + Declarative Proof Mode *) + reset = begin fun () -> + (* We restore the command non terminal to + [noedit_mode]. *) + G_vernac.set_command_entry G_vernac.noedit_mode ; + (* We restore the goal printer to default *) + Printer.set_printer_pr Printer.default_printer_pr + end + } + +(* Two new vernacular commands *) +VERNAC COMMAND EXTEND DeclProof + [ "proof" ] -> [ vernac_decl_proof () ] +END +VERNAC COMMAND EXTEND DeclReturn + [ "return" ] -> [ vernac_return () ] +END + +let none_is_empty = function + None -> [] + | Some l -> l + +GEXTEND Gram +GLOBAL: proof_instr; + thesis : + [[ "thesis" -> Plain + | "thesis"; "for"; i=ident -> (For i) + ]]; + statement : + [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c} + | i=ident -> {st_label=Anonymous; + st_it=Topconstr.CRef (Libnames.Ident (loc, i))} + | c=constr -> {st_label=Anonymous;st_it=c} + ]]; + constr_or_thesis : + [[ t=thesis -> Thesis t ] | + [ c=constr -> This c + ]]; + statement_or_thesis : + [ + [ t=thesis -> {st_label=Anonymous;st_it=Thesis t} ] + | + [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot} + | i=ident -> {st_label=Anonymous; + st_it=This (Topconstr.CRef (Libnames.Ident (loc, i)))} + | c=constr -> {st_label=Anonymous;st_it=This c} + ] + ]; + justification_items : + [[ -> Some [] + | "by"; l=LIST1 constr SEP "," -> Some l + | "by"; "*" -> None ]] + ; + justification_method : + [[ -> None + | "using"; tac = tactic -> Some tac ]] + ; + simple_cut_or_thesis : + [[ ls = statement_or_thesis; + j = justification_items; + taco = justification_method + -> {cut_stat=ls;cut_by=j;cut_using=taco} ]] + ; + simple_cut : + [[ ls = statement; + j = justification_items; + taco = justification_method + -> {cut_stat=ls;cut_by=j;cut_using=taco} ]] + ; + elim_type: + [[ IDENT "induction" -> ET_Induction + | IDENT "cases" -> ET_Case_analysis ]] + ; + block_type : + [[ IDENT "claim" -> B_claim + | IDENT "focus" -> B_focus + | IDENT "proof" -> B_proof + | et=elim_type -> B_elim et ]] + ; + elim_obj: + [[ IDENT "on"; c=constr -> Real c + | IDENT "of"; c=simple_cut -> Virtual c ]] + ; + elim_step: + [[ IDENT "consider" ; + h=consider_vars ; IDENT "from" ; c=constr -> Pconsider (c,h) + | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj) + | IDENT "suffices"; ls=suff_clause; + j = justification_items; + taco = justification_method + -> Psuffices {cut_stat=ls;cut_by=j;cut_using=taco} ]] + ; + rew_step : + [[ "~=" ; c=simple_cut -> (Rhs,c) + | "=~" ; c=simple_cut -> (Lhs,c)]] + ; + cut_step: + [[ "then"; tt=elim_step -> Pthen tt + | "then"; c=simple_cut_or_thesis -> Pthen (Pcut c) + | IDENT "thus"; tt=rew_step -> Pthus (let s,c=tt in Prew (s,c)) + | IDENT "thus"; c=simple_cut_or_thesis -> Pthus (Pcut c) + | IDENT "hence"; c=simple_cut_or_thesis -> Phence (Pcut c) + | tt=elim_step -> tt + | tt=rew_step -> let s,c=tt in Prew (s,c); + | IDENT "have"; c=simple_cut_or_thesis -> Pcut c; + | IDENT "claim"; c=statement -> Pclaim c; + | IDENT "focus"; IDENT "on"; c=statement -> Pfocus c; + | "end"; bt = block_type -> Pend bt; + | IDENT "escape" -> Pescape ]] + ; + (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*) + loc_id: + [[ id=ident -> fun x -> (loc,(id,x)) ]]; + hyp: + [[ id=loc_id -> id None ; + | id=loc_id ; ":" ; c=constr -> id (Some c)]] + ; + consider_vars: + [[ name=hyp -> [Hvar name] + | name=hyp; ","; v=consider_vars -> (Hvar name) :: v + | name=hyp; + IDENT "such"; IDENT "that"; h=consider_hyps -> (Hvar name)::h + ]] + ; + consider_hyps: + [[ st=statement; IDENT "and"; h=consider_hyps -> Hprop st::h + | st=statement; IDENT "and"; + IDENT "consider" ; v=consider_vars -> Hprop st::v + | st=statement -> [Hprop st] + ]] + ; + assume_vars: + [[ name=hyp -> [Hvar name] + | name=hyp; ","; v=assume_vars -> (Hvar name) :: v + | name=hyp; + IDENT "such"; IDENT "that"; h=assume_hyps -> (Hvar name)::h + ]] + ; + assume_hyps: + [[ st=statement; IDENT "and"; h=assume_hyps -> Hprop st::h + | st=statement; IDENT "and"; + IDENT "we"; IDENT "have" ; v=assume_vars -> Hprop st::v + | st=statement -> [Hprop st] + ]] + ; + assume_clause: + [[ IDENT "we" ; IDENT "have" ; v=assume_vars -> v + | h=assume_hyps -> h ]] + ; + suff_vars: + [[ name=hyp; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> + [Hvar name],c + | name=hyp; ","; v=suff_vars -> + let (q,c) = v in ((Hvar name) :: q),c + | name=hyp; + IDENT "such"; IDENT "that"; h=suff_hyps -> + let (q,c) = h in ((Hvar name) :: q),c + ]]; + suff_hyps: + [[ st=statement; IDENT "and"; h=suff_hyps -> + let (q,c) = h in (Hprop st::q),c + | st=statement; IDENT "and"; + IDENT "to" ; IDENT "have" ; v=suff_vars -> + let (q,c) = v in (Hprop st::q),c + | st=statement; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> + [Hprop st],c + ]] + ; + suff_clause: + [[ IDENT "to" ; IDENT "have" ; v=suff_vars -> v + | h=suff_hyps -> h ]] + ; + let_vars: + [[ name=hyp -> [Hvar name] + | name=hyp; ","; v=let_vars -> (Hvar name) :: v + | name=hyp; IDENT "be"; + IDENT "such"; IDENT "that"; h=let_hyps -> (Hvar name)::h + ]] + ; + let_hyps: + [[ st=statement; IDENT "and"; h=let_hyps -> Hprop st::h + | st=statement; IDENT "and"; "let"; v=let_vars -> Hprop st::v + | st=statement -> [Hprop st] + ]]; + given_vars: + [[ name=hyp -> [Hvar name] + | name=hyp; ","; v=given_vars -> (Hvar name) :: v + | name=hyp; IDENT "such"; IDENT "that"; h=given_hyps -> (Hvar name)::h + ]] + ; + given_hyps: + [[ st=statement; IDENT "and"; h=given_hyps -> Hprop st::h + | st=statement; IDENT "and"; IDENT "given"; v=given_vars -> Hprop st::v + | st=statement -> [Hprop st] + ]]; + suppose_vars: + [[name=hyp -> [Hvar name] + |name=hyp; ","; v=suppose_vars -> (Hvar name) :: v + |name=hyp; OPT[IDENT "be"]; + IDENT "such"; IDENT "that"; h=suppose_hyps -> (Hvar name)::h + ]] + ; + suppose_hyps: + [[ st=statement_or_thesis; IDENT "and"; h=suppose_hyps -> Hprop st::h + | st=statement_or_thesis; IDENT "and"; IDENT "we"; IDENT "have"; + v=suppose_vars -> Hprop st::v + | st=statement_or_thesis -> [Hprop st] + ]] + ; + suppose_clause: + [[ IDENT "we"; IDENT "have"; v=suppose_vars -> v; + | h=suppose_hyps -> h ]] + ; + intro_step: + [[ IDENT "suppose" ; h=assume_clause -> Psuppose h + | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ; + po=OPT[ "with"; p=LIST1 hyp SEP ","-> p ] ; + ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> + Pcase (none_is_empty po,c,none_is_empty ho) + | "let" ; v=let_vars -> Plet v + | IDENT "take"; witnesses = LIST1 constr SEP "," -> Ptake witnesses + | IDENT "assume"; h=assume_clause -> Passume h + | IDENT "given"; h=given_vars -> Pgiven h + | IDENT "define"; id=ident; args=LIST0 hyp; + "as"; body=constr -> Pdefine(id,args,body) + | IDENT "reconsider"; id=ident; "as" ; typ=constr -> Pcast (This id,typ) + | IDENT "reconsider"; t=thesis; "as" ; typ=constr -> Pcast (Thesis t ,typ) + ]] + ; + emphasis : + [[ -> 0 + | "*" -> 1 + | "**" -> 2 + | "***" -> 3 + ]] + ; + bare_proof_instr: + [[ c = cut_step -> c ; + | i = intro_step -> i ]] + ; + proof_instr : + [[ e=emphasis;i=bare_proof_instr;"." -> {emph=e;instr=i}]] + ; +END;; + + diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml new file mode 100644 index 00000000..7ba0d4ff --- /dev/null +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -0,0 +1,188 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Pp +open Decl_expr +open Names +open Nameops + +let pr_constr = Printer.pr_constr_env +let pr_tac = Pptactic.pr_glob_tactic +let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr + +let pr_label = function + Anonymous -> mt () + | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () + +let pr_justification_items env = function + Some [] -> mt () + | Some (_::_ as l) -> + spc () ++ str "by" ++ spc () ++ + prlist_with_sep (fun () -> str ",") (pr_constr env) l + | None -> spc () ++ str "by *" + +let pr_justification_method env = function + None -> mt () + | Some tac -> + spc () ++ str "using" ++ spc () ++ pr_tac env tac + +let pr_statement pr_it env st = + pr_label st.st_label ++ pr_it env st.st_it + +let pr_or_thesis pr_this env = function + Thesis Plain -> str "thesis" + | Thesis (For id) -> + str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id + | This c -> pr_this env c + +let pr_cut pr_it env c = + hov 1 (pr_it env c.cut_stat) ++ + pr_justification_items env c.cut_by ++ + pr_justification_method env c.cut_using + +let type_or_thesis = function + Thesis _ -> Term.mkProp + | This c -> c + +let _I x = x + +let rec print_hyps pconstr gtyp env sep _be _have hyps = + let pr_sep = if sep then str "and" ++ spc () else mt () in + match hyps with + (Hvar _ ::_) as rest -> + spc () ++ pr_sep ++ str _have ++ + print_vars pconstr gtyp env false _be _have rest + | Hprop st :: rest -> + begin + let nenv = + match st.st_label with + Anonymous -> env + | Name id -> Environ.push_named (id,None,gtyp st.st_it) env in + spc() ++ pr_sep ++ pr_statement pconstr env st ++ + print_hyps pconstr gtyp nenv true _be _have rest + end + | [] -> mt () + +and print_vars pconstr gtyp env sep _be _have vars = + match vars with + Hvar st :: rest -> + begin + let nenv = + match st.st_label with + Anonymous -> anomaly "anonymous variable" + | Name id -> Environ.push_named (id,None,st.st_it) env in + let pr_sep = if sep then pr_comma () else mt () in + spc() ++ pr_sep ++ + pr_statement pr_constr env st ++ + print_vars pconstr gtyp nenv true _be _have rest + end + | (Hprop _ :: _) as rest -> + let _st = if _be then + str "be such that" + else + str "such that" in + spc() ++ _st ++ print_hyps pconstr gtyp env false _be _have rest + | [] -> mt () + +let pr_suffices_clause env (hyps,c) = + print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++ + str "to show" ++ spc () ++ pr_or_thesis pr_constr env c + +let pr_elim_type = function + ET_Case_analysis -> str "cases" + | ET_Induction -> str "induction" + +let pr_casee env =function + Real c -> str "on" ++ spc () ++ pr_constr env c + | Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut + +let pr_side = function + Lhs -> str "=~" + | Rhs -> str "~=" + +let rec pr_bare_proof_instr _then _thus env = function + | Pescape -> str "escape" + | Pthen i -> pr_bare_proof_instr true _thus env i + | Pthus i -> pr_bare_proof_instr _then true env i + | Phence i -> pr_bare_proof_instr true true env i + | Pcut c -> + begin + match _then,_thus with + false,false -> str "have" ++ spc () ++ + pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + | false,true -> str "thus" ++ spc () ++ + pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + | true,false -> str "then" ++ spc () ++ + pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + | true,true -> str "hence" ++ spc () ++ + pr_cut (pr_statement (pr_or_thesis pr_constr)) env c + end + | Psuffices c -> + str "suffices" ++ pr_cut pr_suffices_clause env c + | Prew (sid,c) -> + (if _thus then str "thus" else str " ") ++ spc () ++ + pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c + | Passume hyps -> + str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps + | Plet hyps -> + str "let" ++ print_vars pr_constr _I env false true "let" hyps + | Pclaim st -> + str "claim" ++ spc () ++ pr_statement pr_constr env st + | Pfocus st -> + str "focus on" ++ spc () ++ pr_statement pr_constr env st + | Pconsider (id,hyps) -> + str "consider" ++ print_vars pr_constr _I env false false "consider" hyps + ++ spc () ++ str "from " ++ pr_constr env id + | Pgiven hyps -> + str "given" ++ print_vars pr_constr _I env false false "given" hyps + | Ptake witl -> + str "take" ++ spc () ++ + prlist_with_sep pr_comma (pr_constr env) witl + | Pdefine (id,args,body) -> + str "define" ++ spc () ++ pr_id id ++ spc () ++ + prlist_with_sep spc + (fun st -> str "(" ++ + pr_statement pr_constr env st ++ str ")") args ++ spc () ++ + str "as" ++ (pr_constr env body) + | Pcast (id,typ) -> + str "reconsider" ++ spc () ++ + pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ + str "as" ++ spc () ++ (pr_constr env typ) + | Psuppose hyps -> + str "suppose" ++ + print_hyps pr_constr _I env false false "we have" hyps + | Pcase (params,pat,hyps) -> + str "suppose it is" ++ spc () ++ pr_pat pat ++ + (if params = [] then mt () else + (spc () ++ str "with" ++ spc () ++ + prlist_with_sep spc + (fun st -> str "(" ++ + pr_statement pr_constr env st ++ str ")") params ++ spc ())) + ++ + (if hyps = [] then mt () else + (spc () ++ str "and" ++ + print_hyps (pr_or_thesis pr_constr) type_or_thesis + env false false "we have" hyps)) + | Pper (et,c) -> + str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ + pr_casee env c + | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et + | _ -> anomaly "unprintable instruction" + +let pr_emph = function + 0 -> str " " + | 1 -> str "* " + | 2 -> str "** " + | 3 -> str "*** " + | _ -> anomaly "unknown emphasis" + +let pr_proof_instr env instr = + pr_emph instr.emph ++ spc () ++ + pr_bare_proof_instr false false env instr.instr + diff --git a/plugins/decl_mode/ppdecl_proof.mli b/plugins/decl_mode/ppdecl_proof.mli new file mode 100644 index 00000000..fd6fb663 --- /dev/null +++ b/plugins/decl_mode/ppdecl_proof.mli @@ -0,0 +1,2 @@ + +val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds |