still a working copy, now towards a cleaner implementation ...

[helm.git] / helm / ocaml / cic_disambiguation / pp.ml

diff --git a/helm/ocaml/cic_disambiguation/pp.ml b/helm/ocaml/cic_disambiguation/pp.ml
index 6ee9cf39a432774d11a273c0678506056ae5d19c..c4b04351c5c7a985b45968a74fc44e4277718cb2 100644 (file)
--- a/helm/ocaml/cic_disambiguation/pp.ml
+++ b/helm/ocaml/cic_disambiguation/pp.ml
@@ -1,3 +1,27 @@
+(* Copyright (C) 2004, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
 
 open Ast
 open Printf
@@ -10,21 +34,26 @@ let pp_binder = function
 
 let rec pp_term = function
   | LocatedTerm ((p_begin, p_end), term) ->
-      sprintf "[%d,%d]%s" p_begin p_end (pp_term term)
+(*       sprintf "[%d,%d]%s" p_begin p_end (pp_term term) *)
+      pp_term term
 
   | Appl terms -> sprintf "(%s)" (String.concat " " (List.map pp_term terms))
+  | Appl_symbol (symbol, terms) ->
+      sprintf "(%s %s)" symbol (String.concat " " (List.map pp_term terms))
   | Binder (kind, var, typ, body) ->
-      sprintf "\\%s %s%s.%s" (pp_binder kind) var
+      sprintf "\\%s %s%s.%s" (pp_binder kind)
+        (match var with Cic.Anonymous -> "_" | Cic.Name s -> s)
         (match typ with None -> "" | Some typ -> ": " ^ pp_term typ)
         (pp_term body)
-  | Case (term, typ, patterns) ->
+  | Case (term, indtype, typ, patterns) ->
       sprintf "%smatch %s with %s"
         (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t))
         (pp_term term) (pp_patterns patterns)
   | LetIn (name, t1, t2) ->
       sprintf "let %s = %s in %s" name (pp_term t1) (pp_term t2)
-  | LetRec (definitions, term) ->
-      sprintf "let rec %s in %s"
+  | LetRec (kind, definitions, term) ->
+      sprintf "let %s %s in %s"
+        (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
         (String.concat " and "
           (List.map
             (fun (name, body, typ, index) ->
@@ -35,11 +64,15 @@ let rec pp_term = function
         (pp_term term)
   | Ident (name, []) -> name
   | Ident (name, substs) -> sprintf "%s[%s]" name (pp_substs substs)
-  | Meta (name, substs) ->
-      sprintf "%s[%s]" name
+  | Meta (index, substs) ->
+      sprintf "%d[%s]" index
         (String.concat "; "
           (List.map (function None -> "_" | Some term -> pp_term term) substs))
-  | Int num -> string_of_int num
+  | Num num -> num
+  | Sort `Set -> "Set"
+  | Sort `Prop -> "Prop"
+  | Sort `Type -> "Type"
+  | Sort `CProp -> "CProp"
 
 and pp_subst (name, term) = sprintf "%s := %s" name (pp_term term)
 and pp_substs substs = String.concat "; " (List.map pp_subst substs)