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) ->
- let strip i t =
- let rec aux i l = function
- | Ast.Binder (_, var, body) when i > 0 -> aux (pred i) (var :: l) body
- | body -> List.rev l, body
- in
- aux i [] t
- in
let rec get_guard i = function
| [] -> (*assert false*) Ast.Implicit
| [term, _] when i = 1 -> term
| _ :: tl -> get_guard (pred i) tl
in
- let map (var, body, i) =
- let id, vars, typ, body = match var with
- | term, Some typ ->
- let pvars, pbody = strip i typ in
- let _, bbody = strip i body in
- term, pvars, pbody, bbody
- | term, None ->
- let pbody = Ast.Implicit in
- let pvars, bbody = strip i body in
- term, pvars, pbody, bbody
- in
+ let map (params, (id,typ), body, i) =
+ let typ =
+ match typ with
+ None -> Ast.Implicit
+ | Some typ -> typ
+ in
sprintf "%s %s on %s: %s \\def %s"
(pp_term ~pp_parens:false term)
- (String.concat " " (List.map pp_capture_variable vars))
- (pp_term ~pp_parens:false (get_guard i vars))
+ (String.concat " " (List.map pp_capture_variable params))
+ (pp_term ~pp_parens:false (get_guard i params))
(pp_term typ) (pp_term body)
in
sprintf "let %s %s in %s"
let pp_params = function
| [] -> ""
- | params ->
- " " ^
- String.concat " "
- (List.map
- (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term typ))
- params)
+ | params -> " " ^ String.concat " " (List.map pp_capture_variable params)
let pp_flavour = function
| `Definition -> "definition"