diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 1175 | ||||
| -rw-r--r-- | proofs/clenv.mli | 142 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 97 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 26 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 181 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 41 | ||||
| -rw-r--r-- | proofs/logic.ml | 452 | ||||
| -rw-r--r-- | proofs/logic.mli | 22 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 54 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 17 | ||||
| -rw-r--r-- | proofs/proof_trees.ml | 173 | ||||
| -rw-r--r-- | proofs/proof_trees.mli | 28 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 10 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 10 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 112 | ||||
| -rw-r--r-- | proofs/redexpr.mli | 35 | ||||
| -rw-r--r-- | proofs/refiner.ml | 198 | ||||
| -rw-r--r-- | proofs/refiner.mli | 25 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 77 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 50 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 30 | ||||
| -rw-r--r-- | proofs/tactic_debug.ml | 36 | ||||
| -rw-r--r-- | proofs/tactic_debug.mli | 12 |
23 files changed, 655 insertions, 2348 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml deleted file mode 100644 index 999bb651..00000000 --- a/proofs/clenv.ml +++ /dev/null @@ -1,1175 +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: clenv.ml,v 1.97.2.4 2004/12/06 12:59:11 herbelin Exp $ *) - -open Pp -open Util -open Names -open Nameops -open Term -open Termops -open Sign -open Instantiate -open Environ -open Evd -open Proof_type -open Refiner -open Proof_trees -open Logic -open Reductionops -open Tacmach -open Evar_refiner -open Rawterm -open Pattern -open Tacexpr - -(* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms, - gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *) - -let abstract_scheme env c l lname_typ = - List.fold_left2 - (fun t (locc,a) (na,_,ta) -> - let na = match kind_of_term a with Var id -> Name id | _ -> na in - if occur_meta ta then error "cannot find a type for the generalisation" - else if occur_meta a then lambda_name env (na,ta,t) - else lambda_name env (na,ta,subst_term_occ locc a t)) - c - (List.rev l) - lname_typ - -let abstract_list_all env sigma typ c l = - let ctxt,_ = decomp_n_prod env sigma (List.length l) typ in - let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in - try - if is_conv_leq env sigma (Typing.type_of env sigma p) typ then p - else error "abstract_list_all" - with UserError _ -> - raise (RefinerError (CannotGeneralize typ)) - -(* Generator of metavariables *) -let new_meta = - let meta_ctr = ref 0 in - fun () -> incr meta_ctr; !meta_ctr - -(* replaces a mapping of existentials into a mapping of metas. - Problem if an evar appears in the type of another one (pops anomaly) *) -let exist_to_meta sigma (emap, c) = - let metamap = ref [] in - let change_exist evar = - let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in - let n = new_meta() in - metamap := (n, ty) :: !metamap; - mkCast (mkMeta n, ty) in - let rec replace c = - match kind_of_term c with - Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev - | _ -> map_constr replace c in - (!metamap, replace c) - -module Metaset = Intset - -module Metamap = Intmap - -let meta_exists p s = Metaset.fold (fun x b -> (p x) || b) s false - -let metamap_in_dom x m = - try let _ = Metamap.find x m in true with Not_found -> false - -let metamap_to_list m = - Metamap.fold (fun n v l -> (n,v)::l) m [] - -let metamap_inv m b = - Metamap.fold (fun n v l -> if v = b then n::l else l) m [] - -type 'a freelisted = { - rebus : 'a; - freemetas : Metaset.t } - -(* collects all metavar occurences, in left-to-right order, preserving - * repetitions and all. *) - -let collect_metas c = - let rec collrec acc c = - match kind_of_term c with - | Meta mv -> mv::acc - | _ -> fold_constr collrec acc c - in - List.rev (collrec [] c) - -let metavars_of c = - let rec collrec acc c = - match kind_of_term c with - | Meta mv -> Metaset.add mv acc - | _ -> fold_constr collrec acc c - in - collrec Metaset.empty c - -let mk_freelisted c = - { rebus = c; freemetas = metavars_of c } - - -(* Clausal environments *) - -type clbinding = - | Cltyp of constr freelisted - | Clval of constr freelisted * constr freelisted - -type 'a clausenv = { - templval : constr freelisted; - templtyp : constr freelisted; - namenv : identifier Metamap.t; - env : clbinding Metamap.t; - hook : 'a } - -type wc = named_context sigma - - -(* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions - * mv0, or if one of the free vars on mv1's freelist mentions - * mv0 *) - -let mentions clenv mv0 = - let rec menrec mv1 = - try - (match Metamap.find mv1 clenv.env with - | Clval (b,_) -> - Metaset.mem mv0 b.freemetas || meta_exists menrec b.freemetas - | Cltyp _ -> false) - with Not_found -> - false - in - menrec - -(* Creates a new clause-environment, whose template has a given - * type, CTY. This is not all that useful, since not very often - * does one know the type of the clause - one usually only has - * a clause which one wants to backchain thru. *) - -let mk_clenv wc cty = - let mv = new_meta () in - let cty_fls = mk_freelisted cty in - { templval = mk_freelisted (mkMeta mv); - templtyp = cty_fls; - namenv = Metamap.empty; - env = Metamap.add mv (Cltyp cty_fls) Metamap.empty ; - hook = wc } - -let clenv_environments bound c = - let rec clrec (ne,e,metas) n c = - match n, kind_of_term c with - | (Some 0, _) -> (ne, e, List.rev metas, c) - | (n, Cast (c,_)) -> clrec (ne,e,metas) n c - | (n, Prod (na,c1,c2)) -> - let mv = new_meta () in - let dep = dependent (mkRel 1) c2 in - let ne' = - if dep then - match na with - | Anonymous -> ne - | Name id -> - if metamap_in_dom mv ne then begin - warning ("Cannot put metavar "^(string_of_meta mv)^ - " in name-environment twice"); - ne - end else - Metamap.add mv id ne - else - ne - in - let e' = Metamap.add mv (Cltyp (mk_freelisted c1)) e in - clrec (ne',e', (mkMeta mv)::metas) (option_app ((+) (-1)) n) - (if dep then (subst1 (mkMeta mv) c2) else c2) - | (n, LetIn (na,b,_,c)) -> - clrec (ne,e,metas) (option_app ((+) (-1)) n) (subst1 b c) - | (n, _) -> (ne, e, List.rev metas, c) - in - clrec (Metamap.empty,Metamap.empty,[]) bound c - -let mk_clenv_from_n wc n (c,cty) = - let (namenv,env,args,concl) = clenv_environments n cty in - { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args)); - templtyp = mk_freelisted concl; - namenv = namenv; - env = env; - hook = wc } - -let mk_clenv_from wc = mk_clenv_from_n wc None - -let map_fl f cfl = { cfl with rebus=f cfl.rebus } - -let map_clb f = function - | Cltyp cfl -> Cltyp (map_fl f cfl) - | Clval (cfl1,cfl2) -> Clval (map_fl f cfl1,map_fl f cfl2) - -let subst_clenv f sub clenv = - { templval = map_fl (subst_mps sub) clenv.templval; - templtyp = map_fl (subst_mps sub) clenv.templtyp; - namenv = clenv.namenv; - env = Metamap.map (map_clb (subst_mps sub)) clenv.env; - hook = f sub clenv.hook } - -let connect_clenv wc clenv = { clenv with hook = wc } - -(* Was used in wcclausenv.ml -(* Changes the head of a clenv with (templ,templty) *) -let clenv_change_head (templ,templty) clenv = - { templval = mk_freelisted templ; - templtyp = mk_freelisted templty; - namenv = clenv.namenv; - env = clenv.env; - hook = clenv.hook } -*) - -let mk_clenv_hnf_constr_type_of wc t = - mk_clenv_from wc (t,w_hnf_constr wc (w_type_of wc t)) - -let mk_clenv_rename_from wc (c,t) = - mk_clenv_from wc (c,rename_bound_var (w_env wc) [] t) - -let mk_clenv_rename_from_n wc n (c,t) = - mk_clenv_from_n wc n (c,rename_bound_var (w_env wc) [] t) - -let mk_clenv_rename_type_of wc t = - mk_clenv_from wc (t,rename_bound_var (w_env wc) [] (w_type_of wc t)) - -let mk_clenv_rename_hnf_constr_type_of wc t = - mk_clenv_from wc - (t,rename_bound_var (w_env wc) [] (w_hnf_constr wc (w_type_of wc t))) - -let mk_clenv_type_of wc t = mk_clenv_from wc (t,w_type_of wc t) - -let clenv_assign mv rhs clenv = - let rhs_fls = mk_freelisted rhs in - if meta_exists (mentions clenv mv) rhs_fls.freemetas then - error "clenv__assign: circularity in unification"; - try - (match Metamap.find mv clenv.env with - | Clval (fls,ty) -> - if not (eq_constr fls.rebus rhs) then - try - (* Streams are lazy, force evaluation of id to catch Not_found*) - let id = Metamap.find mv clenv.namenv in - errorlabstrm "clenv_assign" - (str "An incompatible instantiation has already been found for " ++ - pr_id id) - with Not_found -> - anomaly "clenv_assign: non dependent metavar already assigned" - else - clenv - | Cltyp bty -> - { templval = clenv.templval; - templtyp = clenv.templtyp; - namenv = clenv.namenv; - env = Metamap.add mv (Clval (rhs_fls,bty)) clenv.env; - hook = clenv.hook }) - with Not_found -> - error "clenv_assign" - -let clenv_val_of clenv mv = - let rec valrec mv = - try - (match Metamap.find mv clenv.env with - | Cltyp _ -> mkMeta mv - | Clval(b,_) -> - instance (List.map (fun mv' -> (mv',valrec mv')) - (Metaset.elements b.freemetas)) b.rebus) - with Not_found -> - mkMeta mv - in - valrec mv - -let clenv_instance clenv b = - let c_sigma = - List.map - (fun mv -> (mv,clenv_val_of clenv mv)) (Metaset.elements b.freemetas) - in - instance c_sigma b.rebus - -let clenv_instance_term clenv c = - clenv_instance clenv (mk_freelisted c) - - -(* This function put casts around metavariables whose type could not be - * infered by the refiner, that is head of applications, predicates and - * subject of Cases. - * Does check that the casted type is closed. Anyway, the refiner would - * fail in this case... *) - -let clenv_cast_meta clenv = - let rec crec u = - match kind_of_term u with - | App _ | Case _ -> crec_hd u - | Cast (c,_) when isMeta c -> u - | _ -> map_constr crec u - - and crec_hd u = - match kind_of_term (strip_outer_cast u) with - | Meta mv -> - (try - match Metamap.find mv clenv.env with - | Cltyp b -> - let b' = clenv_instance clenv b in - if occur_meta b' then u else mkCast (mkMeta mv, b') - | Clval(_) -> u - with Not_found -> - u) - | App(f,args) -> mkApp (crec_hd f, Array.map crec args) - | Case(ci,p,c,br) -> - mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) - | _ -> u - in - crec - - -(* [clenv_pose (na,mv,cty) clenv] - * returns a new clausenv which has added to it the metavar MV, - * with type CTY. the name NA, if it is not ANONYMOUS, will - * be entered into the name-map, as a way of accessing the new - * metavar. *) - -let clenv_pose (na,mv,cty) clenv = - { templval = clenv.templval; - templtyp = clenv.templtyp; - env = Metamap.add mv (Cltyp (mk_freelisted cty)) clenv.env; - namenv = (match na with - | Anonymous -> clenv.namenv - | Name id -> Metamap.add mv id clenv.namenv); - hook = clenv.hook } - -let clenv_defined clenv mv = - match Metamap.find mv clenv.env with - | Clval _ -> true - | Cltyp _ -> false - -let clenv_value clenv mv = - match Metamap.find mv clenv.env with - | Clval(b,_) -> b - | Cltyp _ -> failwith "clenv_value" - -let clenv_type clenv mv = - match Metamap.find mv clenv.env with - | Cltyp b -> b - | Clval(_,b) -> b - -let clenv_template clenv = clenv.templval - -let clenv_template_type clenv = clenv.templtyp - -let clenv_instance_value clenv mv = - clenv_instance clenv (clenv_value clenv mv) - -let clenv_instance_type clenv mv = - clenv_instance clenv (clenv_type clenv mv) - -let clenv_instance_template clenv = - clenv_instance clenv (clenv_template clenv) - -let clenv_instance_template_type clenv = - clenv_instance clenv (clenv_template_type clenv) - -let clenv_wtactic wt clenv = - { templval = clenv.templval; - templtyp = clenv.templtyp; - namenv = clenv.namenv; - env = clenv.env; - hook = wt clenv.hook } - -let clenv_type_of ce c = - let metamap = - List.map - (function - | (n,Clval(_,typ)) -> (n,typ.rebus) - | (n,Cltyp typ) -> (n,typ.rebus)) - (metamap_to_list ce.env) - in - Retyping.get_type_of_with_meta (w_env ce.hook) (w_Underlying ce.hook) metamap c - -let clenv_instance_type_of ce c = - clenv_instance ce (mk_freelisted (clenv_type_of ce c)) - - - -(* Unification à l'ordre 0 de m et n: [unify_0 mc wc m n] renvoie deux listes: - - metasubst:(int*constr)list récolte les instances des (Meta k) - evarsubst:(constr*constr)list récolte les instances des (Const "?k") - - Attention : pas d'unification entre les différences instances d'une - même meta ou evar, il peut rester des doublons *) - -(* Unification order: *) -(* Left to right: unifies first argument and then the other arguments *) -(*let unify_l2r x = List.rev x -(* Right to left: unifies last argument and then the other arguments *) -let unify_r2l x = x - -let sort_eqns = unify_r2l -*) - -let unify_0 cv_pb wc m n = - let env = w_env wc - and sigma = w_Underlying wc in - let trivial_unify pb substn m n = - if (not(occur_meta m)) & is_fconv pb env sigma m n then substn - else error_cannot_unify (m,n) in - let rec unirec_rec pb ((metasubst,evarsubst) as substn) m n = - let cM = Evarutil.whd_castappevar sigma m - and cN = Evarutil.whd_castappevar sigma n in - match (kind_of_term cM,kind_of_term cN) with - | Meta k1, Meta k2 -> - if k1 < k2 then (k1,cN)::metasubst,evarsubst - else if k1 = k2 then substn - else (k2,cM)::metasubst,evarsubst - | Meta k, _ -> (k,cN)::metasubst,evarsubst - | _, Meta k -> (k,cM)::metasubst,evarsubst - | Evar _, _ -> metasubst,((cM,cN)::evarsubst) - | _, Evar _ -> metasubst,((cN,cM)::evarsubst) - - | Lambda (_,t1,c1), Lambda (_,t2,c2) -> - unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2 - | Prod (_,t1,c1), Prod (_,t2,c2) -> - unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2 - | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN - | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c) - - | App (f1,l1), App (f2,l2) -> - let len1 = Array.length l1 - and len2 = Array.length l2 in - let (f1,l1,f2,l2) = - if len1 = len2 then (f1,l1,f2,l2) - else if len1 < len2 then - let extras,restl2 = array_chop (len2-len1) l2 in - (f1, l1, appvect (f2,extras), restl2) - else - let extras,restl1 = array_chop (len1-len2) l1 in - (appvect (f1,extras), restl1, f2, l2) in - (try - array_fold_left2 (unirec_rec CONV) - (unirec_rec CONV substn f1 f2) l1 l2 - with ex when catchable_exception ex -> - trivial_unify pb substn cM cN) - | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> - array_fold_left2 (unirec_rec CONV) - (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2 - - | _ -> trivial_unify pb substn cM cN - - in - if (not(occur_meta m)) & is_fconv cv_pb env sigma m n then - ([],[]) - else - let (mc,ec) = unirec_rec cv_pb ([],[]) m n in - ((*sort_eqns*) mc, (*sort_eqns*) ec) - - -(* Unification - * - * Procedure: - * (1) The function [unify mc wc M N] produces two lists: - * (a) a list of bindings Meta->RHS - * (b) a list of bindings EVAR->RHS - * - * The Meta->RHS bindings cannot themselves contain - * meta-vars, so they get applied eagerly to the other - * bindings. This may or may not close off all RHSs of - * the EVARs. For each EVAR whose RHS is closed off, - * we can just apply it, and go on. For each which - * is not closed off, we need to do a mimick step - - * in general, we have something like: - * - * ?X == (c e1 e2 ... ei[Meta(k)] ... en) - * - * so we need to do a mimick step, converting ?X - * into - * - * ?X -> (c ?z1 ... ?zn) - * - * of the proper types. Then, we can decompose the - * equation into - * - * ?z1 --> e1 - * ... - * ?zi --> ei[Meta(k)] - * ... - * ?zn --> en - * - * and keep on going. Whenever we find that a R.H.S. - * is closed, we can, as before, apply the constraint - * directly. Whenever we find an equation of the form: - * - * ?z -> Meta(n) - * - * we can reverse the equation, put it into our metavar - * substitution, and keep going. - * - * The most efficient mimick possible is, for each - * Meta-var remaining in the term, to declare a - * new EVAR of the same type. This is supposedly - * determinable from the clausale form context - - * we look up the metavar, take its type there, - * and apply the metavar substitution to it, to - * close it off. But this might not always work, - * since other metavars might also need to be resolved. *) - -let applyHead n c wc = - let rec apprec n c cty wc = - if n = 0 then - (wc,c) - else - match kind_of_term (w_whd_betadeltaiota wc cty) with - | Prod (_,c1,c2) -> - let evar = Evarutil.new_evar_in_sign (w_env wc) in - let (evar_n, _) = destEvar evar in - (compose - (apprec (n-1) (applist(c,[evar])) (subst1 evar c2)) - (w_Declare evar_n c1)) - wc - | _ -> error "Apply_Head_Then" - in - apprec n c (w_type_of wc c) wc - -let is_mimick_head f = - match kind_of_term f with - (Const _|Var _|Rel _|Construct _|Ind _) -> true - | _ -> false - -let rec mimick_evar hdc nargs sp wc = - let evd = Evd.map wc.sigma sp in - let wc' = extract_decl sp wc in - let (wc'', c) = applyHead nargs hdc wc' in - let (mc,ec) = unify_0 CONV wc'' (w_type_of wc'' c) (evd.evar_concl) in - let (wc''',_) = w_resrec mc ec wc'' in - if wc'== wc''' - then w_Define sp c wc - else - let wc'''' = restore_decl sp evd wc''' in - w_Define sp (Evarutil.nf_evar wc''''.sigma c) {it = wc.it ; sigma = wc''''.sigma} - -and w_Unify cv_pb m n wc = - let (mc',ec') = unify_0 cv_pb wc m n in - w_resrec mc' ec' wc - -and w_resrec metas evars wc = - match evars with - | [] -> (wc,metas) - - | (lhs,rhs) :: t -> - match kind_of_term rhs with - - | Meta k -> w_resrec ((k,lhs)::metas) t wc - - | krhs -> - match kind_of_term lhs with - - | Evar (evn,_) -> - if w_defined_evar wc evn then - let (wc',metas') = w_Unify CONV rhs lhs wc in - w_resrec (metas@metas') t wc' - else - (try - w_resrec metas t (w_Define evn rhs wc) - with ex when catchable_exception ex -> - (match krhs with - | App (f,cl) when is_mimick_head f -> - let wc' = mimick_evar f (Array.length cl) evn wc in - w_resrec metas evars wc' - | _ -> raise ex (*error "w_Unify" *))) - | _ -> anomaly "w_resrec" - - -(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en - particulier ne semblent pas vérifier que des instances différentes - d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas - provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) - -(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) -let unifyTerms m n gls = - tclIDTAC {it = gls.it; - sigma = (get_gc (fst (w_Unify CONV m n (Refiner.project_with_focus gls))))} - -let unify m gls = - let n = pf_concl gls in unifyTerms m n gls - -(* [clenv_merge b metas evars clenv] merges common instances in metas - or in evars, possibly generating new unification problems; if [b] - is true, unification of types of metas is required *) - -let clenv_merge with_types metas evars clenv = - let ty_metas = ref [] in - let ty_evars = ref [] in - let rec clenv_resrec metas evars clenv = - match (evars,metas) with - | ([], []) -> clenv - - | ((lhs,rhs)::t, metas) -> - (match kind_of_term rhs with - - | Meta k -> clenv_resrec ((k,lhs)::metas) t clenv - - | krhs -> - (match kind_of_term lhs with - - | Evar (evn,_) -> - if w_defined_evar clenv.hook evn then - let (metas',evars') = unify_0 CONV clenv.hook rhs lhs in - clenv_resrec (metas'@metas) (evars'@t) clenv - else begin - let rhs' = - if occur_meta rhs then subst_meta metas rhs else rhs - in - if occur_evar evn rhs' then error "w_Unify"; - try - clenv_resrec metas t - (clenv_wtactic (w_Define evn rhs') clenv) - with ex when catchable_exception ex -> - (match krhs with - | App (f,cl) when is_mimick_head f -> - clenv_resrec metas evars - (clenv_wtactic - (mimick_evar f (Array.length cl) evn) - clenv) - | _ -> raise ex (********* error "w_Unify" *)) - end - - | _ -> anomaly "clenv_resrec")) - - | ([], (mv,n)::t) -> - if clenv_defined clenv mv then - let (metas',evars') = - unify_0 CONV clenv.hook (clenv_value clenv mv).rebus n in - clenv_resrec (metas'@t) evars' clenv - else - begin - if with_types (* or occur_meta mvty *) then - (let mvty = clenv_instance_type clenv mv in - try - let nty = clenv_type_of clenv - (clenv_instance clenv (mk_freelisted n)) in - let (mc,ec) = unify_0 CUMUL clenv.hook nty mvty in - ty_metas := mc @ !ty_metas; - ty_evars := ec @ !ty_evars - with e when Logic.catchable_exception e -> ()); - clenv_resrec t [] (clenv_assign mv n clenv) - end in - (* merge constraints *) - let clenv' = clenv_resrec metas evars clenv in - if with_types then - (* merge constraints about types: if they fail, don't worry *) - try clenv_resrec !ty_metas !ty_evars clenv' - with e when Logic.catchable_exception e -> clenv' - else clenv' - -(* [clenv_unify M N clenv] - performs a unification of M and N, generating a bunch of - unification constraints in the process. These constraints - are processed, one-by-one - they may either generate new - bindings, or, if there is already a binding, new unifications, - which themselves generate new constraints. This continues - until we get failure, or we run out of constraints. - [clenv_typed_unify M N clenv] expects in addition that expected - types of metavars are unifiable with the types of their instances *) - -let clenv_unify_core_0 with_types cv_pb m n clenv = - let (mc,ec) = unify_0 cv_pb clenv.hook m n in - clenv_merge with_types mc ec clenv - -let clenv_unify_0 = clenv_unify_core_0 false -let clenv_typed_unify = clenv_unify_core_0 true - - -(* takes a substitution s, an open term op and a closed term cl - try to find a subterm of cl which matches op, if op is just a Meta - FAIL because we cannot find a binding *) - -let iter_fail f a = - let n = Array.length a in - let rec ffail i = - if i = n then error "iter_fail" - else - try f a.(i) - with ex when catchable_exception ex -> ffail (i+1) - in ffail 0 - -(* Tries to find an instance of term [cl] in term [op]. - Unifies [cl] to every subterm of [op] until it finds a match. - Fails if no match is found *) -let unify_to_subterm clause (op,cl) = - let rec matchrec cl = - let cl = strip_outer_cast cl in - (try - if closed0 cl - then clenv_unify_0 CONV op cl clause,cl - else error "Bound 1" - with ex when catchable_exception ex -> - (match kind_of_term cl with - | App (f,args) -> - let n = Array.length args in - assert (n>0); - let c1 = mkApp (f,Array.sub args 0 (n-1)) in - let c2 = args.(n-1) in - (try - matchrec c1 - with ex when catchable_exception ex -> - matchrec c2) - | Case(_,_,c,lf) -> (* does not search in the predicate *) - (try - matchrec c - with ex when catchable_exception ex -> - iter_fail matchrec lf) - | LetIn(_,c1,_,c2) -> - (try - matchrec c1 - with ex when catchable_exception ex -> - matchrec c2) - - | Fix(_,(_,types,terms)) -> - (try - iter_fail matchrec types - with ex when catchable_exception ex -> - iter_fail matchrec terms) - - | CoFix(_,(_,types,terms)) -> - (try - iter_fail matchrec types - with ex when catchable_exception ex -> - iter_fail matchrec terms) - - | Prod (_,t,c) -> - (try - matchrec t - with ex when catchable_exception ex -> - matchrec c) - | Lambda (_,t,c) -> - (try - matchrec t - with ex when catchable_exception ex -> - matchrec c) - | _ -> error "Match_subterm")) - in - try matchrec cl - with ex when catchable_exception ex -> - raise (RefinerError (NoOccurrenceFound op)) - -let unify_to_subterm_list allow_K clause oplist t = - List.fold_right - (fun op (clause,l) -> - if isMeta op then - if allow_K then (clause,op::l) - else error "Match_subterm" - else if occur_meta op then - let (clause',cl) = - try - (* This is up to delta for subterms w/o metas ... *) - unify_to_subterm clause (strip_outer_cast op,t) - with RefinerError (NoOccurrenceFound _) when allow_K -> (clause,op) - in - (clause',cl::l) - else if not allow_K & not (dependent op t) then - (* This is not up to delta ... *) - raise (RefinerError (NoOccurrenceFound op)) - else - (clause,op::l)) - oplist - (clause,[]) - -let secondOrderAbstraction allow_K typ (p, oplist) clause = - let env = w_env clause.hook in - let sigma = w_Underlying clause.hook in - let (clause',cllist) = unify_to_subterm_list allow_K clause oplist typ in - let typp = clenv_instance_type clause' p in - let pred = abstract_list_all env sigma typp typ cllist in - clenv_unify_0 CONV (mkMeta p) pred clause' - -let clenv_unify2 allow_K cv_pb ty1 ty2 clause = - let c1, oplist1 = whd_stack ty1 in - let c2, oplist2 = whd_stack ty2 in - match kind_of_term c1, kind_of_term c2 with - | Meta p1, _ -> - (* Find the predicate *) - let clause' = - secondOrderAbstraction allow_K ty2 (p1,oplist1) clause in - (* Resume first order unification *) - clenv_unify_0 cv_pb (clenv_instance_term clause' ty1) ty2 clause' - | _, Meta p2 -> - (* Find the predicate *) - let clause' = - secondOrderAbstraction allow_K ty1 (p2, oplist2) clause in - (* Resume first order unification *) - clenv_unify_0 cv_pb ty1 (clenv_instance_term clause' ty2) clause' - | _ -> error "clenv_unify2" - - -(* The unique unification algorithm works like this: If the pattern is - flexible, and the goal has a lambda-abstraction at the head, then - we do a first-order unification. - - If the pattern is not flexible, then we do a first-order - unification, too. - - If the pattern is flexible, and the goal doesn't have a - lambda-abstraction head, then we second-order unification. *) - -(* We decide here if first-order or second-order unif is used for Apply *) -(* We apply a term of type (ai:Ai)C and try to solve a goal C' *) -(* The type C is in clenv.templtyp.rebus with a lot of Meta to solve *) - -(* 3-4-99 [HH] New fo/so choice heuristic : - In case we have to unify (Meta(1) args) with ([x:A]t args') - we first try second-order unification and if it fails first-order. - Before, second-order was used if the type of Meta(1) and [x:A]t was - convertible and first-order otherwise. But if failed if e.g. the type of - Meta(1) had meta-variables in it. *) -let clenv_unify allow_K cv_pb ty1 ty2 clenv = - let hd1,l1 = whd_stack ty1 in - let hd2,l2 = whd_stack ty2 in - match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with - (* Pattern case *) - | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true) - when List.length l1 = List.length l2 -> - (try - clenv_typed_unify cv_pb ty1 ty2 clenv - with ex when catchable_exception ex -> - try - clenv_unify2 allow_K cv_pb ty1 ty2 clenv - with RefinerError (NoOccurrenceFound c) as e -> raise e - | ex when catchable_exception ex -> - error "Cannot solve a second-order unification problem") - - (* Second order case *) - | (Meta _, true, _, _ | _, _, Meta _, true) -> - (try - clenv_unify2 allow_K cv_pb ty1 ty2 clenv - with RefinerError (NoOccurrenceFound c) as e -> raise e - | ex when catchable_exception ex -> - try - clenv_typed_unify cv_pb ty1 ty2 clenv - with ex when catchable_exception ex -> - error "Cannot solve a second-order unification problem") - - (* General case: try first order *) - | _ -> clenv_unify_0 cv_pb ty1 ty2 clenv - - -(* [clenv_bchain mv clenv' clenv] - * - * Resolves the value of "mv" (which must be undefined) in clenv to be - * the template of clenv' be the value "c", applied to "n" fresh - * metavars, whose types are chosen by destructing "clf", which should - * be a clausale forme generated from the type of "c". The process of - * resolution can cause unification of already-existing metavars, and - * of the fresh ones which get created. This operation is a composite - * of operations which pose new metavars, perform unification on - * terms, and make bindings. *) - -let clenv_bchain mv subclenv clenv = - (* Add the metavars of [subclenv] to [clenv], with their name-environment *) - let clenv' = - { templval = clenv.templval; - templtyp = clenv.templtyp; - namenv = - List.fold_left (fun ne (mv,id) -> - if clenv_defined subclenv mv then - ne - else if metamap_in_dom mv ne then begin - warning ("Cannot put metavar "^(string_of_meta mv)^ - " in name-environment twice"); - ne - end else - Metamap.add mv id ne) - clenv.namenv (metamap_to_list subclenv.namenv); - env = List.fold_left (fun m (n,v) -> Metamap.add n v m) - clenv.env (metamap_to_list subclenv.env); - hook = clenv.hook } - in - (* unify the type of the template of [subclenv] with the type of [mv] *) - let clenv'' = - clenv_unify true CUMUL - (clenv_instance clenv' (clenv_template_type subclenv)) - (clenv_instance_type clenv' mv) - clenv' - in - (* assign the metavar *) - let clenv''' = - clenv_assign mv (clenv_instance clenv' (clenv_template subclenv)) clenv'' - in - clenv''' - - -(* swaps the "hooks" in [clenv1] and [clenv2], so we can then use - backchain to hook them together *) - -let clenv_swap clenv1 clenv2 = - let clenv1' = { templval = clenv1.templval; - templtyp = clenv1.templtyp; - namenv = clenv1.namenv; - env = clenv1.env; - hook = clenv2.hook} - and clenv2' = { templval = clenv2.templval; - templtyp = clenv2.templtyp; - namenv = clenv2.namenv; - env = clenv2.env; - hook = clenv1.hook} - in - (clenv1',clenv2') - -let clenv_fchain mv nextclenv clenv = - let (clenv',nextclenv') = clenv_swap clenv nextclenv in - clenv_bchain mv clenv' nextclenv' - -let clenv_refine kONT clenv gls = - tclTHEN - (kONT clenv.hook) - (refine (clenv_instance_template clenv)) gls - -let clenv_refine_cast kONT clenv gls = - tclTHEN - (kONT clenv.hook) - (refine (clenv_cast_meta clenv (clenv_instance_template clenv))) - gls - -(* [clenv_metavars clenv mv] - * returns a list of the metavars which appear in the type of - * the metavar mv. The list is unordered. *) - -let clenv_metavars clenv mv = - match Metamap.find mv clenv.env with - | Clval(_,b) -> b.freemetas - | Cltyp b -> b.freemetas - -let clenv_template_metavars clenv = clenv.templval.freemetas - -(* [clenv_dependent hyps_only clenv] - * returns a list of the metavars which appear in the template of clenv, - * and which are dependent, This is computed by taking the metavars in cval, - * in right-to-left order, and collecting the metavars which appear - * in their types, and adding in all the metavars appearing in the - * type of clenv. - * If [hyps_only] then metavariables occurring in the type are _excluded_ *) - -let dependent_metas clenv mvs conclmetas = - List.fold_right - (fun mv deps -> - Metaset.union deps (clenv_metavars clenv mv)) - mvs conclmetas - -let clenv_dependent hyps_only clenv = - let mvs = collect_metas (clenv_instance_template clenv) in - let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in - let deps = dependent_metas clenv mvs ctyp_mvs in - List.filter - (fun mv -> Metaset.mem mv deps && not (hyps_only && Metaset.mem mv ctyp_mvs)) - mvs - -let clenv_missing c = clenv_dependent true c - -(* [clenv_independent clenv] - * returns a list of metavariables which appear in the term cval, - * and which are not dependent. That is, they do not appear in - * the types of other metavars which are in cval, nor in the type - * of cval, ctyp. *) - -let clenv_independent clenv = - let mvs = collect_metas (clenv_instance_template clenv) in - let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in - let deps = dependent_metas clenv mvs ctyp_mvs in - List.filter (fun mv -> not (Metaset.mem mv deps)) mvs - -let w_coerce wc c ctyp target = - let j = make_judge c ctyp in - let env = w_env wc in - let isevars = Evarutil.create_evar_defs (w_Underlying wc) in - let j' = Coercion.inh_conv_coerce_to dummy_loc env isevars j target in - (* faire quelque chose avec isevars ? *) - j'.uj_val - -let clenv_constrain_dep_args hyps_only clause = function - | [] -> clause - | mlist -> - let occlist = clenv_dependent hyps_only clause in - if List.length occlist = List.length mlist then - List.fold_left2 - (fun clenv k c -> - let wc = clause.hook in - try - let k_typ = w_hnf_constr wc (clenv_instance_type clause k) in - let c_typ = w_hnf_constr wc (w_type_of wc c) in - let c' = w_coerce wc c c_typ k_typ in - clenv_unify true CONV (mkMeta k) c' clenv - with _ -> - clenv_unify true CONV (mkMeta k) c clenv) - clause occlist mlist - else - error ("Not the right number of missing arguments (expected " - ^(string_of_int (List.length occlist))^")") - -let clenv_constrain_missing_args mlist clause = - clenv_constrain_dep_args true clause mlist - -let clenv_lookup_name clenv id = - match metamap_inv clenv.namenv id with - | [] -> - errorlabstrm "clenv_lookup_name" - (str"No such bound variable " ++ pr_id id) - | [n] -> - n - | _ -> - anomaly "clenv_lookup_name: a name occurs more than once in clause" - -let clenv_match_args s clause = - let mvs = clenv_independent clause in - let rec matchrec clause = function - | [] -> clause - | (loc,b,c)::t -> - let k = - match b with - | NamedHyp s -> - if List.exists (fun (_,b',_) -> b=b') t then - errorlabstrm "clenv_match_args" - (str "The variable " ++ pr_id s ++ - str " occurs more than once in binding") - else - clenv_lookup_name clause s - | AnonHyp n -> - if List.exists (fun (_,b',_) -> b=b') t then - errorlabstrm "clenv_match_args" - (str "The position " ++ int n ++ - str " occurs more than once in binding"); - try - List.nth mvs (n-1) - with (Failure _|Invalid_argument _) -> - errorlabstrm "clenv_match_args" (str "No such binder") - in - let k_typ = w_hnf_constr clause.hook (clenv_instance_type clause k) - (* nf_betaiota was before in type_of - useful to reduce types like *) - (* (x:A)([x]P u) *) - and c_typ = w_hnf_constr clause.hook - (nf_betaiota (w_type_of clause.hook c)) in - let cl = - (* Try to infer some Meta/Evar from the type of [c] *) - try - clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause) - with _ -> - (* Try to coerce to the type of [k]; cannot merge with the - previous case because Coercion does not handle Meta *) - let c' = w_coerce clause.hook c c_typ k_typ in - try clenv_unify true CONV (mkMeta k) c' clause - with RefinerError (CannotUnify (m,n)) -> - Stdpp.raise_with_loc loc - (RefinerError (CannotUnifyBindingType (m,n))) - in matchrec cl t - in - matchrec clause s - -type arg_bindings = (int * constr) list - -let clenv_constrain_with_bindings bl clause = - if bl = [] then - clause - else - let all_mvs = collect_metas (clenv_template clause).rebus in - let rec matchrec clause = function - | [] -> clause - | (n,c)::t -> - let k = - (try - if n > 0 then - List.nth all_mvs (n-1) - else if n < 0 then - List.nth (List.rev all_mvs) (-n-1) - else error "clenv_constrain_with_bindings" - with Failure _ -> - errorlabstrm "clenv_constrain_with_bindings" - (str"Clause did not have " ++ int n ++ str"-th" ++ - str" absolute argument")) in - let env = Global.env () in - let sigma = Evd.empty in - let k_typ = nf_betaiota (clenv_instance_type clause k) in - let c_typ = nf_betaiota (w_type_of clause.hook c) in - matchrec - (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t - in - matchrec clause bl - - -(* [clenv_pose_dependent_evars clenv] - * For each dependent evar in the clause-env which does not have a value, - * pose a value for it by constructing a fresh evar. We do this in - * left-to-right order, so that every evar's type is always closed w.r.t. - * metas. *) - -let clenv_pose_dependent_evars clenv = - let dep_mvs = clenv_dependent false clenv in - List.fold_left - (fun clenv mv -> - let evar = Evarutil.new_evar_in_sign (w_env clenv.hook) in - let (evar_n,_) = destEvar evar in - let tY = clenv_instance_type clenv mv in - let clenv' = clenv_wtactic (w_Declare evar_n tY) clenv in - clenv_assign mv evar clenv') - clenv - dep_mvs - -(***************************) - -let clenv_unique_resolver allow_K clause gl = - clenv_unify allow_K CUMUL - (clenv_instance_template_type clause) (pf_concl gl) clause - -let res_pf kONT clenv gls = - clenv_refine kONT (clenv_unique_resolver false clenv gls) gls - -let res_pf_cast kONT clenv gls = - clenv_refine_cast kONT (clenv_unique_resolver false clenv gls) gls - -let elim_res_pf kONT clenv allow_K gls = - clenv_refine_cast kONT (clenv_unique_resolver allow_K clenv gls) gls - -let elim_res_pf_THEN_i kONT clenv tac gls = - let clenv' = (clenv_unique_resolver true clenv gls) in - tclTHENLASTn (clenv_refine kONT clenv') (tac clenv') gls - -let e_res_pf kONT clenv gls = - clenv_refine kONT - (clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls - -(* Clausal environment for an application *) - -let make_clenv_binding_gen n wc (c,t) = function - | ImplicitBindings largs -> - let clause = mk_clenv_from_n wc n (c,t) in - clenv_constrain_dep_args (n <> None) clause largs - | ExplicitBindings lbind -> - let clause = mk_clenv_rename_from_n wc n (c,t) in - clenv_match_args lbind clause - | NoBindings -> - mk_clenv_from_n wc n (c,t) - -let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc -let make_clenv_binding = make_clenv_binding_gen None - -open Printer - -let pr_clenv clenv = - let pr_name mv = - try - let id = Metamap.find mv clenv.namenv in - (str"[" ++ pr_id id ++ str"]") - with Not_found -> (mt ()) - in - let pr_meta_binding = function - | (mv,Cltyp b) -> - hov 0 - (pr_meta mv ++ pr_name mv ++ str " : " ++ prterm b.rebus ++ fnl ()) - | (mv,Clval(b,_)) -> - hov 0 - (pr_meta mv ++ pr_name mv ++ str " := " ++ prterm b.rebus ++ fnl ()) - in - (str"TEMPL: " ++ prterm clenv.templval.rebus ++ - str" : " ++ prterm clenv.templtyp.rebus ++ fnl () ++ - (prlist pr_meta_binding (metamap_to_list clenv.env))) diff --git a/proofs/clenv.mli b/proofs/clenv.mli deleted file mode 100644 index 737fbea3..00000000 --- a/proofs/clenv.mli +++ /dev/null @@ -1,142 +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: clenv.mli,v 1.32.2.2 2005/01/21 16:41:51 herbelin Exp $ i*) - -(*i*) -open Util -open Names -open Term -open Sign -open Proof_type -(*i*) - -(* [new_meta] is a generator of unique meta variables *) -val new_meta : unit -> metavariable - -(* [exist_to_meta] generates new metavariables for each existential - and performs the replacement in the given constr *) -val exist_to_meta : - Evd.evar_map -> Pretyping.open_constr -> (Termops.metamap * constr) - -(* The Type of Constructions clausale environments. *) - -module Metaset : Set.S with type elt = metavariable - -module Metamap : Map.S with type key = metavariable - -type 'a freelisted = { - rebus : 'a; - freemetas : Metaset.t } - -type clbinding = - | Cltyp of constr freelisted - | Clval of constr freelisted * constr freelisted - -type 'a clausenv = { - templval : constr freelisted; - templtyp : constr freelisted; - namenv : identifier Metamap.t; - env : clbinding Metamap.t; - hook : 'a } - -type wc = named_context sigma (* for a better reading of the following *) - -(* [templval] is the template which we are trying to fill out. - * [templtyp] is its type. - * [namenv] is a mapping from metavar numbers to names, for - * use in instanciating metavars by name. - * [env] is the mapping from metavar numbers to their types - * and values. - * [hook] is the pointer to the current walking context, for - * integrating existential vars and metavars. *) - -val collect_metas : constr -> metavariable list -val mk_clenv : 'a -> constr -> 'a clausenv -val mk_clenv_from : 'a -> constr * constr -> 'a clausenv -val mk_clenv_from_n : 'a -> int option -> constr * constr -> 'a clausenv -val mk_clenv_rename_from : wc -> constr * constr -> wc clausenv -val mk_clenv_rename_from_n : wc -> int option -> constr * constr -> wc clausenv -val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv -val mk_clenv_type_of : wc -> constr -> wc clausenv - -val subst_clenv : (substitution -> 'a -> 'a) -> - substitution -> 'a clausenv -> 'a clausenv - -val connect_clenv : wc -> 'a clausenv -> wc clausenv -(*i Was used in wcclausenv.ml -val clenv_change_head : constr * constr -> 'a clausenv -> 'a clausenv -i*) -val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv -val clenv_instance_term : wc clausenv -> constr -> constr -val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv -val clenv_template : 'a clausenv -> constr freelisted -val clenv_template_type : 'a clausenv -> constr freelisted -val clenv_instance_type : wc clausenv -> metavariable -> constr -val clenv_instance_template : wc clausenv -> constr -val clenv_instance_template_type : wc clausenv -> constr -val clenv_type_of : wc clausenv -> constr -> constr -val clenv_fchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv -val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv - -(* Unification with clenv *) -type arg_bindings = (int * constr) list - -val unify_0 : - Reductionops.conv_pb -> wc -> constr -> constr - -> Termops.metamap * (constr * constr) list -val clenv_unify : - bool -> Reductionops.conv_pb -> constr -> constr -> - wc clausenv -> wc clausenv -val clenv_match_args : - constr Rawterm.explicit_bindings -> wc clausenv -> wc clausenv -val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv - -(* Bindings *) -val clenv_independent : wc clausenv -> metavariable list -val clenv_missing : 'a clausenv -> metavariable list -val clenv_constrain_missing_args : (* Used in user contrib Lannion *) - constr list -> wc clausenv -> wc clausenv -(*i -val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv -i*) -val clenv_lookup_name : 'a clausenv -> identifier -> metavariable -val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv - -val make_clenv_binding_apply : - wc -> int -> constr * constr -> types Rawterm.bindings -> wc clausenv -val make_clenv_binding : - wc -> constr * constr -> types Rawterm.bindings -> wc clausenv - -(* Tactics *) -val unify : constr -> tactic -val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic -val res_pf : (wc -> tactic) -> wc clausenv -> tactic -val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic -val elim_res_pf : (wc -> tactic) -> wc clausenv -> bool -> tactic -val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic -val elim_res_pf_THEN_i : - (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic - -(* Pretty-print *) -val pr_clenv : 'a clausenv -> Pp.std_ppcmds - -(* Exported for debugging *) -val unify_to_subterm : - wc clausenv -> constr * constr -> wc clausenv * constr -val unify_to_subterm_list : - bool -> wc clausenv -> constr list -> constr -> wc clausenv * constr list -val clenv_typed_unify : - Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv - -(*i This should be in another module i*) - -(* [abstract_list_all env sigma t c l] *) -(* abstracts the terms in l over c to get a term of type t *) -val abstract_list_all : - Environ.env -> Evd.evar_map -> constr -> constr -> constr list -> constr diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml new file mode 100644 index 00000000..71538614 --- /dev/null +++ b/proofs/clenvtac.ml @@ -0,0 +1,97 @@ +(************************************************************************) +(* 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: clenvtac.ml 8023 2006-02-10 18:34:51Z coq $ *) + +open Pp +open Util +open Names +open Nameops +open Term +open Termops +open Sign +open Environ +open Evd +open Evarutil +open Proof_type +open Refiner +open Proof_trees +open Logic +open Reduction +open Reductionops +open Tacmach +open Evar_refiner +open Rawterm +open Pattern +open Tacexpr +open Clenv + + +(* This function put casts around metavariables whose type could not be + * infered by the refiner, that is head of applications, predicates and + * subject of Cases. + * Does check that the casted type is closed. Anyway, the refiner would + * fail in this case... *) + +let clenv_cast_meta clenv = + let rec crec u = + match kind_of_term u with + | App _ | Case _ -> crec_hd u + | Cast (c,_,_) when isMeta c -> u + | _ -> map_constr crec u + + and crec_hd u = + match kind_of_term (strip_outer_cast u) with + | Meta mv -> + (try + let b = Typing.meta_type clenv.env mv in + if occur_meta b then u + else mkCast (mkMeta mv, DEFAULTcast, b) + with Not_found -> u) + | App(f,args) -> mkApp (crec_hd f, Array.map crec args) + | Case(ci,p,c,br) -> + mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) + | _ -> u + in + crec + +let clenv_refine clenv gls = + tclTHEN + (tclEVARS (evars_of clenv.env)) + (refine (clenv_cast_meta clenv (clenv_value clenv))) + gls + + +let res_pf clenv ?(allow_K=false) gls = + clenv_refine (clenv_unique_resolver allow_K clenv gls) gls + +let elim_res_pf_THEN_i clenv tac gls = + let clenv' = (clenv_unique_resolver true clenv gls) in + tclTHENLASTn (clenv_refine clenv') (tac clenv') gls + + +let e_res_pf clenv gls = + clenv_refine (evar_clenv_unique_resolver clenv gls) gls + + + + +(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en + particulier ne semblent pas vérifier que des instances différentes + d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas + provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) + +(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) +let unifyTerms m n gls = + let env = pf_env gls in + let evd = create_evar_defs (project gls) in + let evd' = Unification.w_unify false env CONV m n evd in + tclIDTAC {it = gls.it; sigma = evars_of evd'} + +let unify m gls = + let n = pf_concl gls in unifyTerms m n gls diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli new file mode 100644 index 00000000..505826fa --- /dev/null +++ b/proofs/clenvtac.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* 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: clenvtac.mli 6099 2004-09-12 11:38:09Z barras $ i*) + +(*i*) +open Util +open Names +open Term +open Sign +open Evd +open Clenv +open Proof_type +(*i*) + +(* Tactics *) +val unify : constr -> tactic +val clenv_refine : clausenv -> tactic +val res_pf : clausenv -> ?allow_K:bool -> tactic +val e_res_pf : clausenv -> tactic +val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index ac4dd43a..4ee8001c 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -6,183 +6,44 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_refiner.ml,v 1.36.2.2 2004/08/03 21:37:27 herbelin Exp $ *) +(* $Id: evar_refiner.ml 8654 2006-03-22 15:36:58Z msozeau $ *) -open Pp open Util open Names open Term -open Environ open Evd open Sign -open Reductionops -open Typing -open Instantiate -open Tacred open Proof_trees -open Proof_type -open Logic open Refiner -open Tacexpr -open Nameops - - -type wc = named_context sigma (* for a better reading of the following *) - -let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal -let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it - -type w_tactic = named_context sigma -> named_context sigma - -let startWalk gls = - let evc = project_with_focus gls in - (evc, - (fun wc' gls' -> - if not !Options.debug or (gls.it = gls'.it) then -(* if Intset.equal (get_lc gls.it) (get_focus (ids_it wc')) then*) - tclIDTAC {it=gls'.it; sigma = (get_gc wc')} -(* else - (local_Constraints (get_focus (ids_it wc')) - {it=gls'.it; sigma = get_gc (ids_it wc')})*) - else error "Walking")) - -let extract_decl sp evc = - let evdmap = evc.sigma in - let evd = Evd.map evdmap sp in - { it = evd.evar_hyps; - sigma = Evd.rmv evdmap sp } - -let restore_decl sp evd evc = - (rc_add evc (sp,evd)) - - -(* [w_Focusing sp wt wc] - * - * Focuses the walking context WC onto the declaration SP, given that - * this declaration is UNDEFINED. Then, it runs the walking_tactic, - * WT, on this new context. When the result is returned, we recover - * the resulting focus (access list) and restore it to SP's declaration. - * - * It is an error to cause SP to change state while we are focused on it. *) - -(* let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic) - (wc : named_context sigma) = - let hyps = wc.it - and evd = Evd.map wc.sigma sp in - let (wc' : named_context sigma) = extract_decl sp wc in - let (wc'',rslt) = wt wc' in -(* if not (ids_eq wc wc'') then error "w_saving_focus"; *) - if wc'==wc'' then - wt' rslt wc - else - let wc''' = restore_decl sp evd wc'' in - wt' rslt {it = hyps; sigma = wc'''.sigma} *) - -let w_add_sign (id,t) (wc : named_context sigma) = - { it = Sign.add_named_decl (id,None,t) wc.it; - sigma = wc.sigma } - -let w_Focus sp wc = extract_decl sp wc - -let w_Underlying wc = wc.sigma -let w_whd wc c = Evarutil.whd_castappevar (w_Underlying wc) c -let w_type_of wc c = - type_of (Global.env_of_context wc.it) wc.sigma c -let w_env wc = get_env wc -let w_hyps wc = named_context (get_env wc) -let w_defined_evar wc k = Evd.is_defined (w_Underlying wc) k -let w_const_value wc = constant_value (w_env wc) -let w_conv_x wc m n = is_conv (w_env wc) (w_Underlying wc) m n -let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_env wc) (w_Underlying wc) c -let w_hnf_constr wc c = hnf_constr (w_env wc) (w_Underlying wc) c - - -let w_Declare sp ty (wc : named_context sigma) = - let _ = w_type_of wc ty in (* Utile ?? *) - let sign = get_hyps wc in - let newdecl = mk_goal sign ty in - ((rc_add wc (sp,newdecl)): named_context sigma) - -let w_Define sp c wc = - let spdecl = Evd.map (w_Underlying wc) sp in - let cty = - try - w_type_of (w_Focus sp wc) (mkCast (c,spdecl.evar_concl)) - with - Not_found -> error "Instantiation contains unlegal variables" - | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> - errorlabstrm "w_Define" - (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ - str (string_of_existential sp)) - in - match spdecl.evar_body with - | Evar_empty -> - let spdecl' = { evar_hyps = spdecl.evar_hyps; - evar_concl = spdecl.evar_concl; - evar_body = Evar_defined c } - in - Proof_trees.rc_add wc (sp,spdecl') - | _ -> error "define_evar" - (******************************************) (* Instantiation of existential variables *) (******************************************) -(* The instantiate tactic *) +(* w_tactic pour instantiate *) -let evars_of evc c = - let rec evrec acc c = - match kind_of_term c with - | Evar (n, _) when Evd.in_dom evc n -> c :: acc - | _ -> fold_constr evrec acc c - in - evrec [] c +let w_refine env ev rawc evd = + if Evd.is_defined (evars_of evd) ev then + error "Instantiate called on already-defined evar"; + let e_info = Evd.map (evars_of evd) ev in + let env = Evd.evar_env e_info in + let sigma,typed_c = + Pretyping.Default.understand_tcc (evars_of evd) env + ~expected_type:e_info.evar_concl rawc in + evar_define ev typed_c (evars_reset_evd sigma evd) -let instantiate n c ido gl = - let wc = Refiner.project_with_focus gl in - let evl = - match ido with - None -> evars_of wc.sigma gl.it.evar_concl - | Some (id,_,_) -> - let (_,_,typ)=Sign.lookup_named id gl.it.evar_hyps in - evars_of wc.sigma typ in - if List.length evl < n then error "not enough evars"; - let (n,_) as k = destEvar (List.nth evl (n-1)) in - if Evd.is_defined wc.sigma n then - error "Instantiate called on already-defined evar"; - let wc' = w_Define n c wc in - tclIDTAC {it = gl.it ; sigma = wc'.sigma} - -let pfic gls c = - let evc = gls.sigma in - Constrintern.interp_constr evc (Global.env_of_context gls.it.evar_hyps) c - -(* -let instantiate_tac = function - | [Integer n; Command com] -> - (fun gl -> instantiate n (pfic gl com) gl) - | [Integer n; Constr c] -> - (fun gl -> instantiate n c gl) - | _ -> invalid_arg "Instantiate called with bad arguments" -*) - -(* vernac command existential *) +(* vernac command Existential *) let instantiate_pf_com n com pfts = let gls = top_goal_of_pftreestate pfts in - let wc = project_with_focus gls in - let sigma = (w_Underlying wc) in - let (sp,evd) = + let sigma = gls.sigma in + let (sp,evi) (* as evc *) = try - List.nth (Evd.non_instantiated sigma) (n-1) + List.nth (Evarutil.non_instantiated sigma) (n-1) with Failure _ -> - error "not so many uninstantiated existential variables" - | Invalid_argument _ -> error "incorrect existential variable index" - in - let c = Constrintern.interp_constr sigma (Evarutil.evar_env evd) com in - let wc' = w_Define sp c wc in - let newgc = (w_Underlying wc') in - change_constraints_pftreestate newgc pfts - - + error "not so many uninstantiated existential variables" in + let env = Evd.evar_env evi in + let rawc = Constrintern.intern_constr sigma env com in + let evd = create_evar_defs sigma in + let evd' = w_refine env sp rawc evd in + change_constraints_pftreestate (evars_of evd') pfts diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index d57e1b84..9880f2f0 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -6,52 +6,21 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evar_refiner.mli,v 1.28.2.2 2005/01/21 16:41:51 herbelin Exp $ i*) +(*i $Id: evar_refiner.mli 6616 2005-01-21 17:18:23Z herbelin $ i*) (*i*) open Names open Term -open Sign open Environ open Evd open Refiner -open Proof_type (*i*) -type wc = named_context sigma (* for a better reading of the following *) - (* Refinement of existential variables. *) -val rc_of_pfsigma : proof_tree sigma -> wc -val rc_of_glsigma : goal sigma -> wc - -(* A [w_tactic] is a tactic which modifies the a set of evars of which - a goal depend, either by instantiating one, or by declaring a new - dependent goal *) -type w_tactic = wc -> wc - -val startWalk : goal sigma -> wc * (wc -> tactic) - -val extract_decl : evar -> w_tactic -val restore_decl : evar -> evar_info -> w_tactic -val w_Declare : evar -> types -> w_tactic -val w_Define : evar -> constr -> w_tactic - -val w_Underlying : wc -> evar_map -val w_env : wc -> env -val w_hyps : wc -> named_context -val w_whd : wc -> constr -> constr -val w_type_of : wc -> constr -> constr -val w_add_sign : (identifier * types) -> w_tactic +val w_refine : env -> evar -> Rawterm.rawconstr -> evar_defs -> evar_defs -val w_whd_betadeltaiota : wc -> constr -> constr -val w_hnf_constr : wc -> constr -> constr -val w_conv_x : wc -> constr -> constr -> bool -val w_const_value : wc -> constant -> constr -val w_defined_evar : wc -> existential_key -> bool +val instantiate_pf_com : + int -> Topconstr.constr_expr -> pftreestate -> pftreestate -val instantiate : int -> constr -> identifier Tacexpr.gsimple_clause -> tactic -(*i -val instantiate_tac : tactic_arg list -> tactic -i*) -val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate +(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *) diff --git a/proofs/logic.ml b/proofs/logic.ml index cefeb8ae..1f79d73c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: logic.ml,v 1.80.2.5 2005/12/17 21:15:52 herbelin Exp $ *) +(* $Id: logic.ml 8696 2006-04-11 07:05:50Z herbelin $ *) open Pp open Util @@ -25,7 +25,6 @@ open Proof_trees open Proof_type open Typeops open Type_errors -open Coqast open Retyping open Evarutil @@ -40,114 +39,72 @@ type refiner_error = | NonLinearProof of constr (* Errors raised by the tactics *) - | CannotUnify of constr * constr - | CannotUnifyBindingType of constr * constr - | CannotGeneralize of constr | IntroNeedsProduct | DoesNotOccurIn of constr * identifier - | NoOccurrenceFound of constr exception RefinerError of refiner_error open Pretype_errors -let catchable_exception = function - | Util.UserError _ | TypeError _ | RefinerError _ - | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ | - Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) | - Indtypes.InductiveError (Indtypes.NotAllowedCaseAnalysis _ ))) -> true +let rec catchable_exception = function + | Stdpp.Exc_located(_,e) -> catchable_exception e + | Util.UserError _ | TypeError _ + | RefinerError _ | Indrec.RecursionSchemeError _ + | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) + (* unification errors *) + | PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _| + CannotUnifyBindingType _|NotClean _)) -> true | _ -> false -let error_cannot_unify (m,n) = - raise (RefinerError (CannotUnify (m,n))) - (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) let check = ref false - -let without_check tac gl = - let c = !check in - check := false; - try let r = tac gl in check := c; r with e -> check := c; raise e - let with_check = Options.with_option check - + (************************************************************************) (************************************************************************) (* Implementation of the structural rules (moving and deleting hypotheses around) *) -let check_clear_forward cleared_ids used_ids whatfor = - if !check && cleared_ids<>[] then - Idset.iter - (fun id' -> - if List.mem id' cleared_ids then - error (string_of_id id'^" is used in "^whatfor)) - used_ids - (* The Clear tactic: it scans the context for hypotheses to be removed (instead of iterating on the list of identifier to be removed, which forces the user to give them in order). *) let clear_hyps ids gl = let env = Global.env() in - let (nhyps,rmv) = - Sign.fold_named_context - (fun (id,c,ty as d) (hyps,rmv) -> - if List.mem id ids then - (hyps,id::rmv) - else begin - check_clear_forward rmv (global_vars_set_of_decl env d) - ("hypothesis "^string_of_id id); - (add_named_decl d hyps, rmv) - end) - gl.evar_hyps - ~init:(empty_named_context,[]) in + let (nhyps,cleared_ids) = + let fcheck cleared_ids (id,_,_ as d) = + if !check && cleared_ids<>[] then + Idset.iter + (fun id' -> + if List.mem id' cleared_ids then + error (string_of_id id'^ + " is used in hypothesis "^string_of_id id)) + (global_vars_set_of_decl env d) in + clear_hyps ids fcheck gl.evar_hyps in let ncl = gl.evar_concl in - check_clear_forward rmv (global_vars_set env ncl) "conclusion"; + if !check && cleared_ids<>[] then + Idset.iter + (fun id' -> + if List.mem id' cleared_ids then + error (string_of_id id'^" is used in conclusion")) + (global_vars_set env ncl); mk_goal nhyps ncl (* The ClearBody tactic *) (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and - returns [tail::(f head (id,_,_) tail)] *) + returns [tail::(f head (id,_,_) (rev tail))] *) let apply_to_hyp sign id f = - let found = ref false in - let sign' = - fold_named_context_both_sides - (fun head (idc,c,ct as d) tail -> - if idc = id then begin - found := true; f head d tail - end else - add_named_decl d head) - sign ~init:empty_named_context - in - if (not !check) || !found then sign' else error "No such assumption" - -(* Same but with whole environment *) -let apply_to_hyp2 env id f = - let found = ref false in - let env' = - fold_named_context_both_sides - (fun env (idc,c,ct as d) tail -> - if idc = id then begin - found := true; f env d tail - end else - push_named d env) - (named_context env) ~init:(reset_context env) - in - if (not !check) || !found then env' else error "No such assumption" + try apply_to_hyp sign id f + with Hyp_not_found -> + if !check then error "No such assumption" + else sign let apply_to_hyp_and_dependent_on sign id f g = - let found = ref false in - let sign = - Sign.fold_named_context - (fun (idc,_,_ as d) oldest -> - if idc = id then (found := true; add_named_decl (f d) oldest) - else if !found then add_named_decl (g d) oldest - else add_named_decl d oldest) - sign ~init:empty_named_context - in - if (not !check) || !found then sign else error "No such assumption" + try apply_to_hyp_and_dependent_on sign id f g + with Hyp_not_found -> + if !check then error "No such assumption" + else sign let check_typability env sigma c = if !check then let _ = type_of env sigma c in () @@ -162,26 +119,24 @@ let recheck_typability (what,id) env sigma t = ("The correctness of "^s^" relies on the body of "^(string_of_id id)) let remove_hyp_body env sigma id = - apply_to_hyp2 env id - (fun env (_,c,t) tail -> - match c with - | None -> error ((string_of_id id)^" is not a local definition") - | Some c -> - let env' = push_named (id,None,t) env in - if !check then - ignore - (Sign.fold_named_context - (fun (id',c,t as d) env'' -> - (match c with - | None -> - recheck_typability (Some id',id) env'' sigma t - | Some b -> - let b' = mkCast (b,t) in - recheck_typability (Some id',id) env'' sigma b'); - push_named d env'') - (List.rev tail) ~init:env'); - env') - + let sign = + apply_to_hyp_and_dependent_on (named_context_val env) id + (fun (_,c,t) _ -> + match c with + | None -> error ((string_of_id id)^" is not a local definition") + | Some c ->(id,None,t)) + (fun (id',c,t as d) sign -> + (if !check then + begin + let env = reset_with_named_context sign env in + match c with + | None -> recheck_typability (Some id',id) env sigma t + | Some b -> + let b' = mkCast (b,DEFAULTcast, t) in + recheck_typability (Some id',id) env sigma b' + end;d)) + in + reset_with_named_context sign env (* Auxiliary functions for primitive MOVE tactic * @@ -231,9 +186,16 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = moverec first' middle' right in if toleft then - List.rev_append (moverec [] [declfrom] left) right + let right = + List.fold_right push_named_context_val right empty_named_context_val in + List.fold_left (fun sign d -> push_named_context_val d sign) + right (moverec [] [declfrom] left) else - List.rev_append left (moverec [] [declfrom] right) + let right = + List.fold_right push_named_context_val + (moverec [] [declfrom] right) empty_named_context_val in + List.fold_left (fun sign d -> push_named_context_val d sign) + right left let check_backward_dependencies sign d = if not (Idset.for_all @@ -255,8 +217,8 @@ let check_forward_dependencies id tail = let rename_hyp id1 id2 sign = apply_to_hyp_and_dependent_on sign id1 - (fun (_,b,t) -> (id2,b,t)) - (map_named_declaration (replace_vars [id1,mkVar id2])) + (fun (_,b,t) _ -> (id2,b,t)) + (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) let replace_hyp sign id d = apply_to_hyp sign id @@ -264,13 +226,17 @@ let replace_hyp sign id d = if !check then (check_backward_dependencies sign d; check_forward_dependencies id tail); - add_named_decl d sign) + d) +(* why we dont check that id does not appear in tail ??? *) let insert_after_hyp sign id d = - apply_to_hyp sign id - (fun sign d' _ -> - if !check then check_backward_dependencies sign d; - add_named_decl d (add_named_decl d' sign)) + try + insert_after_hyp sign id d + (fun sign -> + if !check then check_backward_dependencies sign d) + with Hyp_not_found -> + if !check then error "No such assumption" + else sign (************************************************************************) (************************************************************************) @@ -282,7 +248,7 @@ variables only in Application and Case *) let collect_meta_variables c = let rec collrec acc c = match kind_of_term c with | Meta mv -> mv::acc - | Cast(c,_) -> collrec acc c + | Cast(c,_,_) -> collrec acc c | (App _| Case _) -> fold_constr collrec acc c | _ -> acc in @@ -311,13 +277,17 @@ let rec mk_refgoals sigma goal goalacc conclty trm = raise (RefinerError (OccurMetaGoal conclty)); (mk_goal hyps (nf_betaiota conclty))::goalacc, conclty - | Cast (t,ty) -> + | Cast (t,_, ty) -> check_typability env sigma ty; check_conv_leq_goal env sigma trm ty conclty; mk_refgoals sigma goal goalacc ty t | App (f,l) -> - let (acc',hdty) = mk_hdgoals sigma goal goalacc f in + let (acc',hdty) = + if isInd f & not (array_exists occur_meta l) (* we could be finer *) + then (goalacc,type_of_applied_inductive env sigma (destInd f) l) + else mk_hdgoals sigma goal goalacc f + in let (acc'',conclty') = mk_arggoals sigma goal acc' hdty (Array.to_list l) in check_conv_leq_goal env sigma trm conclty' conclty; @@ -346,12 +316,20 @@ and mk_hdgoals sigma goal goalacc trm = let env = evar_env goal in let hyps = goal.evar_hyps in match kind_of_term trm with - | Cast (c,ty) when isMeta c -> + | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; (mk_goal hyps (nf_betaiota ty))::goalacc,ty + | Cast (t,_, ty) -> + check_typability env sigma ty; + mk_refgoals sigma goal goalacc ty t + | App (f,l) -> - let (acc',hdty) = mk_hdgoals sigma goal goalacc f in + let (acc',hdty) = + if isInd f & not (array_exists occur_meta l) (* we could be finer *) + then (goalacc,type_of_applied_inductive env sigma (destInd f) l) + else mk_hdgoals sigma goal goalacc f + in mk_arggoals sigma goal acc' hdty (Array.to_list l) | Case (_,p,c,lf) -> @@ -397,16 +375,13 @@ let error_use_instantiate () = let convert_hyp sign sigma (id,b,bt as d) = apply_to_hyp sign id - (fun sign (_,c,ct) _ -> + (fun _ (_,c,ct) _ -> let env = Global.env_of_context sign in if !check && not (is_conv env sigma bt ct) then - (* Just a warning in V8.0bugfix for compatibility *) - msgnl (str "Compatibility warning: Hazardeous change of the type of " ++ pr_id id ++ - str " (not well-typed in current signature)"); + error ("Incorrect change of the type of "^(string_of_id id)); if !check && not (option_compare (is_conv env sigma) b c) then - msgnl (str "Compatibility warning: Hazardeous change of the body of " ++ pr_id id ++ - str " (not well-typed in current signature)"); - add_named_decl d sign) + error ("Incorrect change of the body of "^(string_of_id id)); + d) (************************************************************************) @@ -420,18 +395,18 @@ let prim_refiner r sigma goal = match r with (* Logical rules *) | Intro id -> - if !check && mem_named_context id sign then + if !check && mem_named_context id (named_context_of_val sign) then error "New variable is already declared"; (match kind_of_term (strip_outer_cast cl) with | Prod (_,c1,b) -> if occur_meta c1 then error_use_instantiate(); - let sg = mk_goal (add_named_decl (id,None,c1) sign) + let sg = mk_goal (push_named_context_val (id,None,c1) sign) (subst1 (mkVar id) b) in [sg] | LetIn (_,c1,t1,b) -> if occur_meta c1 or occur_meta t1 then error_use_instantiate(); let sg = - mk_goal (add_named_decl (id,Some c1,t1) sign) + mk_goal (push_named_context_val (id,Some c1,t1) sign) (subst1 (mkVar id) b) in [sg] | _ -> @@ -453,11 +428,11 @@ let prim_refiner r sigma goal = raise (RefinerError IntroNeedsProduct)) | Cut (b,id,t) -> - if !check && mem_named_context id sign then + if !check && mem_named_context id (named_context_of_val sign) then error "New variable is already declared"; if occur_meta t then error_use_instantiate(); let sg1 = mk_goal sign (nf_betaiota t) in - let sg2 = mk_goal (add_named_decl (id,None,t) sign) cl in + let sg2 = mk_goal (push_named_context_val (id,None,t) sign) cl in if b then [sg1;sg2] else [sg2;sg1] | FixRule (f,n,rest) -> @@ -481,9 +456,9 @@ let prim_refiner r sigma goal = if not (sp=sp') then error ("fixpoints should be on the same " ^ "mutual inductive declaration"); - if !check && mem_named_context f sign then + if !check && mem_named_context f (named_context_of_val sign) then error "name already used in the environment"; - mk_sign (add_named_decl (f,None,ar) sign) oth + mk_sign (push_named_context_val (f,None,ar) sign) oth | [] -> List.map (fun (_,_,c) -> mk_goal sign c) all in @@ -506,11 +481,11 @@ let prim_refiner r sigma goal = let rec mk_sign sign = function | (f,ar)::oth -> (try - (let _ = Sign.lookup_named f sign in + (let _ = lookup_named_val f sign in error "name already used in the environment") with | Not_found -> - mk_sign (add_named_decl (f,None,ar) sign) oth) + mk_sign (push_named_context_val (f,None,ar) sign) oth) | [] -> List.map (fun (_,c) -> mk_goal sign c) all in mk_sign sign all @@ -523,7 +498,7 @@ let prim_refiner r sigma goal = sgl (* Conversion rules *) - | Convert_concl cl' -> + | Convert_concl (cl',_) -> check_typability env sigma cl'; if (not !check) || is_conv_leq env sigma cl' cl then let sg = mk_goal sign cl' in @@ -544,18 +519,20 @@ let prim_refiner r sigma goal = if !check then recheck_typability (None,id) env' sigma cl; env' in - let sign' = named_context (List.fold_left clear_aux env ids) in + let sign' = named_context_val (List.fold_left clear_aux env ids) in let sg = mk_goal sign' cl in [sg] | Move (withdep, hfrom, hto) -> - let (left,right,declfrom,toleft) = split_sign hfrom hto sign in + let (left,right,declfrom,toleft) = + split_sign hfrom hto (named_context_of_val sign) in let hyps' = move_after withdep toleft (left,declfrom,right) hto in [mk_goal hyps' cl] | Rename (id1,id2) -> - if !check & id1 <> id2 & List.mem id2 (ids_of_named_context sign) then + if !check & id1 <> id2 && + List.mem id2 (ids_of_named_context (named_context_of_val sign)) then error ((string_of_id id2)^" is already used"); let sign' = rename_hyp id1 id2 sign in let cl' = replace_vars [id1,mkVar id2] cl in @@ -566,15 +543,39 @@ let prim_refiner r sigma goal = (* Extracting a proof term from the proof tree *) (* Util *) + +type variable_proof_status = ProofVar | SectionVar of identifier + +type proof_variable = name * variable_proof_status + +let subst_proof_vars = + let rec aux p vars = + let _,subst = + List.fold_left (fun (n,l) var -> + let t = match var with + | Anonymous,_ -> l + | Name id, ProofVar -> (id,mkRel n)::l + | Name id, SectionVar id' -> (id,mkVar id')::l in + (n+1,t)) (p,[]) vars + in replace_vars (List.rev subst) + in aux 1 + let rec rebind id1 id2 = function - | [] -> [] - | id::l -> - if id = id1 then id2::l else + | [] -> [Name id2,SectionVar id1] + | (na,_ as x)::l -> + if na = Name id1 then (Name id2,ProofVar)::l else let l' = rebind id1 id2 l in - if id = id2 then - (* TODO: find a more elegant way to hide a variable *) - (id_of_string "_@")::l' - else id::l' + if na = Name id2 then (Anonymous,ProofVar)::l' else x::l' + +let add_proof_var id vl = (Name id,ProofVar)::vl + +let proof_variable_index x = + let rec aux n = function + | (Name id,ProofVar)::l when x = id -> n + | _::l -> aux (n+1) l + | [] -> raise Not_found + in + aux 1 let prim_extractor subfun vl pft = let cl = pft.goal.evar_concl in @@ -582,61 +583,64 @@ let prim_extractor subfun vl pft = | Some (Prim (Intro id), [spf]) -> (match kind_of_term (strip_outer_cast cl) with | Prod (_,ty,_) -> - let cty = subst_vars vl ty in - mkLambda (Name id, cty, subfun (id::vl) spf) + let cty = subst_proof_vars vl ty in + mkLambda (Name id, cty, subfun (add_proof_var id vl) spf) | LetIn (_,b,ty,_) -> - let cb = subst_vars vl b in - let cty = subst_vars vl ty in - mkLetIn (Name id, cb, cty, subfun (id::vl) spf) + let cb = subst_proof_vars vl b in + let cty = subst_proof_vars vl ty in + mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf) | _ -> error "incomplete proof!") | Some (Prim (Intro_replacing id),[spf]) -> (match kind_of_term (strip_outer_cast cl) with | Prod (_,ty,_) -> - let cty = subst_vars vl ty in - mkLambda (Name id, cty, subfun (id::vl) spf) + let cty = subst_proof_vars vl ty in + mkLambda (Name id, cty, subfun (add_proof_var id vl) spf) | LetIn (_,b,ty,_) -> - let cb = subst_vars vl b in - let cty = subst_vars vl ty in - mkLetIn (Name id, cb, cty, subfun (id::vl) spf) + let cb = subst_proof_vars vl b in + let cty = subst_proof_vars vl ty in + mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf) | _ -> error "incomplete proof!") | Some (Prim (Cut (b,id,t)),[spf1;spf2]) -> let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in - mkLetIn (Name id,subfun vl spf1,subst_vars vl t,subfun (id::vl) spf2) + mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t, + subfun (add_proof_var id vl) spf2) | Some (Prim (FixRule (f,n,others)),spfl) -> let all = Array.of_list ((f,n,cl)::others) in - let lcty = Array.map (fun (_,_,ar) -> subst_vars vl ar) all in + let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in let names = Array.map (fun (f,_,_) -> Name f) all in let vn = Array.map (fun (_,n,_) -> n-1) all in - let newvl = List.fold_left (fun vl (id,_,_)->(id::vl)) (f::vl)others in + let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl) + (add_proof_var f vl) others in let lfix = Array.map (subfun newvl) (Array.of_list spfl) in mkFix ((vn,0),(names,lcty,lfix)) | Some (Prim (Cofix (f,others)),spfl) -> let all = Array.of_list ((f,cl)::others) in - let lcty = Array.map (fun (_,ar) -> subst_vars vl ar) all in + let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in let names = Array.map (fun (f,_) -> Name f) all in - let newvl = List.fold_left (fun vl (id,_)->(id::vl)) (f::vl) others in + let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl) + (add_proof_var f vl) others in let lfix = Array.map (subfun newvl) (Array.of_list spfl) in mkCoFix (0,(names,lcty,lfix)) | Some (Prim (Refine c),spfl) -> let mvl = collect_meta_variables c in let metamap = List.combine mvl (List.map (subfun vl) spfl) in - let cc = subst_vars vl c in + let cc = subst_proof_vars vl c in plain_instance metamap cc (* Structural and conversion rules do not produce any proof *) - | Some (Prim (Convert_concl _),[pf]) -> - subfun vl pf - + | Some (Prim (Convert_concl (t,k)),[pf]) -> + if k = DEFAULTcast then subfun vl pf + else mkCast (subfun vl pf,k,subst_proof_vars vl cl) | Some (Prim (Convert_hyp _),[pf]) -> subfun vl pf | Some (Prim (Thin _),[pf]) -> - (* No need to make ids Anonymous in vl: subst_vars take the more recent *) + (* No need to make ids Anon in vl: subst_proof_vars take the most recent*) subfun vl pf | Some (Prim (ThinBody _),[pf]) -> @@ -652,133 +656,3 @@ let prim_extractor subfun vl pft = | None-> error "prim_extractor handed incomplete proof" -(* Pretty-printer *) - -open Printer - -let prterm x = prterm_env (Global.env()) x - -let pr_prim_rule_v7 = function - | Intro id -> - str"Intro " ++ pr_id id - - | Intro_replacing id -> - (str"intro replacing " ++ pr_id id) - - | Cut (b,id,t) -> - if b then - (str"Assert " ++ prterm t) - else - (str"Cut " ++ prterm t ++ str ";[Intro " ++ pr_id id ++ str "|Idtac]") - - | FixRule (f,n,[]) -> - (str"Fix " ++ pr_id f ++ str"/" ++ int n) - - | FixRule (f,n,others) -> - let rec print_mut = function - | (f,n,ar)::oth -> - pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth - | [] -> mt () in - (str"Fix " ++ pr_id f ++ str"/" ++ int n ++ - str" with " ++ print_mut others) - - | Cofix (f,[]) -> - (str"Cofix " ++ pr_id f) - - | Cofix (f,others) -> - let rec print_mut = function - | (f,ar)::oth -> - (pr_id f ++ str" : " ++ prterm ar ++ print_mut oth) - | [] -> mt () in - (str"Cofix " ++ pr_id f ++ str" with " ++ print_mut others) - - | Refine c -> - str(if occur_meta c then "Refine " else "Exact ") ++ - Constrextern.with_meta_as_hole prterm c - - | Convert_concl c -> - (str"Change " ++ prterm c) - - | Convert_hyp (id,None,t) -> - (str"Change " ++ prterm t ++ spc () ++ str"in " ++ pr_id id) - - | Convert_hyp (id,Some c,t) -> - (str"Change " ++ prterm c ++ spc () ++ str"in " - ++ pr_id id ++ str" (Type of " ++ pr_id id ++ str ")") - - | Thin ids -> - (str"Clear " ++ prlist_with_sep pr_spc pr_id ids) - - | ThinBody ids -> - (str"ClearBody " ++ prlist_with_sep pr_spc pr_id ids) - - | Move (withdep,id1,id2) -> - (str (if withdep then "Dependent " else "") ++ - str"Move " ++ pr_id id1 ++ str " after " ++ pr_id id2) - - | Rename (id1,id2) -> - (str "Rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) - -let pr_prim_rule_v8 = function - | Intro id -> - str"intro " ++ pr_id id - - | Intro_replacing id -> - (str"intro replacing " ++ pr_id id) - - | Cut (b,id,t) -> - if b then - (str"assert " ++ prterm t) - else - (str"cut " ++ prterm t ++ str ";[intro " ++ pr_id id ++ str "|idtac]") - - | FixRule (f,n,[]) -> - (str"fix " ++ pr_id f ++ str"/" ++ int n) - - | FixRule (f,n,others) -> - let rec print_mut = function - | (f,n,ar)::oth -> - pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth - | [] -> mt () in - (str"fix " ++ pr_id f ++ str"/" ++ int n ++ - str" with " ++ print_mut others) - - | Cofix (f,[]) -> - (str"cofix " ++ pr_id f) - - | Cofix (f,others) -> - let rec print_mut = function - | (f,ar)::oth -> - (pr_id f ++ str" : " ++ prterm ar ++ print_mut oth) - | [] -> mt () in - (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others) - - | Refine c -> - str(if occur_meta c then "refine " else "exact ") ++ - Constrextern.with_meta_as_hole prterm c - - | Convert_concl c -> - (str"change " ++ prterm c) - - | Convert_hyp (id,None,t) -> - (str"change " ++ prterm t ++ spc () ++ str"in " ++ pr_id id) - - | Convert_hyp (id,Some c,t) -> - (str"change " ++ prterm c ++ spc () ++ str"in " - ++ pr_id id ++ str" (type of " ++ pr_id id ++ str ")") - - | Thin ids -> - (str"clear " ++ prlist_with_sep pr_spc pr_id ids) - - | ThinBody ids -> - (str"clearbody " ++ prlist_with_sep pr_spc pr_id ids) - - | Move (withdep,id1,id2) -> - (str (if withdep then "dependent " else "") ++ - str"move " ++ pr_id id1 ++ str " after " ++ pr_id id2) - - | Rename (id1,id2) -> - (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) - -let pr_prim_rule t = - if! Options.v7 then pr_prim_rule_v7 t else pr_prim_rule_v8 t diff --git a/proofs/logic.mli b/proofs/logic.mli index 7eef22bd..ab65b1d5 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: logic.mli,v 1.27.6.1 2004/07/16 19:30:49 herbelin Exp $ i*) +(*i $Id: logic.mli 8107 2006-03-01 17:34:36Z herbelin $ i*) (*i*) open Names @@ -20,7 +20,6 @@ open Proof_type (* This suppresses check done in [prim_refiner] for the tactic given in argument; works by side-effect *) -val without_check : tactic -> tactic val with_check : tactic -> tactic (* [without_check] respectively means:\\ @@ -37,9 +36,13 @@ val with_check : tactic -> tactic val prim_refiner : prim_rule -> evar_map -> goal -> goal list +type proof_variable + val prim_extractor : - (identifier list -> proof_tree -> constr) - -> identifier list -> proof_tree -> constr + (proof_variable list -> proof_tree -> constr) + -> proof_variable list -> proof_tree -> constr + +val proof_variable_index : identifier -> proof_variable list -> int (*s Refiner errors. *) @@ -54,20 +57,9 @@ type refiner_error = | NonLinearProof of constr (*i Errors raised by the tactics i*) - | CannotUnify of constr * constr - | CannotUnifyBindingType of constr * constr - | CannotGeneralize of constr | IntroNeedsProduct | DoesNotOccurIn of constr * identifier - | NoOccurrenceFound of constr exception RefinerError of refiner_error -val error_cannot_unify : constr * constr -> 'a - val catchable_exception : exn -> bool - - -(*s Pretty-printer. *) - -val pr_prim_rule : prim_rule -> Pp.std_ppcmds diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index f53ea870..fa6f8c37 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pfedit.ml,v 1.47.2.1 2004/07/16 19:30:49 herbelin Exp $ *) +(* $Id: pfedit.ml 6947 2005-04-20 16:18:41Z coq $ *) open Pp open Util @@ -19,7 +19,7 @@ open Entries open Environ open Evd open Typing -open Tacmach +open Refiner open Proof_trees open Tacexpr open Proof_type @@ -33,7 +33,6 @@ open Safe_typing type proof_topstate = { mutable top_end_tac : tactic option; - top_hyps : named_context * named_context; top_goal : goal; top_strength : Decl_kinds.goal_kind; top_hook : declaration_hook } @@ -175,6 +174,21 @@ let undo n = with (Invalid_argument "Edit.undo") -> errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true) +(* Undo current focused proof to reach depth [n]. This is used in + [vernac_backtrack]. *) +let undo_todepth n = + try + Edit.undo_todepth proof_edits n + with (Invalid_argument "Edit.undo") -> + errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true) + +(* Return the depth of the current focused proof stack, this is used + to put informations in coq prompt (in emacs mode). *) +let current_proof_depth() = + try + Edit.depth proof_edits + with (Invalid_argument "Edit.depth") -> -1 + (*********************************************************************) (* Proof cooking *) (*********************************************************************) @@ -192,7 +206,8 @@ let cook_proof () = (ident, ({ const_entry_body = pfterm; const_entry_type = Some concl; - const_entry_opaque = true }, + const_entry_opaque = true; + const_entry_boxed = false}, strength, ts.top_hook)) let current_proof_statement () = @@ -231,7 +246,6 @@ let start_proof na str sign concl hook = let top_goal = mk_goal sign concl in let ts = { top_end_tac = None; - top_hyps = (sign,empty_named_context); top_goal = top_goal; top_strength = str; top_hook = hook} @@ -274,11 +288,11 @@ let common_ancestor l1 l2 = let rec traverse_up = function | 0 -> (function pf -> pf) - | n -> (function pf -> Tacmach.traverse 0 (traverse_up (n - 1) pf)) + | n -> (function pf -> Refiner.traverse 0 (traverse_up (n - 1) pf)) let rec traverse_down = function | [] -> (function pf -> pf) - | n::l -> (function pf -> Tacmach.traverse n (traverse_down l pf)) + | n::l -> (function pf -> Refiner.traverse n (traverse_down l pf)) let traverse_to path = let up_and_down path pfs = @@ -305,29 +319,3 @@ let focused_goal () = let n = !focus_n in if n=0 then 1 else n let reset_top_of_tree () = let pts = get_pftreestate () in if not (is_top_pftreestate pts) then mutate top_of_tree - -(** Printers *) - -let pr_subgoals_of_pfts pfts = - let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in - let sigma = project (top_goal_of_pftreestate pfts) in - pr_subgoals_existential sigma gls - -let pr_open_subgoals () = - let pfts = get_pftreestate () in - match focus() with - | 0 -> - pr_subgoals_of_pfts pfts - | n -> - let pf = proof_of_pftreestate pfts in - let gls = fst (frontier pf) in - assert (n > List.length gls); - if List.length gls < 2 then - pr_subgoal n gls - else - v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++ - pr_subgoal n gls) - -let pr_nth_open_subgoal n = - let pf = proof_of_pftreestate (get_pftreestate ()) in - pr_subgoal n (fst (frontier pf)) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index e95881ba..ca379d2e 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pfedit.mli,v 1.35.2.1 2004/07/16 19:30:49 herbelin Exp $ i*) +(*i $Id: pfedit.mli 7639 2005-12-02 10:01:15Z gregoire $ i*) (*i*) open Util @@ -57,6 +57,14 @@ val delete_all_proofs : unit -> unit val undo : int -> unit +(* Same as undo, but undoes the current proof stack to reach depth + [n]. This is used in [vernac_backtrack]. *) +val undo_todepth : int -> unit + +(* Returns the depth of the current focused proof stack, this is used + to put informations in coq prompt (in emacs mode). *) +val current_proof_depth: unit -> int + (* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None] sets the size to the default value (12) *) @@ -68,7 +76,7 @@ val get_undo : unit -> int option declare the built constructions as a coercion or a setoid morphism) *) val start_proof : - identifier -> goal_kind -> named_context -> constr + identifier -> goal_kind -> named_context_val -> constr -> declaration_hook -> unit (* [restart_proof ()] restarts the current focused proof from the beginning @@ -176,8 +184,3 @@ val traverse_prev_unproven : unit -> unit proof and goal management, as it is done, for instance in pcoq *) val traverse_to : int list -> unit val mutate : (pftreestate -> pftreestate) -> unit - -(** Printers *) - -val pr_open_subgoals : unit -> std_ppcmds -val pr_nth_open_subgoal : int -> std_ppcmds diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index aaf54a36..7e299b89 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: proof_trees.ml,v 1.53.2.1 2004/07/16 19:30:49 herbelin Exp $ *) +(* $Id: proof_trees.ml 6113 2004-09-17 20:28:19Z barras $ *) open Closure open Util @@ -66,29 +66,6 @@ let is_tactic_proof pf = match pf.ref with | _ -> false -(*******************************************************************) -(* Constraints for existential variables *) -(*******************************************************************) - -(* A readable constraint is a global constraint plus a focus set - of existential variables and a signature. *) - -(* Functions on readable constraints *) - -let mt_evcty gc = - { it = empty_named_context; sigma = gc } - -let rc_of_gc evds gl = - { it = gl.evar_hyps; sigma = evds } - -let rc_add evc (k,v) = - { it = evc.it; - sigma = Evd.add evc.sigma k v } - -let get_hyps evc = evc.it -let get_env evc = Global.env_of_context evc.it -let get_gc evc = evc.sigma - let pf_lookup_name_as_renamed env ccl s = Detyping.lookup_name_as_renamed env ccl s @@ -100,154 +77,12 @@ let pf_lookup_index_as_renamed env ccl n = (*********************************************************************) open Pp -open Printer -(* Il faudrait parametrer toutes les pr_term, term_env, etc. par la - strategie de renommage choisie pour Termast (en particulier, il - faudrait pouvoir etre sur que lookup_as_renamed qui est utilisé par - Intros Until fonctionne exactement comme on affiche le but avec - term_env *) - -let pf_lookup_name_as_renamed hyps ccl s = - Detyping.lookup_name_as_renamed hyps ccl s - -let pf_lookup_index_as_renamed ccl n = - Detyping.lookup_index_as_renamed ccl n - -let pr_idl idl = prlist_with_sep pr_spc pr_id idl - -let pr_goal g = +let db_pr_goal g = let env = evar_env g in - let penv = pr_context_of env in - let pc = prterm_env_at_top env g.evar_concl in + let penv = print_named_context env in + let pc = print_constr_env env g.evar_concl in str" " ++ hv 0 (penv ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253))) ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () -let pr_concl n g = - let env = evar_env g in - let pc = prterm_env_at_top env g.evar_concl in - str (emacs_str (String.make 1 (Char.chr 253))) ++ - str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc - -(* print the subgoals but write Subtree proved! even in case some existential - variables remain unsolved, pr_subgoals_existential is a safer version - of pr_subgoals *) - -let pr_subgoals = function - | [] -> (str"Proof completed." ++ fnl ()) - | [g] -> - let pg = pr_goal g in v 0 (str ("1 "^"subgoal") ++cut () ++ pg) - | g1::rest -> - let rec pr_rec n = function - | [] -> (mt ()) - | g::rest -> - let pg = pr_concl n g in - let prest = pr_rec (n+1) rest in - (cut () ++ pg ++ prest) - in - let pg1 = pr_goal g1 in - let pgr = pr_rec 2 rest in - v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () ++ pg1 ++ pgr) - -let pr_subgoal n = - let rec prrec p = function - | [] -> error "No such goal" - | g::rest -> - if p = 1 then - let pg = pr_goal g in - v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg) - else - prrec (p-1) rest - in - prrec n - -let pr_seq evd = - let env = evar_env evd - and cl = evd.evar_concl - in - let pdcl = pr_named_context_of env in - let pcl = prterm_env_at_top env cl in - hov 0 (pdcl ++ spc () ++ hov 0 (str"|- " ++ pcl)) - -let prgl gl = - let pgl = pr_seq gl in - (str"[" ++ pgl ++ str"]" ++ spc ()) - -let pr_evgl gl = - let phyps = pr_idl (List.rev (ids_of_named_context gl.evar_hyps)) in - let pc = prterm gl.evar_concl in - hov 0 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pc ++ str"]") - -let pr_evgl_sign gl = - let ps = pr_named_context_of (evar_env gl) in - let pc = prterm gl.evar_concl in - hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]") - -(* evd.evgoal.lc seems to be printed twice *) -let pr_decl evd = - let pevgl = pr_evgl evd in - let pb = - match evd.evar_body with - | Evar_empty -> (fnl ()) - | Evar_defined c -> let pc = prterm c in (str" => " ++ pc ++ fnl ()) - in - h 0 (pevgl ++ pb) - -let pr_evd evd = - prlist_with_sep pr_fnl - (fun (ev,evd) -> - let pe = pr_decl evd in - h 0 (str (string_of_existential ev) ++ str"==" ++ pe)) - (Evd.to_list evd) - -let pr_decls decls = pr_evd decls - -let pr_evc evc = - let pe = pr_evd evc.sigma in - (pe) - -let pr_evars = - prlist_with_sep pr_fnl - (fun (ev,evd) -> - let pegl = pr_evgl_sign evd in - (str (string_of_existential ev) ++ str " : " ++ pegl)) - -(* Print an enumerated list of existential variables *) -let rec pr_evars_int i = function - | [] -> (mt ()) - | (ev,evd)::rest -> - let pegl = pr_evgl_sign evd in - let pei = pr_evars_int (i+1) rest in - (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++ - str (string_of_existential ev) ++ str " : " ++ pegl)) ++ - fnl () ++ pei - -(* Equivalent to pr_subgoals but start from the prooftree and - check for uninstantiated existential variables *) - -let pr_subgoals_existential sigma = function - | [] -> - let exl = Evd.non_instantiated sigma in - if exl = [] then - (str"Proof completed." ++ fnl ()) - else - let pei = pr_evars_int 1 exl in - (str "No more subgoals but non-instantiated existential " ++ - str "variables :" ++fnl () ++ (hov 0 pei)) - | [g] -> - let pg = pr_goal g in - v 0 (str ("1 "^"subgoal") ++cut () ++ pg) - | g1::rest -> - let rec pr_rec n = function - | [] -> (mt ()) - | g::rest -> - let pc = pr_concl n g in - let prest = pr_rec (n+1) rest in - (cut () ++ pc ++ prest) - in - let pg1 = pr_goal g1 in - let prest = pr_rec 2 rest in - v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () - ++ pg1 ++ prest ++ fnl ()) diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index c31d5207..cbf91c8a 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_trees.mli,v 1.27.2.1 2004/07/16 19:30:49 herbelin Exp $ i*) +(*i $Id: proof_trees.mli 7639 2005-12-02 10:01:15Z gregoire $ i*) (*i*) open Util @@ -21,7 +21,7 @@ open Proof_type (* This module declares readable constraints, and a few utilities on constraints and proof trees *) -val mk_goal : named_context -> constr -> goal +val mk_goal : named_context_val -> constr -> goal val rule_of_proof : proof_tree -> rule val ref_of_proof : proof_tree -> (rule * proof_tree list) @@ -33,16 +33,6 @@ val is_complete_proof : proof_tree -> bool val is_leaf_proof : proof_tree -> bool val is_tactic_proof : proof_tree -> bool -(*s A readable constraint is a global constraint plus a focus set - of existential variables and a signature. *) - -val rc_of_gc : evar_map -> goal -> named_context sigma -val rc_add : named_context sigma -> existential_key * goal -> - named_context sigma -val get_hyps : named_context sigma -> named_context -val get_env : named_context sigma -> env -val get_gc : named_context sigma -> evar_map - val pf_lookup_name_as_renamed : env -> constr -> identifier -> int option val pf_lookup_index_as_renamed : env -> constr -> int -> int option @@ -53,16 +43,4 @@ val pf_lookup_index_as_renamed : env -> constr -> int -> int option open Pp (*i*) -val pr_goal : goal -> std_ppcmds -val pr_subgoals : goal list -> std_ppcmds -val pr_subgoal : int -> goal list -> std_ppcmds - -val pr_decl : goal -> std_ppcmds -val pr_decls : evar_map -> std_ppcmds -val pr_evc : named_context sigma -> std_ppcmds - -val prgl : goal -> std_ppcmds -val pr_seq : goal -> std_ppcmds -val pr_evars : (existential_key * goal) list -> std_ppcmds -val pr_evars_int : int -> (existential_key * goal) list -> std_ppcmds -val pr_subgoals_existential : evar_map -> goal list -> std_ppcmds +val db_pr_goal : goal -> std_ppcmds diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index cbed5e27..009e9d5b 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_type.ml,v 1.29.2.1 2004/07/16 19:30:49 herbelin Exp $ *) +(*i $Id: proof_type.ml 7639 2005-12-02 10:01:15Z gregoire $ *) (*i*) open Environ @@ -32,19 +32,13 @@ type prim_rule = | FixRule of identifier * int * (identifier * int * constr) list | Cofix of identifier * (identifier * constr) list | Refine of constr - | Convert_concl of types + | Convert_concl of types * cast_kind | Convert_hyp of named_declaration | Thin of identifier list | ThinBody of identifier list | Move of bool * identifier * identifier | Rename of identifier * identifier - -(* Signature useful to define the tactic type *) -type 'a sigma = { - it : 'a ; - sigma : evar_map } - (*s Proof trees. [ref] = [None] if the goal has still to be proved, and [Some (r,l)] if the rule [r] was applied to the goal diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 42606552..0e42dcba 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: proof_type.mli,v 1.33.2.1 2004/07/16 19:30:49 herbelin Exp $ i*) +(*i $Id: proof_type.mli 7639 2005-12-02 10:01:15Z gregoire $ i*) (*i*) open Environ @@ -32,7 +32,7 @@ type prim_rule = | FixRule of identifier * int * (identifier * int * constr) list | Cofix of identifier * (identifier * constr) list | Refine of constr - | Convert_concl of types + | Convert_concl of types * cast_kind | Convert_hyp of named_declaration | Thin of identifier list | ThinBody of identifier list @@ -67,12 +67,6 @@ type prim_rule = \end{verbatim} *) -(* The type constructor ['a sigma] adds an evar map to an object of - type ['a] (see below the form of a [goal sigma] *) -type 'a sigma = { - it : 'a ; - sigma : evar_map} - (*s Proof trees. [ref] = [None] if the goal has still to be proved, and [Some (r,l)] if the rule [r] was applied to the goal diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml new file mode 100644 index 00000000..8b3b5f5f --- /dev/null +++ b/proofs/redexpr.ml @@ -0,0 +1,112 @@ +(************************************************************************) +(* 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: redexpr.ml 7639 2005-12-02 10:01:15Z gregoire $ *) + +open Pp +open Util +open Names +open Term +open Declarations +open Libnames +open Rawterm +open Reductionops +open Tacred +open Closure +open RedFlags + + +(* call by value normalisation function using the virtual machine *) +let cbv_vm env _ c = + let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in + Vconv.cbv_vm env c ctyp + + +let set_opaque_const sp = + Conv_oracle.set_opaque_const sp; + Csymtable.set_opaque_const sp + +let set_transparent_const sp = + let cb = Global.lookup_constant sp in + if cb.const_body <> None & cb.const_opaque then + errorlabstrm "set_transparent_const" + (str "Cannot make" ++ spc () ++ + Nametab.pr_global_env Idset.empty (ConstRef sp) ++ + spc () ++ str "transparent because it was declared opaque."); + Conv_oracle.set_transparent_const sp; + Csymtable.set_transparent_const sp + +let set_opaque_var = Conv_oracle.set_opaque_var +let set_transparent_var = Conv_oracle.set_transparent_var + +let _ = + Summary.declare_summary "Transparent constants and variables" + { Summary.freeze_function = Conv_oracle.freeze; + Summary.unfreeze_function = Conv_oracle.unfreeze; + Summary.init_function = Conv_oracle.init; + Summary.survive_module = false; + Summary.survive_section = false } + + +(* Generic reduction: reduction functions used in reduction tactics *) + +type red_expr = (constr, evaluable_global_reference) red_expr_gen + + +let make_flag_constant = function + | EvalVarRef id -> fVAR id + | EvalConstRef sp -> fCONST sp + +let make_flag f = + let red = no_red in + let red = if f.rBeta then red_add red fBETA else red in + let red = if f.rIota then red_add red fIOTA else red in + let red = if f.rZeta then red_add red fZETA else red in + let red = + if f.rDelta then (* All but rConst *) + let red = red_add red fDELTA in + let red = red_add_transparent red (Conv_oracle.freeze ()) in + List.fold_right + (fun v red -> red_sub red (make_flag_constant v)) + f.rConst red + else (* Only rConst *) + let red = red_add_transparent (red_add red fDELTA) all_opaque in + List.fold_right + (fun v red -> red_add red (make_flag_constant v)) + f.rConst red + in red + +let is_reference c = + try let _ref = global_of_constr c in true with _ -> false + +let red_expr_tab = ref Stringmap.empty + +let declare_red_expr s f = + try + let _ = Stringmap.find s !red_expr_tab in + error ("There is already a reduction expression of name "^s) + with Not_found -> + red_expr_tab := Stringmap.add s f !red_expr_tab + +let reduction_of_red_expr = function + | Red internal -> + if internal then (try_red_product,DEFAULTcast) + else (red_product,DEFAULTcast) + | Hnf -> (hnf_constr,DEFAULTcast) + | Simpl (Some (_,c as lp)) -> + (contextually (is_reference c) lp nf,DEFAULTcast) + | Simpl None -> (nf,DEFAULTcast) + | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast) + | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast) + | Unfold ubinds -> (unfoldn ubinds,DEFAULTcast) + | Fold cl -> (fold_commands cl,DEFAULTcast) + | Pattern lp -> (pattern_occs lp,DEFAULTcast) + | ExtraRedExpr s -> + (try (Stringmap.find s !red_expr_tab,DEFAULTcast) + with Not_found -> error("unknown user-defined reduction \""^s^"\"")) + | CbvVm -> (cbv_vm ,VMcast) diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli new file mode 100644 index 00000000..c442b16e --- /dev/null +++ b/proofs/redexpr.mli @@ -0,0 +1,35 @@ +(************************************************************************) +(* 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: redexpr.mli 7639 2005-12-02 10:01:15Z gregoire $ i*) + +open Names +open Term +open Closure +open Rawterm +open Reductionops + + +type red_expr = (constr, evaluable_global_reference) red_expr_gen + +val reduction_of_red_expr : red_expr -> reduction_function * cast_kind +(* [true] if we should use the vm to verify the reduction *) + +val declare_red_expr : string -> reduction_function -> unit + +(* Opaque and Transparent commands. *) +val set_opaque_const : constant -> unit +val set_transparent_const : constant -> unit + +val set_opaque_var : identifier -> unit +val set_transparent_var : identifier -> unit + + + +(* call by value normalisation function using the virtual machine *) +val cbv_vm : reduction_function diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 785e6dd4..2b878d37 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refiner.ml,v 1.67.2.3 2005/11/04 08:59:30 herbelin Exp $ *) +(* $Id: refiner.ml 8708 2006-04-14 08:13:02Z jforest $ *) open Pp open Util @@ -17,12 +17,10 @@ open Evd open Sign open Environ open Reductionops -open Instantiate open Type_errors open Proof_trees open Proof_type open Logic -open Printer type transformation_tactic = proof_tree -> (goal list * validation) @@ -30,10 +28,7 @@ let hypotheses gl = gl.evar_hyps let conclusion gl = gl.evar_concl let sig_it x = x.it -let sig_sig x = x.sigma - - -let project_with_focus gls = rc_of_gc (gls.sigma) (gls.it) +let project x = x.sigma let pf_status pf = pf.open_subgoals @@ -43,6 +38,11 @@ let on_open_proofs f pf = if is_complete pf then pf else f pf let and_status = List.fold_left (+) 0 +(* Getting env *) + +let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps +let pf_hyps gls = named_context_of_val (sig_it gls).evar_hyps + (* Normalizing evars in a goal. Called by tactic Local_constraints (i.e. when the sigma of the proof tree changes). Detect if the goal is unchanged *) @@ -51,13 +51,9 @@ let norm_goal sigma gl = let ncl = red_fun gl.evar_concl in let ngl = { evar_concl = ncl; - evar_hyps = - Sign.fold_named_context - (fun (d,b,ty) sign -> - add_named_decl (d, option_app red_fun b, red_fun ty) sign) - gl.evar_hyps ~init:empty_named_context; + evar_hyps = map_named_val red_fun gl.evar_hyps; evar_body = gl.evar_body} in - if ngl = gl then None else Some ngl + if Evd.eq_evar_info ngl gl then None else Some ngl (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]] @@ -85,7 +81,7 @@ let rec frontier p = ([p.goal], (fun lp' -> let p' = List.hd lp' in - if p'.goal = p.goal then + if Evd.eq_evar_info p'.goal p.goal then p' else errorlabstrm "Refiner.frontier" @@ -105,7 +101,7 @@ let rec frontier_map_rec f n p = match p.ref with | None -> let p' = f p in - if p'.goal == p.goal || p'.goal = p.goal then p' + if Evd.eq_evar_info p'.goal p.goal then p' else errorlabstrm "Refiner.frontier_map" (str"frontier_map was handed back a ill-formed proof.") @@ -131,7 +127,7 @@ let rec frontier_mapi_rec f i p = match p.ref with | None -> let p' = f i p in - if p'.goal == p.goal || p'.goal = p.goal then p' + if Evd.eq_evar_info p'.goal p.goal then p' else errorlabstrm "Refiner.frontier_mapi" (str"frontier_mapi was handed back a ill-formed proof.") @@ -189,7 +185,7 @@ let lookup_tactic s = (* refiner r is a tactic applying the rule r *) let check_subproof_connection gl spfl = - list_for_all2eq (fun g pf -> g=pf.goal) gl spfl + list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl let abstract_tactic_expr te tacfun gls = let (sgl_sigma,v) = tacfun gls in @@ -255,12 +251,6 @@ let vernac_tactic (s,args) = let tacfun = lookup_tactic s args in abstract_extended_tactic s args tacfun -(* [rc_of_pfsigma : proof sigma -> readable_constraints] *) -let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal - -(* [rc_of_glsigma : proof sigma -> readable_constraints] *) -let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it - (* [extract_open_proof : proof_tree -> constr * (int * constr) list] takes a (not necessarly complete) proof and gives a pair (pfterm,obl) where pfterm is the constr corresponding to the proof @@ -292,13 +282,13 @@ let extract_open_proof sigma pf = let visible_rels = map_succeed (fun id -> - try let n = list_index id vl in (n,id) + try let n = proof_variable_index id vl in (n,id) with Not_found -> failwith "caught") - (ids_of_named_context goal.evar_hyps) in + (ids_of_named_context (named_context_of_val goal.evar_hyps)) in let sorted_rels = Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in let sorted_env = - List.map (fun (n,id) -> (n,Sign.lookup_named id goal.evar_hyps)) + List.map (fun (n,id) -> (n,lookup_named_val id goal.evar_hyps)) sorted_rels in let abs_concl = List.fold_right (fun (_,decl) c -> mkNamedProd_or_LetIn decl c) @@ -308,7 +298,7 @@ let extract_open_proof sigma pf = open_obligations := (meta,abs_concl):: !open_obligations; applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst) - | _ -> anomaly "Bug : a case has been forgotten in proof_extractor" + | _ -> anomaly "Bug: a case has been forgotten in proof_extractor" in let pfterm = proof_extractor [] pf in (pfterm, List.rev !open_obligations) @@ -345,17 +335,13 @@ let tclIDTAC gls = (goal_goal_list gls, idtac_valid) (* the message printing identity tactic *) let tclIDTAC_MESSAGE s gls = - if s = "" then tclIDTAC gls - else - begin - msgnl (str ("Idtac says : "^s)); tclIDTAC gls - end + msg (hov 0 s); tclIDTAC gls (* General failure tactic *) let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) (* A special exception for levels for the Fail tactic *) -exception FailError of int * string +exception FailError of int * std_ppcmds (* The Fail tactic *) let tclFAIL lvl s g = raise (FailError (lvl,s)) @@ -469,7 +455,7 @@ let rec tclTHENLIST = function (* various progress criterions *) let same_goal gl subgoal = - (hypotheses subgoal) = (hypotheses gl) & + eq_named_context_val (hypotheses subgoal) (hypotheses gl) && eq_constr (conclusion subgoal) (conclusion gl) @@ -774,15 +760,16 @@ let extract_pftreestate pts = (str"Cannot extract from a proof-tree in which we have descended;" ++ spc () ++ str"Please ascend to the root"); let pfterm,subgoals = extract_open_pftreestate pts in - let exl = Evd.non_instantiated pts.tpfsigma in + let exl = Evarutil.non_instantiated pts.tpfsigma in if subgoals <> [] or exl <> [] then - errorlabstrm "extract_proof" - (if subgoals <> [] then - str "Attempt to save an incomplete proof" - else - str "Attempt to save a proof with existential variables still non-instantiated"); + errorlabstrm "extract_proof" + (if subgoals <> [] then + str "Attempt to save an incomplete proof" + else + str "Attempt to save a proof with existential variables still non-instantiated"); let env = Global.env_of_context pts.tpf.goal.evar_hyps in - strong whd_betaiotaevar env pts.tpfsigma pfterm + nf_betaiotaevar_preserving_vm_cast env pts.tpfsigma pfterm + (* strong whd_betaiotaevar env pts.tpfsigma pfterm *) (*** local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm ***) @@ -894,136 +881,21 @@ let rec top_of_tree pts = if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts) -(* Pretty-printers. *) +(* Change evars *) +let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} -open Pp +(* Pretty-printers. *) -let pr_tactic = function - | Tacexpr.TacArg (Tacexpr.Tacexp t) -> - if !Options.v7 then - Pptactic.pr_glob_tactic t (*top tactic from tacinterp*) - else - Pptacticnew.pr_glob_tactic (Global.env()) t - | t -> - if !Options.v7 then - Pptactic.pr_tactic t - else - Pptacticnew.pr_tactic (Global.env()) t - -let pr_rule = function - | Prim r -> hov 0 (pr_prim_rule r) - | Tactic (texp,_) -> hov 0 (pr_tactic texp) - | Change_evars -> - (* This is internal tactic and cannot be replayed at user-level. - Function pr_rule_dot below is used when we want to hide - Change_evars *) - str "Evar change" - -(* Does not print change of evars *) -let pr_rule_dot = function - | Change_evars -> mt () - | r -> pr_rule r ++ str"." - -exception Different - -(* We remove from the var context of env what is already in osign *) -let thin_sign osign sign = - Sign.fold_named_context - (fun (id,c,ty as d) sign -> - try - if Sign.lookup_named id osign = (id,c,ty) then sign - else raise Different - with Not_found | Different -> add_named_decl d sign) - sign ~init:empty_named_context - -let rec print_proof sigma osign pf = - let {evar_hyps=hyps; evar_concl=cl; - evar_body=body} = pf.goal in - let hyps' = thin_sign osign hyps in - match pf.ref with - | None -> - hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) - | Some(r,spfl) -> - hov 0 - (hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++ - spc () ++ str" BY " ++ - hov 0 (pr_rule r) ++ fnl () ++ - str" " ++ - hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl) -) - -let pr_change gl = - (str"Change " ++ prterm_env (Global.env()) gl.evar_concl ++ str".") - -let rec print_script nochange sigma osign pf = - let {evar_hyps=sign; evar_concl=cl} = pf.goal in - match pf.ref with - | None -> - (if nochange then - (str"<Your Tactic Text here>") - else - pr_change pf.goal) - ++ fnl () - | Some(r,spfl) -> - ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ - pr_rule_dot r ++ fnl () ++ - prlist_with_sep pr_fnl - (print_script nochange sigma sign) spfl) - -let print_treescript nochange sigma _osign pf = - let rec aux top pf = - let {evar_hyps=sign; evar_concl=cl} = pf.goal in - match pf.ref with - | None -> - if nochange then - (str"<Your Tactic Text here>") - else - (pr_change pf.goal) - | Some(r,spfl) -> - (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++ - pr_rule_dot r ++ - match spfl with - | [] -> mt () - | [spf] -> fnl () ++ (if top then mt () else str " ") ++ aux top spf - | _ -> fnl () ++ str " " ++ - hov 0 (prlist_with_sep fnl (aux false) spfl) - in hov 0 (aux true pf) - -let rec print_info_script sigma osign pf = - let {evar_hyps=sign; evar_concl=cl} = pf.goal in - match pf.ref with - | None -> (mt ()) - | Some(Change_evars,[spf]) -> - print_info_script sigma osign spf - | Some(r,spfl) -> - (pr_rule r ++ - match spfl with - | [pf1] -> - if pf1.ref = None then - (str "." ++ fnl ()) - else - (str";" ++ brk(1,3) ++ - print_info_script sigma sign pf1) - | _ -> (str"." ++ fnl () ++ - prlist_with_sep pr_fnl - (print_info_script sigma sign) spfl)) - -let format_print_info_script sigma osign pf = - hov 0 (print_info_script sigma osign pf) - -let print_subscript sigma sign pf = - if is_tactic_proof pf then - format_print_info_script sigma sign (subproof_of_proof pf) - else - format_print_info_script sigma sign pf +let pp_info = ref (fun _ _ _ -> assert false) +let set_info_printer f = pp_info := f let tclINFO (tac : tactic) gls = let (sgl,v) as res = tac gls in begin try let pf = v (List.map leaf (sig_it sgl)) in - let sign = (sig_it gls).evar_hyps in + let sign = named_context_of_val (sig_it gls).evar_hyps in msgnl (hov 0 (str" == " ++ - print_subscript (sig_sig gls) sign pf)) + !pp_info (project gls) sign pf)) with e when catchable_exception e -> msgnl (hov 0 (str "Info failed to apply validation")) end; diff --git a/proofs/refiner.mli b/proofs/refiner.mli index f6f2082e..417ddbcd 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: refiner.mli,v 1.31.2.2 2005/01/21 16:41:51 herbelin Exp $ i*) +(*i $Id: refiner.mli 7911 2006-01-21 11:18:36Z herbelin $ i*) (*i*) open Term @@ -20,9 +20,10 @@ open Tacexpr (* The refiner (handles primitive rules and high-level tactics). *) val sig_it : 'a sigma -> 'a -val sig_sig : 'a sigma -> evar_map +val project : 'a sigma -> evar_map -val project_with_focus : goal sigma -> named_context sigma +val pf_env : goal sigma -> Environ.env +val pf_hyps : goal sigma -> named_context val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma @@ -65,8 +66,10 @@ val frontier_mapi : (* [tclIDTAC] is the identity tactic without message printing*) val tclIDTAC : tactic -val tclIDTAC_MESSAGE : string -> tactic +val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic +(* [tclEVARS sigma] changes the current evar map *) +val tclEVARS : evar_map -> tactic (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) @@ -120,7 +123,7 @@ val tclTHENLASTn : tactic -> tactic array -> tactic val tclTHENFIRSTn : tactic -> tactic array -> tactic (* A special exception for levels for the Fail tactic *) -exception FailError of int * string +exception FailError of int * Pp.std_ppcmds val tclORELSE : tactic -> tactic -> tactic val tclREPEAT : tactic -> tactic @@ -131,7 +134,7 @@ val tclTRY : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic -val tclFAIL : int -> string -> tactic +val tclFAIL : int -> Pp.std_ppcmds -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic @@ -199,11 +202,5 @@ val change_constraints_pftreestate (*i*) open Pp (*i*) - -val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds -val pr_rule : rule -> std_ppcmds -val pr_tactic : tactic_expr -> std_ppcmds -val print_script : - bool -> evar_map -> named_context -> proof_tree -> std_ppcmds -val print_treescript : - bool -> evar_map -> named_context -> proof_tree -> std_ppcmds +val set_info_printer : + (evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index cd8d34db..aff6b944 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacexpr.ml,v 1.33.2.3 2005/05/15 12:47:04 herbelin Exp $ i*) +(*i $Id: tacexpr.ml 8651 2006-03-21 21:54:43Z jforest $ i*) open Names open Topconstr @@ -20,6 +20,7 @@ open Pattern type 'a or_metaid = AI of 'a | MetaId of loc * string type direction_flag = bool (* true = Left-to-right false = right-to-right *) +type lazy_flag = bool (* true = lazy false = eager *) type raw_red_flag = | FBeta @@ -55,8 +56,7 @@ type hyp_location_flag = (* To distinguish body and type of local defs *) | InHypTypeOnly | InHypValueOnly -type 'a raw_hyp_location = - 'a * int list * (hyp_location_flag * hyp_location_flag option ref) +type 'a raw_hyp_location = 'a * int list * hyp_location_flag type 'a induction_arg = | ElimOnConstr of 'a @@ -69,12 +69,17 @@ type inversion_kind = | FullInversionClear type ('c,'id) inversion_strength = - | NonDepInversion of inversion_kind * 'id list * intro_pattern_expr option - | DepInversion of inversion_kind * 'c option * intro_pattern_expr option + | NonDepInversion of inversion_kind * 'id list * intro_pattern_expr + | DepInversion of inversion_kind * 'c option * intro_pattern_expr | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b +type 'id message_token = + | MsgString of string + | MsgInt of int + | MsgIdent of 'id + type 'id gsimple_clause = ('id raw_hyp_location) option (* onhyps: [None] means *on every hypothesis* @@ -84,6 +89,8 @@ type 'id gclause = onconcl : bool; concl_occs :int list } +let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]} + let simple_clause_of = function { onhyps = Some[scl]; onconcl = false } -> Some scl | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None @@ -112,6 +119,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacIntroMove of identifier option * identifier located option | TacAssumption | TacExact of 'constr + | TacExactNoCheck of 'constr | TacApply of 'constr with_bindings | TacElim of 'constr with_bindings * 'constr with_bindings option | TacElimType of 'constr @@ -122,20 +130,19 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacCofix of identifier option | TacMutualCofix of identifier * (identifier * 'constr) list | TacCut of 'constr - | TacTrueCut of name * 'constr - | TacForward of bool * name * 'constr + | TacAssert of 'tac option * intro_pattern_expr * 'constr | TacGeneralize of 'constr list | TacGeneralizeDep of 'constr | TacLetTac of name * 'constr * 'id gclause - | TacInstantiate of int * 'constr * 'id gclause +(* | TacInstantiate of int * 'constr * (('id * hyp_location_flag,unit) location) *) (* Derived basic tactics *) - | TacSimpleInduction of (quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref) - | TacNewInduction of 'constr induction_arg * 'constr with_bindings option - * (intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref) + | TacSimpleInduction of quantified_hypothesis + | TacNewInduction of 'constr induction_arg list * 'constr with_bindings option + * intro_pattern_expr | TacSimpleDestruct of quantified_hypothesis - | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option - * (intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref) + | TacNewDestruct of 'constr induction_arg list * 'constr with_bindings option + * intro_pattern_expr | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis | TacDecomposeAnd of 'constr @@ -145,8 +152,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacLApply of 'constr (* Automation tactics *) - | TacTrivial of string list option - | TacAuto of int or_var option * string list option + | TacTrivial of 'constr list * string list option + | TacAuto of int or_var option * 'constr list * string list option | TacAutoTDB of int option | TacDestructHyp of (bool * identifier located) | TacDestructConcl @@ -154,7 +161,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacDAuto of int or_var option * int option (* Context management *) - | TacClear of 'id list + | TacClear of bool * 'id list | TacClearBody of 'id list | TacMove of bool * 'id * 'id | TacRename of 'id * 'id @@ -185,13 +192,14 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = (* For syntax extensions *) | TacAlias of loc * string * (identifier * ('constr,'tac) generic_argument) list - * (dir_path * 'tac) + * (dir_path * glob_tactic_expr) and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr = | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list + | TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list | TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr @@ -199,14 +207,13 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr = | TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * identifier option - | TacId of string - | TacFail of int or_var * string + | TacId of 'id message_token list + | TacFail of int or_var * 'id message_token list | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr - | TacLetRecIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacLetIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr option * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr - | TacMatch of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list - | TacMatchContext of direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list + | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list + | TacMatchContext of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg @@ -224,9 +231,21 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg = | Integer of int | TacCall of loc * 'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list + | TacExternal of loc * string * string * + ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list | TacFreshId of string option | Tacexp of 'tac +(* Globalized tactics *) +and glob_tactic_expr = + (rawconstr_and_expr, + constr_pattern, + evaluable_global_reference and_short_name or_var, + inductive or_var, + ltac_constant located or_var, + identifier located, + glob_tactic_expr) gen_tactic_expr + type raw_tactic_expr = (constr_expr, pattern_expr, @@ -259,16 +278,6 @@ type raw_generic_argument = type raw_red_expr = (constr_expr, reference) red_expr_gen -(* Globalized tactics *) -type glob_tactic_expr = - (rawconstr_and_expr, - constr_pattern, - evaluable_global_reference and_short_name or_var, - inductive or_var, - ltac_constant located or_var, - identifier located, - glob_tactic_expr) gen_tactic_expr - type glob_atomic_tactic_expr = (rawconstr_and_expr, constr_pattern, @@ -283,8 +292,8 @@ type glob_tactic_arg = constr_pattern, evaluable_global_reference and_short_name or_var, inductive or_var, - ltac_constant located, - identifier located or_var, + ltac_constant located or_var, + identifier located, glob_tactic_expr) gen_tactic_arg type glob_generic_argument = diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 0e3a49b0..b426f75d 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacmach.ml,v 1.61.2.1 2004/07/16 19:30:50 herbelin Exp $ *) +(* $Id: tacmach.ml 7682 2005-12-21 15:06:11Z herbelin $ *) open Util open Names @@ -14,11 +14,11 @@ open Nameops open Sign open Term open Termops -open Instantiate open Environ open Reductionops open Evd open Typing +open Redexpr open Tacred open Proof_trees open Proof_type @@ -32,7 +32,7 @@ let re_sig it gc = { it = it; sigma = gc } (* Operations for handling terms under a local typing context *) (**************************************************************) -type 'a sigma = 'a Proof_type.sigma;; +type 'a sigma = 'a Evd.sigma;; type validation = Proof_type.validation;; type tactic = Proof_type.tactic;; @@ -40,10 +40,10 @@ let unpackage = Refiner.unpackage let repackage = Refiner.repackage let apply_sig_tac = Refiner.apply_sig_tac -let sig_it = Refiner.sig_it -let project = Refiner.sig_sig -let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps -let pf_hyps gls = (sig_it gls).evar_hyps +let sig_it = Refiner.sig_it +let project = Refiner.project +let pf_env = Refiner.pf_env +let pf_hyps = Refiner.pf_hyps let pf_concl gls = (sig_it gls).evar_concl let pf_hyps_types gls = @@ -79,10 +79,6 @@ let pf_interp_constr gls c = let evc = project gls in Constrintern.interp_constr evc (pf_env gls) c -let pf_interp_openconstr gls c = - let evc = project gls in - Constrintern.interp_openconstr evc (pf_env gls) c - let pf_interp_type gls c = let evc = project gls in Constrintern.interp_type evc (pf_env gls) c @@ -91,12 +87,8 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id let pf_parse_const gls = compose (pf_global gls) id_of_string -let pf_execute gls = - let evc = project gls in - Typing.unsafe_machine (pf_env gls) evc - -let pf_reduction_of_redexp gls re c = - reduction_of_redexp re (pf_env gls) (project gls) c +let pf_reduction_of_red_expr gls re c = + (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c let pf_apply f gls = f (pf_env gls) (project gls) let pf_reduce = pf_apply @@ -119,7 +111,8 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls) -let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, c2))) +let pf_check_type gls c1 c2 = + ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2))) (************************************) (* Tactics handling a list of goals *) @@ -194,8 +187,8 @@ let internal_cut_rev_no_check id t gl = let refine_no_check c gl = refiner (Prim (Refine c)) gl -let convert_concl_no_check c gl = - refiner (Prim (Convert_concl c)) gl +let convert_concl_no_check c sty gl = + refiner (Prim (Convert_concl (c,sty))) gl let convert_hyp_no_check d gl = refiner (Prim (Convert_hyp d)) gl @@ -221,9 +214,11 @@ let mutual_cofix f others gl = with_check (refiner (Prim (Cofix (f,others)))) gl let rename_bound_var_goal gls = - let { evar_hyps = sign; evar_concl = cl } as gl = sig_it gls in - let ids = ids_of_named_context sign in - convert_concl_no_check (rename_bound_var (Global.env()) ids cl) gls + let { evar_hyps = sign; evar_concl = cl } = sig_it gls in + let ids = ids_of_named_context (named_context_of_val sign) in + convert_concl_no_check + (rename_bound_var (Global.env()) ids cl) DEFAULTcast gls + (* Versions with consistency checks *) @@ -233,7 +228,7 @@ let intro_replacing id = with_check (intro_replacing_no_check id) let internal_cut d t = with_check (internal_cut_no_check d t) let internal_cut_rev d t = with_check (internal_cut_rev_no_check d t) let refine c = with_check (refine_no_check c) -let convert_concl d = with_check (convert_concl_no_check d) +let convert_concl d sty = with_check (convert_concl_no_check d sty) let convert_hyp d = with_check (convert_hyp_no_check d) let thin l = with_check (thin_no_check l) let thin_body c = with_check (thin_body_no_check c) @@ -243,7 +238,6 @@ let rename_hyp id id' = with_check (rename_hyp_no_check id id') (* Pretty-printers *) open Pp -open Printer open Tacexpr open Rawterm @@ -252,9 +246,9 @@ let rec pr_list f = function | a::l1 -> (f a) ++ pr_list f l1 let pr_gls gls = - hov 0 (pr_decls (sig_sig gls) ++ fnl () ++ pr_seq (sig_it gls)) + hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) let pr_glls glls = - hov 0 (pr_decls (sig_sig glls) ++ fnl () ++ - prlist_with_sep pr_fnl pr_seq (sig_it glls)) + hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ + prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 2990567e..9352cb5d 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacmach.mli,v 1.50.2.2 2005/01/21 16:41:52 herbelin Exp $ i*) +(*i $Id: tacmach.mli 7639 2005-12-02 10:01:15Z gregoire $ i*) (*i*) open Names @@ -18,14 +18,14 @@ open Reduction open Proof_trees open Proof_type open Refiner -open Tacred +open Redexpr open Tacexpr open Rawterm (*i*) (* Operations for handling terms under a local typing context. *) -type 'a sigma = 'a Proof_type.sigma;; +type 'a sigma = 'a Evd.sigma;; type validation = Proof_type.validation;; type tactic = Proof_type.tactic;; @@ -51,7 +51,6 @@ val pf_global : goal sigma -> identifier -> constr val pf_parse_const : goal sigma -> string -> constr val pf_type_of : goal sigma -> constr -> types val pf_check_type : goal sigma -> constr -> types -> unit -val pf_execute : goal sigma -> constr -> unsafe_judgment val hnf_type_of : goal sigma -> constr -> types val pf_interp_constr : goal sigma -> Topconstr.constr_expr -> constr @@ -63,7 +62,7 @@ val pf_get_hyp_typ : goal sigma -> identifier -> types val pf_get_new_id : identifier -> goal sigma -> identifier val pf_get_new_ids : identifier list -> goal sigma -> identifier list -val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr +val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a @@ -120,9 +119,6 @@ val top_of_tree : pftreestate -> pftreestate val change_constraints_pftreestate : evar_map -> pftreestate -> pftreestate -(*i -val vernac_tactic : string * tactic_arg list -> tactic -i*) (*s The most primitive tactics. *) val refiner : rule -> tactic @@ -131,7 +127,7 @@ val intro_replacing_no_check : identifier -> tactic val internal_cut_no_check : identifier -> types -> tactic val internal_cut_rev_no_check : identifier -> types -> tactic val refine_no_check : constr -> tactic -val convert_concl_no_check : types -> tactic +val convert_concl_no_check : types -> cast_kind -> tactic val convert_hyp_no_check : named_declaration -> tactic val thin_no_check : identifier list -> tactic val thin_body_no_check : identifier list -> tactic @@ -149,10 +145,7 @@ val intro_replacing : identifier -> tactic val internal_cut : identifier -> types -> tactic val internal_cut_rev : identifier -> types -> tactic val refine : constr -> tactic -val convert_concl : constr -> tactic -val convert_hyp : named_declaration -> tactic -val thin : identifier list -> tactic -val convert_concl : types -> tactic +val convert_concl : types -> cast_kind -> tactic val convert_hyp : named_declaration -> tactic val thin : identifier list -> tactic val thin_body : identifier list -> tactic @@ -173,11 +166,6 @@ val tactic_list_tactic : tactic_list -> tactic val tclFIRSTLIST : tactic_list list -> tactic_list val tclIDTAC_list : tactic_list -(*s Pretty-printing functions. *) - -(*i*) -open Pp -(*i*) - -val pr_gls : goal sigma -> std_ppcmds -val pr_glls : goal list sigma -> std_ppcmds +(*s Pretty-printing functions (debug only). *) +val pr_gls : goal sigma -> Pp.std_ppcmds +val pr_glls : goal list sigma -> Pp.std_ppcmds diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 1fa1101d..43807872 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -6,17 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Ast open Names open Constrextern open Pp -open Pptactic -open Printer open Tacexpr open Termops -let pr_glob_tactic x = - (if !Options.v7 then pr_glob_tactic else Pptacticnew.pr_glob_tactic (Global.env())) x +let prtac = ref (fun _ -> assert false) +let set_tactic_printer f = prtac := f +let prmatchpatt = ref (fun _ _ -> assert false) +let set_match_pattern_printer f = prmatchpatt := f +let prmatchrl = ref (fun _ -> assert false) +let set_match_rule_printer f = prmatchrl := f (* This module intends to be a beginning of debugger for tactic expressions. Currently, it is quite simple and we can hope to have, in the future, a more @@ -32,7 +33,7 @@ let explain_logic_error = ref (fun e -> mt()) (* Prints the goal *) let db_pr_goal g = - msgnl (str "Goal:" ++ fnl () ++ Proof_trees.pr_goal (Tacmach.sig_it g)) + msgnl (str "Goal:" ++ fnl () ++ Proof_trees.db_pr_goal (Refiner.sig_it g)) (* Prints the commands *) let help () = @@ -46,7 +47,7 @@ let help () = let goal_com g tac = begin db_pr_goal g; - msg (str "Going to execute:" ++ fnl () ++ pr_glob_tactic tac ++ fnl ()) + msg (str "Going to execute:" ++ fnl () ++ !prtac tac ++ fnl ()) end (* Gives the number of a run command *) @@ -107,15 +108,14 @@ let debug_prompt lev g tac f = (* Prints a constr *) let db_constr debug env c = if debug <> DebugOff & !skip = 0 then - msgnl (str "Evaluated term: " ++ prterm_env env c) + msgnl (str "Evaluated term: " ++ print_constr_env env c) (* Prints the pattern rule *) let db_pattern_rule debug num r = if debug <> DebugOff & !skip = 0 then begin msgnl (str "Pattern rule " ++ int num ++ str ":"); - msgnl (str "|" ++ spc () ++ - pr_match_rule false Printer.pr_pattern pr_glob_tactic r) + msgnl (str "|" ++ spc () ++ !prmatchrl r) end (* Prints the hypothesis pattern identifier if it exists *) @@ -128,12 +128,12 @@ let db_matched_hyp debug env (id,c) ido = if debug <> DebugOff & !skip = 0 then msgnl (str "Hypothesis " ++ str ((Names.string_of_id id)^(hyp_bound ido)^ - " has been matched: ") ++ prterm_env env c) + " has been matched: ") ++ print_constr_env env c) (* Prints the matched conclusion *) let db_matched_concl debug env c = if debug <> DebugOff & !skip = 0 then - msgnl (str "Conclusion has been matched: " ++ prterm_env env c) + msgnl (str "Conclusion has been matched: " ++ print_constr_env env c) (* Prints a success message when the goal has been matched *) let db_mc_pattern_success debug = @@ -142,18 +142,16 @@ let db_mc_pattern_success debug = str "Let us execute the right-hand side part..." ++ fnl()) let pp_match_pattern env = function - | Term c -> Term (extern_pattern env (names_of_rel_context env) c) + | Term c -> Term (extern_constr_pattern (names_of_rel_context env) c) | Subterm (o,c) -> - Subterm (o,(extern_pattern env (names_of_rel_context env) c)) + Subterm (o,(extern_constr_pattern (names_of_rel_context env) c)) (* Prints a failure message for an hypothesis pattern *) let db_hyp_pattern_failure debug env (na,hyp) = if debug <> DebugOff & !skip = 0 then msgnl (str ("The pattern hypothesis"^(hyp_bound na)^ " cannot match: ") ++ - pr_match_pattern - (Printer.pr_pattern_env env (names_of_rel_context env)) - hyp) + !prmatchpatt env hyp) (* Prints a matching failure message for a rule *) let db_matching_failure debug = @@ -164,10 +162,10 @@ let db_matching_failure debug = (* Prints an evaluation failure message for a rule *) let db_eval_failure debug s = if debug <> DebugOff & !skip = 0 then - let s = if s="" then "no message" else "message \""^s^"\"" in + let s = str "message \"" ++ s ++ str "\"" in msgnl (str "This rule has failed due to \"Fail\" tactic (" ++ - str s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...") + s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...") (* Prints a logic failure message for a rule *) let db_logic_failure debug err = diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 9ab263c4..fc1b6120 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tactic_debug.mli,v 1.12.2.1 2004/07/16 19:30:50 herbelin Exp $ i*) +(*i $Id: tactic_debug.mli 7911 2006-01-21 11:18:36Z herbelin $ i*) open Environ open Pattern +open Evd open Proof_type open Names open Tacexpr @@ -19,6 +20,13 @@ open Term Currently, it is quite simple and we can hope to have, in the future, a more complete panel of commands dedicated to a proof assistant framework *) +val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit +val set_match_pattern_printer : + (env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit +val set_match_rule_printer : + ((constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) -> + unit + (* Debug information *) type debug_info = | DebugOn of int @@ -53,7 +61,7 @@ val db_hyp_pattern_failure : val db_matching_failure : debug_info -> unit (* Prints an evaluation failure message for a rule *) -val db_eval_failure : debug_info -> string -> unit +val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit (* An exception handler *) val explain_logic_error: (exn -> Pp.std_ppcmds) ref |