diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /interp/notation.ml | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'interp/notation.ml')
-rw-r--r-- | interp/notation.ml | 706 |
1 files changed, 706 insertions, 0 deletions
diff --git a/interp/notation.ml b/interp/notation.ml new file mode 100644 index 00000000..cb996dfe --- /dev/null +++ b/interp/notation.ml @@ -0,0 +1,706 @@ +(************************************************************************) +(* 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: notation.ml 7984 2006-02-04 20:14:55Z herbelin $ *) + +(*i*) +open Util +open Pp +open Bigint +open Names +open Term +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 + - 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 notation_location = dir_path * string + +type scope = { + notations: (string, interpretation * notation_location) Gmap.t; + delimiters: delimiters option +} + +(* Uninterpreted notation map: notation -> level * dir_path *) +let notation_level_map = ref Gmap.empty + +(* Scopes table: scope_name -> symbol_interpretation *) +let scope_map = ref Gmap.empty + +let empty_scope = { + notations = Gmap.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 := Gmap.add default_scope empty_scope !scope_map; + scope_map := Gmap.add type_scope empty_scope !scope_map + +(**********************************************************************) +(* Operations on scopes *) + +let declare_scope scope = + try let _ = Gmap.find scope !scope_map in () + with Not_found -> +(* Options.if_verbose message ("Creating scope "^scope);*) + scope_map := Gmap.add scope empty_scope !scope_map + +let find_scope scope = + try Gmap.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 open_scope i (_,(local,op,sc)) = + if i=1 then begin + (match sc with Scope sc -> check_scope sc | _ -> ()); + scope_stack := if op then sc :: !scope_stack else list_except sc !scope_stack + end + +let cache_scope o = + open_scope 1 o + +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 = open_scope; + 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 + +let push_scopes = List.fold_right push_scope + +(**********************************************************************) +(* Delimiters *) + +let delimiters_map = ref Gmap.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 := Gmap.add scope sc !scope_map; + if Gmap.mem key !delimiters_map then begin + let oldsc = Gmap.find key !delimiters_map in + Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc) + end; + delimiters_map := Gmap.add key scope !delimiters_map + +let find_delimiters_scope loc key = + try Gmap.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 prim_token_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 required_module = section_path * string list + +type 'a prim_token_interpreter = + loc -> 'a -> rawconstr + +type cases_pattern_status = bool (* true = use prim token in patterns *) + +type 'a prim_token_uninterpreter = + rawconstr list * (rawconstr -> 'a option) * cases_pattern_status + +type internal_prim_token_interpreter = + loc -> prim_token -> required_module * (unit -> rawconstr) + +let prim_token_interpreter_tab = + (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t) + +let add_prim_token_interpreter sc interp = + try + let cont = Hashtbl.find prim_token_interpreter_tab sc in + Hashtbl.replace prim_token_interpreter_tab sc (interp cont) + with Not_found -> + let cont = (fun _loc _p -> raise Not_found) in + Hashtbl.add prim_token_interpreter_tab sc (interp cont) + +let declare_prim_token_interpreter sc interp (patl,uninterp,b) = + declare_scope sc; + add_prim_token_interpreter sc interp; + List.iter (fun pat -> + Hashtbl.add prim_token_key_table (rawconstr_key pat) (sc,uninterp,b)) + patl + +let mkNumeral n = Numeral n +let mkString s = String s + +let delay dir int loc x = (dir, (fun () -> int loc x)) + +let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = + declare_prim_token_interpreter sc + (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p) + (patl, (fun r -> option_app mkNumeral (uninterp r)), inpat) + +let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = + declare_prim_token_interpreter sc + (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p) + (patl, (fun r -> option_app mkString (uninterp r)), inpat) + +let check_required_module loc sc (sp,d) = + try let _ = Nametab.absolute_reference sp in () + with Not_found -> + user_err_loc (loc,"prim_token_interpreter", + str ("Cannot interpret in "^sc^" without requiring first module " + ^(list_last d))) + +(* 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 (Gmap.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 Gmap.mem ntn !notation_level_map then + error ("Notation "^ntn^" is already assigned a level"); + notation_level_map := Gmap.add ntn level !notation_level_map + +let level_of_notation ntn = + Gmap.find ntn !notation_level_map + +(* The mapping between notations and their interpretation *) + +let declare_notation_interpretation ntn scopt pat df = + let scope = match scopt with Some s -> s | None -> default_scope in + let sc = find_scope scope in + if Gmap.mem ntn sc.notations && Options.is_verbose () then + warning ("Notation "^ntn^" was already used"^ + (if scopt = None then "" else " in scope "^scope)); + let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in + scope_map := Gmap.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 find = function + | [] -> raise Not_found + | sce :: scopes -> + let sc,sco = match sce with + | Scope sc -> sc, Some sc + | SingleNotation _ -> default_scope, None in + try + let (pat,df) = find sc in + pat,(df,sco) + with Not_found -> + find_interpretation find scopes + +let find_notation ntn sc = + Gmap.find ntn (find_scope sc).notations + +let notation_of_prim_token = function + | Numeral n when is_pos_or_zero n -> to_string n + | Numeral n -> "- "^(to_string (neg n)) + | String _ -> raise Not_found + +let find_prim_token g loc p sc = + (* Try for a user-defined numerical notation *) + try + let (_,c),df = find_notation (notation_of_prim_token p) sc in + g (rawconstr_of_aconstr loc c),df + with Not_found -> + (* Try for a primitive numerical notation *) + let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in + check_required_module loc sc spdir; + g (interp ()), (dirpath (fst spdir),"") + +let interp_prim_token_gen g loc p scopes = + let all_scopes = push_scopes scopes !scope_stack in + try find_interpretation (find_prim_token g loc p) all_scopes + with Not_found -> + user_err_loc (loc,"interp_prim_token", + (match p with + | Numeral n -> str "No interpretation for numeral " ++ pr_bigint n + | String s -> str "No interpretation for string " ++ qs s)) + +let interp_prim_token = + interp_prim_token_gen (fun x -> x) + +let interp_prim_token_cases_pattern loc p name = + interp_prim_token_gen (cases_pattern_of_rawconstr name) loc p + +let rec interp_notation loc ntn scopes = + try find_interpretation (find_notation ntn) (push_scopes 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 = + Gmap.mem ntn (Gmap.find scope !scope_map).notations in + find_without_delimiters f (ntn_scope,Some ntn) scopes + +let uninterp_prim_token c = + try + let (sc,numpr,_) = Hashtbl.find prim_token_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_prim_token_cases_pattern c = + try + let k = cases_pattern_key c in + let (sc,numpr,b) = Hashtbl.find prim_token_key_table k in + if not b then raise No_match; + let na,c = rawconstr_of_closed_cases_pattern c in + match numpr c with + | None -> raise No_match + | Some n -> (na,sc,n) + with Not_found -> raise No_match + +let availability_of_prim_token printer_scope scopes = + let f scope = Hashtbl.mem prim_token_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 = Gmap.find scope !scope_map in + let (r',_) = Gmap.find ntn sc.notations in + r' = r + with Not_found -> false + +(**********************************************************************) +(* 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 + +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 + +(**********************************************************************) +(* Special scopes associated to arguments of a global reference *) + +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 arguments_scope = ref Refmap.empty + +let load_arguments_scope _ (_,(r,scl)) = + List.iter (option_iter check_scope) scl; + arguments_scope := Refmap.add r scl !arguments_scope + +let cache_arguments_scope o = + load_arguments_scope 1 o + +let subst_arguments_scope (_,subst,(r,scl)) = (fst (subst_global subst r),scl) + +let discharge_arguments_scope (r,_) = + match r with + | VarRef _ -> None + | _ -> Some (r,compute_arguments_scope (Global.type_of_global r)) + +let (inArgumentsScope,outArgumentsScope) = + declare_object {(default_object "ARGUMENTS-SCOPE") with + cache_function = cache_arguments_scope; + load_function = load_arguments_scope; + 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 -> [] + +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 pr_notation_info prraw ntn c = + str "\"" ++ str ntn ++ str "\" := " ++ + prraw (rawconstr_of_aconstr dummy_loc c) + +let pr_named_scope prraw scope sc = + (if scope = default_scope then + match Gmap.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 + ++ Gmap.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 = + Gmap.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 Gmap.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 = + Gmap.fold + (fun scope_name sc -> + Gmap.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); + Gmap.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)) = + Gmap.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 (Gmap.empty : (string,unparsing_rule) Gmap.t) + +let declare_notation_printing_rule ntn unpl = + printing_rules := Gmap.add ntn unpl !printing_rules + +let find_notation_printing_rule ntn = + try Gmap.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 := Gmap.empty + arguments_scope := Refmap.empty +*) + notation_level_map := Gmap.empty; + delimiters_map := Gmap.empty; + notations_key_table := Gmapl.empty; + printing_rules := Gmap.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 } |