From fb9e16bf32ce7e3fcb224bd7f1669df32710dce1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 24 Jul 2024 16:26:55 +0200 Subject: [PATCH 1/6] Only keep symbols with positive constants in pruned tables. The term is only used in this situation. --- src/compiler.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/compiler.ml b/src/compiler.ml index 0de1bdca8..3405c4951 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -107,7 +107,7 @@ type table = { type pruned_table = { c2s0 : string D.Constants.Map.t; - c2t0 : D.term D.Constants.Map.t; + c2t0 : D.term option D.Constants.Map.t; } [@@deriving show] let locked { locked } = locked @@ -122,10 +122,10 @@ let symbols { c2s0 } = List.map (fun (c,s) -> s ^ ":" ^ string_of_int c) (D.Constants.Map.bindings c2s0) let prune t ~alive = - { - c2s0 = D.Constants.Map.filter (fun k _ -> D.Constants.Set.mem k alive) t.c2s; - c2t0 = D.Constants.Map.filter (fun k _ -> D.Constants.Set.mem k alive) t.c2t; - } + let c2s0 = D.Constants.Map.filter (fun k _ -> D.Constants.Set.mem k alive) t.c2s in + let c2t0 = D.Constants.Map.filter (fun k _ -> D.Constants.Set.mem k alive) t.c2t in + let c2t0 = D.Constants.Map.mapi (fun k t -> if k < 0 then None else Some t) c2t0 in + { c2s0; c2t0 } let table = D.State.declare ~descriptor:D.elpi_state_descriptor @@ -265,10 +265,11 @@ let build_shift ?(lock_base=false) ~flags:{ print_units } ~base symbols = else if Map.mem v base.c2t then acc else + let t = match t with None -> assert false | Some t -> t in let base = { base with c2t = Map.add v t base.c2t } in base, shift ) - (base,Map.empty) (List.rev (Map.bindings symbols.c2t0))) + (base,Map.empty) (List.rev (Map.bindings symbols.c2t0))) let build_shift ?lock_base ~flags ~base symbols = try Stdlib.Result.Ok (build_shift ?lock_base ~flags ~base symbols) From e0c2f6a363db6aadd70c6cfaecdd4d098229eddd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 24 Jul 2024 22:42:57 +0200 Subject: [PATCH 2/6] Slightly more compact representation of pruned symbols. No need to keep a map as we never access this data by indexing but merely fold over it. --- src/compiler.ml | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/src/compiler.ml b/src/compiler.ml index 3405c4951..3984a7050 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -105,9 +105,14 @@ type table = { uuid : Util.UUID.t; } [@@deriving show] +type entry = +| ENeg of D.constant +| EPos of D.constant * D.term +[@@deriving show] + type pruned_table = { c2s0 : string D.Constants.Map.t; - c2t0 : D.term option D.Constants.Map.t; + c2t0 : entry array; } [@@deriving show] let locked { locked } = locked @@ -116,7 +121,7 @@ let uuid { uuid } = uuid let equal t1 t2 = locked t1 && locked t2 && uuid t1 = uuid t2 -let size t = D.Constants.Map.cardinal t.c2t0 +let size t = Array.length t.c2t0 let symbols { c2s0 } = List.map (fun (c,s) -> s ^ ":" ^ string_of_int c) (D.Constants.Map.bindings c2s0) @@ -124,7 +129,8 @@ let symbols { c2s0 } = let prune t ~alive = let c2s0 = D.Constants.Map.filter (fun k _ -> D.Constants.Set.mem k alive) t.c2s in let c2t0 = D.Constants.Map.filter (fun k _ -> D.Constants.Set.mem k alive) t.c2t in - let c2t0 = D.Constants.Map.mapi (fun k t -> if k < 0 then None else Some t) c2t0 in + let c2t0 = D.Constants.Map.mapi (fun k t -> if k < 0 then ENeg k else EPos (k, t)) c2t0 in + let c2t0 = Array.of_list @@ List.rev_map snd @@ D.Constants.Map.bindings c2t0 in { c2s0; c2t0 } let table = D.State.declare @@ -247,10 +253,11 @@ let build_shift ?(lock_base=false) ~flags:{ print_units } ~base symbols = (* We try hard to respect the same order if possible, since some tests (grundlagen) depend on this order (for performance, the constant-timestamp heuristic in unfolding) *) - List.fold_left (fun (base,shift as acc) (v, t) -> - if v < 0 then + Array.fold_left (fun (base,shift as acc) e -> + match e with + | ENeg v -> let name = Map.find v symbols.c2s0 in - try + begin try let c, _ = F.Map.find (F.from_string name) base.ast2ct in if c == v then acc else begin @@ -262,14 +269,14 @@ let build_shift ?(lock_base=false) ~flags:{ print_units } ~base symbols = | Not_found -> let base, (c,_) = allocate_global_symbol_aux (Ast.Func.from_string name) base in base, Map.add v c shift - else + end + | EPos (v, t) -> if Map.mem v base.c2t then acc else - let t = match t with None -> assert false | Some t -> t in let base = { base with c2t = Map.add v t base.c2t } in base, shift ) - (base,Map.empty) (List.rev (Map.bindings symbols.c2t0))) + (base,Map.empty) symbols.c2t0) let build_shift ?lock_base ~flags ~base symbols = try Stdlib.Result.Ok (build_shift ?lock_base ~flags ~base symbols) From fbbb8439bb8e11e9083d3b521e92640fae702f0f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Thu, 25 Jul 2024 01:00:24 +0200 Subject: [PATCH 3/6] Do not store live symbols in Flat programs. --- src/compiler.ml | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/src/compiler.ml b/src/compiler.ml index 3984a7050..3c1b976dc 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -546,7 +546,6 @@ type program = { clauses : (preterm,Ast.Structured.attribute) Ast.Clause.t list; chr : (constant list * prechr_rule list) list; local_names : int; - symbols : C.Set.t; toplevel_macros : macro_declaration; } @@ -1510,7 +1509,7 @@ module Flatten : sig (* Eliminating the structure (name spaces) *) - val run : State.t -> Structured.program -> Flat.program + val run : State.t -> Structured.program -> C.Set.t * Flat.program val relocate : State.t -> D.constant D.Constants.Map.t -> Flat.program -> Flat.program val relocate_term : State.t -> D.constant D.Constants.Map.t -> term -> term @@ -1709,14 +1708,13 @@ let subst_amap state f { nargs; c2i; i2n; n2t; n2i } = let modes = apply_subst_modes ~live_symbols empty_subst modes in let types, type_abbrevs, modes, clauses, chr = compile_body live_symbols state local_names types type_abbrevs modes [] [] empty_subst body in - { Flat.types; + !live_symbols, { Flat.types; type_abbrevs; modes; clauses; chr = List.rev chr; local_names; toplevel_macros; - symbols = !live_symbols } let relocate_term state s t = let ksub = apply_subst_constant ([],s) in @@ -1730,7 +1728,6 @@ let subst_amap state f { nargs; c2i; i2n; n2t; n2i } = chr; local_names; toplevel_macros; - symbols; } = let f = [], f in { @@ -1741,7 +1738,6 @@ let subst_amap state f { nargs; c2i; i2n; n2t; n2i } = chr = smart_map (apply_subst_chr state f) chr; local_names; toplevel_macros; - symbols; } @@ -2159,7 +2155,7 @@ let unit_or_header_of_ast { print_passes } s ?(toplevel_macros=F.Map.empty) p = Format.eprintf "== Structured ================@\n@[%a@]@\n" (w_symbol_table s Structured.pp_program) p; - let p = Flatten.run s p in + let alive, p = Flatten.run s p in if print_passes then Format.eprintf "== Flat ================@\n@[%a@]@\n" @@ -2168,7 +2164,7 @@ let unit_or_header_of_ast { print_passes } s ?(toplevel_macros=F.Map.empty) p = s, { version = "%%VERSION_NUM%%"; code = p; - symbol_table = Symbols.prune (State.get Symbols.table s) ~alive:p.Flat.symbols + symbol_table = Symbols.prune (State.get Symbols.table s) ~alive } ;; From 9997868ac26fc7083cca317f112687b40a45156a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Thu, 25 Jul 2024 01:09:34 +0200 Subject: [PATCH 4/6] Do not store toplevel macros in Flat programs. --- src/compiler.ml | 30 ++++++++++++------------------ 1 file changed, 12 insertions(+), 18 deletions(-) diff --git a/src/compiler.ml b/src/compiler.ml index 3c1b976dc..756358f02 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -546,8 +546,6 @@ type program = { clauses : (preterm,Ast.Structured.attribute) Ast.Clause.t list; chr : (constant list * prechr_rule list) list; local_names : int; - - toplevel_macros : macro_declaration; } [@@deriving show] @@ -591,7 +589,7 @@ type compilation_unit = { type builtins = string * Data.BuiltInPredicate.declaration list -type header = State.t * compilation_unit +type header = State.t * compilation_unit * macro_declaration type program = State.t * Assembled.program @@ -1509,7 +1507,7 @@ module Flatten : sig (* Eliminating the structure (name spaces) *) - val run : State.t -> Structured.program -> C.Set.t * Flat.program + val run : State.t -> Structured.program -> C.Set.t * macro_declaration * Flat.program val relocate : State.t -> D.constant D.Constants.Map.t -> Flat.program -> Flat.program val relocate_term : State.t -> D.constant D.Constants.Map.t -> term -> term @@ -1708,13 +1706,12 @@ let subst_amap state f { nargs; c2i; i2n; n2t; n2i } = let modes = apply_subst_modes ~live_symbols empty_subst modes in let types, type_abbrevs, modes, clauses, chr = compile_body live_symbols state local_names types type_abbrevs modes [] [] empty_subst body in - !live_symbols, { Flat.types; + !live_symbols, toplevel_macros, { Flat.types; type_abbrevs; modes; clauses; chr = List.rev chr; local_names; - toplevel_macros; } let relocate_term state s t = let ksub = apply_subst_constant ([],s) in @@ -1727,7 +1724,6 @@ let subst_amap state f { nargs; c2i; i2n; n2t; n2i } = clauses; chr; local_names; - toplevel_macros; } = let f = [], f in { @@ -1737,7 +1733,6 @@ let subst_amap state f { nargs; c2i; i2n; n2t; n2i } = clauses = apply_subst_clauses state f clauses; chr = smart_map (apply_subst_chr state f) chr; local_names; - toplevel_macros; } @@ -2082,7 +2077,7 @@ let assemble flags state code (ul : compilation_unit list) = let state, clauses_rev, types, type_abbrevs, modes, chr_rev = List.fold_left (fun (state, cl1, t1, ta1, m1, c1) ({ symbol_table; code } as _u) -> - let state, { Flat.clauses = cl2; types = t2; type_abbrevs = ta2; modes = m2; chr = c2; toplevel_macros = _ } = + let state, { Flat.clauses = cl2; types = t2; type_abbrevs = ta2; modes = m2; chr = c2; } = let state, shift = Stdlib.Result.get_ok @@ Symbols.build_shift ~flags ~base:state symbol_table in let code = if C.Map.is_empty shift then code @@ -2155,7 +2150,7 @@ let unit_or_header_of_ast { print_passes } s ?(toplevel_macros=F.Map.empty) p = Format.eprintf "== Structured ================@\n@[%a@]@\n" (w_symbol_table s Structured.pp_program) p; - let alive, p = Flatten.run s p in + let alive, toplevel_macros, p = Flatten.run s p in if print_passes then Format.eprintf "== Flat ================@\n@[%a@]@\n" @@ -2165,7 +2160,7 @@ let unit_or_header_of_ast { print_passes } s ?(toplevel_macros=F.Map.empty) p = version = "%%VERSION_NUM%%"; code = p; symbol_table = Symbols.prune (State.get Symbols.table s) ~alive - } + }, toplevel_macros ;; let print_unit { print_units } x = @@ -2208,17 +2203,16 @@ let header_of_ast ~flags ~parser:p state_descriptor quotation_descriptor hoas_de | Data.BuiltInPredicate.MLDataC _ -> state | Data.BuiltInPredicate.LPCode _ -> state | Data.BuiltInPredicate.LPDoc _ -> state) state decls) state builtins in - let state, u = unit_or_header_of_ast flags state ast in + let state, u, toplevel_macros = unit_or_header_of_ast flags state ast in print_unit flags u; - state, u + state, u, toplevel_macros -let unit_of_ast ~flags ~header:(s, (header : compilation_unit)) p : compilation_unit = - let toplevel_macros = header.code.Flat.toplevel_macros in - let _, u = unit_or_header_of_ast flags s ~toplevel_macros p in +let unit_of_ast ~flags ~header:(s, (header : compilation_unit), toplevel_macros) p : compilation_unit = + let _, u, _ = unit_or_header_of_ast flags s ~toplevel_macros p in print_unit flags u; u -let assemble_units ~flags ~header:(s,h) units : program = +let assemble_units ~flags ~header:(s,h,toplevel_macros) units : program = let nunits_with_locals = (h :: units) |> List.filter (fun {code = { Flat.local_names = x }} -> x > 0) |> List.length in @@ -2226,7 +2220,7 @@ let assemble_units ~flags ~header:(s,h) units : program = if nunits_with_locals > 0 then error "Only 1 compilation unit is supported when local directives are used"; - let init = { Assembled.empty with toplevel_macros = h.code.toplevel_macros; local_names = h.code.local_names } in + let init = { Assembled.empty with toplevel_macros; local_names = h.code.local_names } in let s, p = Assemble.assemble flags s init (h :: units) in From 17a4555f7fd14cc6591ee7825b941f24fbc7c536 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Thu, 25 Jul 2024 13:30:12 +0200 Subject: [PATCH 5/6] More compact representation of pruned symbol tables. --- src/compiler.ml | 33 ++++++++++++++++++--------------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/src/compiler.ml b/src/compiler.ml index 756358f02..2a3d703de 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -106,14 +106,11 @@ type table = { } [@@deriving show] type entry = -| ENeg of D.constant +| ENeg of D.constant * string | EPos of D.constant * D.term [@@deriving show] -type pruned_table = { - c2s0 : string D.Constants.Map.t; - c2t0 : entry array; -} [@@deriving show] +type pruned_table = entry array [@@deriving show] let locked { locked } = locked let lock t = { t with locked = true } @@ -121,17 +118,24 @@ let uuid { uuid } = uuid let equal t1 t2 = locked t1 && locked t2 && uuid t1 = uuid t2 -let size t = Array.length t.c2t0 +let size t = Array.length t -let symbols { c2s0 } = - List.map (fun (c,s) -> s ^ ":" ^ string_of_int c) (D.Constants.Map.bindings c2s0) +let symbols table = + let map = function + | ENeg (c, s) -> Some (s ^ ":" ^ string_of_int c) + | EPos _ -> None + in + List.rev @@ List.filter_map map @@ Array.to_list table let prune t ~alive = - let c2s0 = D.Constants.Map.filter (fun k _ -> D.Constants.Set.mem k alive) t.c2s in + let c2s = t.c2s in let c2t0 = D.Constants.Map.filter (fun k _ -> D.Constants.Set.mem k alive) t.c2t in - let c2t0 = D.Constants.Map.mapi (fun k t -> if k < 0 then ENeg k else EPos (k, t)) c2t0 in - let c2t0 = Array.of_list @@ List.rev_map snd @@ D.Constants.Map.bindings c2t0 in - { c2s0; c2t0 } + let map k t = + if k < 0 then ENeg (k, D.Constants.Map.find k c2s) + else EPos (k, t) + in + let c2t0 = D.Constants.Map.mapi map c2t0 in + Array.of_list @@ List.rev_map snd @@ D.Constants.Map.bindings c2t0 let table = D.State.declare ~descriptor:D.elpi_state_descriptor @@ -255,8 +259,7 @@ let build_shift ?(lock_base=false) ~flags:{ print_units } ~base symbols = heuristic in unfolding) *) Array.fold_left (fun (base,shift as acc) e -> match e with - | ENeg v -> - let name = Map.find v symbols.c2s0 in + | ENeg (v, name) -> begin try let c, _ = F.Map.find (F.from_string name) base.ast2ct in if c == v then acc @@ -276,7 +279,7 @@ let build_shift ?(lock_base=false) ~flags:{ print_units } ~base symbols = let base = { base with c2t = Map.add v t base.c2t } in base, shift ) - (base,Map.empty) symbols.c2t0) + (base, Map.empty) symbols) let build_shift ?lock_base ~flags ~base symbols = try Stdlib.Result.Ok (build_shift ?lock_base ~flags ~base symbols) From f6e85a795079ac447b4fbf5abaa537ab97c0f1f5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Thu, 25 Jul 2024 15:34:49 +0200 Subject: [PATCH 6/6] More informative names for the constructors of Compiler.Symbols.entry. --- src/compiler.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/compiler.ml b/src/compiler.ml index 2a3d703de..c50dfc2f4 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -106,8 +106,8 @@ type table = { } [@@deriving show] type entry = -| ENeg of D.constant * string -| EPos of D.constant * D.term +| GlobalSymbol of D.constant * string +| BoundVariable of D.constant * D.term [@@deriving show] type pruned_table = entry array [@@deriving show] @@ -122,8 +122,8 @@ let size t = Array.length t let symbols table = let map = function - | ENeg (c, s) -> Some (s ^ ":" ^ string_of_int c) - | EPos _ -> None + | GlobalSymbol (c, s) -> Some (s ^ ":" ^ string_of_int c) + | BoundVariable _ -> None in List.rev @@ List.filter_map map @@ Array.to_list table @@ -131,8 +131,8 @@ let prune t ~alive = let c2s = t.c2s in let c2t0 = D.Constants.Map.filter (fun k _ -> D.Constants.Set.mem k alive) t.c2t in let map k t = - if k < 0 then ENeg (k, D.Constants.Map.find k c2s) - else EPos (k, t) + if k < 0 then GlobalSymbol (k, D.Constants.Map.find k c2s) + else BoundVariable (k, t) in let c2t0 = D.Constants.Map.mapi map c2t0 in Array.of_list @@ List.rev_map snd @@ D.Constants.Map.bindings c2t0 @@ -259,7 +259,7 @@ let build_shift ?(lock_base=false) ~flags:{ print_units } ~base symbols = heuristic in unfolding) *) Array.fold_left (fun (base,shift as acc) e -> match e with - | ENeg (v, name) -> + | GlobalSymbol (v, name) -> begin try let c, _ = F.Map.find (F.from_string name) base.ast2ct in if c == v then acc @@ -273,7 +273,7 @@ let build_shift ?(lock_base=false) ~flags:{ print_units } ~base symbols = let base, (c,_) = allocate_global_symbol_aux (Ast.Func.from_string name) base in base, Map.add v c shift end - | EPos (v, t) -> + | BoundVariable (v, t) -> if Map.mem v base.c2t then acc else let base = { base with c2t = Map.add v t base.c2t } in