aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/funind/rawterm_to_relation.ml6
-rw-r--r--contrib/funind/rawtermops.mli5
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.mli10
-rw-r--r--interp/constrextern.ml12
-rw-r--r--interp/constrintern.ml21
-rw-r--r--interp/topconstr.ml18
-rw-r--r--interp/topconstr.mli2
-rw-r--r--parsing/g_xml.ml460
-rw-r--r--pretyping/cases.ml24
-rw-r--r--pretyping/detyping.ml12
-rw-r--r--pretyping/detyping.mli2
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/inductiveops.mli3
-rw-r--r--pretyping/pattern.ml26
-rw-r--r--pretyping/pattern.mli2
-rw-r--r--pretyping/rawterm.ml7
-rw-r--r--pretyping/rawterm.mli5
17 files changed, 100 insertions, 117 deletions
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 1234c7faa..681e43af0 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -561,10 +561,8 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
build_entry_lc funnames avoid b
| RDynamic _ -> error "Not handled RDynamic"
and build_entry_lc_from_case funname make_discr
- (el:(Rawterm.rawconstr *
- (Names.name * (loc * Names.inductive * Names.name list) option) )
- list)
- (brl:(loc * identifier list * cases_pattern list * rawconstr) list) avoid :
+ (el:tomatch_tuple)
+ (brl:Rawterm.cases_clauses) avoid :
rawconstr build_entry_return =
match el with
| [] -> assert false (* matched on Nothing !*)
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index 92df0ec6c..5dcdb15c5 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -22,10 +22,7 @@ val mkRApp : rawconstr*(rawconstr list) -> rawconstr
val mkRLambda : Names.name*rawconstr*rawconstr -> rawconstr
val mkRProd : Names.name*rawconstr*rawconstr -> rawconstr
val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr
-val mkRCases : rawconstr option *
- (rawconstr * (Names.name * (Util.loc * Names.inductive * Names.name list) option)) list *
- (Util.loc * Names.identifier list * cases_pattern list * rawconstr) list ->
- rawconstr
+val mkRCases : rawconstr option * tomatch_tuple * cases_clauses -> rawconstr
val mkRSort : rawsort -> rawconstr
val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
index b0de06416..128511c13 100644
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -28,12 +28,8 @@ val rewrite_fixpoint :
'c
val list_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
val rewrite_cases_aux :
- Util.loc * Rawterm.rawconstr option *
- (Rawterm.rawconstr *
- (Names.name * (Util.loc * Names.inductive * Names.name list) option))
- list *
- (Util.loc * Names.identifier list * Rawterm.cases_pattern list *
- Rawterm.rawconstr)
- list -> Rawterm.rawconstr
+ Util.loc * Rawterm.rawconstr option *
+ Rawterm.tomatch_tuple * Rawterm.cases_clauses
+ -> Rawterm.rawconstr
val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4fbeff526..e3d4d1a4d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -260,7 +260,7 @@ let rec same_raw c d =
(fun (t1,(al1,oind1)) (t2,(al2,oind2)) ->
same_raw t1 t2;
if al1 <> al2 then failwith "RCases";
- option_iter2(fun (_,i1,nl1) (_,i2,nl2) ->
+ option_iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) ->
if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2;
List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) ->
List.iter2 same_patt pl1 pl2;
@@ -690,11 +690,13 @@ let rec extern inctx scopes vars r =
| Name id, RVar (_,id') when id=id' -> None
| Name _, _ -> Some na in
(sub_extern false scopes vars tm,
- (na',option_map (fun (loc,ind,nal) ->
+ (na',option_map (fun (loc,ind,n,nal) ->
+ let params = list_tabulate
+ (fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in
let args = List.map (function
| Anonymous -> RHole (dummy_loc,Evd.InternalHole)
| Name id -> RVar (dummy_loc,id)) nal in
- let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),args) in
+ let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in
(extern_typ scopes vars t)) x))) tml in
let eqns = List.map (extern_eqn (rtntypopt<>None) scopes vars) eqns in
CCases (loc,rtntypopt',tml,eqns)
@@ -920,8 +922,8 @@ let rec raw_of_pat env = function
let indnames,rtn =
if p = PMeta None then (Anonymous,None),None
else
- let n = out_some ind_nargs in
- return_type_of_predicate ind n (raw_of_pat env p) in
+ let nparams,n = out_some ind_nargs in
+ return_type_of_predicate ind nparams n (raw_of_pat env p) in
RCases (loc,rtn,[raw_of_pat env tm,indnames],mat)
| PFix f -> Detyping.detype false [] env (mkFix f)
| PCoFix c -> Detyping.detype false [] env (mkCoFix c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 376360046..1e8c7fdef 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -22,6 +22,7 @@ open Cases
open Topconstr
open Nametab
open Notation
+open Inductiveops
(* To interpret implicits and arg scopes of recursive variables in
inductive types and recursive definitions *)
@@ -382,11 +383,6 @@ let check_constructor_length env loc cstr pl pl0 =
if n <> nargs && n <> nhyps (* i.e. with let's *) then
error_wrong_numarg_constructor_loc loc env cstr nargs
-let check_inductive_length env (loc,ind,nal) =
- let n = Inductiveops.inductive_nargs env ind in
- if n <> List.length nal then
- error_wrong_numarg_inductive_loc loc env ind n
-
(* Manage multiple aliases *)
(* [merge_aliases] returns the sets of all aliases encountered at this
@@ -950,18 +946,25 @@ let internalise sigma globalenv env allow_soapp lvar c =
let tids = names_of_cases_indtype t in
let tids = List.fold_right Idset.add tids Idset.empty in
let t = intern_type (tids,None,scopes) t in
- let (_,_,nal as indsign) =
+ let (_,_,_,nal as indsign) =
match t with
- | RRef (loc,IndRef ind) -> (loc,ind,[])
+ | RRef (loc,IndRef ind) -> (loc,ind,0,[])
| RApp (loc,RRef (_,IndRef ind),l) ->
+ let nparams, nrealargs = inductive_nargs globalenv ind in
+ let nindargs = nparams + nrealargs in
+ if List.length l <> nindargs then
+ error_wrong_numarg_inductive_loc loc globalenv ind nindargs;
let nal = List.map (function
| RHole _ -> Anonymous
| RVar (_,id) -> Name id
| c ->
user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in
- (loc,ind,nal)
+ let parnal,realnal = list_chop nparams nal in
+ if List.exists ((<>) Anonymous) parnal then
+ user_err_loc (loc,"",
+ str "The parameters of inductive type must be implicit");
+ (loc,ind,nparams,nal)
| _ -> error_bad_inductive_type (loc_of_rawconstr t) in
- check_inductive_length globalenv indsign;
nal, Some indsign
| None ->
[], None in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index cc84d0c10..7a634a71a 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -38,7 +38,7 @@ type aconstr =
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
| ACases of aconstr option *
- (aconstr * (name * (inductive * name list) option)) list *
+ (aconstr * (name * (inductive * int * name list) option)) list *
(identifier list * cases_pattern list * aconstr) list
| ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| AIf of aconstr * (name * aconstr option) * aconstr * aconstr
@@ -76,10 +76,10 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
let e',t' = match t with
| None -> e',None
- | Some (ind,nal) ->
+ | Some (ind,npar,nal) ->
let e',nal' = List.fold_right (fun na (e',nal) ->
let e',na' = name_app g e' na in e',na'::nal) nal (e',[]) in
- e',Some (loc,ind,nal') in
+ e',Some (loc,ind,npar,nal') in
let e',na' = name_app g e' na in
(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
let fold id (idl,e) = let (id,e) = g id e in (id::idl,e) in
@@ -186,8 +186,8 @@ let aconstr_and_vars_of_rawconstr a =
List.map (fun (tm,(na,x)) ->
add_name found na;
option_iter
- (fun (_,_,nl) -> List.iter (add_name found) nl) x;
- (aux tm,(na,option_map (fun (_,ind,nal) -> (ind,nal)) x))) tml,
+ (fun (_,_,_,nl) -> List.iter (add_name found) nl) x;
+ (aux tm,(na,option_map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml,
List.map f eqnl)
| RLetTuple (loc,nal,(na,po),b,c) ->
add_name found na;
@@ -289,9 +289,9 @@ let rec subst_aconstr subst bound raw =
and rl' = list_smartmap
(fun (a,(n,signopt) as x) ->
let a' = subst_aconstr subst bound a in
- let signopt' = option_map (fun ((indkn,i),nal as z) ->
+ let signopt' = option_map (fun ((indkn,i),n,nal as z) ->
let indkn' = subst_kn subst indkn in
- if indkn == indkn' then z else ((indkn',i),nal)) signopt in
+ if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in
if a' == a && signopt' == signopt then x else (a',(n,signopt')))
rl
and branches' = list_smartmap
@@ -349,11 +349,11 @@ let abstract_return_type_context pi mklam tml rtno =
rtno
let abstract_return_type_context_rawconstr =
- abstract_return_type_context pi3
+ abstract_return_type_context (fun (_,_,_,nal) -> nal)
(fun na c -> RLambda(dummy_loc,na,RHole(dummy_loc,Evd.InternalHole),c))
let abstract_return_type_context_aconstr =
- abstract_return_type_context snd
+ abstract_return_type_context pi3
(fun na c -> ALambda(na,AHole Evd.InternalHole,c))
let rec adjust_scopes = function
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 4e2017f44..d5b718d34 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -34,7 +34,7 @@ type aconstr =
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
| ACases of aconstr option *
- (aconstr * (name * (inductive * name list) option)) list *
+ (aconstr * (name * (inductive * int * name list) option)) list *
(identifier list * cases_pattern list * aconstr) list
| ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| AIf of aconstr * (name * aconstr option) * aconstr * aconstr
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 23fdfdaa2..56be1ff5a 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -84,7 +84,7 @@ let global_of_cdata (loc,a) = Nametab.locate (uri_of_data a)
let inductive_of_cdata a = match global_of_cdata a with
| IndRef (kn,_) -> kn
- | _ -> failwith "kn"
+ | _ -> anomaly "XML parser: not an inductive"
let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a))
@@ -108,43 +108,54 @@ let get_xml_inductive al =
let get_xml_constructor al =
(get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al))
-let get_xml_name al =
+let get_xml_binder al =
try Name (ident_of_cdata (List.assoc "binder" al))
with Not_found -> Anonymous
let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al)
+let get_xml_name al = ident_of_cdata (get_xml_attr "name" al)
+
let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al)
+let get_xml_no al = nmtoken (get_xml_attr "no" al)
+
(* A leak in the xml dtd: arities of constructor need to know global env *)
let compute_branches_lengths ind =
let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
mip.Declarations.mind_consnrealdecls
-let compute_predicate_length ind =
- let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
- mip.Declarations.mind_nrealargs
+let compute_inductive_nargs ind =
+ Inductiveops.inductive_nargs (Global.env()) ind
(* Interpreting constr as a rawconstr *)
let rec interp_xml_constr = function
| XmlTag (loc,"REL",al,[]) ->
RVar (loc, get_xml_ident al)
- | XmlTag (loc,"VAR",al,[]) -> failwith ""
- | XmlTag (loc,"LAMBDA",al,[x1;x2]) ->
- let na,t = interp_xml_decl x1 in
- RLambda (loc, na, t, interp_xml_target x2)
- | XmlTag (loc,"PROD",al,[x1;x2]) ->
- let na,t = interp_xml_decl x1 in
- RProd (loc, na, t, interp_xml_target x2)
+ | XmlTag (loc,"VAR",al,[]) ->
+ error "XML parser: unable to interp free variables"
+ | XmlTag (loc,"LAMBDA",al,(_::_ as xl)) ->
+ let body,decls = list_sep_last xl in
+ let ctx = List.map interp_xml_decl decls in
+ List.fold_right (fun (na,t) b -> RLambda (loc, na, t, b))
+ ctx (interp_xml_target body)
+ | XmlTag (loc,"PROD",al,(_::_ as xl)) ->
+ let body,decls = list_sep_last xl in
+ let ctx = List.map interp_xml_decl decls in
+ List.fold_right (fun (na,t) b -> RProd (loc, na, t, b))
+ ctx (interp_xml_target body)
| XmlTag (loc,"LETIN",al,[x1;x2]) ->
let na,t = interp_xml_def x1 in
RLetIn (loc, na, t, interp_xml_target x2)
| XmlTag (loc,"APPLY",_,x::xl) ->
RApp (loc, interp_xml_constr x, List.map interp_xml_constr xl)
+ | XmlTag (loc,"instantiate",_,
+ (XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) ->
+ RApp (loc, interp_xml_constr x, List.map interp_xml_arg xl)
| XmlTag (loc,"META",al,xl) ->
- failwith "META: TODO"
+ REvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl))
| XmlTag (loc,"CONST",al,[]) ->
RRef (loc, ConstRef (get_xml_constant al))
| XmlTag (loc,"MUTCASE",al,x::y::yl) ->
@@ -154,8 +165,8 @@ let rec interp_xml_constr = function
let brs = List.map interp_xml_pattern yl in
let brns = Array.to_list (compute_branches_lengths ind) in
let mat = simple_cases_matrix_of_branches ind brns brs in
- let n = compute_predicate_length ind in
- let nal,rtn = return_type_of_predicate ind n p in
+ let nparams,n = compute_inductive_nargs ind in
+ let nal,rtn = return_type_of_predicate ind nparams n p in
RCases (loc,rtn,[tm,nal],mat)
| XmlTag (loc,"MUTIND",al,[]) ->
RRef (loc, IndRef (get_xml_inductive al))
@@ -164,7 +175,8 @@ let rec interp_xml_constr = function
| XmlTag (loc,"FIX",al,xl) ->
let li,lnct = List.split (List.map interp_xml_FixFunction xl) in
let ln,lc,lt = list_split3 lnct in
- RRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
+ let lctx = List.map (fun _ -> []) ln in
+ RRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt)
| XmlTag (loc,"COFIX",al,xl) ->
let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in
RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
@@ -192,10 +204,13 @@ and interp_xml_body x = interp_xml_constr_alias "body" x
and interp_xml_pattern x = interp_xml_constr_alias "pattern" x
and interp_xml_patternsType x = interp_xml_constr_alias "patternsType" x
and interp_xml_inductiveTerm x = interp_xml_constr_alias "inductiveTerm" x
+and interp_xml_arg x = interp_xml_constr_alias "arg" x
+and interp_xml_substitution x = interp_xml_constr_alias "substitution" x
+ (* no support for empty substitution from official dtd *)
and interp_xml_decl_alias s x =
match interp_xml_tag s x with
- | (_,al,[x]) -> (get_xml_name al, interp_xml_constr x)
+ | (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x)
| (loc,_,_) ->
user_err_loc (loc,"",str "wrong number of arguments (expect one)")
@@ -216,23 +231,22 @@ and interp_xml_recursionOrder x =
| _ ->
user_err_loc (locs,"",str "invalid recursion order")
-
and interp_xml_FixFunction x =
match interp_xml_tag "FixFunction" x with
- | (loc,al,[x1;x2;x3]) ->
+ | (loc,al,[x1;x2;x3]) -> (* Not in official cic.dtd, not in constr *)
((Some (nmtoken (get_xml_attr "recIndex" al)),
interp_xml_recursionOrder x1),
- (get_xml_ident al, interp_xml_type x2, interp_xml_body x3))
- | (loc,al,[x1;x2]) -> (* For backwards compatibility *)
+ (get_xml_name al, interp_xml_type x2, interp_xml_body x3))
+ | (loc,al,[x1;x2]) ->
((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec),
- (get_xml_ident al, interp_xml_type x1, interp_xml_body x2))
+ (get_xml_name al, interp_xml_type x1, interp_xml_body x2))
| (loc,_,_) ->
user_err_loc (loc,"",str "wrong number of arguments (expect one)")
and interp_xml_CoFixFunction x =
match interp_xml_tag "CoFixFunction" x with
| (loc,al,[x1;x2]) ->
- (get_xml_ident al, interp_xml_type x1, interp_xml_body x2)
+ (get_xml_name al, interp_xml_type x1, interp_xml_body x2)
| (loc,_,_) ->
user_err_loc (loc,"",str "wrong number of arguments (expect one)")
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 425221675..f709ab450 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -66,13 +66,10 @@ let error_needs_inversion env x t =
module type S = sig
val compile_cases :
loc ->
- (type_constraint -> env -> rawconstr -> unsafe_judgment) *
+ (type_constraint -> env -> rawconstr -> unsafe_judgment) *
Evd.evar_defs ref ->
type_constraint ->
- env ->
- rawconstr option *
- (rawconstr * (name * (loc * inductive * name list) option)) list *
- (loc * identifier list * cases_pattern list * rawconstr) list ->
+ env -> rawconstr option * tomatch_tuple * cases_clauses ->
unsafe_judgment
end
@@ -344,7 +341,7 @@ let unify_tomatch_with_patterns isevars env typ tm =
let find_tomatch_tycon isevars env loc = function
(* Try first if some 'in I ...' is present and can be used as a constraint *)
- | Some (_,ind,_),_
+ | Some (_,ind,_,_),_
(* Otherwise try to get constraints from (the 1st) constructor in clauses *)
| None, Some (_,(ind,_)) ->
mk_tycon (inductive_template isevars env loc ind)
@@ -1539,7 +1536,7 @@ let extract_arity_signature env0 tomatchl tmsign =
| NotInd (bo,typ) ->
(match t with
| None -> [na,option_map (lift n) bo,lift n typ]
- | Some (loc,_,_) ->
+ | Some (loc,_,_,_) ->
user_err_loc (loc,"",
str "Unexpected type annotation for a term of non inductive type"))
| IsInd (_,IndType(indf,realargs)) ->
@@ -1548,18 +1545,9 @@ let extract_arity_signature env0 tomatchl tmsign =
let nrealargs = List.length realargs in
let realnal =
match t with
- | Some (loc,ind',nal) ->
- let nparams = List.length params in
- if ind <> ind' then
+ | Some (loc,ind',nparams,realnal) ->
+ if ind <> ind' or List.length params <> nparams then
user_err_loc (loc,"",str "Wrong inductive type");
- let nindargs = nparams + nrealargs in
- (* Normally done at interning time *)
- if List.length nal <> nindargs then
- error_wrong_numarg_inductive_loc loc env0 ind' nindargs;
- let parnal,realnal = list_chop nparams nal in
- if List.exists ((<>) Anonymous) parnal then
- user_err_loc (loc,"",
- str "The parameters of inductive type must be implicit");
List.rev realnal
| None -> list_tabulate (fun _ -> Anonymous) nrealargs in
let arsign = fst (get_arity env0 indf') in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 25cf2aedd..1f6e4a86b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -314,9 +314,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
| _ -> Anonymous, typ in
let aliastyp =
if List.for_all ((=) Anonymous) nl then None
- else
- let pars = list_tabulate (fun _ -> Anonymous) nparams in
- Some (dl,indsp,pars@nl) in
+ else Some (dl,indsp,nparams,nl) in
n, aliastyp, Some typ
in
let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
@@ -577,9 +575,9 @@ let rec subst_rawconstr subst raw =
let a' = subst_rawconstr subst a in
let (n,topt) = x in
let topt' = option_smartmap
- (fun (loc,(sp,i),x as t) ->
+ (fun (loc,(sp,i),x,y as t) ->
let sp' = subst_kn subst sp in
- if sp == sp' then t else (loc,(sp',i),x)) topt in
+ if sp == sp' then t else (loc,(sp',i),x,y)) topt in
if a == a' && topt == topt' then y else (a',(n,topt'))) rl
and branches' = list_smartmap
(fun (loc,idl,cpl,r as branch) ->
@@ -647,6 +645,6 @@ let simple_cases_matrix_of_branches ind brns brs =
(dummy_loc,ids,[p],c))
0 brns brs
-let return_type_of_predicate ind n pred =
+let return_type_of_predicate ind nparams n pred =
let nal,p = it_destRLambda_or_LetIn_names (n+1) pred in
- (List.hd nal, Some (dummy_loc,ind,List.tl nal)), Some p
+ (List.hd nal, Some (dummy_loc, ind, nparams, List.tl nal)), Some p
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 4b0adabbd..3068f97c2 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -54,5 +54,5 @@ val it_destRLambda_or_LetIn_names : int -> rawconstr -> name list * rawconstr
val simple_cases_matrix_of_branches :
inductive -> int list -> rawconstr list -> cases_clauses
val return_type_of_predicate :
- inductive -> int -> rawconstr -> predicate_pattern * rawconstr option
+ inductive -> int -> int -> rawconstr -> predicate_pattern * rawconstr option
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index c0902526a..1c290e877 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -120,7 +120,7 @@ let constructor_nrealhyps env (ind,j) =
let inductive_nargs env ind =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
- mip.mind_nrealargs + rel_context_nhyps mib.mind_params_ctxt
+ mib.mind_nparams, mip.mind_nrealargs
(* Annotation for cases *)
let make_case_info env ind style pats_source =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 91425fe79..b4acaafbb 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -60,7 +60,8 @@ val mis_constructor_nargs_env : env -> constructor -> int
val constructor_nrealargs : env -> constructor -> int
val constructor_nrealhyps : env -> constructor -> int
-val inductive_nargs : env -> inductive -> int
+(* Return number of expected parameters and of expected real arguments *)
+val inductive_nargs : env -> inductive -> int * int
type constructor_summary = {
cs_cstr : constructor;
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 5b3eafb30..1453aa218 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -39,7 +39,7 @@ type constr_pattern =
| PSort of rawsort
| PMeta of patvar option
| PIf of constr_pattern * constr_pattern * constr_pattern
- | PCase of (case_style * int array * inductive option * int option)
+ | PCase of (case_style * int array * inductive option * (int * int) option)
* constr_pattern * constr_pattern * constr_pattern array
| PFix of fixpoint
| PCoFix of cofixpoint
@@ -107,7 +107,8 @@ let rec pattern_of_constr t =
| Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
| Case (ci,p,a,br) ->
let cip = ci.ci_pp_info in
- PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,Some cip.ind_nargs),
+ let no = Some (ci.ci_npar,cip.ind_nargs) in
+ PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,no),
pattern_of_constr p,pattern_of_constr a,
Array.map pattern_of_constr br)
| Fix f -> PFix f
@@ -143,23 +144,6 @@ let rec liftn_pattern k n = function
let lift_pattern k = liftn_pattern k 1
-(*
-let rec inst lvar = function
- | PVar id as x -> (try List.assoc id lvar with Not_found -> x)
- | PApp (p,pl) -> PApp (inst lvar p, Array.map (inst lvar) pl)
- | PSoApp (n,pl) -> PSoApp (n, List.map (inst lvar) pl)
- | PLambda (n,a,b) -> PLambda (n,inst lvar a,inst lvar b)
- | PProd (n,a,b) -> PProd (n,inst lvar a,inst lvar b)
- | PLetIn (n,a,b) -> PLetIn (n,inst lvar a,inst lvar b)
- | PCase (ci,po,p,pl) ->
- PCase (ci,option_map (inst lvar) po,inst lvar p,Array.map (inst lvar) pl)
- (* Non recursive *)
- | (PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ as x) -> x
- (* Bound to terms *)
- | (PFix _ | PCoFix _) ->
- error ("Not instantiable pattern")
-*)
-
let rec subst_pattern subst pat = match pat with
| PRef ref ->
let ref',t = subst_global subst ref in
@@ -263,9 +247,9 @@ let rec pat_of_raw metas vars = function
[|pat_of_raw metas vars c|])
| RCases (loc,p,[c,(na,indnames)],brs) ->
let pred,ind_nargs, ind = match p,indnames with
- | Some p, Some (_,ind,nal) ->
+ | Some p, Some (_,ind,n,nal) ->
rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
- Some (List.length nal),Some ind
+ Some (n,List.length nal),Some ind
| _ -> PMeta None, None, None in
let ind = match ind with Some _ -> ind | None ->
match brs with
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 4093f5e11..2ecb85ba4 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -40,7 +40,7 @@ type constr_pattern =
| PSort of rawsort
| PMeta of patvar option
| PIf of constr_pattern * constr_pattern * constr_pattern
- | PCase of (case_style * int array * inductive option * int option)
+ | PCase of (case_style * int array * inductive option * (int * int) option)
* constr_pattern * constr_pattern * constr_pattern array
| PFix of fixpoint
| PCoFix of cofixpoint
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 0fafb916d..d536adcb0 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -47,8 +47,6 @@ type 'a bindings =
type 'a with_bindings = 'a * 'a bindings
-type predicate_pattern = name * (loc * inductive * name list) option
-
type rawconstr =
| RRef of (loc * global_reference)
| RVar of (loc * identifier)
@@ -77,6 +75,9 @@ and fix_kind =
| RFix of ((int option * fix_recursion_order) array * int)
| RCoFix of int
+and predicate_pattern =
+ name * (loc * inductive * int * name list) option
+
and tomatch_tuple = (rawconstr * predicate_pattern) list
and cases_clauses =
@@ -85,7 +86,7 @@ and cases_clauses =
let cases_predicate_names tml =
List.flatten (List.map (function
| (tm,(na,None)) -> [na]
- | (tm,(na,Some (_,_,nal))) -> na::nal) tml)
+ | (tm,(na,Some (_,_,_,nal))) -> na::nal) tml)
(*i - if PRec (_, names, arities, bodies) is in env then arities are
typed in env too and bodies are typed in env enriched by the
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index d20b3fce4..d85ca0158 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -44,8 +44,6 @@ type 'a bindings =
type 'a with_bindings = 'a * 'a bindings
-type predicate_pattern = name * (loc * inductive * name list) option
-
type rawconstr =
| RRef of (loc * global_reference)
| RVar of (loc * identifier)
@@ -74,6 +72,9 @@ and fix_kind =
| RFix of ((int option * fix_recursion_order) array * int)
| RCoFix of int
+and predicate_pattern =
+ name * (loc * inductive * int * name list) option
+
and tomatch_tuple = (rawconstr * predicate_pattern) list
and cases_clauses =
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 01:11:32 +0000