- Unified : some definitions of unified \lambda\delta

[helm.git] / helm / software / components / acic_content / cicNotationPp.ml

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index a23d26add935eef6a406e1cc1a7a55bee7621f35..568faa927155143f892cd598264fa775c9cf80bf 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -92,10 +92,10 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Binder (`Pi, (Ast.Ident ("_", None), typ), body) ->
         sprintf "%s \\to %s"
           (match typ with None -> "?" | Some typ -> pp_term typ)
-          (pp_term body)
+          (pp_term ~pp_parens:true body)
     | Ast.Binder (kind, var, body) ->
         sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var)
-          (pp_term body)
+          (pp_term ~pp_parens:true body)
     | Ast.Case (term, indtype, typ, patterns) ->
         sprintf "match %s%s%s with %s"
           (pp_term term)
@@ -109,10 +109,10 @@ let rec pp_term ?(pp_parens = true) t =
                   sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
               | _ -> ""))
           (pp_patterns patterns)
-    | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2)
+    | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
     | Ast.LetIn (var, t1, t2) ->
-        sprintf "let %s \\def %s in %s" (pp_capture_variable var) (pp_term t1)
-          (pp_term t2)
+        sprintf "let %s \\def %s in %s" (pp_capture_variable var) (pp_term ~pp_parens:true t1)
+          (pp_term ~pp_parens:true t2)
     | Ast.LetRec (kind, definitions, term) ->
         sprintf "let %s %s in %s"
           (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
@@ -147,8 +147,11 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Magic m -> pp_magic m
     | Ast.Variable v -> pp_variable v
   in
-  if pp_parens then sprintf "(%s)\n" t_pp
-  else t_pp
+  match pp_parens, t with
+    | false, _ 
+    | true, Ast.Ident (_, Some []) 
+    | true, Ast.Ident (_, None)    -> t_pp
+    | _                            -> sprintf "(%s)" t_pp
 
 and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
 and pp_substs substs = String.concat "; " (List.map pp_subst substs)
@@ -172,13 +175,9 @@ and pp_patterns patterns =
   sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns))
 
 and pp_capture_variable = 
-  let clean s = 
-    let s = String.sub s 1 (String.length s - 1) in
-    String.sub s 0 (String.length s - 2) 
-  in
   function
-  | term, None -> pp_term term
-  | term, Some typ -> "(" ^ clean (pp_term term) ^ ": " ^ pp_term typ ^ ")"
+  | term, None -> pp_term ~pp_parens:false term
+  | term, Some typ -> "(" ^ pp_term ~pp_parens:false term ^ ": " ^ pp_term typ ^ ")"
 
 and pp_box_spec (kind, spacing, indent) =
   let int_of_bool b = if b then 1 else 0 in