Allow decimal notation for multiple types by scoping builtin map…

src/core/builtin.ml

@@ -6,16 +6,37 @@ open Common open Error open Pos
 open Term
 open Sig_state
 
-(** [get ss pos name] returns the symbol mapped to the builtin [name]. If the
-   symbol cannot be found then [Fatal] is raised. *)
-let get : sig_state -> popt -> string -> sym = fun ss pos name ->
-  try StrMap.find name ss.builtins with Not_found ->
-    fatal pos "Builtin symbol \"%s\" undefined." name
-
-(** [get_opt ss name] returns [Some s] where [s] is the symbol mapped to
-   the builtin [name], and [None] otherwise. *)
-let get_opt : sig_state -> string -> sym option = fun ss name ->
-  try Some (StrMap.find name ss.builtins) with Not_found -> None
+(** [get ss ~mp ~pos name] returns the symbol mapped to the builtin [name].
+   If [mp] is empty (unqualified), it first checks the current signature's path,
+   then searches through all other modules. If [mp] is specified (qualified),
+   it looks only in that specific module path.
+   If the symbol cannot be found then [Fatal] is raised. *)
+let get : sig_state -> ?mp:Path.t -> ?pos:popt -> string -> sym = fun ss ?(mp=[]) ?(pos=None) name ->
+  match mp with
+  | [] ->
+    (* Unqualified: search current signature first, then all other paths *)
+    begin
+      try
+        StrMap.find name (Path.Map.find ss.signature.sign_path ss.builtins)
+      with Not_found ->
+        (* If not found, search through all other paths *)
+        let exception Found of sym in
+        try
+          Path.Map.iter (fun path strmap ->
+            if path <> ss.signature.sign_path then
+              match StrMap.find_opt name strmap with
+              | Some s -> raise (Found s)
+              | None -> ()
+          ) ss.builtins;
+          fatal pos "Unknown builtin symbol %s." name
+        with Found s -> s
+    end
+  | path ->
+    (* Qualified: look in the specific path *)
+    begin
+      try StrMap.find name (Path.Map.find path ss.builtins) with Not_found ->
+        fatal pos "Builtin symbol \"%s\" in %a undefined." name Path.pp path
+    end
 
 (** Hash-table used to record checking functions for builtins. *)
 let htbl : (string, sig_state -> popt -> sym -> unit) Hashtbl.t =

src/core/print.ml

@@ -122,7 +122,7 @@ let var : var pp = fun ppf x -> uid ppf (base_name x)
 exception Not_a_nat
 
 let builtin name =
-  try StrMap.find name (!sig_state).builtins with Not_found -> raise Not_a_nat
+  try StrMap.find name (Path.Map.find (!sig_state).signature.sign_path (!sig_state).builtins) with Not_found -> raise Not_a_nat
 
 (** [nat_of_term t] converts a term into a natural number.
     @raise Not_a_nat if this is not possible. *)

src/core/sig_state.ml

@@ -21,7 +21,7 @@ type sig_state =
   ; in_scope  : sym StrMap.t              (** Symbols in scope.  *)
   ; alias_path: Path.t StrMap.t           (** Alias to path map. *)
   ; path_alias: string Path.Map.t         (** Path to alias map. *)
-  ; builtins  : sym StrMap.t              (** Builtins. *)
+  ; builtins  : sym StrMap.t Path.Map.t   (** Builtins. *)
   ; open_paths : Path.Set.t               (** Open modules. *) }
 
 type t = sig_state
@@ -71,7 +71,13 @@ let add_builtin : sig_state -> string -> sym -> sig_state =
   (* Update the builtins of the current signature. *)
   Sign.add_builtin ss.signature b s;
   (* Update the builtins of the sig_state. *)
