summaryrefslogtreecommitdiff
path: root/plugins/decl_mode
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/decl_mode')
-rw-r--r--plugins/decl_mode/decl_expr.mli103
-rw-r--r--plugins/decl_mode/decl_interp.ml471
-rw-r--r--plugins/decl_mode/decl_interp.mli16
-rw-r--r--plugins/decl_mode/decl_mode.ml123
-rw-r--r--plugins/decl_mode/decl_mode.mli78
-rw-r--r--plugins/decl_mode/decl_mode_plugin.mllib6
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml1501
-rw-r--r--plugins/decl_mode/decl_proof_instr.mli109
-rw-r--r--plugins/decl_mode/g_decl_mode.ml4408
-rw-r--r--plugins/decl_mode/ppdecl_proof.ml188
-rw-r--r--plugins/decl_mode/ppdecl_proof.mli2
11 files changed, 3005 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..fa6acaeb
--- /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-2010 *)
+(* \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..b3e076c4
--- /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-2010 *)
+(* \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..46fbcec7
--- /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-2010 *)
+(* \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..af6aa4bf
--- /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-2010 *)
+(* \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 _ -> 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..4e636598
--- /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-2010 *)
+(* \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..c1553b35
--- /dev/null
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -0,0 +1,1501 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \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 _ ->
+ 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 _ -> 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 _ ->
+ 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..1205060a
--- /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-2010 *)
+(* \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..27def8cc
--- /dev/null
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -0,0 +1,408 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \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_ltype_env_at_top 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 "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 *)
+ 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..b866efab
--- /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-2010 *)
+(* \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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 07:38:13 +0000