Skip to content

Commit e0b6d41

Browse files
polytypicpolytypic
committed
WIP Add derived form for datatypes
1 parent 3d8b317 commit e0b6d41

File tree

6 files changed

+327
-28
lines changed

6 files changed

+327
-28
lines changed

‎Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@
44

55
NAME = 1ml
66
MODULES = \
7-
lib source prim syntax parser lexer \
8-
fomega types iL env erase trace sub elab \
7+
lib source prim fomega types env syntax \
8+
parser lexer iL erase trace sub elab \
99
lambda compile \
1010
main
1111
NOMLI = syntax iL main

‎elab.ml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -557,6 +557,8 @@ Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t));
557557
ExT([], t), Pure, lift_warn exp.at t env (zs1 @ zs2 @ zs3),
558558
IL.LetE(e, "_", materialize_typ t)
559559
)
560+
| EL.WithEnvE (toExp) ->
561+
elab_exp env (toExp env) l
560562

561563
(*
562564
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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,7 @@ rule token = parse
7070
| "_" { HOLE }
7171
| "and" { AND }
7272
| "as" { AS }
73+
| "data" { DATA }
7374
| "do" { DO }
7475
| "else" { ELSE }
7576
| "end" { END }

‎parser.mly

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
3535
%token DOT AT TICK
3636
%token COMMA SEMI
3737
%token TYPE_ERROR
38+
%token DATA
3839

3940
%token EOF
4041

@@ -305,15 +306,19 @@ infexp :
305306
| DO appexp
306307
{ doE($2)@@at() }
307308
;
309+
ascription :
310+
| COLON
311+
{ annotE }
312+
| SEAL
313+
{ sealE }
314+
;
308315
annexp :
309316
| infexp
310317
{ $1 }
311318
| TYPE typ
312319
{ TypE($2)@@at() }
313-
| annexp COLON typ
314-
{ annotE($1, $3)@@at() }
315-
| annexp SEAL typ
316-
{ sealE($1, $3)@@at() }
320+
| annexp ascription typ
321+
{ $2($1, $3)@@at() }
317322
| WRAP infexp COLON typ
318323
{ wrapE($2, $4)@@at() }
319324
| UNWRAP infexp COLON typ
@@ -322,6 +327,8 @@ annexp :
322327
exp :
323328
| annexp
324329
{ $1 }
330+
| DATA name name typparamlist ascription typ
331+
{ dataE($2, $3, $4, $5, $6, at())@@at() }
325332
| FUN param paramlist DARROW exp
326333
{ funE($2::$3, $5)@@at() }
327334
| IF exp THEN exp ELSE infexp COLON typ

‎regression.1ml

Lines changed: 171 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,112 @@ PolyRec = {
5959
t0 = @(t int) (right (@(t (type (int, int))) (left (0, 0))));
6060
};
6161

62+
;;
63+
64+
IT = data case t _ :> {
65+
Int : Int.t -> case Int.t;
66+
Text : Text.t -> case Text.t;
67+
};
68+
69+
IT = let
70+
type I (type t _) (type case _) = {
71+
Int : Int.t -> case Int.t;
72+
Text : Text.t -> case Text.t;
73+
};
74+
type J (type t _) = {type case _; ...I t case};
75+
type T (type t _) x = (c: J t) -> c.case x;
76+
...{
77+
t = rec (type t _) => fun (type x) => type wrap T t x;
78+
case 'x (type case _) (cs: I t case) e =
79+
(unwrap e.@(t _): wrap T t x) {case; ...cs};
80+
mk 'x (c: T t x) = @(t x) (wrap c: wrap T t x);
81+
} :> {
82+
type t _;
83+
case 'x: (type case _) => I t case => t x -> case x;
84+
mk 'x: T t x => t x;
85+
};
86+
J = J t;
87+
in {
88+
t; case;
89+
Int v = mk (fun (r: J) => r.Int v);
90+
Text v = mk (fun (r: J) => r.Text v);
91+
};
92+
93+
IT = {
94+
...IT;
95+
96+
impossible: t int -> int = case (fun (type t) => t) {
97+
Int x = x;
98+
Text x = x;
99+
};
100+
101+
i: int = impossible (Int 9);
102+
;;t: text = impossible (Text "nine");
103+
};
104+
105+
;;
106+
107+
Ord = data case t :> {
108+
Lt : case;
109+
Eq : case;
110+
Gt : case;
111+
};
112+
113+
Opt = data case t x :> {
114+
None : case;
115+
Some : x -> case;
116+
};
117+
118+
Alt = {
119+
...data case t l r :> {
120+
Left : l -> case;
121+
Right : r -> case;
122+
};
123+
124+
;;Left 'l 'r (v: l) = mk (fun (r: J t l r) => r.Left v);
125+
;;Right 'l 'r (v: r) = mk (fun (r: J t l r) => r.Right v);
126+
};
127+
128+
List = let
129+
...let
130+
type I (type case) (type t _) x = {
131+
nil : case;
132+
(::) 'n : x -> t x -> case;
133+
};
134+
type J (type t _) x = {type case; ...I case t x};
135+
type T (type t _) x = (c: J t x) -> c.case;
136+
in {
137+
t = rec (type t _) => fun (type x) => type wrap T t x;
138+
case '(type case) 'x 'n (cs: I case t x) (e: t x) =
139+
(unwrap e.@(t x): wrap T t x) {case; ...cs};
140+
mk 'x (c: T t x) = @(t x) (wrap c: wrap T t x);
141+
D = J t;
142+
} :> {
143+
type t _;
144+
case '(type case) 'x 'n: I case t x => t x -> case;
145+
mk 'x: T t x => t x;
146+
type D x = J t x;
147+
};
148+
in {
149+
t; case;
150+
nil 'x = mk (fun (r: D x) => r.nil);
151+
(::) 'x 'n (v: x) (vs: t x) = mk (fun (r: D x) => r.:: v vs);
152+
};
153+
154+
List' = {
155+
...data case t x :> {
156+
nil : case;
157+
(::) : x -> t x => case;
158+
};
159+
160+
;; nil 'x = mk (fun (r: J x) => r.nil);
161+
;; (::) 'x (v: x) (vs: t x) = mk (fun (r: J x) => r.:: v vs);
162+
163+
isEmpty = case {nil = true; (::) _ _ = false};
164+
};
165+
166+
;;
167+
62168
N :> {
63169
type Z;
64170
type S _;
@@ -67,31 +173,50 @@ N :> {
67173
type S _ = {};
68174
};
69175

176+
ListN'' = let
177+
type I (type case _) (type t _ _) x = {
178+
nil : case N.Z;
179+
(::) 'n : x -> t x n -> case (N.S n);
180+
};
181+
type J (type t _ _) x = {type case _; ...I case t x};
182+
type T (type t _ _) x n = (c: J t x) -> c.case n;
183+
in {
184+
t = rec (type t _ _) => fun (type x) (type n) => type wrap T t x n;
185+
case (type case _) 'x 'n (cs: I case t x) (e: t x n) =
186+
(unwrap e.@(t x n): wrap T t x n) {case; ...cs};
187+
mk 'x 'n (c: T t x n) = @(t x n) (wrap c: wrap T t x n);
188+
D = J t;
189+
} :> {
190+
type t _ _;
191+
case (type case _) 'x 'n: I case t x => t x n -> case n;
192+
mk 'x 'n: T t x n => t x n;
193+
type D x = J t x;
194+
};
195+
70196
ListN = let
71-
type I (type x) (type p _) (type t _ _) = {
72-
nil : p N.Z;
73-
(::) 'n : x -> t x n -> p (N.S n);
197+
...let
198+
type I (type case _) (type t _ _) x = {
199+
nil : case N.Z;
200+
(::) 'n : x -> t x n -> case (N.S n);
201+
};
202+
type J (type t _ _) x = {type case _; ...I case t x};
203+
type T (type t _ _) x n = (c: J t x) -> c.case n;
204+
in {
205+
t = rec (type t _ _) => fun (type x) (type n) => type wrap T t x n;
206+
case (type case _) 'x 'n (cs: I case t x) (e: t x n) =
207+
(unwrap e.@(t x n): wrap T t x n) {case; ...cs};
208+
mk 'x 'n (c: T t x n) = @(t x n) (wrap c: wrap T t x n);
209+
D = J t;
210+
} :> {
211+
type t _ _;
212+
case (type case _) 'x 'n: I case t x => t x n -> case n;
213+
mk 'x 'n: T t x n => t x n;
214+
type D x = J t x;
74215
};
75-
type T x n (type t _ _) = (type p _) => I x p t -> p n;
76216
in {
77-
t = rec (type t _ _) => fun (type x) (type n) => type wrap T x n t;
78-
79-
case 'x 'n (type p _) (cs: I x p t) e =
80-
(unwrap e.@(t _ _): wrap T x n t) p cs;
81-
82-
local
83-
mk 'x 'n (c: T x n t) = @(t x n) (wrap c: wrap T x n t);
84-
in
85-
nil 'x = mk (fun (type p _) (r: I x p t) => r.nil);
86-
(::) 'x 'n (v: x) (vs: t x n) = mk (fun (type p _) (r: I x p t) => r.:: v vs);
87-
end;
88-
} :> {
89-
type t _ _;
90-
91-
case 'x 'n: (type p _) => I x p t => t x n -> p n;
92-
93-
nil 'x : t x N.Z;
94-
(::) 'x 'n : x => t x n => t x (N.S n);
217+
t; case;
218+
nil 'x = mk (fun (r: D x) => r.nil);
219+
(::) 'x 'n (v: x) (vs: t x n) = mk (fun (r: D x) => r.:: v vs);
95220
};
96221

97222
ListN = {
@@ -101,4 +226,28 @@ ListN = {
101226
nil = nil;
102227
(::) x xs = xy x :: map xs;
103228
};
229+
foldLeft 'x 's (sxs: s -> x -> s) = rec (foldLeft: 'n => s -> t x n -> s) => fun v =>
230+
case (fun (type n) => s) {
231+
nil = v;
232+
(::) x xs = foldLeft (sxs v x) xs;
233+
};
234+
otw = 1 :: (2 :: (3 :: nil));
235+
sum = foldLeft (+) 0 otw;
236+
otw' = map (fun i => "Int.toText missing") otw;
237+
};
238+
239+
ListN' = {
240+
...data case t x _ :> {
241+
nil : case N.Z;
242+
(::) 'n : x -> t x n -> case (N.S n);
243+
};
244+
245+
;; nil 'x = mk (fun (r: D x) => r.nil);
246+
;; (::) 'x 'n (v: x) (vs: t x n) = mk (fun (r: D x) => r.:: v vs);
247+
;;
248+
;; map 'x 'y 'n (xy: x -> y) = rec (map: 'n => t x n -> t y n) =>
249+
;; case (t y) {
250+
;; nil = nil;
251+
;; (::) x xs = xy x :: map xs;
252+
;; };
104253
};

0 commit comments

Comments
 (0)