Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 662 insertions, 0 deletions

diff --git a/interp/symbols.ml b/interp/symbols.ml
new file mode 100644
index 00000000..ed151d8e
--- /dev/null
+++ b/interp/symbols.ml
@@ -0,0 +1,662 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: symbols.ml,v 1.31.2.1 2004/07/16 19:30:23 herbelin Exp $ *)
+
+(*i*)
+open Util
+open Pp
+open Bignat
+open Names
+open Nametab
+open Libnames
+open Summary
+open Rawterm
+open Topconstr
+open Ppextend
+(*i*)
+
+(*s A scope is a set of notations; it includes
+
+  - a set of ML interpreters/parsers for positive (e.g. 0, 1, 15, ...) and
+    negative numbers (e.g. -0, -2, -13, ...). These interpreters may
+    fail if a number has no interpretation in the scope (e.g. there is
+    no interpretation for negative numbers in [nat]); interpreters both for
+    terms and patterns can be set; these interpreters are in permanent table
+    [numeral_interpreter_tab]
+  - a set of ML printers for expressions denoting numbers parsable in 
+    this scope (permanently declared in [Esyntax.primitive_printer_tab])
+  - a set of interpretations for infix (more generally distfix) notations
+  - an optional pair of delimiters which, when occurring in a syntactic
+    expression, set this scope to be the current scope
+*)
+
+(**********************************************************************)
+(* Scope of symbols *)
+
+type level = precedence * tolerability list
+type delimiters = string
+
+type scope = {
+  notations: (interpretation * (dir_path * string) * bool) Stringmap.t;
+  delimiters: delimiters option
+}
+
+(* Uninterpreted notation map: notation -> level * dir_path *)
+let notation_level_map = ref Stringmap.empty
+
+(* Scopes table: scope_name -> symbol_interpretation *)
+let scope_map = ref Stringmap.empty
+
+let empty_scope = {
+  notations = Stringmap.empty;
+  delimiters = None
+}
+
+let default_scope = "" (* empty name, not available from outside *)
+let type_scope = "type_scope" (* special scope used for interpreting types *)
+
+let init_scope_map () =
+  scope_map := Stringmap.add default_scope empty_scope !scope_map;
+  scope_map := Stringmap.add type_scope empty_scope !scope_map
+
+(**********************************************************************)
+(* Operations on scopes *)
+
+let declare_scope scope =
+  try let _ = Stringmap.find scope !scope_map in ()
+  with Not_found ->
+(*    Options.if_verbose message ("Creating scope "^scope);*)
+    scope_map := Stringmap.add scope empty_scope !scope_map
+
+let find_scope scope =
+  try Stringmap.find scope !scope_map
+  with Not_found -> error ("Scope "^scope^" is not declared")
+
+let check_scope sc = let _ = find_scope sc in ()
+
+(**********************************************************************)
+(* The global stack of scopes                                         *)
+
+type scope_elem = Scope of scope_name | SingleNotation of string
+type scopes = scope_elem list
+
+let scope_stack = ref []
+
+let current_scopes () = !scope_stack
+
+(* TODO: push nat_scope, z_scope, ... in scopes summary *)
+
+(* Exportation of scopes *)
+let cache_scope (_,(local,op,sc)) =
+  (match sc with Scope sc -> check_scope sc | _ -> ());
+  scope_stack := if op then sc :: !scope_stack else list_except sc !scope_stack
+
+let subst_scope (_,subst,sc) = sc
+
+open Libobject
+
+let classify_scope (_,(local,_,_ as o)) =
+  if local then Dispose else Substitute o
+
+let export_scope (local,_,_ as x) = if local then None else Some x
+
+let (inScope,outScope) = 
+  declare_object {(default_object "SCOPE") with
+      cache_function = cache_scope;
+      open_function = (fun i o -> if i=1 then cache_scope o);
+      subst_function = subst_scope;
+      classify_function = classify_scope;
+      export_function = export_scope }
+
+let open_close_scope (local,opening,sc) =
+  Lib.add_anonymous_leaf (inScope (local,opening,Scope sc))
+
+let empty_scope_stack = []
+
+let push_scope sc scopes = Scope sc :: scopes
+
+(**********************************************************************)
+(* Delimiters *)
+
+let delimiters_map = ref Stringmap.empty
+
+let declare_delimiters scope key =
+  let sc = find_scope scope in
+  if sc.delimiters <> None && Options.is_verbose () then begin
+    let old = out_some sc.delimiters in
+    Options.if_verbose 
+      warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
+  end;
+  let sc = { sc with delimiters = Some key } in
+  scope_map := Stringmap.add scope sc !scope_map;
+  if Stringmap.mem key !delimiters_map then begin
+    let oldsc = Stringmap.find key !delimiters_map in
+    Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
+  end;
+  delimiters_map := Stringmap.add key scope !delimiters_map
+
+let find_delimiters_scope loc key = 
+  try Stringmap.find key !delimiters_map
+  with Not_found -> 
+    user_err_loc 
+    (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
+
+(* Uninterpretation tables *)
+
+type interp_rule =
+  | NotationRule of scope_name option * notation
+  | SynDefRule of kernel_name
+
+(* We define keys for rawterm and aconstr to split the syntax entries
+   according to the key of the pattern (adapted from Chet Murthy by HH) *)
+
+type key =
+  | RefKey of global_reference
+  | Oth
+
+(* Scopes table : interpretation -> scope_name *)
+let notations_key_table = ref Gmapl.empty
+let numeral_key_table = Hashtbl.create 7
+
+let rawconstr_key = function
+  | RApp (_,RRef (_,ref),_) -> RefKey ref
+  | RRef (_,ref) -> RefKey ref
+  | _ -> Oth
+
+let cases_pattern_key = function
+  | PatCstr (_,ref,_,_) -> RefKey (ConstructRef ref)
+  | _ -> Oth
+
+let aconstr_key = function
+  | AApp (ARef ref,args) -> RefKey ref, Some (List.length args)
+  | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey ref, Some (List.length args)
+  | ARef ref -> RefKey ref, Some 0
+  | _ -> Oth, None
+
+let pattern_key = function
+  | PatCstr (_,cstr,_,_) -> RefKey (ConstructRef cstr)
+  | _ -> Oth
+
+(**********************************************************************)
+(* Interpreting numbers (not in summary because functional objects)   *)
+
+type num_interpreter =
+    (loc -> bigint -> rawconstr)
+    * (loc -> bigint -> name -> cases_pattern) option
+
+type num_uninterpreter =
+    rawconstr list * (rawconstr -> bigint option)
+    * (cases_pattern -> bigint option) option
+
+type required_module = global_reference * string list 
+
+let numeral_interpreter_tab =
+  (Hashtbl.create 7 : (scope_name,required_module*num_interpreter) Hashtbl.t)
+
+let declare_numeral_interpreter sc dir interp (patl,uninterp,uninterpc) =
+  declare_scope sc;
+  Hashtbl.add numeral_interpreter_tab sc (dir,interp);
+  List.iter
+    (fun pat -> Hashtbl.add numeral_key_table (rawconstr_key pat)
+      (sc,uninterp,uninterpc))
+    patl
+
+let check_required_module loc sc (ref,d) =
+  let d' = List.map id_of_string d in
+  let dir = make_dirpath (List.rev d') in
+  try let _ = sp_of_global ref in ()
+  with Not_found ->
+    user_err_loc (loc,"numeral_interpreter",
+    str ("Cannot interpret numbers in "^sc^" without requiring first module "
+    ^(list_last d)))
+
+let lookup_numeral_interpreter loc = function
+  | Scope sc ->
+      let (dir,interpreter) = Hashtbl.find numeral_interpreter_tab sc in
+      check_required_module loc sc dir;
+      interpreter
+  | SingleNotation _ -> raise Not_found
+
+(* Look if some notation or numeral printer in [scope] can be used in
+   the scope stack [scopes], and if yes, using delimiters or not *)
+
+let find_with_delimiters = function
+  | None -> None
+  | Some scope ->
+      match (Stringmap.find scope !scope_map).delimiters with
+	| Some key -> Some (Some scope, Some key)
+	| None -> None
+
+let rec find_without_delimiters find (ntn_scope,ntn) = function
+  | Scope scope :: scopes -> 
+      (* Is the expected ntn/numpr attached to the most recently open scope? *)
+      if Some scope = ntn_scope then
+	Some (None,None)
+      else
+	(* If the most recently open scope has a notation/numeral printer
+    	   but not the expected one then we need delimiters *)
+	if find scope then
+	  find_with_delimiters ntn_scope
+	else
+	  find_without_delimiters find (ntn_scope,ntn) scopes
+  | SingleNotation ntn' :: scopes ->
+      if ntn_scope = None & ntn = Some ntn' then 
+	Some (None,None)
+      else
+	find_without_delimiters find (ntn_scope,ntn) scopes
+  | [] ->
+      (* Can we switch to [scope]? Yes if it has defined delimiters *)
+      find_with_delimiters ntn_scope
+
+(* Uninterpreted notation levels *)
+
+let declare_notation_level ntn level =
+  if not !Options.v7 & Stringmap.mem ntn !notation_level_map then
+    error ("Notation "^ntn^" is already assigned a level");
+  notation_level_map := Stringmap.add ntn level !notation_level_map
+
+let level_of_notation ntn =
+  Stringmap.find ntn !notation_level_map
+
+(* The mapping between notations and their interpretation *)
+
+let declare_notation_interpretation ntn scopt pat df pp8only =
+  let scope = match scopt with Some s -> s | None -> default_scope in
+  let sc = find_scope scope in
+  if Stringmap.mem ntn sc.notations && Options.is_verbose () then
+    warning ("Notation "^ntn^" is already used"^
+    (if scopt = None then "" else " in scope "^scope));
+  let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in
+  scope_map := Stringmap.add scope sc !scope_map;
+  if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
+
+let declare_uninterpretation rule (metas,c as pat) =
+  let (key,n) = aconstr_key c in
+  notations_key_table := Gmapl.add key (rule,pat,n) !notations_key_table
+
+let rec find_interpretation f = function
+  | sce :: scopes ->
+      let scope = match sce with
+	| Scope s -> s 
+	| SingleNotation _ -> default_scope in
+      (try f scope
+      with Not_found -> find_interpretation f scopes)
+  | [] -> raise Not_found
+
+let rec interp_notation loc ntn scopes =
+  let f sc =
+    let scope = find_scope sc in
+    let (pat,df,pp8only) = Stringmap.find ntn scope.notations in
+    if pp8only then raise Not_found;
+    pat,(df,if sc = default_scope then None else Some sc) in
+  try find_interpretation f (List.fold_right push_scope scopes !scope_stack)
+  with Not_found -> 
+    user_err_loc
+      (loc,"",str ("Unknown interpretation for notation \""^ntn^"\""))
+
+let uninterp_notations c =
+  Gmapl.find (rawconstr_key c) !notations_key_table
+
+let uninterp_cases_pattern_notations c =
+  Gmapl.find (cases_pattern_key c) !notations_key_table
+
+let availability_of_notation (ntn_scope,ntn) scopes =
+  let f scope =
+    Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
+  find_without_delimiters f (ntn_scope,Some ntn) scopes
+
+let rec interp_numeral_gen loc f n = function
+  | scope :: scopes ->
+      (try f (lookup_numeral_interpreter loc scope)
+       with Not_found -> interp_numeral_gen loc f n scopes)
+  | [] ->
+      user_err_loc (loc,"interp_numeral",
+      str "No interpretation for numeral " ++ pr_bigint n)
+
+let interp_numeral loc n scopes =
+  interp_numeral_gen loc (fun x -> fst x loc n) n
+    (List.fold_right push_scope scopes !scope_stack)
+
+let interp_numeral_as_pattern loc n name scopes =
+  let f x = match snd x with
+    | None -> raise Not_found
+    | Some g -> g loc n name in
+  interp_numeral_gen loc f n (List.fold_right push_scope scopes !scope_stack)
+
+let uninterp_numeral c =
+  try 
+    let (sc,numpr,_) = Hashtbl.find numeral_key_table (rawconstr_key c) in
+    match numpr c with
+      | None -> raise No_match
+      | Some n -> (sc,n)
+  with Not_found -> raise No_match
+
+let uninterp_cases_numeral c =
+  try 
+    match Hashtbl.find numeral_key_table (pattern_key c) with
+      | (_,_,None) -> raise No_match
+      | (sc,_,Some numpr) ->
+	  match numpr c with
+	    | None -> raise No_match
+	    | Some n -> (sc,n)
+  with Not_found -> raise No_match
+
+let availability_of_numeral printer_scope scopes =
+  let f scope = Hashtbl.mem numeral_interpreter_tab scope in
+  option_app snd (find_without_delimiters f (Some printer_scope,None) scopes)
+
+(* Miscellaneous *)
+
+let exists_notation_in_scope scopt ntn r =
+  let scope = match scopt with Some s -> s | None -> default_scope in
+  try
+    let sc = Stringmap.find scope !scope_map in
+    let (r',_,pp8only) = Stringmap.find ntn sc.notations in
+    r' = r, pp8only
+  with Not_found -> false, false
+
+(* Special scopes associated to arguments of a global reference *)
+
+let arguments_scope = ref Refmap.empty
+
+let cache_arguments_scope (_,(r,scl)) =
+  List.iter (option_iter check_scope) scl;
+  arguments_scope := Refmap.add r scl !arguments_scope
+
+let subst_arguments_scope (_,subst,(r,scl)) = (subst_global subst r,scl)
+
+let (inArgumentsScope,outArgumentsScope) = 
+  declare_object {(default_object "ARGUMENTS-SCOPE") with
+      cache_function = cache_arguments_scope;
+      load_function = (fun _ o -> cache_arguments_scope o);
+      subst_function = subst_arguments_scope;
+      classify_function = (fun (_,o) -> Substitute o);
+      export_function = (fun x -> Some x) }
+
+let declare_arguments_scope r scl =
+  Lib.add_anonymous_leaf (inArgumentsScope (r,scl))
+
+let find_arguments_scope r =
+  try Refmap.find r !arguments_scope
+  with Not_found -> []
+
+(**********************************************************************)
+(* Mapping classes to scopes *)
+
+open Classops
+
+let class_scope_map = ref (Gmap.empty : (cl_typ,scope_name) Gmap.t)
+
+let _ = Gmap.add CL_SORT "type_scope" Gmap.empty
+
+let declare_class_scope sc cl =
+  class_scope_map := Gmap.add cl sc !class_scope_map
+
+let find_class_scope cl =
+  Gmap.find cl !class_scope_map
+
+open Term
+
+let find_class t =
+  let t, _ = decompose_app (Reductionops.whd_betaiotazeta t) in
+  match kind_of_term t with
+    | Var id -> CL_SECVAR id
+    | Const sp -> CL_CONST sp
+    | Ind ind_sp -> CL_IND ind_sp
+    | Prod (_,_,_) -> CL_FUN
+    | Sort _ -> CL_SORT
+    |  _ -> raise Not_found
+
+let rec compute_arguments_scope t =
+  match kind_of_term (Reductionops.whd_betaiotazeta t) with
+    | Prod (_,t,u) ->
+	let sc =
+	  try Some (find_class_scope (find_class t)) with Not_found -> None in
+	sc :: compute_arguments_scope u
+    | _ -> []
+
+let declare_ref_arguments_scope ref =
+  let t = Global.type_of_global ref in
+  declare_arguments_scope ref (compute_arguments_scope t)
+
+(********************************)
+(* Encoding notations as string *)
+
+type symbol =
+  | Terminal of string
+  | NonTerminal of identifier
+  | SProdList of identifier * symbol list
+  | Break of int
+
+let rec string_of_symbol = function
+  | NonTerminal _ -> ["_"]
+  | Terminal s -> [s]
+  | SProdList (_,l) -> 
+     let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"]
+  | Break _ -> []
+
+let make_notation_key symbols =
+  String.concat " " (List.flatten (List.map string_of_symbol symbols))
+
+let decompose_notation_key s =
+  let len = String.length s in
+  let rec decomp_ntn dirs n =
+    if n>=len then dirs else
+    let pos =
+      try
+	String.index_from s n ' ' 
+      with Not_found -> len
+    in
+    let tok =
+      match String.sub s n (pos-n) with
+      | "_" -> NonTerminal (id_of_string "_")
+      | s -> Terminal s in
+    decomp_ntn (tok::dirs) (pos+1)	  
+  in
+    decomp_ntn [] 0
+
+(************)
+(* Printing *)
+
+let pr_delimiters_info = function
+  | None -> str "No delimiting key"
+  | Some key -> str "Delimiting key is " ++ str key
+
+let classes_of_scope sc =
+  Gmap.fold (fun cl sc' l -> if sc = sc' then cl::l else l) !class_scope_map []
+
+let pr_scope_classes sc =
+  let l = classes_of_scope sc in
+  if l = [] then mt()
+  else 
+    hov 0 (str ("Bound to class"^(if List.tl l=[] then "" else "es")) ++
+      spc() ++ prlist_with_sep spc pr_class l) ++ fnl()
+
+let rec rawconstr_of_aconstr () x =
+  rawconstr_of_aconstr_with_binders dummy_loc (fun id () -> (id,())) 
+    rawconstr_of_aconstr () x
+
+let pr_notation_info prraw ntn c =
+  str "\"" ++ str ntn ++ str "\" := " ++ prraw (rawconstr_of_aconstr () c)
+
+let pr_named_scope prraw scope sc =
+ (if scope = default_scope then
+   match Stringmap.fold (fun _ _ x -> x+1) sc.notations 0 with
+     | 0 -> str "No lonely notation"
+     | n -> str "Lonely notation" ++ (if n=1 then mt() else str"s")
+  else 
+    str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
+  ++ fnl ()
+  ++ pr_scope_classes scope
+  ++ Stringmap.fold
+       (fun ntn ((_,r),(_,df),_) strm ->
+	 pr_notation_info prraw df r ++ fnl () ++ strm)
+       sc.notations (mt ())
+
+let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
+
+let pr_scopes prraw =
+ Stringmap.fold 
+   (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
+   !scope_map (mt ())
+
+let rec find_default ntn = function
+  | Scope scope::_ when Stringmap.mem ntn (find_scope scope).notations ->
+      Some scope
+  | SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope
+  | _::scopes -> find_default ntn scopes
+  | [] -> None
+
+let factorize_entries = function
+  | [] -> []
+  | (ntn,c)::l ->
+      let (ntn,l_of_ntn,rest) =
+	List.fold_left
+          (fun (a',l,rest) (a,c) ->
+	    if a = a' then (a',c::l,rest) else (a,[c],(a',l)::rest))
+	  (ntn,[c],[]) l in
+      (ntn,l_of_ntn)::rest
+
+let is_ident s = (* Poor analysis *)
+  String.length s <> 0 & is_letter s.[0]
+
+let browse_notation ntn map =
+  let find =
+    if String.contains ntn ' ' then (=) ntn
+    else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
+  let l =
+    Stringmap.fold 
+      (fun scope_name sc ->
+	Stringmap.fold (fun ntn ((_,r),df,_) l ->
+	  if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
+      map [] in
+  let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in
+  factorize_entries l
+
+let locate_notation prraw ntn =
+  let ntns = browse_notation ntn !scope_map in
+  if ntns = [] then
+    str "Unknown notation"
+  else
+    t (str "Notation            " ++
+    tab () ++ str "Scope     " ++ tab () ++ fnl () ++ 
+    prlist (fun (ntn,l) ->
+      let scope = find_default ntn !scope_stack in
+      prlist 
+	(fun (sc,r,(_,df)) ->
+	  hov 0 (
+	    pr_notation_info prraw df r ++ tbrk (1,2) ++
+	    (if sc = default_scope then mt () else (str ": " ++ str sc)) ++ 
+	    tbrk (1,2) ++
+	    (if Some sc = scope then str "(default interpretation)" else mt ())
+	    ++ fnl ()))
+	l) ntns)
+
+let collect_notation_in_scope scope sc known =
+  assert (scope <> default_scope);
+  Stringmap.fold
+    (fun ntn ((_,r),(_,df),_) (l,known as acc) ->
+      if List.mem ntn known then acc else ((df,r)::l,ntn::known))
+    sc.notations ([],known)
+
+let collect_notations stack =
+  fst (List.fold_left
+    (fun (all,knownntn as acc) -> function
+      | Scope scope ->
+	  if List.mem_assoc scope all then acc
+	  else
+	    let (l,knownntn) =
+	      collect_notation_in_scope scope (find_scope scope) knownntn in
+	    ((scope,l)::all,knownntn)
+      | SingleNotation ntn ->
+	  if List.mem ntn knownntn then (all,knownntn)
+	  else
+	    let ((_,r),(_,df),_) =
+	      Stringmap.find ntn (find_scope default_scope).notations in
+	    let all' = match all with
+	      | (s,lonelyntn)::rest when s = default_scope ->
+		  (s,(df,r)::lonelyntn)::rest
+	      | _ -> 
+		  (default_scope,[df,r])::all in
+	    (all',ntn::knownntn))
+    ([],[]) stack)
+
+let pr_visible_in_scope prraw (scope,ntns) =
+  let strm =
+    List.fold_right
+      (fun (df,r) strm -> pr_notation_info prraw df r ++ fnl () ++ strm)
+      ntns (mt ()) in
+  (if scope = default_scope then
+     str "Lonely notation" ++ (if List.length ntns <> 1 then str "s" else mt())
+   else 
+     str "Visible in scope " ++ str scope)
+  ++ fnl () ++ strm
+
+let pr_scope_stack prraw stack = 
+  List.fold_left
+    (fun strm scntns -> strm ++ pr_visible_in_scope prraw scntns ++ fnl ())
+    (mt ()) (collect_notations stack)
+
+let pr_visibility prraw = function
+  | Some scope -> pr_scope_stack prraw (push_scope scope !scope_stack)
+  | None -> pr_scope_stack prraw !scope_stack
+
+(**********************************************************************)
+(* Mapping notations to concrete syntax *)
+
+type unparsing_rule = unparsing list * precedence
+
+(* Concrete syntax for symbolic-extension table *)
+let printing_rules = 
+  ref (Stringmap.empty : unparsing_rule Stringmap.t)
+
+let declare_notation_printing_rule ntn unpl =
+  printing_rules := Stringmap.add ntn unpl !printing_rules
+
+let find_notation_printing_rule ntn =
+  try Stringmap.find ntn !printing_rules
+  with Not_found -> anomaly ("No printing rule found for "^ntn)
+
+(**********************************************************************)
+(* Synchronisation with reset *)
+
+let freeze () =
+ (!scope_map, !notation_level_map, !scope_stack, !arguments_scope,
+  !delimiters_map, !notations_key_table, !printing_rules,
+  !class_scope_map)
+
+let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
+  scope_map := scm;
+  notation_level_map := nlm;
+  scope_stack := scs;
+  delimiters_map := dlm;
+  arguments_scope := asc;
+  notations_key_table := fkm;
+  printing_rules := pprules;
+  class_scope_map := clsc
+
+let init () =
+  init_scope_map ();
+(*
+  scope_stack := Stringmap.empty
+  arguments_scope := Refmap.empty
+*)
+  notation_level_map := Stringmap.empty;
+  delimiters_map := Stringmap.empty;
+  notations_key_table := Gmapl.empty;
+  printing_rules := Stringmap.empty;
+  class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
+
+let _ = 
+  declare_summary "symbols"
+    { freeze_function = freeze;
+      unfreeze_function = unfreeze;
+      init_function = init;
+      survive_module = false;
+      survive_section = false }