| `Set -> "Set"
| `CProp _ -> "CProp"
| `Type _ -> "Type"
+ | `NType s -> "Type[" ^ s ^ "]"
+ | `NCProp s -> "CProp[" ^ s ^ "]"
+
+let map_space f l =
+ HExtlib.list_concat
+ ~sep:[space] (List.map (fun x -> [f x]) l)
+;;
let pp_ast0 t k =
let rec aux =
let mk_case_pattern =
function
Ast.Pattern (head, href, vars) ->
- hvbox true false (ident_w_href href head :: List.map aux_var vars)
+ hvbox true true (ident_w_href href head ::
+ List.flatten (List.map (fun x -> [break;x]) (map_space aux_var vars)))
| Ast.Wildcard -> builtin_symbol "_"
in
let patterns' =
List.map
(fun (lhs, rhs) ->
remove_level_info
- (hvbox false true [
- hbox false true [
- mk_case_pattern lhs; builtin_symbol "\\Rightarrow" ];
+ (hovbox false true [
+ mk_case_pattern lhs; break; builtin_symbol "\\Rightarrow";
break; top_pos (k rhs) ]))
patterns
in
match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
in
let mk_fun (args, (name,ty), body, rec_param) =
- List.map aux_var args ,k name, HExtlib.map_option k ty, k body,
- fst (List.nth args rec_param)
+ List.flatten (List.map (fun x -> [aux_var x; space]) args),
+ k name, HExtlib.map_option k ty, k body, fst (List.nth args rec_param)
in
let mk_funs = List.map mk_fun in
let fst_fun, tl_funs =
space;
keyword rec_op;
space;
- name] @
+ name;
+ space] @
params @
- [space; keyword "on" ; space ; rec_param ;space ] @
+ [keyword "on" ; space ; rec_param ;space ] @
(match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @
[ builtin_symbol "\\def";
break;
(fun (params, name, ty, body, rec_param) ->
[ break;
hvbox false true ([
- keyword "and";
+ keyword "and"; space;
name] @
params @
[space; keyword "on" ; space; rec_param ;space ] @
((hvbox false false
(fst_row :: List.flatten tl_rows
@ [ break; keyword "in"; break; k where ])))
- | Ast.Implicit -> builtin_symbol "?"
+ | Ast.Implicit `JustOne -> builtin_symbol "?"
+ | Ast.Implicit `Vector -> builtin_symbol "…"
| Ast.Meta (n, l) ->
let local_context l =
List.map (function None -> None | Some t -> Some (k t)) l
Ast.Ident (name, Some (aux_substs env substs))
| Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
- | Ast.Implicit
+ | Ast.Implicit _
| Ast.Ident _
| Ast.Num _
| Ast.Sort _
| Ast.Magic magic -> aux_magic env magic
| Ast.Variable var -> aux_variable env var
+ | Ast.Cast (t, ty) -> Ast.Cast (aux env t, aux env ty)
+
| _ -> assert false
and aux_opt env = function
| Some term -> Some (aux env term)