exportation to \lambda\delta representation in elpi

[helm.git] / helm / software / helena / src / toplevel / top.ml

diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml
index ca3abbc529a8f02684149ee7610d32b73cba205e..3ce7bbc7026252f29724ea52559cafa3288d3218 100644 (file)
--- 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 = "<dir>  set location of output directory (manager) to <dir> (default: current directory)" in
@@ -376,7 +380,7 @@ let main =
    let help_i = " show local references by index" in
    let help_k = "<string>  set kernel version (default: \"V3\")" in
    let help_l = " disambiguate binders level (Automath)" in
-   let help_m = "<string>  export kernel entities for this manager (default: no manager, \"ma2\": Grafite NG, \"v8\": Gallina 8)" in
+   let help_m = "<string>  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