diff options
| -rw-r--r-- | interp/notation.ml | 47 |
1 files changed, 26 insertions, 21 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 36d4b0aa15..4b25146c50 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -304,6 +304,8 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) type required_module = full_path * string list +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign + type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr @@ -313,17 +315,19 @@ type 'a prim_token_uninterpreter = glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status type internal_prim_token_interpreter = - ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr) + | ForNumeral of rawnum prim_token_interpreter + | ForString of string prim_token_interpreter let prim_token_interpreter_tab = - (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t) + (Hashtbl.create 7 : + (scope_name, required_module * internal_prim_token_interpreter) Hashtbl.t) -let add_prim_token_interpreter sc interp = - Hashtbl.replace prim_token_interpreter_tab sc interp +let add_prim_token_interpreter sc (dir,interp) = + Hashtbl.replace prim_token_interpreter_tab sc (dir,interp) -let declare_prim_token_interpreter sc interp (patl,uninterp,b) = +let declare_prim_token_interpreter sc (dir,interp) (patl,uninterp,b) = declare_scope sc; - add_prim_token_interpreter sc interp; + add_prim_token_interpreter sc (dir,interp); List.iter (fun pat -> prim_token_key_table := KeyMap.add (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table) @@ -340,29 +344,21 @@ let mkString = function | None -> None | Some s -> if Unicode.is_utf8 s then Some (String s) else None -let delay dir int ?loc x = (dir, (fun () -> int ?loc x)) - -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign - let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) = declare_prim_token_interpreter sc - (fun ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s) - | _ -> raise Not_found) + (dir, ForNumeral interp) (patl, (fun r -> match uninterp r with | None -> None | Some (n,s) -> Some (Numeral (n,s))), inpat) let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = - let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in declare_prim_token_interpreter sc - (fun ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s) - | _ -> raise Not_found) + (dir, ForNumeral (fun ?loc (n,s) -> interp ?loc (ofNumeral n s))) (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat) let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = declare_prim_token_interpreter sc - (fun ?loc -> function String s -> delay dir interp ?loc s - | _ -> raise Not_found) + (dir, ForString interp) (patl, (fun r -> mkString (uninterp r)), inpat) let check_required_module ?loc sc (sp,d) = @@ -472,9 +468,14 @@ let find_prim_token check_allowed ?loc p sc = pat, df with Not_found -> (* Try for a primitive numerical notation *) - let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc ?loc p in + let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc in check_required_module ?loc sc spdir; - let pat = interp () in + let pat = + match p, interp with + | Numeral (n,s), ForNumeral interp -> interp ?loc (n,s) + | String s, ForString interp -> interp ?loc s + | _ -> raise Not_found + in check_allowed pat; pat, ((dirpath (fst spdir),DirPath.empty),"") @@ -680,8 +681,12 @@ let uninterp_prim_token_cases_pattern c = let availability_of_prim_token n printer_scope local_scopes = let f scope = - try ignore ((Hashtbl.find prim_token_interpreter_tab scope) n); true - with Not_found -> false in + match n, Hashtbl.find prim_token_interpreter_tab scope with + | exception Not_found -> false + | Numeral _, (_,ForNumeral _) -> true + | String _, (_,ForString _) -> true + | _ -> false + in let scopes = make_current_scopes local_scopes in Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) |