summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/c/urweb.c1
-rw-r--r--src/cjr_print.sml15
-rw-r--r--src/compiler.sig4
-rw-r--r--src/compiler.sml14
-rw-r--r--src/elab_env.sig2
-rw-r--r--src/elab_env.sml4
-rw-r--r--src/elab_util.sig3
-rw-r--r--src/elab_util.sml6
-rw-r--r--src/elaborate.sml11
-rw-r--r--src/iflow.sml8
-rw-r--r--src/jscomp.sml5
-rw-r--r--src/main.mlton.sml41
-rw-r--r--src/postgres.sml2
-rw-r--r--src/reduce.sml4
-rw-r--r--src/settings.sig7
-rw-r--r--src/settings.sml69
-rw-r--r--src/sources3
-rw-r--r--src/unnest.sml242
18 files changed, 305 insertions, 136 deletions
diff --git a/src/c/urweb.c b/src/c/urweb.c
index a6639ef2..50aac5e8 100644
--- a/src/c/urweb.c
+++ b/src/c/urweb.c
@@ -519,7 +519,6 @@ size_t uw_heap_max = SIZE_MAX;
size_t uw_script_max = SIZE_MAX;
uw_context uw_init(int id, uw_loggers *lg) {
- puts("Initializing");
uw_context ctx = malloc(sizeof(struct uw_context));
ctx->app = NULL;
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index 9e046d84..2c2133d6 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -2944,17 +2944,10 @@ fun p_file env (ds, ps) =
file = "app." ^ timestamp ^ ".js"}
val allScripts =
- let
- val scripts =
- "<script type=\\\"text/javascript\\\" src=\\\""
- ^ app_js
- ^ "\\\"></script>\\n"
- in
- foldl (fn (x, scripts) =>
- scripts
- ^ "<script type=\\\"text/javascript\\\" src=\\\"" ^ x ^ "\\\"></script>\\n")
- scripts (Settings.getScripts ())
- end
+ foldl (fn (x, scripts) =>
+ scripts
+ ^ "<script type=\\\"text/javascript\\\" src=\\\"" ^ x ^ "\\\"></script>\\n")
+ "" (Settings.getScripts () @ [app_js])
fun p_page (ek, s, n, ts, ran, side, dbmode, tellSig) =
let
diff --git a/src/compiler.sig b/src/compiler.sig
index 1ab0f7ae..c154240a 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -114,7 +114,7 @@ signature COMPILER = sig
val untangle : (Mono.file, Mono.file) phase
val mono_reduce : (Mono.file, Mono.file) phase
val mono_shake : (Mono.file, Mono.file) phase
- (* val iflow : (Mono.file, Mono.file) phase *)
+ val iflow : (Mono.file, Mono.file) phase
val namejs : (Mono.file, Mono.file) phase
val scriptcheck : (Mono.file, Mono.file) phase
val jscomp : (Mono.file, Mono.file) phase
@@ -169,7 +169,7 @@ signature COMPILER = sig
val toMono_reduce : (string, Mono.file) transform
val toMono_shake : (string, Mono.file) transform
val toMono_opt2 : (string, Mono.file) transform
- (* val toIflow : (string, Mono.file) transform *)
+ val toIflow : (string, Mono.file) transform
val toNamejs : (string, Mono.file) transform
val toNamejs_untangle : (string, Mono.file) transform
val toScriptcheck : (string, Mono.file) transform
diff --git a/src/compiler.sml b/src/compiler.sml
index d91d02aa..bf7491e5 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -413,11 +413,7 @@ fun inputCommentableLine inf =
val lastUrp = ref ""
fun parseUrp' accLibs fname =
- (if !lastUrp = fname then
- ()
- else
- ModDb.reset ();
- lastUrp := fname;
+ (lastUrp := fname;
if not (Posix.FileSys.access (fname ^ ".urp", []) orelse Posix.FileSys.access (fname ^ "/lib.urp", []))
andalso Posix.FileSys.access (fname ^ ".ur", []) then
let
@@ -879,6 +875,10 @@ fun parseUrp' accLibs fname =
url := {action = Settings.Allow, kind = Settings.Exact, pattern = uri} :: !url)
| _ => ErrorMsg.error "Bad 'file' arguments")
+ | "jsFile" =>
+ (Settings.setFilePath thisPath;
+ Settings.addJsFile arg)
+
| _ => ErrorMsg.error ("Unrecognized command '" ^ cmd ^ "'");
read ()
end
@@ -1372,21 +1372,19 @@ val toMono_shake = transform mono_shake "mono_shake1" o toMono_reduce
val toMono_opt2 = transform mono_opt "mono_opt2" o toMono_shake
-(*
val iflow = {
func = (fn file => (if !doIflow then Iflow.check file else (); file)),
print = MonoPrint.p_file MonoEnv.empty
}
val toIflow = transform iflow "iflow" o toMono_opt2
-*)
val namejs = {
func = NameJS.rewrite,
print = MonoPrint.p_file MonoEnv.empty
}
-val toNamejs = transform namejs "namejs" o toMono_opt2
+val toNamejs = transform namejs "namejs" o toIflow
val toNamejs_untangle = transform untangle "namejs_untangle" o toNamejs
diff --git a/src/elab_env.sig b/src/elab_env.sig
index e0c589c4..cbc85cdd 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -37,6 +37,8 @@ signature ELAB_ENV = sig
type env
+ val dump : env -> unit
+
val empty : env
exception UnboundRel of int
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 9c9cd14f..3523b576 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -239,6 +239,10 @@ type env = {
str : (string * sgn) IM.map
}
+fun dump (env : env) =
+ (print "NamedC:\n";
+ IM.appi (fn (n, (x, k, co)) => print (x ^ " [" ^ Int.toString n ^ "]\n")) (#namedC env))
+
val namedCounter = ref 0
fun newNamed () =
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 6c08442b..dc07f6f8 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -41,6 +41,9 @@ structure Kind : sig
val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
bind : 'context * string -> 'context}
-> 'context -> (Elab.kind -> Elab.kind)
+ val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
+ bind : 'context * string -> 'context}
+ -> 'context -> 'state -> Elab.kind -> 'state
end
structure Con : sig
diff --git a/src/elab_util.sml b/src/elab_util.sml
index acc696dd..ed2e82a0 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -116,6 +116,12 @@ fun exists f k =
S.Return _ => true
| S.Continue _ => false
+fun foldB {kind, bind} ctx st k =
+ case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
+ bind = bind} ctx k st of
+ S.Continue (_, st) => st
+ | S.Return _ => raise Fail "ElabUtil.Kind.foldB: Impossible"
+
end
val mliftConInCon = ref (fn n : int => fn c : con => (raise Fail "You didn't set ElabUtil.mliftConInCon!") : con)
diff --git a/src/elaborate.sml b/src/elaborate.sml
index c3e81b65..25cce6bd 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1359,7 +1359,9 @@
end
and unifyCons env loc c1 c2 =
- unifyCons' env loc c1 c2
+ ((*Print.prefaces "uc" [("c1", p_con env c1),
+ ("c2", p_con env c2)];*)
+ unifyCons' env loc c1 c2)
handle CUnify' (env', err) => raise CUnify (c1, c2, env', err)
| KUnify (arg as {3 = env', ...}) => raise CUnify (c1, c2, env', CKind arg)
@@ -3079,6 +3081,8 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
fun cpart n = IM.find (!counterparts, n)
fun cparts (n2, n1) = counterparts := IM.insert (!counterparts, n2, n1)
+ fun uncparts n2 = (counterparts := #1 (IM.remove (!counterparts, n2)))
+ handle NotFound => ()
val sub2 = U.Con.map {kind = fn k => k,
con = fn c =>
@@ -3107,7 +3111,8 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
if E.checkENamed env n then
env
else
- E.pushCNamedAs env x n k (SOME c)
+ (uncparts n;
+ E.pushCNamedAs env x n k (SOME c))
| L'.SgiConAbs (x, n, k) =>
if E.checkENamed env n then
env
@@ -5019,5 +5024,7 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
@ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)
:: ds' @ file
end
+ handle e => (ModDb.revert ();
+ raise e)
end
diff --git a/src/iflow.sml b/src/iflow.sml
index f68d8f72..8bde7ea3 100644
--- a/src/iflow.sml
+++ b/src/iflow.sml
@@ -1263,7 +1263,7 @@ fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
val new = ref NONE
val old = ref NONE
- val rvs = map (fn (tab, v) =>
+ val rvs = map (fn Table (tab, v) =>
let
val nv = #NextVar arg ()
in
@@ -1272,7 +1272,8 @@ fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
| "Old" => old := SOME (tab, nv)
| _ => ();
(v, nv)
- end) (#From r)
+ end
+ | _ => raise Fail "Iflow: not ready for joins or nesteds") (#From r)
fun rvOf v =
case List.find (fn (v', _) => v' = v) rvs of
@@ -1282,7 +1283,8 @@ fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
val expIn = expIn (#NextVar arg) (#Env arg) rvOf
val saved = #Save arg ()
- fun addFrom () = app (fn (t, v) => #Add arg (AReln (Sql t, [rvOf v]))) (#From r)
+ fun addFrom () = app (fn Table (t, v) => #Add arg (AReln (Sql t, [rvOf v]))
+ | _ => raise Fail "Iflow: not ready for joins or nesteds") (#From r)
fun usedFields e =
case e of
diff --git a/src/jscomp.sml b/src/jscomp.sml
index 4c6bf0a9..e5a0cb27 100644
--- a/src/jscomp.sml
+++ b/src/jscomp.sml
@@ -1358,8 +1358,9 @@ fun process (file : file) =
val script =
if !foundJavaScript then
- lines ^ urlRules ^ String.concat (rev (#script st))
- ^ "\ntime_format = \"" ^ Prim.toCString (Settings.getTimeFormat ()) ^ "\";\n"
+ String.concatWith "" ((lines ^ urlRules ^ String.concat (rev (#script st))
+ ^ "\ntime_format = \"" ^ Prim.toCString (Settings.getTimeFormat ()) ^ "\";\n")
+ :: map (fn r => "\n// " ^ #Filename r ^ "\n\n" ^ #Content r ^ "\n") (Settings.listJsFiles ()))
else
""
in
diff --git a/src/main.mlton.sml b/src/main.mlton.sml
index 164ddfbd..67732b58 100644
--- a/src/main.mlton.sml
+++ b/src/main.mlton.sml
@@ -16,7 +16,7 @@
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
* ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
- * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
* CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
* SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
@@ -64,7 +64,7 @@ fun oneRun args =
fun doArgs args =
case args of
[] => ()
- | "-version" :: rest =>
+ | "-version" :: rest =>
printVersion ()
| "-numeric-version" :: rest =>
printNumericVersion ()
@@ -285,19 +285,25 @@ val () = case CommandLine.arguments () of
in
case cmd of
"" =>
- let
- val success = (oneRun (rev args))
- handle ex => (print "unhandled exception:\n";
- print (General.exnMessage ex ^ "\n");
- OS.Process.failure)
- in
- TextIO.flushOut TextIO.stdOut;
- TextIO.flushOut TextIO.stdErr;
- send (sock, if OS.Process.isSuccess success then
- "\001"
- else
- "\002")
- end
+ (case args of
+ ["stop", "daemon"] =>
+ (((Socket.close listen;
+ OS.FileSys.remove socket) handle OS.SysErr _ => ());
+ OS.Process.exit OS.Process.success)
+ | _ =>
+ let
+ val success = (oneRun (rev args))
+ handle ex => (print "unhandled exception:\n";
+ print (General.exnMessage ex ^ "\n");
+ OS.Process.failure)
+ in
+ TextIO.flushOut TextIO.stdOut;
+ TextIO.flushOut TextIO.stdErr;
+ send (sock, if OS.Process.isSuccess success then
+ "\001"
+ else
+ "\002")
+ end)
| _ => loop' (rest, cmd :: args)
end
end handle OS.SysErr _ => ()
@@ -312,7 +318,7 @@ val () = case CommandLine.arguments () of
(* Redirect the daemon's output to the socket. *)
redirect Posix.FileSys.stdout;
redirect Posix.FileSys.stderr;
-
+
loop' ("", []);
Socket.close sock;
@@ -321,6 +327,7 @@ val () = case CommandLine.arguments () of
Posix.IO.close oldStdout;
Posix.IO.close oldStderr;
+ Settings.reset ();
MLton.GC.pack ();
loop ()
end
@@ -330,8 +337,6 @@ val () = case CommandLine.arguments () of
Socket.listen (listen, 1);
loop ()
end)
- | ["daemon", "stop"] =>
- (OS.FileSys.remove socket handle OS.SysErr _ => OS.Process.exit OS.Process.success)
| args =>
let
val sock = UnixSock.Strm.socket ()
diff --git a/src/postgres.sml b/src/postgres.sml
index bc1238c0..1c95f414 100644
--- a/src/postgres.sml
+++ b/src/postgres.sml
@@ -278,7 +278,7 @@ fun init {dbstring, prepared = ss, tables, views, sequences} =
val sl = CharVector.map Char.toLower s
val q = "SELECT COUNT(*) FROM pg_class WHERE relname = '"
- ^ sl ^ "' AND relkind = 'S'"
+ ^ sl ^ "' AND relkind = 'S' AND pg_catalog.pg_table_is_visible(oid)"
in
box [string "res = PQexec(conn, \"",
string q,
diff --git a/src/reduce.sml b/src/reduce.sml
index 8691b93a..0762a4a1 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -588,7 +588,7 @@ fun kindConAndExp (namedC, namedE) =
(p, body')
end) pes
- val cc' = {disc = disc, result = c2}
+ val cc' = {disc = con env' disc, result = con env' c2}
in
(ECase (e, pes', cc'), loc)
end
@@ -626,7 +626,7 @@ fun kindConAndExp (namedC, namedE) =
end) pes
val c' = E.subConInCon (0, c) c'
- val cc' = {disc = disc, result = c'}
+ val cc' = {disc = con env disc, result = con env c'}
in
(ECase (e, pes', cc'), loc)
end
diff --git a/src/settings.sig b/src/settings.sig
index e94832e0..732a31fa 100644
--- a/src/settings.sig
+++ b/src/settings.sig
@@ -27,6 +27,10 @@
signature SETTINGS = sig
+ (* Call this when compiling a new project, e.g. with the Ur/Web daemon or from the SML/NJ REPL.
+ * Some settings stay, but most are reset, especially files cached for the app to serve. *)
+ val reset : unit -> unit
+
(* XXX these should be unit -> string too *)
val configBin : string ref
val configLib : string ref
@@ -287,4 +291,7 @@ signature SETTINGS = sig
val addFile : {Uri : string, LoadFromFilename : string} -> unit
val listFiles : unit -> {Uri : string, ContentType : string option, LastModified : Time.time, Bytes : Word8Vector.vector} list
+
+ val addJsFile : string (* filename *) -> unit
+ val listJsFiles : unit -> {Filename : string, Content : string} list
end
diff --git a/src/settings.sml b/src/settings.sml
index f9125c64..94692a2e 100644
--- a/src/settings.sml
+++ b/src/settings.sml
@@ -727,11 +727,6 @@ val minHeap = ref 0
fun setMinHeap n = if n >= 0 then minHeap := n else raise Fail "Trying to set negative minHeap"
fun getMinHeap () = !minHeap
-structure SS = BinarySetFn(struct
- type ord_key = string
- val compare = String.compare
- end)
-
val alwaysInline = ref SS.empty
fun addAlwaysInline s = alwaysInline := SS.add (!alwaysInline, s)
fun checkAlwaysInline s = SS.member (!alwaysInline, s)
@@ -913,4 +908,68 @@ fun addFile {Uri, LoadFromFilename} =
fun listFiles () = map #2 (SM.listItems (!files))
+val jsFiles = ref (SM.empty : {Filename : string, Content : string} SM.map)
+
+fun addJsFile LoadFromFilename =
+ let
+ val path = OS.Path.concat (!filePath, LoadFromFilename)
+ val inf = TextIO.openIn path
+ in
+ jsFiles := SM.insert (!jsFiles,
+ path,
+ {Filename = LoadFromFilename,
+ Content = TextIO.inputAll inf});
+ TextIO.closeIn inf
+ end handle IO.Io _ =>
+ ErrorMsg.error ("Error loading file " ^ LoadFromFilename)
+ | OS.SysErr (s, _) =>
+ ErrorMsg.error ("Error loading file " ^ LoadFromFilename ^ " (" ^ s ^ ")")
+
+fun listJsFiles () = SM.listItems (!jsFiles)
+
+fun reset () =
+ (urlPrefixFull := "/";
+ urlPrefix := "/";
+ urlPrePrefix := "";
+ timeout := 0;
+ headers := [];
+ scripts := [];
+ clientToServer := clientToServerBase;
+ effectful := effectfulBase;
+ benign := benignBase;
+ client := clientBase;
+ server := serverBase;
+ jsFuncs := jsFuncsBase;
+ rewrites := [];
+ url := [];
+ mime := [];
+ request := [];
+ response := [];
+ env := [];
+ debug := false;
+ dbstring := NONE;
+ exe := NONE;
+ sql := NONE;
+ coreInline := 5;
+ monoInline := 5;
+ staticLinking := false;
+ deadlines := false;
+ sigFile := NONE;
+ safeGet := SS.empty;
+ onError := NONE;
+ limitsList := [];
+ minHeap := 0;
+ alwaysInline := SS.empty;
+ neverInline := SS.empty;
+ noXsrfProtection := SS.empty;
+ timeFormat := "%c";
+ mangle := true;
+ html5 := false;
+ less := false;
+ noMimeFile := false;
+ mimeTypes := NONE;
+ files := SM.empty;
+ jsFiles := SM.empty;
+ filePath := ".")
+
end
diff --git a/src/sources b/src/sources
index 1436575d..8bf80bc6 100644
--- a/src/sources
+++ b/src/sources
@@ -207,6 +207,9 @@ $(SRC)/mono_shake.sml
$(SRC)/fuse.sig
$(SRC)/fuse.sml
+$(SRC)/iflow.sig
+$(SRC)/iflow.sml
+
$(SRC)/name_js.sig
$(SRC)/name_js.sml
diff --git a/src/unnest.sml b/src/unnest.sml
index fceb5026..3034eb6e 100644
--- a/src/unnest.sml
+++ b/src/unnest.sml
@@ -65,44 +65,71 @@ val subExpInExp =
| ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep)
| (ctx, _) => ctx}
-val fvsCon = U.Con.foldB {kind = fn (_, _, st) => st,
- con = fn (cb, c, cvs) =>
+val fvsKind = U.Kind.foldB {kind = fn (kb, k, kvs) =>
+ case k of
+ KRel n =>
+ if n >= kb then
+ IS.add (kvs, n - kb)
+ else
+ kvs
+ | _ => kvs,
+ bind = fn (kb, b) => kb + 1}
+ 0 IS.empty
+
+val fvsCon = U.Con.foldB {kind = fn ((kb, _), k, st as (kvs, cvs)) =>
+ case k of
+ KRel n =>
+ if n >= kb then
+ (IS.add (kvs, n - kb), cvs)
+ else
+ st
+ | _ => st,
+ con = fn ((_, cb), c, st as (kvs, cvs)) =>
case c of
CRel n =>
if n >= cb then
- IS.add (cvs, n - cb)
+ (kvs, IS.add (cvs, n - cb))
else
- cvs
- | _ => cvs,
- bind = fn (cb, b) =>
+ st
+ | _ => st,
+ bind = fn (ctx as (kb, cb), b) =>
case b of
- U.Con.RelC _ => cb + 1
- | _ => cb}
- 0 IS.empty
-
-fun fvsExp nr = U.Exp.foldB {kind = fn (_, _, st) => st,
- con = fn ((cb, eb), c, st as (cvs, evs)) =>
+ U.Con.RelK _ => (kb + 1, cb + 1)
+ | U.Con.RelC _ => (kb, cb + 1)
+ | _ => ctx}
+ (0, 0) (IS.empty, IS.empty)
+
+fun fvsExp nr = U.Exp.foldB {kind = fn ((kb, _, _), k, st as (kvs, cvs, evs)) =>
+ case k of
+ KRel n =>
+ if n >= kb then
+ (IS.add (kvs, n - kb), cvs, evs)
+ else
+ st
+ | _ => st,
+ con = fn ((kb, cb, eb), c, st as (kvs, cvs, evs)) =>
case c of
CRel n =>
if n >= cb then
- (IS.add (cvs, n - cb), evs)
+ (kvs, IS.add (cvs, n - cb), evs)
else
st
| _ => st,
- exp = fn ((cb, eb), e, st as (cvs, evs)) =>
+ exp = fn ((kb, cb, eb), e, st as (kvs, cvs, evs)) =>
case e of
ERel n =>
if n >= eb then
- (cvs, IS.add (evs, n - eb))
+ (kvs, cvs, IS.add (evs, n - eb))
else
st
| _ => st,
- bind = fn (ctx as (cb, eb), b) =>
+ bind = fn (ctx as (kb, cb, eb), b) =>
case b of
- U.Exp.RelC _ => (cb + 1, eb)
- | U.Exp.RelE _ => (cb, eb + 1)
+ U.Exp.RelK _ => (kb + 1, cb, eb)
+ | U.Exp.RelC _ => (kb, cb + 1, eb)
+ | U.Exp.RelE _ => (kb, cb, eb + 1)
| _ => ctx}
- (0, nr) (IS.empty, IS.empty)
+ (0, 0, nr) (IS.empty, IS.empty, IS.empty)
fun positionOf (x : int) ls =
let
@@ -123,46 +150,62 @@ fun positionOf (x : int) ls =
^ ")")
end
-fun squishCon cfv =
- U.Con.mapB {kind = fn _ => fn k => k,
- con = fn cb => fn c =>
- case c of
- CRel n =>
- if n >= cb then
- CRel (positionOf (n - cb) cfv + cb)
- else
- c
- | _ => c,
- bind = fn (cb, b) =>
- case b of
- U.Con.RelC _ => cb + 1
- | _ => cb}
- 0
-
-fun squishExp (nr, cfv, efv) =
- U.Exp.mapB {kind = fn _ => fn k => k,
- con = fn (cb, eb) => fn c =>
- case c of
- CRel n =>
- if n >= cb then
- CRel (positionOf (n - cb) cfv + cb)
- else
- c
- | _ => c,
- exp = fn (cb, eb) => fn e =>
- case e of
- ERel n =>
- if n >= eb then
- ERel (positionOf (n - eb) efv + eb - nr)
+fun squishCon (kfv, cfv) =
+ U.Con.mapB {kind = fn (kb, _) => fn k =>
+ case k of
+ KRel n =>
+ if n >= kb then
+ KRel (positionOf (n - kb) kfv + kb)
else
- e
- | _ => e,
- bind = fn (ctx as (cb, eb), b) =>
+ k
+ | _ => k,
+ con = fn (_, cb) => fn c =>
+ case c of
+ CRel n =>
+ if n >= cb then
+ CRel (positionOf (n - cb) cfv + cb)
+ else
+ c
+ | _ => c,
+ bind = fn (ctx as (kb, cb), b) =>
+ case b of
+ U.Con.RelK _ => (kb + 1, cb)
+ | U.Con.RelC _ => (kb, cb + 1)
+ | _ => ctx}
+ (0, 0)
+
+fun squishExp (nr, kfv, cfv, efv) =
+ U.Exp.mapB {kind = fn (kb, _, _) => fn k =>
+ case k of
+ KRel n =>
+ if n >= kb then
+ KRel (positionOf (n - kb) kfv + kb)
+ else
+ k
+ | _ => k,
+ con = fn (_, cb, _) => fn c =>
+ case c of
+ CRel n =>
+ if n >= cb then
+ CRel (positionOf (n - cb) cfv + cb)
+ else
+ c
+ | _ => c,
+ exp = fn (_, _, eb) => fn e =>
+ case e of
+ ERel n =>
+ if n >= eb then
+ ERel (positionOf (n - eb) efv + eb - nr)
+ else
+ e
+ | _ => e,
+ bind = fn (ctx as (kb, cb, eb), b) =>
case b of
- U.Exp.RelC _ => (cb + 1, eb)
- | U.Exp.RelE _ => (cb, eb + 1)
+ U.Exp.RelK _ => (kb + 1, cb, eb)
+ | U.Exp.RelC _ => (kb, cb + 1, eb)
+ | U.Exp.RelE _ => (kb, cb, eb + 1)
| _ => ctx}
- (0, nr)
+ (0, 0, nr)
type state = {
maxName : int,
@@ -173,7 +216,7 @@ fun kind (_, k, st) = (k, st)
val basis = ref 0
-fun exp ((ks, ts), e as old, st : state) =
+fun exp ((ns, ks, ts), e as old, st : state) =
case e of
ELet (eds, e, t) =>
let
@@ -249,21 +292,23 @@ fun exp ((ks, ts), e as old, st : state) =
val vis = map (fn (x, t, e) =>
(x, t, doSubst' (e, subsLocal))) vis
- val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) =>
- let
- val (cfv', efv') = fvsExp nr e
- (*val () = Print.prefaces "fvsExp"
- [("e", ElabPrint.p_exp E.empty e),
- ("cfv", Print.PD.string
- (Int.toString (IS.numItems cfv'))),
- ("efv", Print.PD.string
- (Int.toString (IS.numItems efv')))]*)
- val cfv'' = fvsCon t
- in
- (IS.union (cfv, IS.union (cfv', cfv'')),
- IS.union (efv, efv'))
- end)
- (IS.empty, IS.empty) vis
+ val (kfv, cfv, efv) =
+ foldl (fn ((_, t, e), (kfv, cfv, efv)) =>
+ let
+ val (kfv', cfv', efv') = fvsExp nr e
+ (*val () = Print.prefaces "fvsExp"
+ [("e", ElabPrint.p_exp E.empty e),
+ ("cfv", Print.PD.string
+ (Int.toString (IS.numItems cfv'))),
+ ("efv", Print.PD.string
+ (Int.toString (IS.numItems efv')))]*)
+ val (kfv'', cfv'') = fvsCon t
+ in
+ (IS.union (kfv, IS.union (kfv', kfv'')),
+ IS.union (cfv, IS.union (cfv', cfv'')),
+ IS.union (efv, efv'))
+ end)
+ (IS.empty, IS.empty, IS.empty) vis
(*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*)
(*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*)
@@ -272,12 +317,30 @@ fun exp ((ks, ts), e as old, st : state) =
("t", ElabPrint.p_con E.empty t)]) ts
val () = IS.app (fn n => print ("Free: " ^ Int.toString n ^ "\n")) efv*)
+ val kfv = IS.foldl (fn (x, kfv) =>
+ let
+ (*val () = print (Int.toString x ^ "\n")*)
+ val (_, k) = List.nth (ks, x)
+ in
+ IS.union (kfv, fvsKind k)
+ end)
+ kfv cfv
+
+ val kfv = IS.foldl (fn (x, kfv) =>
+ let
+ (*val () = print (Int.toString x ^ "\n")*)
+ val (_, t) = List.nth (ts, x)
+ in
+ IS.union (kfv, #1 (fvsCon t))
+ end)
+ kfv efv
+
val cfv = IS.foldl (fn (x, cfv) =>
let
(*val () = print (Int.toString x ^ "\n")*)
val (_, t) = List.nth (ts, x)
in
- IS.union (cfv, fvsCon t)
+ IS.union (cfv, #2 (fvsCon t))
end)
cfv efv
(*val () = print "B\n"*)
@@ -299,6 +362,10 @@ fun exp ((ks, ts), e as old, st : state) =
val e = (ENamed n, loc)
val e = IS.foldr (fn (x, e) =>
+ (EKApp (e, (KRel x, loc)), loc))
+ e kfv
+
+ val e = IS.foldr (fn (x, e) =>
(ECApp (e, (CRel x, loc)), loc))
e cfv
@@ -311,6 +378,7 @@ fun exp ((ks, ts), e as old, st : state) =
end)
vis
+ val kfv = IS.listItems kfv
val cfv = IS.listItems cfv
val efv = IS.listItems efv
@@ -324,17 +392,17 @@ fun exp ((ks, ts), e as old, st : state) =
(*val () = Print.prefaces "squishCon"
[("t", ElabPrint.p_con E.empty t)]*)
- val t = squishCon cfv t
+ val t = squishCon (kfv, cfv) t
(*val () = Print.prefaces "squishExp"
[("e", ElabPrint.p_exp E.empty e)]*)
- val e = squishExp (nr, cfv, efv) e
+ val e = squishExp (nr, kfv, cfv, efv) e
(*val () = print ("Avail: " ^ Int.toString (length ts) ^ "\n")*)
val (e, t) = foldl (fn (ex, (e, t)) =>
let
(*val () = print (Int.toString ex ^ "\n")*)
val (name, t') = List.nth (ts, ex)
- val t' = squishCon cfv t'
+ val t' = squishCon (kfv, cfv) t'
in
((EAbs (name,
t',
@@ -360,6 +428,17 @@ fun exp ((ks, ts), e as old, st : state) =
t), loc))
end)
(e, t) cfv
+
+ val (e, t) = foldl (fn (kx, (e, t)) =>
+ let
+ val name = List.nth (ns, kx)
+ in
+ ((EKAbs (name,
+ e), loc),
+ (TKFun (name,
+ t), loc))
+ end)
+ (e, t) kfv
in
(*Print.prefaces "Have a vi"
[("x", Print.PD.string x),
@@ -391,11 +470,12 @@ fun exp ((ks, ts), e as old, st : state) =
fun default (ctx, d, st) = (d, st)
-fun bind ((ks, ts), b) =
+fun bind ((ns, ks, ts), b) =
case b of
- U.Decl.RelC p => (p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts)
- | U.Decl.RelE p => (ks, p :: ts)
- | _ => (ks, ts)
+ U.Decl.RelK x => (x :: ns, ks, ts)
+ | U.Decl.RelC p => (ns, p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts)
+ | U.Decl.RelE p => (ns, ks, p :: ts)
+ | _ => (ns, ks, ts)
val unnestDecl = U.Decl.foldMapB {kind = kind,
con = default,
@@ -405,7 +485,7 @@ val unnestDecl = U.Decl.foldMapB {kind = kind,
str = default,
decl = default,
bind = bind}
- ([], [])
+ ([], [], [])
fun unnest file =
let
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 09:58:51 +0000