Improve printing of n-ary abstraction and type abstraction.

This commit is contained in:
Olivier 2022-09-16 15:14:25 +02:00
parent 4b3e0aefb1
commit d9ce1246e7
3 changed files with 44 additions and 27 deletions

View File

@ -67,8 +67,10 @@ let term :=
| ~ = term_abs ; <>
let term_abs :=
| FUN ; x = tevar_ ; "->" ; t = term_abs ;
{ Abs ($loc, x, t) }
| FUN ; xs = list (tevar_) ; "->" ; t = term_abs ;
{
List.fold_right (fun x t -> Abs ($loc, x, t)) xs t
}
| (x, t1, t2) = letin(tevar) ; { Let ($loc, x, t1, t2) }

View File

@ -110,6 +110,30 @@ let print_let_in lhs rhs body =
^^ string "in"
^^ prefix 0 1 empty body
let rec flatten_tyabs t =
match t with
| TyAbs (x, t) ->
let (xs, t) = flatten_tyabs t in
(x::xs, t)
| t ->
([], t)
let rec flatten_abs t =
match t with
| Abs (p, t) ->
let (ps, t) = flatten_abs t in
(p::ps, t)
| t ->
([], t)
let print_nary_abstraction abs print_arg args rhs =
string abs
^^ space
^^ separate_map space print_arg args
^^ space
^^ string "->"
^//^ rhs
let print_annot print_elem (rigidity, tyvars, typ) =
let rigidity_kwd =
string @@ match rigidity with
@ -132,21 +156,17 @@ let rec print_term t =
and print_term_abs t =
group @@ match t with
| TyAbs (x, t1) ->
string "FUN" ^^ space
^^ print_tyvar x ^^ space
^^ string "->"
^//^ print_term_abs t1
| TyAbs _ ->
let (xs, t) = flatten_tyabs t in
print_nary_abstraction "FUN" print_tyvar xs (print_term_abs t)
| Let (p, t1, t2) ->
print_let_in
(print_pattern p)
(print_term t1)
(print_term_abs t2)
| Abs (p, t) ->
string "fun" ^^ space
^^ print_pattern p ^^ space
^^ string "->"
^//^ print_term_abs t
| Abs _ ->
let (ps, t) = flatten_abs t in
print_nary_abstraction "fun" print_pattern ps (print_term_abs t)
| t ->
print_term_app t

View File

@ -103,9 +103,8 @@ Option type
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 ->
FUN a1 ->
Some<option {a1 -> a1*a0 -> a0}> (fun (x : a1) -> x, fun (x : a0) -> x)
FUN a0 a1 ->
Some<option {a1 -> a1*a0 -> a0}> (fun (x : a1) -> x, fun (x : a0) -> x)
Converting the System F term to de Bruijn style...
Type-checking the System F term...
@ -223,12 +222,11 @@ Pattern-matching
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 ->
FUN a1 ->
match<option a0> Some<option (a1 -> a1)> (fun (x : a1) -> x) with
| None<option (a1 -> a1)> () -> None<option a0> ()
| (Some<option (a1 -> a1)> _ : option (a1 -> a1)) -> None<option a0> ()
end
FUN a0 a1 ->
match<option a0> Some<option (a1 -> a1)> (fun (x : a1) -> x) with
| None<option (a1 -> a1)> () -> None<option a0> ()
| (Some<option (a1 -> a1)> _ : option (a1 -> a1)) -> None<option a0> ()
end
Converting the System F term to de Bruijn style...
Type-checking the System F term...
@ -311,7 +309,7 @@ It involves a useless universal quantifier.
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
(FUN a1 -> FUN a2 -> (fun (x : a2) -> x : a2 -> a2)) [[a0] a0] [{}] ()
(FUN a1 a2 -> (fun (x : a2) -> x : a2 -> a2)) [[a0] a0] [{}] ()
Converting the System F term to de Bruijn style...
Type-checking the System F term...
@ -330,11 +328,8 @@ and unreachable from the entry point of a type scheme.
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
(FUN a1 ->
FUN a2 ->
(
(fun (x : a1 -> a1) -> fun (y : a2) -> y) (fun (x : a1) -> x) : a2 -> a2
))
(FUN a1 a2 ->
((fun (x : a1 -> a1) (y : a2) -> y) (fun (x : a1) -> x) : a2 -> a2))
[[a0] a0]
[{}]
()