diff options
| author | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
| commit | ed275fd5eb8b11003f8904010d853d2bd568db79 (patch) | |
| tree | e27b7778175cb0d9d19bd8bde9c593b335a85125 /kernel | |
| parent | a44c4a34202fa6834520fcd6842cc98eecf044ec (diff) | |
| parent | 1ba29c062e30181bda9d931dffe48e457dfee9d6 (diff) | |
Merge PR #8817: SProp: the definitionally proof irrelevant universe
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82
Diffstat (limited to 'kernel')
48 files changed, 1262 insertions, 606 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 5fec55fea1..412637c4b6 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -29,6 +29,7 @@ open Pp open Names open Constr open Declarations +open Context open Environ open Vars open Esubst @@ -98,7 +99,7 @@ module type RedFlagsSig = sig val red_projection : reds -> Projection.t -> bool end -module RedFlags = (struct +module RedFlags : RedFlagsSig = struct (* [r_const=(true,cl)] means all constants but those in [cl] *) (* [r_const=(false,cl)] means only those in [cl] *) @@ -195,7 +196,7 @@ module RedFlags = (struct if Projection.unfolded p then true else red_set red (fCONST (Projection.constant p)) -end : RedFlagsSig) +end open RedFlags @@ -282,12 +283,63 @@ let assoc_defined id env = match Environ.lookup_named id env with type red_state = Norm | Cstr | Whnf | Red let neutr = function - | (Whnf|Norm) -> Whnf - | (Red|Cstr) -> Red + | Whnf|Norm -> Whnf + | Red|Cstr -> Red + +type optrel = Unknown | KnownR | KnownI + +let opt_of_rel = function + | Sorts.Relevant -> KnownR + | Sorts.Irrelevant -> KnownI + +module Mark : sig + + type t + + val mark : red_state -> optrel -> t + val relevance : t -> optrel + val red_state : t -> red_state + + val neutr : t -> t + + val set_norm : t -> t + +end = struct + type t = int + + let[@inline] of_state = function + | Norm -> 0b00 | Cstr -> 0b01 | Whnf -> 0b10 | Red -> 0b11 + + let[@inline] of_relevance = function + | Unknown -> 0 + | KnownR -> 0b01 + | KnownI -> 0b10 + + let[@inline] mark state relevance = (of_state state) * 4 + (of_relevance relevance) + + let[@inline] relevance x = match x land 0b11 with + | 0b00 -> Unknown + | 0b01 -> KnownR + | 0b10 -> KnownI + | _ -> assert false + + let[@inline] red_state x = match x land 0b1100 with + | 0b0000 -> Norm + | 0b0100 -> Cstr + | 0b1000 -> Whnf + | 0b1100 -> Red + | _ -> assert false + + let[@inline] neutr x = x lor 0b1000 (* Whnf|Norm -> Whnf | Red|Cstr -> Red *) + + let[@inline] set_norm x = x land 0b0011 +end +let mark = Mark.mark type fconstr = { - mutable norm: red_state; - mutable term: fterm } + mutable mark : Mark.t; + mutable term: fterm; +} and fterm = | FRel of int @@ -300,9 +352,9 @@ and fterm = | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) - | FLambda of int * (Name.t * constr) list * constr * fconstr subs - | FProd of Name.t * fconstr * constr * fconstr subs - | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs + | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs + | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs + | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FInt of Uint63.t | FLIFT of int * fconstr @@ -310,20 +362,20 @@ and fterm = | FLOCKED let fterm_of v = v.term -let set_norm v = v.norm <- Norm -let is_val v = match v.norm with Norm -> true | Cstr | Whnf | Red -> false +let set_norm v = v.mark <- Mark.set_norm v.mark +let is_val v = match Mark.red_state v.mark with Norm -> true | Cstr | Whnf | Red -> false -let mk_atom c = {norm=Norm;term=FAtom c} -let mk_red f = {norm=Red;term=f} +let mk_atom c = {mark=mark Norm Unknown;term=FAtom c} +let mk_red f = {mark=mark Red Unknown;term=f} (* Could issue a warning if no is still Red, pointing out that we loose sharing. *) -let update ~share v1 no t = +let update ~share v1 mark t = if share then - (v1.norm <- no; + (v1.mark <- mark; v1.term <- t; v1) - else {norm=no;term=t} + else {mark;term=t;} (** Reduction cache *) @@ -383,16 +435,19 @@ let rec stack_args_size = function lft_fconstr always create a new cell, while lift_fconstr avoids it when the lift is 0. *) let rec lft_fconstr n ft = + let r = Mark.relevance ft.mark in match ft.term with | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)|FInt _) -> ft - | FRel i -> {norm=Norm;term=FRel(i+n)} - | FLambda(k,tys,f,e) -> {norm=Cstr; term=FLambda(k,tys,f,subs_shft(n,e))} - | FFix(fx,e) -> {norm=Cstr; term=FFix(fx,subs_shft(n,e))} - | FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))} + | FRel i -> {mark=mark Norm r;term=FRel(i+n)} + | FLambda(k,tys,f,e) -> {mark=mark Cstr r; term=FLambda(k,tys,f,subs_shft(n,e))} + | FFix(fx,e) -> + {mark=mark Cstr r; term=FFix(fx,subs_shft(n,e))} + | FCoFix(cfx,e) -> + {mark=mark Cstr r; term=FCoFix(cfx,subs_shft(n,e))} | FLIFT(k,m) -> lft_fconstr (n+k) m | FLOCKED -> assert false | FFlex (RelKey _) | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _ - | FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(n,ft)} + | FLetIn _ | FEvar _ | FCLOS _ -> {mark=ft.mark; term=FLIFT(n,ft)} let lift_fconstr k f = if Int.equal k 0 then f else lft_fconstr k f let lift_fconstr_vect k v = @@ -401,9 +456,9 @@ let lift_fconstr_vect k v = let clos_rel e i = match expand_rel i e with | Inl(n,mt) -> lift_fconstr n mt - | Inr(k,None) -> {norm=Norm; term= FRel k} + | Inr(k,None) -> {mark=mark Norm Unknown; term= FRel k} | Inr(k,Some p) -> - lift_fconstr (k-p) {norm=Red;term=FFlex(RelKey p)} + lift_fconstr (k-p) {mark=mark Red Unknown;term=FFlex(RelKey p)} (* since the head may be reducible, we might introduce lifts of 0 *) let compact_stack head stk = @@ -414,7 +469,7 @@ let compact_stack head stk = lost by the update operation *) let h' = lft_fconstr depth head in (** The stack contains [Zupdate] marks only if in sharing mode *) - let _ = update ~share:true m h'.norm h'.term in + let _ = update ~share:true m h'.mark h'.term in strip_rec depth s | ((ZcaseT _ | Zproj _ | Zfix _ | Zapp _ | Zprimitive _) :: _ | []) as stk -> zshift depth stk in @@ -423,7 +478,7 @@ let compact_stack head stk = (* Put an update mark in the stack, only if needed *) let zupdate info m s = let share = info.i_cache.i_share in - if share && begin match m.norm with Red -> true | Norm | Whnf | Cstr -> false end + if share && begin match Mark.red_state m.mark with Red -> true | Norm | Whnf | Cstr -> false end then let s' = compact_stack m s in let _ = m.term <- FLOCKED in @@ -436,25 +491,25 @@ let mk_lambda env t = let destFLambda clos_fun t = match [@ocaml.warning "-4"] t.term with - | FLambda(_,[(na,ty)],b,e) -> (na,clos_fun e ty,clos_fun (subs_lift e) b) - | FLambda(n,(na,ty)::tys,b,e) -> - (na,clos_fun e ty,{norm=Cstr;term=FLambda(n-1,tys,b,subs_lift e)}) - | _ -> assert false -(* t must be a FLambda and binding list cannot be empty *) + FLambda(_,[(na,ty)],b,e) -> (na,clos_fun e ty,clos_fun (subs_lift e) b) + | FLambda(n,(na,ty)::tys,b,e) -> + (na,clos_fun e ty,{mark=t.mark;term=FLambda(n-1,tys,b,subs_lift e)}) + | _ -> assert false + (* t must be a FLambda and binding list cannot be empty *) (* Optimization: do not enclose variables in a closure. Makes variable access much faster *) let mk_clos e t = match kind t with | Rel i -> clos_rel e i - | Var x -> { norm = Red; term = FFlex (VarKey x) } - | Const c -> { norm = Red; term = FFlex (ConstKey c) } - | Meta _ | Sort _ -> { norm = Norm; term = FAtom t } - | Ind kn -> { norm = Norm; term = FInd kn } - | Construct kn -> { norm = Cstr; term = FConstruct kn } - | Int i -> {norm = Cstr; term = FInt i} + | Var x -> {mark = mark Red Unknown; term = FFlex (VarKey x) } + | Const c -> {mark = mark Red Unknown; term = FFlex (ConstKey c) } + | Meta _ | Sort _ -> {mark = mark Norm KnownR; term = FAtom t } + | Ind kn -> {mark = mark Norm KnownR; term = FInd kn } + | Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn } + | Int i -> {mark = mark Cstr Unknown; term = FInt i} | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> - {norm = Red; term = FCLOS(t,e)} + {mark = mark Red Unknown; term = FCLOS(t,e)} let inject c = mk_clos (subs_id 0) c @@ -606,23 +661,25 @@ let rec fstrong unfreeze_fun lfts v = let rec zip m stk = match stk with | [] -> m - | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s + | Zapp args :: s -> zip {mark=Mark.neutr m.mark; term=FApp(m, args)} s | ZcaseT(ci,p,br,e)::s -> let t = FCaseT(ci, p, m, br, e) in - zip {norm=neutr m.norm; term=t} s + let mark = mark (neutr (Mark.red_state m.mark)) Unknown in + zip {mark; term=t} s | Zproj p :: s -> - zip {norm=neutr m.norm; term=FProj(Projection.make p true,m)} s + let mark = mark (neutr (Mark.red_state m.mark)) Unknown in + zip {mark; term=FProj(Projection.make p true,m)} s | Zfix(fx,par)::s -> zip fx (par @ append_stack [|m|] s) | Zshift(n)::s -> zip (lift_fconstr n m) s | Zupdate(rf)::s -> (** The stack contains [Zupdate] marks only if in sharing mode *) - zip (update ~share:true rf m.norm m.term) s + zip (update ~share:true rf m.mark m.term) s | Zprimitive(_op,c,rargs,kargs)::s -> let args = List.rev_append rargs (m::List.map snd kargs) in - let f = {norm = Red;term = FFlex (ConstKey c)} in - zip {norm=neutr m.norm; term = FApp (f, Array.of_list args)} s + let f = {mark = mark Red Unknown;term = FFlex (ConstKey c)} in + zip {mark=mark (neutr (Mark.red_state m.mark)) KnownR; term = FApp (f, Array.of_list args)} s let fapp_stack (m,stk) = zip m stk @@ -640,21 +697,21 @@ let strip_update_shift_app_red head stk = strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s | (Zapp args :: s) -> strip_rec (Zapp args :: rstk) - {norm=h.norm;term=FApp(h,args)} depth s + {mark=h.mark;term=FApp(h,args)} depth s | Zupdate(m)::s -> (** The stack contains [Zupdate] marks only if in sharing mode *) - strip_rec rstk (update ~share:true m h.norm h.term) depth s + strip_rec rstk (update ~share:true m h.mark h.term) depth s | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk -> (depth,List.rev rstk, stk) in strip_rec [] head 0 stk let strip_update_shift_app head stack = - assert (match head.norm with Red -> false | Norm | Cstr | Whnf -> true); + assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true); strip_update_shift_app_red head stack let get_nth_arg head n stk = - assert (match head.norm with Red -> false | Norm | Cstr | Whnf -> true); + assert (match Mark.red_state head.mark with Red -> false | Norm | Cstr | Whnf -> true); let rec strip_rec rstk h n = function | Zshift(k) as e :: s -> strip_rec (e::rstk) (lift_fconstr k h) n s @@ -662,7 +719,7 @@ let get_nth_arg head n stk = let q = Array.length args in if n >= q then - strip_rec (Zapp args::rstk) {norm=h.norm;term=FApp(h,args)} (n-q) s' + strip_rec (Zapp args::rstk) {mark=h.mark;term=FApp(h,args)} (n-q) s' else let bef = Array.sub args 0 n in let aft = Array.sub args (n+1) (q-n-1) in @@ -671,7 +728,7 @@ let get_nth_arg head n stk = (Some (stk', args.(n)), append_stack aft s') | Zupdate(m)::s -> (** The stack contains [Zupdate] mark only if in sharing mode *) - strip_rec rstk (update ~share:true m h.norm h.term) n s + strip_rec rstk (update ~share:true m h.mark h.term) n s | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as s -> (None, List.rev rstk @ s) in strip_rec [] head n stk @@ -680,7 +737,7 @@ let get_nth_arg head n stk = let rec get_args n tys f e = function | Zupdate r :: s -> (** The stack contains [Zupdate] mark only if in sharing mode *) - let _hd = update ~share:true r Cstr (FLambda(n,tys,f,e)) in + let _hd = update ~share:true r (mark Cstr (Mark.relevance r.mark)) (FLambda(n,tys,f,e)) in get_args n tys f e s | Zshift k :: s -> get_args n tys f (subs_shft (k,e)) s @@ -695,7 +752,7 @@ let rec get_args n tys f e = function let etys = List.skipn na tys in get_args (n-na) etys f (subs_cons(l,e)) s | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk -> - (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk) + (Inr {mark=mark Cstr Unknown;term=FLambda(n,tys,f,e)}, stk) (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *) let rec eta_expand_stack = function @@ -703,7 +760,7 @@ let rec eta_expand_stack = function | Zshift _ | Zupdate _ | Zprimitive _ as e) :: s -> e :: eta_expand_stack s | [] -> - [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]] + [Zshift 1; Zapp [|{mark=mark Norm Unknown; term= FRel 1}|]] (* Get the arguments of a native operator *) let rec skip_native_args rargs nargs = @@ -731,12 +788,12 @@ let get_native_args op c stk = (skip_native_args [] (List.rev rnargs), Zapp (Array.of_list eargs) :: s') | rnargs, kargs, _ -> - strip_rec rnargs {norm = h.norm;term=FApp(h, args)} depth kargs s' + strip_rec rnargs {mark = h.mark;term=FApp(h, args)} depth kargs s' end | Zupdate(m) :: s -> - strip_rec rnargs (update ~share:true m h.norm h.term) depth kargs s + strip_rec rnargs (update ~share:true m h.mark h.term) depth kargs s | (Zprimitive _ | ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> assert false - in strip_rec [] {norm = Red;term = FFlex(ConstKey c)} 0 kargs stk + in strip_rec [] {mark = mark Red Unknown;term = FFlex(ConstKey c)} 0 kargs stk let get_native_args1 op c stk = match get_native_args op c stk with @@ -807,7 +864,7 @@ let eta_expand_ind_stack env ind m s (f, s') = (** 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 *) + { mark = mark Red Unknown; (* right can't be a constructor though *) term = FProj (Projection.make p true, right) }) projs in @@ -835,13 +892,15 @@ let rec project_nth_arg n = function let contract_fix_vect fix = let (thisbody, make_body, env, nfix) = match [@ocaml.warning "-4"] fix with - | FFix (((reci,i),(_,_,bds as rdcl)),env) -> + | FFix (((reci,i),(nas,_,bds as rdcl)),env) -> (bds.(i), - (fun j -> { norm = Cstr; term = FFix (((reci,j),rdcl),env) }), + (fun j -> { mark = mark Cstr (opt_of_rel nas.(j).binder_relevance); + term = FFix (((reci,j),rdcl),env) }), env, Array.length bds) - | FCoFix ((i,(_,_,bds as rdcl)),env) -> + | FCoFix ((i,(nas,_,bds as rdcl)),env) -> (bds.(i), - (fun j -> { norm = Cstr; term = FCoFix ((j,rdcl),env) }), + (fun j -> { mark = mark Cstr (opt_of_rel nas.(j).binder_relevance); + term = FCoFix ((j,rdcl),env) }), env, Array.length bds) | _ -> assert false in @@ -865,7 +924,7 @@ let rec knh info m stk = | FLOCKED -> assert false | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk)) | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk) - | FFix(((ri,n),(_,_,_)),_) -> + | FFix(((ri,n),_),_) -> (match get_nth_arg m ri.(n) stk with (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk') | (None, stk') -> (m,stk')) @@ -886,18 +945,18 @@ and knht info e t stk = knht info e a (append_stack (mk_clos_vect e b) stk) | Case(ci,p,t,br) -> knht info e t (ZcaseT(ci, p, br, e)::stk) - | Fix fx -> knh info { norm = Cstr; term = FFix (fx, e) } stk + | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk | Cast(a,_,_) -> knht info e a stk | Rel n -> knh info (clos_rel e n) stk - | Proj (p, c) -> knh info { norm = Red; term = FProj (p, mk_clos e c) } stk + | Proj (p, c) -> knh info { mark = mark Red Unknown; term = FProj (p, mk_clos e c) } stk | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _) -> (mk_clos e t, stk) - | CoFix cfx -> { norm = Cstr; term = FCoFix (cfx,e) }, stk - | Lambda _ -> { norm = Cstr; term = mk_lambda e t }, stk + | CoFix cfx -> { mark = mark Cstr Unknown; term = FCoFix (cfx,e) }, stk + | Lambda _ -> { mark = mark Cstr Unknown; term = mk_lambda e t }, stk | Prod (n, t, c) -> - { norm = Whnf; term = FProd (n, mk_clos e t, c, e) }, stk + { mark = mark Whnf KnownR; term = FProd (n, mk_clos e t, c, e) }, stk | LetIn (n,b,t,c) -> - { norm = Red; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk - | Evar ev -> { norm = Red; term = FEvar (ev, e) }, stk + { mark = mark Red Unknown; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk + | Evar ev -> { mark = mark Red Unknown; term = FEvar (ev, e) }, stk let inject c = mk_clos (subs_id 0) c @@ -919,7 +978,7 @@ module FNativeEntries = | FInt i -> i | _ -> raise Primred.NativeDestKO - let dummy = {norm = Norm; term = FRel 0} + let dummy = {mark = mark Norm KnownR; term = FRel 0} let current_retro = ref Retroknowledge.empty let defined_int = ref false @@ -929,7 +988,7 @@ module FNativeEntries = match retro.Retroknowledge.retro_int63 with | Some c -> defined_int := true; - fint := { norm = Norm; term = FFlex (ConstKey (Univ.in_punivs c)) } + fint := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } | None -> defined_int := false let defined_bool = ref false @@ -940,8 +999,8 @@ module FNativeEntries = match retro.Retroknowledge.retro_bool with | Some (ct,cf) -> defined_bool := true; - ftrue := { norm = Cstr; term = FConstruct (Univ.in_punivs ct) }; - ffalse := { norm = Cstr; term = FConstruct (Univ.in_punivs cf) } + ftrue := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs ct) }; + ffalse := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cf) } | None -> defined_bool :=false let defined_carry = ref false @@ -952,8 +1011,8 @@ module FNativeEntries = match retro.Retroknowledge.retro_carry with | Some(c0,c1) -> defined_carry := true; - fC0 := { norm = Cstr; term = FConstruct (Univ.in_punivs c0) }; - fC1 := { norm = Cstr; term = FConstruct (Univ.in_punivs c1) } + fC0 := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs c0) }; + fC1 := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs c1) } | None -> defined_carry := false let defined_pair = ref false @@ -963,7 +1022,7 @@ module FNativeEntries = match retro.Retroknowledge.retro_pair with | Some c -> defined_pair := true; - fPair := { norm = Cstr; term = FConstruct (Univ.in_punivs c) } + fPair := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs c) } | None -> defined_pair := false let defined_cmp = ref false @@ -975,9 +1034,9 @@ module FNativeEntries = match retro.Retroknowledge.retro_cmp with | Some (cEq, cLt, cGt) -> defined_cmp := true; - fEq := { norm = Cstr; term = FConstruct (Univ.in_punivs cEq) }; - fLt := { norm = Cstr; term = FConstruct (Univ.in_punivs cLt) }; - fGt := { norm = Cstr; term = FConstruct (Univ.in_punivs cGt) } + fEq := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cEq) }; + fLt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cLt) }; + fGt := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs cGt) } | None -> defined_cmp := false let defined_refl = ref false @@ -988,7 +1047,7 @@ module FNativeEntries = match retro.Retroknowledge.retro_refl with | Some crefl -> defined_refl := true; - frefl := { norm = Cstr; term = FConstruct (Univ.in_punivs crefl) } + frefl := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs crefl) } | None -> defined_refl := false let init env = @@ -1025,7 +1084,7 @@ module FNativeEntries = let mkInt env i = check_int env; - { norm = Norm; term = FInt i } + { mark = mark Norm KnownR; term = FInt i } let mkBool env b = check_bool env; @@ -1033,12 +1092,12 @@ module FNativeEntries = let mkCarry env b e = check_carry env; - {norm = Cstr; + {mark = mark Cstr KnownR; term = FApp ((if b then !fC1 else !fC0),[|!fint;e|])} let mkIntPair env e1 e2 = check_pair env; - { norm = Cstr; term = FApp(!fPair, [|!fint;!fint;e1;e2|]) } + { mark = mark Cstr KnownR; term = FApp(!fPair, [|!fint;!fint;e1;e2|]) } let mkLt env = check_cmp env; @@ -1124,8 +1183,8 @@ let rec knr info tab m stk = begin match FredNative.red_prim (info_env info) () op args with | Some m -> kni info tab m s | None -> - let f = {norm = Whnf; term = FFlex (ConstKey c)} in - let m = {norm = Whnf; term = FApp(f,args)} in + let f = {mark = mark Whnf KnownR; term = FFlex (ConstKey c)} in + let m = {mark = mark Whnf KnownR; term = FApp(f,args)} in (m,s) end | (kd,a)::nargs -> @@ -1194,12 +1253,12 @@ and norm_head info tab m = if is_val m then (incr prune; term_of_fconstr m) else match m.term with | FLambda(_n,tys,f,e) -> - let (e',rvtys) = - List.fold_left (fun (e,ctxt) (na,ty) -> - (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt)) - (e,[]) tys in - let bd = kl info tab (mk_clos e' f) in - List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys + let (e',info,rvtys) = + List.fold_left (fun (e,info,ctxt) (na,ty) -> + (subs_lift e, info, (na,kl info tab (mk_clos e ty))::ctxt)) + (e,info,[]) tys in + let bd = kl info tab (mk_clos e' f) in + List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys | FLetIn(na,a,b,f,e) -> let c = mk_clos (subs_lift e) f in mkLetIn(na, kl info tab a, kl info tab b, kl info tab c) @@ -1232,7 +1291,7 @@ let whd_val info tab v = let norm_val info tab v = with_stats (lazy (kl info tab v)) -let whd_stack infos tab m stk = match m.norm with +let whd_stack infos tab m stk = match Mark.red_state m.mark with | Whnf | Norm -> (** No need to perform [kni] nor to unlock updates because every head subterm of [m] is [Whnf] or [Norm] *) @@ -1269,3 +1328,6 @@ let unfold_reference info tab key = ref_value_cache info tab key else Undef None | RelKey _ -> ref_value_cache info tab key + +let relevance_of f = Mark.relevance f.mark +let set_relevance r f = f.mark <- Mark.mark (Mark.red_state f.mark) (opt_of_rel r) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index bd04677374..b1b69dded8 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -114,9 +114,9 @@ type fterm = | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) - | FLambda of int * (Name.t * constr) list * constr * fconstr subs - | FProd of Name.t * fconstr * constr * fconstr subs - | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs + | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs + | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs + | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FInt of Uint63.t | FLIFT of int * fconstr @@ -165,7 +165,12 @@ val mk_red : fterm -> fconstr val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr val destFLambda : - (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr + (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t Context.binder_annot * fconstr * fconstr + +type optrel = Unknown | KnownR | KnownI + +val relevance_of : fconstr -> optrel +val set_relevance : Sorts.relevance -> fconstr -> unit (** Global and local constant cache *) type clos_infos diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 718584b3d4..69f004307d 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -550,7 +550,7 @@ let rec compile_lam env cenv lam sz cont = else comp_app compile_structured_constant compile_universe cenv (Const_ind ind) (Univ.Instance.to_array u) sz cont - | Lsort (Sorts.Prop | Sorts.Set as s) -> + | Lsort (Sorts.SProp | Sorts.Prop | Sorts.Set as s) -> compile_structured_constant cenv (Const_sort s) sz cont | Lsort (Sorts.Type u) -> (* We represent universes as a global constant with local universes @@ -562,10 +562,10 @@ let rec compile_lam env cenv lam sz cont = compile_fv_elem cenv (FVuniv_var idx) sz cont in if List.is_empty s then - compile_structured_constant cenv (Const_sort (Sorts.Type u)) sz cont + compile_structured_constant cenv (Const_sort (Sorts.sort_of_univ u)) sz cont else comp_app compile_structured_constant compile_get_univ cenv - (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont + (Const_sort (Sorts.sort_of_univ u)) (Array.of_list s) sz cont | Llet (_id,def,body) -> compile_lam env cenv def sz diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 5c21a5ec25..a764cca354 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -15,8 +15,8 @@ type lambda = | Lvar of Id.t | Levar of Evar.t * lambda array | Lprod of lambda * lambda - | Llam of Name.t array * lambda - | Llet of Name.t * lambda * lambda + | Llam of Name.t Context.binder_annot array * lambda + | Llet of Name.t Context.binder_annot * lambda * lambda | Lapp of lambda * lambda array | Lconst of pconstant | Lprim of pconstant option * CPrimitives.t * lambda array @@ -38,15 +38,17 @@ type lambda = stored in [extra_branches]. *) and lam_branches = { constant_branches : lambda array; - nonconstant_branches : (Name.t array * lambda) array } + nonconstant_branches : (Name.t Context.binder_annot array * lambda) array } (* extra_branches : (name array * lambda) array } *) -and fix_decl = Name.t array * lambda array * lambda array +and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array (** Printing **) +let pr_annot x = Name.print x.Context.binder_name + let pp_names ids = - prlist_with_sep (fun _ -> brk(1,1)) Name.print (Array.to_list ids) + prlist_with_sep (fun _ -> brk(1,1)) pr_annot (Array.to_list ids) let pp_rel name n = Name.print name ++ str "##" ++ int n @@ -55,6 +57,7 @@ let pp_sort s = match Sorts.family s with | InSet -> str "Set" | InProp -> str "Prop" + | InSProp -> str "SProp" | InType -> str "Type" let rec pp_lam lam = @@ -79,7 +82,7 @@ let rec pp_lam lam = str ")") | Llet(id,def,body) -> hov 0 (str "let " ++ - Name.print id ++ + pr_annot id ++ str ":=" ++ pp_lam def ++ str " in" ++ @@ -119,7 +122,7 @@ let rec pp_lam lam = v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> - Name.print na ++ str"/" ++ int i ++ str":" ++ + pr_annot na ++ str"/" ++ int i ++ str":" ++ pp_lam ty ++ cut() ++ str":=" ++ pp_lam bd) (Array.to_list fixl)) ++ str"}") @@ -131,7 +134,7 @@ let rec pp_lam lam = v 0 (prlist_with_sep spc (fun (na,ty,bd) -> - Name.print na ++ str":" ++ pp_lam ty ++ + pr_annot na ++ str":" ++ pp_lam ty ++ cut() ++ str":=" ++ pp_lam bd) (Array.to_list fixl)) ++ str"}") | Lmakeblock(tag, args) -> @@ -393,8 +396,8 @@ and reduce_lapp substf lids body substa largs = Llet(id, a, body) | [], [] -> simplify substf body | _::_, _ -> - Llam(Array.of_list lids, simplify (liftn (List.length lids) substf) body) - | [], _::_ -> simplify_app substf body substa (Array.of_list largs) + Llam(Array.of_list lids, simplify (liftn (List.length lids) substf) body) + | [], _ -> simplify_app substf body substa (Array.of_list largs) @@ -511,7 +514,8 @@ let make_args start _end = (* Translation of constructors *) let expand_constructor tag nparams arity = - let ids = Array.make (nparams + arity) Anonymous in + let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *) + let ids = Array.make (nparams + arity) anon in if arity = 0 then mkLlam ids (Lint tag) else let args = make_args arity 1 in @@ -553,7 +557,8 @@ let prim kn p args = Lprim(Some kn, p, args) let expand_prim kn op arity = - let ids = Array.make arity Anonymous in + (* primitives are always Relevant *) + let ids = Array.make arity Context.anonR in let args = make_args arity 1 in Llam(ids, prim kn op args) @@ -628,7 +633,7 @@ struct construct_tbl = Hashtbl.create 111 } - let push_rel env id = Vect.push env.name_rel id + let push_rel env id = Vect.push env.name_rel id.Context.binder_name let push_rels env ids = Array.iter (push_rel env) ids @@ -678,7 +683,7 @@ let rec lambda_of_constr env c = Renv.push_rel env id; let lc = lambda_of_constr env codom in Renv.pop env; - Lprod(ld, Llam([|id|], lc)) + Lprod(ld, Llam([|id|], lc)) | Lambda _ -> let params, body = decompose_lam c in @@ -725,7 +730,8 @@ let rec lambda_of_constr env c = match b with | Llam(ids, body) when Array.length ids = arity -> (ids, body) | _ -> - let ids = Array.make arity Anonymous in + let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *) + let ids = Array.make arity anon in let args = make_args arity 1 in let ll = lam_lift arity b in (ids, mkLapp ll args) @@ -800,7 +806,7 @@ let optimize_lambda lam = let lambda_of_constr ~optimize genv c = let env = Renv.make genv in - let ids = List.rev_map Context.Rel.Declaration.get_name (rel_context genv) in + let ids = List.rev_map Context.Rel.Declaration.get_annot (rel_context genv) in Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env c in let lam = if optimize then optimize_lambda lam else lam in diff --git a/kernel/clambda.mli b/kernel/clambda.mli index 4d921fd45e..1476bb6e45 100644 --- a/kernel/clambda.mli +++ b/kernel/clambda.mli @@ -8,8 +8,8 @@ type lambda = | Lvar of Id.t | Levar of Evar.t * lambda array | Lprod of lambda * lambda - | Llam of Name.t array * lambda - | Llet of Name.t * lambda * lambda + | Llam of Name.t Context.binder_annot array * lambda + | Llet of Name.t Context.binder_annot * lambda * lambda | Lapp of lambda * lambda array | Lconst of pconstant | Lprim of pconstant option * CPrimitives.t * lambda array @@ -28,15 +28,15 @@ type lambda = and lam_branches = { constant_branches : lambda array; - nonconstant_branches : (Name.t array * lambda) array } + nonconstant_branches : (Name.t Context.binder_annot array * lambda) array } -and fix_decl = Name.t array * lambda array * lambda array +and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array exception TooLargeInductive of Pp.t val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda -val decompose_Llam : lambda -> Name.t array * lambda +val decompose_Llam : lambda -> Name.t Context.binder_annot array * lambda val get_alias : env -> Constant.t -> Constant.t diff --git a/kernel/constr.ml b/kernel/constr.ml index c392494e95..11958c9108 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -28,6 +28,7 @@ open Util open Names open Univ +open Context type existential_key = Evar.t type metavariable = int @@ -60,6 +61,7 @@ type case_info = in addition to the parameters of the related inductive type NOTE: "lets" are therefore excluded from the count NOTE: parameters of the inductive type are also excluded from the count *) + ci_relevance : Sorts.relevance; ci_pp_info : case_printing (* not interpreted by the kernel *) } @@ -71,7 +73,7 @@ type case_info = the same order (i.e. last argument first) *) type 'constr pexistential = existential_key * 'constr array type ('constr, 'types) prec_declaration = - Name.t array * 'types array * 'constr array + Name.t binder_annot array * 'types array * 'constr array type ('constr, 'types) pfixpoint = (int array * int) * ('constr, 'types) prec_declaration type ('constr, 'types) pcofixpoint = @@ -90,9 +92,9 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Evar of 'constr pexistential | Sort of 'sort | Cast of 'constr * cast_kind * 'types - | Prod of Name.t * 'types * 'types - | Lambda of Name.t * 'types * 'constr - | LetIn of Name.t * 'constr * 'types * 'constr + | Prod of Name.t binder_annot * 'types * 'types + | Lambda of Name.t binder_annot * 'types * 'constr + | LetIn of Name.t binder_annot * 'constr * 'types * 'constr | App of 'constr * 'constr array | Const of (Constant.t * 'univs) | Ind of (inductive * 'univs) @@ -127,13 +129,15 @@ let rels = let mkRel n = if 0<n && n<=16 then rels.(n-1) else Rel n (* Construct a type *) +let mkSProp = Sort Sorts.sprop let mkProp = Sort Sorts.prop let mkSet = Sort Sorts.set -let mkType u = Sort (Sorts.Type u) +let mkType u = Sort (Sorts.sort_of_univ u) let mkSort = function + | Sorts.SProp -> mkSProp | Sorts.Prop -> mkProp (* Easy sharing *) | Sorts.Set -> mkSet - | s -> Sort s + | Sorts.Type _ as s -> Sort s (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *) (* (that means t2 is declared as the type of t1) *) @@ -1181,16 +1185,16 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Prod (na,t,c) -> let t, ht = sh_rec t and c, hc = sh_rec c in - (Prod (sh_na na, t, c), combinesmall 4 (combine3 (Name.hash na) ht hc)) + (Prod (sh_na na, t, c), combinesmall 4 (combine3 (hash_annot Name.hash na) ht hc)) | Lambda (na,t,c) -> let t, ht = sh_rec t and c, hc = sh_rec c in - (Lambda (sh_na na, t, c), combinesmall 5 (combine3 (Name.hash na) ht hc)) + (Lambda (sh_na na, t, c), combinesmall 5 (combine3 (hash_annot Name.hash na) ht hc)) | LetIn (na,b,t,c) -> let b, hb = sh_rec b in let t, ht = sh_rec t in let c, hc = sh_rec c in - (LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (Name.hash na) hb ht hc)) + (LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (hash_annot Name.hash na) hb ht hc)) | App (c,l) -> let c, hc = sh_rec c in let l, hl = hash_term_array l in @@ -1214,24 +1218,24 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = let p, hp = sh_rec p and c, hc = sh_rec c in let bl,hbl = hash_term_array bl in - let hbl = combine (combine hc hp) hbl in + let hbl = combine (combine hc hp) hbl in (Case (sh_ci ci, p, c, bl), combinesmall 12 hbl) | Fix (ln,(lna,tl,bl)) -> - let bl,hbl = hash_term_array bl in + let bl,hbl = hash_term_array bl in let tl,htl = hash_term_array tl in let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in - let fold accu na = combine (Name.hash na) accu in + let fold accu na = combine (hash_annot Name.hash na) accu in let hna = Array.fold_left fold 0 lna in let h = combine3 hna hbl htl in - (Fix (ln,(lna,tl,bl)), combinesmall 13 h) + (Fix (ln,(lna,tl,bl)), combinesmall 13 h) | CoFix(ln,(lna,tl,bl)) -> - let bl,hbl = hash_term_array bl in + let bl,hbl = hash_term_array bl in let tl,htl = hash_term_array tl in let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in - let fold accu na = combine (Name.hash na) accu in + let fold accu na = combine (hash_annot Name.hash na) accu in let hna = Array.fold_left fold 0 lna in let h = combine3 hna hbl htl in - (CoFix (ln,(lna,tl,bl)), combinesmall 14 h) + (CoFix (ln,(lna,tl,bl)), combinesmall 14 h) | Meta n -> (t, combinesmall 15 n) | Rel n -> @@ -1322,6 +1326,7 @@ struct info1.style == info2.style let eq ci ci' = ci.ci_ind == ci'.ci_ind && + ci.ci_relevance == ci'.ci_relevance && Int.equal ci.ci_npar ci'.ci_npar && Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *) Array.equal Int.equal ci.ci_cstr_nargs ci'.ci_cstr_nargs && (* we use [Array.equal] on purpose *) @@ -1345,7 +1350,7 @@ struct let h3 = Array.fold_left combine 0 ci.ci_cstr_ndecls in let h4 = Array.fold_left combine 0 ci.ci_cstr_nargs in let h5 = hash_pp_info ci.ci_pp_info in - combine5 h1 h2 h3 h4 h5 + combinesmall (Sorts.relevance_hash ci.ci_relevance) (combine5 h1 h2 h3 h4 h5) end module Hcaseinfo = Hashcons.Make(CaseinfoHash) @@ -1354,6 +1359,18 @@ let case_info_hash = CaseinfoHash.hash let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate Hcaseinfo.hcons hcons_ind +module Hannotinfo = struct + type t = Name.t binder_annot + type u = Name.t -> Name.t + let hash = hash_annot Name.hash + let eq = eq_annot (fun na1 na2 -> na1 == na2) + let hashcons h {binder_name=na;binder_relevance} = + {binder_name=h na;binder_relevance} + end +module Hannot = Hashcons.Make(Hannotinfo) + +let hcons_annot = Hashcons.simple_hcons Hannot.generate Hannot.hcons Name.hcons + let hcons = hashcons (Sorts.hcons, @@ -1361,7 +1378,7 @@ let hcons = hcons_construct, hcons_ind, hcons_con, - Name.hcons, + hcons_annot, Id.hcons) (* let hcons_types = hcons_constr *) @@ -1377,7 +1394,7 @@ type compacted_context = compacted_declaration list let debug_print_fix pr_constr ((t,i),(lna,tl,bl)) = let open Pp in - let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in + let fixl = Array.mapi (fun i na -> (na.binder_name,t.(i),tl.(i),bl.(i))) lna in hov 1 (str"fix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> @@ -1399,17 +1416,17 @@ let rec debug_print c = | Cast (c,_, t) -> hov 1 (str"(" ++ debug_print c ++ cut() ++ str":" ++ debug_print t ++ str")") - | Prod (Name(id),t,c) -> hov 1 + | Prod ({binder_name=Name id;_},t,c) -> hov 1 (str"forall " ++ Id.print id ++ str":" ++ debug_print t ++ str"," ++ spc() ++ debug_print c) - | Prod (Anonymous,t,c) -> hov 0 + | Prod ({binder_name=Anonymous;_},t,c) -> hov 0 (str"(" ++ debug_print t ++ str " ->" ++ spc() ++ debug_print c ++ str")") | Lambda (na,t,c) -> hov 1 - (str"fun " ++ Name.print na ++ str":" ++ + (str"fun " ++ Name.print na.binder_name ++ str":" ++ debug_print t ++ str" =>" ++ spc() ++ debug_print c) | LetIn (na,b,t,c) -> hov 0 - (str"let " ++ Name.print na ++ str":=" ++ debug_print b ++ + (str"let " ++ Name.print na.binder_name ++ str":=" ++ debug_print b ++ str":" ++ brk(1,2) ++ debug_print t ++ cut() ++ debug_print c) | App (c,l) -> hov 1 @@ -1434,7 +1451,7 @@ let rec debug_print c = hov 1 (str"cofix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,ty,bd) -> - Name.print na ++ str":" ++ debug_print ty ++ + Name.print na.binder_name ++ str":" ++ debug_print ty ++ cut() ++ str":=" ++ debug_print bd) (Array.to_list fixl)) ++ str"}") | Int i -> str"Int("++str (Uint63.to_string i) ++ str")" diff --git a/kernel/constr.mli b/kernel/constr.mli index fdc3296a6a..7fc57cdb8a 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -45,6 +45,7 @@ type case_info = in addition to the parameters of the related inductive type NOTE: "lets" are therefore excluded from the count NOTE: parameters of the inductive type are also excluded from the count *) + ci_relevance : Sorts.relevance; (* relevance of the predicate (not of the inductive!) *) ci_pp_info : case_printing (* not interpreted by the kernel *) } @@ -84,6 +85,7 @@ val mkEvar : existential -> constr (** Construct a sort *) val mkSort : Sorts.t -> types +val mkSProp : types val mkProp : types val mkSet : types val mkType : Univ.Universe.t -> types @@ -97,13 +99,13 @@ type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast val mkCast : constr * cast_kind * constr -> constr (** Constructs the product [(x:t1)t2] *) -val mkProd : Name.t * types * types -> types +val mkProd : Name.t Context.binder_annot * types * types -> types (** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *) -val mkLambda : Name.t * types * constr -> constr +val mkLambda : Name.t Context.binder_annot * types * constr -> constr (** Constructs the product [let x = t1 : t2 in t3] *) -val mkLetIn : Name.t * constr * types * constr -> constr +val mkLetIn : Name.t Context.binder_annot * constr * types * constr -> constr (** [mkApp (f, [|t1; ...; tN|]] constructs the application {%html:(f t<sub>1</sub> ... t<sub>n</sub>)%} @@ -160,7 +162,7 @@ val mkCase : case_info * constr * constr * constr array -> constr where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. *) type ('constr, 'types) prec_declaration = - Name.t array * 'types array * 'constr array + Name.t Context.binder_annot array * 'types array * 'constr array type ('constr, 'types) pfixpoint = (int array * int) * ('constr, 'types) prec_declaration (* The array of [int]'s tells for each component of the array of @@ -213,9 +215,9 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Evar of 'constr pexistential | Sort of 'sort | Cast of 'constr * cast_kind * 'types - | Prod of Name.t * 'types * 'types (** Concrete syntax ["forall A:B,C"] is represented as [Prod (A,B,C)]. *) - | Lambda of Name.t * 'types * 'constr (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)]. *) - | LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:C := B in D"] is represented as [LetIn (A,B,C,D)]. *) + | Prod of Name.t Context.binder_annot * 'types * 'types (** Concrete syntax ["forall A:B,C"] is represented as [Prod (A,B,C)]. *) + | Lambda of Name.t Context.binder_annot * 'types * 'constr (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)]. *) + | LetIn of Name.t Context.binder_annot * 'constr * 'types * 'constr (** Concrete syntax ["let A:C := B in D"] is represented as [LetIn (A,B,C,D)]. *) | App of 'constr * 'constr array (** Concrete syntax ["(F P1 P2 ... Pn)"] is represented as [App (F, [|P1; P2; ...; Pn|])]. The {!mkApp} constructor also enforces the following invariant: @@ -297,13 +299,13 @@ val destSort : constr -> Sorts.t val destCast : constr -> constr * cast_kind * constr (** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *) -val destProd : types -> Name.t * types * types +val destProd : types -> Name.t Context.binder_annot * types * types (** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *) -val destLambda : constr -> Name.t * types * constr +val destLambda : constr -> Name.t Context.binder_annot * types * constr (** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *) -val destLetIn : constr -> Name.t * constr * types * constr +val destLetIn : constr -> Name.t Context.binder_annot * constr * types * constr (** Destructs an application *) val destApp : constr -> constr * constr array diff --git a/kernel/context.ml b/kernel/context.ml index 1cc6e79485..290e85294b 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -31,6 +31,27 @@ open Util open Names +type 'a binder_annot = { binder_name : 'a; binder_relevance : Sorts.relevance } + +let eq_annot eq {binder_name=na1;binder_relevance=r1} {binder_name=na2;binder_relevance=r2} = + eq na1 na2 && Sorts.relevance_equal r1 r2 + +let hash_annot h {binder_name=n;binder_relevance=r} = + Hashset.Combine.combinesmall (Sorts.relevance_hash r) (h n) + +let map_annot f {binder_name=na;binder_relevance} = + {binder_name=f na;binder_relevance} + +let make_annot x r = {binder_name=x;binder_relevance=r} + +let binder_name x = x.binder_name +let binder_relevance x = x.binder_relevance + +let annotR x = make_annot x Sorts.Relevant + +let nameR x = annotR (Name x) +let anonR = annotR Anonymous + (** Representation of contexts that can capture anonymous as well as non-anonymous variables. Individual declarations are then designated by de Bruijn indexes. *) module Rel = @@ -40,13 +61,14 @@ struct struct (* local declaration *) type ('constr, 'types) pt = - | LocalAssum of Name.t * 'types (** name, type *) - | LocalDef of Name.t * 'constr * 'types (** name, value, type *) + | LocalAssum of Name.t binder_annot * 'types (** name, type *) + | LocalDef of Name.t binder_annot * 'constr * 'types (** name, value, type *) + + let get_annot = function + | LocalAssum (na,_) | LocalDef (na,_,_) -> na (** Return the name bound by a given declaration. *) - let get_name = function - | LocalAssum (na,_) - | LocalDef (na,_,_) -> na + let get_name x = (get_annot x).binder_name (** Return [Some value] for local-declarations and [None] for local-assumptions. *) let get_value = function @@ -57,11 +79,13 @@ struct let get_type = function | LocalAssum (_,ty) | LocalDef (_,_,ty) -> ty - + + let get_relevance x = (get_annot x).binder_relevance + (** Set the name that is bound by a given declaration. *) let set_name na = function - | LocalAssum (_,ty) -> LocalAssum (na, ty) - | LocalDef (_,v,ty) -> LocalDef (na, v, ty) + | LocalAssum (x,ty) -> LocalAssum ({x with binder_name=na}, ty) + | LocalDef (x,v,ty) -> LocalDef ({x with binder_name=na}, v, ty) (** Set the type of the bound variable in a given declaration. *) let set_type ty = function @@ -92,20 +116,17 @@ struct let equal eq decl1 decl2 = match decl1, decl2 with | LocalAssum (n1,ty1), LocalAssum (n2, ty2) -> - Name.equal n1 n2 && eq ty1 ty2 + eq_annot Name.equal n1 n2 && eq ty1 ty2 | LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) -> - Name.equal n1 n2 && eq v1 v2 && eq ty1 ty2 + eq_annot Name.equal n1 n2 && eq v1 v2 && eq ty1 ty2 | _ -> false (** Map the name bound by a given declaration. *) - let map_name f = function - | LocalAssum (na, ty) as decl -> - let na' = f na in - if na == na' then decl else LocalAssum (na', ty) - | LocalDef (na, v, ty) as decl -> - let na' = f na in - if na == na' then decl else LocalDef (na', v, ty) + let map_name f x = + let na = get_name x in + let na' = f na in + if na == na' then x else set_name na' x (** For local assumptions, this function returns the original local assumptions. For local definitions, this function maps the value in the local definition. *) @@ -120,7 +141,7 @@ struct | LocalAssum (na, ty) as decl -> let ty' = f ty in if ty == ty' then decl else LocalAssum (na, ty') - | LocalDef (na, v, ty) as decl -> + | LocalDef (na, v, ty) as decl -> let ty' = f ty in if ty == ty' then decl else LocalDef (na, v, ty') @@ -250,13 +271,14 @@ struct struct (** local declaration *) type ('constr, 'types) pt = - | LocalAssum of Id.t * 'types (** identifier, type *) - | LocalDef of Id.t * 'constr * 'types (** identifier, value, type *) + | LocalAssum of Id.t binder_annot * 'types (** identifier, type *) + | LocalDef of Id.t binder_annot * 'constr * 'types (** identifier, value, type *) + + let get_annot = function + | LocalAssum (na,_) | LocalDef (na,_,_) -> na (** Return the identifier bound by a given declaration. *) - let get_id = function - | LocalAssum (id,_) -> id - | LocalDef (id,_,_) -> id + let get_id x = (get_annot x).binder_name (** Return [Some value] for local-declarations and [None] for local-assumptions. *) let get_value = function @@ -268,10 +290,14 @@ struct | LocalAssum (_,ty) | LocalDef (_,_,ty) -> ty + let get_relevance x = (get_annot x).binder_relevance + (** Set the identifier that is bound by a given declaration. *) - let set_id id = function - | LocalAssum (_,ty) -> LocalAssum (id, ty) - | LocalDef (_, v, ty) -> LocalDef (id, v, ty) + let set_id id = + let set x = {x with binder_name = id} in + function + | LocalAssum (x,ty) -> LocalAssum (set x, ty) + | LocalDef (x, v, ty) -> LocalDef (set x, v, ty) (** Set the type of the bound variable in a given declaration. *) let set_type ty = function @@ -302,20 +328,17 @@ struct let equal eq decl1 decl2 = match decl1, decl2 with | LocalAssum (id1, ty1), LocalAssum (id2, ty2) -> - Id.equal id1 id2 && eq ty1 ty2 + eq_annot Id.equal id1 id2 && eq ty1 ty2 | LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) -> - Id.equal id1 id2 && eq v1 v2 && eq ty1 ty2 + eq_annot Id.equal id1 id2 && eq v1 v2 && eq ty1 ty2 | _ -> false (** Map the identifier bound by a given declaration. *) - let map_id f = function - | LocalAssum (id, ty) as decl -> - let id' = f id in - if id == id' then decl else LocalAssum (id', ty) - | LocalDef (id, v, ty) as decl -> - let id' = f id in - if id == id' then decl else LocalDef (id', v, ty) + let map_id f x = + let id = get_id x in + let id' = f id in + if id == id' then x else set_id id' x (** For local assumptions, this function returns the original local assumptions. For local definitions, this function maps the value in the local definition. *) @@ -369,15 +392,17 @@ struct let of_rel_decl f = function | Rel.Declaration.LocalAssum (na,t) -> - LocalAssum (f na, t) + LocalAssum (map_annot f na, t) | Rel.Declaration.LocalDef (na,v,t) -> - LocalDef (f na, v, t) - - let to_rel_decl = function + LocalDef (map_annot f na, v, t) + + let to_rel_decl = + let name x = {binder_name=Name x.binder_name;binder_relevance=x.binder_relevance} in + function | LocalAssum (id,t) -> - Rel.Declaration.LocalAssum (Name id, t) + Rel.Declaration.LocalAssum (name id, t) | LocalDef (id,v,t) -> - Rel.Declaration.LocalDef (Name id,v,t) + Rel.Declaration.LocalDef (name id,v,t) end (** Named-context is represented as a list of declarations. @@ -430,7 +455,7 @@ struct gives [Var id1, Var id3]. All [idj] are supposed distinct. *) let to_instance mk l = let filter = function - | Declaration.LocalAssum (id, _) -> Some (mk id) + | Declaration.LocalAssum (id, _) -> Some (mk id.binder_name) | _ -> None in List.map_filter filter l @@ -441,8 +466,8 @@ module Compacted = module Declaration = struct type ('constr, 'types) pt = - | LocalAssum of Id.t list * 'types - | LocalDef of Id.t list * 'constr * 'types + | LocalAssum of Id.t binder_annot list * 'types + | LocalDef of Id.t binder_annot list * 'constr * 'types let map_constr f = function | LocalAssum (ids, ty) as decl -> diff --git a/kernel/context.mli b/kernel/context.mli index 8acae73680..7b67e54ba4 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -24,6 +24,27 @@ open Names +type 'a binder_annot = { binder_name : 'a; binder_relevance : Sorts.relevance } +val eq_annot : ('a -> 'a -> bool) -> 'a binder_annot -> 'a binder_annot -> bool + +val hash_annot : ('a -> int) -> 'a binder_annot -> int + +val map_annot : ('a -> 'b) -> 'a binder_annot -> 'b binder_annot + +val make_annot : 'a -> Sorts.relevance -> 'a binder_annot + +val binder_name : 'a binder_annot -> 'a +val binder_relevance : 'a binder_annot -> Sorts.relevance + +val annotR : 'a -> 'a binder_annot +(** Always Relevant *) + +val nameR : Id.t -> Name.t binder_annot +(** Relevant + Name *) + +val anonR : Name.t binder_annot +(** Relevant + Anonymous *) + (** Representation of contexts that can capture anonymous as well as non-anonymous variables. Individual declarations are then designated by de Bruijn indexes. *) module Rel : @@ -32,8 +53,10 @@ sig sig (* local declaration *) type ('constr, 'types) pt = - | LocalAssum of Name.t * 'types (** name, type *) - | LocalDef of Name.t * 'constr * 'types (** name, value, type *) + | LocalAssum of Name.t binder_annot * 'types (** name, type *) + | LocalDef of Name.t binder_annot * 'constr * 'types (** name, value, type *) + + val get_annot : _ pt -> Name.t binder_annot (** Return the name bound by a given declaration. *) val get_name : ('c, 't) pt -> Name.t @@ -44,6 +67,8 @@ sig (** Return the type of the name bound by a given declaration. *) val get_type : ('c, 't) pt -> 't + val get_relevance : ('c, 't) pt -> Sorts.relevance + (** Set the name that is bound by a given declaration. *) val set_name : Name.t -> ('c, 't) pt -> ('c, 't) pt @@ -87,7 +112,7 @@ sig (** Reduce all terms in a given declaration to a single value. *) val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a - val to_tuple : ('c, 't) pt -> Name.t * 'c option * 't + val to_tuple : ('c, 't) pt -> Name.t binder_annot * 'c option * 't (** Turn [LocalDef] into [LocalAssum], identity otherwise. *) val drop_body : ('c, 't) pt -> ('c, 't) pt @@ -156,8 +181,10 @@ sig module Declaration : sig type ('constr, 'types) pt = - | LocalAssum of Id.t * 'types (** identifier, type *) - | LocalDef of Id.t * 'constr * 'types (** identifier, value, type *) + | LocalAssum of Id.t binder_annot * 'types (** identifier, type *) + | LocalDef of Id.t binder_annot * 'constr * 'types (** identifier, value, type *) + + val get_annot : _ pt -> Id.t binder_annot (** Return the identifier bound by a given declaration. *) val get_id : ('c, 't) pt -> Id.t @@ -168,6 +195,8 @@ sig (** Return the type of the name bound by a given declaration. *) val get_type : ('c, 't) pt -> 't + val get_relevance : ('c, 't) pt -> Sorts.relevance + (** Set the identifier that is bound by a given declaration. *) val set_id : Id.t -> ('c, 't) pt -> ('c, 't) pt @@ -208,8 +237,8 @@ sig (** Reduce all terms in a given declaration to a single value. *) val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a - val to_tuple : ('c, 't) pt -> Id.t * 'c option * 't - val of_tuple : Id.t * 'c option * 't -> ('c, 't) pt + val to_tuple : ('c, 't) pt -> Id.t binder_annot * 'c option * 't + val of_tuple : Id.t binder_annot * 'c option * 't -> ('c, 't) pt (** Turn [LocalDef] into [LocalAssum], identity otherwise. *) val drop_body : ('c, 't) pt -> ('c, 't) pt @@ -276,8 +305,8 @@ sig module Declaration : sig type ('constr, 'types) pt = - | LocalAssum of Id.t list * 'types - | LocalDef of Id.t list * 'constr * 'types + | LocalAssum of Id.t binder_annot list * 'types + | LocalDef of Id.t binder_annot list * 'constr * 'types val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt val of_named_decl : ('c, 't) Named.Declaration.pt -> ('c, 't) pt diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 22de9bfad5..9b974c4ecc 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -21,6 +21,7 @@ open Term open Constr open Declarations open Univ +open Context module NamedDecl = Context.Named.Declaration module RelDecl = Context.Rel.Declaration @@ -134,12 +135,12 @@ let abstract_context hyps = | NamedDecl.LocalDef (id, b, t) -> let b = Vars.subst_vars subst b in let t = Vars.subst_vars subst t in - id, RelDecl.LocalDef (Name id, b, t) + id, RelDecl.LocalDef (map_annot Name.mk_name id, b, t) | NamedDecl.LocalAssum (id, t) -> let t = Vars.subst_vars subst t in - id, RelDecl.LocalAssum (Name id, t) + id, RelDecl.LocalAssum (map_annot Name.mk_name id, t) in - (decl :: ctx, id :: subst) + (decl :: ctx, id.binder_name :: subst) in Context.Named.fold_outside fold hyps ~init:([], []) @@ -159,6 +160,7 @@ type result = { cook_type : types; cook_universes : universes; cook_private_univs : Univ.ContextSet.t option; + cook_relevance : Sorts.relevance; cook_inline : inline; cook_context : Constr.named_context option; } @@ -241,6 +243,7 @@ let cook_constant ~hcons { from = cb; info } = cook_type = typ; cook_universes = univs; cook_private_univs = private_univs; + cook_relevance = cb.const_relevance; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; } diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 89b5c60ad5..b0f143c47d 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -22,6 +22,7 @@ type result = { cook_type : types; cook_universes : universes; cook_private_univs : Univ.ContextSet.t option; + cook_relevance : Sorts.relevance; cook_inline : inline; cook_context : Constr.named_context option; } diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 567850645e..5551742c02 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -91,6 +91,7 @@ type constant_body = { const_hyps : Constr.named_context; (** New: younger hyp at top *) const_body : Constr.t Mod_subst.substituted constant_def; const_type : types; + const_relevance : Sorts.relevance; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : universes; const_private_poly_univs : Univ.ContextSet.t option; @@ -133,7 +134,7 @@ v} type record_info = | NotRecord | FakeRecord -| PrimRecord of (Id.t * Label.t array * types array) array +| PrimRecord of (Id.t * Label.t array * Sorts.relevance array * types array) array type regular_inductive_arity = { mind_user_arity : types; @@ -176,6 +177,8 @@ type one_inductive_body = { mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *) + mind_relevance : Sorts.relevance; + (** {8 Datas for bytecode compilation } *) mind_nb_constant : int; (** number of constant constructor *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index d56502a095..de9a052096 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -114,6 +114,7 @@ let subst_const_body sub cb = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; const_private_poly_univs = cb.const_private_poly_univs; + const_relevance = cb.const_relevance; const_inline_code = cb.const_inline_code; const_typing_flags = cb.const_typing_flags } @@ -222,6 +223,7 @@ let subst_mind_packet sub mbp = mind_nrealdecls = mbp.mind_nrealdecls; mind_kelim = mbp.mind_kelim; mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); + mind_relevance = mbp.mind_relevance; mind_nb_constant = mbp.mind_nb_constant; mind_nb_args = mbp.mind_nb_args; mind_reloc_tbl = mbp.mind_reloc_tbl } @@ -230,10 +232,10 @@ let subst_mind_record sub r = match r with | NotRecord -> NotRecord | FakeRecord -> FakeRecord | PrimRecord infos -> - let map (id, ps, pb as info) = + let map (id, ps, rs, pb as info) = let pb' = Array.Smart.map (subst_mps sub) pb in if pb' == pb then info - else (id, ps, pb') + else (id, ps, rs, pb') in let infos' = Array.Smart.map map infos in if infos' == infos then r else PrimRecord infos' @@ -269,21 +271,32 @@ let inductive_make_projection ind mib ~proj_arg = match mib.mind_record with | NotRecord | FakeRecord -> None | PrimRecord infos -> + let _, labs, _, _ = infos.(snd ind) in Some (Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg - (pi2 infos.(snd ind)).(proj_arg)) + labs.(proj_arg)) let inductive_make_projections ind mib = match mib.mind_record with | NotRecord | FakeRecord -> None | PrimRecord infos -> + let _, labs, _, _ = infos.(snd ind) in let projs = Array.mapi (fun proj_arg lab -> Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab) - (pi2 infos.(snd ind)) + labs in Some projs +let relevance_of_projection_repr mib p = + let _mind,i = Names.Projection.Repr.inductive p in + match mib.mind_record with + | NotRecord | FakeRecord -> + CErrors.anomaly ~label:"relevance_of_projection" Pp.(str "not a projection") + | PrimRecord infos -> + let _,_,rs,_ = infos.(i) in + rs.(Names.Projection.Repr.arg p) + (** {6 Hash-consing of inductive declarations } *) let hcons_regular_ind_arity a = diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 23a44433b3..54a853fc81 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -70,6 +70,8 @@ val inductive_make_projection : Names.inductive -> mutual_inductive_body -> proj val inductive_make_projections : Names.inductive -> mutual_inductive_body -> Names.Projection.Repr.t array option +val relevance_of_projection_repr : mutual_inductive_body -> Names.Projection.Repr.t -> Sorts.relevance + (** {6 Kernel flags} *) (** A default, safe set of flags for kernel type-checking *) diff --git a/kernel/environ.ml b/kernel/environ.ml index ab046f02f7..97c9f8654a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -59,7 +59,8 @@ type globals = { type stratification = { env_universes : UGraph.t; - env_engagement : engagement + env_engagement : engagement; + env_sprop_allowed : bool; } type val_kind = @@ -117,7 +118,9 @@ let empty_env = { env_nb_rel = 0; env_stratification = { env_universes = UGraph.initial_universes; - env_engagement = PredicativeSet }; + env_engagement = PredicativeSet; + env_sprop_allowed = false; + }; env_typing_flags = Declareops.safe_flags Conv_oracle.empty; retroknowledge = Retroknowledge.empty; indirect_pterms = Opaqueproof.empty_opaquetab } @@ -243,7 +246,7 @@ let is_impredicative_set env = | _ -> false let is_impredicative_sort env = function - | Sorts.Prop -> true + | Sorts.SProp | Sorts.Prop -> true | Sorts.Set -> is_impredicative_set env | Sorts.Type _ -> false @@ -432,6 +435,14 @@ let set_typing_flags c env = (* Unsafe *) if same_flags env.env_typing_flags c then env else { env with env_typing_flags = c } +let make_sprop_cumulative = map_universes UGraph.make_sprop_cumulative + +let set_allow_sprop b env = + { env with env_stratification = + { env.env_stratification with env_sprop_allowed = b } } + +let sprop_allowed env = env.env_stratification.env_sprop_allowed + (* Global constants *) let no_link_info = NotLinked @@ -537,7 +548,7 @@ let lookup_projection p env = match mib.mind_record with | NotRecord | FakeRecord -> anomaly ~label:"lookup_projection" Pp.(str "not a projection") | PrimRecord infos -> - let _,_,typs = infos.(i) in + let _,_,_,typs = infos.(i) in typs.(Projection.arg p) let get_projection env ind ~proj_arg = diff --git a/kernel/environ.mli b/kernel/environ.mli index 0df9b91c4a..8c6bc105c7 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -51,7 +51,8 @@ type globals type stratification = { env_universes : UGraph.t; - env_engagement : engagement + env_engagement : engagement; + env_sprop_allowed : bool; } type named_context_val = private { @@ -290,6 +291,9 @@ val push_subgraph : Univ.ContextSet.t -> env -> env val set_engagement : engagement -> env -> env val set_typing_flags : typing_flags -> env -> env +val make_sprop_cumulative : env -> env +val set_allow_sprop : bool -> env -> env +val sprop_allowed : env -> bool val universes_of_global : env -> GlobRef.t -> AUContext.t diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index a5dafc5ab5..4e6e595331 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -122,73 +122,106 @@ let check_cumulativity univs variances env_ar params data = (************************** Type checking *******************************) (************************************************************************) -type univ_info = { ind_squashed : bool; +type univ_info = { ind_squashed : bool; ind_has_relevant_arg : bool; ind_min_univ : Universe.t option; (* Some for template *) ind_univ : Universe.t } -let check_univ_leq env u info = +let check_univ_leq ?(is_real_arg=false) env u info = let ind_univ = info.ind_univ in - if type_in_type env || (UGraph.check_leq (universes env) u ind_univ) + let info = if not info.ind_has_relevant_arg && is_real_arg && not (Univ.Universe.is_sprop u) + then {info with ind_has_relevant_arg=true} + else info + in + (* Inductive types provide explicit lifting from SProp to other universes, so allow SProp <= any. *) + if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ } else if is_impredicative_univ env ind_univ then if Option.is_empty info.ind_min_univ then { info with ind_squashed = true } else raise (InductiveError BadUnivs) else raise (InductiveError BadUnivs) -let check_indices_matter env_params info indices = - let check_index d (info,env) = +let check_context_univs ~ctor env info ctx = + let check_one d (info,env) = let info = match d with | LocalAssum (_,t) -> (* could be retyping if it becomes available in the kernel *) let tj = Typeops.infer_type env t in - check_univ_leq env (Sorts.univ_of_sort tj.utj_type) info + check_univ_leq ~is_real_arg:ctor env (Sorts.univ_of_sort tj.utj_type) info | LocalDef _ -> info in info, push_rel d env in + fst (Context.Rel.fold_outside ~init:(info,env) check_one ctx) + +let check_indices_matter env_params info indices = if not (indices_matter env_params) then info - else fst (Context.Rel.fold_outside ~init:(info,env_params) check_index indices) + else check_context_univs ~ctor:false env_params info indices (* env_ar contains the inductives before the current ones in the block, and no parameters *) let check_arity env_params env_ar ind = let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in let indices, ind_sort = Reduction.dest_arity env_params arity in let ind_min_univ = if ind.mind_entry_template then Some Universe.type0m else None in - let univ_info = {ind_squashed=false;ind_min_univ;ind_univ=Sorts.univ_of_sort ind_sort} in + let univ_info = { + ind_squashed=false; + ind_has_relevant_arg=false; + ind_min_univ; + ind_univ=Sorts.univ_of_sort ind_sort; + } + in let univ_info = check_indices_matter env_params univ_info indices in (* We do not need to generate the universe of the arity with params; if later, after the validation of the inductive definition, full_arity is used as argument or subject to cast, an upper universe will be generated *) let arity = it_mkProd_or_LetIn arity (Environ.rel_context env_params) in - push_rel (LocalAssum (Name ind.mind_entry_typename, arity)) env_ar, + let x = Context.make_annot (Name ind.mind_entry_typename) (Sorts.relevance_of_sort ind_sort) in + push_rel (LocalAssum (x, arity)) env_ar, (arity, indices, univ_info) -let check_constructor_univs env_ar_par univ_info (args,_) = +let check_constructor_univs env_ar_par info (args,_) = (* We ignore the output, positivity will check that it's the expected inductive type *) - (* NB: very similar to check_indices_matter but that will change with SProp *) - fst (Context.Rel.fold_outside ~init:(univ_info,env_ar_par) (fun d (univ_info,env) -> - let univ_info = match d with - | LocalDef _ -> univ_info - | LocalAssum (_,t) -> - (* could be retyping if it becomes available in the kernel *) - let tj = Typeops.infer_type env t in - check_univ_leq env (Sorts.univ_of_sort tj.utj_type) univ_info - in - univ_info, push_rel d env) - args) - -let check_constructors env_ar_par params lc (arity,indices,univ_info) = + check_context_univs ~ctor:true env_ar_par info args + +let check_constructors env_ar_par isrecord params lc (arity,indices,univ_info) = let lc = Array.map_of_list (fun c -> (Typeops.infer_type env_ar_par c).utj_val) lc in let splayed_lc = Array.map (Reduction.dest_prod_assum env_ar_par) lc in - let univ_info = if Array.length lc <= 1 then univ_info - else check_univ_leq env_ar_par Univ.Universe.type0 univ_info + let univ_info = match Array.length lc with + (* Empty type: all OK *) + | 0 -> univ_info + + (* SProp primitive records are OK, if we squash and become fakerecord also OK *) + | 1 when isrecord -> univ_info + + (* Unit and identity types must squash if SProp *) + | 1 -> check_univ_leq env_ar_par Univ.Universe.type0m univ_info + + (* More than 1 constructor: must squash if Prop/SProp *) + | _ -> check_univ_leq env_ar_par Univ.Universe.type0 univ_info in let univ_info = Array.fold_left (check_constructor_univs env_ar_par) univ_info splayed_lc in (* generalize the constructors over the parameters *) let lc = Array.map (fun c -> Term.it_mkProd_or_LetIn c params) lc in (arity, lc), (indices, splayed_lc), univ_info +let check_record data = + List.for_all (fun (_,(_,splayed_lc),info) -> + (* records must have all projections definable -> equivalent to not being squashed *) + not info.ind_squashed + (* relevant records must have at least 1 relevant argument *) + && (Univ.Universe.is_sprop info.ind_univ + || info.ind_has_relevant_arg) + && (match splayed_lc with + (* records must have 1 constructor with at least 1 argument, and no anonymous fields *) + | [|ctx,_|] -> + let module D = Context.Rel.Declaration in + List.exists D.is_local_assum ctx && + List.for_all (fun d -> not (D.is_local_assum d) + || not (Name.is_anonymous (D.get_name d))) + ctx + | _ -> false)) + data + (* Allowed eliminations *) (* Previous comment: *) @@ -199,16 +232,18 @@ let check_constructors env_ar_par params lc (arity,indices,univ_info) = (* - all_sorts in case of small, unitary Prop (not smashed) *) (* - logical_sorts in case of large, unitary Prop (smashed) *) -let all_sorts = [InProp;InSet;InType] -let small_sorts = [InProp;InSet] -let logical_sorts = [InProp] +let all_sorts = [InSProp;InProp;InSet;InType] +let small_sorts = [InSProp;InProp;InSet] +let logical_sorts = [InSProp;InProp] +let sprop_sorts = [InSProp] -let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_} = +let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} = if not ind_squashed then all_sorts else match Sorts.family (Sorts.sort_of_univ ind_univ) with | InType -> assert false | InSet -> small_sorts | InProp -> logical_sorts + | InSProp -> sprop_sorts (* Returns the list [x_1, ..., x_n] of levels contributing to template polymorphism. The elements x_k is None if the k-th parameter (starting @@ -268,18 +303,38 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = in (* Params *) - let env_params = Typeops.check_context env_univs mie.mind_entry_params in - let params = Environ.rel_context env_params in + let env_params, params = Typeops.check_context env_univs mie.mind_entry_params in (* Arities *) let env_ar, data = List.fold_left_map (check_arity env_params) env_univs mie.mind_entry_inds in let env_ar_par = push_rel_context params env_ar in (* Constructors *) - let data = List.map2 (fun ind data -> check_constructors env_ar_par params ind.mind_entry_lc data) + let isrecord = match mie.mind_entry_record with + | Some (Some _) -> true + | Some None | None -> false + in + let data = List.map2 (fun ind data -> + check_constructors env_ar_par isrecord params ind.mind_entry_lc data) mie.mind_entry_inds data in + let record = mie.mind_entry_record in + let data, record = match record with + | None | Some None -> data, record + | Some (Some _) -> + if check_record data then + data, record + else + (* if someone tried to declare a record as SProp but it can't + be primitive we must squash. *) + let data = List.map (fun (a,b,univs) -> + a,b,check_univ_leq env_ar_par Univ.Universe.type0m univs) + data + in + data, Some None + in + let () = match mie.mind_entry_variance with | None -> () | Some variances -> @@ -298,4 +353,4 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = Environ.push_rel_context ctx env in - env_ar_par, univs, mie.mind_entry_variance, params, Array.of_list data + env_ar_par, univs, mie.mind_entry_variance, record, params, Array.of_list data diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 2598548f3f..ad51af66a2 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -17,6 +17,7 @@ open Declarations - environment with inductives + parameters in rel context - abstracted universes - checked variance info + - record entry (checked to be OK) - parameters - for each inductive, (arity * constructors) (with params) @@ -26,6 +27,7 @@ open Declarations val typecheck_inductive : env -> mutual_inductive_entry -> env * universes * Univ.Variance.t array option + * Names.Id.t array option option * Constr.rel_context * ((inductive_arity * Constr.types array) * (Constr.rel_context * (Constr.rel_context * Constr.types) array) * diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 457c17907e..009eb3da38 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -173,7 +173,9 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = let specif = (lookup_mind_specif env mi, u) in let ty = type_of_inductive env specif in let env' = - let decl = LocalAssum (Anonymous, hnf_prod_applist env ty lrecparams) in + let r = (snd (fst specif)).mind_relevance in + let anon = Context.make_annot Anonymous r in + let decl = LocalAssum (anon, hnf_prod_applist env ty lrecparams) in push_rel decl env in let ra_env' = (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: @@ -186,8 +188,8 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = if Int.equal n 0 then (ienv,c) else let c' = whd_all env c in match kind c' with - Prod(na,a,b) -> - let ienv' = ienv_push_var ienv (na,a,mk_norec) in + Prod(na,a,b) -> + let ienv' = ienv_push_var ienv (na,a,mk_norec) in ienv_decompose_prod ienv' (n-1) b | _ -> assert false @@ -215,7 +217,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = let x,largs = decompose_app (whd_all env c) in match kind x with - | Prod (na,b,d) -> + | Prod (na,b,d) -> let () = assert (List.is_empty largs) in (** If one of the inductives of the mutually inductive block occurs in the left-hand side of a product, then @@ -406,8 +408,6 @@ let used_section_variables env inds = let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) let rel_list n m = Array.to_list (rel_vect n m) -exception UndefinableExpansion - (** From a rel context describing the constructor arguments, build an expansion function. The term built is expecting to be substituted first by @@ -433,7 +433,7 @@ let compute_projections (kn, i as ind) mib = mkRel 1 :: List.map (lift 1) subst in subst in - let projections decl (i, j, labs, pbs, letsubst) = + let projections decl (i, j, labs, rs, pbs, letsubst) = match decl with | LocalDef (_na,c,_t) -> (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] @@ -445,10 +445,11 @@ let compute_projections (kn, i as ind) mib = (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)] to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *) let letsubst = c2 :: letsubst in - (i, j+1, labs, pbs, letsubst) + (i, j+1, labs, rs, pbs, letsubst) | LocalAssum (na,t) -> - match na with + match na.Context.binder_name with | Name id -> + let r = na.Context.binder_relevance in let lab = Label.of_id id in let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:i lab in (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)] @@ -460,14 +461,15 @@ let compute_projections (kn, i as ind) mib = (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)] to [params, x:I |- t(proj1 x,..,projj x)] *) let fterm = mkProj (Projection.make kn false, mkRel 1) in - (i + 1, j + 1, lab :: labs, projty :: pbs, fterm :: letsubst) - | Anonymous -> raise UndefinableExpansion + (i + 1, j + 1, lab :: labs, r :: rs, projty :: pbs, fterm :: letsubst) + | Anonymous -> assert false (* checked by indTyping *) in - let (_, _, labs, pbs, _letsubst) = - List.fold_right projections ctx (0, 1, [], [], paramsletsubst) + let (_, _, labs, rs, pbs, _letsubst) = + List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst) in - Array.of_list (List.rev labs), - Array.of_list (List.rev pbs) + Array.of_list (List.rev labs), + Array.of_list (List.rev rs), + Array.of_list (List.rev pbs) let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in @@ -483,7 +485,11 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite splayed_lc in let consnrealargs = Array.map (fun (d,_) -> Context.Rel.nhyps d) - splayed_lc in + splayed_lc in + let mind_relevance = match arity with + | RegularArity { mind_sort;_ } -> Sorts.relevance_of_sort mind_sort + | TemplateArity _ -> Sorts.Relevant + in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in let transf num = @@ -510,8 +516,9 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite mind_consnrealargs = consnrealargs; mind_user_lc = lc; mind_nf_lc = nf_lc; - mind_recargs = recarg; - mind_nb_constant = !nconst; + mind_recargs = recarg; + mind_relevance; + mind_nb_constant = !nconst; mind_nb_args = !nblock; mind_reloc_tbl = rtbl; } in @@ -534,24 +541,12 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite in let record_info = match isrecord with | Some (Some rid) -> - let is_record pkt = - if Array.length pkt.mind_consnames != 1 then - user_err ~hdr:"build_inductive" - Pp.(str "Primitive records must have exactly one constructor.") - else if pkt.mind_consnrealargs.(0) = 0 then - user_err ~hdr:"build_inductive" - Pp.(str "Primitive records must have at least one constructor argument.") - else List.exists (Sorts.family_equal Sorts.InType) pkt.mind_kelim - in (** The elimination criterion ensures that all projections can be defined. *) - if Array.for_all is_record packets then - let map i id = - let labs, projs = compute_projections (kn, i) mib in - (id, labs, projs) - in - try PrimRecord (Array.mapi map rid) - with UndefinableExpansion -> FakeRecord - else FakeRecord + let map i id = + let labs, rs, projs = compute_projections (kn, i) mib in + (id, labs, rs, projs) + in + PrimRecord (Array.mapi map rid) | Some None -> FakeRecord | None -> NotRecord in @@ -562,7 +557,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite let check_inductive env kn mie = (* First type-check the inductive definition *) - let (env_ar_par, univs, variance, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in + let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in (* Then check positivity conditions *) let chkpos = (Environ.typing_flags env).check_guarded in let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames) @@ -574,5 +569,5 @@ let check_inductive env kn mie = in (* Build the inductive packets *) build_inductive env names mie.mind_entry_private univs variance - paramsctxt kn mie.mind_entry_record mie.mind_entry_finite + paramsctxt kn record mie.mind_entry_finite inds nmr recargs diff --git a/kernel/inductive.ml b/kernel/inductive.ml index f4c2483c14..7452038ba5 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -188,13 +188,17 @@ let instantiate_universes env ctx ar argsorts = (* Non singleton type not containing types are interpretable in Set *) else if is_type0_univ level then Sorts.set (* This is a Type with constraints *) - else Sorts.Type level + else Sorts.sort_of_univ level in (ctx, ty) (* Type of an inductive type *) -let type_of_inductive_gen ?(polyprop=true) env ((_mib,mip),u) paramtyps = +let relevance_of_inductive env ind = + let _, mip = lookup_mind_specif env ind in + mip.mind_relevance + +let type_of_inductive_gen ?(polyprop=true) env ((_,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> @@ -226,7 +230,10 @@ let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = (* The max of an array of universes *) let cumulate_constructor_univ u = let open Sorts in function - | Prop -> u + | SProp | Prop -> + (* SProp is non cumulative but allowed in constructors of any + inductive (except non-sprop primitive records) *) + u | Set -> Universe.sup Universe.type0 u | Type u' -> Universe.sup u u' @@ -298,16 +305,12 @@ let build_dependent_inductive ind (_,mip) params = @ Context.Rel.to_extended_list mkRel 0 realargs) (* This exception is local *) -exception LocalArity of (Sorts.family * Sorts.family * arity_error) option +exception LocalArity of (Sorts.family list * Sorts.family * Sorts.family * arity_error) option let check_allowed_sort ksort specif = - let open Sorts in - let eq_ksort s = match ksort, s with - | InProp, InProp | InSet, InSet | InType, InType -> true - | _ -> false in - if not (CList.exists eq_ksort (elim_sorts specif)) then + if not (CList.exists (Sorts.family_equal ksort) (elim_sorts specif)) then let s = inductive_sort_family (snd specif) in - raise (LocalArity (Some(ksort,s,error_elim_explain ksort s))) + raise (LocalArity (Some(elim_sorts specif, ksort,s,error_elim_explain ksort s))) let is_correct_arity env c pj ind specif params = let arsign,_ = get_instantiated_arity ind specif params in @@ -321,7 +324,7 @@ let is_correct_arity env c pj ind specif params = srec (push_rel (LocalAssum (na1,a1)) env) t ar' (* The last Prod domain is the type of the scrutinee *) | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) - let env' = push_rel (LocalAssum (na1,a1)) env in + let env' = push_rel (LocalAssum (na1,a1)) env in let ksort = match kind (whd_all env' a2) with | Sort s -> Sorts.family s | _ -> raise (LocalArity None) in @@ -337,7 +340,7 @@ let is_correct_arity env c pj ind specif params = in try srec env pj.uj_type (List.rev arsign) with LocalArity kinds -> - error_elim_arity env ind (elim_sorts specif) c pj kinds + error_elim_arity env ind c pj kinds (************************************************************************) @@ -380,13 +383,14 @@ let type_case_branches env (pind,largs) pj c = (************************************************************************) (* Checking the case annotation is relevant *) -let check_case_info env (indsp,u) ci = +let check_case_info env (indsp,u) r ci = let (mib,mip as spec) = lookup_mind_specif env indsp in if not (eq_ind indsp ci.ci_ind) || not (Int.equal mib.mind_nparams ci.ci_npar) || not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls) || not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs) || + not (ci.ci_relevance == r) || is_primitive_record spec then raise (TypeError(env,WrongCaseInfo((indsp,u),ci))) @@ -575,7 +579,9 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let mib = Environ.lookup_mind mind env in let ntypes = mib.mind_ntypes in let push_ind specif env = - let decl = LocalAssum (Anonymous, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in + let r = specif.mind_relevance in + let anon = Context.make_annot Anonymous r in + let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in @@ -596,7 +602,8 @@ let rec ienv_decompose_prod (env,_ as ienv) n c = let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0)) let dummy_implicit_sort = mkType (Universe.make dummy_univ) let lambda_implicit_lift n a = - let lambda_implicit a = mkLambda (Anonymous, dummy_implicit_sort, a) in + let anon = Context.make_annot Anonymous Sorts.Relevant in + let lambda_implicit a = mkLambda (anon, dummy_implicit_sort, a) in iterate lambda_implicit n (lift n a) (* This removes global parameters of the inductive types in lc (for @@ -1022,7 +1029,7 @@ let check_one_fix renv recpos trees def = check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body else match kind body with - | Lambda (x,a,b) -> + | Lambda (x,a,b) -> check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in check_nested_fix_body renv' (decr-1) recArgsDecrArg b @@ -1055,7 +1062,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = match kind (whd_all env def) with | Lambda (x,a,b) -> if noccur_with_meta n nbfix a then - let env' = push_rel (LocalAssum (x,a)) env in + let env' = push_rel (LocalAssum (x,a)) env in if Int.equal n (k + 1) then (* get the inductive type of the fixpoint *) let (mind, _) = @@ -1068,8 +1075,19 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (mind, (env', b)) else check_occur env' (n+1) b else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.") - | _ -> raise_err env i NotEnoughAbstractionInFixBody in - check_occur fixenv 1 def in + | _ -> raise_err env i NotEnoughAbstractionInFixBody + in + let ((ind, _), _) as res = check_occur fixenv 1 def in + let _, ind = lookup_mind_specif env ind in + (* recursive sprop means non record with projections -> squashed *) + if Sorts.Irrelevant == ind.mind_relevance + then + begin + if names.(i).Context.binder_relevance == Sorts.Relevant + then raise_err env i FixpointOnIrrelevantInductive + end; + res + in (* Do it on every fixpoint *) let rv = Array.map2_i find_ind nvect bodies in (Array.map fst rv, Array.map snd rv) @@ -1112,7 +1130,7 @@ let rec codomain_is_coind env c = let b = whd_all env c in match kind b with | Prod (x,a,b) -> - codomain_is_coind (push_rel (LocalAssum (x,a)) env) b + codomain_is_coind (push_rel (LocalAssum (x,a)) env) b | _ -> (try find_coinductive env b with Not_found -> @@ -1150,7 +1168,7 @@ let check_one_cofix env nbfix def deftype = | _ -> anomaly_ill_typed () in process_args_of_constr (realargs, lra) - | Lambda (x,a,b) -> + | Lambda (x,a,b) -> let () = assert (List.is_empty args) in if noccur_with_meta n nbfix a then let env' = push_rel (LocalAssum (x,a)) env in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index ad35c16c22..997a620742 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -45,6 +45,8 @@ val constrained_type_of_inductive : env -> mind_specif puniverses -> types const val constrained_type_of_inductive_knowing_parameters : env -> mind_specif puniverses -> types Lazy.t array -> types constrained +val relevance_of_inductive : env -> inductive -> Sorts.relevance + val type_of_inductive : env -> mind_specif puniverses -> types val type_of_inductive_knowing_parameters : @@ -93,7 +95,7 @@ val inductive_sort_family : one_inductive_body -> Sorts.family (** Check a [case_info] actually correspond to a Case expression on the given inductive type. *) -val check_case_info : env -> pinductive -> case_info -> unit +val check_case_info : env -> pinductive -> Sorts.relevance -> case_info -> unit (** {6 Guard conditions for fix and cofix-points. } *) diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 5108744bde..59c1d5890f 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -26,6 +26,7 @@ Conv_oracle Environ Primred CClosure +Retypeops Reduction Clambda Nativelambda diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 421d932d9a..2de5faa6df 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -80,6 +80,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in + assert (j.uj_val == c); (* relevances should already be correct here *) let typ = cb.const_type in let cst' = Reduction.infer_conv_leq env' (Environ.universes env') j.uj_type typ in @@ -101,6 +102,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in + assert (j.uj_val == c); (* relevances should already be correct here *) let typ = cb.const_type in let cst' = Reduction.infer_conv_leq env' (Environ.universes env') j.uj_type typ in diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index df60899b95..2dab14e732 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -11,6 +11,7 @@ open CErrors open Names open Constr +open Context open Declarations open Util open Nativevalues @@ -763,7 +764,7 @@ let empty_env univ () = } let push_rel env id = - let local = fresh_lname id in + let local = fresh_lname id.binder_name in local, { env with env_rel = MLlocal local :: env.env_rel; env_bound = env.env_bound + 1 @@ -772,7 +773,7 @@ let push_rel env id = let push_rels env ids = let lnames, env_rel = Array.fold_left (fun (names,env_rel) id -> - let local = fresh_lname id in + let local = fresh_lname id.binder_name in (local::names, MLlocal local::env_rel)) ([],env.env_rel) ids in Array.of_list (List.rev lnames), { env with env_rel = env_rel; @@ -1945,7 +1946,7 @@ let compile_mind mb mind stack = let tbl = ob.mind_reloc_tbl in (* Building info *) let ci = { ci_ind = ind; ci_npar = nparams; - ci_cstr_nargs = [|0|]; + ci_cstr_nargs = [|0|]; ci_relevance = ob.mind_relevance; ci_cstr_ndecls = [||] (*FIXME*); ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in let asw = { asw_ind = ind; asw_prefix = ""; asw_ci = ci; @@ -1968,7 +1969,7 @@ let compile_mind mb mind stack = let projs = match mb.mind_record with | NotRecord | FakeRecord -> [] | PrimRecord info -> - let _, _, pbs = info.(i) in + let _, _, _, pbs = info.(i) in Array.fold_left_i add_proj [] pbs in projs @ constructors @ gtype :: accu :: stack diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 0869f94042..ec3a7b893d 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -26,9 +26,9 @@ type lambda = | Lmeta of metavariable * lambda (* type *) | Levar of Evar.t * lambda array (* arguments *) | Lprod of lambda * lambda - | Llam of Name.t array * lambda - | Lrec of Name.t * lambda - | Llet of Name.t * lambda * lambda + | Llam of Name.t Context.binder_annot array * lambda + | Lrec of Name.t Context.binder_annot * lambda + | Llet of Name.t Context.binder_annot * lambda * lambda | Lapp of lambda * lambda array | Lconst of prefix * pconstant | Lproj of prefix * inductive * int (* prefix, inductive, index starting from 0 *) @@ -51,9 +51,9 @@ type lambda = | Llazy | Lforce -and lam_branches = (constructor * Name.t array * lambda) array +and lam_branches = (constructor * Name.t Context.binder_annot array * lambda) array -and fix_decl = Name.t array * lambda array * lambda array +and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array type evars = { evars_val : existential -> constr option; @@ -362,7 +362,8 @@ let prim env kn p args = Lprim(prefix, kn, p, args) let expand_prim env kn op arity = - let ids = Array.make arity Anonymous in + (* primitives are always Relevant *) + let ids = Array.make arity Context.anonR in let args = make_args arity 1 in Llam(ids, prim env kn op args) @@ -395,7 +396,7 @@ module Cache = let get_construct_info cache env c : constructor_info = try ConstrTable.find cache c - with Not_found -> + with Not_found -> let ((mind,j), i) = c in let oib = lookup_mind mind env in let oip = oib.mind_packets.(j) in @@ -518,8 +519,10 @@ let rec lambda_of_constr cache env sigma c = else match b with | Llam(ids, body) when Int.equal (Array.length ids) arity -> (cn, ids, body) - | _ -> - let ids = Array.make arity Anonymous in + | _ -> + (** TODO relevance *) + let anon = Context.make_annot Anonymous Sorts.Relevant in + let ids = Array.make arity anon in let args = make_args arity 1 in let ll = lam_lift arity b in (cn, ids, mkLapp ll args) in diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index eb06522a33..b0de257a27 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -21,9 +21,9 @@ type lambda = | Lmeta of metavariable * lambda (* type *) | Levar of Evar.t * lambda array (* arguments *) | Lprod of lambda * lambda - | Llam of Name.t array * lambda - | Lrec of Name.t * lambda - | Llet of Name.t * lambda * lambda + | Llam of Name.t Context.binder_annot array * lambda + | Lrec of Name.t Context.binder_annot * lambda + | Llet of Name.t Context.binder_annot * lambda * lambda | Lapp of lambda * lambda array | Lconst of prefix * pconstant | Lproj of prefix * inductive * int (* prefix, inductive, index starting from 0 *) @@ -45,9 +45,9 @@ type lambda = | Llazy | Lforce -and lam_branches = (constructor * Name.t array * lambda) array +and lam_branches = (constructor * Name.t Context.binder_annot array * lambda) array -and fix_decl = Name.t array * lambda array * lambda array +and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array type evars = { evars_val : existential -> constr option; @@ -55,8 +55,8 @@ type evars = val empty_evars : evars -val decompose_Llam : lambda -> Name.t array * lambda -val decompose_Llam_Llet : lambda -> (Name.t * lambda option) array * lambda +val decompose_Llam : lambda -> Name.t Context.binder_annot array * lambda +val decompose_Llam_Llet : lambda -> (Name.t Context.binder_annot * lambda option) array * lambda val is_lazy : constr -> bool val mk_lazy : lambda -> lambda diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index a6b48cd7e3..3eb51ffc59 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -117,11 +117,11 @@ let mk_ind_accu ind u = let mk_sort_accu s u = let open Sorts in match s with - | Prop | Set -> mk_accu (Asort s) + | SProp | Prop | Set -> mk_accu (Asort s) | Type s -> let u = Univ.Instance.of_array u in - let s = Univ.subst_instance_universe u s in - mk_accu (Asort (Type s)) + let s = Sorts.sort_of_univ (Univ.subst_instance_universe u s) in + mk_accu (Asort s) let mk_var_accu id = mk_accu (Avar id) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b583d33e29..8c364602e9 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -293,12 +293,6 @@ let conv_table_key infos k1 k2 cuniv = exception IrregularPatternShape -let rec skip_pattern n c = - if Int.equal n 0 then c - else match kind c with - | Lambda (_, _, c) -> skip_pattern (pred n) c - | _ -> raise IrregularPatternShape - let unfold_ref_with_args infos tab fl v = match unfold_reference infos tab fl with | Def def -> Some (def, v) @@ -310,6 +304,7 @@ let unfold_ref_with_args infos tab fl v = type conv_tab = { cnv_inf : clos_infos; + relevances : Sorts.relevance list; lft_tab : clos_tab; rgt_tab : clos_tab; } @@ -319,9 +314,23 @@ type conv_tab = { (** The same heap separation invariant must hold for the fconstr arguments passed to each respective side of the conversion function below. *) +let push_relevance infos r = + { infos with relevances = r.Context.binder_relevance :: infos.relevances } + +let rec skip_pattern infos n c1 c2 = + if Int.equal n 0 then infos, c1, c2 + else match kind c1, kind c2 with + | Lambda (x, _, c1), Lambda (_, _, c2) -> skip_pattern (push_relevance infos x) (pred n) c1 c2 + | _ -> raise IrregularPatternShape + +let is_irrelevant infos lft c = + let env = info_env infos.cnv_inf in + try Retypeops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false + (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = - eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv + try eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv + with NotConvertible when is_irrelevant infos lft1 term1 && is_irrelevant infos lft2 term2 -> cuniv (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *) and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = @@ -399,14 +408,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = match unfold_projection infos.cnv_inf p2 with | Some s2 -> eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv - | None -> + | None -> if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2) - && compare_stack_shape v1 v2 then + && compare_stack_shape v1 v2 then let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 u1 - else (* Two projections in WHNF: unfold *) + else (* Two projections in WHNF: unfold *) raise NotConvertible) | (FProj (p1,c1), t2) -> @@ -446,22 +455,22 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Inconsistency: we tolerate that v1, v2 contain shift and update but we throw them away *) if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly (Pp.str "conversion was given ill-typed terms (FLambda)."); - let (_,ty1,bd1) = destFLambda mk_clos hd1 in + anomaly (Pp.str "conversion was given ill-typed terms (FLambda)."); + let (x1,ty1,bd1) = destFLambda mk_clos hd1 in let (_,ty2,bd2) = destFLambda mk_clos hd2 in let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in - ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv + ccnv CONV l2r (push_relevance infos x1) (el_lift el1) (el_lift el2) bd1 bd2 cuniv - | (FProd (_, c1, c2, e), FProd (_, c'1, c'2, e')) -> + | (FProd (x1, c1, c2, e), FProd (_, c'1, c'2, e')) -> if not (is_empty_stack v1 && is_empty_stack v2) then anomaly (Pp.str "conversion was given ill-typed terms (FProd)."); (* Luo's system *) let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in - ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) (mk_clos (subs_lift e) c2) (mk_clos (subs_lift e') c'2) cuniv + ccnv cv_pb l2r (push_relevance infos x1) (el_lift el1) (el_lift el2) (mk_clos (subs_lift e) c2) (mk_clos (subs_lift e') c'2) cuniv (* Eta-expansion on the fly *) | (FLambda _, _) -> @@ -470,19 +479,21 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | _ -> anomaly (Pp.str "conversion was given unreduced term (FLambda).") in - let (_,_ty1,bd1) = destFLambda mk_clos hd1 in + let (x1,_ty1,bd1) = destFLambda mk_clos hd1 in + let infos = push_relevance infos x1 in eqappr CONV l2r infos - (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv + (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv | (_, FLambda _) -> let () = match v2 with | [] -> () | _ -> anomaly (Pp.str "conversion was given unreduced term (FLambda).") in - let (_,_ty2,bd2) = destFLambda mk_clos hd2 in + let (x2,_ty2,bd2) = destFLambda mk_clos hd2 in + let infos = push_relevance infos x2 in eqappr CONV l2r infos - (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv - + (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv + (* only one constant, defined var or defined rel *) | (FFlex fl1, c2) -> begin match unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 with @@ -568,8 +579,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) - | (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) -> - if Int.equal i1 i2 && Array.equal Int.equal op1 op2 + | (FFix (((op1, i1),(na1,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) -> + if Int.equal i1 i2 && Array.equal Int.equal op1 op2 then let n = Array.length cl1 in let fty1 = Array.map (mk_clos e1) tys1 in @@ -580,12 +591,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let el2 = el_stack lft2 v2 in let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = + let infos = Array.fold_left push_relevance infos na1 in convert_vect l2r infos - (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in + (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible - | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) -> + | (FCoFix ((op1,(na1,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) -> if Int.equal op1 op2 then let n = Array.length cl1 in @@ -597,8 +610,10 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let el2 = el_stack lft2 v2 in let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = + let infos = Array.fold_left push_relevance infos na1 in convert_vect l2r infos - (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in + (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible @@ -662,8 +677,8 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv = (** Skip comparison of the pattern types. We know that the two terms are living in a common type, thus this check is useless. *) - let fold n c1 c2 cuniv = match skip_pattern n c1, skip_pattern n c2 with - | (c1, c2) -> + let fold n c1 c2 cuniv = match skip_pattern infos n c1 c2 with + | (infos, c1, c2) -> let lft1 = el_liftn n lft1 in let lft2 = el_liftn n lft2 in let e1 = subs_liftn n e1 in @@ -680,6 +695,7 @@ let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let infos = create_clos_infos ~evars reds env in let infos = { cnv_inf = infos; + relevances = List.map Context.Rel.Declaration.get_relevance (rel_context env); lft_tab = create_tab (); rgt_tab = create_tab (); } in @@ -701,7 +717,8 @@ let check_sort_cmp_universes env pb s0 s1 univs = | CONV -> check_eq univs u0 u1 in match (s0,s1) with - | Prop, Prop | Set, Set -> () + | SProp, SProp | Prop, Prop | Set, Set -> () + | SProp, _ | _, SProp -> raise NotConvertible | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible | Set, Prop -> raise NotConvertible | Set, Type u -> check_pb Univ.type0_univ u @@ -749,7 +766,8 @@ let infer_cmp_universes env pb s0 s1 univs = | CONV -> infer_eq univs u0 u1 in match (s0,s1) with - | Prop, Prop | Set, Set -> univs + | SProp, SProp | Prop, Prop | Set, Set -> univs + | SProp, _ | _, SProp -> raise NotConvertible | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs | Set, Prop -> raise NotConvertible | Set, Type u -> infer_pb Univ.type0_univ u @@ -894,7 +912,7 @@ let dest_prod env = let t = whd_all env c in match kind t with | Prod (n,a,c0) -> - let d = LocalAssum (n,a) in + let d = LocalAssum (n,a) in decrec (push_rel d env) (Context.Rel.add d m) c0 | _ -> m,t in diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml new file mode 100644 index 0000000000..204dec3eda --- /dev/null +++ b/kernel/retypeops.ml @@ -0,0 +1,116 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Names +open Constr +open Declarations +open Environ +open Context + +module RelDecl = Context.Rel.Declaration + +let relevance_of_rel env n = + let decl = lookup_rel n env in + RelDecl.get_relevance decl + +let relevance_of_var env x = + let decl = lookup_named x env in + Context.Named.Declaration.get_relevance decl + +let relevance_of_constant env c = + let decl = lookup_constant c env in + decl.const_relevance + +let relevance_of_constructor env ((mi,i),_) = + let decl = lookup_mind mi env in + let packet = decl.mind_packets.(i) in + packet.mind_relevance + +let relevance_of_projection env p = + let mind = Projection.mind p in + let mib = lookup_mind mind env in + Declareops.relevance_of_projection_repr mib (Projection.repr p) + +let rec relevance_of_rel_extra env extra n = + match extra with + | [] -> relevance_of_rel env n + | r :: _ when Int.equal n 1 -> r + | _ :: extra -> relevance_of_rel_extra env extra (n-1) + +let relevance_of_flex env extra lft = function + | ConstKey (c,_) -> relevance_of_constant env c + | VarKey x -> relevance_of_var env x + | RelKey p -> relevance_of_rel_extra env extra (Esubst.reloc_rel p lft) + +let rec relevance_of_fterm env extra lft f = + let open CClosure in + match CClosure.relevance_of f with + | KnownR -> Sorts.Relevant + | KnownI -> Sorts.Irrelevant + | Unknown -> + let r = match fterm_of f with + | FRel n -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft) + | FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c + | FFlex key -> relevance_of_flex env extra lft key + | FInt _ -> Sorts.Relevant + | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *) + | FConstruct (c,_) -> relevance_of_constructor env c + | FApp (f, _) -> relevance_of_fterm env extra lft f + | FProj (p, _) -> relevance_of_projection env p + | FFix (((_,i),(lna,_,_)), _) -> (lna.(i)).binder_relevance + | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance + | FCaseT (ci, _, _, _, _) -> ci.ci_relevance + | FLambda (len, tys, bdy, e) -> + let extra = List.rev_append (List.map (fun (x,_) -> binder_relevance x) tys) extra in + let lft = Esubst.el_liftn len lft in + relevance_of_term_extra env extra lft e bdy + | FLetIn (x, _, _, bdy, e) -> + relevance_of_term_extra env (x.binder_relevance :: extra) + (Esubst.el_lift lft) (Esubst.subs_lift e) bdy + | FLIFT (k, f) -> relevance_of_fterm env extra (Esubst.el_shft k lft) f + | FCLOS (c, e) -> relevance_of_term_extra env extra lft e c + + | FEvar (_, _) -> Sorts.Relevant (* let's assume evars are relevant for now *) + | FLOCKED -> assert false + in + CClosure.set_relevance r f; + r + +and relevance_of_term_extra env extra lft subs c = + match kind c with + | Rel n -> + (match Esubst.expand_rel n subs with + | Inl (k, f) -> relevance_of_fterm env extra (Esubst.el_liftn k lft) f + | Inr (n, _) -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft)) + | Var x -> relevance_of_var env x + | Sort _ | Ind _ | Prod _ -> Sorts.Relevant (* types are always relevant *) + | Cast (c, _, _) -> relevance_of_term_extra env extra lft subs c + | Lambda ({binder_relevance=r;_}, _, bdy) -> + relevance_of_term_extra env (r::extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy + | LetIn ({binder_relevance=r;_}, _, _, bdy) -> + relevance_of_term_extra env (r::extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy + | App (c, _) -> relevance_of_term_extra env extra lft subs c + | Const (c,_) -> relevance_of_constant env c + | Construct (c,_) -> relevance_of_constructor env c + | Case (ci, _, _, _) -> ci.ci_relevance + | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance + | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance + | Proj (p, _) -> relevance_of_projection env p + | Int _ -> Sorts.Relevant + + | Meta _ | Evar _ -> Sorts.Relevant (* let's assume metas and evars are relevant for now *) + +let relevance_of_fterm env extra lft c = + if Environ.sprop_allowed env then relevance_of_fterm env extra lft c + else Sorts.Relevant + +let relevance_of_term env c = + if Environ.sprop_allowed env + then relevance_of_term_extra env [] Esubst.el_id (Esubst.subs_id 0) c + else Sorts.Relevant diff --git a/kernel/retypeops.mli b/kernel/retypeops.mli new file mode 100644 index 0000000000..f30c541c3f --- /dev/null +++ b/kernel/retypeops.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** We can take advantage of non-cumulativity of SProp to avoid fully + retyping terms when we just want to know if they inhabit some + proof-irrelevant type. *) + +val relevance_of_term : Environ.env -> Constr.constr -> Sorts.relevance + +val relevance_of_fterm : Environ.env -> Sorts.relevance list -> + Esubst.lift -> CClosure.fconstr -> + Sorts.relevance + + +(** Helpers *) +open Names +val relevance_of_rel_extra : Environ.env -> Sorts.relevance list -> int -> Sorts.relevance +val relevance_of_var : Environ.env -> Id.t -> Sorts.relevance +val relevance_of_constant : Environ.env -> Constant.t -> Sorts.relevance +val relevance_of_constructor : Environ.env -> constructor -> Sorts.relevance +val relevance_of_projection : Environ.env -> Projection.t -> Sorts.relevance diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a05f7b9b04..edb1d0a02e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -211,6 +211,10 @@ let set_native_compiler b senv = let flags = Environ.typing_flags senv.env in set_typing_flags { flags with enable_native_compiler = b } senv +let make_sprop_cumulative senv = { senv with env = Environ.make_sprop_cumulative senv.env } + +let set_allow_sprop b senv = { senv with env = Environ.set_allow_sprop b senv.env } + (** Check that the engagement [c] expected by a library matches the current (initial) one *) let check_engagement env expected_impredicative_set = @@ -437,14 +441,16 @@ let safe_push_named d env = let push_named_def (id,de) senv = - let c, typ = Term_typing.translate_local_def senv.env id de in - let env'' = safe_push_named (LocalDef (id, c, typ)) senv.env in + let c, r, typ = Term_typing.translate_local_def senv.env id de in + let x = Context.make_annot id r in + let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in { senv with env = env'' } let push_named_assum ((id,t,poly),ctx) senv = let senv' = push_context_set poly ctx senv in - let t = Term_typing.translate_local_assum senv'.env t in - let env'' = safe_push_named (LocalAssum (id,t)) senv'.env in + let t, r = Term_typing.translate_local_assum senv'.env t in + let x = Context.make_annot id r in + let env'' = safe_push_named (LocalAssum (x,t)) senv'.env in {senv' with env=env''} @@ -603,7 +609,7 @@ let inline_side_effects env body side_eff = if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs) else (** Second step: compute the lifts and substitutions to apply *) - let cname c = Name (Label.to_id (Constant.label c)) in + let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r in let fold (subst, var, ctx, args) (c, cb, b) = let (b, opaque) = match cb.const_body, b with | Def b, _ -> (Mod_subst.force_constr b, false) @@ -616,7 +622,7 @@ let inline_side_effects env body side_eff = let ty = cb.const_type in let subst = Cmap_env.add c (Inr var) subst in let ctx = Univ.ContextSet.union ctx univs in - (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) + (subst, var + 1, ctx, (cname c cb.const_relevance, b, ty, opaque) :: args) | Polymorphic _ -> (** Inline the term to emulate universe polymorphism *) let subst = Cmap_env.add c (Inl b) subst in @@ -1239,7 +1245,7 @@ let check_register_ind ind r env = check_if (Constr.is_Type d) s; check_if (Constr.equal - (mkProd (Anonymous,mkRel 1, mkApp (mkRel 3,[|mkRel 2|]))) + (mkProd (Context.anonR,mkRel 1, mkApp (mkRel 3,[|mkRel 2|]))) cd) s in check_name 0 "C0"; diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 8539fdd504..46c97c1fb8 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -141,6 +141,8 @@ val set_typing_flags : Declarations.typing_flags -> safe_transformer0 val set_share_reduction : bool -> safe_transformer0 val set_VM : bool -> safe_transformer0 val set_native_compiler : bool -> safe_transformer0 +val make_sprop_cumulative : safe_transformer0 +val set_allow_sprop : bool -> safe_transformer0 val check_engagement : Environ.env -> Declarations.set_predicativity -> unit diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 566dce04c6..09c98ca1bc 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -10,13 +10,15 @@ open Univ -type family = InProp | InSet | InType +type family = InSProp | InProp | InSet | InType type t = + | SProp | Prop | Set | Type of Universe.t +let sprop = SProp let prop = Prop let set = Set let type1 = Type type1_univ @@ -25,15 +27,20 @@ let univ_of_sort = function | Type u -> u | Set -> Universe.type0 | Prop -> Universe.type0m + | SProp -> Universe.sprop let sort_of_univ u = - if is_type0m_univ u then prop + if Universe.is_sprop u then sprop + else if is_type0m_univ u then prop else if is_type0_univ u then set else Type u let compare s1 s2 = if s1 == s2 then 0 else match s1, s2 with + | SProp, SProp -> 0 + | SProp, _ -> -1 + | _, SProp -> 1 | Prop, Prop -> 0 | Prop, _ -> -1 | Set, Prop -> 1 @@ -44,34 +51,52 @@ let compare s1 s2 = let equal s1 s2 = Int.equal (compare s1 s2) 0 +let super = function + | SProp | Prop | Set -> Type (Universe.type1) + | Type u -> Type (Universe.super u) + +let is_sprop = function + | SProp -> true + | Prop | Set | Type _ -> false + let is_prop = function | Prop -> true - | Type u when Universe.equal Universe.type0m u -> true - | _ -> false + | SProp | Set | Type _ -> false let is_set = function | Set -> true - | Type u when Universe.equal Universe.type0 u -> true - | _ -> false + | SProp | Prop | Type _ -> false let is_small = function - | Prop | Set -> true - | Type u -> is_small_univ u + | SProp | Prop | Set -> true + | Type _ -> false let family = function + | SProp -> InSProp | Prop -> InProp | Set -> InSet - | Type u when is_type0m_univ u -> InProp - | Type u when is_type0_univ u -> InSet | Type _ -> InType +let family_compare a b = match a,b with + | InSProp, InSProp -> 0 + | InSProp, _ -> -1 + | _, InSProp -> 1 + | InProp, InProp -> 0 + | InProp, _ -> -1 + | _, InProp -> 1 + | InSet, InSet -> 0 + | InSet, _ -> -1 + | _, InSet -> 1 + | InType, InType -> 0 + let family_equal = (==) open Hashset.Combine let hash = function - | Prop -> combinesmall 1 0 - | Set -> combinesmall 1 1 + | SProp -> combinesmall 1 0 + | Prop -> combinesmall 1 1 + | Set -> combinesmall 1 2 | Type u -> let h = Univ.Universe.hash u in combinesmall 2 h @@ -103,12 +128,33 @@ module Hsorts = let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ +(** On binders: is this variable proof relevant *) +type relevance = Relevant | Irrelevant + +let relevance_equal r1 r2 = match r1,r2 with + | Relevant, Relevant | Irrelevant, Irrelevant -> true + | (Relevant | Irrelevant), _ -> false + +let relevance_of_sort_family = function + | InSProp -> Irrelevant + | _ -> Relevant + +let relevance_hash = function + | Relevant -> 0 + | Irrelevant -> 1 + +let relevance_of_sort = function + | SProp -> Irrelevant + | _ -> Relevant + let debug_print = function - | Set -> Pp.(str "Set") + | SProp -> Pp.(str "SProp") | Prop -> Pp.(str "Prop") + | Set -> Pp.(str "Set") | Type u -> Pp.(str "Type(" ++ Univ.Universe.pr u ++ str ")") let pr_sort_family = function - | InSet -> Pp.(str "Set") + | InSProp -> Pp.(str "SProp") | InProp -> Pp.(str "Prop") + | InSet -> Pp.(str "Set") | InType -> Pp.(str "Type") diff --git a/kernel/sorts.mli b/kernel/sorts.mli index 6c5ce4df80..c49728b146 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -10,13 +10,15 @@ (** {6 The sorts of CCI. } *) -type family = InProp | InSet | InType +type family = InSProp | InProp | InSet | InType -type t = +type t = private + | SProp | Prop | Set | Type of Univ.Universe.t +val sprop : t val set : t val prop : t val type1 : t @@ -25,6 +27,7 @@ val equal : t -> t -> bool val compare : t -> t -> int val hash : t -> int +val is_sprop : t -> bool val is_set : t -> bool val is_prop : t -> bool val is_small : t -> bool @@ -32,6 +35,7 @@ val family : t -> family val hcons : t -> t +val family_compare : family -> family -> int val family_equal : family -> family -> bool module List : sig @@ -42,6 +46,18 @@ end val univ_of_sort : t -> Univ.Universe.t val sort_of_univ : Univ.Universe.t -> t +val super : t -> t + +(** On binders: is this variable proof relevant *) +type relevance = Relevant | Irrelevant + +val relevance_hash : relevance -> int + +val relevance_equal : relevance -> relevance -> bool + +val relevance_of_sort : t -> relevance +val relevance_of_sort_family : family -> relevance + val debug_print : t -> Pp.t val pr_sort_family : family -> Pp.t diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index dea72e8b59..1857ea3329 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -23,6 +23,7 @@ open Declareops open Reduction open Inductive open Modops +open Context open Mod_subst (*i*) @@ -190,8 +191,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 check (fun mib -> mib.mind_record <> NotRecord) (==) (fun x -> RecordFieldExpected x); if mib1.mind_record <> NotRecord then begin let rec names_prod_letin t = match kind t with - | Prod(n,_,t) -> n::(names_prod_letin t) - | LetIn(n,_,_,t) -> n::(names_prod_letin t) + | Prod(n,_,t) -> n.binder_name::(names_prod_letin t) + | LetIn(n,_,_,t) -> n.binder_name::(names_prod_letin t) | Cast(t,_,_) -> names_prod_letin t | _ -> [] in diff --git a/kernel/term.ml b/kernel/term.ml index 58b289eaa5..f09c45715f 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -14,13 +14,14 @@ open CErrors open Names open Vars open Constr +open Context (* Deprecated *) -type sorts_family = Sorts.family = InProp | InSet | InType +type sorts_family = Sorts.family = InSProp | InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] -type sorts = Sorts.t = - | Prop | Set +type sorts = Sorts.t = private + | SProp | Prop | Set | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] @@ -32,9 +33,11 @@ type sorts = Sorts.t = (* Other term constructors *) (***************************) -let mkNamedProd id typ c = mkProd (Name id, typ, subst_var id c) -let mkNamedLambda id typ c = mkLambda (Name id, typ, subst_var id c) -let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, subst_var id c2) +let name_annot = map_annot Name.mk_name + +let mkNamedProd id typ c = mkProd (name_annot id, typ, subst_var id.binder_name c) +let mkNamedLambda id typ c = mkLambda (name_annot id, typ, subst_var id.binder_name c) +let mkNamedLetIn id c1 t c2 = mkLetIn (name_annot id, c1, t, subst_var id.binder_name c2) (* Constructs either [(x:t)c] or [[x=b:t]c] *) let mkProd_or_LetIn decl c = @@ -60,10 +63,11 @@ let mkNamedProd_wo_LetIn decl c = let open Context.Named.Declaration in match decl with | LocalAssum (id,t) -> mkNamedProd id t c - | LocalDef (id,b,_t) -> subst1 b (subst_var id c) + | LocalDef (id,b,_) -> subst1 b (subst_var id.binder_name c) (* non-dependent product t1 -> t2 *) -let mkArrow t1 t2 = mkProd (Anonymous, t1, t2) +let mkArrow t1 r t2 = mkProd (make_annot Anonymous r, t1, t2) +let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2 (* Constructs either [[x:t]c] or [[x=b:t]c] *) let mkLambda_or_LetIn decl c = @@ -366,8 +370,8 @@ let rec isArity c = type ('constr, 'types) kind_of_type = | SortType of Sorts.t | CastType of 'types * 'types - | ProdType of Name.t * 'types * 'types - | LetInType of Name.t * 'constr * 'types * 'types + | ProdType of Name.t Context.binder_annot * 'types * 'types + | LetInType of Name.t Context.binder_annot * 'constr * 'types * 'types | AtomicType of 'constr * 'constr array let kind_of_type t = match kind t with diff --git a/kernel/term.mli b/kernel/term.mli index 181d714ed7..4265324693 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -17,12 +17,15 @@ open Constr [forall (_:t1), t2]. Beware [t_2] is NOT lifted. Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 1) (mkRel 2))] *) -val mkArrow : types -> types -> constr +val mkArrow : types -> Sorts.relevance -> types -> constr + +val mkArrowR : types -> types -> constr +(** For an always-relevant domain *) (** Named version of the functions from [Term]. *) -val mkNamedLambda : Id.t -> types -> constr -> constr -val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr -val mkNamedProd : Id.t -> types -> types -> types +val mkNamedLambda : Id.t Context.binder_annot -> types -> constr -> constr +val mkNamedLetIn : Id.t Context.binder_annot -> constr -> types -> constr -> constr +val mkNamedProd : Id.t Context.binder_annot -> types -> types -> types (** Constructs either [(x:t)c] or [[x=b:t]c] *) val mkProd_or_LetIn : Constr.rel_declaration -> types -> types @@ -45,24 +48,24 @@ val appvectc : constr -> constr array -> constr (** [prodn n l b] = [forall (x_1:T_1)...(x_n:T_n), b] where [l] is [(x_n,T_n)...(x_1,T_1)...]. *) -val prodn : int -> (Name.t * constr) list -> constr -> constr +val prodn : int -> (Name.t Context.binder_annot * constr) list -> constr -> constr (** [compose_prod l b] @return [forall (x_1:T_1)...(x_n:T_n), b] where [l] is [(x_n,T_n)...(x_1,T_1)]. Inverse of [decompose_prod]. *) -val compose_prod : (Name.t * constr) list -> constr -> constr +val compose_prod : (Name.t Context.binder_annot * constr) list -> constr -> constr (** [lamn n l b] @return [fun (x_1:T_1)...(x_n:T_n) => b] where [l] is [(x_n,T_n)...(x_1,T_1)...]. *) -val lamn : int -> (Name.t * constr) list -> constr -> constr +val lamn : int -> (Name.t Context.binder_annot * constr) list -> constr -> constr (** [compose_lam l b] @return [fun (x_1:T_1)...(x_n:T_n) => b] where [l] is [(x_n,T_n)...(x_1,T_1)]. Inverse of [it_destLam] *) -val compose_lam : (Name.t * constr) list -> constr -> constr +val compose_lam : (Name.t Context.binder_annot * constr) list -> constr -> constr (** [to_lambda n l] @return [fun (x_1:T_1)...(x_n:T_n) => T] @@ -107,22 +110,22 @@ val prod_applist_assum : int -> types -> constr list -> types (** Transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. *) -val decompose_prod : constr -> (Name.t*constr) list * constr +val decompose_prod : constr -> (Name.t Context.binder_annot * constr) list * constr (** Transforms a lambda term {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a lambda. *) -val decompose_lam : constr -> (Name.t*constr) list * constr +val decompose_lam : constr -> (Name.t Context.binder_annot * constr) list * constr (** Given a positive integer n, decompose a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. Raise a user error if not enough products. *) -val decompose_prod_n : int -> constr -> (Name.t * constr) list * constr +val decompose_prod_n : int -> constr -> (Name.t Context.binder_annot * constr) list * constr (** Given a positive integer {% $ %}n{% $ %}, decompose a lambda term {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}. Raise a user error if not enough lambdas. *) -val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr +val decompose_lam_n : int -> constr -> (Name.t Context.binder_annot * constr) list * constr (** Extract the premisses and the conclusion of a term of the form "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *) @@ -183,17 +186,17 @@ val isArity : types -> bool type ('constr, 'types) kind_of_type = | SortType of Sorts.t | CastType of 'types * 'types - | ProdType of Name.t * 'types * 'types - | LetInType of Name.t * 'constr * 'types * 'types + | ProdType of Name.t Context.binder_annot * 'types * 'types + | LetInType of Name.t Context.binder_annot * 'constr * 'types * 'types | AtomicType of 'constr * 'constr array val kind_of_type : types -> (constr, types) kind_of_type (* Deprecated *) -type sorts_family = Sorts.family = InProp | InSet | InType +type sorts_family = Sorts.family = InSProp | InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] -type sorts = Sorts.t = - | Prop | Set +type sorts = Sorts.t = private + | SProp | Prop | Set | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 929f1c13a3..f773f800c6 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -21,7 +21,6 @@ open Constr open Declarations open Environ open Entries -open Typeops module NamedDecl = Context.Named.Declaration @@ -72,15 +71,16 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | Monomorphic_entry uctx -> push_context_set ~strict:true uctx env | Polymorphic_entry (_, uctx) -> push_context ~strict:false uctx env in - let j = infer env t in + let j = Typeops.infer env t in let usubst, univs = Declareops.abstract_universes uctx in - let c = Typeops.assumption_of_judgment env j in - let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in + let r = Typeops.assumption_of_judgment env j in + let t = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in { Cooking.cook_body = Undef nl; cook_type = t; cook_universes = univs; cook_private_univs = None; + cook_relevance = r; cook_inline = false; cook_context = ctx; } @@ -93,12 +93,12 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let env = push_context_set ~strict:true uctxt env in let ty = match otyp with | Some typ -> - let tyj = infer_type env typ in - check_primitive_type env op_t tyj.utj_val; - Constr.hcons tyj.utj_val + let typ = Typeops.infer_type env typ in + Typeops.check_primitive_type env op_t typ.utj_val; + Constr.hcons typ.utj_val | None -> match op_t with - | CPrimitives.OT_op op -> type_of_prim env op + | CPrimitives.OT_op op -> Typeops.type_of_prim env op | CPrimitives.OT_type _ -> mkSet in let cd = @@ -110,7 +110,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_universes = Monomorphic uctxt; cook_private_univs = None; cook_inline = false; - cook_context = None + cook_context = None; + cook_relevance = Sorts.Relevant; } (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, @@ -128,8 +129,8 @@ the polymorphic case const_entry_opaque = true; const_entry_universes = Monomorphic_entry univs; _ } as c) -> let env = push_context_set ~strict:true univs env in - let { const_entry_body = body; const_entry_feedback = feedback_id ; _ } = c in - let tyj = infer_type env typ in + let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in + let tyj = Typeops.infer_type env typ in let proofterm = Future.chain body (fun ((body,uctx),side_eff) -> (* don't redeclare universes which are declared for the type *) @@ -137,17 +138,17 @@ the polymorphic case let j, uctx = match trust with | Pure -> let env = push_context_set uctx env in - let j = infer env body in - let _ = judge_of_cast env j DEFAULTcast tyj in + let j = Typeops.infer env body in + let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in j, uctx | SideEffects handle -> let (body, uctx', valid_signatures) = handle env body side_eff in let uctx = Univ.ContextSet.union uctx uctx' in let env = push_context_set uctx env in let body,env,ectx = skip_trusted_seff valid_signatures body env in - let j = infer env body in + let j = Typeops.infer env body in let j = unzip ectx j in - let _ = judge_of_cast env j DEFAULTcast tyj in + let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in j, uctx in let c = Constr.hcons j.uj_val in @@ -156,9 +157,10 @@ the polymorphic case let def = OpaqueDef (Opaqueproof.create proofterm) in { Cooking.cook_body = def; - cook_type = typ; + cook_type = tyj.utj_val; cook_universes = Monomorphic univs; cook_private_univs = None; + cook_relevance = Sorts.relevance_of_sort tyj.utj_type; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } @@ -194,14 +196,14 @@ the polymorphic case in env, sbst, Polymorphic auctx, local in - let j = infer env body in + let j = Typeops.infer env body in let typ = match typ with | None -> Vars.subst_univs_level_constr usubst j.uj_type | Some t -> - let tj = infer_type env t in - let _ = judge_of_cast env j DEFAULTcast tj in - Vars.subst_univs_level_constr usubst t + let tj = Typeops.infer_type env t in + let _ = Typeops.judge_of_cast env j DEFAULTcast tj in + Vars.subst_univs_level_constr usubst tj.utj_val in let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in let def = @@ -214,6 +216,7 @@ the polymorphic case cook_type = typ; cook_universes = univs; cook_private_univs = private_univs; + cook_relevance = Retypeops.relevance_of_term env j.uj_val; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } @@ -309,6 +312,7 @@ let build_constant_declaration _kn env result = const_body_code = tps; const_universes = univs; const_private_poly_univs = result.cook_private_univs; + const_relevance = result.cook_relevance; const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } @@ -319,9 +323,9 @@ let translate_constant mb env kn ce = (infer_declaration ~trust:mb env ce) let translate_local_assum env t = - let j = infer env t in + let j = Typeops.infer env t in let t = Typeops.assumption_of_judgment env j in - t + j.uj_val, t let translate_recipe ~hcons env kn r = build_constant_declaration kn env (Cooking.cook_constant ~hcons r) @@ -366,7 +370,7 @@ let translate_local_def env _id centry = p | Undef _ | Primitive _ -> assert false in - c, typ + c, decl.cook_relevance, typ (* Insertion of inductive types. *) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index faf434c142..d34c28138e 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -27,9 +27,9 @@ type _ trust = | SideEffects : 'a effect_handler -> 'a trust val translate_local_def : env -> Id.t -> section_def_entry -> - constr * types + constr * Sorts.relevance * types -val translate_local_assum : env -> types -> types +val translate_local_assum : env -> types -> types * Sorts.relevance val translate_constant : 'a trust -> env -> Constant.t -> 'a constant_entry -> diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 481ffc290c..c45fe1cf00 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -33,6 +33,7 @@ type 'constr pguard_error = | RecCallInCasePred of 'constr | NotGuardedForm of 'constr | ReturnPredicateNotCoInductive of 'constr + | FixpointOnIrrelevantInductive type guard_error = constr pguard_error @@ -47,8 +48,8 @@ type ('constr, 'types) ptype_error = | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment | ReferenceVariables of Id.t * 'constr - | ElimArity of pinductive * Sorts.family list * 'constr * ('constr, 'types) punsafe_judgment - * (Sorts.family * Sorts.family * arity_error) option + | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment + * (Sorts.family list * Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info | NumberBranches of ('constr, 'types) punsafe_judgment * int @@ -59,11 +60,13 @@ type ('constr, 'types) ptype_error = | CantApplyBadType of (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array - | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array + | IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of - int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array + int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.Constraint.t | UndeclaredUniverse of Univ.Level.t + | DisallowedSProp + | BadRelevance type type_error = (constr, types) ptype_error @@ -102,8 +105,8 @@ let error_assumption env j = let error_reference_variables env id c = raise (TypeError (env, ReferenceVariables (id,c))) -let error_elim_arity env ind aritylst c pj okinds = - raise (TypeError (env, ElimArity (ind,aritylst,c,pj,okinds))) +let error_elim_arity env ind c pj okinds = + raise (TypeError (env, ElimArity (ind,c,pj,okinds))) let error_case_not_inductive env j = raise (TypeError (env, CaseNotInductive j)) @@ -149,6 +152,12 @@ let error_unsatisfied_constraints env c = let error_undeclared_universe env l = raise (TypeError (env, UndeclaredUniverse l)) +let error_disallowed_sprop env = + raise (TypeError (env, DisallowedSProp)) + +let error_bad_relevance env = + raise (TypeError (env, BadRelevance)) + let map_pguard_error f = function | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody | RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c) @@ -165,6 +174,7 @@ let map_pguard_error f = function | RecCallInCasePred c -> RecCallInCasePred (f c) | NotGuardedForm c -> NotGuardedForm (f c) | ReturnPredicateNotCoInductive c -> ReturnPredicateNotCoInductive (f c) +| FixpointOnIrrelevantInductive -> FixpointOnIrrelevantInductive let map_ptype_error f = function | UnboundRel n -> UnboundRel n @@ -172,7 +182,7 @@ let map_ptype_error f = function | NotAType j -> NotAType (on_judgment f j) | BadAssumption j -> BadAssumption (on_judgment f j) | ReferenceVariables (id, c) -> ReferenceVariables (id, f c) -| ElimArity (pi, dl, c, j, ar) -> ElimArity (pi, dl, f c, on_judgment f j, ar) +| ElimArity (pi, c, j, ar) -> ElimArity (pi, f c, on_judgment f j, ar) | CaseNotInductive j -> CaseNotInductive (on_judgment f j) | WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci) | NumberBranches (j, n) -> NumberBranches (on_judgment f j, n) @@ -189,3 +199,5 @@ let map_ptype_error f = function IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t) | UnsatisfiedConstraints g -> UnsatisfiedConstraints g | UndeclaredUniverse l -> UndeclaredUniverse l +| DisallowedSProp -> DisallowedSProp +| BadRelevance -> BadRelevance diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index c5ab9a4e73..88165a4f07 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -34,6 +34,7 @@ type 'constr pguard_error = | RecCallInCasePred of 'constr | NotGuardedForm of 'constr | ReturnPredicateNotCoInductive of 'constr + | FixpointOnIrrelevantInductive type guard_error = constr pguard_error @@ -48,8 +49,8 @@ type ('constr, 'types) ptype_error = | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment | ReferenceVariables of Id.t * 'constr - | ElimArity of pinductive * Sorts.family list * 'constr * ('constr, 'types) punsafe_judgment - * (Sorts.family * Sorts.family * arity_error) option + | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment + * (Sorts.family list * Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info | NumberBranches of ('constr, 'types) punsafe_judgment * int @@ -60,11 +61,13 @@ type ('constr, 'types) ptype_error = | CantApplyBadType of (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array - | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array + | IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of - int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array + int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.Constraint.t | UndeclaredUniverse of Univ.Level.t + | DisallowedSProp + | BadRelevance type type_error = (constr, types) ptype_error @@ -100,8 +103,8 @@ val error_assumption : env -> unsafe_judgment -> 'a val error_reference_variables : env -> Id.t -> constr -> 'a val error_elim_arity : - env -> pinductive -> Sorts.family list -> constr -> unsafe_judgment -> - (Sorts.family * Sorts.family * arity_error) option -> 'a + env -> pinductive -> constr -> unsafe_judgment -> + (Sorts.family list * Sorts.family * Sorts.family * arity_error) option -> 'a val error_case_not_inductive : env -> unsafe_judgment -> 'a @@ -123,10 +126,10 @@ val error_cant_apply_bad_type : unsafe_judgment -> unsafe_judgment array -> 'a val error_ill_formed_rec_body : - env -> guard_error -> Name.t array -> int -> env -> unsafe_judgment array -> 'a + env -> guard_error -> Name.t Context.binder_annot array -> int -> env -> unsafe_judgment array -> 'a val error_ill_typed_rec_body : - env -> int -> Name.t array -> unsafe_judgment array -> types array -> 'a + env -> int -> Name.t Context.binder_annot array -> unsafe_judgment array -> types array -> 'a val error_elim_explain : Sorts.family -> Sorts.family -> arity_error @@ -134,5 +137,9 @@ val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a val error_undeclared_universe : env -> Univ.Level.t -> 'a +val error_disallowed_sprop : env -> 'a + +val error_bad_relevance : env -> 'a + val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 227a164549..be878dd99b 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -12,8 +12,10 @@ open CErrors open Util open Names open Univ +open Sorts open Term open Constr +open Context open Vars open Declarations open Environ @@ -47,11 +49,32 @@ let check_type env c t = (* This should be a type intended to be assumed. The error message is not as useful as for [type_judgment]. *) -let check_assumption env t ty = - try let _ = check_type env t ty in t +let infer_assumption env t ty = + try + let s = check_type env t ty in + (match s with Sorts.SProp -> Irrelevant | _ -> Relevant) with TypeError _ -> error_assumption env (make_judge t ty) +let warn_bad_relevance_name = "bad-relevance" +let warn_bad_relevance = + CWarnings.create ~name:warn_bad_relevance_name ~category:"debug" ~default:CWarnings.Disabled + Pp.(function + | None -> str "Bad relevance in case annotation." + | Some x -> str "Bad relevance for binder " ++ Name.print x.binder_name ++ str ".") + +let warn_bad_relevance_ci ?loc () = warn_bad_relevance ?loc None +let warn_bad_relevance ?loc x = warn_bad_relevance ?loc (Some x) + +let check_assumption env x t ty = + let r = x.binder_relevance in + let r' = infer_assumption env t ty in + let x = if Sorts.relevance_equal r r' + then x + else (warn_bad_relevance x; {x with binder_relevance = r'}) + in + x + (************************************************) (* Incremental typing rules: builds a typing judgment given the *) (* judgments for the subterms. *) @@ -69,7 +92,7 @@ let type_of_type u = mkType uu let type_of_sort = function - | Prop | Set -> type1 + | SProp | Prop | Set -> type1 | Type u -> type_of_type u (*s Type of a de Bruijn index. *) @@ -220,7 +243,7 @@ let type_of_prim env t = in let rec nary_int63_op arity ty = if Int.equal arity 0 then ty - else Constr.mkProd(Name (Id.of_string "x"), int_ty, nary_int63_op (arity-1) ty) + else Constr.mkProd(Context.nameR (Id.of_string "x"), int_ty, nary_int63_op (arity-1) ty) in let return_ty = let open CPrimitives in @@ -264,6 +287,7 @@ let judge_of_int env i = let sort_of_product env domsort rangsort = match (domsort, rangsort) with + | (_, SProp) | (SProp, _) -> rangsort (* Product rule (s,Prop,Prop) *) | (_, Prop) -> rangsort (* Product rule (Prop/Set,Set,Set) *) @@ -275,13 +299,13 @@ let sort_of_product env domsort rangsort = rangsort else (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) - Type (Universe.sup Universe.type0 u1) + Sorts.sort_of_univ (Universe.sup Universe.type0 u1) (* Product rule (Prop,Type_i,Type_i) *) - | (Set, Type u2) -> Type (Universe.sup Universe.type0 u2) + | (Set, Type u2) -> Sorts.sort_of_univ (Universe.sup Universe.type0 u2) (* Product rule (Prop,Type_i,Type_i) *) | (Prop, Type _) -> rangsort (* Product rule (Type_i,Type_i,Type_i) *) - | (Type u1, Type u2) -> Type (Universe.sup u1 u2) + | (Type u1, Type u2) -> Sorts.sort_of_univ (Universe.sup u1 u2) (* [judge_of_product env name (typ1,s1) (typ2,s2)] implements the rule @@ -376,11 +400,17 @@ let type_of_case env ci p pt c ct _lf lft = let (pind, _ as indspec) = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - let () = check_case_info env pind ci in + let _, sp = try dest_arity env pt + with NotArity -> error_elim_arity env pind c (make_judge p pt) None in + let rp = Sorts.relevance_of_sort sp in + let ci = if ci.ci_relevance == rp then ci + else (warn_bad_relevance_ci (); {ci with ci_relevance=rp}) + in + let () = check_case_info env pind rp ci in let (bty,rslty) = type_case_branches env indspec (make_judge p pt) c in let () = check_branch_types env pind c ct lft bty in - rslty + ci, rslty let type_of_projection env p c ct = let pty = lookup_projection p env in @@ -455,6 +485,13 @@ let constr_of_global_in_context env r = (************************************************************************) (************************************************************************) +let check_binder_annot s x = + let r = x.binder_relevance in + let r' = Sorts.relevance_of_sort s in + if r' == r + then x + else (warn_bad_relevance x; {x with binder_relevance = r'}) + (* The typing machine. *) (* ATTENTION : faudra faire le typage du contexte des Const, Ind et Constructsi un jour cela devient des constructions @@ -463,88 +500,110 @@ let rec execute env cstr = let open Context.Rel.Declaration in match kind cstr with (* Atomic terms *) - | Sort s -> type_of_sort s + | Sort s -> + (match s with + | SProp -> if not (Environ.sprop_allowed env) then error_disallowed_sprop env + | _ -> ()); + cstr, type_of_sort s | Rel n -> - type_of_relative env n + cstr, type_of_relative env n | Var id -> - type_of_variable env id + cstr, type_of_variable env id | Const c -> - type_of_constant env c + cstr, type_of_constant env c | Proj (p, c) -> - let ct = execute env c in - type_of_projection env p c ct + let c', ct = execute env c in + let cstr = if c == c' then cstr else mkProj (p,c') in + cstr, type_of_projection env p c' ct (* Lambda calculus operators *) | App (f,args) -> - let argst = execute_array env args in - let ft = + let args', argst = execute_array env args in + let f', ft = match kind f with | Ind ind when Environ.template_polymorphic_pind ind env -> let args = Array.map (fun t -> lazy t) argst in - type_of_inductive_knowing_parameters env ind args + f, type_of_inductive_knowing_parameters env ind args | _ -> (* No template polymorphism *) execute env f in - - type_of_apply env f ft args argst + let cstr = if f == f' && args == args' then cstr else mkApp (f',args') in + cstr, type_of_apply env f' ft args' argst | Lambda (name,c1,c2) -> - let _ = execute_is_type env c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let c2t = execute env1 c2 in - type_of_abstraction env name c1 c2t + let c1', s = execute_is_type env c1 in + let name' = check_binder_annot s name in + let env1 = push_rel (LocalAssum (name',c1')) env in + let c2', c2t = execute env1 c2 in + let cstr = if name == name' && c1 == c1' && c2 == c2' then cstr else mkLambda(name',c1',c2') in + cstr, type_of_abstraction env name' c1 c2t | Prod (name,c1,c2) -> - let vars = execute_is_type env c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let vars' = execute_is_type env1 c2 in - type_of_product env name vars vars' + let c1', vars = execute_is_type env c1 in + let name' = check_binder_annot vars name in + let env1 = push_rel (LocalAssum (name',c1')) env in + let c2', vars' = execute_is_type env1 c2 in + let cstr = if name == name' && c1 == c1' && c2 == c2' then cstr else mkProd(name',c1',c2') in + cstr, type_of_product env name' vars vars' | LetIn (name,c1,c2,c3) -> - let c1t = execute env c1 in - let _c2s = execute_is_type env c2 in - let () = check_cast env c1 c1t DEFAULTcast c2 in - let env1 = push_rel (LocalDef (name,c1,c2)) env in - let c3t = execute env1 c3 in - subst1 c1 c3t + let c1', c1t = execute env c1 in + let c2', c2s = execute_is_type env c2 in + let name' = check_binder_annot c2s name in + let () = check_cast env c1' c1t DEFAULTcast c2' in + let env1 = push_rel (LocalDef (name',c1',c2')) env in + let c3', c3t = execute env1 c3 in + let cstr = if name == name' && c1 == c1' && c2 == c2' && c3 == c3' then cstr + else mkLetIn(name',c1',c2',c3') + in + cstr, subst1 c1 c3t | Cast (c,k,t) -> - let ct = execute env c in - let _ts = (check_type env t (execute env t)) in - let () = check_cast env c ct k t in - t + let c', ct = execute env c in + let t', _ts = execute_is_type env t in + let () = check_cast env c' ct k t' in + let cstr = if c == c' && t == t' then cstr else mkCast(c',k,t') in + cstr, t' (* Inductive types *) | Ind ind -> - type_of_inductive env ind + cstr, type_of_inductive env ind | Construct c -> - type_of_constructor env c + cstr, type_of_constructor env c | Case (ci,p,c,lf) -> - let ct = execute env c in - let pt = execute env p in - let lft = execute_array env lf in - type_of_case env ci p pt c ct lf lft - - | Fix ((_vn,i as vni),recdef) -> + let c', ct = execute env c in + let p', pt = execute env p in + let lf', lft = execute_array env lf in + let ci', t = type_of_case env ci p' pt c' ct lf' lft in + let cstr = if ci == ci' && c == c' && p == p' && lf == lf' then cstr + else mkCase(ci',p',c',lf') + in + cstr, t + + | Fix ((_vn,i as vni),recdef as fix) -> let (fix_ty,recdef') = execute_recdef env recdef i in - let fix = (vni,recdef') in - check_fix env fix; fix_ty + let cstr, fix = if recdef == recdef' then cstr, fix else + let fix = (vni,recdef') in mkFix fix, fix + in + check_fix env fix; cstr, fix_ty - | CoFix (i,recdef) -> + | CoFix (i,recdef as cofix) -> let (fix_ty,recdef') = execute_recdef env recdef i in - let cofix = (i,recdef') in - check_cofix env cofix; fix_ty + let cstr, cofix = if recdef == recdef' then cstr, cofix else + let cofix = (i,recdef') in mkCoFix cofix, cofix + in + check_cofix env cofix; cstr, fix_ty (* Primitive types *) - | Int _ -> type_of_int env - + | Int _ -> cstr, type_of_int env + (* Partial proofs: unsupported by the kernel *) | Meta _ -> anomaly (Pp.str "the kernel does not support metavariables.") @@ -553,18 +612,22 @@ let rec execute env cstr = anomaly (Pp.str "the kernel does not support existential variables.") and execute_is_type env constr = - let t = execute env constr in - check_type env constr t - -and execute_recdef env (names,lar,vdef) i = - let lart = execute_array env lar in - let lara = Array.map2 (check_assumption env) lar lart in - let env1 = push_rec_types (names,lara,vdef) env in - let vdeft = execute_array env1 vdef in - let () = check_fixpoint env1 names lara vdef vdeft in - (lara.(i),(names,lara,vdef)) - -and execute_array env = Array.map (execute env) + let c, t = execute env constr in + c, check_type env constr t + +and execute_recdef env (names,lar,vdef as recdef) i = + let lar', lart = execute_array env lar in + let names' = Array.Smart.map_i (fun i na -> check_assumption env na lar'.(i) lart.(i)) names in + let env1 = push_rec_types (names',lar',vdef) env in (* vdef is ignored *) + let vdef', vdeft = execute_array env1 vdef in + let () = check_fixpoint env1 names' lar' vdef' vdeft in + let recdef = if names == names' && lar == lar' && vdef == vdef' then recdef else (names',lar',vdef') in + (lar'.(i),recdef) + +and execute_array env cs = + let tys = Array.make (Array.length cs) mkProp in + let cs = Array.Smart.map_i (fun i c -> let c, ty = execute env c in tys.(i) <- ty; c) cs in + cs, tys (* Derived functions *) @@ -576,8 +639,8 @@ let check_wellformed_universes env c = let infer env constr = let () = check_wellformed_universes env constr in - let t = execute env constr in - make_judge constr t + let constr, t = execute env constr in + make_judge constr t let infer = if Flags.profile then @@ -586,7 +649,7 @@ let infer = else (fun b c -> infer b c) let assumption_of_judgment env {uj_val=c; uj_type=t} = - check_assumption env c t + infer_assumption env c t let type_judgment env {uj_val=c; uj_type=t} = let s = check_type env c t in @@ -594,30 +657,27 @@ let type_judgment env {uj_val=c; uj_type=t} = let infer_type env constr = let () = check_wellformed_universes env constr in - let t = execute env constr in + let constr, t = execute env constr in let s = check_type env constr t in {utj_val = constr; utj_type = s} -let infer_v env cv = - let () = Array.iter (check_wellformed_universes env) cv in - let jv = execute_array env cv in - make_judgev cv jv - (* Typing of several terms. *) let check_context env rels = let open Context.Rel.Declaration in - Context.Rel.fold_outside (fun d env -> + Context.Rel.fold_outside (fun d (env,rels) -> match d with - | LocalAssum (_,ty) -> - let _ = infer_type env ty in - push_rel d env - | LocalDef (_,bd,ty) -> + | LocalAssum (x,ty) -> + let jty = infer_type env ty in + let x = check_binder_annot jty.utj_type x in + push_rel d env, LocalAssum (x,jty.utj_val) :: rels + | LocalDef (x,bd,ty) -> let j1 = infer env bd in - let _ = infer_type env ty in + let jty = infer_type env ty in conv_leq false env j1.uj_type ty; - push_rel d env) - rels ~init:env + let x = check_binder_annot jty.utj_type x in + push_rel d env, LocalDef (x,j1.uj_val,jty.utj_val) :: rels) + rels ~init:(env,[]) let judge_of_prop = make_judge mkProp type1 let judge_of_set = make_judge mkSet type1 @@ -639,17 +699,17 @@ let judge_of_apply env funj argjv = let args, argtys = dest_judgev argjv in make_judge (mkApp (funj.uj_val, args)) (type_of_apply env funj.uj_val funj.uj_type args argtys) -let judge_of_abstraction env x varj bodyj = - make_judge (mkLambda (x, varj.utj_val, bodyj.uj_val)) - (type_of_abstraction env x varj.utj_val bodyj.uj_type) +(* let judge_of_abstraction env x varj bodyj = *) +(* make_judge (mkLambda (x, varj.utj_val, bodyj.uj_val)) *) +(* (type_of_abstraction env x varj.utj_val bodyj.uj_type) *) -let judge_of_product env x varj outj = - make_judge (mkProd (x, varj.utj_val, outj.utj_val)) - (mkSort (sort_of_product env varj.utj_type outj.utj_type)) +(* let judge_of_product env x varj outj = *) +(* make_judge (mkProd (x, varj.utj_val, outj.utj_val)) *) +(* (mkSort (sort_of_product env varj.utj_type outj.utj_type)) *) -let judge_of_letin _env name defj typj j = - make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) - (subst1 defj.uj_val j.uj_type) +(* let judge_of_letin env name defj typj j = *) +(* make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) *) +(* (subst1 defj.uj_val j.uj_type) *) let judge_of_cast env cj k tj = let () = check_cast env cj.uj_val cj.uj_type k tj.utj_val in @@ -664,8 +724,8 @@ let judge_of_constructor env cu = let judge_of_case env ci pj cj lfj = let lf, lft = dest_judgev lfj in - make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) - (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) + let ci, t = type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft in + make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) t (* Building type of primitive operators and type *) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 52c261c5e8..cc1885f42d 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -16,27 +16,29 @@ open Environ (** {6 Typing functions (not yet tagged as safe) } They return unsafe judgments that are "in context" of a set of - (local) universe variables (the ones that appear in the term) - and associated constraints. In case of polymorphic definitions, - these variables and constraints will be generalized. - *) + (local) universe variables (the ones that appear in the term) and + associated constraints. In case of polymorphic definitions, these + variables and constraints will be generalized. + When typechecking a term it may be updated to fix relevance marks. + Do not discard the result. *) val infer : env -> constr -> unsafe_judgment -val infer_v : env -> constr array -> unsafe_judgment array val infer_type : env -> types -> unsafe_type_judgment val check_context : - env -> Constr.rel_context -> env + env -> Constr.rel_context -> env * Constr.rel_context (** {6 Basic operations of the typing machine. } *) (** If [j] is the judgement {% $ %}c:t{% $ %}, then [assumption_of_judgement env j] returns the type {% $ %}c{% $ %}, checking that {% $ %}t{% $ %} is a sort. *) -val assumption_of_judgment : env -> unsafe_judgment -> types +val assumption_of_judgment : env -> unsafe_judgment -> Sorts.relevance val type_judgment : env -> unsafe_judgment -> unsafe_type_judgment +val check_binder_annot : Sorts.t -> Name.t Context.binder_annot -> Name.t Context.binder_annot + (** {6 Type of sorts. } *) val type1 : types val type_of_sort : Sorts.t -> types @@ -65,21 +67,21 @@ val judge_of_apply : -> unsafe_judgment (** {6 Type of an abstraction. } *) -val judge_of_abstraction : - env -> Name.t -> unsafe_type_judgment -> unsafe_judgment - -> unsafe_judgment +(* val judge_of_abstraction : *) +(* env -> Name.t -> unsafe_type_judgment -> unsafe_judgment *) +(* -> unsafe_judgment *) (** {6 Type of a product. } *) val sort_of_product : env -> Sorts.t -> Sorts.t -> Sorts.t -val type_of_product : env -> Name.t -> Sorts.t -> Sorts.t -> types -val judge_of_product : - env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment - -> unsafe_judgment +val type_of_product : env -> Name.t Context.binder_annot -> Sorts.t -> Sorts.t -> types +(* val judge_of_product : *) +(* env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment *) +(* -> unsafe_judgment *) (** s Type of a let in. *) -val judge_of_letin : - env -> Name.t -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment - -> unsafe_judgment +(* val judge_of_letin : *) +(* env -> Name.t -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment *) +(* -> unsafe_judgment *) (** {6 Type of a cast. } *) val judge_of_cast : @@ -128,3 +130,6 @@ val judge_of_int : env -> Uint63.t -> unsafe_judgment val type_of_prim_type : env -> CPrimitives.prim_type -> types val type_of_prim : env -> CPrimitives.t -> types + +val warn_bad_relevance_name : string +(** Allow the checker to make this warning into an error. *) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 8187dea41b..0d5b55ca1b 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -29,15 +29,22 @@ module G = AcyclicGraph.Make(struct code (eg add_universe with a constraint vs G.add with no constraint) *) -type t = G.t -type 'a check_function = 'a G.check_function +type t = { graph: G.t; sprop_cumulative : bool } +type 'a check_function = t -> 'a -> 'a -> bool + +let g_map f g = + let g' = f g.graph in + if g.graph == g' then g + else {g with graph=g'} + +let make_sprop_cumulative g = {g with sprop_cumulative=true} let check_smaller_expr g (u,n) (v,m) = let diff = n - m in match diff with - | 0 -> G.check_leq g u v - | 1 -> G.check_lt g u v - | x when x < 0 -> G.check_leq g u v + | 0 -> G.check_leq g.graph u v + | 1 -> G.check_lt g.graph u v + | x when x < 0 -> G.check_leq g.graph u v | _ -> false let exists_bigger g ul l = @@ -48,24 +55,28 @@ let real_check_leq g u v = Universe.for_all (fun ul -> exists_bigger g ul v) u let check_leq g u v = - Universe.equal u v || - is_type0m_univ u || - real_check_leq g u v + Universe.equal u v || (g.sprop_cumulative && Universe.is_sprop u) || + (not (Universe.is_sprop u) && not (Universe.is_sprop v) && + (is_type0m_univ u || + real_check_leq g u v)) let check_eq g u v = Universe.equal u v || - (real_check_leq g u v && real_check_leq g v u) + (not (Universe.is_sprop u || Universe.is_sprop v) && + (real_check_leq g u v && real_check_leq g v u)) -let check_eq_level = G.check_eq +let check_eq_level g u v = + u == v || + (not (Level.is_sprop u || Level.is_sprop v) && G.check_eq g.graph u v) -let empty_universes = G.empty +let empty_universes = {graph=G.empty; sprop_cumulative=false} let initial_universes = let big_rank = 1000000 in let g = G.empty in let g = G.add ~rank:big_rank Level.prop g in let g = G.add ~rank:big_rank Level.set g in - G.enforce_lt Level.prop Level.set g + {graph=G.enforce_lt Level.prop Level.set g; sprop_cumulative=false} let enforce_constraint (u,d,v) g = match d with @@ -73,6 +84,13 @@ let enforce_constraint (u,d,v) g = | Lt -> G.enforce_lt u v g | Eq -> G.enforce_eq u v g +let enforce_constraint (u,d,v as cst) g = + match Level.is_sprop u, d, Level.is_sprop v with + | false, _, false -> g_map (enforce_constraint cst) g + | true, (Eq|Le), true -> g + | true, Le, false when g.sprop_cumulative -> g + | _ -> raise (UniverseInconsistency (d,Universe.make u, Universe.make v, None)) + let merge_constraints csts g = Constraint.fold enforce_constraint csts g let check_constraint g (u,d,v) = @@ -81,6 +99,13 @@ let check_constraint g (u,d,v) = | Lt -> G.check_lt g u v | Eq -> G.check_eq g u v +let check_constraint g (u,d,v as cst) = + match Level.is_sprop u, d, Level.is_sprop v with + | false, _, false -> check_constraint g.graph cst + | true, (Eq|Le), true -> true + | true, Le, false -> g.sprop_cumulative + | _ -> false + let check_constraints csts g = Constraint.for_all (check_constraint g) csts let leq_expr (u,m) (v,n) = @@ -125,17 +150,17 @@ let enforce_leq_alg u v g = exception AlreadyDeclared = G.AlreadyDeclared let add_universe u strict g = - let g = G.add u g in + let graph = G.add u g.graph in let d = if strict then Lt else Le in - enforce_constraint (Level.set,d,u) g + enforce_constraint (Level.set,d,u) {g with graph} -let add_universe_unconstrained u g = G.add u g +let add_universe_unconstrained u g = {g with graph=G.add u g.graph} exception UndeclaredLevel = G.Undeclared -let check_declared_universes = G.check_declared +let check_declared_universes g l = G.check_declared g.graph (LSet.remove Level.sprop l) -let constraints_of_universes = G.constraints_of -let constraints_for = G.constraints_for +let constraints_of_universes g = G.constraints_of g.graph +let constraints_for ~kept g = G.constraints_for ~kept:(LSet.remove Level.sprop kept) g.graph (** Subtyping of polymorphic contexts *) @@ -160,18 +185,20 @@ let check_eq_instances g t1 t2 = (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1)) in aux 0) -let domain = G.domain -let choose = G.choose +let domain g = LSet.add Level.sprop (G.domain g.graph) +let choose p g u = if Level.is_sprop u + then if p u then Some u else None + else G.choose p g.graph u -let dump_universes = G.dump +let dump_universes f g = G.dump f g.graph -let check_universes_invariants g = G.check_invariants ~required_canonical:Level.is_small g +let check_universes_invariants g = G.check_invariants ~required_canonical:Level.is_small g.graph -let pr_universes = G.pr +let pr_universes prl g = G.pr prl g.graph let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] let make_dummy i = Level.(make (UGlobal.make dummy_mp i)) -let sort_universes g = G.sort make_dummy [Level.prop;Level.set] g +let sort_universes g = g_map (G.sort make_dummy [Level.prop;Level.set]) g (** Profiling *) diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index e1a5d50425..17d6c6e6d3 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -13,6 +13,9 @@ open Univ (** {6 Graphs of universes. } *) type t +val make_sprop_cumulative : t -> t +(** Don't use this in the kernel, it makes the system incomplete. *) + type 'a check_function = t -> 'a -> 'a -> bool val check_leq : Universe.t check_function diff --git a/kernel/univ.ml b/kernel/univ.ml index 09bf695915..8263c68bf5 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -53,6 +53,7 @@ struct end type t = + | SProp | Prop | Set | Level of UGlobal.t @@ -63,6 +64,7 @@ struct let equal x y = x == y || match x, y with + | SProp, SProp -> true | Prop, Prop -> true | Set, Set -> true | Level l, Level l' -> UGlobal.equal l l' @@ -71,6 +73,9 @@ struct let compare u v = match u, v with + | SProp, SProp -> 0 + | SProp, _ -> -1 + | _, SProp -> 1 | Prop,Prop -> 0 | Prop, _ -> -1 | _, Prop -> 1 @@ -88,6 +93,7 @@ struct let hequal x y = x == y || match x, y with + | SProp, SProp -> true | Prop, Prop -> true | Set, Set -> true | Level (n,d), Level (n',d') -> @@ -96,6 +102,7 @@ struct | _ -> false let hcons = function + | SProp as x -> x | Prop as x -> x | Set as x -> x | Level (d,n) as x -> @@ -106,8 +113,9 @@ struct open Hashset.Combine let hash = function - | Prop -> combinesmall 1 0 - | Set -> combinesmall 1 1 + | SProp -> combinesmall 1 0 + | Prop -> combinesmall 1 1 + | Set -> combinesmall 1 2 | Var n -> combinesmall 2 n | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d)) @@ -118,6 +126,7 @@ module Level = struct module UGlobal = RawLevel.UGlobal type raw_level = RawLevel.t = + | SProp | Prop | Set | Level of UGlobal.t @@ -155,11 +164,13 @@ module Level = struct let set = make Set let prop = make Prop + let sprop = make SProp let is_small x = match data x with | Level _ -> false | Var _ -> false + | SProp -> true | Prop -> true | Set -> true @@ -173,12 +184,18 @@ module Level = struct | Set -> true | _ -> false + let is_sprop x = + match data x with + | SProp -> true + | _ -> false + let compare u v = if u == v then 0 else RawLevel.compare (data u) (data v) let to_string x = match data x with + | SProp -> "SProp" | Prop -> "Prop" | Set -> "Set" | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n @@ -188,6 +205,7 @@ module Level = struct let apart u v = match data u, data v with + | SProp, _ | _, SProp | Prop, Set | Set, Prop -> true | _ -> false @@ -308,6 +326,7 @@ struct if Int.equal n n' then Level.compare x x' else n - n' + let sprop = hcons (Level.sprop, 0) let prop = hcons (Level.prop, 0) let set = hcons (Level.set, 0) let type1 = hcons (Level.set, 1) @@ -326,16 +345,16 @@ struct let cmp = Level.compare u v in if Int.equal cmp 0 then n <= n' else if n <= n' then - (Level.is_prop u && Level.is_small v) + (Level.is_prop u && not (Level.is_sprop v)) else false let successor (u,n) = - if Level.is_prop u then type1 + if Level.is_small u then type1 else (u, n + 1) let addn k (u,n as x) = if k = 0 then x - else if Level.is_prop u then + else if Level.is_small u then (Level.set,n+k) else (u,n+k) @@ -353,13 +372,16 @@ struct left expression is "smaller" than the right one in both cases. *) let super (u,n) (v,n') = let cmp = Level.compare u v in - if Int.equal cmp 0 then SuperSame (n < n') + if Int.equal cmp 0 then SuperSame (n < n') else let open RawLevel in match Level.data u, n, Level.data v, n' with - | Prop, _, Prop, _ -> SuperSame (n < n') - | Prop, 0, _, _ -> SuperSame true - | _, _, Prop, 0 -> SuperSame false + | SProp, _, SProp, _ | Prop, _, Prop, _ -> SuperSame (n < n') + | SProp, 0, Prop, 0 -> SuperSame true + | Prop, 0, SProp, 0 -> SuperSame false + | (SProp | Prop), 0, _, _ -> SuperSame true + | _, _, (SProp | Prop), 0 -> SuperSame false + | _, _, _, _ -> SuperDiff cmp let to_string (v, n) = @@ -445,6 +467,8 @@ struct | [l] -> Expr.is_small l | _ -> false + let sprop = tip Expr.sprop + (* The lower predicative level of the hierarchy that contains (impredicative) Prop and singleton inductive types *) let type0m = tip Expr.prop @@ -454,8 +478,9 @@ struct (* When typing [Prop] and [Set], there is no constraint on the level, hence the definition of [type1_univ], the type of [Prop] *) - let type1 = tip (Expr.successor Expr.set) + let type1 = tip Expr.type1 + let is_sprop x = equal sprop x let is_type0m x = equal type0m x let is_type0 x = equal type0 x @@ -656,7 +681,7 @@ let enforce_eq u v c = let constraint_add_leq v u c = (* We just discard trivial constraints like u<=u *) if Expr.equal v u then c - else + else match v, u with | (x,n), (y,m) -> let j = m - n in @@ -679,7 +704,12 @@ let check_univ_leq u v = Universe.for_all (fun u -> check_univ_leq_one u v) u let enforce_leq u v c = - List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v + match is_sprop u, is_sprop v with + | true, true -> c + | true, false | false, true -> + raise (UniverseInconsistency (Le, u, v, None)) + | false, false -> + List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v let enforce_leq u v c = if check_univ_leq u v then c @@ -845,7 +875,7 @@ struct else Array.append x y let of_array a = - assert(Array.for_all (fun x -> not (Level.is_prop x)) a); + assert(Array.for_all (fun x -> not (Level.is_prop x || Level.is_sprop x)) a); a let to_array a = a diff --git a/kernel/univ.mli b/kernel/univ.mli index 1fbebee350..5543c35741 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -30,11 +30,13 @@ sig val set : t val prop : t + val sprop : t (** The set and prop universe levels. *) val is_small : t -> bool (** Is the universe set or prop? *) + val is_sprop : t -> bool val is_prop : t -> bool val is_set : t -> bool (** Is it specifically Prop or Set *) @@ -119,6 +121,8 @@ sig val sup : t -> t -> t (** The l.u.b. of 2 universes *) + val sprop : t + val type0m : t (** image of Prop in the universes hierarchy *) @@ -128,6 +132,10 @@ sig val type1 : t (** the universe of the type of Prop/Set *) + val is_sprop : t -> bool + val is_type0m : t -> bool + val is_type0 : t -> bool + val exists : (Level.t * int -> bool) -> t -> bool val for_all : (Level.t * int -> bool) -> t -> bool diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 9a3eadf747..777a207013 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names -open Sorts open Univ open Constr @@ -138,6 +137,7 @@ let hash_annot_switch asw = let pp_sort s = let open Sorts in match s with + | SProp -> Pp.str "SProp" | Prop -> Pp.str "Prop" | Set -> Pp.str "Set" | Type u -> Pp.(str "Type@{" ++ Univ.pr_uni u ++ str "}") @@ -335,10 +335,10 @@ let rec whd_accu a stk = let args = Array.init (nargs args) (arg args) in let s = Obj.obj (Obj.field at 0) in begin match s with - | Type u -> + | Sorts.Type u -> let inst = Instance.of_array (Array.map uni_lvl_val args) in let u = Univ.subst_instance_universe inst u in - Vatom_stk (Asort (Type u), []) + Vatom_stk (Asort (Sorts.sort_of_univ u), []) | _ -> assert false end | _ -> assert false |