diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 30 | ||||
| -rw-r--r-- | library/declare.mli | 3 | ||||
| -rw-r--r-- | library/global.mli | 12 | ||||
| -rw-r--r-- | library/indrec.ml | 98 | ||||
| -rw-r--r-- | library/indrec.mli | 24 |
5 files changed, 76 insertions, 91 deletions
diff --git a/library/declare.ml b/library/declare.ml index 8766467fce..ff46ad72ae 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -274,19 +274,19 @@ let is_global id = with Not_found -> false -let mind_path = function - | DOPN(MutInd (sp,0),_) -> sp - | DOPN(MutInd (sp,tyi),_) -> - let mib = Global.lookup_mind sp in - let mip = mind_nth_type_packet mib tyi in - let (pa,_,k) = repr_path sp in - Names.make_path pa (mip.mind_typename) k - | DOPN(MutConstruct ((sp,tyi),ind),_) -> - let mib = Global.lookup_mind sp in - let mip = mind_nth_type_packet mib tyi in - let (pa,_,k) = repr_path sp in - Names.make_path pa (mip.mind_consnames.(ind-1)) k - | _ -> invalid_arg "mind_path" +let path_of_constructor_path ((sp,tyi),ind) = + let mib = Global.lookup_mind sp in + let mip = mind_nth_type_packet mib tyi in + let (pa,_,k) = repr_path sp in + Names.make_path pa (mip.mind_consnames.(ind-1)) k + +let path_of_inductive_path (sp,tyi) = + if tyi = 0 then sp + else + let mib = Global.lookup_mind sp in + let mip = mind_nth_type_packet mib tyi in + let (pa,_,k) = repr_path sp in + Names.make_path pa (mip.mind_typename) k (* Eliminations. *) @@ -294,8 +294,8 @@ let declare_eliminations sp i = let oper = MutInd (sp,i) in let mib = Global.lookup_mind sp in let ids = ids_of_sign mib.mind_hyps in - let mind = DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids)) in - let mispec = Global.lookup_mind_specif mind in + let ctxt = Array.of_list (List.map (fun id -> VAR id) ids) in + let mispec = Global.lookup_mind_specif ((sp,i),ctxt) in let mindstr = string_of_id (mis_typename mispec) in let declare na c = declare_constant (id_of_string na) diff --git a/library/declare.mli b/library/declare.mli index c4644b4654..8541c20921 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -71,4 +71,5 @@ val construct_reference : Environ.env -> path_kind -> identifier -> constr val is_global : identifier -> bool -val mind_path : constr -> section_path +val path_of_inductive_path : inductive_path -> section_path +val path_of_constructor_path : constructor_path -> section_path diff --git a/library/global.mli b/library/global.mli index a61b09c58f..e9e42cf5eb 100644 --- a/library/global.mli +++ b/library/global.mli @@ -34,7 +34,7 @@ val lookup_var : identifier -> name * typed_type val lookup_rel : int -> name * typed_type val lookup_constant : section_path -> constant_body val lookup_mind : section_path -> mutual_inductive_body -val lookup_mind_specif : constr -> mind_specif +val lookup_mind_specif : inductive -> mind_specif val export : string -> compiled_env val import : compiled_env -> unit @@ -46,10 +46,10 @@ val id_of_global : sorts oper -> identifier (*s Re-exported functions of [Inductive], composed with [lookup_mind_specif]. *) -val mind_is_recursive : constr -> bool -val mind_nconstr : constr -> int -val mind_nparams : constr -> int -val mind_arity : constr -> constr +val mind_is_recursive : inductive -> bool +val mind_nconstr : inductive -> int +val mind_nparams : inductive -> int +val mind_arity : inductive -> constr -val mind_lc_without_abstractions : constr -> constr array +val mind_lc_without_abstractions : inductive -> constr array diff --git a/library/indrec.ml b/library/indrec.ml index d24120bf09..2d1761daf3 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -97,8 +97,7 @@ let mis_make_case_com depopt env sigma mispec kinds = in it_lambda_name env (make_lambda_string "P" typP (add_branch 0)) lnamespar -let make_case_com depopt env sigma mind kinds = - let ity = mrectype_spec env sigma mind in +let make_case_com depopt env sigma ity kinds = let mispec = lookup_mind_specif ity env in mis_make_case_com depopt env sigma mispec kinds @@ -356,11 +355,6 @@ let mis_make_indrec env sigma listdepkind mispec = in Array.init nrec make_one_rec -let make_indrec env sigma listdepkind mind = - let ity = minductype_spec env sigma mind in - let mispec = lookup_mind_specif ity env in - mis_make_indrec env sigma listdepkind mispec - let change_sort_arity sort = let rec drec = function | (DOP2(Cast,c,t)) -> drec c @@ -394,24 +388,25 @@ let check_arities listdepkind = 'sTR "is not allowed">]) listdepkind +(* Utilisé pour construire les Scheme *) let build_indrec env sigma = function | (mind,dep,s)::lrecspec -> - let redind = minductype_spec env sigma mind in - let (sp,tyi,_) = destMutInd redind in + let ((sp,tyi),_) = mind in + let mispec = lookup_mind_specif mind env in let listdepkind = - (lookup_mind_specif redind env, dep,s):: - (List.map (function (mind',dep',s') -> - let redind' = minductype_spec env sigma mind' in - let (sp',_,_) = destMutInd redind' in - if sp=sp' then - (lookup_mind_specif redind' env,dep',s') - else - error - "Induction schemes concern mutually inductive types") + (mispec, dep,s):: + (List.map + (function (mind',dep',s') -> + let ((sp',_),_) = mind' in + if sp=sp' then + (lookup_mind_specif mind' env,dep',s') + else + error + "Induction schemes concern mutually inductive types") lrecspec) in let _ = check_arities listdepkind in - make_indrec env sigma listdepkind mind + mis_make_indrec env sigma listdepkind mispec | _ -> assert false @@ -433,7 +428,7 @@ let type_mutind_rec env sigma ct pt p c = let (constrvec,typeconstrvec) = mis_type_mconstructs mispec in let lft = array_map3 (type_rec_branch dep env sigma (vargs,depPvec,0)) constrvec typeconstrvec recargs in - (mI, lft, + (mkMutInd mI, lft, if dep then applist(p,realargs@[c]) else applist(p,realargs) ) else @@ -476,7 +471,7 @@ let norec_branch_scheme env sigma typc = in crec typc -let rec_branch_scheme env sigma j typc recargs = +let rec_branch_scheme env sigma ((sp,j),_) typc recargs = let rec crec (typc,recargs) = match whd_betadeltaiota env sigma typc, recargs with | (DOP2(Prod,c,DLAM(name,t)),(ra::reca)) -> @@ -493,14 +488,12 @@ let rec_branch_scheme env sigma j typc recargs = in crec (typc,recargs) -let branch_scheme env sigma isrec i mind = - let typc = type_inst_construct env sigma i mind in +let branch_scheme env sigma isrec i (mind,args as appmind) = + let typc = type_inst_construct env sigma i appmind in if isrec then - let (mI,_) = find_mrectype env sigma mind in - let (_,j,_) = destMutInd mI in - let mispec = lookup_mind_specif mI env in + let mispec = lookup_mind_specif mind env in let recarg = (mis_recarg mispec).(i-1) in - rec_branch_scheme env sigma j typc recarg + rec_branch_scheme env sigma mind typc recarg else norec_branch_scheme env sigma typc @@ -522,44 +515,33 @@ let build_notdep_pred env sigma mispec nparams globargs pred = in finalpred -let pred_case_ml_fail env sigma isrec ct (i,ft) = - try - let (mI,largs) = find_mrectype env sigma ct in - let (_,j,_) = destMutInd mI in - let mispec = lookup_mind_specif mI env in - let nparams = mis_nparams mispec in - let (globargs,la) = list_chop nparams largs in - let pred = - let recargs = (mis_recarg mispec) in - assert (Array.length recargs <> 0); - let recargi = recargs.(i-1) in - let nbrec = if isrec then count_rec_arg j recargi else 0 in - let nb_arg = List.length (recargs.(i-1)) + nbrec in - let pred = concl_n env sigma nb_arg ft in - if noccur_bet 1 nb_arg pred then - lift (-nb_arg) pred - else - failwith "Dependent" - in - if la = [] then - pred - else (* we try with [_:T1]..[_:Tn](lift n pred) *) - build_notdep_pred env sigma mispec nparams globargs pred - with Induc -> - failwith "Inductive" +let pred_case_ml_fail env sigma isrec (mI,globargs,la) (i,ft) = + let (_,j),_ = mI in + let mispec = lookup_mind_specif mI env in + let nparams = mis_nparams mispec in + let pred = + let recargs = (mis_recarg mispec) in + assert (Array.length recargs <> 0); + let recargi = recargs.(i-1) in + let nbrec = if isrec then count_rec_arg j recargi else 0 in + let nb_arg = List.length (recargs.(i-1)) + nbrec in + let pred = concl_n env sigma nb_arg ft in + if noccur_bet 1 nb_arg pred then + lift (-nb_arg) pred + else + failwith "Dependent" + in + if la = [] then + pred + else (* we try with [_:T1]..[_:Tn](lift n pred) *) + build_notdep_pred env sigma mispec nparams globargs pred let pred_case_ml env sigma isrec (c,ct) lf (i,ft) = - try pred_case_ml_fail env sigma isrec ct (i,ft) - with Failure mes -> - error_ml_case CCI env mes c ct lf.(i-1) ft (* similar to pred_case_ml but does not expect the list lf of braches *) let pred_case_ml_onebranch env sigma isrec (c,ct) (i,f,ft) = - try pred_case_ml_fail env sigma isrec ct (i,ft) - with Failure mes -> - error_ml_case CCI env mes c ct f ft let make_case_ml isrec pred c ci lf = if isrec then diff --git a/library/indrec.mli b/library/indrec.mli index f1d1b51904..4b078c4f13 100644 --- a/library/indrec.mli +++ b/library/indrec.mli @@ -11,12 +11,9 @@ open Evd (* Eliminations. *) -val make_case_dep : env -> 'a evar_map -> constr -> sorts -> constr -val make_case_nodep : env -> 'a evar_map -> constr -> sorts -> constr -val make_case_gen : env -> 'a evar_map -> constr -> sorts -> constr - -val make_indrec : env -> 'a evar_map -> - (mind_specif * bool * sorts) list -> constr -> constr array +val make_case_dep : env -> 'a evar_map -> inductive -> sorts -> constr +val make_case_nodep : env -> 'a evar_map -> inductive -> sorts -> constr +val make_case_gen : env -> 'a evar_map -> inductive -> sorts -> constr val mis_make_indrec : env -> 'a evar_map -> (mind_specif * bool * sorts) list -> mind_specif -> constr array @@ -24,7 +21,7 @@ val mis_make_indrec : env -> 'a evar_map -> val instanciate_indrec_scheme : sorts -> int -> constr -> constr val build_indrec : - env -> 'a evar_map -> (constr * bool * sorts) list -> constr array + env -> 'a evar_map -> (inductive * bool * sorts) list -> constr array val type_rec_branches : bool -> env -> 'c evar_map -> constr -> constr -> constr -> constr -> constr * constr array * constr @@ -42,13 +39,18 @@ i*) val is_mutind : env -> 'a evar_map -> constr -> bool val branch_scheme : - env -> 'a evar_map -> bool -> int -> constr -> constr + env -> 'a evar_map -> bool -> int -> inductive * constr list -> constr + +(* In [inductive * constr list * constr list], the second argument is + the list of global parameters and the third the list of real args *) -val pred_case_ml : env -> 'c evar_map -> bool -> (constr * constr) - -> constr array -> (int*constr) ->constr +val pred_case_ml : env -> 'c evar_map -> bool -> + constr * (inductive * constr list * constr list) + -> constr array -> int * constr ->constr val pred_case_ml_onebranch : env ->'c evar_map -> bool -> - constr * constr ->int * constr * constr -> constr + constr * (inductive * constr list * constr list) + -> int * constr * constr -> constr val make_case_ml : bool -> constr -> constr -> case_info -> constr array -> constr |