diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-05-08 13:43:26 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-08 19:23:51 +0200 |
commit | f912004bbe2c8f77de09cc290c3c687dc4ebf7f8 (patch) | |
tree | eadad13bfd7e178d782bb46a9bd3e0daff84264b | |
parent | 0db1d850b940a5f2351c1ec6e26d1f8087064d40 (diff) |
Adapt the checker to polymorphic universes and projections (untested).
-rw-r--r-- | checker/checker.ml | 3 | ||||
-rw-r--r-- | checker/cic.mli | 58 | ||||
-rw-r--r-- | checker/closure.ml | 147 | ||||
-rw-r--r-- | checker/closure.mli | 20 | ||||
-rw-r--r-- | checker/declarations.ml | 65 | ||||
-rw-r--r-- | checker/environ.ml | 45 | ||||
-rw-r--r-- | checker/environ.mli | 7 | ||||
-rw-r--r-- | checker/indtypes.ml | 29 | ||||
-rw-r--r-- | checker/inductive.ml | 201 | ||||
-rw-r--r-- | checker/inductive.mli | 19 | ||||
-rw-r--r-- | checker/mod_checking.ml | 37 | ||||
-rw-r--r-- | checker/modops.ml | 6 | ||||
-rw-r--r-- | checker/print.ml | 16 | ||||
-rw-r--r-- | checker/reduction.ml | 113 | ||||
-rw-r--r-- | checker/subtyping.ml | 34 | ||||
-rw-r--r-- | checker/term.ml | 97 | ||||
-rw-r--r-- | checker/term.mli | 4 | ||||
-rw-r--r-- | checker/type_errors.ml | 6 | ||||
-rw-r--r-- | checker/type_errors.mli | 6 | ||||
-rw-r--r-- | checker/typeops.ml | 90 | ||||
-rw-r--r-- | checker/typeops.mli | 6 |
21 files changed, 793 insertions, 216 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index b9009da82..f3c583b83 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -297,7 +297,8 @@ let rec explain_exn = function str("\nCantApplyBadType at argument " ^ string_of_int n) | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" | IllFormedRecBody _ -> str"IllFormedRecBody" - | IllTypedRecBody _ -> str"IllTypedRecBody")) + | IllTypedRecBody _ -> str"IllTypedRecBody" + | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints")) | Indtypes.InductiveError e -> hov 0 (str "Error related to inductive types") diff --git a/checker/cic.mli b/checker/cic.mli index d2f785abf..484d64973 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -79,6 +79,10 @@ type 'constr pfixpoint = (int array * int) * 'constr prec_declaration type 'constr pcofixpoint = int * 'constr prec_declaration +type 'a puniverses = 'a Univ.puniverses +type pconstant = constant puniverses +type pinductive = inductive puniverses +type pconstructor = constructor puniverses type constr = | Rel of int @@ -91,12 +95,13 @@ type constr = | Lambda of Name.t * constr * constr | LetIn of Name.t * constr * constr * constr | App of constr * constr array - | Const of constant - | Ind of inductive - | Construct of constructor + | Const of pconstant + | Ind of pinductive + | Construct of pconstructor | Case of case_info * constr * constr * constr array | Fix of constr pfixpoint | CoFix of constr pcofixpoint + | Proj of constant * constr type existential = constr pexistential type rec_declaration = constr prec_declaration @@ -163,7 +168,17 @@ type engagement = ImpredicativeSet (** {6 Representation of constants (Definition/Axiom) } *) -type constant_type = constr + +type template_arity = { + template_param_levels : Univ.universe option list; + template_level : Univ.universe; +} + +type ('a, 'b) declaration_arity = + | RegularArity of 'a + | TemplateArity of 'b + +type constant_type = (constr, rel_context * template_arity) declaration_arity (** Inlining level of parameters at functor applications. This is ignored by the checker. *) @@ -173,11 +188,24 @@ type inline = int option (** A constant can have no body (axiom/parameter), or a transparent body, or an opaque one *) +(** Projections are a particular kind of constant: + always transparent. *) + +type projection_body = { + proj_ind : mutual_inductive; + proj_npars : int; + proj_arg : int; + proj_type : constr; (* Type under params *) + proj_body : constr; (* For compatibility, the match version *) +} + type constant_def = | Undef of inline | Def of constr_substituted | OpaqueDef of lazy_constr +type constant_universes = Univ.universe_context + type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; @@ -185,6 +213,9 @@ type constant_body = { const_body_code : to_patch_substituted; const_constraints : Univ.constraints; const_native_name : native_name ref; + const_polymorphic : bool; (** Is it polymorphic or not *) + const_universes : constant_universes; + const_proj : projection_body option; const_inline_code : bool } (** {6 Representation of mutual inductive types } *) @@ -196,6 +227,13 @@ type recarg = type wf_paths = recarg Rtree.t +type regular_inductive_arity = { + mind_user_arity : constr; + mind_sort : sorts; +} + +type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity + type one_inductive_body = { (** {8 Primitive datas } *) @@ -203,7 +241,7 @@ type one_inductive_body = { mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *) - mind_arity : constr; (** Arity sort and original user arity if monomorphic *) + mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *) mind_consnames : Id.t array; (** Names of the constructors: [cij] *) @@ -245,7 +283,9 @@ type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) - mind_record : bool; (** Whether the inductive type has been declared as a record *) + mind_record : (constr * constant 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 *) @@ -259,7 +299,11 @@ type mutual_inductive_body = { mind_params_ctxt : rel_context; (** The context of parameters (includes let-in declaration) *) - mind_constraints : Univ.constraints; (** Universes constraints enforced by the inductive declaration *) + mind_polymorphic : bool; (** Is it polymorphic or not *) + + mind_universes : Univ.universe_context; (** Local universe variables and constraints *) + + mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) (** {8 Data for native compilation } *) diff --git a/checker/closure.ml b/checker/closure.ml index 831f50454..5bd636b16 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -160,16 +160,19 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] * instantiations (cbv or lazy) are. *) -type table_key = - | ConstKey of constant +type 'a tableKey = + | ConstKey of 'a | VarKey of Id.t | RelKey of int +type table_key = constant puniverses tableKey + module KeyHash = struct type t = table_key let equal k1 k2 = match k1, k2 with - | ConstKey c1, ConstKey c2 -> Constant.UserOrd.equal c1 c2 + | ConstKey (c1,u1), ConstKey (c2,u2) -> Constant.UserOrd.equal c1 c2 + && Univ.Instance.equal u1 u2 | VarKey id1, VarKey id2 -> Id.equal id1 id2 | RelKey i1, RelKey i2 -> Int.equal i1 i2 | (ConstKey _ | VarKey _ | RelKey _), _ -> false @@ -177,7 +180,7 @@ struct open Hashset.Combine let hash = function - | ConstKey c -> combinesmall 1 (Constant.UserOrd.hash c) + | ConstKey (c,u) -> combinesmall 1 (Constant.UserOrd.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) end @@ -223,10 +226,7 @@ let defined_rels flags env = let mind_equiv_infos info = mind_equiv info.i_env -let eq_table_key k1 k2 = - match k1,k2 with - | ConstKey con1 ,ConstKey con2 -> eq_con_chk con1 con2 - | _,_ -> k1=k2 +let eq_table_key = KeyHash.equal let create mk_cl flgs env = { i_flags = flgs; @@ -273,9 +273,10 @@ and fterm = | FAtom of constr (* Metas and Sorts *) | FCast of fconstr * cast_kind * fconstr | FFlex of table_key - | FInd of inductive - | FConstruct of constructor + | FInd of pinductive + | FConstruct of pconstructor | FApp of fconstr * fconstr array + | FProj of constant * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array @@ -305,6 +306,7 @@ let update v1 (no,t) = type stack_member = | Zapp of fconstr array | Zcase of case_info * fconstr * fconstr array + | Zproj of int * int * constant | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -390,6 +392,9 @@ let rec compact_constr (lg, subs as s) c k = let (f',s) = compact_constr s f k in let (v',s) = compact_vect s v k in if f==f' && v==v' then c,s else App(f',v'), s + | Proj (p, t) -> + let (t', s) = compact_constr s t k in + if t' == t then c,s else Proj(p,t'), s | Lambda(n,a,b) -> let (a',s) = compact_constr s a k in let (b',s) = compact_constr s b (k+1) in @@ -459,7 +464,7 @@ let mk_clos e t = | Meta _ | Sort _ -> { norm = Norm; term = FAtom t } | Ind kn -> { norm = Norm; term = FInd kn } | Construct kn -> { norm = Cstr; term = FConstruct kn } - | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _) -> + | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> {norm = Red; term = FCLOS(t,e)} let mk_clos_vect env v = Array.map (mk_clos env) v @@ -478,6 +483,9 @@ let mk_clos_deep clos_fun env t = | App (f,v) -> { norm = Red; term = FApp (clos_fun env f, Array.map (clos_fun env) v) } + | Proj (p,c) -> + { norm = Red; + term = FProj (p, clos_fun env c) } | Case (ci,p,c,v) -> { norm = Red; term = FCases (ci, clos_fun env p, clos_fun env c, @@ -533,6 +541,8 @@ let rec to_constr constr_fun lfts v = | FApp (f,ve) -> App (constr_fun lfts f, Array.map (constr_fun lfts) ve) + | FProj (p,c) -> + Proj (p,constr_fun lfts c) | FLambda _ -> let (na,ty,bd) = destFLambda mk_clos2 v in Lambda (na, constr_fun lfts ty, @@ -584,6 +594,8 @@ let rec zip m stk = | Zcase(ci,p,br)::s -> let t = FCases(ci, p, m, br) in zip {norm=neutr m.norm; term=t} s + | Zproj (i,j,cst) :: s -> + zip {norm=neutr m.norm; term=FProj (cst,m)} s | Zfix(fx,par)::s -> zip fx (par @ append_stack [|m|] s) | Zshift(n)::s -> @@ -660,7 +672,7 @@ let rec get_args n tys f e stk = (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *) let rec eta_expand_stack = function - | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ as e) :: s -> + | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ | Zproj _ as e) :: s -> e :: eta_expand_stack s | [] -> [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]] @@ -690,6 +702,65 @@ let rec drop_parameters depth n stk = | [] -> assert (n=0); [] | _ -> assert false (* we know that n < stack_args_size(stk) *) +(** Projections and eta expansion *) + +let rec get_parameters depth n argstk = + match argstk with + Zapp args::s -> + let q = Array.length args in + if n > q then Array.append args (get_parameters depth (n-q) s) + else if Int.equal n q then [||] + else Array.sub args 0 n + | Zshift(k)::s -> + get_parameters (depth-k) n s + | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *) + if Int.equal n 0 then [||] + else raise Not_found (* Trying to eta-expand a partial application..., should do + eta expansion first? *) + | _ -> 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 mib = lookup_mind (fst ind) env in + match mib.mind_record with + | Some (exp,projs) when Array.length projs > 0 -> + 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 rec project_nth_arg n argstk = + match argstk with + | Zapp args :: s -> + let q = Array.length args in + if n >= q then project_nth_arg (n - q) s + else (* n < q *) args.(n) + | _ -> assert false + (* After drop_parameters we have a purely applicative stack *) + (* Iota reduction: expansion of a fixpoint. * Given a fixpoint and a substitution, returns the corresponding @@ -721,33 +792,44 @@ let contract_fix_vect fix = atom or a subterm that may produce a redex (abstraction, constructor, cofix, letin, constant), or a neutral term (product, inductive) *) -let rec knh m stk = +let rec knh info m stk = match m.term with - | FLIFT(k,a) -> knh a (zshift k stk) - | FCLOS(t,e) -> knht e t (zupdate m stk) + | FLIFT(k,a) -> knh info a (zshift k stk) + | FCLOS(t,e) -> knht info e t (zupdate m stk) | FLOCKED -> assert false - | FApp(a,b) -> knh a (append_stack b (zupdate m stk)) - | FCases(ci,p,t,br) -> knh t (Zcase(ci,p,br)::zupdate m stk) + | FApp(a,b) -> knh info a (append_stack b (zupdate m stk)) + | FCases(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk) | FFix(((ri,n),(_,_,_)),_) -> (match get_nth_arg m ri.(n) stk with - (Some(pars,arg),stk') -> knh arg (Zfix(m,pars)::stk') + (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk') | (None, stk') -> (m,stk')) - | FCast(t,_,_) -> knh t stk + | FCast(t,_,_) -> knh info t stk + + | FProj (p,c) -> + (* if red_set info.i_flags (fCONST p) then *) + (match try Some (lookup_projection p (info.i_env)) with Not_found -> None with + | None -> (m, stk) + | Some pb -> + knh info c (Zproj (pb.proj_npars, pb.proj_arg, p) + :: zupdate m stk)) + (* else (m,stk) *) + (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _) -> (m, stk) (* The same for pure terms *) -and knht e t stk = +and knht info e t stk = match t with | App(a,b) -> - knht e a (append_stack (mk_clos_vect e b) stk) + knht info e a (append_stack (mk_clos_vect e b) stk) | Case(ci,p,t,br) -> - knht e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk) - | Fix _ -> knh (mk_clos2 e t) stk - | Cast(a,_,_) -> knht e a stk - | Rel n -> knh (clos_rel e n) stk + knht info e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk) + | Fix _ -> knh info (mk_clos2 e t) stk + | Cast(a,_,_) -> knht info e a stk + | Rel n -> knh info (clos_rel e n) stk + | Proj (p,c) -> knh info (mk_clos2 e t) stk | (Lambda _|Prod _|Construct _|CoFix _|Ind _| LetIn _|Const _|Var _|Evar _|Meta _|Sort _) -> (mk_clos2 e t, stk) @@ -762,7 +844,7 @@ let rec knr info m stk = (match get_args n tys f e stk with Inl e', s -> knit info e' f s | Inr lam, s -> (lam,s)) - | FFlex(ConstKey kn) when red_set info.i_flags (fCONST kn) -> + | FFlex(ConstKey kn) when red_set info.i_flags (fCONST (fst kn)) -> (match ref_value_cache info (ConstKey kn) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) @@ -774,7 +856,7 @@ let rec knr info m stk = (match ref_value_cache info (RelKey k) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) - | FConstruct(ind,c) when red_set info.i_flags fIOTA -> + | FConstruct((ind,c),u) when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with (depth, args, Zcase(ci,_,br)::s) -> assert (ci.ci_npar>=0); @@ -785,6 +867,10 @@ let rec knr info m stk = let stk' = par @ append_stack [|rarg|] s in let (fxe,fxbd) = contract_fix_vect fx.term in knit info fxe fxbd stk' + | (depth, args, Zproj (n, m, cst)::s) -> + let rargs = drop_parameters depth n args in + let rarg = project_nth_arg m rargs in + kni info rarg s | (_,args,s) -> (m,args@s)) | FCoFix _ when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with @@ -798,10 +884,10 @@ let rec knr info m stk = (* Computes the weak head normal form of a term *) and kni info m stk = - let (hm,s) = knh m stk in + let (hm,s) = knh info m stk in knr info hm s and knit info e t stk = - let (ht,s) = knht e t stk in + let (ht,s) = knht info e t stk in knr info ht s let kh info v stk = fapp_stack(kni info v stk) @@ -823,6 +909,9 @@ let whd_stack infos m stk = (* cache of constants: the body is computed only when needed. *) type clos_infos = fconstr infos +let infos_env x = x.i_env +let infos_flags x = x.i_flags + let create_clos_infos flgs env = create (fun _ -> inject) flgs env diff --git a/checker/closure.mli b/checker/closure.mli index 13bc0c07e..9b152eb6a 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -66,11 +66,13 @@ val betaiotazeta : reds val betadeltaiotanolet : reds (***********************************************************************) -type table_key = - | ConstKey of constant +type 'a tableKey = + | ConstKey of 'a | VarKey of Id.t | RelKey of int +type table_key = constant puniverses tableKey + type 'a infos val ref_value_cache: 'a infos -> table_key -> 'a option val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos @@ -90,9 +92,10 @@ type fterm = | FAtom of constr (* Metas and Sorts *) | FCast of fconstr * cast_kind * fconstr | FFlex of table_key - | FInd of inductive - | FConstruct of constructor + | FInd of pinductive + | FConstruct of pconstructor | FApp of fconstr * fconstr array + | FProj of constant * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array @@ -112,6 +115,7 @@ type fterm = type stack_member = | Zapp of fconstr array | Zcase of case_info * fconstr * fconstr array + | Zproj of int * int * constant | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -121,6 +125,12 @@ 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 -> + (fconstr * stack) -> stack * stack + (* To lazy reduce a constr, create a [clos_infos] with [create_clos_infos], inject the term to reduce with [inject]; then use a reduction function *) @@ -135,6 +145,8 @@ val destFLambda : (* Global and local constant cache *) type clos_infos val create_clos_infos : reds -> env -> clos_infos +val infos_env : clos_infos -> env +val infos_flags : clos_infos -> reds (* Reduction function *) diff --git a/checker/declarations.ml b/checker/declarations.ml index 4dd814d57..f500693ce 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -186,12 +186,12 @@ let make_con_equiv mpu mpc dir l = if mpu == mpc then constant_of_kn knu else constant_of_kn_equiv knu (make_kn mpc dir l) -let subst_con0 sub con = +let subst_con0 sub con u = let kn1,kn2 = user_con con,canonical_con con in let mp1,dir,l = repr_kn kn1 in let mp2,_,_ = repr_kn kn2 in let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in - let dup con = con, Const con in + let dup con = con, Const (con, u) in let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in match constant_of_delta_with_inline resolve con' with | Some t -> con', t @@ -205,13 +205,21 @@ let subst_con0 sub con = let rec map_kn f f' c = let func = map_kn f f' in match c with - | Const kn -> (try snd (f' kn) with No_subst -> c) - | Ind (kn,i) -> + | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c) + | Proj (kn,t) -> + let kn' = + try fst (f' kn Univ.Instance.empty) + with No_subst -> kn + in + let t' = func t in + if kn' == kn && t' == t then c + else Proj (kn', t') + | Ind ((kn,i),u) -> let kn' = f kn in - if kn'==kn then c else Ind (kn',i) - | Construct ((kn,i),j) -> + if kn'==kn then c else Ind ((kn',i),u) + | Construct (((kn,i),j),u) -> let kn' = f kn in - if kn'==kn then c else Construct ((kn',i),j) + if kn'==kn then c else Construct (((kn',i),j),u) | Case (ci,p,ct,l) -> let ci_ind = let (kn,i) = ci.ci_ind in @@ -491,8 +499,35 @@ let eq_wf_paths = Rtree.equal eq_recarg with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn *) -let subst_arity sub s = subst_mps sub s +let subst_decl_arity f g sub ar = + match ar with + | RegularArity x -> + let x' = f sub x in + if x' == x then ar + else RegularArity x' + | TemplateArity x -> + let x' = g sub x in + if x' == x then ar + else TemplateArity x' + +let map_decl_arity f g = function + | RegularArity a -> RegularArity (f a) + | TemplateArity a -> TemplateArity (g a) + + +let subst_rel_declaration sub (id,copt,t as x) = + let copt' = Option.smartmap (subst_mps sub) copt in + let t' = subst_mps sub t in + if copt == copt' && t == t' then x else (id,copt',t') + +let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) + +let subst_template_cst_arity sub (ctx,s as arity) = + let ctx' = subst_rel_context sub ctx in + if ctx==ctx' then arity else (ctx',s) + +let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s (* TODO: should be changed to non-coping after Term.subst_mps *) (* NB: we leave bytecode and native code fields untouched *) @@ -501,6 +536,18 @@ let subst_const_body sub cb = const_body = subst_constant_def sub cb.const_body; const_type = subst_arity sub cb.const_type } + +let subst_regular_ind_arity sub s = + let uar' = subst_mps sub s.mind_user_arity in + if uar' == s.mind_user_arity then s + else { mind_user_arity = uar'; mind_sort = s.mind_sort } + +let subst_template_ind_arity sub s = s + +(* FIXME records *) +let subst_ind_arity = + subst_decl_arity subst_regular_ind_arity subst_template_ind_arity + let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; mind_consnrealdecls = mbp.mind_consnrealdecls; @@ -508,7 +555,7 @@ let subst_mind_packet sub mbp = mind_typename = mbp.mind_typename; mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; - mind_arity = subst_arity sub mbp.mind_arity; + mind_arity = subst_ind_arity sub mbp.mind_arity; mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; diff --git a/checker/environ.ml b/checker/environ.ml index 79234e9e2..d650e194e 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -84,6 +84,9 @@ let add_constraints c env = { env with env_stratification = { s with env_universes = merge_constraints c s.env_universes } } +let check_constraints cst env = + Univ.check_constraints cst env.env_stratification.env_universes + (* Global constants *) let lookup_constant kn env = @@ -104,20 +107,54 @@ let add_constant kn cs env = type const_evaluation_result = NoBody | Opaque +(* Constant types *) + +let universes_and_subst_of cb u = + let univs = cb.const_universes in + let subst = Univ.make_universe_subst u univs in + subst, Univ.instantiate_univ_context subst univs + +let map_regular_arity f = function + | RegularArity a as ar -> + let a' = f a in + if a' == a then ar else RegularArity a' + | TemplateArity _ -> assert false + +(* constant_type gives the type of a constant *) +let constant_type env (kn,u) = + let cb = lookup_constant kn env in + if cb.const_polymorphic then + let subst, csts = universes_and_subst_of cb u in + (map_regular_arity (subst_univs_constr subst) cb.const_type, csts) + else cb.const_type, Univ.Constraint.empty + exception NotEvaluableConst of const_evaluation_result -let constant_value env kn = +let constant_value env (kn,u) = let cb = lookup_constant kn env in - match cb.const_body with - | Def l_body -> force_constr l_body + match cb.const_body with + | Def l_body -> + let b = force_constr l_body in + if cb.const_polymorphic then + let subst = Univ.make_universe_subst u cb.const_universes in + subst_univs_constr subst b + else b | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) (* A global const is evaluable if it is defined and not opaque *) let evaluable_constant cst env = - try let _ = constant_value env cst in true + try let _ = constant_value env (cst, Univ.Instance.empty) in true with Not_found | NotEvaluableConst _ -> false +let is_projection cst env = + not (Option.is_empty (lookup_constant cst env).const_proj) + +let lookup_projection cst env = + match (lookup_constant cst env).const_proj with + | Some pb -> pb + | None -> anomaly ("lookup_projection: constant is not a projection") + (* Mutual Inductives *) let scrape_mind env kn= try diff --git a/checker/environ.mli b/checker/environ.mli index 46b390d0a..d3448b127 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -39,15 +39,20 @@ val push_rec_types : name array * constr array * 'a -> env -> env (* Universes *) val universes : env -> Univ.universes val add_constraints : Univ.constraints -> env -> env +val check_constraints : Univ.constraints -> env -> bool (* Constants *) val lookup_constant : constant -> env -> Cic.constant_body val add_constant : constant -> Cic.constant_body -> env -> env +val constant_type : env -> constant puniverses -> constant_type Univ.constrained type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result -val constant_value : env -> constant -> constr +val constant_value : env -> constant puniverses -> constr val evaluable_constant : constant -> env -> bool +val is_projection : constant -> env -> bool +val lookup_projection : constant -> env -> projection_body + (* Inductives *) val mind_equiv : env -> inductive -> inductive -> bool diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 5927e1633..bfc20d7f8 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -139,12 +139,15 @@ let typecheck_arity env params inds = let nparamargs = rel_context_nhyps params in let nparamdecls = rel_context_length params in let check_arity arctxt = function - mar -> - let _ = infer_type env mar in - mar in - (* | Polymorphic par -> *) - (* check_polymorphic_arity env params par; *) - (* it_mkProd_or_LetIn (Sort(Type par.poly_level)) arctxt in *) + | RegularArity mar -> + let ar = mar.mind_user_arity in + let _ = infer_type env ar in + conv env (it_mkProd_or_LetIn (Sort mar.mind_sort) arctxt) ar; + ar + | TemplateArity par -> + check_polymorphic_arity env params par; + it_mkProd_or_LetIn (Sort(Type par.template_level)) arctxt + in let env_arities = Array.fold_left (fun env_ar ind -> @@ -189,8 +192,8 @@ let check_predicativity env s small level = let sort_of_ind = function - mar -> snd (destArity mar) - (* | Polymorphic par -> Type par.poly_level *) + | RegularArity mar -> mar.mind_sort + | TemplateArity par -> Type par.template_level let all_sorts = [InProp;InSet;InType] let small_sorts = [InProp;InSet] @@ -371,12 +374,12 @@ let abstract_mind_lc env ntyps npars lc = let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra) -let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = +let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) = let auxntyp = 1 in let specif = lookup_mind_specif env mi in let env' = push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive env specif) lpar) env in + hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) env in let ra_env' = (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in @@ -429,7 +432,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc else failwith_non_pos_list n ntypes (x::largs) (* accesses to the environment are not factorised, but is it worth it? *) - and check_positive_imbr (env,n,ntypes,ra_env as ienv) (mi, largs) = + and check_positive_imbr (env,n,ntypes,ra_env as ienv) ((mi,u), largs) = let (mib,mip) = lookup_mind_specif env mi in let auxnpar = mib.mind_nparams_rec in let nonrecpar = mib.mind_nparams - auxnpar in @@ -447,7 +450,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in (* Extends the environment with a variable corresponding to the inductive def *) - let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in + let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),lpar) in (* Parameters expressed in env' *) let lpar' = List.map (lift auxntyp) lpar in let irecargs = @@ -528,7 +531,7 @@ let check_positivity env_ar mind params nrecp inds = let check_inductive env kn mib = Flags.if_verbose ppnl (str " checking ind: " ++ pr_mind kn); pp_flush (); (* check mind_constraints: should be consistent with env *) - let env = add_constraints mib.mind_constraints env in + let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in (* check mind_record : TODO ? check #constructor = 1 ? *) (* check mind_finite : always OK *) (* check mind_ntypes *) diff --git a/checker/inductive.ml b/checker/inductive.ml index b32379b35..55acd9f97 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -39,32 +39,58 @@ let find_rectype env c = let find_inductive env c = let (t, l) = decompose_app (whd_betadeltaiota env c) in match t with - | Ind ind + | Ind (ind,_) when (fst (lookup_mind_specif env ind)).mind_finite -> (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 + | Ind (ind,_) when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l) | _ -> raise Not_found let inductive_params (mib,_) = mib.mind_nparams +(** Polymorphic inductives *) + +let make_inductive_subst mib u = + if mib.mind_polymorphic then + make_universe_subst u mib.mind_universes + else Univ.empty_subst + +let inductive_params_ctxt (mib,u) = + let subst = make_inductive_subst mib u in + subst_univs_context subst mib.mind_params_ctxt + +let inductive_instance mib = + if mib.mind_polymorphic then + UContext.instance mib.mind_universes + else Instance.empty + +let inductive_context mib = + if mib.mind_polymorphic then + mib.mind_universes + else UContext.empty + +let instantiate_inductive_constraints mib subst = + if mib.mind_polymorphic then + instantiate_univ_context subst mib.mind_universes + else Constraint.empty + (************************************************************************) (* Build the substitution that replaces Rels by the appropriate *) (* inductives *) -let ind_subst mind mib = +let ind_subst mind mib u = let ntypes = mib.mind_ntypes in - let make_Ik k = Ind (mind,ntypes-k-1) in + let make_Ik k = Ind ((mind,ntypes-k-1),u) in List.init ntypes make_Ik (* Instantiate inductives in constructor type *) -let constructor_instantiate mind mib c = - let s = ind_subst mind mib in - substl s c +let constructor_instantiate mind u subst mib c = + let s = ind_subst mind mib u in + substl s (subst_univs_constr subst c) let instantiate_params full t args sign = let fail () = @@ -83,13 +109,16 @@ let instantiate_params full t args sign = if rem_args <> [] then fail(); substl subs ty -let full_inductive_instantiate mib params sign = +let full_inductive_instantiate mib u params sign = let dummy = Prop Null in let t = mkArity (sign,dummy) in - fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) + let subst = make_inductive_subst mib u in + let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in + subst_univs_context subst ar -let full_constructor_instantiate ((mind,_),(mib,_),params) = - let inst_ind = constructor_instantiate mind mib in +let full_constructor_instantiate ((mind,_),u,(mib,_),params) = + let subst = make_inductive_subst mib u in + let inst_ind = constructor_instantiate mind u subst mib in (fun t -> instantiate_params true (inst_ind t) params mib.mind_params_ctxt) @@ -173,25 +202,82 @@ let rec make_subst env = function | [], _, _ -> assert false -(* let instantiate_universes env ctx ar argsorts = *) -(* let args = Array.to_list argsorts in *) -(* let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in *) -(* let level = subst_large_constraints subst ar.poly_level in *) -(* ctx, *) -(* if is_type0m_univ level then Prop Null *) -(* else if is_type0_univ level then Prop Pos *) -(* else Type level *) - -let type_of_inductive_knowing_parameters env mip paramtyps = - mip.mind_arity - (* | Polymorphic ar -> *) - (* let ctx = List.rev mip.mind_arity_ctxt in *) - (* let ctx,s = instantiate_universes env ctx ar paramtyps in *) - (* mkArity (List.rev ctx,s) *) + +exception SingletonInductiveBecomesProp of Id.t + +let instantiate_universes env ctx ar argsorts = + let args = Array.to_list argsorts in + let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in + let level = subst_large_constraints subst ar.template_level in + let ty = + (* Singleton type not containing types are interpretable in Prop *) + if is_type0m_univ level then Prop Null + (* Non singleton type not containing types are interpretable in Set *) + else if is_type0_univ level then Prop Pos + (* This is a Type with constraints *) + else Type level + in + (ctx, ty) + +(* Type of an inductive type *) + +let is_prop_sort = function + | Prop Null -> true + | _ -> false + +let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps = + match mip.mind_arity with + | RegularArity a -> + if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty) + else + let subst = make_inductive_subst mib u in + (subst_univs_constr subst a.mind_user_arity, subst) + | TemplateArity ar -> + let ctx = List.rev mip.mind_arity_ctxt in + let ctx,s = instantiate_universes env ctx ar paramtyps in + (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. + the situation where a non-Prop singleton inductive becomes Prop + when applied to Prop params *) + if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s + then raise (SingletonInductiveBecomesProp mip.mind_typename); + mkArity (List.rev ctx,s), Univ.LMap.empty + +let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = + match mip.mind_arity with + | RegularArity a -> + if not mib.mind_polymorphic then a.mind_user_arity + else + let subst = make_inductive_subst mib u in + (subst_univs_constr subst a.mind_user_arity) + | TemplateArity ar -> + let ctx = List.rev mip.mind_arity_ctxt in + let ctx,s = instantiate_universes env ctx ar paramtyps in + (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. + the situation where a non-Prop singleton inductive becomes Prop + when applied to Prop params *) + if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s + then raise (SingletonInductiveBecomesProp mip.mind_typename); + mkArity (List.rev ctx,s) + +let type_of_inductive env pind = + type_of_inductive_gen env pind [||] + +let constrained_type_of_inductive env ((mib,mip),u as pind) = + let ty, subst = type_of_inductive_subst env pind [||] in + let cst = instantiate_inductive_constraints mib subst in + (ty, cst) + +let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args = + let ty, subst = type_of_inductive_subst env pind args in + let cst = instantiate_inductive_constraints mib subst in + (ty, cst) + +let type_of_inductive_knowing_parameters env mip args = + type_of_inductive_gen env mip args (* Type of a (non applied) inductive type *) -let type_of_inductive env (_,mip) = +let type_of_inductive env mip = type_of_inductive_knowing_parameters env mip [||] (* The max of an array of universes *) @@ -207,17 +293,36 @@ let max_inductive_sort = (************************************************************************) (* Type of a constructor *) -let type_of_constructor cstr (mib,mip) = +let type_of_constructor_subst cstr u subst (mib,mip) = let ind = inductive_of_constructor cstr in let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in - if i > nconstr then error "Not enough constructors in the type"; - constructor_instantiate (fst ind) mib specif.(i-1) + if i > nconstr then error "Not enough constructors in the type."; + let c = constructor_instantiate (fst ind) u subst mib specif.(i-1) in + c + +let type_of_constructor_gen (cstr,u) (mib,mip as mspec) = + let subst = make_inductive_subst mib u in + type_of_constructor_subst cstr u subst mspec, subst + +let type_of_constructor cstru mspec = + fst (type_of_constructor_gen cstru mspec) -let arities_of_specif kn (mib,mip) = +let type_of_constructor_in_ctx cstr (mib,mip as mspec) = + let u = UContext.instance mib.mind_universes in + let c = type_of_constructor_gen (cstr, u) mspec in + (fst c, mib.mind_universes) + +let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = + let ty, subst = type_of_constructor_gen cstru ind in + let cst = instantiate_inductive_constraints mib subst in + (ty, cst) + +let arities_of_specif (kn,u) (mib,mip) = let specif = mip.mind_nf_lc in - Array.map (constructor_instantiate kn mib) specif + let subst = make_inductive_subst mib u in + Array.map (constructor_instantiate kn u subst mib) specif @@ -234,14 +339,16 @@ let error_elim_expln kp ki = (* Get type of inductive, with parameters instantiated *) let inductive_sort_family mip = - family_of_sort (snd (destArity mip.mind_arity)) + match mip.mind_arity with + | RegularArity s -> family_of_sort s.mind_sort + | TemplateArity _ -> InType let mind_arity mip = mip.mind_arity_ctxt, inductive_sort_family mip -let get_instantiated_arity (mib,mip) params = +let get_instantiated_arity (ind,u) (mib,mip) params = let sign, s = mind_arity mip in - full_inductive_instantiate mib params sign, s + full_inductive_instantiate mib u params sign, s let elim_sorts (_,mip) = mip.mind_kelim @@ -269,7 +376,7 @@ let check_allowed_sort ksort specif = raise (LocalArity (Some(ksort,s,error_elim_expln ksort s))) let is_correct_arity env c (p,pj) ind specif params = - let arsign,_ = get_instantiated_arity specif params in + let arsign,_ = get_instantiated_arity ind specif params in let rec srec env pt ar = let pt' = whd_betadeltaiota env pt in match pt', ar with @@ -305,9 +412,9 @@ let is_correct_arity env c (p,pj) ind specif params = (* [p] is the predicate, [i] is the constructor number (starting from 0), and [cty] is the type of the constructor (params not instantiated) *) -let build_branches_type ind (_,mip as specif) params dep p = +let build_branches_type (ind,u) (_,mip as specif) params dep p = let build_one_branch i cty = - let typi = full_constructor_instantiate (ind,specif,params) cty in + let typi = full_constructor_instantiate (ind,u,specif,params) cty in let (args,ccl) = decompose_prod_assum typi in let nargs = rel_context_length args in let (_,allargs) = decompose_app ccl in @@ -316,7 +423,7 @@ let build_branches_type ind (_,mip as specif) params dep p = if dep then let cstr = ith_constructor_of_inductive ind (i+1) in let dep_cstr = - applist (Construct cstr,lparams@extended_rel_list 0 args) in + applist (Construct (cstr,u),lparams@extended_rel_list 0 args) in vargs @ [dep_cstr] else vargs in @@ -330,12 +437,12 @@ let build_case_type dep p c realargs = let args = if dep then realargs@[c] else realargs in beta_appvect p (Array.of_list args) -let type_case_branches env (ind,largs) (p,pj) c = - let specif = lookup_mind_specif env ind in +let type_case_branches env (pind,largs) (p,pj) c = + let specif = lookup_mind_specif env (fst pind) in let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in - let dep = is_correct_arity env c (p,pj) ind specif params in - let lc = build_branches_type ind specif params dep p in + let dep = is_correct_arity env c (p,pj) pind specif params in + let lc = build_branches_type pind specif params dep p in let ty = build_case_type dep p c realargs in (lc, ty) @@ -724,11 +831,11 @@ let check_one_fix renv recpos def = else check_rec_call renv' [] body) bodies - | Const kn -> + | Const (kn,u) -> if evaluable_constant kn renv.env then try List.iter (check_rec_call renv []) l with (FixGuardError _ ) -> - let value = (applist(constant_value renv.env kn, l)) in + let value = (applist(constant_value renv.env (kn,u), l)) in check_rec_call renv stack value else List.iter (check_rec_call renv []) l @@ -761,6 +868,8 @@ let check_one_fix renv recpos def = | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) + | Proj (p, c) -> check_rec_call renv [] c + and check_nested_fix_body renv decr recArgsDecrArg body = if decr = 0 then check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body @@ -859,7 +968,7 @@ let check_one_cofix env nbfix def deftype = else if not(List.for_all (noccur_with_meta n nbfix) args) then raise (CoFixGuardError (env,NestedRecursiveOccurrences)) - | Construct (_,i as cstr_kn) -> + | Construct ((_,i as cstr_kn),u) -> let lra = vlra.(i-1) in let mI = inductive_of_constructor cstr_kn in let (mib,mip) = lookup_mind_specif env mI in diff --git a/checker/inductive.mli b/checker/inductive.mli index 082bdae19..e223af0c9 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -14,7 +14,7 @@ open Environ (*s Extracting an inductive type from a construction *) -val find_rectype : env -> constr -> inductive * constr list +val find_rectype : env -> constr -> pinductive * constr list type mind_specif = mutual_inductive_body * one_inductive_body @@ -22,12 +22,15 @@ type mind_specif = mutual_inductive_body * one_inductive_body Raises [Not_found] if the inductive type is not found. *) val lookup_mind_specif : env -> inductive -> mind_specif -val type_of_inductive : env -> mind_specif -> constr +val make_inductive_subst : mutual_inductive_body -> Univ.universe_instance -> Univ.universe_subst +val inductive_instance : mutual_inductive_body -> Univ.universe_instance + +val type_of_inductive : env -> mind_specif puniverses -> constr (* Return type as quoted by the user *) -val type_of_constructor : constructor -> mind_specif -> constr +val type_of_constructor : pconstructor -> mind_specif -> constr -val arities_of_specif : mutual_inductive -> mind_specif -> constr array +val arities_of_specif : mutual_inductive puniverses -> mind_specif -> constr array (* [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression: @@ -36,7 +39,7 @@ val arities_of_specif : mutual_inductive -> mind_specif -> constr array introduced by products) and the type for the whole expression. *) val type_case_branches : - env -> inductive * constr list -> constr * constr -> constr + env -> pinductive * constr list -> constr * constr -> constr -> constr array * constr (* Check a [case_info] actually correspond to a Case expression on the @@ -50,12 +53,12 @@ val check_cofix : env -> cofixpoint -> unit (*s Support for sort-polymorphic inductive types *) val type_of_inductive_knowing_parameters : - env -> one_inductive_body -> constr array -> constr + env -> mind_specif puniverses -> constr array -> constr val max_inductive_sort : sorts array -> Univ.universe -(* val instantiate_universes : env -> rel_context -> *) -(* inductive_arity -> constr array -> rel_context * sorts *) +val instantiate_universes : env -> rel_context -> + template_arity -> constr array -> rel_context * sorts (***************************************************************) (* Debug *) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 53316a2cb..12a97bf68 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -14,30 +14,31 @@ open Environ (** {6 Checking constants } *) -(* let refresh_arity ar = *) -(* let ctxt, hd = decompose_prod_assum ar in *) -(* match hd with *) -(* Sort (Type u) when not (Univ.is_univ_variable u) -> *) -(* let u' = Univ.fresh_local_univ() in *) -(* mkArity (ctxt,Type u'), *) -(* Univ.enforce_leq u u' Univ.empty_constraint *) -(* | _ -> ar, Univ.empty_constraint *) +let refresh_arity ar = + let ctxt, hd = decompose_prod_assum ar in + match hd with + Sort (Type u) when not (Univ.is_univ_variable u) -> + let u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in + mkArity (ctxt,Prop Null), + Univ.enforce_leq u u' Univ.empty_constraint + | _ -> ar, Univ.empty_constraint let check_constant_declaration env kn cb = Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn); -(* let env = add_constraints cb.const_constraints env in*) + let env = add_constraints (Univ.UContext.constraints cb.const_universes) env in (match cb.const_type with - ty -> - let env' = add_constraints cb.const_constraints env in (*MS: FIXME*) - let _ = infer_type env' ty in - (match body_of_constant cb with + RegularArity ty -> + let ty, cu = refresh_arity ty in + let envty = add_constraints cu env in + let _ = infer_type envty ty in + (match body_of_constant cb with | Some bd -> - let j = infer env' bd in - conv_leq env' j ty + let j = infer envty bd in + conv_leq envty j ty | None -> ()) - (* | PolymorphicArity(ctxt,par) -> *) - (* let _ = check_ctxt env ctxt in *) - (* check_polymorphic_arity env ctxt par *)); + | TemplateArity(ctxt,par) -> + let _ = check_ctxt env ctxt in + check_polymorphic_arity env ctxt par); add_constant kn cb env diff --git a/checker/modops.ml b/checker/modops.ml index 2d20dd0f3..c27c5d598 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -90,7 +90,11 @@ let strengthen_const mp_from l cb resolver = | _ -> let con = Constant.make2 mp_from l in (* let con = constant_of_delta resolver con in*) - { cb with const_body = Def (Declarations.from_val (Const con)) } + let u = + if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + else Univ.Instance.empty + in + { cb with const_body = Def (Declarations.from_val (Const (con,u))) } let rec strengthen_mod mp_from mp_to mb = if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then diff --git a/checker/print.ml b/checker/print.ml index f25b8cf09..8a5464dae 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -10,6 +10,8 @@ open Format open Cic open Names +let print_instance i = Pp.pp (Univ.Instance.pr i) + let print_pure_constr csr = let rec term_display c = match c with | Rel n -> print_string "#"; print_int n @@ -43,19 +45,22 @@ let print_pure_constr csr = Array.iter (fun x -> print_space (); box_display x) l; print_string ")" | Evar _ -> print_string "Evar#" - | Const c -> print_string "Cons("; + | Const (c,u) -> print_string "Cons("; sp_con_display c; + print_string ","; print_instance u; print_string ")" - | Ind (sp,i) -> + | Ind ((sp,i),u) -> print_string "Ind("; sp_display sp; print_string ","; print_int i; + print_string ","; print_instance u; print_string ")" - | Construct ((sp,i),j) -> + | Construct (((sp,i),j),u) -> print_string "Constr("; sp_display sp; print_string ","; - print_int i; print_string ","; print_int j; print_string ")" + print_int i; print_string ","; print_int j; + print_string ","; print_instance u; print_string ")" | Case (ci,p,c,bl) -> open_vbox 0; print_string "<"; box_display p; print_string ">"; @@ -94,6 +99,9 @@ let print_pure_constr csr = print_cut(); done in print_string"{"; print_fix (); print_string"}" + | Proj (p, c) -> + print_string "Proj("; sp_con_display p; print_string ","; + box_display c; print_string ")" and box_display c = open_hovbox 1; term_display c; close_box() diff --git a/checker/reduction.ml b/checker/reduction.ml index 54d79484e..384b9ad7f 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -50,6 +50,7 @@ let compare_stack_shape stk1 stk2 = type lft_constr_stack_elt = Zlapp of (lift * fconstr) array + | Zlproj of Names.constant * lift | Zlfix of (lift * fconstr) * lft_constr_stack | Zlcase of case_info * lift * fconstr * fconstr array and lft_constr_stack = lft_constr_stack_elt list @@ -68,6 +69,8 @@ let pure_stack lfts stk = | (Zshift n,(l,pstk)) -> (el_shft n l, pstk) | (Zapp a, (l,pstk)) -> (l,zlapp (Array.map (fun t -> (l,t)) a) pstk) + | (Zproj (n,m,c), (l,pstk)) -> + (l, Zlproj (c,l)::pstk) | (Zfix(fx,a),(l,pstk)) -> let (lfx,pa) = pure_rec l a in (l, Zlfix((lfx,fx),pa)::pstk) @@ -116,6 +119,10 @@ type 'a conversion_function = env -> 'a -> 'a -> unit exception NotConvertible exception NotConvertibleVect of int +let convert_universes univ u u' = + if Univ.Instance.check_eq univ u u' then () + else raise NotConvertible + let compare_stacks f fmind lft1 stk1 lft2 stk2 = let rec cmp_rec pstk1 pstk2 = match (pstk1,pstk2) with @@ -163,6 +170,7 @@ let rec no_arg_available = function | Zupdate _ :: stk -> no_arg_available stk | Zshift _ :: stk -> no_arg_available stk | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk + | Zproj _ :: _ -> true | Zcase _ :: _ -> true | Zfix _ :: _ -> true @@ -174,6 +182,7 @@ let rec no_nth_arg_available n = function let k = Array.length v in if n >= k then no_nth_arg_available (n-k) stk else false + | Zproj _ :: _ -> true | Zcase _ :: _ -> true | Zfix _ :: _ -> true @@ -182,6 +191,7 @@ let rec no_case_available = function | Zupdate _ :: stk -> no_case_available stk | Zshift _ :: stk -> no_case_available stk | Zapp _ :: stk -> no_case_available stk + | Zproj (_,_,_) :: _ -> false | Zcase _ :: _ -> false | Zfix _ :: _ -> true @@ -192,7 +202,7 @@ let in_whnf (t,stk) = | FConstruct _ -> no_case_available stk | FCoFix _ -> no_case_available stk | FFix(((ri,n),(_,_,_)),_) -> no_nth_arg_available ri.(n) stk - | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _) -> true + | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true | FLOCKED -> assert false let oracle_order fl1 fl2 = @@ -201,6 +211,15 @@ let oracle_order fl1 fl2 = | _, ConstKey _ -> true | _ -> false +let unfold_projection infos p c = + (* if RedFlags.red_set infos.i_flags (RedFlags.fCONST p) then *) + (match try Some (lookup_projection p (infos_env infos)) with Not_found -> None with + | Some pb -> + let s = Zproj (pb.proj_npars, pb.proj_arg, p) in + Some (c, s) + | None -> None) + (* else None *) + (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[])) @@ -255,19 +274,49 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = let (app1,app2) = if oracle_order fl1 fl2 then match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) - | None -> - (match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) - | None -> raise NotConvertible) + | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) + | None -> + (match unfold_reference infos fl2 with + | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) + | None -> raise NotConvertible) else match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) - | None -> - (match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) - | None -> raise NotConvertible) in - eqappr univ cv_pb infos app1 app2) + | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) + | None -> + (match unfold_reference infos fl1 with + | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) + | None -> raise NotConvertible) in + eqappr univ cv_pb infos app1 app2) + + | (FProj (p1,c1), FProj (p2, c2)) -> + (* Projections: prefer unfolding to first-order unification, + which will happen naturally if the terms c1, c2 are not in constructor + form *) + (match unfold_projection infos p1 c1 with + | Some (def1,s1) -> + eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2 + | None -> + match unfold_projection infos p2 c2 with + | Some (def2,s2) -> + eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2)) + | None -> + if Names.eq_con_chk p1 p2 && compare_stack_shape v1 v2 then + let () = ccnv univ CONV infos el1 el2 c1 c2 in + convert_stacks univ infos lft1 lft2 v1 v2 + else (* Two projections in WHNF: unfold *) + raise NotConvertible) + + | (FProj (p1,c1), t2) -> + (match unfold_projection infos p1 c1 with + | Some (def1,s1) -> + eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2 + | None -> raise NotConvertible) + + | (_, FProj (p2,c2)) -> + (match unfold_projection infos p2 c2 with + | Some (def2,s2) -> + eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2)) + | None -> raise NotConvertible) (* other constructors *) | (FLambda _, FLambda _) -> @@ -300,29 +349,47 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[])) (* only one constant, defined var or defined rel *) - | (FFlex fl1, _) -> + | (FFlex fl1, c2) -> (match unfold_reference infos fl1 with | Some def1 -> eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2 - | None -> raise NotConvertible) - | (_, FFlex fl2) -> + | None -> + match c2 with + | FConstruct ((ind2,j2),u2) -> + (try + let v2, v1 = + eta_expand_ind_stacks (infos_env infos) ind2 hd2 v2 (snd appr1) + in convert_stacks univ infos lft1 lft2 v1 v2 + with Not_found -> raise NotConvertible) + | _ -> raise NotConvertible) + + | (c1, FFlex fl2) -> (match unfold_reference infos fl2 with | Some def2 -> eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2) - | None -> raise NotConvertible) + | None -> + match c1 with + | FConstruct ((ind1,j1),u1) -> + (try let v1, v2 = + eta_expand_ind_stacks (infos_env infos) ind1 hd1 v1 (snd appr2) + in convert_stacks univ infos lft1 lft2 v1 v2 + with Not_found -> raise NotConvertible) + | _ -> raise NotConvertible) (* Inductive types: MutInd MutConstruct Fix Cofix *) - | (FInd ind1, FInd ind2) -> - if mind_equiv_infos infos ind1 ind2 - then - convert_stacks univ infos lft1 lft2 v1 v2 - else raise NotConvertible + | (FInd (ind1,u1), FInd (ind2,u2)) -> + if mind_equiv_infos infos ind1 ind2 + then + (let () = convert_universes univ u1 u2 in + convert_stacks univ infos lft1 lft2 v1 v2) + else raise NotConvertible - | (FConstruct (ind1,j1), FConstruct (ind2,j2)) -> + | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then - convert_stacks univ infos lft1 lft2 v1 v2 + (let () = convert_universes univ u1 u2 in + convert_stacks univ infos lft1 lft2 v1 v2) else raise NotConvertible | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) -> diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 070ed1924..6c66ca60b 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -93,6 +93,15 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= | _ -> error () 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 = + check bool_equal (fun x -> x.mind_polymorphic); + if mib1.mind_polymorphic then ( + check Univ.Instance.equal (fun x -> Univ.UContext.instance x.mind_universes); + UContext.instance mib1.mind_universes) + else Instance.empty + in let check_inductive_type env t1 t2 = (* Due to sort-polymorphism in inductive types, the conclusions of @@ -146,15 +155,13 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= (* params_ctxt done because part of the inductive types *) (* Don't check the sort of the type if polymorphic *) check_inductive_type env - (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2)) + (type_of_inductive env ((mib1,p1),u)) (type_of_inductive env ((mib2,p2),u)) in let check_cons_types i p1 p2 = Array.iter2 (check_conv conv env) - (arities_of_specif kn (mib1,p1)) - (arities_of_specif kn (mib2,p2)) + (arities_of_specif (kn,u) (mib1,p1)) + (arities_of_specif (kn,u) (mib2,p2)) 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 check bool_equal (fun mib -> mib.mind_finite); check Int.equal (fun mib -> mib.mind_ntypes); assert (Array.length mib1.mind_packets >= 1 @@ -179,8 +186,15 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= if kn1 <> kn2 then error () end;*) (* we check that records and their field names are preserved. *) - check bool_equal (fun mib -> mib.mind_record); - if mib1.mind_record then begin + 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 + | _, _ -> false + in + check record_equal (fun mib -> mib.mind_record); + if mib1.mind_record != None then begin let rec names_prod_letin t = match t with | Prod(n,_,t) -> n::(names_prod_letin t) | LetIn(n,_,_,t) -> n::(names_prod_letin t) @@ -282,7 +296,8 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = "inductive type and give a definition to map the old name to the new " ^ "name.")); if constant_has_body cb2 then error () ; - let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in + let u = inductive_instance mind1 in + let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> @@ -292,7 +307,8 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = "constructor and give a definition to map the old name to the new " ^ "name.")); if constant_has_body cb2 then error () ; - let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in + let u1 = inductive_instance mind1 in + let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in let ty2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv env ty1 ty2 diff --git a/checker/term.ml b/checker/term.ml index ea81f5dab..ad26c5edc 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -76,6 +76,7 @@ let iter_constr_with_binders g f n c = match c with | CoFix (_,(_,tl,bl)) -> Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl + | Proj (p, c) -> f n c exception LocalOccur @@ -152,6 +153,7 @@ let map_constr_with_binders g f l c = match c with | CoFix(ln,(lna,tl,bl)) -> let l' = iterate g (Array.length tl) l in CoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) + | Proj (p, c) -> Proj (p, f l c) (* The generic lifting function *) let rec exliftn el c = match c with @@ -351,6 +353,9 @@ let compare_sorts s1 s2 = match s1, s2 with | Prop _, Type _ -> false | Type _, Prop _ -> false +let eq_puniverses f (c1,u1) (c2,u2) = + Univ.Instance.equal u1 u2 && f c1 c2 + let compare_constr f t1 t2 = match t1, t2 with | Rel n1, Rel n2 -> Int.equal n1 n2 @@ -372,9 +377,10 @@ let compare_constr f t1 t2 = f h1 h2 && List.for_all2 f l1 l2 else false | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2 - | Const c1, Const c2 -> eq_con_chk c1 c2 - | Ind c1, Ind c2 -> eq_ind_chk c1 c2 - | Construct (c1,i1), Construct (c2,i2) -> Int.equal i1 i2 && eq_ind_chk c1 c2 + | Const c1, Const c2 -> eq_puniverses eq_con_chk c1 c2 + | Ind c1, Ind c2 -> eq_puniverses eq_ind_chk c1 c2 + | Construct ((c1,i1),u1), Construct ((c2,i2),u2) -> Int.equal i1 i2 && eq_ind_chk c1 c2 + && Univ.Instance.equal u1 u2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> f p1 p2 && f c1 c2 && Array.equal f bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> @@ -389,3 +395,88 @@ let rec eq_constr m n = compare_constr eq_constr m n let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) + +(* Universe substitutions *) + +let subst_univs_puniverses subst = + if Univ.is_empty_level_subst subst then fun c -> c + else + let f = Univ.Instance.subst subst in + fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u') + +let subst_univs_fn_puniverses fn = + let f = Univ.Instance.subst_fn fn in + fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u') + +let map_constr f c = map_constr_with_binders (fun x -> x) (fun _ c -> f c) 0 c + +let subst_univs_fn_constr f c = + let changed = ref false in + let fu = Univ.subst_univs_universe f in + let fi = Univ.Instance.subst_fn (Univ.level_subst_of f) in + let rec aux t = + match t with + | Sort (Type u) -> + let u' = fu u in + if u' == u then t else + (changed := true; Sort (Type u')) + | Const (c, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; Const (c, u')) + | Ind (i, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; Ind (i, u')) + | Construct (c, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; Construct (c, u')) + | _ -> map_constr aux t + in + let c' = aux c in + if !changed then c' else c + +let subst_univs_constr subst c = + if Univ.is_empty_subst subst then c + else + let f = Univ.make_subst subst in + subst_univs_fn_constr f c + + +let subst_univs_level_constr subst c = + if Univ.is_empty_level_subst subst then c + else + let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in + let changed = ref false in + let rec aux t = + match t with + | Const (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; Const (c, u')) + | Ind (i, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; Ind (i, u')) + | Construct (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (changed := true; Construct (c, u')) + | Sort (Type u) -> + let u' = Univ.subst_univs_level_universe subst u in + if u' == u then t else + (changed := true; Sort (Type u')) + | _ -> map_constr aux t + in + let c' = aux c in + if !changed then c' else c + +let subst_univs_context s = + map_rel_context (subst_univs_constr s) diff --git a/checker/term.mli b/checker/term.mli index f75341b9d..cf488f536 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -52,3 +52,7 @@ val destArity : constr -> arity val isArity : constr -> bool val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool val eq_constr : constr -> constr -> bool + +val subst_univs_constr : Univ.universe_subst -> constr -> constr +val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr +val subst_univs_context : Univ.universe_subst -> rel_context -> rel_context diff --git a/checker/type_errors.ml b/checker/type_errors.ml index e800ee3ef..565005b90 100644 --- a/checker/type_errors.ml +++ b/checker/type_errors.ml @@ -45,7 +45,7 @@ type type_error = | NotAType of unsafe_judgment | BadAssumption of unsafe_judgment | ReferenceVariables of constr - | ElimArity of inductive * sorts_family list * constr * unsafe_judgment + | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment * (sorts_family * sorts_family * arity_error) option | CaseNotInductive of unsafe_judgment | WrongCaseInfo of inductive * case_info @@ -59,6 +59,7 @@ type type_error = | IllFormedRecBody of guard_error * name array * int | IllTypedRecBody of int * name array * unsafe_judgment array * constr array + | UnsatisfiedConstraints of Univ.constraints exception TypeError of env * type_error @@ -107,4 +108,5 @@ let error_ill_formed_rec_body env why lna i = let error_ill_typed_rec_body env i lna vdefj vargs = raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs))) - +let error_unsatisfied_constraints env c = + raise (TypeError (env, UnsatisfiedConstraints c)) diff --git a/checker/type_errors.mli b/checker/type_errors.mli index bcd4360b3..24086f16f 100644 --- a/checker/type_errors.mli +++ b/checker/type_errors.mli @@ -47,7 +47,7 @@ type type_error = | NotAType of unsafe_judgment | BadAssumption of unsafe_judgment | ReferenceVariables of constr - | ElimArity of inductive * sorts_family list * constr * unsafe_judgment + | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment * (sorts_family * sorts_family * arity_error) option | CaseNotInductive of unsafe_judgment | WrongCaseInfo of inductive * case_info @@ -61,6 +61,7 @@ type type_error = | IllFormedRecBody of guard_error * name array * int | IllTypedRecBody of int * name array * unsafe_judgment array * constr array + | UnsatisfiedConstraints of Univ.constraints exception TypeError of env * type_error @@ -75,7 +76,7 @@ val error_assumption : env -> unsafe_judgment -> 'a val error_reference_variables : env -> constr -> 'a val error_elim_arity : - env -> inductive -> sorts_family list -> constr -> unsafe_judgment -> + env -> pinductive -> sorts_family list -> constr -> unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'a val error_case_not_inductive : env -> unsafe_judgment -> 'a @@ -99,3 +100,4 @@ val error_ill_formed_rec_body : val error_ill_typed_rec_body : env -> int -> name array -> unsafe_judgment array -> constr array -> 'a +val error_unsatisfied_constraints : env -> Univ.constraints -> 'a diff --git a/checker/typeops.ml b/checker/typeops.ml index 6a705b198..887d9dc1d 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -28,6 +28,10 @@ let conv_leq_vecti env v1 v2 = v1 v2 +let check_constraints cst env = + if Environ.check_constraints cst env then () + else error_unsatisfied_constraints env cst + (* This should be a type (a priori without intension to be an assumption) *) let type_judgment env (c,ty as j) = match whd_betadeltaiota env ty with @@ -66,23 +70,34 @@ let judge_of_relative env n = (* Type of constants *) -let type_of_constant_knowing_parameters env t paramtyps = - t - (* | PolymorphicArity (sign,ar) -> *) - (* let ctx = List.rev sign in *) - (* let ctx,s = instantiate_universes env ctx ar paramtyps in *) - (* mkArity (List.rev ctx,s) *) + +let type_of_constant_type_knowing_parameters env t paramtyps = + match t with + | RegularArity t -> t + | TemplateArity (sign,ar) -> + let ctx = List.rev sign in + let ctx,s = instantiate_universes env ctx ar paramtyps in + mkArity (List.rev ctx,s) + +let type_of_constant_knowing_parameters env cst paramtyps = + let ty, cu = constant_type env cst in + type_of_constant_type_knowing_parameters env ty paramtyps, cu let type_of_constant_type env t = - type_of_constant_knowing_parameters env t [||] + type_of_constant_type_knowing_parameters env t [||] -let judge_of_constant_knowing_parameters env cst paramstyp = - let cb = - try lookup_constant cst env +let type_of_constant env cst = + type_of_constant_knowing_parameters env cst [||] + +let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp = + let _cb = + try lookup_constant kn env with Not_found -> - failwith ("Cannot find constant: "^string_of_con cst) + failwith ("Cannot find constant: "^string_of_con kn) in - type_of_constant_knowing_parameters env cb.const_type paramstyp + let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in + let () = check_constraints cu env in + ty let judge_of_constant env cst = judge_of_constant_knowing_parameters env cst [||] @@ -160,27 +175,27 @@ let judge_of_cast env (c,cj) k tj = the App case of execute; from this constraints, the expected dynamic constraints of the form u<=v are enforced *) -let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) = - let (mib,mip) = +let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) = + let specif = try lookup_mind_specif env ind with Not_found -> failwith ("Cannot find inductive: "^string_of_mind (fst ind)) in - type_of_inductive_knowing_parameters env mip paramstyp + type_of_inductive_knowing_parameters env (specif,u) paramstyp let judge_of_inductive env ind = judge_of_inductive_knowing_parameters env ind [||] (* Constructors. *) -let judge_of_constructor env c = +let judge_of_constructor env (c,u) = let ind = inductive_of_constructor c in let specif = try lookup_mind_specif env ind with Not_found -> failwith ("Cannot find inductive: "^string_of_mind (fst ind)) in - type_of_constructor c specif + type_of_constructor (c,u) specif (* Case. *) @@ -196,11 +211,24 @@ let judge_of_case env ci pj (c,cj) lfj = let indspec = try find_rectype env cj with Not_found -> error_case_not_inductive env (c,cj) in - let _ = check_case_info env (fst indspec) ci in + let _ = check_case_info env (fst (fst indspec)) ci in let (bty,rslty) = type_case_branches env indspec pj c in check_branch_types env (c,cj) (lfj,bty); rslty +(* Projection. *) + +let judge_of_projection env p c ct = + let pb = lookup_projection p env in + let (ind,u), args = + try find_rectype env ct + with Not_found -> error_case_not_inductive env (c, ct) + in + assert(eq_mind pb.proj_ind (fst ind)); + let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in + let ty = subst_univs_constr usubst pb.proj_type in + substl (c :: List.rev args) ty + (* Fixpoints. *) (* Checks the type of a general (co)fixpoint, i.e. without checking *) @@ -264,6 +292,10 @@ let rec execute env cstr = let jl = Array.map2 (fun c ty -> c,ty) args jl in judge_of_apply env (f,j) jl + | Proj (p, c) -> + let ct = execute env c in + judge_of_projection env p c ct + | Lambda (name,c1,c2) -> let _ = execute_type env c1 in let env1 = push_rel (name,None,c1) env in @@ -364,14 +396,14 @@ let check_kind env ar u = if snd (dest_prod env ar) = Sort(Type u) then () else failwith "not the correct sort" -(* let check_polymorphic_arity env params par = *) -(* let pl = par.poly_param_levels in *) -(* let rec check_p env pl params = *) -(* match pl, params with *) -(* Some u::pl, (na,None,ty)::params -> *) -(* check_kind env ty u; *) -(* check_p (push_rel (na,None,ty) env) pl params *) -(* | None::pl,d::params -> check_p (push_rel d env) pl params *) -(* | [], _ -> () *) -(* | _ -> failwith "check_poly: not the right number of params" in *) -(* check_p env pl (List.rev params) *) +let check_polymorphic_arity env params par = + let pl = par.template_param_levels in + let rec check_p env pl params = + match pl, params with + Some u::pl, (na,None,ty)::params -> + check_kind env ty u; + check_p (push_rel (na,None,ty) env) pl params + | None::pl,d::params -> check_p (push_rel d env) pl params + | [], _ -> () + | _ -> failwith "check_poly: not the right number of params" in + check_p env pl (List.rev params) diff --git a/checker/typeops.mli b/checker/typeops.mli index 97d79fe54..32920b02f 100644 --- a/checker/typeops.mli +++ b/checker/typeops.mli @@ -16,8 +16,8 @@ open Environ val infer : env -> constr -> constr val infer_type : env -> constr -> sorts val check_ctxt : env -> rel_context -> env -(* val check_polymorphic_arity : *) -(* env -> rel_context -> polymorphic_arity -> unit *) +val check_polymorphic_arity : + env -> rel_context -> template_arity -> unit -val type_of_constant_type : env -> constr -> constr +val type_of_constant_type : env -> constant_type -> constr |