diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 67 | ||||
| -rw-r--r-- | kernel/constr.mli | 3 | ||||
| -rw-r--r-- | kernel/indtypes.mli | 13 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 4 | ||||
| -rw-r--r-- | kernel/sorts.ml | 10 | ||||
| -rw-r--r-- | kernel/sorts.mli | 4 |
7 files changed, 103 insertions, 0 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index d7f35da10d..704e6de6b8 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1338,3 +1338,70 @@ type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt type rel_context = rel_declaration list type named_context = named_declaration list type compacted_context = compacted_declaration list + +(* Sorts and sort family *) + +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 + hov 1 + (str"fix " ++ int i ++ spc() ++ str"{" ++ + v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> + Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ + cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ + str"}") + +let pr_puniverses p u = + if Univ.Instance.is_empty u then p + else Pp.(p ++ str"(*" ++ Univ.Instance.pr Univ.Level.pr u ++ str"*)") + +(* Minimalistic constr printer, typically for debugging *) + +let rec debug_print c = + let open Pp in + match kind c with + | Rel n -> str "#"++int n + | Meta n -> str "Meta(" ++ int n ++ str ")" + | Var id -> Id.print id + | Sort s -> Sorts.debug_print s + | Cast (c,_, t) -> hov 1 + (str"(" ++ debug_print c ++ cut() ++ + str":" ++ debug_print t ++ str")") + | Prod (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 + (str"(" ++ debug_print t ++ str " ->" ++ spc() ++ + debug_print c ++ str")") + | Lambda (na,t,c) -> hov 1 + (str"fun " ++ Name.print na ++ 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":" ++ brk(1,2) ++ debug_print t ++ cut() ++ + debug_print c) + | App (c,l) -> hov 1 + (str"(" ++ debug_print c ++ spc() ++ + prlist_with_sep spc debug_print (Array.to_list l) ++ str")") + | Evar (e,l) -> hov 1 + (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++ + prlist_with_sep spc debug_print (Array.to_list l) ++str"}") + | Const (c,u) -> str"Cst(" ++ pr_puniverses (Constant.debug_print c) u ++ str")" + | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")" + | Construct (((sp,i),j),u) -> + str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")" + | Proj (p,c) -> str"Proj(" ++ Constant.debug_print (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ debug_print c ++ str")" + | Case (_ci,p,c,bl) -> v 0 + (hv 0 (str"<"++debug_print p++str">"++ cut() ++ str"Case " ++ + debug_print c ++ str"of") ++ cut() ++ + prlist_with_sep (fun _ -> brk(1,2)) debug_print (Array.to_list bl) ++ + cut() ++ str"end") + | Fix f -> debug_print_fix debug_print f + | CoFix(i,(lna,tl,bl)) -> + let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in + 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 ++ + cut() ++ str":=" ++ debug_print bd) (Array.to_list fixl)) ++ + str"}") diff --git a/kernel/constr.mli b/kernel/constr.mli index 8753c20eac..1be1f63ff7 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -590,3 +590,6 @@ val case_info_hash : case_info -> int (*********************************************************************) val hcons : constr -> constr + +val debug_print : constr -> Pp.t +val debug_print_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index cb09cfa827..a827c17683 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -34,6 +34,19 @@ type inductive_error = exception InductiveError of inductive_error +val infos_and_sort : env -> constr -> Univ.Universe.t + +val check_subtyping_arity_constructor : env -> (constr -> constr) -> types -> int -> bool -> unit + +val check_positivity : chkpos:bool -> + Names.MutInd.t -> + Environ.env -> + (Constr.constr, Constr.types) Context.Rel.pt -> + Declarations.recursivity_kind -> + ('a * Names.Id.t list * Constr.types array * + (('b, 'c) Context.Rel.pt * 'd)) + array -> Int.t * Declarations.recarg Rtree.t array + (** The following function does checks on inductive declarations. *) val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 4b64cc6d11..8b11851bbb 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1061,6 +1061,8 @@ type compiled_library = { comp_natsymbs : Nativecode.symbols } +let module_of_library lib = lib.comp_mod + type native_library = Nativecode.global list let get_library_native_symbols senv dir = diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 8fb33b04d4..7af773e3bc 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -141,6 +141,8 @@ val set_share_reduction : bool -> safe_transformer0 val set_VM : bool -> safe_transformer0 val set_native_compiler : bool -> safe_transformer0 +val check_engagement : Environ.env -> Declarations.set_predicativity -> unit + (** {6 Interactive module functions } *) val start_module : Label.t -> ModPath.t safe_transformer @@ -177,6 +179,8 @@ type compiled_library type native_library = Nativecode.global list +val module_of_library : compiled_library -> Declarations.module_body + val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols val start_library : DirPath.t -> ModPath.t safe_transformer diff --git a/kernel/sorts.ml b/kernel/sorts.ml index a7bb08f5b6..566dce04c6 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -102,3 +102,13 @@ module Hsorts = end) let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ + +let debug_print = function + | Set -> Pp.(str "Set") + | Prop -> Pp.(str "Prop") + | Type u -> Pp.(str "Type(" ++ Univ.Universe.pr u ++ str ")") + +let pr_sort_family = function + | InSet -> Pp.(str "Set") + | InProp -> Pp.(str "Prop") + | InType -> Pp.(str "Type") diff --git a/kernel/sorts.mli b/kernel/sorts.mli index cac6229b91..6c5ce4df80 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -41,3 +41,7 @@ end val univ_of_sort : t -> Univ.Universe.t val sort_of_univ : Univ.Universe.t -> t + +val debug_print : t -> Pp.t + +val pr_sort_family : family -> Pp.t |