Refactor builtin lookup to use unified API with optional parameters

In response to PR review feedback, this commit consolidates the builtin
lookup functions into a single  function with optional
labeled parameters, replacing the previous split between ,
, and .

Author: NotBad4U

src/core/builtin.ml

@@ -6,42 +6,37 @@ open Common open Error open Pos
 open Term
 open Sig_state
 
-(** [find_builtin ss pos name] returns the symbol mapped to the builtin [name] by looking through all builtins scope.
-   It first checks the current signature's path, then searches through all other modules.
+(** [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 find_builtin : sig_state -> popt -> string -> sym = fun ss pos name ->
-  (* First, try to find in the current signature's path *)
-  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 symbol %s." name
-    with Found s -> s
-
-(** [get_at ss path pos name] returns the symbol mapped to the builtin [name]
-   in the module located at [path]. If the symbol cannot be found then
-   [Fatal] is raised. *)
-let get_at : sig_state -> Path.t -> popt -> string -> sym = fun ss path pos name ->
-  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
-
-(** [get ss pos name] returns the symbol mapped to the builtin [name] in the current signature from [ss].
-  If the symbol cannot be found then [Fatal] is raised. *)
-let get : sig_state -> popt -> string -> sym = fun ss pos name ->
-  get_at ss ss.signature.sign_path pos 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 (Path.Map.find ss.signature.sign_path ss.builtins)) with Not_found -> None
+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/handle/command.ml

@@ -11,19 +11,6 @@ open Goal
 (** Type alias for a function that compiles a Lambdapi module. *)
 type compiler = Path.t -> Sign.t
 
-(** [find_builtin ss name] searches for a builtin symbol named [name] across
-    all paths in [ss.builtins]. Returns [Some sym] if found, [None] otherwise. *)
-let find_builtin : sig_state -> string -> sym option = fun ss name ->
-  let exception Found of sym in
-  try
-    Path.Map.iter (fun _ strmap ->
-      match StrMap.find_opt name strmap with
-      | Some s -> raise (Found s)
-      | None -> ()
-    ) ss.builtins;
-    None
-  with Found s -> Some s
-
 (** Register a check for the type of the builtin symbols "nat_zero" and
     "nat_succ". *)
 let _ =
@@ -34,19 +21,20 @@ let _ =
   in
   let register = Builtin.register_expected_type eq_noexn term in
   let expected_zero_type ss _pos =
-    match find_builtin ss "nat_succ" with
-    | Some s ->
-        (match !(s.sym_type) with
-         | Prod(a,_) -> a
-         | _ -> assert false)
-    | None -> mk_Meta (LibMeta.fresh (new_problem()) mk_Type 0, [||])
+    try
+      let s = Builtin.get ss "nat_succ" in
+      match !(s.sym_type) with
+      | Prod(a,_) -> a
+      | _ -> assert false
+    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 =
-      match find_builtin ss "nat_zero" with
-      | Some s -> !(s.sym_type)
-      | None -> 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
@@ -298,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 find_builtin ss n 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.find_builtin 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.find_builtin 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.find_builtin 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.find_builtin pos map "T" in
-    let symb_P = Builtin.find_builtin 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.find_builtin pos map "T" in
-    let symb_P = Builtin.find_builtin pos map "P" in
-    let symb_eq = Builtin.find_builtin 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.find_builtin 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.find_builtin 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.find_builtin 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.find_builtin 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.find_builtin 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,8 +96,7 @@ type token =
   (* other tokens *)
   | DEBUG_FLAGS of (bool * string)
       (* Tuple constructor (with parens) required by Menhir. *)
-  | INT of string
-  | PINT of (Path.t * string)
+  | INT of (Path.t * string)
   | FLOAT of string
   | SIDE of Pratter.associativity
   | STRINGLIT of string
@@ -273,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))
 
@@ -323,7 +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 -> PINT(ids, Utf8.lexeme 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,8 +89,7 @@
 // other tokens
 
 %token <bool * string> DEBUG_FLAGS
-%token <string> INT
-%token <Path.t * string> PINT
+%token <Path.t * string> INT
 %token <string> FLOAT
 %token <Pratter.associativity> SIDE
 %token <string> STRINGLIT
@@ -218,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
@@ -295,11 +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)) }
-  | m=PINT {
+  | m=INT {
       let (p, n) = m in
         make_pos $sloc (P_NLit(List.rev p, n)) }
-  | n=INT {
-      make_pos $sloc (P_NLit([], n)) }
   | s=STRINGLIT { make_pos $sloc (P_SLit s) }
 
 env: DOT L_SQ_BRACKET ts=separated_list(SEMICOLON, term) R_SQ_BRACKET { ts }
@@ -425,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(ps, i)           , _    ) -> out ppf "%a %s" (raw_path) ps 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,7 +285,7 @@ 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.find_builtin 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
@@ -298,12 +298,11 @@ and scope_head : ?find_sym:find_sym ->
         let s = if neg then String.sub s 1 (String.length s - 1) else s in
         neg, s
       in
-      (* Use Builtin.find_builtin for unqualified numeric literals (path=[]),
-         and Builtin.find_builtin_at for qualified ones (e.g., Nat.12). *)
+      (* 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
-          (if path = [] then Builtin.find_builtin ss pos s
-           else Builtin.get_at ss path pos s)
+        mk_Symb (Builtin.get ss ~mp:path ~pos s)
       in
       let sym = Array.map sym_of strint in
       let digit = function