let hvbox = box Ast.HV
let hovbox = box Ast.HOV
let break = Ast.Layout Ast.Break
+let space = Ast.Literal (`Symbol " ")
let builtin_symbol s = Ast.Literal (`Symbol s)
let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k))
match outty_opt with
| None -> []
| Some outty ->
- [ keyword "return"; break; remove_level_info (k outty)]
+ [ space; keyword "return"; space; break; remove_level_info (k outty)]
in
let indty_box =
match indty_opt with
| None -> []
- | Some (indty, href) -> [ keyword "in"; break; ident_w_href href indty ]
+ | Some (indty, href) -> [ space; keyword "in"; space; break; ident_w_href href indty ]
in
let match_box =
hvbox false false [
hvbox false true [
- hvbox false true [ keyword "match"; break; top_pos (k what) ];
+ hvbox false true [keyword "match"; space; break; top_pos (k what)];
break;
hvbox false true indty_box;
break;
hvbox false true outty_box
];
break;
- keyword "with"
+ space;
+ keyword "with";
+ space
]
in
let mk_case_pattern (head, href, vars) =
let rec_op =
match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
in
- let mk_fun (var, body, _) = aux_var var, k body in
+ let mk_fun (args, (name,ty), body, _) =
+ List.map aux_var args ,k name, HExtlib.map_option k ty, k body in
let mk_funs = List.map mk_fun in
let fst_fun, tl_funs =
match mk_funs funs with hd :: tl -> hd, tl | [] -> assert false
in
let fst_row =
- let (name, body) = fst_fun in
- hvbox false true [
- keyword "let"; keyword rec_op; name; builtin_symbol "\\def"; break;
- top_pos body ]
+ let (params, name, ty, body) = fst_fun in
+ hvbox false true ([
+ keyword "let";
+ space;
+ keyword rec_op;
+ space;
+ name] @
+ params @
+ (match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @
+ [ builtin_symbol "\\def";
+ break;
+ top_pos body ])
in
let tl_rows =
List.map
- (fun (name, body) ->
+ (fun (params, name, ty, body) ->
[ break;
- hvbox false true [
- keyword "and"; name; builtin_symbol "\\def"; break; body ] ])
+ hvbox false true ([
+ keyword "and";
+ name] @
+ params @
+ (match ty with
+ None -> []
+ | Some ty -> [builtin_symbol ":"; ty]) @
+ [ builtin_symbol "\\def"; break; body ])])
tl_funs
in
add_level_info Ast.let_in_prec Ast.let_in_assoc
| Ast.Implicit -> builtin_symbol "?"
| Ast.Meta (n, l) ->
let local_context l =
- CicNotationUtil.dress (builtin_symbol ";")
- (List.map (function None -> builtin_symbol "_" | Some t -> k t) l)
+ List.map (function None -> None | Some t -> Some (k t)) l
in
- hbox false false
- ([ builtin_symbol "?"; number (string_of_int n) ]
- @ (if l <> [] then local_context l else []))
+ Ast.Meta(n, local_context l)
| Ast.Sort sort -> aux_sort sort
| Ast.Num _
| Ast.Symbol _
(aux_pattern env pattern, aux env term)
and aux_pattern env (head, hrefs, vars) =
(head, hrefs, List.map (aux_capture_var env) vars)
- and aux_definition env (var, term, i) =
- (aux_capture_var env var, aux env term, i)
+ and aux_definition env (params, var, term, i) =
+ (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i)
and aux_substs env substs =
List.map (fun (name, term) -> (name, aux env term)) substs
and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs