From 0733cddeeaf5ef0f21b8eed716f2864b9fb408c0 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Tue, 31 Dec 2019 13:34:40 +0200
Subject: [PATCH] WIP Added derived form for datatypes

---
 elab.ml        |  2 ++
 lexer.mll      |  1 +
 parser.mly     |  3 +++
 regression.1ml | 51 ++++++++++++++++++++++++++++++++++++++++++++++++++
 syntax.ml      | 39 ++++++++++++++++++++++++++++++++++++++
 5 files changed, 96 insertions(+)

diff --git a/elab.ml b/elab.ml
index 915b540c..c69a40e6 100644
--- a/elab.ml
+++ b/elab.ml
@@ -556,6 +556,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.DataE(e) ->
+    elab_exp env e 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
index f8e33b8d..00d5c909 100644
--- 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
index 8c0ea361..3ed3a9a7 100644
--- a/parser.mly
+++ b/parser.mly
@@ -34,6 +34,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 %token LBRACE RBRACE
 %token DOT AT TICK
 %token COMMA SEMI
+%token DATA
 
 %token EOF
 
@@ -321,6 +322,8 @@ annexp :
 exp :
   | annexp
     { $1 }
+  | DATA name typparamlist SEAL typ
+    { dataE($2, $3, $5, 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
index bb2b8273..403db9ce 100644
--- a/regression.1ml
+++ b/regression.1ml
@@ -84,3 +84,54 @@ ListN = {
       (::) x xs = xy x :: map xs;
     };
 };
+
+;;
+
+IT = data t _ :> {
+  Int  :  Int.t -> t Int.t;
+  Text : Text.t -> t Text.t;
+};
+
+IT = let
+  type I (type p _) (type t _) = {
+    Int  :  Int.t -> p Int.t;
+    Text : Text.t -> p Text.t;
+  };
+  type T x (type t _) = (type p _) => I p t -> p x;
+in {
+  t = rec (type t _) => fun (type x) => type wrap T x t;
+
+  case 'x (p: {type t _}) (cs: I p.t t) e =
+    (unwrap e.@(t _): wrap T x t) p.t cs;
+
+  local
+    mk 'x (c: T x t) = @(t x) (wrap c: wrap T x t);
+  in
+    Int  v = mk (fun (type p _) (r: I p t) => r.Int  v);
+    Text v = mk (fun (type p _) (r: I p t) => r.Text v);
+  end;
+} :> {
+  type t _;
+
+  case 'x: (p: {type t _}) => I p.t t => t x -> p.t x;
+
+  Int  :  Int.t => t Int.t;
+  Text : Text.t => t Text.t;
+};
+
+IT = {
+  ...IT;
+
+  impossible: t int -> int = case {type t x = x} {
+    Int  x = x;
+    Text x = x;
+  };
+
+  i: int = impossible (Int 9);
+  ;;t: text = impossible (Text "nine");
+};
+
+ListN = data t x _ :> {
+  nil     :               t x N.Z;
+  (::) 'n : x -> t x n -> t x (N.S n);
+};
diff --git a/syntax.ml b/syntax.ml
index b2cb3276..e4fe2ca2 100644
--- a/syntax.ml
+++ b/syntax.ml
@@ -51,6 +51,7 @@ and exp' =
   | UnwrapE of var * typ
   | UnrollE of var * typ
   | RecE of var * typ * exp
+  | DataE of exp
 
 and bind = (bind', unit) phrase
 and bind' =
@@ -314,6 +315,42 @@ let rollP(p, t2) =
     Some (AsT(t2, PathT(RecE("_"@@t1.at, TypT@@t1.at,
       TypE(t1.it@@p.at)@@p.at)@@p.at)@@p.at)@@span[p.at; t2.at])
 
+(* data *)
+
+(*
+data t ts :> { cs };
+
+let
+  type I$ ts (type p$ *_) (type t *_) = { cs };
+  type T$ ts ks (type t *_) = (type p$ *_) => I$ ts p$ t -> p$ ts ks;
+in {
+  t = rec (type t *_) => fun ts ks => type wrap T ts ks t;
+  local
+    mk$ 'ts 'ks (f$: T$ ts ks t) = @(t ts ks) (wrap f$: wrap T$ ts ks t;
+  in
+    toCon t ts k cs I$ mk$;
+  end;
+} :> {
+  type t *_;
+  case 'ts 'tk : (p$: {type t *_}) => I$ ts p$.t t => t ts tk -> p$.t ts tk
+  toPure t ts k cs;
+};
+*)
+
+let mk_type_p v tps =
+  let at = v.at in
+  let type_p = annotP(varP(v)@@at, funT(tps, TypT@@at, Pure@@at)@@at)@@at in
+  let type_p_p = let b, t = (defaultP type_p).it in (b, t, Expl@@at)@@at in
+  (type_p, type_p_p)
+
+let dataE(n, tps, cs, at) =
+  let named_tps =
+    tps |> List.filter (function
+               | {it = ({it = EmptyB}, _, _)} -> false
+               | _ -> true) in
+  let type_n, type_n_p = mk_type_p n tps in
+  DataE(funE(named_tps @ [type_n_p], TypE(cs)@@at)@@at)
+
 
 (* String conversion *)
 
@@ -366,6 +403,7 @@ let label_of_exp e =
   | UnwrapE _ -> "UnwrapE"
   | UnrollE _ -> "UnrollE"
   | RecE _ -> "RecE"
+  | DataE _ -> "DataE"
 
 let label_of_bind b =
   match b.it with
@@ -423,6 +461,7 @@ and string_of_exp e =
   | UnwrapE(x, t) -> node' [string_of_var x; string_of_typ t]
   | UnrollE(x, t) -> node' [string_of_var x; string_of_typ t]
   | RecE(x, t, e) -> node' [string_of_var x; string_of_typ t; string_of_exp e]
+  | DataE(e) -> node' [string_of_exp e]
 
 and string_of_bind b =
   let node' = node (label_of_bind b) in