diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_expr.mli | 25 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 212 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_interp.mli | 7 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 51 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_mode.mli | 23 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 450 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.mli | 53 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 100 | ||||
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 12 |
9 files changed, 450 insertions, 483 deletions
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 86b5e95b..7467604a 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -1,22 +1,21 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Names -open Util open Tacexpr type 'it statement = - {st_label:name; + {st_label:Name.t; st_it:'it} type thesis_kind = Plain - | For of identifier + | For of Id.t type 'this or_thesis = This of 'this @@ -60,8 +59,8 @@ type ('hyp,'constr,'pat,'tac) bare_proof_instr = | Pconsider of 'constr*('hyp,'constr) hyp list | Pclaim of 'constr statement | Pfocus of 'constr statement - | Pdefine of identifier * 'hyp list * 'constr - | Pcast of identifier or_thesis * 'constr + | Pdefine of Id.t * 'hyp list * 'constr + | Pcast of Id.t or_thesis * 'constr | Psuppose of ('hyp,'constr) hyp list | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list) | Ptake of 'constr list @@ -77,15 +76,15 @@ type ('hyp,'constr,'pat,'tac) gen_proof_instr= type raw_proof_instr = - ((identifier*(Topconstr.constr_expr option)) located, - Topconstr.constr_expr, - Topconstr.cases_pattern_expr, + ((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 = - ((identifier*(Genarg.glob_constr_and_expr option)) located, - Genarg.glob_constr_and_expr, - Topconstr.cases_pattern_expr, + ((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 = @@ -94,7 +93,7 @@ type proof_pattern = pat_constr: Term.constr; pat_typ: Term.types; pat_pat: Glob_term.cases_pattern; - pat_expr: Topconstr.cases_pattern_expr} + pat_expr: Constrexpr.cases_pattern_expr} type proof_instr = (Term.constr statement, diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 60988dd1..1c56586c 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -1,27 +1,29 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names -open Topconstr -open Tacinterp -open Tacmach +open Constrexpr +open Tacintern open Decl_expr open Decl_mode -open Pretyping.Default +open Pretyping open Glob_term open Term +open Vars open Pp -open Compat +open Decl_kinds +open Misctypes (* INTERN *) -let glob_app (loc,hd,args) = if args =[] then hd else GApp(loc,hd,args) +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)) @@ -41,8 +43,7 @@ let intern_constr_or_thesis globs = function | This c -> This (intern_constr globs c) let add_var id globs= - let l1,l2=globs.ltacvars in - {globs with ltacvars= (id::l1),(id::l2)} + {globs with ltacvars = Id.Set.add id globs.ltacvars} let add_name nam globs= match nam with @@ -56,7 +57,7 @@ let intern_hyp iconstr globs = function Hprop (intern_statement iconstr globs st) let intern_hyps iconstr globs hyps = - snd (list_fold_map (intern_hyp 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 @@ -73,10 +74,10 @@ 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 + 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 + 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= @@ -93,10 +94,11 @@ let rec add_vars_of_simple_pattern globs = function (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) | CPatDelimiters (_,_,p) -> add_vars_of_simple_pattern globs p - | CPatCstr (_,_,pl) | CPatCstrExpl (_,_,pl) -> - List.fold_left add_vars_of_simple_pattern globs pl - | CPatNotation(_,_,(pl,pll)) -> - List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pll)) + | CPatCstr (_,_,pl1,pl2) -> + List.fold_left add_vars_of_simple_pattern + (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 @@ -135,33 +137,33 @@ let rec intern_bare_proof_instr globs = function | Pcast (id,typ) -> Pcast (id,intern_constr globs typ) -let rec intern_proof_instr globs instr= +let intern_proof_instr globs instr= {emph = instr.emph; instr = intern_bare_proof_instr globs instr.instr} (* INTERP *) -let interp_justification_items sigma env = - Option.map (List.map (fun c ->understand sigma env (fst c))) +let interp_justification_items env sigma = + Option.map (List.map (fun c -> fst (*FIXME*)(understand env sigma (fst c)))) -let interp_constr check_sort sigma env c = +let interp_constr check_sort env sigma c = if check_sort then - understand_type sigma env (fst c) + fst (understand env sigma ~expected_type:IsType (fst c) (* FIXME *)) else - understand sigma env (fst c) + fst (understand env sigma (fst c)) let special_whd env = let infos=Closure.create_clos_infos Closure.betadeltaiota env in (fun t -> Closure.whd_val infos (Closure.inject t)) -let _eq = Libnames.constr_of_global (Coqlib.glob_eq) +let _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 _eq && (Array.length args)=3 + 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." @@ -170,30 +172,30 @@ let get_eq_typ info env = let typ = decompose_eq env (get_last env) in typ -let interp_constr_in_type typ sigma env c = - understand sigma env (fst c) ~expected_type:typ +let interp_constr_in_type typ env sigma c = + fst (understand env sigma (fst c) ~expected_type:(OfType typ))(*FIXME*) -let interp_statement interp_it sigma env st = +let interp_statement interp_it env sigma st = {st_label=st.st_label; - st_it=interp_it sigma env st.st_it} + st_it=interp_it env sigma st.st_it} -let interp_constr_or_thesis check_sort sigma env = function +let interp_constr_or_thesis check_sort env sigma = function Thesis n -> Thesis n - | This c -> This (interp_constr check_sort sigma env c) + | 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 (dummy_loc,Name id, Explicit, GHole (loc,Evd.BinderType (Name id)), glob) + GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob) | Hvar (loc,(id,Some typ)) -> - GProd (dummy_loc,Name id, Explicit, fst typ, glob) + GProd (Loc.ghost,Name id, Explicit, fst typ, glob) | Hprop st -> - GProd (dummy_loc,st.st_label, Explicit, inject st.st_it, glob) + 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 (dummy_loc,GProp Null) +let glob_prop = GSort (Loc.ghost,GProp) let rec match_hyps blend names constr = function [] -> [],substl names constr @@ -210,13 +212,13 @@ let rec match_hyps blend names constr = function let rhyps,head = match_hyps blend qnames body q in qhyp::rhyps,head -let interp_hyps_gen inject blend sigma env hyps head = - let constr=understand sigma env (glob_constr_of_hyps inject hyps head) in +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 sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps glob_prop) +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 dummy_prefix= Id.of_string "__" let rec deanonymize ids = function @@ -234,34 +236,34 @@ let rec deanonymize ids = let rec glob_of_pat = function - PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable" + 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(dummy_loc, - Evd.TomatchTypeParameter(ind,n))::q) in + 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(dummy_loc,Libnames.ConstructRef cstr), + 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 (dummy_loc,Name id, Explicit, - GHole (loc,Evd.BinderType (Name id)), 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 (dummy_loc,Name id, Explicit, fst typ, glob)) + GProd (Loc.ghost,Name id, Explicit, fst typ, glob)) let prod_one_id (loc,id) glob = - GProd (dummy_loc,Name id, Explicit, - GHole (loc,Evd.BinderType (Name id)), glob) + 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 (dummy_loc,Name id, glob_of_pat pat, glob) + GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob) let rec bind_primary_aliases map pat = match pat with @@ -275,7 +277,7 @@ let rec bind_primary_aliases map pat = List.fold_left bind_primary_aliases map1 lpat let bind_secondary_aliases map subst = - List.fold_left (fun map (ids,idp) -> (ids,List.assoc idp map)::map) map subst + 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 @@ -285,10 +287,10 @@ let bind_aliases patvars subst patt = let interp_pattern env pat_expr = let patvars,pats = Constrintern.intern_pattern env pat_expr in match pats with - [] -> anomaly "empty pattern list" + [] -> anomaly (Pp.str "empty pattern list") | [subst,patt] -> (patvars,bind_aliases patvars subst patt,patt) - | _ -> anomaly "undetected disjunctive pattern" + | _ -> anomaly (Pp.str "undetected disjunctive pattern") let rec match_args dest names constr = function [] -> [],names,substl names constr @@ -314,9 +316,9 @@ let rec match_aliases names constr = function let args,bnames,body = match_aliases qnames body q in st::args,bnames,body -let detype_ground c = Detyping.detype false [] [] c +let detype_ground env c = Detyping.detype false [] env Evd.empty c -let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = +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 @@ -325,31 +327,31 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let num_params = pinfo.per_nparams in let _ = let expected = mib.Declarations.mind_nparams - num_params in - if List.length params <> expected then + if not (Int.equal (List.length params) expected) then errorlabstrm "suppose it is" (str "Wrong number of extra arguments: " ++ - (if expected = 0 then str "none" else int expected) ++ spc () ++ + (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++ str "expected.") in let app_ind = - let rind = GRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in - let rparams = List.map detype_ground pinfo.per_params in + let 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_tabulate (fun _ -> GHole (dummy_loc,Evd.QuestionMark (Evd.Define false))) - oib.Declarations.mind_nrealargs in - glob_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in + 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(dummy_loc,GProp Null) + Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp) | Thesis (For rec_occ) -> - if not (List.mem rec_occ pat_vars) then + if not (Id.List.mem rec_occ pat_vars) then errorlabstrm "suppose it is" (str "Variable " ++ Nameops.pr_id rec_occ ++ str " does not occur in pattern."); - Glob_term.GSort(dummy_loc,GProp Null) + 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 = @@ -357,13 +359,13 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let npatt= deanonymize rids patt in List.rev (fst !rids),npatt in let term2 = - GLetIn(dummy_loc,Anonymous, - GCast(dummy_loc,glob_of_pat npatt, - CastConv (DEFAULTcast,app_ind)),term1) in + GLetIn(Loc.ghost,Anonymous, + GCast(Loc.ghost,glob_of_pat npatt, + CastConv app_ind),term1) in let term3=List.fold_right let_in_one_alias aliases term2 in let term4=List.fold_right prod_one_id loc_ids term3 in let term5=List.fold_right prod_one_hyp params term4 in - let constr = understand sigma env term5 in + let 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 @@ -380,22 +382,22 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = pat_pat=patt; pat_expr=pat},thyps -let interp_cut interp_it sigma env cut= - let nenv,nstat = interp_it sigma env cut.cut_stat in +let interp_cut interp_it env sigma cut= + let nenv,nstat = interp_it env sigma cut.cut_stat in {cut with cut_stat=nstat; - cut_by=interp_justification_items sigma nenv cut.cut_by} + cut_by=interp_justification_items nenv sigma cut.cut_by} -let interp_no_bind interp_it sigma env x = - env,interp_it sigma env x +let interp_no_bind interp_it env sigma x = + env,interp_it env sigma x -let interp_suffices_clause sigma env (hyps,cot)= +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) sigma env hyps c in + let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) env sigma hyps c in nhyps,This nc - | Thesis Plain as th -> interp_hyps sigma env hyps,th + | 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 @@ -406,66 +408,66 @@ let interp_suffices_clause sigma env (hyps,cot)= let nenv = List.fold_right push_one locvars env in nenv,res -let interp_casee sigma env = function - Real c -> Real (understand sigma env (fst c)) - | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) sigma env cut) +let 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 (dummy_loc,Name id, Explicit, - GHole (loc,Evd.BinderType (Name id)), 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 (dummy_loc,Name id, Explicit, fst typ, 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 sigma env args body = - let constr=understand sigma env (glob_constr_of_fun args body) in +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 (sigma:Evd.evar_map) (env:Environ.env) = function - Pthus i -> Pthus (interp_bare_proof_instr info sigma env i) - | Pthen i -> Pthen (interp_bare_proof_instr info sigma env i) - | Phence i -> Phence (interp_bare_proof_instr info sigma env i) +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))) - sigma env c) + env sigma c) | Psuffices c -> - Psuffices (interp_cut interp_suffices_clause sigma env 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)))) - sigma env c) + env sigma c) - | Psuppose hyps -> Psuppose (interp_hyps sigma env hyps) + | Psuppose hyps -> Psuppose (interp_hyps env sigma hyps) | Pcase (params,pat,hyps) -> - let tparams,tpat,thyps = interp_cases info sigma env params pat hyps in + let tparams,tpat,thyps = interp_cases info env sigma params pat hyps in Pcase (tparams,tpat,thyps) | Ptake witl -> - Ptake (List.map (fun c -> understand sigma env (fst c)) witl) - | Pconsider (c,hyps) -> Pconsider (interp_constr false sigma env c, - interp_hyps sigma env hyps) - | Pper (et,c) -> Pper (et,interp_casee sigma env c) + 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 sigma env hyps) - | Pgiven hyps -> Pgiven (interp_hyps sigma env hyps) - | Plet hyps -> Plet (interp_hyps sigma env hyps) - | Pclaim st -> Pclaim (interp_statement (interp_constr true) sigma env st) - | Pfocus st -> Pfocus (interp_statement (interp_constr true) sigma env st) + | 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 sigma env args body in + let nargs,_,nbody = interp_fun env sigma args body in Pdefine (id,nargs,nbody) | Pcast (id,typ) -> - Pcast(id,interp_constr true sigma env typ) + Pcast(id,interp_constr true env sigma typ) -let rec interp_proof_instr info sigma env instr= +let interp_proof_instr info env sigma instr= {emph = instr.emph; - instr = interp_bare_proof_instr info sigma env instr.instr} + 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 index f7227946..b3d6f82b 100644 --- a/plugins/decl_mode/decl_interp.mli +++ b/plugins/decl_mode/decl_interp.mli @@ -1,16 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Tacinterp +open Tacintern open Decl_expr -open Mod_subst val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr val interp_proof_instr : Decl_mode.pm_info -> - Evd.evar_map -> Environ.env -> glob_proof_instr -> proof_instr + 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 index 55742386..d169dc13 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,9 +9,9 @@ open Names open Term open Evd +open Errors open Util - let daimon_flag = ref false let set_daimon_flag () = daimon_flag:=true @@ -20,15 +20,13 @@ let get_daimon_flag () = !daimon_flag -(* Information associated to goals. *) -open Store.Field type split_tree= - Skip_patt of Idset.t * split_tree - | Split_patt of Idset.t * inductive * - (bool array * (Idset.t * split_tree) option) array + 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 (identifier * (int * int)) + | End_patt of (Id.t * (int * int)) type elim_kind = EK_dep of split_tree @@ -48,7 +46,7 @@ type per_info = per_wf:recpath} type stack_info = - Per of Decl_expr.elim_type * per_info * elim_kind * identifier list + Per of Decl_expr.elim_type * per_info * elim_kind * Id.t list | Suppose_case | Claim | Focus_claim @@ -69,27 +67,27 @@ let mode_of_pftreestate pts = (* spiwack: it used to be "top_goal_..." but this should be fine *) let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in let goal = List.hd goals in - if info.get (Goal.V82.extra sigma goal) = None then - Mode_tactic - else - Mode_proof + match Store.get (Goal.V82.extra sigma goal) info with + | None -> Mode_tactic + | Some _ -> Mode_proof let get_current_mode () = - try + try mode_of_pftreestate (Pfedit.get_pftreestate ()) - with e when Errors.noncritical e -> Mode_none + with Proof_global.NoCurrentProof -> Mode_none let check_not_proof_mode str = - if get_current_mode () = Mode_proof then - error str + match get_current_mode () with + | Mode_proof -> error str + | _ -> () let get_info sigma gl= - match info.get (Goal.V82.extra sigma gl) with + match Store.get (Goal.V82.extra sigma gl) info with | None -> invalid_arg "get_info" | Some pm -> pm let try_get_info sigma gl = - info.get (Goal.V82.extra sigma gl) + Store.get (Goal.V82.extra sigma gl) info let get_stack pts = let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in @@ -102,11 +100,13 @@ let proof_cond = Proof.no_cond proof_focus let focus p = let inf = get_stack p in - Proof.focus proof_cond inf 1 p + Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1) -let unfocus = Proof.unfocus proof_focus +let unfocus () = + Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) -let maximal_unfocus = Proof_global.maximal_unfocus proof_focus +let maximal_unfocus () = + Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus) let get_top_stack pts = try @@ -116,8 +116,7 @@ let get_top_stack pts = let info = get_info sigma gl in info.pm_stack -let get_last env = - try - let (id,_,_) = List.hd (Environ.named_context env) in id - with Invalid_argument _ -> error "no previous statement to use" +let get_last env = match Environ.named_context env with + | (id,_,_)::_ -> id + | [] -> error "no previous statement to use" diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index b36f2333..2864ba18 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,7 +9,6 @@ open Names open Term open Evd -open Tacmach val set_daimon_flag : unit -> unit val clear_daimon_flag : unit -> unit @@ -27,11 +26,11 @@ val get_current_mode : unit -> command_mode val check_not_proof_mode : string -> unit type split_tree= - Skip_patt of Idset.t * split_tree - | Split_patt of Idset.t * inductive * - (bool array * (Idset.t * split_tree) option) array + 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 (identifier * (int * int)) + | End_patt of (Id.t * (int * int)) type elim_kind = EK_dep of split_tree @@ -51,7 +50,7 @@ type per_info = per_wf:recpath} type stack_info = - Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list + Per of Decl_expr.elim_type * per_info * elim_kind * Names.Id.t list | Suppose_case | Claim | Focus_claim @@ -59,7 +58,7 @@ type stack_info = type pm_info = {pm_stack : stack_info list } -val info : pm_info Store.Field.t +val info : pm_info Store.field val get_info : Evd.evar_map -> Proof_type.goal -> pm_info @@ -69,10 +68,12 @@ val get_stack : Proof.proof -> stack_info list val get_top_stack : Proof.proof -> stack_info list -val get_last: Environ.env -> identifier +val get_last: Environ.env -> Id.t +(** [get_last] raises a [UserError] when it cannot find a previous + statement in the environment. *) val focus : Proof.proof -> unit -val unfocus : Proof.proof -> unit +val unfocus : unit -> unit -val maximal_unfocus : Proof.proof -> unit +val maximal_unfocus : unit -> unit diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e69f2bb6..9d25681d 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1,34 +1,34 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Evd -open Refiner -open Proof_type open Tacmach -open Tacinterp +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 Reductionops open Goptions - +open Misctypes (* Strictness option *) @@ -49,20 +49,21 @@ let _ = 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) (sig_it gls) in - let extra = Goal.V82.extra (project gls) (sig_it 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 (sig_it gls) ev in - { it = [gl] ; sigma= sigma } ) - -open Store.Field + let sigma = Goal.V82.partial_solution sigma it ev in + { it = [gl] ; sigma= sigma; } ) -let tcl_change_info info gls = - let info_gen = Decl_mode.info.set info in +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 = tcl_change_info_gen (Decl_mode.info.remove) 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=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in @@ -74,7 +75,7 @@ let special_nf gl= let is_good_inductive env ind = let mib,oib = Inductive.lookup_mind_specif env ind in - oib.mind_nrealargs = 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib)) + 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 @@ -90,7 +91,7 @@ let mk_evd metalist gls = meta_declare meta typ evd in List.fold_right add_one metalist evd0 -let is_tmp id = (string_of_id id).[0] = '_' +let is_tmp id = (Id.to_string id).[0] == '_' let tmp_ids gls = let ctx = pf_hyps gls in @@ -108,7 +109,7 @@ let clean_tmp gls = clean_all (tmp_ids gls) gls let assert_postpone id t = - assert_tac (Name id) t + assert_before (Name id) t (* start a proof *) @@ -118,7 +119,7 @@ let start_proof_tac gls= tcl_change_info info gls let go_to_proof_mode () = - Pfedit.by start_proof_tac; + ignore (Pfedit.by (Proofview.V82.tactic start_proof_tac)); let p = Proof_global.give_me_the_proof () in Decl_mode.focus p @@ -126,50 +127,34 @@ let go_to_proof_mode () = let daimon_tac gls = set_daimon_flag (); - {it=[];sigma=sig_sig gls} - - -(* marking closed blocks *) - -let rec is_focussing_instr = function - Pthus i | Pthen i | Phence i -> is_focussing_instr i - | Pescape | Pper _ | Pclaim _ | Pfocus _ - | Psuppose _ | Pcase (_,_,_) -> true - | _ -> false - -let mark_rule_as_done = function - Decl_proof true -> Decl_proof false - | Decl_proof false -> - anomaly "already marked as done" - | _ -> anomaly "mark_rule_as_done" - + {it=[];sigma=sig_sig gls;} (* post-instruction focus management *) (* spiwack: This used to fail if there was no focusing command above, but I don't think it ever happened. I hope it doesn't mess things up*) -let goto_current_focus pts = - Decl_mode.maximal_unfocus pts +let goto_current_focus () = + Decl_mode.maximal_unfocus () -let goto_current_focus_or_top pts = - goto_current_focus pts +let goto_current_focus_or_top () = + goto_current_focus () (* return *) -let close_tactic_mode pts = - try goto_current_focus pts +let close_tactic_mode () = + try goto_current_focus () with Not_found -> error "\"return\" cannot be used outside of Declarative Proof Mode." let return_from_tactic_mode () = - close_tactic_mode (Proof_global.give_me_the_proof ()) + close_tactic_mode () (* end proof/claim *) let close_block bt pts = if Proof.no_focused_goal pts then - goto_current_focus pts + goto_current_focus () else let stack = if Proof.is_done pts then @@ -179,7 +164,7 @@ let close_block bt pts = in match bt,stack with B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> - (goto_current_focus pts) + (goto_current_focus ()) | _, Claim::_ -> error "\"end claim\" expected." | _, Focus_claim::_ -> @@ -192,7 +177,7 @@ let close_block bt pts = ET_Case_analysis -> error "\"end cases\" expected." | ET_Induction -> error "\"end induction\" expected." end - | _,_ -> anomaly "Lonely suppose on stack." + | _,_ -> anomaly (Pp.str "Lonely suppose on stack.") (* utility for suppose / suppose it is *) @@ -202,15 +187,15 @@ let close_previous_case pts = Proof.is_done pts then match get_top_stack pts with - Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..." + Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...") | Suppose_case :: Per (et,_,_,_) :: _ -> - goto_current_focus (pts) + goto_current_focus () | _ -> error "Not inside a proof per cases or induction." else match get_stack pts with Per (et,_,_,_) :: _ -> () | Suppose_case :: Per (et,_,_,_) :: _ -> - goto_current_focus ((pts)) + goto_current_focus () | _ -> error "Not inside a proof per cases or induction." (* Proof instructions *) @@ -225,38 +210,38 @@ let filter_hyps f gls = tclTRY (clear [id]) in tclMAP filter_aux (pf_hyps gls) gls -let local_hyp_prefix = id_of_string "___" +let local_hyp_prefix = Id.of_string "___" let add_justification_hyps keep items gls = let add_aux c gls= match kind_of_term c with Var id -> - keep:=Idset.add id !keep; + keep:=Id.Set.add id !keep; tclIDTAC gls | _ -> let id=pf_get_new_id local_hyp_prefix gls in - keep:=Idset.add id !keep; - tclTHEN (letin_tac None (Names.Name id) c None Tacexpr.nowhere) - (thin_body [id]) gls in + keep:=Id.Set.add id !keep; + 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 Idset.empty in + 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 -> Idset.mem id keep)] gls + filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls let my_automation_tac = ref - (fun gls -> anomaly "No automation registered") + (Proofview.tclZERO (Errors.make_anomaly (Pp.str"No automation registered"))) let register_automation_tac tac = my_automation_tac:= tac -let automation_tac gls = !my_automation_tac gls +let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac) let justification tac gls= tclORELSE - (tclSOLVE [tclTHEN tac assumption]) + (tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)]) (fun gls -> if get_strictness () then error "Insufficient justification." @@ -267,7 +252,7 @@ let justification tac gls= end) gls let default_justification elems gls= - justification (tclTHEN (prepare_goal elems) automation_tac) gls + justification (tclTHEN (prepare_goal elems) (Proofview.V82.of_tactic automation_tac)) gls (* code for conclusion refining *) @@ -302,21 +287,21 @@ type stackd_elt = let rec replace_in_list m l = function [] -> raise Not_found - | c::q -> if m=fst c then l@q else c::replace_in_list m l q + | 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 se.se_type) in match kind_of_term hd with - Ind ind when is_good_inductive env ind -> + 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 ind (mib,oib) in + Inductive.arities_of_constructors indu (mib,oib) in let process i gentyp = - let constructor = mkConstruct(ind,succ i) + 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 apptype = prod_applist gentyp params in let rc,_ = Reduction.dest_prod env apptype in let rec meta_aux last lenv = function [] -> (last,lenv,[]) @@ -352,7 +337,7 @@ let rec nf_list evd = if meta_defined evd m then nf_list evd others else - (m,nf_meta evd typ)::nf_list evd others + (m,Reductionops.nf_meta evd typ)::nf_list evd others let find_subsubgoal c ctyp skip submetas gls = let env= pf_env gls in @@ -372,7 +357,7 @@ let find_subsubgoal c ctyp skip submetas gls = try let unifier = Unification.w_unify env se.se_evd Reduction.CUMUL - ~flags:Unification.elim_flags ctyp se.se_type in + ~flags:(Unification.elim_flags ()) ctyp se.se_type in if n <= 0 then {se with se_evd=meta_assign se.se_meta @@ -387,23 +372,23 @@ let find_subsubgoal c ctyp skip submetas 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) + nf_list nse.se_evd nse.se_meta_list,Reductionops.nf_meta nse.se_evd (mkMeta 0) let concl_refiner metas body gls = let concl = pf_concl gls in let evd = sig_sig gls in let env = pf_env gls in - let sort = family_of_sort (Typing.sort_of env evd concl) in + let sort = family_of_sort (Typing.sort_of env (ref evd) concl) in let rec aux env avoid subst = function - [] -> anomaly "concl_refiner: cannot happen" + [] -> 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 _A Anonymous in let _x = fresh_id avoid x gls in let nenv = Environ.push_named (_x,None,_A) env in - let asort = family_of_sort (Typing.sort_of nenv evd _A) in + let asort = family_of_sort (Typing.sort_of nenv (ref evd) _A) in let nsubst = (n,mkVar _x)::subst in - if rest = [] then + if List.is_empty rest then asort,_A,mkNamedLambda _x _A (subst_meta nsubst body) else let bsort,_B,nbody = @@ -451,8 +436,8 @@ let thus_tac c ctyp submetas gls = find_subsubgoal c ctyp 0 submetas gls with Not_found -> error "I could not relate this statement to the thesis." in - if list = [] then - exact_check proof gls + if List.is_empty list then + Proofview.V82.of_tactic (exact_check proof) gls else let refiner = concl_refiner list proof gls in Tactics.refine refiner gls @@ -465,12 +450,13 @@ let mk_stat_or_thesis info gls = function error "\"thesis for ...\" is not applicable here." | Thesis Plain -> pf_concl gls -let just_tac _then cut info gls0 = - let last_item = if _then then - let last_id = try get_last (pf_env gls0) with Failure _ -> - error "\"then\" and \"hence\" require at least one previous fact" in - [mkVar last_id] - else [] +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 @@ -479,9 +465,9 @@ let just_tac _then cut info gls0 = let method_tac gls = match cut.cut_using with None -> - automation_tac gls + Proofview.V82.of_tactic automation_tac gls | Some tac -> - (Tacinterp.eval_tactic tac) gls in + Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in justification (tclTHEN items_tac method_tac) gls0 let instr_cut mkstat _thus _then cut gls0 = @@ -489,28 +475,27 @@ let instr_cut mkstat _thus _then cut gls0 = 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 + pf_get_new_id (Id.of_string "_fact") gls0,false | Name id -> id,true in let c_stat = mkstat info gls0 stat.st_it in let thus_tac gls= if _thus then thus_tac (mkVar c_id) c_stat [] gls else tclIDTAC gls in - tclTHENS (assert_postpone c_id c_stat) + 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 = Libnames.constr_of_global (Coqlib.glob_eq) +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 eq_constr f _eq && (Array.length args)=3 + if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3 then (args.(0), args.(1), args.(2)) @@ -520,8 +505,7 @@ let decompose_eq id gls = let instr_rew _thus rew_side cut gls0 = let last_id = try get_last (pf_env gls0) - with e when Errors.noncritical e -> - error "No previous equality." + with UserError _ -> error "No previous equality." in let typ,lhs,rhs = decompose_eq last_id gls0 in let items_tac gls = @@ -531,14 +515,14 @@ let instr_rew _thus rew_side cut gls0 = let method_tac gls = match cut.cut_using with None -> - automation_tac gls + Proofview.V82.of_tactic automation_tac gls | Some tac -> - (Tacinterp.eval_tactic tac) gls in + Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in let just_tac gls = justification (tclTHEN items_tac method_tac) gls in let (c_id,_) = match cut.cut_stat.st_label with Anonymous -> - pf_get_new_id (id_of_string "_eq") gls0,false + pf_get_new_id (Id.of_string "_eq") gls0,false | Name id -> id,true in let thus_tac new_eq gls= if _thus then @@ -546,28 +530,27 @@ let instr_rew _thus rew_side cut gls0 = else tclIDTAC gls in match rew_side with Lhs -> - let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in - tclTHENS (assert_postpone c_id new_eq) + 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 (transitivity lhs) - [just_tac;exact_check (mkVar last_id)]); + (tclTHENS (Proofview.V82.of_tactic (transitivity lhs)) + [just_tac;Proofview.V82.of_tactic (exact_check (mkVar last_id))]); thus_tac new_eq] gls0 | Rhs -> - let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in - tclTHENS (assert_postpone c_id new_eq) + 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 (transitivity rhs) - [exact_check (mkVar last_id);just_tac]); + (tclTHENS (Proofview.V82.of_tactic (transitivity rhs)) + [Proofview.V82.of_tactic (exact_check (mkVar last_id));just_tac]); thus_tac new_eq] gls0 - (* tactics for claim/focus *) let instr_claim _thus st gls0 = let info = get_its_info gls0 in let (id,_) = match st.st_label with - Anonymous -> pf_get_new_id (id_of_string "_claim") gls0,false + Anonymous -> pf_get_new_id (Id.of_string "_claim") gls0,false | Name id -> id,true in let thus_tac gls= if _thus then @@ -575,7 +558,7 @@ let instr_claim _thus st gls0 = else tclIDTAC gls in let ninfo1 = {pm_stack= (if _thus then Focus_claim else Claim)::info.pm_stack} in - tclTHENS (assert_postpone id st.st_it) + tclTHENS (Proofview.V82.of_tactic (assert_postpone id st.st_it)) [thus_tac; tcl_change_info ninfo1] gls0 @@ -584,10 +567,10 @@ let instr_claim _thus st gls0 = let push_intro_tac coerce nam gls = let (hid,_) = match nam with - Anonymous -> pf_get_new_id (id_of_string "_hyp") gls,false + Anonymous -> pf_get_new_id (Id.of_string "_hyp") gls,false | Name id -> id,true in tclTHENLIST - [intro_mustbe_force hid; + [Proofview.V82.of_tactic (intro_mustbe_force hid); coerce hid] gls @@ -597,7 +580,7 @@ let assume_tac hyps gls = tclTHEN (push_intro_tac (fun id -> - convert_hyp (id,None,st.st_it)) st.st_label)) + Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label)) hyps tclIDTAC gls let assume_hyps_or_theses hyps gls = @@ -607,7 +590,7 @@ let assume_hyps_or_theses hyps gls = tclTHEN (push_intro_tac (fun id -> - convert_hyp (id,None,c)) nam) + Proofview.V82.of_tactic (convert_hyp (id,None,c))) nam) | Hprop {st_label=nam;st_it=Thesis (tk)} -> tclTHEN (push_intro_tac @@ -619,7 +602,7 @@ let assume_st hyps gls = (fun st -> tclTHEN (push_intro_tac - (fun id -> convert_hyp (id,None,st.st_it)) st.st_label)) + (fun id -> Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label)) hyps tclIDTAC gls let assume_st_letin hyps gls = @@ -628,7 +611,7 @@ let assume_st_letin hyps gls = tclTHEN (push_intro_tac (fun id -> - convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label)) + Proofview.V82.of_tactic (convert_hyp (id,Some (fst st.st_it),snd st.st_it))) st.st_label)) hyps tclIDTAC gls (* suffices *) @@ -653,12 +636,12 @@ 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 + let ctx,head = build_applist (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 c_id = pf_get_new_id (Id.of_string "_cofact") gls0 in let ctx,hd = cut.cut_stat in let c_stat = build_product ctx (mk_stat_or_thesis info gls0 hd) in let metas = metas_from 1 ctx in @@ -666,7 +649,7 @@ let instr_suffices _then cut gls0 = let c_term = applist (mkVar c_id,List.map mkMeta metas) in let thus_tac gls= thus_tac c_term c_head c_ctx gls in - tclTHENS (assert_postpone c_id c_stat) + tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat)) [tclTHENLIST [ assume_tac ctx; tcl_erase_info; @@ -680,13 +663,13 @@ let conjunction_arity id gls = let hd,params = decompose_app (special_whd gls typ) in let env =pf_env gls in match kind_of_term hd with - Ind ind when is_good_inductive env ind -> + 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 ind (mib,oib) in - let _ = if Array.length gentypes <> 1 then raise Not_found in - let apptype = Term.prod_applist gentypes.(0) params in + Inductive.arities_of_constructors indu (mib,oib) in + let _ = if not (Int.equal (Array.length gentypes) 1) then raise Not_found in + let apptype = prod_applist gentypes.(0) params in let rc,_ = Reduction.dest_prod env apptype in List.length rc | _ -> raise Not_found @@ -695,9 +678,9 @@ 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 + let id = pf_get_new_id (Id.of_string "_tmp") gls in tclTHEN - (intro_mustbe_force id) + (Proofview.V82.of_tactic (intro_mustbe_force id)) (intron_then (pred n) (id::ids) ltac) gls @@ -710,9 +693,9 @@ let rec consider_match may_intro introduced available expected gls = | [],hyps -> if may_intro then begin - let id = pf_get_new_id (id_of_string "_tmp") gls in + let id = pf_get_new_id (Id.of_string "_tmp") gls in tclIFTHENELSE - (intro_mustbe_force id) + (Proofview.V82.of_tactic (intro_mustbe_force id)) (consider_match true [] [id] hyps) (fun _ -> error "Not enough sub-hypotheses to match statements.") @@ -722,14 +705,14 @@ let rec consider_match may_intro introduced available expected gls = error "Not enough sub-hypotheses to match statements." (* should tell which ones *) | id::rest_ids,(Hvar st | Hprop st)::rest -> - tclIFTHENELSE (convert_hyp (id,None,st.st_it)) + tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) begin match st.st_label with Anonymous -> consider_match may_intro ((id,false)::introduced) rest_ids rest | Name hid -> tclTHENLIST - [rename_hyp [id,hid]; + [Proofview.V82.of_tactic (rename_hyp [id,hid]); consider_match may_intro ((hid,true)::introduced) rest_ids rest] end begin @@ -738,7 +721,7 @@ let rec consider_match may_intro introduced available expected gls = try conjunction_arity id gls with Not_found -> error "Matching hypothesis not found." in tclTHENLIST - [general_case_analysis false (mkVar id,NoBindings); + [Proofview.V82.of_tactic (simplest_case (mkVar id)); intron_then nhyps [] (fun l -> consider_match may_intro introduced (List.rev_append l rest_ids) expected)] gls) @@ -750,9 +733,9 @@ let consider_tac c hyps gls = Var id -> consider_match false [] [id] hyps gls | _ -> - let id = pf_get_new_id (id_of_string "_tmp") gls in + let id = pf_get_new_id (Id.of_string "_tmp") gls in tclTHEN - (forward None (Some (dummy_loc, Genarg.IntroIdentifier id)) c) + (Proofview.V82.of_tactic (pose_proof (Name id) c)) (consider_match false [] [id] hyps) gls @@ -783,7 +766,7 @@ let rec build_function args body = let define_tac id args body gls = let t = build_function args body in - letin_tac None (Name id) t None Tacexpr.nowhere gls + Proofview.V82.of_tactic (letin_tac None (Name id) t None Locusops.nowhere) gls (* tactics for reconsider *) @@ -791,11 +774,11 @@ let cast_tac id_or_thesis typ gls = match id_or_thesis with This id -> let (_,body,_) = pf_get_hyp gls id in - convert_hyp (id,body,typ) gls + Proofview.V82.of_tactic (convert_hyp (id,body,typ)) gls | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here." | Thesis Plain -> - convert_concl typ DEFAULTcast gls + Proofview.V82.of_tactic (convert_concl typ DEFAULTcast) gls (* per cases *) @@ -804,7 +787,7 @@ let is_rec_pos (main_ind,wft) = None -> false | Some index -> match fst (Rtree.dest_node wft) with - Mrec (_,i) when i = index -> true + Mrec (_,i) when Int.equal i index -> true | _ -> false let rec constr_trees (main_ind,wft) ind = @@ -841,7 +824,7 @@ let map_tree id_fun mapi = function let start_tree env ind rp = - init_tree Idset.empty ind rp (fun _ _ -> None) + init_tree Id.Set.empty ind rp (fun _ _ -> None) let build_per_info etype casee gls = let concl=pf_concl gls in @@ -849,17 +832,17 @@ let build_per_info etype casee gls = let ctyp=pf_type_of gls casee in let is_dep = dependent casee concl in let hd,args = decompose_app (special_whd gls ctyp) in - let ind = + let (ind,u) = try destInd hd - with e when Errors.noncritical e -> + 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 params,real_args = List.chop nparams args in let abstract_obj c body = let typ=pf_type_of gls c in lambda_create env (typ,subst_term c body) in @@ -889,8 +872,8 @@ let per_tac etype casee gls= {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 + 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 @@ -914,17 +897,17 @@ let register_nodep_subcase id= function | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"." end - | _ -> anomaly "wrong stack state" + | _ -> 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 id = pf_get_new_id (id_of_string "subcase_") gls0 in + let id = pf_get_new_id (Id.of_string "subcase_") gls0 in let clause = build_product hyps thesis in let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in let old_clauses,stack = register_nodep_subcase id info.pm_stack in let ninfo2 = {pm_stack=stack} in - tclTHENS (assert_postpone id clause) + tclTHENS (Proofview.V82.of_tactic (assert_postpone id clause)) [tclTHENLIST [tcl_change_info ninfo1; assume_tac hyps; clear old_clauses]; @@ -949,17 +932,17 @@ let rec tree_of_pats ((id,_) as cpl) pats = | (patt,rp) :: rest_args -> match patt with PatVar (_,v) -> - Skip_patt (Idset.singleton id, + Skip_patt (Id.Set.singleton id, tree_of_pats cpl (rest_args::stack)) | PatCstr (_,(ind,cnum),args,nam) -> let nexti i ati = - if i = pred cnum then + if Int.equal i (pred cnum) then let nargs = - list_map_i (fun j a -> (a,ati.(j))) 0 args in - Some (Idset.singleton id, + 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 Idset.empty ind rp nexti + in init_tree Id.Set.empty ind rp nexti let rec add_branch ((id,_) as cpl) pats tree= match pats with @@ -968,7 +951,7 @@ let rec add_branch ((id,_) as cpl) pats tree= match tree with End_patt cpl0 -> End_patt cpl0 (* this ensures precedence for overlapping patterns *) - | _ -> anomaly "tree is expected to end here" + | _ -> anomaly (Pp.str "tree is expected to end here") end | args::stack -> match args with @@ -977,7 +960,7 @@ let rec add_branch ((id,_) as cpl) pats tree= match tree with Close_patt t -> Close_patt (add_branch cpl stack t) - | _ -> anomaly "we should pop here" + | _ -> anomaly (Pp.str "we should pop here") end | (patt,rp) :: rest_args -> match patt with @@ -985,23 +968,23 @@ let rec add_branch ((id,_) as cpl) pats tree= begin match tree with Skip_patt (ids,t) -> - Skip_patt (Idset.add id ids, + Skip_patt (Id.Set.add id ids, add_branch cpl (rest_args::stack) t) | Split_patt (_,_,_) -> - map_tree (Idset.add id) + map_tree (Id.Set.add id) (fun i bri -> append_branch cpl 1 (rest_args::stack) bri) tree - | _ -> anomaly "No pop/stop expected here" + | _ -> 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 i = pred cnum then + if Int.equal i (pred cnum) then let nargs = - list_map_i (fun j a -> (a,ati.(j))) 0 args in - Some (Idset.add id ids, + 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 @@ -1009,57 +992,57 @@ let rec add_branch ((id,_) as cpl) pats tree= skip_args t ids (Array.length ati)) in init_tree ids ind rp nexti | Split_patt (_,ind0,_) -> - if (ind <> ind0) then error + 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 i = pred cnum then + if Int.equal i (pred cnum) then let nargs = - list_map_i (fun j a -> (a,ati.(j))) 0 args in + List.map_i (fun j a -> (a,ati.(j))) 0 args in append_branch cpl 0 (nargs::rest_args::stack) bri else bri in map_tree_rp rp (fun ids -> ids) mapi tree - | _ -> anomaly "No pop/stop expected here" + | _ -> anomaly (Pp.str "No pop/stop expected here") and append_branch ((id,_) as cpl) depth pats = function Some (ids,tree) -> - Some (Idset.add id ids,append_tree cpl depth pats tree) + Some (Id.Set.add id ids,append_tree cpl depth pats tree) | None -> - Some (Idset.singleton id,tree_of_pats cpl pats) + 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 (Idset.add id ids,append_tree cpl depth pats t) - | End_patt _ -> anomaly "Premature end of branch" + 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 (Idset.add id) + 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 st.st_label = id -> st.st_it + | 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 = destInd cind in - let _ = if ind <> per_info.per_ind then + let ind,u = destInd cind in + let _ = if not (eq_ind ind per_info.per_ind) then errorlabstrm "thesis_for" - ((Printer.pr_constr_env env obj) ++ spc () ++ + ((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 params,args = List.chop per_info.per_nparams all_args in let _ = if not (List.for_all2 eq_constr params per_info.per_params) then errorlabstrm "thesis_for" - ((Printer.pr_constr_env env obj) ++ spc () ++ + ((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 (whd_beta Evd.empty hd2) + compose_prod rc (Reductionops.whd_beta Evd.empty hd2) let rec build_product_dep pat_info per_info args body gls = match args with @@ -1119,18 +1102,18 @@ let rec register_dep_subcase id env per_info pat = function 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 id = pf_get_new_id (Id.of_string "subcase_") gls0 in let et,per_info,ek,old_clauses,rest = match info.pm_stack with Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) - | _ -> anomaly "wrong place for cases" in + | _ -> 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 (assert_postpone id clause) + tclTHENS (Proofview.V82.of_tactic (assert_postpone id clause)) [tclTHENLIST [tcl_change_info ninfo1; assume_st (params@pat_info.pat_vars); @@ -1141,14 +1124,14 @@ let case_tac params pat_info hyps gls0 = (* end cases *) -type instance_stack = - (constr option*(constr list) list) list +type ('a, 'b) instance_stack = + ('b * (('a option * constr list) list)) list -let initial_instance_stack ids = +let initial_instance_stack ids : (_, _) instance_stack = List.map (fun id -> id,[None,[]]) ids let push_one_arg arg = function - [] -> anomaly "impossible" + [] -> anomaly (Pp.str "impossible") | (head,args) :: ctx -> ((head,(arg::args)) :: ctx) @@ -1157,7 +1140,7 @@ let push_arg arg stacks = let push_one_head c ids (id,stack) = - let head = if Idset.mem id ids then Some c else None in + let head = if Id.Set.mem id ids then Some c else None in id,(head,[]) :: stack let push_head c ids stacks = @@ -1166,7 +1149,7 @@ let push_head c ids stacks = let pop_one (id,stack) = let nstack= match stack with - [] -> anomaly "impossible" + [] -> anomaly (Pp.str "impossible") | [c] as l -> l | (Some head,args)::(head0,args0)::ctx -> let arg = applist (head,(List.rev args)) in @@ -1183,13 +1166,13 @@ let hrec_for fix_id per_info gls obj_id = let typ=pf_get_hyp_typ gls obj_id in let rc,hd1=decompose_prod typ in let cind,all_args=decompose_app typ in - let ind = destInd cind in assert (ind=per_info.per_ind); - let params,args= list_chop per_info.per_nparams all_args in + 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 eq_constr params per_info.per_params with Invalid_argument _ -> false end; let hd2 = applist (mkVar fix_id,args@[obj]) in - compose_lam rc (whd_beta gls.sigma hd2) + compose_lam rc (Reductionops.whd_beta gls.sigma hd2) let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = @@ -1202,18 +1185,18 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls | End_patt (id,(nparams,nhyps)),[] -> begin - match List.assoc id args with + match Id.List.assoc id args with [None,br_args] -> let all_metas = - list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in - let param_metas,hyp_metas = list_chop nparams all_metas in + List.init (nparams + nhyps) (fun n -> mkMeta (succ n)) in + let param_metas,hyp_metas = List.chop nparams all_metas in tclTHEN - (tclDO nhrec introf) + (tclDO nhrec (Proofview.V82.of_tactic introf)) (tacnext (applist (mkVar id, List.append param_metas (List.rev_append br_args hyp_metas)))) gls - | _ -> anomaly "wrong stack size" + | _ -> 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 @@ -1222,18 +1205,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let env=pf_env gls in let ctyp=pf_type_of gls casee in let hd,all_args = decompose_app (special_whd gls ctyp) in - let _ = assert (destInd hd = ind) in (* just in case *) - let params,real_args = list_chop nparams all_args in + let 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_type_of gls c in lambda_create env (typ,subst_term c body) in let elim_pred = List.fold_right abstract_obj real_args (lambda_create env (ctyp,subst_term casee concl)) in let case_info = Inductiveops.make_case_info env ind RegularStyle in - let gen_arities = Inductive.arities_of_constructors ind spec in + let gen_arities = Inductive.arities_of_constructors (ind,u) spec in let f_ids typ = let sign = - (prod_assum (Term.prod_applist typ params)) in + (prod_assum (prod_applist typ params)) in find_intro_names sign gls in let constr_args_ids = Array.map f_ids gen_arities in let case_term = @@ -1243,7 +1227,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let args_ids = constr_args_ids.(i) in let rec aux n = function [] -> - assert (n=Array.length recargs); + assert (Int.equal n (Array.length recargs)); next_objs,[],nhrec | id :: q -> let objs,recs,nrec = aux (succ n) q in @@ -1252,7 +1236,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = else (mkVar id::objs),recs,nrec in let objs,recs,nhrec = aux 0 args_ids in tclTHENLIST - [tclMAP intro_mustbe_force args_ids; + [tclMAP (fun id -> Proofview.V82.of_tactic (intro_mustbe_force id)) args_ids; begin fun gls1 -> let hrecs = @@ -1269,7 +1253,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = | Some (sub_ids,tree) -> let br_args = List.filter - (fun (id,_) -> Idset.mem id sub_ids) args in + (fun (id,_) -> Id.Set.mem id sub_ids) args in let construct = applist (mkConstruct(ind,succ i),params) in let p_args = @@ -1280,22 +1264,24 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = (refine case_term) (Array.mapi branch_tac br) gls | Split_patt (_, _, _) , [] -> - anomaly "execute_cases : Nothing to split" + anomaly ~label:"execute_cases " (Pp.str "Nothing to split") | Skip_patt _ , [] -> - anomaly "execute_cases : Nothing to skip" + anomaly ~label:"execute_cases " (Pp.str "Nothing to skip") | End_patt (_,_) , _ :: _ -> - anomaly "execute_cases : End of branch with garbage left" - -let understand_my_constr c gls = - let env = pf_env gls in - let nc = names_of_rel_context env in - let rawc = Detyping.detype false [] nc c in - let rec frob = function GEvar _ -> GHole (dummy_loc,QuestionMark Expand) | rc -> map_glob_constr frob rc in - Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) + 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 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 = understand_my_constr c gls in - Refine.refine oc gls + let oc sigma = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in + Proofview.V82.of_tactic (Tactics.New.refine oc) gls (* end focus/claim *) @@ -1304,43 +1290,41 @@ let end_tac et2 gls = let et1,pi,ek,clauses = match info.pm_stack with Suppose_case::_ -> - anomaly "This case should already be trapped" + 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 "This case should already be trapped" in - let et = - if et1 <> et2 then - match et1 with - ET_Case_analysis -> - error "\"end cases\" expected." - | ET_Induction -> - error "\"end induction\" expected." - else et1 in + 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 [simplest_elim pi.per_casee] + tclSOLVE [Proofview.V82.of_tactic (simplest_elim pi.per_casee)] | ET_Case_analysis,EK_nodep -> tclTHEN - (general_case_analysis false (pi.per_casee,NoBindings)) + (Proofview.V82.of_tactic (simplest_case pi.per_casee)) (default_justification (List.map mkVar clauses)) | ET_Induction,EK_nodep -> tclTHENLIST [generalize (pi.per_args@[pi.per_casee]); - simple_induct (AnonHyp (succ (List.length pi.per_args))); + 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 assumption]) + 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 @@ -1348,20 +1332,20 @@ let end_tac et2 gls = begin fun gls0 -> let fix_id = - pf_get_new_id (id_of_string "_fix") gls0 in + pf_get_new_id (Id.of_string "_fix") gls0 in let c_id = - pf_get_new_id (id_of_string "_main_arg") gls0 in + pf_get_new_id (Id.of_string "_main_arg") gls0 in tclTHENLIST [fix (Some fix_id) (succ nargs); - tclDO nargs introf; - intro_mustbe_force c_id; + 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 assumption]) + justification (Proofview.V82.of_tactic assumption)]) (initial_instance_stack clauses) [mkVar c_id] 0 tree] gls0 end @@ -1409,7 +1393,7 @@ let rec do_proof_instr_gen _thus _then instr = | Psuppose hyps -> suppose_tac hyps | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps | Pend (B_elim et) -> end_tac et - | Pend _ -> anomaly "Not applicable" + | Pend _ -> anomaly (Pp.str "Not applicable") | Pescape -> escape_tac let eval_instr {instr=instr} = @@ -1454,33 +1438,33 @@ let rec postprocess pts instr = in try Inductiveops.control_only_guard env pfterm; - goto_current_focus_or_top pts + goto_current_focus_or_top () with Type_errors.TypeError(env, Type_errors.IllFormedRecBody(_,_,_,_,_)) -> - anomaly "\"end induction\" generated an ill-formed fixpoint" + anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint") end | Pend _ -> - goto_current_focus_or_top (pts) + goto_current_focus_or_top () let do_instr raw_instr pts = let has_tactic = preprocess pts raw_instr.instr in begin if has_tactic then - let { it=gls ; sigma=sigma } = Proof.V82.subgoals pts in - let gl = { it=List.hd gls ; sigma=sigma } in + let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in + let gl = { it=List.hd gls ; sigma=sigma; } in let env= pf_env gl in - let ist = {ltacvars = ([],[]); ltacrecvars = []; - gsigma = sigma; genv = env} in + let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in let glob_instr = intern_proof_instr ist raw_instr in let instr = - interp_proof_instr (get_its_info gl) sigma env glob_instr in - Pfedit.by (tclTHEN (eval_instr instr) clean_tmp) + interp_proof_instr (get_its_info gl) env sigma glob_instr in + ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp))) else () end; postprocess pts raw_instr.instr; (* spiwack: this should restore a compatible semantics with v8.3 where we never stayed focused on 0 goal. *) - Decl_mode.maximal_unfocus pts + Proof_global.set_proof_mode "Declarative" ; + Decl_mode.maximal_unfocus () let proof_instr raw_instr = let p = Proof_global.give_me_the_proof () in diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli index 48986c2d..f86bfea7 100644 --- a/plugins/decl_mode/decl_proof_instr.mli +++ b/plugins/decl_mode/decl_proof_instr.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Refiner open Names open Term open Tacmach @@ -15,9 +14,9 @@ open Decl_mode val go_to_proof_mode: unit -> unit val return_from_tactic_mode: unit -> unit -val register_automation_tac: tactic -> unit +val register_automation_tac: unit Proofview.tactic -> unit -val automation_tac : tactic +val automation_tac : unit Proofview.tactic val concl_refiner: Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr @@ -28,27 +27,27 @@ val proof_instr: Decl_expr.raw_proof_instr -> unit val tcl_change_info : Decl_mode.pm_info -> tactic val execute_cases : - Names.name -> + Name.t -> Decl_mode.per_info -> (Term.constr -> Proof_type.tactic) -> - (Names.Idset.elt * (Term.constr option * Term.constr list) list) list -> + (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 : - identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> + Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> split_tree val add_branch : - identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> + Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> split_tree -> split_tree val append_branch : - identifier *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> - (Names.Idset.t * Decl_mode.split_tree) option -> - (Names.Idset.t * Decl_mode.split_tree) option + 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 : - identifier * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> + 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 -> @@ -58,7 +57,7 @@ val build_dep_clause : Term.types Decl_expr.statement list -> Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types val register_dep_subcase : - Names.identifier * (int * int) -> + Id.t * (int * int) -> Environ.env -> Decl_mode.per_info -> Glob_term.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind @@ -69,41 +68,41 @@ val thesis_for : Term.constr -> val close_previous_case : Proof.proof -> unit val pop_stacks : - (Names.identifier * + (Id.t * (Term.constr option * Term.constr list) list) list -> - (Names.identifier * + (Id.t * (Term.constr option * Term.constr list) list) list val push_head : Term.constr -> - Names.Idset.t -> - (Names.identifier * + Id.Set.t -> + (Id.t * (Term.constr option * Term.constr list) list) list -> - (Names.identifier * + (Id.t * (Term.constr option * Term.constr list) list) list val push_arg : Term.constr -> - (Names.identifier * + (Id.t * (Term.constr option * Term.constr list) list) list -> - (Names.identifier * + (Id.t * (Term.constr option * Term.constr list) list) list val hrec_for: - Names.identifier -> + Id.t -> Decl_mode.per_info -> Proof_type.goal Tacmach.sigma -> - Names.identifier -> Term.constr + Id.t -> Term.constr val consider_match : bool -> - (Names.Idset.elt*bool) list -> - Names.Idset.elt list -> + (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: - Names.Idset.t -> - Names.inductive -> + Id.Set.t -> + inductive -> int option * Declarations.wf_paths -> (int -> (int option * Declarations.recarg Rtree.t) array -> - (Names.Idset.t * Decl_mode.split_tree) option) -> + (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 index 9a1e00ee..03929b3b 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -1,35 +1,33 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) - -(* arnaud: veiller à l'aspect tutorial des commentaires *) +(*i camlp4deps: "grammar/grammar.cma" i*) +open Util +open Compat open Pp -open Tok open Decl_expr open Names -open Term -open Genarg open Pcoq +open Vernacexpr +open Tok (* necessary for camlp4 *) open Pcoq.Constr open Pcoq.Tactic -open Pcoq.Vernac_ let pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in - let env = Goal.V82.unfiltered_env sigma g in + let env = Goal.V82.env sigma g in let preamb,thesis,penv,pc = (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), (str "thesis := " ++ fnl ()), - Printer.pr_context_of env, - Printer.pr_goal_concl_style_env env (Goal.V82.concl sigma g) + Printer.pr_context_of env sigma, + Printer.pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ @@ -37,7 +35,7 @@ let pr_goal gs = str "============================" ++ fnl () ++ thesis ++ str " " ++ pc) ++ fnl () -(* arnaud: rebrancher ça +(* arnaud: rebrancher ça ? let pr_open_subgoals () = let p = Proof_global.give_me_the_proof () in let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in @@ -45,29 +43,27 @@ let pr_open_subgoals () = pr_subgoals close_cmd sigma goals *) -let pr_proof_instr instr = - Util.anomaly "Cannot print a proof_instr" +let pr_raw_proof_instr _ _ _ instr = + Errors.anomaly (Pp.str "Cannot print a proof_instr") (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller dans cette direction Ppdecl_proof.pr_proof_instr (Global.env()) instr *) -let pr_raw_proof_instr instr = - Util.anomaly "Cannot print a raw proof_instr" -let pr_glob_proof_instr instr = - Util.anomaly "Cannot print a non-interpreted proof_instr" +let pr_proof_instr _ _ _ instr = Empty.abort instr +let pr_glob_proof_instr _ _ _ instr = Empty.abort instr let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= Decl_interp.interp_proof_instr (Decl_mode.get_info sigma gl) - (sigma) (Goal.V82.env sigma gl) + (sigma) let vernac_decl_proof () = let pf = Proof_global.give_me_the_proof () in if Proof.is_done pf then - Util.error "Nothing left to prove here." + Errors.error "Nothing left to prove here." else - Proof.transaction pf begin fun () -> + begin Decl_proof_instr.go_to_proof_mode () ; Proof_global.set_proof_mode "Declarative" ; Vernacentries.print_subgoals () @@ -75,24 +71,18 @@ let vernac_decl_proof () = (* spiwack: some bureaucracy is not performed here *) let vernac_return () = - Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + begin Decl_proof_instr.return_from_tactic_mode () ; Proof_global.set_proof_mode "Declarative" ; Vernacentries.print_subgoals () end let vernac_proof_instr instr = - Proof.transaction (Proof_global.give_me_the_proof ()) begin fun () -> + begin Decl_proof_instr.proof_instr instr; Vernacentries.print_subgoals () end -(* We create a new parser entry [proof_mode]. The Declarative proof mode - will replace the normal parser entry for tactics with this one. *) -let proof_mode = Gram.entry_create "vernac:proof_command" -(* Auxiliary grammar entry. *) -let proof_instr = Gram.entry_create "proofmode:instr" - (* Before we can write an new toplevel command (see below) which takes a [proof_instr] as argument, we need to declare how to parse it, print it, globalise it and interprete it. @@ -101,33 +91,28 @@ let proof_instr = Gram.entry_create "proofmode:instr" indirect through the [proof_instr] grammar entry. *) (* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *) -(* [Genarg.create_arg] creates a new embedding into Genarg. *) -let (wit_proof_instr,globwit_proof_instr,rawwit_proof_instr) = - Genarg.create_arg None "proof_instr" -let _ = Tacinterp.add_interp_genarg "proof_instr" - begin - begin fun e x -> (* declares the globalisation function *) - Genarg.in_gen globwit_proof_instr - (Decl_interp.intern_proof_instr e (Genarg.out_gen rawwit_proof_instr x)) - end, - begin fun ist gl x -> (* declares the interpretation function *) - Tacmach.project gl , - Genarg.in_gen wit_proof_instr - (interp_proof_instr ist gl (Genarg.out_gen globwit_proof_instr x)) - end, - begin fun _ x -> x end (* declares the substitution function, irrelevant in our case *) - end +(* Only declared at raw level, because only used in vernac commands. *) +let wit_proof_instr : (raw_proof_instr, Empty.t, Empty.t) Genarg.genarg_type = + Genarg.make0 None "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 "proof_instr" (Genarg.rawwit wit_proof_instr) -let _ = Pptactic.declare_extra_genarg_pprule - (rawwit_proof_instr, pr_raw_proof_instr) - (globwit_proof_instr, pr_glob_proof_instr) - (wit_proof_instr, pr_proof_instr) +let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr + pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr + +let classify_proof_instr _ = VtProofStep false, VtLater (* 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 +VERNAC proof_mode EXTEND ProofInstr CLASSIFIED BY classify_proof_instr [ - proof_instr(instr) ] -> [ vernac_proof_instr instr ] END @@ -140,7 +125,7 @@ GEXTEND Gram GLOBAL: proof_mode ; proof_mode: LAST - [ [ c=G_vernac.subgoal_command -> c (Some 1) ] ] + [ [ c=G_vernac.subgoal_command -> c (Some (Vernacexpr.SelectNth 1)) ] ] ; END @@ -171,12 +156,11 @@ let _ = end } -(* Two new vernacular commands *) VERNAC COMMAND EXTEND DeclProof - [ "proof" ] -> [ vernac_decl_proof () ] +[ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ] END VERNAC COMMAND EXTEND DeclReturn - [ "return" ] -> [ vernac_return () ] +[ "return" ] => [ VtProofMode "Classic", VtNow ] -> [ vernac_return () ] END let none_is_empty = function @@ -192,7 +176,7 @@ GLOBAL: proof_instr; statement : [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c} | i=ident -> {st_label=Anonymous; - st_it=Topconstr.CRef (Libnames.Ident (loc, i))} + st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i), None)} | c=constr -> {st_label=Anonymous;st_it=c} ]]; constr_or_thesis : @@ -205,7 +189,7 @@ GLOBAL: proof_instr; | [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot} | i=ident -> {st_label=Anonymous; - st_it=This (Topconstr.CRef (Libnames.Ident (loc, i)))} + st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i), None))} | c=constr -> {st_label=Anonymous;st_it=This c} ] ]; @@ -273,7 +257,7 @@ GLOBAL: proof_instr; ; (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*) loc_id: - [[ id=ident -> fun x -> (loc,(id,x)) ]]; + [[ id=ident -> fun x -> (!@loc,(id,x)) ]]; hyp: [[ id=loc_id -> id None ; | id=loc_id ; ":" ; c=constr -> id (Some c)]] @@ -405,5 +389,3 @@ GLOBAL: 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 index 102da8cc..27308666 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Errors open Pp open Decl_expr open Names @@ -20,6 +20,8 @@ let pr_label = function Anonymous -> mt () | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () +let pr_constr env c = pr_constr env Evd.empty c + let pr_justification_items env = function Some [] -> mt () | Some (_::_ as l) -> @@ -75,7 +77,7 @@ and print_vars pconstr gtyp env sep _be _have vars = begin let nenv = match st.st_label with - Anonymous -> anomaly "anonymous variable" + Anonymous -> anomaly (Pp.str "anonymous variable") | Name id -> Environ.push_named (id,None,st.st_it) env in let pr_sep = if sep then pr_comma () else mt () in spc() ++ pr_sep ++ @@ -173,14 +175,14 @@ let rec pr_bare_proof_instr _then _thus env = function str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ pr_casee env c | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et - | _ -> anomaly "unprintable instruction" + | _ -> anomaly (Pp.str "unprintable instruction") let pr_emph = function 0 -> str " " | 1 -> str "* " | 2 -> str "** " | 3 -> str "*** " - | _ -> anomaly "unknown emphasis" + | _ -> anomaly (Pp.str "unknown emphasis") let pr_proof_instr env instr = pr_emph instr.emph ++ spc () ++ |