diff options
-rw-r--r-- | checker/cic.mli | 10 | ||||
-rw-r--r-- | checker/closure.ml | 63 | ||||
-rw-r--r-- | checker/closure.mli | 5 | ||||
-rw-r--r-- | checker/inductive.ml | 4 | ||||
-rw-r--r-- | checker/reduction.ml | 4 | ||||
-rw-r--r-- | checker/subtyping.ml | 19 | ||||
-rw-r--r-- | kernel/closure.ml | 4 | ||||
-rw-r--r-- | kernel/closure.mli | 4 | ||||
-rw-r--r-- | kernel/reduction.ml | 8 |
9 files changed, 64 insertions, 57 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index cd6d0afee..c1d7b0d73 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -196,6 +196,7 @@ type projection_body = { proj_npars : int; proj_arg : int; proj_type : constr; (* Type under params *) + proj_eta : constr * constr; (* Eta-expanded term and type *) proj_body : constr; (* For compatibility, the match version *) } @@ -232,6 +233,11 @@ type regular_inductive_arity = { mind_sort : sorts; } +type recursivity_kind = + | Finite (** = inductive *) + | CoFinite (** = coinductive *) + | BiFinite (** = non-recursive, like in "Record" definitions *) + type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity type one_inductive_body = { @@ -283,11 +289,11 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : (constr * constant array) option; + mind_record : (constant array * projection_body array) option; (** Whether the inductive type has been declared as a record, In that case we get its canonical eta-expansion and list of projections. *) - mind_finite : bool; (** Whether the type is inductive or coinductive *) + mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) mind_ntypes : int; (** Number of types in the block *) diff --git a/checker/closure.ml b/checker/closure.ml index 5bd636b16..6f19fc59f 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -689,18 +689,26 @@ let rec reloc_rargs_rec depth stk = let reloc_rargs depth stk = if depth = 0 then stk else reloc_rargs_rec depth stk -let rec drop_parameters depth n stk = - match stk with +let rec try_drop_parameters depth n argstk = + match argstk with Zapp args::s -> let q = Array.length args in - if n > q then drop_parameters depth (n-q) s - else if n = q then reloc_rargs depth s + if n > q then try_drop_parameters depth (n-q) s + else if Int.equal n q then reloc_rargs depth s else let aft = Array.sub args n (q-n) in reloc_rargs depth (append_stack aft s) - | Zshift(k)::s -> drop_parameters (depth-k) n s - | [] -> assert (n=0); [] - | _ -> assert false (* we know that n < stack_args_size(stk) *) + | Zshift(k)::s -> try_drop_parameters (depth-k) n s + | [] -> + if Int.equal n 0 then [] + else raise Not_found + | _ -> assert false + (* strip_update_shift_app only produces Zapp and Zshift items *) + +let drop_parameters depth n argstk = + try try_drop_parameters depth n argstk + with Not_found -> assert false + (* we know that n < stack_args_size(argstk) (if well-typed term) *) (** Projections and eta expansion *) @@ -720,37 +728,22 @@ let rec get_parameters depth n argstk = | _ -> assert false (* strip_update_shift_app only produces Zapp and Zshift items *) -let eta_expand_ind_stack env lft (ind,u) m s (lft, h) = - let mib = lookup_mind (fst ind) env in - match mib.mind_record with - | None -> raise Not_found - | Some (exp,_) -> - let pars = mib.mind_nparams in - let h' = fapp_stack h in - let (depth, args, _) = strip_update_shift_app m s in - let paramargs = get_parameters depth pars args in - let subs = subs_cons (Array.append paramargs [|h'|], subs_id 0) in - let fexp = mk_clos subs exp in - (lft, (fexp, [])) - -let eta_expand_ind_stacks env ind m s h = +let eta_expand_ind_stack env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.mind_record with - | Some (exp,projs) when Array.length projs > 0 -> + | Some (projs,pbs) when Array.length projs > 0 + && mib.mind_finite <> CoFinite -> + (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> + arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) let pars = mib.mind_nparams in - let h' = fapp_stack h in - let (depth, args, _) = strip_update_shift_app m s in - let primitive = Environ.is_projection projs.(0) env in - if primitive then - let s' = drop_parameters depth pars args in - (* Construct, pars1 .. parsm :: arg1...argn :: s ~= (t, []) -> - arg1..argn :: s ~= (proj1 t...projn t) s - *) - let hstack = Array.map (fun p -> { norm = Red; - term = FProj (p, h') }) projs in - s', [Zapp hstack] - else raise Not_found (* disallow eta-exp for non-primitive records *) - | _ -> raise Not_found + let right = fapp_stack (f, s') in + let (depth, args, s) = strip_update_shift_app m s in + (** Try to drop the params, might fail on partially applied constructors. *) + let argss = try_drop_parameters depth pars args in + let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *) + term = FProj (p, right) }) projs in + argss, [Zapp hstack] + | _ -> raise Not_found (* disallow eta-exp for non-primitive records *) let rec project_nth_arg n argstk = match argstk with diff --git a/checker/closure.mli b/checker/closure.mli index 9b152eb6a..03970fc9f 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -124,11 +124,8 @@ and stack = stack_member list val append_stack : fconstr array -> stack -> stack val eta_expand_stack : stack -> stack - -val eta_expand_ind_stack : env -> lift -> pinductive -> fconstr -> stack -> - (lift * (fconstr * stack)) -> lift * (fconstr * stack) -val eta_expand_ind_stacks : env -> inductive -> fconstr -> stack -> +val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (fconstr * stack) -> stack * stack (* To lazy reduce a constr, create a [clos_infos] with diff --git a/checker/inductive.ml b/checker/inductive.ml index f60094cfb..adb9e0347 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -40,14 +40,14 @@ let find_inductive env c = let (t, l) = decompose_app (whd_betadeltaiota env c) in match t with | Ind (ind,_) - when (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l) + when (fst (lookup_mind_specif env ind)).mind_finite != CoFinite -> (ind, l) | _ -> raise Not_found let find_coinductive env c = let (t, l) = decompose_app (whd_betadeltaiota env c) in match t with | Ind (ind,_) - when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l) + when (fst (lookup_mind_specif env ind)).mind_finite == CoFinite -> (ind, l) | _ -> raise Not_found let inductive_params (mib,_) = mib.mind_nparams diff --git a/checker/reduction.ml b/checker/reduction.ml index 7bdc96283..403d27779 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -357,7 +357,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = | FConstruct ((ind2,j2),u2) -> (try let v2, v1 = - eta_expand_ind_stacks (infos_env infos) ind2 hd2 v2 (snd appr1) + eta_expand_ind_stack (infos_env infos) ind2 hd2 v2 (snd appr1) in convert_stacks univ infos lft1 lft2 v1 v2 with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) @@ -370,7 +370,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = match c1 with | FConstruct ((ind1,j1),u1) -> (try let v1, v2 = - eta_expand_ind_stacks (infos_env infos) ind1 hd1 v1 (snd appr2) + eta_expand_ind_stack (infos_env infos) ind1 hd1 v1 (snd appr2) in convert_stacks univ infos lft1 lft2 v1 v2 with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) diff --git a/checker/subtyping.ml b/checker/subtyping.ml index c4688e190..a9a037bce 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -91,7 +91,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= | IndType ((_,0), mib) -> mib | _ -> error () in - let mib2 = subst_mind subst2 mib2 in + let mib2 = subst_mind subst2 mib2 in let check eq f = if not (eq (f mib1) (f mib2)) then error () in let bool_equal (x : bool) (y : bool) = x = y in let u = @@ -101,6 +101,16 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= Univ.UContext.instance mib1.mind_universes) else Univ.Instance.empty in + let eq_projection_body p1 p2 = + let check eq f = if not (eq (f p1) (f p2)) then error () in + check eq_mind (fun x -> x.proj_ind); + check (==) (fun x -> x.proj_npars); + check (==) (fun x -> x.proj_arg); + check (eq_constr) (fun x -> x.proj_type); + check (eq_constr) (fun x -> fst x.proj_eta); + check (eq_constr) (fun x -> snd x.proj_eta); + check (eq_constr) (fun x -> x.proj_body); true + in let check_inductive_type env t1 t2 = (* Due to sort-polymorphism in inductive types, the conclusions of @@ -161,7 +171,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= (arities_of_specif (kn,u) (mib1,p1)) (arities_of_specif (kn,u) (mib2,p2)) in - check bool_equal (fun mib -> mib.mind_finite); + check (==) (fun mib -> mib.mind_finite); check Int.equal (fun mib -> mib.mind_ntypes); assert (Array.length mib1.mind_packets >= 1 && Array.length mib2.mind_packets >= 1); @@ -188,8 +198,9 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let record_equal x y = match x, y with | None, None -> true - | Some (r1,p1), Some (r2,p2) -> - eq_constr r1 r2 && Array.for_all2 eq_con_chk p1 p2 + | Some (p1,pb1), Some (p2,pb2) -> + Array.for_all2 eq_con_chk p1 p2 && + Array.for_all2 eq_projection_body pb1 pb2 | _, _ -> false in check record_equal (fun mib -> mib.mind_record); diff --git a/kernel/closure.ml b/kernel/closure.ml index d0a9ffd64..8851ea2b6 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -854,7 +854,7 @@ let rec get_parameters depth n argstk = (* strip_update_shift_app only produces Zapp and Zshift items *) -(** [eta_expand_ind_stacks env ind c s t] computes stacks correspoding +(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. @@ -863,7 +863,7 @@ let rec get_parameters depth n argstk = @raises Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) -let eta_expand_ind_stacks env ind m s (f, s') = +let eta_expand_ind_stack env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (projs,pbs) when Array.length projs > 0 diff --git a/kernel/closure.mli b/kernel/closure.mli index 8c3eb81f4..adcf25857 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -187,7 +187,7 @@ val whd_val : clos_infos -> fconstr -> constr val whd_stack : clos_infos -> fconstr -> stack -> fconstr * stack -(** [eta_expand_ind_stacks env ind c s t] computes stacks correspoding +(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. @@ -196,7 +196,7 @@ val whd_stack : @raises Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) -val eta_expand_ind_stacks : env -> inductive -> fconstr -> stack -> +val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (fconstr * stack) -> stack * stack (** Conversion auxiliary functions to do step by step normalisation *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 78d2105ab..ebba23165 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -434,7 +434,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | FConstruct ((ind2,j2),u2) -> (try let v2, v1 = - eta_expand_ind_stacks (info_env infos) ind2 hd2 v2 (snd appr1) + eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) @@ -447,7 +447,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = match c1 with | FConstruct ((ind1,j1),u1) -> (try let v1, v2 = - eta_expand_ind_stacks (info_env infos) ind1 hd1 v1 (snd appr2) + eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) @@ -472,14 +472,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FConstruct ((ind1,j1),u1), _) -> (try let v1, v2 = - eta_expand_ind_stacks (info_env infos) ind1 hd1 v1 (snd appr2) + eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | (_, FConstruct ((ind2,j2),u2)) -> (try let v2, v1 = - eta_expand_ind_stacks (info_env infos) ind2 hd2 v2 (snd appr1) + eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) |