summaryrefslogtreecommitdiff
path: root/interp/notation.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation.ml')
-rw-r--r--interp/notation.ml192
1 files changed, 106 insertions, 86 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index 6e02c40b..8f19ab85 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: notation.ml 14820 2011-12-18 22:11:32Z herbelin $ *)
-
(*i*)
open Util
open Pp
@@ -17,7 +15,7 @@ open Term
open Nametab
open Libnames
open Summary
-open Rawterm
+open Glob_term
open Topconstr
open Ppextend
(*i*)
@@ -73,7 +71,7 @@ let init_scope_map () =
let declare_scope scope =
try let _ = Gmap.find scope !scope_map in ()
with Not_found ->
-(* Flags.if_verbose message ("Creating scope "^scope);*)
+(* Flags.if_warn message ("Creating scope "^scope);*)
scope_map := Gmap.add scope empty_scope !scope_map
let find_scope scope =
@@ -119,7 +117,7 @@ let discharge_scope (_,(local,_,_ as o)) =
let classify_scope (local,_,_ as o) =
if local then Dispose else Substitute o
-let (inScope,outScope) =
+let inScope : bool * bool * scope_elem -> obj =
declare_object {(default_object "SCOPE") with
cache_function = cache_scope;
open_function = open_scope;
@@ -153,15 +151,15 @@ let declare_delimiters scope key =
| None -> scope_map := Gmap.add scope newsc !scope_map
| Some oldkey when oldkey = key -> ()
| Some oldkey ->
- Flags.if_verbose warning
- ("overwriting previous delimiting key "^oldkey^" in scope "^scope);
+ Flags.if_warn msg_warning
+ (str ("Overwriting previous delimiting key "^oldkey^" in scope "^scope));
scope_map := Gmap.add scope newsc !scope_map
end;
try
let oldscope = Gmap.find key !delimiters_map in
if oldscope = scope then ()
else begin
- Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldscope);
+ Flags.if_warn msg_warning (str ("Hiding binding of key "^key^" to "^oldscope));
delimiters_map := Gmap.add key scope !delimiters_map
end
with Not_found -> delimiters_map := Gmap.add key scope !delimiters_map
@@ -178,7 +176,7 @@ 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
+(* We define keys for glob_constr and aconstr to split the syntax entries
according to the key of the pattern (adapted from Chet Murthy by HH) *)
type key =
@@ -189,30 +187,25 @@ type key =
let notations_key_table = ref Gmapl.empty
let prim_token_key_table = Hashtbl.create 7
-
-let make_gr = function
- | ConstRef con ->
- ConstRef(constant_of_kn(canonical_con con))
- | IndRef (kn,i) ->
- IndRef(mind_of_kn(canonical_mind kn),i)
- | ConstructRef ((kn,i),j )->
- ConstructRef((mind_of_kn(canonical_mind kn),i),j)
- | VarRef id -> VarRef id
-
-let rawconstr_key = function
- | RApp (_,RRef (_,ref),_) -> RefKey (make_gr ref)
- | RRef (_,ref) -> RefKey (make_gr ref)
+let glob_prim_constr_key = function
+ | GApp (_,GRef (_,ref),_) | GRef (_,ref) -> RefKey (canonical_gr ref)
| _ -> Oth
+let glob_constr_keys = function
+ | GApp (_,GRef (_,ref),_) -> [RefKey (canonical_gr ref); Oth]
+ | GRef (_,ref) -> [RefKey (canonical_gr ref)]
+ | _ -> [Oth]
+
let cases_pattern_key = function
- | PatCstr (_,ref,_,_) -> RefKey (make_gr (ConstructRef ref))
+ | PatCstr (_,ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
| _ -> Oth
let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
- | AApp (ARef ref,args) -> RefKey(make_gr ref), Some (List.length args)
+ | AApp (ARef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
| AList (_,_,AApp (ARef ref,args),_,_)
- | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (make_gr ref), Some (List.length args)
- | ARef ref -> RefKey(make_gr ref), None
+ | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args)
+ | ARef ref -> RefKey(canonical_gr ref), None
+ | AApp (_,args) -> Oth, Some (List.length args)
| _ -> Oth, None
(**********************************************************************)
@@ -221,15 +214,15 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
type required_module = full_path * string list
type 'a prim_token_interpreter =
- loc -> 'a -> rawconstr
+ loc -> 'a -> glob_constr
type cases_pattern_status = bool (* true = use prim token in patterns *)
type 'a prim_token_uninterpreter =
- rawconstr list * (rawconstr -> 'a option) * cases_pattern_status
+ glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
type internal_prim_token_interpreter =
- loc -> prim_token -> required_module * (unit -> rawconstr)
+ loc -> prim_token -> required_module * (unit -> glob_constr)
let prim_token_interpreter_tab =
(Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
@@ -246,7 +239,8 @@ 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))
+ Hashtbl.add prim_token_key_table
+ (glob_prim_constr_key pat) (sc,uninterp,b))
patl
let mkNumeral n = Numeral n
@@ -353,7 +347,7 @@ 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
+ g (glob_constr_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
@@ -374,7 +368,7 @@ 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
+ interp_prim_token_gen (cases_pattern_of_glob_constr name) loc p
let rec interp_notation loc ntn local_scopes =
let scopes = make_current_scopes local_scopes in
@@ -383,8 +377,11 @@ let rec interp_notation loc ntn local_scopes =
user_err_loc
(loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))
+let isGApp = function GApp _ -> true | _ -> false
+
let uninterp_notations c =
- Gmapl.find (rawconstr_key c) !notations_key_table
+ list_map_append (fun key -> Gmapl.find key !notations_key_table)
+ (glob_constr_keys c)
let uninterp_cases_pattern_notations c =
Gmapl.find (cases_pattern_key c) !notations_key_table
@@ -396,7 +393,8 @@ let availability_of_notation (ntn_scope,ntn) scopes =
let uninterp_prim_token c =
try
- let (sc,numpr,_) = Hashtbl.find prim_token_key_table (rawconstr_key c) in
+ let (sc,numpr,_) =
+ Hashtbl.find prim_token_key_table (glob_prim_constr_key c) in
match numpr c with
| None -> raise No_match
| Some n -> (sc,n)
@@ -407,7 +405,7 @@ let uninterp_prim_token_cases_pattern c =
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
+ let na,c = glob_constr_of_closed_cases_pattern c in
match numpr c with
| None -> raise No_match
| Some n -> (na,sc,n)
@@ -439,7 +437,8 @@ 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 _ =
+ class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
let declare_class_scope sc cl =
class_scope_map := Gmap.add cl sc !class_scope_map
@@ -447,27 +446,39 @@ let declare_class_scope sc cl =
let find_class_scope cl =
Gmap.find cl !class_scope_map
-let find_class t =
- let t, _ = decompose_app (Reductionops.whd_betaiotazeta Evd.empty 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 find_class_scope_opt = function
+ | None -> None
+ | Some cl -> try Some (find_class_scope cl) with Not_found -> None
+
+let find_class t = fst (find_class_type Evd.empty t)
(**********************************************************************)
(* Special scopes associated to arguments of a global reference *)
-let rec compute_arguments_scope t =
+let rec compute_arguments_classes t =
match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty 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 cl = try Some (find_class t) with Not_found -> None in
+ cl :: compute_arguments_classes u
| _ -> []
+let compute_arguments_scope_full t =
+ let cls = compute_arguments_classes t in
+ let scs = List.map find_class_scope_opt cls in
+ scs, cls
+
+let compute_arguments_scope t = fst (compute_arguments_scope_full t)
+
+(** When merging scope list, we give priority to the first one (computed
+ by substitution), using the second one (user given or earlier automatic)
+ as fallback *)
+
+let rec merge_scope sc1 sc2 = match sc1, sc2 with
+ | [], _ -> sc2
+ | _, [] -> sc1
+ | Some sc :: sc1, _ :: sc2 -> Some sc :: merge_scope sc1 sc2
+ | None :: sc1, sco :: sc2 -> sco :: merge_scope sc1 sc2
+
let arguments_scope = ref Refmap.empty
type arguments_scope_discharge_request =
@@ -475,36 +486,47 @@ type arguments_scope_discharge_request =
| ArgsScopeManual
| ArgsScopeNoDischarge
-let load_arguments_scope _ (_,(_,r,scl)) =
+let load_arguments_scope _ (_,(_,r,scl,cls)) =
List.iter (Option.iter check_scope) scl;
- arguments_scope := Refmap.add r scl !arguments_scope
+ arguments_scope := Refmap.add r (scl,cls) !arguments_scope
let cache_arguments_scope o =
load_arguments_scope 1 o
-let subst_arguments_scope (subst,(req,r,scl)) =
- (ArgsScopeNoDischarge,fst (subst_global subst r),scl)
+let subst_arguments_scope (subst,(req,r,scl,cls)) =
+ let r' = fst (subst_global subst r) in
+ let subst_cl cl =
+ try Option.smartmap (subst_cl_typ subst) cl with Not_found -> None in
+ let cls' = list_smartmap subst_cl cls in
+ let scl' = merge_scope (List.map find_class_scope_opt cls') scl in
+ let scl'' = List.map (Option.map Declaremods.subst_scope) scl' in
+ (ArgsScopeNoDischarge,r',scl'',cls')
-let discharge_arguments_scope (_,(req,r,l)) =
+let discharge_arguments_scope (_,(req,r,l,_)) =
if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None
- else Some (req,Lib.discharge_global r,l)
+ else Some (req,Lib.discharge_global r,l,[])
-let classify_arguments_scope (req,_,_ as obj) =
+let classify_arguments_scope (req,_,_,_ as obj) =
if req = ArgsScopeNoDischarge then Dispose else Substitute obj
-let rebuild_arguments_scope (req,r,l) =
+let rebuild_arguments_scope (req,r,l,_) =
match req with
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->
- (req,r,compute_arguments_scope (Global.type_of_global r))
+ let scs,cls = compute_arguments_scope_full (Global.type_of_global r) in
+ (req,r,scs,cls)
| ArgsScopeManual ->
(* Add to the manually given scopes the one found automatically
for the extra parameters of the section *)
- let l' = compute_arguments_scope (Global.type_of_global r) in
+ let l',cls = compute_arguments_scope_full (Global.type_of_global r) in
let l1,_ = list_chop (List.length l' - List.length l) l' in
- (req,r,l1@l)
+ (req,r,l1@l,cls)
+
+type arguments_scope_obj =
+ arguments_scope_discharge_request * global_reference *
+ scope_name option list * Classops.cl_typ option list
-let (inArgumentsScope,outArgumentsScope) =
+let inArgumentsScope : arguments_scope_obj -> obj =
declare_object {(default_object "ARGUMENTS-SCOPE") with
cache_function = cache_arguments_scope;
load_function = load_arguments_scope;
@@ -515,21 +537,22 @@ let (inArgumentsScope,outArgumentsScope) =
let is_local local ref = local || isVarRef ref && Lib.is_in_section ref
-let declare_arguments_scope_gen req r scl =
- Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl))
+let declare_arguments_scope_gen req r (scl,cls) =
+ Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl,cls))
let declare_arguments_scope local ref scl =
let req =
if is_local local ref then ArgsScopeNoDischarge else ArgsScopeManual in
- declare_arguments_scope_gen req ref scl
+ declare_arguments_scope_gen req ref (scl,[])
let find_arguments_scope r =
- try Refmap.find r !arguments_scope
+ try fst (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_gen ArgsScopeAuto ref (compute_arguments_scope t)
+ declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope_full t)
+
(********************************)
(* Encoding notations as string *)
@@ -585,11 +608,11 @@ let pr_scope_classes sc =
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 =
+let pr_notation_info prglob ntn c =
str "\"" ++ str ntn ++ str "\" := " ++
- prraw (rawconstr_of_aconstr dummy_loc c)
+ prglob (glob_constr_of_aconstr dummy_loc c)
-let pr_named_scope prraw scope sc =
+let pr_named_scope prglob scope sc =
(if scope = default_scope then
match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with
| 0 -> str "No lonely notation"
@@ -600,14 +623,14 @@ let pr_named_scope prraw scope sc =
++ pr_scope_classes scope
++ Gmap.fold
(fun ntn ((_,r),(_,df)) strm ->
- pr_notation_info prraw df r ++ fnl () ++ strm)
+ pr_notation_info prglob df r ++ fnl () ++ strm)
sc.notations (mt ())
-let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
+let pr_scope prglob scope = pr_named_scope prglob scope (find_scope scope)
-let pr_scopes prraw =
+let pr_scopes prglob =
Gmap.fold
- (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
+ (fun scope sc strm -> pr_named_scope prglob scope sc ++ fnl () ++ strm)
!scope_map (mt ())
let rec find_default ntn = function
@@ -627,9 +650,6 @@ let factorize_entries = function
(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 strict ntn map =
let find =
if String.contains ntn ' ' then (=) ntn
@@ -677,7 +697,7 @@ let interp_notation_as_global_reference loc test ntn sc =
| [] -> error_notation_not_reference loc ntn
| _ -> error_ambiguous_notation loc ntn
-let locate_notation prraw ntn scope =
+let locate_notation prglob ntn scope =
let ntns = factorize_entries (browse_notation false ntn !scope_map) in
let scopes = Option.fold_right push_scope scope !scope_stack in
if ntns = [] then
@@ -690,7 +710,7 @@ let locate_notation prraw ntn scope =
prlist
(fun (sc,r,(_,df)) ->
hov 0 (
- pr_notation_info prraw df r ++ tbrk (1,2) ++
+ pr_notation_info prglob 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 ())
@@ -726,10 +746,10 @@ let collect_notations stack =
(all',ntn::knownntn))
([],[]) stack)
-let pr_visible_in_scope prraw (scope,ntns) =
+let pr_visible_in_scope prglob (scope,ntns) =
let strm =
List.fold_right
- (fun (df,r) strm -> pr_notation_info prraw df r ++ fnl () ++ strm)
+ (fun (df,r) strm -> pr_notation_info prglob 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())
@@ -737,14 +757,14 @@ let pr_visible_in_scope prraw (scope,ntns) =
str "Visible in scope " ++ str scope)
++ fnl () ++ strm
-let pr_scope_stack prraw stack =
+let pr_scope_stack prglob stack =
List.fold_left
- (fun strm scntns -> strm ++ pr_visible_in_scope prraw scntns ++ fnl ())
+ (fun strm scntns -> strm ++ pr_visible_in_scope prglob 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
+let pr_visibility prglob = function
+ | Some scope -> pr_scope_stack prglob (push_scope scope !scope_stack)
+ | None -> pr_scope_stack prglob !scope_stack
(**********************************************************************)
(* Mapping notations to concrete syntax *)