From e88e0b2140bdd2d194a52bc09f8338b5667d0f92 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 14 Nov 2002 18:37:54 +0000 Subject: Réforme de l'interprétation des termes : - Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/closure.ml | 4 ---- kernel/closure.mli | 4 ---- kernel/modops.ml | 11 +++++++---- kernel/modops.mli | 5 ++++- kernel/names.ml | 5 +++++ kernel/names.mli | 5 +++++ kernel/term.ml | 4 ++-- kernel/term.mli | 4 ++-- 8 files changed, 25 insertions(+), 17 deletions(-) (limited to 'kernel') diff --git a/kernel/closure.ml b/kernel/closure.ml index 078f46b8d6..c3b828a39d 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -52,10 +52,6 @@ let with_stats c = end else Lazy.force c -type evaluable_global_reference = - | EvalVarRef of identifier - | EvalConstRef of constant - type transparent_state = Idpred.t * KNpred.t let all_opaque = (Idpred.empty, KNpred.empty) diff --git a/kernel/closure.mli b/kernel/closure.mli index d3c5e5c59f..4442e49f9f 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -22,10 +22,6 @@ val share : bool ref val with_stats: 'a Lazy.t -> 'a -type evaluable_global_reference = - | EvalVarRef of identifier - | EvalConstRef of kernel_name - (*s Delta implies all consts (both global (= by [kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's. Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of diff --git a/kernel/modops.ml b/kernel/modops.ml index 758bf21596..a75f2d4832 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -10,6 +10,7 @@ (*i*) open Util +open Pp open Names open Univ open Term @@ -51,11 +52,13 @@ let error_no_module_to_end _ = let error_no_modtype_to_end _ = error "No open module type to end" -let error_not_a_modtype s = - error ("\""^s^"\" is not a module type") +let error_not_a_modtype_loc loc s = + user_err_loc (loc,"",str ("\""^s^"\" is not a module type")) -let error_not_a_module s = - error ("\""^s^"\" is not a module") +let error_not_a_module_loc loc s = + user_err_loc (loc,"",str ("\""^s^"\" is not a module")) + +let error_not_a_module s = error_not_a_module_loc dummy_loc s let error_not_a_constant l = error ("\""^(string_of_label l)^"\" is not a constant") diff --git a/kernel/modops.mli b/kernel/modops.mli index 68f8ea38aa..e865159c5b 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -9,6 +9,7 @@ (*i $Id$ i*) (*i*) +open Util open Names open Univ open Environ @@ -80,7 +81,9 @@ val error_no_module_to_end : unit -> 'a val error_no_modtype_to_end : unit -> 'a -val error_not_a_modtype : string -> 'a +val error_not_a_modtype_loc : loc -> string -> 'a + +val error_not_a_module_loc : loc -> string -> 'a val error_not_a_module : string -> 'a diff --git a/kernel/names.ml b/kernel/names.ml index 402e321d06..c9a1aa2ae8 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -260,6 +260,11 @@ let ith_constructor_of_inductive ind i = (ind,i) let inductive_of_constructor (ind,i) = ind let index_of_constructor (ind,i) = i +(* Better to have it here that in closure, since used in grammar.cma *) +type evaluable_global_reference = + | EvalVarRef of identifier + | EvalConstRef of constant + (* Hash-consing of name objects *) module Hname = Hashcons.Make( struct diff --git a/kernel/names.mli b/kernel/names.mli index d9b9ddc9cd..2ecdd602d8 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -157,6 +157,11 @@ val ith_constructor_of_inductive : inductive -> int -> constructor val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int +(* Better to have it here that in Closure, since required in grammar.cma *) +type evaluable_global_reference = + | EvalVarRef of identifier + | EvalConstRef of constant + (* Hash-consing *) val hcons_names : unit -> (kernel_name -> kernel_name) * (dir_path -> dir_path) * diff --git a/kernel/term.ml b/kernel/term.ml index cc6404631b..47bd656aea 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -22,11 +22,11 @@ type existential_key = int (* This defines Cases annotations *) type pattern_source = DefaultPat of int | RegularPat -type case_style = PrintLet | PrintIf | PrintCases +type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle type case_printing = { cnames : identifier array; ind_nargs : int; (* number of real args of the inductive type *) - style : case_style option; + style : case_style; source : pattern_source array } type case_info = { ci_ind : inductive; diff --git a/kernel/term.mli b/kernel/term.mli index 6da9d1f5f4..1867cc4505 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -37,11 +37,11 @@ type existential_key = int (*s Case annotation *) type pattern_source = DefaultPat of int | RegularPat -type case_style = PrintLet | PrintIf | PrintCases +type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle type case_printing = { cnames : identifier array; ind_nargs : int; (* number of real args of the inductive type *) - style : case_style option; + style : case_style; source : pattern_source array } (* the integer is the number of real args, needed for reduction *) type case_info = -- cgit v1.2.3