| 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 "%smatch %s%s with %s"
- (match typ with None -> "" | Some t -> sprintf "[%s]" (pp_term t))
+ sprintf "match %s%s%s with %s"
(pp_term term)
+ (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))
(match indtype with
| None -> ""
| Some (ty, href_opt) ->
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 = %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")
| Ast.Magic m -> pp_magic m
| Ast.Variable v -> pp_variable v
in
- if pp_parens then sprintf "(%s)" 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)
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 - 1)
- 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
| Ast.Ascription (t, n) -> assert false
| Ast.FreshVar n -> "fresh " ^ n
-let pp_term t = pp_term ~pp_parens:false t
+let _pp_term = ref (pp_term ~pp_parens:false)
+let pp_term t = !_pp_term t
+let set_pp_term f = _pp_term := f
let pp_params = function
| [] -> ""