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) =
- hbox true false (ident_w_href href head :: List.map aux_var vars)
+ let mk_case_pattern =
+ function
+ Ast.Pattern (head, href, vars) ->
+ hbox true false (ident_w_href href head :: List.map aux_var vars)
+ | Ast.Wildcard -> builtin_symbol "_"
in
let patterns' =
List.map
add_level_info Ast.let_in_prec Ast.let_in_assoc
(hvbox false true [
hvbox false true [
- keyword "let";
+ keyword "let"; space;
hvbox false true [
- aux_var var; builtin_symbol "\\def"; break; top_pos (k s) ];
- break; keyword "in" ];
+ aux_var var; space;
+ builtin_symbol "\\def"; break; top_pos (k s) ];
+ break; space; keyword "in" ];
break;
k t ])
| Ast.LetRec (rec_kind, funs, where) ->
let rec_op =
match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
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_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)
+ 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 (params, name, ty, body) = fst_fun in
+ let (params, name, ty, body, rec_param) = fst_fun in
hvbox false true ([
keyword "let";
+ space;
keyword rec_op;
+ space;
name] @
params @
+ [space; keyword "on" ; space ; rec_param ;space ] @
(match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @
[ builtin_symbol "\\def";
break;
in
let tl_rows =
List.map
- (fun (params, name, ty, body) ->
+ (fun (params, name, ty, body, rec_param) ->
[ break;
hvbox false true ([
keyword "and";
name] @
params @
+ [space; keyword "on" ; space; rec_param ;space ] @
(match ty with
None -> []
| Some ty -> [builtin_symbol ":"; ty]) @
in
aux true l1_pattern *)
+let counter = ref ~-1
+let reset () = counter := ~-1;;
let fresh_id =
- let counter = ref ~-1 in
fun () ->
incr counter;
!counter
| Ast.Case (term, indty, outty_opt, patterns) ->
Ast.Case (aux env term, indty, aux_opt env outty_opt,
List.map (aux_branch env) patterns)
- | Ast.LetIn (var, t1, t2) ->
- Ast.LetIn (aux_capture_var env var, aux env t1, aux env t2)
+ | Ast.LetIn (var, t1, t3) ->
+ Ast.LetIn (aux_capture_var env var, aux env t1, aux env t3)
| Ast.LetRec (kind, definitions, body) ->
Ast.LetRec (kind, List.map (aux_definition env) definitions,
aux env body)
and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
and aux_branch env (pattern, term) =
(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_pattern env =
+ function
+ Ast.Pattern (head, hrefs, vars) ->
+ Ast.Pattern (head, hrefs, List.map (aux_capture_var env) vars)
+ | Ast.Wildcard -> Ast.Wildcard
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 =
let _ = load_patterns21 []
+
+