-  let builtins = StrMap.add b s ss.builtins in
+  let path = ss.signature.sign_path in
+  let path_builtins =
+    try Path.Map.find path ss.builtins
+    with Not_found -> StrMap.empty
+  in
+  let path_builtins = StrMap.add b s path_builtins in
+  let builtins = Path.Map.add path path_builtins ss.builtins in
   {ss with builtins}
 
 (** [open_sign ss sign] extends the signature state [ss] with every symbol of
@@ -92,7 +98,7 @@ let of_sign : Sign.t -> sig_state = fun signature ->
     ; in_scope = StrMap.empty
     ; alias_path = StrMap.empty
     ; path_alias = Path.Map.empty
-    ; builtins = StrMap.empty
+    ; builtins = Path.Map.empty
     ; open_paths = Path.Set.empty }
   in
   open_sign (open_sign ss Ghost.sign) signature

src/core/sign.ml

@@ -39,9 +39,11 @@ let mem : t -> string -> bool = fun sign name ->
   StrMap.mem name !(sign.sign_symbols)
 
 (** [find sign name] finds the symbol named [name] in signature [sign] if it
-    exists, and raises the [Not_found] exception otherwise. *)
+    exists, and raises the [Not_found] exception otherwise. Searches first in
+    sign_symbols, then in sign_builtins. *)
 let find : t -> string -> sym = fun sign name ->
-  StrMap.find name !(sign.sign_symbols)
+  try StrMap.find name !(sign.sign_symbols)
+  with Not_found -> StrMap.find name !(sign.sign_builtins)
 
 (** [loaded] stores the signatures of the known (already compiled or currently
     being compiled) modules. The current module is stored in [loaded] so that

src/handle/command.ml

@@ -22,17 +22,19 @@ let _ =
   let register = Builtin.register_expected_type eq_noexn term in
   let expected_zero_type ss _pos =
     try
-      match !((StrMap.find "nat_succ" ss.builtins).sym_type) with
+      let s = Builtin.get ss "nat_succ" in
+      match !(s.sym_type) with
       | Prod(a,_) -> a
       | _ -> assert false
-    with Not_found -> mk_Meta (LibMeta.fresh (new_problem()) mk_Type 0, [||])
+    with Fatal _ -> mk_Meta (LibMeta.fresh (new_problem()) mk_Type 0, [||])
   in
   register "nat_zero" expected_zero_type;
   let expected_succ_type ss _pos =
     let typ_0 =
-      try !((StrMap.find "nat_zero" ss.builtins).sym_type)
-      with Not_found ->
-        mk_Meta (LibMeta.fresh (new_problem()) mk_Type 0, [||])
+      try
+        let s = Builtin.get ss "nat_zero" in
+        !(s.sym_type)
+      with Fatal _ -> mk_Meta (LibMeta.fresh (new_problem()) mk_Type 0, [||])
     in
     mk_Arro (typ_0, typ_0)
   in
@@ -98,9 +100,8 @@ let rec rec_require : compiler -> sig_state -> Path.t -> sig_state =
         (* Recurse on the dependencies of [p]. *)
         let f p _ ss = rec_require compile ss p in
         let ss = Path.Map.fold f !(sign.sign_deps) ss in
-        (* Add builtins of [p] in [ss]. *)
-        let f _k _v1 v2 = Some v2 in (* hides previous symbols *)
-        let builtins = StrMap.union f ss.builtins !(sign.sign_builtins) in
+        (* Add builtins of [p] in [ss] under the path key [p]. *)
+        let builtins = Path.Map.add p !(sign.sign_builtins) ss.builtins in
         let ss = {ss with builtins} in
         (* Add [p] in dependencies. *)
         let dep = {dep_symbols=StrMap.empty; dep_open=false} in
@@ -285,10 +286,14 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
   | P_builtin(n,qid) ->
       let s = find_sym ~prt:true ~prv:true ss qid in
       begin
-        match StrMap.find_opt n ss.builtins with
-        | Some s' when s' == s ->
-          fatal pos "Builtin \"%s\" already mapped to %a" n sym s
-        | _ ->
+        try
+          let s' = Builtin.get ss n in
+          if s' == s then
+            fatal pos "Builtin \"%s\" already mapped to %a" n sym s
+          else
+            fatal pos "Builtin \"%s\" already mapped to another symbol" n
+        with Fatal _ ->
+          (* Builtin not yet defined, proceed *)
           Builtin.check ss pos n s;
           Console.out 2 (Color.gre "builtin \"%s\" ≔ %a") n sym s;
           (Sig_state.add_builtin ss n s, None, None)

src/handle/fol.ml

@@ -21,7 +21,7 @@ type config =
 
 (** [get_config ss pos] build the configuration using [ss]. *)
 let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos ->
-  let builtin = Builtin.get ss pos in
+  let builtin name = Builtin.get ss ~pos name in
   let symb_P = builtin "P" and symb_T = builtin "T" in
   let symb_Prop =
     match unfold Timed.(!(symb_P.sym_type)) with

src/handle/inductive.ml

@@ -30,7 +30,7 @@ type config =
 
 (** [get_config ss pos] build the configuration using [ss]. *)
 let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos ->
-  let builtin = Builtin.get ss pos in
+  let builtin name = Builtin.get ss ~pos name in
   { symb_Prop = builtin "Prop"
   ; symb_prf  = builtin "P" }
 

src/handle/rewrite.ml

@@ -18,9 +18,9 @@ type eq_config =
   ; symb_refl  : sym (** Reflexivity of equality.         *) }
 
 (** [get_eq_config ss pos] returns the current configuration for
-    equality, used by tactics such as “rewrite” or “reflexivity”. *)
+    equality, used by tactics such as "rewrite" or "reflexivity". *)
 let get_eq_config : Sig_state.t -> popt -> eq_config = fun ss pos ->
