Minigent recursive types (#329)

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

minigent/.gitignore

@@ -1,3 +1,4 @@
 .stack-work/
 minigent.cabal
-*~
+stack.yaml.lock
+*~

minigent/examples/3_records/04-double-take/expected.err

@@ -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,𝛉...}#

minigent/examples/6_recursive/01-basic/expected.out

@@ -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>};

minigent/examples/6_recursive/01-basic/in.minigent

@@ -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;

minigent/examples/6_recursive/02-poly/expected.out

@@ -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>};

minigent/examples/6_recursive/02-poly/in.minigent

@@ -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;
+
+

minigent/examples/6_recursive/03-non-strictly-positive/expected.err

@@ -0,0 +1,2 @@
+Reorg failed.
+Variables occuring non-strictly positive: t

minigent/examples/6_recursive/03-non-strictly-positive/in.minigent

@@ -0,0 +1,2 @@
+listop : Unit -> mu t { f : (t -> U8) };
+listop a = { f = End Unit };

minigent/examples/6_recursive/04-harder-non-strictly-positive/expected.err

@@ -0,0 +1,2 @@
+Reorg failed.
+Variables occuring non-strictly positive: t

minigent/examples/6_recursive/04-harder-non-strictly-positive/in.minigent

@@ -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 };

minigent/examples/6_recursive/05-strictly-positive-allowed/expected.out

@@ -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}>};

minigent/examples/6_recursive/05-strictly-positive-allowed/in.minigent

@@ -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;

minigent/examples/6_recursive/06-list-push/expected.out

@@ -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>};

minigent/examples/6_recursive/06-list-push/in.minigent

@@ -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;

minigent/examples/6_recursive/07-self-calling/expected.out

@@ -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;

minigent/examples/6_recursive/07-self-calling/in.minigent

@@ -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;

minigent/examples/6_recursive/08-list-sum/expected.out

@@ -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;

minigent/examples/6_recursive/08-list-sum/in.minigent

@@ -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;