Skip to content

Commit

Permalink
Minigent recursive types (#329)
Browse files Browse the repository at this point in the history 
Recursive Types for Minigent:
* Adds `mu` keyword for boxed record syntax
* Adds extra rules to solver for permitting recursive types
* Adds termination checking phase as per thesis
  • Loading branch information
@emmet-m
emmet-m authored Dec 17, 2019
1 parent 4d75b4f commit 4fca630
Show file tree
Hide file tree
Showing 54 changed files with 1,209 additions and 244 deletions.
3 changes: 2 additions & 1 deletion minigent/.gitignore
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
.stack-work/
minigent.cabal
*~
stack.yaml.lock
*~
4 changes: 2 additions & 2 deletions minigent/examples/3_records/04-double-take/expected.err
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
Typecheck failed in function foo
• {x : Foo take}# :< {x : Foo,𝛈...}#
• Drop {x : Foo take,𝛈...}#
• {x : Foo take}# :< {x : Foo,𝛉...}#
• Drop {x : Foo take,𝛉...}#
Empty file added minigent/examples/6_recursive/01-basic/expected.err
View file
Empty file.
13 changes: 13 additions & 0 deletions minigent/examples/6_recursive/01-basic/expected.out
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
alloc : Unit -> mu t {l : <Cons {d : U8,r : rec t}#|End Unit> take};
makeEmptyList : Unit -> mu t {l : <Cons {d : U8,r : rec t}#|End Unit>};
makeEmptyList a = let r = (alloc[] : Unit
-> mu t {l : <Cons {d : U8,r : rec t}#
|End Unit> take}) (Unit : Unit) : mu t {l : <Cons {d : U8
,r : rec t}#
|End Unit> take}
in put r : mu t {l : <Cons {d : U8,r : rec t}#
|End Unit> take}.l := End (Unit : Unit) : <Cons {d : U8
,r : rec t}#
|End Unit>
end : mu t {l : <Cons {d : U8,r : rec t}#|End Unit>}
end : mu t {l : <Cons {d : U8,r : rec t}#|End Unit>};
7 changes: 7 additions & 0 deletions minigent/examples/6_recursive/01-basic/in.minigent
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
alloc : Unit -> mu t { l : < End Unit | Cons { d : U8, r : t }# > take };

makeEmptyList : Unit -> mu t { l : < End Unit | Cons { d : U8, r : t }# > };
makeEmptyList a =
let r = alloc Unit in
put r.l := End Unit end
end;
Empty file added minigent/examples/6_recursive/02-poly/expected.err
View file
Empty file.
18 changes: 18 additions & 0 deletions minigent/examples/6_recursive/02-poly/expected.out
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
allocNode : [a]
.
Unit -> mu t {l : <Cons {data : a,rest : rec t}#|Nil Unit> take};
createEmptyList : [a]
.
U8 -> mu t {l : <Cons {data : a,rest : rec t}#|Nil Unit>};
createEmptyList a = let node = (allocNode[a] : Unit
-> mu t {l : <Cons {data : a
,rest : rec t}#
|Nil Unit> take}) (Unit : Unit) : mu t {l : <Cons {data : a
,rest : rec t}#
|Nil Unit> take}
in put node : mu t {l : <Cons {data : a,rest : rec t}#
|Nil Unit> take}.l := Nil (Unit : Unit) : <Cons {data : a
,rest : rec t}#
|Nil Unit>
end : mu t {l : <Cons {data : a,rest : rec t}#|Nil Unit>}
end : mu t {l : <Cons {data : a,rest : rec t}#|Nil Unit>};
9 changes: 9 additions & 0 deletions minigent/examples/6_recursive/02-poly/in.minigent
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
allocNode : [a]. Unit -> mu t { l: < Nil Unit | Cons { data: a, rest: t }# > take };

createEmptyList : [a]. U8 -> mu t { l : < Nil Unit | Cons { data : a, rest : t }# >};
createEmptyList a =
let node = allocNode Unit in
put node.l := Nil Unit end
end;


2 changes: 2 additions & 0 deletions minigent/examples/6_recursive/03-non-strictly-positive/expected.err
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
Reorg failed.
Variables occuring non-strictly positive: t
Empty file added minigent/examples/6_recursive/03-non-strictly-positive/expected.out
View file
Empty file.
2 changes: 2 additions & 0 deletions minigent/examples/6_recursive/03-non-strictly-positive/in.minigent
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
listop : Unit -> mu t { f : (t -> U8) };
listop a = { f = End Unit };
2 changes: 2 additions & 0 deletions minigent/examples/6_recursive/04-harder-non-strictly-positive/expected.err
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
Reorg failed.
Variables occuring non-strictly positive: t
Empty file added minigent/examples/6_recursive/04-harder-non-strictly-positive/expected.out
View file
Empty file.
12 changes: 12 additions & 0 deletions minigent/examples/6_recursive/04-harder-non-strictly-positive/in.minigent
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
listop : Unit ->
mu t {
f : < Left U8
| Midde Unit
| Right {
a : U64,
b: (((U8 -> t) -> U8) -> Unit)
}
>
};

listop a = { f = Middle Unit };
Empty file added minigent/examples/6_recursive/05-strictly-positive-allowed/expected.err
View file
Empty file.
3 changes: 3 additions & 0 deletions minigent/examples/6_recursive/05-strictly-positive-allowed/expected.out
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
id : mu t {l : <End Unit|Rest {a : U8,b : rec t}>}
-> mu t {l : <End Unit|Rest {a : U8,b : rec t}>};
id a = a : mu t {l : <End Unit|Rest {a : U8,b : rec t}>};
2 changes: 2 additions & 0 deletions minigent/examples/6_recursive/05-strictly-positive-allowed/in.minigent
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
id : mu t { l : < End Unit | Rest { a : U8, b : t } > } -> mu t { l : < End Unit | Rest { a : U8, b : t } > };
id a = a;
Empty file added minigent/examples/6_recursive/06-list-push/expected.err
View file
Empty file.
32 changes: 32 additions & 0 deletions minigent/examples/6_recursive/06-list-push/expected.out
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
allocNode : [a]
.
Unit -> mu t {l : <Cons {data : a,rest : rec t}#|Nil Unit> take};
push : [a]
.
{data : a,list : mu t {l : <Cons {data : a,rest : rec t}#|Nil Unit>}}#
-> mu t {l : <Cons {data : a,rest : rec t}#|Nil Unit>};
push r = let node = (allocNode[a] : Unit
-> mu t {l : <Cons {data : a,rest : rec t}#
|Nil Unit> take}) (Unit : Unit) : mu t {l : <Cons {data : a
,rest : rec t}#
|Nil Unit> take}
in take r2 { data = x } = r : {data : a
,list : mu t {l : <Cons {data : a
,rest : rec t}#
|Nil Unit>}}#
in take r3 { list = y } = r2 : {data : a take
,list : mu t {l : <Cons {data : a
,rest : rec t}#
|Nil Unit>}}#
in put node : mu t {l : <Cons {data : a,rest : rec t}#
|Nil Unit> take}.l := Cons ({data = x : a
,rest = y : mu t {l : <Cons {data : a
,rest : rec t}#
|Nil Unit>}} : {data : a
,rest : rec t}#) : <Cons {data : a
,rest : rec t}#
|Nil Unit>
end : mu t {l : <Cons {data : a,rest : rec t}#|Nil Unit>}
end : mu t {l : <Cons {data : a,rest : rec t}#|Nil Unit>}
end : mu t {l : <Cons {data : a,rest : rec t}#|Nil Unit>}
end : mu t {l : <Cons {data : a,rest : rec t}#|Nil Unit>};
12 changes: 12 additions & 0 deletions minigent/examples/6_recursive/06-list-push/in.minigent
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
allocNode : [a]. Unit -> mu t { l: < Nil Unit | Cons { data: a, rest: t }# > take };

push : [a]. { data: a, list: mu t { l: < Nil Unit | Cons { data: a, rest: t }# > } }#
-> mu t { l: < Nil Unit | Cons { data: a, rest: t }# >};
push r =
let node = allocNode Unit in
take r2 { data = x } = r in
take r3 { list = y } = r2 in
put node.l := Cons { data = x, rest = y } end
end
end
end;
Empty file added minigent/examples/6_recursive/07-self-calling/expected.err
View file
Empty file.
12 changes: 12 additions & 0 deletions minigent/examples/6_recursive/07-self-calling/expected.out
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
add : {x : U8,y : U8}# -> U8;
add r = take r2 { x = a } = r : {x : U8,y : U8}#
in take r3 { y = b } = r2 : {x : U8 take,y : U8}#
in if (a : U8) == (0 : U8) : Bool
then b : U8
else (add[] : {x : U8,y : U8}#
-> U8) ({x = (a : U8) - (1 : U8) : U8
,y = (b : U8) + (1 : U8) : U8} : {x : U8
,y : U8}#) : U8
end : U8
end : U8
end : U8;
9 changes: 9 additions & 0 deletions minigent/examples/6_recursive/07-self-calling/in.minigent
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
add : { x: U8, y: U8 }# -> U8;
add r =
take r2 { x = a } = r in
take r3 { y = b } = r2 in
if a == 0 then b
else add { x = a-1, y = b+1 }
end
end
end;
Empty file added minigent/examples/6_recursive/08-list-sum/expected.err
View file
Empty file.
22 changes: 22 additions & 0 deletions minigent/examples/6_recursive/08-list-sum/expected.out
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
sumList : mu t {l : <Cons {data : U32,rest : rec t!}#|Nil Unit>}! -> U32;
sumList r = take r2 { l = z } = r : mu t {l : <Cons {data : U32,rest : rec t!}#
|Nil Unit>}!
in case z : <Cons {data : U32,rest : rec t!}#|Nil Unit> of
Nil u -> 0 : U32
| v2 -> case v2 : <Cons {data : U32,rest : rec t!}#
|Nil Unit take> of
Cons s -> take s2 { rest = x } = s : {data : U32
,rest : mu t {l : <Cons {data : U32
,rest : rec t!}#
|Nil Unit>}!}#
in ((s : {data : U32
,rest : rec t!}#).data : U32) + ((sumList[ ] : mu t {l : <Cons {data : U32
,rest : rec t!}#
|Nil Unit>}!
-> U32) (x : mu t {l : <Cons {data : U32
,rest : rec t!}#
|Nil Unit>}!) : U32) : U32
end : U32
end : U32
end : U32
end : U32;
14 changes: 14 additions & 0 deletions minigent/examples/6_recursive/08-list-sum/in.minigent
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
sumList : mu t { l: < Nil Unit | Cons { data: U32, rest: t! }# >}! -> U32;
sumList r =
take r2 { l = z } = r in
case z of
Nil u -> 0
| v2 ->
case v2 of
Cons s ->
take s2 { rest = x } = s in
s.data + sumList x
end
end
end
end;
Empty file added minigent/examples/6_recursive/09-map/expected.err
View file
Empty file.
Loading

0 comments on commit 4fca630

Please sign in to comment.