Skip to content

Commit 27164b6

Browse files
polytypicpolytypic
committed
WIP Add derived form for datatypes
1 parent 77ab9bb commit 27164b6

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

564566
(*
565567
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
@@ -106,6 +106,112 @@ PolyRec = {
106106
t0 = @(t int) (right (@(t (type (int, int))) (left (0, 0))));
107107
};
108108

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

223+
ListN'' = let
224+
type I (type case _) (type t _ _) x = {
225+
nil : case N.Z;
226+
(::) 'n : x -> t x n -> case (N.S n);
227+
};
228+
type J (type t _ _) x = {type case _; ...I case t x};
229+
type T (type t _ _) x n = (c: J t x) -> c.case n;
230+
in {
231+
t = rec (type t _ _) => fun (type x) (type n) => type wrap T t x n;
232+
case (type case _) 'x 'n (cs: I case t x) (e: t x n) =
233+
(unwrap e.@(t x n): wrap T t x n) {case; ...cs};
234+
mk 'x 'n (c: T t x n) = @(t x n) (wrap c: wrap T t x n);
235+
D = J t;
236+
} :> {
237+
type t _ _;
238+
case (type case _) 'x 'n: I case t x => t x n -> case n;
239+
mk 'x 'n: T t x n => t x n;
240+
type D x = J t x;
241+
};
242+
117243
ListN = let
118-
type I (type x) (type p _) (type t _ _) = {
119-
nil : p N.Z;
120-
(::) 'n : x -> t x n -> p (N.S n);
244+
...let
245+
type I (type case _) (type t _ _) x = {
246+
nil : case N.Z;
247+
(::) 'n : x -> t x n -> case (N.S n);
248+
};
249+
type J (type t _ _) x = {type case _; ...I case t x};
250+
type T (type t _ _) x n = (c: J t x) -> c.case n;
251+
in {
252+
t = rec (type t _ _) => fun (type x) (type n) => type wrap T t x n;
253+
case (type case _) 'x 'n (cs: I case t x) (e: t x n) =
254+
(unwrap e.@(t x n): wrap T t x n) {case; ...cs};
255+
mk 'x 'n (c: T t x n) = @(t x n) (wrap c: wrap T t x n);
256+
D = J t;
257+
} :> {
258+
type t _ _;
259+
case (type case _) 'x 'n: I case t x => t x n -> case n;
260+
mk 'x 'n: T t x n => t x n;
261+
type D x = J t x;
121262
};
122-
type T x n (type t _ _) = (type p _) => I x p t -> p n;
123263
in {
124-
t = rec (type t _ _) => fun (type x) (type n) => type wrap T x n t;
125-
126-
case 'x 'n (type p _) (cs: I x p t) e =
127-
(unwrap e.@(t _ _): wrap T x n t) p cs;
128-
129-
local
130-
mk 'x 'n (c: T x n t) = @(t x n) (wrap c: wrap T x n t);
131-
in
132-
nil 'x = mk (fun (type p _) (r: I x p t) => r.nil);
133-
(::) 'x 'n (v: x) (vs: t x n) = mk (fun (type p _) (r: I x p t) => r.:: v vs);
134-
end;
135-
} :> {
136-
type t _ _;
137-
138-
case 'x 'n: (type p _) => I x p t => t x n -> p n;
139-
140-
nil 'x : t x N.Z;
141-
(::) 'x 'n : x => t x n => t x (N.S n);
264+
t; case;
265+
nil 'x = mk (fun (r: D x) => r.nil);
266+
(::) 'x 'n (v: x) (vs: t x n) = mk (fun (r: D x) => r.:: v vs);
142267
};
143268

144269
ListN = {
@@ -148,4 +273,28 @@ ListN = {
148273
nil = nil;
149274
(::) x xs = xy x :: map xs;
150275
};
276+
foldLeft 'x 's (sxs: s -> x -> s) = rec (foldLeft: 'n => s -> t x n -> s) => fun v =>
277+
case (fun (type n) => s) {
278+
nil = v;
279+
(::) x xs = foldLeft (sxs v x) xs;
280+
};
281+
otw = 1 :: (2 :: (3 :: nil));
282+
sum = foldLeft (+) 0 otw;
283+
otw' = map (fun i => "Int.toText missing") otw;
284+
};
285+
286+
ListN' = {
287+
...data case t x _ :> {
288+
nil : case N.Z;
289+
(::) 'n : x -> t x n -> case (N.S n);
290+
};
291+
292+
;; nil 'x = mk (fun (r: D x) => r.nil);
293+
;; (::) 'x 'n (v: x) (vs: t x n) = mk (fun (r: D x) => r.:: v vs);
294+
;;
295+
;; map 'x 'y 'n (xy: x -> y) = rec (map: 'n => t x n -> t y n) =>
296+
;; case (t y) {
297+
;; nil = nil;
298+
;; (::) x xs = xy x :: map xs;
299+
;; };
151300
};

0 commit comments

Comments
 (0)