WIP Added derived form for datatypes

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)}

lexer.mll

@@ -70,6 +70,7 @@ rule token = parse
  | "_" { HOLE }
  | "and" { AND }
  | "as" { AS }
+ | "data" { DATA }
  | "do" { DO }
  | "else" { ELSE }
  | "end" { END }

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

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);
+};

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