diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 25 | ||||
| -rw-r--r-- | pretyping/cases.mli | 12 | ||||
| -rw-r--r-- | pretyping/cbv.ml | 21 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 8 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 4 |
5 files changed, 52 insertions, 18 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index a793e217d4..d2859b1b4e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -46,8 +46,10 @@ module NamedDecl = Context.Named.Declaration type pattern_matching_error = | BadPattern of constructor * constr | BadConstructor of constructor * inductive - | WrongNumargConstructor of constructor * int - | WrongNumargInductive of inductive * int + | WrongNumargConstructor of + {cstr:constructor; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int} + | WrongNumargInductive of + {ind:inductive; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int} | UnusedClause of cases_pattern list | NonExhaustive of cases_pattern list | CannotInferPredicate of (constr * types) array @@ -65,11 +67,13 @@ let error_bad_constructor ?loc env cstr ind = raise_pattern_matching_error ?loc (env, Evd.empty, BadConstructor (cstr,ind)) -let error_wrong_numarg_constructor ?loc env c n = - raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargConstructor(c,n)) +let error_wrong_numarg_constructor ?loc env ~cstr ~expanded ~nargs ~expected_nassums ~expected_ndecls = + raise_pattern_matching_error ?loc (env, Evd.empty, + WrongNumargConstructor {cstr; expanded; nargs; expected_nassums; expected_ndecls}) -let error_wrong_numarg_inductive ?loc env c n = - raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargInductive(c,n)) +let error_wrong_numarg_inductive ?loc env ~ind ~expanded ~nargs ~expected_nassums ~expected_ndecls = + raise_pattern_matching_error ?loc (env, Evd.empty, + WrongNumargInductive {ind; expanded; nargs; expected_nassums; expected_ndecls}) let list_try_compile f l = let rec aux errors = function @@ -519,13 +523,18 @@ let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with (* Check the constructor has the right number of args *) let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in - if Int.equal (List.length args) nb_args_constr then pat + let nargs = List.length args in + if Int.equal nargs nb_args_constr then pat else try let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args) in DAst.make ?loc @@ PatCstr (cstr, args', alias) with NotAdjustable -> - error_wrong_numarg_constructor ?loc env cstr nb_args_constr + let nlet = List.count (function LocalDef _ -> true | _ -> false) ci.cs_args in + (* In practice, this is already checked at interning *) + error_wrong_numarg_constructor ?loc env ~cstr + (* as if not expanded: *) ~expanded:false ~nargs ~expected_nassums:nb_args_constr + ~expected_ndecls:(nb_args_constr + nlet) else (* Try to insert a coercion *) try diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 9a986bc14c..ade1fbf3d3 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -23,17 +23,21 @@ open Evardefine type pattern_matching_error = | BadPattern of constructor * constr | BadConstructor of constructor * inductive - | WrongNumargConstructor of constructor * int - | WrongNumargInductive of inductive * int + | WrongNumargConstructor of + {cstr:constructor; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int} + | WrongNumargInductive of + {ind:inductive; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int} | UnusedClause of cases_pattern list | NonExhaustive of cases_pattern list | CannotInferPredicate of (constr * types) array exception PatternMatchingError of env * evar_map * pattern_matching_error -val error_wrong_numarg_constructor : ?loc:Loc.t -> env -> constructor -> int -> 'a +val error_wrong_numarg_constructor : + ?loc:Loc.t -> env -> cstr:constructor -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a -val error_wrong_numarg_inductive : ?loc:Loc.t -> env -> inductive -> int -> 'a +val error_wrong_numarg_inductive : + ?loc:Loc.t -> env -> ind:inductive -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a val irrefutable : env -> cases_pattern -> bool diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 2661000a39..bada2c3a60 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -111,15 +111,20 @@ let shift_value n v = * (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1})) * -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti) *) + +let rec mk_fix_subs make_body n env i = + if Int.equal i n then env + else mk_fix_subs make_body n (subs_cons (make_body i) env) (i + 1) + let contract_fixp env ((reci,i),(_,_,bds as bodies)) = let make_body j = FIXP(((reci,j),bodies), env, [||]) in let n = Array.length bds in - subs_cons(Array.init n make_body, env), bds.(i) + mk_fix_subs make_body n env 0, bds.(i) let contract_cofixp env (i,(_,_,bds as bodies)) = let make_body j = COFIXP((j,bodies), env, [||]) in let n = Array.length bds in - subs_cons(Array.init n make_body, env), bds.(i) + mk_fix_subs make_body n env 0, bds.(i) let make_constr_ref n k t = match k with @@ -401,6 +406,10 @@ let rec strip_app = function | APP (args,st) -> APP (args,strip_app st) | s -> TOP +let rec subs_consn v i n s = + if Int.equal i n then s + else subs_consn v (i + 1) n (subs_cons v.(i) s) + (* The main recursive functions * * Go under applications and cases/projections (pushed in the stack), @@ -456,7 +465,7 @@ let rec norm_head info env t stack = (* New rule: for Cbv, Delta does not apply to locally bound variables or red_set info.reds fDELTA *) - let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in + let env' = subs_cons (cbv_stack_term info TOP env b) env in norm_head info env' c stack else (CBN(t,env), stack) (* Should we consider a commutative cut ? *) @@ -526,14 +535,14 @@ and cbv_stack_value info env = function when red_set info.reds fBETA -> let nargs = Array.length args in if nargs == nlams then - cbv_stack_term info stk (subs_cons(args,env)) b + cbv_stack_term info stk (subs_consn args 0 nargs env) b else if nlams < nargs then - let env' = subs_cons(Array.sub args 0 nlams, env) in + let env' = subs_consn args 0 nlams env in let eargs = Array.sub args nlams (nargs-nlams) in cbv_stack_term info (APP(eargs,stk)) env' b else let ctxt' = List.skipn nargs ctxt in - LAM(nlams-nargs,ctxt', b, subs_cons(args,env)) + LAM(nlams-nargs,ctxt', b, subs_consn args 0 nargs env) (* a Fix applied enough -> IOTA *) | (FIXP(fix,env,[||]), stk) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 23145b1629..bd875cf68b 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -245,6 +245,14 @@ let inductive_alldecls env (ind,u) = let inductive_alldecls_env env (ind,u) = inductive_alldecls env (ind,u) [@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"] +let inductive_alltags env ind = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + Context.Rel.to_tags mip.mind_arity_ctxt + +let constructor_alltags env (ind,j) = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + Context.Rel.to_tags (fst mip.mind_nf_lc.(j-1)) + let constructor_has_local_defs env (indsp,j) = let (mib,mip) = Inductive.lookup_mind_specif env indsp in let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 1e2bba9f73..3705d39280 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -138,6 +138,10 @@ val constructor_nrealdecls : env -> constructor -> int val constructor_nrealdecls_env : env -> constructor -> int [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"] +(** @return tags of all decls: true = assumption, false = letin *) +val inductive_alltags : env -> inductive -> bool list +val constructor_alltags : env -> constructor -> bool list + (** Is there local defs in params or args ? *) val constructor_has_local_defs : env -> constructor -> bool val inductive_has_local_defs : env -> inductive -> bool |