debian version 0.6.3-2

[helm.git] / helm / ocaml / cic_transformations / cicAstPp.ml

diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml
index b1e6588766beeeb2b9b3fa1414cdfb2e06ec5871..2cc83e74312f8f2e62ac70ab9835048553fcedc4 100644 (file)
--- a/helm/ocaml/cic_transformations/cicAstPp.ml
+++ b/helm/ocaml/cic_transformations/cicAstPp.ml
@@ -27,7 +27,7 @@ open Printf
 
 let pp_binder = function
   | `Lambda -> "lambda"
-  | `Pi -> "pi"
+  | `Pi -> "Pi"
   | `Exists -> "exists"
   | `Forall -> "forall"
 
@@ -38,6 +38,11 @@ let rec pp_term = function
 
   | CicAst.Appl terms ->
       sprintf "(%s)" (String.concat " " (List.map pp_term terms))
+  | CicAst.Binder (`Forall, (Cic.Anonymous, typ), body)
+  | CicAst.Binder (`Pi, (Cic.Anonymous, typ), body) ->
+      sprintf "(%s \\to %s)"
+        (match typ with None -> "?" | Some typ -> pp_term typ)
+        (pp_term body)
   | CicAst.Binder (kind, var, body) ->
       sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var)
         (pp_term body)
@@ -57,8 +62,10 @@ let rec pp_term = function
               sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
             definitions))
         (pp_term term)
-  | CicAst.Ident (name, []) -> name
-  | CicAst.Ident (name, substs) -> sprintf "%s[%s]" name (pp_substs substs)
+  | CicAst.Ident (name, Some [])
+  | CicAst.Ident (name, None) ->
+      name
+  | CicAst.Ident (name, Some substs) -> sprintf "%s \\subst [%s]" name (pp_substs substs)
   | CicAst.Implicit -> "?"
   | CicAst.Meta (index, substs) ->
       sprintf "%d[%s]" index
@@ -71,11 +78,11 @@ let rec pp_term = function
   | CicAst.Sort `CProp -> "CProp"
   | CicAst.Symbol (name, _) -> name
 
-and pp_subst (name, term) = sprintf "%s := %s" name (pp_term term)
+and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
 and pp_substs substs = String.concat "; " (List.map pp_subst substs)
 
 and pp_pattern ((head, vars), term) =
-  sprintf "%s -> %s"
+  sprintf "%s \Rightarrow %s"
     (match vars with
     | [] -> head
     | _ ->