aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-04-07 11:50:57 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-04-07 11:50:57 +0200
commit3a1df73d60372d1966c69450f80a66ca72cb9b44 (patch)
tree34f2b0419b52861cb83bb42a90728161c7f792b4 /plugins
parentd6175b9980808ff91f1299ca26a9a49a117169ca (diff)
parent63c73f54023f53a790ef57c9afc22111b9b95412 (diff)
Merge branch 'master' into econstr
Diffstat (limited to 'plugins')
-rw-r--r--plugins/decl_mode/decl_expr.mli102
-rw-r--r--plugins/decl_mode/decl_interp.ml471
-rw-r--r--plugins/decl_mode/decl_interp.mli15
-rw-r--r--plugins/decl_mode/decl_mode.ml136
-rw-r--r--plugins/decl_mode/decl_mode.mli79
-rw-r--r--plugins/decl_mode/decl_mode_plugin.mlpack5
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml1575
-rw-r--r--plugins/decl_mode/decl_proof_instr.mli108
-rw-r--r--plugins/decl_mode/g_decl_mode.ml4387
-rw-r--r--plugins/decl_mode/ppdecl_proof.ml218
-rw-r--r--plugins/decl_mode/ppdecl_proof.mli14
-rw-r--r--plugins/firstorder/g_ground.ml418
-rw-r--r--plugins/ltac/extratactics.ml48
-rw-r--r--plugins/ltac/g_auto.ml42
-rw-r--r--plugins/ltac/tacinterp.ml24
15 files changed, 17 insertions, 3145 deletions
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
deleted file mode 100644
index 29ecb94ca..000000000
--- a/plugins/decl_mode/decl_expr.mli
+++ /dev/null
@@ -1,102 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Names
-open Tacexpr
-
-type 'it statement =
- {st_label:Name.t;
- st_it:'it}
-
-type thesis_kind =
- Plain
- | For of Id.t
-
-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 ('var,'constr,'pat,'tac) bare_proof_instr =
- | Pthen of ('var,'constr,'pat,'tac) bare_proof_instr
- | Pthus of ('var,'constr,'pat,'tac) bare_proof_instr
- | Phence of ('var,'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 ((('var,'constr) hyp list * 'constr or_thesis),'constr,'tac) cut
- | Passume of ('var,'constr) hyp list
- | Plet of ('var,'constr) hyp list
- | Pgiven of ('var,'constr) hyp list
- | Pconsider of 'constr*('var,'constr) hyp list
- | Pclaim of 'constr statement
- | Pfocus of 'constr statement
- | Pdefine of Id.t * 'var list * 'constr
- | Pcast of Id.t or_thesis * 'constr
- | Psuppose of ('var,'constr) hyp list
- | Pcase of 'var list*'pat*(('var,'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 ('var,'constr,'pat,'tac) gen_proof_instr=
- {emph: emphasis;
- instr: ('var,'constr,'pat,'tac) bare_proof_instr }
-
-
-type raw_proof_instr =
- ((Id.t * (Constrexpr.constr_expr option)) Loc.located,
- Constrexpr.constr_expr,
- Constrexpr.cases_pattern_expr,
- raw_tactic_expr) gen_proof_instr
-
-type glob_proof_instr =
- ((Id.t * (Tacexpr.glob_constr_and_expr option)) Loc.located,
- Tacexpr.glob_constr_and_expr,
- Constrexpr.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: Constrexpr.cases_pattern_expr}
-
-type proof_instr =
- (Term.constr statement,
- Term.constr,
- proof_pattern,
- Geninterp.Val.t) gen_proof_instr
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
deleted file mode 100644
index a29480a55..000000000
--- a/plugins/decl_mode/decl_interp.ml
+++ /dev/null
@@ -1,471 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Ltac_plugin
-open CErrors
-open Util
-open Names
-open Constrexpr
-open Tacintern
-open Decl_expr
-open Decl_mode
-open Pretyping
-open Glob_term
-open Term
-open Vars
-open Pp
-open Decl_kinds
-open Misctypes
-
-(* INTERN *)
-
-let glob_app (loc,hd,args) = if List.is_empty 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=
- {globs with ltacvars = Id.Set.add id globs.ltacvars}
-
-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 (Some "simple_pattern",str "\"(_ | _)\" is not allowed here"))
- | CPatDelimiters (_,_,p) ->
- add_vars_of_simple_pattern globs p
- | CPatCstr (_,_,pl1,pl2) ->
- List.fold_left add_vars_of_simple_pattern
- (Option.fold_left (List.fold_left add_vars_of_simple_pattern) globs pl1) pl2
- | CPatNotation(_,_,(pl,pll),pl') ->
- List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::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 intern_proof_instr globs instr=
- {emph = instr.emph;
- instr = intern_bare_proof_instr globs instr.instr}
-
-(* INTERP *)
-
-let interp_justification_items env sigma =
- Option.map (List.map (fun c -> fst (*FIXME*)(understand env sigma (fst c))))
-
-let interp_constr check_sort env sigma c =
- if check_sort then
- fst (understand env sigma ~expected_type:IsType (fst c) (* FIXME *))
- else
- fst (understand env sigma (fst c))
-
-let special_whd env =
- let infos=CClosure.create_clos_infos CClosure.all env in
- (fun t -> CClosure.whd_val infos (CClosure.inject t))
-
-let _eq = lazy (Universes.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 (Lazy.force _eq) && Int.equal (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 env sigma c =
- fst (understand env sigma (fst c) ~expected_type:(OfType (EConstr.of_constr typ)))(*FIXME*)
-
-let interp_statement interp_it env sigma st =
- {st_label=st.st_label;
- st_it=interp_it env sigma st.st_it}
-
-let interp_constr_or_thesis check_sort env sigma = function
- Thesis n -> Thesis n
- | This c -> This (interp_constr check_sort env sigma c)
-
-let abstract_one_hyp inject h glob =
- match h with
- Hvar (loc,(id,None)) ->
- GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob)
- | Hvar (loc,(id,Some typ)) ->
- GProd (Loc.ghost,Name id, Explicit, fst typ, glob)
- | Hprop st ->
- GProd (Loc.ghost,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 (Loc.ghost,GProp)
-
-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 env sigma hyps head =
- let constr= fst(*FIXME*) (understand env sigma (glob_constr_of_hyps inject hyps head)) in
- match_hyps blend [] constr hyps
-
-let interp_hyps env sigma hyps = fst (interp_hyps_gen fst (fun x _ -> x) env sigma 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 (Pp.str "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(Loc.ghost,
- Evar_kinds.TomatchTypeParameter(ind,n), Misctypes.IntroAnonymous, None)::q) in
- let args = List.map glob_of_pat lpat in
- glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr,None),
- add_params mind.Declarations.mind_nparams args)
-
-let prod_one_hyp = function
- (loc,(id,None)) ->
- (fun glob ->
- GProd (Loc.ghost,Name id, Explicit,
- GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob))
- | (loc,(id,Some typ)) ->
- (fun glob ->
- GProd (Loc.ghost,Name id, Explicit, fst typ, glob))
-
-let prod_one_id (loc,id) glob =
- GProd (Loc.ghost,Name id, Explicit,
- GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob)
-
-let let_in_one_alias (id,pat) glob =
- GLetIn (Loc.ghost,Name id, glob_of_pat pat, None, 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 =
- Id.Map.fold (fun ids idp map -> (ids,Id.List.assoc idp map)::map) subst map
-
-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 (Pp.str "empty pattern list")
- | [subst,patt] ->
- (patvars,bind_aliases patvars subst patt,patt)
- | _ -> anomaly (Pp.str "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 env c = Detyping.detype false [] env Evd.empty (EConstr.of_constr c)
-
-let interp_cases info env sigma 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 not (Int.equal (List.length params) expected) then
- user_err ~hdr:"suppose it is"
- (str "Wrong number of extra arguments: " ++
- (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++
- str "expected.") in
- let app_ind =
- let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind,None) in
- let rparams = List.map (detype_ground env) pinfo.per_params in
- let rparams_rec =
- List.map
- (fun (loc,(id,_)) ->
- GVar (loc,id)) params in
- let dum_args=
- List.init oib.Declarations.mind_nrealargs
- (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false),Misctypes.IntroAnonymous, None)) in
- glob_app(Loc.ghost,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(Loc.ghost,GProp)
- | Thesis (For rec_occ) ->
- if not (Id.List.mem rec_occ pat_vars) then
- user_err ~hdr:"suppose it is"
- (str "Variable " ++ Nameops.pr_id rec_occ ++
- str " does not occur in pattern.");
- Glob_term.GSort(Loc.ghost,GProp)
- | 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(Loc.ghost,Anonymous,glob_of_pat npatt,Some 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 = fst (understand env sigma term5)(*FIXME*) 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 (Vars.lift (-1) 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 env sigma cut=
- let nenv,nstat = interp_it env sigma cut.cut_stat in
- { cut_using=Option.map (Tacinterp.Value.of_closure (Tacinterp.default_ist ())) cut.cut_using;
- cut_stat=nstat;
- cut_by=interp_justification_items nenv sigma cut.cut_by}
-
-let interp_no_bind interp_it env sigma x =
- env,interp_it env sigma x
-
-let interp_suffices_clause env sigma (hyps,cot)=
- let (locvars,_) as res =
- match cot with
- This (c,_) ->
- let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) env sigma hyps c in
- nhyps,This nc
- | Thesis Plain as th -> interp_hyps env sigma 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 (Context.Named.Declaration.LocalAssum (id,st.st_it)) env0
- | _ -> env in
- let nenv = List.fold_right push_one locvars env in
- nenv,res
-
-let interp_casee env sigma = function
- Real c -> Real (fst (understand env sigma (fst c)))(*FIXME*)
- | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) env sigma cut)
-
-let abstract_one_arg = function
- (loc,(id,None)) ->
- (fun glob ->
- GLambda (Loc.ghost,Name id, Explicit,
- GHole (loc,Evar_kinds.BinderType (Name id),Misctypes.IntroAnonymous,None), glob))
- | (loc,(id,Some typ)) ->
- (fun glob ->
- GLambda (Loc.ghost,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 env sigma args body =
- let constr=fst (*FIXME*) (understand env sigma (glob_constr_of_fun args body)) in
- match_args destLambda [] constr args
-
-let rec interp_bare_proof_instr info env sigma = function
- Pthus i -> Pthus (interp_bare_proof_instr info env sigma i)
- | Pthen i -> Pthen (interp_bare_proof_instr info env sigma i)
- | Phence i -> Phence (interp_bare_proof_instr info env sigma i)
- | Pcut c -> Pcut (interp_cut
- (interp_no_bind (interp_statement
- (interp_constr_or_thesis true)))
- env sigma c)
- | Psuffices c ->
- Psuffices (interp_cut interp_suffices_clause env sigma c)
- | Prew (s,c) -> Prew (s,interp_cut
- (interp_no_bind (interp_statement
- (interp_constr_in_type (get_eq_typ info env))))
- env sigma c)
-
- | Psuppose hyps -> Psuppose (interp_hyps env sigma hyps)
- | Pcase (params,pat,hyps) ->
- let tparams,tpat,thyps = interp_cases info env sigma params pat hyps in
- Pcase (tparams,tpat,thyps)
- | Ptake witl ->
- Ptake (List.map (fun c -> fst (*FIXME*) (understand env sigma (fst c))) witl)
- | Pconsider (c,hyps) -> Pconsider (interp_constr false env sigma c,
- interp_hyps env sigma hyps)
- | Pper (et,c) -> Pper (et,interp_casee env sigma c)
- | Pend bt -> Pend bt
- | Pescape -> Pescape
- | Passume hyps -> Passume (interp_hyps env sigma hyps)
- | Pgiven hyps -> Pgiven (interp_hyps env sigma hyps)
- | Plet hyps -> Plet (interp_hyps env sigma hyps)
- | Pclaim st -> Pclaim (interp_statement (interp_constr true) env sigma st)
- | Pfocus st -> Pfocus (interp_statement (interp_constr true) env sigma st)
- | Pdefine (id,args,body) ->
- let nargs,_,nbody = interp_fun env sigma args body in
- Pdefine (id,nargs,nbody)
- | Pcast (id,typ) ->
- Pcast(id,interp_constr true env sigma typ)
-
-let interp_proof_instr info env sigma instr=
- {emph = instr.emph;
- instr = interp_bare_proof_instr info env sigma instr.instr}
-
-
-
diff --git a/plugins/decl_mode/decl_interp.mli b/plugins/decl_mode/decl_interp.mli
deleted file mode 100644
index 4303ecdb4..000000000
--- a/plugins/decl_mode/decl_interp.mli
+++ /dev/null
@@ -1,15 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Tacintern
-open Decl_expr
-
-
-val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr
-val interp_proof_instr : Decl_mode.pm_info ->
- Environ.env -> Evd.evar_map -> glob_proof_instr -> proof_instr
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
deleted file mode 100644
index 92d408901..000000000
--- a/plugins/decl_mode/decl_mode.ml
+++ /dev/null
@@ -1,136 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \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 CErrors
-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
-
-
-
-
-type split_tree=
- Skip_patt of Id.Set.t * split_tree
- | Split_patt of Id.Set.t * inductive *
- (bool array * (Id.Set.t * split_tree) option) array
- | Close_patt of split_tree
- | End_patt of (Id.t * (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 * Id.t 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
- match Store.get (Goal.V82.extra sigma goal) info with
- | None -> Mode_tactic
- | Some _ -> Mode_proof
-
-let get_current_mode () =
- try
- mode_of_pftreestate (Pfedit.get_pftreestate ())
- with Proof_global.NoCurrentProof -> Mode_none
-
-let check_not_proof_mode str =
- match get_current_mode () with
- | Mode_proof -> error str
- | _ -> ()
-
-let get_info sigma gl=
- match Store.get (Goal.V82.extra sigma gl) info with
- | None -> invalid_arg "get_info"
- | Some pm -> pm
-
-let try_get_info sigma gl =
- Store.get (Goal.V82.extra sigma gl) info
-
-let get_goal_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.done_cond proof_focus
-
-let focus p =
- let inf = get_goal_stack p in
- Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
-
-let unfocus () =
- Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
-
-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_stack pts = Proof.get_at_focus proof_focus pts
-
-let get_last env = match Environ.named_context env with
- | decl :: _ -> Context.Named.Declaration.get_id decl
- | [] -> error "no previous statement to use"
-
-
-let get_end_command pts =
- match get_top_stack pts with
- | [] -> "\"end proof\""
- | Claim::_ -> "\"end claim\""
- | Focus_claim::_-> "\"end focus\""
- | Suppose_case :: Per (et,_,_,_) :: _ | Per (et,_,_,_) :: _ ->
- begin
- match et with
- Decl_expr.ET_Case_analysis ->
- "\"end cases\" or start a new case"
- | Decl_expr.ET_Induction ->
- "\"end induction\" or start a new case"
- end
- | _ -> anomaly (Pp.str"lonely suppose")
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
deleted file mode 100644
index dfeee833c..000000000
--- a/plugins/decl_mode/decl_mode.mli
+++ /dev/null
@@ -1,79 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Names
-open Term
-open Evd
-
-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 Id.Set.t * split_tree
- | Split_patt of Id.Set.t * inductive *
- (bool array * (Id.Set.t * split_tree) option) array
- | Close_patt of split_tree
- | End_patt of (Id.t * (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.Id.t list
- | Suppose_case
- | Claim
- | Focus_claim
-
-type pm_info =
- {pm_stack : stack_info list }
-
-val info : pm_info Store.field
-
-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 -> Id.t
-(** [get_last] raises a [UserError] when it cannot find a previous
- statement in the environment. *)
-
-val get_end_command : Proof.proof -> string
-
-val focus : Proof.proof -> unit
-
-val unfocus : unit -> unit
diff --git a/plugins/decl_mode/decl_mode_plugin.mlpack b/plugins/decl_mode/decl_mode_plugin.mlpack
deleted file mode 100644
index 1b84a0790..000000000
--- a/plugins/decl_mode/decl_mode_plugin.mlpack
+++ /dev/null
@@ -1,5 +0,0 @@
-Decl_mode
-Decl_interp
-Decl_proof_instr
-Ppdecl_proof
-G_decl_mode
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
deleted file mode 100644
index 2ea4538c3..000000000
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ /dev/null
@@ -1,1575 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Ltac_plugin
-open CErrors
-open Util
-open Pp
-open Evd
-
-open Tacmach
-open Tacintern
-open Decl_expr
-open Decl_mode
-open Decl_interp
-open Glob_term
-open Glob_ops
-open Names
-open Nameops
-open Declarations
-open Tactics
-open Tacticals
-open Term
-open Vars
-open Termops
-open Namegen
-open Goptions
-open Misctypes
-open Sigma.Notations
-open Context.Named.Declaration
-
-module RelDecl = Context.Rel.Declaration
-module NamedDecl = Context.Named.Declaration
-
-(* Strictness option *)
-
-let clear ids { it = goal; sigma } =
- let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
- let env = Goal.V82.env sigma goal in
- let sign = Goal.V82.hyps sigma goal in
- let cl = Goal.V82.concl sigma goal in
- let evdref = ref (Evd.clear_metas sigma) in
- let (hyps, concl) =
- try Evarutil.clear_hyps_in_evi env evdref sign cl ids
- with Evarutil.ClearDependencyError (id, _) ->
- user_err (str "Cannot clear " ++ pr_id id)
- in
- let sigma = !evdref in
- let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
- let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
- { it = [gl]; sigma }
-
-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 proofs";
- optkey = ["Strict";"Proofs"];
- optread = get_strictness;
- optwrite = set_strictness }
-
-let tcl_change_info_gen info_gen =
- (fun gls ->
- let it = sig_it gls in
- let concl = pf_concl gls in
- let hyps = Goal.V82.hyps (project gls) it in
- let extra = Goal.V82.extra (project gls) it in
- let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in
- let sigma = Goal.V82.partial_solution sigma it ev in
- { it = [gl] ; sigma= sigma; } )
-
-let tcl_change_info info gls =
- let info_gen s = Store.set s Decl_mode.info info in
- tcl_change_info_gen info_gen gls
-
-let tcl_erase_info gls =
- let info_gen s = Store.remove s Decl_mode.info in
- tcl_change_info_gen info_gen gls
-
-let special_whd gl=
- let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
- (fun t -> CClosure.whd_val infos (CClosure.inject (EConstr.Unsafe.to_constr t)))
-
-let special_nf gl=
- let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
- (fun t -> CClosure.norm_val infos (CClosure.inject t))
-
-let is_good_inductive env ind =
- let mib,oib = Inductive.lookup_mind_specif env ind in
- Int.equal 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= clear_metas (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 = (Id.to_string 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_before (Name id) (EConstr.of_constr t)
-
-(* start a proof *)
-
-
-let start_proof_tac gls=
- let info={pm_stack=[]} in
- tcl_change_info info gls
-
-let go_to_proof_mode () =
- ignore (Pfedit.by (Proofview.V82.tactic start_proof_tac));
- let p = Proof_global.give_me_the_proof () in
- Decl_mode.focus p
-
-(* closing gaps *)
-
-(* spiwack: should use [Proofview.give_up] but that would require
- moving the whole declarative mode into the new proof engine. It
- will eventually have to be done.
-
- As far as I can tell, [daimon_tac] is used after a [thus thesis],
- it will leave uninstantiated variables instead of giving a relevant
- message at [Qed]. *)
-let daimon_tac gls =
- set_daimon_flag ();
- {it=[];sigma=sig_sig gls;}
-
-let daimon_instr env p =
- let (p,(status,_)) =
- Proof.run_tactic env begin
- Proofview.tclINDEPENDENT Proofview.give_up
- end p
- in
- p,status
-
-let do_daimon () =
- let env = Global.env () in
- let status =
- Proof_global.with_current_proof begin fun _ p ->
- daimon_instr env p
- end
- in
- if not status then Feedback.feedback Feedback.AddedAxiom else ()
-
-(* post-instruction focus management *)
-
-let goto_current_focus () =
- Decl_mode.unfocus ()
-
-(* spiwack: used to catch errors indicating lack of "focusing command"
- in the proof tree. In the current implementation, however, entering
- the declarative mode puts a focus first, there should, therefore,
- never be exception raised here. *)
-let goto_current_focus_or_top () =
- goto_current_focus ()
-
-(* return *)
-
-let close_tactic_mode () =
- try do_daimon ();goto_current_focus ()
- with Not_found ->
- error "\"return\" cannot be used outside of Declarative Proof Mode."
-
-let return_from_tactic_mode () =
- close_tactic_mode ()
-
-(* end proof/claim *)
-
-let close_block bt pts =
- if Proof.no_focused_goal pts then
- goto_current_focus ()
- 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, [] ->
- do_daimon ();goto_current_focus ()
- | _, 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 (Pp.str "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 (Pp.str "Weird case occurred ...")
- | Suppose_case :: Per (et,_,_,_) :: _ ->
- goto_current_focus ()
- | _ -> error "Not inside a proof per cases or induction."
- else
- match get_stack pts with
- Per (et,_,_,_) :: _ -> ()
- | Suppose_case :: Per (et,_,_,_) :: _ ->
- do_daimon ();goto_current_focus ()
- | _ -> error "Not inside a proof per cases or induction."
-
-(* Proof instructions *)
-
-(* automation *)
-
-let filter_hyps f gls =
- let filter_aux id =
- let id = NamedDecl.get_id id in
- 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:=Id.Set.add id !keep;
- tclIDTAC gls
- | _ ->
- let id=pf_get_new_id local_hyp_prefix gls in
- keep:=Id.Set.add id !keep;
- let c = EConstr.of_constr c in
- tclTHEN (Proofview.V82.of_tactic (letin_tac None (Names.Name id) c None Locusops.nowhere))
- (Proofview.V82.of_tactic (clear_body [id])) gls in
- tclMAP add_aux items gls
-
-let prepare_goal items gls =
- let tokeep = ref Id.Set.empty in
- let auxres = add_justification_hyps tokeep items gls in
- tclTHENLIST
- [ (fun _ -> auxres);
- filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls
-
-let my_automation_tac = ref
- (Proofview.tclZERO (CErrors.make_anomaly (Pp.str"No automation registered")))
-
-let register_automation_tac tac = my_automation_tac:= tac
-
-let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac)
-
-let warn_insufficient_justification =
- CWarnings.create ~name:"declmode-insufficient-justification" ~category:"declmode"
- (fun () -> strbrk "Insufficient justification.")
-
-let justification tac gls=
- tclORELSE
- (tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)])
- (fun gls ->
- if get_strictness () then
- error "Insufficient justification."
- else
- begin
- warn_insufficient_justification ();
- daimon_tac gls
- end) gls
-
-let default_justification elems gls=
- justification (tclTHEN (prepare_goal elems) (Proofview.V82.of_tactic 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 Int.equal 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 (EConstr.of_constr se.se_type)) in
- match kind_of_term hd with
- Ind (ind,u as indu) when is_good_inductive env ind -> (* MS: FIXME *)
- let mib,oib=
- Inductive.lookup_mind_specif env ind in
- let gentypes=
- Inductive.arities_of_constructors indu (mib,oib) in
- let process i gentyp =
- let constructor = mkConstructU ((ind,succ i),u)
- (* 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,[])
- | decl::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 (RelDecl.get_type decl)))::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 nf_meta sigma c =
- EConstr.Unsafe.to_constr (Reductionops.nf_meta sigma (EConstr.of_constr c))
-
-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 concl = EConstr.Unsafe.to_constr concl 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 (EConstr.of_constr se.se_type) in
- if n <= 0 then
- {se with
- se_evd=meta_assign se.se_meta
- (c,(Conv,TypeNotProcessed (* ?? *))) unifier;
- se_meta_list=replace_in_list
- se.se_meta submetas se.se_meta_list}
- else
- dfs (pred n)
- with e when CErrors.noncritical e ->
- begin
- enstack_subsubgoals env se stack gls;
- dfs n
- end in
- let nse= try dfs skip with Stack.Empty -> raise Not_found in
- nf_list nse.se_evd nse.se_meta_list,nf_meta nse.se_evd (mkMeta 0)
-
-let concl_refiner metas body gls =
- let concl = pf_concl gls in
- let evd = sig_sig gls in
- let env = pf_env gls in
- let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in
- let concl = EConstr.Unsafe.to_constr concl in
- let rec aux env avoid subst = function
- [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
- | (n,typ)::rest ->
- let _A = subst_meta subst typ in
- let x = id_of_name_using_hdchar env evd (EConstr.of_constr _A) Anonymous in
- let _x = fresh_id avoid x gls in
- let nenv = Environ.push_named (LocalAssum (_x,_A)) env in
- let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) (EConstr.of_constr _A)) in
- let nsubst = (n,mkVar _x)::subst in
- if List.is_empty 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 local_occur_var evd _x (EConstr.of_constr _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.is_empty list then
- let proof = EConstr.of_constr proof in
- Proofview.V82.of_tactic (exact_check proof) gls
- else
- let refiner = concl_refiner list proof gls in
- Tacmach.refine (EConstr.of_constr 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 -> EConstr.Unsafe.to_constr (pf_concl gls)
-
-let just_tac _then cut info gls0 =
- let last_item =
- if _then then
- try [mkVar (get_last (pf_env gls0))]
- with UserError _ ->
- error "\"then\" and \"hence\" require at least one previous fact"
- 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 ->
- Proofview.V82.of_tactic automation_tac gls
- | Some tac ->
- Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) 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) (EConstr.of_constr c_stat) [] gls
- else tclIDTAC gls in
- tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat))
- [tclTHEN tcl_erase_info (just_tac _then cut info);
- thus_tac] gls0
-
-
-(* iterated equality *)
-let _eq = lazy (Universes.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 Term.eq_constr f (Lazy.force _eq) && Int.equal (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 UserError _ -> 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 ->
- Proofview.V82.of_tactic automation_tac gls
- | Some tac ->
- Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) 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) (EConstr.of_constr new_eq) [] gls
- else tclIDTAC gls in
- match rew_side with
- Lhs ->
- let new_eq = mkApp(Lazy.force _eq,[|typ;cut.cut_stat.st_it;rhs|]) in
- tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
- [tclTHEN tcl_erase_info
- (tclTHENS (Proofview.V82.of_tactic (transitivity (EConstr.of_constr lhs)))
- [just_tac;Proofview.V82.of_tactic (exact_check (EConstr.mkVar last_id))]);
- thus_tac new_eq] gls0
- | Rhs ->
- let new_eq = mkApp(Lazy.force _eq,[|typ;lhs;cut.cut_stat.st_it|]) in
- tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
- [tclTHEN tcl_erase_info
- (tclTHENS (Proofview.V82.of_tactic (transitivity (EConstr.of_constr rhs)))
- [Proofview.V82.of_tactic (exact_check (EConstr.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) (EConstr.of_constr st.st_it) [] gls
- else tclIDTAC gls in
- let ninfo1 = {pm_stack=
- (if _thus then Focus_claim else Claim)::info.pm_stack} in
- tclTHENS (Proofview.V82.of_tactic (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
- [Proofview.V82.of_tactic (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 ->
- Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr 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 ->
- Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr 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 -> Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr 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 ->
- Proofview.V82.of_tactic (convert_hyp (LocalDef (id, EConstr.of_constr (fst st.st_it), EConstr.of_constr (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 sigma args body =
- match args with
- (Hprop st| Hvar st )::rest ->
- let pprod= lift 1 (build_product sigma rest body) in
- let lbody =
- match st.st_label with
- Anonymous -> pprod
- | Name id -> subst_var 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 (project gls0) 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 (EConstr.of_constr c_head) c_ctx gls in
- tclTHENS (Proofview.V82.of_tactic (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,u as indu) when is_good_inductive env ind ->
- let mib,oib=
- Inductive.lookup_mind_specif env ind in
- let gentypes=
- Inductive.arities_of_constructors indu (mib,oib) in
- let _ = if not (Int.equal (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
- (Proofview.V82.of_tactic (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
- (Proofview.V82.of_tactic (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 (Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,EConstr.of_constr st.st_it))))
- begin
- match st.st_label with
- Anonymous ->
- consider_match may_intro ((id,false)::introduced) rest_ids rest
- | Name hid ->
- tclTHENLIST
- [Proofview.V82.of_tactic (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
- [Proofview.V82.of_tactic (simplest_case (EConstr.mkVar id));
- 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 =
- let c = EConstr.of_constr c in
- match EConstr.kind (project gls) (strip_outer_cast (project gls) c) with
- Var id ->
- consider_match false [] [id] hyps gls
- | _ ->
- let id = pf_get_new_id (Id.of_string "_tmp") gls in
- tclTHEN
- (Proofview.V82.of_tactic (pose_proof (Name 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_unsafe_type_of gls (EConstr.of_constr wit) in
- tclTHEN (thus_tac wit typ []) (take_tac rest) gls
-
-
-(* tactics for define *)
-
-let subst_term sigma c t =
- EConstr.Unsafe.to_constr (subst_term sigma c t)
-
-let rec build_function sigma args body =
- match args with
- st::rest ->
- let pfun= lift 1 (build_function sigma 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 sigma (EConstr.mkVar id) (EConstr.of_constr pfun))
- | [] -> body
-
-let define_tac id args body gls =
- let t = build_function (project gls) args body in
- let t = EConstr.of_constr t in
- Proofview.V82.of_tactic (letin_tac None (Name id) t None Locusops.nowhere) gls
-
-(* tactics for reconsider *)
-
-let cast_tac id_or_thesis typ gls =
- let typ = EConstr.of_constr typ in
- match id_or_thesis with
- | This id ->
- Proofview.V82.of_tactic (id |> pf_get_hyp gls |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls
- | Thesis (For _ ) ->
- error "\"thesis for ...\" is not applicable here."
- | Thesis Plain ->
- Proofview.V82.of_tactic (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 Int.equal 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 Id.Set.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_unsafe_type_of gls (EConstr.of_constr casee) in
- let is_dep = dependent (project gls) (EConstr.of_constr casee) concl in
- let hd,args = decompose_app (special_whd gls ctyp) in
- let (ind,u) =
- try
- destInd hd
- with DestKO ->
- 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_unsafe_type_of gls (EConstr.of_constr c) in
- lambda_create env (project gls) (typ,Termops.subst_term (project gls) (EConstr.of_constr c) body) in
- let pred= List.fold_right abstract_obj
- real_args (lambda_create env (project gls) (ctyp,Termops.subst_term (project gls) (EConstr.of_constr casee) concl)) in
- let ctyp = EConstr.Unsafe.to_constr ctyp in
- let pred = EConstr.Unsafe.to_constr pred 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 (Pp.str "wrong stack state")
-
-let suppose_tac hyps gls0 =
- let info = get_its_info gls0 in
- let thesis = pf_concl gls0 in
- let thesis = EConstr.Unsafe.to_constr thesis in
- let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
- let clause = build_product (project gls0) 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 (Proofview.V82.of_tactic (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 (Id.Set.singleton id,
- tree_of_pats cpl (rest_args::stack))
- | PatCstr (_,(ind,cnum),args,nam) ->
- let nexti i ati =
- if Int.equal i (pred cnum) then
- let nargs =
- List.map_i (fun j a -> (a,ati.(j))) 0 args in
- Some (Id.Set.singleton id,
- tree_of_pats cpl (nargs::rest_args::stack))
- else None
- in init_tree Id.Set.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 (Pp.str "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 (Pp.str "we should pop here")
- end
- | (patt,rp) :: rest_args ->
- match patt with
- PatVar (_,v) ->
- begin
- match tree with
- Skip_patt (ids,t) ->
- Skip_patt (Id.Set.add id ids,
- add_branch cpl (rest_args::stack) t)
- | Split_patt (_,_,_) ->
- map_tree (Id.Set.add id)
- (fun i bri ->
- append_branch cpl 1 (rest_args::stack) bri)
- tree
- | _ -> anomaly (Pp.str "No pop/stop expected here")
- end
- | PatCstr (_,(ind,cnum),args,nam) ->
- match tree with
- Skip_patt (ids,t) ->
- let nexti i ati =
- if Int.equal i (pred cnum) then
- let nargs =
- List.map_i (fun j a -> (a,ati.(j))) 0 args in
- Some (Id.Set.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 (not (eq_ind ind ind0)) then error
- (* this can happen with coercions *)
- "Case pattern belongs to wrong inductive type.";
- let mapi i ati bri =
- if Int.equal 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 (Pp.str "No pop/stop expected here")
-and append_branch ((id,_) as cpl) depth pats = function
- Some (ids,tree) ->
- Some (Id.Set.add id ids,append_tree cpl depth pats tree)
- | None ->
- Some (Id.Set.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 (Id.Set.add id ids,append_tree cpl depth pats t)
- | End_patt _ -> anomaly (Pp.str "Premature end of branch")
- | Split_patt (_,_,_) ->
- map_tree (Id.Set.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 Name.equal 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,u = destInd cind in
- let _ = if not (eq_ind ind per_info.per_ind) then
- user_err ~hdr:"thesis_for"
- ((Printer.pr_constr_env env Evd.empty 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 Term.eq_constr params per_info.per_params) then
- user_err ~hdr:"thesis_for"
- ((Printer.pr_constr_env env Evd.empty 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 (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty (EConstr.of_constr 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 -> EConstr.Unsafe.to_constr (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 (Pp.str "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 (Proofview.V82.of_tactic (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 ('a, 'b) instance_stack =
- ('b * (('a option * constr list) list)) list
-
-let initial_instance_stack ids : (_, _) instance_stack =
- List.map (fun id -> id,[None,[]]) ids
-
-let push_one_arg arg = function
- [] -> anomaly (Pp.str "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 Id.Set.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 (Pp.str "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 typ = EConstr.Unsafe.to_constr typ in
- let rc,hd1=decompose_prod typ in
- let cind,all_args=decompose_app typ in
- let ind,u = destInd cind in assert (eq_ind ind per_info.per_ind);
- let params,args= List.chop per_info.per_nparams all_args in
- assert begin
- try List.for_all2 Term.eq_constr params per_info.per_params with
- Invalid_argument _ -> false end;
- let hd2 = applist (mkVar fix_id,args@[obj]) in
- EConstr.of_constr (compose_lam rc (EConstr.Unsafe.to_constr (Reductionops.whd_beta gls.sigma (EConstr.of_constr hd2))))
-
-let warn_missing_case =
- CWarnings.create ~name:"declmode-missing-case" ~category:"declmode"
- (fun () -> strbrk "missing case")
-
-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 Id.List.assoc id args with
- [None,br_args] ->
- let all_metas =
- List.init (nparams + nhyps) (fun n -> mkMeta (succ n)) in
- let param_metas,hyp_metas = List.chop nparams all_metas in
- tclTHEN
- (tclDO nhrec (Proofview.V82.of_tactic introf))
- (tacnext
- (applist (mkVar id,
- List.append param_metas
- (List.rev_append br_args hyp_metas)))) gls
- | _ -> anomaly (Pp.str "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_unsafe_type_of gls (EConstr.of_constr casee) in
- let hd,all_args = decompose_app (special_whd gls ctyp) in
- let ind', u = destInd hd in
- let _ = assert (eq_ind ind' ind) in (* just in case *)
- let params,real_args = List.chop nparams all_args in
- let abstract_obj c body =
- let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
- lambda_create env (project gls) (typ,Termops.subst_term (project gls) (EConstr.of_constr c) body) in
- let elim_pred = List.fold_right abstract_obj
- real_args (lambda_create env (project gls) (ctyp,Termops.subst_term (project gls) (EConstr.of_constr casee) concl)) in
- let elim_pred = EConstr.Unsafe.to_constr elim_pred in
- let case_info = Inductiveops.make_case_info env ind RegularStyle in
- let gen_arities = Inductive.arities_of_constructors (ind,u) spec in
- let f_ids typ =
- let sign =
- (prod_assum (Term.prod_applist typ params)) in
- let sign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) sign 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 (Int.equal 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 (fun id -> Proofview.V82.of_tactic (intro_mustbe_force id)) args_ids;
- begin
- fun gls1 ->
- let hrecs =
- List.map
- (fun id ->
- hrec_for (out_name fix_name) per_info gls1 id)
- recs in
- Proofview.V82.of_tactic (generalize hrecs) gls1
- end;
- match bro with
- None ->
- warn_missing_case ();
- tacnext (mkMeta 1)
- | Some (sub_ids,tree) ->
- let br_args =
- List.filter
- (fun (id,_) -> Id.Set.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 (EConstr.of_constr case_term))
- (Array.mapi branch_tac br) gls
- | Split_patt (_, _, _) , [] ->
- anomaly ~label:"execute_cases " (Pp.str "Nothing to split")
- | Skip_patt _ , [] ->
- anomaly ~label:"execute_cases " (Pp.str "Nothing to skip")
- | End_patt (_,_) , _ :: _ ->
- anomaly ~label:"execute_cases " (Pp.str "End of branch with garbage left")
-
-let understand_my_constr env sigma c concl =
- let env = env in
- let c = EConstr.of_constr c in
- let rawc = Detyping.detype false [] env Evd.empty c in
- let rec frob = function
- | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,Misctypes.IntroAnonymous,None)
- | rc -> map_glob_constr frob rc
- in
- Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc)
-
-let my_refine c gls =
- let oc = { run = begin fun sigma ->
- let sigma = Sigma.to_evar_map sigma in
- let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
- Sigma.Unsafe.of_pair (c, sigma)
- end } in
- Proofview.V82.of_tactic (Tactics.New.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 (Pp.str "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 (Pp.str "This case should already be trapped") in
- let et = match et1, et2 with
- | ET_Case_analysis, ET_Case_analysis -> et1
- | ET_Induction, ET_Induction -> et1
- | ET_Case_analysis, _ -> error "\"end cases\" expected."
- | ET_Induction, _ -> error "\"end induction\" expected."
- in
- tclTHEN
- tcl_erase_info
- begin
- match et,ek with
- _,EK_unknown ->
- tclSOLVE [Proofview.V82.of_tactic (simplest_elim (EConstr.of_constr pi.per_casee))]
- | ET_Case_analysis,EK_nodep ->
- tclTHEN
- (Proofview.V82.of_tactic (simplest_case (EConstr.of_constr pi.per_casee)))
- (default_justification (List.map mkVar clauses))
- | ET_Induction,EK_nodep ->
- tclTHENLIST
- [Proofview.V82.of_tactic (generalize (List.map EConstr.of_constr (pi.per_args@[pi.per_casee])));
- Proofview.V82.of_tactic (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 (Proofview.V82.of_tactic assumption)])
- (initial_instance_stack clauses) [pi.per_casee] 0 tree
- | ET_Induction,EK_dep tree ->
- let nargs = (List.length pi.per_args) in
- tclTHEN (Proofview.V82.of_tactic (generalize (List.map EConstr.of_constr (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
- [Proofview.V82.of_tactic (fix (Some fix_id) (succ nargs));
- tclDO nargs (Proofview.V82.of_tactic introf);
- Proofview.V82.of_tactic (intro_mustbe_force c_id);
- execute_cases (Name fix_id) pi
- (fun c ->
- tclTHENLIST
- [clear [fix_id];
- my_refine c;
- clear clauses;
- justification (Proofview.V82.of_tactic 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 (Pp.str "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 pfterm = EConstr.Unsafe.to_constr pfterm 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 ()
- with
- Type_errors.TypeError(env,
- Type_errors.IllFormedRecBody(_,_,_,_,_)) ->
- anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint")
- end
- | Pend (B_elim ET_Case_analysis) -> goto_current_focus ()
- | Pend B_proof -> Proof_global.set_proof_mode "Classic"
- | Pend _ -> ()
-
-let do_instr raw_instr pts =
- let has_tactic = preprocess pts raw_instr.instr in
- (* spiwack: hack! [preprocess] assumes that the [pts] is indeed the
- current proof (and, actually so does [do_instr] later one, so
- it's ok to do the same here. Ideally the proof should be properly
- threaded through the commands here, but since the are interleaved
- with actions on the proof mode, which is attached to the global
- proof environment, it is not possible without heavy lifting. *)
- let pts = Proof_global.give_me_the_proof () in
- let pts =
- 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 = Id.Set.empty; genv = env} in
- let glob_instr = intern_proof_instr ist raw_instr in
- let instr =
- interp_proof_instr (get_its_info gl) env sigma glob_instr in
- let (pts',_) = Proof.run_tactic (Global.env())
- (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) pts in
- pts'
- else pts
- in
- Proof_global.simple_with_current_proof (fun _ _ -> pts);
- postprocess pts raw_instr.instr
-
-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
deleted file mode 100644
index ba196ff01..000000000
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ /dev/null
@@ -1,108 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-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: unit Proofview.tactic -> unit
-
-val automation_tac : unit Proofview.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 :
- Name.t ->
- Decl_mode.per_info ->
- (Term.constr -> Proof_type.tactic) ->
- (Id.Set.elt * (Term.constr option * Term.constr list) list) list ->
- Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic
-
-val tree_of_pats :
- Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list ->
- split_tree
-
-val add_branch :
- Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list ->
- split_tree -> split_tree
-
-val append_branch :
- Id.t *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list ->
- (Id.Set.t * Decl_mode.split_tree) option ->
- (Id.Set.t * Decl_mode.split_tree) option
-
-val append_tree :
- Id.t * (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 :
- Id.t * (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 :
- (Id.t *
- (Term.constr option * Term.constr list) list) list ->
- (Id.t *
- (Term.constr option * Term.constr list) list) list
-
-val push_head : Term.constr ->
- Id.Set.t ->
- (Id.t *
- (Term.constr option * Term.constr list) list) list ->
- (Id.t *
- (Term.constr option * Term.constr list) list) list
-
-val push_arg : Term.constr ->
- (Id.t *
- (Term.constr option * Term.constr list) list) list ->
- (Id.t *
- (Term.constr option * Term.constr list) list) list
-
-val hrec_for:
- Id.t ->
- Decl_mode.per_info -> Proof_type.goal Tacmach.sigma ->
- Id.t -> EConstr.constr
-
-val consider_match :
- bool ->
- (Id.Set.elt*bool) list ->
- Id.Set.elt list ->
- (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list ->
- Proof_type.tactic
-
-val init_tree:
- Id.Set.t ->
- inductive ->
- int option * Declarations.wf_paths ->
- (int ->
- (int option * Declarations.recarg Rtree.t) array ->
- (Id.Set.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
deleted file mode 100644
index a71d20f0d..000000000
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ /dev/null
@@ -1,387 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-DECLARE PLUGIN "decl_mode_plugin"
-
-open Ltac_plugin
-open Compat
-open Pp
-open Decl_expr
-open Names
-open Pcoq
-open Vernacexpr
-open Tok (* necessary for camlp4 *)
-
-open Pcoq.Constr
-open Pltac
-open Ppdecl_proof
-
-let pr_goal gs =
- let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
- let env = Goal.V82.env sigma g in
- let concl = Goal.V82.concl sigma g in
- let goal =
- Printer.pr_context_of env sigma ++ cut () ++
- str "============================" ++ cut () ++
- str "thesis :=" ++ cut () ++
- Printer.pr_goal_concl_style_env env sigma concl in
- str " *** Declarative Mode ***" ++ fnl () ++ fnl () ++
- str " " ++ v 0 goal
-
-let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll =
- match gll with
- | [goal] when pr_first ->
- pr_goal { Evd.it = goal ; sigma = sigma }
- | _ ->
- (* spiwack: it's not very nice to have to call proof global
- here, a more robust solution would be to add a hook for
- [Printer.pr_open_subgoals] in proof modes, in order to
- compute the end command. Yet a more robust solution would be
- to have focuses give explanations of their unfocusing
- behaviour. *)
- let p = Proof_global.give_me_the_proof () in
- let close_cmd = Decl_mode.get_end_command p in
- str "Subproof completed, now type " ++ str close_cmd ++ str "."
-
-let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
- Decl_interp.interp_proof_instr
- (Decl_mode.get_info sigma gl)
- (Goal.V82.env sigma gl)
- (sigma)
-
-let vernac_decl_proof () =
- let pf = Proof_global.give_me_the_proof () in
- if Proof.is_done pf then
- CErrors.error "Nothing left to prove here."
- else
- begin
- Decl_proof_instr.go_to_proof_mode () ;
- Proof_global.set_proof_mode "Declarative"
- end
-
-(* spiwack: some bureaucracy is not performed here *)
-let vernac_return () =
- begin
- Decl_proof_instr.return_from_tactic_mode () ;
- Proof_global.set_proof_mode "Declarative"
- end
-
-let vernac_proof_instr instr =
- Decl_proof_instr.proof_instr 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 ? *)
-
-(* Only declared at raw level, because only used in vernac commands. *)
-let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type =
- Genarg.make0 "proof_instr"
-
-(* 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 : vernac_expr Gram.entry =
- Gram.entry_create "vernac:proof_command"
-(* Auxiliary grammar entry. *)
-let proof_instr : raw_proof_instr Gram.entry =
- Pcoq.create_generic_entry Pcoq.utactic "proof_instr" (Genarg.rawwit wit_proof_instr)
-
-let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
- pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
-
-let classify_proof_instr = function
- | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow
- | _ -> Vernac_classifier.classify_as_proofstep
-
-(* 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) ] => [classify_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 (Vernacexpr.SelectNth 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). *)
- Pcoq.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;
- pr_subgoals = pr_subgoals; }
- 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]. *)
- Pcoq.set_command_entry Pcoq.Vernac_.noedit_mode ;
- (* We restore the goal printer to default *)
- Printer.set_printer_pr Printer.default_printer_pr
- end
- }
-
-VERNAC COMMAND EXTEND DeclProof
-[ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ]
-END
-VERNAC COMMAND EXTEND DeclReturn
-[ "return" ] => [ VtProofMode "Declarative", VtNow ] -> [ 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=Constrexpr.CRef (Libnames.Ident (!@loc, i), None)}
- | 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 (Constrexpr.CRef (Libnames.Ident (!@loc, i), None))}
- | 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
deleted file mode 100644
index 92045e775..000000000
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ /dev/null
@@ -1,218 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Ltac_plugin
-open CErrors
-open Pp
-open Decl_expr
-open Names
-open Nameops
-
-let pr_label = function
- Anonymous -> mt ()
- | Name id -> pr_id id ++ spc () ++ str ":" ++ spc ()
-
-let pr_justification_items pr_constr = function
- Some [] -> mt ()
- | Some (_::_ as l) ->
- spc () ++ str "by" ++ spc () ++
- prlist_with_sep (fun () -> str ",") pr_constr l
- | None -> spc () ++ str "by *"
-
-let pr_justification_method pr_tac = function
- None -> mt ()
- | Some tac ->
- spc () ++ str "using" ++ spc () ++ pr_tac tac
-
-let pr_statement pr_constr st =
- pr_label st.st_label ++ pr_constr st.st_it
-
-let pr_or_thesis pr_this = function
- Thesis Plain -> str "thesis"
- | Thesis (For id) ->
- str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id
- | This c -> pr_this c
-
-let pr_cut pr_constr pr_tac pr_it c =
- hov 1 (pr_it c.cut_stat) ++
- pr_justification_items pr_constr c.cut_by ++
- pr_justification_method pr_tac c.cut_using
-
-let type_or_thesis = function
- Thesis _ -> Term.mkProp
- | This c -> c
-
-let _I x = x
-
-let rec pr_hyps pr_var pr_constr gtyp 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 ++
- pr_vars pr_var pr_constr gtyp false _be _have rest
- | Hprop st :: rest ->
- begin
- (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*)
- spc() ++ pr_sep ++ pr_statement pr_constr st ++
- pr_hyps pr_var pr_constr gtyp true _be _have rest
- end
- | [] -> mt ()
-
-and pr_vars pr_var pr_constr gtyp sep _be _have vars =
- match vars with
- Hvar st :: rest ->
- begin
- (* let npr_constr env = pr_constr (Environ.push_named (id,None,gtyp st.st_it) env)*)
- let pr_sep = if sep then pr_comma () else mt () in
- spc() ++ pr_sep ++
- pr_var st ++
- pr_vars pr_var pr_constr gtyp true _be _have rest
- end
- | (Hprop _ :: _) as rest ->
- let _st = if _be then
- str "be such that"
- else
- str "such that" in
- spc() ++ _st ++ pr_hyps pr_var pr_constr gtyp false _be _have rest
- | [] -> mt ()
-
-let pr_suffices_clause pr_var pr_constr (hyps,c) =
- pr_hyps pr_var pr_constr _I false false "to have" hyps ++ spc () ++
- str "to show" ++ spc () ++ pr_or_thesis pr_constr c
-
-let pr_elim_type = function
- ET_Case_analysis -> str "cases"
- | ET_Induction -> str "induction"
-
-let pr_block_type = function
- B_elim et -> pr_elim_type et
- | B_proof -> str "proof"
- | B_claim -> str "claim"
- | B_focus -> str "focus"
-
-let pr_casee pr_constr pr_tac =function
- Real c -> str "on" ++ spc () ++ pr_constr c
- | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) cut
-
-let pr_side = function
- Lhs -> str "=~"
- | Rhs -> str "~="
-
-let rec pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then _thus = function
- | Pescape -> str "escape"
- | Pthen i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true _thus i
- | Pthus i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac _then true i
- | Phence i -> pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac true true i
- | Pcut c ->
- begin
- match _then,_thus with
- false,false -> str "have" ++ spc () ++
- pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
- | false,true -> str "thus" ++ spc () ++
- pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
- | true,false -> str "then" ++ spc () ++
- pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
- | true,true -> str "hence" ++ spc () ++
- pr_cut pr_constr pr_tac (pr_statement (pr_or_thesis pr_constr)) c
- end
- | Psuffices c ->
- str "suffices" ++ pr_cut pr_constr pr_tac (pr_suffices_clause pr_var pr_constr) c
- | Prew (sid,c) ->
- (if _thus then str "thus" else str " ") ++ spc () ++
- pr_side sid ++ spc () ++ pr_cut pr_constr pr_tac (pr_statement pr_constr) c
- | Passume hyps ->
- str "assume" ++ pr_hyps pr_var pr_constr _I false false "we have" hyps
- | Plet hyps ->
- str "let" ++ pr_vars pr_var pr_constr _I false true "let" hyps
- | Pclaim st ->
- str "claim" ++ spc () ++ pr_statement pr_constr st
- | Pfocus st ->
- str "focus on" ++ spc () ++ pr_statement pr_constr st
- | Pconsider (id,hyps) ->
- str "consider" ++ pr_vars pr_var pr_constr _I false false "consider" hyps
- ++ spc () ++ str "from " ++ pr_constr id
- | Pgiven hyps ->
- str "given" ++ pr_vars pr_var pr_constr _I false false "given" hyps
- | Ptake witl ->
- str "take" ++ spc () ++
- prlist_with_sep pr_comma pr_constr witl
- | Pdefine (id,args,body) ->
- str "define" ++ spc () ++ pr_id id ++ spc () ++
- prlist_with_sep spc
- (fun st -> str "(" ++
- pr_var st ++ str ")") args ++ spc () ++
- str "as" ++ (pr_constr body)
- | Pcast (id,typ) ->
- str "reconsider" ++ spc () ++
- pr_or_thesis pr_id id ++ spc () ++
- str "as" ++ spc () ++ (pr_constr typ)
- | Psuppose hyps ->
- str "suppose" ++
- pr_hyps pr_var pr_constr _I 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_var st ++ str ")") params ++ spc ()))
- ++
- (if hyps = [] then mt () else
- (spc () ++ str "and" ++
- pr_hyps pr_var (pr_or_thesis pr_constr) type_or_thesis
- false false "we have" hyps))
- | Pper (et,c) ->
- str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
- pr_casee pr_constr pr_tac c
- | Pend blk -> str "end" ++ spc () ++ pr_block_type blk
-
-let pr_emph = function
- 0 -> str " "
- | 1 -> str "* "
- | 2 -> str "** "
- | 3 -> str "*** "
- | _ -> anomaly (Pp.str "unknown emphasis")
-
-let pr_gen_proof_instr pr_var pr_constr pr_pat pr_tac instr =
- pr_emph instr.emph ++ spc () ++
- pr_bare_proof_instr pr_var pr_constr pr_pat pr_tac false false instr.instr
-
-
-let pr_raw_proof_instr pconstr1 pconstr2 ptac (instr : raw_proof_instr) =
- pr_gen_proof_instr
- (fun (_,(id,otyp)) ->
- match otyp with
- None -> pr_id id
- | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")"
- )
- pconstr2
- Ppconstr.pr_cases_pattern_expr
- (ptac Pptactic.ltop)
- instr
-
-let pr_glob_proof_instr pconstr1 pconstr2 ptac (instr : glob_proof_instr) =
- pr_gen_proof_instr
- (fun (_,(id,otyp)) ->
- match otyp with
- None -> pr_id id
- | Some typ -> str "(" ++ pr_id id ++ str ":" ++ pconstr1 typ ++str ")")
- pconstr2
- Ppconstr.pr_cases_pattern_expr
- (ptac Pptactic.ltop)
- instr
-
-let pr_proof_instr pconstr1 pconstr2 ptac (instr : proof_instr) =
- let pconstr1 c = pconstr1 (EConstr.of_constr c) in
- let pconstr2 c = pconstr2 (EConstr.of_constr c) in
- pr_gen_proof_instr
- (fun st -> pr_statement pconstr1 st)
- pconstr2
- (fun mpat -> Ppconstr.pr_cases_pattern_expr mpat.pat_expr)
- (ptac Pptactic.ltop)
- instr
-
diff --git a/plugins/decl_mode/ppdecl_proof.mli b/plugins/decl_mode/ppdecl_proof.mli
deleted file mode 100644
index 678fc0768..000000000
--- a/plugins/decl_mode/ppdecl_proof.mli
+++ /dev/null
@@ -1,14 +0,0 @@
-
-open Decl_expr
-open Pptactic
-
-val pr_gen_proof_instr :
- ('var -> Pp.std_ppcmds) ->
- ('constr -> Pp.std_ppcmds) ->
- ('pat -> Pp.std_ppcmds) ->
- ('tac -> Pp.std_ppcmds) ->
- ('var,'constr,'pat,'tac) gen_proof_instr -> Pp.std_ppcmds
-
-val pr_raw_proof_instr : raw_proof_instr raw_extra_genarg_printer
-val pr_glob_proof_instr : glob_proof_instr glob_extra_genarg_printer
-val pr_proof_instr : proof_instr extra_genarg_printer
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index e28d6aa62..3c0319319 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -159,21 +159,3 @@ END
open Proofview.Notations
open Cc_plugin
-open Decl_mode_plugin
-
-let default_declarative_automation =
- Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *)
- Tacticals.New.tclORELSE
- (Tacticals.New.tclORELSE (Auto.h_trivial [] None)
- (Cctac.congruence_tac !congruence_depth []))
- (Proofview.V82.tactic (gen_ground_tac true
- (Some (Tacticals.New.tclTHEN
- (snd (default_solver ()))
- (Cctac.congruence_tac !congruence_depth [])))
- [] []))
-
-
-
-let () =
- Decl_proof_instr.register_automation_tac default_declarative_automation
-
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 1ec52718a..38fdfb759 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -38,7 +38,7 @@ let with_delayed_uconstr ist c tac =
let flags = {
Pretyping.use_typeclasses = false;
solve_unification_constraints = true;
- use_hook = Some Pfedit.solve_by_implicit_tactic;
+ use_hook = Pfedit.solve_by_implicit_tactic ();
fail_evar = false;
expand_evars = true
} in
@@ -348,10 +348,10 @@ END
open EConstr
open Vars
-let constr_flags = {
+let constr_flags () = {
Pretyping.use_typeclasses = true;
Pretyping.solve_unification_constraints = true;
- Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
+ Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
Pretyping.fail_evar = false;
Pretyping.expand_evars = true }
@@ -360,7 +360,7 @@ let refine_tac ist simple with_classes c =
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let flags =
- { constr_flags with Pretyping.use_typeclasses = with_classes } in
+ { constr_flags () with Pretyping.use_typeclasses = with_classes } in
let expected_type = Pretyping.OfType concl in
let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
let update = { run = fun sigma ->
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index e9a6e9e04..dfa8331ff 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -46,7 +46,7 @@ let eval_uconstrs ist cs =
let flags = {
Pretyping.use_typeclasses = false;
solve_unification_constraints = true;
- use_hook = Some Pfedit.solve_by_implicit_tactic;
+ use_hook = Pfedit.solve_by_implicit_tactic ();
fail_evar = false;
expand_evars = true
} in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 928646bcb..50f43931e 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -642,32 +642,32 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
Proofview.NonLogical.run (db_constr (curr_debug ist) env evd c);
(evd,c)
-let constr_flags = {
+let constr_flags () = {
use_typeclasses = true;
solve_unification_constraints = true;
- use_hook = Some solve_by_implicit_tactic;
+ use_hook = solve_by_implicit_tactic ();
fail_evar = true;
expand_evars = true }
(* Interprets a constr; expects evars to be solved *)
let interp_constr_gen kind ist env sigma c =
- interp_gen kind ist false constr_flags env sigma c
+ interp_gen kind ist false (constr_flags ()) env sigma c
let interp_constr = interp_constr_gen WithoutTypeConstraint
let interp_type = interp_constr_gen IsType
-let open_constr_use_classes_flags = {
+let open_constr_use_classes_flags () = {
use_typeclasses = true;
solve_unification_constraints = true;
- use_hook = Some solve_by_implicit_tactic;
+ use_hook = solve_by_implicit_tactic ();
fail_evar = false;
expand_evars = true }
-let open_constr_no_classes_flags = {
+let open_constr_no_classes_flags () = {
use_typeclasses = false;
solve_unification_constraints = true;
- use_hook = Some solve_by_implicit_tactic;
+ use_hook = solve_by_implicit_tactic ();
fail_evar = false;
expand_evars = true }
@@ -679,11 +679,11 @@ let pure_open_constr_flags = {
expand_evars = false }
(* Interprets an open constr *)
-let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist =
+let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c =
let flags =
- if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags
- else open_constr_use_classes_flags in
- interp_gen expected_type ist false flags
+ if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags ()
+ else open_constr_use_classes_flags () in
+ interp_gen expected_type ist false flags env sigma c
let interp_pure_open_constr ist =
interp_gen WithoutTypeConstraint ist false pure_open_constr_flags
@@ -1789,7 +1789,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(TacLetTac(na,c,clp,b,eqpat))
(Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*)
(let_pat_tac b (interp_name ist env sigma na)
- ((sigma,sigma'),c) clp eqpat) sigma')
+ (sigma,c) clp eqpat) sigma')
end }
(* Derived basic tactics *)