Mercurial > urweb

comparison src/corify.sml @ 377:78358e5df273

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proper generation of relation names; checking that sequences exist
author Adam Chlipala <adamc@hcoop.net>
date Sun, 19 Oct 2008 12:12:59 -0400
parents 6fd102fa28f9
children ab3177746c78
comparison
equal deleted inserted replaced
376:6fd102fa28f9 377:78358e5df273
47 s 47 s
48 in 48 in
49 !restify (String.concatWith "/" (rev (s :: mods))) 49 !restify (String.concatWith "/" (rev (s :: mods)))
50 end 50 end
51 51
52 val relify = CharVector.map (fn #"/" => #"_"
53 | ch => ch)
54
52 local 55 local
53 val count = ref 0 56 val count = ref 0
54 in 57 in
55 58
56 fun reset v = count := v 59 fun reset v = count := v
104 val bindStr : t -> string -> int -> t -> t 107 val bindStr : t -> string -> int -> t -> t
105 val lookupStrById : t -> int -> t 108 val lookupStrById : t -> int -> t
106 val lookupStrByName : string * t -> t 109 val lookupStrByName : string * t -> t
107 val lookupStrByNameOpt : string * t -> t option 110 val lookupStrByNameOpt : string * t -> t option
108 111
109 val bindFunctor : t -> string -> int -> string -> int -> L.str -> t 112 val bindFunctor : t -> string list -> string -> int -> string -> int -> L.str -> t
110 val lookupFunctorById : t -> int -> string * int * L.str 113 val lookupFunctorById : t -> int -> string list * string * int * L.str
111 val lookupFunctorByName : string * t -> string * int * L.str 114 val lookupFunctorByName : string * t -> string list * string * int * L.str
112 end = struct 115 end = struct
113 116
114 datatype flattening = 117 datatype flattening =
115 FNormal of {name : string list, 118 FNormal of {name : string list,
116 cons : int SM.map, 119 cons : int SM.map,
117 constructors : L'.patCon SM.map, 120 constructors : L'.patCon SM.map,
118 vals : int SM.map, 121 vals : int SM.map,
119 strs : flattening SM.map, 122 strs : flattening SM.map,
120 funs : (string * int * L.str) SM.map} 123 funs : (string list * string * int * L.str) SM.map}
121 | FFfi of {mod : string, 124 | FFfi of {mod : string,
122 vals : L'.con SM.map, 125 vals : L'.con SM.map,
123 constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map} 126 constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map}
124 127
125 type t = { 128 type t = {
126 basis : int option, 129 basis : int option,
127 cons : int IM.map, 130 cons : int IM.map,
128 constructors : L'.patCon IM.map, 131 constructors : L'.patCon IM.map,
129 vals : int IM.map, 132 vals : int IM.map,
130 strs : flattening IM.map, 133 strs : flattening IM.map,
131 funs : (string * int * L.str) IM.map, 134 funs : (string list * string * int * L.str) IM.map,
132 current : flattening, 135 current : flattening,
133 nested : flattening list 136 nested : flattening list
134 } 137 }
135 138
136 val empty = { 139 val empty = {
400 | lookupStrByNameOpt _ = NONE 403 | lookupStrByNameOpt _ = NONE
401 404
402 fun bindFunctor ({basis, cons, constructors, vals, strs, funs, 405 fun bindFunctor ({basis, cons, constructors, vals, strs, funs,
403 current = FNormal {name, cons = mcons, constructors = mconstructors, 406 current = FNormal {name, cons = mcons, constructors = mconstructors,
404 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) 407 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
405 x n xa na str = 408 mods x n xa na str =
406 {basis = basis, 409 {basis = basis,
407 cons = cons, 410 cons = cons,
408 constructors = constructors, 411 constructors = constructors,
409 vals = vals, 412 vals = vals,
410 strs = strs, 413 strs = strs,
411 funs = IM.insert (funs, n, (xa, na, str)), 414 funs = IM.insert (funs, n, (mods, xa, na, str)),
412 current = FNormal {name = name, 415 current = FNormal {name = name,
413 cons = mcons, 416 cons = mcons,
414 constructors = mconstructors, 417 constructors = mconstructors,
415 vals = mvals, 418 vals = mvals,
416 strs = mstrs, 419 strs = mstrs,
417 funs = SM.insert (mfuns, x, (xa, na, str))}, 420 funs = SM.insert (mfuns, x, (mods, xa, na, str))},
418 nested = nested} 421 nested = nested}
419 | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" 422 | bindFunctor _ _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
420 423
421 fun lookupFunctorById ({funs, ...} : t) n = 424 fun lookupFunctorById ({funs, ...} : t) n =
422 case IM.find (funs, n) of 425 case IM.find (funs, n) of
423 NONE => raise Fail "Corify.St.lookupFunctorById" 426 NONE => raise Fail "Corify.St.lookupFunctorById"
424 | SOME v => v 427 | SOME v => v
691 ([(L'.DValRec vis, loc)], st) 694 ([(L'.DValRec vis, loc)], st)
692 end 695 end
693 | L.DSgn _ => ([], st) 696 | L.DSgn _ => ([], st)
694 697
695 | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) => 698 | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
696 ([], St.bindFunctor st x n xa na str) 699 ([], St.bindFunctor st mods x n xa na str)
697 700
698 | L.DStr (x, n, _, (L.StrProj (str, x'), _)) => 701 | L.DStr (x, n, _, (L.StrProj (str, x'), _)) =>
699 let 702 let
700 val (ds, {inner, outer}) = corifyStr mods (str, st) 703 val (ds, {inner, outer}) = corifyStr mods (str, st)
701 704
702 val st = case St.lookupStrByNameOpt (x', inner) of 705 val st = case St.lookupStrByNameOpt (x', inner) of
703 SOME st' => St.bindStr st x n st' 706 SOME st' => St.bindStr st x n st'
704 | NONE => 707 | NONE =>
705 let 708 let
706 val (x', n', str') = St.lookupFunctorByName (x', inner) 709 val (mods', x', n', str') = St.lookupFunctorByName (x', inner)
707 in 710 in
708 St.bindFunctor st x n x' n' str' 711 St.bindFunctor st mods' x n x' n' str'
709 end 712 end
710 in 713 in
711 ([], st) 714 ([], st)
712 end 715 end
713 716
714 | L.DStr (x, n, _, str) => 717 | L.DStr (x, n, _, str) =>
715 let 718 let
716 val (ds, {inner, outer}) = corifyStr (x :: mods) (str, st) 719 val mods' =
720 if x = "anon" then
721 mods
722 else
723 x :: mods
724
725 val (ds, {inner, outer}) = corifyStr mods' (str, st)
717 val st = St.bindStr outer x n inner 726 val st = St.bindStr outer x n inner
718 in 727 in
719 (ds, st) 728 (ds, st)
720 end 729 end
721 730
901 | _ => raise Fail "Non-const signature for 'export'") 910 | _ => raise Fail "Non-const signature for 'export'")
902 911
903 | L.DTable (_, x, n, c) => 912 | L.DTable (_, x, n, c) =>
904 let 913 let
905 val (st, n) = St.bindVal st x n 914 val (st, n) = St.bindVal st x n
906 val s = doRestify (mods, x) 915 val s = relify (doRestify (mods, x))
907 in 916 in
908 ([(L'.DTable (x, n, corifyCon st c, s), loc)], st) 917 ([(L'.DTable (x, n, corifyCon st c, s), loc)], st)
909 end 918 end
910 | L.DSequence (_, x, n) => 919 | L.DSequence (_, x, n) =>
911 let 920 let
912 val (st, n) = St.bindVal st x n 921 val (st, n) = St.bindVal st x n
913 val s = doRestify (mods, x) 922 val s = relify (doRestify (mods, x))
914 in 923 in
915 ([(L'.DSequence (x, n, s), loc)], st) 924 ([(L'.DSequence (x, n, s), loc)], st)
916 end 925 end
917 926
918 | L.DDatabase s => ([(L'.DDatabase s, loc)], st) 927 | L.DDatabase s => ([(L'.DDatabase s, loc)], st)
946 case str of 955 case str of
947 L.StrVar n => St.lookupFunctorById st n 956 L.StrVar n => St.lookupFunctorById st n
948 | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str) 957 | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str)
949 | _ => raise Fail "Corify of fancy functor application [2]" 958 | _ => raise Fail "Corify of fancy functor application [2]"
950 959
951 val (xa, na, body) = unwind str1 960 val (fmods, xa, na, body) = unwind str1
952 961
953 val (ds1, {inner = inner', outer}) = corifyStr mods (str2, st) 962 val (ds1, {inner = inner', outer}) = corifyStr mods (str2, st)
954 963
955 val mods' = mods 964 val mods' = case #1 str2 of
965 L.StrConst _ => fmods @ mods
966 | _ =>
967 let
968 val ast = unwind' str2
969 in
970 fmods @ St.name ast
971 end
956 972
957 val (ds2, {inner, outer}) = corifyStr mods' (body, St.bindStr outer xa na inner') 973 val (ds2, {inner, outer}) = corifyStr mods' (body, St.bindStr outer xa na inner')
958 in 974 in
959 (ds1 @ ds2, {inner = St.bindStr inner xa na inner', outer = outer}) 975 (ds1 @ ds2, {inner = St.bindStr inner xa na inner', outer = outer})
960 end 976 end