- siimplifified RTM (one register less) now counts x-steps.

[helm.git] / helm / software / helena / src / basic_rg / brgELPI.ml

diff --git a/helm/software/helena/src/basic_rg/brgELPI.ml b/helm/software/helena/src/basic_rg/brgELPI.ml
index e81bd4b2ecc964e7c7d9de36583e2783a3c9867f..0ead752807986204f85ca6db85fddd71a87fb6da 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgELPI.ml
+++ b/helm/software/helena/src/basic_rg/brgELPI.ml
@@ -73,29 +73,30 @@ let out_name och a =
    E.name err f a
 
 let rec out_term st e och = function
-   | B.Sort (_, h)           -> 
+   | 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)           ->       
+   | B.LRef (_, i)                   ->
       let _, _, a, b = B.get e i in
       KP.fprintf och "%a" out_name a
-   | B.GRef (_, s)           ->
+   | B.GRef (_, s)                   ->
       KP.fprintf och "%a" out_uri s
-   | B.Cast (_, u, t)        ->
+   | 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) ->
+   | B.Appl (_, v, t)                ->
+      KP.fprintf och "(appr %a %a)" (out_term st e) v (out_term st e) t
+   | B.Bind (a, B.Abst (x, 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 ee = B.push e B.empty a (B.abst x n w) in
+      let c = if x 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 "(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) ->
+      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)"
@@ -135,7 +136,6 @@ let open_out fname =
    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 "main :- grundlagen.";
    out_clause och "grundlagen :- gv+ (";
    output_entity och, close_out och