diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 67 | ||||
| -rw-r--r-- | proofs/clenv.mli | 10 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 11 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 7 | ||||
| -rw-r--r-- | proofs/logic.ml | 44 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 3 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 2 | ||||
| -rw-r--r-- | proofs/refiner.ml | 11 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 4 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 37 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 37 |
13 files changed, 97 insertions, 140 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0fd86d9a3c..630f45007e 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -20,6 +20,28 @@ open Proof_type open Logic open Reduction open Tacmach +open Evar_refiner + + +(* Generator of metavariables *) +let meta_ctr=ref 0;; + +let new_meta ()=incr meta_ctr;!meta_ctr;; + +(* replaces a mapping of existentials into a mapping of metas. *) +let exist_to_meta (emap, c) = + let subst = ref [] in + let mmap = ref [] in + let add_binding (e,ty) = + let n = new_meta() in + subst := (e, mkMeta n) :: !subst; + mmap := (n, ty) :: !mmap in + List.iter add_binding emap; + let rec replace c = + match kind_of_term c with + IsEvar k -> List.assoc k !subst + | _ -> map_constr replace c in + (!mmap, replace c) type 'a freelisted = { rebus : 'a; @@ -38,15 +60,6 @@ type 'a clausenv = { type wc = walking_constraints -let new_evar_in_sign env = - let ev = new_evar () in - mkEvar (ev, Array.of_list (Evarutil.make_evar_instance env)) - -let rec whd_evar sigma t = match kind_of_term t with - | IsEvar (ev,_ as evc) when is_defined sigma ev -> - whd_evar sigma (existential_value sigma evc) - | _ -> collapse_appl t - let applyHead n c wc = let rec apprec n c cty wc = if n = 0 then @@ -55,7 +68,7 @@ let applyHead n c wc = match kind_of_term (w_whd_betadeltaiota wc cty) with | IsProd (_,c1,c2) -> let c1ty = w_type_of wc c1 in - let evar = new_evar_in_sign (w_env wc) in + 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)) @@ -83,8 +96,8 @@ let unify_0 mc wc m n = let env = w_env wc and sigma = w_Underlying wc in let rec unirec_rec ((metasubst,evarsubst) as substn) m n = - let cM = whd_evar sigma m - and cN = whd_evar sigma n in + let cM = whd_ise1 sigma m + and cN = whd_ise1 sigma n in try match (kind_of_term cM,kind_of_term cN) with | IsCast (c,_), _ -> unirec_rec substn c cN @@ -165,21 +178,6 @@ let unify_0 mc wc m n = else unirec_rec (mc,[]) m n - -let whd_castappevar_stack sigma c = - let rec whrec (c, l as s) = - match kind_of_term c with - | IsEvar (ev,args) when is_defined sigma ev -> - whrec (existential_value sigma (ev,args), l) - | IsCast (c,_) -> whrec (c, l) - | IsApp (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l) - | _ -> s - in - whrec (c, []) - -let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c) - -let w_whd wc c = whd_castappevar (w_Underlying wc) c (* Unification * @@ -700,11 +698,14 @@ let clenv_refine_cast kONT clenv gls = 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 +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 let constrain_clenv_to_subterm clause (op,cl) = let rec matchrec cl = @@ -934,7 +935,7 @@ let clenv_pose_dependent_evars clenv = clenv_template_type clenv) in List.fold_left (fun clenv mv -> - let evar = new_evar_in_sign (w_env clenv.hook) in + 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 tYty = w_type_of clenv.hook tY in diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 59d61a5670..106369d330 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -14,8 +14,18 @@ open Names open Term open Tacmach open Proof_type +open Evar_refiner (*i*) +(* [new_meta] is a generator of unique meta variables *) +val new_meta : unit -> int + +(* [exist_to_meta] generates new metavariables for each existential + and performs the replacement in the given constr *) +val exist_to_meta : + ((existential * constr) list * constr) -> + ((int * constr) list * constr) + (* The Type of Constructions clausale environments. *) type 'a freelisted = { diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index ca6e2108cc..957605dfdd 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -17,6 +17,8 @@ open Environ open Evd open Reduction open Typing +open Instantiate +open Tacred open Proof_trees open Proof_type open Logic @@ -117,11 +119,19 @@ let w_Focusing sp wt = let w_Focus sp wc = ids_mod (extract_decl sp) wc let w_Underlying wc = (ts_it (ids_it wc)).decls +let w_whd wc c = whd_castappevar (w_Underlying wc) c let w_type_of wc c = ctxt_type_of (ids_it wc) c let w_env wc = get_env (ids_it wc) let w_hyps wc = named_context (get_env (ids_it wc)) let w_ORELSE wt1 wt2 wc = try wt1 wc with e when catchable_exception e -> wt2 wc +let w_defined_const wc (sp,_) = defined_constant (w_env wc) sp +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,s) (wc : walking_constraints) = let c = mkCast (ty,s) in @@ -165,6 +175,7 @@ let w_Define sp c wc = (ids_mod (fun evc -> (Proof_trees.remap evc (sp,spdecl'))) wc) | _ -> error "define_evar" + (******************************************) (* Instantiation of existential variables *) (******************************************) diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index bddbc2b352..b5af7f131f 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -59,6 +59,7 @@ val w_Define : evar -> constr -> w_tactic val w_Underlying : walking_constraints -> enamed_declarations val w_env : walking_constraints -> env val w_hyps : walking_constraints -> named_context +val w_whd : walking_constraints -> constr -> constr val w_type_of : walking_constraints -> constr -> constr val w_add_sign : (identifier * types) -> walking_constraints -> walking_constraints @@ -66,6 +67,12 @@ val w_add_sign : (identifier * types) -> walking_constraints val w_IDTAC : w_tactic val w_ORELSE : w_tactic -> w_tactic -> w_tactic val ctxt_type_of : readable_constraints -> constr -> constr +val w_whd_betadeltaiota : walking_constraints -> constr -> constr +val w_hnf_constr : walking_constraints -> constr -> constr +val w_conv_x : walking_constraints -> constr -> constr -> bool +val w_const_value : walking_constraints -> constant -> constr +val w_defined_const : walking_constraints -> constant -> bool +val w_defined_evar : walking_constraints -> existential_key -> bool val evars_of : readable_constraints -> constr -> local_constraints diff --git a/proofs/logic.ml b/proofs/logic.ml index b3800da28e..b06f16682c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -27,13 +27,27 @@ open Declare open Retyping open Evarutil +(* 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 splay_constr c with + | OpMeta mv, _ -> mv::acc + | OpCast, [|c;_|] -> collrec acc c + | (OpApp | OpMutCase _), cl -> Array.fold_left collrec acc cl + | _ -> acc + in + List.rev(collrec [] c) + 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 @@ -78,9 +92,9 @@ let rec mk_refgoals sigma goal goalacc conclty trm = else *) match kind_of_term trm with - | IsMeta mv -> + | IsMeta _ -> if occur_meta conclty then - error "Cannot refine to conclusions with meta-variables"; + raise (RefinerError (OccurMetaGoal conclty)); let ctxt = out_some goal.evar_info in (mk_goal ctxt hyps (nf_betaiota env sigma conclty))::goalacc, conclty @@ -162,29 +176,6 @@ and mk_casegoals sigma goal goalacc p c = (acc'',lbrty,conclty) -(* Will only be used on terms given to the Refine rule which have meta -varaibles only in Application and Case *) - -let collect_meta_variables c = - let rec collrec acc c = match splay_constr c with - | OpMeta mv, _ -> mv::acc - | OpCast, [|c;_|] -> collrec acc c - | (OpApp | OpMutCase _), cl -> Array.fold_left collrec acc cl - | _ -> acc - in - List.rev(collrec [] c) - -let new_meta_variables = - let rec newrec x = match kind_of_term x with - | IsMeta _ -> mkMeta (new_meta()) - | IsCast (c,t) -> mkCast (newrec c, t) - | IsApp (f,cl) -> appvect (newrec f, Array.map newrec cl) - | IsMutCase (ci,p,c,lf) -> - mkMutCase (ci, newrec p, newrec c, Array.map newrec lf) - | _ -> x - in - newrec - let error_use_instantiate () = errorlabstrm "Logic.prim_refiner" [< 'sTR"cannot intro when there are open metavars in the domain type"; @@ -439,7 +430,8 @@ let prim_refiner r sigma goal = mk_sign sign (cl::lar,lf) | { name = Refine; terms = [c] } -> - let c = new_meta_variables c in + 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 diff --git a/proofs/logic.mli b/proofs/logic.mli index 5381cffc46..a1c525a349 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -47,8 +47,10 @@ 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 diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7778702495..b1cf3764e5 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -219,7 +219,8 @@ let solve_nth k tac = let by tac = mutate (solve_pftreestate tac) -let instantiate_nth_evar_com n c = mutate (instantiate_pf_com n c) +let instantiate_nth_evar_com n c = + mutate (instantiate_pf_com n c) let traverse n = mutate (traverse n) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 6a22de3e64..cf92c41e6d 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -92,7 +92,7 @@ and validation = (proof_tree list -> proof_tree) and tactic_arg = | Command of Coqast.t | Constr of constr - | OpenConstr of ((int * constr) list * constr) (* constr with holes *) + | OpenConstr of Pretyping.open_constr | Constr_context of constr | Identifier of identifier | Qualid of Nametab.qualid diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 1c9605b2e7..a09504b366 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -124,7 +124,7 @@ and validation = (proof_tree list -> proof_tree) and tactic_arg = | Command of Coqast.t | Constr of constr - | OpenConstr of ((int * constr) list * constr) (* constr with holes *) + | OpenConstr of Pretyping.open_constr | Constr_context of constr | Identifier of identifier | Qualid of Nametab.qualid diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 0752b2ca95..8e358adea2 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -226,6 +226,7 @@ let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it Their proof should be completed in order to complete the initial proof *) let extract_open_proof sigma pf = + let meta_cnt = ref 0 in let open_obligations = ref [] in let rec proof_extractor vl = function | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf @@ -253,11 +254,11 @@ let extract_open_proof sigma pf = (fun (_,id) concl -> let (c,ty) = lookup_id id goal.evar_hyps in mkNamedProd_or_LetIn (id,c,ty) concl) - sorted_rels goal.evar_concl - in - let mv = new_meta() in - open_obligations := (mv,abs_concl):: !open_obligations; - applist (mkMeta mv, List.map (fun (n,_) -> mkRel n) sorted_rels) + sorted_rels goal.evar_concl in + incr meta_cnt; + open_obligations := (!meta_cnt,abs_concl):: !open_obligations; + applist + (mkMeta !meta_cnt, List.map (fun (n,_) -> mkRel n) sorted_rels) | _ -> anomaly "Bug : a case has been forgotten in proof_extractor" in diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 6b7d118ae3..c422b00699 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -691,7 +691,7 @@ and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl);exat] (* let lic = mkLetIn (Name id,csr,typ,ccl) in - let ntac = refine (mkCast (mkMeta (Environ.new_meta ()),lic)) in + let ntac = refine (mkCast (mkMeta (Logic.new_meta ()),lic)) in tclTHEN ntac (tclTHEN (introduction id) (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl))*) @@ -718,7 +718,7 @@ and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl);exat] (* let lic = mkLetIn (Name id,pft,typ,ccl) in - let ntac = refine (mkCast (mkMeta (Environ.new_meta ()),lic)) in + let ntac = refine (mkCast (mkMeta (Logic.new_meta ()),lic)) in tclTHEN ntac (tclTHEN (introduction id) (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl))*) with | NotTactic -> diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 81aa16c6fb..b3ad1225e5 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -23,7 +23,6 @@ open Proof_trees open Proof_type open Logic open Refiner -open Evar_refiner let re_sig it gc = { it = it; sigma = gc } @@ -164,40 +163,8 @@ let prev_unproven = prev_unproven let top_of_tree = top_of_tree let frontier = frontier let change_constraints_pftreestate = change_constraints_pftreestate -let instantiate_pf = instantiate_pf -let instantiate_pf_com = instantiate_pf_com - -(***********************************) -(* Walking constraints re-exported *) -(***********************************) - -type walking_constraints = Evar_refiner.walking_constraints -type 'a result_w_tactic = walking_constraints -> walking_constraints * 'a -type w_tactic = walking_constraints -> walking_constraints - -let startWalk = startWalk -let walking_THEN = walking_THEN -let walking = walking -let w_Focusing_THEN = w_Focusing_THEN -let w_Declare = w_Declare -let w_Declare_At = w_Declare_At -let w_Define = w_Define -let w_Underlying = w_Underlying -let w_env = w_env -let w_hyps = w_hyps -let w_type_of = w_type_of -let w_IDTAC = w_IDTAC -let w_ORELSE = w_ORELSE -let w_add_sign = w_add_sign -let ctxt_type_of = ctxt_type_of - -let w_defined_const wc (sp,_) = defined_constant (w_env wc) sp -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 instantiate_pf = Evar_refiner.instantiate_pf +let instantiate_pf_com = Evar_refiner.instantiate_pf_com (*************************************************) (* Tacticals re-exported from the Refiner module.*) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 6deb243917..5481491d53 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -17,7 +17,6 @@ open Reduction open Proof_trees open Proof_type open Refiner -open Evar_refiner open Tacred (*i*) @@ -186,40 +185,6 @@ val tclFIRSTLIST : tactic_list list -> tactic_list val tclIDTAC_list : tactic_list -(*s Walking constraints re-exported. *) - -type walking_constraints = Evar_refiner.walking_constraints - -type 'a result_w_tactic = walking_constraints -> walking_constraints * 'a -type w_tactic = walking_constraints -> walking_constraints - -val startWalk : - goal sigma -> walking_constraints * (walking_constraints -> tactic) - -val walking_THEN : 'a result_w_tactic -> ('a -> tactic) -> tactic -val walking : w_tactic -> tactic -val w_Focusing_THEN : int -> 'a result_w_tactic - -> ('a -> w_tactic) -> w_tactic -val w_Declare : int -> constr * constr -> w_tactic -val w_Declare_At : int -> int -> constr * constr -> w_tactic -val w_Define : int -> constr -> w_tactic -val w_Underlying : walking_constraints -> enamed_declarations -val w_env : walking_constraints -> env -val w_hyps : walking_constraints -> named_context -val w_type_of : walking_constraints -> constr -> constr -val w_add_sign : (identifier * types) - -> walking_constraints -> walking_constraints -val w_IDTAC : w_tactic -val w_ORELSE : w_tactic -> w_tactic -> w_tactic -val ctxt_type_of : readable_constraints -> constr -> constr -val w_whd_betadeltaiota : walking_constraints -> constr -> constr -val w_hnf_constr : walking_constraints -> constr -> constr -val w_conv_x : walking_constraints -> constr -> constr -> bool -val w_const_value : walking_constraints -> constant -> constr -val w_defined_const : walking_constraints -> constant -> bool -val w_defined_evar : walking_constraints -> existential_key -> bool - - (*s Tactic Registration. *) val add_tactic : string -> (tactic_arg list -> tactic) -> unit @@ -259,7 +224,7 @@ type 'a hide_combinator = string -> ('a -> tactic) -> ('a -> tactic) val hide_atomic_tactic : string -> tactic -> tactic val hide_constr_tactic : constr hide_combinator -val hide_openconstr_tactic : ((int * constr) list * constr) hide_combinator +val hide_openconstr_tactic : Pretyping.open_constr hide_combinator val hide_constrl_tactic : (constr list) hide_combinator val hide_numarg_tactic : int hide_combinator val hide_ident_tactic : identifier hide_combinator |