From 6965121294e2a083c0111d6ff3da2158ed6f4a7a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 15 Jan 2015 14:11:46 +0100 Subject: Update header of CHANGES. --- CHANGES | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGES b/CHANGES index 2088fa6ff7..e41743d986 100644 --- a/CHANGES +++ b/CHANGES @@ -1,5 +1,5 @@ -Changes from V8.4 -================= +Changes from V8.4 to V8.5beta1 +============================== Logic -- cgit v1.2.3 From 004b7f53cd9a9f8bd78156310f516af8fe42554b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 14 Jan 2015 18:05:40 +0530 Subject: Optionally allow eta-conversion during unification for type classes. Off by default as it can be backwards-incompatible (e.g. produces loop in the library without an additional Typeclasses Opaque directive in RelationPairs). --- tactics/class_tactics.ml | 17 ++++++++++++++++- theories/Classes/RelationPairs.v | 1 + 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 44204a9f0e..9d49a7bbb7 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -32,6 +32,21 @@ open Hints let typeclasses_debug = ref false let typeclasses_depth = ref None +let typeclasses_modulo_eta = ref false +let set_typeclasses_modulo_eta d = (:=) typeclasses_modulo_eta d +let get_typeclasses_modulo_eta () = !typeclasses_modulo_eta + +open Goptions + +let set_typeclasses_modulo_eta = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "do typeclass search modulo eta conversion"; + optkey = ["Typeclasses";"Modulo";"Eta"]; + optread = get_typeclasses_modulo_eta; + optwrite = set_typeclasses_modulo_eta; } + (** We transform the evars that are concerned by this resolution (according to predicate p) into goals. Invariant: function p only manipulates and returns undefined evars *) @@ -65,7 +80,7 @@ let auto_core_unif_flags st freeze = { frozen_evars = freeze; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = true; - modulo_eta = false; + modulo_eta = !typeclasses_modulo_eta; } let auto_unif_flags freeze st = diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index cbde5f9ab5..8ce3e4b6b7 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -42,6 +42,7 @@ Generalizable Variables A B RA RB Ri Ro f. Definition RelCompFun {A} {B : Type}(R:relation B)(f:A->B) : relation A := fun a a' => R (f a) (f a'). +Typeclasses Opaque RelCompFun. Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope. -- cgit v1.2.3 From 4ddddba01d49ba7c019ebb0444cd58c18c8ad40d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 14 Jan 2015 20:56:29 +0530 Subject: Remove typeclass opaque directive, some proofs in the stdlib rely on it being transparent --- theories/Classes/RelationPairs.v | 1 - 1 file changed, 1 deletion(-) diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index 8ce3e4b6b7..cbde5f9ab5 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -42,7 +42,6 @@ Generalizable Variables A B RA RB Ri Ro f. Definition RelCompFun {A} {B : Type}(R:relation B)(f:A->B) : relation A := fun a a' => R (f a) (f a'). -Typeclasses Opaque RelCompFun. Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope. -- cgit v1.2.3 From acf1f8c1fd02589f137603178ab713f14c949e77 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 14 Jan 2015 20:57:08 +0530 Subject: Expand Credits for 8.5 and doc on universes --- doc/refman/Classes.tex | 2 +- doc/refman/RefMan-pre.tex | 30 +++++++++++++++++++++--------- doc/refman/Universes.tex | 42 ++++++++++++++++++++++++++++++++++++------ 3 files changed, 58 insertions(+), 16 deletions(-) diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index f683e4543b..35d64053c1 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -10,7 +10,7 @@ \label{typeclasses} \begin{flushleft} - \em The status of Type Classes is (extremely) experimental. + \em The status of Type Classes is experimental. \end{flushleft} This chapter presents a quick reference of the commands related to type diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index ef7a61931c..46ee361e09 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -980,16 +980,28 @@ help from Makarius Wenzel) or PIDE/Coqoon (with help from Alexander Faithfull and Jesper Bengtson). The development of such features was funded by the Paral-ITP French ANR project. -The universe polymorphism extension is based on a change of the kernel -architecture to handle constraint checking only, leaving the generation -of constraints outside it. +The full universe polymorphism extension was designed by Matthieu +Sozeau. It conservatively extends the universes system and core calculus +with definitions and inductive declarations parameterized by universes +and constraints. It is based on a change of the kernel architecture to +handle constraint checking only, leaving the generation of constraints +to the refinement/type inference engine. Accordingly, tactics are now +fully universe aware, resulting in more localized error messages in case +of inconsistencies and allowing higher-level algorithms like unification +to be entirely type safe. The internal representation of universes has +been modified but this invisible to the user. The underlying logic has been extended with $\eta$-conversion for -primitive records thanks to Matthieu Sozeau. This additional form of -$\eta$-conversion is justified using the same principle than the -previously added $\eta$-conversion for function types, based on -formulations of the Calculus of Inductive Constructions with typed -equality. +records defined with primitive projections by Matthieu Sozeau. This +additional form of $\eta$-conversion is justified using the same +principle than the previously added $\eta$-conversion for function +types, based on formulations of the Calculus of Inductive Constructions +with typed equality. Primitive projections, which do not carry the +parameters of the record and are rigid names (not defined as a +pattern-matching construct), make working with nested records more +manageable in terms of time and space consumption. This extension and +universe polymorphism were carried partly while the author was working +at the IAS in Princeton. The guard condition has been made compliant with extensional equality principles such as propositional equality and univalence, thanks to @@ -1021,7 +1033,7 @@ Pierre Courtieu contributed new features for using {\Coq} through Proof General and for better interactive experience (bullets, Search etc). \begin{flushright} -Paris, Janvier 2015\\ +Paris, January 2015\\ Hugo Herbelin \& Matthieu Sozeau\\ \end{flushright} diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 530086961f..4b71a25867 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -6,6 +6,12 @@ \asection{General Presentation} +\begin{flushleft} + \em The status of Universe Polymorphism is experimental. Some features + are not compatible with it (yet): native compilation and bytecode + compilation do not handle polymorphic definitions. +\end{flushleft} + This section describes the universe polymorphic extension of Coq. Universe polymorphism allows writing generic definitions making use of universes and reuse them at different and sometimes incompatible levels. @@ -119,7 +125,7 @@ producing global universe constraints, one can use the them. In other words, two definitions in the section sharing a common variable will both get parameterized by the universes produced by the variable declaration. This is in contrast to a ``mononorphic'' variable - which introduce global universes, making the two definitions depend on + which introduces global universes, making the two definitions depend on the \emph{same} universes associated to the variable. \item \texttt{Hint \{Resolve, Rewrite\}} will use the auto/rewrite hint polymorphically, not at a single instance. @@ -133,17 +139,41 @@ references. The semantics respect the fact that definitions are transparent, so indistinguishable from their bodies during conversion. This is accomplished by changing one rule of unification, the -first-order approximation rule: - +first-order approximation rule, which applies when two applicative terms +with the same head are compared. It tries to short-cut unfolding by +comparing the arguments directly. In case the constant is universe +polymorphic, we allow this rule to fire only when unifying the universes +results in instantiating a so-called flexible universe variables (not +given by the user). Similarly for conversion, if such an equation of +applicative terms fail due to a universe comparison not being satisfied, +the terms are unfolded. This change implies that conversion and +unification can have different unfolding behaviors on the same +development with universe polymorphism switched on or off. -TODO +\asection{Explicit Universes} +\begin{flushleft} + \em The design and implementation of explicit universes is very + experimental and is likely to change in future versions. +\end{flushleft} +The syntax has been extended to allow users to explicitely bind names to +universes and explicitely instantantiate polymorphic +definitions. Currently, binding is implicit at the first occurrence of a +universe name. For example below, i and j are introduced by the +annotations attached to Types. -\asection{Explicit Universes} +\begin{coq_example*} +Polymorphic Definition le (A : Type@{i}) : Type@{j} := A. +\end{coq_example*} -TODO +Definitions can also be instantiated explicitely: +\begin{coq_example} +Check (pidentity@{Set}). +Check (le@{Type Set}). +\end{coq_example} +User-named universes are considered rigid for unification. %%% Local Variables: %%% mode: latex -- cgit v1.2.3 From 4f2f4741be7b4eaf30495070ff62eaa7244f4db3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 15 Jan 2015 18:03:46 +0530 Subject: Add a (by default deactivated) option to force typeclass resolution to respect dependencies between typeclass goals, trying to solve the least dependent ones first. --- tactics/class_tactics.ml | 63 +++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 52 insertions(+), 11 deletions(-) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 9d49a7bbb7..7964c0a8fe 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -36,6 +36,10 @@ let typeclasses_modulo_eta = ref false let set_typeclasses_modulo_eta d = (:=) typeclasses_modulo_eta d let get_typeclasses_modulo_eta () = !typeclasses_modulo_eta +let typeclasses_dependency_order = ref false +let set_typeclasses_dependency_order d = (:=) typeclasses_dependency_order d +let get_typeclasses_dependency_order () = !typeclasses_dependency_order + open Goptions let set_typeclasses_modulo_eta = @@ -47,20 +51,46 @@ let set_typeclasses_modulo_eta = optread = get_typeclasses_modulo_eta; optwrite = set_typeclasses_modulo_eta; } +let set_typeclasses_dependency_order = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "during typeclass resolution, solve instances according to their dependency order"; + optkey = ["Typeclasses";"Dependency";"Order"]; + optread = get_typeclasses_dependency_order; + optwrite = set_typeclasses_dependency_order; } + (** We transform the evars that are concerned by this resolution (according to predicate p) into goals. Invariant: function p only manipulates and returns undefined evars *) +let top_sort evm undefs = + let l' = ref [] in + let tosee = ref undefs in + let rec visit ev evi = + let evs = Evarutil.undefined_evars_of_evar_info evm evi in + Evar.Set.iter (fun ev -> + if Evar.Map.mem ev !tosee then + visit ev (Evar.Map.find ev !tosee)) evs; + tosee := Evar.Map.remove ev !tosee; + l' := ev :: !l'; + in + while not (Evar.Map.is_empty !tosee) do + let ev, evi = Evar.Map.min_binding !tosee in + visit ev evi + done; + List.rev !l' + let evars_to_goals p evm = let goals = ref Evar.Map.empty in let map ev evi = let evi, goal = p evm ev evi in - let () = if goal then goals := Evar.Map.add ev ev !goals in + let () = if goal then goals := Evar.Map.add ev evi !goals in evi in let evm = Evd.raw_map_undefined map evm in if Evar.Map.is_empty !goals then None - else Some (Evar.Map.bindings !goals, evm) + else Some (!goals, evm) (** Typeclasses instance search tactic / eauto *) @@ -408,8 +438,14 @@ let hints_tac hints = match sgls with | None -> gls', s' | Some (evgls, s') -> - (* Reorder with dependent subgoals. *) - (gls' @ List.map (fun (ev, x) -> Some ev, x) evgls, s') + if not !typeclasses_dependency_order then + (gls' @ List.map (fun (ev,_) -> (Some ev, ev)) (Evar.Map.bindings evgls), s') + else + (* Reorder with dependent subgoals. *) + let evm = List.fold_left + (fun acc g -> Evar.Map.add g (Evd.find_undefined s' g) acc) evgls gls in + let gls = top_sort s' evm in + (List.map (fun ev -> Some ev, ev) gls, s') in let gls' = List.map_i (fun j (evar, g) -> @@ -515,7 +551,7 @@ let make_autogoals ?(only_classes=true) ?(unique=false) let cut = cut_of_hints hints in { it = List.map_i (fun i g -> let (gl, auto) = make_autogoal ~only_classes ~unique - ~st cut (Some (fst g)) {it = snd g; sigma = evm'; } in + ~st cut (Some g) {it = g; sigma = evm'; } in (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm'; } let get_result r = @@ -527,12 +563,17 @@ let run_on_evars ?(only_classes=true) ?(unique=false) ?(st=full_transparent_stat match evars_to_goals p evm with | None -> None (* This happens only because there's no evar having p *) | Some (goals, evm') -> - let res = run_list_tac tac p goals - (make_autogoals ~only_classes ~unique ~st hints goals evm') in - match get_result res with - | None -> raise Not_found - | Some (evm', fk) -> - Some (evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm, fk) + let goals = + if !typeclasses_dependency_order then + top_sort evm' goals + else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals) + in + let res = run_list_tac tac p goals + (make_autogoals ~only_classes ~unique ~st hints goals evm') in + match get_result res with + | None -> raise Not_found + | Some (evm', fk) -> + Some (evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm, fk) let eauto_tac hints = then_tac normevars_tac (or_tac (hints_tac hints) intro_tac) -- cgit v1.2.3 From 2d2b145ca9914df4b1eaab5acb3a11504b4308d5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 15 Jan 2015 18:31:06 +0530 Subject: Move explanations about primitive projections to the manual. --- CHANGES | 19 +------------------ doc/refman/RefMan-ext.tex | 31 +++++++++++++++++++++++++++++++ 2 files changed, 32 insertions(+), 18 deletions(-) diff --git a/CHANGES b/CHANGES index e41743d986..f0dd06e04f 100644 --- a/CHANGES +++ b/CHANGES @@ -15,24 +15,7 @@ Logic Records with primitive projections have eta-conversion, the canonical form being [mkR pars (p1 t) ... (pn t)]. - With native projections, the parsing of projection applications changes: - - - r.(p) and (p r) elaborate to native projection application, and - the parameters cannot be mentioned. The following arguments are - parsed according to the remaining implicit arguments declared for the - projection (i.e. the implicit arguments after the record type - argument). In dot notation, the record type argument is considered - explicit no matter what its implicit status is. - - r.(@p params) and @p args are parsed as regular applications of the - projection with explicit parameters. - - [simpl p] is forbidden, but [simpl @p] will simplify both the projection - and its explicit [@p] version. - - [unfold p] has no effect on projection applications unless it is applied - to a constructor. If the explicit version appears it reduces to the - projection application. - - [pattern x at n], [rewrite x at n] and in general abstraction and selection - of occurrences may fail due to the disappearance of parameters. -- New universe polymorphism. +- New universe polymorphism (see reference manual) - New option -type-in-type to collapse the universe hierarchy (this makes the logic inconsistent). - The guard condition for fixpoints is now a bit stricter. Propagation of diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 6eca9fc4c2..2a976a07b3 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -282,6 +282,37 @@ the inductive type. To deactivate the printing of projections, use {\tt Unset Printing Projections}. +\subsection{Primitive Projections} +\index{Primitive projections} +\label{prim-proj} + +The option {\tt Set Primitive Projections} turns on the use of primitive +projections when defining subsequent records. Primitive projections +extended the calculus of inductive constructions with a new binary term +constructor {\tt r.(p)} representing a primitive projection p applied to +a record object {\tt r} (i.e., primitive projections are always +applied). Even if the record type has parameters, these do not appear at +applications of the projection, considerably reducing the sizes of terms +when manipulating parameterized records and typechecking time. On the +user level, primitive projections are a transparent replacement +for the usual defined ones. + + % - r.(p) and (p r) elaborate to native projection application, and + % the parameters cannot be mentioned. The following arguments are + % parsed according to the remaining implicit arguments declared for the + % projection (i.e. the implicit arguments after the record type + % argument). In dot notation, the record type argument is considered + % explicit no matter what its implicit status is. + % - r.(@p params) and @p args are parsed as regular applications of the + % projection with explicit parameters. + % - [simpl p] is forbidden, but [simpl @p] will simplify both the projection + % and its explicit [@p] version. + % - [unfold p] has no effect on projection applications unless it is applied + % to a constructor. If the explicit version appears it reduces to the + % projection application. + % - [pattern x at n], [rewrite x at n] and in general abstraction and selection + % of occurrences may fail due to the disappearance of parameters. + \section{Variants and extensions of {\mbox{\tt match}} \label{Extensions-of-match} -- cgit v1.2.3 From 58153a5bc59bbde6534425d66a2fe5d9943eb44b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 15 Jan 2015 18:44:59 +0530 Subject: Minor fixes to the refman credits to be continued. --- doc/refman/RefMan-pre.tex | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 46ee361e09..e75ade9419 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -952,8 +952,7 @@ projects: The full integration of the proof engine brings to primitive tactics and the user level Ltac language deep tactic backtracking and multi-goal -handling. This allows -... +handling. The way Coq processes a document in batch and interactive mode has been redesigned by Enrico Tassi with help from Bruno Barras. Opaque @@ -1014,13 +1013,12 @@ the relations between homotopy theory and type theory. {\Coq} 8.5 also comes with a bunch of many various smaller-scale changes and improvements regarding the different components of the system. -High-Level Specification Language: -- tactics in terms -- Universe inconsistency and unification error messages -- Named existentials - -Opam Coq Guillaume Claret and Thomas Braibant +% High-Level Specification Language: +% - tactics in terms +% - Universe inconsistency and unification error messages +% - Named existentials +% Opam Coq Guillaume Claret and Thomas Braibant Maxime Dénès and Benjamin Grégoire developed an implementation of the conversion test using the OCaml native compiler. -- cgit v1.2.3 From 8309a98096facfba448c9d8d298ba3903145831a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 15 Jan 2015 18:45:27 +0530 Subject: Correct restriction of vm_compute when handling universe polymorphic definitions. Instead of failing with an anomaly when trying to do conversion or computation with the vm's, consider polymorphic constants as being opaque and keep instances around. This way the code is still correct but (obviously) incomplete for polymorphic definitions and we avoid introducing an anomaly. The patch does nothing clever, it only keeps around instances with constants/inductives and compile constant bodies only for non-polymorphic definitions. --- kernel/cbytecodes.ml | 6 +++--- kernel/cbytecodes.mli | 4 ++-- kernel/cbytegen.ml | 18 +++++++++--------- kernel/cbytegen.mli | 4 ++-- kernel/cemitcodes.ml | 14 +++++++------- kernel/cemitcodes.mli | 4 ++-- kernel/conv_oracle.ml | 10 ++++++---- kernel/conv_oracle.mli | 3 ++- kernel/csymtable.ml | 14 ++++++++------ kernel/environ.ml | 4 ++-- kernel/modops.ml | 2 +- kernel/names.ml | 4 ---- kernel/names.mli | 3 --- kernel/nativecode.ml | 6 +++--- kernel/nativelambda.ml | 8 ++++---- kernel/nativelambda.mli | 2 +- kernel/reduction.ml | 2 +- kernel/univ.ml | 2 ++ kernel/univ.mli | 2 ++ kernel/vars.ml | 3 +++ kernel/vars.mli | 3 +++ kernel/vconv.ml | 11 ++++++----- kernel/vm.ml | 13 +++++++------ kernel/vm.mli | 8 ++++---- pretyping/unification.ml | 4 ++-- pretyping/vnorm.ml | 11 +++++------ theories/Init/Datatypes.v | 4 ++-- theories/Init/Specif.v | 8 ++++---- theories/Program/Basics.v | 4 +--- 29 files changed, 94 insertions(+), 87 deletions(-) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 473a14c248..ae679027d6 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -27,7 +27,7 @@ let cofix_evaluated_tag = 6 type structured_constant = | Const_sorts of sorts - | Const_ind of inductive + | Const_ind of pinductive | Const_b0 of tag | Const_bn of tag * structured_constant array @@ -67,7 +67,7 @@ type instruction = (* nb fv, init, lbl types, lbl bodies *) | Kclosurecofix of int * int * Label.t array * Label.t array (* nb fv, init, lbl types, lbl bodies *) - | Kgetglobal of constant + | Kgetglobal of pconstant | Kconst of structured_constant | Kmakeblock of int * tag (* size, tag *) | Kmakeprod @@ -185,7 +185,7 @@ let rec instruction ppf = function Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt; print_string " bodies = "; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; - | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id) + | Kgetglobal (id,u) -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id) | Kconst cst -> fprintf ppf "\tconst" | Kmakeblock(n, m) -> diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 225198fcc9..b65268f722 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -23,7 +23,7 @@ val cofix_evaluated_tag : tag type structured_constant = | Const_sorts of sorts - | Const_ind of inductive + | Const_ind of pinductive | Const_b0 of tag | Const_bn of tag * structured_constant array @@ -60,7 +60,7 @@ type instruction = (** nb fv, init, lbl types, lbl bodies *) | Kclosurecofix of int * int * Label.t array * Label.t array (** nb fv, init, lbl types, lbl bodies *) - | Kgetglobal of constant + | Kgetglobal of pconstant | Kconst of structured_constant | Kmakeblock of int * tag (** size, tag *) | Kmakeprod diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 39d8007370..65ee655dab 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -422,7 +422,7 @@ let rec str_const c = end | _ -> Bconstr c end - | Ind (ind,u) -> Bstrconst (Const_ind ind) + | Ind ind -> Bstrconst (Const_ind ind) | Construct (((kn,j),i),u) -> begin (* spiwack: tries first to apply the run-time compilation @@ -486,12 +486,12 @@ let rec compile_fv reloc l sz cont = (* Compiling constants *) -let rec get_allias env kn = +let rec get_allias env (kn,u as p) = let cb = lookup_constant kn env in let tps = cb.const_body_code in (match Cemitcodes.force tps with | BCallias kn' -> get_allias env kn' - | _ -> kn) + | _ -> p) (* Compiling expressions *) @@ -700,10 +700,10 @@ and compile_const = (mkConstU (kn,u)) reloc args sz cont with Not_found -> if Int.equal nargs 0 then - Kgetglobal (get_allias !global_env kn) :: cont + Kgetglobal (get_allias !global_env (kn, u)) :: cont else comp_app (fun _ _ _ cont -> - Kgetglobal (get_allias !global_env kn) :: cont) + Kgetglobal (get_allias !global_env (kn,u)) :: cont) compile_constr reloc () args sz cont let compile env c = @@ -729,10 +729,10 @@ let compile_constant_body env = function | Def sb -> let body = Mod_subst.force_constr sb in match kind_of_term body with - | Const kn' -> + | Const (kn',u) -> (* we use the canonical name of the constant*) - let con= constant_of_kn (canonical_con (Univ.out_punivs kn')) in - BCallias (get_allias env con) + let con= constant_of_kn (canonical_con kn') in + BCallias (get_allias env (con,u)) | _ -> let res = compile env body in let to_patch = to_memory res in @@ -740,7 +740,7 @@ let compile_constant_body env = function (* Shortcut of the previous function used during module strengthening *) -let compile_alias kn = BCallias (constant_of_kn (canonical_con kn)) +let compile_alias (kn,u) = BCallias (constant_of_kn (canonical_con kn), u) (* spiwack: additional function which allow different part of compilation of the 31-bit integers *) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index d0bfd46c00..eab36d8b24 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -13,7 +13,7 @@ val compile_constant_body : env -> constant_def -> body_code (** Shortcut of the previous function used during module strengthening *) -val compile_alias : constant -> body_code +val compile_alias : pconstant -> body_code (** spiwack: this function contains the information needed to perform the static compilation of int31 (trying and obtaining @@ -33,7 +33,7 @@ val dynamic_int31_compilation : bool -> comp_env -> works as follow: checks if all the arguments are non-pointers if they are applies the operation (second argument) if not all of them are, returns to a coq definition (third argument) *) -val op_compilation : int -> instruction -> constant -> bool -> comp_env -> +val op_compilation : int -> instruction -> pconstant -> bool -> comp_env -> constr array -> int -> bytecodes-> bytecodes (*spiwack: compiling function to insert dynamic decompilation before diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 2091440447..3c9692a5c6 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -20,7 +20,7 @@ open Mod_subst type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of constant + | Reloc_getglobal of pconstant type patch = reloc_info * int @@ -147,8 +147,8 @@ and slot_for_annot a = enter (Reloc_annot a); out_int 0 -and slot_for_getglobal id = - enter (Reloc_getglobal id); +and slot_for_getglobal p = + enter (Reloc_getglobal p); out_int 0 @@ -320,7 +320,7 @@ let rec subst_strcst s sc = match sc with | Const_sorts _ | Const_b0 _ -> sc | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) - | Const_ind(ind) -> let kn,i = ind in Const_ind((subst_mind s kn, i)) + | Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u) let subst_patch s (ri,pos) = match ri with @@ -329,19 +329,19 @@ let subst_patch s (ri,pos) = let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in (Reloc_annot {a with ci = ci},pos) | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos) - | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con_kn s kn)), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (subst_pcon s kn), pos) let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv type body_code = | BCdefined of to_patch - | BCallias of constant + | BCallias of pconstant | BCconstant let subst_body_code s = function | BCdefined tp -> BCdefined (subst_to_patch s tp) - | BCallias kn -> BCallias (fst (subst_con_kn s kn)) + | BCallias (kn,u) -> BCallias (fst (subst_con_kn s kn), u) | BCconstant -> BCconstant type to_patch_substituted = body_code substituted diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 287c393046..cec9013060 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -4,7 +4,7 @@ open Cbytecodes type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of constant + | Reloc_getglobal of constant Univ.puniverses type patch = reloc_info * int @@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch type body_code = | BCdefined of to_patch - | BCallias of constant + | BCallias of constant Univ.puniverses | BCconstant diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 1c2eea17b7..3b01538b92 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -40,12 +40,12 @@ let empty = { cst_trstate = Cpred.full; } -let get_strategy { var_opacity; cst_opacity } = function +let get_strategy { var_opacity; cst_opacity } f = function | VarKey id -> (try Id.Map.find id var_opacity with Not_found -> default) | ConstKey c -> - (try Cmap.find c cst_opacity + (try Cmap.find (f c) cst_opacity with Not_found -> default) | RelKey _ -> Expand @@ -83,9 +83,11 @@ let get_transp_state { var_trstate; cst_trstate } = (var_trstate, cst_trstate) (* Unfold the first constant only if it is "more transparent" than the second one. In case of tie, expand the second one. *) -let oracle_order o l2r k1 k2 = - match get_strategy o k1, get_strategy o k2 with +let oracle_order f o l2r k1 k2 = + match get_strategy o f k1, get_strategy o f k2 with | Expand, _ -> true | Level n1, Opaque -> true | Level n1, Level n2 -> n1 < n2 | _ -> l2r (* use recommended default *) + +let get_strategy o = get_strategy o (fun x -> x) diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 550076782c..629912220f 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -16,7 +16,8 @@ val empty : oracle If [oracle_order kn1 kn2] is true, then unfold kn1 first. Note: the oracle does not introduce incompleteness, it only tries to postpone unfolding of "opaque" constants. *) -val oracle_order : oracle -> bool -> constant tableKey -> constant tableKey -> bool +val oracle_order : ('a -> constant) -> oracle -> bool -> + 'a tableKey -> 'a tableKey -> bool (** Priority for the expansion of constant in the conversion test. * Higher levels means that the expansion is less prioritary. diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 794d945811..ed8b0a6d1d 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -57,7 +57,7 @@ let set_global v = let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2 -| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 +| Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2 | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 | Const_bn (t1, a1), Const_bn (t2, a2) -> Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2 @@ -67,7 +67,7 @@ let rec hash_structured_constant c = let open Hashset.Combine in match c with | Const_sorts s -> combinesmall 1 (Sorts.hash s) - | Const_ind i -> combinesmall 2 (ind_hash i) + | Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u)) | Const_b0 t -> combinesmall 3 (Int.hash t) | Const_bn (t, a) -> let fold h c = combine h (hash_structured_constant c) in @@ -142,7 +142,7 @@ let slot_for_annot key = AnnotTable.add annot_tbl key n; n -let rec slot_for_getglobal env kn = +let rec slot_for_getglobal env (kn,u) = let (cb,(_,rk)) = lookup_constant_key kn env in try key rk with NotEvaluated -> @@ -150,10 +150,12 @@ let rec slot_for_getglobal env kn = let pos = match Cemitcodes.force cb.const_body_code with | BCdefined(code,pl,fv) -> - let v = eval_to_patch env (code,pl,fv) in - set_global v + if Univ.Instance.is_empty u then + let v = eval_to_patch env (code,pl,fv) in + set_global v + else set_global (val_of_constant (kn,u)) | BCallias kn' -> slot_for_getglobal env kn' - | BCconstant -> set_global (val_of_constant kn) in + | BCconstant -> set_global (val_of_constant (kn,u)) in (*Pp.msgnl(str"value stored at: "++int pos);*) rk := Some (Ephemeron.create pos); pos diff --git a/kernel/environ.ml b/kernel/environ.ml index 8b1e499191..0ebff440a1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -594,7 +594,7 @@ let dispatch = let int31_op n op prim kn = { empty_reactive_info with vm_compiling = Some (Cbytegen.op_compilation n op kn); - native_compiling = Some (Nativelambda.compile_prim prim kn); + native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); } in @@ -602,7 +602,7 @@ fun rk value field -> (* subfunction which shortens the (very common) dispatch of operations *) let int31_op_from_const n op prim = match kind_of_term value with - | Const (kn,_) -> int31_op n op prim kn + | Const kn -> int31_op n op prim kn | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant") in let int31_binop_from_const op prim = int31_op_from_const 2 op prim in diff --git a/kernel/modops.ml b/kernel/modops.ml index e04eb354e0..392e667b8e 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -337,7 +337,7 @@ let strengthen_const mp_from l cb resolver = in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); - const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) } + const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias (con,u)) } let rec strengthen_mod mp_from mp_to mb = if mp_in_delta mb.mod_mp mb.mod_delta then mb diff --git a/kernel/names.ml b/kernel/names.ml index 2c28866236..b349ccb009 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -686,8 +686,6 @@ type inv_rel_key = int (* index in the [rel_context] part of environment starting by the end, {\em inverse} of de Bruijn indice *) -type id_key = Constant.t tableKey - let eq_table_key f ik1 ik2 = if ik1 == ik2 then true else match ik1,ik2 with @@ -696,8 +694,6 @@ let eq_table_key f ik1 ik2 = | RelKey k1, RelKey k2 -> Int.equal k1 k2 | _ -> false -let eq_id_key = eq_table_key Constant.UserOrd.equal - let eq_con_chk = Constant.UserOrd.equal let eq_mind_chk = MutInd.UserOrd.equal let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2 diff --git a/kernel/names.mli b/kernel/names.mli index 9fbe7d5e58..d82043da1a 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -458,11 +458,8 @@ type inv_rel_key = int (** index in the [rel_context] part of environment starting by the end, {e inverse} of de Bruijn indice *) -type id_key = Constant.t tableKey - val eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> bool val eq_constant_key : Constant.t -> Constant.t -> bool -val eq_id_key : id_key -> id_key -> bool (** equalities on constant and inductive names (for the checker) *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 433e2c5055..66577fecc4 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1772,7 +1772,7 @@ let compile_constant env sigma prefix ~interactive con cb = match cb.const_proj with | None -> begin match cb.const_body with - | Def t -> + | Def t when not cb.const_polymorphic -> let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code"); @@ -1902,8 +1902,8 @@ let compile_mind_deps env prefix ~interactive let rec compile_deps env sigma prefix ~interactive init t = match kind_of_term t with | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind - | Const (c,u) -> - let c = get_allias env c in + | Const c -> + let c,u = get_allias env c in let cb,(nameref,_) = lookup_constant_key c env in let (_, (_, const_updates)) = init in if is_code_loaded ~interactive nameref diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index c5417b2b69..947e0a1481 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -373,11 +373,11 @@ let makeblock env cn tag args = (* Translation of constants *) -let rec get_allias env kn = +let rec get_allias env (kn, u as p) = let tps = (lookup_constant kn env).const_body_code in match Cemitcodes.force tps with | Cemitcodes.BCallias kn' -> get_allias env kn' - | _ -> kn + | _ -> p (*i Global environment *) @@ -647,8 +647,8 @@ let rec lambda_of_constr env sigma c = and lambda_of_app env sigma f args = match kind_of_term f with - | Const (kn,u) -> - let kn = get_allias !global_env kn in + | Const (kn,u as c) -> + let kn,u = get_allias !global_env c in let cb = lookup_constant kn !global_env in (try let prefix = get_const_prefix !global_env kn in diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 10818e1aa0..6a97edc40c 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -27,7 +27,7 @@ val mk_lazy : lambda -> lambda val get_mind_prefix : env -> mutual_inductive -> string -val get_allias : env -> constant -> constant +val get_allias : env -> pconstant -> pconstant val lambda_of_constr : env -> evars -> Constr.constr -> lambda diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 62f454047f..4153b323b6 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -350,7 +350,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* else the oracle tells which constant is to be expanded *) let oracle = Closure.oracle_of_infos infos in let (app1,app2) = - if Conv_oracle.oracle_order oracle l2r (conv_key fl1) (conv_key fl2) then + if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then match unfold_reference infos fl1 with | Some def1 -> ((lft1, whd def1 v1), appr2) | None -> diff --git a/kernel/univ.ml b/kernel/univ.ml index d5939c67e8..e2a19b0e87 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1744,6 +1744,8 @@ type universe_instance = Instance.t type 'a puniverses = 'a * Instance.t let out_punivs (x, y) = x let in_punivs x = (x, Instance.empty) +let eq_puniverses f (x, u) (y, u') = + f x y && Instance.equal u u' (** A context of universe levels with universe constraints, representiong local universe variables and constraints *) diff --git a/kernel/univ.mli b/kernel/univ.mli index 36f3349c05..454134f21a 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -306,6 +306,8 @@ type 'a puniverses = 'a * universe_instance val out_punivs : 'a puniverses -> 'a val in_punivs : 'a -> 'a puniverses +val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool + (** A vector of universe levels with universe constraints, representiong local universe variables and associated constraints *) diff --git a/kernel/vars.ml b/kernel/vars.ml index 1685817a3f..88c1e1038c 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -336,3 +336,6 @@ let subst_instance_constr subst c = let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else map_rel_context (fun x -> subst_instance_constr s x) ctx + +type id_key = pconstant tableKey +let eq_id_key x y = Names.eq_table_key (Univ.eq_puniverses Constant.equal) x y diff --git a/kernel/vars.mli b/kernel/vars.mli index bdbecdedce..fdd4603b5b 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -87,3 +87,6 @@ val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_ (** Instance substitution for polymorphism. *) val subst_instance_constr : universe_instance -> constr -> constr val subst_instance_context : universe_instance -> rel_context -> rel_context + +type id_key = pconstant tableKey +val eq_id_key : id_key -> id_key -> bool diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 3f9345ff8c..80b15f8bad 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -86,23 +86,24 @@ and conv_whd env pb k whd1 whd2 cu = and conv_atom env pb k a1 stk1 a2 stk2 cu = match a1, a2 with - | Aind (kn1,i1), Aind(kn2,i2) -> - if eq_ind (kn1,i1) (kn2,i2) && compare_stack stk1 stk2 + | Aind ind1, Aind ind2 -> + if eq_puniverses eq_ind ind1 ind2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible | Aid ik1, Aid ik2 -> - if eq_id_key ik1 ik2 && compare_stack stk1 stk2 then + if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible | Aiddef(ik1,v1), Aiddef(ik2,v2) -> begin try - if eq_table_key ik1 ik2 && compare_stack stk1 stk2 then + if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible with NotConvertible -> - if oracle_order (oracle_of_infos !infos) false ik1 ik2 then + if oracle_order Univ.out_punivs (oracle_of_infos !infos) + false ik1 ik2 then conv_whd env pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu else conv_whd env pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu end diff --git a/kernel/vm.ml b/kernel/vm.ml index a7e5a55c45..2cc1efe431 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -137,10 +137,11 @@ type vswitch = { (* Generally the first field is a code pointer. *) (* Do not edit this type without editing C code, especially "coq_values.h" *) + type atom = - | Aid of id_key - | Aiddef of id_key * values - | Aind of inductive + | Aid of Vars.id_key + | Aiddef of Vars.id_key * values + | Aind of pinductive (* Zippers *) @@ -306,11 +307,11 @@ let val_of_atom a = val_of_obj (obj_of_atom a) module IdKeyHash = struct - type t = id_key - let equal = Names.eq_id_key + type t = pconstant tableKey + let equal = Names.eq_table_key (Univ.eq_puniverses Constant.equal) open Hashset.Combine let hash = function - | ConstKey c -> combinesmall 1 (Constant.hash c) + | ConstKey (c,u) -> combinesmall 1 (Constant.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) end diff --git a/kernel/vm.mli b/kernel/vm.mli index fa88418cef..295ea83c49 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -24,9 +24,9 @@ type vswitch type arguments type atom = - | Aid of id_key - | Aiddef of id_key * values - | Aind of inductive + | Aid of Vars.id_key + | Aiddef of Vars.id_key * values + | Aind of pinductive (** Zippers *) @@ -54,7 +54,7 @@ type whd = val val_of_str_const : structured_constant -> values val val_of_rel : int -> values val val_of_named : Id.t -> values -val val_of_constant : constant -> values +val val_of_constant : pconstant -> values external val_of_annot_switch : annot_switch -> values = "%identity" diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3f9f7ff289..203b1ec8a6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -511,8 +511,8 @@ let oracle_order env cf1 cf2 = when eq_constant p (Projection.constant p') -> Some (Projection.unfolded p') | _ -> - Some (Conv_oracle.oracle_order (Environ.oracle env) false - (translate_key k1) (translate_key k2)) + Some (Conv_oracle.oracle_order (fun x -> x) + (Environ.oracle env) false (translate_key k1) (translate_key k2)) let is_rigid_head flags t = match kind_of_term t with diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 1d97aef278..3f1e6e5d60 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -93,12 +93,11 @@ let construct_of_constr_const env tag typ = let construct_of_constr_block = construct_of_constr false -(* FIXME: treatment of universes *) let constr_type_of_idkey env idkey = match idkey with | ConstKey cst -> - let const_type = (Environ.lookup_constant cst env).const_type in - mkConst cst, Typeops.type_of_constant_type env const_type + let const_type = Typeops.type_of_constant_in env cst in + mkConstU cst, const_type | VarKey id -> let (_,_,ty) = lookup_named id env in mkVar id, ty @@ -107,7 +106,7 @@ let constr_type_of_idkey env idkey = let (_,_,ty) = lookup_rel n env in mkRel n, lift n ty -let type_of_ind env ind u = +let type_of_ind env (ind, u) = type_of_inductive env (Inductive.lookup_mind_specif env ind, u) let build_branches_type env (mind,_ as _ind) mib mip u params dep p = @@ -176,7 +175,7 @@ and nf_whd env whd typ = | Vatom_stk(Aiddef(idkey,v), stk) -> nf_whd env (whd_stack v stk) typ | Vatom_stk(Aind ind, stk) -> - nf_stk env (mkInd ind) (type_of_ind env ind Univ.Instance.empty (*FIXME*)) stk + nf_stk env (mkIndU ind) (type_of_ind env ind) stk and nf_stk env c t stk = match stk with @@ -194,7 +193,7 @@ and nf_stk env c t stk = let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in let pT = - hnf_prod_applist env (type_of_ind env ind u) (Array.to_list params) in + hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in let pT = whd_betadeltaiota env pT in let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in (* Calcul du type des branches *) diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index a04535f407..de615301d0 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -342,8 +342,8 @@ Arguments identity_rect [A] a P f y i. (** Identity type *) -Polymorphic Definition ID := forall A:Type, A -> A. -Polymorphic Definition id : ID := fun A x => x. +Definition ID := forall A:Type, A -> A. +Definition id : ID := fun A x => x. Definition IDProp := forall A:Prop, A -> A. Definition idProp : IDProp := fun A x => x. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 47e302e32b..1384901b70 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -21,19 +21,19 @@ Require Import Logic. Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset of elements of the type [A] which satisfy both [P] and [Q]. *) -(* Polymorphic *) Inductive sig (A:Type) (P:A -> Prop) : Type := +Inductive sig (A:Type) (P:A -> Prop) : Type := exist : forall x:A, P x -> sig P. -(* Polymorphic *) Inductive sig2 (A:Type) (P Q:A -> Prop) : Type := +Inductive sig2 (A:Type) (P Q:A -> Prop) : Type := exist2 : forall x:A, P x -> Q x -> sig2 P Q. (** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type. Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *) -(* Polymorphic *) Inductive sigT (A:Type) (P:A -> Type) : Type := +Inductive sigT (A:Type) (P:A -> Type) : Type := existT : forall x:A, P x -> sigT P. -(* Polymorphic *) Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := +Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := existT2 : forall x:A, P x -> Q x -> sigT2 P Q. (* Notations *) diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 4bc29a0719..e5be0ca925 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -15,8 +15,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* Set Universe Polymorphism. *) - (** The polymorphic identity function is defined in [Datatypes]. *) Arguments id {A} x. @@ -47,7 +45,7 @@ Definition const {A B} (a : A) := fun _ : B => a. (** The [flip] combinator reverses the first two arguments of a function. *) -Monomorphic Definition flip {A B C} (f : A -> B -> C) x y := f y x. +Definition flip {A B C} (f : A -> B -> C) x y := f y x. (** Application as a combinator. *) -- cgit v1.2.3 From 13140f20c1080a6ac0c0c7ad878fa1ff3f34de60 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 15 Jan 2015 15:04:48 +0100 Subject: vm_printers: fix compilation --- dev/vm_printers.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 50207157bb..4578a3b33d 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -13,7 +13,7 @@ let ppripos (ri,pos) = ("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n") | Reloc_const _ -> print_string "structured constant\n" - | Reloc_getglobal kn -> + | Reloc_getglobal (kn,_) -> print_string ("getglob "^(string_of_con kn)^"\n")); print_flush () @@ -30,7 +30,7 @@ let ppsort = function let print_idkey idk = match idk with - | ConstKey sp -> + | ConstKey (sp,_) -> print_string "Cons("; print_string (string_of_con sp); print_string ")" @@ -61,7 +61,7 @@ and ppatom a = match a with | Aid idk -> print_idkey idk | Aiddef(idk,_) -> print_string "&";print_idkey idk - | Aind(sp,i) -> print_string "Ind("; + | Aind((sp,i),_) -> print_string "Ind("; print_string (string_of_mind sp); print_string ","; print_int i; print_string ")" -- cgit v1.2.3 From 81489f299ef60c21ac3da1d2157b02c3b41886d1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 16 Jan 2015 17:33:54 +0530 Subject: Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _" Not supposed to be part of 8.5beta. This reverts commit 74682bb27da074fedc115238f3085baaccf12d73. --- tactics/class_tactics.ml | 10 +++++----- test-suite/bugs/closed/3794.v | 6 ------ 2 files changed, 5 insertions(+), 11 deletions(-) delete mode 100644 test-suite/bugs/closed/3794.v diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 7964c0a8fe..1c15fa40bf 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -197,8 +197,8 @@ let rec e_trivial_fail_db db_list local_db goal = in tclFIRST (List.map tclCOMPLETE tacl) goal -and e_my_find_search db_list local_db hdc complete sigma oconcl = - let prods, concl = decompose_prod_assum oconcl in +and e_my_find_search db_list local_db hdc complete sigma concl = + let prods, concl = decompose_prod_assum concl in let nprods = List.length prods in let freeze = try @@ -213,8 +213,8 @@ and e_my_find_search db_list local_db hdc complete sigma oconcl = (fun db -> let tacs = if Hint_db.use_dn db then (* Using dnet *) - Hint_db.map_eauto hdc oconcl db - else Hint_db.map_existential hdc oconcl db + Hint_db.map_eauto hdc concl db + else Hint_db.map_existential hdc concl db in let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in List.map (fun x -> (flags, x)) tacs) @@ -232,7 +232,7 @@ and e_my_find_search db_list local_db hdc complete sigma oconcl = (if complete then tclIDTAC else e_trivial_fail_db db_list local_db) | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]) | Extern tacast -> - Proofview.V82.of_tactic (conclPattern oconcl p tacast) + Proofview.V82.of_tactic (conclPattern concl p tacast) in let tac = if complete then tclCOMPLETE tac else tac in match t with diff --git a/test-suite/bugs/closed/3794.v b/test-suite/bugs/closed/3794.v deleted file mode 100644 index 6963d81c14..0000000000 --- a/test-suite/bugs/closed/3794.v +++ /dev/null @@ -1,6 +0,0 @@ -Hint Extern 10 ((?X = ?Y) -> False) => intros; discriminate. -Hint Unfold not : core. - -Goal true<>false. -typeclasses eauto with core. -Qed. \ No newline at end of file -- cgit v1.2.3 From cbe7a174cf6450dcfd402d407e8afefccccde92b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 16 Jan 2015 15:34:31 +0100 Subject: Documenting the removal of coercions between sig, sigT, sig2, etc. (source of incompatibility). --- CHANGES | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGES b/CHANGES index f0dd06e04f..3471bc61c4 100644 --- a/CHANGES +++ b/CHANGES @@ -388,6 +388,8 @@ Libraries - SetoidPermutation: a notion of permutation for lists modulo a setoid equality. - BigN: fixed the ocaml code doing the parsing/printing of big numbers. - List: a couple of lemmas added especially about no-duplication, partitions. +- Init: Removal of the coercions between variants of sigma-types and + subset types (possible source of incompatibility). Changes from V8.4beta to V8.4beta2 ================================== -- cgit v1.2.3 From 4985f0ff99278beb3b934f86edf1398659c611a8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 Jan 2015 21:09:30 +0100 Subject: coq_makefile: install also .v and .glob This is useful for PIDE based interfaces, since they can build hyperlinks out of .glob files and let the user jump to the corresponding .v files --- tools/coq_makefile.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index e9bdb6caca..d660f4205d 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -257,7 +257,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in let cmxsfiles = List.rev_append cmofiles mllibfiles in let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxsfiles)] inc in let where_what_oth = vars_to_put_by_root - [("VOFILES",vfiles);("NATIVEFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)] + [("VOFILES",vfiles);("VFILES",vfiles);("GLOBFILES",vfiles);("NATIVEFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)] inc in let doc_dir = where_put_doc inc in let () = if is_install = Project_file.UnspecInstall then -- cgit v1.2.3 From 9f5586d88880cbb98c92edfe9c33c76564f1a19c Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 16 Jan 2015 22:17:03 +0100 Subject: Make native compiler handle universe polymorphic definitions. One remaining issue: aliased constants raise an anomaly when some unsubstituted universe variables remain. VM may suffer from the same problem. --- kernel/declareops.ml | 10 ++ kernel/declareops.mli | 5 + kernel/inductive.ml | 15 +-- kernel/inductive.mli | 2 - kernel/nativecode.ml | 242 ++++++++++++++++++++++++++++++++++-------------- kernel/nativecode.mli | 2 + kernel/nativeconv.ml | 81 ++++++++-------- kernel/nativeinstr.mli | 8 +- kernel/nativelambda.ml | 26 +++--- kernel/nativevalues.ml | 21 +++-- kernel/nativevalues.mli | 10 +- kernel/subtyping.ml | 1 + kernel/univ.ml | 4 + kernel/univ.mli | 4 + pretyping/nativenorm.ml | 8 +- tactics/elimschemes.ml | 4 +- toplevel/record.ml | 2 +- toplevel/search.ml | 2 +- 18 files changed, 285 insertions(+), 162 deletions(-) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index d5df24a1a1..48a6098eee 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -260,6 +260,16 @@ let subst_mind_body sub mib = mind_universes = mib.mind_universes; mind_private = mib.mind_private } +let inductive_instance mib = + if mib.mind_polymorphic then + Univ.UContext.instance mib.mind_universes + else Univ.Instance.empty + +let inductive_context mib = + if mib.mind_polymorphic then + Univ.instantiate_univ_context mib.mind_universes + else Univ.UContext.empty + (** {6 Hash-consing of inductive declarations } *) let hcons_regular_ind_arity a = diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 02090ade5d..47a82cc6c0 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -8,6 +8,8 @@ open Declarations open Mod_subst +open Univ +open Context (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -75,6 +77,9 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body +val inductive_instance : mutual_inductive_body -> universe_instance +val inductive_context : mutual_inductive_body -> universe_context + (** {6 Hash-consing} *) (** Here, strictly speaking, we don't perform true hash-consing diff --git a/kernel/inductive.ml b/kernel/inductive.ml index fee510e966..bb57ad2566 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -53,20 +53,11 @@ let inductive_params (mib,_) = mib.mind_nparams let inductive_paramdecls (mib,u) = Vars.subst_instance_context u mib.mind_params_ctxt -let inductive_instance mib = - if mib.mind_polymorphic then - UContext.instance mib.mind_universes - else Instance.empty - -let inductive_context mib = - if mib.mind_polymorphic then - instantiate_univ_context mib.mind_universes - else UContext.empty - let instantiate_inductive_constraints mib u = if mib.mind_polymorphic then - subst_instance_constraints u (UContext.constraints mib.mind_universes) - else Constraint.empty + Univ.subst_instance_constraints u (Univ.UContext.constraints mib.mind_universes) + else Univ.Constraint.empty + (************************************************************************) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 9a321e5ca6..5847d25f6f 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -35,8 +35,6 @@ val lookup_mind_specif : env -> inductive -> mind_specif (** {6 Functions to build standard types related to inductive } *) val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list -val inductive_instance : mutual_inductive_body -> universe_instance -val inductive_context : mutual_inductive_body -> universe_context val inductive_paramdecls : mutual_inductive_body puniverses -> rel_context val instantiate_inductive_constraints : diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 66577fecc4..1a4a4b54d7 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -45,9 +45,9 @@ let fresh_lname n = (** Global names **) type gname = - | Gind of string * inductive (* prefix, inductive name *) - | Gconstruct of string * constructor (* prefix, constructor name *) - | Gconstant of string * constant (* prefix, constant name *) + | Gind of string * pinductive (* prefix, inductive name *) + | Gconstruct of string * pconstructor (* prefix, constructor name *) + | Gconstant of string * pconstant (* prefix, constant name *) | Gproj of string * constant (* prefix, constant name *) | Gcase of label option * int | Gpred of label option * int @@ -60,11 +60,12 @@ type gname = let eq_gname gn1 gn2 = match gn1, gn2 with - | Gind (s1, ind1), Gind (s2, ind2) -> String.equal s1 s2 && eq_ind ind1 ind2 + | Gind (s1, ind1), Gind (s2, ind2) -> + String.equal s1 s2 && Univ.eq_puniverses eq_ind ind1 ind2 | Gconstruct (s1, c1), Gconstruct (s2, c2) -> - String.equal s1 s2 && eq_constructor c1 c2 + String.equal s1 s2 && Univ.eq_puniverses eq_constructor c1 c2 | Gconstant (s1, c1), Gconstant (s2, c2) -> - String.equal s1 s2 && Constant.equal c1 c2 + String.equal s1 s2 && Univ.eq_puniverses Constant.equal c1 c2 | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2 | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2 @@ -85,9 +86,12 @@ let eq_gname gn1 gn2 = open Hashset.Combine let gname_hash gn = match gn with -| Gind (s, i) -> combinesmall 1 (combine (String.hash s) (ind_hash i)) -| Gconstruct (s, c) -> combinesmall 2 (combine (String.hash s) (constructor_hash c)) -| Gconstant (s, c) -> combinesmall 3 (combine (String.hash s) (Constant.hash c)) +| Gind (s, (ind,u)) -> + combinesmall 1 (combine3 (String.hash s) (ind_hash ind) (Univ.Instance.hash u)) +| Gconstruct (s, (c,u)) -> + combinesmall 2 (combine3 (String.hash s) (constructor_hash c) (Univ.Instance.hash u)) +| Gconstant (s, (c,u)) -> + combinesmall 3 (combine3 (String.hash s) (Constant.hash c) (Univ.Instance.hash u)) | Gcase (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i)) | Gpred (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i)) | Gfixtype (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i)) @@ -149,6 +153,7 @@ type symbol = | SymbInd of inductive | SymbMeta of metavariable | SymbEvar of existential + | SymbLevel of Univ.Level.t let dummy_symb = SymbValue (dummy_value ()) @@ -163,6 +168,7 @@ let eq_symbol sy1 sy2 = | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2 | SymbEvar (evk1,args1), SymbEvar (evk2,args2) -> Evar.equal evk1 evk2 && Array.for_all2 eq_constr args1 args2 + | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2 | _, _ -> false let hash_symbol symb = @@ -178,6 +184,7 @@ let hash_symbol symb = let evh = Evar.hash evk in let hl = Array.fold_left (fun h t -> combine h (Constr.hash t)) evh args in combinesmall 8 hl + | SymbLevel l -> combinesmall 9 (Univ.Level.hash l) module HashedTypeSymbol = struct type t = symbol @@ -231,6 +238,11 @@ let get_evar tbl i = | SymbEvar ev -> ev | _ -> anomaly (Pp.str "get_evar failed") +let get_level tbl i = + match tbl.(i) with + | SymbLevel u -> u + | _ -> anomaly (Pp.str "get_level failed") + let push_symbol x = try HashtblSymbol.find symb_tbl x with Not_found -> @@ -282,6 +294,8 @@ type primitive = | MLsub | MLmul | MLmagic + | MLarrayget + | Mk_empty_instance | Coq_primitive of Primitives.t * (prefix * constant) option let eq_primitive p1 p2 = @@ -302,6 +316,7 @@ let eq_primitive p1 p2 = | Mk_meta, Mk_meta -> true | Mk_evar, Mk_evar -> true | Mk_proj, Mk_proj -> true + | MLarrayget, MLarrayget -> true | _ -> false @@ -350,6 +365,8 @@ let primitive_hash = function | Coq_primitive (prim, Some (prefix,kn)) -> combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (Primitives.hash prim)) | Mk_proj -> 38 + | MLarrayget -> 39 + | Mk_empty_instance -> 40 type mllambda = | MLlocal of lname @@ -368,6 +385,7 @@ type mllambda = | MLuint of Uint31.t | MLsetref of string * mllambda | MLsequence of mllambda * mllambda + | MLarray of mllambda array and mllam_branches = ((constructor * lname option array) list * mllambda) array @@ -429,10 +447,13 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = | MLsetref (id1, ml1), MLsetref (id2, ml2) -> String.equal id1 id2 && eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 - | MLsequence (ml1, ml'1), MLsequence (ml2, ml'2) -> - eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 && - eq_mllambda gn1 gn2 n env1 env2 ml'1 ml'2 - | _, _ -> false + | MLsequence (ml1, ml'1), MLsequence (ml2, ml'2) -> + eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 && + eq_mllambda gn1 gn2 n env1 env2 ml'1 ml'2 + | MLarray arr1, MLarray arr2 -> + Array.equal (eq_mllambda gn1 gn2 n env1 env2) arr1 arr2 + + | _, _ -> false and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 = let eq_def (_,args1,ml1) (_,args2,ml2) = @@ -505,6 +526,8 @@ let rec hash_mllambda gn n env t = let hml = hash_mllambda gn n env ml in let hml' = hash_mllambda gn n env ml' in combinesmall 14 (combine hml hml') + | MLarray arr -> + combinesmall 15 (hash_mllambda_array gn n env 1 arr) and hash_mllambda_letrec gn n env init defs = let hash_def (_,args,ml) = @@ -569,7 +592,9 @@ let fv_lam l = | MLconstruct (_,_,p) -> Array.fold_right (fun a fv -> aux a bind fv) p fv | MLsetref(_,l) -> aux l bind fv - | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv) in + | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv) + | MLarray arr -> Array.fold_right (fun a fv -> aux a bind fv) arr fv + in aux l LNset.empty LNset.empty @@ -698,13 +723,15 @@ type env = env_bound : int; (* length of env_rel *) (* free variables *) env_urel : (int * mllambda) list ref; (* list of unbound rel *) - env_named : (identifier * mllambda) list ref } + env_named : (identifier * mllambda) list ref; + env_univ : lname option} -let empty_env () = +let empty_env univ () = { env_rel = []; env_bound = 0; env_urel = ref []; - env_named = ref [] + env_named = ref []; + env_univ = univ } let push_rel env id = @@ -741,7 +768,10 @@ let get_var env id = let local = MLlocal (fresh_lname (Name id)) in env.env_named := (id, local)::!(env.env_named); local - + +let fresh_univ () = + fresh_lname (Name (Id.of_string "univ")) + (*s Traduction of lambda to mllambda *) let get_prod_name codom = @@ -754,14 +784,18 @@ let get_lname (_,l) = | MLlocal id -> id | _ -> invalid_arg "Nativecode.get_lname" +(* Collects free variables from env in an array of local names *) let fv_params env = let fvn, fvr = !(env.env_named), !(env.env_urel) in let size = List.length fvn + List.length fvr in - if Int.equal size 0 then empty_params + let start,params = match env.env_univ with + | None -> 0, Array.make size dummy_lname + | Some u -> 1, let t = Array.make (size + 1) dummy_lname in t.(0) <- u; t + in + if Array.is_empty params then empty_params else begin - let params = Array.make size dummy_lname in let fvn = ref fvn in - let i = ref 0 in + let i = ref start in while not (List.is_empty !fvn) do params.(!i) <- get_lname (List.hd !fvn); fvn := List.tl !fvn; @@ -783,12 +817,15 @@ let empty_args = [||] let fv_args env fvn fvr = let size = List.length fvn + List.length fvr in - if Int.equal size 0 then empty_args + let start,args = match env.env_univ with + | None -> 0, Array.make size (MLint 0) + | Some u -> 1, let t = Array.make (size + 1) (MLint 0) in t.(0) <- MLlocal u; t + in + if Array.is_empty args then empty_args else begin - let args = Array.make size (MLint 0) in let fvn = ref fvn in - let i = ref 0 in + let i = ref start in while not (List.is_empty !fvn) do args.(!i) <- get_var env (fst (List.hd !fvn)); fvn := List.tl !fvn; @@ -837,6 +874,10 @@ let get_evar_code i = MLapp (MLglobal (Ginternal "get_evar"), [|MLglobal symbols_tbl_name; MLint i|]) +let get_level_code i = + MLapp (MLglobal (Ginternal "get_level"), + [|MLglobal symbols_tbl_name; MLint i|]) + type rlist = | Rnil | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist' @@ -978,6 +1019,19 @@ let compile_prim decl cond paux = List.fold_left (fun body (x,d) -> MLlet(x,d,body)) body decl in add_decl decl (compile_cond cond paux) +let ml_of_instance instance u = + let ml_of_level l = + match Univ.Level.var_index l with + | Some i -> + let univ = MLapp(MLprimitive MLmagic, [|MLlocal (Option.get instance)|]) in + mkMLapp (MLprimitive MLarrayget) [|univ; MLint i|] + | None -> let i = push_symbol (SymbLevel l) in get_level_code i + in + let u = Univ.Instance.to_array u in + if Array.is_empty u then [||] + else let u = Array.map ml_of_level u in + [|MLapp (MLprimitive MLmagic, [|MLarray u|])|] + let rec ml_of_lam env l t = match t with | Lrel(id ,i) -> get_rel env id i @@ -1007,7 +1061,9 @@ let compile_prim decl cond paux = MLlet(lname,def,body) | Lapp(f,args) -> MLapp(ml_of_lam env l f, Array.map (ml_of_lam env l) args) - | Lconst (prefix,c) -> MLglobal(Gconstant (prefix,c)) + | Lconst (prefix,c) -> + let args = ml_of_instance env.env_univ (snd c) in + mkMLapp (MLglobal(Gconstant (prefix,c))) args | Lproj (prefix,c) -> MLglobal(Gproj (prefix,c)) | Lprim _ -> let decl,cond,paux = extract_prim (ml_of_lam env l) t in @@ -1023,20 +1079,21 @@ let compile_prim decl cond paux = (* Remark: if we do not want to compile the predicate we should a least compute the fv, then store the lambda representation of the predicate (not the mllambda) *) - let env_p = empty_env () in + let env_p = empty_env env.env_univ () in let pn = fresh_gpred l in let mlp = ml_of_lam env_p l p in let mlp = generalize_fv env_p mlp in let (pfvn,pfvr) = !(env_p.env_named), !(env_p.env_urel) in let pn = push_global_let pn mlp in (* Compilation of the case *) - let env_c = empty_env () in + let env_c = empty_env env.env_univ () in let a_uid = fresh_lname Anonymous in let la_uid = MLlocal a_uid in (* compilation of branches *) let ml_br (c,params, body) = - let lnames, env = push_rels env_c params in - (c, lnames, ml_of_lam env l body) in + let lnames, env_c = push_rels env_c params in + (c, lnames, ml_of_lam env_c l body) + in let bs = Array.map ml_br bs in let cn = fresh_gcase l in (* Compilation of accu branch *) @@ -1080,7 +1137,7 @@ let compile_prim decl cond paux = start *) (* Compilation of type *) - let env_t = empty_env () in + let env_t = empty_env env.env_univ () in let ml_t = Array.map (ml_of_lam env_t l) tt in let params_t = fv_params env_t in let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in @@ -1089,7 +1146,7 @@ let compile_prim decl cond paux = let mk_type = MLapp(MLglobal gft, args_t) in (* Compilation of norm_i *) let ndef = Array.length ids in - let lf,env_n = push_rels (empty_env ()) ids in + let lf,env_n = push_rels (empty_env env.env_univ ()) ids in let t_params = Array.make ndef [||] in let t_norm_f = Array.make ndef (Gnorm (l,-1)) in let mk_let envi (id,def) t = MLlet (id,def,t) in @@ -1145,7 +1202,7 @@ let compile_prim decl cond paux = MLletrec(Array.mapi mkrec lf, lf_args.(start)) | Lcofix (start, (ids, tt, tb)) -> (* Compilation of type *) - let env_t = empty_env () in + let env_t = empty_env env.env_univ () in let ml_t = Array.map (ml_of_lam env_t l) tt in let params_t = fv_params env_t in let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in @@ -1154,7 +1211,7 @@ let compile_prim decl cond paux = let mk_type = MLapp(MLglobal gft, args_t) in (* Compilation of norm_i *) let ndef = Array.length ids in - let lf,env_n = push_rels (empty_env ()) ids in + let lf,env_n = push_rels (empty_env env.env_univ ()) ids in let t_params = Array.make ndef [||] in let t_norm_f = Array.make ndef (Gnorm (l,-1)) in let ml_of_fix i body = @@ -1212,33 +1269,42 @@ let compile_prim decl cond paux = (lname, paramsi, body) in MLletrec(Array.mapi mkrec lf, lf_args.(start)) *) - | Lmakeblock (prefix,cn,_,args) -> - MLconstruct(prefix,cn,Array.map (ml_of_lam env l) args) - | Lconstruct (prefix, cn) -> - MLglobal (Gconstruct (prefix, cn)) + | Lmakeblock (prefix,(cn,u),_,args) -> + let args = Array.map (ml_of_lam env l) args in + MLconstruct(prefix,cn,args) + | Lconstruct (prefix, (cn,u)) -> + let uargs = ml_of_instance env.env_univ u in + mkMLapp (MLglobal (Gconstruct (prefix, (cn,u)))) uargs | Luint v -> (match v with | UintVal i -> MLapp(MLprimitive Mk_uint, [|MLuint i|]) | UintDigits (prefix,cn,ds) -> - let c = MLglobal (Gconstruct (prefix, cn)) in + let c = MLglobal (Gconstruct (prefix, (cn, Univ.Instance.empty))) in let ds = Array.map (ml_of_lam env l) ds in let i31 = MLapp (MLprimitive Mk_I31_accu, [|c|]) in MLapp(i31, ds) | UintDecomp (prefix,cn,t) -> - let c = MLglobal (Gconstruct (prefix, cn)) in + let c = MLglobal (Gconstruct (prefix, (cn, Univ.Instance.empty))) in let t = ml_of_lam env l t in MLapp (MLprimitive Decomp_uint, [|c;t|])) | Lval v -> let i = push_symbol (SymbValue v) in get_value_code i | Lsort s -> let i = push_symbol (SymbSort s) in - MLapp(MLprimitive Mk_sort, [|get_sort_code i|]) - | Lind (prefix, ind) -> MLglobal (Gind (prefix, ind)) + let uarg = match env.env_univ with + | None -> MLarray [||] + | Some u -> MLlocal u + in + let uarg = MLapp(MLprimitive MLmagic, [|uarg|]) in + MLapp(MLprimitive Mk_sort, [|get_sort_code i; uarg|]) + | Lind (prefix, pind) -> + let uargs = ml_of_instance env.env_univ (snd pind) in + mkMLapp (MLglobal (Gind (prefix, pind))) uargs | Llazy -> MLglobal (Ginternal "lazy") | Lforce -> MLglobal (Ginternal "Lazy.force") -let mllambda_of_lambda auxdefs l t = - let env = empty_env () in +let mllambda_of_lambda univ auxdefs l t = + let env = empty_env univ () in global_stack := auxdefs; let ml = ml_of_lam env l t in let fv_rel = !(env.env_urel) in @@ -1285,6 +1351,7 @@ let subst s l = | MLconstruct(prefix,c,args) -> MLconstruct(prefix,c,Array.map aux args) | MLsetref(s,l1) -> MLsetref(s,aux l1) | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2) + | MLarray arr -> MLarray (Array.map aux arr) in aux l @@ -1391,6 +1458,7 @@ let optimize gdef l = MLconstruct(prefix,c,Array.map (optimize s) args) | MLsetref(r,l) -> MLsetref(r, optimize s l) | MLsequence(l1,l2) -> MLsequence(optimize s l1, optimize s l2) + | MLarray arr -> MLarray (Array.map (optimize s) arr) in optimize LNmap.empty l @@ -1462,11 +1530,11 @@ let string_of_mind mind = string_of_kn (user_mind mind) let string_of_gname g = match g with - | Gind (prefix, (mind, i)) -> + | Gind (prefix, ((mind,i), _)) -> Format.sprintf "%sindaccu_%s_%i" prefix (string_of_mind mind) i - | Gconstruct (prefix, ((mind, i), j)) -> + | Gconstruct (prefix, (((mind, i), j), _)) -> Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1) - | Gconstant (prefix, c) -> + | Gconstant (prefix, (c,_)) -> Format.sprintf "%sconst_%s" prefix (string_of_con c) | Gproj (prefix, c) -> Format.sprintf "%sproj_%s" prefix (string_of_con c) @@ -1544,6 +1612,17 @@ let pp_mllam fmt l = Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body | MLsequence(l1,l2) -> Format.fprintf fmt "@[%a;@\n%a@]" pp_mllam l1 pp_mllam l2 + | MLarray arr -> + let len = Array.length arr in + Format.fprintf fmt "@[[|"; + if 0 < len then begin + for i = 0 to len - 2 do + Format.fprintf fmt "%a;" pp_mllam arr.(i) + done; + pp_mllam fmt arr.(len-1) + end; + Format.fprintf fmt "|]@]" + and pp_letrec fmt defs = let len = Array.length defs in @@ -1662,11 +1741,14 @@ let pp_mllam fmt l = | MLsub -> Format.fprintf fmt "(-)" | MLmul -> Format.fprintf fmt "( * )" | MLmagic -> Format.fprintf fmt "Obj.magic" + | MLarrayget -> Format.fprintf fmt "Array.get" + | Mk_empty_instance -> Format.fprintf fmt "Univ.Instance.empty" | Coq_primitive (op,None) -> Format.fprintf fmt "no_check_%s" (Primitives.to_string op) | Coq_primitive (op, Some (prefix,kn)) -> + let u = Univ.Instance.empty in Format.fprintf fmt "%s %a" (Primitives.to_string op) - pp_mllam (MLglobal (Gconstant (prefix,kn))) + pp_mllam (MLglobal (Gconstant (prefix,(kn,u)))) in Format.fprintf fmt "@[%a@]" pp_mllam l @@ -1717,18 +1799,18 @@ let pp_global fmt g = Format.fprintf fmt "@[(* %s *)@]@." s (** Compilation of elements in environment **) -let rec compile_with_fv env sigma auxdefs l t = - let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda auxdefs l t in +let rec compile_with_fv env sigma univ auxdefs l t = + let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda univ auxdefs l t in if List.is_empty fv_named && List.is_empty fv_rel then (auxdefs,ml) - else apply_fv env sigma (fv_named,fv_rel) auxdefs ml + else apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml -and apply_fv env sigma (fv_named,fv_rel) auxdefs ml = +and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = let get_rel_val (n,_) auxdefs = (* match !(lookup_rel_native_val n env) with | NVKnone -> *) - compile_rel env sigma auxdefs n + compile_rel env sigma univ auxdefs n (* | NVKvalue (v,d) -> assert false *) in let get_named_val (id,_) auxdefs = @@ -1736,7 +1818,7 @@ and apply_fv env sigma (fv_named,fv_rel) auxdefs ml = match !(lookup_named_native_val id env) with | NVKnone -> *) - compile_named env sigma auxdefs id + compile_named env sigma univ auxdefs id (* | NVKvalue (v,d) -> assert false *) in let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in @@ -1747,23 +1829,23 @@ and apply_fv env sigma (fv_named,fv_rel) auxdefs ml = let aux_name = fresh_lname Anonymous in auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named))) -and compile_rel env sigma auxdefs n = +and compile_rel env sigma univ auxdefs n = let (_,body,_) = lookup_rel n env.env_rel_context in let n = rel_context_length env.env_rel_context - n in match body with | Some t -> let code = lambda_of_constr env sigma t in - let auxdefs,code = compile_with_fv env sigma auxdefs None code in + let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in Glet(Grel n, code)::auxdefs | None -> Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs -and compile_named env sigma auxdefs id = +and compile_named env sigma univ auxdefs id = let (_,body,_) = lookup_named id env.env_named_context in match body with | Some t -> let code = lambda_of_constr env sigma t in - let auxdefs,code = compile_with_fv env sigma auxdefs None code in + let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in Glet(Gnamed id, code)::auxdefs | None -> Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs @@ -1771,8 +1853,12 @@ and compile_named env sigma auxdefs id = let compile_constant env sigma prefix ~interactive con cb = match cb.const_proj with | None -> + let u = + if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + else Univ.Instance.empty + in begin match cb.const_body with - | Def t when not cb.const_polymorphic -> + | Def t -> let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code"); @@ -1783,20 +1869,34 @@ let compile_constant env sigma prefix ~interactive con cb = else Linked prefix in let l = con_label con in - let auxdefs,code = compile_with_fv env sigma [] (Some l) code in + let auxdefs,code = + if Univ.Instance.is_empty u then compile_with_fv env sigma None [] (Some l) code + else + let univ = fresh_univ () in + let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in + (auxdefs,mkMLlam [|univ|] code) + in if !Flags.debug then Pp.msg_debug (Pp.str "Generated mllambda code"); let code = - optimize_stk (Glet(Gconstant ("",con),code)::auxdefs) + optimize_stk (Glet(Gconstant ("",(con,u)),code)::auxdefs) in if !Flags.debug then Pp.msg_debug (Pp.str "Optimized mllambda code"); code, name | _ -> let i = push_symbol (SymbConst con) in - [Glet(Gconstant ("",con), MLapp (MLprimitive Mk_const, [|get_const_code i|]))], + let args = + if Univ.Instance.is_empty u then [|get_const_code i; MLarray [||]|] + else [|get_const_code i|] + in + (* + let t = mkMLlam [|univ|] (mkMLapp (MLprimitive Mk_const) + *) + [Glet(Gconstant ("",(con,u)), mkMLapp (MLprimitive Mk_const) args)], if interactive then LinkedInteractive prefix else Linked prefix end | Some pb -> + let u = Univ.Instance.empty in let mind = pb.proj_ind in let ind = (mind,0) in let mib = lookup_mind mind env in @@ -1823,7 +1923,7 @@ let compile_constant env sigma prefix ~interactive con cb = let gn = Gproj ("",con) in let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in let arg = fargs.(pb.proj_npars) in - Glet(Gconstant ("",con), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal + Glet(Gconstant ("",(con,u)), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal arg|]))):: [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix @@ -1849,12 +1949,18 @@ let param_name = Name (id_of_string "params") let arg_name = Name (id_of_string "arg") let compile_mind prefix ~interactive mb mind stack = + let u = Declareops.inductive_instance mb in let f i stack ob = let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in let j = push_symbol (SymbInd (mind,i)) in - let name = Gind ("", (mind, i)) in + let name = Gind ("", ((mind, i), u)) in let accu = - Glet(name, MLapp (MLprimitive Mk_ind, [|get_ind_code j|])) + let args = + if Univ.Instance.is_empty u then + [|get_ind_code j; MLarray [||]|] + else [|get_ind_code j|] + in + Glet(name, MLapp (MLprimitive Mk_ind, args)) in let nparams = mb.mind_nparams in let params = @@ -1862,7 +1968,7 @@ let compile_mind prefix ~interactive mb mind stack = let add_construct j acc (_,arity) = let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in let c = (mind,i), (j+1) in - Glet(Gconstruct ("",c), + Glet(Gconstruct ("",(c,u)), mkMLlam (Array.append params args) (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc in @@ -1961,8 +2067,8 @@ let mk_conv_code env sigma prefix t1 t2 = in let code1 = lambda_of_constr env sigma t1 in let code2 = lambda_of_constr env sigma t2 in - let (gl,code1) = compile_with_fv env sigma gl None code1 in - let (gl,code2) = compile_with_fv env sigma gl None code2 in + let (gl,code1) = compile_with_fv env sigma None gl None code1 in + let (gl,code2) = compile_with_fv env sigma None gl None code2 in let t1 = mk_internal_let "t1" code1 in let t2 = mk_internal_let "t2" code2 in let g1 = MLglobal (Ginternal "t1") in @@ -1983,7 +2089,7 @@ let mk_norm_code env sigma prefix t = compile_deps env sigma prefix ~interactive:true init t in let code = lambda_of_constr env sigma t in - let (gl,code) = compile_with_fv env sigma gl None code in + let (gl,code) = compile_with_fv env sigma None gl None code in let t1 = mk_internal_let "t1" code in let g1 = MLglobal (Ginternal "t1") in let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 385c77283b..893db92dd8 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -42,6 +42,8 @@ val get_meta : symbol array -> int -> metavariable val get_evar : symbol array -> int -> existential +val get_level : symbol array -> int -> Univ.Level.t + val get_symbols_tbl : unit -> symbol array type code_location_update diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 8930250fc2..75a3fc4582 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -16,17 +16,17 @@ open Nativecode (** This module implements the conversion test by compiling to OCaml code *) -let rec conv_val env pb lvl v1 v2 cu = - if v1 == v2 then cu +let rec conv_val env pb lvl cu v1 v2 = + if v1 == v2 then () else match kind_of_value v1, kind_of_value v2 with | Vaccu k1, Vaccu k2 -> - conv_accu env pb lvl k1 k2 cu + conv_accu env pb lvl cu k1 k2 | Vfun f1, Vfun f2 -> let v = mk_rel_accu lvl in - conv_val env CONV (lvl+1) (f1 v) (f2 v) cu + conv_val env CONV (lvl+1) cu (f1 v) (f2 v) | Vconst i1, Vconst i2 -> - if Int.equal i1 i2 then cu else raise NotConvertible + if not (Int.equal i1 i2) then raise NotConvertible | Vblock b1, Vblock b2 -> let n1 = block_size b1 in let n2 = block_size b2 in @@ -34,79 +34,76 @@ let rec conv_val env pb lvl v1 v2 cu = raise NotConvertible; let rec aux lvl max b1 b2 i cu = if Int.equal i max then - conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu + conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i) else - let cu = - conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in - aux lvl max b1 b2 (i+1) cu in + (conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i); + aux lvl max b1 b2 (i+1) cu) + in aux lvl (n1-1) b1 b2 0 cu | Vfun f1, _ -> - conv_val env CONV lvl v1 (fun x -> v2 x) cu + conv_val env CONV lvl cu v1 (fun x -> v2 x) | _, Vfun f2 -> - conv_val env CONV lvl (fun x -> v1 x) v2 cu + conv_val env CONV lvl cu (fun x -> v1 x) v2 | _, _ -> raise NotConvertible -and conv_accu env pb lvl k1 k2 cu = +and conv_accu env pb lvl cu k1 k2 = let n1 = accu_nargs k1 in let n2 = accu_nargs k2 in if not (Int.equal n1 n2) then raise NotConvertible; if Int.equal n1 0 then conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu else - let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in - List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu + (conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu; + List.iter2 (conv_val env CONV lvl cu) (args_of_accu k1) (args_of_accu k2)) and conv_atom env pb lvl a1 a2 cu = - if a1 == a2 then cu + if a1 == a2 then () else match a1, a2 with | Arel i1, Arel i2 -> - if not (Int.equal i1 i2) then raise NotConvertible; - cu + if not (Int.equal i1 i2) then raise NotConvertible | Aind ind1, Aind ind2 -> - if not (eq_ind ind1 ind2) then raise NotConvertible; - cu + if not (eq_puniverses eq_ind ind1 ind2) then raise NotConvertible | Aconstant c1, Aconstant c2 -> - if not (eq_constant c1 c2) then raise NotConvertible; - cu + if not (eq_puniverses eq_constant c1 c2) then raise NotConvertible | Asort s1, Asort s2 -> - check_sort_cmp_universes env pb s1 s2 cu; cu + check_sort_cmp_universes env pb s1 s2 cu | Avar id1, Avar id2 -> - if not (Id.equal id1 id2) then raise NotConvertible; - cu + if not (Id.equal id1 id2) then raise NotConvertible | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) -> if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible; - let cu = conv_accu env CONV lvl ac1 ac2 cu in + conv_accu env CONV lvl cu ac1 ac2; let tbl = a1.asw_reloc in let len = Array.length tbl in - if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu - else - let cu = conv_val env CONV lvl p1 p2 cu in + if Int.equal len 0 then conv_val env CONV lvl cu p1 p2 + else begin + conv_val env CONV lvl cu p1 p2; let max = len - 1 in - let rec aux i cu = + let rec aux i = let tag,arity = tbl.(i) in let ci = if Int.equal arity 0 then mk_const tag else mk_block tag (mk_rels_accu lvl arity) in let bi1 = bs1 ci and bi2 = bs2 ci in - if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu - else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in - aux 0 cu + if Int.equal i max then conv_val env CONV (lvl + arity) cu bi1 bi2 + else (conv_val env CONV (lvl + arity) cu bi1 bi2; aux (i+1)) in + aux 0 + end | Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) -> if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible; - if f1 == f2 then cu + if f1 == f2 then () else conv_fix env lvl t1 f1 t2 f2 cu | (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)), (Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) -> if not (Int.equal s1 s2) then raise NotConvertible; - if f1 == f2 then cu + if f1 == f2 then () else if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible else conv_fix env lvl t1 f1 t2 f2 cu | Aprod(_,d1,c1), Aprod(_,d2,c2) -> - let cu = conv_val env CONV lvl d1 d2 cu in + conv_val env CONV lvl cu d1 d2; let v = mk_rel_accu lvl in - conv_val env pb (lvl + 1) (d1 v) (d2 v) cu + conv_val env pb (lvl + 1) cu (d1 v) (d2 v) | _, _ -> raise NotConvertible (* Precondition length t1 = length f1 = length f2 = length t2 *) @@ -115,13 +112,13 @@ and conv_fix env lvl t1 f1 t2 f2 cu = let max = len - 1 in let fargs = mk_rels_accu lvl len in let flvl = lvl + len in - let rec aux i cu = - let cu = conv_val env CONV lvl t1.(i) t2.(i) cu in + let rec aux i = + conv_val env CONV lvl cu t1.(i) t2.(i); let fi1 = napply f1.(i) fargs in let fi2 = napply f2.(i) fargs in - if Int.equal i max then conv_val env CONV flvl fi1 fi2 cu - else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in - aux 0 cu + if Int.equal i max then conv_val env CONV flvl cu fi1 fi2 + else (conv_val env CONV flvl cu fi1 fi2; aux (i+1)) in + aux 0 let native_conv pb sigma env t1 t2 = if !Flags.no_native_compiler then begin @@ -144,7 +141,7 @@ let native_conv pb sigma env t1 t2 = let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in if !Flags.debug then Pp.msg_debug (Pp.str time_info); (* TODO change 0 when we can have deBruijn *) - ignore(conv_val env pb 0 !rt1 !rt2 (Environ.universes env)) + conv_val env pb 0 (Environ.universes env) !rt1 !rt2 end | _ -> anomaly (Pp.str "Compilation failure") diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index ad541ad73c..b7d3dadcd8 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -28,7 +28,7 @@ and lambda = | Llam of name array * lambda | Llet of name * lambda * lambda | Lapp of lambda * lambda array - | Lconst of prefix * constant + | Lconst of prefix * pconstant | Lproj of prefix * constant (* prefix, projection name *) | Lprim of prefix * constant * Primitives.t * lambda array | Lcase of annot_sw * lambda * lambda * lam_branches @@ -36,15 +36,15 @@ and lambda = | Lif of lambda * lambda * lambda | Lfix of (int array * int) * fix_decl | Lcofix of int * fix_decl - | Lmakeblock of prefix * constructor * int * lambda array + | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor name, constructor tag, arguments *) (* A fully applied constructor *) - | Lconstruct of prefix * constructor + | Lconstruct of prefix * pconstructor (* A partially applied constructor *) | Luint of uint | Lval of Nativevalues.t | Lsort of sorts - | Lind of prefix * inductive + | Lind of prefix * pinductive | Llazy | Lforce diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 947e0a1481..543397df53 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -363,13 +363,13 @@ let make_args start _end = (* Translation of constructors *) -let makeblock env cn tag args = +let makeblock env cn u tag args = if Array.for_all is_value args && Array.length args > 0 then let args = Array.map get_value args in Lval (Nativevalues.mk_block tag args) else let prefix = get_mind_prefix env (fst (fst cn)) in - Lmakeblock(prefix, cn, tag, args) + Lmakeblock(prefix, (cn,u), tag, args) (* Translation of constants *) @@ -553,9 +553,9 @@ let rec lambda_of_constr env sigma c = | Sort s -> Lsort s - | Ind (ind,u) -> + | Ind (ind,u as pind) -> let prefix = get_mind_prefix !global_env (fst ind) in - Lind (prefix, ind) + Lind (prefix, pind) | Prod(id, dom, codom) -> let ld = lambda_of_constr env sigma dom in @@ -666,13 +666,13 @@ and lambda_of_app env sigma f args = let prefix = get_const_prefix !global_env kn in let t = if is_lazy prefix (Mod_subst.force_constr csubst) then - mkLapp Lforce [|Lconst (prefix, kn)|] - else Lconst (prefix, kn) + mkLapp Lforce [|Lconst (prefix, (kn,u))|] + else Lconst (prefix, (kn,u)) in mkLapp t (lambda_of_args env sigma 0 args) | OpaqueDef _ | Undef _ -> let prefix = get_const_prefix !global_env kn in - mkLapp (Lconst (prefix, kn)) (lambda_of_args env sigma 0 args) + mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args env sigma 0 args) end) | Construct (c,u) -> let tag, nparams, arity = Renv.get_construct_info env c in @@ -692,14 +692,14 @@ and lambda_of_app env sigma f args = (!global_env).retroknowledge f prefix c args with Not_found -> let args = lambda_of_args env sigma nparams args in - makeblock !global_env c tag args + makeblock !global_env c u tag args else let args = lambda_of_args env sigma 0 args in (try Retroknowledge.get_native_constant_dynamic_info (!global_env).retroknowledge f prefix c args with Not_found -> - mkLapp (Lconstruct (prefix, c)) args) + mkLapp (Lconstruct (prefix, (c,u))) args) | _ -> let f = lambda_of_constr env sigma f in let args = lambda_of_args env sigma 0 args in @@ -752,8 +752,8 @@ let compile_dynamic_int31 fc prefix c args = (* We are relying here on the order of digits constructors *) let digits_from_uint digits_ind prefix i = - let d0 = Lconstruct (prefix, (digits_ind, 1)) in - let d1 = Lconstruct (prefix, (digits_ind, 2)) in + let d0 = Lconstruct (prefix, ((digits_ind, 1), Univ.Instance.empty)) in + let d1 = Lconstruct (prefix, ((digits_ind, 2), Univ.Instance.empty)) in let digits = Array.make 31 d0 in for k = 0 to 30 do if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then @@ -768,9 +768,9 @@ let before_match_int31 digits_ind fc prefix c t = match t with | Luint (UintVal i) -> let digits = digits_from_uint digits_ind prefix i in - mkLapp (Lconstruct (prefix,c)) digits + mkLapp (Lconstruct (prefix,(c, Univ.Instance.empty))) digits | Luint (UintDigits (prefix,c,args)) -> - mkLapp (Lconstruct (prefix,c)) args + mkLapp (Lconstruct (prefix,(c, Univ.Instance.empty))) args | _ -> Luint (UintDecomp (prefix,c,t)) let compile_prim prim kn fc prefix args = diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 098c59e823..d7a2195052 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -49,8 +49,8 @@ let eq_rec_pos = Array.equal Int.equal type atom = | Arel of int - | Aconstant of constant - | Aind of inductive + | Aconstant of pconstant + | Aind of pinductive | Asort of sorts | Avar of identifier | Acase of annot_sw * accumulator * t * (t -> t) @@ -106,14 +106,19 @@ let mk_rels_accu lvl len = let napply (f:t) (args: t array) = Array.fold_left (fun f a -> f a) f args -let mk_constant_accu kn = - mk_accu (Aconstant kn) +let mk_constant_accu kn u = + mk_accu (Aconstant (kn,Univ.Instance.of_array u)) -let mk_ind_accu s = - mk_accu (Aind s) +let mk_ind_accu ind u = + mk_accu (Aind (ind,Univ.Instance.of_array u)) -let mk_sort_accu s = - mk_accu (Asort s) +let mk_sort_accu s u = + match s with + | Prop _ -> mk_accu (Asort s) + | Type s -> + let u = Univ.Instance.of_array u in + let s = Univ.subst_instance_universe u s in + mk_accu (Asort (Type s)) let mk_var_accu id = mk_accu (Avar id) diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 983e7588d6..79e35d4a04 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -41,8 +41,8 @@ val eq_rec_pos : rec_pos -> rec_pos -> bool type atom = | Arel of int - | Aconstant of constant - | Aind of inductive + | Aconstant of pconstant + | Aind of pinductive | Asort of sorts | Avar of identifier | Acase of annot_sw * accumulator * t * (t -> t) @@ -59,9 +59,9 @@ type atom = val mk_accu : atom -> t val mk_rel_accu : int -> t val mk_rels_accu : int -> int -> t array -val mk_constant_accu : constant -> t -val mk_ind_accu : inductive -> t -val mk_sort_accu : sorts -> t +val mk_constant_accu : constant -> Univ.Level.t array -> t +val mk_ind_accu : inductive -> Univ.Level.t array -> t +val mk_sort_accu : sorts -> Univ.Level.t array -> t val mk_var_accu : identifier -> t val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t) val mk_prod_accu : name -> t -> t -> t diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index fa4f1c7c9f..db155e6c86 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -17,6 +17,7 @@ open Names open Univ open Term open Declarations +open Declareops open Reduction open Inductive open Modops diff --git a/kernel/univ.ml b/kernel/univ.ml index e2a19b0e87..7d64e894da 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -303,6 +303,10 @@ module Level = struct let var n = if n < 20 then vars.(n) else make (Var n) + let var_index u = + match data u with + | Var n -> Some n | _ -> None + let make m n = make (Level (n, Names.DirPath.hcons m)) end diff --git a/kernel/univ.mli b/kernel/univ.mli index 454134f21a..490ec03694 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -27,6 +27,8 @@ sig val equal : t -> t -> bool (** Equality function *) + val hash : t -> int + val make : Names.DirPath.t -> int -> t (** Create a new universe level from a unique identifier and an associated module path. *) @@ -35,6 +37,8 @@ sig (** Pretty-printing *) val var : int -> t + + val var_index : t -> int option end type universe_level = Level.t diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index ff48119ba2..bd427ecd08 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -257,8 +257,8 @@ and nf_bargs env b t = and nf_atom env atom = match atom with | Arel i -> mkRel (nb_rel env - i) - | Aconstant cst -> mkConst cst - | Aind ind -> mkInd ind + | Aconstant cst -> mkConstU cst + | Aind ind -> mkIndU ind | Asort s -> mkSort s | Avar id -> mkVar id | Aprod(n,dom,codom) -> @@ -280,9 +280,9 @@ and nf_atom_type env atom = let n = (nb_rel env - i) in mkRel n, type_of_rel env n | Aconstant cst -> - mkConst cst, fst (Typeops.type_of_constant env (cst,Univ.Instance.empty)) (* FIXME *) + mkConstU cst, Typeops.type_of_constant_in env cst | Aind ind -> - mkInd ind, Inductiveops.type_of_inductive env (ind,Univ.Instance.empty) + mkIndU ind, Inductiveops.type_of_inductive env ind | Asort s -> mkSort s, type_of_sort s | Avar id -> diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 9914ff3411..749e0d2b5b 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -47,7 +47,7 @@ let optimize_non_type_induction_scheme kind dep sort ind = (nf c', Evd.evar_universe_context sigma), eff else let mib,mip = Inductive.lookup_mind_specif env ind in - let ctx = Inductive.inductive_context mib in + let ctx = Declareops.inductive_context mib in let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in let ectx = Evd.evar_universe_context_of ctxset in @@ -58,7 +58,7 @@ let build_induction_scheme_in_type dep sort ind = let env = Global.env () in let ctx = let mib,mip = Inductive.lookup_mind_specif env ind in - Inductive.inductive_context mib + Declareops.inductive_context mib in let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in diff --git a/toplevel/record.ml b/toplevel/record.ml index e34206a41e..55f533512b 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -230,7 +230,7 @@ let instantiate_possibly_recursive_type indu paramdecls fields = let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in - let u = Inductive.inductive_instance mib in + let u = Declareops.inductive_instance mib in let paramdecls = Inductive.inductive_paramdecls (mib, u) in let poly = mib.mind_polymorphic and ctx = Univ.instantiate_univ_context mib.mind_universes in let indu = indsp, u in diff --git a/toplevel/search.ml b/toplevel/search.ml index bb0c2a2e72..59283edf9f 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -78,7 +78,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) = let mib = Global.lookup_mind mind in let iter_packet i mip = let ind = (mind, i) in - let u = Inductive.inductive_instance mib in + let u = Declareops.inductive_instance mib in let i = (ind, u) in let typ = Inductiveops.type_of_inductive env i in let () = fn (IndRef ind) env typ in -- cgit v1.2.3 From 9d60a8655f37ee922c662d15b3df0d94a8fd32aa Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 17 Jan 2015 14:11:13 +0530 Subject: Univs: Fix alias computation for VMs, computation of normal form of match predicates for vm_compute and compile polymorphic definitions to constant code. Add univscompute test-suite file testing VM computations in presence of polymorphic universes. --- kernel/cbytegen.ml | 2 +- kernel/term_typing.ml | 12 ++++++++---- pretyping/vnorm.ml | 4 ++-- test-suite/success/univscompute.v | 32 ++++++++++++++++++++++++++++++++ 4 files changed, 43 insertions(+), 7 deletions(-) create mode 100644 test-suite/success/univscompute.v diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 65ee655dab..d6c160c3dd 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -490,7 +490,7 @@ let rec get_allias env (kn,u as p) = let cb = lookup_constant kn env in let tps = cb.const_body_code in (match Cemitcodes.force tps with - | BCallias kn' -> get_allias env kn' + | BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u') | _ -> p) (* Compiling expressions *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 2e71b98062..a3441aa3ec 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -248,10 +248,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred) lc) in let tps = - match proj with - | None -> Cemitcodes.from_val (compile_constant_body env def) - | Some pb -> - Cemitcodes.from_val (compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))) + (* FIXME: incompleteness of the bytecode vm: we compile polymorphic + constants like opaque definitions. *) + if poly then Cemitcodes.from_val Cemitcodes.BCconstant + else + match proj with + | None -> Cemitcodes.from_val (compile_constant_body env def) + | Some pb -> + Cemitcodes.from_val (compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))) in { const_hyps = hyps; const_body = def; diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 3f1e6e5d60..19613c4e06 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -195,7 +195,7 @@ and nf_stk env c t stk = let pT = hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in let pT = whd_betadeltaiota env pT in - let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in + let dep, p = nf_predicate env (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) let btypes = build_branches_type env ind mib mip u params dep p in (* calcul des branches *) @@ -226,7 +226,7 @@ and nf_predicate env ind mip params v pT = let n = mip.mind_nrealargs in let rargs = Array.init n (fun i -> mkRel (n-i)) in let params = if Int.equal n 0 then params else Array.map (lift n) params in - let dom = mkApp(mkInd ind,Array.append params rargs) in + let dom = mkApp(mkIndU ind,Array.append params rargs) in let body = nf_vtype (push_rel (name,None,dom) env) vb in true, mkLambda(name,dom,body) | _, _ -> false, nf_val env v crazy_type diff --git a/test-suite/success/univscompute.v b/test-suite/success/univscompute.v new file mode 100644 index 0000000000..1d60ab360c --- /dev/null +++ b/test-suite/success/univscompute.v @@ -0,0 +1,32 @@ +Set Universe Polymorphism. + +Polymorphic Definition id {A : Type} (a : A) := a. + +Eval vm_compute in id 1. + +Polymorphic Inductive ind (A : Type) := cons : A -> ind A. + +Eval vm_compute in ind unit. + +Check ind unit. + +Eval vm_compute in ind unit. + +Definition bar := Eval vm_compute in ind unit. +Definition bar' := Eval vm_compute in id (cons _ tt). + +Definition bar'' := Eval native_compute in id 1. +Definition bar''' := Eval native_compute in id (cons _ tt). + +Definition barty := Eval native_compute in id (cons _ Set). + +Definition one := @id. + +Monomorphic Definition sec := one. + +Eval native_compute in sec. +Definition sec' := Eval native_compute in sec. +Eval vm_compute in sec. +Definition sec'' := Eval vm_compute in sec. + + -- cgit v1.2.3 From d030ce0721a46c539f9d6addb450ccc9d13163b3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 17 Jan 2015 14:49:26 +0530 Subject: Avoid compilation warning... might not be the best fix though. --- library/library.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/library.ml b/library/library.ml index f1bc491871..b443c2a4c7 100644 --- a/library/library.ml +++ b/library/library.ml @@ -465,7 +465,7 @@ let rec_intern_by_filename_only id f = m.library_name, needed let native_name_from_filename f = - let paths = Loadpath.get_paths () in + let _paths = Loadpath.get_paths () in let ch = System.with_magic_number_check raw_intern_library f in let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in Nativecode.mod_uid_of_dirpath lmd.md_name -- cgit v1.2.3 From 6d56defdaaa31e34422a70d3c2f236979426abb8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sat, 17 Jan 2015 09:43:39 +0100 Subject: Revert "Fix files in test-suite having to do with Require inside modules." This reverts commit a7ed77403cd15ba1cc2c05f2b6193b46f0028eda. --- test-suite/bugs/closed/335.v | 5 + test-suite/success/import_lib.v | 202 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 207 insertions(+) create mode 100644 test-suite/bugs/closed/335.v create mode 100644 test-suite/success/import_lib.v diff --git a/test-suite/bugs/closed/335.v b/test-suite/bugs/closed/335.v new file mode 100644 index 0000000000..166fa7a9f2 --- /dev/null +++ b/test-suite/bugs/closed/335.v @@ -0,0 +1,5 @@ +(* Compatibility of Require with backtracking at interactive module end *) + +Module A. +Require List. +End A. diff --git a/test-suite/success/import_lib.v b/test-suite/success/import_lib.v new file mode 100644 index 0000000000..fcedb2b1ad --- /dev/null +++ b/test-suite/success/import_lib.v @@ -0,0 +1,202 @@ +Definition le_trans := 0. + + +Module Test_Read. + Module M. + Require Le. (* Reading without importing *) + + Check Le.le_trans. + + Lemma th0 : le_trans = 0. + reflexivity. + Qed. + End M. + + Check Le.le_trans. + + Lemma th0 : le_trans = 0. + reflexivity. + Qed. + + Import M. + + Lemma th1 : le_trans = 0. + reflexivity. + Qed. +End Test_Read. + + +(****************************************************************) + +Definition le_decide := 1. (* from Arith/Compare *) +Definition min := 0. (* from Arith/Min *) + +Module Test_Require. + + Module M. + Require Import Compare. (* Imports Min as well *) + + Lemma th1 : le_decide = le_decide. + reflexivity. + Qed. + + Lemma th2 : min = min. + reflexivity. + Qed. + + End M. + + (* Checks that Compare and List are loaded *) + Check Compare.le_decide. + Check Min.min. + + + (* Checks that Compare and List are _not_ imported *) + Lemma th1 : le_decide = 1. + reflexivity. + Qed. + + Lemma th2 : min = 0. + reflexivity. + Qed. + + (* It should still be the case after Import M *) + Import M. + + Lemma th3 : le_decide = 1. + reflexivity. + Qed. + + Lemma th4 : min = 0. + reflexivity. + Qed. + +End Test_Require. + +(****************************************************************) + +Module Test_Import. + Module M. + Import Compare. (* Imports Min as well *) + + Lemma th1 : le_decide = le_decide. + reflexivity. + Qed. + + Lemma th2 : min = min. + reflexivity. + Qed. + + End M. + + (* Checks that Compare and List are loaded *) + Check Compare.le_decide. + Check Min.min. + + + (* Checks that Compare and List are _not_ imported *) + Lemma th1 : le_decide = 1. + reflexivity. + Qed. + + Lemma th2 : min = 0. + reflexivity. + Qed. + + (* It should still be the case after Import M *) + Import M. + + Lemma th3 : le_decide = 1. + reflexivity. + Qed. + + Lemma th4 : min = 0. + reflexivity. + Qed. +End Test_Import. + +(************************************************************************) + +Module Test_Export. + Module M. + Export Compare. (* Exports Min as well *) + + Lemma th1 : le_decide = le_decide. + reflexivity. + Qed. + + Lemma th2 : min = min. + reflexivity. + Qed. + + End M. + + + (* Checks that Compare and List are _not_ imported *) + Lemma th1 : le_decide = 1. + reflexivity. + Qed. + + Lemma th2 : min = 0. + reflexivity. + Qed. + + + (* After Import M they should be imported as well *) + + Import M. + + Lemma th3 : le_decide = le_decide. + reflexivity. + Qed. + + Lemma th4 : min = min. + reflexivity. + Qed. +End Test_Export. + + +(************************************************************************) + +Module Test_Require_Export. + + Definition mult_sym := 1. (* from Arith/Mult *) + Definition plus_sym := 0. (* from Arith/Plus *) + + Module M. + Require Export Mult. (* Exports Plus as well *) + + Lemma th1 : mult_comm = mult_comm. + reflexivity. + Qed. + + Lemma th2 : plus_comm = plus_comm. + reflexivity. + Qed. + + End M. + + + (* Checks that Mult and Plus are _not_ imported *) + Lemma th1 : mult_sym = 1. + reflexivity. + Qed. + + Lemma th2 : plus_sym = 0. + reflexivity. + Qed. + + + (* After Import M they should be imported as well *) + + Import M. + + Lemma th3 : mult_comm = mult_comm. + reflexivity. + Qed. + + Lemma th4 : plus_comm = plus_comm. + reflexivity. + Qed. + +End Test_Require_Export. -- cgit v1.2.3 From 335c960105971b2a86833793d893df4d9d0d1c90 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sat, 17 Jan 2015 09:43:54 +0100 Subject: Revert "Update test for #3363 now that Require is forbidden inside modules." This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d. --- test-suite/bugs/opened/3363.v | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/test-suite/bugs/opened/3363.v b/test-suite/bugs/opened/3363.v index 8307fdf506..800d89573c 100644 --- a/test-suite/bugs/opened/3363.v +++ b/test-suite/bugs/opened/3363.v @@ -1,4 +1,19 @@ -(** In this file, either both [Check]s should fail, or both should succeed. *) +(** In this file, either all four [Check]s should fail, or all four should succeed. *) +Module A. + Section HexStrings. + Require Import String. + End HexStrings. + Fail Check string. +End A. + +Module B. + Section HexStrings. + Require String. + Import String. + End HexStrings. + Fail Check string. +End B. + Section HexStrings. Require String. Import String. -- cgit v1.2.3 From 20f9a1404f84ddabde2d1cbacc9063d9de87dfa9 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sat, 17 Jan 2015 09:44:44 +0100 Subject: Revert "Adapting two files from test-suite to now forbidden Require's in modules." This reverts commit b0fceb96d0aaa2db6e774c629503be459017608e. --- test-suite/bugs/closed/2830.v | 4 ++-- test-suite/bugs/closed/3188.v | 6 ++---- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v index 219838aa3a..b72c821dfd 100644 --- a/test-suite/bugs/closed/2830.v +++ b/test-suite/bugs/closed/2830.v @@ -39,10 +39,10 @@ End A. (* 2- This was submitted by Andrew Appel *) -Require Import Program Relations. - Module B. +Require Import Program Relations. + Record ageable_facts (A:Type) (level: A -> nat) (age1:A -> option A) := { af_unage : forall x x' y', level x' = level y' -> age1 x = Some x' -> exists y, age1 y = Some y' ; af_level1 : forall x, age1 x = None <-> level x = 0 diff --git a/test-suite/bugs/closed/3188.v b/test-suite/bugs/closed/3188.v index 09ab4ca583..0117602670 100644 --- a/test-suite/bugs/closed/3188.v +++ b/test-suite/bugs/closed/3188.v @@ -1,8 +1,7 @@ (* File reduced by coq-bug-finder from 1656 lines to 221 lines to 26 lines to 7 lines. *) -Require Import Coq.Classes.RelationClasses. - Module Long. + Require Import Coq.Classes.RelationClasses. Hint Extern 0 => apply reflexivity : typeclass_instances. Hint Extern 1 => symmetry. @@ -12,9 +11,8 @@ Module Long. Abort. End Long. -Require Import Coq.Classes.RelationClasses. - Module Short. + Require Import Coq.Classes.RelationClasses. Hint Extern 0 => apply reflexivity : typeclass_instances. -- cgit v1.2.3 From b3b229aae5df17272d0d1060da4795be5d2c9573 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sat, 17 Jan 2015 11:48:21 +0100 Subject: Partially revert "Forbid Require inside interactive modules and module types." This reverts commit 6d5b56d971506dfadcfc824bfbb09dc21718e42b but does not put back in place the Requires inside modules that were found in the std lib. Conflicts: kernel/safe_typing.ml --- kernel/safe_typing.ml | 43 +++++++++++++++++++++++++++++++++++++++---- library/declaremods.ml | 1 - library/library.ml | 22 ++++++++++++++++------ 3 files changed, 55 insertions(+), 11 deletions(-) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 7c32ed379b..3a16bf806c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -85,6 +85,9 @@ open Declarations - [type_in_type] : does the universe hierarchy collapse? - [required] : names and digests of Require'd libraries since big-bang. This field will only grow + - [loads] : list of libraries Require'd inside the current module. + They will be propagated to the upper module level when + the current module ends. - [local_retroknowledge] *) @@ -121,6 +124,7 @@ type safe_environment = engagement : engagement option; type_in_type : bool; required : vodigest DPMap.t; + loads : (module_path * module_body) list; local_retroknowledge : Retroknowledge.action list } and modvariant = @@ -149,6 +153,7 @@ let empty_environment = engagement = None; type_in_type = false; required = DPMap.empty; + loads = []; local_retroknowledge = [] } let is_initial senv = @@ -284,7 +289,8 @@ let check_empty_context senv = it must have been freshly started *) let check_empty_struct senv = - assert (List.is_empty senv.revstruct) + assert (List.is_empty senv.revstruct + && List.is_empty senv.loads) (** When starting a library, the current environment should be initial i.e. only composed of Require's *) @@ -559,6 +565,12 @@ let add_module_parameter mbid mte inl senv = let functorize params init = List.fold_left (fun e (mbid,mt) -> MoreFunctor(mbid,mt,e)) init params +let propagate_loads senv = + List.fold_left + (fun env (_,mb) -> full_add_module mb env) + senv + (List.rev senv.loads) + (** Build the module body of the current module, taking in account a possible return type (_:T) *) @@ -603,6 +615,7 @@ let propagate_senv newdef newenv newresolver senv oldsenv = (* engagement is propagated to the upper level *) engagement = senv.engagement; required = senv.required; + loads = senv.loads@oldsenv.loads; local_retroknowledge = senv.local_retroknowledge@oldsenv.local_retroknowledge } @@ -616,7 +629,7 @@ let end_module l restype senv = let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in let newenv = set_engagement_opt newenv senv.engagement in let senv'= - { senv with + propagate_loads { senv with env = newenv; univ = Univ.Constraint.union senv.univ mb.mod_constraints} in let newenv = Environ.add_constraints mb.mod_constraints senv'.env in @@ -646,7 +659,7 @@ let end_modtype l senv = let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in let newenv = Environ.add_constraints senv.univ newenv in let newenv = set_engagement_opt newenv senv.engagement in - let senv' = {senv with env=newenv} in + let senv' = propagate_loads {senv with env=newenv} in let auto_tb = functorize params (NoFunctor (List.rev senv.revstruct)) in let mtb = build_mtb mp auto_tb senv'.univ senv.modresolver in let newenv = Environ.add_modtype mtb senv'.env in @@ -785,7 +798,8 @@ let import lib cst vodigest senv = in Modops.add_linked_module mb linkinfo env); modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver; - required = DPMap.add lib.comp_name vodigest senv.required } + required = DPMap.add lib.comp_name vodigest senv.required; + loads = (mp,mb)::senv.loads } (** {6 Safe typing } *) @@ -829,6 +843,27 @@ let register_inline kn senv = let add_constraints c = add_constraints (Now c) + +(* NB: The next old comment probably refers to [propagate_loads] above. + When a Require is done inside a module, we'll redo this require + at the upper level after the module is ended, and so on. + This is probably not a big deal anyway, since these Require's + inside modules should be pretty rare. Maybe someday we could + brutally forbid this tricky "feature"... *) + +(* we have an inefficiency: Since loaded files are added to the +environment every time a module is closed, their components are +calculated many times. This could be avoided in several ways: + +1 - for each file create a dummy environment containing only this +file's components, merge this environment with the global +environment, and store for the future (instead of just its type) + +2 - create "persistent modules" environment table in Environ add put +loaded by side-effect once and for all (like it is done in OCaml). +Would this be correct with respect to undo's and stuff ? +*) + let set_strategy e k l = { e with env = (Environ.set_oracle e.env (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) } diff --git a/library/declaremods.ml b/library/declaremods.ml index 53f270701c..cc7c4d7f11 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -850,7 +850,6 @@ let library_values = Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES" let register_library dir cenv (objs:library_objects) digest univ = - assert (not (Lib.is_module_or_modtype ())); let mp = MPfile dir in let () = try diff --git a/library/library.ml b/library/library.ml index b443c2a4c7..481d8707a9 100644 --- a/library/library.ml +++ b/library/library.ml @@ -537,12 +537,18 @@ let in_require : require_obj -> obj = if [export = Some true] *) let require_library_from_dirpath modrefl export = - if Lib.is_module_or_modtype () then - error "Require is not allowed inside a module or a module type"; let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in let modrefl = List.map fst modrefl in - add_anonymous_leaf (in_require (needed,modrefl,export)); + if Lib.is_module_or_modtype () then + begin + add_anonymous_leaf (in_require (needed,modrefl,None)); + Option.iter (fun exp -> + List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) + export + end + else + add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () let require_library qidl export = @@ -550,11 +556,15 @@ let require_library qidl export = require_library_from_dirpath modrefl export let require_library_from_file idopt file export = - if Lib.is_module_or_modtype () then - error "Require is not allowed inside a module or a module type"; let modref,needed = rec_intern_library_from_file idopt file in let needed = List.rev_map snd needed in - add_anonymous_leaf (in_require (needed,[modref],export)); + if Lib.is_module_or_modtype () then begin + add_anonymous_leaf (in_require (needed,[modref],None)); + Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) + export + end + else + add_anonymous_leaf (in_require (needed,[modref],export)); add_frozen_state () (* the function called by Vernacentries.vernac_import *) -- cgit v1.2.3 From 014878c3a05365d4af7e3edcfc8d612c45fdf1f3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 17 Jan 2015 19:06:10 +0530 Subject: Univs: Complete documentation in refman. --- doc/refman/Universes.tex | 71 +++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 64 insertions(+), 7 deletions(-) diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 4b71a25867..65218ba0dd 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -8,8 +8,8 @@ \begin{flushleft} \em The status of Universe Polymorphism is experimental. Some features - are not compatible with it (yet): native compilation and bytecode - compilation do not handle polymorphic definitions. + are not compatible with it (yet): bytecode compilation does not handle + polymorphic definitions, it treats them as opaque constants. \end{flushleft} This section describes the universe polymorphic extension of Coq. @@ -126,7 +126,7 @@ producing global universe constraints, one can use the variable will both get parameterized by the universes produced by the variable declaration. This is in contrast to a ``mononorphic'' variable which introduces global universes, making the two definitions depend on - the \emph{same} universes associated to the variable. + the \emph{same} global universes associated to the variable. \item \texttt{Hint \{Resolve, Rewrite\}} will use the auto/rewrite hint polymorphically, not at a single instance. \end{itemize} @@ -150,6 +150,31 @@ the terms are unfolded. This change implies that conversion and unification can have different unfolding behaviors on the same development with universe polymorphism switched on or off. +\asection{Minimization} + +Universe polymorphism with cumulativity tends to generate many useless +inclusion constraints in general. Typically at each application of a +polymorphic constant $f$, if an argument has expected type +\verb|Type@{i}| and is given a term of type \verb|Type@{j}|, a $j \le i$ +constraint will be generated. It is however often the case that an +equation $j = i$ would be more appropriate, when $f$'s +universes are fresh for example. Consider the following example: + +\begin{coq_eval} +Set Printing Universes. +\end{coq_eval} +\begin{coq_example} +Definition id0 := @pidentity nat 0. +Print id0. +\end{coq_example} + +This definition is elaborated by minimizing the universe of id to level +\Set~while the more general definition would keep the fresh level i +generated at the application of id and a constraint that $\Set \le i$. +This minimization process is applied only to fresh universe +variables. It simply adds an equation between the variable and its lower +bound if it is an atomic universe (i.e. not an algebraic max()). + \asection{Explicit Universes} \begin{flushleft} @@ -160,20 +185,52 @@ development with universe polymorphism switched on or off. The syntax has been extended to allow users to explicitely bind names to universes and explicitely instantantiate polymorphic definitions. Currently, binding is implicit at the first occurrence of a -universe name. For example below, i and j are introduced by the +universe name. For example, i and j below are introduced by the annotations attached to Types. \begin{coq_example*} Polymorphic Definition le (A : Type@{i}) : Type@{j} := A. \end{coq_example*} +\begin{coq_example} +Print le. +\end{coq_example} + +During refinement we find that $j$ must be larger or equal than $i$, as +we are using $A : Type@{i} <= Type@{j}$, hence the generated +constraint. Note that the names here are not bound in the final +definition, they just allow to specify locally what relations should +hold. In the term and in general in proof mode, universe names +introduced in the types can be refered to in terms. -Definitions can also be instantiated explicitely: +Definitions can also be instantiated explicitely, giving their full instance: \begin{coq_example} Check (pidentity@{Set}). -Check (le@{Type Set}). +Check (le@{i j}). \end{coq_example} -User-named universes are considered rigid for unification. +User-named universes are considered rigid for unification and are never +miminimized. + +Finally, two commands allow to name \emph{global} universes and constraints. + +\subsection{\tt Universe {\ident}. + \comindex{Universe} + \label{UniverseCmd}} + +This command declare a new global universe named {\ident}. + +\subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}. + \comindex{Constraint} + \label{ConstraintCmd}} + +This command declare a new constraint between named universes. +The order relation can be one of $<$, $<=$ or $=$. If consistent, +the constraint is then enforced in the global environment. + +\begin{ErrMsgs} +\item \errindex{Undeclared universe {\ident}}. +\item \errindex{Universe inconsistency} +\end{ErrMsgs} %%% Local Variables: %%% mode: latex -- cgit v1.2.3 From 3bcca0aecb368a723d247d1f8b2348790bc87035 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 17 Jan 2015 20:17:17 +0530 Subject: Univs: proper printing of global and local universe names (only printing functions touched in the kernel). --- dev/top_printers.ml | 13 ++++---- interp/constrextern.ml | 2 +- interp/constrextern.mli | 2 +- kernel/univ.ml | 69 ++++++++++++++++++++++--------------------- kernel/univ.mli | 16 +++++----- library/universes.ml | 3 ++ library/universes.mli | 2 ++ pretyping/detyping.ml | 25 +++++++--------- pretyping/detyping.mli | 2 +- pretyping/evd.ml | 35 +++++++++++++++------- pretyping/evd.mli | 1 + pretyping/reductionops.ml | 3 +- pretyping/termops.ml | 2 +- printing/pptactic.ml | 2 +- printing/printer.ml | 12 +++----- printing/printer.mli | 3 +- tactics/inv.ml | 2 +- test-suite/bugs/closed/3392.v | 2 +- toplevel/cerrors.ml | 3 +- toplevel/himsg.ml | 17 ++++++----- toplevel/vernacentries.ml | 4 +-- 21 files changed, 119 insertions(+), 101 deletions(-) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 202f9db023..dea70360a5 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -207,21 +207,22 @@ let ppuni u = pp(pr_uni u) let ppuni_level u = pp (Level.pr u) let ppuniverse u = pp (str"[" ++ Universe.pr u ++ str"]") -let ppuniverse_set l = pp (LSet.pr l) -let ppuniverse_instance l = pp (Instance.pr l) -let ppuniverse_context l = pp (pr_universe_context l) -let ppuniverse_context_set l = pp (pr_universe_context_set l) +let prlev = Universes.pr_with_global_universes +let ppuniverse_set l = pp (LSet.pr prlev l) +let ppuniverse_instance l = pp (Instance.pr prlev l) +let ppuniverse_context l = pp (pr_universe_context prlev l) +let ppuniverse_context_set l = pp (pr_universe_context_set prlev l) let ppuniverse_subst l = pp (Univ.pr_universe_subst l) let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l) let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l) let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l) let ppconstraints_map c = pp (Universes.pr_constraints_map c) -let ppconstraints c = pp (pr_constraints c) +let ppconstraints c = pp (pr_constraints Level.pr c) let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -let ppuniverses u = pp (Univ.pr_universes u) +let ppuniverses u = pp (Univ.pr_universes Level.pr u) let ppnamedcontextval e = pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e)) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 4b20b024dd..58e1eb1d17 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -956,7 +956,7 @@ let extern_type goal_concl_style env sigma t = let r = Detyping.detype goal_concl_style avoid env sigma t in extern_glob_type (vars_of_env env) r -let extern_sort s = extern_glob_sort (detype_sort s) +let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) let extern_closed_glob ?lax goal_concl_style env sigma t = let avoid = if goal_concl_style then ids_of_context env else [] in diff --git a/interp/constrextern.mli b/interp/constrextern.mli index d11248a595..b797e455c0 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -40,7 +40,7 @@ val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr -val extern_sort : sorts -> glob_sort +val extern_sort : Evd.evar_map -> sorts -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> rel_context -> local_binder list diff --git a/kernel/univ.ml b/kernel/univ.ml index 7d64e894da..08e9fee051 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -343,8 +343,8 @@ end module LSet = struct include LMap.Set - let pr s = - str"{" ++ prlist_with_sep spc Level.pr (elements s) ++ str"}" + let pr prl s = + str"{" ++ prlist_with_sep spc prl (elements s) ++ str"}" let of_array l = Array.fold_left (fun acc x -> add x acc) empty l @@ -1265,10 +1265,10 @@ struct module S = Set.Make(UConstraintOrd) include S - let pr c = + let pr prl c = fold (fun (u1,op,u2) pp_std -> - pp_std ++ Level.pr u1 ++ pr_constraint_type op ++ - Level.pr u2 ++ fnl () ) c (str "") + pp_std ++ prl u1 ++ pr_constraint_type op ++ + prl u2 ++ fnl () ) c (str "") end @@ -1641,7 +1641,7 @@ module Instance : sig val subst_fn : universe_level_subst_fn -> t -> t - val pr : t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds val levels : t -> LSet.t val check_eq : t check_function end = @@ -1718,7 +1718,7 @@ struct let levels x = LSet.of_array x let pr = - prvect_with_sep spc Level.pr + prvect_with_sep spc let equal t u = t == u || @@ -1764,9 +1764,9 @@ struct let empty = (Instance.empty, Constraint.empty) let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst - let pr (univs, cst as ctx) = + let pr prl (univs, cst as ctx) = if is_empty ctx then mt() else - Instance.pr univs ++ str " |= " ++ v 0 (Constraint.pr cst) + Instance.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst) let hcons (univs, cst) = (Instance.hcons univs, hcons_constraints cst) @@ -1832,9 +1832,9 @@ struct let of_context (ctx, cst) = (Instance.levels ctx, cst) - let pr (univs, cst as ctx) = + let pr prl (univs, cst as ctx) = if is_empty ctx then mt() else - LSet.pr univs ++ str " |= " ++ v 0 (Constraint.pr cst) + LSet.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst) let constraints (univs, cst) = cst let levels (univs, cst) = univs @@ -1983,7 +1983,7 @@ let abstract_universes poly ctx = (** Pretty-printing *) -let pr_arc = function +let pr_arc prl = function | _, Canonical {univ=u; lt=[]; le=[]} -> mt () | _, Canonical {univ=u; lt=lt; le=le} -> @@ -1991,20 +1991,20 @@ let pr_arc = function | [], _ | _, [] -> mt () | _ -> spc () in - Level.pr u ++ str " " ++ + prl u ++ str " " ++ v 0 - (pr_sequence (fun v -> str "< " ++ Level.pr v) lt ++ + (pr_sequence (fun v -> str "< " ++ prl v) lt ++ opt_sep ++ - pr_sequence (fun v -> str "<= " ++ Level.pr v) le) ++ + pr_sequence (fun v -> str "<= " ++ prl v) le) ++ fnl () | u, Equiv v -> - Level.pr u ++ str " = " ++ Level.pr v ++ fnl () + prl u ++ str " = " ++ prl v ++ fnl () -let pr_universes g = +let pr_universes prl g = let graph = UMap.fold (fun u a l -> (u,a)::l) g [] in - prlist pr_arc graph + prlist (pr_arc prl) graph -let pr_constraints = Constraint.pr +let pr_constraints prl = Constraint.pr prl let pr_universe_context = UContext.pr @@ -2049,21 +2049,22 @@ let hcons_universe_context_set (v, c) = let hcons_univ x = Universe.hcons x -let explain_universe_inconsistency (o,u,v,p) = - let pr_rel = function - | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" - in - let reason = match p with - | None | Some [] -> mt() - | Some p -> - str " because" ++ spc() ++ pr_uni v ++ - prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v) - p ++ - (if Universe.equal (snd (List.last p)) u then mt() else - (spc() ++ str "= " ++ pr_uni u)) - in - str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++ - pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")" +let explain_universe_inconsistency prl (o,u,v,p) = + let pr_uni = Universe.pr_with prl in + let pr_rel = function + | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" + in + let reason = match p with + | None | Some [] -> mt() + | Some p -> + str " because" ++ spc() ++ pr_uni v ++ + prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v) + p ++ + (if Universe.equal (snd (List.last p)) u then mt() else + (spc() ++ str "= " ++ pr_uni u)) + in + str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++ + pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")" let compare_levels = Level.compare let eq_levels = Level.equal diff --git a/kernel/univ.mli b/kernel/univ.mli index 490ec03694..7aaf2ffe61 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -49,7 +49,7 @@ module LSet : sig include CSig.SetS with type elt = universe_level - val pr : t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds (** Pretty-printing *) end @@ -292,7 +292,7 @@ sig val subst_fn : universe_level_subst_fn -> t -> t (** Substitution by a level-to-level function. *) - val pr : t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds (** Pretty-printing, no comments *) val levels : t -> LSet.t @@ -413,14 +413,16 @@ val instantiate_univ_constraints : universe_instance -> universe_context -> cons (** {6 Pretty-printing of universes. } *) -val pr_universes : universes -> Pp.std_ppcmds +val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds val pr_constraint_type : constraint_type -> Pp.std_ppcmds -val pr_constraints : constraints -> Pp.std_ppcmds -val pr_universe_context : universe_context -> Pp.std_ppcmds -val pr_universe_context_set : universe_context_set -> Pp.std_ppcmds +val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds +val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds +val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds +val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) -> + univ_inconsistency -> Pp.std_ppcmds + val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds val pr_universe_subst : universe_subst -> Pp.std_ppcmds -val explain_universe_inconsistency : univ_inconsistency -> Pp.std_ppcmds (** {6 Dumping to a file } *) diff --git a/library/universes.ml b/library/universes.ml index 31bbd15041..79070763ec 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -22,6 +22,9 @@ let global_universes = Summary.ref ~name:"Global universe names" let global_universe_names () = !global_universes let set_global_universe_names s = global_universes := s +let pr_with_global_universes l = + try Nameops.pr_id (LMap.find l (snd !global_universes)) + with Not_found -> Level.pr l type universe_constraint_type = ULe | UEq | ULub diff --git a/library/universes.mli b/library/universes.mli index 0053d8f4f7..f2f68d329c 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -23,6 +23,8 @@ type universe_names = val global_universe_names : unit -> universe_names val set_global_universe_names : universe_names -> unit +val pr_with_global_universes : Level.t -> Pp.std_ppcmds + (** The global universe counter *) val set_remote_new_univ_level : universe_level RemoteCounter.installer diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 2df1975461..046ee0dad5 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -394,18 +394,13 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let eqnl = detype_eqns constructs constagsl bl in GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) -let detype_sort = function +let detype_sort sigma = function | Prop Null -> GProp | Prop Pos -> GSet | Type u -> GType (if !print_universes - then - let _, map = Universes.global_universe_names () in - let pr_level u = - try Nameops.pr_id (Univ.LMap.find u map) with Not_found -> Univ.Level.pr u - in - [Pp.string_of_ppcmds (Univ.Universe.pr_with pr_level u)] + then [Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)] else []) type binder_kind = BProd | BLambda | BLetIn @@ -416,12 +411,12 @@ type binder_kind = BProd | BLambda | BLetIn let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable")) let set_detype_anonymous f = detype_anonymous := f -let detype_level l = - GType (Some (Pp.string_of_ppcmds (Univ.Level.pr l))) +let detype_level sigma l = + GType (Some (Pp.string_of_ppcmds (Evd.pr_evd_level sigma l))) -let detype_instance l = +let detype_instance sigma l = if Univ.Instance.is_empty l then None - else Some (List.map detype_level (Array.to_list (Univ.Instance.to_array l))) + else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) let rec detype flags avoid env sigma t = match kind_of_term (collapse_appl t) with @@ -439,7 +434,7 @@ let rec detype flags avoid env sigma t = | Var id -> (try let _ = Global.lookup_named id in GRef (dl, VarRef id, None) with Not_found -> GVar (dl, id)) - | Sort s -> GSort (dl,detype_sort s) + | Sort s -> GSort (dl,detype_sort sigma s) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> detype flags avoid env sigma c1 | Cast (c1,k,c2) -> @@ -463,7 +458,7 @@ let rec detype flags avoid env sigma t = in mkapp (detype flags avoid env sigma f) (Array.map_to_list (detype flags avoid env sigma) args) - | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance u) + | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance sigma u) | Proj (p,c) -> let noparams () = let pb = Environ.lookup_projection p (snd env) in @@ -521,9 +516,9 @@ let rec detype flags avoid env sigma t = GEvar (dl,id, List.map (on_snd (detype flags avoid env sigma)) l) | Ind (ind_sp,u) -> - GRef (dl, IndRef ind_sp, detype_instance u) + GRef (dl, IndRef ind_sp, detype_instance sigma u) | Construct (cstr_sp,u) -> - GRef (dl, ConstructRef cstr_sp, detype_instance u) + GRef (dl, ConstructRef cstr_sp, detype_instance sigma u) | Case (ci,p,c,bl) -> let comp = computable p (List.length (ci.ci_pp_info.ind_tags)) in detype_case comp (detype flags avoid env sigma) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 725fff5b2c..eb158686aa 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -43,7 +43,7 @@ val detype_case : Id.t list -> inductive * case_style * bool list array * bool list -> constr option -> constr -> constr array -> glob_constr -val detype_sort : sorts -> glob_sort +val detype_sort : evar_map -> sorts -> glob_sort val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> evar_map -> rel_context -> glob_decl list diff --git a/pretyping/evd.ml b/pretyping/evd.ml index d629fd5f5d..ee72d31471 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -275,7 +275,7 @@ end (* 2nd part used to check consistency on the fly. *) type evar_universe_context = - { uctx_names : Univ.Level.t UNameMap.t; + { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t; uctx_local : Univ.universe_context_set; (** The local context of variables *) uctx_univ_variables : Universes.universe_opt_subst; (** The local universes that are unification variables *) @@ -288,7 +288,7 @@ type evar_universe_context = } let empty_evar_universe_context = - { uctx_names = UNameMap.empty; + { uctx_names = UNameMap.empty, Univ.LMap.empty; uctx_local = Univ.ContextSet.empty; uctx_univ_variables = Univ.LMap.empty; uctx_univ_algebraic = Univ.LSet.empty; @@ -309,8 +309,9 @@ let union_evar_universe_context ctx ctx' = else if is_empty_evar_universe_context ctx' then ctx else let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in - let names = UNameMap.union ctx.uctx_names ctx'.uctx_names in - { uctx_names = names; + let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in + let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in + { uctx_names = (names, names_rev); uctx_local = local; uctx_univ_variables = Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; @@ -1004,6 +1005,9 @@ let merge_universe_subst evd subst = let with_context_set rigid d (a, ctx) = (merge_context_set rigid d ctx, a) +let add_uctx_names s l (names, names_rev) = + (UNameMap.add s l names, Univ.LMap.add l s names_rev) + let uctx_new_univ_variable rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = let u = Universes.new_univ_level (Global.current_dirpath ()) in @@ -1018,7 +1022,7 @@ let uctx_new_univ_variable rigid name else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in let names = match name with - | Some n -> UNameMap.add n u uctx.uctx_names + | Some n -> add_uctx_names n u uctx.uctx_names | None -> uctx.uctx_names in {uctx' with uctx_names = names; uctx_local = ctx'; @@ -1253,11 +1257,10 @@ let nf_constraints = else nf_constraints let universe_of_name evd s = - UNameMap.find s evd.universes.uctx_names + UNameMap.find s (fst evd.universes.uctx_names) let add_universe_name evd s l = - let names = evd.universes.uctx_names in - let names' = UNameMap.add s l names in + let names' = add_uctx_names s l evd.universes.uctx_names in {evd with universes = {evd.universes with uctx_names = names'}} let universes evd = evd.universes.uctx_universes @@ -1689,11 +1692,23 @@ let evar_dependency_closure n sigma = let has_no_evar sigma = EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars +let pr_uctx_level uctx = + let map, map_rev = uctx.uctx_names in + fun l -> + try str(Univ.LMap.find l map_rev) + with Not_found -> + Universes.pr_with_global_universes l + +let pr_evd_level evd = pr_uctx_level evd.universes + let pr_evar_universe_context ctx = + let prl = pr_uctx_level ctx in if is_empty_evar_universe_context ctx then mt () else - (str"UNIVERSES:"++brk(0,1)++ h 0 (Univ.pr_universe_context_set ctx.uctx_local) ++ fnl () ++ - str"ALGEBRAIC UNIVERSES:"++brk(0,1)++h 0 (Univ.LSet.pr ctx.uctx_univ_algebraic) ++ fnl() ++ + (str"UNIVERSES:"++brk(0,1)++ + h 0 (Univ.pr_universe_context_set prl ctx.uctx_local) ++ fnl () ++ + str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ + h 0 (Univ.LSet.pr prl ctx.uctx_univ_algebraic) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables) ++ fnl()) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 82daa7da3d..53f8b0db8c 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -598,6 +598,7 @@ val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) -> evar_map -> Pp.std_ppcmds val pr_metaset : Metaset.t -> Pp.std_ppcmds val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds +val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds (** {5 Deprecated functions} *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index b8e3b3b145..a23963abca 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -306,7 +306,8 @@ struct match c with | Cst_const (c, u) -> if Univ.Instance.is_empty u then Constant.print c - else str"(" ++ Constant.print c ++ str ", " ++ Univ.Instance.pr u ++ str")" + else str"(" ++ Constant.print c ++ str ", " ++ + Univ.Instance.pr Univ.Level.pr u ++ str")" | Cst_proj p -> str".(" ++ Constant.print (Projection.constant p) ++ str")" diff --git a/pretyping/termops.ml b/pretyping/termops.ml index eee94f228f..5862a8525d 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -46,7 +46,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) = let pr_puniverses p u = if Univ.Instance.is_empty u then p - else p ++ str"(*" ++ Univ.Instance.pr u ++ str"*)" + else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" let rec pr_constr c = match kind_of_term c with | Rel n -> str "#"++int n diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7cc193a8d5..f8264e5af6 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1451,7 +1451,7 @@ let () = (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id))) ; Genprint.register_print0 Constrarg.wit_sort - pr_glob_sort pr_glob_sort pr_sort; + pr_glob_sort pr_glob_sort (pr_sort Evd.empty); Genprint.register_print0 Constrarg.wit_uconstr Ppconstr.pr_constr_expr diff --git a/printing/printer.ml b/printing/printer.ml index 7d5b71f340..3403fb9c3b 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -143,17 +143,12 @@ let pr_constr_pattern t = let (sigma, env) = get_current_context () in pr_constr_pattern_env env sigma t -let pr_sort s = pr_glob_sort (extern_sort s) +let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) let _ = Termops.set_print_constr (fun env t -> pr_lconstr_expr (extern_constr ~lax:true false env Evd.empty t)) let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" -let pr_univ_cstr (c:Univ.constraints) = - if !Detyping.print_universes && not (Univ.Constraint.is_empty c) then - fnl()++pr_in_comment (fun c -> v 0 (Univ.pr_constraints c)) c - else - mt() (** Term printers resilient to [Nametab] errors *) @@ -216,7 +211,8 @@ let safe_pr_constr t = let pr_universe_ctx c = if !Detyping.print_universes && not (Univ.UContext.is_empty c) then - fnl()++pr_in_comment (fun c -> v 0 (Univ.pr_universe_context c)) c + fnl()++pr_in_comment (fun c -> v 0 + (Univ.pr_universe_context Universes.pr_with_global_universes c)) c else mt() @@ -229,7 +225,7 @@ let pr_global = pr_global_env Id.Set.empty let pr_puniverses f env (c,u) = f env c ++ (if !Constrextern.print_universes then - str"(*" ++ Univ.Instance.pr u ++ str"*)" + str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" else mt ()) let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) diff --git a/printing/printer.mli b/printing/printer.mli index 75ab1722db..6b9c70815d 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -79,12 +79,11 @@ val pr_constr_pattern : constr_pattern -> std_ppcmds val pr_cases_pattern : cases_pattern -> std_ppcmds -val pr_sort : sorts -> std_ppcmds +val pr_sort : evar_map -> sorts -> std_ppcmds (** Universe constraints *) val pr_polymorphic : bool -> std_ppcmds -val pr_univ_cstr : Univ.constraints -> std_ppcmds val pr_universe_ctx : Univ.universe_context -> std_ppcmds (** Printing global references using names as short as possible *) diff --git a/tactics/inv.ml b/tactics/inv.ml index 5becb1ed3a..5502356fbf 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -478,7 +478,7 @@ let wrap_inv_error id = function (e, info) -> match e with Proofview.tclENV >>= fun env -> tclZEROMSG ( (strbrk "Inversion would require case analysis on sort " ++ - pr_sort k ++ + pr_sort Evd.empty k ++ strbrk " which is not allowed for inductive definition " ++ pr_inductive env (fst i) ++ str ".")) | e -> Proofview.tclZERO ~info e diff --git a/test-suite/bugs/closed/3392.v b/test-suite/bugs/closed/3392.v index 43acb7bb48..29ee148733 100644 --- a/test-suite/bugs/closed/3392.v +++ b/test-suite/bugs/closed/3392.v @@ -25,7 +25,7 @@ Proof. refine (isequiv_adjointify (functor_forall f g) (functor_forall (f^-1) (fun (x:A) (y:Q (f^-1 x)) => @eisretr _ _ f _ x # (g (f^-1 x))^-1 y - )) _ _); + )) _ _); intros h. - abstract ( apply path_forall; intros b; unfold functor_forall; diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index f0f366c483..22ea09c53f 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -62,7 +62,8 @@ let process_vernac_interp_error exn = match fst exn with | Univ.UniverseInconsistency i -> let msg = if !Constrextern.print_universes then - str "." ++ spc() ++ Univ.explain_universe_inconsistency i + str "." ++ spc() ++ + Univ.explain_universe_inconsistency Universes.pr_with_global_universes i else mt() in wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".") diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index f660f50d25..9341f2f70a 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -180,7 +180,7 @@ let rec pr_disjunction pr = function let pr_puniverses f env (c,u) = f env c ++ (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then - str"(*" ++ Univ.Instance.pr u ++ str"*)" + str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" else mt()) let explain_elim_arity env sigma ind sorts c pj okinds = @@ -301,7 +301,7 @@ let rec explain_unification_error env sigma p1 p2 = function | UnifUnivInconsistency p -> if !Constrextern.print_universes then [str "universe inconsistency: " ++ - Univ.explain_universe_inconsistency p] + Univ.explain_universe_inconsistency Universes.pr_with_global_universes p] else [str "universe inconsistency"] | CannotSolveConstraint ((pb,env,t,u),e) -> @@ -659,8 +659,9 @@ let explain_non_linear_unification env sigma m t = strbrk " which would require to abstract twice on " ++ pr_lconstr_env env sigma t ++ str "." -let explain_unsatisfied_constraints env cst = - strbrk "Unsatisfied constraints: " ++ Univ.pr_constraints cst ++ +let explain_unsatisfied_constraints env sigma cst = + strbrk "Unsatisfied constraints: " ++ + Univ.pr_constraints (Evd.pr_evd_level sigma) cst ++ spc () ++ str "(maybe a bugged tactic)." let explain_type_error env sigma err = @@ -699,7 +700,7 @@ let explain_type_error env sigma err = | WrongCaseInfo (ind,ci) -> explain_wrong_case_info env ind ci | UnsatisfiedConstraints cst -> - explain_unsatisfied_constraints env cst + explain_unsatisfied_constraints env sigma cst let pr_position (cl,pos) = let clpos = match cl with @@ -860,7 +861,7 @@ let explain_not_match_error = function str"polymorphic universe instances do not match" | IncompatibleUniverses incon -> str"the universe constraints are inconsistent: " ++ - Univ.explain_universe_inconsistency incon + Univ.explain_universe_inconsistency Universes.pr_with_global_universes incon | IncompatiblePolymorphism (env, t1, t2) -> str "conversion of polymorphic values generates additional constraints: " ++ quote (Printer.safe_pr_lconstr_env env Evd.empty t1) ++ spc () ++ @@ -868,7 +869,7 @@ let explain_not_match_error = function quote (Printer.safe_pr_lconstr_env env Evd.empty t2) | IncompatibleConstraints cst -> str " the expected (polymorphic) constraints do not imply " ++ - quote (Univ.pr_constraints cst) + quote (Univ.pr_constraints (Evd.pr_evd_level Evd.empty) cst) let explain_signature_mismatch l spec why = str "Signature components for label " ++ str (Label.to_string l) ++ @@ -1112,7 +1113,7 @@ let error_large_non_prop_inductive_not_in_type () = let error_not_allowed_case_analysis isrec kind i = str (if isrec then "Induction" else "Case analysis") ++ - strbrk " on sort " ++ pr_sort kind ++ + strbrk " on sort " ++ pr_sort Evd.empty kind ++ strbrk " is not allowed for inductive definition " ++ pr_inductive (Global.env()) (fst i) ++ str "." diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2a2a82770b..fb12edfbc2 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -78,7 +78,7 @@ let show_universes () = let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in let cstrs = Univ.merge_constraints (Univ.ContextSet.constraints ctx) Univ.empty_universes in msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma)); - msg_notice (str"Normalized constraints: " ++ Univ.pr_universes cstrs) + msg_notice (str"Normalized constraints: " ++ Univ.pr_universes (Evd.pr_evd_level sigma) cstrs) let show_prooftree () = (* Spiwack: proof tree is currently not working *) @@ -1604,7 +1604,7 @@ let vernac_print = function | PrintUniverses (b, None) -> let univ = Global.universes () in let univ = if b then Univ.sort_universes univ else univ in - msg_notice (Univ.pr_universes univ) + msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ) | PrintUniverses (b, Some s) -> dump_universes b s | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) -- cgit v1.2.3 From 9d8347abc07dec1edd804b2fa39db40088b5cf3d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 17 Jan 2015 20:42:40 +0530 Subject: Back to 4 expected universes. --- test-suite/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-suite/Makefile b/test-suite/Makefile index 4a3a287c08..055485d0bb 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -387,7 +387,7 @@ misc/deps-order.log: } > "$@" # Sort universes for the whole standard library -EXPECTED_UNIVERSES := 3 +EXPECTED_UNIVERSES := 4 universes: misc/universes.log misc/universes.log: misc/universes/all_stdlib.v @echo "TEST misc/universes" -- cgit v1.2.3 From 5e5d51762df0e34769225e8c59c77b97b1212c29 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 18 Jan 2015 00:07:32 +0530 Subject: There was one more universe needed due to the use of now non-universe-polymorphic ID, fixing the script results in 3 universes for the stdlib again. --- test-suite/Makefile | 2 +- theories/Vectors/VectorSpec.v | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/test-suite/Makefile b/test-suite/Makefile index 055485d0bb..4a3a287c08 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -387,7 +387,7 @@ misc/deps-order.log: } > "$@" # Sort universes for the whole standard library -EXPECTED_UNIVERSES := 4 +EXPECTED_UNIVERSES := 3 universes: misc/universes.log misc/universes.log: misc/universes/all_stdlib.v @echo "TEST misc/universes" diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 3e8c1175ff..7f4228dd62 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -62,12 +62,12 @@ Proof. refine (@Fin.rectS _ _ _); lazy beta; [ intros n v | intros n p H v ]. revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t. revert p H. - refine (match v as v' in t _ m return match m as m' return t A m' -> Type with + refine (match v as v' in t _ m return match m as m' return t A m' -> Prop with |S (S n) => fun v => forall p : Fin.t (S n), (forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) -> (shiftrepeat v) [@Fin.L_R 1 (Fin.FS p)] = v [@Fin.FS p] - |_ => fun _ => @ID end v' with - |[] => @id |h :: t => _ end). destruct n0. exact @id. now simpl. + |_ => fun _ => True end v' with + |[] => I |h :: t => _ end). destruct n0. exact I. now simpl. Qed. Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v. -- cgit v1.2.3