Skip to content

Commit 4e29ac2

Browse files
polytypicpolytypic
committed
WIP Add derived form for datatypes
1 parent 11eae0b commit 4e29ac2

6 files changed

Lines changed: 327 additions & 28 deletions

File tree

‎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
@@ -559,6 +559,8 @@ Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t));
559559
ExT([], t), Pure, lift_warn exp.at t env (zs1 @ zs2 @ zs3),
560560
IL.LetE(e, "_", materialize_typ t)
561561
)
562+
| EL.WithEnvE (toExp) ->
563+
elab_exp env (toExp env) l
562564

563565
(*
564566
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
| "&&" { LOGICAL_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
@@ -117,6 +117,112 @@ PolyRec = {
117117
t0 = @(t int) (right (@(t (type (int, int))) (left (0, 0))));
118118
};
119119

120+
;;
121+
122+
IT = data case t _ :> {
123+
Int : Int.t -> case Int.t;
124+
Text : Text.t -> case Text.t;
125+
};
126+
127+
IT = let
128+
type I (type t _) (type case _) = {
129+
Int : Int.t -> case Int.t;
130+
Text : Text.t -> case Text.t;
131+
};
132+
type J (type t _) = {type case _; ...I t case};
133+
type T (type t _) x = (c: J t) -> c.case x;
134+
...{
135+
...rec {type t _} => {type t x = wrap T t x};
136+
case 'x (type case _) (cs: I t case) e =
137+
(unwrap e.@(t _): wrap T t x) {case; ...cs};
138+
mk 'x (c: T t x) = @(t x) (wrap c: wrap T t x);
139+
} :> {
140+
type t _;
141+
case 'x: (type case _) => I t case => t x -> case x;
142+
mk 'x: T t x => t x;
143+
};
144+
J = J t;
145+
in {
146+
t; case;
147+
Int v = mk (fun (r: J) => r.Int v);
148+
Text v = mk (fun (r: J) => r.Text v);
149+
};
150+
151+
IT = {
152+
...IT;
153+
154+
impossible: t int -> int = case (fun (type t) => t) {
155+
Int x = x;
156+
Text x = x;
157+
};
158+
159+
i: int = impossible (Int 9);
160+
;;t: text = impossible (Text "nine");
161+
};
162+
163+
;;
164+
165+
Ord = data case t :> {
166+
Lt : case;
167+
Eq : case;
168+
Gt : case;
169+
};
170+
171+
Opt = data case t x :> {
172+
None : case;
173+
Some : x -> case;
174+
};
175+
176+
Alt = {
177+
...data case t l r :> {
178+
Left : l -> case;
179+
Right : r -> case;
180+
};
181+
182+
;;Left 'l 'r (v: l) = mk (fun (r: J t l r) => r.Left v);
183+
;;Right 'l 'r (v: r) = mk (fun (r: J t l r) => r.Right v);
184+
};
185+
186+
List = let
187+
...let
188+
type I (type case) (type t _) x = {
189+
nil : case;
190+
(::) 'n : x -> t x -> case;
191+
};
192+
type J (type t _) x = {type case; ...I case t x};
193+
type T (type t _) x = (c: J t x) -> c.case;
194+
in {
195+
...rec {type t _} => {type t x = wrap T t x};
196+
case '(type case) 'x 'n (cs: I case t x) (e: t x) =
197+
(unwrap e.@(t x): wrap T t x) {case; ...cs};
198+
mk 'x (c: T t x) = @(t x) (wrap c: wrap T t x);
199+
D = J t;
200+
} :> {
201+
type t _;
202+
case '(type case) 'x 'n: I case t x => t x -> case;
203+
mk 'x: T t x => t x;
204+
type D x = J t x;
205+
};
206+
in {
207+
t; case;
208+
nil 'x = mk (fun (r: D x) => r.nil);
209+
(::) 'x 'n (v: x) (vs: t x) = mk (fun (r: D x) => r.:: v vs);
210+
};
211+
212+
List' = {
213+
...data case t x :> {
214+
nil : case;
215+
(::) : x -> t x => case;
216+
};
217+
218+
;; nil 'x = mk (fun (r: J x) => r.nil);
219+
;; (::) 'x (v: x) (vs: t x) = mk (fun (r: J x) => r.:: v vs);
220+
221+
isEmpty = case {nil = true; (::) _ _ = false};
222+
};
223+
224+
;;
225+
120226
N :> {
121227
type Z;
122228
type S _;
@@ -125,31 +231,50 @@ N :> {
125231
type S _ = {};
126232
};
127233

234+
ListN'' = let
235+
type I (type case _) (type t _ _) x = {
236+
nil : case N.Z;
237+
(::) 'n : x -> t x n -> case (N.S n);
238+
};
239+
type J (type t _ _) x = {type case _; ...I case t x};
240+
type T (type t _ _) x n = (c: J t x) -> c.case n;
241+
in {
242+
...rec {type t _ _} => {type t x n = wrap T t x n};
243+
case (type case _) 'x 'n (cs: I case t x) (e: t x n) =
244+
(unwrap e.@(t x n): wrap T t x n) {case; ...cs};
245+
mk 'x 'n (c: T t x n) = @(t x n) (wrap c: wrap T t x n);
246+
D = J t;
247+
} :> {
248+
type t _ _;
249+
case (type case _) 'x 'n: I case t x => t x n -> case n;
250+
mk 'x 'n: T t x n => t x n;
251+
type D x = J t x;
252+
};
253+
128254
ListN = let
129-
type I (type x) (type p _) (type t _ _) = {
130-
nil : p N.Z;
131-
(::) 'n : x -> t x n -> p (N.S n);
255+
...let
256+
type I (type case _) (type t _ _) x = {
257+
nil : case N.Z;
258+
(::) 'n : x -> t x n -> case (N.S n);
259+
};
260+
type J (type t _ _) x = {type case _; ...I case t x};
261+
type T (type t _ _) x n = (c: J t x) -> c.case n;
262+
in {
263+
...rec {type t _ _} => {type t x n = wrap T t x n};
264+
case (type case _) 'x 'n (cs: I case t x) (e: t x n) =
265+
(unwrap e.@(t x n): wrap T t x n) {case; ...cs};
266+
mk 'x 'n (c: T t x n) = @(t x n) (wrap c: wrap T t x n);
267+
D = J t;
268+
} :> {
269+
type t _ _;
270+
case (type case _) 'x 'n: I case t x => t x n -> case n;
271+
mk 'x 'n: T t x n => t x n;
272+
type D x = J t x;
132273
};
133-
type T x n (type t _ _) = (type p _) => I x p t -> p n;
134274
in {
135-
...rec {type t _ _} => {type t x n = wrap T x n t};
136-
137-
case 'x 'n (type p _) (cs: I x p t) e =
138-
(unwrap e.@(t _ _): wrap T x n t) p cs;
139-
140-
local
141-
mk 'x 'n (c: T x n t) = @(t x n) (wrap c: wrap T x n t);
142-
in
143-
nil 'x = mk (fun (type p _) (r: I x p t) => r.nil);
144-
(::) 'x 'n (v: x) (vs: t x n) = mk (fun (type p _) (r: I x p t) => r.:: v vs);
145-
end;
146-
} :> {
147-
type t _ _;
148-
149-
case 'x 'n: (type p _) => I x p t => t x n -> p n;
150-
151-
nil 'x : t x N.Z;
152-
(::) 'x 'n : x => t x n => t x (N.S n);
275+
t; case;
276+
nil 'x = mk (fun (r: D x) => r.nil);
277+
(::) 'x 'n (v: x) (vs: t x n) = mk (fun (r: D x) => r.:: v vs);
153278
};
154279

155280
ListN = {
@@ -159,4 +284,28 @@ ListN = {
159284
nil = nil;
160285
(::) x xs = xy x :: map xs;
161286
};
287+
foldLeft 'x 's (sxs: s -> x -> s) = rec (foldLeft: 'n => s -> t x n -> s) => fun v =>
288+
case (fun (type n) => s) {
289+
nil = v;
290+
(::) x xs = foldLeft (sxs v x) xs;
291+
};
292+
otw = 1 :: (2 :: (3 :: nil));
293+
sum = foldLeft (+) 0 otw;
294+
otw' = map (fun i => "Int.toText missing") otw;
295+
};
296+
297+
ListN' = {
298+
...data case t x _ :> {
299+
nil : case N.Z;
300+
(::) 'n : x -> t x n -> case (N.S n);
301+
};
302+
303+
;; nil 'x = mk (fun (r: D x) => r.nil);
304+
;; (::) 'x 'n (v: x) (vs: t x n) = mk (fun (r: D x) => r.:: v vs);
305+
;;
306+
;; map 'x 'y 'n (xy: x -> y) = rec (map: 'n => t x n -> t y n) =>
307+
;; case (t y) {
308+
;; nil = nil;
309+
;; (::) x xs = xy x :: map xs;
310+
;; };
162311
};

0 commit comments

Comments
 (0)