diff options
Diffstat (limited to 'interp/symbols.ml')
| -rw-r--r-- | interp/symbols.ml | 331 |
1 files changed, 331 insertions, 0 deletions
diff --git a/interp/symbols.ml b/interp/symbols.ml new file mode 100644 index 000000000..c6eff9ab9 --- /dev/null +++ b/interp/symbols.ml @@ -0,0 +1,331 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(*i*) +open Util +open Pp +open Bignat +open Names +open Nametab +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 * precedence list +type delimiters = string * string +type scope = { + notations: (aconstr * level) Stringmap.t; + delimiters: delimiters option +} +type scopes = scope_name list + +(* Scopes table: scope_name -> symbol_interpretation *) +let scope_map = ref Stringmap.empty + +let empty_scope = { + notations = Stringmap.empty; + delimiters = None +} + +let default_scope = "core_scope" + +let _ = Stringmap.add default_scope empty_scope !scope_map + +let scope_stack = ref [default_scope] + +let current_scopes () = !scope_stack + +(* TODO: push nat_scope, z_scope, ... in scopes summary *) + +(**********************************************************************) +(* Interpreting numbers (not in summary because functional objects) *) + +type numeral_interpreter_name = string +type numeral_interpreter = + (loc -> bigint -> rawconstr) + * (loc -> bigint -> name -> cases_pattern) option + +let numeral_interpreter_tab = + (Hashtbl.create 17 : (numeral_interpreter_name,numeral_interpreter)Hashtbl.t) + +let declare_numeral_interpreter sc t = + Hashtbl.add numeral_interpreter_tab sc t + +let lookup_numeral_interpreter s = + try + Hashtbl.find numeral_interpreter_tab s + with Not_found -> + error ("No interpretation for numerals in scope "^s) + +(* For loading without opening *) +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 () + +let declare_delimiters scope dlm = + let sc = find_scope scope in + if sc.delimiters <> None && Options.is_verbose () then + warning ("Overwriting previous delimiters in "^scope); + let sc = { sc with delimiters = Some dlm } in + scope_map := Stringmap.add scope sc !scope_map + +(* The mapping between notations and production *) + +let declare_notation nt scope (c,prec as info) = + let sc = find_scope scope in + if Stringmap.mem nt sc.notations && Options.is_verbose () then + warning ("Notation "^nt^" is already used in scope "^scope); + let sc = { sc with notations = Stringmap.add nt info sc.notations } in + scope_map := Stringmap.add scope sc !scope_map + +let rec find_interpretation f = function + | scope::scopes -> + (try f (find_scope scope) + with Not_found -> find_interpretation f scopes) + | [] -> raise Not_found + +let rec interp_notation ntn scopes = + let f scope = fst (Stringmap.find ntn scope.notations) in + try find_interpretation f scopes + with Not_found -> anomaly ("Unknown interpretation for notation "^ntn) + +let find_notation_with_delimiters scope = + match (Stringmap.find scope !scope_map).delimiters with + | Some dlm -> Some (Some dlm) + | None -> None + +let rec find_notation_without_delimiters ntn_scope ntn = function + | scope::scopes -> + (* Is the expected printer attached to the most recently open scope? *) + if scope = ntn_scope then + Some None + else + (* If the most recently open scope has a printer for this pattern + but not the expected one then we need delimiters *) + if Stringmap.mem ntn (Stringmap.find scope !scope_map).notations then + find_notation_with_delimiters ntn_scope + else + find_notation_without_delimiters ntn_scope ntn scopes + | [] -> + find_notation_with_delimiters ntn_scope + +let find_notation ntn_scope ntn scopes = + match + find_notation_without_delimiters ntn_scope ntn scopes + with + | None -> None + | Some None -> Some (None,scopes) + | Some x -> Some (x,ntn_scope::scopes) + +let exists_notation_in_scope scope prec ntn r = + try Stringmap.find ntn (Stringmap.find scope !scope_map).notations = (r,prec) + with Not_found -> false + +let exists_notation_prec prec nt sc = + try snd (Stringmap.find nt sc.notations) = prec with Not_found -> false + +let exists_notation prec nt = + Stringmap.fold (fun scn sc b -> b or exists_notation_prec prec nt sc) + !scope_map false + +(* We have to print delimiters; look for the more recent defined one *) +(* Do we need to print delimiters? To know it, we look for a numeral *) +(* printer available in the current stack of scopes *) +let find_numeral_with_delimiters scope = + match (Stringmap.find scope !scope_map).delimiters with + | Some dlm -> Some (Some dlm) + | None -> None + +let rec find_numeral_without_delimiters printer_scope = function + | scope :: scopes -> + (* Is the expected printer attached to the most recently open scope? *) + if scope = printer_scope then + Some None + else + (* If the most recently open scope has a printer for numerals + but not the expected one then we need delimiters *) + if not (Hashtbl.mem numeral_interpreter_tab scope) then + find_numeral_without_delimiters printer_scope scopes + else + find_numeral_with_delimiters printer_scope + | [] -> + (* Can we switch to [scope]? Yes if it has defined delimiters *) + find_numeral_with_delimiters printer_scope + +let find_numeral_printer printer_scope scopes = + match + find_numeral_without_delimiters printer_scope scopes + with + | None -> None + | Some None -> Some (None,scopes) + | Some x -> Some (x,printer_scope::scopes) + +(* This is the map associating the scope a numeral printer belongs to *) +(* +let numeral_printer_map = ref (Stringmap.empty : scope_name Stringmap.t) +*) + +let rec interp_numeral loc n = function + | scope :: scopes -> + (try fst (lookup_numeral_interpreter scope) loc n + with Not_found -> interp_numeral loc n scopes) + | [] -> + user_err_loc (loc,"interp_numeral", + str "No interpretation for numeral " ++ pr_bigint n) + +let rec interp_numeral_as_pattern loc n name = function + | scope :: scopes -> + (try + match snd (lookup_numeral_interpreter scope) with + | None -> raise Not_found + | Some g -> g loc n name + with Not_found -> interp_numeral_as_pattern loc n name scopes) + | [] -> + user_err_loc (loc,"interp_numeral_as_pattern", + str "No interpretation for numeral " ++ pr_bigint n) + +(* Exportation of scopes *) +let cache_scope (_,sc) = + check_scope sc; + scope_stack := sc :: !scope_stack + +let subst_scope (_,subst,sc) = sc + +open Libobject + +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 = (fun (_,o) -> Substitute o); + export_function = (fun x -> Some x) } + +let open_scope sc = Lib.add_anonymous_leaf (inScope sc) + + +(* Special scopes associated to arguments of a global reference *) + +open Libnames + +module RefOrdered = + struct + type t = global_reference + let compare = Pervasives.compare + end + +module Refmap = Map.Make(RefOrdered) + +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; + open_function = (fun i o -> if i=1 then 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 -> [] + +(* Printing *) + +let pr_delimiters = function + | None -> str "No delimiters" + | Some (l,r) -> str "Delimiters are " ++ str l ++ str " and " ++ str r + +let pr_notation prraw ntn r = + str ntn ++ str " stands for " ++ prraw r + +let pr_named_scope prraw scope sc = + str "Scope " ++ str scope ++ fnl () + ++ pr_delimiters sc.delimiters ++ fnl () + ++ Stringmap.fold + (fun ntn (r,_) strm -> pr_notation prraw ntn 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 ()) + +(* Synchronisation with reset *) + +let freeze () = (!scope_map, !scope_stack, !arguments_scope) + +let unfreeze (scm,scs,asc) = + scope_map := scm; + scope_stack := scs; + arguments_scope := asc + +let init () = () +(* + scope_map := Strinmap.empty; + scope_stack := Stringmap.empty +*) + +let _ = + declare_summary "symbols" + { freeze_function = freeze; + unfreeze_function = unfreeze; + init_function = init; + survive_section = false } + + +let printing_rules = + ref (Stringmap.empty : (unparsing list * precedence) Stringmap.t) + +let declare_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) |