aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/term.ml19
-rw-r--r--kernel/term.mli11
-rw-r--r--parsing/termast.ml55
-rw-r--r--pretyping/cases.ml39
-rw-r--r--pretyping/pretyping.ml18
-rw-r--r--pretyping/retyping.ml6
6 files changed, 76 insertions, 72 deletions
diff --git a/kernel/term.ml b/kernel/term.ml
index 72ab35f12..576a92182 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -13,6 +13,13 @@ open Univ
type existential_key = int
+type pattern_source = DefaultPat of int | RegularPat
+type case_style = PrintLet | PrintIf | PrintCases
+type case_printing =
+ inductive_path * identifier array * int
+ * case_style option * pattern_source array
+type case_info = int array * case_printing
+
type 'a oper =
(* DOP0 *)
| Meta of int
@@ -32,8 +39,6 @@ type 'a oper =
(* an extra slot, for putting in whatever sort of
operator we need for whatever sort of application *)
-and case_info = inductive_path
-
(* Sorts. *)
type contents = Pos | Null
@@ -458,8 +463,6 @@ let args_of_mind = function
| DOPN(MutInd _,args) -> args
| _ -> anomaly "args_of_mind called with bad args"
-let ci_of_mind = op_of_mind
-
(* Destructs a constructor *)
let destMutConstruct = function
| DOPN (MutConstruct cstr_sp,l) -> (cstr_sp,l)
@@ -1325,8 +1328,8 @@ module Hoper =
| Abst sp -> Abst (hsp sp)
| MutInd (sp,i) -> MutInd (hsp sp, i)
| MutConstruct ((sp,i),j) -> MutConstruct ((hsp sp,i),j)
- | MutCase(sp,i) -> MutCase(hsp sp, i)
- | t -> t
+ | MutCase ci as t -> t (* TO DO: extract ind_sp *)
+ | t -> t
let equal o1 o2 =
match (o1,o2) with
| (XTRA s1, XTRA s2) -> s1==s2
@@ -1336,10 +1339,10 @@ module Hoper =
| (MutInd (sp1,i1), MutInd (sp2,i2)) -> sp1==sp2 & i1=i2
| (MutConstruct((sp1,i1),j1), MutConstruct((sp2,i2),j2)) ->
sp1==sp2 & i1=i2 & j1=j2
- | (MutCase(sp1,i1),MutCase(sp2,i2)) -> sp1==sp2 & i1=i2
+ | (MutCase ci1,MutCase ci2) -> ci1==ci2 (* A simplification ?? *)
| _ -> o1=o2
let hash = Hashtbl.hash
- end)
+ end)
module Hconstr =
Hashcons.Make(
diff --git a/kernel/term.mli b/kernel/term.mli
index 8e1c40259..d307e8dae 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -13,6 +13,14 @@ open Generic
type existential_key = int
+type pattern_source = DefaultPat of int | RegularPat
+type case_style = PrintLet | PrintIf | PrintCases
+type case_printing =
+ inductive_path * identifier array * int
+ * case_style option * pattern_source array
+(* the integer is the number of real args, needed for reduction *)
+type case_info = int array * case_printing
+
type 'a oper =
| Meta of int
| Sort of 'a
@@ -26,8 +34,6 @@ type 'a oper =
| CoFix of int
| XTRA of string
-and case_info = inductive_path
-
(*s The sorts of CCI. *)
type contents = Pos | Null
@@ -300,7 +306,6 @@ val args_of_abst : constr -> constr array
val destMutInd : constr -> inductive
val op_of_mind : constr -> inductive_path
val args_of_mind : constr -> constr array
-val ci_of_mind : constr -> case_info
(* Destructs a constructor *)
val destMutConstruct : constr -> constructor
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 15e0b63bd..bd7a22cbd 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -390,6 +390,7 @@ let ids_of_env = Sign.ids_of_env
(* These functions implement a light form of Termenv.mind_specif_of_mind *)
(* specially for handle Cases printing; they respect arities but not typing *)
+(*
let mind_specif_of_mind_light (sp,tyi) =
let mib = Global.lookup_mind sp in
(mib,mind_nth_type_packet mib tyi)
@@ -407,7 +408,7 @@ let rec remove_params n t =
| DOP2(Prod,_,DLAM(_,c)) -> remove_params (n-1) c
| DOP2(Cast,c,_) -> remove_params n c
| _ -> anomaly "remove_params : insufficiently quantified"
-
+
let rec get_params = function
| DOP2(Prod,_,DLAM(x,c)) -> x::(get_params c)
| DOP2(Cast,c,_) -> get_params c
@@ -421,6 +422,7 @@ let sp_of_spi ((sp,_) as spi) =
let (_,mip) = mind_specif_of_mind_light spi in
let (pa,_,k) = repr_path sp in
make_path pa (mip.mind_typename) k
+*)
let bdize_app c al =
let impl =
@@ -564,32 +566,25 @@ let old_bdize at_top env t =
let pred = bdrec avoid env p in
let bl' = array_map_to_list (bdrec avoid env) bl in
ope("MUTCASE",pred::tomatch::bl')
- | Some *) indsp ->
- let (mib,mip as lmis) =
- mind_specif_of_mind_light indsp in
- let lc = lc_of_lmis lmis in
- let lcparams = Array.map get_params lc in
- let k = (nb_prod mip.mind_arity.body) -
- mib.mind_nparams in
+ | Some *) (consnargsl,(_,considl,k,style,tags) as ci) ->
let pred =
- if synth_type & computable p k & lcparams <> [||] then
+ if synth_type & computable p k & considl <> [||] then
(str "SYNTH")
else
bdrec avoid env p
in
- if Detyping.force_if indsp then
+ if Detyping.force_if ci then
ope("FORCEIF", [ pred; tomatch;
bdrec avoid env bl.(0);
bdrec avoid env bl.(1) ])
else
- let idconstructs = mip.mind_consnames in
let asttomatch = ope("TOMATCH", [tomatch]) in
let eqnv =
- array_map3 (bdize_eqn avoid env) idconstructs
- lcparams bl in
+ array_map3 (bdize_eqn avoid env)
+ considl consnargsl bl in
let eqnl = Array.to_list eqnv in
let tag =
- if Detyping.force_let indsp then
+ if Detyping.force_let ci then
"FORCELET"
else
"CASES"
@@ -658,12 +653,19 @@ let old_bdize at_top env t =
in
ope("COFIX", (nvar (string_of_id f))::listdecl))
- and bdize_eqn avoid env constructid construct_params branch =
+ and bdize_eqn avoid env constructid nargs branch =
let print_underscore = Detyping.force_wildcard () in
let cnvar = nvar (string_of_id constructid) in
let rec buildrec nvarlist avoid env = function
- _::l, DOP2(Lambda,_,DLAM(x,b))
+ | 0, b
+ -> let pattern =
+ if nvarlist = [] then cnvar
+ else ope ("PATTCONSTRUCT", cnvar::(List.rev nvarlist)) in
+ let action = bdrec avoid env b in
+ ope("EQN", [action; pattern])
+
+ | n, DOP2(Lambda,_,DLAM(x,b))
-> let x'=
if not print_underscore or (dependent (Rel 1) b) then x
else Anonymous in
@@ -671,29 +673,22 @@ let old_bdize at_top env t =
let new_env = (add_rel (Name id,()) env) in
let new_avoid = id::avoid in
let new_nvarlist = (nvar (string_of_id id))::nvarlist in
- buildrec new_nvarlist new_avoid new_env (l,b)
+ buildrec new_nvarlist new_avoid new_env (n-1,b)
- | l , DOP2(Cast,b,_) (* Oui, il y a parfois des cast *)
- -> buildrec nvarlist avoid env (l,b)
+ | n, DOP2(Cast,b,_) (* Oui, il y a parfois des cast *)
+ -> buildrec nvarlist avoid env (n,b)
- | x::l, b (* eta-expansion : n'arrivera plus lorsque tous les
+ | n, b (* eta-expansion : n'arrivera plus lorsque tous les
termes seront construits à partir de la syntaxe Cases *)
-> (* nommage de la nouvelle variable *)
- let id = next_name_away_with_default "x" x avoid in
+ let id = next_ident_away (id_of_string "x") avoid in
let new_nvarlist = (nvar (string_of_id id))::nvarlist in
let new_env = (add_rel (Name id,()) env) in
let new_avoid = id::avoid in
let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in
- buildrec new_nvarlist new_avoid new_env (l,new_b)
-
- | [] , b
- -> let pattern =
- if nvarlist = [] then cnvar
- else ope ("PATTCONSTRUCT", cnvar::(List.rev nvarlist)) in
- let action = bdrec avoid env b in
- ope("EQN", [action; pattern])
+ buildrec new_nvarlist new_avoid new_env (n-1,new_b)
- in buildrec [] avoid env (construct_params,branch)
+ in buildrec [] avoid env (nargs,branch)
and factorize_binder n avoid env oper na ty c =
let (env2, avoid2,na2) =
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 00dd44445..844e36431 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -115,8 +115,6 @@ type rhs =
rhs_lift : int;
it : rawconstr }
-type pattern_source = DefaultPat of int | RegularPat
-
type equation =
{ dependencies : constr lifted list;
patterns : pattern list;
@@ -222,9 +220,9 @@ let liftn_ind_data n depth md =
nrealargs = md.nrealargs;
nconstr = md.nconstr;
params = List.map (liftn n depth) md.params;
- realargs = List.map (liftn n depth) md.realargs;
- make_arity = md.make_arity;
- make_constrs = md.make_constrs }
+ realargs = List.map (liftn n depth) md.realargs }
+
+let lift_ind_data n = liftn_ind_data n 1
let liftn_tomatch_type n depth = function
| IsInd ind_data -> IsInd (liftn_ind_data n depth ind_data)
@@ -245,9 +243,7 @@ let substn_many_ind_data cv depth md =
nrealargs = md.nrealargs;
nconstr = md.nconstr;
params = List.map (substn_many cv depth) md.params;
- realargs = List.map (substn_many cv depth) md.realargs;
- make_arity = md.make_arity;
- make_constrs = md.make_constrs }
+ realargs = List.map (substn_many cv depth) md.realargs }
let substn_many_tomatch v depth = function
| IsInd ind_data -> IsInd (substn_many_ind_data v depth ind_data)
@@ -501,7 +497,7 @@ let infer_predicate env isevars typs cstrs ind_data =
let (cclargs,_,typn) = eqns.(ind_data.nconstr -1) in
if array_for_all (fun (_,_,typ) -> the_conv_x env isevars typn typ) eqns
then
- let (sign,_) = ind_data.make_arity ind_data.mind ind_data.params in
+ let (sign,_) = get_arity env !isevars ind_data in
let pred = lam_it (lift (List.length sign) typn) sign in
(false,pred) (* true = dependent -- par défaut *)
else
@@ -559,10 +555,10 @@ let rec extract_predicate = function
| PrLetIn ((args,None),pred) -> substl args (extract_predicate pred)
| PrCcl ccl -> ccl
-let abstract_predicate ind_data = function
+let abstract_predicate env sigma ind_data = function
| PrProd _ | PrCcl _ -> anomaly "abstract_predicate: must be some LetIn"
| PrLetIn ((_,copt),pred) ->
- let asign,_ = ind_data.make_arity ind_data.mind ind_data.params in
+ let asign,_ = get_arity env sigma ind_data in
let sign =
List.map (fun (na,t) -> (named_hd (Global.env()) t na,t)) asign in
let dep = copt<> None in
@@ -590,7 +586,7 @@ let specialize_predicate_match tomatchs cs = function
let find_predicate env isevars p typs cstrs current ind_data =
let (dep,pred) =
match p with
- | Some p -> abstract_predicate ind_data p
+ | Some p -> abstract_predicate env !isevars ind_data p
| None -> infer_predicate env isevars typs cstrs ind_data in
let typ = applist (pred, ind_data.realargs) in
if dep then (pred, applist (typ, [current]), dummy_sort)
@@ -721,7 +717,7 @@ and match_current pb (n,tm) =
check_all_variables typ pb.mat;
compile (shift_problem pb)
| IsInd ind_data ->
- let cstrs = ind_data.make_constrs ind_data.mind ind_data.params in
+ let cstrs = get_constructors pb.env !(pb.isevars) ind_data in
let eqns,defaults = group_equations ind_data.mind cstrs pb.mat in
if array_for_all ((=) []) eqns
then compile (shift_problem pb)
@@ -736,8 +732,9 @@ and match_current pb (n,tm) =
let (pred,typ,s) =
find_predicate pb.env pb.isevars
pb.pred brtyps cstrs current ind_data in
- { uj_val = mkMutCaseA (ci_of_mind (mkMutInd ind_data.mind (*,tags*)))
- (*eta_reduce_if_rel*) pred current brvals;
+ let ci = make_case_info
+ (lookup_mind_specif ind_data.mind pb.env) None tags in
+ { uj_val = mkMutCaseA ci (*eta_reduce_if_rel*) pred current brvals;
uj_type = typ;
uj_kind = s }
@@ -858,11 +855,11 @@ let coerce_to_indtype typing_fun isevars env matx tomatchl =
(***********************************************************************)
(* preparing the elimination predicate if any *)
-let build_expected_arity isdep tomatchl sort =
+let build_expected_arity env sigma isdep tomatchl sort =
let cook n = function
| _,IsInd ind_data ->
- (build_dependent_inductive ind_data,
- fst (ind_data.make_arity ind_data.mind ind_data.params))
+ let is = lift_ind_data n ind_data in
+ (build_dependent_inductive is, fst (get_arity env sigma is))
| _,NotInd _ -> anomaly "Should have been catched in case_dependent"
in
let rec buildrec n = function
@@ -870,7 +867,7 @@ let build_expected_arity isdep tomatchl sort =
| tm::ltm ->
let (ty1,aritysign) = cook n tm in
let rec follow n = function
- | (na,ty2)::sign -> DOP2(Prod,lift n ty2,DLAM(na,follow (n+1) sign))
+ | (na,ty2)::sign -> DOP2(Prod,ty2,DLAM(na,follow (n+1) sign))
| _ ->
if isdep then DOP2(Prod,ty1,DLAM(Anonymous,buildrec (n+1) ltm))
else buildrec n ltm
@@ -930,9 +927,9 @@ let case_dependent env sigma loc predj tomatchs =
let ndepv = List.map nb_dep_ity tomatchs in
let sum = List.fold_right (fun i j -> i+j) ndepv 0 in
let depsum = sum + List.length tomatchs in
- if n = sum then (false,build_expected_arity true tomatchs sort)
+ if n = sum then (false,build_expected_arity env sigma false tomatchs sort)
else if n = depsum
- then (true,build_expected_arity true tomatchs sort)
+ then (true,build_expected_arity env sigma true tomatchs sort)
else error_wrong_predicate_arity_loc loc CCI env etapred sum depsum
let prepare_predicate typing_fun isevars env tomatchs = function
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 02742b64c..3af306fe4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -83,7 +83,7 @@ let transform_rec loc env sigma cl (ct,pt) =
error_number_branches_loc loc CCI env c ct expn;
if is_recursive [mispec.mis_tyi] recargs then
let (dep,_) = find_case_dep_nparams env sigma (c,p) appmind pt in
- let ntypes = mis_nconstr mispec
+ let ntypes = mis_ntypes mispec (* was mis_nconstr !?! *)
and tyi = mispec.mis_tyi
and nparams = mis_nparams mispec in
let depFvec = Array.create ntypes (None : (bool * constr) option) in
@@ -96,6 +96,7 @@ let transform_rec loc env sigma cl (ct,pt) =
hnf_prod_appvect env sigma "make_branch" (mis_arity mispec) vargs in
let lnames,_ = splay_prod env sigma realar in
let nar = List.length lnames in
+ let ci = make_default_case_info mispec in
let branches =
array_map3
(fun f t reca ->
@@ -110,8 +111,7 @@ let transform_rec loc env sigma cl (ct,pt) =
(lambda_create env
(appvect (mI,Array.append (Array.map (lift (nar+1)) vargs)
(rel_vect 0 nar)),
- mkMutCaseA (ci_of_mind mI)
- (lift (nar+2) p) (Rel 1) branches))
+ mkMutCaseA ci (lift (nar+2) p) (Rel 1) branches))
(lift_context 1 lnames)
in
if noccurn 1 deffix then
@@ -136,8 +136,11 @@ let transform_rec loc env sigma cl (ct,pt) =
DLAMV(Name(id_of_string "F"),[|deffix|])|])
in
applist (fix,realargs@[c])
- else
- mkMutCaseA (ci_of_mind mI) p c lf
+ else
+ let lnames,_ = splay_prod env sigma (mis_arity mispec) in
+ let nar = List.length lnames in
+ let ci = make_default_case_info mispec in
+ mkMutCaseA ci p c lf
(***********************************************************************)
let ctxt_of_ids ids =
@@ -411,7 +414,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
let evalct = nf_ise1 !isevars cj.uj_type
and evalPt = nf_ise1 !isevars pj.uj_type in
- let (mind,bty,rsty) =
+ let (_,bty,rsty) =
Indrec.type_rec_branches isrec env !isevars evalct evalPt pj.uj_val cj.uj_val in
if Array.length bty <> Array.length lf then
wrong_number_of_cases_message loc env isevars (cj.uj_val,evalct)
@@ -428,7 +431,8 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
then
let rEC = Array.append [|pj.uj_val; cj.uj_val|] lfv in
transform_rec loc env !isevars rEC (evalct,evalPt)
- else let ci = ci_of_mind mind in
+ else
+ let ci = make_default_case_info (lookup_mind_specif mind env) in
mkMutCaseA ci pj.uj_val cj.uj_val (Array.map (fun j-> j.uj_val) lfj) in
{uj_val = v;
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index b84e1f0be..51f7e66e3 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -53,14 +53,14 @@ let rec type_of env cstr=
| IsMutConstruct cstr ->
let (typ,kind) = destCast (type_of_constructor env sigma cstr) in typ
| IsMutCase (_,p,c,lf) ->
- let {realargs=args;make_arity=make_arity;params=params;mind=mind} =
+ let ind_data =
try try_mutind_of env sigma (type_of env c)
with Induc -> anomaly "type_of: Bad inductive" in
- let (aritysign,_) = make_arity mind params in
+ let (aritysign,_) = get_arity env sigma ind_data in
let (psign,_) = splay_prod env sigma (type_of env p) in
let al =
if List.length psign > List.length aritysign
- then args@[c] else args in
+ then ind_data.realargs@[c] else ind_data.realargs in
whd_betadeltaiota env sigma (applist (p,al))
| IsLambda (name,c1,c2) ->
let var = make_typed c1 (sort_of env c1) in
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 03:42:55 +0000