Allow decimal notation for multiple types by scoping builtin map… #1326

NotBad4U · 2025-11-26T14:03:02Z

Previously, Lambdapi only allowed decimal notation (e.g., "0", "+1") to map to a single type, preventing its use across multiple types simultaneously. This change introduces scoped builtin mappings, enabling users to define decimal notation for multiple types in the same context. This PR, when finished, will close #1268.

TODO:

revert changes on sig_state type definition
change Builtin.get following Allow decimal notation for multiple types by scoping builtin map… #1326 (review)
in notation data type, add path information on constructors used for decimal notation
fix print.ml accordingly to prefix decimal numbers by the appropriate path whenever it is not in scope

NotBad4U · 2025-11-26T14:56:50Z

I think we can start the review @fblanqui. I removed the tag WIP.

NotBad4U · 2025-11-26T16:22:34Z

Hum, the CI is failing at the export test, but I do not know how we should modify the find_sym for the case when someone write e.g. Nat.3 that hits the fail during export.

fblanqui

Hi Alessio. Thank you for your PR. I started to review it. I think that we do not need to have so many changes, and to change the type of sig_state. You should simply modify the function Builtin.get in a way similar to Sig_state.find_sym:

let get : sig_state -> popt -> Path.t -> string -> sym = fun ss pos mp name ->
try
  match mp with
  | [] -> StrMap.find name ss.builtins
  | [m] when StrMap.mem m ss.alias_path -> (* Aliased module path. *)
          (* The signature must be loaded (alias is mapped). *)
          let sign =
            try Path.Map.find (StrMap.find m ss.alias_path) !loaded
            with _ -> assert false (* Should not happen. *)
          in
          (* Look for the symbol. *)
           StrMap.find !(sign.sign_builtins) name
  | _ ->
          (* Check that the signature was required (or is the current one). *)
          if mp <> ss.signature.sign_path then
            if not (Path.Map.mem mp !(ss.signature.sign_deps)) then
              fatal pos "No module [%a] required." Path.pp mp;
          (* The signature must have been loaded. *)
          let sign =
            try Path.Map.find mp !loaded
            with Not_found -> assert false (* Should not happen. *)
          in
          (* Look for the builtin. *)
          StrMap.find !(sign.sign_builtins) name
with Not_found ->
  if mp=[] then fatal pos "Builtin symbol \"%s\" undefined." name
  else fatal pos "Builtin symbol \"%a.%s\" undefined." Path.pp mp name

fblanqui · 2025-11-26T16:18:09Z

src/parsing/pretty.ml

        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


should be "%a.%s" raw_path

and keep arrows aligned ;-)

fblanqui · 2025-11-26T16:23:35Z

src/parsing/lpParser.mly


 %token <bool * string> DEBUG_FLAGS
 %token <string> INT
+%token <Path.t * string> PINT


Instead of introducing a new token, I suggest to change the type of INT by adding a path.

I tried to do that, but since I am not an expert in OcamlLex, I ran into many issues.
This parser is supposed to be replaced by #1129 so I do not think it is a problem.

fblanqui · 2025-11-26T16:38:15Z

src/parsing/lpLexer.ml

  | "/*" -> 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)


ids -> List.rev ids

fblanqui · 2025-11-26T16:55:28Z

src/export/rawdk.ml

  | P_Type -> out ppf "Type"
  | P_Wild -> out ppf "_"
-  | P_NLit i -> string ppf i
+  | P_NLit (path, i) -> out ppf "%a%s" Dk.path path i


Integer literals are undefined in Dedukti. Actually we should fail (already in master) like for string literals. I'm going to change master accordingly.

NotBad4U · 2025-11-26T17:42:59Z

Hi Alessio. Thank you for your PR. I started to review it. I think that we do not need to have so many changes, and to change the type of sig_state. You should simply modify the function Builtin.get in a way similar to Sig_state.find_sym:

let get : sig_state -> popt -> Path.t -> string -> sym = fun ss pos mp name ->
try
  match mp with
  | [] -> StrMap.find name ss.builtins
  | [m] when StrMap.mem m ss.alias_path -> (* Aliased module path. *)
          (* The signature must be loaded (alias is mapped). *)
          let sign =
            try Path.Map.find (StrMap.find m ss.alias_path) !loaded
            with _ -> assert false (* Should not happen. *)
          in
          (* Look for the symbol. *)
           StrMap.find !(sign.sign_builtins) name
  | _ ->
          (* Check that the signature was required (or is the current one). *)
          if mp <> ss.signature.sign_path then
            if not (Path.Map.mem mp !(ss.signature.sign_deps)) then
              fatal pos "No module [%a] required." Path.pp mp;
          (* The signature must have been loaded. *)
          let sign =
            try Path.Map.find mp !loaded
            with Not_found -> assert false (* Should not happen. *)
          in
          (* Look for the builtin. *)
          StrMap.find !(sign.sign_builtins) name
