diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 7 | ||||
| -rw-r--r-- | tactics/autorewrite.ml | 6 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 141 | ||||
| -rw-r--r-- | tactics/decl_interp.ml | 472 | ||||
| -rw-r--r-- | tactics/decl_interp.mli | 18 | ||||
| -rw-r--r-- | tactics/decl_proof_instr.ml | 1518 | ||||
| -rw-r--r-- | tactics/decl_proof_instr.mli | 119 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 20 | ||||
| -rw-r--r-- | tactics/eqdecide.ml4 | 1 | ||||
| -rw-r--r-- | tactics/evar_tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/hipattern.ml4 | 1 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 1 | ||||
| -rw-r--r-- | tactics/leminv.ml | 46 | ||||
| -rw-r--r-- | tactics/refine.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 18 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 19 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 7 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 2 |
21 files changed, 115 insertions, 2293 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 06c4fab6e1..d2bb1a06fc 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -280,9 +280,7 @@ let try_head_pattern c = try head_pattern_bound c with BoundPattern -> error "Bound head variable." -let dummy_goal = - {it = make_evar empty_named_context_val mkProp; - sigma = empty} +let dummy_goal = Goal.V82.dummy_goal let make_exact_entry sigma pri (c,cty) = let cty = strip_outer_cast cty in @@ -700,7 +698,8 @@ let print_hint_term cl = ppnl (pr_hint_term cl) (* print all hints that apply to the concl of the current goal *) let print_applicable_hint () = let pts = get_pftreestate () in - let gl = nth_goal_of_pftreestate 1 pts in + let glss = Proof.V82.subgoals pts in + let gl = { Evd.it = List.hd glss.Evd.it; sigma = glss.Evd.sigma } in print_hint_term (pf_concl gl) (* displays the whole hint database db *) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index b0645744b4..a0dea0292e 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -132,16 +132,16 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic = let to_be_cleared = ref false in fun dir cstr tac gl -> let last_hyp_id = - match (Environ.named_context_of_val gl.Evd.it.Evd.evar_hyps) with + match Tacmach.pf_hyps gl with (last_hyp_id,_,_)::_ -> last_hyp_id | _ -> (* even the hypothesis id is missing *) error ("No such hypothesis: " ^ (string_of_id !id) ^".") in let gl' = general_rewrite_in dir all_occurrences ~tac:(tac, conds) false !id cstr false gl in - let gls = (fst gl').Evd.it in + let gls = gl'.Evd.it in match gls with g::_ -> - (match Environ.named_context_of_val g.Evd.evar_hyps with + (match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with (lastid,_,_)::_ -> if last_hyp_id <> lastid then begin diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 4c58edf595..e0e7aae2fe 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -20,7 +20,6 @@ open Termops open Sign open Reduction open Proof_type -open Proof_trees open Declarations open Tacticals open Tacmach @@ -54,17 +53,6 @@ let is_dependent ev evm = else dep || occur_evar ev evi.evar_concl) evm false -let valid goals p res_sigma l = - let evm = - List.fold_left2 - (fun sigma (ev, evi) prf -> - let cstr, obls = Refiner.extract_open_proof !res_sigma prf in - if not (Evd.is_defined sigma ev) then - Evd.define ev cstr sigma - else sigma) - !res_sigma goals l - in raise (Found evm) - let evar_filter evi = let hyps' = evar_filtered_context evi in { evi with @@ -78,7 +66,7 @@ let evars_to_goals p evm = if evi.evar_body = Evar_empty then let evi', goal = p evm ev evi in if goal then - ((ev, evi') :: gls, Evd.add evm' ev evi') + ((ev,Goal.V82.build ev) :: gls, Evd.add evm' ev evi') else (gls, Evd.add evm' ev evi') else (gls, Evd.add evm' ev evi)) evm ([], Evd.empty) @@ -223,29 +211,17 @@ let rec catchable = function | Stdpp.Exc_located (_, e) -> catchable e | e -> Logic.catchable_exception e -let is_dep gl gls = - let evs = Evarutil.evars_of_term gl.evar_concl in - if evs = Intset.empty then false - else - List.fold_left - (fun b gl -> - if b then b - else - let evs' = Evarutil.evars_of_term gl.evar_concl in - intersects evs evs') - false gls - let is_ground gl = Evarutil.is_ground_term (project gl) (pf_concl gl) let nb_empty_evars s = Evd.fold (fun ev evi acc -> if evi.evar_body = Evar_empty then succ acc else acc) s 0 -let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) +let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar evs (Goal.V82.concl evs ev)) -let typeclasses_debug = ref false +let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l) -type validation = evar_map -> proof_tree list -> proof_tree +let typeclasses_debug = ref false let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l) @@ -256,7 +232,7 @@ type 'ans fk = unit -> 'ans type ('a,'ans) sk = 'a -> 'ans fk -> 'ans type 'a tac = { skft : 'ans. ('a,'ans) sk -> 'ans fk -> autogoal sigma -> 'ans } -type auto_result = autogoal list sigma * validation +type auto_result = autogoal list sigma type atac = auto_result tac @@ -281,7 +257,7 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) = else [] let pf_filtered_hyps gls = - evar_filtered_context (sig_it gls) + Goal.V82.filtered_context gls.Evd.sigma (sig_it gls) let make_autogoal_hints only_classes ?(st=full_transparent_state) g = let sign = pf_filtered_hyps g in @@ -292,7 +268,7 @@ let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : ' { skft = fun sk fk {it = gl,hints; sigma=s} -> let res = try Some (tac {it=gl; sigma=s}) with e when catchable e -> None in match res with - | Some (gls,v) -> sk (f gls hints, fun _ -> v) fk + | Some gls -> sk (f gls hints) fk | None -> fk () } let intro_tac : atac = @@ -300,28 +276,33 @@ let intro_tac : atac = (fun {it = gls; sigma = s} info -> let gls' = List.map (fun g' -> - let env = evar_env g' in + let env = Goal.V82.env s g' in + let context = Environ.named_context_of_val (Goal.V82.hyps s g') in let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints) - (true,false,false) info.only_classes None (List.hd (evar_context g')) in + (true,false,false) info.only_classes None (List.hd context) in let ldb = Hint_db.add_list hint info.hints in (g', { info with is_evar = None; hints = ldb; auto_last_tac = str"intro" })) gls in {it = gls'; sigma = s}) let normevars_tac : atac = - lift_tactic tclNORMEVAR - (fun {it = gls; sigma = s} info -> - let gls' = - List.map (fun g' -> - (g', { info with auto_last_tac = str"NORMEVAR" })) gls - in {it = gls'; sigma = s}) + { skft = fun sk fk {it = gl; sigma = s} -> + let gl', sigma' = Goal.V82.nf_evar s (fst gl) in + sk {it = [gl', snd gl]; sigma = sigma'} fk } + + (* lift_tactic tclNORMEVAR *) + (* (fun {it = gls; sigma = s} info -> *) + (* let gls' = *) + (* List.map (fun g' -> *) + (* (g', { info with auto_last_tac = str"NORMEVAR" })) gls *) + (* in {it = gls'; sigma = s}) *) let id_tac : atac = { skft = fun sk fk {it = gl; sigma = s} -> - sk ({it = [gl]; sigma = s}, fun _ pfs -> List.hd pfs) fk } + sk {it = [gl]; sigma = s} fk } (* Ordering of states is lexicographic on the number of remaining goals. *) -let compare (pri, _, _, (res, _)) (pri', _, _, (res', _)) = +let compare (pri, _, _, res) (pri', _, _, res') = let nbgoals s = List.length (sig_it s) + nb_empty_evars (sig_sig s) in @@ -344,11 +325,11 @@ let solve_unif_tac : atac = let hints_tac hints = { skft = fun sk fk {it = gl,info; sigma = s} -> - let possible_resolve ((lgls,v) as res, pri, b, pp) = + let possible_resolve (lgls as res, pri, b, pp) = (pri, pp, b, res) in let tacs = - let concl = gl.evar_concl in + let concl = Goal.V82.concl s gl in let poss = e_possible_resolve hints info.hints concl in let l = let tacgl = {it = gl; sigma = s} in @@ -358,25 +339,26 @@ let hints_tac hints = in if l = [] && !typeclasses_debug then msgnl (pr_depth info.auto_depth ++ str": no match for " ++ - Printer.pr_constr_env (Evd.evar_env gl) concl ++ + Printer.pr_constr_env (Goal.V82.env s gl) concl ++ spc () ++ int (List.length poss) ++ str" possibilities"); List.map possible_resolve l in let tacs = List.sort compare tacs in let rec aux i = function - | (_, pp, b, ({it = gls; sigma = s}, v)) :: tl -> + | (_, pp, b, {it = gls; sigma = s}) :: tl -> if !typeclasses_debug then msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ pp ++ str" on" ++ spc () ++ pr_ev s gl); let fk = (fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *) aux (succ i) tl) in - let sgls = evars_to_goals (fun evm ev evi -> - if Typeclasses.is_resolvable evi && - (not info.only_classes || Typeclasses.is_class_evar evm evi) then - Typeclasses.mark_unresolvable evi, true - else evi, false) s - in + let sgls = None in + (* evars_to_goals (fun evm ev evi -> *) + (* if Typeclasses.is_resolvable evi && *) + (* (not info.only_classes || Typeclasses.is_class_evar evm evi) then *) + (* Typeclasses.mark_unresolvable evi, true *) + (* else evi, false) s *) + (* in *) let nbgls, newgls, s' = let gls' = List.map (fun g -> (None, g)) gls in match sgls with @@ -389,12 +371,12 @@ let hints_tac hints = { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp; is_evar = evar; hints = - if b && g.evar_hyps <> gl.evar_hyps + if b && Goal.V82.hyps s g <> Goal.V82.hyps s gl then make_autogoal_hints info.only_classes ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'} else info.hints } in g, info) 1 newgls in - let glsv = {it = gls'; sigma = s'}, (fun _ pfl -> v (list_firstn nbgls pfl)) in + let glsv = {it = gls'; sigma = s'} in sk glsv fk | [] -> fk () in aux 1 tacs } @@ -423,9 +405,9 @@ let dependent only_classes evd oev concl = in not (Intset.is_empty concl_evars) let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk = - let rec aux s (acc : (autogoal list * validation) list) fk = function + let rec aux s (acc : autogoal list list) fk = function | (gl,info) :: gls -> - second.skft (fun ({it=gls';sigma=s'},v') fk' -> + second.skft (fun {it=gls';sigma=s'} fk' -> let s', needs_backtrack = if gls' = [] then match info.is_evar with @@ -433,30 +415,23 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk let s' = if Evd.is_defined s' ev then s' else - let prf = v' s' [] in - let term, _ = Refiner.extract_open_proof s' prf in - Evd.define ev term s' - in s', dependent info.only_classes s' (Some ev) gl.evar_concl - | None -> s', dependent info.only_classes s' None gl.evar_concl + s' + in s', dependent info.only_classes s' (Some ev) (Goal.V82.concl s' gl) + | None -> + s', dependent info.only_classes s' None (Goal.V82.concl s' gl) else s', true in let fk'' = if not needs_backtrack then (if !typeclasses_debug then msgnl (str"no backtrack on " ++ pr_ev s gl); fk) else fk' - in aux s' ((gls',v')::acc) fk'' gls) + in aux s' (gls'::acc) fk'' gls) fk {it = (gl,info); sigma = s} | [] -> Some (List.rev acc, s, fk) - in fun ({it = gls; sigma = s},v) fk -> + in fun {it = gls; sigma = s} fk -> let rec aux' = function | None -> fk () | Some (res, s', fk') -> - let goals' = List.concat (List.map (fun (gls,v) -> gls) res) in - let v' s' pfs' : proof_tree = - let (newpfs, rest) = List.fold_left (fun (newpfs,pfs') (gls,v) -> - let before, after = list_chop (List.length gls) pfs' in - (v s' before :: newpfs, after)) - ([], pfs') res - in assert(rest = []); v s' (List.rev newpfs) - in sk ({it = goals'; sigma = s'}, v') (fun () -> aux' (fk' ())) + let goals' = List.concat res in + sk {it = goals'; sigma = s'} (fun () -> aux' (fk' ())) in aux' (aux s [] (fun () -> None) gls) let then_tac (first : atac) (second : atac) : atac = @@ -469,7 +444,7 @@ type run_list_res = (auto_result * run_list_res fk) option let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res = (then_list t (fun x fk -> Some (x, fk))) - (gl, fun s pfs -> valid goals p (ref s) pfs) + gl (fun _ -> None) let rec fix (t : 'a tac) : 'a tac = @@ -488,10 +463,8 @@ let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) gs evm' = let get_result r = match r with | None -> None - | Some ((gls, v), fk) -> - try ignore(v (sig_sig gls) []); assert(false) - with Found evm' -> Some (evm', fk) - + | Some (gls, fk) -> Some (gls.sigma,fk) + let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac = match evars_to_goals p evm with | None -> None (* This happens only because there's no evar having p *) @@ -508,8 +481,8 @@ let eauto ?(only_classes=true) ?st hints g = let gl = { it = make_autogoal ~only_classes ?st None g; sigma = project g } in match run_tac (eauto_tac hints) gl with | None -> raise Not_found - | Some ({it = goals; sigma = s}, valid) -> - {it = List.map fst goals; sigma = s}, valid s + | Some {it = goals; sigma = s} -> + {it = List.map fst goals; sigma = s} let real_eauto st hints p evd = let rec aux evd fails = @@ -531,17 +504,15 @@ let resolve_all_evars_once debug (mode, depth) p evd = let db = searchtable_map typeclasses_db in real_eauto (Hint_db.transparent_state db) [db] p evd -exception FoundTerm of constr - let resolve_one_typeclass env ?(sigma=Evd.empty) gl = - let gls = { it = Evd.make_evar (Environ.named_context_val env) gl; sigma = sigma } in + let (gl,t,sigma) = + Goal.V82.mk_goal sigma (Environ.named_context_val env) gl Store.empty in + let gls = { it = gl ; sigma = sigma } in let hints = searchtable_map typeclasses_db in - let gls', v = eauto ~st:(Hint_db.transparent_state hints) [hints] gls in - let term = v [] in + let gls' = eauto ~st:(Hint_db.transparent_state hints) [hints] gls in let evd = sig_sig gls' in - let term = fst (Refiner.extract_open_proof evd term) in - let term = Evarutil.nf_evar evd term in - evd, term + let term = Evarutil.nf_evar evd t in + evd, term let _ = Typeclasses.solve_instanciation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z) diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml deleted file mode 100644 index 2b583af407..0000000000 --- a/tactics/decl_interp.ml +++ /dev/null @@ -1,472 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -open Util -open Names -open Topconstr -open Tacinterp -open Tacmach -open Decl_expr -open Decl_mode -open Pretyping.Default -open Rawterm -open Term -open Pp - -(* INTERN *) - -let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args) - -let intern_justification_items globs = - Option.map (List.map (intern_constr globs)) - -let intern_justification_method globs = - Option.map (intern_tactic globs) - -let intern_statement intern_it globs st = - {st_label=st.st_label; - st_it=intern_it globs st.st_it} - -let intern_no_bind intern_it globs x = - globs,intern_it globs x - -let intern_constr_or_thesis globs = function - Thesis n -> Thesis n - | This c -> This (intern_constr globs c) - -let add_var id globs= - let l1,l2=globs.ltacvars in - {globs with ltacvars= (id::l1),(id::l2)} - -let add_name nam globs= - match nam with - Anonymous -> globs - | Name id -> add_var id globs - -let intern_hyp iconstr globs = function - Hvar (loc,(id,topt)) -> add_var id globs, - Hvar (loc,(id,Option.map (intern_constr globs) topt)) - | Hprop st -> add_name st.st_label globs, - Hprop (intern_statement iconstr globs st) - -let intern_hyps iconstr globs hyps = - snd (list_fold_map (intern_hyp iconstr) globs hyps) - -let intern_cut intern_it globs cut= - let nglobs,nstat=intern_it globs cut.cut_stat in - {cut_stat=nstat; - cut_by=intern_justification_items nglobs cut.cut_by; - cut_using=intern_justification_method nglobs cut.cut_using} - -let intern_casee globs = function - Real c -> Real (intern_constr globs c) - | Virtual cut -> Virtual - (intern_cut (intern_no_bind (intern_statement intern_constr)) globs cut) - -let intern_hyp_list args globs = - let intern_one globs (loc,(id,opttyp)) = - (add_var id globs), - (loc,(id,Option.map (intern_constr globs) opttyp)) in - list_fold_map intern_one globs args - -let intern_suffices_clause globs (hyps,c) = - let nglobs,nhyps = list_fold_map (intern_hyp intern_constr) globs hyps in - nglobs,(nhyps,intern_constr_or_thesis nglobs c) - -let intern_fundecl args body globs= - let nglobs,nargs = intern_hyp_list args globs in - nargs,intern_constr nglobs body - -let rec add_vars_of_simple_pattern globs = function - CPatAlias (loc,p,id) -> - add_vars_of_simple_pattern (add_var id globs) p -(* Stdpp.raise_with_loc loc - (UserError ("simple_pattern",str "\"as\" is not allowed here"))*) - | CPatOr (loc, _)-> - Stdpp.raise_with_loc loc - (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) - | CPatDelimiters (_,_,p) -> - add_vars_of_simple_pattern globs p - | CPatCstr (_,_,pl) -> - List.fold_left add_vars_of_simple_pattern globs pl - | CPatNotation(_,_,(pl,pll)) -> - List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pll)) - | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs - | _ -> globs - -let rec intern_bare_proof_instr globs = function - Pthus i -> Pthus (intern_bare_proof_instr globs i) - | Pthen i -> Pthen (intern_bare_proof_instr globs i) - | Phence i -> Phence (intern_bare_proof_instr globs i) - | Pcut c -> Pcut - (intern_cut - (intern_no_bind (intern_statement intern_constr_or_thesis)) globs c) - | Psuffices c -> - Psuffices (intern_cut intern_suffices_clause globs c) - | Prew (s,c) -> Prew - (s,intern_cut - (intern_no_bind (intern_statement intern_constr)) globs c) - | Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps) - | Pcase (params,pat,hyps) -> - let nglobs,nparams = intern_hyp_list params globs in - let nnglobs= add_vars_of_simple_pattern nglobs pat in - let nhyps = intern_hyps intern_constr_or_thesis nnglobs hyps in - Pcase (nparams,pat,nhyps) - | Ptake witl -> Ptake (List.map (intern_constr globs) witl) - | Pconsider (c,hyps) -> Pconsider (intern_constr globs c, - intern_hyps intern_constr globs hyps) - | Pper (et,c) -> Pper (et,intern_casee globs c) - | Pend bt -> Pend bt - | Pescape -> Pescape - | Passume hyps -> Passume (intern_hyps intern_constr globs hyps) - | Pgiven hyps -> Pgiven (intern_hyps intern_constr globs hyps) - | Plet hyps -> Plet (intern_hyps intern_constr globs hyps) - | Pclaim st -> Pclaim (intern_statement intern_constr globs st) - | Pfocus st -> Pfocus (intern_statement intern_constr globs st) - | Pdefine (id,args,body) -> - let nargs,nbody = intern_fundecl args body globs in - Pdefine (id,nargs,nbody) - | Pcast (id,typ) -> - Pcast (id,intern_constr globs typ) - -let rec intern_proof_instr globs instr= - {emph = instr.emph; - instr = intern_bare_proof_instr globs instr.instr} - -(* INTERP *) - -let interp_justification_items sigma env = - Option.map (List.map (fun c ->understand sigma env (fst c))) - -let interp_constr check_sort sigma env c = - if check_sort then - understand_type sigma env (fst c) - else - understand sigma env (fst c) - -let special_whd env = - let infos=Closure.create_clos_infos Closure.betadeltaiota env in - (fun t -> Closure.whd_val infos (Closure.inject t)) - -let _eq = Libnames.constr_of_global (Coqlib.glob_eq) - -let decompose_eq env id = - let typ = Environ.named_type id env in - let whd = special_whd env typ in - match kind_of_term whd with - App (f,args)-> - if eq_constr f _eq && (Array.length args)=3 - then args.(0) - else error "Previous step is not an equality." - | _ -> error "Previous step is not an equality." - -let get_eq_typ info env = - let typ = decompose_eq env (get_last env) in - typ - -let interp_constr_in_type typ sigma env c = - understand sigma env (fst c) ~expected_type:typ - -let interp_statement interp_it sigma env st = - {st_label=st.st_label; - st_it=interp_it sigma env st.st_it} - -let interp_constr_or_thesis check_sort sigma env = function - Thesis n -> Thesis n - | This c -> This (interp_constr check_sort sigma env c) - -let abstract_one_hyp inject h raw = - match h with - Hvar (loc,(id,None)) -> - RProd (dummy_loc,Name id, Explicit, RHole (loc,Evd.BinderType (Name id)), raw) - | Hvar (loc,(id,Some typ)) -> - RProd (dummy_loc,Name id, Explicit, fst typ, raw) - | Hprop st -> - RProd (dummy_loc,st.st_label, Explicit, inject st.st_it, raw) - -let rawconstr_of_hyps inject hyps head = - List.fold_right (abstract_one_hyp inject) hyps head - -let raw_prop = RSort (dummy_loc,RProp Null) - -let rec match_hyps blend names constr = function - [] -> [],substl names constr - | hyp::q -> - let (name,typ,body)=destProd constr in - let st= {st_label=name;st_it=substl names typ} in - let qnames= - match name with - Anonymous -> mkMeta 0 :: names - | Name id -> mkVar id :: names in - let qhyp = match hyp with - Hprop st' -> Hprop (blend st st') - | Hvar _ -> Hvar st in - let rhyps,head = match_hyps blend qnames body q in - qhyp::rhyps,head - -let interp_hyps_gen inject blend sigma env hyps head = - let constr=understand sigma env (rawconstr_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 raw_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 raw_of_pat = - function - PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable" - | PatVar (loc,Name id) -> - RVar (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) (RHole(dummy_loc, - Evd.TomatchTypeParameter(ind,n))::q) in - let args = List.map raw_of_pat lpat in - raw_app(loc,RRef(dummy_loc,Libnames.ConstructRef cstr), - add_params mind.Declarations.mind_nparams args) - -let prod_one_hyp = function - (loc,(id,None)) -> - (fun raw -> - RProd (dummy_loc,Name id, Explicit, - RHole (loc,Evd.BinderType (Name id)), raw)) - | (loc,(id,Some typ)) -> - (fun raw -> - RProd (dummy_loc,Name id, Explicit, fst typ, raw)) - -let prod_one_id (loc,id) raw = - RProd (dummy_loc,Name id, Explicit, - RHole (loc,Evd.BinderType (Name id)), raw) - -let let_in_one_alias (id,pat) raw = - RLetIn (dummy_loc,Name id, raw_of_pat pat, raw) - -let rec bind_primary_aliases map pat = - match pat with - PatVar (_,_) -> map - | PatCstr(loc,_,lpat,nam) -> - let map1 = - match nam with - Anonymous -> map - | Name id -> (id,pat)::map - in - List.fold_left bind_primary_aliases map1 lpat - -let bind_secondary_aliases map subst = - List.fold_left (fun map (ids,idp) -> (ids,List.assoc idp map)::map) map subst - -let bind_aliases patvars subst patt = - let map = bind_primary_aliases [] patt in - let map1 = bind_secondary_aliases map subst in - List.rev map1 - -let interp_pattern env pat_expr = - let patvars,pats = Constrintern.intern_pattern env pat_expr in - match pats with - [] -> anomaly "empty pattern list" - | [subst,patt] -> - (patvars,bind_aliases patvars subst patt,patt) - | _ -> anomaly "undetected disjunctive pattern" - -let rec match_args dest names constr = function - [] -> [],names,substl names constr - | _::q -> - let (name,typ,body)=dest constr in - let st={st_label=name;st_it=substl names typ} in - let qnames= - match name with - Anonymous -> assert false - | Name id -> mkVar id :: names in - let args,bnames,body = match_args dest qnames body q in - st::args,bnames,body - -let rec match_aliases names constr = function - [] -> [],names,substl names constr - | _::q -> - let (name,c,typ,body)=destLetIn constr in - let st={st_label=name;st_it=(substl names c,substl names typ)} in - let qnames= - match name with - Anonymous -> assert false - | Name id -> mkVar id :: names in - let args,bnames,body = match_aliases qnames body q in - st::args,bnames,body - -let detype_ground c = Detyping.detype false [] [] c - -let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = - let et,pinfo = - match info.pm_stack with - Per(et,pi,_,_)::_ -> et,pi - | _ -> error "No proof per cases/induction/inversion in progress." in - let mib,oib=Global.lookup_inductive pinfo.per_ind in - let num_params = pinfo.per_nparams in - let _ = - let expected = mib.Declarations.mind_nparams - num_params in - if List.length params <> expected then - errorlabstrm "suppose it is" - (str "Wrong number of extra arguments: " ++ - (if expected = 0 then str "none" else int expected) ++ spc () ++ - str "expected.") in - let app_ind = - let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in - let rparams = List.map detype_ground pinfo.per_params in - let rparams_rec = - List.map - (fun (loc,(id,_)) -> - RVar (loc,id)) params in - let dum_args= - list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark (Evd.Define false))) - oib.Declarations.mind_nrealargs in - raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in - let pat_vars,aliases,patt = interp_pattern env pat in - let inject = function - Thesis (Plain) -> Rawterm.RSort(dummy_loc,RProp Null) - | Thesis (For rec_occ) -> - if not (List.mem rec_occ pat_vars) then - errorlabstrm "suppose it is" - (str "Variable " ++ Nameops.pr_id rec_occ ++ - str " does not occur in pattern."); - Rawterm.RSort(dummy_loc,RProp Null) - | This (c,_) -> c in - let term1 = rawconstr_of_hyps inject hyps raw_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 = - RLetIn(dummy_loc,Anonymous, - RCast(dummy_loc,raw_of_pat npatt, - CastConv (DEFAULTcast,app_ind)),term1) in - let term3=List.fold_right let_in_one_alias aliases term2 in - let term4=List.fold_right prod_one_id loc_ids term3 in - let term5=List.fold_right prod_one_hyp params term4 in - let constr = understand sigma env term5 in - let tparams,nam4,rest4 = match_args destProd [] constr params in - let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in - let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in - let (_,pat_pat,pat_typ,rest1) = destLetIn rest2 in - let blend st st' = - match st'.st_it with - Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label} - | This _ -> {st_it = This st.st_it;st_label=st.st_label} in - let thyps = fst (match_hyps blend nam2 (Termops.pop rest1) hyps) in - tparams,{pat_vars=tpatvars; - pat_aliases=taliases; - pat_constr=pat_pat; - pat_typ=pat_typ; - pat_pat=patt; - pat_expr=pat},thyps - -let interp_cut interp_it sigma env cut= - let nenv,nstat = interp_it sigma env cut.cut_stat in - {cut with - cut_stat=nstat; - cut_by=interp_justification_items sigma nenv cut.cut_by} - -let interp_no_bind interp_it sigma env x = - env,interp_it sigma env x - -let interp_suffices_clause sigma env (hyps,cot)= - let (locvars,_) as res = - match cot with - This (c,_) -> - let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in - nhyps,This nc - | Thesis Plain as th -> interp_hyps sigma env hyps,th - | Thesis (For n) -> error "\"thesis for\" is not applicable here." in - let push_one hyp env0 = - match hyp with - (Hprop st | Hvar st) -> - match st.st_label with - Name id -> Environ.push_named (id,None,st.st_it) env0 - | _ -> env in - let nenv = List.fold_right push_one locvars env in - nenv,res - -let interp_casee sigma env = function - Real c -> Real (understand sigma env (fst c)) - | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) sigma env cut) - -let abstract_one_arg = function - (loc,(id,None)) -> - (fun raw -> - RLambda (dummy_loc,Name id, Explicit, - RHole (loc,Evd.BinderType (Name id)), raw)) - | (loc,(id,Some typ)) -> - (fun raw -> - RLambda (dummy_loc,Name id, Explicit, fst typ, raw)) - -let rawconstr_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 (rawconstr_of_fun args body) in - match_args destLambda [] constr args - -let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = function - Pthus i -> Pthus (interp_bare_proof_instr info sigma env i) - | Pthen i -> Pthen (interp_bare_proof_instr info sigma env i) - | Phence i -> Phence (interp_bare_proof_instr info sigma env i) - | Pcut c -> Pcut (interp_cut - (interp_no_bind (interp_statement - (interp_constr_or_thesis true))) - sigma env c) - | Psuffices c -> - Psuffices (interp_cut interp_suffices_clause sigma env c) - | Prew (s,c) -> Prew (s,interp_cut - (interp_no_bind (interp_statement - (interp_constr_in_type (get_eq_typ info env)))) - sigma env c) - - | Psuppose hyps -> Psuppose (interp_hyps sigma env hyps) - | Pcase (params,pat,hyps) -> - let tparams,tpat,thyps = interp_cases info sigma env params pat hyps in - Pcase (tparams,tpat,thyps) - | Ptake witl -> - Ptake (List.map (fun c -> understand sigma env (fst c)) witl) - | Pconsider (c,hyps) -> Pconsider (interp_constr false sigma env c, - interp_hyps sigma env hyps) - | Pper (et,c) -> Pper (et,interp_casee sigma env c) - | Pend bt -> Pend bt - | Pescape -> Pescape - | Passume hyps -> Passume (interp_hyps sigma env hyps) - | Pgiven hyps -> Pgiven (interp_hyps sigma env hyps) - | Plet hyps -> Plet (interp_hyps sigma env hyps) - | Pclaim st -> Pclaim (interp_statement (interp_constr true) sigma env st) - | Pfocus st -> Pfocus (interp_statement (interp_constr true) sigma env st) - | Pdefine (id,args,body) -> - let nargs,_,nbody = interp_fun sigma env args body in - Pdefine (id,nargs,nbody) - | Pcast (id,typ) -> - Pcast(id,interp_constr true sigma env typ) - -let rec interp_proof_instr info sigma env instr= - {emph = instr.emph; - instr = interp_bare_proof_instr info sigma env instr.instr} - - - diff --git a/tactics/decl_interp.mli b/tactics/decl_interp.mli deleted file mode 100644 index bd0859382b..0000000000 --- a/tactics/decl_interp.mli +++ /dev/null @@ -1,18 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -open Tacinterp -open Decl_expr -open Mod_subst - - -val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr -val interp_proof_instr : Decl_mode.pm_info -> - Evd.evar_map -> Environ.env -> glob_proof_instr -> proof_instr diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml deleted file mode 100644 index 9c58f06ee9..0000000000 --- a/tactics/decl_proof_instr.ml +++ /dev/null @@ -1,1518 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -open Util -open Pp -open Evd - -open Refiner -open Proof_type -open Proof_trees -open Tacmach -open Tacinterp -open Decl_expr -open Decl_mode -open Decl_interp -open Rawterm -open Names -open Nameops -open Declarations -open Tactics -open Tacticals -open Term -open Termops -open Namegen -open Reductionops -open Goptions - - -(* Strictness option *) - -let get_its_info gls = get_info gls.it - -let get_strictness,set_strictness = - let strictness = ref false in - (fun () -> (!strictness)),(fun b -> strictness:=b) - -let _ = - declare_bool_option - { optsync = true; - optname = "strict mode"; - optkey = ["Strict";"Proofs"]; - optread = get_strictness; - optwrite = set_strictness } - -let tcl_change_info_gen info_gen = - (fun gls -> - let gl =sig_it gls in - {it=[{gl with evar_extra=info_gen}];sigma=sig_sig gls}, - function - [pftree] -> - {pftree with - goal=gl; - ref=Some (Prim Change_evars,[pftree])} - | _ -> anomaly "change_info : Wrong number of subtrees") - -let tcl_change_info info gls = tcl_change_info_gen (Some (pm_in info)) gls - -let tcl_erase_info gls = tcl_change_info_gen None gls - -let special_whd gl= - let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in - (fun t -> Closure.whd_val infos (Closure.inject t)) - -let special_nf gl= - let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in - (fun t -> Closure.norm_val infos (Closure.inject t)) - -let is_good_inductive env ind = - let mib,oib = Inductive.lookup_mind_specif env ind in - oib.mind_nrealargs = 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib)) - -let check_not_per pts = - if not (Proof_trees.is_complete_proof (proof_of_pftreestate pts)) then - match get_stack pts with - Per (_,_,_,_)::_ -> - error "You are inside a proof per cases/induction.\n\ -Please \"suppose\" something or \"end\" it now." - | _ -> () - -let mk_evd metalist gls = - let evd0= create_goal_evar_defs (sig_sig gls) in - let add_one (meta,typ) evd = - meta_declare meta typ evd in - List.fold_right add_one metalist evd0 - -let is_tmp id = (string_of_id id).[0] = '_' - -let tmp_ids gls = - let ctx = pf_hyps gls in - match ctx with - [] -> [] - | _::q -> List.filter is_tmp (ids_of_named_context q) - -let clean_tmp gls = - let clean_id id0 gls0 = - tclTRY (clear [id0]) gls0 in - let rec clean_all = function - [] -> tclIDTAC - | id :: rest -> tclTHEN (clean_id id) (clean_all rest) - in - clean_all (tmp_ids gls) gls - -let assert_postpone id t = - assert_tac (Name id) t - -(* start a proof *) - -let start_proof_tac gls= - let gl=sig_it gls in - let info={pm_stack=[]} in - {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls}, - function - [pftree] -> - {pftree with - goal=gl; - ref=Some (Decl_proof true,[pftree])} - | _ -> anomaly "Dem : Wrong number of subtrees" - -let go_to_proof_mode () = - Pfedit.mutate - (fun pts -> nth_unproven 1 (solve_pftreestate start_proof_tac pts)) - -(* closing gaps *) - -let daimon_tac gls = - set_daimon_flag (); - ({it=[];sigma=sig_sig gls}, - function - [] -> - {open_subgoals=0; - goal=sig_it gls; - ref=Some (Daimon,[])} - | _ -> anomaly "Daimon: Wrong number of subtrees") - -let daimon _ pftree = - set_daimon_flag (); - {pftree with - open_subgoals=0; - ref=Some (Daimon,[])} - -let daimon_subtree = map_pftreestate (fun _ -> frontier_mapi daimon ) - -(* 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" - | Nested(Proof_instr (lock_focus,instr),spfl) -> - if lock_focus then - Nested(Proof_instr (false,instr),spfl) - else - anomaly "already marked as done" - | _ -> anomaly "mark_rule_as_done" - -let mark_proof_tree_as_done pt = - match pt.ref with - None -> anomaly "mark_proof_tree_as_done" - | Some (r,spfl) -> - {pt with ref= Some (mark_rule_as_done r,spfl)} - -let mark_as_done pts = - map_pftreestate - (fun _ -> mark_proof_tree_as_done) - (up_to_matching_rule is_focussing_command pts) - -(* post-instruction focus management *) - -let goto_current_focus pts = up_until_matching_rule is_focussing_command pts - -let goto_current_focus_or_top pts = - try - up_until_matching_rule is_focussing_command pts - with Not_found -> top_of_tree pts - -(* return *) - -let close_tactic_mode pts = - let pts1= - try goto_current_focus pts - with Not_found -> - error "\"return\" cannot be used outside of Declarative Proof Mode." in - let pts2 = daimon_subtree pts1 in - let pts3 = mark_as_done pts2 in - goto_current_focus pts3 - -let return_from_tactic_mode () = Pfedit.mutate close_tactic_mode - -(* end proof/claim *) - -let close_block bt pts = - let stack = - if Proof_trees.is_complete_proof (proof_of_pftreestate pts) then - get_top_stack pts - else - get_stack pts in - match bt,stack with - B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> - daimon_subtree (goto_current_focus pts) - | _, Claim::_ -> - error "\"end claim\" expected." - | _, Focus_claim::_ -> - error "\"end focus\" expected." - | _, [] -> - error "\"end proof\" expected." - | _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) -> - begin - match et with - ET_Case_analysis -> error "\"end cases\" expected." - | ET_Induction -> error "\"end induction\" expected." - end - | _,_ -> anomaly "Lonely suppose on stack." - -(* utility for suppose / suppose it is *) - -let close_previous_case pts = - if - Proof_trees.is_complete_proof (proof_of_pftreestate pts) - then - match get_top_stack pts with - Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..." - | Suppose_case :: Per (et,_,_,_) :: _ -> - goto_current_focus (mark_as_done pts) - | _ -> error "Not inside a proof per cases or induction." - else - match get_stack pts with - Per (et,_,_,_) :: _ -> pts - | Suppose_case :: Per (et,_,_,_) :: _ -> - goto_current_focus (mark_as_done (daimon_subtree pts)) - | _ -> error "Not inside a proof per cases or induction." - -(* Proof instructions *) - -(* automation *) - -let filter_hyps f gls = - let filter_aux (id,_,_) = - if f id then - tclIDTAC - else - tclTRY (clear [id]) in - tclMAP filter_aux (Environ.named_context_of_val gls.it.evar_hyps) gls - -let local_hyp_prefix = id_of_string "___" - -let add_justification_hyps keep items gls = - let add_aux c gls= - match kind_of_term c with - Var id -> - keep:=Idset.add id !keep; - tclIDTAC gls - | _ -> - let id=pf_get_new_id local_hyp_prefix gls in - keep:=Idset.add id !keep; - tclTHEN (letin_tac None (Names.Name id) c None Tacexpr.nowhere) - (thin_body [id]) gls in - tclMAP add_aux items gls - -let prepare_goal items gls = - let tokeep = ref Idset.empty in - let auxres = add_justification_hyps tokeep items gls in - tclTHENLIST - [ (fun _ -> auxres); - filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep)] gls - -let my_automation_tac = ref - (fun gls -> anomaly "No automation registered") - -let register_automation_tac tac = my_automation_tac:= tac - -let automation_tac gls = !my_automation_tac gls - -let justification tac gls= - tclORELSE - (tclSOLVE [tclTHEN tac assumption]) - (fun gls -> - if get_strictness () then - error "Insufficient justification." - else - begin - msg_warning (str "Insufficient justification."); - daimon_tac gls - end) gls - -let default_justification elems gls= - justification (tclTHEN (prepare_goal elems) automation_tac) gls - -(* code for conclusion refining *) - -let constant dir s = lazy (Coqlib.gen_constant "Declarative" dir s) - -let _and = constant ["Init";"Logic"] "and" - -let _and_rect = constant ["Init";"Logic"] "and_rect" - -let _prod = constant ["Init";"Datatypes"] "prod" - -let _prod_rect = constant ["Init";"Datatypes"] "prod_rect" - -let _ex = constant ["Init";"Logic"] "ex" - -let _ex_ind = constant ["Init";"Logic"] "ex_ind" - -let _sig = constant ["Init";"Specif"] "sig" - -let _sig_rect = constant ["Init";"Specif"] "sig_rect" - -let _sigT = constant ["Init";"Specif"] "sigT" - -let _sigT_rect = constant ["Init";"Specif"] "sigT_rect" - -type stackd_elt = -{se_meta:metavariable; - se_type:types; - se_last_meta:metavariable; - se_meta_list:(metavariable*types) list; - se_evd: evar_map} - -let rec replace_in_list m l = function - [] -> raise Not_found - | c::q -> if m=fst c then l@q else c::replace_in_list m l q - -let enstack_subsubgoals env se stack gls= - let hd,params = decompose_app (special_whd gls se.se_type) in - match kind_of_term hd with - Ind ind when is_good_inductive env ind -> - let mib,oib= - Inductive.lookup_mind_specif env ind in - let gentypes= - Inductive.arities_of_constructors ind (mib,oib) in - let process i gentyp = - let constructor = mkConstruct(ind,succ i) - (* constructors numbering*) in - let appterm = applist (constructor,params) in - let apptype = Term.prod_applist gentyp params in - let rc,_ = Reduction.dest_prod env apptype in - let rec meta_aux last lenv = function - [] -> (last,lenv,[]) - | (nam,_,typ)::q -> - let nlast=succ last in - let (llast,holes,metas) = - meta_aux nlast (mkMeta nlast :: lenv) q in - (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in - let (nlast,holes,nmetas) = - meta_aux se.se_last_meta [] (List.rev rc) in - let refiner = applist (appterm,List.rev holes) in - let evd = meta_assign se.se_meta - (refiner,(ConvUpToEta 0,TypeProcessed (* ? *))) se.se_evd in - let ncreated = replace_in_list - se.se_meta nmetas se.se_meta_list in - let evd0 = List.fold_left - (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in - List.iter (fun (m,typ) -> - Stack.push - {se_meta=m; - se_type=typ; - se_evd=evd0; - se_meta_list=ncreated; - se_last_meta=nlast} stack) (List.rev nmetas) - in - Array.iteri process gentypes - | _ -> () - -let rec nf_list evd = - function - [] -> [] - | (m,typ)::others -> - if meta_defined evd m then - nf_list evd others - else - (m,nf_meta evd typ)::nf_list evd others - -let find_subsubgoal c ctyp skip submetas gls = - let env= pf_env gls in - let concl = pf_concl gls in - let evd = mk_evd ((0,concl)::submetas) gls in - let stack = Stack.create () in - let max_meta = - List.fold_left (fun a (m,_) -> max a m) 0 submetas in - let _ = Stack.push - {se_meta=0; - se_type=concl; - se_last_meta=max_meta; - se_meta_list=[0,concl]; - se_evd=evd} stack in - let rec dfs n = - let se = Stack.pop stack in - try - let unifier = - Unification.w_unify true env Reduction.CUMUL - ctyp se.se_type se.se_evd in - if n <= 0 then - {se with - se_evd=meta_assign se.se_meta - (c,(ConvUpToEta 0,TypeNotProcessed (* ?? *))) unifier; - se_meta_list=replace_in_list - se.se_meta submetas se.se_meta_list} - else - dfs (pred n) - with _ -> - begin - enstack_subsubgoals env se stack gls; - dfs n - end in - let nse= try dfs skip with Stack.Empty -> raise Not_found in - nf_list nse.se_evd nse.se_meta_list,nf_meta nse.se_evd (mkMeta 0) - -let concl_refiner metas body gls = - let concl = pf_concl gls in - let evd = sig_sig gls in - let env = pf_env gls in - let sort = family_of_sort (Typing.sort_of env evd concl) in - let rec aux env avoid subst = function - [] -> anomaly "concl_refiner: cannot happen" - | (n,typ)::rest -> - let _A = subst_meta subst typ in - let x = id_of_name_using_hdchar env _A Anonymous in - let _x = fresh_id avoid x gls in - let nenv = Environ.push_named (_x,None,_A) env in - let asort = family_of_sort (Typing.sort_of nenv evd _A) in - let nsubst = (n,mkVar _x)::subst in - if rest = [] then - asort,_A,mkNamedLambda _x _A (subst_meta nsubst body) - else - let bsort,_B,nbody = - aux nenv (_x::avoid) ((n,mkVar _x)::subst) rest in - let body = mkNamedLambda _x _A nbody in - if occur_term (mkVar _x) _B then - begin - let _P = mkNamedLambda _x _A _B in - match bsort,sort with - InProp,InProp -> - let _AxB = mkApp(Lazy.force _ex,[|_A;_P|]) in - InProp,_AxB, - mkApp(Lazy.force _ex_ind,[|_A;_P;concl;body|]) - | InProp,_ -> - let _AxB = mkApp(Lazy.force _sig,[|_A;_P|]) in - let _P0 = mkLambda(Anonymous,_AxB,concl) in - InType,_AxB, - mkApp(Lazy.force _sig_rect,[|_A;_P;_P0;body|]) - | _,_ -> - let _AxB = mkApp(Lazy.force _sigT,[|_A;_P|]) in - let _P0 = mkLambda(Anonymous,_AxB,concl) in - InType,_AxB, - mkApp(Lazy.force _sigT_rect,[|_A;_P;_P0;body|]) - end - else - begin - match asort,bsort with - InProp,InProp -> - let _AxB = mkApp(Lazy.force _and,[|_A;_B|]) in - InProp,_AxB, - mkApp(Lazy.force _and_rect,[|_A;_B;concl;body|]) - |_,_ -> - let _AxB = mkApp(Lazy.force _prod,[|_A;_B|]) in - let _P0 = mkLambda(Anonymous,_AxB,concl) in - InType,_AxB, - mkApp(Lazy.force _prod_rect,[|_A;_B;_P0;body|]) - end - in - let (_,_,prf) = aux env [] [] metas in - mkApp(prf,[|mkMeta 1|]) - -let thus_tac c ctyp submetas gls = - let list,proof = - try - find_subsubgoal c ctyp 0 submetas gls - with Not_found -> - error "I could not relate this statement to the thesis." in - if list = [] then - exact_check proof gls - else - let refiner = concl_refiner list proof gls in - Tactics.refine refiner gls - -(* general forward step *) - -let mk_stat_or_thesis info gls = function - This c -> c - | Thesis (For _ ) -> - error "\"thesis for ...\" is not applicable here." - | Thesis Plain -> pf_concl gls - -let just_tac _then cut info gls0 = - let items_tac gls = - match cut.cut_by with - None -> tclIDTAC gls - | Some items -> - let items_ = - if _then then - let last_id = get_last (pf_env gls) in - (mkVar last_id)::items - else items - in prepare_goal items_ gls in - let method_tac gls = - match cut.cut_using with - None -> - automation_tac gls - | Some tac -> - (Tacinterp.eval_tactic tac) gls in - justification (tclTHEN items_tac method_tac) gls0 - -let instr_cut mkstat _thus _then cut gls0 = - let info = get_its_info gls0 in - let stat = cut.cut_stat in - let (c_id,_) = match stat.st_label with - Anonymous -> - pf_get_new_id (id_of_string "_fact") gls0,false - | Name id -> id,true in - let c_stat = mkstat info gls0 stat.st_it in - let thus_tac gls= - if _thus then - thus_tac (mkVar c_id) c_stat [] gls - else tclIDTAC gls in - tclTHENS (assert_postpone c_id c_stat) - [tclTHEN tcl_erase_info (just_tac _then cut info); - thus_tac] gls0 - - - -(* iterated equality *) -let _eq = Libnames.constr_of_global (Coqlib.glob_eq) - -let decompose_eq id gls = - let typ = pf_get_hyp_typ gls id in - let whd = (special_whd gls typ) in - match kind_of_term whd with - App (f,args)-> - if eq_constr f _eq && (Array.length args)=3 - then (args.(0), - args.(1), - args.(2)) - else error "Previous step is not an equality." - | _ -> error "Previous step is not an equality." - -let instr_rew _thus rew_side cut gls0 = - let last_id = - try get_last (pf_env gls0) with _ -> error "No previous equality." in - let typ,lhs,rhs = decompose_eq last_id gls0 in - let items_tac gls = - match cut.cut_by with - None -> tclIDTAC gls - | Some items -> prepare_goal items gls in - let method_tac gls = - match cut.cut_using with - None -> - automation_tac gls - | Some tac -> - (Tacinterp.eval_tactic tac) gls in - let just_tac gls = - justification (tclTHEN items_tac method_tac) gls in - let (c_id,_) = match cut.cut_stat.st_label with - Anonymous -> - pf_get_new_id (id_of_string "_eq") gls0,false - | Name id -> id,true in - let thus_tac new_eq gls= - if _thus then - thus_tac (mkVar c_id) new_eq [] gls - else tclIDTAC gls in - match rew_side with - Lhs -> - let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in - tclTHENS (assert_postpone c_id new_eq) - [tclTHEN tcl_erase_info - (tclTHENS (transitivity lhs) - [just_tac;exact_check (mkVar last_id)]); - thus_tac new_eq] gls0 - | Rhs -> - let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in - tclTHENS (assert_postpone c_id new_eq) - [tclTHEN tcl_erase_info - (tclTHENS (transitivity rhs) - [exact_check (mkVar last_id);just_tac]); - thus_tac new_eq] gls0 - - - -(* tactics for claim/focus *) - -let instr_claim _thus st gls0 = - let info = get_its_info gls0 in - let (id,_) = match st.st_label with - Anonymous -> pf_get_new_id (id_of_string "_claim") gls0,false - | Name id -> id,true in - let thus_tac gls= - if _thus then - thus_tac (mkVar id) st.st_it [] gls - else tclIDTAC gls in - let ninfo1 = {pm_stack= - (if _thus then Focus_claim else Claim)::info.pm_stack} in - tclTHENS (assert_postpone id st.st_it) - [tcl_change_info ninfo1; - thus_tac] gls0 - -(* tactics for assume *) - -let push_intro_tac coerce nam gls = - let (hid,_) = - match nam with - Anonymous -> pf_get_new_id (id_of_string "_hyp") gls,false - | Name id -> id,true in - tclTHENLIST - [intro_mustbe_force hid; - coerce hid] - gls - -let assume_tac hyps gls = - List.fold_right - (fun (Hvar st | Hprop st) -> - tclTHEN - (push_intro_tac - (fun id -> - convert_hyp (id,None,st.st_it)) st.st_label)) - hyps tclIDTAC gls - -let assume_hyps_or_theses hyps gls = - List.fold_right - (function - (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) -> - tclTHEN - (push_intro_tac - (fun id -> - convert_hyp (id,None,c)) nam) - | Hprop {st_label=nam;st_it=Thesis (tk)} -> - tclTHEN - (push_intro_tac - (fun id -> tclIDTAC) nam)) - hyps tclIDTAC gls - -let assume_st hyps gls = - List.fold_right - (fun st -> - tclTHEN - (push_intro_tac - (fun id -> convert_hyp (id,None,st.st_it)) st.st_label)) - hyps tclIDTAC gls - -let assume_st_letin hyps gls = - List.fold_right - (fun st -> - tclTHEN - (push_intro_tac - (fun id -> - convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label)) - hyps tclIDTAC gls - -(* suffices *) - -let rec metas_from n hyps = - match hyps with - _ :: q -> n :: metas_from (succ n) q - | [] -> [] - -let rec build_product args body = - match args with - (Hprop st| Hvar st )::rest -> - let pprod= lift 1 (build_product rest body) in - let lbody = - match st.st_label with - Anonymous -> pprod - | Name id -> subst_term (mkVar id) pprod in - mkProd (st.st_label, st.st_it, lbody) - | [] -> body - -let rec build_applist prod = function - [] -> [],prod - | n::q -> - let (_,typ,_) = destProd prod in - let ctx,head = build_applist (Term.prod_applist prod [mkMeta n]) q in - (n,typ)::ctx,head - -let instr_suffices _then cut gls0 = - let info = get_its_info gls0 in - let c_id = pf_get_new_id (id_of_string "_cofact") gls0 in - let ctx,hd = cut.cut_stat in - let c_stat = build_product ctx (mk_stat_or_thesis info gls0 hd) in - let metas = metas_from 1 ctx in - let c_ctx,c_head = build_applist c_stat metas in - let c_term = applist (mkVar c_id,List.map mkMeta metas) in - let thus_tac gls= - thus_tac c_term c_head c_ctx gls in - tclTHENS (assert_postpone c_id c_stat) - [tclTHENLIST - [ assume_tac ctx; - tcl_erase_info; - just_tac _then cut info]; - thus_tac] gls0 - -(* tactics for consider/given *) - -let conjunction_arity id gls = - let typ = pf_get_hyp_typ gls id in - let hd,params = decompose_app (special_whd gls typ) in - let env =pf_env gls in - match kind_of_term hd with - Ind ind when is_good_inductive env ind -> - let mib,oib= - Inductive.lookup_mind_specif env ind in - let gentypes= - Inductive.arities_of_constructors ind (mib,oib) in - let _ = if Array.length gentypes <> 1 then raise Not_found in - let apptype = Term.prod_applist gentypes.(0) params in - let rc,_ = Reduction.dest_prod env apptype in - List.length rc - | _ -> raise Not_found - -let rec intron_then n ids ltac gls = - if n<=0 then - ltac ids gls - else - let id = pf_get_new_id (id_of_string "_tmp") gls in - tclTHEN - (intro_mustbe_force id) - (intron_then (pred n) (id::ids) ltac) gls - - -let rec consider_match may_intro introduced available expected gls = - match available,expected with - [],[] -> - tclIDTAC gls - | _,[] -> error "Last statements do not match a complete hypothesis." - (* should tell which ones *) - | [],hyps -> - if may_intro then - begin - let id = pf_get_new_id (id_of_string "_tmp") gls in - tclIFTHENELSE - (intro_mustbe_force id) - (consider_match true [] [id] hyps) - (fun _ -> - error "Not enough sub-hypotheses to match statements.") - gls - end - else - error "Not enough sub-hypotheses to match statements." - (* should tell which ones *) - | id::rest_ids,(Hvar st | Hprop st)::rest -> - tclIFTHENELSE (convert_hyp (id,None,st.st_it)) - begin - match st.st_label with - Anonymous -> - consider_match may_intro ((id,false)::introduced) rest_ids rest - | Name hid -> - tclTHENLIST - [rename_hyp [id,hid]; - consider_match may_intro ((hid,true)::introduced) rest_ids rest] - end - begin - (fun gls -> - let nhyps = - try conjunction_arity id gls with - Not_found -> error "Matching hypothesis not found." in - tclTHENLIST - [general_case_analysis false (mkVar id,NoBindings); - intron_then nhyps [] - (fun l -> consider_match may_intro introduced - (List.rev_append l rest_ids) expected)] gls) - end - gls - -let consider_tac c hyps gls = - match kind_of_term (strip_outer_cast c) with - Var id -> - consider_match false [] [id] hyps gls - | _ -> - let id = pf_get_new_id (id_of_string "_tmp") gls in - tclTHEN - (forward None (Some (dummy_loc, Genarg.IntroIdentifier id)) c) - (consider_match false [] [id] hyps) gls - - -let given_tac hyps gls = - consider_match true [] [] hyps gls - -(* tactics for take *) - -let rec take_tac wits gls = - match wits with - [] -> tclIDTAC gls - | wit::rest -> - let typ = pf_type_of gls wit in - tclTHEN (thus_tac wit typ []) (take_tac rest) gls - - -(* tactics for define *) - -let rec build_function args body = - match args with - st::rest -> - let pfun= lift 1 (build_function rest body) in - let id = match st.st_label with - Anonymous -> assert false - | Name id -> id in - mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun) - | [] -> body - -let define_tac id args body gls = - let t = build_function args body in - letin_tac None (Name id) t None Tacexpr.nowhere gls - -(* tactics for reconsider *) - -let cast_tac id_or_thesis typ gls = - match id_or_thesis with - This id -> - let (_,body,_) = pf_get_hyp gls id in - convert_hyp (id,body,typ) gls - | Thesis (For _ ) -> - error "\"thesis for ...\" is not applicable here." - | Thesis Plain -> - convert_concl typ DEFAULTcast gls - -(* per cases *) - -let is_rec_pos (main_ind,wft) = - match main_ind with - None -> false - | Some index -> - match fst (Rtree.dest_node wft) with - Mrec i when i = index -> true - | _ -> false - -let rec constr_trees (main_ind,wft) ind = - match Rtree.dest_node wft with - Norec,_ -> - let itree = - (snd (Global.lookup_inductive ind)).mind_recargs in - constr_trees (None,itree) ind - | _,constrs -> main_ind,constrs - -let ind_args rp ind = - let main_ind,constrs = constr_trees rp ind in - let args ctree = - Array.map (fun t -> main_ind,t) (snd (Rtree.dest_node ctree)) in - Array.map args constrs - -let init_tree ids ind rp nexti = - let indargs = ind_args rp ind in - let do_i i arp = (Array.map is_rec_pos arp),nexti i arp in - Split_patt (ids,ind,Array.mapi do_i indargs) - -let map_tree_rp rp id_fun mapi = function - Split_patt (ids,ind,branches) -> - let indargs = ind_args rp ind in - let do_i i (recargs,bri) = recargs,mapi i indargs.(i) bri in - Split_patt (id_fun ids,ind,Array.mapi do_i branches) - | _ -> failwith "map_tree_rp: not a splitting node" - -let map_tree id_fun mapi = function - Split_patt (ids,ind,branches) -> - let do_i i (recargs,bri) = recargs,mapi i bri in - Split_patt (id_fun ids,ind,Array.mapi do_i branches) - | _ -> failwith "map_tree: not a splitting node" - - -let start_tree env ind rp = - init_tree Idset.empty ind rp (fun _ _ -> None) - -let build_per_info etype casee gls = - let concl=pf_concl gls in - let env=pf_env gls in - let ctyp=pf_type_of gls casee in - let is_dep = dependent casee concl in - let hd,args = decompose_app (special_whd gls ctyp) in - let ind = - try - destInd hd - with _ -> - error "Case analysis must be done on an inductive object." in - let mind,oind = Global.lookup_inductive ind in - let nparams,index = - match etype with - ET_Induction -> mind.mind_nparams_rec,Some (snd ind) - | _ -> mind.mind_nparams,None in - let params,real_args = list_chop nparams args in - let abstract_obj c body = - let typ=pf_type_of gls c in - lambda_create env (typ,subst_term c body) in - let pred= List.fold_right abstract_obj - real_args (lambda_create env (ctyp,subst_term casee concl)) in - is_dep, - {per_casee=casee; - per_ctype=ctyp; - per_ind=ind; - per_pred=pred; - per_args=real_args; - per_params=params; - per_nparams=nparams; - per_wf=index,oind.mind_recargs} - -let per_tac etype casee gls= - let env=pf_env gls in - let info = get_its_info gls in - match casee with - Real c -> - let is_dep,per_info = build_per_info etype c gls in - let ek = - if is_dep then - EK_dep (start_tree env per_info.per_ind per_info.per_wf) - else EK_unknown in - tcl_change_info - {pm_stack= - Per(etype,per_info,ek,[])::info.pm_stack} gls - | Virtual cut -> - assert (cut.cut_stat.st_label=Anonymous); - let id = pf_get_new_id (id_of_string "anonymous_matched") gls in - let c = mkVar id in - let modified_cut = - {cut with cut_stat={cut.cut_stat with st_label=Name id}} in - tclTHEN - (instr_cut (fun _ _ c -> c) false false modified_cut) - (fun gls0 -> - let is_dep,per_info = build_per_info etype c gls0 in - assert (not is_dep); - tcl_change_info - {pm_stack= - Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0) - gls - -(* suppose *) - -let register_nodep_subcase id= function - Per(et,pi,ek,clauses)::s -> - begin - match ek with - EK_unknown -> clauses,Per(et,pi,EK_nodep,id::clauses)::s - | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s - | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"." - end - | _ -> anomaly "wrong stack state" - -let suppose_tac hyps gls0 = - let info = get_its_info gls0 in - let thesis = pf_concl gls0 in - let id = pf_get_new_id (id_of_string "subcase_") gls0 in - let clause = build_product hyps thesis in - let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in - let old_clauses,stack = register_nodep_subcase id info.pm_stack in - let ninfo2 = {pm_stack=stack} in - tclTHENS (assert_postpone id clause) - [tclTHENLIST [tcl_change_info ninfo1; - assume_tac hyps; - clear old_clauses]; - tcl_change_info ninfo2] gls0 - -(* suppose it is ... *) - -(* pattern matching compiling *) - -let rec skip_args rest ids n = - if n <= 0 then - Close_patt rest - else - Skip_patt (ids,skip_args rest ids (pred n)) - -let rec tree_of_pats ((id,_) as cpl) pats = - match pats with - [] -> End_patt cpl - | args::stack -> - match args with - [] -> Close_patt (tree_of_pats cpl stack) - | (patt,rp) :: rest_args -> - match patt with - PatVar (_,v) -> - Skip_patt (Idset.singleton id, - tree_of_pats cpl (rest_args::stack)) - | PatCstr (_,(ind,cnum),args,nam) -> - let nexti i ati = - if i = pred cnum then - let nargs = - list_map_i (fun j a -> (a,ati.(j))) 0 args in - Some (Idset.singleton id, - tree_of_pats cpl (nargs::rest_args::stack)) - else None - in init_tree Idset.empty ind rp nexti - -let rec add_branch ((id,_) as cpl) pats tree= - match pats with - [] -> - begin - match tree with - End_patt cpl0 -> End_patt cpl0 - (* this ensures precedence for overlapping patterns *) - | _ -> anomaly "tree is expected to end here" - end - | args::stack -> - match args with - [] -> - begin - match tree with - Close_patt t -> - Close_patt (add_branch cpl stack t) - | _ -> anomaly "we should pop here" - end - | (patt,rp) :: rest_args -> - match patt with - PatVar (_,v) -> - begin - match tree with - Skip_patt (ids,t) -> - Skip_patt (Idset.add id ids, - add_branch cpl (rest_args::stack) t) - | Split_patt (_,_,_) -> - map_tree (Idset.add id) - (fun i bri -> - append_branch cpl 1 (rest_args::stack) bri) - tree - | _ -> anomaly "No pop/stop expected here" - end - | PatCstr (_,(ind,cnum),args,nam) -> - match tree with - Skip_patt (ids,t) -> - let nexti i ati = - if i = pred cnum then - let nargs = - list_map_i (fun j a -> (a,ati.(j))) 0 args in - Some (Idset.add id ids, - add_branch cpl (nargs::rest_args::stack) - (skip_args t ids (Array.length ati))) - else - Some (ids, - skip_args t ids (Array.length ati)) - in init_tree ids ind rp nexti - | Split_patt (_,ind0,_) -> - if (ind <> ind0) then error - (* this can happen with coercions *) - "Case pattern belongs to wrong inductive type."; - let mapi i ati bri = - if i = pred cnum then - let nargs = - list_map_i (fun j a -> (a,ati.(j))) 0 args in - append_branch cpl 0 - (nargs::rest_args::stack) bri - else bri in - map_tree_rp rp (fun ids -> ids) mapi tree - | _ -> anomaly "No pop/stop expected here" -and append_branch ((id,_) as cpl) depth pats = function - Some (ids,tree) -> - Some (Idset.add id ids,append_tree cpl depth pats tree) - | None -> - Some (Idset.singleton id,tree_of_pats cpl pats) -and append_tree ((id,_) as cpl) depth pats tree = - if depth<=0 then add_branch cpl pats tree - else match tree with - Close_patt t -> - Close_patt (append_tree cpl (pred depth) pats t) - | Skip_patt (ids,t) -> - Skip_patt (Idset.add id ids,append_tree cpl depth pats t) - | End_patt _ -> anomaly "Premature end of branch" - | Split_patt (_,_,_) -> - map_tree (Idset.add id) - (fun i bri -> append_branch cpl (succ depth) pats bri) tree - -(* suppose it is *) - -let rec st_assoc id = function - [] -> raise Not_found - | st::_ when st.st_label = id -> st.st_it - | _ :: rest -> st_assoc id rest - -let thesis_for obj typ per_info env= - let rc,hd1=decompose_prod typ in - let cind,all_args=decompose_app typ in - let ind = destInd cind in - let _ = if ind <> per_info.per_ind then - errorlabstrm "thesis_for" - ((Printer.pr_constr_env env obj) ++ spc () ++ - str"cannot give an induction hypothesis (wrong inductive type).") in - let params,args = list_chop per_info.per_nparams all_args in - let _ = if not (List.for_all2 eq_constr params per_info.per_params) then - errorlabstrm "thesis_for" - ((Printer.pr_constr_env env obj) ++ spc () ++ - str "cannot give an induction hypothesis (wrong parameters).") in - let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in - compose_prod rc (whd_beta Evd.empty hd2) - -let rec build_product_dep pat_info per_info args body gls = - match args with - (Hprop {st_label=nam;st_it=This c} - | Hvar {st_label=nam;st_it=c})::rest -> - let pprod= - lift 1 (build_product_dep pat_info per_info rest body gls) in - let lbody = - match nam with - Anonymous -> body - | Name id -> subst_var id pprod in - mkProd (nam,c,lbody) - | Hprop ({st_it=Thesis tk} as st)::rest -> - let pprod= - lift 1 (build_product_dep pat_info per_info rest body gls) in - let lbody = - match st.st_label with - Anonymous -> body - | Name id -> subst_var id pprod in - let ptyp = - match tk with - For id -> - let obj = mkVar id in - let typ = - try st_assoc (Name id) pat_info.pat_vars - with Not_found -> - snd (st_assoc (Name id) pat_info.pat_aliases) in - thesis_for obj typ per_info (pf_env gls) - | Plain -> pf_concl gls in - mkProd (st.st_label,ptyp,lbody) - | [] -> body - -let build_dep_clause params pat_info per_info hyps gls = - let concl= - thesis_for pat_info.pat_constr pat_info.pat_typ per_info (pf_env gls) in - let open_clause = - build_product_dep pat_info per_info hyps concl gls in - let prod_one st body = - match st.st_label with - Anonymous -> mkProd(Anonymous,st.st_it,lift 1 body) - | Name id -> mkNamedProd id st.st_it (lift 1 body) in - let let_one_in st body = - match st.st_label with - Anonymous -> mkLetIn(Anonymous,fst st.st_it,snd st.st_it,lift 1 body) - | Name id -> - mkNamedLetIn id (fst st.st_it) (snd st.st_it) (lift 1 body) in - let aliased_clause = - List.fold_right let_one_in pat_info.pat_aliases open_clause in - List.fold_right prod_one (params@pat_info.pat_vars) aliased_clause - -let rec register_dep_subcase id env per_info pat = function - EK_nodep -> error "Only \"suppose it is\" can be used here." - | EK_unknown -> - register_dep_subcase id env per_info pat - (EK_dep (start_tree env per_info.per_ind per_info.per_wf)) - | EK_dep tree -> EK_dep (add_branch id [[pat,per_info.per_wf]] tree) - -let case_tac params pat_info hyps gls0 = - let info = get_its_info gls0 in - let id = pf_get_new_id (id_of_string "subcase_") gls0 in - let et,per_info,ek,old_clauses,rest = - match info.pm_stack with - Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) - | _ -> anomaly "wrong place for cases" in - let clause = build_dep_clause params pat_info per_info hyps gls0 in - let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in - let nek = - register_dep_subcase (id,(List.length params,List.length hyps)) - (pf_env gls0) per_info pat_info.pat_pat ek in - let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in - tclTHENS (assert_postpone id clause) - [tclTHENLIST - [tcl_change_info ninfo1; - assume_st (params@pat_info.pat_vars); - assume_st_letin pat_info.pat_aliases; - assume_hyps_or_theses hyps; - clear old_clauses]; - tcl_change_info ninfo2] gls0 - -(* end cases *) - -type instance_stack = - (constr option*(constr list) list) list - -let initial_instance_stack ids = - List.map (fun id -> id,[None,[]]) ids - -let push_one_arg arg = function - [] -> anomaly "impossible" - | (head,args) :: ctx -> - ((head,(arg::args)) :: ctx) - -let push_arg arg stacks = - List.map (fun (id,stack) -> (id,push_one_arg arg stack)) stacks - - -let push_one_head c ids (id,stack) = - let head = if Idset.mem id ids then Some c else None in - id,(head,[]) :: stack - -let push_head c ids stacks = - List.map (push_one_head c ids) stacks - -let pop_one (id,stack) = - let nstack= - match stack with - [] -> anomaly "impossible" - | [c] as l -> l - | (Some head,args)::(head0,args0)::ctx -> - let arg = applist (head,(List.rev args)) in - (head0,(arg::args0))::ctx - | (None,args)::(head0,args0)::ctx -> - (head0,(args@args0))::ctx - in id,nstack - -let pop_stacks stacks = - List.map pop_one stacks - -let hrec_for fix_id per_info gls obj_id = - let obj=mkVar obj_id in - let typ=pf_get_hyp_typ gls obj_id in - let rc,hd1=decompose_prod typ in - let cind,all_args=decompose_app typ in - let ind = destInd cind in assert (ind=per_info.per_ind); - let params,args= list_chop per_info.per_nparams all_args in - assert begin - try List.for_all2 eq_constr params per_info.per_params with - Invalid_argument _ -> false end; - let hd2 = applist (mkVar fix_id,args@[obj]) in - compose_lam rc (whd_beta gls.sigma hd2) - - -let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = - match tree, objs with - Close_patt t,_ -> - let args0 = pop_stacks args in - execute_cases fix_name per_info tacnext args0 objs nhrec t gls - | Skip_patt (_,t),skipped::next_objs -> - let args0 = push_arg skipped args in - execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls - | End_patt (id,(nparams,nhyps)),[] -> - begin - match List.assoc id args with - [None,br_args] -> - let all_metas = - list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in - let param_metas,hyp_metas = list_chop nparams all_metas in - tclTHEN - (tclDO nhrec introf) - (tacnext - (applist (mkVar id, - List.append param_metas - (List.rev_append br_args hyp_metas)))) gls - | _ -> anomaly "wrong stack size" - end - | Split_patt (ids,ind,br), casee::next_objs -> - let (mind,oind) as spec = Global.lookup_inductive ind in - let nparams = mind.mind_nparams in - let concl=pf_concl gls in - let env=pf_env gls in - let ctyp=pf_type_of gls casee in - let hd,all_args = decompose_app (special_whd gls ctyp) in - let _ = assert (destInd hd = ind) in (* just in case *) - let params,real_args = list_chop nparams all_args in - let abstract_obj c body = - let typ=pf_type_of gls c in - lambda_create env (typ,subst_term c body) in - let elim_pred = List.fold_right abstract_obj - real_args (lambda_create env (ctyp,subst_term casee concl)) in - let case_info = Inductiveops.make_case_info env ind RegularStyle in - let gen_arities = Inductive.arities_of_constructors ind spec in - let f_ids typ = - let sign = - (prod_assum (Term.prod_applist typ params)) in - find_intro_names sign gls in - let constr_args_ids = Array.map f_ids gen_arities in - let case_term = - mkCase(case_info,elim_pred,casee, - Array.mapi (fun i _ -> mkMeta (succ i)) constr_args_ids) in - let branch_tac i (recargs,bro) gls0 = - let args_ids = constr_args_ids.(i) in - let rec aux n = function - [] -> - assert (n=Array.length recargs); - next_objs,[],nhrec - | id :: q -> - let objs,recs,nrec = aux (succ n) q in - if recargs.(n) - then (mkVar id::objs),(id::recs),succ nrec - else (mkVar id::objs),recs,nrec in - let objs,recs,nhrec = aux 0 args_ids in - tclTHENLIST - [tclMAP intro_mustbe_force args_ids; - begin - fun gls1 -> - let hrecs = - List.map - (fun id -> - hrec_for (out_name fix_name) per_info gls1 id) - recs in - generalize hrecs gls1 - end; - match bro with - None -> - msg_warning (str "missing case"); - tacnext (mkMeta 1) - | Some (sub_ids,tree) -> - let br_args = - List.filter - (fun (id,_) -> Idset.mem id sub_ids) args in - let construct = - applist (mkConstruct(ind,succ i),params) in - let p_args = - push_head construct ids br_args in - execute_cases fix_name per_info tacnext - p_args objs nhrec tree] gls0 in - tclTHENSV - (refine case_term) - (Array.mapi branch_tac br) gls - | Split_patt (_, _, _) , [] -> - anomaly "execute_cases : Nothing to split" - | Skip_patt _ , [] -> - anomaly "execute_cases : Nothing to skip" - | End_patt (_,_) , _ :: _ -> - anomaly "execute_cases : End of branch with garbage left" - -let understand_my_constr c gls = - let env = pf_env gls in - let nc = names_of_rel_context env in - let rawc = Detyping.detype false [] nc c in - let rec frob = function REvar _ -> RHole (dummy_loc,QuestionMark Expand) | rc -> map_rawconstr frob rc in - Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) - -let set_refine,my_refine = -let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in -((fun tac -> refine:= tac), -(fun c gls -> - let oc = understand_my_constr c gls in - !refine oc gls)) - -(* end focus/claim *) - -let end_tac et2 gls = - let info = get_its_info gls in - let et1,pi,ek,clauses = - match info.pm_stack with - Suppose_case::_ -> - anomaly "This case should already be trapped" - | Claim::_ -> - error "\"end claim\" expected." - | Focus_claim::_ -> - error "\"end focus\" expected." - | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) - | [] -> - anomaly "This case should already be trapped" in - let et = - if et1 <> et2 then - match et1 with - ET_Case_analysis -> - error "\"end cases\" expected." - | ET_Induction -> - error "\"end induction\" expected." - else et1 in - tclTHEN - tcl_erase_info - begin - match et,ek with - _,EK_unknown -> - tclSOLVE [simplest_elim pi.per_casee] - | ET_Case_analysis,EK_nodep -> - tclTHEN - (general_case_analysis false (pi.per_casee,NoBindings)) - (default_justification (List.map mkVar clauses)) - | ET_Induction,EK_nodep -> - tclTHENLIST - [generalize (pi.per_args@[pi.per_casee]); - simple_induct (AnonHyp (succ (List.length pi.per_args))); - default_justification (List.map mkVar clauses)] - | ET_Case_analysis,EK_dep tree -> - execute_cases Anonymous pi - (fun c -> tclTHENLIST - [my_refine c; - clear clauses; - justification assumption]) - (initial_instance_stack clauses) [pi.per_casee] 0 tree - | ET_Induction,EK_dep tree -> - let nargs = (List.length pi.per_args) in - tclTHEN (generalize (pi.per_args@[pi.per_casee])) - begin - fun gls0 -> - let fix_id = - pf_get_new_id (id_of_string "_fix") gls0 in - let c_id = - pf_get_new_id (id_of_string "_main_arg") gls0 in - tclTHENLIST - [fix (Some fix_id) (succ nargs); - tclDO nargs introf; - intro_mustbe_force c_id; - execute_cases (Name fix_id) pi - (fun c -> - tclTHENLIST - [clear [fix_id]; - my_refine c; - clear clauses; - justification assumption]) - (initial_instance_stack clauses) - [mkVar c_id] 0 tree] gls0 - end - end gls - -(* escape *) - -let escape_tac gls = tcl_erase_info gls - -(* General instruction engine *) - -let rec do_proof_instr_gen _thus _then instr = - match instr with - Pthus i -> - assert (not _thus); - do_proof_instr_gen true _then i - | Pthen i -> - assert (not _then); - do_proof_instr_gen _thus true i - | Phence i -> - assert (not (_then || _thus)); - do_proof_instr_gen true true i - | Pcut c -> - instr_cut mk_stat_or_thesis _thus _then c - | Psuffices c -> - instr_suffices _then c - | Prew (s,c) -> - assert (not _then); - instr_rew _thus s c - | Pconsider (c,hyps) -> consider_tac c hyps - | Pgiven hyps -> given_tac hyps - | Passume hyps -> assume_tac hyps - | Plet hyps -> assume_tac hyps - | Pclaim st -> instr_claim false st - | Pfocus st -> instr_claim true st - | Ptake witl -> take_tac witl - | Pdefine (id,args,body) -> define_tac id args body - | Pcast (id,typ) -> cast_tac id typ - | Pper (et,cs) -> per_tac et cs - | Psuppose hyps -> suppose_tac hyps - | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps - | Pend (B_elim et) -> end_tac et - | Pend _ -> anomaly "Not applicable" - | Pescape -> escape_tac - -let eval_instr {instr=instr} = - do_proof_instr_gen false false instr - -let rec preprocess pts instr = - match instr with - Phence i |Pthus i | Pthen i -> preprocess pts i - | Psuffices _ | Pcut _ | Passume _ | Plet _ | Pclaim _ | Pfocus _ - | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ - | Pdefine (_,_,_) | Pper _ | Prew _ -> - check_not_per pts; - true,pts - | Pescape -> - check_not_per pts; - true,pts - | Pcase _ | Psuppose _ | Pend (B_elim _) -> - true,close_previous_case pts - | Pend bt -> - false,close_block bt pts - -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 (_,_) -> pts - | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ - | Pescape -> nth_unproven 1 pts - | Pend (B_elim ET_Induction) -> - begin - let pf = proof_of_pftreestate pts in - let (pfterm,_) = extract_open_pftreestate pts in - let env = Evd.evar_env (goal_of_proof pf) in - try - Inductiveops.control_only_guard env pfterm; - goto_current_focus_or_top (mark_as_done pts) - with - Type_errors.TypeError(env, - Type_errors.IllFormedRecBody(_,_,_,_,_)) -> - anomaly "\"end induction\" generated an ill-formed fixpoint" - end - | Pend _ -> - goto_current_focus_or_top (mark_as_done pts) - -let do_instr raw_instr pts = - let has_tactic,pts1 = preprocess pts raw_instr.instr in - let pts2 = - if has_tactic then - let gl = nth_goal_of_pftreestate 1 pts1 in - let env= pf_env gl in - let sigma= project gl in - let ist = {ltacvars = ([],[]); ltacrecvars = []; - gsigma = sigma; genv = env} in - let glob_instr = intern_proof_instr ist raw_instr in - let instr = - interp_proof_instr (get_its_info gl) sigma env glob_instr in - let lock_focus = is_focussing_instr instr.instr in - let marker= Proof_instr (lock_focus,instr) in - solve_nth_pftreestate 1 - (abstract_operation marker (tclTHEN (eval_instr instr) clean_tmp)) pts1 - else pts1 in - postprocess pts2 raw_instr.instr - -let proof_instr raw_instr = - Pfedit.mutate (do_instr raw_instr) - -(* - -(* 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/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli deleted file mode 100644 index 1cfcfedf14..0000000000 --- a/tactics/decl_proof_instr.mli +++ /dev/null @@ -1,119 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -open Refiner -open Names -open Term -open Tacmach -open Decl_mode - -val go_to_proof_mode: unit -> unit -val return_from_tactic_mode: unit -> unit - -val register_automation_tac: tactic -> unit - -val automation_tac : tactic - -val daimon_subtree: pftreestate -> pftreestate - -val concl_refiner: - Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr - -val do_instr: Decl_expr.raw_proof_instr -> pftreestate -> pftreestate -val proof_instr: Decl_expr.raw_proof_instr -> unit - -val tcl_change_info : Decl_mode.pm_info -> tactic - -val mark_proof_tree_as_done : Proof_type.proof_tree -> Proof_type.proof_tree - -val mark_as_done : pftreestate -> pftreestate - -val execute_cases : - Names.name -> - Decl_mode.per_info -> - (Term.constr -> Proof_type.tactic) -> - (Names.Idset.elt * (Term.constr option * Term.constr list) list) list -> - Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic - -val tree_of_pats : - identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list -> - split_tree - -val add_branch : - identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list -> - split_tree -> split_tree - -val append_branch : - identifier *(int * int) -> int -> (Rawterm.cases_pattern*recpath) list list -> - (Names.Idset.t * Decl_mode.split_tree) option -> - (Names.Idset.t * Decl_mode.split_tree) option - -val append_tree : - identifier * (int * int) -> int -> (Rawterm.cases_pattern*recpath) list list -> - split_tree -> split_tree - -val build_dep_clause : Term.types Decl_expr.statement list -> - Decl_expr.proof_pattern -> - Decl_mode.per_info -> - (Term.types Decl_expr.statement, Term.types Decl_expr.or_thesis) - Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types - -val register_dep_subcase : - Names.identifier * (int * int) -> - Environ.env -> - Decl_mode.per_info -> - Rawterm.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 : pftreestate -> pftreestate - -val pop_stacks : - (Names.identifier * - (Term.constr option * Term.constr list) list) list -> - (Names.identifier * - (Term.constr option * Term.constr list) list) list - -val push_head : Term.constr -> - Names.Idset.t -> - (Names.identifier * - (Term.constr option * Term.constr list) list) list -> - (Names.identifier * - (Term.constr option * Term.constr list) list) list - -val push_arg : Term.constr -> - (Names.identifier * - (Term.constr option * Term.constr list) list) list -> - (Names.identifier * - (Term.constr option * Term.constr list) list) list - -val hrec_for: - Names.identifier -> - Decl_mode.per_info -> Proof_type.goal Tacmach.sigma -> - Names.identifier -> Term.constr - -val consider_match : - bool -> - (Names.Idset.elt*bool) list -> - Names.Idset.elt list -> - (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list -> - Proof_type.tactic - -val init_tree: - Names.Idset.t -> - Names.inductive -> - int option * Declarations.wf_paths -> - (int -> - (int option * Declarations.recarg Rtree.t) array -> - (Names.Idset.t * Decl_mode.split_tree) option) -> - Decl_mode.split_tree - -val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index b0fef2b71b..49af8b40ea 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -19,7 +19,6 @@ open Termops open Sign open Reduction open Proof_type -open Proof_trees open Declarations open Tacticals open Tacmach @@ -170,7 +169,7 @@ let find_first_goal gls = type search_state = { depth : int; (*r depth of search before failing *) - tacres : goal list sigma * validation; + tacres : goal list sigma; last_tactic : std_ppcmds; dblist : Auto.hint_db list; localdb : Auto.hint_db list } @@ -179,7 +178,7 @@ module SearchProblem = struct type state = search_state - let success s = (sig_it (fst s.tacres)) = [] + let success s = (sig_it s.tacres) = [] let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) @@ -187,7 +186,7 @@ module SearchProblem = struct let evars = Evarutil.nf_evars (Refiner.project gls) in prlist (pr_ev evars) (sig_it gls) - let filter_tactics (glls,v) l = + let filter_tactics glls l = (* let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) (* let evars = Evarutil.nf_evars (Refiner.project glls) in *) (* msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *) @@ -195,11 +194,10 @@ module SearchProblem = struct | [] -> [] | (tac,pptac) :: tacl -> try - let (lgls,ptl) = apply_tac_list tac glls in - let v' p = v (ptl p) in + let lgls = apply_tac_list tac glls in (* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) - ((lgls,v'),pptac) :: aux tacl + (lgls,pptac) :: aux tacl with e -> Refiner.catch_failerror e; aux tacl in aux l @@ -207,14 +205,14 @@ module SearchProblem = struct number of remaining goals. *) let compare s s' = let d = s'.depth - s.depth in - let nbgoals s = List.length (sig_it (fst s.tacres)) in + let nbgoals s = List.length (sig_it s.tacres) in if d <> 0 then d else nbgoals s - nbgoals s' let branching s = if s.depth = 0 then [] else - let lg = fst s.tacres in + let lg = s.tacres in let nbgl = List.length (sig_it lg) in assert (nbgl > 0); let g = find_first_goal lg in @@ -232,7 +230,7 @@ module SearchProblem = struct in let intro_tac = List.map - (fun ((lgls,_) as res,pp) -> + (fun (lgls as res,pp) -> let g' = first_goal lgls in let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') @@ -248,7 +246,7 @@ module SearchProblem = struct filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) in List.map - (fun ((lgls,_) as res, pp) -> + (fun (lgls as res, pp) -> let nbgl' = List.length (sig_it lgls) in if nbgl' < nbgl then { depth = s.depth; tacres = res; last_tactic = pp; diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 0d1699b1cf..d5e4ca17d7 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -29,7 +29,6 @@ open Auto open Pattern open Matching open Hipattern -open Proof_trees open Proof_type open Tacmach open Coqlib diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index ad392c7d84..906c32c57a 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -33,9 +33,9 @@ let instantiate n (ist,rawc) ido gl = let sigma = gl.sigma in let evl = match ido with - ConclLocation () -> evar_list sigma gl.it.evar_concl + ConclLocation () -> evar_list sigma (pf_concl gl) | HypLocation (id,hloc) -> - let decl = Environ.lookup_named_val id gl.it.evar_hyps in + let decl = Environ.lookup_named_val id (Goal.V82.hyps sigma (sig_it gl)) in match hloc with InHyp -> (match decl with diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 9aec0e0914..b6112c34fb 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -21,7 +21,6 @@ open Reductionops open Inductiveops open Evd open Environ -open Proof_trees open Clenv open Pattern open Matching diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index d98d2a2b36..9b04a2cd27 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -15,7 +15,6 @@ open Term open Sign open Evd open Pattern -open Proof_trees open Coqlib (*i*) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index d0f6e82263..395a7c206e 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -24,7 +24,6 @@ open Entries open Inductiveops open Environ open Tacmach -open Proof_trees open Proof_type open Pfedit open Evar_refiner @@ -217,29 +216,31 @@ let inversion_scheme env sigma t sort dep_option inv_op = errorlabstrm "lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) - let invSign = named_context_val invEnv in - let pfs = mk_pftreestate (mk_goal invSign invGoal None) in - let pfs = solve_pftreestate (tclTHEN intro (onLastHypId inv_op)) pfs in - let (pfterm,meta_types) = extract_open_pftreestate pfs in + let pf = Proof.start [invEnv,invGoal] in + Proof.run_tactic env (Proofview.V82.tactic (tclTHEN intro (onLastHypId inv_op))) pf; + let pfterm = List.hd (Proof.partial_proof pf) in let global_named_context = Global.named_context () in - let ownSign = + let ownSign = ref begin fold_named_context (fun env (id,_,_ as d) sign -> if mem_named_context id global_named_context then sign else add_named_decl d sign) invEnv ~init:empty_named_context - in - let (_,ownSign,mvb) = - List.fold_left - (fun (avoid,sign,mvb) (mv,mvty) -> - let h = next_ident_away (id_of_string "H") avoid in - (h::avoid, add_named_decl (h,None,mvty) sign, (mv,mkVar h)::mvb)) - (ids_of_context invEnv, ownSign, []) - meta_types + end in + let avoid = ref [] in + let { sigma=sigma } = Proof.V82.subgoals pf in + let rec fill_holes c = + match kind_of_term c with + | Evar (e,_) -> + let h = next_ident_away (id_of_string "H") !avoid in + let ty = (Evd.find sigma e).evar_concl in + avoid := h::!avoid; + ownSign := add_named_decl (h,None,ty) !ownSign; + mkVar h + | _ -> map_constr fill_holes c in let invProof = - it_mkNamedLambda_or_LetIn - (local_strong (fun _ -> whd_meta mvb) Evd.empty pfterm) ownSign + it_mkNamedLambda_or_LetIn (fill_holes pfterm) !ownSign in invProof @@ -255,26 +256,17 @@ let add_inversion_lemma name env sigma t sort dep inv_op = IsProof Lemma) in () -(* open Pfedit *) - (* inv_op = Inv (derives de complete inv. lemma) * inv_op = InvNoThining (derives de semi inversion lemma) *) let inversion_lemma_from_goal n na (loc,id) sort dep_option inv_op = let pts = get_pftreestate() in - let gl = nth_goal_of_pftreestate n pts in + let { it=gls ; sigma=sigma } = Proof.V82.subgoals pts in + let gl = { it = List.nth gls (n-1) ; sigma=sigma } in let t = try pf_get_hyp_typ gl id with Not_found -> Pretype_errors.error_var_not_found_loc loc id in let env = pf_env gl and sigma = project gl in -(* Pourquoi ??? - let fv = global_vars env t in - let thin_ids = thin_ids (hyps,fv) in - if not(list_subset thin_ids fv) then - errorlabstrm "lemma_inversion" - (str"Cannot compute lemma inversion when there are" ++ spc () ++ - str"free variables in the types of an inductive" ++ spc () ++ - str"which are not free in its instance."); *) add_inversion_lemma na env sigma t sort dep_option inv_op let add_inversion_lemma_exn na com comsort bool tac = diff --git a/tactics/refine.ml b/tactics/refine.ml index 67a73b9be5..cb6cb961f4 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -382,5 +382,3 @@ let refine (evd,c) gl = complicated to update meta types when passing through a binder *) let th = compute_metamap (pf_env gl) evd c in tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl - -let _ = Decl_proof_instr.set_refine refine (* dirty trick to solve circular dependency *) diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index e08e5e9ede..1af2d33988 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -21,7 +21,6 @@ open Termops open Sign open Reduction open Proof_type -open Proof_trees open Declarations open Tacticals open Tacmach @@ -569,7 +568,7 @@ let apply_rule hypinfo loccs : strategy = if eq_constr t c2 then Some None else let goalevars = Evd.evar_merge (fst evars) - (Evd.undefined_evars (Evarutil.nf_evar_map env'.evd)) + (Evd.undefined_evars env'.evd) in let res = { rew_car = ty; rew_from = c1; rew_to = c2; rew_prf = RewPrf (rel, prf); rew_evars = goalevars, snd evars } @@ -908,8 +907,8 @@ module Strategies = let hints (db : string) : strategy = fun env sigma t ty cstr evars -> - let rules = Autorewrite.find_matches db t in - lemmas (List.map (fun hint -> (inj_open hint.Autorewrite.rew_lemma, hint.Autorewrite.rew_l2r)) rules) + let rules = Autorewrite.find_matches db t in + lemmas (List.map (fun hint -> (inj_open hint.Autorewrite.rew_lemma, hint.Autorewrite.rew_l2r)) rules) env sigma t ty cstr evars let reduce (r : Redexpr.red_expr) : strategy = @@ -1051,8 +1050,8 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = change_in_concl None newt) in let evartac = - if not (undef = Evd.empty) then - Refiner.tclEVARS undef + if not (Evd.is_empty undef) then + Refiner.tclEVARS evars else tclIDTAC in tclTHENLIST [evartac; rewtac] gl with @@ -1575,9 +1574,10 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = let meta = Evarutil.new_meta() in let hypinfo, strat = apply_lemma gl c cl l2r occs in try - tclTHEN - (Refiner.tclEVARS hypinfo.cl.evd) - (cl_rewrite_clause_aux ~abs:hypinfo.abs strat meta cl) gl + tclWEAK_PROGRESS + (tclTHEN + (Refiner.tclEVARS hypinfo.cl.evd) + (cl_rewrite_clause_aux ~abs:hypinfo.abs strat meta cl)) gl with RewriteFailure -> let {l2r=l2r; c1=x; c2=y} = hypinfo in raise (Pretype_errors.PretypeError diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0e352110a0..6e3957ac05 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -73,7 +73,7 @@ type ltac_type = (* Values for interpretation *) type value = - | VRTactic of (goal list sigma * validation) (* For Match results *) + | VRTactic of (goal list sigma) (* For Match results *) (* Not a true value *) | VFun of ltac_trace * (identifier*value) list * identifier option list * glob_tactic_expr @@ -347,11 +347,6 @@ let vars_of_ist (lfun,_,_,env) = List.fold_left (fun s id -> Idset.add id s) (vars_of_env env) lfun -let get_current_context () = - try Pfedit.get_current_goal_context () - with e when Logic.catchable_exception e -> - (Evd.empty, Global.env()) - let strict_check = ref false let adjust_loc loc = if !strict_check then dloc else loc @@ -1794,11 +1789,11 @@ let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c) let pack_sigma (sigma,c) = {it=c;sigma=sigma} -let extend_gl_hyps gl sign = - { gl with - it = { gl.it with - evar_hyps = - List.fold_right Environ.push_named_context_val sign gl.it.evar_hyps } } +let extend_gl_hyps { it=gl ; sigma=sigma } sign = + let hyps = Goal.V82.hyps sigma gl in + let new_hyps = List.fold_right Environ.push_named_context_val sign hyps in + (* spiwack: (2010/01/13) if a bug was reintroduced in [change] in is probably here *) + Goal.V82.new_goal_with sigma gl new_hyps (* Interprets an l-tac expression into a value *) let rec val_interp ist gl (tac:glob_tactic_expr) = @@ -1988,6 +1983,8 @@ and interp_letin ist gl llc u = (* Interprets the Match Context expressions *) and interp_match_goal ist goal lz lr lmr = + let (gl,sigma) = Goal.V82.nf_evar (project goal) (sig_it goal) in + let goal = { it = gl ; sigma = sigma } in let hyps = pf_hyps goal in let hyps = if lr then List.rev hyps else hyps in let concl = pf_concl goal in diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index fe4e9f6aab..71ee29f8cc 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -25,7 +25,7 @@ open Redexpr (* Values for interpretation *) type value = - | VRTactic of (goal list sigma * validation) + | VRTactic of (goal list sigma) | VFun of ltac_trace * (identifier*value) list * identifier option list * glob_tactic_expr | VVoid diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 332855052d..045f70c61b 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -61,8 +61,8 @@ let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE let tclFAIL = Refiner.tclFAIL let tclFAIL_lazy = Refiner.tclFAIL_lazy let tclDO = Refiner.tclDO -let tclPROGRESS = Refiner.tclPROGRESS let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS +let tclPROGRESS = Refiner.tclPROGRESS let tclNOTSAMEGOAL = Refiner.tclNOTSAMEGOAL let tclTHENTRY = Refiner.tclTHENTRY let tclIFTHENELSE = Refiner.tclIFTHENELSE diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index b9c8ab928b..3dd73c92c3 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -55,8 +55,8 @@ val tclAT_LEAST_ONCE : tactic -> tactic val tclFAIL : int -> std_ppcmds -> tactic val tclFAIL_lazy : int -> std_ppcmds Lazy.t -> tactic val tclDO : int -> tactic -> tactic -val tclPROGRESS : tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic +val tclPROGRESS : tactic -> tactic val tclNOTSAMEGOAL : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclMAP : ('a -> tactic) -> 'a list -> tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 41fab4e716..e6201aad9d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -27,7 +27,6 @@ open Pfedit open Tacred open Rawterm open Tacmach -open Proof_trees open Proof_type open Logic open Evar_refiner @@ -516,8 +515,8 @@ let intro_move idopt hto = match idopt with | Some id -> intro_gen dloc (IntroMustBe id) hto true false let pf_lookup_hypothesis_as_renamed env ccl = function - | AnonHyp n -> pf_lookup_index_as_renamed env ccl n - | NamedHyp id -> pf_lookup_name_as_displayed env ccl id + | AnonHyp n -> Detyping.lookup_index_as_renamed env ccl n + | NamedHyp id -> Detyping.lookup_name_as_displayed env ccl id let pf_lookup_hypothesis_as_renamed_gen red h gl = let env = pf_env gl in @@ -614,7 +613,7 @@ let bring_hyps hyps = let resolve_classes gl = let env = pf_env gl and evd = project gl in - if evd = Evd.empty then tclIDTAC gl + if Evd.is_empty evd then tclIDTAC gl else let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in (tclTHEN (tclEVARS evd') tclNORMEVAR) gl diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index b885b15243..333d6a3a21 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -19,6 +19,4 @@ Leminv Tacinterp Evar_tactics Autorewrite -Decl_interp -Decl_proof_instr Tactic_option |