summaryrefslogtreecommitdiff
path: root/interp/symbols.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /interp/symbols.ml
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'interp/symbols.ml')
-rw-r--r--interp/symbols.ml662
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 }