WIP Add derived form for datatypes

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

elab.ml

@@ -560,6 +560,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)}

lexer.mll

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

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
 
@@ -305,15 +306,19 @@ infexp :
  | DO appexp
  { doE($2)@@at() }
 ;
+ascription :
+ | COLON
+ { annotE }
+ | SEAL
+ { sealE }
+;
 annexp :
  | infexp
  { $1 }
  | TYPE typ
  { TypE($2)@@at() }
- | annexp COLON typ
- { annotE($1, $3)@@at() }
- | annexp SEAL typ
- { sealE($1, $3)@@at() }
+ | annexp ascription typ
+ { $2($1, $3)@@at() }
  | WRAP infexp COLON typ
  { wrapE($2, $4)@@at() }
  | UNWRAP infexp COLON typ
@@ -322,6 +327,8 @@ annexp :
 exp :
  | annexp
  { $1 }
+ | DATA name name typparamlist ascription typ
+ { dataE($2, $3, $4, $5, $6, at())@@at() }
  | FUN param paramlist DARROW exp
  { funE($2::$3, $5)@@at() }
  | IF exp THEN exp ELSE infexp COLON typ

regression.1ml

@@ -106,6 +106,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 _;
@@ -114,31 +220,50 @@ 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 N.Z;
- (::) 'n : x -> t x n -> p (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 n;
 in {
- t = rec (type t _ _) => fun (type x) (type n) => type wrap T x n t;
-
- case 'x 'n (type p _) (cs: I x p t) e =
- (unwrap e.@(t _ _): wrap T x n t) p 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: (type p _) => I x p t => t x n -> p 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 = {
@@ -148,4 +273,28 @@ ListN = {
  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;
+;; };
 };