lambda-delta: we added the support for position indexes in global references

[helm.git] / helm / software / lambda-delta / toplevel / metaOutput.ml

diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml
index 27157de37b44977d7767ef642731ff09c6a85c8f..4efee4a6833e511ba53428c3670cc2aec2e79082 100644 (file)
--- a/helm/software/lambda-delta/toplevel/metaOutput.ml
+++ b/helm/software/lambda-delta/toplevel/metaOutput.ml
@@ -23,6 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
+module F = Format
 module M = Meta
 
 type counters = {
@@ -43,19 +44,19 @@ let initial_counters = {
 }
 
 let rec count_term f c = function
-   | M.Sort _         -> 
+   | M.Sort _          -> 
       f {c with tsorts = succ c.tsorts}
-   | M.LRef _         -> 
+   | M.LRef _          -> 
       f {c with tlrefs = succ c.tlrefs}
-   | M.GRef (_, ts)   -> 
+   | M.GRef (_, _, ts) -> 
       let c = {c with tgrefs = succ c.tgrefs} in
       let c = {c with pappls = c.pappls + List.length ts} in
       Cps.list_fold_left f count_term c ts
-   | M.Appl (v, t)    -> 
+   | M.Appl (v, t)     -> 
       let c = {c with tappls = succ c.tappls} in
       let f c = count_term f c t in
       count_term f c v
-   | M.Abst (_, w, t) -> 
+   | M.Abst (_, w, t)  -> 
       let c = {c with tabsts = succ c.tabsts} in
       let f c = count_term f c t in
       count_term f c w
@@ -63,12 +64,12 @@ let rec count_term f c = function
 let count_par f c (_, w) = count_term f c w
 
 let count_item f c = function
-   | pars, _, w, None        ->
+   | _, pars, _, w, None        ->
       let c = {c with eabsts = succ c.eabsts} in
       let c = {c with pabsts = c.pabsts + List.length pars} in
       let f c = count_term f c w in
       Cps.list_fold_left f count_par c pars   
-   | pars, _, w, Some (_, v) ->
+   | _, pars, _, w, Some (_, v) ->
       let c = {c with eabbrs = succ c.eabbrs} in
       let c = {c with pabsts = c.pabsts + List.length pars} in
       let f c = count_term f c v in
@@ -97,7 +98,53 @@ let print_counters f c =
    Printf.printf "      Abstraction items:      %6u\n" c.tabsts;
    flush stdout; f ()
 
+let string_of_sort = function
+   | true -> "Type"
+   | false -> "Prop"
+
 let string_of_qid (id, path) =
    let path = String.concat "/" path in
    Filename.concat path id
-   
+
+let string_of_transparent = function
+   | true  -> "="
+   | false -> "~"
+
+let pp_list pp opend sep closed frm l =
+   let rec aux frm = function
+      | []       -> ()
+      | [hd]     -> pp frm hd
+      | hd :: tl -> F.fprintf frm "%a%s%a" pp hd sep aux tl 
+   in
+   if l = [] then () else F.fprintf frm "%s%a%s" opend aux l closed
+
+let rec pp_args frm args = pp_list pp_term "(" "," ")" frm args
+
+and pp_term frm = function
+   | M.Sort s            -> 
+      F.fprintf frm "@[*%s@]" (string_of_sort s)
+   | M.LRef i            ->
+      F.fprintf frm "@[#%u@]" i
+   | M.GRef (l, qid, ts) ->
+      F.fprintf frm "@[%u@@$%s%a@]" l (string_of_qid qid) pp_args ts
+   | M.Appl (v, t)       ->
+      F.fprintf frm "@[(%a).%a@]" pp_term v pp_term t
+   | M.Abst (id, w, t)   ->
+      F.fprintf frm "@[[%s:%a].%a@]" id pp_term w pp_term t
+
+let pp_par frm (qid, w) =
+    F.fprintf frm "%s:%a" (string_of_qid qid) pp_term w
+
+let pp_pars = pp_list pp_par "[" "," "]"
+
+let pp_body frm = function
+   | None            -> ()
+   | Some (trans, t) ->
+      F.fprintf frm "%s%a" (string_of_transparent trans) pp_term t
+
+let pp_item frm (l, pars, qid, u, body) =
+   F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" 
+      l (string_of_qid qid) pp_pars pars pp_body body pp_term u
+
+let pp_environment f frm genv =
+   List.iter (pp_item frm) genv; f ()