WIP Add derived form for datatypes

1ml-prime · Jan 12, 2020 · 7d43f62 · 7d43f62
1 parent 0cd8d64
commit 7d43f62
Show file tree

Hide file tree

Showing 6 changed files with 320 additions and 25 deletions.
diff --git a/Makefile b/Makefile
@@ -4,8 +4,8 @@
 
 NAME = 1ml
 MODULES = \
-  lib source prim syntax parser lexer \
-  fomega types iL env erase trace sub elab \
+  lib source prim fomega types env syntax \
+  parser lexer iL erase trace sub elab \
   lambda compile \
   main
 NOMLI = syntax iL main

diff --git a/elab.ml b/elab.ml
@@ -557,6 +557,8 @@ Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t));
       ExT([], t), Pure, lift_warn exp.at t env (zs1 @ zs2 @ zs3),
       IL.LetE(e, "_", materialize_typ t)
     )
+  | EL.WithEnvE (toExp) ->
+    elab_exp env (toExp env) l
 
 (*
 rec (X : (b : type) => {type t; type u a}) fun (b : type) => {type t = (X int.u b, X bool.t); type u a = (a, X b.t)}

diff --git a/lexer.mll b/lexer.mll
@@ -70,6 +70,7 @@ rule token = parse
   | "_" { HOLE }
   | "and" { AND }
   | "as" { AS }
+  | "data" { DATA }
   | "do" { DO }
   | "else" { ELSE }
   | "end" { END }

diff --git a/parser.mly b/parser.mly
@@ -35,6 +35,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 %token DOT AT TICK
 %token COMMA SEMI
 %token TYPE_ERROR
+%token DATA
 
 %token EOF
 
@@ -322,6 +323,8 @@ annexp :
 exp :
   | annexp
     { $1 }
+  | DATA name name typparamlist SEAL typ
+    { dataE($2, $3, $4, $6, at())@@at() }
   | FUN param paramlist DARROW exp
     { funE($2::$3, $5)@@at() }
   | IF exp THEN exp ELSE infexp COLON typ

diff --git a/regression.1ml b/regression.1ml
@@ -59,6 +59,112 @@ PolyRec = {
   t0 = @(t int) (right (@(t (type (int, int))) (left (0, 0))));
 };
 
+;;
+
+IT = data case t _ :> {
+  Int  :  Int.t -> case Int.t;
+  Text : Text.t -> case Text.t;
+};
+
+IT = let
+  type I (type t _) (type case _) = {
+    Int  :  Int.t -> case Int.t;
+    Text : Text.t -> case Text.t;
+  };
+  type J (type t _) = {type case _; ...I t case};
+  type T (type t _) x = (c: J t) -> c.case x;
+  ...{
+    t = rec (type t _) => fun (type x) => type wrap T t x;
+    case 'x (type case _) (cs: I t case) e =
+      (unwrap e.@(t _): wrap T t x) {case; ...cs};
+    mk 'x (c: T t x) = @(t x) (wrap c: wrap T t x);
+  } :> {
+    type t _;
+    case 'x: (type case _) => I t case => t x -> case x;
+    mk 'x: T t x => t x;
+  };
+  J = J t;
+in {
+  t; case;
+  Int  v = mk (fun (r: J) => r.Int  v);
+  Text v = mk (fun (r: J) => r.Text v);
+};
+
+IT = {
+  ...IT;
+
+  impossible: t int -> int = case (fun (type t) => t) {
+    Int  x = x;
+    Text x = x;
+  };
+
+  i: int = impossible (Int 9);
+  ;;t: text = impossible (Text "nine");
+};
+
+;;
+
+Ord = data case t :> {
+  Lt : case;
+  Eq : case;
+  Gt : case;
+};
+
+Opt = data case t x :> {
+  None :      case;
+  Some : x -> case;
+};
+
+Alt = {
+  ...data case t l r :> {
+    Left  : l -> case;
+    Right : r -> case;
+  };
+
+  ;;Left  'l 'r (v: l) = mk (fun (r: J t l r) => r.Left v);
+  ;;Right 'l 'r (v: r) = mk (fun (r: J t l r) => r.Right v);
+};
+
+List = let
+  ...let
+    type I (type case) (type t _) x = {
+      nil     :             case;
+      (::) 'n : x -> t x -> case;
+    };
+    type J (type t _) x = {type case; ...I case t x};
+    type T (type t _) x = (c: J t x) -> c.case;
+  in {
+    t = rec (type t _) => fun (type x) => type wrap T t x;
+    case '(type case) 'x 'n (cs: I case t x) (e: t x) =
+      (unwrap e.@(t x): wrap T t x) {case; ...cs};
+    mk 'x (c: T t x) = @(t x) (wrap c: wrap T t x);
+    D = J t;
+  } :> {
+    type t _;
+    case '(type case) 'x 'n: I case t x => t x -> case;
+    mk 'x: T t x => t x;
+    type D x = J t x;
+  };
+in {
+  t; case;
+  nil  'x                     = mk (fun (r: D x) => r.nil);
+  (::) 'x 'n (v: x) (vs: t x) = mk (fun (r: D x) => r.:: v vs);
+};
+
+List' = {
+  ...data case t x :> {
+    nil  :             case;
+    (::) : x -> t x => case;
+  };
+
+;;  nil  'x                  = mk (fun (r: J x) => r.nil);
+;;  (::) 'x (v: x) (vs: t x) = mk (fun (r: J x) => r.:: v vs);
+
+  isEmpty = case {nil = true; (::) _ _ = false};
+};
+
+;;
+
 N :> {
   type Z;
   type S _;
@@ -67,38 +173,81 @@ N :> {
   type S _ = {};
 };
 
+ListN'' = let
+    type I (type case _) (type t _ _) x = {
+      nil     :               case N.Z;
+      (::) 'n : x -> t x n -> case (N.S n);
+    };
+    type J (type t _ _) x = {type case _; ...I case t x};
+    type T (type t _ _) x n = (c: J t x) -> c.case n;
+  in {
+    t = rec (type t _ _) => fun (type x) (type n) => type wrap T t x n;
+    case (type case _) 'x 'n (cs: I case t x) (e: t x n) =
+      (unwrap e.@(t x n): wrap T t x n) {case; ...cs};
+    mk 'x 'n (c: T t x n) = @(t x n) (wrap c: wrap T t x n);
+    D = J t;
+  } :> {
+    type t _ _;
+    case (type case _) 'x 'n: I case t x => t x n -> case n;
+    mk 'x 'n: T t x n => t x n;
+    type D x = J t x;
+  };
+
 ListN = let
-  type I (type x) (type p _ _) (type t _ _) = {
-    nil     :               p x N.Z;
-    (::) 'n : x -> t x n -> p x (N.S n);
+  ...let
+    type I (type case _) (type t _ _) x = {
+      nil     :               case N.Z;
+      (::) 'n : x -> t x n -> case (N.S n);
+    };
+    type J (type t _ _) x = {type case _; ...I case t x};
+    type T (type t _ _) x n = (c: J t x) -> c.case n;
+  in {
+    t = rec (type t _ _) => fun (type x) (type n) => type wrap T t x n;
+    case (type case _) 'x 'n (cs: I case t x) (e: t x n) =
+      (unwrap e.@(t x n): wrap T t x n) {case; ...cs};
+    mk 'x 'n (c: T t x n) = @(t x n) (wrap c: wrap T t x n);
+    D = J t;
+  } :> {
+    type t _ _;
+    case (type case _) 'x 'n: I case t x => t x n -> case n;
+    mk 'x 'n: T t x n => t x n;
+    type D x = J t x;
   };
-  type T x n (type t _ _) = (type p _ _) => I x p t -> p x n;
 in {
-  t = rec (type t _ _) => fun (type x) (type n) => type wrap T x n t;
-
-  case 'x 'n (p: {type t _ _}) (cs: I x p.t t) e =
-    (unwrap e.@(t _ _): wrap T x n t) p.t cs;
-
-  local
-    mk 'x 'n (c: T x n t) = @(t x n) (wrap c: wrap T x n t);
-  in
-    nil  'x                       = mk (fun (type p _ _) (r: I x p t) => r.nil);
-    (::) 'x 'n (v: x) (vs: t x n) = mk (fun (type p _ _) (r: I x p t) => r.:: v vs);
-  end;
-} :> {
-  type t _ _;
-
-  case 'x 'n: (p: {type t _ _}) => I x p.t t => t x n -> p.t x n;
-
-  nil  'x    :               t x N.Z;
-  (::) 'x 'n : x => t x n => t x (N.S n);
+  t; case;
+  nil  'x                       = mk (fun (r: D x) => r.nil);
+  (::) 'x 'n (v: x) (vs: t x n) = mk (fun (r: D x) => r.:: v vs);
 };
 
 ListN = {
   ...ListN;
   map 'x 'y 'n (xy: x -> y) = rec (map: 'n => t x n -> t y n) =>
-    case {type t _ n = t y n} {
+    case (t y) {
       nil = nil;
       (::) x xs = xy x :: map xs;
     };
+  foldLeft 'x 's (sxs: s -> x -> s) = rec (foldLeft: 'n => s -> t x n -> s) => fun v =>
+    case (fun (type n) => s) {
+      nil = v;
+      (::) x xs = foldLeft (sxs v x) xs;
+    };
+  otw = 1 :: (2 :: (3 :: nil));
+  sum = foldLeft (+) 0 otw;
+  otw' = map (fun i => "Int.toText missing") otw;
+};
+
+ListN' = {
+  ...data case t x _ :> {
+    nil     :               case N.Z;
+    (::) 'n : x -> t x n -> case (N.S n);
+  };
+
+;;  nil  'x                       = mk (fun (r: D x) => r.nil);
+;;  (::) 'x 'n (v: x) (vs: t x n) = mk (fun (r: D x) => r.:: v vs);
+;;
+;;  map 'x 'y 'n (xy: x -> y) = rec (map: 'n => t x n -> t y n) =>
+;;    case (t y) {
+;;      nil = nil;
+;;      (::) x xs = xy x :: map xs;
+;;    };
 };