diff options
-rw-r--r-- | dev/TODO | 4 | ||||
-rw-r--r-- | kernel/typing.ml | 2 | ||||
-rw-r--r-- | kernel/typing.mli | 1 | ||||
-rw-r--r-- | library/declare.ml | 17 | ||||
-rw-r--r-- | library/global.ml | 1 | ||||
-rw-r--r-- | library/global.mli | 1 |
6 files changed, 21 insertions, 5 deletions
@@ -1,4 +1,7 @@ + o Termes + - introduire un constructeur pour les variables existentielles + o Lib - écrire une fonction d'export qui supprimme les FrozenState, vérifie qu'il n'y a pas de section ouvert, et présente les @@ -17,6 +20,7 @@ - utiliser DOPL plutôt que DOPN (sauf pour Case) - batch mode => pas de undo, ni de reset - conversion : déplier la constante la plus récente + - un cache pour type_of_const, type_of_inductive, type_of_constructor o Lexer à compléter diff --git a/kernel/typing.ml b/kernel/typing.ml index dfce2e442..46fbbf17c 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -415,6 +415,8 @@ let add_mind sp mie env = in add_mind sp mib (add_constraints cst env) +let add_constraints = add_constraints + let export = export let import = import diff --git a/kernel/typing.mli b/kernel/typing.mli index a960b78dd..f93494a95 100644 --- a/kernel/typing.mli +++ b/kernel/typing.mli @@ -36,6 +36,7 @@ val add_parameter : section_path -> constr -> 'a environment -> 'a environment val add_mind : section_path -> mutual_inductive_entry -> 'a environment -> 'a environment +val add_constraints : constraints -> 'a environment -> 'a environment val lookup_var : identifier -> 'a environment -> name * typed_type val lookup_rel : int -> 'a environment -> name * typed_type diff --git a/library/declare.ml b/library/declare.ml index 1af5ad6a8..79588e750 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -3,6 +3,7 @@ open Util open Names +open Constant open Inductive open Libobject open Lib @@ -42,7 +43,9 @@ let cache_parameter (sp,c) = Global.add_parameter sp c; Nametab.push (basename sp) sp -let load_parameter _ = () +let load_parameter (sp,_) = + let cb = Global.lookup_constant sp in + Global.add_constraints cb.const_constraints let open_parameter (sp,_) = Nametab.push (basename sp) sp @@ -69,7 +72,9 @@ let cache_constant (sp,ce) = Nametab.push (basename sp) sp; declare_constant_implicits sp -let load_constant _ = () +let load_constant (sp,_) = + let cb = Global.lookup_constant sp in + Global.add_constraints cb.const_constraints let open_constant (sp,_) = Nametab.push (basename sp) sp; @@ -83,7 +88,7 @@ let (in_constant, out_constant) = load_function = load_constant; open_function = open_constant; specification_function = specification_constant } in - declare_object ("Parameter", od) + declare_object ("Constant", od) let declare_constant id ce = let sp = add_leaf id CCI (in_constant ce) in @@ -105,7 +110,9 @@ let cache_inductive (sp,mie) = push_inductive_names sp mie; declare_inductive_implicits sp -let load_inductive _ = () +let load_inductive (sp,_) = + let mib = Global.lookup_mind sp in + Global.add_constraints mib.mind_constraints let open_inductive (sp,mie) = push_inductive_names sp mie; @@ -119,7 +126,7 @@ let (in_inductive, out_inductive) = load_function = load_inductive; open_function = open_inductive; specification_function = specification_inductive } in - declare_object ("Parameter", od) + declare_object ("Inductive", od) let declare_mind mie = let id = match mie.mind_entry_inds with diff --git a/library/global.ml b/library/global.ml index 7ffbd2110..f7fac0313 100644 --- a/library/global.ml +++ b/library/global.ml @@ -29,6 +29,7 @@ let push_rel nac = global_env := push_rel nac !global_env let add_constant sp ce = global_env := add_constant sp ce !global_env let add_parameter sp c = global_env := add_parameter sp c !global_env let add_mind sp mie = global_env := add_mind sp mie !global_env +let add_constraints c = global_env := add_constraints c !global_env let lookup_var id = lookup_var id !global_env let lookup_rel n = lookup_rel n !global_env diff --git a/library/global.mli b/library/global.mli index 9436e446b..e959c6091 100644 --- a/library/global.mli +++ b/library/global.mli @@ -29,6 +29,7 @@ val push_rel : name * constr -> unit val add_constant : section_path -> constant_entry -> unit val add_parameter : section_path -> constr -> unit val add_mind : section_path -> mutual_inductive_entry -> unit +val add_constraints : constraints -> unit val lookup_var : identifier -> name * typed_type val lookup_rel : int -> name * typed_type |