diff options
52 files changed, 335 insertions, 305 deletions
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml index dcd0ea469..515d4aa93 100644 --- a/contrib/cc/cctac.ml +++ b/contrib/cc/cctac.ml @@ -228,10 +228,10 @@ let build_projection intype outtype (cstr:constructor) special default gls= let ci=pred (snd cstr) in let branch i= let ti=Term.prod_appvect types.(i) argv in - let rc=fst (Sign.decompose_prod_assum ti) in + let rc=fst (decompose_prod_assum ti) in let head= if i=ci then special else default in - Sign.it_mkLambda_or_LetIn head rc in + it_mkLambda_or_LetIn head rc in let branches=Array.init lp branch in let casee=mkRel 1 in let pred=mkLambda(Anonymous,intype,outtype) in diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index a4d2445ec..f290fea81 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -773,7 +773,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *) let rec decomp_lams_eta_n n env c t = - let rels = fst (decomp_n_prod env none n t) in + let rels = fst (splay_prod_n env none n t) in let rels = List.map (fun (id,_,c) -> (id,c)) rels in let m = nb_lam c in if m >= n then decompose_lam_n n c diff --git a/contrib/firstorder/formula.ml b/contrib/firstorder/formula.ml index ac32f6abe..0be3a4b39 100644 --- a/contrib/firstorder/formula.ml +++ b/contrib/firstorder/formula.ml @@ -57,8 +57,8 @@ let ind_hyps nevar ind largs gls= let lp=Array.length types in let myhyps i= let t1=Term.prod_applist types.(i) largs in - let t2=snd (Sign.decompose_prod_n_assum nevar t1) in - fst (Sign.decompose_prod_assum t2) in + let t2=snd (decompose_prod_n_assum nevar t1) in + fst (decompose_prod_assum t2) in Array.init lp myhyps let special_nf gl= diff --git a/contrib/firstorder/formula.mli b/contrib/firstorder/formula.mli index dca55d0bd..9e9d1e122 100644 --- a/contrib/firstorder/formula.mli +++ b/contrib/firstorder/formula.mli @@ -29,7 +29,7 @@ type counter = bool -> metavariable val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array val ind_hyps : int -> inductive -> constr list -> - Proof_type.goal Tacmach.sigma -> Sign.rel_context array + Proof_type.goal Tacmach.sigma -> rel_context array type atoms = {positive:constr list;negative:constr list} diff --git a/contrib/firstorder/instances.ml b/contrib/firstorder/instances.ml index 56cea8e07..3e087cd8b 100644 --- a/contrib/firstorder/instances.ml +++ b/contrib/firstorder/instances.ml @@ -133,7 +133,7 @@ let mk_open_instance id gl m t= Pretyping.Default.understand evmap env (raux m rawt) with _ -> error "Untypable instance, maybe higher-order non-prenex quantification" in - Sign.decompose_lam_n_assum m ntt + decompose_lam_n_assum m ntt (* tactics *) diff --git a/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml index 6c00e4eac..91607ec40 100644 --- a/contrib/firstorder/rules.ml +++ b/contrib/firstorder/rules.ml @@ -128,7 +128,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl= let vars=Array.init p (fun j->mkRel (p-j)) in let capply=mkApp ((lift p cstr),vars) in let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in - Sign.it_mkLambda_or_LetIn head rc in + it_mkLambda_or_LetIn head rc in let lp=Array.length rcs in let newhyps=list_tabulate myterm lp in tclIFTHENELSE diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 52543cea1..b9b47fde1 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -205,7 +205,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta -let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type = +let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let nochange ?t' msg = begin observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t ); @@ -295,7 +295,7 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type = in let new_type_of_hyp = Reductionops.nf_betaiota new_type_of_hyp in let new_ctxt,new_end_of_type = - Sign.decompose_prod_n_assum ctxt_size new_type_of_hyp + decompose_prod_n_assum ctxt_size new_type_of_hyp in let prove_new_hyp : tactic = tclTHEN @@ -390,7 +390,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in (* length of context didn't change ? *) let new_context,new_typ_of_hyp = - Sign.decompose_prod_n_assum (List.length context) reduced_type_of_hyp + decompose_prod_n_assum (List.length context) reduced_type_of_hyp in tclTHENLIST [ @@ -858,7 +858,7 @@ let build_proof (* Proof of principles from structural functions *) let is_pte_type t = - isSort (snd (decompose_prod t)) + isSort ((strip_prod t)) let is_pte (_,_,t) = is_pte_type t @@ -948,7 +948,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *) let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) - let type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args) + let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args) (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in let lemma_type = it_mkProd_or_LetIn ~init:eqn type_ctxt in @@ -1206,7 +1206,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let intros_after_fixes : tactic = fun gl -> - let ctxt,pte_app = (Sign.decompose_prod_assum (pf_concl gl)) in + let ctxt,pte_app = (decompose_prod_assum (pf_concl gl)) in let pte,pte_args = (decompose_app pte_app) in try let pte = try destVar pte with _ -> anomaly "Property is not a variable" in diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml index 49efe362c..49d1a179b 100644 --- a/contrib/funind/functional_principles_types.ml +++ b/contrib/funind/functional_principles_types.ml @@ -63,7 +63,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let env = Global.env () in let env_with_params = Environ.push_rel_context princ_type_info.params env in let tbl = Hashtbl.create 792 in - let rec change_predicates_names (avoid:identifier list) (predicates:Sign.rel_context) : Sign.rel_context = + let rec change_predicates_names (avoid:identifier list) (predicates:rel_context) : rel_context = match predicates with | [] -> [] |(Name x,v,t)::predicates -> @@ -433,7 +433,7 @@ exception Not_Rec let get_funs_constant mp dp = let rec get_funs_constant const e : (Names.constant*int) array = - match kind_of_term (snd (decompose_lam e)) with + match kind_of_term ((strip_lam e)) with | Fix((_,(na,_,_))) -> Array.mapi (fun i na -> @@ -600,20 +600,20 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types in let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in - let ctxt,fix = Sign.decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*) + let ctxt,fix = decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = destFix fix in let other_result = List.map (* we can now compute the other principles *) (fun scheme_type -> incr i; observe (Printer.pr_lconstr scheme_type); - let type_concl = snd (Sign.decompose_prod_assum scheme_type) in + let type_concl = (strip_prod_assum scheme_type) in let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in let f = fst (decompose_app applied_f) in try (* we search the number of the function in the fix block (name of the function) *) Array.iteri (fun j t -> - let t = snd (Sign.decompose_prod_assum t) in + let t = (strip_prod_assum t) in let applied_g = List.hd (List.rev (snd (decompose_app t))) in let g = fst (decompose_app applied_g) in if eq_constr f g diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index c09c79c18..a78746d29 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -11,7 +11,7 @@ let is_rec_info scheme_info = let test_branche min acc (_,_,br) = acc || ( let new_branche = - Sign.it_mkProd_or_LetIn mkProp (fst (Sign.decompose_prod_assum br)) in + it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum br)) in let free_rels_in_br = Termops.free_rels new_branche in let max = min + scheme_info.Tactics.npredicates in Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index f45efe50b..3e80be65e 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -812,7 +812,7 @@ let rec unify_clauses k pv = let abstract_conclusion typ cs = let n = List.length (assums_of_rel_context cs.cs_args) in let (sign,p) = decompose_prod_n n typ in - lam_it p sign + it_mkLambda p sign let infer_predicate loc env isevars typs cstrs indf = (* Il faudra substituer les isevars a un certain moment *) @@ -1911,7 +1911,7 @@ let build_dependent_signature env evars avoid tomatchs arsign = let previd, id = let name = match kind_of_term arg with - Rel n -> pi1 (lookup_rel n (rel_context env)) + Rel n -> pi1 (lookup_rel n env) | _ -> name in make_prime avoid name diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index 510229ae6..cbfec12df 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -116,7 +116,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let k, ctx', imps, subst = let c = Command.generalize_constr_expr tclass ctx in let c', imps = interp_type_evars_impls ~evdref:isevars env c in - let ctx, c = Sign.decompose_prod_assum c' in + let ctx, c = decompose_prod_assum c' in let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in cl, ctx, imps, (List.rev args) in diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 519626a3a..0af732f85 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -119,7 +119,7 @@ module Coercion = struct and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env isevars x y in let dest_prod c = - match Reductionops.decomp_n_prod env (evars_of !isevars) 1 c with + match Reductionops.splay_prod_n env (evars_of !isevars) 1 c with | [(na,b,t)], c -> (na,t), c | _ -> raise NoSubtacCoercion in @@ -484,7 +484,7 @@ module Coercion = struct | Some (init, cur) -> init, cur in try - let rels, rng = Reductionops.decomp_n_prod env (evars_of isevars) nabs t in + let rels, rng = Reductionops.splay_prod_n env (evars_of isevars) nabs t in (* The final range free variables must have been replaced by evars, we accept only that evars in rng are applied to free vars. *) if noccur_with_meta 1 (succ nabs) rng then ( diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index cc1e2dde2..839597ece 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -226,7 +226,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = doesn't seem to worth the effort (except for huge mutual fixpoints ?) *) let m = Term.nb_prod fixtype in - let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in + let ctx = fst (decompose_prod_n_assum m fixtype) in list_map_i (fun i _ -> i) 0 ctx let reduce_fix = @@ -238,7 +238,7 @@ let declare_mutual_definition l = list_split3 (List.map (fun x -> let subs, typ = (subst_body false x) in - snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l) + (strip_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l) in (* let fixdefs = List.map reduce_fix fixdefs in *) let fixkind = Option.get (List.hd l).prg_fixkind in diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 8201e8fdc..023213ecb 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -144,7 +144,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let s' = mkProd (Anonymous, ind, s) in let ccl = lift 1 (decomp n pj.uj_val) in let ccl' = mkLambda (Anonymous, ind, ccl) in - {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} + {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign} (*************************************************************************) (* Main pretyping function *) diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index d81b98ac4..26b997f0f 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -143,7 +143,7 @@ and slot_for_fv env fv = match !rv with | VKvalue (v, _) -> v | VKnone -> - let (_, b, _) = Sign.lookup_rel i env.env_rel_context in + let (_, b, _) = lookup_rel i env.env_rel_context in let (v, d) = match b with | None -> (val_of_rel i, Idset.empty) diff --git a/kernel/environ.ml b/kernel/environ.ml index 80c24058e..c43b63370 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -41,7 +41,7 @@ let empty_context env = (* Rel context *) let lookup_rel n env = - Sign.lookup_rel n env.env_rel_context + lookup_rel n env.env_rel_context let evaluable_rel n env = try diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f09ba50ec..3452be55c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -215,7 +215,7 @@ let typecheck_inductive env mie = let lev = (* Decide that if the conclusion is not explicitly Type *) (* then the inductive type is not polymorphic *) - match kind_of_term (snd (decompose_prod_assum arity.utj_val)) with + match kind_of_term ((strip_prod_assum arity.utj_val)) with | Sort (Type u) -> Some u | _ -> None in (cst,env_ar',(id,full_arity,lev)::l)) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 118d19830..d09cdbdb7 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -66,7 +66,7 @@ val type_case_branches : -> types array * types * constraints (* Return the arity of an inductive type *) -val mind_arity : one_inductive_body -> Sign.rel_context * sorts_family +val mind_arity : one_inductive_body -> rel_context * sorts_family val inductive_sort_family : one_inductive_body -> sorts_family @@ -85,8 +85,8 @@ val type_of_inductive_knowing_parameters : val max_inductive_sort : sorts array -> universe -val instantiate_universes : env -> Sign.rel_context -> - polymorphic_arity -> types array -> Sign.rel_context * sorts +val instantiate_universes : env -> rel_context -> + polymorphic_arity -> types array -> rel_context * sorts (***************************************************************) (* Debug *) diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 8d45bb9e3..0c0126762 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -103,7 +103,7 @@ let push_named_context_val d (ctxt,vals) = let rval = ref VKnone in Sign.add_named_decl d ctxt, (id,rval)::vals -exception ASSERT of Sign.rel_context +exception ASSERT of rel_context let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); diff --git a/kernel/reduction.ml b/kernel/reduction.ml index e2e1e57d9..3d2f3e9b9 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -471,10 +471,10 @@ let dest_prod env = match kind_of_term t with | Prod (n,a,c0) -> let d = (n,None,a) in - decrec (push_rel d env) (Sign.add_rel_decl d m) c0 + decrec (push_rel d env) (add_rel_decl d m) c0 | _ -> m,t in - decrec env Sign.empty_rel_context + decrec env empty_rel_context (* The same but preserving lets *) let dest_prod_assum env = @@ -483,14 +483,14 @@ let dest_prod_assum env = match kind_of_term rty with | Prod (x,t,c) -> let d = (x,None,t) in - prodec_rec (push_rel d env) (Sign.add_rel_decl d l) c + prodec_rec (push_rel d env) (add_rel_decl d l) c | LetIn (x,b,t,c) -> let d = (x,Some b,t) in - prodec_rec (push_rel d env) (Sign.add_rel_decl d l) c + prodec_rec (push_rel d env) (add_rel_decl d l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> l,rty in - prodec_rec env Sign.empty_rel_context + prodec_rec env empty_rel_context let dest_arity env c = let l, c = dest_prod_assum env c in diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 2e344b217..6ac1591bb 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -70,8 +70,8 @@ val hnf_prod_applist : env -> types -> constr list -> types (************************************************************************) (*s Recognizing products and arities modulo reduction *) -val dest_prod : env -> types -> Sign.rel_context * types -val dest_prod_assum : env -> types -> Sign.rel_context * types +val dest_prod : env -> types -> rel_context * types +val dest_prod_assum : env -> types -> rel_context * types -val dest_arity : env -> types -> Sign.arity +val dest_arity : env -> types -> arity val is_arity : env -> types -> bool diff --git a/kernel/sign.ml b/kernel/sign.ml index 218ac6c48..d30d70860 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -43,31 +43,6 @@ let fold_named_context_reverse f ~init l = List.fold_left f init l (*s Signatures of ordered section variables *) type section_context = named_context -(*s Signatures of ordered optionally named variables, intended to be - accessed by de Bruijn indices (to represent bound variables) *) - -type rel_declaration = name * constr option * types -type rel_context = rel_declaration list - -let empty_rel_context = [] - -let add_rel_decl d ctxt = d::ctxt - -let rec lookup_rel n sign = - match n, sign with - | 1, decl :: _ -> decl - | n, _ :: sign -> lookup_rel (n-1) sign - | _, [] -> raise Not_found - -let rel_context_length = List.length - -let rel_context_nhyps hyps = - let rec nhyps acc = function - | [] -> acc - | (_,None,_)::hyps -> nhyps (1+acc) hyps - | (_,Some _,_)::hyps -> nhyps acc hyps in - nhyps 0 hyps - let fold_rel_context f l ~init:x = List.fold_right f l x let fold_rel_context_reverse f ~init:x l = List.fold_left f x l @@ -102,98 +77,3 @@ let push_named_to_rel_context hyps ctxt = (n+1), (map_rel_declaration (substn_vars n s) d)::ctxt | [] -> 1, hyps in snd (subst ctxt) - - -(*********************************) -(* Term constructors *) -(*********************************) - -let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) -let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) - -(*********************************) -(* Term destructors *) -(*********************************) - -type arity = rel_context * sorts - -(* Decompose an arity (i.e. a product of the form (x1:T1)..(xn:Tn)s - with s a sort) into the pair ([(xn,Tn);...;(x1,T1)],s) *) - -let destArity = - let rec prodec_rec l c = - match kind_of_term c with - | Prod (x,t,c) -> prodec_rec ((x,None,t)::l) c - | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c - | Cast (c,_,_) -> prodec_rec l c - | Sort s -> l,s - | _ -> anomaly "destArity: not an arity" - in - prodec_rec [] - -let mkArity (sign,s) = it_mkProd_or_LetIn (mkSort s) sign - -let rec isArity c = - match kind_of_term c with - | Prod (_,_,c) -> isArity c - | LetIn (_,b,_,c) -> isArity (subst1 b c) - | Cast (c,_,_) -> isArity c - | Sort _ -> true - | _ -> false - -(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair - ([(xn,Tn);...;(x1,T1)],T), where T is not a product *) -let decompose_prod_assum = - let rec prodec_rec l c = - match kind_of_term c with - | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) c - | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c - | Cast (c,_,_) -> prodec_rec l c - | _ -> l,c - in - prodec_rec empty_rel_context - -(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair - ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *) -let decompose_lam_assum = - let rec lamdec_rec l c = - match kind_of_term c with - | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) c - | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) c - | Cast (c,_,_) -> lamdec_rec l c - | _ -> l,c - in - lamdec_rec empty_rel_context - -(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T - into the pair ([(xn,Tn);...;(x1,T1)],T) *) -let decompose_prod_n_assum n = - if n < 0 then - error "decompose_prod_n_assum: integer parameter must be positive"; - let rec prodec_rec l n c = - if n=0 then l,c - else match kind_of_term c with - | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c - | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c - | Cast (c,_,_) -> prodec_rec l n c - | c -> error "decompose_prod_n_assum: not enough assumptions" - in - prodec_rec empty_rel_context n - -(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T - into the pair ([(xn,Tn);...;(x1,T1)],T) - Lets in between are not expanded but turn into local definitions, - but n is the actual number of destructurated lambdas. *) -let decompose_lam_n_assum n = - if n < 0 then - error "decompose_lam_n_assum: integer parameter must be positive"; - let rec lamdec_rec l n c = - if n=0 then l,c - else match kind_of_term c with - | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c - | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) n c - | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_assum: not enough abstractions" - in - lamdec_rec empty_rel_context n - diff --git a/kernel/sign.mli b/kernel/sign.mli index 5d34c5ab4..b3e7ace55 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -40,16 +40,6 @@ val instance_from_named_context : named_context -> constr array (*s Signatures of ordered optionally named variables, intended to be accessed by de Bruijn indices *) -(* In [rel_context], more recent declaration is on top *) -type rel_context = rel_declaration list - -val empty_rel_context : rel_context -val add_rel_decl : rel_declaration -> rel_context -> rel_context - -val lookup_rel : int -> rel_context -> rel_declaration -val rel_context_length : rel_context -> int -val rel_context_nhyps : rel_context -> int - val push_named_to_rel_context : named_context -> rel_context -> rel_context (*s Recurrence on [rel_context]: older declarations processed first *) @@ -70,35 +60,3 @@ val iter_rel_context : (constr -> unit) -> rel_context -> unit (*s Map function of [named_context] *) val iter_named_context : (constr -> unit) -> named_context -> unit - -(*s Term constructors *) - -val it_mkLambda_or_LetIn : constr -> rel_context -> constr -val it_mkProd_or_LetIn : types -> rel_context -> types - -(*s Term destructors *) - -(* Destructs a term of the form $(x_1:T_1)..(x_n:T_n)s$ into the pair *) -type arity = rel_context * sorts -val destArity : types -> arity -val mkArity : arity -> types -val isArity : types -> bool - -(* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ including letins - into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a - product nor a let. *) -val decompose_prod_assum : types -> rel_context * types - -(* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ including letins - into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a - lambda nor a let. *) -val decompose_lam_assum : constr -> rel_context * constr - -(* Given a positive integer n, transforms a product term - $(x_1:T_1)..(x_n:T_n)T$ - into the pair $([(xn,Tn);...;(x1,T1)],T)$. *) -val decompose_prod_n_assum : int -> types -> rel_context * types - -(* Given a positive integer $n$, transforms a lambda term - $[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *) -val decompose_lam_n_assum : int -> constr -> rel_context * constr diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 387d97de9..1f77c3e43 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -115,8 +115,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = | Type _, Type _ -> (* shortcut here *) prop_sort, prop_sort | (Prop _, Type _) | (Type _,Prop _) -> error () | _ -> (s1, s2) in - check_conv cst conv_leq env - (Sign.mkArity (ctx1,s1)) (Sign.mkArity (ctx2,s2)) + check_conv cst conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) in let check_packet cst p1 p2 = @@ -210,8 +209,8 @@ let check_constant cst env msid1 l info1 cb2 spec2 = Hence they don't have to be checked again *) let t1,t2 = - if Sign.isArity t2 then - let (ctx2,s2) = Sign.destArity t2 in + if isArity t2 then + let (ctx2,s2) = destArity t2 in match s2 with | Type v when not (is_univ_variable v) -> (* The type in the interface is inferred and is made of algebraic @@ -222,13 +221,13 @@ let check_constant cst env msid1 l info1 cb2 spec2 = | Type u when not (is_univ_variable u) -> (* Both types are inferred, no need to recheck them. We cheat and collapse the types to Prop *) - Sign.mkArity (ctx1,prop_sort), Sign.mkArity (ctx2,prop_sort) + mkArity (ctx1,prop_sort), mkArity (ctx2,prop_sort) | Prop _ -> (* The type in the interface is inferred, it may be the case that the type in the implementation is smaller because the body is more reduced. We safely collapse the upper type to Prop *) - Sign.mkArity (ctx1,prop_sort), Sign.mkArity (ctx2,prop_sort) + mkArity (ctx1,prop_sort), mkArity (ctx2,prop_sort) | Type _ -> (* The type in the interface is inferred and the type in the implementation is not inferred or is inferred but from a diff --git a/kernel/term.ml b/kernel/term.ml index 49d7afa22..24879f41d 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -654,6 +654,34 @@ let map_rel_declaration = map_named_declaration let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a) let fold_rel_declaration = fold_named_declaration +(***************************************************************************) +(* Type of local contexts (telescopes) *) +(***************************************************************************) + +(*s Signatures of ordered optionally named variables, intended to be + accessed by de Bruijn indices (to represent bound variables) *) + +type rel_context = rel_declaration list + +let empty_rel_context = [] + +let add_rel_decl d ctxt = d::ctxt + +let rec lookup_rel n sign = + match n, sign with + | 1, decl :: _ -> decl + | n, _ :: sign -> lookup_rel (n-1) sign + | _, [] -> raise Not_found + +let rel_context_length = List.length + +let rel_context_nhyps hyps = + let rec nhyps acc = function + | [] -> acc + | (_,None,_)::hyps -> nhyps (1+acc) hyps + | (_,Some _,_)::hyps -> nhyps acc hyps in + nhyps 0 hyps + (****************************************************************************) (* Functions for dealing with constr terms *) (****************************************************************************) @@ -1049,6 +1077,9 @@ let prod_appvect t nL = Array.fold_left prod_app t nL (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *) let prod_applist t nL = List.fold_left prod_app t nL +let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) +let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) + (*********************************) (* Other term destructors *) (*********************************) @@ -1099,6 +1130,62 @@ let decompose_lam_n n = in lamdec_rec [] n +(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair + ([(xn,Tn);...;(x1,T1)],T), where T is not a product *) +let decompose_prod_assum = + let rec prodec_rec l c = + match kind_of_term c with + | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) c + | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c + | Cast (c,_,_) -> prodec_rec l c + | _ -> l,c + in + prodec_rec empty_rel_context + +(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair + ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *) +let decompose_lam_assum = + let rec lamdec_rec l c = + match kind_of_term c with + | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) c + | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) c + | Cast (c,_,_) -> lamdec_rec l c + | _ -> l,c + in + lamdec_rec empty_rel_context + +(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T + into the pair ([(xn,Tn);...;(x1,T1)],T) *) +let decompose_prod_n_assum n = + if n < 0 then + error "decompose_prod_n_assum: integer parameter must be positive"; + let rec prodec_rec l n c = + if n=0 then l,c + else match kind_of_term c with + | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c + | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c + | Cast (c,_,_) -> prodec_rec l n c + | c -> error "decompose_prod_n_assum: not enough assumptions" + in + prodec_rec empty_rel_context n + +(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T + into the pair ([(xn,Tn);...;(x1,T1)],T) + Lets in between are not expanded but turn into local definitions, + but n is the actual number of destructurated lambdas. *) +let decompose_lam_n_assum n = + if n < 0 then + error "decompose_lam_n_assum: integer parameter must be positive"; + let rec lamdec_rec l n c = + if n=0 then l,c + else match kind_of_term c with + | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) n c + | Cast (c,_,_) -> lamdec_rec l n c + | c -> error "decompose_lam_n_assum: not enough abstractions" + in + lamdec_rec empty_rel_context n + (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction * gives n (casts are ignored) *) let nb_lam = @@ -1118,7 +1205,47 @@ let nb_prod = in nbrec 0 -(* Rem: end of import from old module Generic *) +let prod_assum t = fst (decompose_prod_assum t) +let prod_n_assum n t = fst (decompose_prod_n_assum n t) +let strip_prod_assum t = snd (decompose_prod_assum t) +let strip_prod t = snd (decompose_prod t) +let strip_prod_n n t = snd (decompose_prod_n n t) +let lam_assum t = fst (decompose_lam_assum t) +let lam_n_assum n t = fst (decompose_lam_n_assum n t) +let strip_lam_assum t = snd (decompose_lam_assum t) +let strip_lam t = snd (decompose_lam t) +let strip_lam_n n t = snd (decompose_lam_n n t) + +(***************************) +(* Arities *) +(***************************) + +(* An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort. + Such a term can canonically be seen as the pair of a context of types + and of a sort *) + +type arity = rel_context * sorts + +let destArity = + let rec prodec_rec l c = + match kind_of_term c with + | Prod (x,t,c) -> prodec_rec ((x,None,t)::l) c + | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c + | Cast (c,_,_) -> prodec_rec l c + | Sort s -> l,s + | _ -> anomaly "destArity: not an arity" + in + prodec_rec [] + +let mkArity (sign,s) = it_mkProd_or_LetIn (mkSort s) sign + +let rec isArity c = + match kind_of_term c with + | Prod (_,_,c) -> isArity c + | LetIn (_,b,_,c) -> isArity (subst1 b c) + | Cast (c,_,_) -> isArity c + | Sort _ -> true + | _ -> false (*******************************) (* alpha conversion functions *) diff --git a/kernel/term.mli b/kernel/term.mli index 5d75df4bf..6a6a4ad28 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -331,6 +331,18 @@ val fold_named_declaration : val fold_rel_declaration : (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a +(*s Contexts of declarations referred to by de Bruijn indices *) + +(* In [rel_context], more recent declaration is on top *) +type rel_context = rel_declaration list + +val empty_rel_context : rel_context +val add_rel_decl : rel_declaration -> rel_context -> rel_context + +val lookup_rel : int -> rel_context -> rel_declaration +val rel_context_length : rel_context -> int +val rel_context_nhyps : rel_context -> int + (* Constructs either [(x:t)c] or [[x=b:t]c] *) val mkProd_or_LetIn : rel_declaration -> types -> types val mkNamedProd_or_LetIn : named_declaration -> types -> types @@ -368,7 +380,7 @@ val lamn : int -> (name * constr) list -> constr -> constr (* [compose_lam l b] = $[x_1:T_1]..[x_n:T_n]b$ where $l = [(x_n,T_n);\dots;(x_1,T_1)]$. - Inverse of [decompose_lam] *) + Inverse of [it_destLam] *) val compose_lam : (name * constr) list -> constr -> constr (* [to_lambda n l] @@ -387,6 +399,9 @@ val to_prod : int -> constr -> constr val prod_appvect : constr -> constr array -> constr val prod_applist : constr -> constr list -> constr +val it_mkLambda_or_LetIn : constr -> rel_context -> constr +val it_mkProd_or_LetIn : types -> rel_context -> types + (*s Other term destructors. *) (* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ into the pair @@ -407,13 +422,44 @@ val decompose_prod_n : int -> constr -> (name * constr) list * constr $[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *) val decompose_lam_n : int -> constr -> (name * constr) list * constr +(* Extract the premisses and the conclusion of a term of the form + "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *) +val decompose_prod_assum : types -> rel_context * types + +(* Idem with lambda's *) +val decompose_lam_assum : constr -> rel_context * constr + +(* Idem but extract the first [n] premisses *) +val decompose_prod_n_assum : int -> types -> rel_context * types +val decompose_lam_n_assum : int -> constr -> rel_context * constr + (* [nb_lam] $[x_1:T_1]...[x_n:T_n]c$ where $c$ is not an abstraction gives $n$ (casts are ignored) *) val nb_lam : constr -> int -(* similar to [nb_lam], but gives the number of products instead *) +(* Similar to [nb_lam], but gives the number of products instead *) val nb_prod : constr -> int +(* Returns the premisses/parameters of a type/term (let-in included) *) +val prod_assum : types -> rel_context +val lam_assum : constr -> rel_context + +(* Returns the first n-th premisses/parameters of a type/term (let included)*) +val prod_n_assum : int -> types -> rel_context +val lam_n_assum : int -> constr -> rel_context + +(* Remove the premisses/parameters of a type/term *) +val strip_prod : types -> types +val strip_lam : constr -> constr + +(* Remove the first n-th premisses/parameters of a type/term *) +val strip_prod_n : int -> types -> types +val strip_lam_n : int -> constr -> constr + +(* Remove the premisses/parameters of a type/term (including let-in) *) +val strip_prod_assum : types -> types +val strip_lam_assum : constr -> constr + (* flattens application lists *) val collapse_appl : constr -> constr @@ -428,6 +474,21 @@ val under_casts : (constr -> constr) -> constr -> constr (* Apply a function under components of Cast if any *) val under_outer_cast : (constr -> constr) -> constr -> constr +(*s An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort. + Such a term can canonically be seen as the pair of a context of types + and of a sort *) + +type arity = rel_context * sorts + +(* Build an "arity" from its canonical form *) +val mkArity : arity -> types + +(* Destructs an "arity" into its canonical form *) +val destArity : types -> arity + +(* Tells if a term has the form of an arity *) +val isArity : types -> bool + (*s Occur checks *) (* [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 5bb0dee1d..23c755690 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -25,7 +25,7 @@ val infer_type : env -> types -> unsafe_type_judgment * constraints val infer_local_decls : env -> (identifier * local_entry) list - -> env * Sign.rel_context * constraints + -> env * rel_context * constraints (*s Basic operations of the typing machine. *) diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 3163cfb71..d24f2dd6f 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -105,7 +105,7 @@ let print_argument_scopes = function let need_expansion impl ref = let typ = Global.type_of_global ref in - let ctx = fst (decompose_prod_assum typ) in + let ctx = (prod_assum typ) in let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in impl <> [] & let _,lastimpl = list_chop nprods impl in List.filter is_status_implicit lastimpl <> [] diff --git a/pretyping/cases.ml b/pretyping/cases.ml index a4d0b25ce..00df4c87a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1425,10 +1425,10 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t = match b with | Some c -> assert (isRel c); - let p = n + destRel c in aux p (lookup_rel p (rel_context extenv)) + let p = n + destRel c in aux p (lookup_rel p extenv) | None -> (n,ty) in - let (p,ty) = aux p (lookup_rel p (rel_context extenv)) in + let (p,ty) = aux p (lookup_rel p extenv) in if noccur_between_without_evar 1 (n'-p-n+1) ty then let u = lift (n'-n) u in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d161ce612..8fe807f2e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -370,7 +370,7 @@ let set_pattern_names env ind brv = let arities = Array.map (fun c -> - rel_context_length (fst (decompose_prod_assum c)) - + rel_context_length ((prod_assum c)) - mib.mind_nparams) mip.mind_nf_lc in array_map2 (set_names env) arities brv diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 7e7b49d26..5d416cede 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -75,7 +75,7 @@ type constructor_summary = { cs_cstr : constructor; cs_params : constr list; cs_nargs : int; - cs_args : Sign.rel_context; + cs_args : rel_context; cs_concl_realargs : constr array; } val lift_constructor : int -> constructor_summary -> constructor_summary @@ -86,7 +86,7 @@ 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 -> 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/pretyping.ml b/pretyping/pretyping.ml index 7fe358e32..35c5d376b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -264,7 +264,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let s' = mkProd (Anonymous, ind, s) in let ccl = lift 1 (decomp n pj.uj_val) in let ccl' = mkLambda (Anonymous, ind, ccl) in - {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} + {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign} let evar_kind_of_term sigma c = kind_of_term (whd_evar (Evd.evars_of sigma) c) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 99f439224..e8860c065 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -163,7 +163,7 @@ let cs_pattern_of_constr t = let compute_canonical_projections (con,ind) = let v = mkConst con in let c = Environ.constant_value (Global.env()) con in - let lt,t = Reductionops.splay_lambda (Global.env()) Evd.empty c in + let lt,t = Reductionops.splay_lam (Global.env()) Evd.empty c in let lt = List.rev (List.map snd lt) in let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = @@ -234,7 +234,7 @@ let check_and_decompose_canonical_structure ref = let vc = match Environ.constant_opt_value env sp with | Some vc -> vc | None -> error_not_structure ref in - let body = snd (splay_lambda (Global.env()) Evd.empty vc) in + let body = snd (splay_lam (Global.env()) Evd.empty vc) in let f,args = match kind_of_term body with | App (f,args) -> f,args | _ -> error_not_structure ref in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 4bb9a9a5d..f51820bf6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -750,7 +750,7 @@ let splay_prod env sigma = in decrec env [] -let splay_lambda env sigma = +let splay_lam env sigma = let rec decrec env m c = let t = whd_betadeltaiota env sigma c in match kind_of_term t with @@ -767,14 +767,14 @@ let splay_prod_assum env sigma = match kind_of_term t with | Prod (x,t,c) -> prodec_rec (push_rel (x,None,t) env) - (Sign.add_rel_decl (x, None, t) l) c + (add_rel_decl (x, None, t) l) c | LetIn (x,b,t,c) -> prodec_rec (push_rel (x, Some b, t) env) - (Sign.add_rel_decl (x, Some b, t) l) c + (add_rel_decl (x, Some b, t) l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> l,t in - prodec_rec env Sign.empty_rel_context + prodec_rec env empty_rel_context let splay_arity env sigma c = let l, c = splay_prod env sigma c in @@ -784,15 +784,25 @@ let splay_arity env sigma c = let sort_of_arity env c = snd (splay_arity env Evd.empty c) -let decomp_n_prod env sigma n = +let splay_prod_n env sigma n = let rec decrec env m ln c = if m = 0 then (ln,c) else match kind_of_term (whd_betadeltaiota env sigma c) with | Prod (n,a,c0) -> decrec (push_rel (n,None,a) env) - (m-1) (Sign.add_rel_decl (n,None,a) ln) c0 - | _ -> invalid_arg "decomp_n_prod" + (m-1) (add_rel_decl (n,None,a) ln) c0 + | _ -> invalid_arg "splay_prod_n" in - decrec env n Sign.empty_rel_context + decrec env n empty_rel_context + +let splay_lam_n env sigma n = + let rec decrec env m ln c = if m = 0 then (ln,c) else + match kind_of_term (whd_betadeltaiota env sigma c) with + | Lambda (n,a,c0) -> + decrec (push_rel (n,None,a) env) + (m-1) (add_rel_decl (n,None,a) ln) c0 + | _ -> invalid_arg "splay_lam_n" + in + decrec env n empty_rel_context exception NotASort diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 371a66a9d..edbb4f90c 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -156,13 +156,13 @@ val hnf_lam_appvect : env -> evar_map -> constr -> constr array -> constr val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr val splay_prod : env -> evar_map -> constr -> (name * constr) list * constr -val splay_lambda : env -> evar_map -> constr -> (name * constr) list * constr +val splay_lam : env -> evar_map -> constr -> (name * constr) list * constr val splay_arity : env -> evar_map -> constr -> (name * constr) list * sorts val sort_of_arity : env -> constr -> sorts -val decomp_n_prod : - env -> evar_map -> int -> constr -> Sign.rel_context * constr +val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr +val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_prod_assum : - env -> evar_map -> constr -> Sign.rel_context * constr + env -> evar_map -> constr -> rel_context * constr val decomp_sort : env -> evar_map -> types -> sorts val is_sort : env -> evar_map -> types -> bool diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 418bb5d2f..2c2bddb45 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -674,7 +674,7 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = with Redelimination -> match reference_opt_value sigma env ref with | Some c -> - (match kind_of_term (snd (decompose_lam c)) with + (match kind_of_term ((strip_lam c)) with | CoFix _ | Fix _ -> s | _ -> redrec (c, stack)) | None -> s) @@ -692,7 +692,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c = if isEvalRef env constr then match reference_opt_value sigma env (destEvalRef constr) with | Some c -> - (match kind_of_term (snd (decompose_lam c)) with + (match kind_of_term ((strip_lam c)) with | CoFix _ | Fix _ -> s' | _ -> redrec (c, stack)) | None -> s' diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 24ab23f4a..987db88b1 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -180,12 +180,6 @@ let new_sort_in_family = function -(* prod_it b [xn:Tn;..;x1:T1] = (x1:T1)..(xn:Tn)b *) -let prod_it ~init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init - -(* lam_it b [xn:Tn;..;x1:T1] = [x1:T1]..[xn:Tn]b *) -let lam_it ~init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init - (* [Rel (n+m);...;Rel(n+1)] *) let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) @@ -232,34 +226,30 @@ let rec lookup_rel_id id sign = in lookrec (1,sign) -(* Constructs either [(x:t)c] or [[x=b:t]c] *) +(* Constructs either [forall x:t, c] or [let x:=b:t in c] *) let mkProd_or_LetIn (na,body,t) c = match body with | None -> mkProd (na, t, c) | Some b -> mkLetIn (na, b, t, c) -(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *) +(* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *) let mkProd_wo_LetIn (na,body,t) c = match body with | None -> mkProd (na, t, c) | Some b -> subst1 b c -let it_mkProd_wo_LetIn ~init = - List.fold_left (fun c d -> mkProd_wo_LetIn d c) init - -let it_mkProd_or_LetIn ~init = - List.fold_left (fun c d -> mkProd_or_LetIn d c) init - -let it_mkLambda_or_LetIn ~init = - List.fold_left (fun c d -> mkLambda_or_LetIn d c) init +let it_mkProd ~init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init +let it_mkLambda ~init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init let it_named_context_quantifier f ~init = List.fold_left (fun c d -> f d c) init +let it_mkProd_or_LetIn = it_named_context_quantifier mkProd_or_LetIn +let it_mkProd_wo_LetIn = it_named_context_quantifier mkProd_wo_LetIn +let it_mkLambda_or_LetIn = it_named_context_quantifier mkLambda_or_LetIn let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn -let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn - let it_mkNamedProd_wo_LetIn = it_named_context_quantifier mkNamedProd_wo_LetIn +let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn (* *) @@ -794,9 +784,9 @@ let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b let it_mkProd_or_LetIn_name env b hyps = - it_mkProd_or_LetIn b (name_context env hyps) + it_mkProd_or_LetIn ~init:b (name_context env hyps) let it_mkLambda_or_LetIn_name env b hyps = - it_mkLambda_or_LetIn b (name_context env hyps) + it_mkLambda_or_LetIn ~init:b (name_context env hyps) (*************************) (* Names environments *) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index ccdb98031..9163a1d9e 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -35,27 +35,32 @@ val pr_rel_decl : env -> rel_declaration -> std_ppcmds val print_rel_context : env -> std_ppcmds val print_env : env -> std_ppcmds -(* iterators on terms *) -val prod_it : init:types -> (name * types) list -> types -val lam_it : init:constr -> (name * types) list -> constr -val rel_vect : int -> int -> constr array -val rel_list : int -> int -> constr list -val extended_rel_list : int -> rel_context -> constr list -val extended_rel_vect : int -> rel_context -> constr array +(* about contexts *) val push_rel_assum : name * types -> env -> env val push_rels_assum : (name * types) list -> env -> env val push_named_rec_types : name array * types array * 'a -> env -> env val lookup_rel_id : identifier -> rel_context -> int * types + +(* builds argument lists matching a block of binders or a context *) +val rel_vect : int -> int -> constr array +val rel_list : int -> int -> constr list +val extended_rel_list : int -> rel_context -> constr list +val extended_rel_vect : int -> rel_context -> constr array + +(* iterators/destructors on terms *) val mkProd_or_LetIn : rel_declaration -> types -> types val mkProd_wo_LetIn : rel_declaration -> types -> types -val it_mkProd_wo_LetIn : init:types -> rel_context -> types +val it_mkProd : init:types -> (name * types) list -> types +val it_mkLambda : init:constr -> (name * types) list -> constr val it_mkProd_or_LetIn : init:types -> rel_context -> types +val it_mkProd_wo_LetIn : init:types -> rel_context -> types val it_mkLambda_or_LetIn : init:constr -> rel_context -> constr -val it_named_context_quantifier : - (named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a val it_mkNamedProd_or_LetIn : init:types -> named_context -> types -val it_mkNamedLambda_or_LetIn : init:constr -> named_context -> constr val it_mkNamedProd_wo_LetIn : init:types -> named_context -> types +val it_mkNamedLambda_or_LetIn : init:constr -> named_context -> constr + +val it_named_context_quantifier : + (named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a (**********************************************************************) (* Generic iterators on constr *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f7762afbe..80d7d34a9 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -43,7 +43,7 @@ let abstract_scheme env c l lname_typ = lname_typ let abstract_list_all env evd typ c l = - let ctxt,_ = decomp_n_prod env (evars_of evd) (List.length l) typ in + let ctxt,_ = splay_prod_n env (evars_of evd) (List.length l) typ in let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in let p = abstract_scheme env c l_with_all_occs ctxt in try diff --git a/tactics/auto.ml b/tactics/auto.ml index ec3a8d6c9..36e8add7e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1081,7 +1081,7 @@ let compileAutoArg contac = function tclFIRST (List.map (fun (id,_,typ) -> - let cl = snd (decompose_prod typ) in + let cl = (strip_prod_assum typ) in if Hipattern.is_conjunction cl then tclTHENSEQ [simplest_elim (mkVar id); clear [id]; contac] diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index b556676ee..b6272115a 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -888,7 +888,7 @@ let unfold_all t = | _ -> assert false let decomp_prod env evm n c = - snd (Reductionops.decomp_n_prod env evm n c) + snd (Reductionops.splay_prod_n env evm n c) let rec decomp_pointwise n c = if n = 0 then c @@ -1402,7 +1402,7 @@ open Entries open Libnames let respect_projection r ty = - let ctx, inst = Sign.decompose_prod_assum ty in + let ctx, inst = decompose_prod_assum ty in let mor, args = destApp inst in let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in let app = mkApp (Lazy.force respect_proj, @@ -1414,7 +1414,7 @@ let declare_projection n instance_id r = let c = constr_of_global r in let term = respect_projection c ty in let typ = Typing.type_of (Global.env ()) Evd.empty term in - let ctx, typ = Sign.decompose_prod_assum typ in + let ctx, typ = decompose_prod_assum typ in let typ = let n = let rec aux t = @@ -1430,7 +1430,7 @@ let declare_projection n instance_id r = | _ -> typ in aux init in - let ctx,ccl = Reductionops.decomp_n_prod (Global.env()) Evd.empty (3 * n) typ + let ctx,ccl = Reductionops.splay_prod_n (Global.env()) Evd.empty (3 * n) typ in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in @@ -1799,7 +1799,7 @@ let setoid_transitivity c gl = *) let setoid_symmetry_in id gl = let ctype = pf_type_of gl (mkVar id) in - let binders,concl = Sign.decompose_prod_assum ctype in + let binders,concl = decompose_prod_assum ctype in let (equiv, args) = decompose_app concl in let rec split_last_two = function | [c1;c2] -> [],(c1, c2) diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 741874cb3..7e25b072e 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -1265,7 +1265,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let gen_arities = Inductive.arities_of_constructors ind spec in let f_ids typ = let sign = - fst (Sign.decompose_prod_assum (Term.prod_applist typ params)) in + (prod_assum (Term.prod_applist typ params)) in find_intro_names sign gls in let constr_args_ids = Array.map f_ids gen_arities in let case_term = diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 9fb4becda..5f7405c93 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -94,7 +94,7 @@ let match_with_one_constructor style t = then if style = Some true (* strict conjunction *) then let ctx = - fst (decompose_prod_assum (snd + (prod_assum (snd (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))) in if List.for_all @@ -104,7 +104,7 @@ let match_with_one_constructor style t = else None else let ctyp = prod_applist mip.mind_nf_lc.(0) args in - let cargs = List.map pi3 (fst (decompose_prod_assum ctyp)) in + let cargs = List.map pi3 ((prod_assum ctyp)) in if style <> Some false || has_nodep_prod ctyp then (* Record or non strict conjunction *) Some (hdapp,List.rev cargs) @@ -134,7 +134,7 @@ let is_record t = let test_strict_disjunction n lc = array_for_all_i (fun i c -> - match fst (decompose_prod_assum (snd (decompose_prod_n_assum n c))) with + match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> c = mkRel (n - i) | _ -> false) 0 lc diff --git a/tactics/inv.ml b/tactics/inv.ml index b6923bb83..46ce6e20b 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -127,7 +127,7 @@ let make_inv_predicate env sigma indf realargs id status concl = push <Ai>(mkRel k)=ai (when Ai is closed). In any case, we carry along the rest of pairs *) let rec build_concl eqns n = function - | [] -> (prod_it concl eqns,n) + | [] -> (it_mkProd concl eqns,n) | (ai,(xi,ti))::restlist -> let (lhs,eqnty,rhs) = if closed0 ti then diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index f74d6dfdf..fcb1d2bb5 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -967,7 +967,7 @@ let check_a env a = let check_eq env a_quantifiers_rev a aeq = let typ = - Sign.it_mkProd_or_LetIn + it_mkProd_or_LetIn (mkApp ((Lazy.force coq_relation),[| apply_to_rels a a_quantifiers_rev |])) a_quantifiers_rev in if @@ -981,7 +981,7 @@ let check_property env a_quantifiers_rev a aeq strprop coq_prop t = if not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) - (Sign.it_mkProd_or_LetIn + (it_mkProd_or_LetIn (mkApp ((Lazy.force coq_prop), [| apply_to_rels a a_quantifiers_rev ; apply_to_rels aeq a_quantifiers_rev |])) a_quantifiers_rev)) @@ -1002,7 +1002,7 @@ let check_setoid_theory env a_quantifiers_rev a aeq th = if not (is_conv env Evd.empty (Typing.type_of env Evd.empty th) - (Sign.it_mkProd_or_LetIn + (it_mkProd_or_LetIn (mkApp ((Lazy.force coq_Setoid_Theory), [| apply_to_rels a a_quantifiers_rev ; apply_to_rels aeq a_quantifiers_rev |])) a_quantifiers_rev)) @@ -1039,7 +1039,7 @@ let int_add_relation id a aeq refl sym trans = Declare.declare_internal_constant id (DefinitionEntry {const_entry_body = - Sign.it_mkLambda_or_LetIn x_relation_class + it_mkLambda_or_LetIn x_relation_class ([ Name (id_of_string "v"),None,mkRel 1; Name (id_of_string "X"),None,mkType (Termops.new_univ ())] @ a_quantifiers_rev); @@ -1059,7 +1059,7 @@ let int_add_relation id a aeq refl sym trans = Declare.declare_internal_constant id_precise (DefinitionEntry {const_entry_body = - Sign.it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev; + it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev; const_entry_type = None; const_entry_opaque = false; const_entry_boxed = Flags.boxed_definitions() }, @@ -1119,7 +1119,7 @@ let int_add_relation id a aeq refl sym trans = let _ = Declare.declare_internal_constant mor_name (DefinitionEntry - {const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev; + {const_entry_body = it_mkLambda_or_LetIn lemma a_quantifiers_rev; const_entry_type = None; const_entry_opaque = false; const_entry_boxed = Flags.boxed_definitions()}, @@ -1153,15 +1153,15 @@ let add_setoid id a aeq th = let aeq_instance = apply_to_rels aeq a_quantifiers_rev in let th_instance = apply_to_rels th a_quantifiers_rev in let refl = - Sign.it_mkLambda_or_LetIn + it_mkLambda_or_LetIn (mkApp ((Lazy.force coq_seq_refl), [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in let sym = - Sign.it_mkLambda_or_LetIn + it_mkLambda_or_LetIn (mkApp ((Lazy.force coq_seq_sym), [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in let trans = - Sign.it_mkLambda_or_LetIn + it_mkLambda_or_LetIn (mkApp ((Lazy.force coq_seq_trans), [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in int_add_relation id a aeq (Some refl) (Some sym) (Some trans) @@ -1976,7 +1976,7 @@ let setoid_replace_in tac_opt id relation c1 c2 ~new_goals gl = (* let setoid_symmetry_in id gl = *) (* let ctype = pf_type_of gl (mkVar id) in *) -(* let binders,concl = Sign.decompose_prod_assum ctype in *) +(* let binders,concl = decompose_prod_assum ctype in *) (* let (equiv, args) = decompose_app concl in *) (* let rec split_last_two = function *) (* | [c1;c2] -> [],(c1, c2) *) @@ -2009,7 +2009,7 @@ let setoid_replace_in tac_opt id relation c1 c2 ~new_goals gl = (* | Some trans -> *) (* let transty = nf_betaiota (pf_type_of gl trans) in *) (* let argsrev, _ = *) -(* Reductionops.decomp_n_prod (pf_env gl) Evd.empty 2 transty in *) +(* Reductionops.splay_prod_n (pf_env gl) Evd.empty 2 transty in *) (* let binder = *) (* match List.rev argsrev with *) (* _::(Name n2,None,_)::_ -> Rawterm.NamedHyp n2 *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 44f07d37b..c8d078aee 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -709,7 +709,7 @@ let simplest_case c = general_case_analysis false (c,NoBindings) let descend_in_conjunctions with_evars tac exit c gl = try let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in - match match_with_conjunction (snd (decompose_prod t)) with + match match_with_conjunction ((strip_prod t)) with | Some _ -> let n = (mis_constr_nargs mind).(0) in let sort = elimination_sort_of_goal gl in @@ -1236,7 +1236,7 @@ let ipat_of_name = function let allow_replace c gl = function (* A rather arbitrary condition... *) | Some (_, IntroIdentifier id) -> - fst (decompose_app (snd (decompose_lam_assum c))) = mkVar id + fst (decompose_app ((strip_lam_assum c))) = mkVar id | _ -> false @@ -2086,7 +2086,7 @@ let abstract_args gl id = *) let aux (prod, ctx, ctxenv, c, args, eqs, refls, vars, env) arg = let (name, _, ty), arity = - let rel, c = Reductionops.decomp_n_prod env sigma 1 prod in + let rel, c = Reductionops.splay_prod_n env sigma 1 prod in List.hd rel, c in let argty = pf_type_of gl arg in @@ -2224,7 +2224,7 @@ let decompose_paramspred_branch_args elimt = let rec cut_noccur elimt acc2 : rel_context * rel_context * types = match kind_of_term elimt with | Prod(nme,tpe,elimt') -> - let hd_tpe,_ = decompose_app (snd (decompose_prod_assum tpe)) in + let hd_tpe,_ = decompose_app ((strip_prod_assum tpe)) in if not (occur_rel 1 elimt') && isRel hd_tpe then cut_noccur elimt' ((nme,None,tpe)::acc2) else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl @@ -2455,7 +2455,7 @@ let find_elim_signature isrec elim hyp0 gl = let elimt = pf_type_of gl elimc in ((elimc, NoBindings), elimt), mkInd mind | Some (elimc,lbind as e) -> - let ind_type_guess,_ = decompose_app (snd (decompose_prod tmptyp0)) in + let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in (e, pf_type_of gl elimc), ind_type_guess in let indsign,elim_scheme = compute_elim_signature elimc elimt hyp0 ind in @@ -2599,7 +2599,7 @@ let induction_from_context isrec with_evars elim_info (hyp0,lbind) names let tmptyp0 = pf_get_hyp_typ gl hyp0 in let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in let indvars = - find_atomic_param_of_ind scheme.nparams (snd (decompose_prod typ0)) in + find_atomic_param_of_ind scheme.nparams ((strip_prod typ0)) in let induct_tac = tclTHENLIST [ induction_tac with_evars (hyp0,lbind) typ0 scheme; tclTRY (unfold_body hyp0); diff --git a/toplevel/class.ml b/toplevel/class.ml index f577355d3..d2d399f10 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -199,7 +199,7 @@ let build_id_coercion idf_opt source = let c = match constant_opt_value env (destConst vs) with | Some c -> c | None -> error_not_transparent source in - let lams,t = Sign.decompose_lam_assum c in + let lams,t = decompose_lam_assum c in let val_f = it_mkLambda_or_LetIn (mkLambda (Name (id_of_string "x"), diff --git a/toplevel/command.ml b/toplevel/command.ml index 47c51b83f..07f501956 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -355,7 +355,7 @@ let adjust_guardness_conditions const = | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> let possible_indexes = List.map (fun c -> - interval 0 (List.length (fst (Sign.decompose_lam_assum c)))) + interval 0 (List.length ((lam_assum c)))) (Array.to_list fixdefs) in let indexes = search_guard dummy_loc (Global.env()) possible_indexes fixdecls in { const with const_entry_body = mkFix ((indexes,0),fixdecls) } @@ -1125,7 +1125,7 @@ let look_for_mutual_statements thms = (* common coinductive conclusion *) let n = List.length thms in let inds = List.map (fun (id,(t,_) as x) -> - let (hyps,ccl) = Sign.decompose_prod_assum t in + let (hyps,ccl) = decompose_prod_assum t in let whnf_hyp_hds = map_rel_context_with_binders (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c))) hyps in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 1bc4e4f33..52581a15d 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -92,7 +92,7 @@ let explain_elim_arity env ind sorts c pj okinds = | WrongArity -> "wrong arity" in let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in - let ppt = pr_lconstr_env env (snd (decompose_prod_assum pj.uj_type)) in + let ppt = pr_lconstr_env env ((strip_prod_assum pj.uj_type)) in hov 0 (str "the return type has sort" ++ spc () ++ ppt ++ spc () ++ str "while it" ++ spc () ++ str "should be " ++ ppar ++ str ".") ++ diff --git a/toplevel/record.ml b/toplevel/record.ml index 79d34e878..9978d7bf6 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -269,7 +269,7 @@ let set_rigid c = let declare_instance_cst glob con = let instance = Typeops.type_of_constant (Global.env ()) con in - let _, r = Sign.decompose_prod_assum instance in + let _, r = decompose_prod_assum instance in match class_of_constr r with | Some tc -> add_instance (new_instance tc None glob con) | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.") diff --git a/toplevel/record.mli b/toplevel/record.mli index b74c1a4af..3fe18e192 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -29,7 +29,7 @@ val declare_projections : val declare_structure : bool (*coinductive?*)-> identifier -> identifier -> manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *) - Impargs.manual_explicitation list list -> Sign.rel_context -> (* fields *) + Impargs.manual_explicitation list list -> rel_context -> (* fields *) ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool -> (* coercion? *) bool list -> (* field coercions *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 465c55a4b..a4d3e5458 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -119,7 +119,7 @@ let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) () let show_intro all = let pf = get_pftreestate() in let gl = nth_goal_of_pftreestate 1 pf in - let l,_= Sign.decompose_prod_assum (strip_outer_cast (pf_concl gl)) in + let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in |