path: root/interp/symbols.ml

(***********************************************************************)
(*  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)