diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 35 | ||||
| -rw-r--r-- | proofs/clenv.mli | 11 | ||||
| -rw-r--r-- | proofs/logic.ml | 3 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 17 |
5 files changed, 30 insertions, 38 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index dd5ebb6ef..721552fad 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -943,41 +943,34 @@ let clenv_fo_resolver clenv gls = let clenv_typed_fo_resolver clenv gls = clenv_typed_unify (clenv_instance_template_type clenv) (pf_concl gls) clenv -let args_typ gls = - let rec decrec l c = match pf_whd_betadeltaiota gls c with - | DOP2(Prod,a,DLAM(n,b)) -> - decrec ((Environ.named_hd Environ.empty_env a n,a)::l) b - | x -> l - in - decrec [] - -(* if lname_type typ is [xn,An;..;x1,A1] and l is a list of terms, +(* 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 c l lname_typ = +let abstract_scheme env c l lname_typ = List.fold_left2 (fun t (locc,a) (na,ta) -> if occur_meta ta then error "cannot find a type for the generalisation" - else if occur_meta a then DOP2(Lambda,ta,DLAM(na,t)) - else DOP2(Lambda,ta,DLAM(na,subst_term_occ locc a t))) - c + 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 gls typ c l = - let p = - abstract_scheme c (List.map (function a -> [],a) l) (args_typ gls typ) in + +let abstract_list_all env sigma typ c l = + let lname_typ,_ = splay_prod env sigma typ in + let p = abstract_scheme env c (List.map (function a -> [],a) l) lname_typ in try - if pf_conv_x gls (pf_type_of gls p) typ then p else - error "abstract_list_all" + if is_conv env sigma (Typing.type_of env sigma p) typ then p + else error "abstract_list_all" with UserError _ -> - raise (RefinerError (CannotGeneralize (pf_hyps gls,typ))) + raise (RefinerError (CannotGeneralize typ)) let secondOrderAbstraction allow_K gl p oplist clause = let (clause',cllist) = constrain_clenv_using_subterm_list allow_K clause oplist (pf_concl gl) in let typp = clenv_instance_type clause' p in - clenv_unify (DOP0(Meta p)) (abstract_list_all gl typp (pf_concl gl) cllist) + clenv_unify (DOP0(Meta p)) + (abstract_list_all (pf_env gl) (project gl) typp (pf_concl gl) cllist) clause' let clenv_so_resolver allow_K clause gl = diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 6354a34e3..353fe5198 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -78,10 +78,6 @@ val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic val clenv_type_of : wc clausenv -> constr -> constr val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv -(* [abstract_list_all sig c t l] *) -(* abstracts the terms in l over c to get a term of type t *) -val abstract_list_all : goal sigma -> constr -> constr -> constr list -> constr - (* Exported for program.ml only *) val clenv_add_sign : (identifier * typed_type) -> wc clausenv -> wc clausenv @@ -95,3 +91,10 @@ val clenv_typed_unify : constr -> constr -> wc clausenv -> wc clausenv val pr_clenv : 'a clausenv -> Pp.std_ppcmds +(*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 -> 'a Evd.evar_map -> constr -> constr -> constr list -> constr + diff --git a/proofs/logic.ml b/proofs/logic.ml index 2d4e8a903..6a12e8d35 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -10,6 +10,7 @@ open Term open Sign open Environ open Reduction +open Inductive open Typing open Proof_trees open Proof_type @@ -23,7 +24,7 @@ type refiner_error = | OccurMeta of constr | CannotApply of constr * constr | CannotUnify of constr * constr - | CannotGeneralize of typed_type signature * constr + | CannotGeneralize of constr | NotWellTyped of constr | BadTacticArgs of string * tactic_arg list diff --git a/proofs/logic.mli b/proofs/logic.mli index 31f0b5199..5476bbfe1 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -28,7 +28,7 @@ type refiner_error = | OccurMeta of constr | CannotApply of constr * constr | CannotUnify of constr * constr - | CannotGeneralize of typed_type signature * constr + | CannotGeneralize of constr | NotWellTyped of constr | BadTacticArgs of string * tactic_arg list diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index c0254a7ca..350b3c1db 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -55,17 +55,6 @@ let pf_get_hyp gls id = let pf_ctxt gls = get_ctxt (sig_it gls) -let pf_type_of gls c = - type_of (sig_it gls).evar_env (ts_it (sig_sig gls)) c - -let hnf_type_of gls = - compose - (whd_betadeltaiota (sig_it gls).evar_env (project gls)) - (pf_type_of gls) - -let pf_check_type gls c1 c2 = - let casted = mkCast c1 c2 in pf_type_of gls casted - let pf_interp_constr gls c = let evc = project gls in Astterm.interp_constr evc (sig_it gls).evar_env c @@ -95,6 +84,7 @@ let pf_nf = pf_reduce nf let pf_nf_betaiota = pf_reduce 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 @@ -103,6 +93,11 @@ let pf_one_step_reduce = pf_reduce one_step_reduce let pf_reduce_to_mind = pf_reduce reduce_to_mind let pf_reduce_to_ind = pf_reduce reduce_to_ind +let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls) + +let pf_check_type gls c1 c2 = + let casted = mkCast c1 c2 in pf_type_of gls casted + (************************************) (* Tactics handling a list of goals *) (************************************) |