diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /proofs |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/clenv.ml | 1175 | ||||
-rw-r--r-- | proofs/clenv.mli | 142 | ||||
-rw-r--r-- | proofs/doc.tex | 14 | ||||
-rw-r--r-- | proofs/evar_refiner.ml | 187 | ||||
-rw-r--r-- | proofs/evar_refiner.mli | 57 | ||||
-rw-r--r-- | proofs/logic.ml | 786 | ||||
-rw-r--r-- | proofs/logic.mli | 73 | ||||
-rw-r--r-- | proofs/pfedit.ml | 333 | ||||
-rw-r--r-- | proofs/pfedit.mli | 183 | ||||
-rw-r--r-- | proofs/proof_trees.ml | 253 | ||||
-rw-r--r-- | proofs/proof_trees.mli | 68 | ||||
-rw-r--r-- | proofs/proof_type.ml | 101 | ||||
-rw-r--r-- | proofs/proof_type.mli | 128 | ||||
-rw-r--r-- | proofs/refiner.ml | 1030 | ||||
-rw-r--r-- | proofs/refiner.mli | 210 | ||||
-rw-r--r-- | proofs/tacexpr.ml | 314 | ||||
-rw-r--r-- | proofs/tacmach.ml | 260 | ||||
-rw-r--r-- | proofs/tacmach.mli | 183 | ||||
-rw-r--r-- | proofs/tactic_debug.ml | 179 | ||||
-rw-r--r-- | proofs/tactic_debug.mli | 62 | ||||
-rw-r--r-- | proofs/tmp-src | 56 |
21 files changed, 5794 insertions, 0 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml new file mode 100644 index 00000000..423350d7 --- /dev/null +++ b/proofs/clenv.ml @@ -0,0 +1,1175 @@ +(************************************************************************) +(* 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.3 2004/07/16 19:30:48 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; + mkMeta n 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 new file mode 100644 index 00000000..10e0004e --- /dev/null +++ b/proofs/clenv.mli @@ -0,0 +1,142 @@ +(************************************************************************) +(* 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.1 2004/07/16 19:30:49 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 +(* +val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv +*) +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/doc.tex b/proofs/doc.tex new file mode 100644 index 00000000..431027ef --- /dev/null +++ b/proofs/doc.tex @@ -0,0 +1,14 @@ + +\newpage +\section*{The Proof Engine} + +\ocwsection \label{proofs} +This chapter describes the \Coq\ proof engine, which is also called +the ``refiner'', since it provides a way to build terms by successive +refining steps. Those steps are either primitive rules or higher-level +tactics. +The modules of the proof engine are organized as follows. + +\bigskip +\begin{center}\epsfig{file=proofs.dep.ps,width=\linewidth}\end{center} + diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml new file mode 100644 index 00000000..d59ff835 --- /dev/null +++ b/proofs/evar_refiner.ml @@ -0,0 +1,187 @@ +(************************************************************************) +(* 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: evar_refiner.ml,v 1.36.2.1 2004/07/16 19:30:49 herbelin Exp $ *) + +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 *) + +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 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 *) + +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) = + try + List.nth (Evd.non_instantiated sigma) (n-1) + with Failure _ -> + error "not so many uninstantiated existential variables" + 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 + + diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli new file mode 100644 index 00000000..d7f393b3 --- /dev/null +++ b/proofs/evar_refiner.mli @@ -0,0 +1,57 @@ +(************************************************************************) +(* 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: evar_refiner.mli,v 1.28.2.1 2004/07/16 19:30:49 herbelin Exp $ 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_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 : int -> constr -> identifier Tacexpr.gsimple_clause -> tactic +(* +val instantiate_tac : tactic_arg list -> tactic +*) +val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate diff --git a/proofs/logic.ml b/proofs/logic.ml new file mode 100644 index 00000000..3cc44a0f --- /dev/null +++ b/proofs/logic.ml @@ -0,0 +1,786 @@ +(************************************************************************) +(* 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: logic.ml,v 1.80.2.1 2004/07/16 19:30:49 herbelin Exp $ *) + +open Pp +open Util +open Names +open Nameops +open Evd +open Term +open Termops +open Sign +open Environ +open Reductionops +open Inductive +open Inductiveops +open Typing +open Proof_trees +open Proof_type +open Typeops +open Type_errors +open Coqast +open Retyping +open Evarutil + +type refiner_error = + + (* Errors raised by the refiner *) + | BadType of constr * constr * constr + | OccurMeta of constr + | OccurMetaGoal of constr + | CannotApply of constr * constr + | NotWellTyped of constr + | 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 _))) -> 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; + let r = tac gl in + check := c; + r + +let with_check tac gl = + let c = !check in + check := true; + let r = tac gl in + check := c; + r + +(************************************************************************) +(************************************************************************) +(* 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 ncl = gl.evar_concl in + check_clear_forward rmv (global_vars_set env ncl) "conclusion"; + 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)] *) +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" + +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" + +let check_typability env sigma c = + if !check then let _ = type_of env sigma c in () + +let recheck_typability (what,id) env sigma t = + try check_typability env sigma t + with _ -> + let s = match what with + | None -> "the conclusion" + | Some id -> "hypothesis "^(string_of_id id) in + error + ("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') + + +(* Auxiliary functions for primitive MOVE tactic + * + * [move_after with_dep toleft (left,(hfrom,typfrom),right) hto] moves + * hyp [hfrom] just after the hyp [hto] which belongs to the hyps on the + * left side [left] of the full signature if [toleft=true] or to the hyps + * on the right side [right] if [toleft=false]. + * If [with_dep] then dependent hypotheses are moved accordingly. *) + +let split_sign hfrom hto l = + let rec splitrec left toleft = function + | [] -> error ("No such hypothesis : " ^ (string_of_id hfrom)) + | (hyp,c,typ) as d :: right -> + if hyp = hfrom then + (left,right,d,toleft) + else + splitrec (d::left) (toleft or (hyp = hto)) right + in + splitrec [] false l + +let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = + let env = Global.env() in + let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) = + if toleft + then occur_var_in_decl env hyp2 d + else occur_var_in_decl env hyp d2 + in + let rec moverec first middle = function + | [] -> error ("No such hypothesis : " ^ (string_of_id hto)) + | (hyp,_,_) as d :: right -> + let (first',middle') = + if List.exists (test_dep d) middle then + if with_dep & (hyp <> hto) then + (first, d::middle) + else + error + ("Cannot move "^(string_of_id idfrom)^" after " + ^(string_of_id hto) + ^(if toleft then ": it occurs in " else ": it depends on ") + ^(string_of_id hyp)) + else + (d::first, middle) + in + if hyp = hto then + (List.rev first')@(List.rev middle')@right + else + moverec first' middle' right + in + if toleft then + List.rev_append (moverec [] [declfrom] left) right + else + List.rev_append left (moverec [] [declfrom] right) + +let check_backward_dependencies sign d = + if not (Idset.for_all + (fun id -> mem_named_context id sign) + (global_vars_set_of_decl (Global.env()) d)) + then + error "Can't introduce at that location: free variable conflict" + + +let check_forward_dependencies id tail = + let env = Global.env() in + List.iter + (function (id',_,_ as decl) -> + if occur_var_in_decl env id decl then + error ((string_of_id id) ^ " is used in hypothesis " + ^ (string_of_id 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])) + +let replace_hyp sign id d = + apply_to_hyp sign id + (fun sign _ tail -> + if !check then + (check_backward_dependencies sign d; + check_forward_dependencies id tail); + add_named_decl d sign) + +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)) + +(************************************************************************) +(************************************************************************) +(* Implementation of the logical rules *) + +(* Will only be used on terms given to the Refine rule which have meta +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 + | (App _| Case _) -> fold_constr collrec acc c + | _ -> acc + in + List.rev(collrec [] c) + +let check_conv_leq_goal env sigma arg ty conclty = + if !check & not (is_conv_leq env sigma ty conclty) then + raise (RefinerError (BadType (arg,ty,conclty))) + +let goal_type_of env sigma c = + (if !check then type_of else Retyping.get_type_of) env sigma c + +let rec mk_refgoals sigma goal goalacc conclty trm = + let env = evar_env goal in + let hyps = goal.evar_hyps in +(* + if not (occur_meta trm) then + let t'ty = (unsafe_machine env sigma trm).uj_type in + let _ = conv_leq_goal env sigma trm t'ty conclty in + (goalacc,t'ty) + else +*) + match kind_of_term trm with + | Meta _ -> + if occur_meta conclty then + raise (RefinerError (OccurMetaGoal conclty)); + (mk_goal hyps (nf_betaiota conclty))::goalacc, conclty + + | 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'',conclty') = + mk_arggoals sigma goal acc' hdty (Array.to_list l) in + check_conv_leq_goal env sigma trm conclty' conclty; + (acc'',conclty') + + | Case (_,p,c,lf) -> + let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in + check_conv_leq_goal env sigma trm conclty' conclty; + let acc'' = + array_fold_left2 + (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi)) + acc' lbrty lf + in + (acc'',conclty') + + | _ -> + if occur_meta trm then raise (RefinerError (OccurMeta trm)); + let t'ty = goal_type_of env sigma trm in + check_conv_leq_goal env sigma trm t'ty conclty; + (goalacc,t'ty) + +(* Same as mkREFGOALS but without knowing te type of the term. Therefore, + * Metas should be casted. *) + +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 -> + check_typability env sigma ty; + (mk_goal hyps (nf_betaiota ty))::goalacc,ty + + | App (f,l) -> + let (acc',hdty) = mk_hdgoals sigma goal goalacc f in + mk_arggoals sigma goal acc' hdty (Array.to_list l) + + | Case (_,p,c,lf) -> + let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in + let acc'' = + array_fold_left2 + (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi)) + acc' lbrty lf + in + (acc'',conclty') + + | _ -> goalacc, goal_type_of env sigma trm + +and mk_arggoals sigma goal goalacc funty = function + | [] -> goalacc,funty + | harg::tlargs as allargs -> + let t = whd_betadeltaiota (evar_env goal) sigma funty in + match kind_of_term t with + | Prod (_,c1,b) -> + let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in + mk_arggoals sigma goal acc' (subst1 harg b) tlargs + | LetIn (_,c1,_,b) -> + mk_arggoals sigma goal goalacc (subst1 c1 b) allargs + | _ -> raise (RefinerError (CannotApply (t,harg))) + +and mk_casegoals sigma goal goalacc p c = + let env = evar_env goal in + let (acc',ct) = mk_hdgoals sigma goal goalacc c in + let (acc'',pt) = mk_hdgoals sigma goal acc' p in + let pj = {uj_val=p; uj_type=pt} in + let indspec = + try find_mrectype env sigma ct + with Not_found -> anomaly "mk_casegoals" in + let (lbrty,conclty) = + type_case_branches_with_names env indspec pj c in + (acc'',lbrty,conclty) + + +let error_use_instantiate () = + errorlabstrm "Logic.prim_refiner" + (str"cannot intro when there are open metavars in the domain type" ++ + spc () ++ str"- use Instantiate") + +let convert_hyp sign sigma (id,b,bt as d) = + apply_to_hyp sign id + (fun sign (_,c,ct) _ -> + let env = Global.env_of_context sign in + if !check && not (is_conv env sigma bt ct) && + not (option_compare (is_conv env sigma) b c) then + error "convert-hyp rule passed non-converting term"; + add_named_decl d sign) + + +(************************************************************************) +(************************************************************************) +(* Primitive tactics are handled here *) + +let prim_refiner r sigma goal = + let env = evar_env goal in + let sign = goal.evar_hyps in + let cl = goal.evar_concl in + match r with + (* Logical rules *) + | Intro id -> + if !check && mem_named_context id 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) + (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) + (subst1 (mkVar id) b) in + [sg] + | _ -> + raise (RefinerError IntroNeedsProduct)) + + | Intro_replacing id -> + (match kind_of_term (strip_outer_cast cl) with + | Prod (_,c1,b) -> + if occur_meta c1 then error_use_instantiate(); + let sign' = replace_hyp sign id (id,None,c1) in + let sg = mk_goal sign' (subst1 (mkVar id) b) in + [sg] + | LetIn (_,c1,t1,b) -> + if occur_meta c1 then error_use_instantiate(); + let sign' = replace_hyp sign id (id,Some c1,t1) in + let sg = mk_goal sign' (subst1 (mkVar id) b) in + [sg] + | _ -> + raise (RefinerError IntroNeedsProduct)) + + | Cut (b,id,t) -> + if !check && mem_named_context id 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 + if b then [sg1;sg2] else [sg2;sg1] + + | FixRule (f,n,rest) -> + let rec check_ind env k cl = + match kind_of_term (strip_outer_cast cl) with + | Prod (na,c1,b) -> + if k = 1 then + try + fst (find_inductive env sigma c1) + with Not_found -> + error "cannot do a fixpoint on a non inductive type" + else + check_ind (push_rel (na,None,c1) env) (k-1) b + | _ -> error "not enough products" + in + let (sp,_) = check_ind env n cl in + let all = (f,n,cl)::rest in + let rec mk_sign sign = function + | (f,n,ar)::oth -> + let (sp',_) = check_ind env n ar in + if not (sp=sp') then + error ("fixpoints should be on the same " ^ + "mutual inductive declaration"); + if !check && mem_named_context f sign then + error "name already used in the environment"; + mk_sign (add_named_decl (f,None,ar) sign) oth + | [] -> + List.map (fun (_,_,c) -> mk_goal sign c) all + in + mk_sign sign all + + | Cofix (f,others) -> + let rec check_is_coind env cl = + let b = whd_betadeltaiota env sigma cl in + match kind_of_term b with + | Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b + | _ -> + try + let _ = find_coinductive env sigma b in () + with Not_found -> + error ("All methods must construct elements " ^ + "in coinductive types") + in + let all = (f,cl)::others in + List.iter (fun (_,c) -> check_is_coind env c) all; + let rec mk_sign sign = function + | (f,ar)::oth -> + (try + (let _ = Sign.lookup_named f sign in + error "name already used in the environment") + with + | Not_found -> + mk_sign (add_named_decl (f,None,ar) sign) oth) + | [] -> List.map (fun (_,c) -> mk_goal sign c) all + in + mk_sign sign all + + | Refine c -> + if not (list_distinct (collect_meta_variables c)) then + raise (RefinerError (NonLinearProof c)); + let (sgl,cl') = mk_refgoals sigma goal [] cl c in + let sgl = List.rev sgl in + sgl + + (* Conversion rules *) + | 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 + [sg] + else + error "convert-concl rule passed non-converting term" + + | Convert_hyp (id,copt,ty) -> + [mk_goal (convert_hyp sign sigma (id,copt,ty)) cl] + + (* And now the structural rules *) + | Thin ids -> + [clear_hyps ids goal] + + | ThinBody ids -> + let clear_aux env id = + let env' = remove_hyp_body env sigma id in + 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 sg = mk_goal sign' cl in + [sg] + + | Move (withdep, hfrom, hto) -> + let (left,right,declfrom,toleft) = split_sign hfrom hto 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 + 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 + [mk_goal sign' cl'] + +(************************************************************************) +(************************************************************************) +(* Extracting a proof term from the proof tree *) + +(* Util *) +let rec rebind id1 id2 = function + | [] -> [] + | id::l -> + if id = id1 then id2::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' + +let prim_extractor subfun vl pft = + let cl = pft.goal.evar_concl in + match pft.ref with + | 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) + | 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) + | _ -> 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) + | 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) + | _ -> 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) + + | 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 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 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 names = Array.map (fun (f,_) -> Name f) all in + let newvl = List.fold_left (fun vl (id,_)->(id::vl)) (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 + plain_instance metamap cc + + (* Structural and conversion rules do not produce any proof *) + | Some (Prim (Convert_concl _),[pf]) -> + subfun vl pf + + | 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 *) + subfun vl pf + + | Some (Prim (ThinBody _),[pf]) -> + subfun vl pf + + | Some (Prim (Move _),[pf]) -> + subfun vl pf + + | Some (Prim (Rename (id1,id2)),[pf]) -> + subfun (rebind id1 id2 vl) pf + + | Some _ -> anomaly "prim_extractor" + + | 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 new file mode 100644 index 00000000..7eef22bd --- /dev/null +++ b/proofs/logic.mli @@ -0,0 +1,73 @@ +(************************************************************************) +(* 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: logic.mli,v 1.27.6.1 2004/07/16 19:30:49 herbelin Exp $ i*) + +(*i*) +open Names +open Term +open Sign +open Evd +open Environ +open Proof_type +(*i*) + +(* 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:\\ + [Intro]: no check that the name does not exist\\ + [Intro_after]: no check that the name does not exist and that variables in + its type does not escape their scope\\ + [Intro_replacing]: no check that the name does not exist and that + variables in its type does not escape their scope\\ + [Convert_hyp]: + no check that the name exist and that its type is convertible\\ +*) + +(* The primitive refiner. *) + +val prim_refiner : prim_rule -> evar_map -> goal -> goal list + +val prim_extractor : + (identifier list -> proof_tree -> constr) + -> identifier list -> proof_tree -> constr + +(*s Refiner errors. *) + +type refiner_error = + + (*i Errors raised by the refiner i*) + | BadType of constr * constr * constr + | OccurMeta of constr + | OccurMetaGoal of constr + | CannotApply of constr * constr + | NotWellTyped of constr + | 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 new file mode 100644 index 00000000..f53ea870 --- /dev/null +++ b/proofs/pfedit.ml @@ -0,0 +1,333 @@ +(************************************************************************) +(* 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: pfedit.ml,v 1.47.2.1 2004/07/16 19:30:49 herbelin Exp $ *) + +open Pp +open Util +open Names +open Nameops +open Sign +open Term +open Declarations +open Entries +open Environ +open Evd +open Typing +open Tacmach +open Proof_trees +open Tacexpr +open Proof_type +open Lib +open Safe_typing + +(*********************************************************************) +(* Managing the proofs state *) +(* Mainly contributed by C. Murthy *) +(*********************************************************************) + +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 } + +let proof_edits = + (Edit.empty() : (identifier,pftreestate,proof_topstate) Edit.t) + +let get_all_proof_names () = Edit.dom proof_edits + +let msg_proofs use_resume = + match Edit.dom proof_edits with + | [] -> (spc () ++ str"(No proof-editing in progress).") + | l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++ + (prlist_with_sep pr_spc pr_id (get_all_proof_names ())) ++ + str"." ++ + (if use_resume then (fnl () ++ str"Use \"Resume\" first.") + else (mt ())) +) + +let undo_default = 50 +let undo_limit = ref undo_default + +(*********************************************************************) +(* Functions for decomposing and modifying the proof state *) +(*********************************************************************) + +let get_state () = + match Edit.read proof_edits with + | None -> errorlabstrm "Pfedit.get_state" + (str"No focused proof" ++ msg_proofs true) + | Some(_,pfs,ts) -> (pfs,ts) + +let get_topstate () = snd(get_state()) +let get_pftreestate () = fst(get_state()) + +let get_end_tac () = let ts = get_topstate () in ts.top_end_tac + +let get_goal_context n = + let pftree = get_pftreestate () in + let goal = nth_goal_of_pftreestate n pftree in + (project goal, pf_env goal) + +let get_current_goal_context () = get_goal_context 1 + +let set_current_proof = Edit.focus proof_edits + +let resume_proof (loc,id) = + try + Edit.focus proof_edits id + with Invalid_argument "Edit.focus" -> + user_err_loc(loc,"Pfedit.set_proof",str"No such proof" ++ msg_proofs false) + +let suspend_proof () = + try + Edit.unfocus proof_edits + with Invalid_argument "Edit.unfocus" -> + errorlabstrm "Pfedit.suspend_current_proof" + (str"No active proof" ++ (msg_proofs true)) + +let resume_last_proof () = + match (Edit.last_focused proof_edits) with + | None -> + errorlabstrm "resume_last" (str"No proof-editing in progress.") + | Some p -> + Edit.focus proof_edits p + +let get_current_proof_name () = + match Edit.read proof_edits with + | None -> + errorlabstrm "Pfedit.get_proof" + (str"No focused proof" ++ msg_proofs true) + | Some(na,_,_) -> na + +let add_proof (na,pfs,ts) = + Edit.create proof_edits (na,pfs,ts,!undo_limit+1) + +let delete_proof_gen = Edit.delete proof_edits + +let delete_proof (loc,id) = + try + delete_proof_gen id + with (UserError ("Edit.delete",_)) -> + user_err_loc + (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false) + +let init_proofs () = Edit.clear proof_edits + +let mutate f = + try + Edit.mutate proof_edits (fun _ pfs -> f pfs) + with Invalid_argument "Edit.mutate" -> + errorlabstrm "Pfedit.mutate" + (str"No focused proof" ++ msg_proofs true) + +let start (na,ts) = + let pfs = mk_pftreestate ts.top_goal in + add_proof(na,pfs,ts) + +let restart_proof () = + match Edit.read proof_edits with + | None -> + errorlabstrm "Pfedit.restart" + (str"No focused proof to restart" ++ msg_proofs true) + | Some(na,_,ts) -> + delete_proof_gen na; + start (na,ts); + set_current_proof na + +let proof_term () = + extract_pftreestate (get_pftreestate()) + +(* Detect is one has completed a subtree of the initial goal *) +let subtree_solved () = + let pts = get_pftreestate () in + is_complete_proof (proof_of_pftreestate pts) & + not (is_top_pftreestate pts) + +(*********************************************************************) +(* Undo functions *) +(*********************************************************************) + +let set_undo = function + | None -> undo_limit := undo_default + | Some n -> + if n>=0 then + undo_limit := n + else + error "Cannot set a negative undo limit" + +let get_undo () = Some !undo_limit + +let undo n = + try + Edit.undo proof_edits n; + (* needed because the resolution of a subtree is done in 2 steps + then a sequence of undo can lead to a focus on a completely solved + subtree - this solution only works properly if undoing one step *) + if subtree_solved() then Edit.undo proof_edits 1 + with (Invalid_argument "Edit.undo") -> + errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true) + +(*********************************************************************) +(* Proof cooking *) +(*********************************************************************) + +let xml_cook_proof = ref (fun _ -> ()) +let set_xml_cook_proof f = xml_cook_proof := f + +let cook_proof () = + let (pfs,ts) = get_state() + and ident = get_current_proof_name () in + let {evar_concl=concl} = ts.top_goal + and strength = ts.top_strength in + let pfterm = extract_pftreestate pfs in + !xml_cook_proof (strength,pfs); + (ident, + ({ const_entry_body = pfterm; + const_entry_type = Some concl; + const_entry_opaque = true }, + strength, ts.top_hook)) + +let current_proof_statement () = + let ts = get_topstate() in + (get_current_proof_name (), ts.top_strength, + ts.top_goal.evar_concl, ts.top_hook) + +(*********************************************************************) +(* Abort functions *) +(*********************************************************************) + +let refining () = [] <> (Edit.dom proof_edits) + +let check_no_pending_proofs () = + if refining () then + errorlabstrm "check_no_pending_proofs" + (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++ + str"Use \"Abort All\" first or complete proof(s).") + +let delete_current_proof () = delete_proof_gen (get_current_proof_name ()) + +let delete_all_proofs = init_proofs + +(*********************************************************************) +(* Modifying the end tactic of the current profftree *) +(*********************************************************************) +let set_end_tac tac = + let top = get_topstate () in + top.top_end_tac <- Some tac + +(*********************************************************************) +(* Modifying the current prooftree *) +(*********************************************************************) + +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} + in + start(na,ts); + set_current_proof na + + +let solve_nth k tac = + let pft = get_pftreestate () in + if not (List.mem (-1) (cursor_of_pftreestate pft)) then + mutate (solve_nth_pftreestate k tac) + else + error "cannot apply a tactic when we are descended behind a tactic-node" + +let by tac = mutate (solve_pftreestate tac) + +let instantiate_nth_evar_com n c = + mutate (Evar_refiner.instantiate_pf_com n c) + +let traverse n = mutate (traverse n) + +(* [traverse_to path] + + Traverses the current proof to get to the location specified by + [path]. + + ALGORITHM: The algorithm works on reversed paths. One just has to remove + the common part on the reversed paths. + +*) + +let common_ancestor l1 l2 = + let rec common_aux l1 l2 = + match l1, l2 with + | a1::l1', a2::l2' when a1 = a2 -> common_aux l1' l2' + | _, _ -> List.rev l1, List.length l2 + in + common_aux (List.rev l1) (List.rev l2) + +let rec traverse_up = function + | 0 -> (function pf -> pf) + | n -> (function pf -> Tacmach.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)) + +let traverse_to path = + let up_and_down path pfs = + let cursor = cursor_of_pftreestate pfs in + let down_list, up_count = common_ancestor path cursor in + traverse_down down_list (traverse_up up_count pfs) + in + mutate (up_and_down path) + +(* traverse the proof tree until it reach the nth subgoal *) +let traverse_nth_goal n = mutate (nth_unproven n) + +let traverse_prev_unproven () = mutate prev_unproven + +let traverse_next_unproven () = mutate next_unproven + + +(* The goal focused on *) +let focus_n = ref 0 +let make_focus n = focus_n := n +let focus () = !focus_n +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 new file mode 100644 index 00000000..e95881ba --- /dev/null +++ b/proofs/pfedit.mli @@ -0,0 +1,183 @@ +(************************************************************************) +(* 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: pfedit.mli,v 1.35.2.1 2004/07/16 19:30:49 herbelin Exp $ i*) + +(*i*) +open Util +open Pp +open Names +open Term +open Sign +open Environ +open Decl_kinds +open Tacmach +open Tacexpr +(*i*) + +(*s Several proofs can be opened simultaneously but at most one is + focused at some time. The following functions work by side-effect + on current set of open proofs. In this module, ``proofs'' means an + open proof (something started by vernacular command [Goal], [Lemma] + or [Theorem]), and ``goal'' means a subgoal of the current focused + proof *) + +(*s [refining ()] tells if there is some proof in progress, even if a not + focused one *) + +val refining : unit -> bool + +(* [check_no_pending_proofs ()] fails if there is still some proof in + progress *) + +val check_no_pending_proofs : unit -> unit + +(*s [delete_proof name] deletes proof of name [name] or fails if no proof + has this name *) + +val delete_proof : identifier located -> unit + +(* [delete_current_proof ()] deletes current focused proof or fails if + no proof is focused *) + +val delete_current_proof : unit -> unit + +(* [delete_all_proofs ()] deletes all open proofs if any *) + +val delete_all_proofs : unit -> unit + +(*s [undo n] undoes the effect of the last [n] tactics applied to the + current proof; it fails if no proof is focused or if the ``undo'' + stack is exhausted *) + +val undo : int -> unit + +(* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None] + sets the size to the default value (12) *) + +val set_undo : int option -> unit +val get_undo : unit -> int option + +(*s [start_proof s str env t hook] starts a proof of name [s] and conclusion + [t]; [hook] is optionally a function to be applied at proof end (e.g. to + declare the built constructions as a coercion or a setoid morphism) *) + +val start_proof : + identifier -> goal_kind -> named_context -> constr + -> declaration_hook -> unit + +(* [restart_proof ()] restarts the current focused proof from the beginning + or fails if no proof is focused *) + +val restart_proof : unit -> unit + +(*s [resume_last_proof ()] focus on the last unfocused proof or fails + if there is no suspended proofs *) + +val resume_last_proof : unit -> unit + +(* [resume_proof name] focuses on the proof of name [name] or + raises [UserError] if no proof has name [name] *) + +val resume_proof : identifier located -> unit + +(* [suspend_proof ()] unfocuses the current focused proof or + failed with [UserError] if no proof is currently focused *) + +val suspend_proof : unit -> unit + +(*s [cook_proof opacity] turns the current proof (assumed completed) into + a constant with its name, kind and possible hook (see [start_proof]); + it fails if there is no current proof of if it is not completed *) + +val cook_proof : unit -> + identifier * (Entries.definition_entry * goal_kind * declaration_hook) + +(* To export completed proofs to xml *) +val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit + +(*s [get_pftreestate ()] returns the current focused pending proof or + raises [UserError "no focused proof"] *) + +val get_pftreestate : unit -> pftreestate + +(* [get_end_tac ()] returns the current tactic to apply to all new subgoal *) + +val get_end_tac : unit -> tactic option + +(* [get_goal_context n] returns the context of the [n]th subgoal of + the current focused proof or raises a [UserError] if there is no + focused proof or if there is no more subgoals *) + +val get_goal_context : int -> Evd.evar_map * env + +(* [get_current_goal_context ()] works as [get_goal_context 1] *) + +val get_current_goal_context : unit -> Evd.evar_map * env + +(* [current_proof_statement] *) + +val current_proof_statement : + unit -> identifier * goal_kind * types * declaration_hook + +(*s [get_current_proof_name ()] return the name of the current focused + proof or failed if no proof is focused *) + +val get_current_proof_name : unit -> identifier + +(* [get_all_proof_names ()] returns the list of all pending proof names *) + +val get_all_proof_names : unit -> identifier list + +(*s [set_end_tac tac] applies tactic [tac] to all subgoal generate + by [solve_nth] *) + +val set_end_tac : tactic -> unit + +(*s [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the + current focused proof or raises a UserError if no proof is focused or + if there is no [n]th subgoal *) + +val solve_nth : int -> tactic -> unit + +(* [by tac] applies tactic [tac] to the 1st subgoal of the current + focused proof or raises a UserError if there is no focused proof or + if there is no more subgoals *) + +val by : tactic -> unit + +(* [instantiate_nth_evar_com n c] instantiate the [n]th undefined + existential variable of the current focused proof by [c] or raises a + UserError if no proof is focused or if there is no such [n]th + existential variable *) + +val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit + +(*s To deal with subgoal focus *) + +val make_focus : int -> unit +val focus : unit -> int +val focused_goal : unit -> int +val subtree_solved : unit -> bool + +val reset_top_of_tree : unit -> unit +val traverse : int -> unit +val traverse_nth_goal : int -> unit +val traverse_next_unproven : unit -> unit +val traverse_prev_unproven : unit -> unit + + +(* These two functions make it possible to implement more elaborate + 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 new file mode 100644 index 00000000..aaf54a36 --- /dev/null +++ b/proofs/proof_trees.ml @@ -0,0 +1,253 @@ +(************************************************************************) +(* 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: proof_trees.ml,v 1.53.2.1 2004/07/16 19:30:49 herbelin Exp $ *) + +open Closure +open Util +open Names +open Nameops +open Term +open Termops +open Sign +open Evd +open Environ +open Evarutil +open Proof_type +open Tacred +open Typing +open Libnames +open Nametab + +(* +let is_bind = function + | Tacexpr.Cbindings _ -> true + | _ -> false +*) + +(* Functions on goals *) + +let mk_goal hyps cl = + { evar_hyps = hyps; evar_concl = cl; + evar_body = Evar_empty} + +(* Functions on proof trees *) + +let ref_of_proof pf = + match pf.ref with + | None -> failwith "rule_of_proof" + | Some r -> r + +let rule_of_proof pf = + let (r,_) = ref_of_proof pf in r + +let children_of_proof pf = + let (_,cl) = ref_of_proof pf in cl + +let goal_of_proof pf = pf.goal + +let subproof_of_proof pf = match pf.ref with + | Some (Tactic (_,pf), _) -> pf + | _ -> failwith "subproof_of_proof" + +let status_of_proof pf = pf.open_subgoals + +let is_complete_proof pf = pf.open_subgoals = 0 + +let is_leaf_proof pf = (pf.ref = None) + +let is_tactic_proof pf = match pf.ref with + | Some (Tactic _, _) -> true + | _ -> 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 + +let pf_lookup_index_as_renamed env ccl n = + Detyping.lookup_index_as_renamed env ccl n + +(*********************************************************************) +(* Pretty printing functions *) +(*********************************************************************) + +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 env = evar_env g in + let penv = pr_context_of env in + let pc = prterm_env_at_top 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 new file mode 100644 index 00000000..c31d5207 --- /dev/null +++ b/proofs/proof_trees.mli @@ -0,0 +1,68 @@ +(************************************************************************) +(* 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: proof_trees.mli,v 1.27.2.1 2004/07/16 19:30:49 herbelin Exp $ i*) + +(*i*) +open Util +open Names +open Term +open Sign +open Evd +open Environ +open Proof_type +(*i*) + +(* This module declares readable constraints, and a few utilities on + constraints and proof trees *) + +val mk_goal : named_context -> constr -> goal + +val rule_of_proof : proof_tree -> rule +val ref_of_proof : proof_tree -> (rule * proof_tree list) +val children_of_proof : proof_tree -> proof_tree list +val goal_of_proof : proof_tree -> goal +val subproof_of_proof : proof_tree -> proof_tree +val status_of_proof : proof_tree -> int +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 + + +(*s Pretty printing functions. *) + +(*i*) +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 diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml new file mode 100644 index 00000000..cbed5e27 --- /dev/null +++ b/proofs/proof_type.ml @@ -0,0 +1,101 @@ +(************************************************************************) +(* 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: proof_type.ml,v 1.29.2.1 2004/07/16 19:30:49 herbelin Exp $ *) + +(*i*) +open Environ +open Evd +open Names +open Libnames +open Term +open Util +open Tacexpr +open Rawterm +open Genarg +open Nametab +open Pattern +(*i*) + +(* This module defines the structure of proof tree and the tactic type. So, it + is used by Proof_tree and Refiner *) + +type prim_rule = + | Intro of identifier + | Intro_replacing of identifier + | Cut of bool * identifier * types + | FixRule of identifier * int * (identifier * int * constr) list + | Cofix of identifier * (identifier * constr) list + | Refine of constr + | Convert_concl of types + | 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 + and gave [l] as subproofs to be completed. + if [ref = (Some(Tactic (t,p),l))] then [p] is the proof + that the goal can be proven if the goals in [l] are solved. *) +type proof_tree = { + open_subgoals : int; + goal : goal; + ref : (rule * proof_tree list) option } + +and rule = + | Prim of prim_rule + | Tactic of tactic_expr * proof_tree + | Change_evars + +and goal = evar_info + +and tactic = goal sigma -> (goal list sigma * validation) + +and validation = (proof_tree list -> proof_tree) + +and tactic_expr = + (constr, + constr_pattern, + evaluable_global_reference, + inductive, + ltac_constant, + identifier, + glob_tactic_expr) + Tacexpr.gen_tactic_expr + +and atomic_tactic_expr = + (constr, + constr_pattern, + evaluable_global_reference, + inductive, + ltac_constant, + identifier, + glob_tactic_expr) + Tacexpr.gen_atomic_tactic_expr + +and tactic_arg = + (constr, + constr_pattern, + evaluable_global_reference, + inductive, + ltac_constant, + identifier, + glob_tactic_expr) + Tacexpr.gen_tactic_arg + +type hyp_location = identifier Tacexpr.raw_hyp_location + diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli new file mode 100644 index 00000000..42606552 --- /dev/null +++ b/proofs/proof_type.mli @@ -0,0 +1,128 @@ +(************************************************************************) +(* 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: proof_type.mli,v 1.33.2.1 2004/07/16 19:30:49 herbelin Exp $ i*) + +(*i*) +open Environ +open Evd +open Names +open Libnames +open Term +open Util +open Tacexpr +open Rawterm +open Genarg +open Nametab +open Pattern +(*i*) + +(* This module defines the structure of proof tree and the tactic type. So, it + is used by [Proof_tree] and [Refiner] *) + +type prim_rule = + | Intro of identifier + | Intro_replacing of identifier + | Cut of bool * identifier * types + | FixRule of identifier * int * (identifier * int * constr) list + | Cofix of identifier * (identifier * constr) list + | Refine of constr + | Convert_concl of types + | Convert_hyp of named_declaration + | Thin of identifier list + | ThinBody of identifier list + | Move of bool * identifier * identifier + | Rename of identifier * identifier + +(* The type [goal sigma] is the type of subgoal. It has the following form +\begin{verbatim} + it = { evar_concl = [the conclusion of the subgoal] + evar_hyps = [the hypotheses of the subgoal] + evar_body = Evar_Empty; + evar_info = { pgm : [The Realizer pgm if any] + lc : [Set of evar num occurring in subgoal] }} + sigma = { stamp = [an int characterizing the ed field, for quick compare] + ed : [A set of existential variables depending in the subgoal] + number of first evar, + it = { evar_concl = [the type of first evar] + evar_hyps = [the context of the evar] + evar_body = [the body of the Evar if any] + evar_info = { pgm : [Useless ??] + lc : [Set of evars occurring + in the type of evar] } }; + ... + number of last evar, + it = { evar_concl = [the type of evar] + evar_hyps = [the context of the evar] + evar_body = [the body of the Evar if any] + evar_info = { pgm : [Useless ??] + lc : [Set of evars occurring + in the type of evar] } } } + } +\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 + and gave [l] as subproofs to be completed. + if [ref = (Some(Tactic (t,p),l))] then [p] is the proof + that the goal can be proven if the goals in [l] are solved. *) +type proof_tree = { + open_subgoals : int; + goal : goal; + ref : (rule * proof_tree list) option } + +and rule = + | Prim of prim_rule + | Tactic of tactic_expr * proof_tree + | Change_evars + +and goal = evar_info + +and tactic = goal sigma -> (goal list sigma * validation) + +and validation = (proof_tree list -> proof_tree) + +and tactic_expr = + (constr, + constr_pattern, + evaluable_global_reference, + inductive, + ltac_constant, + identifier, + glob_tactic_expr) + Tacexpr.gen_tactic_expr + +and atomic_tactic_expr = + (constr, + constr_pattern, + evaluable_global_reference, + inductive, + ltac_constant, + identifier, + glob_tactic_expr) + Tacexpr.gen_atomic_tactic_expr + +and tactic_arg = + (constr, + constr_pattern, + evaluable_global_reference, + inductive, + ltac_constant, + identifier, + glob_tactic_expr) + Tacexpr.gen_tactic_arg + +type hyp_location = identifier Tacexpr.raw_hyp_location diff --git a/proofs/refiner.ml b/proofs/refiner.ml new file mode 100644 index 00000000..55f11d52 --- /dev/null +++ b/proofs/refiner.ml @@ -0,0 +1,1030 @@ +(************************************************************************) +(* 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: refiner.ml,v 1.67.2.1 2004/07/16 19:30:49 herbelin Exp $ *) + +open Pp +open Util +open Term +open Termops +open Sign +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) + +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 pf_status pf = pf.open_subgoals + +let is_complete pf = (0 = (pf_status pf)) + +let on_open_proofs f pf = if is_complete pf then pf else f pf + +let and_status = List.fold_left (+) 0 + +(* 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 *) +let norm_goal sigma gl = + let red_fun = Evarutil.nf_evar sigma in + 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_body = gl.evar_body} in + if ngl = gl then None else Some ngl + + +(* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]] + gives + [ (v1 [p_1 ... p_l1]) ; (v2 [ p_(l1+1) ... p_(l1+l2) ]) ; ... ; + (vk [ p_(l1+...+l(k-1)+1) ... p_(l1+...lk) ]) ] + *) + +let rec mapshape nl (fl : (proof_tree list -> proof_tree) list) + (l : proof_tree list) = + match nl with + | [] -> [] + | h::t -> + let m,l = list_chop h l in + (List.hd fl m) :: (mapshape t (List.tl fl) l) + +(* [frontier : proof_tree -> goal list * validation] + given a proof [p], [frontier p] gives [(l,v)] where [l] is the list of goals + to be solved to complete the proof, and [v] is the corresponding + validation *) + +let rec frontier p = + match p.ref with + | None -> + ([p.goal], + (fun lp' -> + let p' = List.hd lp' in + if p'.goal = p.goal then + p' + else + errorlabstrm "Refiner.frontier" + (str"frontier was handed back a ill-formed proof."))) + | Some(r,pfl) -> + let gll,vl = List.split(List.map frontier pfl) in + (List.flatten gll, + (fun retpfl -> + let pfl' = mapshape (List.map List.length gll) vl retpfl in + { open_subgoals = and_status (List.map pf_status pfl'); + goal = p.goal; + ref = Some(r,pfl')})) + + +let rec frontier_map_rec f n p = + if n < 1 || n > p.open_subgoals then p else + match p.ref with + | None -> + let p' = f p in + if p'.goal == p.goal || p'.goal = p.goal then p' + else + errorlabstrm "Refiner.frontier_map" + (str"frontier_map was handed back a ill-formed proof.") + | Some(r,pfl) -> + let (_,rpfl') = + List.fold_left + (fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc)) + (n,[]) pfl in + let pfl' = List.rev rpfl' in + { open_subgoals = and_status (List.map pf_status pfl'); + goal = p.goal; + ref = Some(r,pfl')} + +let frontier_map f n p = + let nmax = p.open_subgoals in + let n = if n < 0 then nmax + n + 1 else n in + if n < 1 || n > nmax then + errorlabstrm "Refiner.frontier_map" (str "No such subgoal"); + frontier_map_rec f n p + +let rec frontier_mapi_rec f i p = + if p.open_subgoals = 0 then p else + match p.ref with + | None -> + let p' = f i p in + if p'.goal == p.goal || p'.goal = p.goal then p' + else + errorlabstrm "Refiner.frontier_mapi" + (str"frontier_mapi was handed back a ill-formed proof.") + | Some(r,pfl) -> + let (_,rpfl') = + List.fold_left + (fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc)) + (i,[]) pfl in + let pfl' = List.rev rpfl' in + { open_subgoals = and_status (List.map pf_status pfl'); + goal = p.goal; + ref = Some(r,pfl')} + +let frontier_mapi f p = frontier_mapi_rec f 1 p + +(* [list_pf p] is the lists of goals to be solved in order to complete the + proof [p] *) + +let list_pf p = fst (frontier p) + +let rec nb_unsolved_goals pf = pf.open_subgoals + +(* leaf g is the canonical incomplete proof of a goal g *) + +let leaf g = { + open_subgoals = 1; + goal = g; + ref = None } + +(* Tactics table. *) + +let tac_tab = Hashtbl.create 17 + +let add_tactic s t = + if Hashtbl.mem tac_tab s then + errorlabstrm ("Refiner.add_tactic: ") + (str ("Cannot redeclare tactic "^s)); + Hashtbl.add tac_tab s t + +let overwriting_add_tactic s t = + if Hashtbl.mem tac_tab s then begin + Hashtbl.remove tac_tab s; + warning ("Overwriting definition of tactic "^s) + end; + Hashtbl.add tac_tab s t + +let lookup_tactic s = + try + Hashtbl.find tac_tab s + with Not_found -> + errorlabstrm "Refiner.lookup_tactic" + (str"The tactic " ++ str s ++ str" is not installed") + + +(* refiner r is a tactic applying the rule r *) + +let bad_subproof () = + anomalylabstrm "Refiner.refiner" (str"Bad subproof in validation.") + +let check_subproof_connection gl spfl = + if not (list_for_all2eq (fun g pf -> g=pf.goal) gl spfl) + then (bad_subproof (); false) else true + +let abstract_tactic_expr te tacfun gls = + let (sgl_sigma,v) = tacfun gls in + let hidden_proof = v (List.map leaf sgl_sigma.it) in + (sgl_sigma, + fun spfl -> + assert (check_subproof_connection sgl_sigma.it spfl); + { open_subgoals = and_status (List.map pf_status spfl); + goal = gls.it; + ref = Some(Tactic(te,hidden_proof),spfl) }) + +let refiner = function + | Prim pr as r -> + let prim_fun = prim_refiner pr in + (fun goal_sigma -> + let sgl = prim_fun goal_sigma.sigma goal_sigma.it in + ({it=sgl; sigma = goal_sigma.sigma}, + (fun spfl -> + assert (check_subproof_connection sgl spfl); + { open_subgoals = and_status (List.map pf_status spfl); + goal = goal_sigma.it; + ref = Some(r,spfl) }))) + + | Tactic _ -> failwith "Refiner: should not occur" + + (* [Local_constraints lc] makes the local constraints be [lc] and + normalizes evars *) + + | Change_evars as r -> + (fun goal_sigma -> + let gl = goal_sigma.it in + (match norm_goal goal_sigma.sigma gl with + Some ngl -> + ({it=[ngl];sigma=goal_sigma.sigma}, + (fun spfl -> + assert (check_subproof_connection [ngl] spfl); + { open_subgoals = (List.hd spfl).open_subgoals; + goal = gl; + ref = Some(r,spfl) })) + (* if the evar change does not affect the goal, leave the + proof tree unchanged *) + | None -> ({it=[gl];sigma=goal_sigma.sigma}, + (fun spfl -> + assert (List.length spfl = 1); + List.hd spfl)))) + + +let local_Constraints gl = refiner Change_evars gl + +let norm_evar_tac = local_Constraints + +(* +let vernac_tactic (s,args) = + let tacfun = lookup_tactic s args in + abstract_extra_tactic s args tacfun +*) +let abstract_tactic te = abstract_tactic_expr (Tacexpr.TacAtom (dummy_loc,te)) + +let abstract_extended_tactic s args = + abstract_tactic (Tacexpr.TacExtend (dummy_loc, s, args)) + +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 + and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)] + where the mi are metavariables numbers, and ci are their types. + Their proof should be completed in order to complete the initial proof *) + +let extract_open_proof sigma pf = + let next_meta = + let meta_cnt = ref 0 in + let rec f () = + incr meta_cnt; + if in_dom sigma (existential_of_int !meta_cnt) then f () + else !meta_cnt + in f + in + let open_obligations = ref [] in + let rec proof_extractor vl = function + | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf + + | {ref=Some(Tactic (_,hidden_proof),spfl)} -> + let sgl,v = frontier hidden_proof in + let flat_proof = v spfl in + proof_extractor vl flat_proof + + | {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf + + | {ref=None;goal=goal} -> + let visible_rels = + map_succeed + (fun id -> + try let n = list_index id vl in (n,id) + with Not_found -> failwith "caught") + (ids_of_named_context 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)) + sorted_rels in + let abs_concl = + List.fold_right (fun (_,decl) c -> mkNamedProd_or_LetIn decl c) + sorted_env goal.evar_concl in + let inst = List.filter (fun (_,(_,b,_)) -> b = None) sorted_env in + let meta = next_meta () in + 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" + in + let pfterm = proof_extractor [] pf in + (pfterm, List.rev !open_obligations) + +(*********************) +(* Tacticals *) +(*********************) + +(* unTAC : tactic -> goal sigma -> proof sigma *) + +let unTAC tac g = + let (gl_sigma,v) = tac g in + { it = v (List.map leaf gl_sigma.it); sigma = gl_sigma.sigma } + +let unpackage glsig = (ref (glsig.sigma)),glsig.it + +let repackage r v = {it=v;sigma = !r} + +let apply_sig_tac r tac g = + check_for_interrupt (); (* Breakpoint *) + let glsigma,v = tac (repackage r g) in + r := glsigma.sigma; + (glsigma.it,v) + +let idtac_valid = function + [pf] -> pf + | _ -> anomaly "Refiner.idtac_valid" + +(* [goal_goal_list : goal sigma -> goal list sigma] *) +let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma} + +(* identity tactic without any message *) +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 + +(* 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 + +(* The Fail tactic *) +let tclFAIL lvl s g = raise (FailError (lvl,s)) + +let start_tac gls = + let (sigr,g) = unpackage gls in + (sigr,[g],idtac_valid) + +let finish_tac (sigr,gl,p) = (repackage sigr gl, p) + +(* Apply [taci.(i)] on the first n-th subgoals and [tac] on the others *) +let thensf_tac taci tac (sigr,gs,p) = + let n = Array.length taci in + let nsg = List.length gs in + if nsg<n then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals."); + let gll,pl = + List.split + (list_map_i (fun i -> apply_sig_tac sigr (if i<n then taci.(i) else tac)) + 0 gs) in + (sigr, List.flatten gll, + compose p (mapshape (List.map List.length gll) pl)) + +(* Apply [taci.(i)] on the last n-th subgoals and [tac] on the others *) +let thensl_tac tac taci (sigr,gs,p) = + let n = Array.length taci in + let nsg = List.length gs in + if nsg<n then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals."); + let gll,pl = + List.split + (list_map_i (fun i -> apply_sig_tac sigr (if i<0 then tac else taci.(i))) + (n-nsg) gs) in + (sigr, List.flatten gll, + compose p (mapshape (List.map List.length gll) pl)) + +(* Apply [tac i] on the ith subgoal (no subgoals number check) *) +let thensi_tac tac (sigr,gs,p) = + let gll,pl = + List.split (list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs) in + (sigr, List.flatten gll, compose p (mapshape (List.map List.length gll) pl)) + +let then_tac tac = thensf_tac [||] tac + +let non_existent_goal n = + errorlabstrm ("No such goal: "^(string_of_int n)) + (str"Trying to apply a tactic to a non existent goal") + +(* Apply tac on the i-th goal (if i>0). If i<0, then start counting from + the last goal (i=-1). *) +let theni_tac i tac ((_,gl,_) as subgoals) = + let nsg = List.length gl in + let k = if i < 0 then nsg + i + 1 else i in + if nsg < 1 then errorlabstrm "theni_tac" (str"No more subgoals.") + else if k >= 1 & k <= nsg then + thensf_tac + (Array.init k (fun i -> if i+1 = k then tac else tclIDTAC)) tclIDTAC + subgoals + else non_existent_goal k + +(* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1] + to [gls] and applies [t1], ..., [tn] to the [n] first resulting + subgoals, and [tac2] to the others subgoals. Raises an error if + the number of resulting subgoals is strictly less than [n] *) +let tclTHENSFIRSTn tac1 taci tac gls = + finish_tac (thensf_tac taci tac (then_tac tac1 (start_tac gls))) + +(* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1] + to [gls] and applies [t1], ..., [tn] to the [n] last resulting + subgoals, and [tac2] to the other subgoals. Raises an error if the + number of resulting subgoals is strictly less than [n] *) +let tclTHENSLASTn tac1 tac taci gls = + finish_tac (thensl_tac tac taci (then_tac tac1 (start_tac gls))) + +(* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies + [(taci i)] to the i_th resulting subgoal (starting from 1), whatever the + number of subgoals is *) +let tclTHEN_i tac taci gls = + finish_tac (thensi_tac taci (then_tac tac (start_tac gls))) + +let tclTHENLASTn tac1 taci = tclTHENSLASTn tac1 tclIDTAC taci +let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC + +(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [tac2] to every resulting subgoals *) +let tclTHEN tac1 tac2 = tclTHENSFIRSTn tac1 [||] tac2 + +(* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to + [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises + an error if the number of resulting subgoals is not [n] *) +let tclTHENSV tac1 tac2v = + tclTHENSFIRSTn tac1 tac2v (tclFAIL_s "Wrong number of tactics.") + +let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l) + +(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the last resulting subgoal *) +let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|] + +(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the first resulting subgoal *) +let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC + + +(* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More + convenient than [tclTHEN] when [n] is large. *) +let rec tclTHENLIST = function + [] -> tclIDTAC + | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl) + + + + +(* various progress criterions *) +let same_goal gl subgoal = + (hypotheses subgoal) = (hypotheses gl) & + eq_constr (conclusion subgoal) (conclusion gl) + + +let weak_progress gls ptree = + (List.length gls.it <> 1) or + (not (same_goal (List.hd gls.it) ptree.it)) + +(* Il y avait ici un ts_eq ........ *) +let progress gls ptree = + (weak_progress gls ptree) or + (not (ptree.sigma == gls.sigma)) + + +(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves +the goal unchanged *) +let tclPROGRESS tac ptree = + let rslt = tac ptree in + if progress (fst rslt) ptree then rslt + else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.") + +(* weak_PROGRESS tac ptree applies tac to the goal ptree and fails + if tac leaves the goal unchanged, possibly modifying sigma *) +let tclWEAK_PROGRESS tac ptree = + let rslt = tac ptree in + if weak_progress (fst rslt) ptree then rslt + else errorlabstrm "Refiner.tclWEAK_PROGRESS" (str"Failed to progress.") + + +(* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals, + one of them being identical to the original goal *) +let tclNOTSAMEGOAL (tac : tactic) goal = + let rslt = tac goal in + let gls = (fst rslt).it in + if List.exists (same_goal goal.it) gls + then errorlabstrm "Refiner.tclNOTSAMEGOAL" + (str"Tactic generated a subgoal identical to the original goal.") + else rslt + + + +(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) +let tclORELSE0 t1 t2 g = + try + t1 g + with (* Breakpoint *) + | e when catchable_exception e -> check_for_interrupt (); t2 g + | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) -> + check_for_interrupt (); t2 g + | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) + | Stdpp.Exc_located (s,FailError (lvl,s')) -> + raise (Stdpp.Exc_located (s,FailError (lvl - 1, s'))) + +(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, + then applies t2 *) +let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 + +(* TRY f tries to apply f, and if it fails, leave the goal unchanged *) +let tclTRY f = (tclORELSE0 f tclIDTAC) + +let tclTHENTRY f g = (tclTHEN f (tclTRY g)) + +(* Try the first tactic that does not fail in a list of tactics *) + +let rec tclFIRST = function + | [] -> tclFAIL_s "No applicable tactic." + | t::rest -> tclORELSE0 t (tclFIRST rest) + +let ite_gen tcal tac_if continue tac_else gl= + let success=ref false in + let tac_if0 gl= + let result=tac_if gl in + success:=true;result in + let tac_else0 e gl= + if !success then + raise e + else + tac_else gl in + try + tcal tac_if0 continue gl + with (* Breakpoint *) + | e when catchable_exception e -> + check_for_interrupt (); tac_else0 e gl + | (FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))) as e -> + check_for_interrupt (); tac_else0 e gl + | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) + | Stdpp.Exc_located (s,FailError (lvl,s')) -> + raise (Stdpp.Exc_located (s,FailError (lvl - 1, s'))) + +(* Try the first tactic and, if it succeeds, continue with + the second one, and if it fails, use the third one *) + +let tclIFTHENELSE=ite_gen tclTHEN + +(* Idem with tclTHENS and tclTHENSV *) + +let tclIFTHENSELSE=ite_gen tclTHENS + +let tclIFTHENSVELSE=ite_gen tclTHENSV + + +(* Fails if a tactic did not solve the goal *) +let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") + +(* Try the first thats solves the current goal *) +let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) + + +(* Iteration tacticals *) + +let tclDO n t = + let rec dorec k = + if k < 0 then errorlabstrm "Refiner.tclDO" + (str"Wrong argument : Do needs a positive integer."); + if k = 0 then tclIDTAC + else if k = 1 then t else (tclTHEN t (dorec (k-1))) + in + dorec n + +(* Beware: call by need of CAML, g is needed *) +let rec tclREPEAT t g = + (tclORELSE (tclTHEN t (tclREPEAT t)) tclIDTAC) g + +let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) + +(* Repeat on the first subgoal (no failure if no more subgoal) *) +let rec tclREPEAT_MAIN t g = + (tclORELSE (tclTHEN_i t (fun i -> if i = 1 then (tclREPEAT_MAIN t) else + tclIDTAC)) tclIDTAC) g + +(*s Tactics handling a list of goals. *) + +type validation_list = proof_tree list -> proof_tree list + +type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list + +(* Functions working on goal list for correct backtracking in Prolog *) + +let tclFIRSTLIST = tclFIRST +let tclIDTAC_list gls = (gls, fun x -> x) + +(* first_goal : goal list sigma -> goal sigma *) + +let first_goal gls = + let gl = gls.it and sig_0 = gls.sigma in + if gl = [] then error "first_goal"; + { it = List.hd gl; sigma = sig_0 } + +(* goal_goal_list : goal sigma -> goal list sigma *) + +let goal_goal_list gls = + let gl = gls.it and sig_0 = gls.sigma in { it = [gl]; sigma = sig_0 } + +(* tactic -> tactic_list : Apply a tactic to the first goal in the list *) + +let apply_tac_list tac glls = + let (sigr,lg) = unpackage glls in + match lg with + | (g1::rest) -> + let (gl,p) = apply_sig_tac sigr tac g1 in + let n = List.length gl in + (repackage sigr (gl@rest), + fun pfl -> let (pfg,pfrest) = list_chop n pfl in (p pfg)::pfrest) + | _ -> error "apply_tac_list" + +let then_tactic_list tacl1 tacl2 glls = + let (glls1,pl1) = tacl1 glls in + let (glls2,pl2) = tacl2 glls1 in + (glls2, compose pl1 pl2) + +(* Transform a tactic_list into a tactic *) + +let tactic_list_tactic tac gls = + let (glres,vl) = tac (goal_goal_list gls) in + (glres, compose idtac_valid vl) + + + + +(* The type of proof-trees state and a few utilities + A proof-tree state is built from a proof-tree, a set of global + constraints, and a stack which allows to navigate inside the + proof-tree remembering how to rebuild the global proof-tree + possibly after modification of one of the focused children proof-tree. + The number in the stack corresponds to + either the selected subtree and the validation is a function from a + proof-tree list consisting only of one proof-tree to the global + proof-tree + or -1 when the move is done behind a registered tactic in which + case the validation corresponds to a constant function giving back + the original proof-tree. *) + +type pftreestate = { + tpf : proof_tree ; + tpfsigma : evar_map; + tstack : (int * validation) list } + +let proof_of_pftreestate pts = pts.tpf +let is_top_pftreestate pts = pts.tstack = [] +let cursor_of_pftreestate pts = List.map fst pts.tstack +let evc_of_pftreestate pts = pts.tpfsigma + +let top_goal_of_pftreestate pts = + { it = goal_of_proof pts.tpf; sigma = pts.tpfsigma } + +let nth_goal_of_pftreestate n pts = + let goals = fst (frontier pts.tpf) in + try {it = List.nth goals (n-1); sigma = pts.tpfsigma } + with Invalid_argument _ | Failure _ -> non_existent_goal n + +let descend n p = + match p.ref with + | None -> error "It is a leaf." + | Some(r,pfl) -> + if List.length pfl >= n then + (match list_chop (n-1) pfl with + | left,(wanted::right) -> + (wanted, + (fun pfl' -> + if (List.length pfl' = 1) + & (List.hd pfl').goal = wanted.goal + then + let pf' = List.hd pfl' in + let spfl = left@(pf'::right) in + let newstatus = and_status (List.map pf_status spfl) in + { open_subgoals = newstatus; + goal = p.goal; + ref = Some(r,spfl) } + else + error "descend: validation")) + | _ -> assert false) + else + error "Too few subproofs" + +let traverse n pts = match n with + | 0 -> (* go to the parent *) + (match pts.tstack with + | [] -> error "traverse: no ancestors" + | (_,v)::tl -> + { tpf = v [pts.tpf]; + tstack = tl; + tpfsigma = pts.tpfsigma }) + | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *) + (match pts.tpf.ref with + | Some (Tactic (_,spf),_) -> + let v = (fun pfl -> pts.tpf) in + { tpf = spf; + tstack = (-1,v)::pts.tstack; + tpfsigma = pts.tpfsigma } + | _ -> error "traverse: not a tactic-node") + | n -> (* when n>0, go to the nth child *) + let (npf,v) = descend n pts.tpf in + { tpf = npf; + tpfsigma = pts.tpfsigma; + tstack = (n,v):: pts.tstack } + +let change_constraints_pftreestate newgc pts = { pts with tpfsigma = newgc } + +let app_tac sigr tac p = + let (gll,v) = tac {it=p.goal;sigma= !sigr} in + sigr := gll.sigma; + v (List.map leaf gll.it) + +(* solve the nth subgoal with tactic tac *) +let solve_nth_pftreestate n tac pts = + let sigr = ref pts.tpfsigma in + let tpf' = frontier_map (app_tac sigr tac) n pts.tpf in + let tpf'' = + if !sigr == pts.tpfsigma then tpf' + else frontier_mapi (fun _ g -> app_tac sigr norm_evar_tac g) tpf' in + { tpf = tpf''; + tpfsigma = !sigr; + tstack = pts.tstack } + +let solve_pftreestate = solve_nth_pftreestate 1 + +(* This function implements a poor man's undo at the current goal. + This is a gross approximation as it does not attempt to clean correctly + the global constraints given in tpfsigma. *) + +let weak_undo_pftreestate pts = + let pf = leaf pts.tpf.goal in + { tpf = pf; + tpfsigma = pts.tpfsigma; + tstack = pts.tstack } + +(* Gives a new proof (a leaf) of a goal gl *) +let mk_pftreestate g = + { tpf = leaf g; + tstack = []; + tpfsigma = Evd.empty } + +(* Extracts a constr from a proof-tree state ; raises an error if the + proof is not complete or the state does not correspond to the head + of the proof-tree *) + +let extract_open_pftreestate pts = + extract_open_proof pts.tpfsigma pts.tpf + +let extract_pftreestate pts = + if pts.tstack <> [] then + errorlabstrm "extract_pftreestate" + (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 + if subgoals <> [] then + errorlabstrm "extract_proof" + (str "Attempt to save an incomplete proof"); + let env = Global.env_of_context pts.tpf.goal.evar_hyps in + strong whd_betaiotaevar env pts.tpfsigma pfterm + (*** + local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm + ***) +(* Focus on the first leaf proof in a proof-tree state *) + +let rec first_unproven pts = + let pf = (proof_of_pftreestate pts) in + if is_complete_proof pf then + errorlabstrm "first_unproven" (str"No unproven subgoals"); + if is_leaf_proof pf then + pts + else + let childnum = + list_try_find_i + (fun n pf -> + if not(is_complete_proof pf) then n else failwith "caught") + 1 (children_of_proof pf) + in + first_unproven (traverse childnum pts) + +(* Focus on the last leaf proof in a proof-tree state *) + +let rec last_unproven pts = + let pf = proof_of_pftreestate pts in + if is_complete_proof pf then + errorlabstrm "last_unproven" (str"No unproven subgoals"); + if is_leaf_proof pf then + pts + else + let children = (children_of_proof pf) in + let nchilds = List.length children in + let childnum = + list_try_find_i + (fun n pf -> + if not(is_complete_proof pf) then n else failwith "caught") + 1 (List.rev children) + in + last_unproven (traverse (nchilds-childnum+1) pts) + +let rec nth_unproven n pts = + let pf = proof_of_pftreestate pts in + if is_complete_proof pf then + errorlabstrm "nth_unproven" (str"No unproven subgoals"); + if is_leaf_proof pf then + if n = 1 then + pts + else + errorlabstrm "nth_unproven" (str"Not enough unproven subgoals") + else + let children = children_of_proof pf in + let rec process i k = function + | [] -> + errorlabstrm "nth_unproven" (str"Not enough unproven subgoals") + | pf1::rest -> + let k1 = nb_unsolved_goals pf1 in + if k1 < k then + process (i+1) (k-k1) rest + else + nth_unproven k (traverse i pts) + in + process 1 n children + +let rec node_prev_unproven loc pts = + let pf = proof_of_pftreestate pts in + match cursor_of_pftreestate pts with + | [] -> last_unproven pts + | n::l -> + if is_complete_proof pf or loc = 1 then + node_prev_unproven n (traverse 0 pts) + else + let child = List.nth (children_of_proof pf) (loc - 2) in + if is_complete_proof child then + node_prev_unproven (loc - 1) pts + else + first_unproven (traverse (loc - 1) pts) + +let rec node_next_unproven loc pts = + let pf = proof_of_pftreestate pts in + match cursor_of_pftreestate pts with + | [] -> first_unproven pts + | n::l -> + if is_complete_proof pf || + loc = (List.length (children_of_proof pf)) then + node_next_unproven n (traverse 0 pts) + else if is_complete_proof (List.nth (children_of_proof pf) loc) then + node_next_unproven (loc + 1) pts + else + last_unproven(traverse (loc + 1) pts) + +let next_unproven pts = + let pf = proof_of_pftreestate pts in + if is_leaf_proof pf then + match cursor_of_pftreestate pts with + | [] -> error "next_unproven" + | n::_ -> node_next_unproven n (traverse 0 pts) + else + node_next_unproven (List.length (children_of_proof pf)) pts + +let prev_unproven pts = + let pf = proof_of_pftreestate pts in + if is_leaf_proof pf then + match cursor_of_pftreestate pts with + | [] -> error "prev_unproven" + | n::_ -> node_prev_unproven n (traverse 0 pts) + else + node_prev_unproven 1 pts + +let rec top_of_tree pts = + if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts) + + +(* Pretty-printers. *) + +open Pp + +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 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 + msgnl (hov 0 (str" == " ++ + print_subscript (sig_sig gls) sign pf)) + with e when catchable_exception e -> + msgnl (hov 0 (str "Info failed to apply validation")) + end; + res diff --git a/proofs/refiner.mli b/proofs/refiner.mli new file mode 100644 index 00000000..bed1158d --- /dev/null +++ b/proofs/refiner.mli @@ -0,0 +1,210 @@ + +(************************************************************************) +(* 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: refiner.mli,v 1.31.2.1 2004/07/16 19:30:49 herbelin Exp $ i*) + +(*i*) +open Term +open Sign +open Evd +open Proof_trees +open Proof_type +open Tacexpr +(*i*) + +(* The refiner (handles primitive rules and high-level tactics). *) + +val sig_it : 'a sigma -> 'a +val sig_sig : 'a sigma -> evar_map + +val project_with_focus : goal sigma -> named_context sigma + +val unpackage : 'a sigma -> evar_map ref * 'a +val repackage : evar_map ref -> 'a -> 'a sigma +val apply_sig_tac : + evar_map ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c + +type transformation_tactic = proof_tree -> (goal list * validation) + +val add_tactic : string -> (closed_generic_argument list -> tactic) -> unit +val overwriting_add_tactic : string -> (closed_generic_argument list -> tactic) -> unit +val lookup_tactic : string -> (closed_generic_argument list) -> tactic + +(*s Hiding the implementation of tactics. *) + +(* [abstract_tactic tac] hides the (partial) proof produced by [tac] under + a single proof node *) +val abstract_tactic : atomic_tactic_expr -> tactic -> tactic +val abstract_tactic_expr : tactic_expr -> tactic -> tactic +val abstract_extended_tactic : string -> closed_generic_argument list -> tactic -> tactic + +val refiner : rule -> tactic +val vernac_tactic : string * closed_generic_argument list -> tactic +val frontier : transformation_tactic +val list_pf : proof_tree -> goal list +val unTAC : tactic -> goal sigma -> proof_tree sigma + +val local_Constraints : tactic + +(* [frontier_map f n p] applies f on the n-th open subgoal of p and + rebuilds proof-tree. + n=1 for first goal, n negative counts from the right *) +val frontier_map : + (proof_tree -> proof_tree) -> int -> proof_tree -> proof_tree + +(* [frontier_mapi f p] applies (f i) on the i-th open subgoal of p. *) +val frontier_mapi : + (int -> proof_tree -> proof_tree) -> proof_tree -> proof_tree + +(*s Tacticals. *) + +(* [tclIDTAC] is the identity tactic without message printing*) +val tclIDTAC : tactic +val tclIDTAC_MESSAGE : string -> tactic + + +(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [tac2] to every resulting subgoals *) +val tclTHEN : tactic -> tactic -> tactic + +(* [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More + convenient than [tclTHEN] when [n] is large *) +val tclTHENLIST : tactic list -> tactic + +(* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [(tac2 i)] to the [i]$^{th}$ resulting subgoal (starting from 1) *) +val tclTHEN_i : tactic -> (int -> tactic) -> tactic + +(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the last resulting subgoal (previously called [tclTHENL]) *) +val tclTHENLAST : tactic -> tactic -> tactic + +(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the first resulting subgoal *) +val tclTHENFIRST : tactic -> tactic -> tactic + +(* [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to + [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises + an error if the number of resulting subgoals is not [n] *) +val tclTHENSV : tactic -> tactic array -> tactic + +(* Same with a list of tactics *) +val tclTHENS : tactic -> tactic list -> tactic + +(* [tclTHENST] is renamed [tclTHENSFIRSTn] +val tclTHENST : tactic -> tactic array -> tactic -> tactic +*) + +(* [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the + last [n] resulting subgoals and [tac2] on the remaining first subgoals *) +val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic + +(* [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then + applies [t1],...,[tn] on the first [n] resulting subgoals and + [tac2] for the remaining last subgoals (previously called tclTHENST) *) +val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic + +(* [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, + applies [t1],...,[tn] on the last [n] resulting subgoals and leaves + unchanged the other subgoals *) +val tclTHENLASTn : tactic -> tactic array -> tactic + +(* [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, + applies [t1],...,[tn] on the first [n] resulting subgoals and leaves + unchanged the other subgoals (previously called [tclTHENSI]) *) +val tclTHENFIRSTn : tactic -> tactic array -> tactic + +(* A special exception for levels for the Fail tactic *) +exception FailError of int * string + +val tclORELSE : tactic -> tactic -> tactic +val tclREPEAT : tactic -> tactic +val tclREPEAT_MAIN : tactic -> tactic +val tclFIRST : tactic list -> tactic +val tclSOLVE : tactic list -> tactic +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 tclDO : int -> tactic -> tactic +val tclPROGRESS : tactic -> tactic +val tclWEAK_PROGRESS : tactic -> tactic +val tclNOTSAMEGOAL : tactic -> tactic +val tclINFO : tactic -> tactic + +(* [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, + if it succeeds, applies [tac2] to the resulting subgoals, + and if not applies [tac3] to the initial goal [gls] *) +val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic +val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic +val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic + +(*s Tactics handling a list of goals. *) + +type validation_list = proof_tree list -> proof_tree list + +type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list + +val tclFIRSTLIST : tactic_list list -> tactic_list +val tclIDTAC_list : tactic_list +val first_goal : 'a list sigma -> 'a sigma +val apply_tac_list : tactic -> tactic_list +val then_tactic_list : tactic_list -> tactic_list -> tactic_list +val tactic_list_tactic : tactic_list -> tactic +val goal_goal_list : 'a sigma -> 'a list sigma + + +(*s Functions for handling the state of the proof editor. *) + +type pftreestate + +val proof_of_pftreestate : pftreestate -> proof_tree +val cursor_of_pftreestate : pftreestate -> int list +val is_top_pftreestate : pftreestate -> bool +val evc_of_pftreestate : pftreestate -> evar_map +val top_goal_of_pftreestate : pftreestate -> goal sigma +val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma + +val traverse : int -> pftreestate -> pftreestate +val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate +val solve_pftreestate : tactic -> pftreestate -> pftreestate + +(* a weak version of logical undoing, that is really correct only *) +(* if there are no existential variables. *) +val weak_undo_pftreestate : pftreestate -> pftreestate + +val mk_pftreestate : goal -> pftreestate +val extract_open_pftreestate : pftreestate -> constr * Termops.metamap +val extract_pftreestate : pftreestate -> constr +val first_unproven : pftreestate -> pftreestate +val last_unproven : pftreestate -> pftreestate +val nth_unproven : int -> pftreestate -> pftreestate +val node_prev_unproven : int -> pftreestate -> pftreestate +val node_next_unproven : int -> pftreestate -> pftreestate +val next_unproven : pftreestate -> pftreestate +val prev_unproven : pftreestate -> pftreestate +val top_of_tree : pftreestate -> pftreestate +val change_constraints_pftreestate + : evar_map -> pftreestate -> pftreestate + + +(*s Pretty-printers. *) + +(*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 diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml new file mode 100644 index 00000000..d8d7319d --- /dev/null +++ b/proofs/tacexpr.ml @@ -0,0 +1,314 @@ +(************************************************************************) +(* 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: tacexpr.ml,v 1.33.2.1 2004/07/16 19:30:49 herbelin Exp $ *) + +open Names +open Topconstr +open Libnames +open Nametab +open Rawterm +open Util +open Genarg +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 raw_red_flag = + | FBeta + | FIota + | FZeta + | FConst of reference list + | FDeltaBut of reference list + +let make_red_flag = + let rec add_flag red = function + | [] -> red + | FBeta :: lf -> add_flag { red with rBeta = true } lf + | FIota :: lf -> add_flag { red with rIota = true } lf + | FZeta :: lf -> add_flag { red with rZeta = true } lf + | FConst l :: lf -> + if red.rDelta then + error + "Cannot set both constants to unfold and constants not to unfold"; + add_flag { red with rConst = list_union red.rConst l } lf + | FDeltaBut l :: lf -> + if red.rConst <> [] & not red.rDelta then + error + "Cannot set both constants to unfold and constants not to unfold"; + add_flag + { red with rConst = list_union red.rConst l; rDelta = true } + lf + in + add_flag + {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} + +type hyp_location_flag = (* To distinguish body and type of local defs *) + | InHyp + | InHypTypeOnly + | InHypValueOnly + +type 'a raw_hyp_location = + 'a * int list * (hyp_location_flag * hyp_location_flag option ref) + +type 'a induction_arg = + | ElimOnConstr of 'a + | ElimOnIdent of identifier located + | ElimOnAnonHyp of int + +type inversion_kind = + | SimpleInversion + | FullInversion + | 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 + | InversionUsing of 'c * 'id list + +type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b + +type 'id gsimple_clause = ('id raw_hyp_location) option +(* onhyps: + [None] means *on every hypothesis* + [Some l] means on hypothesis belonging to l *) +type 'id gclause = + { onhyps : 'id raw_hyp_location list option; + onconcl : bool; + concl_occs :int list } + +let simple_clause_of = function + { onhyps = Some[scl]; onconcl = false } -> Some scl + | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None + | _ -> error "not a simple clause (one hypothesis or conclusion)" + +type pattern_expr = constr_expr + +(* Type of patterns *) +type 'a match_pattern = + | Term of 'a + | Subterm of identifier option * 'a + +(* Type of hypotheses for a Match Context rule *) +type 'a match_context_hyps = + | Hyp of name located * 'a match_pattern + +(* Type of a Match rule for Match Context and Match *) +type ('a,'t) match_rule = + | Pat of 'a match_context_hyps list * 'a match_pattern * 't + | All of 't + +type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = + (* Basic tactics *) + | TacIntroPattern of intro_pattern_expr list + | TacIntrosUntil of quantified_hypothesis + | TacIntroMove of identifier option * identifier located option + | TacAssumption + | TacExact of 'constr + | TacApply of 'constr with_bindings + | TacElim of 'constr with_bindings * 'constr with_bindings option + | TacElimType of 'constr + | TacCase of 'constr with_bindings + | TacCaseType of 'constr + | TacFix of identifier option * int + | TacMutualFix of identifier * int * (identifier * int * 'constr) list + | TacCofix of identifier option + | TacMutualCofix of identifier * (identifier * 'constr) list + | TacCut of 'constr + | TacTrueCut of name * 'constr + | TacForward of bool * name * 'constr + | TacGeneralize of 'constr list + | TacGeneralizeDep of 'constr + | TacLetTac of name * 'constr * 'id gclause + | TacInstantiate of int * 'constr * 'id gclause + + (* 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) + | 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) + + | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis + | TacDecomposeAnd of 'constr + | TacDecomposeOr of 'constr + | TacDecompose of 'ind list * 'constr + | TacSpecialize of int option * 'constr with_bindings + | TacLApply of 'constr + + (* Automation tactics *) + | TacTrivial of string list option + | TacAuto of int option * string list option + | TacAutoTDB of int option + | TacDestructHyp of (bool * identifier located) + | TacDestructConcl + | TacSuperAuto of (int option * reference list * bool * bool) + | TacDAuto of int option * int option + + (* Context management *) + | TacClear of 'id list + | TacClearBody of 'id list + | TacMove of bool * 'id * 'id + | TacRename of 'id * 'id + + (* Constructors *) + | TacLeft of 'constr bindings + | TacRight of 'constr bindings + | TacSplit of bool * 'constr bindings + | TacAnyConstructor of 'tac option + | TacConstructor of int or_metaid * 'constr bindings + + (* Conversion *) + | TacReduce of ('constr,'cst) red_expr_gen * 'id gclause + | TacChange of + 'constr occurrences option * 'constr * 'id gclause + + (* Equivalence relations *) + | TacReflexivity + | TacSymmetry of 'id gclause + | TacTransitivity of 'constr + + (* Equality and inversion *) + | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis + + (* For ML extensions *) + | TacExtend of loc * string * ('constr,'tac) generic_argument list + + (* For syntax extensions *) + | TacAlias of loc * string * + (identifier * ('constr,'tac) generic_argument) list + * (dir_path * 'tac) + +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 + | 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 + | TacDo of int or_var * ('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 + | 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 + | 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 + +and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast = + identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr + + (* These are possible arguments of a tactic definition *) +and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg = + | TacDynamic of loc * Dyn.t + | TacVoid + | MetaIdArg of loc * string + | ConstrMayEval of ('constr,'cst) may_eval + | IntroPattern of intro_pattern_expr + | Reference of 'ref + | Integer of int + | TacCall of loc * + 'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list + | TacFreshId of string option + | Tacexp of 'tac + +type raw_tactic_expr = + (constr_expr, + pattern_expr, + reference, + reference, + reference, + identifier located or_metaid, + raw_tactic_expr) gen_tactic_expr + +type raw_atomic_tactic_expr = + (constr_expr, (* constr *) + pattern_expr, (* pattern *) + reference, (* evaluable reference *) + reference, (* inductive *) + reference, (* ltac reference *) + identifier located or_metaid, (* identifier *) + raw_tactic_expr) gen_atomic_tactic_expr + +type raw_tactic_arg = + (constr_expr, + pattern_expr, + reference, + reference, + reference, + identifier located or_metaid, + raw_tactic_expr) gen_tactic_arg + +type raw_generic_argument = + (constr_expr,raw_tactic_expr) 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, + evaluable_global_reference and_short_name or_var, + inductive or_var, + ltac_constant located or_var, + identifier located, + glob_tactic_expr) gen_atomic_tactic_expr + +type glob_tactic_arg = + (rawconstr_and_expr, + constr_pattern, + evaluable_global_reference and_short_name or_var, + inductive or_var, + ltac_constant located, + identifier located or_var, + glob_tactic_expr) gen_tactic_arg + +type glob_generic_argument = + (rawconstr_and_expr,glob_tactic_expr) generic_argument + +type glob_red_expr = + (rawconstr_and_expr, evaluable_global_reference or_var) red_expr_gen + +type closed_raw_generic_argument = + (constr_expr,raw_tactic_expr) generic_argument + +type 'a raw_abstract_argument_type = + ('a,constr_expr,raw_tactic_expr) abstract_argument_type + +type 'a glob_abstract_argument_type = + ('a,rawconstr_and_expr,glob_tactic_expr) abstract_argument_type + +type open_generic_argument = + (Term.constr,glob_tactic_expr) generic_argument + +type closed_generic_argument = + (Term.constr,glob_tactic_expr) generic_argument + +type 'a closed_abstract_argument_type = + ('a,Term.constr,glob_tactic_expr) abstract_argument_type + +type declaration_hook = Decl_kinds.strength -> global_reference -> unit diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml new file mode 100644 index 00000000..0e3a49b0 --- /dev/null +++ b/proofs/tacmach.ml @@ -0,0 +1,260 @@ +(************************************************************************) +(* 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: tacmach.ml,v 1.61.2.1 2004/07/16 19:30:50 herbelin Exp $ *) + +open Util +open Names +open Nameops +open Sign +open Term +open Termops +open Instantiate +open Environ +open Reductionops +open Evd +open Typing +open Tacred +open Proof_trees +open Proof_type +open Logic +open Refiner +open Tacexpr + +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 validation = Proof_type.validation;; +type tactic = Proof_type.tactic;; + +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 pf_concl gls = (sig_it gls).evar_concl +let pf_hyps_types gls = + let sign = Environ.named_context (pf_env gls) in + List.map (fun (id,_,x) -> (id, x)) sign + +let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id + +let pf_last_hyp gl = List.hd (pf_hyps gl) + +let pf_get_hyp gls id = + try + Sign.lookup_named id (pf_hyps gls) + with Not_found -> + error ("No such hypothesis : " ^ (string_of_id id)) + +let pf_get_hyp_typ gls id = + let (_,_,ty)= (pf_get_hyp gls id) in + ty + +let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) + +let pf_get_new_id id gls = + next_ident_away id (pf_ids_of_hyps gls) + +let pf_get_new_ids ids gls = + let avoid = pf_ids_of_hyps gls in + List.fold_right + (fun id acc -> (next_ident_away id (acc@avoid))::acc) + ids [] + +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 + +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_apply f gls = f (pf_env gls) (project gls) +let pf_reduce = pf_apply + +let pf_whd_betadeltaiota = pf_reduce whd_betadeltaiota +let pf_whd_betadeltaiota_stack = pf_reduce whd_betadeltaiota_stack +let pf_hnf_constr = pf_reduce hnf_constr +let pf_red_product = pf_reduce red_product +let pf_nf = pf_reduce nf +let pf_nf_betaiota = pf_reduce (fun _ _ -> nf_betaiota) +let pf_compute = pf_reduce compute +let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) +let pf_type_of = pf_reduce type_of + +let pf_conv_x = pf_reduce is_conv +let pf_conv_x_leq = pf_reduce is_conv_leq +let pf_const_value = pf_reduce (fun env _ -> constant_value env) +let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind +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))) + +(************************************) +(* Tactics handling a list of goals *) +(************************************) + +type transformation_tactic = proof_tree -> (goal list * validation) + +type validation_list = proof_tree list -> proof_tree list + +type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list + +let first_goal = first_goal +let goal_goal_list = goal_goal_list +let apply_tac_list = apply_tac_list +let then_tactic_list = then_tactic_list +let tactic_list_tactic = tactic_list_tactic +let tclFIRSTLIST = tclFIRSTLIST +let tclIDTAC_list = tclIDTAC_list + + +(********************************************************) +(* Functions for handling the state of the proof editor *) +(********************************************************) + +type pftreestate = Refiner.pftreestate + +let proof_of_pftreestate = proof_of_pftreestate +let cursor_of_pftreestate = cursor_of_pftreestate +let is_top_pftreestate = is_top_pftreestate +let evc_of_pftreestate = evc_of_pftreestate +let top_goal_of_pftreestate = top_goal_of_pftreestate +let nth_goal_of_pftreestate = nth_goal_of_pftreestate +let traverse = traverse +let solve_nth_pftreestate = solve_nth_pftreestate +let solve_pftreestate = solve_pftreestate +let weak_undo_pftreestate = weak_undo_pftreestate +let mk_pftreestate = mk_pftreestate +let extract_pftreestate = extract_pftreestate +let extract_open_pftreestate = extract_open_pftreestate +let first_unproven = first_unproven +let last_unproven = last_unproven +let nth_unproven = nth_unproven +let node_prev_unproven = node_prev_unproven +let node_next_unproven = node_next_unproven +let next_unproven = next_unproven +let prev_unproven = prev_unproven +let top_of_tree = top_of_tree +let frontier = frontier +let change_constraints_pftreestate = change_constraints_pftreestate + + +(********************************************) +(* Definition of the most primitive tactics *) +(********************************************) + +let refiner = refiner + +(* This does not check that the variable name is not here *) +let introduction_no_check id = + refiner (Prim (Intro id)) + +(* This does not check that the dependencies are correct *) +let intro_replacing_no_check whereid gl = + refiner (Prim (Intro_replacing whereid)) gl + +let internal_cut_no_check id t gl = + refiner (Prim (Cut (true,id,t))) gl + +let internal_cut_rev_no_check id t gl = + refiner (Prim (Cut (false,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_hyp_no_check d gl = + refiner (Prim (Convert_hyp d)) gl + +(* This does not check dependencies *) +let thin_no_check ids gl = + if ids = [] then tclIDTAC gl else refiner (Prim (Thin ids)) gl + +(* This does not check dependencies *) +let thin_body_no_check ids gl = + if ids = [] then tclIDTAC gl else refiner (Prim (ThinBody ids)) gl + +let move_hyp_no_check with_dep id1 id2 gl = + refiner (Prim (Move (with_dep,id1,id2))) gl + +let rename_hyp_no_check id1 id2 gl = + refiner (Prim (Rename (id1,id2))) gl + +let mutual_fix f n others gl = + with_check (refiner (Prim (FixRule (f,n,others)))) gl + +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 + + +(* Versions with consistency checks *) + +let introduction id = with_check (introduction_no_check id) +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_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) +let move_hyp b id id' = with_check (move_hyp_no_check b id id') +let rename_hyp id id' = with_check (rename_hyp_no_check id id') + +(* Pretty-printers *) + +open Pp +open Printer +open Tacexpr +open Rawterm + +let rec pr_list f = function + | [] -> mt () + | 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)) + +let pr_glls glls = + hov 0 (pr_decls (sig_sig glls) ++ fnl () ++ + prlist_with_sep pr_fnl pr_seq (sig_it glls)) + diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli new file mode 100644 index 00000000..59b48da2 --- /dev/null +++ b/proofs/tacmach.mli @@ -0,0 +1,183 @@ +(************************************************************************) +(* 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: tacmach.mli,v 1.50.2.1 2004/07/16 19:30:50 herbelin Exp $ i*) + +(*i*) +open Names +open Term +open Sign +open Environ +open Evd +open Reduction +open Proof_trees +open Proof_type +open Refiner +open Tacred +open Tacexpr +open Rawterm +(*i*) + +(* Operations for handling terms under a local typing context. *) + +type 'a sigma = 'a Proof_type.sigma;; +type validation = Proof_type.validation;; +type tactic = Proof_type.tactic;; + +val sig_it : 'a sigma -> 'a +val project : goal sigma -> evar_map + +val re_sig : 'a -> evar_map -> 'a sigma + +val unpackage : 'a sigma -> evar_map ref * 'a +val repackage : evar_map ref -> 'a -> 'a sigma +val apply_sig_tac : + evar_map ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c + +val pf_concl : goal sigma -> types +val pf_env : goal sigma -> env +val pf_hyps : goal sigma -> named_context +(*i val pf_untyped_hyps : goal sigma -> (identifier * constr) list i*) +val pf_hyps_types : goal sigma -> (identifier * types) list +val pf_nth_hyp_id : goal sigma -> int -> identifier +val pf_last_hyp : goal sigma -> named_declaration +val pf_ids_of_hyps : goal sigma -> identifier list +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 +val pf_interp_type : goal sigma -> Topconstr.constr_expr -> types + +val pf_get_hyp : goal sigma -> identifier -> named_declaration +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_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a +val pf_reduce : + (env -> evar_map -> constr -> constr) -> + goal sigma -> constr -> constr + +val pf_whd_betadeltaiota : goal sigma -> constr -> constr +val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list +val pf_hnf_constr : goal sigma -> constr -> constr +val pf_red_product : goal sigma -> constr -> constr +val pf_nf : goal sigma -> constr -> constr +val pf_nf_betaiota : goal sigma -> constr -> constr +val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types +val pf_reduce_to_atomic_ind : goal sigma -> types -> inductive * types +val pf_compute : goal sigma -> constr -> constr +val pf_unfoldn : (int list * evaluable_global_reference) list + -> goal sigma -> constr -> constr + +val pf_const_value : goal sigma -> constant -> constr +val pf_conv_x : goal sigma -> constr -> constr -> bool +val pf_conv_x_leq : goal sigma -> constr -> constr -> bool + +type transformation_tactic = proof_tree -> (goal list * validation) + +val frontier : transformation_tactic + + +(*s Functions for handling the state of the proof editor. *) + +type pftreestate = Refiner.pftreestate + +val proof_of_pftreestate : pftreestate -> proof_tree +val cursor_of_pftreestate : pftreestate -> int list +val is_top_pftreestate : pftreestate -> bool +val evc_of_pftreestate : pftreestate -> evar_map +val top_goal_of_pftreestate : pftreestate -> goal sigma +val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma +val traverse : int -> pftreestate -> pftreestate +val weak_undo_pftreestate : pftreestate -> pftreestate +val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate +val solve_pftreestate : tactic -> pftreestate -> pftreestate +val mk_pftreestate : goal -> pftreestate +val extract_open_pftreestate : pftreestate -> constr * Termops.metamap +val extract_pftreestate : pftreestate -> constr +val first_unproven : pftreestate -> pftreestate +val last_unproven : pftreestate -> pftreestate +val nth_unproven : int -> pftreestate -> pftreestate +val node_prev_unproven : int -> pftreestate -> pftreestate +val node_next_unproven : int -> pftreestate -> pftreestate +val next_unproven : pftreestate -> pftreestate +val prev_unproven : pftreestate -> pftreestate +val top_of_tree : pftreestate -> pftreestate +val change_constraints_pftreestate : + evar_map -> pftreestate -> pftreestate + +(* +val vernac_tactic : string * tactic_arg list -> tactic +*) +(*s The most primitive tactics. *) + +val refiner : rule -> tactic +val introduction_no_check : identifier -> tactic +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_hyp_no_check : named_declaration -> tactic +val thin_no_check : identifier list -> tactic +val thin_body_no_check : identifier list -> tactic +val move_hyp_no_check : bool -> identifier -> identifier -> tactic +val rename_hyp_no_check : identifier -> identifier -> tactic +val mutual_fix : + identifier -> int -> (identifier * int * constr) list -> tactic +val mutual_cofix : identifier -> (identifier * constr) list -> tactic +val rename_bound_var_goal : tactic + +(*s The most primitive tactics with consistency and type checking *) + +val introduction : identifier -> tactic +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_hyp : named_declaration -> tactic +val thin : identifier list -> tactic +val thin_body : identifier list -> tactic +val move_hyp : bool -> identifier -> identifier -> tactic +val rename_hyp : identifier -> identifier -> tactic + +(*s Tactics handling a list of goals. *) + +type validation_list = proof_tree list -> proof_tree list + +type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list + +val first_goal : 'a list sigma -> 'a sigma +val goal_goal_list : 'a sigma -> 'a list sigma +val apply_tac_list : tactic -> tactic_list +val then_tactic_list : tactic_list -> tactic_list -> tactic_list +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 diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml new file mode 100644 index 00000000..1fa1101d --- /dev/null +++ b/proofs/tactic_debug.ml @@ -0,0 +1,179 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +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 + +(* 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 + complete panel of commands dedicated to a proof assistant framework *) + +(* Debug information *) +type debug_info = + | DebugOn of int + | DebugOff + +(* An exception handler *) +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)) + +(* Prints the commands *) +let help () = + msgnl (str "Commands: <Enter>=Continue" ++ fnl() ++ + str " h/?=Help" ++ fnl() ++ + str " r<num>=Run <num> times" ++ fnl() ++ + str " s=Skip" ++ fnl() ++ + str " x=Exit") + +(* Prints the goal and the command to be executed *) +let goal_com g tac = + begin + db_pr_goal g; + msg (str "Going to execute:" ++ fnl () ++ pr_glob_tactic tac ++ fnl ()) + end + +(* Gives the number of a run command *) +let run_com inst = + if (String.get inst 0)='r' then + let num = int_of_string (String.sub inst 1 ((String.length inst)-1)) in + if num>0 then num + else raise (Invalid_argument "run_com") + else + raise (Invalid_argument "run_com") + +let allskip = ref 0 +let skip = ref 0 + +(* Prints the run counter *) +let run ini = + if not ini then + for i=1 to 2 do + print_char (Char.chr 8);print_char (Char.chr 13) + done; + msg (str "Executed expressions: " ++ int (!allskip - !skip) ++ + fnl() ++ fnl()) + +(* Prints the prompt *) +let rec prompt level = + begin + msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > "); + flush stdout; + let inst = read_line () in + match inst with + | "" -> true + | "s" -> false + | "x" -> print_char (Char.chr 8);skip:=0;allskip:=0;raise Sys.Break + | "h"| "?" -> + begin + help (); + prompt level + end + | _ -> + (try let ctr=run_com inst in skip:=ctr;allskip:=ctr;run true;true + with Failure _ | Invalid_argument _ -> prompt level) + end + +(* Prints the state and waits for an instruction *) +let debug_prompt lev g tac f = + (* What to print and to do next *) + let continue = + if !skip = 0 then (goal_com g tac; prompt lev) + else (decr skip; run false; if !skip=0 then allskip:=0; true) in + (* What to execute *) + try f (if continue then DebugOn (lev+1) else DebugOff) + with e -> + skip:=0; allskip:=0; + if Logic.catchable_exception e then + ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e); + raise e + +(* Prints a constr *) +let db_constr debug env c = + if debug <> DebugOff & !skip = 0 then + msgnl (str "Evaluated term: " ++ prterm_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) + end + +(* Prints the hypothesis pattern identifier if it exists *) +let hyp_bound = function + | Anonymous -> " (unbound)" + | Name id -> " (bound to "^(Names.string_of_id id)^")" + +(* Prints a matched hypothesis *) +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) + +(* 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) + +(* Prints a success message when the goal has been matched *) +let db_mc_pattern_success debug = + if debug <> DebugOff & !skip = 0 then + msgnl (str "The goal has been successfully matched!" ++ fnl() ++ + 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) + | Subterm (o,c) -> + Subterm (o,(extern_pattern env (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) + +(* Prints a matching failure message for a rule *) +let db_matching_failure debug = + if debug <> DebugOff & !skip = 0 then + msgnl (str "This rule has failed due to matching errors!" ++ fnl() ++ + str "Let us try the next one...") + +(* 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 + msgnl + (str "This rule has failed due to \"Fail\" tactic (" ++ + str 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 = + if debug <> DebugOff & !skip = 0 then + begin + msgnl (!explain_logic_error err); + msgnl (str "This rule has failed due to a logic error!" ++ fnl() ++ + str "Let us try the next one...") + end diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli new file mode 100644 index 00000000..9ab263c4 --- /dev/null +++ b/proofs/tactic_debug.mli @@ -0,0 +1,62 @@ +(************************************************************************) +(* 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: tactic_debug.mli,v 1.12.2.1 2004/07/16 19:30:50 herbelin Exp $ i*) + +open Environ +open Pattern +open Proof_type +open Names +open Tacexpr +open Term + +(* 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 + complete panel of commands dedicated to a proof assistant framework *) + +(* Debug information *) +type debug_info = + | DebugOn of int + | DebugOff + +(* Prints the state and waits *) +val debug_prompt : + int -> goal sigma -> glob_tactic_expr -> (debug_info -> 'a) -> 'a + +(* Prints a constr *) +val db_constr : debug_info -> env -> constr -> unit + +(* Prints the pattern rule *) +val db_pattern_rule : + debug_info -> int -> (constr_pattern,glob_tactic_expr) match_rule -> unit + +(* Prints a matched hypothesis *) +val db_matched_hyp : + debug_info -> env -> identifier * constr -> name -> unit + +(* Prints the matched conclusion *) +val db_matched_concl : debug_info -> env -> constr -> unit + +(* Prints a success message when the goal has been matched *) +val db_mc_pattern_success : debug_info -> unit + +(* Prints a failure message for an hypothesis pattern *) +val db_hyp_pattern_failure : + debug_info -> env -> name * constr_pattern match_pattern -> unit + +(* Prints a matching failure message for a rule *) +val db_matching_failure : debug_info -> unit + +(* Prints an evaluation failure message for a rule *) +val db_eval_failure : debug_info -> string -> unit + +(* An exception handler *) +val explain_logic_error: (exn -> Pp.std_ppcmds) ref + +(* Prints a logic failure message for a rule *) +val db_logic_failure : debug_info -> exn -> unit diff --git a/proofs/tmp-src b/proofs/tmp-src new file mode 100644 index 00000000..1da11fe0 --- /dev/null +++ b/proofs/tmp-src @@ -0,0 +1,56 @@ + +(********* INSTANTIATE ****************************************************) + +(* existential_type gives the type of an existential *) +let existential_type env k = + let (sp,args) = destConst k in + let evd = Evd.map (evar_map env) sp in + instantiate_constr + (ids_of_sign evd.evar_hyps) evd.evar_concl.body (Array.to_list args) + +(* existential_value gives the value of a defined existential *) +let existential_value env k = + let (sp,args) = destConst k in + if defined_const env k then + let evd = Evd.map (evar_map env) sp in + match evd.evar_body with + | EVAR_DEFINED c -> + instantiate_constr (ids_of_sign evd.evar_hyps) c (Array.to_list args) + | _ -> anomalylabstrm "termenv__existential_value" + [< 'sTR"The existential variable code just registered a" ; + 'sPC ; 'sTR"grave internal error." >] + else + failwith "undefined existential" + + +(******* REDUCTION ********************************************************) + + +(************ REDUCTION.MLI **********************************************) + +(*********** TYPEOPS *****************************************************) + + +(* Constants or existentials. *) + +let type_of_constant_or_existential env c = + if is_existential c then + type_of_existential env c + else + type_of_constant env c + + +(******** TYPING **********************************************************) + + | IsMeta n -> + let metaty = + try lookup_meta n env + with Not_found -> error "A variable remains non instanciated" + in + (match kind_of_term metaty with + | IsCast (typ,kind) -> + ({ uj_val = cstr; uj_type = typ; uj_kind = kind }, cst0) + | _ -> + let (jty,cst) = execute mf env metaty in + let k = whd_betadeltaiotaeta env jty.uj_type in + ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, cst)) |