Mercurial > urweb

comparison src/corify.sml @ 185:19ee24bffbc0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FFI datatypes
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 Aug 2008 17:57:47 -0400
parents d11754ffe252
children 88d46972de53
comparison
equal deleted inserted replaced
184:98c29e3986d3 185:19ee24bffbc0
60 60
61 val debug : t -> unit 61 val debug : t -> unit
62 62
63 val enter : t -> t 63 val enter : t -> t
64 val leave : t -> {outer : t, inner : t} 64 val leave : t -> {outer : t, inner : t}
65 val ffi : string -> L'.con SM.map -> t 65 val ffi : string -> L'.con SM.map -> string SM.map -> t
66 66
67 datatype core_con = 67 datatype core_con =
68 CNormal of int 68 CNormal of int
69 | CFfi of string 69 | CFfi of string
70 val bindCon : t -> string -> int -> t * int 70 val bindCon : t -> string -> int -> t * int
97 constructors : L'.patCon SM.map, 97 constructors : L'.patCon SM.map,
98 vals : int SM.map, 98 vals : int SM.map,
99 strs : flattening SM.map, 99 strs : flattening SM.map,
100 funs : (string * int * L.str) SM.map} 100 funs : (string * int * L.str) SM.map}
101 | FFfi of {mod : string, 101 | FFfi of {mod : string,
102 vals : L'.con SM.map} 102 vals : L'.con SM.map,
103 constructors : string SM.map}
103 104
104 type t = { 105 type t = {
105 cons : int IM.map, 106 cons : int IM.map,
106 constructors : L'.patCon IM.map, 107 constructors : L'.patCon IM.map,
107 vals : int IM.map, 108 vals : int IM.map,
256 NONE => raise Fail "Corify.St.lookupConstructorById" 257 NONE => raise Fail "Corify.St.lookupConstructorById"
257 | SOME x => x 258 | SOME x => x
258 259
259 fun lookupConstructorByName ({current, ...} : t) x = 260 fun lookupConstructorByName ({current, ...} : t) x =
260 case current of 261 case current of
261 FFfi {mod = m, ...} => L'.PConFfi (m, x) 262 FFfi {mod = m, constructors, ...} =>
263 (case SM.find (constructors, x) of
264 NONE => raise Fail "Corify.St.lookupConstructorByName [1]"
265 | SOME n => L'.PConFfi {mod = m, datatyp = n, con = x})
262 | FNormal {constructors, ...} => 266 | FNormal {constructors, ...} =>
263 case SM.find (constructors, x) of 267 case SM.find (constructors, x) of
264 NONE => raise Fail "Corify.St.lookupConstructorByName" 268 NONE => raise Fail "Corify.St.lookupConstructorByName [2]"
265 | SOME n => n 269 | SOME n => n
266 270
267 fun enter {cons, constructors, vals, strs, funs, current, nested} = 271 fun enter {cons, constructors, vals, strs, funs, current, nested} =
268 {cons = cons, 272 {cons = cons,
269 constructors = constructors, 273 constructors = constructors,
294 current = m1, 298 current = m1,
295 nested = rest}, 299 nested = rest},
296 inner = dummy current} 300 inner = dummy current}
297 | leave _ = raise Fail "Corify.St.leave" 301 | leave _ = raise Fail "Corify.St.leave"
298 302
299 fun ffi m vals = dummy (FFfi {mod = m, vals = vals}) 303 fun ffi m vals constructors = dummy (FFfi {mod = m, vals = vals, constructors = constructors})
300 304
301 fun bindStr ({cons, constructors, vals, strs, funs, 305 fun bindStr ({cons, constructors, vals, strs, funs,
302 current = FNormal {cons = mcons, constructors = mconstructors, 306 current = FNormal {cons = mcons, constructors = mconstructors,
303 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) 307 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
304 x n ({current = f, ...} : t) = 308 x n ({current = f, ...} : t) =
504 val t = (L'.CNamed n, loc) 508 val t = (L'.CNamed n, loc)
505 val dcons = map (fn (x, n, to) => 509 val dcons = map (fn (x, n, to) =>
506 let 510 let
507 val (e, t) = 511 val (e, t) =
508 case to of 512 case to of
509 NONE => ((L'.ECon (n, NONE), loc), t) 513 NONE => ((L'.ECon (L'.PConVar n, NONE), loc), t)
510 | SOME t' => ((L'.EAbs ("x", t', t, 514 | SOME t' => ((L'.EAbs ("x", t', t,
511 (L'.ECon (n, SOME (L'.ERel 0, loc)), loc)), 515 (L'.ECon (L'.PConVar n, SOME (L'.ERel 0, loc)), loc)),
512 loc), 516 loc),
513 (L'.TFun (t', t), loc)) 517 (L'.TFun (t', t), loc))
514 in 518 in
515 (L'.DVal (x, n, t, e, ""), loc) 519 (L'.DVal (x, n, t, e, ""), loc)
516 end) xncs 520 end) xncs
599 603
600 | L.DFfiStr (m, n, (sgn, _)) => 604 | L.DFfiStr (m, n, (sgn, _)) =>
601 (case sgn of 605 (case sgn of
602 L.SgnConst sgis => 606 L.SgnConst sgis =>
603 let 607 let
604 val (ds, cmap, st) = 608 val (ds, cmap, conmap, st) =
605 foldl (fn ((sgi, _), (ds, cmap, st)) => 609 foldl (fn ((sgi, _), (ds, cmap, conmap, st)) =>
606 case sgi of 610 case sgi of
607 L.SgiConAbs (x, n, k) => 611 L.SgiConAbs (x, n, k) =>
608 let 612 let
609 val (st, n') = St.bindCon st x n 613 val (st, n') = St.bindCon st x n
610 in 614 in
611 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, 615 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
612 cmap, 616 cmap,
617 conmap,
613 st) 618 st)
614 end 619 end
615 | L.SgiCon (x, n, k, _) => 620 | L.SgiCon (x, n, k, _) =>
616 let 621 let
617 val (st, n') = St.bindCon st x n 622 val (st, n') = St.bindCon st x n
618 in 623 in
619 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, 624 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
620 cmap, 625 cmap,
626 conmap,
627 st)
628 end
629
630 | L.SgiDatatype (x, n, xnts) =>
631 let
632 val (st, n') = St.bindCon st x n
633 val (xnts, (st, cmap, conmap)) =
634 ListUtil.foldlMap
635 (fn ((x', n, to), (st, cmap, conmap)) =>
636 let
637 val st = St.bindConstructor st x' n
638 (L'.PConFfi {mod = m,
639 datatyp = x,
640 con = x'})
641 val st = St.bindConstructorVal st x' n
642
643 val dt = (L'.CNamed n', loc)
644
645 val (to, cmap) =
646 case to of
647 NONE => (NONE, SM.insert (cmap, x', dt))
648 | SOME t =>
649 let
650 val t = corifyCon st t
651 in
652 (SOME t, SM.insert (cmap, x',
653 (L'.TFun (t, dt), loc)))
654 end
655
656 val conmap = SM.insert (conmap, x', x)
657 in
658 ((x', n, to),
659 (st, cmap, conmap))
660 end) (st, cmap, conmap) xnts
661 in
662 ((L'.DDatatype (x, n', xnts), loc) :: ds,
663 cmap,
664 conmap,
621 st) 665 st)
622 end 666 end
623 667
624 | L.SgiVal (x, _, c) => 668 | L.SgiVal (x, _, c) =>
625 (ds, 669 (ds,
626 SM.insert (cmap, x, corifyCon st c), 670 SM.insert (cmap, x, corifyCon st c),
671 conmap,
627 st) 672 st)
628 | _ => (ds, cmap, st)) ([], SM.empty, st) sgis 673 | _ => (ds, cmap, conmap, st)) ([], SM.empty, SM.empty, st) sgis
629 674
630 val st = St.bindStr st m n (St.ffi m cmap) 675 val st = St.bindStr st m n (St.ffi m cmap conmap)
631 in 676 in
632 (rev ds, st) 677 (rev ds, st)
633 end 678 end
634 | _ => raise Fail "Non-const signature for FFI structure") 679 | _ => raise Fail "Non-const signature for FFI structure")
635 680