-  let builtin = Builtin.get ss pos in
+  let builtin name = Builtin.get ss ~pos name in
   { symb_P     = builtin "P"
   ; symb_T     = builtin "T"
   ; symb_eq    = builtin "eq"
@@ -50,10 +50,10 @@ let _ =
   let register_builtin =
     Builtin.register_expected_type (Eval.eq_modulo []) term
   in
-  let expected_eq_type pos map =
+  let expected_eq_type ss pos =
     (* [Π (a:U), T a → T a → Prop] *)
-    let symb_T = Builtin.get pos map "T" in
-    let symb_P = Builtin.get pos map "P" in
+    let symb_T = Builtin.get ss ~pos "T" in
+    let symb_P = Builtin.get ss ~pos "P" in
     let term_U = get_domain_of_type symb_T in
     let term_Prop = get_domain_of_type symb_P in
     let a = new_var "a" in
@@ -62,11 +62,11 @@ let _ =
     mk_Prod (term_U, bind_var a impls)
   in
   register_builtin "eq" expected_eq_type;
-  let expected_refl_type pos map =
+  let expected_refl_type ss pos =
     (* [Π (a:U) (x:T a), P (eq a x x)] *)
-    let symb_T = Builtin.get pos map "T" in
-    let symb_P = Builtin.get pos map "P" in
-    let symb_eq = Builtin.get pos map "eq" in
+    let symb_T = Builtin.get ss ~pos "T" in
+    let symb_P = Builtin.get ss ~pos "P" in
+    let symb_eq = Builtin.get ss ~pos "eq" in
     let term_U = get_domain_of_type symb_T in
     let a = new_var "a" in
     let x = new_var "x" in
@@ -78,13 +78,13 @@ let _ =
     mk_Prod (term_U, bind_var a prod)
   in
   register_builtin "refl" expected_refl_type;
-  let expected_eqind_type pos map =
+  let expected_eqind_type ss pos =
     (* [Π (a:U) (x y:T a), P (eq x y) → Π (p:T a→Prop), P (p y) → P (p x)] *)
-    let symb_T = Builtin.get pos map "T" in
+    let symb_T = Builtin.get ss ~pos "T" in
     let term_T = mk_Symb symb_T in
-    let symb_P = Builtin.get pos map "P" in
+    let symb_P = Builtin.get ss ~pos "P" in
     let term_P = mk_Symb symb_P in
-    let symb_eq = Builtin.get pos map "eq" in
+    let symb_eq = Builtin.get ss ~pos "eq" in
     let term_eq = mk_Symb symb_eq in
     let term_U = get_domain_of_type symb_T in
     let term_Prop = get_domain_of_type symb_P in

src/handle/tactic.ml

@@ -224,7 +224,7 @@ type config = (string,tactic) Hashtbl.t
 (** [get_config ss pos] build the configuration using [ss]. *)
 let get_config (ss:Sig_state.t) (pos:Pos.popt) : config =
   let t = Hashtbl.create 17 in
-  let add n v = let s = Builtin.get ss pos n in Hashtbl.add t s.sym_name v in
+  let add n v = let s = Builtin.get ss ~pos n in Hashtbl.add t s.sym_name v in
   add "admit" T_admit;
   add "and" T_and;
   add "apply" T_apply;
@@ -366,7 +366,7 @@ let p_tactic (ss:Sig_state.t) (pos:popt) :int StrMap.t -> term -> p_tactic =
             | T_generalize, [_;t] -> P_tac_generalize(p_ident_of_var pos t)
             | T_generalize, _ -> assert false
             | T_have, [t1;t2] ->
-                let prf_sym = Builtin.get ss pos "P" in
+                let prf_sym = Builtin.get ss ~pos "P" in
                 let prf = p_term pos idmap (mk_Symb prf_sym) in
                 let t2 = Pos.make pos (P_Appl(prf, p_term pos idmap t2)) in
                 P_tac_have(p_ident_of_sym pos t1, t2)

src/parsing/lpLexer.ml

@@ -96,7 +96,7 @@ type token =
   (* other tokens *)
   | DEBUG_FLAGS of (bool * string)
       (* Tuple constructor (with parens) required by Menhir. *)
-  | INT of string
+  | INT of (Path.t * string)
   | FLOAT of string
   | SIDE of Pratter.associativity
   | STRINGLIT of string
@@ -272,7 +272,7 @@ let rec token lb =
   (* other tokens *)
   | '+', Plus lowercase -> DEBUG_FLAGS(true, remove_first lb)
   | '-', Plus lowercase -> DEBUG_FLAGS(false, remove_first lb)
-  | int -> INT(Utf8.lexeme lb)
+  | int -> INT(([], Utf8.lexeme lb))
   | float -> FLOAT(Utf8.lexeme lb)
   | string -> STRINGLIT(Utf8.sub_lexeme lb 1 (lexeme_length lb - 2))
 
@@ -322,6 +322,7 @@ and qid expl ids lb =
   | "/*" -> comment (qid expl ids) 0 lb
   | regid, '.' -> qid expl (remove_last lb :: ids) lb
   | escid, '.' -> qid expl (remove_useless_escape(remove_last lb) :: ids) lb
+  | int -> INT(ids, Utf8.lexeme lb)
   | regid ->
     if expl then QID_EXPL(Utf8.lexeme lb :: ids)
     else QID(Utf8.lexeme lb :: ids)

src/parsing/lpParser.mly

@@ -89,7 +89,7 @@
 // other tokens
 
 %token <bool * string> DEBUG_FLAGS
-%token <string> INT
+%token <Path.t * string> INT
 %token <string> FLOAT
 %token <Pratter.associativity> SIDE
 %token <string> STRINGLIT
@@ -217,8 +217,11 @@ query:
   | FLAG s=STRINGLIT b=SWITCH { make_pos $sloc (P_query_flag(s,b)) }
   | PROVER s=STRINGLIT { make_pos $sloc (P_query_prover(s)) }
   | PROVER_TIMEOUT n=INT
-    { make_pos $sloc (P_query_prover_timeout n) }
-  | VERBOSE n=INT { make_pos $sloc (P_query_verbose n) }
+    { let (_, m) = n in
+      make_pos $sloc (P_query_prover_timeout m) }
+  | VERBOSE n=INT
+    { let (_, m) = n in
+        make_pos $sloc (P_query_verbose  m) }
   | TYPE_QUERY t=term
     { make_pos $sloc (P_query_infer(t, {strategy=NONE; steps=None}))}
   | SEARCH s=STRINGLIT
@@ -294,7 +297,9 @@ aterm:
       make_pos $sloc (P_Patt(i, Option.map Array.of_list e)) }
   | L_PAREN t=term R_PAREN { make_pos $sloc (P_Wrap(t)) }
   | L_SQ_BRACKET t=term R_SQ_BRACKET { make_pos $sloc (P_Expl(t)) }
