From 54191356ed05e187754076ebf5aa30d9dd6f213d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 8 Jun 2015 17:09:52 +0000 Subject: [PATCH] exportation to \lambda\delta representation in elpi --- helm/software/helena/.depend.opt | 13 +- helm/software/helena/Makefile | 31 +++- helm/software/helena/src/basic_rg/Make | 2 +- helm/software/helena/src/basic_rg/brgELPI.ml | 141 ++++++++++++++++++ helm/software/helena/src/basic_rg/brgELPI.mli | 12 ++ helm/software/helena/src/common/options.ml | 5 +- helm/software/helena/src/common/output.ml | 10 +- helm/software/helena/src/modules.ml | 1 + helm/software/helena/src/toplevel/top.ml | 16 +- 9 files changed, 211 insertions(+), 20 deletions(-) create mode 100644 helm/software/helena/src/basic_rg/brgELPI.ml create mode 100644 helm/software/helena/src/basic_rg/brgELPI.mli diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index ad474da2e..ae5016a32 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -193,6 +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/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/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ + src/common/alpha.cmx src/basic_rg/brgELPI.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 \ @@ -262,7 +269,8 @@ src/toplevel/top.cmo : src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ 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/brgCrg.cmi src/basic_rg/brg.cmx \ + src/basic_rg/brgGallina.cmi src/basic_rg/brgELPI.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 \ src/automath/autProcess.cmi src/automath/autParser.cmi \ @@ -276,7 +284,8 @@ src/toplevel/top.cmx : src/xml/xmlLibrary.cmx src/xml/xmlCrg.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/brgCrg.cmx src/basic_rg/brg.cmx \ + src/basic_rg/brgGallina.cmx src/basic_rg/brgELPI.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 \ src/automath/autProcess.cmx src/automath/autParser.cmx \ diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 5f17bc89b..c0d702cf7 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -10,10 +10,10 @@ KEEP = README CLEAN = etc/log.txt etc/profile.txt -TAGS = test-si-fast test-si test \ +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-coq export-matita export-elpi \ matita matitac include Makefile.common @@ -30,11 +30,13 @@ INPUT = examples/automath/grundlagen_2.aut INPUTFAST = examples/automath/grundlagen_1.aut -MA = grundlagen_2.ma -V = grundlagen_2.v +MA = grundlagen_2.ma +V = grundlagen_2.v +ELPI = grundlagen_2.elpi -PREAMBLE_MA = ../matita/matita.ma.templ -PREAMBLE_V = coq/grundlagen.template +PREAMBLE_MA = ../matita/matita.ma.templ +PREAMBLE_V = coq/grundlagen.template +PREAMBLE_ELPI = elpi/grundlagen.template test-si-fast: $(MAIN).opt etc @echo " HELENA -o -q -1 $(INPUTFAST)" @@ -44,9 +46,17 @@ test-si: $(MAIN).opt etc @echo " HELENA -d -l -p -o $(INPUT)" $(H)./$(MAIN).opt -T 2 -d -l -p -o $(O) $(INPUT) > etc/log.txt -test: $(MAIN).opt etc +test2: $(MAIN).opt etc @echo " HELENA -d -l $(INPUT)" - $(H)./$(MAIN).opt -l -o $(INPUT) -X -T 2 -d -l $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -l -o $(INPUT) -X -T 2 -d -l $(O) $(INPUT) > etc/log.txt + +test3: $(MAIN).opt etc + @echo " HELENA -d -l $(INPUT)" + $(H)./$(MAIN).opt -l -o $(INPUT) -X -T 3 -d -l $(O) $(INPUT) > etc/log.txt + +test6: $(MAIN).opt etc + @echo " HELENA -d -l $(INPUT)" + $(H)./$(MAIN).opt -l -o $(INPUT) -X -T 6 -d -l $(O) $(INPUT) > etc/log.txt xml-si: $(MAIN).opt etc @echo " HELENA -l -o -s 1 -x $(INPUT)" @@ -74,6 +84,11 @@ export-matita matita/$(MA): $(MAIN).opt etc $(H)mkdir -p matita $(H)./$(MAIN).opt -T 1 -a n -c $(PREAMBLE_MA) -l -m MA2 -o $(O) $(INPUT) > etc/log.txt +export-elpi elpi/$(ELPI): $(MAIN).opt etc + @echo " HELENA -l -m ELPI -o $(INPUT)" + $(H)mkdir -p elpi + $(H)./$(MAIN).opt -T 1 -a n -c $(PREAMBLE_ELPI) -l -m ELPI -o $(O) $(INPUT) > etc/log.txt + profile-fast: $(MAIN).opt etc @echo " HELENA -o -q $(INPUTFAST) (31 TIMES)" $(H)rm -f etc/log.txt diff --git a/helm/software/helena/src/basic_rg/Make b/helm/software/helena/src/basic_rg/Make index 9a8ce877b..d230dace7 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 +brgGrafite brgGallina brgELPI diff --git a/helm/software/helena/src/basic_rg/brgELPI.ml b/helm/software/helena/src/basic_rg/brgELPI.ml new file mode 100644 index 000000000..e81bd4b2e --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgELPI.ml @@ -0,0 +1,141 @@ +(* + ||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 level = ref 0 + +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+0" else if h = 1 then "k+1" 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 (_, v, t) -> + KP.fprintf och "(appx %a %a)" (out_term st e) v (out_term st e) t + | B.Bind (a, B.Abst (n, w), t) -> + let a = R.alpha B.mem e a in + let ee = B.push e B.empty a (B.abst n w) in + let l = match N.to_string st n with + | "1" -> "l+1" + | "2" -> "l+2" + | _ -> ok := false; "?" + in + KP.fprintf och "(abst %s %a %a\\ %a)" + 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 + +let output_entity och st (_, na, s, b) = +(* if na.E.n_apix <= 4500 then begin *) + out_comment och (KP.sprintf "constant %u" na.E.n_apix); + match b with + | E.Abbr t -> + KP.fprintf och "(gdef c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) t out_uri s; + incr level; !ok + | E.Abst u -> + KP.fprintf och "(gdec c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) u out_uri s; + incr level; !ok + | E.Void -> C.err () +(* end else !ok *) + +let close_out och () = + let rec aux () = + if !level <= 0 then KP.fprintf och "%s" "\n\n).\n" + else begin KP.fprintf och "%s" ")"; decr level; aux () end + in + KP.fprintf och "%s" "gtop"; + aux (); close_out och + +(* Interface functions ******************************************************) + +let open_out fname = + let dir = KF.concat !G.manager_dir base in + let path = KF.concat dir fname in + let och = open_out (path ^ 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 "k+succ k+0 k+2."; + out_clause och "k+succ k+1 k+3."; + out_clause och "grundlagen :- gv+ ("; + output_entity och, close_out och diff --git a/helm/software/helena/src/basic_rg/brgELPI.mli b/helm/software/helena/src/basic_rg/brgELPI.mli new file mode 100644 index 000000000..d96b7f45d --- /dev/null +++ b/helm/software/helena/src/basic_rg/brgELPI.mli @@ -0,0 +1,12 @@ +(* + ||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: string -> Brg.manager diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index b8ea00387..7d76b7d33 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -18,12 +18,13 @@ type uri_generator = string -> string type kernel = V4 | V3 | V0 type manager = Quiet - | Matita | Coq + | Matita + | ELPI (* interface functions ******************************************************) -let version_string = "Helena 0.8.2 M (February 2015)" +let version_string = "Helena 0.8.2 M (May 2015)" let stage = ref 3 (* stage *) diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml index 23829c095..a72f94318 100644 --- a/helm/software/helena/src/common/output.ml +++ b/helm/software/helena/src/common/output.ml @@ -41,7 +41,15 @@ let clear_reductions () = reductions := initial_reductions let add ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) () -= reductions := { += +(* + if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta); + if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta); + if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta); + if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt); + if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt); +*) +reductions := { beta = !reductions.beta + beta; zeta = !reductions.zeta + zeta; theta = !reductions.theta + theta; diff --git a/helm/software/helena/src/modules.ml b/helm/software/helena/src/modules.ml index e6073d6ff..c6767aae7 100644 --- a/helm/software/helena/src/modules.ml +++ b/helm/software/helena/src/modules.ml @@ -52,6 +52,7 @@ module BV = BrgValidity module BU = BrgUntrusted module BG = BrgGrafite (**) module BA = BrgGallina (**) +module BP = BrgELPI (**) 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 ca3abbc52..3ce7bbc70 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -37,6 +37,7 @@ module BR = BrgReduction module BU = BrgUntrusted module BG = BrgGrafite module BA = BrgGallina +module BP = BrgELPI module ZD = BagCrg module ZO = BagOutput module ZT = BagType @@ -312,9 +313,10 @@ 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 - | s -> L.warn level (KP.sprintf "Unknown manager: %s" s) + | "v8" -> G.manager := G.Coq + | "ma2" -> G.manager := G.Matita + | "elpi" -> G.manager := G.ELPI + | s -> L.warn level (KP.sprintf "Unknown manager: %s" s) in let clear_options () = export := false; preprocess := false; @@ -331,8 +333,9 @@ let main = if !G.stage <= 1 then G.kernel := G.V4; G.cover := cover; begin match !G.manager with - | G.Matita -> st := {!st with mst = Some (BG.open_out base_name)} | 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.ELPI -> st := {!st with mst = Some (BP.open_out base_name)} | G.Quiet -> () end; P.clear_marks (); @@ -358,7 +361,8 @@ let main = "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 processed objects,\n" ^ " 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" + "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n\n" ^ + "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"elpi\" (lambda-Prolog)\n" in let help_L = " show lexer debug information" in let help_M = " set location of output directory (manager) to (default: current directory)" in @@ -376,7 +380,7 @@ let main = let help_i = " show local references by index" in let help_k = " set kernel version (default: \"V3\")" in let help_l = " disambiguate binders level (Automath)" in - let help_m = " export kernel entities for this manager (default: no manager, \"ma2\": Grafite NG, \"v8\": Gallina 8)" in + let help_m = " export kernel entities for this manager (see above, default: no manager)" in let help_o = " activate sort inclusion (default: false)" in let help_p = " preprocess source (Automath)" in let help_q = " disable quotation of identifiers" in -- 2.39.2