Mentions légales du service

Skip to content
Snippets Groups Projects

Improve the printing of n-ary abstraction and type abstraction.

Merged MARTINOT Olivier requested to merge omartino/inferno:n-ary-fun-printing into master
1 unresolved thread
3 files
+ 44
27
Compare changes
  • Side-by-side
  • Inline
Files
3
+ 10
15
@@ -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]
[{}]
()
Loading