From 4ea53eb93717cb1bcd6a0ccb7b1a4d711c1c7a9b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 30 Jan 2018 17:15:39 +0100 Subject: [PATCH] helena: updated prolog exportation to ld3 and ALT-0/PTS --- .gitignore | 3 +- helm/software/helena/Makefile | 32 ++-- helm/software/helena/README | 2 +- .../software/helena/src/basic_rg/brgHelena.ml | 4 +- helm/software/helena/src/basic_rg/brgPTS.ml | 163 ++++++++++++++++++ helm/software/helena/src/basic_rg/brgPTS.mli | 16 ++ helm/software/helena/src/common/options.ml | 4 +- helm/software/helena/src/modules.ml | 2 +- helm/software/helena/src/toplevel/helena.ml | 12 +- 9 files changed, 205 insertions(+), 33 deletions(-) create mode 100644 helm/software/helena/src/basic_rg/brgPTS.ml create mode 100644 helm/software/helena/src/basic_rg/brgPTS.mli diff --git a/.gitignore b/.gitignore index 45d3126b7..72f97fe46 100644 --- a/.gitignore +++ b/.gitignore @@ -37,7 +37,8 @@ matita/matita/help/C/version.txt helm/software/helena/matita helm/software/helena/scripts/lp/grundlagen_2b_lyp.elpi -helm/software/helena/scripts/cc +helm/software/helena/scripts/lp/grundlagen_2b_ld3.elpi +helm/software/helena/scripts/lp/grundlagen_2b_pts.elpi helm/software/helena/etc helm/www/lambdadelta/html diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 38dab9e6b..71abf95d2 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -24,7 +24,7 @@ TARGETS = test-si-fast test-si test2-opt test2-byte test3 test6 \ profile-fast profile profile-coq profile-coq-byte \ xml-si xml-si-v3 xml xml-v3 \ export-coq export-matita \ - export-lp1 export-lp2 export-tj2 export-tj3 export-lyp \ + export-lp1 export-lp2 export-tj2 export-tj3 export-pts export-lyp \ matita matitac include Makefile.common @@ -49,11 +49,11 @@ OUTPUT = scripts MA = grundlagen_2.ma V = grundlagen_2.v -LP1 = grundlagen_21.elpi -LP2 = grundlagen_22.elpi -TJ2 = grundlagen_22.mod -TJ3 = grundlagen_23.mod -CC0 = grundlagen_20.elpi +LP1 = grundlagen_2a_ld3.elpi +LP2 = grundlagen_2b_ld3.elpi +TJ2 = grundlagen_2b_ld3.mod +TJ3 = grundlagen_2c_ld3.mod +PTS = grundlagen_2b_pts.elpi LYP = grundlagen_2b_lyp.elpi PREAMBLE_MA = ../matita/matita.ma.templ @@ -146,34 +146,34 @@ xml-v3: $(EXEC).native etc export-coq $(OUTPUT)/coq/$(V): $(EXEC).native etc @echo " HELENA -m V8 -q $(INPUT)" - $(H)./$(EXEC).native -M $(OUTPUT) -a n -m V8 -p $(PREAMBLE_V) -q $(TEST1) > etc/log.txt + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m V8 -p $(PREAMBLE_V) -q $(O) $(TEST1) > etc/log.txt export-matita $(OUTPUT)/matita/$(MA): $(EXEC).native etc @echo " HELENA -m MA2 -q $(INPUT)" - $(H)./$(EXEC).native -M $(OUTPUT) -a n -m MA2 -p $(PREAMBLE_MA) -q $(TEST1) > etc/log.txt + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m MA2 -p $(PREAMBLE_MA) -q $(O) $(TEST1) > etc/log.txt export-lp1 $(OUTPUT)/lp/$(LP1): $(EXEC).native etc @echo " HELENA -m LP1 -q $(INPUT)" - $(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP1 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP1 -p $(PREAMBLE_LP) -q $(O) $(TEST1) > etc/log.txt export-lp2 $(OUTPUT)/lp/$(LP2): $(EXEC).native etc @echo " HELENA -m LP2 -q $(INPUT)" - $(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP2 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP2 -p $(PREAMBLE_LP) -q $(O) $(TEST1) > etc/log.txt export-tj2 $(OUTPUT)/lp/$(TJ2): $(EXEC).native etc @echo " HELENA -m TJ2 -q $(INPUT)" - $(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ2 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ2 -p $(PREAMBLE_LP) -q $(O) $(TEST1) > etc/log.txt export-tj3 $(OUTPUT)/lp/$(TJ3): $(EXEC).native etc @echo " HELENA -m TJ3 -q $(INPUT)" - $(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ3 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ3 -p $(PREAMBLE_LP) -q $(O) $(TEST1) > etc/log.txt -export-cc0 $(OUTPUT)/cc/$(CC0): $(EXEC).native etc - @echo " HELENA -m CC0 -q $(INPUT)" - $(H)./$(EXEC).native -M $(OUTPUT) -a n -m CC0 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt +export-pts $(OUTPUT)/lp/$(PTS): $(EXEC).native etc + @echo " HELENA -m PTS -c -q $(INPUT)" + $(H)./$(EXEC).native -M $(OUTPUT) -a n -m PTS -p $(PREAMBLE_LP) -c -q $(O) $(TEST1) > etc/log.txt export-lyp $(OUTPUT)/lp/$(LYP): $(EXEC).native etc - @echo " HELENA -m lyp -q $(INPUT)" + @echo " HELENA -m lyp -c -q $(INPUT)" $(H)./$(EXEC).native -M $(OUTPUT) -a n -m lyp -p $(PREAMBLE_LP) -c -q $(O) $(TEST1) > etc/log.txt matita: $(OUTPUT)/matita/$(MA) diff --git a/helm/software/helena/README b/helm/software/helena/README index 3a7b77d67..1e7b2af63 100644 --- a/helm/software/helena/README +++ b/helm/software/helena/README @@ -43,7 +43,7 @@ TYPE enable option -t (if unset, -t is disabled) xml-si xml-si-v3 xml xml-v3 * Set at least F="MANAGER QUOTE" for targets: - export-coq export-matita export-lp1 export-lp2 export-tj2 export-tj3 export-cc0 export-lyp + export-coq export-matita export-lp1 export-lp2 export-tj2 export-tj3 export-pts export-lyp * Type "make profile.opt" or "make profile.byte" to validate the "grundlagen" 31 times (two runs each time) diff --git a/helm/software/helena/src/basic_rg/brgHelena.ml b/helm/software/helena/src/basic_rg/brgHelena.ml index 07aa99601..43146aebb 100644 --- a/helm/software/helena/src/basic_rg/brgHelena.ml +++ b/helm/software/helena/src/basic_rg/brgHelena.ml @@ -304,7 +304,6 @@ let close_out_tj3 och () = end in let chunks = out_list och 1 true size (List.rev !uris) in - out_clause och "main :- grundlagen."; KP.fprintf och "grundlagen :-\n"; out_chunks och (pred chunks) 1; close_out och @@ -325,10 +324,9 @@ let open_out_lp1 fname = 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 + let och = open_out (path ^ "b_ld3" ^ ext_lp) in out_preamble och; out_top_comment och version; - out_clause och "accumulate helena."; output_entity_lp2 och, close_out_lp2 och let open_out_tj2 fname = diff --git a/helm/software/helena/src/basic_rg/brgPTS.ml b/helm/software/helena/src/basic_rg/brgPTS.ml new file mode 100644 index 000000000..2476bf313 --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgPTS.ml @@ -0,0 +1,163 @@ +(* + ||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 + +IFDEF MANAGER THEN + +(* Internal functions *******************************************************) + +let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true) + +let ok = ref true + +let uris = ref [] + +let chunk = ref 0 + +let sub_och = ref stdout + +let top_age = 7000 + +let size = 250 + +let base = "lp" + +let ext_lp = ".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 k -> + let sort = if k = 0 then "(s+type 0)" else if k = 1 then "(s+prop 0)" else assert false in + KP.fprintf och "(sort %s)" sort + | B.LRef (_, i) -> + let _, _, _, y, b = B.get e i in + KP.fprintf och "%a" out_name y + | B.GRef (_, s) -> + KP.fprintf och "%a" out_uri s + | B.Cast (u, t) -> + KP.fprintf och "(abbr %a %a x\\ x)" (out_term st e) t (out_term st e) u + | B.Appl (_, v, t) -> + KP.fprintf och "(appl %a %a)" (out_term st e) t (out_term st e) v + | B.Bind (y, B.Abst (r, n, w), t) -> + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y (B.abst r n w) in + let c = match r, N.to_string st n with + | false, "1" -> "prod" + | false, "2" -> "abst" + | _ -> ok := false; "?" + in + KP.fprintf och "(%s %a %a\\ %a)" + c (out_term st e) w out_name y (out_term st ee) t + | B.Bind (_, B.Void, _) -> C.err () + | B.Bind (_, B.Abbr _, _) -> C.err () + +(* PTS variant 2 ************************************************************) + +let output_entity_pts2 och st (_, na, u, b) = + if na.E.n_apix < !G.first then begin + match b with + | E.Abbr (_, B.Cast (w, v)) -> + KP.fprintf och "get_expansion %a %u %a.\n" + out_uri u na.E.n_apix (out_term st B.empty) v; + KP.fprintf och "get_type %a %a.\n\n" + out_uri u (out_term st B.empty) w; !ok + | E.Abst (_, w) -> + KP.fprintf och "get_type %a %a.\n\n" + out_uri u (out_term st B.empty) w; !ok + | _ -> C.err () + end else if na.E.n_apix <= !G.last then begin + match b with + | E.Abbr (_, B.Cast (w, v)) -> + KP.fprintf och "g+line+2 %a %u\n %a\n %a\n.\n\n" + out_uri u na.E.n_apix (out_term st B.empty) v (out_term st B.empty) w; + uris := (true, u) :: !uris; !ok + | E.Abst (_, w) -> + KP.fprintf och "g+line+1 %a %u\n %a\n.\n\n" + out_uri u na.E.n_apix (out_term st B.empty) w; + uris := (false, u) :: !uris; !ok + | _ -> C.err () + end else !ok + +let close_out_pts2 och () = + let aux_name (b, s) = + let gde = if b then "gdef" else "gdec" in + KP.fprintf och "(%s %a\n" gde out_uri s + in + let aux_sep _ = KP.fprintf och "%s" ")" in + out_clause och "grundlagen :- is+valid"; + 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_pts2 fname = + let dir = KF.concat !G.manager_dir base in + let path = KF.concat dir fname in + let och = open_out (path ^ "b_pts" ^ ext_lp) in + out_preamble och; + out_top_comment och version; + output_entity_pts2 och, close_out_pts2 och + +END diff --git a/helm/software/helena/src/basic_rg/brgPTS.mli b/helm/software/helena/src/basic_rg/brgPTS.mli new file mode 100644 index 000000000..60f2b8060 --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgPTS.mli @@ -0,0 +1,16 @@ +(* + ||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_______________________________________________________________ *) + +IFDEF MANAGER THEN + +val open_out_pts2: string -> Brg.manager + +END diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index cdf88c308..379c24fca 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -26,9 +26,7 @@ type manager = Quiet | LP2 (* elpi helena *) | TJ2 (* teyjus helena *) | TJ3 (* teyjus helena *) -(* - | CC0 (* elpi cic *) -*) + | PTS (* elpi pts *) | LYP (* elpi lyp *) END diff --git a/helm/software/helena/src/modules.ml b/helm/software/helena/src/modules.ml index dd8cd7358..f8623ce70 100644 --- a/helm/software/helena/src/modules.ml +++ b/helm/software/helena/src/modules.ml @@ -53,7 +53,7 @@ module BU = BrgUntrusted module BM = BrgMatita module BQ = BrgCoq module BH = BrgHelena -module BC = BrgCC +module BP = BrgPTS module BY = BrgLYP module Z = Bag diff --git a/helm/software/helena/src/toplevel/helena.ml b/helm/software/helena/src/toplevel/helena.ml index 1070dd915..63a8c0621 100644 --- a/helm/software/helena/src/toplevel/helena.ml +++ b/helm/software/helena/src/toplevel/helena.ml @@ -40,7 +40,7 @@ module BU = BrgUntrusted module BM = BrgMatita module BQ = BrgCoq module BH = BrgHelena -(* module BC = BrgCC *) +module BP = BrgPTS module BY = BrgLYP module ZD = BagCrg module ZO = BagOutput @@ -393,9 +393,7 @@ let set_manager s = match KS.lowercase s with | "lp2" -> G.manager := G.LP2 | "tj2" -> G.manager := G.TJ2 | "tj3" -> G.manager := G.TJ3 -(* - | "cc0" -> G.manager := G.CC0 -*) + | "pts" -> G.manager := G.PTS | "lyp" -> G.manager := G.LYP | s -> L.warn level (KP.sprintf "Unknown manager: %s" s) @@ -492,9 +490,7 @@ IFDEF MANAGER THEN | G.LP2 -> st := {!st with mst = Some (BH.open_out_lp2 base_name)} | G.TJ2 -> st := {!st with mst = Some (BH.open_out_tj2 base_name)} | G.TJ3 -> st := {!st with mst = Some (BH.open_out_tj3 base_name)} -(* - | G.CC0 -> st := {!st with mst = Some (BC.open_out_cc0 base_name)} -*) + | G.PTS -> st := {!st with mst = Some (BP.open_out_pts2 base_name)} | G.LYP -> st := {!st with mst = Some (BY.open_out_lyp2 base_name)} | G.Quiet -> () end @@ -530,7 +526,7 @@ ELSE () END " 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), \"lp1\" \"lp2\" \"tj2\" \"tj3\" \"lyp\" (lambda-Prolog)\n" + "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"lp1\" \"lp2\" \"tj2\" \"tj3\" \"pts\" \"lyp\" (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