From: Ferruccio Guidi Date: Thu, 25 Jun 2015 19:00:51 +0000 (+0000) Subject: advances on exportation to prolog X-Git-Tag: make_still_working~717 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=98fef490e55d1d780e8c0bb19de0218e08ae73b1;p=helm.git advances on exportation to prolog --- 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/elpi/elpi.template deleted file mode 100644 index e69de29bb..000000000 diff --git a/helm/software/helena/lp/lp.template b/helm/software/helena/lp/lp.template new file mode 100644 index 000000000..e69de29bb 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/brgELPI.ml deleted file mode 100644 index 4e78eac13..000000000 --- a/helm/software/helena/src/basic_rg/brgELPI.ml +++ /dev/null @@ -1,185 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -module KF = Filename -module KP = Printf - -module U = NUri -module C = Cps -module G = Options -module N = Layer -module E = Entity -module R = Alpha -module B = Brg - -(* Internal functions *******************************************************) - -let ok = ref true - -let uris = ref [] - -let base = "elpi" - -let ext = ".elpi" - -let reserved = ["pi"; "sigma"; "nil"; "delay"; "in"; "with"; "resume"; "context"] - -let alpha n = - if List.mem n reserved then !G.alpha ^ n else n - -let out_preamble och = - let ich = open_in !G.preamble in - let rec aux () = KP.fprintf och "%s\n" (input_line ich); aux () in - try aux () with End_of_file -> close_in ich - -let out_top_comment och msg = - KP.fprintf och "%% %s\n\n" msg - -let out_comment och msg = - KP.fprintf och "%% %s\n" msg - -let out_clause och msg = - KP.fprintf och "%s\n\n" msg - -let out_uri och u = - let str = U.string_of_uri u in - let rec aux i = - let c = str.[i] in - if c = '.' then () else begin - output_char och (if c = '/' then '_' else c); - aux (succ i) - end - in - let rec strip i n = - if n <= 0 then succ i else - strip (String.index_from str (succ i) '/') (pred n) - in - aux (strip 0 3) - -let out_name och a = - let f n = function - | true -> KP.fprintf och "%s" (alpha n) - | false -> KP.fprintf och "_" - in - let err () = f "" false in - E.name err f a - -let rec out_term st e och = function - | B.Sort (_, h) -> - let sort = if h = 0 then "k+set" else if h = 1 then "k+prop" else assert false in - KP.fprintf och "(sort %s)" sort - | B.LRef (_, i) -> - let _, _, a, b = B.get e i in - KP.fprintf och "%a" out_name a - | B.GRef (_, s) -> - KP.fprintf och "%a" out_uri s - | B.Cast (_, u, t) -> - KP.fprintf och "(cast %a %a)" (out_term st e) u (out_term st e) t - | B.Appl (_, x, v, t) -> - let c = if x then "appx" else "appr" in - KP.fprintf och "(%s %a %a)" c (out_term st e) v (out_term st e) t - | B.Bind (a, B.Abst (r, n, w), t) -> - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a (B.abst r n w) in - let c = if r then "prod" else "abst" in - let l = match N.to_string st n with - | "1" -> "l+1" - | "2" -> "l+2" - | _ -> ok := false; "?" - in - KP.fprintf och "(%s %s %a %a\\ %a)" - c l (out_term st e) w out_name a (out_term st ee) t - | B.Bind (a, B.Abbr v, t) -> - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a (B.abbr v) in - KP.fprintf och "(abbr %a %a\\ %a)" - (out_term st e) v out_name a (out_term st ee) t - | B.Bind (a, B.Void, t) -> - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a (B.Void) in - KP.fprintf och "(void %a\\ %a)" - out_name a (out_term st ee) t - -(* variant 1 *************************************************) - -let output_entity_1 och st (_, na, s, b) = - if na.E.n_apix <= !G.last then begin - match b with - | E.Abbr t -> - KP.fprintf och "(gdef+1 c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) t out_uri s; - uris := (true, s) :: !uris; !ok - | E.Abst u -> - KP.fprintf och "(gdec+1 c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) u out_uri s; - uris := (false, s) :: !uris; !ok - | E.Void -> C.err () - end else !ok - -let close_out_1 och () = - let aux_sep _ = KP.fprintf och "%s" ")" in - KP.fprintf och "%s" "gtop"; - List.iter aux_sep !uris; - out_clause och "\n\n)."; - close_out och - -(* Variant 2 *************************************************) - -let output_entity_2 och st (_, na, s, b) = - if na.E.n_apix <= !G.last then begin - match b with - | E.Abbr t -> - KP.fprintf och "g+line %a c+%u\n %a\n.\n\n" - out_uri s na.E.n_apix (out_term st B.empty) t; - uris := (true, s) :: !uris; !ok - | E.Abst u -> - KP.fprintf och "g+line %a c+%u\n %a\n.\n\n" - out_uri s 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_2 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 - -(* Interface functions ******************************************************) - -let open_out_1 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 - 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 - -let open_out_2 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 - 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 diff --git a/helm/software/helena/src/basic_rg/brgELPI.mli b/helm/software/helena/src/basic_rg/brgELPI.mli deleted file mode 100644 index 96c16ec37..000000000 --- a/helm/software/helena/src/basic_rg/brgELPI.mli +++ /dev/null @@ -1,14 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -val open_out_1: string -> Brg.manager - -val open_out_2: string -> Brg.manager diff --git a/helm/software/helena/src/basic_rg/brgLP.ml b/helm/software/helena/src/basic_rg/brgLP.ml new file mode 100644 index 000000000..d4ed3c9dd --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgLP.ml @@ -0,0 +1,283 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module KF = Filename +module KP = Printf + +module U = NUri +module C = Cps +module G = Options +module N = Layer +module E = Entity +module R = Alpha +module B = Brg + +(* Internal functions *******************************************************) + +let ok = ref true + +let top_age = 7000 + +let uris = ref [] + +let base = "lp" + +let ext_lp = ".elpi" +let ext_tj = ".mod" + +let reserved = ["pi"; "sigma"; "nil"; "delay"; "in"; "with"; "resume"; "context"] + +let alpha n = + if List.mem n reserved then !G.alpha ^ n else n + +let out_preamble och = + let ich = open_in !G.preamble in + let rec aux () = KP.fprintf och "%s\n" (input_line ich); aux () in + try aux () with End_of_file -> close_in ich + +let out_top_comment och msg = + KP.fprintf och "%% %s\n\n" msg + +let out_comment och msg = + KP.fprintf och "%% %s\n" msg + +let out_clause och msg = + KP.fprintf och "%s\n\n" msg + +let out_uri och u = + let str = U.string_of_uri u in + let rec aux i = + let c = str.[i] in + if c = '.' then () else begin + output_char och (if c = '/' then '_' else c); + aux (succ i) + end + in + let rec strip i n = + if n <= 0 then succ i else + strip (String.index_from str (succ i) '/') (pred n) + in + aux (strip 0 3) + +let out_name och a = + let f n = function + | true -> KP.fprintf och "%s" (alpha n) + | false -> KP.fprintf och "_" + in + let err () = f "" false in + E.name err f a + +let rec out_term st e och = function + | B.Sort (_, h) -> + let sort = if h = 0 then "k+set" else if h = 1 then "k+prop" else assert false in + KP.fprintf och "(sort %s)" sort + | B.LRef (_, i) -> + let _, _, a, b = B.get e i in + KP.fprintf och "%a" out_name a + | B.GRef (_, s) -> + KP.fprintf och "%a" out_uri s + | B.Cast (_, u, t) -> + KP.fprintf och "(cast %a %a)" (out_term st e) u (out_term st e) t + | B.Appl (_, x, v, t) -> + let c = if x then "appx" else "appr" in + KP.fprintf och "(%s %a %a)" c (out_term st e) v (out_term st e) t + | B.Bind (a, B.Abst (r, n, w), t) -> + let a = R.alpha B.mem e a in + let ee = B.push e B.empty a (B.abst r n w) in + let c = if r then "prod" else "abst" in + let l = match N.to_string st n with + | "1" -> "l+1" + | "2" -> "l+2" + | _ -> ok := false; "?" + in + KP.fprintf och "(%s %s %a %a\\ %a)" + c l (out_term st e) w out_name a (out_term st ee) t + | B.Bind (a, B.Abbr v, t) -> + let a = R.alpha B.mem e a in + let ee = B.push e B.empty a (B.abbr v) in + KP.fprintf och "(abbr %a %a\\ %a)" + (out_term st e) v out_name a (out_term st ee) t + | B.Bind (a, B.Void, t) -> + let a = R.alpha B.mem e a in + let ee = B.push e B.empty a (B.Void) in + KP.fprintf och "(void %a\\ %a)" + out_name a (out_term st ee) t + +(* elpi variant 1 ***********************************************************) + +let output_entity_lp1 och st (_, na, s, b) = + if na.E.n_apix <= !G.last then begin + match b with + | E.Abbr t -> + KP.fprintf och "(gdef+1 c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) t out_uri s; + uris := (true, s) :: !uris; !ok + | E.Abst u -> + KP.fprintf och "(gdec+1 c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) u out_uri s; + uris := (false, s) :: !uris; !ok + | E.Void -> C.err () + end else !ok + +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."; + close_out och + +(* elpi variant 2 ***********************************************************) + +let output_entity_lp2 och st (_, na, s, b) = + if na.E.n_apix <= !G.last then begin + match b with + | E.Abbr t -> + KP.fprintf och "g+line %a c+%u\n %a\n.\n\n" + out_uri s na.E.n_apix (out_term st B.empty) t; + uris := (true, s) :: !uris; !ok + | E.Abst u -> + KP.fprintf och "g+line %a c+%u\n %a\n.\n\n" + out_uri s 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_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 + 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 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_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_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_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_tj3 fname = + let dir = KF.concat !G.manager_dir base in + let path = KF.concat dir fname 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); + 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/brgLP.mli b/helm/software/helena/src/basic_rg/brgLP.mli new file mode 100644 index 000000000..1fb878c17 --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgLP.mli @@ -0,0 +1,18 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +val open_out_lp1: 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