-  | n=INT { make_pos $sloc (P_NLit n) }
+  | m=INT {
+      let (p, n) = m in
+        make_pos $sloc (P_NLit(List.rev p, n)) }
   | s=STRINGLIT { make_pos $sloc (P_SLit s) }
 
 env: DOT L_SQ_BRACKET ts=separated_list(SEMICOLON, term) R_SQ_BRACKET { ts }
@@ -420,7 +425,7 @@ notation:
 
 float_or_int:
   | s=FLOAT { s }
-  | s=INT { s }
+  | s=INT { let (_, m) = s in m }
 
 maybe_generalize:
   | g = GENERALIZE?

src/parsing/pretty.ml

@@ -151,7 +151,7 @@ let rec term : p_term pp = fun ppf t ->
     | (P_LLet(x,xs,a,t,u)  , `Func) ->
         out ppf "@[@[<hv2>let @[<2>%a%a%a@] ≔@ %a@ @]in@ %a@]"
           ident x params_list xs typ a func t func u
-    | (P_NLit(i)           , _    ) -> out ppf "%s" i
+    | (P_NLit(ps, i)       , _    ) -> out ppf "%a %s" (raw_path) ps i
     | (P_SLit(s)           , _    ) -> out ppf "\"%s\"" s
     | (P_Wrap(t)           , _    ) -> out ppf "(@[<hv2>%a@])" func t
     | (P_Expl(t)           , _    ) -> out ppf "[@[<hv2>%a@]]" func t

src/parsing/scope.ml

@@ -285,20 +285,25 @@ and scope_head : ?find_sym:find_sym ->
         let sym =
           try Sign.find Sign.Ghost.sign s
           with Not_found ->
-            let s_typ = mk_Symb (Builtin.get ss pos "String") in
+            let s_typ = mk_Symb (Builtin.get ss ~pos "String") in
             Sign.add_symbol Sign.Ghost.sign Public Const Eager true
               {elt=s;pos} pos s_typ []
         in
         mk_Symb sym
       end
 
-  | (P_NLit s, _) ->
+  | (P_NLit (path, s), _) ->
       let neg, s =
         let neg = s.[0] = '-' in
         let s = if neg then String.sub s 1 (String.length s - 1) else s in
         neg, s
       in
-      let sym_of s = mk_Symb (Builtin.get ss pos s) in
+      (* Use Builtin.get for numeric literals, with optional path parameter.
+         For unqualified (path=[]), it searches current module first.
+         For qualified (e.g., Nat.12), it uses the specified path. *)
+      let sym_of s =
+        mk_Symb (Builtin.get ss ~mp:path ~pos s)
+      in
       let sym = Array.map sym_of strint in
       let digit = function
         | '0' -> sym.(0) | '1' -> sym.(1) | '2' -> sym.(2) | '3' -> sym.(3)

src/parsing/syntax.ml

@@ -66,7 +66,7 @@ and p_term_aux =
   | P_Prod of p_params list * p_term (** Product. *)
   | P_LLet of p_ident * p_params list * p_term option * p_term * p_term
     (** Let. *)
-  | P_NLit of string (** Integer literal. *)
+  | P_NLit of Path.t * string (** Integer literal. *)
   | P_SLit of string (** String literal. *)
   | P_Wrap of p_term (** Term between parentheses. *)
   | P_Expl of p_term (** Term between curly brackets. *)
@@ -367,7 +367,7 @@ let rec eq_p_term : p_term eq = fun {elt=t1;_} {elt=t2;_} ->
       && Option.eq eq_p_term a1 a2 && eq_p_term t1 t2 && eq_p_term u1 u2
   | P_Wrap t1, P_Wrap t2
   | P_Expl t1, P_Expl t2 -> eq_p_term t1 t2
-  | P_NLit s1, P_NLit s2
+  | P_NLit (p1, s1), P_NLit (p2, s2) -> p1 = p2 && s1 = s2
   | P_SLit s1, P_SLit s2 -> s1 = s2
   | _,_ -> false