Skip to content

Commit

Permalink
WIP Add derived form for datatypes
Browse files Browse the repository at this point in the history
  • Loading branch information
@polytypic
polytypic committed Jan 21, 2020
1 parent 380ae2f commit f9e98de
Show file tree
Hide file tree
Showing 6 changed files with 327 additions and 28 deletions.
4 changes: 2 additions & 2 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions elab.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)}
Expand Down
1 change: 1 addition & 0 deletions lexer.mll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@ rule token = parse
| "_" { HOLE }
| "and" { AND }
| "as" { AS }
| "data" { DATA }
| "do" { DO }
| "else" { ELSE }
| "end" { END }
Expand Down
15 changes: 11 additions & 4 deletions parser.mly
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
193 changes: 171 additions & 22 deletions regression.1ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 _;
Expand All @@ -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 = {
Expand All @@ -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;
;; };
};
Loading

0 comments on commit f9e98de

Please sign in to comment.