open CicNotationEnv
open CicNotationPt
+let print_attributes = true
+
let pp_binder = function
| `Lambda -> "lambda"
| `Pi -> "Pi"
| `Number s -> s)
let rec pp_term = function
+ | AttributedTerm (_, term) when print_attributes ->
+ sprintf "@[%s]" (pp_term term)
| AttributedTerm (_, term) -> pp_term term
| Appl terms ->
sprintf "\\VBOX [%s]" (String.concat " " (List.map pp_term terms))
and pp_magic = function
- | List0 (t, sep_opt) -> sprintf "\\LIST0 %s%s" (pp_term t) (pp_sep_opt sep_opt)
- | List1 (t, sep_opt) -> sprintf "\\LIST1 %s%s" (pp_term t) (pp_sep_opt sep_opt)
+ | List0 (t, sep_opt) ->
+ sprintf "\\LIST0 %s%s" (pp_term t) (pp_sep_opt sep_opt)
+ | List1 (t, sep_opt) ->
+ sprintf "\\LIST1 %s%s" (pp_term t) (pp_sep_opt sep_opt)
| Opt t -> sprintf "\\OPT %s" (pp_term t)
- | _ -> failwith "magic not implemented"
+ | Fold (k, p_base, names, p_rec) ->
+ let acc = match names with acc :: _ -> acc | _ -> assert false in
+ sprintf "\\FOLD %s \\[%s\\] \\LAMBDA %s \\[%s\\]"
+ (pp_fold_kind k) (pp_term p_base) acc (pp_term p_rec)
+ | Default (p_some, p_none) ->
+ sprintf "\\DEFAULT \\[%s\\] \\[%s\\]" (pp_term p_some) (pp_term p_none)
+
+and pp_fold_kind = function
+ | `Left -> "left"
+ | `Right -> "right"
and pp_sep_opt = function
| None -> ""