with Not_found ->
  if mp=[] then fatal pos "Builtin symbol \"%s\" undefined." name
  else fatal pos "Builtin symbol \"%a.%s\" undefined." Path.pp mp name

Oh, I see what you mean now, since it is clearer to me. Yeah, let me find a moment to just change the function Builtin.get

fblanqui · 2025-11-26T17:44:31Z

Hum, the CI is failing at the export test, but I do not know how we should modify the find_sym for the case when someone write e.g. Nat.3 that hits the fail during export.

This is related to #1327: integer literals cannot be translated to dedukti literally. You must add your new test file integers.lp in tests/export_raw_dk.sh.

…pings

- Add Builtin.find_builtin function that searches for a builtin symbol by iterating through all builtin scopes in sig_state.builtins - Add Sig_state.find_builtin with identical implementation and type alias - Replace Builtin.get calls with Builtin.find_builtin throughout codebase to enable cross-module builtin lookup for qualified numeric literals - Update scope.ml to use find_builtin for unqualified paths and get_at for qualified paths in numeric literal desugaring - Modify fol.ml, inductive.ml, rewrite.ml, and tactic.ml to use the new find_builtin function for builtin symbol resolution

…s path first, then search through all other modules

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 .

NotBad4U · 2025-11-27T17:36:27Z

I've consolidated the Builting.get function into a unified API as suggested.
I replaced the previous three functions (find_builtin, get_at, get) with a single function:

val get : sig_state -> ?mp:Path.t -> ?pos:popt -> string -> sym

I also merged INT/PINT tokens and updated scoping.

NotBad4U · 2025-11-27T17:41:36Z

Hum, the CI is failing at the export test, but I do not know how we should modify the find_sym for the case when someone write e.g. Nat.3 that hits the fail during export.

This is related to #1327: integer literals cannot be translated to dedukti literally. You must add your new test file integers.lp in tests/export_raw_dk.sh.

I added my test like this and rebased my PR on #1327

diff --git i/tests/export_raw_dk.sh w/tests/export_raw_dk.sh
index a4af665b..86e05dc8 100755
--- i/tests/export_raw_dk.sh
+++ w/tests/export_raw_dk.sh
@@ -52,7 +52,7 @@ do
         # "as"
         729);;
         # "notation"
-        xor|Set|quant*|Prop|prefix|parametricCoercions|opaque|nat_id*|michael|max-suc-alg|lpparse|861|infix|infer|indrec|implicitArgs[34]|group|cr_qu|cp*|coercions|plus_ac|693|693_assume|679|665|655|655b|649_fo_27|595_and_elim|584_c_slow|579_or_elim_long|579_long_no_duplicate|359|328|245|245b|244|1026|991|706|1101|1190b|1190c|1120|1247);;
+        xor|Set|quant*|Prop|prefix|parametricCoercions|opaque|nat_id*|michael|max-suc-alg|lpparse|861|infix|infer|indrec|integers|implicitArgs[34]|group|cr_qu|cp*|coercions|plus_ac|693|693_assume|679|665|655|655b|649_fo_27|595_and_elim|584_c_slow|579_or_elim_long|579_long_no_duplicate|359|328|245|245b|244|1026|991|706|1101|1190b|1190c|1120|1247);;
         # "quantifier"
         683|650|573|565|430);;
         # nested module name

but I still have the issue:

lambdapi check /tmp/tests/OK/integers.lp ...
[/private/tmp/tests/OK/integers.lp:41:13-20] No module [tests.OK] required.

fblanqui · 2025-11-27T18:10:50Z

Don't do rebasings; do merges instead. Otherwise it's problematic for those following your branch... The history does not matter so much since every thing is squashed into a single commit when I merge a PR.

fblanqui · 2025-11-27T18:14:39Z

Hi. There are still some problems: 1) you changed the sig_state type but you shouldn't, 2) your get does not follow the code I proposed which takes care of path aliases, 3) don't use optional arguments in get; this is not useful here.

NotBad4U · 2025-11-27T18:26:02Z

you changed the sig_state type but you shouldn't

What do you mean? You even mention that we should do that in issue #1268

changing in the sig_state the type of the builtins field from sym StrMap.t to sym StrMap.t PathMap.t.

your get does not follow the code I proposed which takes care of path aliases

I will fix that

don't use optional arguments in get; this is not useful here.
But it is necessary because there is some previous code, such as the one below (in command.ml), that is not passing any opt or path

((StrMap.find "nat_succ" ss.builtins).sym_type)

fblanqui · 2025-11-27T18:33:41Z

you changed the sig_state type but you shouldn't

What do you mean? You even mention that we should do that in issue #1268

changing in the sig_state the type of the builtins field from sym StrMap.t to sym StrMap.t PathMap.t.

Right but I changed my mind: I don't think that this is necessary anymore.

your get does not follow the code I proposed which takes care of path aliases

I will fix that

Thanks.

