From c88b410bfaf8d232402511b81e88625309c42412 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 5 Jul 2015 14:36:36 +0000 Subject: [PATCH] more flexibility in the exported data for Teyjus --- helm/software/helena/Makefile | 4 +- helm/software/helena/profile.txt | 8 +-- helm/software/helena/src/basic_rg/brgLP.ml | 62 ++++++++++++++-------- 3 files changed, 46 insertions(+), 28 deletions(-) diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 137084bf9..02604aae8 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -155,8 +155,8 @@ export-lp2 lp/$(LP2): $(MAIN).opt etc $(H)./$(MAIN).opt -a n -m LP2 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt export-tj2 lp/$(TJ2): $(MAIN).opt etc - @echo " HELENA -l -m TJ2 -u $(INPUT)" - $(H)./$(MAIN).opt -a n -e 253 -m TJ2 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt + @echo " HELENA -m TJ2 $(INPUT)" + $(H)./$(MAIN).opt -a n -m TJ2 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt export-tj3 lp/$(TJ3): $(MAIN).opt etc @echo " HELENA -m TJ3 $(INPUT)" diff --git a/helm/software/helena/profile.txt b/helm/software/helena/profile.txt index 65c909fe6..a0ff3f28c 100644 --- a/helm/software/helena/profile.txt +++ b/helm/software/helena/profile.txt @@ -10,11 +10,11 @@ coqtop.opt : 27.73 to 28.07 ages coqtop.opt : 28.64 to 28.83 reversed ages -elpi : 00.19 to 00.20 exex, 253 lines -elpi : 00.26 to 00.28 user, 253 lines +elpi : 00.20 to 00.22 exex, 255 lines +elpi : 00.27 to 00.31 user, 255 lines -teyjus : 02.03 to 02.18 exec, 253 lines -teyjus : 01.63 to 01.68 link, 253 lines +teyjus : 02.13 to 02.26 exec, 255 lines +teyjus : 03.24 to 03.31 link, 255 lines elpi : 21.15 to 21.45 exec, full elpi : 27.52 to 27.82 user, full diff --git a/helm/software/helena/src/basic_rg/brgLP.ml b/helm/software/helena/src/basic_rg/brgLP.ml index 1eb1bae3d..9b832b20e 100644 --- a/helm/software/helena/src/basic_rg/brgLP.ml +++ b/helm/software/helena/src/basic_rg/brgLP.ml @@ -26,9 +26,11 @@ IFDEF MANAGER THEN let ok = ref true +let uris = ref [] + let top_age = 7000 -let uris = ref [] +let size = 16 let base = "lp" @@ -183,22 +185,27 @@ let output_entity_tj2 och st (_, na, u, b) = end else !ok let close_out_tj2 och () = - let aux_name (b, u) = + let out_name (b, u) = let gde = if b then "gdef+2" else "gdec+2" in KP.fprintf och "(%s %a\n" gde out_uri u in - let aux_sep _ = KP.fprintf och "%s" ")" in - if !G.first > 0 then begin - let s = KP.sprintf "tv+c C T :- $lt C c+%u, !." !G.first in - out_clause och s; - out_clause och "tv+c C T :- tv+ T." - end; + let rec out_pars och p = + if p > 0 then begin KP.fprintf och "%s" ")"; out_pars och (pred p) end + in + let rec out_list och chunk pars first items uris = match first, items, uris with + | true, _, _ -> + KP.fprintf och "g+list %u\n" chunk; + out_list och (succ chunk) pars false items uris + | false, _, [] -> KP.fprintf och "gtop%a.\n\n" out_pars pars + | false, 0, _ -> + KP.fprintf och "(genv %u)%a.\n\n" chunk out_pars pars; + out_list och chunk 0 true size uris + | false, _, hd :: tl -> + out_name hd; out_list och chunk (succ pars) false (pred items) tl + in + out_list och 1 0 true size (List.rev !uris); out_clause och "main :- grundlagen."; - out_clause och "grundlagen :- gv+"; - List.iter aux_name (List.rev !uris); - KP.fprintf och "%s" "gtop"; - List.iter aux_sep !uris; - out_clause och "\n\n."; + out_clause och "grundlagen :- gv+ (genv 1)."; close_out och (* teyjus variant 3 *************************************************) @@ -226,18 +233,29 @@ let output_entity_tj3 och st (_, na, u, b) = end else !ok let close_out_tj3 och () = - let aux_name (_, u) = + let out_name (_, u) = KP.fprintf och "gv+3 %a,\n" out_uri u in - if !G.first > 0 then begin - let s = KP.sprintf "tv+c C T :- $lt C c+%u, !." !G.first in - out_clause och s; - out_clause och "tv+c C T :- tv+ T." - end; + let rec out_list och chunk first items uris = match first, items, uris with + | true, _, _ -> + KP.fprintf och "chunk %u :-\n" chunk; + out_list och (succ chunk) false items uris + | false, _, [] -> KP.fprintf och "!.\n\n"; chunk + | false, 0, _ -> + KP.fprintf och "!.\n\n"; + out_list och chunk true size uris + | false, _, hd :: tl -> + out_name hd; out_list och chunk false (pred items) tl + in + let rec out_chunks och chunks c = + if chunks < c then out_clause och "!." else begin + KP.fprintf och "chunk %u,\n" c; out_chunks och chunks (succ c) + end + in + let chunks = out_list och 1 true size (List.rev !uris) in out_clause och "main :- grundlagen."; - out_clause och "grundlagen :-"; - List.iter aux_name (List.rev !uris); - out_clause och "!."; + KP.fprintf och "grundlagen :-\n"; + out_chunks och (pred chunks) 1; close_out och (* Interface functions ******************************************************) -- 2.39.2