From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- pretyping/cases.ml | 145 ++++++------------------ pretyping/cases.mli | 10 +- pretyping/cbv.ml | 138 ++++++++++++----------- pretyping/cbv.mli | 14 +-- pretyping/clenv.ml | 10 +- pretyping/coercion.ml | 18 ++- pretyping/coercion.mli | 10 +- pretyping/detyping.ml | 90 ++++++++------- pretyping/detyping.mli | 13 ++- pretyping/evarconv.ml | 6 +- pretyping/evarutil.ml | 27 ++--- pretyping/evd.ml | 26 ++--- pretyping/evd.mli | 9 +- pretyping/indrec.ml | 20 ++-- pretyping/inductiveops.ml | 59 +++++++--- pretyping/inductiveops.mli | 25 +++-- pretyping/matching.ml | 36 ++++-- pretyping/pattern.ml | 112 ++++++++++++------- pretyping/pattern.mli | 9 +- pretyping/pretype_errors.ml | 6 +- pretyping/pretyping.ml | 102 ++++++++--------- pretyping/rawterm.ml | 48 +++++--- pretyping/rawterm.mli | 39 ++++--- pretyping/recordops.ml | 4 +- pretyping/reductionops.ml | 263 ++++++++++++++++++++++---------------------- pretyping/reductionops.mli | 37 +++++-- pretyping/retyping.ml | 26 ++--- pretyping/retyping.mli | 4 +- pretyping/tacred.ml | 6 +- pretyping/tacred.mli | 4 +- pretyping/termops.ml | 6 +- pretyping/termops.mli | 4 +- pretyping/typing.ml | 31 ++---- pretyping/unification.ml | 4 +- 34 files changed, 721 insertions(+), 640 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index a32aaf45..b0fe83a3 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 8693 2006-04-10 12:05:05Z msozeau $ *) +(* $Id: cases.ml 8875 2006-05-29 19:59:11Z msozeau $ *) open Util open Names @@ -66,13 +66,10 @@ let error_needs_inversion env x t = module type S = sig val compile_cases : loc -> - (type_constraint -> env -> rawconstr -> unsafe_judgment) * + (type_constraint -> env -> rawconstr -> unsafe_judgment) * Evd.evar_defs ref -> type_constraint -> - env -> - rawconstr option * - (rawconstr * (name * (loc * inductive * name list) option)) list * - (loc * identifier list * cases_pattern list * rawconstr) list -> + env -> rawconstr option * tomatch_tuple * cases_clauses -> unsafe_judgment end @@ -138,14 +135,9 @@ type 'a lifted = int * 'a let insert_lifted a = (0,a);; -(* The pattern variables for [it] are in [user_ids] and the variables - to avoid are in [other_ids]. -*) - type rhs = { rhs_env : env; - other_ids : identifier list; - user_ids : identifier list; + avoid_ids : identifier list; rhs_lift : int; it : rawconstr } @@ -321,16 +313,21 @@ let rec find_row_ind = function | PatCstr(loc,c,_,_) :: _ -> Some (loc,c) let inductive_template isevars env tmloc ind = - let (mib,mip) = Inductive.lookup_mind_specif env ind in - let (ntys,_) = splay_prod env (Evd.evars_of !isevars) mip.mind_nf_arity in + let arsign = get_full_arity_sign env ind in let hole_source = match tmloc with | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (ind,i)) | None -> fun _ -> (dummy_loc, Evd.InternalHole) in - let (evarl,_) = + let (_,evarl,_) = List.fold_right - (fun (na,ty) (evl,n) -> - (e_new_evar isevars env ~src:(hole_source n) (substl evl ty))::evl,n+1) - ntys ([],1) in + (fun (na,b,ty) (subst,evarl,n) -> + match b with + | None -> + let ty' = substl subst ty in + let e = e_new_evar isevars env ~src:(hole_source n) ty' in + (e::subst,e::evarl,n+1) + | Some b -> + (b::subst,evarl,n+1)) + arsign ([],[],1) in applist (mkInd ind,List.rev evarl) let inh_coerce_to_ind isevars env ty tyi = @@ -349,7 +346,7 @@ let unify_tomatch_with_patterns isevars env typ tm = let find_tomatch_tycon isevars env loc = function (* Try first if some 'in I ...' is present and can be used as a constraint *) - | Some (_,ind,_),_ + | Some (_,ind,_,_),_ (* Otherwise try to get constraints from (the 1st) constructor in clauses *) | None, Some (_,(ind,_)) -> mk_tycon (inductive_template isevars env loc ind) @@ -434,7 +431,7 @@ let mkDeclTomatch na = function let map_tomatch_type f = function | IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind) - | NotInd (c,t) -> NotInd (option_app f c, f t) + | NotInd (c,t) -> NotInd (option_map f c, f t) let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth) let lift_tomatch_type n = liftn_tomatch_type n 1 @@ -701,7 +698,7 @@ let get_names env sign eqns = (* Otherwise, we take names from the parameters of the constructor but avoiding conflicts with user ids *) let allvars = - List.fold_left (fun l (_,eqn) -> list_union l eqn.rhs.other_ids) [] eqns in + List.fold_left (fun l (_,eqn) -> list_union l eqn.rhs.avoid_ids) [] eqns in let names4,_ = List.fold_left2 (fun (l,avoid) d na -> @@ -793,7 +790,7 @@ let prepare_unif_pb typ cs = let typ' = if noccur_between_without_evar 1 n typ then lift (-n) typ else (* TODO4-1 *) - error "Inference of annotation not yet implemented in this case" in + error "Unable to infer return clause of this pattern-matching problem" in let args = extended_rel_list (-n) cs.cs_args in let ci = applist (mkConstruct cs.cs_cstr, cs.cs_params@args) in @@ -1172,7 +1169,7 @@ let rec generalize_problem pb current = function let tomatch = regeneralize_index_tomatch (i+1) tomatch in { pb with tomatch = Abstract d :: tomatch; - pred = option_app (generalize_predicate current i d) pb'.pred } + pred = option_map (generalize_predicate current i d) pb'.pred } (* No more patterns: typing the right-hand-side of equations *) let build_leaf pb = @@ -1187,7 +1184,7 @@ let build_leaf pb = let shift_problem (current,t) pb = {pb with tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch; - pred = option_app (specialize_predicate_var (current,t)) pb.pred; + pred = option_map (specialize_predicate_var (current,t)) pb.pred; history = push_history_pattern 0 AliasLeaf pb.history; mat = List.map remove_current_pattern pb.mat } @@ -1257,7 +1254,7 @@ let build_branch current deps pb eqns const_info = { pb with env = push_rels sign pb.env; tomatch = List.rev_append currents tomatch; - pred = option_app (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred; + pred = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred; history = history; mat = List.map (push_rels_eqn_with_names sign) submat } @@ -1329,7 +1326,7 @@ and compile_generalization pb d rest = { pb with env = push_rel d pb.env; tomatch = rest; - pred = option_app ungeneralize_predicate pb.pred; + pred = option_map ungeneralize_predicate pb.pred; mat = List.map (push_rels_eqn [d]) pb.mat } in let patstat,j = compile pb in patstat, @@ -1355,7 +1352,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest = {pb with env = newenv; tomatch = tomatch; - pred = option_app (lift_predicate n) pb.pred; + pred = option_map (lift_predicate n) pb.pred; history = history; mat = mat } in let patstat,j = compile pb in @@ -1368,78 +1365,16 @@ substituer apr (**************************************************************************) (* Preparation of the pattern-matching problem *) -(* Qu'est-ce qui faut pas faire pour traiter les alias ... *) - -(* On ne veut pas ajouter de primitive à Environ et le problème, c'est - donc de faire un renommage en se contraignant à parcourir l'env - dans le sens croissant. Ici, subst renomme des variables repérées - par leur numéro et seen_ids collecte celles dont on sait que les - variables de subst annule le scope *) -let rename_env subst env = - let n = ref (rel_context_length (rel_context env)) in - let seen_ids = ref [] in - process_rel_context - (fun (na,c,t as d) env -> - let d = - try - let id = List.assoc !n subst in - seen_ids := id :: !seen_ids; - (Name id,c,t) - with Not_found -> - match na with - | Name id when List.mem id !seen_ids -> (Anonymous,c,t) - | _ -> d in - decr n; - push_rel d env) env - -let is_dependent_indtype = function - | NotInd _ -> false - | IsInd (_, IndType(_,realargs)) -> realargs <> [] - -let prepare_initial_alias_eqn isdep tomatchl eqn = - let (subst, pats) = - List.fold_right2 - (fun pat (tm,tmtyp) (subst, stripped_pats) -> - match alias_of_pat pat with - | Anonymous -> (subst, pat::stripped_pats) - | Name idpat -> - match kind_of_term tm with - | Rel n when not (is_dependent_indtype tmtyp) & not isdep - -> (n, idpat)::subst, (unalias_pat pat::stripped_pats) - | _ -> (subst, pat::stripped_pats)) - eqn.patterns tomatchl ([], []) in - let env = rename_env subst eqn.rhs.rhs_env in - { eqn with patterns = pats; rhs = { eqn.rhs with rhs_env = env } } - -let prepare_initial_aliases isdep tomatchl mat = mat -(* List.map (prepare_initial_alias_eqn isdep tomatchl) mat*) - -(* -let prepare_initial_alias lpat tomatchl rhs = - List.fold_right2 - (fun pat tm (stripped_pats, rhs) -> - match alias_of_pat pat with - | Anonymous -> (pat::stripped_pats, rhs) - | Name _ as na -> - match tm with - | RVar _ -> - (unalias_pat pat::stripped_pats, - RLetIn (dummy_loc, na, tm, rhs)) - | _ -> (pat::stripped_pats, rhs)) - lpat tomatchl ([], rhs) -*) (* builds the matrix of equations testing that each eqn has n patterns * and linearizing the _ patterns. * Syntactic correctness has already been done in astterm *) let matx_of_eqns env tomatchl eqns = let build_eqn (loc,ids,lpat,rhs) = -(* let initial_lpat,initial_rhs = prepare_initial_alias lpat tomatchl rhs in*) let initial_lpat,initial_rhs = lpat,rhs in let initial_rhs = rhs in let rhs = { rhs_env = env; - other_ids = ids@(ids_of_named_context (named_context env)); - user_ids = ids; + avoid_ids = ids@(ids_of_named_context (named_context env)); rhs_lift = 0; it = initial_rhs } in { dependencies = []; @@ -1547,7 +1482,7 @@ let set_arity_signature dep n arsign tomatchl pred x = in decomp_block [] pred (tomatchl,arsign) -let prepare_predicate_from_tycon loc dep env isevars tomatchs c = +let prepare_predicate_from_tycon loc dep env isevars tomatchs sign c = let cook (n, l, env, signs) = function | c,IsInd (_,IndType(indf,realargs)) -> let indf' = lift_inductive_family n indf in @@ -1605,8 +1540,8 @@ let extract_arity_signature env0 tomatchl tmsign = match tm with | NotInd (bo,typ) -> (match t with - | None -> [na,option_app (lift n) bo,lift n typ] - | Some (loc,_,_) -> + | None -> [na,option_map (lift n) bo,lift n typ] + | Some (loc,_,_,_) -> user_err_loc (loc,"", str "Unexpected type annotation for a term of non inductive type")) | IsInd (_,IndType(indf,realargs)) -> @@ -1615,18 +1550,12 @@ let extract_arity_signature env0 tomatchl tmsign = let nrealargs = List.length realargs in let realnal = match t with - | Some (loc,ind',nal) -> - let nparams = List.length params in + | Some (loc,ind',nparams,realnal) -> if ind <> ind' then user_err_loc (loc,"",str "Wrong inductive type"); - let nindargs = nparams + nrealargs in - (* Normally done at interning time *) - if List.length nal <> nindargs then - error_wrong_numarg_inductive_loc loc env0 ind' nindargs; - let parnal,realnal = list_chop nparams nal in - if List.exists ((<>) Anonymous) parnal then - user_err_loc (loc,"", - str "The parameters of inductive type must be implicit"); + if List.length params <> nparams + or nrealargs <> List.length realnal then + anomaly "Ill-formed 'in' clause in cases"; List.rev realnal | None -> list_tabulate (fun _ -> Anonymous) nrealargs in let arsign = fst (get_arity env0 indf') in @@ -1665,7 +1594,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function (match tycon with | Some (None, t) -> let names,pred = - prepare_predicate_from_tycon loc false env isevars tomatchs t + prepare_predicate_from_tycon loc false env isevars tomatchs sign t in Some (build_initial_predicate false names pred) | _ -> None) @@ -1677,8 +1606,9 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function let allnames = List.rev (List.map (List.map pi1) arsign) in let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in let _ = - option_app (fun tycon -> - isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val tycon) + option_map (fun tycon -> + isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val + (lift_tycon_type (List.length arsign) tycon)) tycon in let predccl = (j_nf_isevar !isevars predcclj).uj_val in @@ -1701,9 +1631,6 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e let tmsign = List.map snd tomatchl in let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in - (* We deal with initial aliases *) - let matx = prepare_initial_aliases (known_dependent pred) tomatchs matx in - (* We push the initial terms to match and push their alias to rhs' envs *) (* names of aliases will be recovered from patterns (hence Anonymous here) *) let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 5919c42a..9e902126 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cases.mli 8654 2006-03-22 15:36:58Z msozeau $ i*) +(*i $Id: cases.mli 8741 2006-04-26 22:30:32Z herbelin $ i*) (*i*) open Util @@ -41,13 +41,9 @@ val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a module type S = sig val compile_cases : loc -> - (type_constraint -> env -> rawconstr -> unsafe_judgment) * - evar_defs ref -> + (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref -> type_constraint -> - env -> - rawconstr option * - (rawconstr * (name * (loc * inductive * name list) option)) list * - (loc * identifier list * cases_pattern list * rawconstr) list -> + env -> rawconstr option * tomatch_tuple * cases_clauses -> unsafe_judgment end diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 33166ba8..2a01e901 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cbv.ml 7639 2005-12-02 10:01:15Z gregoire $ *) +(* $Id: cbv.ml 8802 2006-05-10 20:47:28Z barras $ *) open Util open Pp @@ -45,10 +45,10 @@ open Esubst *) type cbv_value = | VAL of int * constr - | LAM of name * constr * constr * cbv_value subs - | FIXP of fixpoint * cbv_value subs * cbv_value list - | COFIXP of cofixpoint * cbv_value subs * cbv_value list - | CONSTR of constructor * cbv_value list + | LAM of int * (name * constr) list * constr * cbv_value subs + | FIXP of fixpoint * cbv_value subs * cbv_value array + | COFIXP of cofixpoint * cbv_value subs * cbv_value array + | CONSTR of constructor * cbv_value array (* les vars pourraient etre des constr, cela permet de retarder les lift: utile ?? *) @@ -58,14 +58,15 @@ type cbv_value = *) let rec shift_value n = function | VAL (k,v) -> VAL ((k+n),v) - | LAM (x,a,b,s) -> LAM (x,a,b,subs_shft (n,s)) + | LAM (nlams,ctxt,b,s) -> LAM (nlams,ctxt,b,subs_shft (n,s)) | FIXP (fix,s,args) -> - FIXP (fix,subs_shft (n,s), List.map (shift_value n) args) + FIXP (fix,subs_shft (n,s), Array.map (shift_value n) args) | COFIXP (cofix,s,args) -> - COFIXP (cofix,subs_shft (n,s), List.map (shift_value n) args) + COFIXP (cofix,subs_shft (n,s), Array.map (shift_value n) args) | CONSTR (c,args) -> - CONSTR (c, List.map (shift_value n) args) - + CONSTR (c, Array.map (shift_value n) args) +let shift_value n v = + if n = 0 then v else shift_value n v (* Contracts a fixpoint: given a fixpoint and a bindings, * returns the corresponding fixpoint body, and the bindings in which @@ -74,22 +75,14 @@ let rec shift_value n = function * -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti) *) let contract_fixp env ((reci,i),(_,_,bds as bodies)) = - let make_body j = FIXP(((reci,j),bodies), env, []) in + let make_body j = FIXP(((reci,j),bodies), env, [||]) in let n = Array.length bds in - let rec subst_bodies_from_i i subs = - if i=n then subs - else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs)) - in - subst_bodies_from_i 0 env, bds.(i) + subs_cons(Array.init n make_body, env), bds.(i) let contract_cofixp env (i,(_,_,bds as bodies)) = - let make_body j = COFIXP((j,bodies), env, []) in + let make_body j = COFIXP((j,bodies), env, [||]) in let n = Array.length bds in - let rec subst_bodies_from_i i subs = - if i=n then subs - else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs)) - in - subst_bodies_from_i 0 env, bds.(i) + subs_cons(Array.init n make_body, env), bds.(i) let make_constr_ref n = function | RelKey p -> mkRel (n+p) @@ -99,9 +92,11 @@ let make_constr_ref n = function (* type of terms with a hole. This hole can appear only under App or Case. * TOP means the term is considered without context - * APP(l,stk) means the term is applied to l, and then we have the context st + * APP(v,stk) means the term is applied to v, and then the context stk + * (v.0 is the first argument). * this corresponds to the application stack of the KAM. - * The members of l are values: we evaluate arguments before the function. + * The members of l are values: we evaluate arguments before + calling the function. * CASE(t,br,pat,S,stk) means the term is in a case (which is himself in stk * t is the type of the case and br are the branches, all of them under * the subs S, pat is information on the patterns of the Case @@ -114,15 +109,15 @@ let make_constr_ref n = function type cbv_stack = | TOP - | APP of cbv_value list * cbv_stack + | APP of cbv_value array * cbv_stack | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack (* Adds an application list. Collapse APPs! *) let stack_app appl stack = - match (appl, stack) with - | ([], _) -> stack - | (_, APP(args,stk)) -> APP(appl@args,stk) - | _ -> APP(appl, stack) + if Array.length appl = 0 then stack else + match stack with + | APP(args,stk) -> APP(Array.append appl args,stk) + | _ -> APP(appl, stack) open RedFlags @@ -137,23 +132,21 @@ let red_set_ref flags = function *) let strip_appl head stack = match head with - | FIXP (fix,env,app) -> (FIXP(fix,env,[]), stack_app app stack) - | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[]), stack_app app stack) - | CONSTR (c,app) -> (CONSTR(c,[]), stack_app app stack) + | FIXP (fix,env,app) -> (FIXP(fix,env,[||]), stack_app app stack) + | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[||]), stack_app app stack) + | CONSTR (c,app) -> (CONSTR(c,[||]), stack_app app stack) | _ -> (head, stack) -(* Tests if fixpoint reduction is possible. A reduction function is given as - argument *) -let rec check_app_constr = function - | ([], _) -> false - | ((CONSTR _)::_, 0) -> true - | (_::l, n) -> check_app_constr (l,(pred n)) - +(* Tests if fixpoint reduction is possible. *) let fixp_reducible flgs ((reci,i),_) stk = if red_set flgs fIOTA then - match stk with (* !!! for Acc_rec: reci.(i) = -2 *) - | APP(appl,_) -> reci.(i) >=0 & check_app_constr (appl, reci.(i)) + match stk with + | APP(appl,_) -> + Array.length appl > reci.(i) && + (match appl.(reci.(i)) with + CONSTR _ -> true + | _ -> false) | _ -> false else false @@ -166,6 +159,7 @@ let cofixp_reducible flgs _ stk = else false + (* The main recursive functions * * Go under applications and cases (pushed in the stack), expand head @@ -184,7 +178,7 @@ let rec norm_head info env t stack = | App (head,args) -> (* Applied terms are normalized immediately; they could be computed when getting out of the stack *) let nargs = Array.map (cbv_stack_term info TOP env) args in - norm_head info env head (stack_app (Array.to_list nargs) stack) + norm_head info env head (stack_app nargs stack) | Case (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack)) | Cast (ct,_,_) -> norm_head info env ct stack @@ -212,7 +206,7 @@ let rec norm_head info env t stack = or red_set (info_flags info) fDELTA *) then - subs_cons (cbv_stack_term info TOP env b,env) + subs_cons ([|cbv_stack_term info TOP env b|],env) else subs_lift env in if zeta then @@ -225,10 +219,12 @@ let rec norm_head info env t stack = (VAL(0,normt), stack) (* Considérer une coupure commutative ? *) (* non-neutral cases *) - | Lambda (x,a,b) -> (LAM(x,a,b,env), stack) - | Fix fix -> (FIXP(fix,env,[]), stack) - | CoFix cofix -> (COFIXP(cofix,env,[]), stack) - | Construct c -> (CONSTR(c, []), stack) + | Lambda _ -> + let ctxt,b = decompose_lam t in + (LAM(List.length ctxt, List.rev ctxt,b,env), stack) + | Fix fix -> (FIXP(fix,env,[||]), stack) + | CoFix cofix -> (COFIXP(cofix,env,[||]), stack) + | Construct c -> (CONSTR(c, [||]), stack) (* neutral cases *) | (Sort _ | Meta _ | Ind _|Evar _) -> (VAL(0, t), stack) @@ -253,10 +249,18 @@ and norm_head_ref k info env stack normt = and cbv_stack_term info stack env t = match norm_head info env t stack with (* a lambda meets an application -> BETA *) - | (LAM (x,a,b,env), APP (arg::args, stk)) + | (LAM (nlams,ctxt,b,env), APP (args, stk)) when red_set (info_flags info) fBETA -> - let subs = subs_cons (arg,env) in - cbv_stack_term info (stack_app args stk) subs b + let nargs = Array.length args in + if nargs == nlams then + cbv_stack_term info stk (subs_cons(args,env)) b + else if nlams < nargs then + let env' = subs_cons(Array.sub args 0 nlams, env) in + let eargs = Array.sub args nlams (nargs-nlams) in + cbv_stack_term info (APP(eargs,stk)) env' b + else + let ctxt' = list_skipn nargs ctxt in + LAM(nlams-nargs,ctxt', b, subs_cons(args,env)) (* a Fix applied enough -> IOTA *) | (FIXP(fix,env,_), stk) @@ -273,8 +277,9 @@ and cbv_stack_term info stack env t = (* constructor in a Case -> IOTA *) | (CONSTR((sp,n),_), APP(args,CASE(_,br,ci,env,stk))) when red_set (info_flags info) fIOTA -> - let real_args = list_skipn ci.ci_npar args in - cbv_stack_term info (stack_app real_args stk) env br.(n-1) + let cargs = + Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in + cbv_stack_term info (stack_app cargs stk) env br.(n-1) (* constructor of arity 0 in a Case -> IOTA *) | (CONSTR((_,n),_), CASE(_,br,_,env,stk)) @@ -287,6 +292,9 @@ and cbv_stack_term info stack env t = | (COFIXP(cofix,env,_), APP(appl,TOP)) -> COFIXP(cofix,env,appl) | (CONSTR(c,_), APP(appl,TOP)) -> CONSTR(c,appl) + (* absurd cases (ill-typed) *) + | (LAM _, CASE _) -> assert false + (* definitely a value *) | (head,stk) -> VAL(0,apply_stack info (cbv_norm_value info head) stk) @@ -298,7 +306,7 @@ and cbv_stack_term info stack env t = and apply_stack info t = function | TOP -> t | APP (args,st) -> - apply_stack info (applistc t (List.map (cbv_norm_value info) args)) st + apply_stack info (mkApp(t,Array.map (cbv_norm_value info) args)) st | CASE (ty,br,ci,env,st) -> apply_stack info (mkCase (ci, cbv_norm_term info env ty, t, @@ -314,28 +322,28 @@ and cbv_norm_term info env t = (* reduction of a cbv_value to a constr *) and cbv_norm_value info = function (* reduction under binders *) | VAL (n,v) -> lift n v - | LAM (x,a,b,env) -> - mkLambda (x, cbv_norm_term info env a, - cbv_norm_term info (subs_lift env) b) + | LAM (n,ctxt,b,env) -> + let nctxt = + list_map_i (fun i (x,ty) -> + (x,cbv_norm_term info (subs_liftn i env) ty)) 0 ctxt in + compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b) | FIXP ((lij,(names,lty,bds)),env,args) -> - applistc + mkApp (mkFix (lij, (names, Array.map (cbv_norm_term info env) lty, Array.map (cbv_norm_term info - (subs_liftn (Array.length lty) env)) bds))) - (List.map (cbv_norm_value info) args) + (subs_liftn (Array.length lty) env)) bds)), + Array.map (cbv_norm_value info) args) | COFIXP ((j,(names,lty,bds)),env,args) -> - applistc + mkApp (mkCoFix (j, (names,Array.map (cbv_norm_term info env) lty, Array.map (cbv_norm_term info - (subs_liftn (Array.length lty) env)) bds))) - (List.map (cbv_norm_value info) args) + (subs_liftn (Array.length lty) env)) bds)), + Array.map (cbv_norm_value info) args) | CONSTR (c,args) -> - applistc - (mkConstruct c) - (List.map (cbv_norm_value info) args) + mkApp(mkConstruct c, Array.map (cbv_norm_value info) args) (* with profiling *) let cbv_norm infos constr = diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index dfdf12dd..8c969e2c 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cbv.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: cbv.mli 8799 2006-05-09 21:15:07Z barras $ i*) (*i*) open Names @@ -29,19 +29,19 @@ val cbv_norm : cbv_infos -> constr -> constr (*i This is for cbv debug *) type cbv_value = | VAL of int * constr - | LAM of name * constr * constr * cbv_value subs - | FIXP of fixpoint * cbv_value subs * cbv_value list - | COFIXP of cofixpoint * cbv_value subs * cbv_value list - | CONSTR of constructor * cbv_value list + | LAM of int * (name * constr) list * constr * cbv_value subs + | FIXP of fixpoint * cbv_value subs * cbv_value array + | COFIXP of cofixpoint * cbv_value subs * cbv_value array + | CONSTR of constructor * cbv_value array val shift_value : int -> cbv_value -> cbv_value type cbv_stack = | TOP - | APP of cbv_value list * cbv_stack + | APP of cbv_value array * cbv_stack | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack -val stack_app : cbv_value list -> cbv_stack -> cbv_stack +val stack_app : cbv_value array -> cbv_stack -> cbv_stack val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack (* recursive functions... *) diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 0b88b14b..6113ec2d 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: clenv.ml 8688 2006-04-07 15:08:12Z msozeau $ *) +(* $Id: clenv.ml 8752 2006-04-27 19:37:33Z herbelin $ *) open Pp open Util @@ -84,10 +84,10 @@ let clenv_environments evd bound c = let dep = dependent (mkRel 1) c2 in let na' = if dep then na else Anonymous in let e' = meta_declare mv c1 ~name:na' e in - clrec (e', (mkMeta mv)::metas) (option_app ((+) (-1)) n) + clrec (e', (mkMeta mv)::metas) (option_map ((+) (-1)) n) (if dep then (subst1 (mkMeta mv) c2) else c2) | (n, LetIn (na,b,_,c)) -> - clrec (e,metas) (option_app ((+) (-1)) n) (subst1 b c) + clrec (e,metas) (option_map ((+) (-1)) n) (subst1 b c) | (n, _) -> (e, List.rev metas, c) in clrec (evd,[]) bound c @@ -100,10 +100,10 @@ let clenv_environments_evars env evd bound c = | (n, Prod (na,c1,c2)) -> let e',constr = Evarutil.new_evar e env c1 in let dep = dependent (mkRel 1) c2 in - clrec (e', constr::ts) (option_app ((+) (-1)) n) + clrec (e', constr::ts) (option_map ((+) (-1)) n) (if dep then (subst1 constr c2) else c2) | (n, LetIn (na,b,_,c)) -> - clrec (e,ts) (option_app ((+) (-1)) n) (subst1 b c) + clrec (e,ts) (option_map ((+) (-1)) n) (subst1 b c) | (n, _) -> (e, List.rev ts, c) in clrec (evd,[]) bound c diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index e01dac47..d0ee913f 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coercion.ml 8695 2006-04-10 16:33:52Z msozeau $ *) +(* $Id: coercion.ml 8875 2006-05-29 19:59:11Z msozeau $ *) open Util open Names @@ -35,6 +35,12 @@ module type S = sig type a sort; it fails if no coercion is applicable *) val inh_coerce_to_sort : loc -> env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment + + (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it + inserts a coercion into [j], if needed, in such a way it gets as + type its base type (the notion depends on the coercion system) *) + val inh_coerce_to_base : loc -> + env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and @@ -143,6 +149,8 @@ module Default = struct | _ -> inh_tosort_force loc env isevars j + let inh_coerce_to_base loc env isevars j = (isevars, j) + let inh_coerce_to_fail env isevars c1 v t = let v', t' = try @@ -168,7 +176,7 @@ module Default = struct (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t), kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with | Prod (_,t1,t2), Prod (name,u1,u2) -> - let v' = option_app (whd_betadeltaiota env (evars_of isevars)) v in + let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in let (evd',b) = match v' with Some v' -> @@ -184,7 +192,7 @@ module Default = struct let env1 = push_rel (x,None,v1) env in let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd' (Some v2) t2 u2 in - (evd'', option_app (fun v2' -> mkLambda (x, v1, v2')) v2', + (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', mkProd (x, v1, t2')) | None -> (* Mismatch on t1 and u1 or not a lambda: we eta-expand *) @@ -201,7 +209,7 @@ module Default = struct let (evd'', v2', t2') = let v2 = match v with - Some v -> option_app (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1' + Some v -> option_map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1' | None -> None and evd', t2 = match v1' with @@ -212,7 +220,7 @@ module Default = struct in inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2 in - (evd'', option_app (fun v2' -> mkLambda (name, u1, v2')) v2', + (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2', mkProd (name, u1, t2'))) | _ -> raise NoCoercion)) diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index f675beff..42ce27fd 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coercion.mli 8688 2006-04-07 15:08:12Z msozeau $ i*) +(*i $Id: coercion.mli 8875 2006-05-29 19:59:11Z msozeau $ i*) (*i*) open Util @@ -33,13 +33,19 @@ module type S = sig type a sort; it fails if no coercion is applicable *) val inh_coerce_to_sort : loc -> env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment + + (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it + inserts a coercion into [j], if needed, in such a way it gets as + type its base type (the notion depends on the coercion system) *) + val inh_coerce_to_base : loc -> + env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and [j.uj_type] are convertible; it fails if no coercion is applicable *) val inh_conv_coerce_to : loc -> env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment - + (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; it fails if no coercion exists *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 3f2aed34..7a170bcf 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: detyping.ml 8624 2006-03-13 17:38:17Z msozeau $ *) +(* $Id: detyping.ml 8875 2006-05-29 19:59:11Z msozeau $ *) open Pp open Util @@ -277,6 +277,25 @@ let extract_nondep_branches test c b n = | _ -> assert false in if test c n then Some (strip n b) else None +let it_destRLambda_or_LetIn_names n c = + let rec aux n nal c = + if n=0 then (List.rev nal,c) else match c with + | RLambda (_,na,_,c) -> aux (n-1) (na::nal) c + | RLetIn (_,na,_,c) -> aux (n-1) (na::nal) c + | _ -> + (* eta-expansion *) + let rec next l = + let x = Nameops.next_ident_away (id_of_string "x") l in + (* Not efficient but unusual and no function to get free rawvars *) + if occur_rawconstr x c then next (x::l) else x in + let x = next [] in + let a = RVar (dl,x) in + aux (n-1) (Name x :: nal) + (match c with + | RApp (loc,p,l) -> RApp (loc,c,l@[a]) + | _ -> (RApp (dl,c,[a]))) + in aux n [] c + let detype_case computable detype detype_eqns testdep avoid data p c bl = let (indsp,st,nparams,consnargsl,k) = data in let synth_type = synthetize_type () in @@ -286,32 +305,16 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = then Anonymous, None, None else - match option_app detype p with + match option_map detype p with | None -> Anonymous, None, None | Some p -> - let decompose_lam k c = - let rec lamdec_rec l avoid k c = - if k = 0 then List.rev l,c else match c with - | RLambda (_,x,t,c) -> - lamdec_rec (x::l) (name_cons x avoid) (k-1) c - | c -> - let x = next_ident_away (id_of_string "x") avoid in - lamdec_rec ((Name x)::l) (x::avoid) (k-1) - (let a = RVar (dl,x) in - match c with - | RApp (loc,p,l) -> RApp (loc,p,l@[a]) - | _ -> (RApp (dl,c,[a]))) - in - lamdec_rec [] [] k c in - let nl,typ = decompose_lam k p in + let nl,typ = it_destRLambda_or_LetIn_names k p in let n,typ = match typ with | RLambda (_,x,t,c) -> x, c | _ -> Anonymous, typ in let aliastyp = if List.for_all ((=) Anonymous) nl then None - else - let pars = list_tabulate (fun _ -> Anonymous) nparams in - Some (dl,indsp,pars@nl) in + else Some (dl,indsp,nparams,nl) in n, aliastyp, Some typ in let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in @@ -331,22 +334,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = match tag with | LetStyle when aliastyp = None -> let bl' = Array.map detype bl in - let rec decomp_lam_force n avoid l p = - if n = 0 then (List.rev l,p) else - match p with - | RLambda (_,na,_,c) -> - decomp_lam_force (n-1) (name_cons na avoid) (na::l) c - | RLetIn (_,na,_,c) -> - decomp_lam_force (n-1) (name_cons na avoid) (na::l) c - | _ -> - let x = Nameops.next_ident_away (id_of_string "x") avoid in - decomp_lam_force (n-1) (x::avoid) (Name x :: l) - (* eta-expansion *) - (let a = RVar (dl,x) in - match p with - | RApp (loc,p,l) -> RApp (loc,p,l@[a]) - | _ -> (RApp (dl,p,[a]))) in - let (nal,d) = decomp_lam_force consnargsl.(0) avoid [] bl'.(0) in + let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in RLetTuple (dl,nal,(alias,pred),tomatch,d) | IfStyle when aliastyp = None -> let bl' = Array.map detype bl in @@ -360,6 +348,10 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | _ -> RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl) +let detype_sort = function + | Prop c -> RProp c + | Type u -> RType (Some u) + (**********************************************************************) (* Main detyping function *) @@ -380,10 +372,9 @@ let rec detype isgoal avoid env t = let _ = Global.lookup_named id in RRef (dl, VarRef id) with _ -> RVar (dl, id)) - | Sort (Prop c) -> RSort (dl,RProp c) - | Sort (Type u) -> RSort (dl,RType (Some u)) + | Sort s -> RSort (dl,detype_sort s) | Cast (c1,k,c2) -> - RCast(dl,detype isgoal avoid env c1, k, + RCast(dl,detype isgoal avoid env c1, CastConv k, detype isgoal avoid env c2) | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c @@ -421,7 +412,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) = let v = array_map3 (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t)) bodies tys vn in - RRec(dl,RFix (Array.map (fun i -> i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), + RRec(dl,RFix (Array.map (fun i -> Some i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) @@ -587,9 +578,9 @@ let rec subst_rawconstr subst raw = let a' = subst_rawconstr subst a in let (n,topt) = x in let topt' = option_smartmap - (fun (loc,(sp,i),x as t) -> + (fun (loc,(sp,i),x,y as t) -> let sp' = subst_kn subst sp in - if sp == sp' then t else (loc,(sp',i),x)) topt in + if sp == sp' then t else (loc,(sp',i),x,y)) topt in if a == a' && topt == topt' then y else (a',(n,topt'))) rl and branches' = list_smartmap (fun (loc,idl,cpl,r as branch) -> @@ -645,3 +636,18 @@ let rec subst_rawconstr subst raw = RCast (loc,r1',k,r2') | RDynamic _ -> raw + +(* Utilities to transform kernel cases to simple pattern-matching problem *) + +let simple_cases_matrix_of_branches ind brns brs = + list_map2_i (fun i n b -> + let nal,c = it_destRLambda_or_LetIn_names n b in + let mkPatVar na = PatVar (dummy_loc,na) in + let p = PatCstr (dummy_loc,(ind,i+1),List.map mkPatVar nal,Anonymous) in + let ids = map_succeed Nameops.out_name nal in + (dummy_loc,ids,[p],c)) + 0 brns brs + +let return_type_of_predicate ind nparams n pred = + let nal,p = it_destRLambda_or_LetIn_names (n+1) pred in + (List.hd nal, Some (dummy_loc, ind, nparams, List.tl nal)), Some p diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 0b35728c..bbe2fcc9 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: detyping.mli 7881 2006-01-16 14:03:05Z herbelin $ i*) +(*i $Id: detyping.mli 8831 2006-05-19 09:29:54Z herbelin $ i*) (*i*) open Util @@ -38,6 +38,8 @@ val detype_case : identifier list -> inductive * case_style * int * int array * int -> 'a option -> 'a -> 'a array -> rawconstr +val detype_sort : sorts -> rawsort + (* look for the index of a named var or a nondep var as it is renamed *) val lookup_name_as_renamed : env -> constr -> identifier -> int option val lookup_index_as_renamed : env -> constr -> int -> int option @@ -47,3 +49,12 @@ val force_wildcard : unit -> bool val synthetize_type : unit -> bool val force_if : case_info -> bool val force_let : case_info -> bool + +(* Utilities to transform kernel cases to simple pattern-matching problem *) + +val it_destRLambda_or_LetIn_names : int -> rawconstr -> name list * rawconstr +val simple_cases_matrix_of_branches : + inductive -> int list -> rawconstr list -> cases_clauses +val return_type_of_predicate : + inductive -> int -> int -> rawconstr -> predicate_pattern * rawconstr option + diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 2b04b693..458f5bd3 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml 8111 2006-03-02 17:23:41Z herbelin $ *) +(* $Id: evarconv.ml 8793 2006-05-05 17:41:41Z barras $ *) open Util open Names open Term +open Closure open Reduction open Reductionops -open Closure open Environ open Typing open Classops @@ -41,7 +41,7 @@ let eval_flexible_term env c = match kind_of_term c with | Const c -> constant_opt_value env c | Rel n -> - (try let (_,v,_) = lookup_rel n env in option_app (lift n) v + (try let (_,v,_) = lookup_rel n env in option_map (lift n) v with Not_found -> None) | Var id -> (try let (_,v,_) = lookup_named id env in v with Not_found -> None) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index aeaaefef..506cd03f 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarutil.ml 8695 2006-04-10 16:33:52Z msozeau $ *) +(* $Id: evarutil.ml 8759 2006-04-28 12:24:14Z herbelin $ *) open Util open Pp @@ -35,7 +35,7 @@ exception Uninstantiated_evar of existential_key let rec whd_ise sigma c = match kind_of_term c with - | Evar (ev,args) when Evd.in_dom sigma ev -> + | Evar (ev,args) when Evd.mem sigma ev -> if Evd.is_defined sigma ev then whd_ise sigma (existential_value sigma (ev,args)) else raise (Uninstantiated_evar ev) @@ -46,7 +46,7 @@ let rec whd_ise sigma c = let whd_castappevar_stack sigma c = let rec whrec (c, l as s) = match kind_of_term c with - | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> + | Evar (ev,args) when Evd.mem sigma ev & Evd.is_defined sigma ev -> whrec (existential_value sigma (ev,args), l) | Cast (c,_,_) -> whrec (c, l) | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l) @@ -93,7 +93,7 @@ let collect_evars emap c = let rec collrec acc c = match kind_of_term c with | Evar (k,_) -> - if Evd.in_dom emap k & not (Evd.is_defined emap k) then k::acc + if Evd.mem emap k & not (Evd.is_defined emap k) then k::acc else (* No recursion on the evar instantiation *) acc | _ -> fold_constr collrec acc c in @@ -103,13 +103,14 @@ let push_dependent_evars sigma emap = Evd.fold (fun ev {evar_concl = ccl} (sigma',emap') -> List.fold_left (fun (sigma',emap') ev -> - (Evd.add sigma' ev (Evd.map emap' ev),Evd.rmv emap' ev)) + (Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev)) (sigma',emap') (collect_evars emap' ccl)) emap (sigma,emap) (* replaces a mapping of existentials into a mapping of metas. Problem if an evar appears in the type of another one (pops anomaly) *) let evars_to_metas sigma (emap, c) = + let emap = nf_evars emap in let sigma',emap' = push_dependent_evars sigma emap in let change_exist evar = let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in @@ -117,7 +118,7 @@ let evars_to_metas sigma (emap, c) = mkCast (mkMeta n, DEFAULTcast, ty) in let rec replace c = match kind_of_term c with - Evar (k,_ as ev) when Evd.in_dom emap' k -> change_exist ev + Evar (k,_ as ev) when Evd.mem emap' k -> change_exist ev | _ -> map_constr replace c in (sigma', replace c) @@ -209,7 +210,7 @@ let push_rel_context_to_named_context env = let id = next_name_away na avoid in ((mkVar id)::subst, id::avoid, - push_named (id,option_app (substl subst) c, + push_named (id,option_map (substl subst) c, type_app (substl subst) t) env)) (rel_context env) ~init:([],ids_of_named_context (named_context env),env) @@ -297,7 +298,7 @@ let is_defined_equation env evd (ev,inst) rhs = is_pattern inst && not (occur_evar ev rhs) && try - let evi = Evd.map (evars_of evd) ev in + let evi = Evd.find (evars_of evd) ev in let (evd',body) = inverse_instance env evd ev evi inst rhs in evar_well_typed_body evd' ev evi body with Failure _ -> false @@ -313,7 +314,7 @@ let is_defined_equation env evd (ev,inst) rhs = let do_restrict_hyps evd ev args = let args = Array.to_list args in - let evi = Evd.map (evars_of !evd) ev in + let evi = Evd.find (evars_of !evd) ev in let env = evar_env evi in let hyps = evar_context evi in let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in @@ -395,7 +396,7 @@ let evar_define env (ev,argsv) rhs isevars = if occur_evar ev rhs then error_occur_check env (evars_of isevars) ev rhs; let args = Array.to_list argsv in - let evi = Evd.map (evars_of isevars) ev in + let evi = Evd.find (evars_of isevars) ev in (* the bindings to invert *) let worklist = make_subst (evar_env evi) args in let (isevars',body) = real_clean env isevars ev evi worklist rhs in @@ -502,7 +503,7 @@ let status_changed lev (pbty,t1,t2) = let solve_refl conv_algo env isevars ev argsv1 argsv2 = if argsv1 = argsv2 then (isevars,[]) else - let evd = Evd.map (evars_of isevars) ev in + let evd = Evd.find (evars_of isevars) ev in let hyps = evar_context evd in let (isevars',_,rsign) = array_fold_left2 @@ -599,7 +600,7 @@ let mk_valcon c = Some c cumulativity now includes Prop and Set in Type... It is, but that's not too bad *) let define_evar_as_abstraction abs evd (ev,args) = - let evi = Evd.map (evars_of evd) ev in + let evi = Evd.find (evars_of evd) ev in let evenv = evar_env evi in let (evd1,dom) = new_evar evd evenv (new_Type()) in let nvar = @@ -679,7 +680,7 @@ let lift_abstr_tycon_type n (abs, t) = else (Some (init, abs'), t) let lift_tycon_type n (abs, t) = (abs, lift n t) -let lift_tycon n = option_app (lift_tycon_type n) +let lift_tycon n = option_map (lift_tycon_type n) let pr_tycon_type env (abs, t) = match abs with diff --git a/pretyping/evd.ml b/pretyping/evd.ml index c9f771c9..33f88ebd 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evd.ml 8688 2006-04-07 15:08:12Z msozeau $ *) +(* $Id: evd.ml 8759 2006-04-28 12:24:14Z herbelin $ *) open Pp open Util @@ -48,17 +48,16 @@ let empty = Evarmap.empty let to_list evc = Evarmap.fold (fun ev x acc -> (ev,x)::acc) evc [] let dom evc = Evarmap.fold (fun ev _ acc -> ev::acc) evc [] -let map evc k = Evarmap.find k evc -let rmv evc k = Evarmap.remove k evc -let remap evc k i = Evarmap.add k i evc -let in_dom evc k = Evarmap.mem k evc +let find evc k = Evarmap.find k evc +let remove evc k = Evarmap.remove k evc +let mem evc k = Evarmap.mem k evc let fold = Evarmap.fold let add evd ev newinfo = Evarmap.add ev newinfo evd let define evd ev body = let oldinfo = - try map evd ev + try find evd ev with Not_found -> error "Evd.define: cannot define undeclared evar" in let newinfo = { evar_concl = oldinfo.evar_concl; @@ -68,10 +67,10 @@ let define evd ev body = | Evar_empty -> Evarmap.add ev newinfo evd | _ -> anomaly "Evd.define: cannot define an isevar twice" -let is_evar sigma ev = in_dom sigma ev +let is_evar sigma ev = mem sigma ev let is_defined sigma ev = - let info = map sigma ev in + let info = find sigma ev in not (info.evar_body = Evar_empty) let evar_body ev = ev.evar_body @@ -112,7 +111,7 @@ let instantiate_evar sign c args = let existential_type sigma (n,args) = let info = - try map sigma n + try find sigma n with Not_found -> anomaly ("Evar "^(string_of_existential n)^" was not declared") in let hyps = evar_context info in @@ -121,7 +120,7 @@ let existential_type sigma (n,args) = exception NotInstantiatedEvar let existential_value sigma (n,args) = - let info = map sigma n in + let info = find sigma n in let hyps = evar_context info in match evar_body info with | Evar_defined c -> @@ -270,10 +269,9 @@ type evar_map = evar_map1 * sort_constraints let empty = empty, UniverseMap.empty let add (sigma,sm) k v = (add sigma k v, sm) let dom (sigma,_) = dom sigma -let map (sigma,_) = map sigma -let rmv (sigma,sm) k = (rmv sigma k, sm) -let remap (sigma,sm) k v = (remap sigma k v, sm) -let in_dom (sigma,_) = in_dom sigma +let find (sigma,_) = find sigma +let remove (sigma,sm) k = (remove sigma k, sm) +let mem (sigma,_) = mem sigma let to_list (sigma,_) = to_list sigma let fold f (sigma,_) = fold f sigma let define (sigma,sm) k v = (define sigma k v, sm) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 40ecce6e..cbc96b04 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evd.mli 8688 2006-04-07 15:08:12Z msozeau $ i*) +(*i $Id: evd.mli 8759 2006-04-28 12:24:14Z herbelin $ i*) (*i*) open Util @@ -43,10 +43,9 @@ val empty : evar_map val add : evar_map -> evar -> evar_info -> evar_map val dom : evar_map -> evar list -val map : evar_map -> evar -> evar_info -val rmv : evar_map -> evar -> evar_map -val remap : evar_map -> evar -> evar_info -> evar_map -val in_dom : evar_map -> evar -> bool +val find : evar_map -> evar -> evar_info +val remove : evar_map -> evar -> evar_map +val mem : evar_map -> evar -> bool val to_list : evar_map -> (evar * evar_info) list val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index a587dd20..07ca5d83 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indrec.ml 7662 2005-12-17 22:03:35Z herbelin $ *) +(* $Id: indrec.ml 8845 2006-05-23 07:41:58Z herbelin $ *) open Pp open Util @@ -48,13 +48,13 @@ let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c) lift_constructor et lift_inductive_family qui ne se contentent pas de lifter les paramètres globaux *) -let mis_make_case_com depopt env sigma (ind,mib,mip) kind = +let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind = let lnamespar = mib.mind_params_ctxt in let dep = match depopt with - | None -> mip.mind_sort <> (Prop Null) + | None -> inductive_sort_family mip <> InProp | Some d -> d in - if not (List.exists ((=) kind) mip.mind_kelim) then + if not (List.mem kind (elim_sorts specif)) then raise (RecursionSchemeError (NotAllowedCaseAnalysis @@ -431,7 +431,7 @@ let mis_make_indrec env sigma listdepkind mib = it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamesparrec else - mis_make_case_com (Some dep) env sigma (indi,mibi,mipi) kind + mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind in (* Body of mis_make_indrec *) list_tabulate make_one_rec nrec @@ -441,7 +441,7 @@ let mis_make_indrec env sigma listdepkind mib = let make_case_com depopt env sigma ity kind = let (mib,mip) = lookup_mind_specif env ity in - mis_make_case_com depopt env sigma (ity,mib,mip) kind + mis_make_case_com depopt env sigma ity (mib,mip) kind let make_case_dep env = make_case_com (Some true) env let make_case_nodep env = make_case_com (Some false) env @@ -504,7 +504,7 @@ let check_arities listdepkind = let _ = List.fold_left (fun ln ((_,ni),mibi,mipi,dep,kind) -> let id = mipi.mind_typename in - let kelim = mipi.mind_kelim in + let kelim = elim_sorts (mibi,mipi) in if not (List.exists ((=) kind) kelim) then raise (RecursionSchemeError (BadInduction (dep,id,new_sort_in_family kind))) else if List.mem ni ln then raise @@ -534,7 +534,7 @@ let build_mutual_indrec env sigma = function let build_indrec env sigma ind = let (mib,mip) = lookup_mind_specif env ind in - let kind = family_of_sort mip.mind_sort in + let kind = inductive_sort_family mip in let dep = kind <> InProp in List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib) @@ -596,7 +596,7 @@ let lookup_eliminator ind_sp s = pr_id id ++ spc () ++ str "The elimination of the inductive definition " ++ pr_id id ++ spc () ++ str "on sort " ++ - spc () ++ print_sort_family s ++ + spc () ++ pr_sort_family s ++ str " is probably not allowed") @@ -617,6 +617,6 @@ let lookup_eliminator ind_sp s = pr_id id ++ spc () ++ str "The elimination of the inductive definition " ++ pr_id base ++ spc () ++ str "on sort " ++ - spc () ++ print_sort_family s ++ + spc () ++ pr_sort_family s ++ str " is probably not allowed") *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 57d966f1..e0cdeeee 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductiveops.ml 8653 2006-03-22 09:41:17Z herbelin $ *) +(* $Id: inductiveops.ml 8845 2006-05-23 07:41:58Z herbelin $ *) open Util open Names @@ -116,11 +116,15 @@ let constructor_nrealhyps env (ind,j) = let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealdecls.(j-1) +let get_full_arity_sign env ind = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + mip.mind_arity_ctxt + (* Length of arity (w/o local defs) *) let inductive_nargs env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in - mip.mind_nrealargs + rel_context_nhyps mib.mind_params_ctxt + mib.mind_nparams, mip.mind_nrealargs (* Annotation for cases *) let make_case_info env ind style pats_source = @@ -196,10 +200,40 @@ let rec instantiate args c = match kind_of_term c, args with | _, [] -> c | _ -> anomaly "too short arity" +(* substitution in a signature *) + +let substnl_rel_context subst n sign = + let rec aux n = function + | d::sign -> substnl_decl subst n d :: aux (n+1) sign + | [] -> [] + in List.rev (aux n (List.rev sign)) + +let substl_rel_context subst = substnl_rel_context subst 0 + +let rec instantiate_context sign args = + let rec aux subst = function + | (_,None,_)::sign, a::args -> aux (a::subst) (sign,args) + | (_,Some b,_)::sign, args -> aux (substl subst b::subst) (sign,args) + | [], [] -> subst + | _ -> anomaly "Signature/instance mismatch in inductive family" + in aux [] (List.rev sign,args) + let get_arity env (ind,params) = let (mib,mip) = Inductive.lookup_mind_specif env ind in - let arity = mip.mind_nf_arity in - destArity (instantiate params arity) + let parsign = + (* Dynamically detect if called with an instance of recursively + uniform parameter only or also of non recursively uniform + parameters *) + let parsign = mib.mind_params_ctxt in + let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in + if List.length params = rel_context_nhyps parsign - nnonrecparams then + snd (list_chop nnonrecparams mib.mind_params_ctxt) + else + parsign in + let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in + let arsign,_ = list_chop arproperlength mip.mind_arity_ctxt in + let subst = instantiate_context parsign params in + (substl_rel_context subst arsign, Inductive.inductive_sort_family mip) (* Functions to build standard types related to inductive *) let build_dependent_constructor cs = @@ -284,12 +318,12 @@ let find_coinductive env sigma c = (* find appropriate names for pattern variables. Useful in the Case and Inversion (case_then_using et case_nodep_then_using) tactics. *) -let is_predicate_explicitly_dep env pred nodep_ar = - let rec srec env pval nodep_ar = +let is_predicate_explicitly_dep env pred arsign = + let rec srec env pval arsign = let pv' = whd_betadeltaiota env Evd.empty pval in - match kind_of_term pv', kind_of_term nodep_ar with - | Lambda (na,t,b), Prod (_,_,a') -> - srec (push_rel_assum (na,t) env) b a' + match kind_of_term pv', arsign with + | Lambda (na,t,b), (_,None,_)::arsign -> + srec (push_rel_assum (na,t) env) b arsign | Lambda (na,_,_), _ -> (* The following code has impact on the introduction names @@ -317,12 +351,11 @@ let is_predicate_explicitly_dep env pred nodep_ar = | _ -> anomaly "Non eta-expanded dep-expanded \"match\" predicate" in - srec env pred nodep_ar + srec env pred arsign let is_elim_predicate_explicitly_dependent env pred indf = - let arsign,s = get_arity env indf in - let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in - is_predicate_explicitly_dep env pred glob_t + let arsign,_ = get_arity env indf in + is_predicate_explicitly_dep env pred arsign let set_names env n brty = let (ctxt,cl) = decompose_prod_n_assum n brty in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 2993eed3..dcd86716 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -6,13 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: inductiveops.mli 7955 2006-01-30 22:56:15Z herbelin $ i*) +(*i $Id: inductiveops.mli 8845 2006-05-23 07:41:58Z herbelin $ i*) open Names open Term open Declarations open Environ open Evd +open Sign (* The following three functions are similar to the ones defined in Inductive, but they expect an env *) @@ -42,8 +43,7 @@ val dest_ind_type : inductive_type -> inductive_family * constr list val map_inductive_type : (constr -> constr) -> inductive_type -> inductive_type val liftn_inductive_type : int -> int -> inductive_type -> inductive_type val lift_inductive_type : int -> inductive_type -> inductive_type -val substnl_ind_type : - constr list -> int -> inductive_type -> inductive_type +val substnl_ind_type : constr list -> int -> inductive_type -> inductive_type val mkAppliedInd : inductive_type -> constr val mis_is_recursive_subset : int list -> wf_paths -> bool @@ -51,16 +51,22 @@ val mis_is_recursive : inductive * mutual_inductive_body * one_inductive_body -> bool val mis_nf_constructor_type : inductive * mutual_inductive_body * one_inductive_body -> int -> constr -val mis_constr_nargs : inductive -> int array +(* Extract information from an inductive name *) + +val mis_constr_nargs : inductive -> int array val mis_constr_nargs_env : env -> inductive -> int array -val mis_constructor_nargs_env : env -> constructor -> int +(* Return number of expected parameters and of expected real arguments *) +val inductive_nargs : env -> inductive -> int * int +val mis_constructor_nargs_env : env -> constructor -> int val constructor_nrealargs : env -> constructor -> int val constructor_nrealhyps : env -> constructor -> int -val inductive_nargs : env -> inductive -> int +val get_full_arity_sign : env -> inductive -> rel_context + +(* Extract information from an inductive family *) type constructor_summary = { cs_cstr : constructor; @@ -68,17 +74,16 @@ type constructor_summary = { cs_nargs : int; cs_args : Sign.rel_context; cs_concl_realargs : constr array; -} +} val lift_constructor : int -> constructor_summary -> constructor_summary val get_constructor : inductive * mutual_inductive_body * one_inductive_body * constr list -> int -> constructor_summary -val get_arity : env -> inductive_family -> Sign.arity +val get_arity : env -> inductive_family -> rel_context * sorts_family val get_constructors : env -> inductive_family -> constructor_summary array val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr -val make_arity_signature : - env -> bool -> inductive_family -> Sign.rel_context +val make_arity_signature : env -> bool -> inductive_family -> Sign.rel_context val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 5ee245b5..12c1ea33 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: matching.ml 7970 2006-02-01 15:09:07Z herbelin $ *) +(* $Id: matching.ml 8827 2006-05-17 15:15:34Z jforest $ *) (*i*) open Util @@ -17,6 +17,7 @@ open Termops open Reductionops open Term open Rawterm +open Sign open Environ open Pattern (*i*) @@ -70,6 +71,11 @@ let memb_metavars m n = let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2 +let same_case_structure (_,cs1,ind,_) ci2 br1 br2 = + match ind with + | Some ind -> ind = ci2.ci_ind + | None -> cs1 = ci2.ci_cstr_nargs + let matches_core convert allow_partial_app pat c = let rec sorec stk sigma p t = let cT = strip_outer_cast t in @@ -79,7 +85,7 @@ let matches_core convert allow_partial_app pat c = List.map (function | PRel n -> n - | _ -> error "Only bound indices are currently allowed in second order pattern matching") + | _ -> error "Only bound indices allowed in second order pattern matching") args in let frels = Intset.elements (free_rels cT) in if list_subset frels relargs then @@ -150,15 +156,27 @@ let matches_core convert allow_partial_app pat c = if is_conv env evars c cT then sigma else raise PatternMatchingFailure - | PCase (_,_,a1,br1), Case (_,_,a2,br2) -> - (* On ne teste pas le prédicat *) - if (Array.length br1) = (Array.length br2) then - array_fold_left2 (sorec stk) (sorec stk sigma a1 a2) br1 br2 + | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> + let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_nargs.(0) b2 in + let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_nargs.(1) b2' in + let n = List.length ctx and n' = List.length ctx' in + if noccur_between 1 n b2 & noccur_between 1 n' b2' then + let s = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx in + let s' = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx' in + let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in + sorec s' (sorec s (sorec stk sigma a1 a2) b1 b2) b1' b2' else raise PatternMatchingFailure - (* À faire *) - | PFix f0, Fix f1 when f0 = f1 -> sigma - | PCoFix c0, CoFix c1 when c0 = c1 -> sigma + + | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) -> + if same_case_structure ci1 ci2 br1 br2 then + array_fold_left2 (sorec stk) + (sorec stk (sorec stk sigma a1 a2) p1 p2) br1 br2 + else + raise PatternMatchingFailure + + | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> sigma + | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> sigma | _ -> raise PatternMatchingFailure in diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 390b884c..ef97250a 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pattern.ml 7732 2005-12-26 13:51:24Z herbelin $ *) +(* $Id: pattern.ml 8755 2006-04-27 22:22:15Z herbelin $ *) open Util open Names @@ -38,8 +38,9 @@ type constr_pattern = | PLetIn of name * constr_pattern * constr_pattern | PSort of rawsort | PMeta of patvar option - | PCase of (inductive option * case_style) - * constr_pattern option * constr_pattern * constr_pattern array + | PIf of constr_pattern * constr_pattern * constr_pattern + | PCase of (case_style * int array * inductive option * (int * int) option) + * constr_pattern * constr_pattern * constr_pattern array | PFix of fixpoint | PCoFix of cofixpoint @@ -49,9 +50,10 @@ let rec occur_meta_pattern = function | PLambda (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) | PProd (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) | PLetIn (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) - | PCase(_,None,c,br) -> - (occur_meta_pattern c) or (array_exists occur_meta_pattern br) - | PCase(_,Some p,c,br) -> + | PIf (c,c1,c2) -> + (occur_meta_pattern c) or + (occur_meta_pattern c1) or (occur_meta_pattern c2) + | PCase(_,p,c,br) -> (occur_meta_pattern p) or (occur_meta_pattern c) or (array_exists occur_meta_pattern br) | PMeta _ | PSoApp _ -> true @@ -70,6 +72,7 @@ let rec head_pattern_bound t = | PProd (_,_,b) -> head_pattern_bound b | PLetIn (_,_,b) -> head_pattern_bound b | PApp (c,args) -> head_pattern_bound c + | PIf (c,_,_) -> head_pattern_bound c | PCase (_,p,c,br) -> head_pattern_bound c | PRef r -> r | PVar id -> VarRef id @@ -103,28 +106,43 @@ let rec pattern_of_constr t = | Construct sp -> PRef (ConstructRef sp) | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt) | Case (ci,p,a,br) -> - PCase ((Some ci.ci_ind,ci.ci_pp_info.style), - Some (pattern_of_constr p),pattern_of_constr a, + let cip = ci.ci_pp_info in + let no = Some (ci.ci_npar,cip.ind_nargs) in + PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,no), + pattern_of_constr p,pattern_of_constr a, Array.map pattern_of_constr br) | Fix f -> PFix f | CoFix f -> PCoFix f (* To process patterns, we need a translation without typing at all. *) -let rec inst lvar = function - | PVar id as x -> (try List.assoc id lvar with Not_found -> x) - | PApp (p,pl) -> PApp (inst lvar p, Array.map (inst lvar) pl) - | PSoApp (n,pl) -> PSoApp (n, List.map (inst lvar) pl) - | PLambda (n,a,b) -> PLambda (n,inst lvar a,inst lvar b) - | PProd (n,a,b) -> PProd (n,inst lvar a,inst lvar b) - | PLetIn (n,a,b) -> PLetIn (n,inst lvar a,inst lvar b) - | PCase (ci,po,p,pl) -> - PCase (ci,option_app (inst lvar) po,inst lvar p,Array.map (inst lvar) pl) +let map_pattern_with_binders g f l = function + | PApp (p,pl) -> PApp (f l p, Array.map (f l) pl) + | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl) + | PLambda (n,a,b) -> PLambda (n,f l a,f (g l) b) + | PProd (n,a,b) -> PProd (n,f l a,f (g l) b) + | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g l) b) + | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2) + | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p,Array.map (f l) pl) (* Non recursive *) - | (PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ as x) -> x + | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ (* Bound to terms *) - | (PFix _ | PCoFix _) -> - error ("Not instantiable pattern") + | PFix _ | PCoFix _ as x) -> x + +let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) () + +let rec instantiate_pattern lvar = function + | PVar id as x -> (try List.assoc id lvar with Not_found -> x) + | (PFix _ | PCoFix _) -> error ("Not instantiable pattern") + | c -> map_pattern (instantiate_pattern lvar) c + +let rec liftn_pattern k n = function + | PRel i as x -> if i >= n then PRel (i+k) else x + | PFix x -> PFix (destFix (liftn k n (mkFix x))) + | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x))) + | c -> map_pattern_with_binders succ (liftn_pattern k) n c + +let lift_pattern k = liftn_pattern k 1 let rec subst_pattern subst pat = match pat with | PRef ref -> @@ -160,12 +178,20 @@ let rec subst_pattern subst pat = match pat with PLetIn (name,c1',c2') | PSort _ | PMeta _ -> pat - | PCase (cs,typ, c, branches) -> - let typ' = option_smartmap (subst_pattern subst) typ in + | PIf (c,c1,c2) -> + let c' = subst_pattern subst c in + let c1' = subst_pattern subst c1 in + let c2' = subst_pattern subst c2 in + if c' == c && c1' == c1 && c2' == c2 then pat else + PIf (c',c1',c2') + | PCase ((a,b,ind,n as cs),typ,c,branches) -> + let ind' = option_smartmap (Inductiveops.subst_inductive subst) ind in + let typ' = subst_pattern subst typ in let c' = subst_pattern subst c in let branches' = array_smartmap (subst_pattern subst) branches in + let cs' = if ind == ind' then cs else (a,b,ind',n) in if typ' == typ && c' == c && branches' == branches then pat else - PCase(cs,typ', c', branches') + PCase(cs',typ', c', branches') | PFix fixpoint -> let cstr = mkFix fixpoint in let fixpoint' = destFix (subst_mps subst cstr) in @@ -177,8 +203,8 @@ let rec subst_pattern subst pat = match pat with if cofixpoint' == cofixpoint then pat else PCoFix cofixpoint' - -let instantiate_pattern = inst +let mkPLambda na b = PLambda(na,PMeta None,b) +let rev_it_mkPLambda = List.fold_right mkPLambda let rec pat_of_raw metas vars = function | RVar (_,id) -> @@ -212,17 +238,30 @@ let rec pat_of_raw metas vars = function Pp.warning "Cast not taken into account in constr pattern"; pat_of_raw metas vars c | RIf (_,c,(_,None),b1,b2) -> - PCase ((None,IfStyle),None, pat_of_raw metas vars c, - [|pat_of_raw metas vars b1; pat_of_raw metas vars b2|]) - | RCases (loc,None,[c,_],brs) -> - let sp = + PIf (pat_of_raw metas vars c, + pat_of_raw metas vars b1,pat_of_raw metas vars b2) + | RLetTuple (loc,nal,(_,None),b,c) -> + let mkRLambda c na = RLambda (loc,na,RHole (loc,Evd.InternalHole),c) in + let c = List.fold_left mkRLambda c nal in + PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b, + [|pat_of_raw metas vars c|]) + | RCases (loc,p,[c,(na,indnames)],brs) -> + let pred,ind_nargs, ind = match p,indnames with + | Some p, Some (_,ind,n,nal) -> + rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)), + Some (n,List.length nal),Some ind + | _ -> PMeta None, None, None in + let ind = match ind with Some _ -> ind | None -> match brs with | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind | _ -> None in - PCase ((sp,Term.RegularStyle),None, - pat_of_raw metas vars c, - Array.init (List.length brs) - (pat_of_raw_branch loc metas vars sp brs)) + let cbrs = + Array.init (List.length brs) (pat_of_raw_branch loc metas vars ind brs) + in + let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in + PCase ((RegularStyle,cstr_nargs,ind,ind_nargs), pred, + pat_of_raw metas vars c, brs) + | r -> let loc = loc_of_rawconstr r in user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Pattern not supported") @@ -230,12 +269,12 @@ let rec pat_of_raw metas vars = function and pat_of_raw_branch loc metas vars ind brs i = let bri = List.filter (function - (_,_,[PatCstr(_,c,lv,_)],_) -> snd c = i+1 + (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1 | (loc,_,_,_) -> user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Not supported pattern")) brs in match bri with - [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] -> + | [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] -> if ind <> None & ind <> Some indsp then user_err_loc (loc,"pattern_of_rawconstr", Pp.str "All constructors must be in the same inductive type"); @@ -246,8 +285,7 @@ and pat_of_raw_branch loc metas vars ind brs i = user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Not supported pattern")) lv in let vars' = List.rev lna @ vars in - List.fold_right (fun na b -> PLambda(na,PMeta None,b)) lna - (pat_of_raw metas vars' br) + List.length lv, rev_it_mkPLambda lna (pat_of_raw metas vars' br) | _ -> user_err_loc (loc,"pattern_of_rawconstr", str "No unique branch for " ++ int (i+1) ++ str"-th constructor") diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 25a57ed2..1637fc5f 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pattern.mli 7732 2005-12-26 13:51:24Z herbelin $ i*) +(*i $Id: pattern.mli 8755 2006-04-27 22:22:15Z herbelin $ i*) (*i*) open Pp @@ -39,8 +39,9 @@ type constr_pattern = | PLetIn of name * constr_pattern * constr_pattern | PSort of rawsort | PMeta of patvar option - | PCase of (inductive option * case_style) - * constr_pattern option * constr_pattern * constr_pattern array + | PIf of constr_pattern * constr_pattern * constr_pattern + | PCase of (case_style * int array * inductive option * (int * int) option) + * constr_pattern * constr_pattern * constr_pattern array | PFix of fixpoint | PCoFix of cofixpoint @@ -76,3 +77,5 @@ val pattern_of_rawconstr : rawconstr -> val instantiate_pattern : (identifier * constr_pattern) list -> constr_pattern -> constr_pattern + +val lift_pattern : int -> constr_pattern -> constr_pattern diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 48295c92..f5a81659 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretype_errors.ml 8688 2006-04-07 15:08:12Z msozeau $ *) +(* $Id: pretype_errors.ml 8752 2006-04-27 19:37:33Z herbelin $ *) open Util open Stdpp @@ -59,7 +59,7 @@ let env_ise sigma env = Sign.fold_rel_context (fun (na,b,ty) e -> push_rel - (na, option_app (nf_evar sigma) b, nf_evar sigma ty) + (na, option_map (nf_evar sigma) b, nf_evar sigma ty) e) ctxt ~init:env0 @@ -75,7 +75,7 @@ let contract env lc = env | _ -> let t' = substl !l t in - let c' = option_app (substl !l) c in + let c' = option_map (substl !l) c in let na' = named_hd env t' na in l := (mkRel 1) :: List.map (lift 1) !l; push_rel (na',c',t') env in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2d1e297f..ca797f97 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml 8695 2006-04-10 16:33:52Z msozeau $ *) +(* $Id: pretyping.ml 8875 2006-05-29 19:59:11Z msozeau $ *) open Pp open Util @@ -273,7 +273,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | REvar (loc, ev, instopt) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) - let hyps = evar_context (Evd.map (evars_of !isevars) ev) in + let hyps = evar_context (Evd.find (evars_of !isevars) ev) in let args = match instopt with | None -> instance_from_named_context hyps | Some inst -> failwith "Evar subtitutions not implemented" in @@ -329,34 +329,43 @@ module Pretyping_F (Coercion : Coercion.S) = struct { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - evar_type_fixpoint loc env isevars names ftys vdefj; - let fixj = - match fixkind with - | RFix (vn,i) -> - let fix = ((Array.map fst vn, i),(names,ftys,Array.map j_val vdefj)) in - (try check_fix env fix with e -> Stdpp.raise_with_loc loc e); - make_judge (mkFix fix) ftys.(i) - | RCoFix i -> - let cofix = (i,(names,ftys,Array.map j_val vdefj)) in - (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); - make_judge (mkCoFix cofix) ftys.(i) in - inh_conv_coerce_to_tycon loc env isevars fixj tycon + evar_type_fixpoint loc env isevars names ftys vdefj; + let fixj = match fixkind with + | RFix (vn,i) -> + let guard_indexes = Array.mapi + (fun i (n,_) -> match n with + | Some n -> n + | None -> + (* Recursive argument was not given by the user : We + check that there is only one inductive argument *) + let ctx = ctxtv.(i) in + let isIndApp t = + isInd (fst (decompose_app (strip_head_cast t))) in + (* This could be more precise (e.g. do some delta) *) + let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in + try (list_unique_index true lb) - 1 + with Not_found -> + Util.user_err_loc + (loc,"pretype", + Pp.str "cannot guess decreasing argument of fix")) + vn + in + let fix = ((guard_indexes, i),(names,ftys,Array.map j_val vdefj)) in + (try check_fix env fix with e -> Stdpp.raise_with_loc loc e); + make_judge (mkFix fix) ftys.(i) + | RCoFix i -> + let cofix = (i,(names,ftys,Array.map j_val vdefj)) in + (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); + make_judge (mkCoFix cofix) ftys.(i) in + inh_conv_coerce_to_tycon loc env isevars fixj tycon | RSort (loc,s) -> inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon | RApp (loc,f,args) -> - let length = List.length args in - let ftycon = - match tycon with - None -> None - | Some (None, ty) -> mk_abstr_tycon length ty - | Some (Some (init, cur), ty) -> - Some (Some (length + init, length + cur), ty) - in let fj = pretype empty_tycon env isevars lvar f in let floc = loc_of_rawconstr f in - let rec apply_rec env n resj tycon = function + let rec apply_rec env n resj = function | [] -> resj | c::rest -> let argloc = loc_of_rawconstr c in @@ -367,38 +376,22 @@ module Pretyping_F (Coercion : Coercion.S) = struct let hj = pretype (mk_tycon c1) env isevars lvar c in let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in let typ' = nf_isevar !isevars typ in - let tycon = - option_app - (fun (abs, ty) -> - match abs with - None -> - isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' - (abs, ty); - (abs, ty) - | Some (init, cur) -> - isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' - (abs, ty); - (Some (init, pred cur), ty)) - tycon - in apply_rec env (n+1) { uj_val = nf_isevar !isevars value; - uj_type = nf_isevar !isevars typ' } - (option_app (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest - + uj_type = typ' } + rest | _ -> let hj = pretype empty_tycon env isevars lvar c in error_cant_apply_not_functional_loc (join_loc floc argloc) env (evars_of !isevars) resj [hj] in - let ftycon = option_app (lift_abstr_tycon_type (-1)) ftycon in - let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in + let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in let resj = match kind_of_term resj.uj_val with | App (f,args) when isInd f -> let sigma = evars_of !isevars in - let t = Retyping.type_of_applied_inductive env sigma (destInd f) args in + let t = Retyping.type_of_inductive_knowing_parameters env sigma (destInd f) args in let s = snd (splay_arity env sigma t) in on_judgment_type (set_inductive_level env s) resj (* Rem: no need to send sigma: no head evar, it's an arity *) @@ -573,12 +566,19 @@ module Pretyping_F (Coercion : Coercion.S) = struct tycon env (* loc *) (po,tml,eqns) | RCast(loc,c,k,t) -> - let tj = pretype_type empty_valcon env isevars lvar t in - let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in - (* User Casts are for helping pretyping, experimentally not to be kept*) - (* ... except for Correctness *) - let v = mkCast (cj.uj_val, k, tj.utj_val) in - let cj = { uj_val = v; uj_type = tj.utj_val } in + let cj = + match k with + CastCoerce -> + let cj = pretype empty_tycon env isevars lvar c in + evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj + | CastConv k -> + let tj = pretype_type empty_valcon env isevars lvar t in + let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in + (* User Casts are for helping pretyping, experimentally not to be kept*) + (* ... except for Correctness *) + let v = mkCast (cj.uj_val, k, tj.utj_val) in + { uj_val = v; uj_type = tj.utj_val } + in inh_conv_coerce_to_tycon loc env isevars cj tycon | RDynamic (loc,d) -> @@ -640,8 +640,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct let rec proc_rec c = match kind_of_term c with | Evar (ev,args) -> - assert (Evd.in_dom sigma ev); - if not (Evd.in_dom initial_sigma ev) then + assert (Evd.mem sigma ev); + if not (Evd.mem initial_sigma ev) then let (loc,k) = evar_source ev !isevars in error_unsolvable_implicit loc env sigma k | _ -> iter_constr proc_rec c diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 5d177326..e61bf2c3 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: rawterm.ml 8624 2006-03-13 17:38:17Z msozeau $ *) +(* $Id: rawterm.ml 8878 2006-05-30 16:44:25Z herbelin $ *) (*i*) open Util @@ -47,6 +47,10 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings +type cast_type = + | CastConv of cast_kind + | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *) + type rawconstr = | RRef of (loc * global_reference) | RVar of (loc * identifier) @@ -56,9 +60,7 @@ type rawconstr = | RLambda of loc * name * rawconstr * rawconstr | RProd of loc * name * rawconstr * rawconstr | RLetIn of loc * name * rawconstr * rawconstr - | RCases of loc * rawconstr option * - (rawconstr * (name * (loc * inductive * name list) option)) list * - (loc * identifier list * cases_pattern list * rawconstr) list + | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses | RLetTuple of loc * name list * (name * rawconstr option) * rawconstr * rawconstr | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr @@ -66,19 +68,29 @@ type rawconstr = rawconstr array * rawconstr array | RSort of loc * rawsort | RHole of (loc * hole_kind) - | RCast of loc * rawconstr * cast_kind * rawconstr + | RCast of loc * rawconstr * cast_type * rawconstr | RDynamic of loc * Dyn.t and rawdecl = name * rawconstr option * rawconstr and fix_recursion_order = RStructRec | RWfRec of rawconstr -and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int +and fix_kind = + | RFix of ((int option * fix_recursion_order) array * int) + | RCoFix of int + +and predicate_pattern = + name * (loc * inductive * int * name list) option + +and tomatch_tuple = (rawconstr * predicate_pattern) list + +and cases_clauses = + (loc * identifier list * cases_pattern list * rawconstr) list let cases_predicate_names tml = List.flatten (List.map (function | (tm,(na,None)) -> [na] - | (tm,(na,Some (_,_,nal))) -> na::nal) tml) + | (tm,(na,Some (_,_,_,nal))) -> na::nal) tml) (*i - if PRec (_, names, arities, bodies) is in env then arities are typed in env too and bodies are typed in env enriched by the @@ -89,7 +101,7 @@ let cases_predicate_names tml = - boolean in POldCase means it is recursive i*) -let map_rawdecl f (na,obd,ty) = (na,option_app f obd,f ty) +let map_rawdecl f (na,obd,ty) = (na,option_map f obd,f ty) let map_rawconstr f = function | RVar (loc,id) -> RVar (loc,id) @@ -98,13 +110,13 @@ let map_rawconstr f = function | RProd (loc,na,ty,c) -> RProd (loc,na,f ty,f c) | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c) | RCases (loc,rtntypopt,tml,pl) -> - RCases (loc,option_app f rtntypopt, + RCases (loc,option_map f rtntypopt, List.map (fun (tm,x) -> (f tm,x)) tml, List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl) | RLetTuple (loc,nal,(na,po),b,c) -> - RLetTuple (loc,nal,(na,option_app f po),f b,f c) + RLetTuple (loc,nal,(na,option_map f po),f b,f c) | RIf (loc,c,(na,po),b1,b2) -> - RIf (loc,f c,(na,option_app f po),f b1,f b2) + RIf (loc,f c,(na,option_map f po),f b1,f b2) | RRec (loc,fk,idl,bl,tyl,bv) -> RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl, Array.map f tyl,Array.map f bv) @@ -137,7 +149,7 @@ let map_rawconstr_with_binders_loc loc g f e = function let g' id e = snd (g id e) in let h (_,idl,p,c) = (loc,idl,p,f (List.fold_right g' idl e) c) in RCases - (loc,option_app (f e) tyopt,List.map (f e) tml, List.map h pl) + (loc,option_map (f e) tyopt,List.map (f e) tml, List.map h pl) | RRec (_,fk,idl,tyl,bv) -> let idl',e' = fold_ident g idl e in RRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv) @@ -251,22 +263,24 @@ type 'a raw_red_flag = { let all_flags = {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []} -type 'a occurrences = int list * 'a +type 'a or_var = ArgArg of 'a | ArgVar of identifier located + +type 'a with_occurrences = int or_var list * 'a type ('a,'b) red_expr_gen = | Red of bool | Hnf - | Simpl of 'a occurrences option + | Simpl of 'a with_occurrences option | Cbv of 'b raw_red_flag | Lazy of 'b raw_red_flag - | Unfold of 'b occurrences list + | Unfold of 'b with_occurrences list | Fold of 'a list - | Pattern of 'a occurrences list + | Pattern of 'a with_occurrences list | ExtraRedExpr of string | CbvVm type ('a,'b) may_eval = | ConstrTerm of 'a - | ConstrEval of ('a, 'b) red_expr_gen * 'a + | ConstrEval of ('a,'b) red_expr_gen * 'a | ConstrContext of (loc * identifier) * 'a | ConstrTypeOf of 'a diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 22317b5f..b29cc7b6 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: rawterm.mli 8624 2006-03-13 17:38:17Z msozeau $ i*) +(*i $Id: rawterm.mli 8878 2006-05-30 16:44:25Z herbelin $ i*) (*i*) open Util @@ -44,6 +44,10 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings +type cast_type = + | CastConv of cast_kind + | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *) + type rawconstr = | RRef of (loc * global_reference) | RVar of (loc * identifier) @@ -53,9 +57,7 @@ type rawconstr = | RLambda of loc * name * rawconstr * rawconstr | RProd of loc * name * rawconstr * rawconstr | RLetIn of loc * name * rawconstr * rawconstr - | RCases of loc * rawconstr option * - (rawconstr * (name * (loc * inductive * name list) option)) list * - (loc * identifier list * cases_pattern list * rawconstr) list + | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses | RLetTuple of loc * name list * (name * rawconstr option) * rawconstr * rawconstr | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr @@ -63,17 +65,26 @@ type rawconstr = rawconstr array * rawconstr array | RSort of loc * rawsort | RHole of (loc * Evd.hole_kind) - | RCast of loc * rawconstr * cast_kind * rawconstr + | RCast of loc * rawconstr * cast_type * rawconstr | RDynamic of loc * Dyn.t and rawdecl = name * rawconstr option * rawconstr and fix_recursion_order = RStructRec | RWfRec of rawconstr -and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int +and fix_kind = + | RFix of ((int option * fix_recursion_order) array * int) + | RCoFix of int + +and predicate_pattern = + name * (loc * inductive * int * name list) option + +and tomatch_tuple = (rawconstr * predicate_pattern) list -val cases_predicate_names : - (rawconstr * (name * (loc * inductive * name list) option)) list -> name list +and cases_clauses = + (loc * identifier list * cases_pattern list * rawconstr) list + +val cases_predicate_names : tomatch_tuple -> name list (*i - if PRec (_, names, arities, bodies) is in env then arities are typed in env too and bodies are typed in env enriched by the @@ -121,22 +132,24 @@ type 'a raw_red_flag = { val all_flags : 'a raw_red_flag -type 'a occurrences = int list * 'a +type 'a or_var = ArgArg of 'a | ArgVar of identifier located + +type 'a with_occurrences = int or_var list * 'a type ('a,'b) red_expr_gen = | Red of bool | Hnf - | Simpl of 'a occurrences option + | Simpl of 'a with_occurrences option | Cbv of 'b raw_red_flag | Lazy of 'b raw_red_flag - | Unfold of 'b occurrences list + | Unfold of 'b with_occurrences list | Fold of 'a list - | Pattern of 'a occurrences list + | Pattern of 'a with_occurrences list | ExtraRedExpr of string | CbvVm type ('a,'b) may_eval = | ConstrTerm of 'a - | ConstrEval of ('a, 'b) red_expr_gen * 'a + | ConstrEval of ('a,'b) red_expr_gen * 'a | ConstrContext of (loc * identifier) * 'a | ConstrTypeOf of 'a diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 87997d99..5d38f52c 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: recordops.ml 8642 2006-03-17 10:09:02Z notin $ *) +(* $Id: recordops.ml 8752 2006-04-27 19:37:33Z herbelin $ *) open Util open Pp @@ -67,7 +67,7 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) = let discharge_structure (_,(ind,id,kl,projs)) = Some (Lib.discharge_inductive ind, id, kl, - List.map (option_app Lib.discharge_con) projs) + List.map (option_map Lib.discharge_con) projs) let (inStruc,outStruc) = declare_object {(default_object "STRUCTURE") with diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index b590f743..82cc1b7d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: reductionops.ml 8708 2006-04-14 08:13:02Z jforest $ *) +(* $Id: reductionops.ml 8845 2006-05-23 07:41:58Z herbelin $ *) open Pp open Util @@ -23,6 +23,91 @@ open Reduction exception Elimconst + +(**********************************************************************) +(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) + +type 'a stack_member = + | Zapp of 'a list + | Zcase of case_info * 'a * 'a array + | Zfix of 'a * 'a stack + | Zshift of int + | Zupdate of 'a + +and 'a stack = 'a stack_member list + +let empty_stack = [] +let append_stack_list = function + | ([],s) -> s + | (l1, Zapp l :: s) -> Zapp (l1@l) :: s + | (l1, s) -> Zapp l1 :: s +let append_stack v s = append_stack_list (Array.to_list v, s) + +(* Collapse the shifts in the stack *) +let zshift n s = + match (n,s) with + (0,_) -> s + | (_,Zshift(k)::s) -> Zshift(n+k)::s + | _ -> Zshift(n)::s + +let rec stack_args_size = function + | Zapp l::s -> List.length l + stack_args_size s + | Zshift(_)::s -> stack_args_size s + | Zupdate(_)::s -> stack_args_size s + | _ -> 0 + +(* When used as an argument stack (only Zapp can appear) *) +let rec decomp_stack = function + | Zapp[v]::s -> Some (v, s) + | Zapp(v::l)::s -> Some (v, (Zapp l :: s)) + | Zapp [] :: s -> decomp_stack s + | _ -> None +let rec decomp_stackn = function + | Zapp [] :: s -> decomp_stackn s + | Zapp l :: s -> (Array.of_list l, s) + | _ -> assert false +let array_of_stack s = + let rec stackrec = function + | [] -> [] + | Zapp args :: s -> args :: (stackrec s) + | _ -> assert false + in Array.of_list (List.concat (stackrec s)) +let rec list_of_stack = function + | [] -> [] + | Zapp args :: s -> args @ (list_of_stack s) + | _ -> assert false +let rec app_stack = function + | f, [] -> f + | f, (Zapp [] :: s) -> app_stack (f, s) + | f, (Zapp args :: s) -> + app_stack (applist (f, args), s) + | _ -> assert false +let rec stack_assign s p c = match s with + | Zapp args :: s -> + let q = List.length args in + if p >= q then + Zapp args :: stack_assign s (p-q) c + else + (match list_chop p args with + (bef, _::aft) -> Zapp (bef@c::aft) :: s + | _ -> assert false) + | _ -> s +let rec stack_tail p s = + if p = 0 then s else + match s with + | Zapp args :: s -> + let q = List.length args in + if p >= q then stack_tail (p-q) s + else Zapp (list_skipn p args) :: s + | _ -> failwith "stack_tail" +let rec stack_nth s p = match s with + | Zapp args :: s -> + let q = List.length args in + if p >= q then stack_nth s (p-q) + else List.nth args p + | _ -> raise Not_found + +(**************************************************************) (* The type of (machine) states (= lambda-bar-calculus' cuts) *) type state = constr * constr stack @@ -428,13 +513,13 @@ let whd_betadeltaiota_nolet env sigma x = let rec whd_evar sigma c = match kind_of_term c with | Evar (ev,args) - when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> + when Evd.mem sigma ev & Evd.is_defined sigma ev -> whd_evar sigma (Evd.existential_value sigma (ev,args)) | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c | _ -> collapse_appl c -let nf_evar evd = - local_strong (whd_evar evd) +let nf_evar sigma = + local_strong (whd_evar sigma) (* lazy reduction functions. The infos must be created for each term *) let clos_norm_flags flgs env sigma t = @@ -451,113 +536,49 @@ let nf_betadeltaiota env sigma = du type checking : (fun x => x + x) M *) -let nf_betaiotaevar_preserving_vm_cast env sigma t = - let push decl (env,subst) = - (Environ.push_rel decl env, Esubst.subs_lift subst) in - let cons decl v (env, subst) = (push_rel decl env, Esubst.subs_cons (v,subst)) in - - let app_stack t (f, stack) = - let t' = app_stack (f,stack) in - match kind_of_term t, kind_of_term t' with - | App(f,args), App(f',args') when f == f' && array_for_all2 (==) args args' -> t - | _ -> t' - in - let rec whrec (env, subst as es) (t, stack as s) = - match kind_of_term t with - | Rel i -> - let t' = - match Esubst.expand_rel i subst with - | Inl (k,e) -> lift k e - | Inr (k,None) -> mkRel k - | Inr (k, Some p) -> lift (k-p) (mkRel p) (*??????? == mkRel k ! Julien *) - (* Est correct ??? *) - in - if t = t' then s else t', stack - | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> s - | Evar (e,al) -> - let al' = Array.map (norm es) al in - begin match existential_opt_value sigma (e,al') with - | Some body -> whrec (env,Esubst.ESID 0) (body, stack) (**** ????? ****) - | None -> - if array_for_all2 (==) al al' then s else (mkEvar (e, al'), stack) - end - | Cast (c,VMcast,t) -> - let c' = norm es c in - let t' = norm es t in - if c == c' && t == t' then s - else (mkCast(c',VMcast,t'),stack) - | Cast (c,DEFAULTcast,_) -> - whrec es (c, stack) - - | Prod (na,t,c) -> - let t' = norm es t in - let c' = norm (push (na, None, t') es) c in - if t==t' && c==c' then s else (mkProd (na, t', c'), stack) - - | Lambda (na,t,c) -> - begin match decomp_stack stack with - | Some (a,m) -> - begin match kind_of_term a with - | Rel i when not (evaluable_rel i env) -> - whrec (cons (na,None,t) a es) (c, m) - | Var id when not (evaluable_named id env)-> - whrec (cons (na,None,t) a es) (c, m) - | _ -> - let t' = norm es t in - let c' = norm (push (na, None, t') es) c in - if t == t' && c == c' then s - else mkLambda (na, t', c'), stack - end - | _ -> - let t' = norm es t in - let c' = norm (push (na, None, t') es) c in - if t == t' && c == c' then s - else mkLambda(na,t',c'),stack - - end - | LetIn (na,b,t,c) -> - let b' = norm es b in - let t' = norm es t in - let c' = norm (push (na, Some b', t') es) c in - if b==b' && t==t' && c==c' then s - else mkLetIn (na, b', t', c'), stack - - | App (f,cl) -> - let cl' = Array.map (norm es) cl in - whrec es (f, append_stack cl' stack) - - | Case (ci,p,d,lf) -> - let (c,cargs) = whrec es (d, empty_stack) in - if reducible_mind_case c then - whrec es (reduce_mind_case - {mP=p; mconstr=c; mcargs=list_of_stack cargs; - mci=ci; mlf=lf}, stack) - else - let p' = norm es p in - let d' = app_stack d (c,cargs) in - let lf' = Array.map (norm es) lf in - if p==p' && d==d' && array_for_all2 (==) lf lf' then s - else (mkCase (ci, p', d', lf'), stack) - | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.map (norm es) tl in - let es' = - array_fold_left2 (fun es na t -> push (na,None,t) es) es lna tl' in - let bl' = Array.map (norm es') bl in - if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl' - then s - else (mkFix (ln,(lna,tl',bl')), stack) - | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.map (norm es) tl in - let es' = - array_fold_left2 (fun es na t -> push (na,None,t) es) es lna tl in - let bl' = Array.map (norm es') bl in - if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl' - then s - else (mkCoFix (ln,(lna,tl',bl')), stack) - - and norm es t = app_stack t (whrec es (t,empty_stack)) in - norm (env, Esubst.ESID 0) t - +let rec whd_betaiotaevar_preserving_vm_cast env sigma t = + let rec stacklam_var subst t stack = + match (decomp_stack stack,kind_of_term t) with + | Some (h,stacktl), Lambda (_,_,c) -> + begin match kind_of_term h with + | Rel i when not (evaluable_rel i env) -> + stacklam_var (h::subst) c stacktl + | Var id when not (evaluable_named id env)-> + stacklam_var (h::subst) c stacktl + | _ -> whrec (substl subst t, stack) + end + | _ -> whrec (substl subst t, stack) + and whrec (x, stack as s) = + match kind_of_term x with + | Evar ev -> + (match existential_opt_value sigma ev with + | Some body -> whrec (body, stack) + | None -> s) + | Cast (c,VMcast,t) -> + let c = app_stack (whrec (c,empty_stack)) in + let t = app_stack (whrec (t,empty_stack)) in + (mkCast(c,VMcast,t),stack) + | Cast (c,DEFAULTcast,_) -> + whrec (c, stack) + | App (f,cl) -> whrec (f, append_stack cl stack) + | Lambda (na,t,c) -> + (match decomp_stack stack with + | Some (a,m) -> stacklam_var [a] c m + | _ -> s) + | Case (ci,p,d,lf) -> + let (c,cargs) = whrec (d, empty_stack) in + if reducible_mind_case c then + whrec (reduce_mind_case + {mP=p; mconstr=c; mcargs=list_of_stack cargs; + mci=ci; mlf=lf}, stack) + else + (mkCase (ci, p, app_stack (c,cargs), lf), stack) + | x -> s + in + app_stack (whrec (t,empty_stack)) + +let nf_betaiotaevar_preserving_vm_cast = + strong whd_betaiotaevar_preserving_vm_cast (* lazy weak head reduction functions *) let whd_flags flgs env sigma t = @@ -825,26 +846,6 @@ let is_arity env sigma c = match find_conclusion env sigma c with | Sort _ -> true | _ -> false - -let info_arity env sigma c = - match find_conclusion env sigma c with - | Sort (Prop Null) -> false - | Sort (Prop Pos) -> true - | _ -> raise IsType - -let is_info_arity env sigma c = - try (info_arity env sigma c) with IsType -> true - -let is_type_arity env sigma c = - match find_conclusion env sigma c with - | Sort (Type _) -> true - | _ -> false - -let is_info_type env sigma t = - let s = t.utj_type in - (s = Prop Pos) || - (s <> Prop Null && - try info_arity env sigma t.utj_val with IsType -> true) (*************************************) (* Metas *) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index ff55cc0e..78afd22b 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: reductionops.mli 8708 2006-04-14 08:13:02Z jforest $ i*) +(*i $Id: reductionops.mli 8812 2006-05-13 11:46:02Z herbelin $ i*) (*i*) open Names @@ -21,6 +21,34 @@ open Closure exception Elimconst +(************************************************************************) +(*s A [stack] is a context of arguments, arguments are pushed by + [append_stack] one array at a time but popped with [decomp_stack] + one by one *) + +type 'a stack_member = + | Zapp of 'a list + | Zcase of case_info * 'a * 'a array + | Zfix of 'a * 'a stack + | Zshift of int + | Zupdate of 'a + +and 'a stack = 'a stack_member list + +val empty_stack : 'a stack +val append_stack : 'a array -> 'a stack -> 'a stack + +val decomp_stack : 'a stack -> ('a * 'a stack) option +val list_of_stack : 'a stack -> 'a list +val array_of_stack : 'a stack -> 'a array +val stack_assign : 'a stack -> int -> 'a -> 'a stack +val stack_args_size : 'a stack -> int +val app_stack : constr * constr stack -> constr +val stack_tail : int -> 'a stack -> 'a stack +val stack_nth : 'a stack -> int -> 'a + +(************************************************************************) + type state = constr * constr stack type contextual_reduction_function = env -> evar_map -> constr -> constr @@ -147,13 +175,6 @@ val reduce_mind_case : constr miota_args -> constr val find_conclusion : env -> evar_map -> constr -> (constr,constr) kind_of_term val is_arity : env -> evar_map -> constr -> bool -val is_info_type : env -> evar_map -> unsafe_type_judgment -> bool -val is_info_arity : env -> evar_map -> constr -> bool -(*i Pour l'extraction -val is_type_arity : env -> 'a evar_map -> constr -> bool -val is_info_cast_type : env -> 'a evar_map -> constr -> bool -val contents_of_cast_type : env -> 'a evar_map -> constr -> contents -i*) val whd_programs : reduction_function diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 32da4cea..428a7306 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: retyping.ml 8673 2006-03-29 21:21:52Z herbelin $ *) +(* $Id: retyping.ml 8871 2006-05-28 16:46:48Z herbelin $ *) open Util open Term @@ -74,7 +74,7 @@ let typeur sigma metamap = | Fix ((_,i),(_,tys,_)) -> tys.(i) | CoFix (i,(_,tys,_)) -> tys.(i) | App(f,args) when isInd f -> - let t = type_of_applied_inductive env (destInd f) args in + let t = type_of_inductive_knowing_parameters env (destInd f) args in strip_outer_cast (subst_type env sigma t (Array.to_list args)) | App(f,args) -> strip_outer_cast @@ -98,7 +98,7 @@ let typeur sigma metamap = | Prop Null, (Type _ as s) -> s | Type u1, Type u2 -> Type (Univ.sup u1 u2)) | App(f,args) when isInd f -> - let t = type_of_applied_inductive env (destInd f) args in + let t = type_of_inductive_knowing_parameters env (destInd f) args in sort_of_atomic_type env sigma t args | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | Lambda _ | Fix _ | Construct _ -> @@ -117,25 +117,17 @@ let typeur sigma metamap = anomaly "sort_of: Not a type (1)" | _ -> family_of_sort (decomp_sort env sigma (type_of env t)) - and type_of_applied_inductive env ind args = - let specif = lookup_mind_specif env ind in - let t = Inductive.type_of_inductive specif in - if is_small_inductive specif then - (* No polymorphism *) - t - else - (* Retyping constructor with the actual arguments *) - let env',llc,ls0 = constructor_instances env specif ind args in - let lls = Array.map (Array.map (sort_of env')) llc in - let ls = Array.map max_inductive_sort lls in - set_inductive_level env (find_inductive_level env specif ind ls0 ls) t + and type_of_inductive_knowing_parameters env ind args = + let (_,mip) = lookup_mind_specif env ind in + let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in + Inductive.type_of_inductive_knowing_parameters env mip argtyps - in type_of, sort_of, sort_family_of, type_of_applied_inductive + in type_of, sort_of, sort_family_of, type_of_inductive_knowing_parameters let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c -let type_of_applied_inductive env sigma ind args = +let type_of_inductive_knowing_parameters env sigma ind args = let _,_,_,f = typeur sigma [] in f env ind args let get_type_of_with_meta env sigma metamap = diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 7adec66b..923123c5 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: retyping.mli 8673 2006-03-29 21:21:52Z herbelin $ i*) +(*i $Id: retyping.mli 8871 2006-05-28 16:46:48Z herbelin $ i*) (*i*) open Names @@ -34,5 +34,5 @@ val get_assumption_of : env -> evar_map -> constr -> types (* Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment -val type_of_applied_inductive : env -> evar_map -> inductive -> +val type_of_inductive_knowing_parameters : env -> evar_map -> inductive -> constr array -> types diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 88af6290..006e14b3 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml 8003 2006-02-07 22:11:50Z herbelin $ *) +(* $Id: tacred.ml 8793 2006-05-05 17:41:41Z barras $ *) open Pp open Util @@ -18,8 +18,8 @@ open Termops open Declarations open Inductive open Environ -open Reductionops open Closure +open Reductionops open Cbv open Rawterm @@ -80,7 +80,7 @@ let reference_opt_value sigma env = function v | EvalRel n -> let (_,v,_) = lookup_rel n env in - option_app (lift n) v + option_map (lift n) v | EvalEvar ev -> Evd.existential_opt_value sigma ev exception NotEvaluable diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index a5468435..691fdf01 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacred.mli 8003 2006-02-07 22:11:50Z herbelin $ i*) +(*i $Id: tacred.mli 8878 2006-05-30 16:44:25Z herbelin $ i*) (*i*) open Names @@ -77,5 +77,5 @@ val reduce_to_quantified_ref : val reduce_to_atomic_ref : env -> evar_map -> Libnames.global_reference -> types -> types -val contextually : bool -> constr occurrences -> reduction_function +val contextually : bool -> int list * constr -> reduction_function -> reduction_function diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 89de5537..823da969 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: termops.ml 8003 2006-02-07 22:11:50Z herbelin $ *) +(* $Id: termops.ml 8845 2006-05-23 07:41:58Z herbelin $ *) open Pp open Util @@ -25,7 +25,7 @@ let print_sort = function | Prop Null -> (str "Prop") | Type u -> (str "Type(" ++ Univ.pr_uni u ++ str ")") -let print_sort_family = function +let pr_sort_family = function | InSet -> (str "Set") | InProp -> (str "Prop") | InType -> (str "Type") @@ -961,7 +961,7 @@ let assums_of_rel_context sign = let lift_rel_context n sign = let rec liftrec k = function | (na,c,t)::sign -> - (na,option_app (liftn n k) c,type_app (liftn n k) t) + (na,option_map (liftn n k) c,type_app (liftn n k) t) ::(liftrec (k-1) sign) | [] -> [] in diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 5f8b5376..49de4838 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: termops.mli 8003 2006-02-07 22:11:50Z herbelin $ i*) +(*i $Id: termops.mli 8845 2006-05-23 07:41:58Z herbelin $ i*) open Util open Pp @@ -24,7 +24,7 @@ val refresh_universes : types -> types (* printers *) val print_sort : sorts -> std_ppcmds -val print_sort_family : sorts_family -> std_ppcmds +val pr_sort_family : sorts_family -> std_ppcmds (* debug printer: do not use to display terms to the casual user... *) val set_print_constr : (env -> constr -> std_ppcmds) -> unit val print_constr : constr -> std_ppcmds diff --git a/pretyping/typing.ml b/pretyping/typing.ml index be922c7d..78902a7d 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: typing.ml 8673 2006-03-29 21:21:52Z herbelin $ *) +(* $Id: typing.ml 8871 2006-05-28 16:46:48Z herbelin $ *) open Util open Names @@ -88,14 +88,16 @@ let rec execute env evd cstr = judge_of_type u | App (f,args) -> - let j = execute env evd f in let jl = execute_array env evd args in - let (j,_) = judge_of_apply env j jl in + let j = if isInd f then (* Sort-polymorphism of inductive types *) - adjust_inductive_level env evd (destInd f) args j + judge_of_inductive_knowing_parameters env (destInd f) + (jv_nf_evar (evars_of evd) jl) else - j + execute env evd f + in + fst (judge_of_apply env j jl) | Lambda (name,c1,c2) -> let j = execute env evd c1 in @@ -141,25 +143,6 @@ and execute_array env evd = Array.map (execute env evd) and execute_list env evd = List.map (execute env evd) -and adjust_inductive_level env evd ind args j = - let specif = lookup_mind_specif env ind in - if is_small_inductive specif then - (* No polymorphism *) - j - else - (* Retyping constructor with the actual arguments *) - let env',llc,ls0 = constructor_instances env specif ind args in - let llj = Array.map (execute_array env' evd) llc in - let ls = - Array.map (fun lj -> - let ls = - Array.map (fun c -> decomp_sort env (evars_of evd) c.uj_type) lj - in - max_inductive_sort ls) llj - in - let s = find_inductive_level env specif ind ls0 ls in - on_judgment_type (set_inductive_level env s) j - let mcheck env evd c t = let sigma = Evd.evars_of evd in let j = execute env evd (nf_evar sigma c) in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e51f5e0e..e4bde925 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: unification.ml 7113 2005-06-05 17:13:06Z barras $ *) +(* $Id: unification.ml 8759 2006-04-28 12:24:14Z herbelin $ *) open Pp open Util @@ -259,7 +259,7 @@ let w_merge env with_types mod_delta metas evars evd = end and mimick_evar evd mod_delta hdc nargs sp = - let ev = Evd.map (evars_of evd) sp in + let ev = Evd.find (evars_of evd) sp in let sp_env = Global.env_of_context ev.evar_hyps in let (evd', c) = applyHead sp_env evd nargs hdc in let (mc,ec) = -- cgit v1.2.3