diff options
Diffstat (limited to 'kernel')
37 files changed, 593 insertions, 261 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 5fec55fea1..a29f3c6833 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -98,7 +98,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 +195,7 @@ module RedFlags = (struct if Projection.unfolded p then true else red_set red (fCONST (Projection.constant p)) -end : RedFlagsSig) +end open RedFlags @@ -300,9 +300,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 @@ -865,7 +865,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')) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index bd04677374..2852d48a5d 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,7 @@ 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 (** Global and local constant cache *) type clos_infos diff --git a/kernel/clambda.ml b/kernel/clambda.ml index d2147884ba..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 @@ -80,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" ++ @@ -120,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"}") @@ -132,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) -> @@ -394,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) @@ -512,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 @@ -554,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) @@ -629,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 @@ -679,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 @@ -726,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) @@ -801,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 57ece320cf..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.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..14cfba187e 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_relevant : 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..da5217eb33 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_relevant = mbp.mind_relevant; 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 5f6d5f3d0e..97c9f8654a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -548,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/indTyping.ml b/kernel/indTyping.ml index 0d63c8feba..5e294c9729 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -161,7 +161,8 @@ let check_arity env_params env_ar ind = 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,_) = diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 457c17907e..545c0fe7b7 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_relevant 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 @@ -433,7 +435,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 +447,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 +463,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) + (i + 1, j + 1, lab :: labs, r :: rs, projty :: pbs, fterm :: letsubst) | Anonymous -> raise UndefinableExpansion 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 +487,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_relevant = 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 +518,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_relevant; + mind_nb_constant = !nconst; mind_nb_args = !nblock; mind_reloc_tbl = rtbl; } in @@ -546,8 +555,8 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite (** 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) + let labs, rs, projs = compute_projections (kn, i) mib in + (id, labs, rs, projs) in try PrimRecord (Array.mapi map rid) with UndefinableExpansion -> FakeRecord diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 66cd4cba9e..8b8295c64b 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -194,7 +194,11 @@ let instantiate_universes env ctx ar argsorts = (* 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_relevant + +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 -> @@ -301,12 +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 = 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 @@ -320,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 @@ -336,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 (************************************************************************) @@ -379,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))) @@ -574,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_relevant 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 @@ -595,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 @@ -1021,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 @@ -1054,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, _) = @@ -1111,7 +1119,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 -> @@ -1149,7 +1157,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/nativecode.ml b/kernel/nativecode.ml index df60899b95..b1d177e76d 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_relevant; 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/reduction.ml b/kernel/reduction.ml index d526b25e5b..101f02323f 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -446,7 +446,7 @@ 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)."); + anomaly (Pp.str "conversion was given ill-typed terms (FLambda)."); let (_,ty1,bd1) = destFLambda mk_clos hd1 in let (_,ty2,bd2) = destFLambda mk_clos hd2 in let el1 = el_stack lft1 v1 in @@ -470,7 +470,7 @@ 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 (_,_,bd1) = destFLambda mk_clos hd1 in eqappr CONV l2r infos (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv | (_, FLambda _) -> @@ -479,10 +479,10 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | _ -> anomaly (Pp.str "conversion was given unreduced term (FLambda).") in - let (_,_ty2,bd2) = destFLambda mk_clos hd2 in + let (_,_,bd2) = destFLambda mk_clos hd2 in eqappr CONV l2r infos (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 @@ -569,7 +569,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) 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 + 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 @@ -896,7 +896,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..dc1aa20310 --- /dev/null +++ b/kernel/retypeops.ml @@ -0,0 +1,109 @@ +(************************************************************************) +(* 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_relevant + +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 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 + | 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 + | FInt _ -> Sorts.Relevant + | 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 + +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 badd8d320f..edb1d0a02e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -441,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''} @@ -607,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) @@ -620,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 @@ -1243,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/sorts.ml b/kernel/sorts.ml index 1e4e4e00b4..09c98ca1bc 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -128,6 +128,25 @@ 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 | SProp -> Pp.(str "SProp") | Prop -> Pp.(str "Prop") diff --git a/kernel/sorts.mli b/kernel/sorts.mli index 65078c2a62..c49728b146 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -48,6 +48,16 @@ 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 e67c2130d5..f09c45715f 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -14,6 +14,7 @@ open CErrors open Names open Vars open Constr +open Context (* Deprecated *) type sorts_family = Sorts.family = InSProp | InProp | InSet | InType @@ -32,9 +33,11 @@ type sorts = Sorts.t = private (* 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 7fa817bada..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,8 +186,8 @@ 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 diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 929f1c13a3..af96cfdb4f 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -74,13 +74,14 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = in let j = infer env t in let usubst, univs = Declareops.abstract_universes uctx in - let c = Typeops.assumption_of_judgment env j in + let c, r = Typeops.assumption_of_judgment env j in let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) 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; } @@ -110,7 +111,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, @@ -159,6 +161,7 @@ the polymorphic case cook_type = typ; 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; } @@ -214,6 +217,7 @@ the polymorphic case cook_type = typ; cook_universes = univs; cook_private_univs = private_univs; + cook_relevance = Retypeops.relevance_of_term env body; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } @@ -309,6 +313,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 } @@ -366,7 +371,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 814ef8bdfc..9168c32f0e 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -47,8 +47,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,12 +59,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 @@ -103,8 +104,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)) @@ -153,6 +154,9 @@ let error_undeclared_universe env 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) @@ -176,7 +180,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) @@ -194,3 +198,4 @@ let map_ptype_error f = function | 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 e208c57e0a..41a5f19e78 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -48,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 @@ -60,12 +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 @@ -101,8 +102,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 @@ -124,10 +125,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 @@ -137,5 +138,7 @@ 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 1232ab654e..337b66e8e7 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -12,6 +12,7 @@ open CErrors open Util open Names open Univ +open Sorts open Term open Constr open Vars @@ -47,11 +48,19 @@ 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 + t, (match s with Sorts.SProp -> Irrelevant | _ -> Relevant) with TypeError _ -> error_assumption env (make_judge t ty) +let check_assumption env x t ty = + let r = x.Context.binder_relevance in + let t, r' = infer_assumption env t ty in + if not (r == r') then error_bad_relevance env; + t + (************************************************) (* Incremental typing rules: builds a typing judgment given the *) (* judgments for the subterms. *) @@ -220,7 +229,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 @@ -377,7 +386,9 @@ 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 () = check_case_info env pind (Sorts.relevance_of_sort sp) 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 @@ -456,6 +467,10 @@ let constr_of_global_in_context env r = (************************************************************************) (************************************************************************) +let check_binder_annot env s x = + let r = x.Context.binder_relevance in + if not (Sorts.relevance_of_sort s == r) then error_bad_relevance env + (* The typing machine. *) (* ATTENTION : faudra faire le typage du contexte des Const, Ind et Constructsi un jour cela devient des constructions @@ -499,20 +514,23 @@ let rec execute env cstr = type_of_apply env f ft args argst | Lambda (name,c1,c2) -> - let _ = execute_is_type env c1 in + let s = execute_is_type env c1 in + check_binder_annot env s name; let env1 = push_rel (LocalAssum (name,c1)) env in let c2t = execute env1 c2 in type_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> let vars = execute_is_type env c1 in + check_binder_annot env vars name; let env1 = push_rel (LocalAssum (name,c1)) env in let vars' = execute_is_type env1 c2 in 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 c2s = execute_is_type env c2 in + check_binder_annot env c2s name; 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 @@ -563,7 +581,7 @@ and execute_is_type env constr = 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 lara = Array.map3 (check_assumption env) names 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 @@ -591,7 +609,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 @@ -644,17 +662,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 diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 52c261c5e8..e57d6622c9 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -34,9 +34,11 @@ val check_context : (** 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 -> types * Sorts.relevance val type_judgment : env -> unsafe_judgment -> unsafe_type_judgment +val check_binder_annot : env -> Sorts.t -> Name.t Context.binder_annot -> unit + (** {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 : |