ported to latest Ast changes (mainly capture_variable addition)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml
index 83da7724478a8f29f49e5ecdbc7f67f9548177b7..896e1dcc32cff08cf973e8671b0e8f53f81f1e3b 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml
@@ -32,7 +32,11 @@ let pp_binder = function
   | `Exists -> "exists"
   | `Forall -> "forall"
 
-let rec pp_term = function
+let pp_name = function Cic.Anonymous -> "_" | Cic.Name s -> s
+let rec pp_capture_variable = function
+  | name, None -> pp_name name
+  | name, Some typ -> "(" ^ pp_name name ^ ": " ^ pp_term typ ^ ")"
+and pp_term = function
   | LocatedTerm ((p_begin, p_end), term) ->
 (*       sprintf "[%d,%d]%s" p_begin p_end (pp_term term) *)
       pp_term term
@@ -40,26 +44,23 @@ let rec pp_term = function
   | 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)
-        (match var with Cic.Anonymous -> "_" | Cic.Name s -> s)
-        (match typ with None -> "" | Some typ -> ": " ^ pp_term typ)
+  | Binder (kind, var, body) ->
+      sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var)
         (pp_term body)
   | 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)
+  | LetIn (var, t1, t2) ->
+      sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1)
+        (pp_term t2)
   | 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) ->
-              sprintf "%s%s = %s" name
-                (match typ with None -> "" | Some typ -> ": " ^ pp_term typ)
-                (pp_term body))
+            (fun (var, body, _) ->
+              sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
             definitions))
         (pp_term term)
   | Ident (name, []) -> name
@@ -77,11 +78,13 @@ let rec pp_term = function
 and pp_subst (name, term) = sprintf "%s := %s" name (pp_term term)
 and pp_substs substs = String.concat "; " (List.map pp_subst substs)
 
-and pp_pattern (names, term) =
+and pp_pattern ((head, vars), term) =
   sprintf "%s -> %s"
-    (match names with
-    | [n] -> n
-    | names -> "(" ^ String.concat " " names ^ ")")
+    (match vars with
+    | [] -> head
+    | _ ->
+        sprintf "(%s %s)" head
+          (String.concat " " (List.map pp_capture_variable vars)))
     (pp_term term)
 
 and pp_patterns patterns =