Merge pull request #372 from Janno/janno/fix-extend-signature

Update symbols and index when extending with a signature

Author: gares

CHANGES.md

@@ -1,3 +1,10 @@
+# v3.4.1 (September 2025)
+
+Requires Menhir 20211230 and OCaml 4.13 or above.
+
+- Compiler:
+  - Fix extend_signature, was not updating the symbol table
+
 # v3.4.0 (September 2025)
 
 - Parser:

src/compiler/compiler.ml

@@ -2021,6 +2021,25 @@ let extend1_signature base_signature (signature : checked_compilation_unit_signa
 
   { Assembled.kinds; types; type_abbrevs; toplevel_macros }
 
+let new_symbols_of_types ~(base_sig:checked_compilation_unit_signature) new_types =
+  let symbs = TypingEnv.all_symbols new_types in
+  symbs |> List.filter_map (fun (symb,m) -> if TypingEnv.mem_symbol base_sig.types symb then None else Some symb),
+  symbs |> List.filter_map (fun (symb, { TypingEnv.indexing } ) -> match indexing with Index m -> Some (symb, m) | _ -> None)
+
+let allocate_new_symbols state ~symbols ~new_defined_symbols =
+  (* THE MISTERY: allocating symbols following their declaration order makes the grundlagen job 30% faster (600M less memory):
+          time   typchk wall   mem
+    with: 14.75   0.53  16.69 2348.4M
+    wout: 19.61   0.56  21.72 2789.1M 
+  *)
+  let new_defined_symbols =
+    if List.length new_defined_symbols > 2000 then
+      new_defined_symbols |> List.sort (fun s1 s2 -> compare (Symbol.get_loc s1).line (Symbol.get_loc s2).line)
+    else
+      new_defined_symbols in
+  List.fold_left (fun symbols s -> SymbolMap.allocate_global_symbol state symbols s |> fst)
+    symbols new_defined_symbols
+
 let extend1 flags (state, base) unit =
 
   let signature =
@@ -2033,25 +2052,9 @@ let extend1 flags (state, base) unit =
 
   (* Format.eprintf "extend %a\n%!" (F.Map.pp (fun _ _ -> ())) types_indexing; *)
 
-  let new_defined_symbols, new_indexable =
-    let symbs = TypingEnv.all_symbols new_types in
-    symbs |> List.filter_map (fun (symb,m) -> if TypingEnv.mem_symbol bsig.types symb then None else Some symb),
-    symbs |> List.filter_map (fun (symb, { TypingEnv.indexing } ) -> match indexing with Index m -> Some (symb, m) | _ -> None) in
-
-  let symbols =
-    (* THE MISTERY: allocating symbols following their declaration order makes the grundlagen job 30% faster (600M less memory):
-            time   typchk wall   mem
-      with: 14.75   0.53  16.69 2348.4M
-      wout: 19.61   0.56  21.72 2789.1M 
-    *)
-    let new_defined_symbols =
-      if List.length new_defined_symbols > 2000 then
-        new_defined_symbols |> List.sort (fun s1 s2 -> compare (Symbol.get_loc s1).line (Symbol.get_loc s2).line)
-      else
-        new_defined_symbols in
-    List.fold_left (fun symbols s -> SymbolMap.allocate_global_symbol state symbols s |> fst)
-      symbols new_defined_symbols in
+  let new_defined_symbols, new_indexable = new_symbols_of_types ~base_sig:bsig new_types  in
 
+  let symbols = allocate_new_symbols state ~symbols ~new_defined_symbols in
 
   let prolog_program, indexing = update_indexing state symbols prolog_program new_indexable indexing in
   (* Format.eprintf "extended\n%!"; *)
@@ -2081,11 +2084,15 @@ let extend1 flags (state, base) unit =
   let hash = hash_base base in
   state, { base with hash }
 
-  let extend flags state assembled u = extend1 flags (state, assembled) u
-  let extend_signature state assembled u =
-    let signature = extend1_signature assembled.Assembled.signature u in
-    let base = { assembled with signature } in
-    state, { base with hash = hash_base base }
+let extend flags state assembled u = extend1 flags (state, assembled) u
+let extend_signature state assembled u =
+  let signature = extend1_signature assembled.Assembled.signature u in
+  let base_sig = assembled.Assembled.signature in
+  let new_defined_symbols, new_indexable = new_symbols_of_types ~base_sig signature.types in
+  let symbols = allocate_new_symbols state ~symbols:assembled.symbols ~new_defined_symbols in
+  let prolog_program, indexing = update_indexing state symbols assembled.prolog_program new_indexable assembled.indexing in
+  let base = { assembled with symbols; prolog_program; indexing; signature } in
+  state, { base with hash = hash_base base }
 
   let compile_query state { Assembled.symbols; builtins; signature = { types; type_abbrevs } } (needs_spilling,t) =
     let (symbols, amap), t = spill_todbl ~builtins ~needs_spilling ~types ~type_abbrevs state symbols t in

tests/sources/dune

@@ -15,4 +15,6 @@
 (executable (name sepcomp_perf5) (modules sepcomp_perf5) (libraries sepcomp))
 (executable (name sepcomp_tyid)  (modules sepcomp_tyid)  (libraries sepcomp))
 (executable (name sepcomp_tyid2)  (modules sepcomp_tyid2)  (libraries sepcomp))
-(executable (name sepcomp_hover)  (modules sepcomp_hover)  (libraries sepcomp))
+(executable (name sepcomp_hover)  (modules sepcomp_hover)  (libraries sepcomp))
+(executable (name sepcomp_extend_sig)  (modules sepcomp_extend_sig)  (libraries sepcomp))
+(executable (name sepcomp_extend_sig2)  (modules sepcomp_extend_sig2)  (libraries sepcomp))

tests/sources/sepcomp_extend_sig.ml

@@ -0,0 +1,28 @@
+let u = {|
+
+pred p i:int.
+p 2 :- !, fail.
+
+|}
+;;
+
+let v = {|
+
+p _.
+
+main :- p 2.
+
+|}
+;;
+
+let () =
+  let open Sepcomp.Sepcomp_template in
+  let elpi = init () in
+  let flags = Elpi.API.Compile.default_flags in
+  let base = Elpi.API.Compile.empty_base ~elpi in
+  let _, u = cc ~elpi ~flags ~base 0 u in
+  let su = signature_of u in
+  let p = extend_signature ~flags ~base su in
+  let p, _ = cc ~elpi ~flags ~base:p 0 v in
+  let q = query ~elpi p in
+  exec q

tests/sources/sepcomp_extend_sig2.ml

@@ -0,0 +1,32 @@
+let u = {|
+
+pred p i:int.
+p 2 :- !, fail.
+
+|}
+;;
+
+let v = {|
+
+p _.
+main :- p 2.
+
+|}
+;;
+
+let () =
+  let open Sepcomp.Sepcomp_template in
+  let elpi = init () in
+  let flags = Elpi.API.Compile.default_flags in
+  let base = Elpi.API.Compile.empty_base ~elpi in
+  let _, u = cc ~elpi ~flags ~base 0 u in
+  let su = signature_of u in
+  let base = extend_signature ~flags ~base su in
+  let base = extend ~flags ~base u in
+  let base, _ = cc ~elpi ~flags ~base 0 v in
+  let q = query ~elpi base in
+  assert(try_exec q = false);
+  let base, _ = cc ~elpi ~flags ~base 0 "fail." in
+  let q = query ~elpi base in
+  exec q
+

tests/sources/sepcomp_template.ml

@@ -11,6 +11,10 @@ let cc ~elpi ~flags ~base i u =
         (Lexing.from_string u))) in
   Compile.extend ~flags ~base u, u
 
+let signature_of u = Compile.signature u
+
+let extend ~flags ~base u = Compile.extend ~flags ~base u
+let extend_signature ~flags ~base u = Compile.extend_signature ~flags ~base u
 
 let check q =
   ()
@@ -28,6 +32,13 @@ let exec q =
     | Execute.Success _ -> exit 0
     | Execute.NoMoreSteps -> assert false
 
+let try_exec q =
+    let exe = Compile.optimize q in
+    match Execute.once exe with
+    | Execute.Failure -> false
+    | Execute.Success _ -> true
+    | Execute.NoMoreSteps -> assert false
+    
 let main us =
   let elpi = init () in
   let flags = Compile.default_flags in

tests/suite/elpi_api.ml

@@ -66,3 +66,15 @@ let () = declare "sepcomp_hover"
   ~expectation:Test.Success
   ()
 
+let () = declare "sepcomp_extend_sig"
+  ~source_dune:"sepcomp_extend_sig.exe"
+  ~description:"extend unit with signature"
+  ~expectation:Test.Success
+  ()
+
+let () = declare "sepcomp_extend_sig2"
+  ~source_dune:"sepcomp_extend_sig2.exe"
+  ~description:"extend unit with signature then code"
+  ~expectation:Test.Success
+  ()
+