don't use optional arguments in get; this is not useful here.
But it is necessary because there is some previous code, such as the one below (in command.ml), that is not passing any opt or path
((StrMap.find "nat_succ" ss.builtins).sym_type)

But there is no need to change that part of the code.

NotBad4U · 2025-11-27T18:41:05Z

Or I do not understand a point, or it will not work if we do not change the type of sig_state .
Imagine someone has two files:
A first file Nat.lp

builtin "0" ≔ _0;
builtin "1" ≔ _1;
builtin "2" ≔ _2;

and a second one Z.lp

builtin "0" ≔ Z0;
builtin "1" ≔ _1;
builtin "2" ≔ _2;

Then, if we have the sig_state with builtins: sym StrMap.t, adding the new builtins "0", "1", etc. from Z.lp will replace the one from Nat.lp. The example above is the current situation of the Standard library.

fblanqui · 2025-11-27T18:44:55Z

Yes. Actually, it will depend on the order of require's. But it will always be possible to write Nat.1. Isn't it what we want?

NotBad4U · 2025-11-27T18:49:52Z

let sign =
   try Path.Map.find (StrMap.find m ss.alias_path) !loaded
     with _ -> assert false (* Should not happen. *)
       in
       (* Look for the symbol. *)
       StrMap.find !(sign.sign_builtins) name

So this loaded is a pointer that contains all the signatures of each different module?
And what do you want to do is that when you have a path, you find the correct signature related to this path and then look at is builtin? If that is case then yeah I guess it will works.

fblanqui · 2025-11-27T18:52:56Z

But Print.builtin needs to be modified to prefix the generated decimal number by the appropriate path. Problem: what is the appropriate path? It should be added in some of the constructors of the notation data type.

fblanqui · 2025-11-27T18:55:37Z

So this loaded is a pointer that contains all the signatures of each different module?

Yes.

And what do you want to do is that when you have a path, you find the correct signature related to this path and then look at is builtin? If that is case then yeah I guess it will works.

Yes.

fblanqui · 2025-11-27T19:01:05Z

I added a todo list at the top.

NotBad4U changed the title ~~[WIP] Allow decimal notation for multiple types by scoping builtin map…~~ Allow decimal notation for multiple types by scoping builtin map… Nov 26, 2025

fblanqui requested changes Nov 26, 2025

View reviewed changes

NotBad4U added 4 commits November 27, 2025 10:57

Fix: Allow decimal notation for multiple types by scoping builtin map…

da395fe

…pings

modify the find_builtin function to prioritize the current signature'…

aa44438

…s path first, then search through all other modules

Refactor builtin lookup to use unified API with optional parameters

f078c81

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 .

NotBad4U force-pushed the update-decimal-notation branch from a34071c to f078c81 Compare November 27, 2025 17:22

Allow decimal notation for multiple types by scoping builtin map… #1326

Are you sure you want to change the base?

Allow decimal notation for multiple types by scoping builtin map… #1326

Uh oh!

Conversation

NotBad4U commented Nov 26, 2025 • edited by fblanqui Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

NotBad4U commented Nov 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

NotBad4U commented Nov 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

fblanqui left a comment

Choose a reason for hiding this comment

Uh oh!

fblanqui Nov 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

fblanqui Nov 26, 2025

Choose a reason for hiding this comment

Uh oh!

NotBad4U Nov 26, 2025

Choose a reason for hiding this comment

Uh oh!

fblanqui Nov 26, 2025

Choose a reason for hiding this comment

Uh oh!

fblanqui Nov 26, 2025

Choose a reason for hiding this comment

Uh oh!

fblanqui Nov 26, 2025

Choose a reason for hiding this comment

Uh oh!

NotBad4U commented Nov 26, 2025

Uh oh!

fblanqui commented Nov 26, 2025

Uh oh!

NotBad4U commented Nov 27, 2025

Uh oh!

NotBad4U commented Nov 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

fblanqui commented Nov 27, 2025

Uh oh!

fblanqui commented Nov 27, 2025

Uh oh!

NotBad4U commented Nov 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

fblanqui commented Nov 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

NotBad4U commented Nov 27, 2025

Uh oh!

fblanqui commented Nov 27, 2025

Uh oh!

NotBad4U commented Nov 27, 2025

Uh oh!

fblanqui commented Nov 27, 2025

Uh oh!

fblanqui commented Nov 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

fblanqui commented Nov 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

NotBad4U commented Nov 26, 2025 •

edited by fblanqui

Loading

NotBad4U commented Nov 26, 2025 •

edited

Loading

NotBad4U commented Nov 26, 2025 •

edited

Loading

fblanqui Nov 26, 2025 •

edited

Loading

NotBad4U commented Nov 27, 2025 •

edited

Loading

NotBad4U commented Nov 27, 2025 •

edited

Loading

fblanqui commented Nov 27, 2025 •

edited

Loading

fblanqui commented Nov 27, 2025 •

edited

Loading