From 98fef490e55d1d780e8c0bb19de0218e08ae73b1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 25 Jun 2015 19:00:51 +0000 Subject: [PATCH] advances on exportation to prolog --- helm/software/helena/.depend.opt | 18 +-- helm/software/helena/Makefile | 40 ++++-- .../{elpi/elpi.template => lp/lp.template} | 0 helm/software/helena/src/basic_rg/Make | 2 +- .../src/basic_rg/{brgELPI.ml => brgLP.ml} | 134 +++++++++++++++--- .../src/basic_rg/{brgELPI.mli => brgLP.mli} | 8 +- helm/software/helena/src/common/options.ml | 6 +- helm/software/helena/src/modules.ml | 2 +- helm/software/helena/src/toplevel/top.ml | 22 +-- 9 files changed, 176 insertions(+), 56 deletions(-) rename helm/software/helena/{elpi/elpi.template => lp/lp.template} (100%) rename helm/software/helena/src/basic_rg/{brgELPI.ml => brgLP.ml} (56%) rename helm/software/helena/src/basic_rg/{brgELPI.mli => brgLP.mli} (80%) diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index ae5016a32..7babc30d3 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -193,13 +193,13 @@ src/basic_rg/brgGallina.cmo : src/common/options.cmx src/common/layer.cmi \ src/basic_rg/brgGallina.cmx : src/common/options.cmx src/common/layer.cmx \ src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ src/common/alpha.cmx src/basic_rg/brgGallina.cmi -src/basic_rg/brgELPI.cmi : src/basic_rg/brg.cmx -src/basic_rg/brgELPI.cmo : src/common/options.cmx src/common/layer.cmi \ +src/basic_rg/brgLP.cmi : src/basic_rg/brg.cmx +src/basic_rg/brgLP.cmo : src/common/options.cmx src/common/layer.cmi \ src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/common/alpha.cmi src/basic_rg/brgELPI.cmi -src/basic_rg/brgELPI.cmx : src/common/options.cmx src/common/layer.cmx \ + src/common/alpha.cmi src/basic_rg/brgLP.cmi +src/basic_rg/brgLP.cmx : src/common/options.cmx src/common/layer.cmx \ src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ - src/common/alpha.cmx src/basic_rg/brgELPI.cmi + src/common/alpha.cmx src/basic_rg/brgLP.cmi src/basic_ag/bag.cmo : src/lib/marks.cmi src/lib/log.cmi \ src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bag.cmx : src/lib/marks.cmx src/lib/log.cmx \ @@ -268,8 +268,8 @@ src/toplevel/top.cmo : src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ src/common/layer.cmi src/common/hierarchy.cmi src/common/entity.cmx \ src/complete_rg/crgOutput.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \ src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \ - src/basic_rg/brgOutput.cmi src/basic_rg/brgGrafite.cmi \ - src/basic_rg/brgGallina.cmi src/basic_rg/brgELPI.cmi \ + src/basic_rg/brgOutput.cmi src/basic_rg/brgLP.cmi \ + src/basic_rg/brgGrafite.cmi src/basic_rg/brgGallina.cmi \ src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \ src/basic_ag/bagUntrusted.cmi src/basic_ag/bagType.cmi \ src/basic_ag/bagOutput.cmi src/basic_ag/bagCrg.cmi src/basic_ag/bag.cmx \ @@ -283,8 +283,8 @@ src/toplevel/top.cmx : src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \ src/common/layer.cmx src/common/hierarchy.cmx src/common/entity.cmx \ src/complete_rg/crgOutput.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \ - src/basic_rg/brgOutput.cmx src/basic_rg/brgGrafite.cmx \ - src/basic_rg/brgGallina.cmx src/basic_rg/brgELPI.cmx \ + src/basic_rg/brgOutput.cmx src/basic_rg/brgLP.cmx \ + src/basic_rg/brgGrafite.cmx src/basic_rg/brgGallina.cmx \ src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \ src/basic_ag/bagUntrusted.cmx src/basic_ag/bagType.cmx \ src/basic_ag/bagOutput.cmx src/basic_ag/bagCrg.cmx src/basic_ag/bag.cmx \ diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 42cf240fc..8ae171cd0 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -13,7 +13,8 @@ CLEAN = etc/log.txt etc/profile.txt TAGS = test-si-fast test-si test2 test3 test6 \ profile-fast profile profile-coq \ xml-si xml-si-v3 xml xml-v3 \ - export-coq export-matita export-elpi \ + export-coq export-matita \ + export-lp1 export-lp2 export-tj2 export-tj3 \ matita matitac include Makefile.common @@ -30,13 +31,16 @@ INPUT = examples/automath/grundlagen_2.aut INPUTFAST = examples/automath/grundlagen_1.aut -MA = grundlagen_2.ma -V = grundlagen_2.v -ELPI = grundlagen_2.elpi +MA = grundlagen_2.ma +V = grundlagen_2.v +LP1 = grundlagen_21.elpi +LP2 = grundlagen_22.elpi +TJ2 = grundlagen_22.mod +TJ2 = grundlagen_23.mod -PREAMBLE_MA = ../matita/matita.ma.templ -PREAMBLE_V = coq/grundlagen.template -PREAMBLE_ELPI = elpi/elpi.template +PREAMBLE_MA = ../matita/matita.ma.templ +PREAMBLE_V = coq/grundlagen.template +PREAMBLE_LP = lp/lp.template test-si-fast: $(MAIN).opt etc @echo " HELENA -q -u -x -1 $(INPUTFAST)" @@ -75,20 +79,28 @@ xml-v3: $(MAIN).opt etc $(H)./$(MAIN).opt -l -u $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 2 $(INPUT) > etc/log.txt export-coq coq/$(V): $(MAIN).opt etc - $(H)mkdir -p coq @echo " HELENA -l -m V8 -u $(INPUT)" $(H)./$(MAIN).opt -T 1 -a n -l -m V8 -p $(PREAMBLE_V) -u $(O) $(INPUT) > etc/log.txt export-matita matita/$(MA): $(MAIN).opt etc @echo " HELENA -l -m MA2 -u $(INPUT)" - $(H)mkdir -p matita $(H)./$(MAIN).opt -T 1 -a n -l -m MA2 -p $(PREAMBLE_MA) -u $(O) $(INPUT) > etc/log.txt -export-elpi elpi/$(ELPI): $(MAIN).opt etc - @echo " HELENA -l -m ELPI -u $(INPUT)" - $(H)mkdir -p elpi - $(H)./$(MAIN).opt -T 1 -a n -l -m ELPI1 -p $(PREAMBLE_ELPI) -u $(O) $(INPUT) > etc/log.txt - $(H)./$(MAIN).opt -T 1 -a n -l -m ELPI2 -p $(PREAMBLE_ELPI) -u $(O) $(INPUT) >> etc/log.txt +export-lp1 lp/$(LP1): $(MAIN).opt etc + @echo " HELENA -l -m LP1 -u $(INPUT)" + $(H)./$(MAIN).opt -T 1 -a n -l -m LP1 -p $(PREAMBLE_LP) -u $(O) $(INPUT) > etc/log.txt + +export-lp2 lp/$(LP2): $(MAIN).opt etc + @echo " HELENA -l -m LP2 -u $(INPUT)" + $(H)./$(MAIN).opt -T 1 -a n -l -m LP2 -p $(PREAMBLE_LP) -u $(O) $(INPUT) > etc/log.txt + +export-tj2 lp/$(TJ2): $(MAIN).opt etc + @echo " HELENA -l -m TJ2 -u $(INPUT)" + $(H)./$(MAIN).opt -T 1 -a n -e 253 -l -m TJ2 -p $(PREAMBLE_LP) -u $(O) $(INPUT) > etc/log.txt + +export-tj3 lp/$(TJ3): $(MAIN).opt etc + @echo " HELENA -l -m TJ3 -u $(INPUT)" + $(H)./$(MAIN).opt -T 1 -a n -l -m TJ3 -p $(PREAMBLE_LP) -u $(O) $(INPUT) > etc/log.txt profile-fast: $(MAIN).opt etc @echo " HELENA -q -u -x $(INPUTFAST) (31 TIMES)" diff --git a/helm/software/helena/elpi/elpi.template b/helm/software/helena/lp/lp.template similarity index 100% rename from helm/software/helena/elpi/elpi.template rename to helm/software/helena/lp/lp.template diff --git a/helm/software/helena/src/basic_rg/Make b/helm/software/helena/src/basic_rg/Make index d230dace7..df1b318e5 100644 --- a/helm/software/helena/src/basic_rg/Make +++ b/helm/software/helena/src/basic_rg/Make @@ -1,3 +1,3 @@ brg brgCrg brgOutput brgEnvironment brgSubstitution brgReduction brgValidity brgType brgUntrusted -brgGrafite brgGallina brgELPI +brgGrafite brgGallina brgLP diff --git a/helm/software/helena/src/basic_rg/brgELPI.ml b/helm/software/helena/src/basic_rg/brgLP.ml similarity index 56% rename from helm/software/helena/src/basic_rg/brgELPI.ml rename to helm/software/helena/src/basic_rg/brgLP.ml index 4e78eac13..d4ed3c9dd 100644 --- a/helm/software/helena/src/basic_rg/brgELPI.ml +++ b/helm/software/helena/src/basic_rg/brgLP.ml @@ -24,11 +24,14 @@ module B = Brg let ok = ref true +let top_age = 7000 + let uris = ref [] -let base = "elpi" +let base = "lp" -let ext = ".elpi" +let ext_lp = ".elpi" +let ext_tj = ".mod" let reserved = ["pi"; "sigma"; "nil"; "delay"; "in"; "with"; "resume"; "context"] @@ -108,9 +111,9 @@ let rec out_term st e och = function KP.fprintf och "(void %a\\ %a)" out_name a (out_term st ee) t -(* variant 1 *************************************************) +(* elpi variant 1 ***********************************************************) -let output_entity_1 och st (_, na, s, b) = +let output_entity_lp1 och st (_, na, s, b) = if na.E.n_apix <= !G.last then begin match b with | E.Abbr t -> @@ -122,16 +125,16 @@ let output_entity_1 och st (_, na, s, b) = | E.Void -> C.err () end else !ok -let close_out_1 och () = +let close_out_lp1 och () = let aux_sep _ = KP.fprintf och "%s" ")" in KP.fprintf och "%s" "gtop"; List.iter aux_sep !uris; - out_clause och "\n\n)."; + out_clause och "\n\n."; close_out och -(* Variant 2 *************************************************) +(* elpi variant 2 ***********************************************************) -let output_entity_2 och st (_, na, s, b) = +let output_entity_lp2 och st (_, na, s, b) = if na.E.n_apix <= !G.last then begin match b with | E.Abbr t -> @@ -145,7 +148,7 @@ let output_entity_2 och st (_, na, s, b) = | E.Void -> C.err () end else !ok -let close_out_2 och () = +let close_out_lp2 och () = let aux_name (b, s) = let gde = if b then "gdef+2" else "gdec+2" in KP.fprintf och "(%s %a\n" gde out_uri s @@ -157,29 +160,124 @@ let close_out_2 och () = out_clause och "tv+c C T :- tv+ T." end; out_clause och "main :- grundlagen."; - out_clause och "grundlagen :- (gv+ "; + 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 "\n\n."; + close_out och + +(* teyjus variant 2 *************************************************) + +let output_entity_tj2 och st (_, na, s, b) = + if na.E.n_apix <= !G.last then begin + out_comment och (KP.sprintf "constant %u" na.E.n_apix); + match b with + | E.Abbr t -> + KP.fprintf och "g+line %a %u\n %a\n.\n\n" + out_uri s (top_age - na.E.n_apix) (out_term st B.empty) t; + uris := (true, s) :: !uris; !ok + | E.Abst u -> + KP.fprintf och "g+line %a %u\n %a\n.\n\n" + out_uri s (top_age - na.E.n_apix) (out_term st B.empty) u; + uris := (false, s) :: !uris; !ok + | E.Void -> C.err () + end else !ok + +let close_out_tj2 och () = + let aux_name (b, s) = + let gde = if b then "gdef+2" else "gdec+2" in + KP.fprintf och "(%s %a\n" gde out_uri s + 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; + 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."; + close_out och + +(* teyjus variant 3 *************************************************) + +let output_entity_tj3 och st (_, na, u, b) = + if na.E.n_apix <= !G.last then begin + out_comment och (KP.sprintf "constant %u" na.E.n_apix); + let age = top_age - na.E.n_apix in + match b with + | E.Abbr v -> + KP.fprintf och "g+line %a %u\n %a\n.\n\n" + out_uri u age (out_term st B.empty) v; + KP.fprintf och "tv+ %a.\n\n" out_uri u; + KP.fprintf och "r+exp %a M C E M V :- g+line %a C V.\n\n" + out_uri u out_uri u; + uris := (true, u) :: !uris; !ok + | E.Abst w -> + KP.fprintf och "g+line %a %u\n %a\n.\n\n" + out_uri u age (out_term st B.empty) w; + KP.fprintf och "tv+ %a.\n\n" out_uri u; + KP.fprintf och "r+exp %a M1 C E M2 W :- m+pred M1 M2, g+line %a C W.\n\n" + out_uri u out_uri u; + uris := (false, u) :: !uris; !ok + | E.Void -> C.err () + end else !ok + +let close_out_tj3 och () = + let aux_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; + out_clause och "main :- grundlagen."; + out_clause och "grundlagen :-"; + List.iter aux_name (List.rev !uris); + out_clause och "!."; close_out och (* Interface functions ******************************************************) -let open_out_1 fname = +let open_out_lp1 fname = let dir = KF.concat !G.manager_dir base in let path = KF.concat dir fname in - let och = open_out (path ^ "1" ^ ext) in + let och = open_out (path ^ "1" ^ ext_lp) in out_preamble och; out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string); out_clause och "main :- grundlagen."; - out_clause och "grundlagen :- gv+ ("; - output_entity_1 och, close_out_1 och + out_clause och "grundlagen :- gv+"; + output_entity_lp1 och, close_out_lp1 och + +let open_out_lp2 fname = + let dir = KF.concat !G.manager_dir base in + let path = KF.concat dir fname in + let och = open_out (path ^ "2" ^ ext_lp) in + out_preamble och; + out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string); + output_entity_lp2 och, close_out_lp2 och + +let open_out_tj2 fname = + let dir = KF.concat !G.manager_dir base in + let path = KF.concat dir fname in + let och = open_out (path ^ "2" ^ ext_tj) in + out_preamble och; + out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string); + out_clause och "module grundlagen."; + out_clause och "accumulate helena."; + output_entity_tj2 och, close_out_tj2 och -let open_out_2 fname = +let open_out_tj3 fname = let dir = KF.concat !G.manager_dir base in let path = KF.concat dir fname in - let och = open_out (path ^ "2" ^ ext) in + let och = open_out (path ^ "3" ^ ext_tj) in out_preamble och; out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string); - output_entity_2 och, close_out_2 och + out_clause och "module grundlagen."; + out_clause och "accumulate helena."; + output_entity_tj3 och, close_out_tj3 och diff --git a/helm/software/helena/src/basic_rg/brgELPI.mli b/helm/software/helena/src/basic_rg/brgLP.mli similarity index 80% rename from helm/software/helena/src/basic_rg/brgELPI.mli rename to helm/software/helena/src/basic_rg/brgLP.mli index 96c16ec37..1fb878c17 100644 --- a/helm/software/helena/src/basic_rg/brgELPI.mli +++ b/helm/software/helena/src/basic_rg/brgLP.mli @@ -9,6 +9,10 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val open_out_1: string -> Brg.manager +val open_out_lp1: string -> Brg.manager -val open_out_2: string -> Brg.manager +val open_out_lp2: string -> Brg.manager + +val open_out_tj2: string -> Brg.manager + +val open_out_tj3: string -> Brg.manager diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index 89a085e5e..3ac27296d 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -20,8 +20,10 @@ type kernel = V4 | V3 | V0 type manager = Quiet | Coq | Matita - | ELPI1 - | ELPI2 + | LP1 (* newelpi *) + | LP2 (* newelpi *) + | TJ2 (* teyjus *) + | TJ3 (* teyjus *) (* interface functions ******************************************************) diff --git a/helm/software/helena/src/modules.ml b/helm/software/helena/src/modules.ml index c6767aae7..72895c06f 100644 --- a/helm/software/helena/src/modules.ml +++ b/helm/software/helena/src/modules.ml @@ -52,7 +52,7 @@ module BV = BrgValidity module BU = BrgUntrusted module BG = BrgGrafite (**) module BA = BrgGallina (**) -module BP = BrgELPI (**) +module BP = BrgLP module Z = Bag module ZD = BrgCrg diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index 05320d3bc..0f953949e 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -37,7 +37,7 @@ module BR = BrgReduction module BU = BrgUntrusted module BG = BrgGrafite module BA = BrgGallina -module BP = BrgELPI +module BP = BrgLP module ZD = BagCrg module ZO = BagOutput module ZT = BagType @@ -313,11 +313,13 @@ let main = if !G.trace >= 2 then begin preprocess := true; G.summary := true end in let set_manager s = match KS.lowercase s with - | "v8" -> G.manager := G.Coq - | "ma2" -> G.manager := G.Matita - | "elpi1" -> G.manager := G.ELPI1 - | "elpi2" -> G.manager := G.ELPI2 - | s -> L.warn level (KP.sprintf "Unknown manager: %s" s) + | "v8" -> G.manager := G.Coq + | "ma2" -> G.manager := G.Matita + | "lp1" -> G.manager := G.LP1 + | "lp2" -> G.manager := G.LP2 + | "tj2" -> G.manager := G.TJ2 + | "tj3" -> G.manager := G.TJ3 + | s -> L.warn level (KP.sprintf "Unknown manager: %s" s) in let clear_options () = export := false; preprocess := false; @@ -336,8 +338,10 @@ let main = begin match !G.manager with | G.Coq -> st := {!st with mst = Some (BA.open_out base_name)} | G.Matita -> st := {!st with mst = Some (BG.open_out base_name)} - | G.ELPI1 -> st := {!st with mst = Some (BP.open_out_1 base_name)} - | G.ELPI2 -> st := {!st with mst = Some (BP.open_out_2 base_name)} + | G.LP1 -> st := {!st with mst = Some (BP.open_out_lp1 base_name)} + | G.LP2 -> st := {!st with mst = Some (BP.open_out_lp2 base_name)} + | G.TJ2 -> st := {!st with mst = Some (BP.open_out_tj2 base_name)} + | G.TJ3 -> st := {!st with mst = Some (BP.open_out_tj3 base_name)} | G.Quiet -> () end; P.clear_marks (); @@ -364,7 +368,7 @@ let main = " 4 typing information, 5 conversion information, 6 reduction information,\n" ^ " 7 level disambiguation\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n\n" ^ - "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"elpi1\" \"elpi2\" (lambda-Prolog)\n" + "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"lp1\" \"lp2\" \"tj2\" (lambda-Prolog)\n" in let help_L = " [lexer] Show lexer debug information" in let help_M = " [manager] Set location of output directory (manager) to (default: current directory)" in -- 2.39.2