advances on exportation to prolog

[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 05320d3bc074458e0c0b3bbd4c0c289acff75d24..0f953949efff60ea83e2d5a3b9fc0784379e9b17 100644 (file)
--- 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 = "<dir>    [manager]   Set location of output directory (manager) to <dir> (default: current directory)" in