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 import elab \
+  lib source prim fomega types env syntax \
+  parser lexer iL erase trace sub import elab \
   lambda compile \
   main
 NOMLI = syntax iL main import

elab.ml

@@ -576,6 +576,7 @@ 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.ImportE(path) ->
     (match Import.resolve (Source.at_file path) path.it with
     | None -> Source.error path.at ("\""^path.it^"\" does not resolve to a file")
@@ -589,6 +590,9 @@ Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t));
       appE(FunE(x'@@t.at, t, VarE(x'@@t.at)@@t.at, Expl@@t.at)@@span[e.at; t.at], e)@@exp.at in
     elab_exp env exp l
 
+  | 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)}
 s1 = ?Xt:*->*, Xu:*->*->*. !b:*. [= b] -> {t : [= Xt b], u : !a:*. [= a] => [= Xu b a]}

examples/hoas.1ml

@@ -5,36 +5,13 @@ local import "prelude"
 ;;
 ;;   https://github.com/palladin/idris-snippets/blob/master/src/HOAS.idr
 
-let
-  type I (type case _) (type t _) = {
-    Val 'x       :                           x ~> case x
-    Bin 'x 'y 'z : (x ~> y ~> z) ~> t x ~> t y ~> case z
-    If  'x       :      t Bool.t ~> t x ~> t x ~> case x
-    App 'x 'y    :           t (x ~> y) ~> t x ~> case y
-    Lam 'x 'y    :                (t x ~> t y) ~> case (x ~> y)
-    Fix 'x 'y    :      t ((x ~> y) ~> x ~> y) ~> case (x ~> y)
-  }
-  type J (type t _) = {type case _, ...I case t}
-  type T (type t _) x = (c: J t) ~> c.case x
-  ...{
-    ...rec {type t _} => {type t x = wrap T t x}
-    case 'x (type case _) (cs: I case t) (e :# wrap T t x :@ t _) =
-      e {case, ...cs}
-    mk 'x (fn: T t x) = fn :# wrap T t x :@ t _
-  } :> {
-    type t _
-    case 'x: (type case _) -> I case t -> t x ~> case x
-    mk 'x: T t x -> t x
-  }
-  J = J t
-in {
-  t, case
-  Val 'x                                   (v: x) = mk fun (e: J) => e.Val v
-  Bin 'x 'y 'z (f: x ~> y ~> z) (l: t x) (r: t y) = mk fun (e: J) => e.Bin f l r
-  If  'x          (b: t Bool.t) (c: t x) (a: t x) = mk fun (e: J) => e.If b c a
-  App 'x 'y              (f: t (x ~> y)) (a: t x) = mk fun (e: J) => e.App f a
-  Lam 'x 'y                       (f: t x ~> t y) = mk fun (e: J) => e.Lam f
-  Fix 'x 'y           (f: t ((x ~> y) ~> x ~> y)) = mk fun (e: J) => e.Fix f
+data case t _ :> {
+  Val 'x       :                           x ~> case x
+  Bin 'x 'y 'z : (x ~> y ~> z) ~> t x ~> t y ~> case z
+  If  'x       :      t Bool.t ~> t x ~> t x ~> case x
+  App 'x 'y    :           t (x ~> y) ~> t x ~> case y
+  Lam 'x 'y    :                (t x ~> t y) ~> case (x ~> y)
+  Fix 'x 'y    :      t ((x ~> y) ~> x ~> y) ~> case (x ~> y)
 }
 
 Fact = Fix <| Lam fun f => Lam fun x =>

examples/tiv.1ml

@@ -0,0 +1,116 @@
+local import "prelude"
+
+;; As 1ML is powerful enough to encode GADTs we can define a value independent
+;; type representation or a deep embedding of type constructors.
+
+type iso a b = {to: a ~> b, from: b ~> a}
+
+Rep = {
+  data case t _ :> {
+    bool: case bool
+    char: case char
+    int : case int
+    text: case text
+    unit: case unit
+
+    alt   'x 'y: t x ~> t y ~> case (alt x y)
+    (~~>) 'x 'y: t x ~> t y ~> case (x ~> y)
+    pair  'x 'y: t x ~> t y ~> case (x, y)
+
+    iso 'x 'y: iso x y ~> t y ~> case x
+
+    lazy 'x: ({} ~> t x) ~> case x
+  }
+
+  defaults (type t _) (default 'a: t a) = {
+    bool = default
+    char = default
+    int  = default
+    unit = default
+    text = default
+
+    alt   _ _ = default
+    _ ~~> _   = default
+    pair  _ _ = default
+
+    iso _ _ = default
+
+    lazy _ = default
+  }
+
+  local i = {to = Opt.case {none = inl {}, some = inr}
+             from = Alt.case {inl {} = none, inr = some}}
+  opt a = iso i (alt unit a)
+
+  local i = {to = List.case {nil = inl {}, (::) x xs = inr (x, xs)}
+             from = Alt.case {inl {} = nil, inr (x, xs) = x::xs}}
+  list v = rec vs => lazy fun {} => iso i (alt unit (pair v vs))
+}
+
+;; Generic toText
+
+ToText = {type t x = x ~> text}
+
+toText = rec (toText 'x: Rep.t x ~> ToText.t x) => Rep.case ToText.t {
+  bool = Bool.toText
+  char c =  "'" ++ Text.fromChar c ++ "'"
+  int = Int.toText
+  text t = "\"" ++ t ++ "\""
+  unit {} = "{}"
+
+  alt aT bT = Alt.case {
+    inl a = "(inl " ++ toText aT a ++ ")"
+    inr b = "(inr " ++ toText bT b ++ ")"
+  }
+
+  (_ ~~> _) _ = "<fun>"
+
+  pair aT bT (a, b) = "(" ++ toText aT a ++ ", " ++ toText bT b ++ ")"
+
+  iso ab bT = ab.to >> toText bT
+
+  lazy th = toText (th {})
+}
+
+println rep x = print (toText rep x ++ "\n")
+
+do let ...Rep
+   println int 101
+   println (pair bool text) (true, "that")
+   println (opt bool) (some false)
+   println (iso {to i = i <> 0, from b = if b then 1 else 0} bool) 1
+   println (list int) (3 :: (1 :: (4 :: nil)))
+
+;; Generic eq
+
+Eq = {type t x = x ~> x ~> bool}
+
+eq = rec (eq 'x: Rep.t x ~> Eq.t x) => Rep.case Eq.t {
+  bool = Bool.==
+  char = Char.==
+  int = Int.==
+  text = Text.==
+  unit _ _ = true
+
+  alt aT bT l r = l |> Alt.case {
+    inl l = r |> Alt.case {inl = eq aT l, inr _ = false}
+    inr l = r |> Alt.case {inl _ = false, inr = eq bT l}
+  }
+
+  (_ ~~> _) _ _ = false
+
+  pair aT bT (l1, l2) (r1, r2) = eq aT l1 r1 && eq bT l2 r2
+
+  iso ab bT l r = eq bT (ab.to l) (ab.to r)
+
+  lazy th l r = eq (th {}) l r
+}
+
+do let ...Rep
+       test t l r = print ("eq " ++ toText t l ++
+                             " " ++ toText t r ++
+                           " = " ++ toText bool (eq t l r) ++ "\n")
+   test int 101 42
+   test (pair int bool) (1, true) (1, true)
+   test (list int) (3 :: (1 :: nil)) (4 :: (1 :: nil))
+   test (list int) (4 :: (2 :: nil)) (4 :: (2 :: nil))

lexer.mll

@@ -263,6 +263,7 @@ rule token = parse
   | "_" { HOLE }
   | "&&" { LOGICAL_AND }
   | "as" { AS }
+  | "data" { DATA }
   | "do" { DO }
   | "else" { ELSE }
   | "type_error" { TYPE_ERROR }

parser.mly

@@ -39,6 +39,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 %token IMPORT
 %token WRAP_OP UNWRAP_OP
 %token ROLL_OP UNROLL_OP
+%token DATA
 
 %token EOF
 
@@ -373,6 +374,8 @@ annexp :
     { $2($1, $3)@@at() }
 ;
 exp :
+  | DATA name name typparamlist annexp_op typ
+    { dataE($2, $3, $4, $5, $6, at())@@at() }
   | LET bind IN exp
     { letE($2, $4)@@at() }
   | IF exp THEN exp ELSE exp
@@ -453,6 +456,8 @@ atbind :
     { InclB(letE($2, $4)@@at())@@at() }
   | IMPORT TEXT
     { InclB(ImportE($2@@ati 2)@@at())@@at() }
+  | DATA name name typparamlist annexp_op typ
+    { InclB(dataE($2, $3, $4, $5, $6, at())@@at())@@at() }
 /*
   | LPAR bind RPAR
     { $2 }

prelude/index.1mls

@@ -100,6 +100,10 @@ Text: {
   print: t ~> {}
 }
 
+Unit: {
+  type t = {}
+}
+
 Zero: {
   type t
 }
@@ -111,6 +115,7 @@ type int = Int.t
 type list a = List.t a
 type opt a = Opt.t a
 type text = Text.t
+type unit = Unit.t
 type zero = Zero.t
 
 (%): int -> int -> int

regression.1ml

@@ -305,6 +305,112 @@ PolyRec = {
   t0 = inr (inl (0, 0) :@ t (int, int)) :@ t int
 }
 
+;;
+
+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
+  ...{
+    ...rec {type t _} => {type t x = wrap T t x}
+    case 'x (type case _) (cs: I t case) (e :# wrap T t x :@ t _) =
+      e {case, ...cs}
+    mk 'x (c: T t x) = c :# wrap T t x :@ 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 {
+    ...rec {type t _} => {type t x = wrap T t x}
+    case '(type case) 'x 'n (cs: I case t x) (e :# wrap T t x :@ t x) =
+      e {case, ...cs}
+    mk 'x (c: T t x) = c :# wrap T t x :@ 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 _
@@ -345,3 +451,36 @@ ListN = {
       x :: xs = xy x :: map xs
     }
 }
+
+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 {
+  ...rec {type t _ _} => {type t x n = wrap T t x n}
+  case (type case _) 'x 'n (cs: I case t x) (e :# wrap T t x n :@ t x n) =
+    e {case, ...cs}
+  mk 'x 'n (c: T t x n) = c :# wrap T t x n :@ 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' = {
+  ...data case t x _ :> {
+    nil     :               case N.Z
+    (::) 'n : x ~> t x n ~> case (N.S n)
+  }
+
+  map 'x 'y 'n (xy: x -> y) = rec (map 'n: t x n ~> t y n) =>
+    case (t y) {
+      nil
+      x :: xs = xy x :: map xs
+    }
+}