diff options
| -rw-r--r-- | interp/constrintern.ml | 23 | ||||
| -rw-r--r-- | interp/symbols.ml | 21 | ||||
| -rw-r--r-- | interp/symbols.mli | 8 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 21 |
4 files changed, 48 insertions, 25 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 84be73849..e4bf4c9d7 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -137,6 +137,23 @@ let add_glob loc ref = let dp = string_of_dirpath (Lib.library_part ref) in dump_string (Printf.sprintf "R%d %s.%s\n" (fst loc) dp id) +let loc_of_notation f loc args ntn = + if args=[] or ntn.[0] <> '_' then fst loc else snd (f (List.hd args)) + +let ntn_loc = loc_of_notation constr_loc +let patntn_loc = loc_of_notation cases_pattern_loc + +let dump_notation_location = + let token_number = ref 0 in + fun pos ntn ((path,df),sc) -> + let rec next () = + let (bp,_ as loc) = !Lexer.current_location_function !token_number in + if bp >= pos then loc else (incr token_number; next ()) in + let loc = next () in + let path = string_of_dirpath path in + let sc = match sc with Some sc -> " "^sc | None -> "" in + dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst loc) path df sc) + (**********************************************************************) (* Remembering the parsing scope of variables in notations *) @@ -408,7 +425,8 @@ let rec intern_cases_pattern scopes aliases tmp_scope = function intern_cases_pattern scopes aliases tmp_scope a | CPatNotation (loc, ntn, args) -> let scopes = option_cons tmp_scope scopes in - let (ids,c) = Symbols.interp_notation ntn scopes in + let ((ids,c),df) = Symbols.interp_notation ntn scopes in + if !dump then dump_notation_location (patntn_loc loc args ntn) ntn df; let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in subst_cases_pattern loc aliases intern_cases_pattern subst scopes c | CPatNumeral (loc, n) -> @@ -630,7 +648,8 @@ let internalise sigma env allow_soapp lvar c = | CNotation (_,"( _ )",[a]) -> intern env a | CNotation (loc,ntn,args) -> let scopes = option_cons tmp_scope scopes in - let (ids,c) = Symbols.interp_notation ntn scopes in + let ((ids,c),df) = Symbols.interp_notation ntn scopes in + if !dump then dump_notation_location (ntn_loc loc args ntn) ntn df; let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in subst_rawconstr loc intern subst env c | CNumeral (loc, n) -> diff --git a/interp/symbols.ml b/interp/symbols.ml index 44237b6c9..32d74b651 100644 --- a/interp/symbols.ml +++ b/interp/symbols.ml @@ -43,11 +43,11 @@ type level = precedence * tolerability list type delimiters = string type scope = { - notations: (interpretation * string * bool) Stringmap.t; + notations: (interpretation * (dir_path * string) * bool) Stringmap.t; delimiters: delimiters option } -(* Uninterpreted notation map: notation -> level *) +(* Uninterpreted notation map: notation -> level * dir_path *) let notation_level_map = ref Stringmap.empty (* Scopes table: scope_name -> symbol_interpretation *) @@ -284,15 +284,16 @@ let rec find_interpretation f = function let scope = match sce with | Scope s -> s | SingleNotation _ -> default_scope in - (try f (find_scope scope) + (try f scope with Not_found -> find_interpretation f scopes) | [] -> raise Not_found let rec interp_notation ntn scopes = - let f scope = - let (pat,_,pp8only) = Stringmap.find ntn scope.notations in + 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 in + 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 -> error ("Unknown interpretation for notation \""^ntn^"\"") @@ -488,7 +489,7 @@ let pr_named_scope prraw scope sc = ++ fnl () ++ pr_scope_classes scope ++ Stringmap.fold - (fun ntn ((_,r),df,_) strm -> + (fun ntn ((_,r),(_,df),_) strm -> pr_notation_info prraw df r ++ fnl () ++ strm) sc.notations (mt ()) @@ -542,7 +543,7 @@ let locate_notation prraw ntn = prlist (fun (ntn,l) -> let scope = find_default ntn !scope_stack in prlist - (fun (sc,r,df) -> + (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)) ++ @@ -554,7 +555,7 @@ let locate_notation prraw ntn = let collect_notation_in_scope scope sc known = assert (scope <> default_scope); Stringmap.fold - (fun ntn ((_,r),df,_) (l,known as acc) -> + (fun ntn ((_,r),(_,df),_) (l,known as acc) -> if List.mem ntn known then acc else ((df,r)::l,ntn::known)) sc.notations ([],known) @@ -570,7 +571,7 @@ let collect_notations stack = | SingleNotation ntn -> if List.mem ntn knownntn then (all,knownntn) else - let ((_,r),df,_) = + let ((_,r),(_,df),_) = Stringmap.find ntn (find_scope default_scope).notations in let all' = match all with | (s,lonelyntn)::rest when s = default_scope -> diff --git a/interp/symbols.mli b/interp/symbols.mli index ffd82c808..a86ed49f1 100644 --- a/interp/symbols.mli +++ b/interp/symbols.mli @@ -88,12 +88,13 @@ type interp_rule = | NotationRule of scope_name option * notation | SynDefRule of kernel_name val declare_notation_interpretation : notation -> scope_name option -> - interpretation -> string -> bool -> unit + interpretation -> dir_path * string -> bool -> unit val declare_uninterpretation : interp_rule -> interpretation -> unit (* Returns the interpretation bound to a notation *) -val interp_notation : notation -> scope_name list -> interpretation +val interp_notation : notation -> scope_name list -> + interpretation * ((dir_path * string) * scope_name option) (* Returns the possible notations for a given term *) val uninterp_notations : rawconstr -> @@ -111,7 +112,8 @@ val availability_of_notation : scope_name option * notation -> scopes -> (*s Declare and test the level of a (possibly uninterpreted) notation *) val declare_notation_level : notation -> level option * level -> unit -val level_of_notation : notation -> level option * level (* [Not_found] if no level *) +val level_of_notation : notation -> level option * level + (* raise [Not_found] if no level *) (*s** Miscellaneous *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 5e32e5547..f5016c7d3 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -874,20 +874,20 @@ let compute_syntax_data forv7 (df,modifiers) = (* To globalize... *) let typs = List.map (set_entry_type etyps) typs in let (prec,notation) = make_symbolic n symbols typs in - ((onlyparse,vars,notation),prec,(n,typs,symbols,fmt)) + ((onlyparse,vars,notation),prec,(n,typs,symbols,fmt),(Lib.library_dp(),df)) let add_syntax_extension local mv mv8 = let data8 = option_app (compute_syntax_data false) mv8 in let data = option_app (compute_syntax_data !Options.v7) mv in let prec,gram_rule = match data with | None -> None, None - | Some ((_,_,notation),prec,(n,typs,symbols,_)) -> + | Some ((_,_,notation),prec,(n,typs,symbols,_),_) -> Some prec, Some (make_grammar_rule n typs symbols notation) in match data, data8 with | None, None -> (* Nothing to do: V8Notation while not translating *) () | _, Some d | Some d, None -> - let ((_,_,notation),ppprec,ppdata) = d in - let notation = match data with Some ((_,_,ntn),_,_) -> ntn | _ -> notation in + let ((_,_,notation),ppprec,ppdata,_) = d in + let notation = match data with Some ((_,_,ntn),_,_,_) -> ntn | _ -> notation in let pp_rule = make_pp_rule ppdata in Lib.add_anonymous_leaf (inSyntaxExtension (local,(prec,ppprec),notation,gram_rule,pp_rule)) @@ -963,7 +963,7 @@ let make_old_pp_rule n symbols typs r ntn scope vars = make_syntax_rule n rule_name symbols typs ast ntn scope let add_notation_in_scope local df c mods omodv8 scope toks = - let ((onlyparse,vars,notation),prec,(n,typs,symbols,_ as ppdata)) = + let ((onlyparse,vars,notation),prec,(n,typs,symbols,_ as ppdata),df') = compute_syntax_data !Options.v7 (df,mods) in (* Declare the parsing and printing rules if not already done *) (* For both v7 and translate: parsing is as described for v7 in v7 file *) @@ -977,7 +977,7 @@ let add_notation_in_scope local df c mods omodv8 scope toks = let ppnot,ppprec,pp_rule = match omodv8 with | Some mv8 -> - let (_,_,ntn8),p,d = compute_syntax_data false mv8 in + let (_,_,ntn8),p,d,_ = compute_syntax_data false mv8 in ntn8,p,make_pp_rule d | _ -> (* means the rule already exists: recover it *) @@ -1003,7 +1003,7 @@ let add_notation_in_scope local df c mods omodv8 scope toks = let onlyparse = onlyparse or !Options.v7_only in let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in Lib.add_anonymous_leaf - (inNotation(local,old_pp_rule,ppnot,scope,a,onlyparse,false,df)) + (inNotation(local,old_pp_rule,ppnot,scope,a,onlyparse,false,df')) let level_rule (n,p) = if p = E then n else max (n-1) 0 @@ -1034,7 +1034,8 @@ let add_notation_interpretation_core local symbs for_old df a scope onlyparse option_app (build_old_pp_rule notation scope symbs) for_old else None in Lib.add_anonymous_leaf - (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,onlypp,df)) + (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,onlypp, + (Lib.library_dp(),df))) let add_notation_interpretation df names c sc = let (vars,symbs) = analyse_notation_tokens (split_notation_string df) in @@ -1046,7 +1047,7 @@ let add_notation_interpretation df names c sc = add_notation_interpretation_core false symbs for_oldpp df a sc false false let add_notation_in_scope_v8only local df c mv8 scope toks = - let (_,vars,notation),prec,ppdata = compute_syntax_data false (df,mv8) in + let (_,vars,notation),prec,ppdata,df' = compute_syntax_data false (df,mv8) in let pp_rule = make_pp_rule ppdata in Lib.add_anonymous_leaf (inSyntaxExtension(local,(None,prec),notation,None,pp_rule)); @@ -1054,7 +1055,7 @@ let add_notation_in_scope_v8only local df c mv8 scope toks = let onlyparse = false in let a = interp_aconstr [] vars c in Lib.add_anonymous_leaf - (inNotation(local,None,notation,scope,a,onlyparse,true,df)) + (inNotation(local,None,notation,scope,a,onlyparse,true,df')) let add_notation_v8only local c (df,modifiers) sc = let toks = split_notation_string df in |