diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 136 |
1 files changed, 22 insertions, 114 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 066df12096..c8cbf31a62 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -18,126 +18,36 @@ open Declarations open Environ open Reductionops -(* -type inductive_instance = { - mis_sp : section_path; - mis_mib : mutual_inductive_body; - mis_tyi : int; - mis_mip : one_inductive_body } - - -let build_mis (sp,tyi) mib = - { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; - mis_mip = mind_nth_type_packet mib tyi } - -let mis_ntypes mis = mis.mis_mib.mind_ntypes -let mis_nparams mis = mis.mis_mip.mind_nparams - -let mis_index mis = mis.mis_tyi - -let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames) -let mis_nrealargs mis = mis.mis_mip.mind_nrealargs -let mis_kelim mis = mis.mis_mip.mind_kelim -let mis_recargs mis = - Array.map (fun mip -> mip.mind_listrec) mis.mis_mib.mind_packets -let mis_recarg mis = mis.mis_mip.mind_listrec -let mis_typename mis = mis.mis_mip.mind_typename -let mis_typepath mis = - make_path (dirpath mis.mis_sp) mis.mis_mip.mind_typename CCI -let mis_consnames mis = mis.mis_mip.mind_consnames -let mis_conspaths mis = - let dir = dirpath mis.mis_sp in - Array.map (fun id -> make_path dir id CCI) mis.mis_mip.mind_consnames -let mis_inductive mis = (mis.mis_sp,mis.mis_tyi) -let mis_finite mis = mis.mis_mip.mind_finite - -let mis_typed_nf_lc mis = - let sign = mis.mis_mib.mind_hyps in - mis.mis_mip.mind_nf_lc - -let mis_nf_lc mis = Array.map body_of_type (mis_typed_nf_lc mis) - -let mis_user_lc mis = - let sign = mis.mis_mib.mind_hyps in - (mind_user_lc mis.mis_mip) - -(* gives the vector of constructors and of - types of constructors of an inductive definition - correctly instanciated *) - -let mis_type_mconstructs mispec = - let specif = Array.map body_of_type (mis_user_lc mispec) - and ntypes = mis_ntypes mispec - and nconstr = mis_nconstr mispec in - let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) - and make_Ck k = - mkMutConstruct ((mispec.mis_sp,mispec.mis_tyi),k+1) in - (Array.init nconstr make_Ck, - Array.map (substl (list_tabulate make_Ik ntypes)) specif) -*) -let mis_nf_constructor_type (ind,mib,mip) j = - let specif = mip.mind_nf_lc - and ntypes = mib.mind_ntypes - and nconstr = Array.length mip.mind_consnames in - let make_Ik k = mkInd ((fst ind),ntypes-k-1) in - if j > nconstr then error "Not enough constructors in the type"; - substl (list_tabulate make_Ik ntypes) specif.(j-1) -(* -let mis_constructor_type i mispec = - let specif = mis_user_lc mispec - and ntypes = mis_ntypes mispec - and nconstr = mis_nconstr mispec in - let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) in - if i > nconstr then error "Not enough constructors in the type"; - substl (list_tabulate make_Ik ntypes) specif.(i-1) - -let mis_arity mis = - let hyps = mis.mis_mib.mind_hyps in - mind_user_arity mis.mis_mip - -let mis_nf_arity mis = - let hyps = mis.mis_mib.mind_hyps in - mis.mis_mip.mind_nf_arity - -let mis_params_ctxt mis = mis.mis_mip.mind_params_ctxt -(* - let paramsign,_ = - decompose_prod_n_assum mis.mis_mip.mind_nparams - (body_of_type (mis_nf_arity mis)) - in paramsign -*) - -let mis_sort mispec = mispec.mis_mip.mind_sort -*) - (* [inductive_family] = [inductive_instance] applied to global parameters *) type inductive_family = inductive * constr list -type inductive_type = IndType of inductive_family * constr list +let make_ind_family (mis, params) = (mis,params) +let dest_ind_family (mis,params) = (mis,params) let liftn_inductive_family n d (mis,params) = (mis, List.map (liftn n d) params) let lift_inductive_family n = liftn_inductive_family n 1 -let liftn_inductive_type n d (IndType (indf, realargs)) = - IndType (liftn_inductive_family n d indf, List.map (liftn n d) realargs) -let lift_inductive_type n = liftn_inductive_type n 1 - let substnl_ind_family l n (mis,params) = (mis, List.map (substnl l n) params) -let substnl_ind_type l n (IndType (indf,realargs)) = - IndType (substnl_ind_family l n indf, List.map (substnl l n) realargs) -let make_ind_family (mis, params) = (mis,params) -let dest_ind_family (mis,params) = (mis,params) +type inductive_type = IndType of inductive_family * constr list let make_ind_type (indf, realargs) = IndType (indf,realargs) let dest_ind_type (IndType (indf,realargs)) = (indf,realargs) +let liftn_inductive_type n d (IndType (indf, realargs)) = + IndType (liftn_inductive_family n d indf, List.map (liftn n d) realargs) +let lift_inductive_type n = liftn_inductive_type n 1 + +let substnl_ind_type l n (IndType (indf,realargs)) = + IndType (substnl_ind_family l n indf, List.map (substnl l n) realargs) + let mkAppliedInd (IndType ((ind,params), realargs)) = applist (mkInd ind,params@realargs) + let mis_is_recursive_subset listind mip = let rec one_is_rec rvec = List.exists @@ -152,6 +62,14 @@ let mis_is_recursive_subset listind mip = let mis_is_recursive (mib,mip) = mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1)) mip +let mis_nf_constructor_type (ind,mib,mip) j = + let specif = mip.mind_nf_lc + and ntypes = mib.mind_ntypes + and nconstr = Array.length mip.mind_consnames in + let make_Ik k = mkInd ((fst ind),ntypes-k-1) in + if j > nconstr then error "Not enough constructors in the type"; + substl (list_tabulate make_Ik ntypes) specif.(j-1) + (* Annotation for cases *) let make_case_info env ind style pats_source = let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -200,15 +118,7 @@ let instantiate_params t args sign = | [], [] -> substl s t | _ -> anomaly"instantiate_params: type, ctxt and args mismatch" in inst [] t (List.rev sign,args) -(* -let get_constructor_type (IndFamily (mispec,params)) j = - assert (j <= mis_nconstr mispec); - let typi = mis_constructor_type j mispec in - instantiate_params typi params (mis_params_ctxt mispec) - -let get_constructors_types (IndFamily (mispec,params) as indf) = - Array.init (mis_nconstr mispec) (fun j -> get_constructor_type indf (j+1)) -*) + let get_constructor (ind,mib,mip,params) j = assert (j <= Array.length mip.mind_consnames); let typi = mis_nf_constructor_type (ind,mib,mip) j in @@ -340,10 +250,8 @@ let is_dep env predty (ind,args) = is_dep_arity env kelim predty glob_t - let set_names env n brty = - let (args,cl) = decompose_prod_n n brty in - let ctxt = List.map (fun (x,ty) -> (x,None,ty)) args in + let (ctxt,cl) = decompose_prod_n_assum n brty in it_mkProd_or_LetIn_name env cl ctxt let set_pattern_names env ind brv = @@ -365,7 +273,7 @@ let type_case_branches_with_names env indspec pj c = (* Guard condition *) (* A function which checks that a term well typed verifies both - syntaxic conditions *) + syntactic conditions *) let control_only_guard env = let rec control_rec c = match kind_of_term c with |