summaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml1175
-rw-r--r--proofs/clenv.mli142
-rw-r--r--proofs/clenvtac.ml97
-rw-r--r--proofs/clenvtac.mli26
-rw-r--r--proofs/evar_refiner.ml181
-rw-r--r--proofs/evar_refiner.mli41
-rw-r--r--proofs/logic.ml452
-rw-r--r--proofs/logic.mli22
-rw-r--r--proofs/pfedit.ml54
-rw-r--r--proofs/pfedit.mli17
-rw-r--r--proofs/proof_trees.ml173
-rw-r--r--proofs/proof_trees.mli28
-rw-r--r--proofs/proof_type.ml10
-rw-r--r--proofs/proof_type.mli10
-rw-r--r--proofs/redexpr.ml112
-rw-r--r--proofs/redexpr.mli35
-rw-r--r--proofs/refiner.ml198
-rw-r--r--proofs/refiner.mli25
-rw-r--r--proofs/tacexpr.ml77
-rw-r--r--proofs/tacmach.ml50
-rw-r--r--proofs/tacmach.mli30
-rw-r--r--proofs/tactic_debug.ml36
-rw-r--r--proofs/tactic_debug.mli12
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