diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/reduction.ml | 36 | ||||
| -rw-r--r-- | kernel/reduction.mli | 4 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/term.ml | 36 | ||||
| -rw-r--r-- | kernel/term.mli | 3 |
6 files changed, 41 insertions, 42 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 6ae5bb931d..e46be516a6 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -133,7 +133,7 @@ let check_params nparams params c = try List.iter2 (fun (n1,t1) (n2,t2) -> - if n1 <> n2 || strip_outer_cast t1 <> strip_outer_cast t2 then + if n1 <> n2 || strip_all_casts t1 <> strip_all_casts t2 then raise (InductiveError BadEntry)) eparams params with Invalid_argument _ -> diff --git a/kernel/reduction.ml b/kernel/reduction.ml index cbc3fe343e..195b4ce18f 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1309,39 +1309,3 @@ let rec whd_ise1_metas sigma = function | DOP2(Cast,c,_) -> whd_ise1_metas sigma c | c -> c - -(* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *) - -let under_outer_cast f = function - | DOP2 (Cast,b,t) -> DOP2 (Cast,f b,f t) - | c -> f c - -let rec strip_all_casts t = - match t with - | DOP2 (Cast, b, _) -> strip_all_casts b - | DOP0 _ as t -> t - (* Cas ad hoc *) - | DOPN(Fix _ as f,v) -> - let n = Array.length v in - let ts = Array.sub v 0 (n-1) in - let b = v.(n-1) in - DOPN(f, Array.append - (Array.map strip_all_casts ts) - [|under_outer_cast strip_all_casts b|]) - | DOPN(CoFix _ as f,v) -> - let n = Array.length v in - let ts = Array.sub v 0 (n-1) in - let b = v.(n-1) in - DOPN(f, Array.append - (Array.map strip_all_casts ts) - [|under_outer_cast strip_all_casts b|]) - | DOP1(oper,c) -> DOP1(oper,strip_all_casts c) - | DOP2(oper,c1,c2) -> DOP2(oper,strip_all_casts c1,strip_all_casts c2) - | DOPN(oper,cl) -> DOPN(oper,Array.map strip_all_casts cl) - | DOPL(oper,cl) -> DOPL(oper,List.map strip_all_casts cl) - | DLAM(na,c) -> DLAM(na,strip_all_casts c) - | DLAMV(na,c) -> DLAMV(na,Array.map (under_outer_cast strip_all_casts) c) - | VAR _ as t -> t - | Rel _ as t -> t - - diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 572d4bcff9..dd06af8adc 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -206,7 +206,3 @@ val find_mcoinductype : val check_mrectype_spec : env -> 'a evar_map -> constr -> constr val minductype_spec : env -> 'a evar_map -> constr -> constr val mrectype_spec : env -> 'a evar_map -> constr -> constr - -(* Special function, which keep the key casts under Fix and MutCase. *) - -val strip_all_casts : constr -> constr diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a4cde03717..6722b023fb 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -367,7 +367,7 @@ let type_one_constructor env_ar nparams ar c = | Prop _ -> cst in let (j,cst'') = safe_machine env_ar c in - let issmall = is_small_type env_par c in + let issmall = is_small_type env_par dc in ((issmall,j), Constraint.union cst' cst'') let logic_constr env c = diff --git a/kernel/term.ml b/kernel/term.ml index 8e9c94c711..31e52ebb3f 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -331,6 +331,42 @@ let rec strip_outer_cast = function | DOP2(Cast,c,_) -> strip_outer_cast c | c -> c + + +(* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *) + +let under_outer_cast f = function + | DOP2 (Cast,b,t) -> DOP2 (Cast,f b,f t) + | c -> f c + +let rec strip_all_casts t = + match t with + | DOP2 (Cast, b, _) -> strip_all_casts b + | DOP0 _ as t -> t + (* Cas ad hoc *) + | DOPN(Fix _ as f,v) -> + let n = Array.length v in + let ts = Array.sub v 0 (n-1) in + let b = v.(n-1) in + DOPN(f, Array.append + (Array.map strip_all_casts ts) + [|under_outer_cast strip_all_casts b|]) + | DOPN(CoFix _ as f,v) -> + let n = Array.length v in + let ts = Array.sub v 0 (n-1) in + let b = v.(n-1) in + DOPN(f, Array.append + (Array.map strip_all_casts ts) + [|under_outer_cast strip_all_casts b|]) + | DOP1(oper,c) -> DOP1(oper,strip_all_casts c) + | DOP2(oper,c1,c2) -> DOP2(oper,strip_all_casts c1,strip_all_casts c2) + | DOPN(oper,cl) -> DOPN(oper,Array.map strip_all_casts cl) + | DOPL(oper,cl) -> DOPL(oper,List.map strip_all_casts cl) + | DLAM(na,c) -> DLAM(na,strip_all_casts c) + | DLAMV(na,c) -> DLAMV(na,Array.map (under_outer_cast strip_all_casts) c) + | VAR _ as t -> t + | Rel _ as t -> t + (* Destructs the product (x:t1)t2 *) let destProd = function | DOP2 (Prod, t1, (DLAM (x,t2))) -> (x,t1,t2) diff --git a/kernel/term.mli b/kernel/term.mli index 869e65ca40..ff296c2dd3 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -260,6 +260,9 @@ val isCast : constr -> bool [strip_outer_cast] (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) val strip_outer_cast : constr -> constr +(* Special function, which keep the key casts under Fix and MutCase. *) +val strip_all_casts : constr -> constr + (* Destructs the product $(x:t_1)t_2$ *) val destProd : constr -> name * constr * constr val hd_of_prod : constr -> constr |