summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/bg_thread.dummy.sml9
-rw-r--r--src/bg_thread.mlton.sml65
-rw-r--r--src/bg_thread.sig7
-rw-r--r--src/compiler.sml2
-rw-r--r--src/elab_env.sig4
-rw-r--r--src/elab_env.sml10
-rw-r--r--src/elab_print.sig1
-rw-r--r--src/elab_util_pos.sig66
-rw-r--r--src/elab_util_pos.sml910
-rw-r--r--src/elaborate.sig25
-rw-r--r--src/elaborate.sml27
-rw-r--r--src/elisp/urweb-mode.el27
-rw-r--r--src/errormsg.sig8
-rw-r--r--src/errormsg.sml29
-rw-r--r--src/fromjson.sig8
-rw-r--r--src/fromjson.sml35
-rw-r--r--src/getinfo.sig50
-rw-r--r--src/getinfo.sml304
-rw-r--r--src/json.sig13
-rw-r--r--src/json.sml293
-rw-r--r--src/lsp.sig3
-rw-r--r--src/lsp.sml514
-rw-r--r--src/lspspec.sml450
-rw-r--r--src/main.mlton.sml1
-rw-r--r--src/mod_db.sig5
-rw-r--r--src/mod_db.sml81
-rw-r--r--src/prefix.cm2
-rw-r--r--src/prefix.mlb3
-rw-r--r--src/search.sig5
-rw-r--r--src/search.sml8
-rw-r--r--src/sources17
31 files changed, 2960 insertions, 22 deletions
diff --git a/src/bg_thread.dummy.sml b/src/bg_thread.dummy.sml
new file mode 100644
index 00000000..699fa741
--- /dev/null
+++ b/src/bg_thread.dummy.sml
@@ -0,0 +1,9 @@
+(*
+ Dummy implementation. Threading is only supported in MLton.
+ All other implementations just immediately run the background tasks
+*)
+structure BgThread:> BGTHREAD = struct
+ fun queueBgTask filename f = f ()
+ fun hasBgTasks () = false
+ fun runBgTaskForABit () = ()
+end
diff --git a/src/bg_thread.mlton.sml b/src/bg_thread.mlton.sml
new file mode 100644
index 00000000..91195940
--- /dev/null
+++ b/src/bg_thread.mlton.sml
@@ -0,0 +1,65 @@
+(* Notice: API is kinda bad. We only allow queuing a single task per file *)
+(* This works for us because we only do elaboration in the background, nothing else *)
+
+structure BgThread:> BGTHREAD = struct
+ open Posix.Signal
+ open MLton
+ open Itimer Signal Thread
+
+ val topLevel: Thread.Runnable.t option ref = ref NONE
+ val currentRunningThreadIsForFileName: string ref = ref ""
+ (* FIFO queue: Max one task per fileName *)
+ val tasks: ((Thread.Runnable.t * string) list) ref = ref []
+ fun hasBgTasks () = List.length (!tasks) > 0
+
+ fun setItimer t =
+ Itimer.set (Itimer.Real,
+ {value = t,
+ interval = t})
+
+
+ fun done () = Thread.atomically
+ (fn () =>
+ ( tasks := (List.filter (fn q => #2 q <> (!currentRunningThreadIsForFileName)) (!tasks))
+ ; case !tasks of
+ [] => (setItimer Time.zeroTime
+ ; currentRunningThreadIsForFileName := ""
+ ; switch (fn _ => valOf (!topLevel)))
+ | t :: rest => (currentRunningThreadIsForFileName := #2 t
+ ; switch (fn _ => #1 t))))
+
+ fun queueBgTask fileName f =
+ let
+ fun new (f: unit -> unit): Thread.Runnable.t =
+ Thread.prepare
+ (Thread.new (fn () => ((f () handle _ => done ())
+ ; done ())),
+ ())
+ in
+ case List.find (fn t => #2 t = fileName) (!tasks) of
+ NONE => tasks := (new f, fileName) :: (!tasks)
+ | SOME t =>
+ (* Move existing task to front of list *)
+ tasks := t :: List.filter (fn q => #2 q <> fileName) (!tasks)
+ end
+
+ fun replaceInList (l: 'a list) (f: 'a -> bool) (replacement: 'a) =
+ List.map (fn a => if f a then replacement else a ) l
+ fun runBgTaskForABit () =
+ case !(tasks) of
+ [] => ()
+ | t :: rest =>
+ (setHandler (alrm, Handler.handler (fn t => (setItimer Time.zeroTime
+ (* This might some not needed, but other wise you get "Dead thread" error *)
+ ; tasks := replaceInList
+ (!tasks)
+ (fn t => #2 t = (!currentRunningThreadIsForFileName))
+ (t, (!currentRunningThreadIsForFileName))
+ ; currentRunningThreadIsForFileName := ""
+ ; valOf (!topLevel))))
+ ; setItimer (Time.fromMilliseconds 200)
+ ; currentRunningThreadIsForFileName := #2 t
+ ; switch (fn top => (topLevel := SOME (Thread.prepare (top, ())); #1 t)) (* store top level thread and activate BG thread *)
+ ; setItimer Time.zeroTime
+ )
+ end
diff --git a/src/bg_thread.sig b/src/bg_thread.sig
new file mode 100644
index 00000000..5455bbc8
--- /dev/null
+++ b/src/bg_thread.sig
@@ -0,0 +1,7 @@
+(* Notice: API is kinda bad. We only allow queuing a single task per file *)
+(* This works for us because we only do elaboration in the background, nothing else *)
+signature BGTHREAD = sig
+ val queueBgTask: string (* fileName *) -> (unit -> unit) -> unit
+ val hasBgTasks: unit -> bool
+ val runBgTaskForABit: unit -> unit
+end
diff --git a/src/compiler.sml b/src/compiler.sml
index 06abed0c..9cbe9949 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -1283,7 +1283,7 @@ val elaborate = {
in
Elaborate.elabFile basis (OS.FileSys.modTime basisF)
topStr topSgn (if Time.< (tm1, tm2) then tm2 else tm1)
- ElabEnv.empty file
+ ElabEnv.empty (fn env => env) file
end,
print = ElabPrint.p_file ElabEnv.empty
}
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 47b31c08..4f994221 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -100,6 +100,10 @@ signature ELAB_ENV = sig
val lookupStrNamed : env -> int -> string * Elab.sgn
val lookupStr : env -> string -> (int * Elab.sgn) option
+
+ val dumpCs: env -> (string * Elab.kind) list
+ val dumpEs: env -> (string * Elab.con) list
+ val dumpStrs: env -> (string * (int * Elab.sgn)) list
val edeclBinds : env -> Elab.edecl -> env
val declBinds : env -> Elab.decl -> env
diff --git a/src/elab_env.sml b/src/elab_env.sml
index a2097aa9..5fa32cd2 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -986,6 +986,16 @@ fun lookupStrNamed (env : env) n =
fun lookupStr (env : env) x = SM.find (#renameStr env, x)
+fun dumpCs (env: env): (string * kind) list =
+ List.map (fn (name, value) => case value of
+ Rel' (_, x) => (name, x)
+ | Named' (_, x) => (name, x))
+ (SM.listItemsi (#renameC env))
+(* TODO try again with #renameE *)
+fun dumpEs (env: env): (string * con) list =
+ #relE env @ IM.listItems (#namedE env)
+fun dumpStrs (env: env) =
+ SM.listItemsi (#renameStr env)
fun sgiSeek (sgi, (sgns, strs, cons)) =
case sgi of
diff --git a/src/elab_print.sig b/src/elab_print.sig
index 1eb832b3..84715b9d 100644
--- a/src/elab_print.sig
+++ b/src/elab_print.sig
@@ -38,6 +38,7 @@ signature ELAB_PRINT = sig
val p_sgn : ElabEnv.env -> Elab.sgn Print.printer
val p_str : ElabEnv.env -> Elab.str Print.printer
val p_file : ElabEnv.env -> Elab.file Print.printer
+
val debug : bool ref
end
diff --git a/src/elab_util_pos.sig b/src/elab_util_pos.sig
new file mode 100644
index 00000000..95d8b591
--- /dev/null
+++ b/src/elab_util_pos.sig
@@ -0,0 +1,66 @@
+(* Copyright (c) 2008-2010, 2012, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ * this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ * this list of conditions and the following disclaimer in the documentation
+ * and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ * derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * 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
+ * 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
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+(* This is identical to ELAB_UTIL, but keeps source spans around *)
+(* Maybe these modules can be unified? *)
+
+signature ELAB_UTIL_POS = sig
+
+ val mliftConInCon : (int -> Elab.con -> Elab.con) ref
+
+ structure Decl : sig
+ datatype binder =
+ RelK of string
+ | RelC of string * Elab.kind
+ | NamedC of string * int * Elab.kind * Elab.con option
+ | RelE of string * Elab.con
+ | NamedE of string * Elab.con
+ | Str of string * int * Elab.sgn
+ | Sgn of string * int * Elab.sgn
+
+ val fold : {kind : Elab.kind * 'state -> 'state,
+ con : Elab.con * 'state -> 'state,
+ exp : Elab.exp * 'state -> 'state,
+ sgn_item : Elab.sgn_item * 'state -> 'state,
+ sgn : Elab.sgn * 'state -> 'state,
+ str : Elab.str * 'state -> 'state,
+ decl : Elab.decl * 'state -> 'state}
+ -> 'state -> Elab.decl -> 'state
+
+ val foldB : {kind : 'context * Elab.kind * 'state -> 'state,
+ con : 'context * Elab.con * 'state -> 'state,
+ exp : 'context * Elab.exp * 'state -> 'state,
+ sgn_item : 'context * Elab.sgn_item * 'state -> 'state,
+ sgn : 'context * Elab.sgn * 'state -> 'state,
+ str : 'context * Elab.str * 'state -> 'state,
+ decl : 'context * Elab.decl * 'state -> 'state,
+ bind: 'context * binder -> 'context
+ }
+ -> 'context -> 'state -> Elab.decl -> 'state
+ end
+
+end
diff --git a/src/elab_util_pos.sml b/src/elab_util_pos.sml
new file mode 100644
index 00000000..d8d1bfdd
--- /dev/null
+++ b/src/elab_util_pos.sml
@@ -0,0 +1,910 @@
+(* Copyright (c) 2008-2010, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ * this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ * this list of conditions and the following disclaimer in the documentation
+ * and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ * derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * 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
+ * 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
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure ElabUtilPos :> ELAB_UTIL_POS = struct
+
+open Elab
+
+structure S = Search
+
+structure Kind = struct
+
+fun mapfoldB {kind, bind} =
+ let
+ fun mfk ctx k acc =
+ S.bindPWithPos (mfk' ctx k acc, kind ctx)
+
+ and mfk' ctx (kAll as (k, loc)) =
+ case k of
+ KType => S.return2 kAll
+
+ | KArrow (k1, k2) =>
+ S.bind2 (mfk ctx k1,
+ fn k1' =>
+ S.map2 (mfk ctx k2,
+ fn k2' =>
+ (KArrow (k1', k2'), loc)))
+
+ | KName => S.return2 kAll
+
+ | KRecord k =>
+ S.map2 (mfk ctx k,
+ fn k' =>
+ (KRecord k', loc))
+
+ | KUnit => S.return2 kAll
+
+ | KTuple ks =>
+ S.map2 (ListUtil.mapfold (mfk ctx) ks,
+ fn ks' =>
+ (KTuple ks', loc))
+
+ | KError => S.return2 kAll
+
+ | KUnif (_, _, ref (KKnown k)) => mfk' ctx k
+ | KUnif _ => S.return2 kAll
+
+ | KTupleUnif (_, _, ref (KKnown k)) => mfk' ctx k
+ | KTupleUnif (loc, nks, r) =>
+ S.map2 (ListUtil.mapfold (fn (n, k) =>
+ S.map2 (mfk ctx k,
+ fn k' =>
+ (n, k'))) nks,
+ fn nks' =>
+ (KTupleUnif (loc, nks', r), loc))
+
+
+ | KRel _ => S.return2 kAll
+ | KFun (x, k) =>
+ S.map2 (mfk (bind (ctx, x)) k,
+ fn k' =>
+ (KFun (x, k'), loc))
+ in
+ mfk
+ end
+
+end
+
+val mliftConInCon = ref (fn n : int => fn c : con => (raise Fail "You didn't set ElabUtil.mliftConInCon!") : con)
+
+structure Con = struct
+
+datatype binder =
+ RelK of string
+ | RelC of string * Elab.kind
+ | NamedC of string * int * Elab.kind * Elab.con option
+
+fun mapfoldB {kind = fk, con = fc, bind} =
+ let
+ val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, s) => bind (ctx, RelK s)}
+
+ fun mfc ctx c acc =
+ S.bindPWithPos (mfc' ctx c acc, fc ctx)
+
+ and mfc' ctx (cAll as (c, loc)) =
+ case c of
+ TFun (c1, c2) =>
+ S.bind2 (mfc ctx c1,
+ fn c1' =>
+ S.map2 (mfc ctx c2,
+ fn c2' =>
+ (TFun (c1', c2'), loc)))
+ | TCFun (e, x, k, c) =>
+ S.bind2 (mfk ctx k,
+ fn k' =>
+ S.map2 (mfc (bind (ctx, RelC (x, k))) c,
+ fn c' =>
+ (TCFun (e, x, k', c'), loc)))
+ | TDisjoint (c1, c2, c3) =>
+ S.bind2 (mfc ctx c1,
+ fn c1' =>
+ S.bind2 (mfc ctx c2,
+ fn c2' =>
+ S.map2 (mfc ctx c3,
+ fn c3' =>
+ (TDisjoint (c1', c2', c3'), loc))))
+ | TRecord c =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (TRecord c', loc))
+
+ | CRel _ => S.return2 cAll
+ | CNamed _ => S.return2 cAll
+ | CModProj _ => S.return2 cAll
+ | CApp (c1, c2) =>
+ S.bind2 (mfc ctx c1,
+ fn c1' =>
+ S.map2 (mfc ctx c2,
+ fn c2' =>
+ (CApp (c1', c2'), loc)))
+ | CAbs (x, k, c) =>
+ S.bind2 (mfk ctx k,
+ fn k' =>
+ S.map2 (mfc (bind (ctx, RelC (x, k))) c,
+ fn c' =>
+ (CAbs (x, k', c'), loc)))
+
+ | CName _ => S.return2 cAll
+
+ | CRecord (k, xcs) =>
+ S.bind2 (mfk ctx k,
+ fn k' =>
+ S.map2 (ListUtil.mapfold (fn (x, c) =>
+ S.bind2 (mfc ctx x,
+ fn x' =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (x', c'))))
+ xcs,
+ fn xcs' =>
+ (CRecord (k', xcs'), loc)))
+ | CConcat (c1, c2) =>
+ S.bind2 (mfc ctx c1,
+ fn c1' =>
+ S.map2 (mfc ctx c2,
+ fn c2' =>
+ (CConcat (c1', c2'), loc)))
+ | CMap (k1, k2) =>
+ S.bind2 (mfk ctx k1,
+ fn k1' =>
+ S.map2 (mfk ctx k2,
+ fn k2' =>
+ (CMap (k1', k2'), loc)))
+
+ | CUnit => S.return2 cAll
+
+ | CTuple cs =>
+ S.map2 (ListUtil.mapfold (mfc ctx) cs,
+ fn cs' =>
+ (CTuple cs', loc))
+
+ | CProj (c, n) =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (CProj (c', n), loc))
+
+ | CError => S.return2 cAll
+ | CUnif (nl, _, _, _, ref (Known c)) => mfc' ctx (!mliftConInCon nl c)
+ | CUnif _ => S.return2 cAll
+
+ | CKAbs (x, c) =>
+ S.map2 (mfc (bind (ctx, RelK x)) c,
+ fn c' =>
+ (CKAbs (x, c'), loc))
+ | CKApp (c, k) =>
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.map2 (mfk ctx k,
+ fn k' =>
+ (CKApp (c', k'), loc)))
+ | TKFun (x, c) =>
+ S.map2 (mfc (bind (ctx, RelK x)) c,
+ fn c' =>
+ (TKFun (x, c'), loc))
+ in
+ mfc
+ end
+
+end
+
+structure Exp = struct
+
+datatype binder =
+ RelK of string
+ | RelC of string * Elab.kind
+ | NamedC of string * int * Elab.kind * Elab.con option
+ | RelE of string * Elab.con
+ | NamedE of string * Elab.con
+
+fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
+ let
+ val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
+
+ fun bind' (ctx, b) =
+ let
+ val b' = case b of
+ Con.RelK x => RelK x
+ | Con.RelC x => RelC x
+ | Con.NamedC x => NamedC x
+ in
+ bind (ctx, b')
+ end
+ val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
+
+ fun doVars ((p, _), ctx) =
+ case p of
+ PVar xt => bind (ctx, RelE xt)
+ | PPrim _ => ctx
+ | PCon (_, _, _, NONE) => ctx
+ | PCon (_, _, _, SOME p) => doVars (p, ctx)
+ | PRecord xpcs =>
+ foldl (fn ((_, p, _), ctx) => doVars (p, ctx))
+ ctx xpcs
+
+ fun mfe ctx e acc =
+ S.bindPWithPos (mfe' ctx e acc, fe ctx)
+
+ and mfe' ctx (eAll as (e, loc)) =
+ case e of
+ EPrim _ => S.return2 eAll
+ | ERel _ => S.return2 eAll
+ | ENamed _ => S.return2 eAll
+ | EModProj _ => S.return2 eAll
+ | EApp (e1, e2) =>
+ S.bind2 (mfe ctx e1,
+ fn e1' =>
+ S.map2 (mfe ctx e2,
+ fn e2' =>
+ (EApp (e1', e2'), loc)))
+ | EAbs (x, dom, ran, e) =>
+ S.bind2 (mfc ctx dom,
+ fn dom' =>
+ S.bind2 (mfc ctx ran,
+ fn ran' =>
+ S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
+ fn e' =>
+ (EAbs (x, dom', ran', e'), loc))))
+
+ | ECApp (e, c) =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (ECApp (e', c'), loc)))
+ | ECAbs (expl, x, k, e) =>
+ S.bind2 (mfk ctx k,
+ fn k' =>
+ S.map2 (mfe (bind (ctx, RelC (x, k))) e,
+ fn e' =>
+ (ECAbs (expl, x, k', e'), loc)))
+
+ | ERecord xes =>
+ S.map2 (ListUtil.mapfold (fn (x, e, t) =>
+ S.bind2 (mfc ctx x,
+ fn x' =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.map2 (mfc ctx t,
+ fn t' =>
+ (x', e', t')))))
+ xes,
+ fn xes' =>
+ (ERecord xes', loc))
+ | EField (e, c, {field, rest}) =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.bind2 (mfc ctx field,
+ fn field' =>
+ S.map2 (mfc ctx rest,
+ fn rest' =>
+ (EField (e', c', {field = field', rest = rest'}), loc)))))
+ | EConcat (e1, c1, e2, c2) =>
+ S.bind2 (mfe ctx e1,
+ fn e1' =>
+ S.bind2 (mfc ctx c1,
+ fn c1' =>
+ S.bind2 (mfe ctx e2,
+ fn e2' =>
+ S.map2 (mfc ctx c2,
+ fn c2' =>
+ (EConcat (e1', c1', e2', c2'),
+ loc)))))
+ | ECut (e, c, {field, rest}) =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.bind2 (mfc ctx field,
+ fn field' =>
+ S.map2 (mfc ctx rest,
+ fn rest' =>
+ (ECut (e', c', {field = field', rest = rest'}), loc)))))
+
+ | ECutMulti (e, c, {rest}) =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.map2 (mfc ctx rest,
+ fn rest' =>
+ (ECutMulti (e', c', {rest = rest'}), loc))))
+
+ | ECase (e, pes, {disc, result}) =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.bind2 (ListUtil.mapfold (fn (p, e) =>
+ let
+ fun pb ((p, _), ctx) =
+ case p of
+ PVar (x, t) => bind (ctx, RelE (x, t))
+ | PPrim _ => ctx
+ | PCon (_, _, _, NONE) => ctx
+ | PCon (_, _, _, SOME p) => pb (p, ctx)
+ | PRecord xps => foldl (fn ((_, p, _), ctx) =>
+ pb (p, ctx)) ctx xps
+ in
+ S.bind2 (mfp ctx p,
+ fn p' =>
+ S.map2 (mfe (pb (p', ctx)) e,
+ fn e' => (p', e')))
+ end) pes,
+ fn pes' =>
+ S.bind2 (mfc ctx disc,
+ fn disc' =>
+ S.map2 (mfc ctx result,
+ fn result' =>
+ (ECase (e', pes', {disc = disc', result = result'}), loc)))))
+
+ | EError => S.return2 eAll
+ | EUnif (ref (SOME e)) => mfe ctx e
+ | EUnif _ => S.return2 eAll
+
+ | ELet (des, e, t) =>
+ let
+ val (des, ctx') = foldl (fn (ed, (des, ctx)) =>
+ let
+ val ctx' =
+ case #1 ed of
+ EDVal (p, _, _) => doVars (p, ctx)
+ | EDValRec vis =>
+ foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t)))
+ ctx vis
+ in
+ (S.bind2 (des,
+ fn des' =>
+ S.map2 (mfed ctx ed,
+ fn ed' => ed' :: des')),
+ ctx')
+ end)
+ (S.return2 [], ctx) des
+ in
+ S.bind2 (des,
+ fn des' =>
+ S.bind2 (mfe ctx' e,
+ fn e' =>
+ S.map2 (mfc ctx t,
+ fn t' =>
+ (ELet (rev des', e', t'), loc))))
+ end
+
+ | EKAbs (x, e) =>
+ S.map2 (mfe (bind (ctx, RelK x)) e,
+ fn e' =>
+ (EKAbs (x, e'), loc))
+ | EKApp (e, k) =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.map2 (mfk ctx k,
+ fn k' =>
+ (EKApp (e', k'), loc)))
+
+ and mfp ctx (pAll as (p, loc)) =
+ case p of
+ PVar (x, t) =>
+ S.map2 (mfc ctx t,
+ fn t' =>
+ (PVar (x, t'), loc))
+ | PPrim _ => S.return2 pAll
+ | PCon (dk, pc, args, po) =>
+ S.bind2 (ListUtil.mapfold (mfc ctx) args,
+ fn args' =>
+ S.map2 ((case po of
+ NONE => S.return2 NONE
+ | SOME p => S.map2 (mfp ctx p, SOME)),
+ fn po' =>
+ (PCon (dk, pc, args', po'), loc)))
+ | PRecord xps =>
+ S.map2 (ListUtil.mapfold (fn (x, p, c) =>
+ S.bind2 (mfp ctx p,
+ fn p' =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (x, p', c')))) xps,
+ fn xps' =>
+ (PRecord xps', loc))
+
+ and mfed ctx (dAll as (d, loc)) =
+ case d of
+ EDVal (p, t, e) =>
+ S.bind2 (mfc ctx t,
+ fn t' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (EDVal (p, t', e'), loc)))
+ | EDValRec vis =>
+ let
+ val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
+ in
+ S.map2 (ListUtil.mapfold (mfvi ctx) vis,
+ fn vis' =>
+ (EDValRec vis', loc))
+ end
+
+ and mfvi ctx (x, c, e) =
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (x, c', e')))
+ in
+ mfe
+ end
+
+end
+
+structure Sgn = struct
+
+datatype binder =
+ RelK of string
+ | RelC of string * Elab.kind
+ | NamedC of string * int * Elab.kind * Elab.con option
+ | Str of string * int * Elab.sgn
+ | Sgn of string * int * Elab.sgn
+
+fun mapfoldB {kind, con, sgn_item, sgn, bind} =
+ let
+ fun bind' (ctx, b) =
+ let
+ val b' = case b of
+ Con.RelK x => RelK x
+ | Con.RelC x => RelC x
+ | Con.NamedC x => NamedC x
+ in
+ bind (ctx, b')
+ end
+ val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
+
+ val kind = Kind.mapfoldB {kind = kind, bind = fn (ctx, x) => bind (ctx, RelK x)}
+
+ fun sgi ctx si acc =
+ S.bindPWithPos (sgi' ctx si acc, sgn_item ctx)
+
+ and sgi' ctx (siAll as (si, loc)) =
+ case si of
+ SgiConAbs (x, n, k) =>
+ S.map2 (kind ctx k,
+ fn k' =>
+ (SgiConAbs (x, n, k'), loc))
+ | SgiCon (x, n, k, c) =>
+ S.bind2 (kind ctx k,
+ fn k' =>
+ S.map2 (con ctx c,
+ fn c' =>
+ (SgiCon (x, n, k', c'), loc)))
+ | SgiDatatype dts =>
+ S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
+ S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+ case c of
+ NONE => S.return2 (x, n, c)
+ | SOME c =>
+ S.map2 (con ctx c,
+ fn c' => (x, n, SOME c'))) xncs,
+ fn xncs' => (x, n, xs, xncs'))) dts,
+ fn dts' =>
+ (SgiDatatype dts', loc))
+ | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
+ S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+ case c of
+ NONE => S.return2 (x, n, c)
+ | SOME c =>
+ S.map2 (con ctx c,
+ fn c' => (x, n, SOME c'))) xncs,
+ fn xncs' =>
+ (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
+ | SgiVal (x, n, c) =>
+ S.map2 (con ctx c,
+ fn c' =>
+ (SgiVal (x, n, c'), loc))
+ | SgiStr (im, x, n, s) =>
+ S.map2 (sg ctx s,
+ fn s' =>
+ (SgiStr (im, x, n, s'), loc))
+ | SgiSgn (x, n, s) =>
+ S.map2 (sg ctx s,
+ fn s' =>
+ (SgiSgn (x, n, s'), loc))
+ | SgiConstraint (c1, c2) =>
+ S.bind2 (con ctx c1,
+ fn c1' =>
+ S.map2 (con ctx c2,
+ fn c2' =>
+ (SgiConstraint (c1', c2'), loc)))
+ | SgiClassAbs (x, n, k) =>
+ S.map2 (kind ctx k,
+ fn k' =>
+ (SgiClassAbs (x, n, k'), loc))
+ | SgiClass (x, n, k, c) =>
+ S.bind2 (kind ctx k,
+ fn k' =>
+ S.map2 (con ctx c,
+ fn c' =>
+ (SgiClass (x, n, k', c'), loc)))
+
+ and sg ctx s acc =
+ S.bindPWithPos (sg' ctx s acc, sgn ctx)
+
+ and sg' ctx (sAll as (s, loc)) =
+ case s of
+ SgnConst sgis =>
+ S.map2 (ListUtil.mapfoldB (fn (ctx, si) =>
+ (case #1 si of
+ SgiConAbs (x, n, k) =>
+ bind (ctx, NamedC (x, n, k, NONE))
+ | SgiCon (x, n, k, c) =>
+ bind (ctx, NamedC (x, n, k, SOME c))
+ | SgiDatatype dts =>
+ foldl (fn ((x, n, ks, _), ctx) =>
+ let
+ val k' = (KType, loc)
+ val k = foldl (fn (_, k) => (KArrow (k', k), loc))
+ k' ks
+ in
+ bind (ctx, NamedC (x, n, k, NONE))
+ end) ctx dts
+ | SgiDatatypeImp (x, n, m1, ms, s, _, _) =>
+ bind (ctx, NamedC (x, n, (KType, loc),
+ SOME (CModProj (m1, ms, s), loc)))
+ | SgiVal _ => ctx
+ | SgiStr (_, x, n, sgn) =>
+ bind (ctx, Str (x, n, sgn))
+ | SgiSgn (x, n, sgn) =>
+ bind (ctx, Sgn (x, n, sgn))
+ | SgiConstraint _ => ctx
+ | SgiClassAbs (x, n, k) =>
+ bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), NONE))
+ | SgiClass (x, n, k, c) =>
+ bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), SOME c)),
+ sgi ctx si)) ctx sgis,
+ fn sgis' =>
+ (SgnConst sgis', loc))
+
+ | SgnVar _ => S.return2 sAll
+ | SgnFun (m, n, s1, s2) =>
+ S.bind2 (sg ctx s1,
+ fn s1' =>
+ S.map2 (sg (bind (ctx, Str (m, n, s1'))) s2,
+ fn s2' =>
+ (SgnFun (m, n, s1', s2'), loc)))
+ | SgnProj _ => S.return2 sAll
+ | SgnWhere (sgn, ms, x, c) =>
+ S.bind2 (sg ctx sgn,
+ fn sgn' =>
+ S.map2 (con ctx c,
+ fn c' =>
+ (SgnWhere (sgn', ms, x, c'), loc)))
+ | SgnError => S.return2 sAll
+ in
+ sg
+ end
+
+end
+
+structure Decl = struct
+
+datatype binder =
+ RelK of string
+ | RelC of string * Elab.kind
+ | NamedC of string * int * Elab.kind * Elab.con option
+ | RelE of string * Elab.con
+ | NamedE of string * Elab.con
+ | Str of string * int * Elab.sgn
+ | Sgn of string * int * Elab.sgn
+
+fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} =
+ let
+ val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
+
+ fun bind' (ctx, b) =
+ let
+ val b' = case b of
+ Con.RelK x => RelK x
+ | Con.RelC x => RelC x
+ | Con.NamedC x => NamedC x
+ in
+ bind (ctx, b')
+ end
+ val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
+
+ fun bind' (ctx, b) =
+ let
+ val b' = case b of
+ Exp.RelK x => RelK x
+ | Exp.RelC x => RelC x
+ | Exp.NamedC x => NamedC x
+ | Exp.RelE x => RelE x
+ | Exp.NamedE x => NamedE x
+ in
+ bind (ctx, b')
+ end
+ val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind'}
+
+ fun bind' (ctx, b) =
+ let
+ val b' = case b of
+ Sgn.RelK x => RelK x
+ | Sgn.RelC x => RelC x
+ | Sgn.NamedC x => NamedC x
+ | Sgn.Sgn x => Sgn x
+ | Sgn.Str x => Str x
+ in
+ bind (ctx, b')
+ end
+ val mfsg = Sgn.mapfoldB {kind = fk, con = fc, sgn_item = fsgi, sgn = fsg, bind = bind'}
+
+ fun mfst ctx str acc =
+ S.bindPWithPos (mfst' ctx str acc, fst ctx)
+
+ and mfst' ctx (strAll as (str, loc)) =
+ case str of
+ StrConst ds =>
+ S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
+ (case #1 d of
+ DCon (x, n, k, c) =>
+ bind (ctx, NamedC (x, n, k, SOME c))
+ | DDatatype dts =>
+ let
+ fun doOne ((x, n, xs, xncs), ctx) =
+ let
+ val ctx = bind (ctx, NamedC (x, n, (KType, loc), NONE))
+ in
+ foldl (fn ((x, _, co), ctx) =>
+ let
+ val t =
+ case co of
+ NONE => CNamed n
+ | SOME t => TFun (t, (CNamed n, loc))
+
+ val k = (KType, loc)
+ val t = (t, loc)
+ val t = foldr (fn (x, t) =>
+ (TCFun (Explicit,
+ x,
+ k,
+ t), loc))
+ t xs
+ in
+ bind (ctx, NamedE (x, t))
+ end)
+ ctx xncs
+ end
+ in
+ foldl doOne ctx dts
+ end
+ | DDatatypeImp (x, n, m, ms, x', _, _) =>
+ bind (ctx, NamedC (x, n, (KType, loc),
+ SOME (CModProj (m, ms, x'), loc)))
+ | DVal (x, _, c, _) =>
+ bind (ctx, NamedE (x, c))
+ | DValRec vis =>
+ foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis
+ | DSgn (x, n, sgn) =>
+ bind (ctx, Sgn (x, n, sgn))
+ | DStr (x, n, sgn, _) =>
+ bind (ctx, Str (x, n, sgn))
+ | DFfiStr (x, n, sgn) =>
+ bind (ctx, Str (x, n, sgn))
+ | DConstraint _ => ctx
+ | DExport _ => ctx
+ | DTable (tn, x, n, c, _, pc, _, cc) =>
+ let
+ val ct = (CModProj (n, [], "sql_table"), loc)
+ val ct = (CApp (ct, c), loc)
+ val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
+ in
+ bind (ctx, NamedE (x, ct))
+ end
+ | DSequence (tn, x, n) =>
+ bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc)))
+ | DView (tn, x, n, _, c) =>
+ let
+ val ct = (CModProj (n, [], "sql_view"), loc)
+ val ct = (CApp (ct, c), loc)
+ in
+ bind (ctx, NamedE (x, ct))
+ end
+ | DDatabase _ => ctx
+ | DCookie (tn, x, n, c) =>
+ bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc),
+ c), loc)))
+ | DStyle (tn, x, n) =>
+ bind (ctx, NamedE (x, (CModProj (n, [], "css_class"), loc)))
+ | DTask _ => ctx
+ | DPolicy _ => ctx
+ | DOnError _ => ctx
+ | DFfi (x, _, _, t) => bind (ctx, NamedE (x, t)),
+ mfd ctx d)) ctx ds,
+ fn ds' => (StrConst ds', loc))
+ | StrVar _ => S.return2 strAll
+ | StrProj (str, x) =>
+ S.map2 (mfst ctx str,
+ fn str' =>
+ (StrProj (str', x), loc))
+ | StrFun (x, n, sgn1, sgn2, str) =>
+ S.bind2 (mfsg ctx sgn1,
+ fn sgn1' =>
+ S.bind2 (mfsg ctx sgn2,
+ fn sgn2' =>
+ S.map2 (mfst ctx str,
+ fn str' =>
+ (StrFun (x, n, sgn1', sgn2', str'), loc))))
+ | StrApp (str1, str2) =>
+ S.bind2 (mfst ctx str1,
+ fn str1' =>
+ S.map2 (mfst ctx str2,
+ fn str2' =>
+ (StrApp (str1', str2'), loc)))
+ | StrError => S.return2 strAll
+
+ and mfd ctx d acc =
+ S.bindPWithPos (mfd' ctx d acc, fd ctx)
+
+ and mfd' ctx (dAll as (d, loc)) =
+ case d of
+ DCon (x, n, k, c) =>
+ S.bind2 (mfk ctx k,
+ fn k' =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (DCon (x, n, k', c'), loc)))
+ | DDatatype dts =>
+ S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
+ S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+ case c of
+ NONE => S.return2 (x, n, c)
+ | SOME c =>
+ S.map2 (mfc ctx c,
+ fn c' => (x, n, SOME c'))) xncs,
+ fn xncs' =>
+ (x, n, xs, xncs'))) dts,
+ fn dts' =>
+ (DDatatype dts', loc))
+ | DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
+ S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+ case c of
+ NONE => S.return2 (x, n, c)
+ | SOME c =>
+ S.map2 (mfc ctx c,
+ fn c' => (x, n, SOME c'))) xncs,
+ fn xncs' =>
+ (DDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
+ | DVal vi =>
+ S.map2 (mfvi ctx vi,
+ fn vi' =>
+ (DVal vi', loc))
+ | DValRec vis =>
+ S.map2 (ListUtil.mapfold (mfvi ctx) vis,
+ fn vis' =>
+ (DValRec vis', loc))
+ | DSgn (x, n, sgn) =>
+ S.map2 (mfsg ctx sgn,
+ fn sgn' =>
+ (DSgn (x, n, sgn'), loc))
+ | DStr (x, n, sgn, str) =>
+ S.bind2 (mfsg ctx sgn,
+ fn sgn' =>
+ S.map2 (mfst ctx str,
+ fn str' =>
+ (DStr (x, n, sgn', str'), loc)))
+ | DFfiStr (x, n, sgn) =>
+ S.map2 (mfsg ctx sgn,
+ fn sgn' =>
+ (DFfiStr (x, n, sgn'), loc))
+ | DConstraint (c1, c2) =>
+ S.bind2 (mfc ctx c1,
+ fn c1' =>
+ S.map2 (mfc ctx c2,
+ fn c2' =>
+ (DConstraint (c1', c2'), loc)))
+ | DExport (en, sgn, str) =>
+ S.bind2 (mfsg ctx sgn,
+ fn sgn' =>
+ S.map2 (mfst ctx str,
+ fn str' =>
+ (DExport (en, sgn', str'), loc)))
+
+ | DTable (tn, x, n, c, pe, pc, ce, cc) =>
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.bind2 (mfe ctx pe,
+ fn pe' =>
+ S.bind2 (mfc ctx pc,
+ fn pc' =>
+ S.bind2 (mfe ctx ce,
+ fn ce' =>
+ S.map2 (mfc ctx cc,
+ fn cc' =>
+ (DTable (tn, x, n, c', pe', pc', ce', cc'), loc))))))
+ | DSequence _ => S.return2 dAll
+ | DView (tn, x, n, e, c) =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (DView (tn, x, n, e', c'), loc)))
+
+ | DDatabase _ => S.return2 dAll
+
+ | DCookie (tn, x, n, c) =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (DCookie (tn, x, n, c'), loc))
+ | DStyle _ => S.return2 dAll
+ | DTask (e1, e2) =>
+ S.bind2 (mfe ctx e1,
+ fn e1' =>
+ S.map2 (mfe ctx e2,
+ fn e2' =>
+ (DTask (e1', e2'), loc)))
+ | DPolicy e1 =>
+ S.map2 (mfe ctx e1,
+ fn e1' =>
+ (DPolicy e1', loc))
+ | DOnError _ => S.return2 dAll
+ | DFfi (x, n, modes, t) =>
+ S.map2 (mfc ctx t,
+ fn t' =>
+ (DFfi (x, n, modes, t'), loc))
+
+ and mfvi ctx (x, n, c, e) =
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (x, n, c', e')))
+ in
+ mfd
+ end
+
+ fun fold {kind, con, exp, sgn_item, sgn, str, decl} (st : 'a) d : 'a =
+ case mapfoldB {kind = fn () => fn k => fn st => S.Continue (#1 k, kind (k, st)),
+ con = fn () => fn c => fn st => S.Continue (#1 c, con (c, st)),
+ exp = fn () => fn e => fn st => S.Continue (#1 e, exp (e, st)),
+ sgn_item = fn () => fn sgi => fn st => S.Continue (#1 sgi, sgn_item (sgi, st)),
+ sgn = fn () => fn s => fn st => S.Continue (#1 s, sgn (s, st)),
+ str = fn () => fn str' => fn st => S.Continue (#1 str', str (str', st)),
+ decl = fn () => fn d => fn st => S.Continue (#1 d, decl (d, st)),
+ bind = fn ((), _) => ()
+ } () d st of
+ S.Continue (_, st) => st
+ | S.Return _ => raise Fail "ElabUtil.Decl.fold: Impossible"
+
+ fun foldB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx (st : 'a) d : 'a =
+ case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (#1 k, kind (ctx, k, st)),
+ con = fn ctx => fn c => fn st => S.Continue (#1 c, con (ctx, c, st)),
+ exp = fn ctx => fn e => fn st => S.Continue (#1 e, exp (ctx, e, st)),
+ sgn_item = fn ctx => fn sgi => fn st => S.Continue (#1 sgi, sgn_item (ctx, sgi, st)),
+ sgn = fn ctx => fn s => fn st => S.Continue (#1 s, sgn (ctx, s, st)),
+ str = fn ctx => fn str' => fn st => S.Continue (#1 str', str (ctx, str', st)),
+ decl = fn ctx => fn d => fn st => S.Continue (#1 d, decl (ctx, d, st)),
+ bind = bind
+ } ctx d st of
+ S.Continue (_, st) => st
+ | S.Return _ => raise Fail "ElabUtil.Decl.foldB: Impossible"
+ end
+end
diff --git a/src/elaborate.sig b/src/elaborate.sig
index d60cff42..d6747241 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -29,7 +29,10 @@ signature ELABORATE = sig
val elabFile : Source.sgn_item list -> Time.time
-> Source.decl list -> Source.sgn_item list -> Time.time
- -> ElabEnv.env -> Source.file -> Elab.file
+ -> ElabEnv.env
+ -> (ElabEnv.env -> ElabEnv.env) (* Adapt env after stdlib but before elaborate *)
+ -> Source.file
+ -> Elab.file
val resolveClass : ElabEnv.env -> Elab.con -> Elab.exp option
@@ -47,4 +50,24 @@ signature ELABORATE = sig
val incremental : bool ref
val verbose : bool ref
+ val dopen: ElabEnv.env
+ -> { str: int
+ , strs: string list
+ , sgn: Elab.sgn }
+ -> (Elab.decl list * ElabEnv.env)
+
+ val elabSgn: (ElabEnv.env * Disjoint.env)
+ -> Source.sgn
+ -> (Elab.sgn * Disjoint.goal list)
+
+ datatype constraint =
+ Disjoint of Disjoint.goal
+ | TypeClass of ElabEnv.env * Elab.con * Elab.exp option ref * ErrorMsg.span
+
+ val elabStr: (ElabEnv.env * Disjoint.env)
+ -> Source.str
+ -> (Elab.str * Elab.sgn * constraint list)
+
+ val subSgn: ElabEnv.env -> ErrorMsg.span -> Elab.sgn -> Elab.sgn -> unit
+
end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 9718ccad..85234775 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2822,7 +2822,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, []))
end)
-and elabSgn (env, denv) (sgn, loc) =
+and elabSgn (env, denv) (sgn, loc): (L'.sgn * D.goal list) =
case sgn of
L.SgnConst sgis =>
let
@@ -4187,6 +4187,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
| NONE =>
let
val () = if !verbose then TextIO.print ("CHECK: " ^ x ^ "\n") else ()
+ val () = ErrorMsg.startElabStructure x
val () = if x = "Basis" then
raise Fail "Not allowed to redefine structure 'Basis'"
@@ -4228,7 +4229,10 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
L'.StrFun _ => ()
| _ => strError env (FunctorRebind loc))
| _ => ();
- Option.map (fn tm => ModDb.insert (dNew, tm)) tmo;
+ Option.map (fn tm => ModDb.insert (dNew,
+ tm,
+ ErrorMsg.stopElabStructureAndGetErrored x
+ )) tmo;
([dNew], (env', denv', gs' @ gs))
end)
@@ -4243,6 +4247,8 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
end
| NONE =>
let
+ val () = ErrorMsg.startElabStructure x
+
val (sgn', gs') = enterSignature (fn () => elabSgn (env, denv) sgn)
val (env', n) = E.pushStrNamed env x sgn'
@@ -4261,7 +4267,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
epreface ("item", p_sgn_item env sgi)))
| _ => raise Fail "FFI signature isn't SgnConst";
- Option.map (fn tm => ModDb.insert (dNew, tm)) tmo;
+ Option.map (fn tm => ModDb.insert (dNew, tm, ErrorMsg.stopElabStructureAndGetErrored x)) tmo;
([dNew], (env', denv, enD gs' @ gs))
end)
@@ -4754,9 +4760,11 @@ and elabStr (env, denv) (str, loc) =
fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env
-fun elabFile basis basis_tm topStr topSgn top_tm env file =
+fun elabFile basis basis_tm topStr topSgn top_tm env changeEnv file =
let
val () = ModDb.snapshot ()
+ val () = ErrorMsg.resetStructureTracker ()
+
val () = mayDelay := true
val () = delayedUnifs := []
@@ -4779,7 +4787,7 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
val (env', basis_n) = E.pushStrNamed env "Basis" sgn
in
- ModDb.insert ((L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan), basis_tm);
+ ModDb.insert ((L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan), basis_tm, false); (* TODO: also check for errors? *)
(basis_n, env', sgn)
end
| SOME (d' as (L'.DFfiStr (_, basis_n, sgn), _)) =>
@@ -4838,7 +4846,7 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
val (env', top_n) = E.pushStrNamed env' "Top" topSgn
in
- ModDb.insert ((L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan), top_tm);
+ ModDb.insert ((L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan), top_tm, false); (* TODO: also check for errors? *)
(top_n, env', topSgn, topStr)
end
| SOME (d' as (L'.DStr (_, top_n, topSgn, topStr), _)) =>
@@ -4849,6 +4857,8 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}
+ val env' = changeEnv env'
+
fun elabDecl' x =
(resetKunif ();
resetCunif ();
@@ -5121,11 +5131,6 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
else
();
- if ErrorMsg.anyErrors () then
- ModDb.revert ()
- else
- ();
-
(*Print.preface("File", ElabPrint.p_file env file);*)
(L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
diff --git a/src/elisp/urweb-mode.el b/src/elisp/urweb-mode.el
index 69b0e23c..057761ac 100644
--- a/src/elisp/urweb-mode.el
+++ b/src/elisp/urweb-mode.el
@@ -925,6 +925,33 @@ Optional argument STYLE is currently ignored."
(urweb-skip-siblings))
fullname)))
+(defun urweb-get-proj-dir (bfn)
+ (locate-dominating-file
+ bfn
+ (lambda (dir)
+ (some (lambda (f) (s-suffix? ".urp" f))
+ (if (f-dir? dir)
+ (directory-files dir)
+ (list '(dir)))))))
+
+(defun urweb-get-info ()
+ (interactive)
+ (let*
+ ((row (line-number-at-pos))
+ (col (evil-column))
+ (bfn (buffer-file-name))
+ (proj-dir (urweb-get-proj-dir bfn))
+ (filename (file-relative-name bfn proj-dir))
+ (loc (concat filename ":" (number-to-string row) ":" (number-to-string col)))
+ )
+ (require 's)
+ (require 'f)
+ (require 'simple)
+ (message (let
+ ((default-directory proj-dir))
+ (shell-command-to-string (concat "urweb -getInfo " loc)))))
+ )
+
(provide 'urweb-mode)
;;; urweb-mode.el ends here
diff --git a/src/errormsg.sig b/src/errormsg.sig
index 92425842..1fa4013c 100644
--- a/src/errormsg.sig
+++ b/src/errormsg.sig
@@ -48,9 +48,17 @@ signature ERROR_MSG = sig
val posOf : int -> pos
val spanOf : int * int -> span
+ (* To monitor in which modules the elaboration phase finds errors *)
+ val startElabStructure : string -> unit
+ val stopElabStructureAndGetErrored : string -> bool (* Did the module elab encounter errors? *)
+
+ val resetStructureTracker: unit -> unit
val resetErrors : unit -> unit
val anyErrors : unit -> bool
val error : string -> unit
val errorAt : span -> string -> unit
val errorAt' : int * int -> string -> unit
+ val readErrorLog: unit ->
+ { span: span
+ , message: string } list
end
diff --git a/src/errormsg.sml b/src/errormsg.sml
index 8f3c93b1..d40789ed 100644
--- a/src/errormsg.sml
+++ b/src/errormsg.sml
@@ -88,12 +88,34 @@ fun spanOf (pos1, pos2) = {file = !file,
val errors = ref false
+val errorLog = ref ([]: { span: span
+ , message: string } list)
+fun readErrorLog () = !errorLog
+val structuresCurrentlyElaborating: ((string * bool) list) ref = ref nil
+
+fun startElabStructure s =
+ structuresCurrentlyElaborating := ((s, false) :: !structuresCurrentlyElaborating)
+fun stopElabStructureAndGetErrored s =
+ let
+ val errored =
+ case List.find (fn x => #1 x = s) (!structuresCurrentlyElaborating) of
+ NONE => false
+ | SOME tup => #2 tup
+ val () = structuresCurrentlyElaborating :=
+ (List.filter (fn x => #1 x <> s) (!structuresCurrentlyElaborating))
+ in
+ errored
+ end
+fun resetStructureTracker () =
+ structuresCurrentlyElaborating := []
-fun resetErrors () = errors := false
+fun resetErrors () = (errors := false; errorLog := [])
fun anyErrors () = !errors
fun error s = (TextIO.output (TextIO.stdErr, s);
TextIO.output1 (TextIO.stdErr, #"\n");
- errors := true)
+ errors := true;
+ structuresCurrentlyElaborating :=
+ List.map (fn (s, e) => (s, true)) (!structuresCurrentlyElaborating))
fun errorAt (span : span) s = (TextIO.output (TextIO.stdErr, #file span);
TextIO.output (TextIO.stdErr, ":");
@@ -101,6 +123,9 @@ fun errorAt (span : span) s = (TextIO.output (TextIO.stdErr, #file span);
TextIO.output (TextIO.stdErr, ": (to ");
TextIO.output (TextIO.stdErr, posToString (#last span));
TextIO.output (TextIO.stdErr, ") ");
+ errorLog := ({ span = span
+ , message = s
+ } :: !errorLog);
error s)
fun errorAt' span s = errorAt (spanOf span) s
diff --git a/src/fromjson.sig b/src/fromjson.sig
new file mode 100644
index 00000000..3fdc1a89
--- /dev/null
+++ b/src/fromjson.sig
@@ -0,0 +1,8 @@
+signature FROMJSON = sig
+ val getO: string -> Json.json -> Json.json option
+ val get: string -> Json.json -> Json.json
+ val asInt: Json.json -> int
+ val asString: Json.json -> string
+ val asOptionalInt: Json.json -> int option
+ val asOptionalString: Json.json -> string option
+end
diff --git a/src/fromjson.sml b/src/fromjson.sml
new file mode 100644
index 00000000..6a9bd71b
--- /dev/null
+++ b/src/fromjson.sml
@@ -0,0 +1,35 @@
+structure FromJson :> FROMJSON = struct
+fun getO (s: string) (l: Json.json): Json.json option =
+ case l of
+ Json.Obj pairs =>
+ (case List.find (fn tup => #1 tup = s) pairs of
+ NONE => NONE
+ | SOME tup => SOME (#2 tup))
+ | _ => raise Fail ("Expected JSON object, got: " ^ Json.print l)
+fun get (s: string) (l: Json.json): Json.json =
+ (case getO s l of
+ NONE => raise Fail ("Failed to find JSON object key " ^ s ^ " in " ^ Json.print l)
+ | SOME a => a)
+
+fun asInt (j: Json.json): int =
+ case j of
+ Json.Int i => i
+ | _ => raise Fail ("Expected JSON int, got: " ^ Json.print j)
+
+fun asString (j: Json.json): string =
+ case j of
+ Json.String s => s
+ | _ => raise Fail ("Expected JSON string, got: " ^ Json.print j)
+
+fun asOptionalInt (j: Json.json): int option =
+ case j of
+ Json.Null => NONE
+ | Json.Int i => SOME i
+ | _ => raise Fail ("Expected JSON int or null, got: " ^ Json.print j)
+
+fun asOptionalString (j: Json.json): string option =
+ case j of
+ Json.Null => NONE
+ | Json.String s => SOME s
+ | _ => raise Fail ("Expected JSON string or null, got: " ^ Json.print j)
+end
diff --git a/src/getinfo.sig b/src/getinfo.sig
new file mode 100644
index 00000000..63850ef2
--- /dev/null
+++ b/src/getinfo.sig
@@ -0,0 +1,50 @@
+(* Copyright (c) 2012, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ * this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ * this list of conditions and the following disclaimer in the documentation
+ * and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ * derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * 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
+ * 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
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+signature GET_INFO = sig
+
+ datatype foundInEnv = FoundStr of (string * Elab.sgn)
+ | FoundKind of (string * Elab.kind)
+ | FoundCon of (string * Elab.con)
+
+ val findStringInEnv:
+ ElabEnv.env ->
+ Elab.str' ->
+ string (* fileName *) ->
+ {line: int, char: int} ->
+ string (* query *) ->
+ (ElabEnv.env * string (* prefix *) * foundInEnv option)
+
+ val matchStringInEnv:
+ ElabEnv.env ->
+ Elab.str' ->
+ string (* fileName *) ->
+ {line: int, char: int} ->
+ string (* query *) ->
+ (ElabEnv.env * string (* prefix *) * foundInEnv list)
+end
+
diff --git a/src/getinfo.sml b/src/getinfo.sml
new file mode 100644
index 00000000..2b27b8df
--- /dev/null
+++ b/src/getinfo.sml
@@ -0,0 +1,304 @@
+(* Copyright (c) 2012, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ * this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ * this list of conditions and the following disclaimer in the documentation
+ * and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ * derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * 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
+ * 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
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+structure GetInfo :> GET_INFO = struct
+
+structure U = ElabUtilPos
+structure E = ElabEnv
+structure L = Elab
+
+fun isPosIn (file: string) (line: int) (char: int) (span: ErrorMsg.span) =
+ let
+ val start = #first span
+ val end_ = #last span
+ in
+ OS.Path.base file = OS.Path.base (#file span)
+ andalso
+ (#line start < line orelse
+ #line start = line andalso #char start <= char)
+ andalso
+ (#line end_ > line orelse
+ #line end_ = line andalso #char end_ >= char)
+ end
+
+fun isSmallerThan (s1: ErrorMsg.span) (s2: ErrorMsg.span) =
+ (#line (#first s1) > #line (#first s2) orelse
+ (#line (#first s1) = #line (#first s2) andalso (#char (#first s1) >= #char (#first s2))))
+ andalso
+ (#line (#last s1) < #line (#last s2) orelse
+ (#line (#last s1) = #line (#last s2) andalso (#char (#last s1) <= #char (#last s2))))
+
+datatype item =
+ Kind of L.kind
+ | Con of L.con
+ | Exp of L.exp
+ | Sgn_item of L.sgn_item
+ | Sgn of L.sgn
+ | Str of L.str
+ | Decl of L.decl
+
+fun getSpan (f: item) =
+ case f of
+ Kind k => #2 k
+ | Con c => #2 c
+ | Exp e => #2 e
+ | Sgn_item si => #2 si
+ | Sgn s => #2 s
+ | Str s => #2 s
+ | Decl d => #2 d
+
+
+fun findInStr (f: ElabEnv.env -> item (* curr *) -> item (* prev *) -> bool)
+ (init: item)
+ env str fileName {line = line, char = char}: {item: item, env: ElabEnv.env} =
+ let
+ val () = U.mliftConInCon := E.mliftConInCon
+ val {env: ElabEnv.env, found: Elab.decl option} =
+ (case str of
+ L.StrConst decls =>
+ List.foldl (fn (d, acc as {env, found}) =>
+ if #line (#last (#2 d)) < line
+ then {env = E.declBinds env d, found = found}
+ else
+ if #line (#first (#2 d)) <= line andalso line <= #line (#last (#2 d))
+ then {env = env, found = SOME d}
+ else {env = env, found = found})
+ {env = env, found = NONE} decls
+ | _ => { env = env, found = NONE })
+ val dummyResult = (init, env)
+ val result =
+ case found of
+ NONE => dummyResult
+ | SOME d =>
+ U.Decl.foldB
+ { kind = fn (env, i, acc as (prev, env')) => if f env (Kind i) prev then (Kind i, env) else acc,
+ con = fn (env, i, acc as (prev, env')) => if f env (Con i) prev then (Con i, env) else acc,
+ exp = fn (env, i, acc as (prev, env')) => if f env (Exp i) prev then (Exp i, env) else acc,
+ sgn_item = fn (env, i, acc as (prev, env')) => if f env (Sgn_item i) prev then (Sgn_item i, env) else acc,
+ sgn = fn (env, i, acc as (prev, env')) => if f env (Sgn i) prev then (Sgn i, env) else acc,
+ str = fn (env, i, acc as (prev, env')) => if f env (Str i) prev then (Str i, env) else acc,
+ decl = fn (env, i, acc as (prev, env')) => if f env (Decl i) prev then (Decl i, env) else acc,
+ bind = fn (env, binder) =>
+ case binder of
+ U.Decl.RelK x => E.pushKRel env x
+ | U.Decl.RelC (x, k) => E.pushCRel env x k
+ | U.Decl.NamedC (x, n, k, co) => E.pushCNamedAs env x n k co
+ | U.Decl.RelE (x, c) => E.pushERel env x c
+ | U.Decl.NamedE (x, c) => #1 (E.pushENamed env x c)
+ | U.Decl.Str (x, n, sgn) => #1 (E.pushStrNamed env x sgn)
+ | U.Decl.Sgn (x, n, sgn) => #1 (E.pushSgnNamed env x sgn)
+ }
+ env dummyResult d
+ in
+ {item = #1 result, env = #2 result}
+ end
+
+fun findClosestSpan env str fileName {line = line, char = char} =
+ let
+ fun getDistance (i: item): int =
+ let
+ val {first, last, file} = getSpan i
+ in
+ Int.abs (#char first - char)
+ + Int.abs (#char last - char)
+ + Int.abs (#line first - line) * 25
+ + Int.abs (#line last - line) * 25
+ end
+ fun isCloser (env: ElabEnv.env) (curr: item) (prev: item) =
+ getDistance curr < getDistance prev
+ val init = Str (str, { file = fileName
+ , first = { line = 0, char = 0}
+ , last = { line = 0, char = 0} })
+ in
+ findInStr isCloser init env str fileName {line = line, char = char}
+ end
+
+fun findFirstExpAfter env str fileName {line = line, char = char} =
+ let
+ fun currIsAfterPosAndBeforePrev (env: ElabEnv.env) (curr: item) (prev: item) =
+ (* curr is an exp *)
+ (case curr of Exp _ => true | _ => false)
+ andalso
+ (* curr is after input pos *)
+ ( line < #line (#first (getSpan curr))
+ orelse ( line = #line (#first (getSpan curr))
+ andalso char < #char (#first (getSpan curr))))
+ andalso
+ (* curr is before prev *)
+ (#line (#first (getSpan curr)) < #line (#first (getSpan prev))
+ orelse
+ (#line (#first (getSpan curr)) = #line (#first (getSpan prev))
+ andalso #char (#first (getSpan curr)) < #char (#first (getSpan prev))))
+ val init = Exp (Elab.EPrim (Prim.Int 0),
+ { file = fileName
+ , first = { line = Option.getOpt (Int.maxInt, 99999), char = Option.getOpt (Int.maxInt, 99999)}
+ , last = { line = Option.getOpt (Int.maxInt, 99999), char = Option.getOpt (Int.maxInt, 99999)} })
+ in
+ findInStr currIsAfterPosAndBeforePrev init env str fileName {line = line, char = char}
+ end
+
+
+datatype foundInEnv = FoundStr of (string * Elab.sgn)
+ | FoundKind of (string * Elab.kind)
+ | FoundCon of (string * Elab.con)
+
+fun getNameOfFoundInEnv (f: foundInEnv) =
+ case f of
+ FoundStr (x, _) => x
+ | FoundKind (x, _) => x
+ | FoundCon (x, _) => x
+
+fun filterSgiItems (items: Elab.sgn_item list) : foundInEnv list =
+ let
+ fun processDatatype loc (dtx, i, ks, cs) =
+ let
+ val k' = (Elab.KType, loc)
+ val k = FoundKind (dtx, foldl (fn (_, k) => (Elab.KArrow (k', k), loc)) k' ks)
+ val foundCs = List.map (fn (x, j, co) =>
+ let
+ val c = case co of
+ NONE => (Elab.CNamed i, loc)
+ | SOME c => (Elab.TFun (c, (Elab.CNamed i, loc)), loc)
+ in
+ FoundCon (x, c)
+ end) cs
+ in
+ k :: foundCs
+ end
+ fun mapF item =
+ case item of
+ (Elab.SgiVal (name, _, c), _) => [FoundCon (name, c)]
+ | (Elab.SgiCon (name, _, k, _), _) => [FoundKind (name, k)]
+ | (Elab.SgiDatatype ds, loc) =>
+ List.concat (List.map (processDatatype loc) ds)
+ | (Elab.SgiDatatypeImp (dtx, i, _, ks, _, _, cs), loc) => processDatatype loc (dtx, i, ks, cs)
+ | (Elab.SgiStr (_, name, _, sgn), _) =>
+ [FoundStr (name, sgn)]
+ | (Elab.SgiSgn (name, _, sgn), _) => []
+ | _ => []
+ in
+ List.concat (List.map mapF items)
+ end
+
+fun resolvePrefixes
+ (env: ElabEnv.env)
+ (prefixes: string list)
+ (items : foundInEnv list)
+ : foundInEnv list
+ =
+ case prefixes of
+ [] => items
+ | first :: rest =>
+ (case List.find (fn item => getNameOfFoundInEnv item = first) items of
+ NONE => []
+ | SOME (FoundStr (name, sgn)) => (case ElabEnv.hnormSgn env sgn of
+ (Elab.SgnConst sgis, _) => resolvePrefixes env rest (filterSgiItems sgis)
+ | _ => [])
+ | SOME (FoundCon (name, c)) =>
+ let
+ val fields = case ElabOps.reduceCon env c of
+ (Elab.TRecord (Elab.CRecord (_, fields), l2_), l1_) =>
+ fields
+ | ( ( Elab.CApp
+ ( ( (Elab.CApp
+ ( ( Elab.CModProj (_, _, "sql_table") , l4_)
+ , ( Elab.CRecord (_, fields) , l3_)))
+ , l2_)
+ , _))
+ , l1_) => fields
+ | _ => []
+ val items =
+ List.mapPartial (fn (c1, c2) => case c1 of
+ (Elab.CName fieldName, _) => SOME (FoundCon (fieldName, c2))
+ | _ => NONE) fields
+ in
+ resolvePrefixes env rest items
+ end
+ | SOME (FoundKind (_, _)) => [])
+
+
+fun findStringInEnv' (env: ElabEnv.env) (preferCon: bool) (str: string): (string (* prefix *) * foundInEnv option) =
+ let
+ val splitted = List.map Substring.string (Substring.fields (fn c => c = #".") (Substring.full str))
+ val afterResolve = resolvePrefixes env (List.take (splitted, List.length splitted - 1))
+ ( List.map (fn (name, (_, sgn)) => FoundStr (name, sgn)) (ElabEnv.dumpStrs env)
+ @ List.map FoundKind (ElabEnv.dumpCs env)
+ @ List.map FoundCon (ElabEnv.dumpEs env))
+ val query = List.last splitted
+ val prefix = String.extract (str, 0, SOME (String.size str - String.size query))
+ in
+ (prefix, List.find (fn i => getNameOfFoundInEnv i = query) afterResolve)
+ end
+
+fun matchStringInEnv' (env: ElabEnv.env) (str: string): (string (* prefix *) * foundInEnv list) =
+ let
+ val splitted = List.map Substring.string (Substring.fields (fn c => c = #".") (Substring.full str))
+ val afterResolve = resolvePrefixes env (List.take (splitted, List.length splitted - 1))
+ ( List.map (fn (name, (_, sgn)) => FoundStr (name, sgn)) (ElabEnv.dumpStrs env)
+ @ List.map FoundKind (ElabEnv.dumpCs env)
+ @ List.map FoundCon (ElabEnv.dumpEs env))
+ val query = List.last splitted
+ val prefix = String.extract (str, 0, SOME (String.size str - String.size query))
+ in
+ (prefix, List.filter (fn i => String.isPrefix query (getNameOfFoundInEnv i)) afterResolve)
+ end
+
+fun getDesc item =
+ case item of
+ Kind (_, s) => "Kind " ^ ErrorMsg.spanToString s
+ | Con (_, s) => "Con " ^ ErrorMsg.spanToString s
+ | Exp (_, s) => "Exp " ^ ErrorMsg.spanToString s
+ | Sgn_item (_, s) => "Sgn_item " ^ ErrorMsg.spanToString s
+ | Sgn (_, s) => "Sgn " ^ ErrorMsg.spanToString s
+ | Str (_, s) => "Str " ^ ErrorMsg.spanToString s
+ | Decl (_, s) => "Decl " ^ ErrorMsg.spanToString s
+
+fun matchStringInEnv env str fileName pos query: (ElabEnv.env * string (* prefix *) * foundInEnv list) =
+ let
+ val {item = _, env} = findClosestSpan env str fileName pos
+ val (prefix, matches) = matchStringInEnv' env query
+ in
+ (env, prefix, matches)
+ end
+
+fun findStringInEnv env str fileName pos (query: string): (ElabEnv.env * string (* prefix *) * foundInEnv option) =
+ let
+ val {item, env} = findClosestSpan env str fileName pos
+ val env = case item of
+ Exp (L.ECase _, _) => #env (findFirstExpAfter env str fileName pos)
+ | Exp (L.ELet _, _) => #env (findFirstExpAfter env str fileName pos)
+ | Exp (L.EAbs _, _) => #env (findFirstExpAfter env str fileName pos)
+ | Exp e => env
+ | Con _ => #env (findFirstExpAfter env str fileName pos)
+ | _ => #env (findFirstExpAfter env str fileName pos)
+ val preferCon = case item of Con _ => true
+ | _ => false
+ val (prefix, found) = findStringInEnv' env preferCon query
+ in
+ (env, prefix, found)
+ end
+end
diff --git a/src/json.sig b/src/json.sig
new file mode 100644
index 00000000..f92ef495
--- /dev/null
+++ b/src/json.sig
@@ -0,0 +1,13 @@
+signature JSON = sig
+ datatype json =
+ Array of json list
+ | Null
+ | Float of real
+ | String of string
+ | Bool of bool
+ | Int of int
+ | Obj of (string * json) list
+
+ val parse: string -> json
+ val print: json -> string
+end
diff --git a/src/json.sml b/src/json.sml
new file mode 100644
index 00000000..81d7b8b4
--- /dev/null
+++ b/src/json.sml
@@ -0,0 +1,293 @@
+(*******************************************************************************
+* Standard ML JSON parser
+* Copyright (C) 2010 Gian Perrone
+*
+* This program is free software: you can redistribute it and/or modify
+* it under the terms of the GNU General Public License as published by
+* the Free Software Foundation, either version 3 of the License, or
+* (at your option) any later version.
+*
+* This program is distributed in the hope that it will be useful,
+* but WITHOUT ANY WARRANTY; without even the implied warranty of
+* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+* GNU General Public License for more details.
+*
+* You should have received a copy of the GNU General Public License
+* along with this program. If not, see <http://www.gnu.org/licenses/>.
+******************************************************************************)
+
+signature JSON_CALLBACKS =
+sig
+ type json_data
+
+ val json_object : json_data list -> json_data
+ val json_pair : string * json_data -> json_data
+ val json_array : json_data list -> json_data
+ val json_value : json_data -> json_data
+ val json_string : string -> json_data
+ val json_int : int -> json_data
+ val json_real : real -> json_data
+ val json_bool : bool -> json_data
+ val json_null : unit -> json_data
+
+ val error_handle : string * int * string -> json_data
+end
+
+functor JSONParser (Callbacks : JSON_CALLBACKS) =
+struct
+ type json_data = Callbacks.json_data
+
+ exception JSONParseError of string * int
+
+ val inputData = ref ""
+ val inputPosition = ref 0
+
+ fun isDigit () = Char.isDigit (String.sub (!inputData,0))
+
+ fun ws () = while (String.isPrefix " " (!inputData) orelse
+ String.isPrefix "\n" (!inputData) orelse
+ String.isPrefix "\t" (!inputData) orelse
+ String.isPrefix "\r" (!inputData))
+ do (inputData := String.extract (!inputData, 1, NONE))
+
+ fun peek () = String.sub (!inputData,0)
+ fun take () =
+ String.sub (!inputData,0) before
+ inputData := String.extract (!inputData, 1, NONE)
+
+ fun matches s = (ws(); String.isPrefix s (!inputData))
+ fun consume s =
+ if matches s then
+ (inputData := String.extract (!inputData, size s, NONE);
+ inputPosition := !inputPosition + size s)
+ else
+ raise JSONParseError ("Expected '"^s^"'", !inputPosition)
+
+ fun parseObject () =
+ if not (matches "{") then
+ raise JSONParseError ("Expected '{'", !inputPosition)
+ else
+ (consume "{"; ws ();
+ if matches "}" then Callbacks.json_object [] before consume "}"
+ else
+ (Callbacks.json_object (parseMembers ())
+ before (ws (); consume "}")))
+
+ and parseMembers () =
+ parsePair () ::
+ (if matches "," then (consume ","; parseMembers ()) else [])
+
+ and parsePair () =
+ Callbacks.json_pair (parseString (),
+ (ws(); consume ":"; ws(); parseValue ()))
+
+ and parseArray () =
+ if not (matches "[") then
+ raise JSONParseError ("Expected '['", !inputPosition)
+ else
+ (consume "[";
+ if matches "]" then
+ Callbacks.json_array [] before consume "]"
+ else
+ Callbacks.json_array (parseElements ()) before (ws (); consume "]"))
+
+ and parseElements () =
+ parseValue () ::
+ (if matches "," then (consume ","; parseElements ()) else [])
+
+ and parseValue () =
+ Callbacks.json_value (
+ if matches "\"" then Callbacks.json_string (parseString ()) else
+ if matches "-" orelse isDigit () then parseNumber () else
+ if matches "true" then Callbacks.json_bool true before consume "true" else
+ if matches "false" then Callbacks.json_bool false before consume "false" else
+ if matches "null" then Callbacks.json_null () before consume "null" else
+ if matches "[" then parseArray () else
+ if matches "{" then parseObject () else
+ raise JSONParseError ("Expected value", !inputPosition))
+
+ and parseString () =
+ (ws () ;
+ consume ("\"") ;
+ parseChars () before consume "\"")
+
+ and parseChars () =
+ let
+ val escapedchars = ["n", "r", "b", "f", "t"]
+ fun pickChars s =
+ if peek () = #"\"" (* " = end of string *)
+ then s
+ else
+ if peek () = #"\\" andalso (String.sub (!inputData, 1)) = #"\""
+ then (consume "\\\""; pickChars (s ^ "\""))
+ else
+ if peek () = #"\\" andalso String.sub (!inputData, 1) = #"\\" andalso String.sub (!inputData, 2) = #"n"
+ then (consume "\\\\n"; pickChars (s ^ "\\n"))
+ else
+ if peek () = #"\\" andalso (String.sub (!inputData, 1)) = #"n"
+ then (consume "\\n"; pickChars (s ^ "\n"))
+ else
+ if peek () = #"\\" andalso String.sub (!inputData, 1) = #"\\" andalso String.sub (!inputData, 2) = #"r"
+ then (consume "\\\\r"; pickChars (s ^ "\\r"))
+ else
+ if peek () = #"\\" andalso (String.sub (!inputData, 1)) = #"r"
+ then (consume "\\r"; pickChars (s ^ "\r"))
+ else pickChars (s ^ String.str (take ()))
+ in
+ pickChars ""
+ end
+
+ and parseNumber () =
+ let
+ val i = parseInt ()
+ in
+ if peek () = #"e" orelse peek () = #"E" then
+ Callbacks.json_int (valOf (Int.fromString (i^parseExp())))
+ else if peek () = #"." then
+ let
+ val f = parseFrac()
+
+ val f' = if peek() = #"e" orelse peek() = #"E" then
+ i ^ f ^ parseExp ()
+ else i ^ f
+ in
+ Callbacks.json_real (valOf (Real.fromString f'))
+ end
+ else Callbacks.json_int (valOf (Int.fromString i))
+ end
+
+ and parseInt () =
+ let
+ val f =
+ if peek () = #"-"
+ then (take (); "~")
+ else String.str (take ())
+ in
+ f ^ parseDigits ()
+ end
+
+ and parseDigits () =
+ let
+ val r = ref ""
+ in
+ (while Char.isDigit (peek ()) do
+ r := !r ^ String.str (take ());
+ !r)
+ end
+
+ and parseFrac () =
+ (consume "." ;
+ "." ^ parseDigits ())
+
+ and parseExp () =
+ let
+ val _ =
+ if peek () = #"e" orelse
+ peek () = #"E" then take ()
+ else
+ raise JSONParseError ("Invalid number", !inputPosition)
+
+ val f = if peek () = #"-" then (take (); "~")
+ else if peek () = #"+" then (take (); "")
+ else ""
+ in
+ "e" ^ f ^ parseDigits ()
+ end
+
+ fun parse s =
+ (inputData := s ;
+ inputPosition := 0 ;
+ parseObject ()) handle JSONParseError (m,p) =>
+ Callbacks.error_handle (m,p,!inputData)
+end
+
+structure JsonIntermAst =
+struct
+datatype ast =
+ Array of ast list
+ | Null
+ | Float of real
+ | String of string
+ | Bool of bool
+ | Int of int
+ | Pair of (string * ast)
+ | Obj of ast list
+end
+
+structure Json :> JSON = struct
+datatype json =
+ Array of json list
+ | Null
+ | Float of real
+ | String of string
+ | Bool of bool
+ | Int of int
+ | Obj of (string * json) list
+
+fun fromInterm (interm: JsonIntermAst.ast): json =
+ case interm of
+ JsonIntermAst.Array l => Array (List.map fromInterm l)
+ | JsonIntermAst.Null => Null
+ | JsonIntermAst.Float r => Float r
+ | JsonIntermAst.String s => String s
+ | JsonIntermAst.Bool b => Bool b
+ | JsonIntermAst.Int i => Int i
+ | JsonIntermAst.Pair (k,v) =>
+ raise Fail ("JSON Parsing error. Pair of JSON found where it shouldn't. Key = " ^ k)
+ | JsonIntermAst.Obj l =>
+ Obj
+ (List.foldl
+ (fn (a, acc) =>
+ case a of
+ JsonIntermAst.Pair (k, v) => (k, fromInterm v) :: acc
+ | JsonIntermAst.Array _ => raise Fail ("JSON Parsing error. Found Array in object instead of key-value pair")
+ | JsonIntermAst.Null => raise Fail ("JSON Parsing error. Found Null in object instead of key-value pair")
+ | JsonIntermAst.Float _ => raise Fail ("JSON Parsing error. Found Float in object instead of key-value pair")
+ | JsonIntermAst.String _ => raise Fail ("JSON Parsing error. Found String in object instead of key-value pair")
+ | JsonIntermAst.Bool _ => raise Fail ("JSON Parsing error. Found Bool in object instead of key-value pair")
+ | JsonIntermAst.Int _ => raise Fail ("JSON Parsing error. Found Int in object instead of key-value pair")
+ | JsonIntermAst.Obj _ => raise Fail ("JSON Parsing error. Found Obj in object instead of key-value pair")
+ ) [] l)
+
+structure StandardJsonParserCallbacks =
+struct
+ type json_data = JsonIntermAst.ast
+ fun json_object l = JsonIntermAst.Obj l
+ fun json_pair (k,v) = JsonIntermAst.Pair (k,v)
+ fun json_array l = JsonIntermAst.Array l
+ fun json_value x = x
+ fun json_string s = JsonIntermAst.String s
+ fun json_int i = JsonIntermAst.Int i
+ fun json_real r = JsonIntermAst.Float r
+ fun json_bool b = JsonIntermAst.Bool b
+ fun json_null () = JsonIntermAst.Null
+ fun error_handle (msg,pos,data) =
+ raise Fail ("Error: " ^ msg ^ " near " ^ Int.toString pos ^ " data: " ^
+ data)
+end
+
+structure MyJsonParser = JSONParser (StandardJsonParserCallbacks)
+
+fun parse (str: string): json =
+ fromInterm (MyJsonParser.parse str)
+fun print (ast: json): string =
+ case ast of
+ Array l => "["
+ ^ List.foldl (fn (a, acc) => acc ^ (if acc = "" then "" else ", ") ^ print a) "" l
+ ^ "]"
+ | Null => "null"
+ | Float r => Real.toString r
+ | String s =>
+ "\"" ^
+ String.translate
+ (fn c => if c = #"\"" then "\\\"" else Char.toString c)
+ s ^
+ "\""
+ | Bool b => if b then "true" else "false"
+ | Int i => if i >= 0
+ then (Int.toString i)
+ else "-" ^ (Int.toString (Int.abs i)) (* default printing uses ~ instead of - *)
+ | Obj l => "{"
+ ^ List.foldl (fn ((k, v), acc) => acc ^ (if acc = "" then "" else ", ") ^ "\"" ^ k ^ "\": " ^ print v ) "" l
+ ^ "}"
+end
diff --git a/src/lsp.sig b/src/lsp.sig
new file mode 100644
index 00000000..0dc95801
--- /dev/null
+++ b/src/lsp.sig
@@ -0,0 +1,3 @@
+signature LSP = sig
+ val startServer : unit -> unit
+end
diff --git a/src/lsp.sml b/src/lsp.sml
new file mode 100644
index 00000000..c99a6f2e
--- /dev/null
+++ b/src/lsp.sml
@@ -0,0 +1,514 @@
+structure Lsp :> LSP = struct
+
+structure C = Compiler
+structure P = Print
+
+val debug = LspSpec.debug
+
+structure SK = struct
+ type ord_key = string
+ val compare = String.compare
+end
+structure SM = BinaryMapFn(SK)
+
+type fileState =
+ { envBeforeThisModule: ElabEnv.env
+ , decls: Elab.decl list
+ , text: string}
+type state =
+ { urpPath : string
+ , fileStates : fileState SM.map
+ }
+
+(* Wrapping this in structure as an attempt to not get concurrency bugs *)
+structure State :
+ sig
+ val init: state -> unit
+ val insertText: string -> string -> unit
+ val insertElabRes: string -> ElabEnv.env -> Elab.decl list -> unit
+ val removeFile: string -> unit
+ val withState: (state -> 'a) -> 'a
+ end = struct
+val stateRef = ref (NONE: state option)
+fun init (s: state) =
+ stateRef := SOME s
+fun withState (f: state -> 'a): 'a =
+ case !stateRef of
+ NONE => raise LspSpec.LspError LspSpec.ServerNotInitialized
+ | SOME s => f s
+
+fun insertText (fileName: string) (text: string) =
+ withState (fn oldS =>
+ stateRef := SOME { urpPath = #urpPath oldS
+ , fileStates =
+ case SM.find (#fileStates oldS, fileName) of
+ NONE => SM.insert ( #fileStates oldS
+ , fileName
+ , { text = text
+ , decls = []
+ , envBeforeThisModule = ElabEnv.empty })
+ | SOME oldfs =>
+ SM.insert ( #fileStates oldS
+ , fileName
+ , { text = text
+ , decls = #decls oldfs
+ , envBeforeThisModule = #envBeforeThisModule oldfs })
+ }
+ )
+
+fun insertElabRes (fileName: string) (env: ElabEnv.env) decls =
+ withState (fn oldS =>
+ stateRef := SOME { urpPath = #urpPath oldS
+ , fileStates =
+ case SM.find (#fileStates oldS, fileName) of
+ NONE => raise Fail ("No text found for file " ^ fileName)
+ | SOME oldfs =>
+ SM.insert ( #fileStates oldS
+ , fileName
+ , { text = #text oldfs
+ , decls = decls
+ , envBeforeThisModule = env })
+ }
+ )
+
+fun removeFile (fileName: string) =
+ withState (fn oldS =>
+ stateRef := SOME { urpPath = #urpPath oldS
+ , fileStates = #1 (SM.remove (#fileStates oldS, fileName))
+ }
+ )
+
+end
+
+
+
+fun scanDir (f: string -> bool) (path: string) =
+ let
+ val dir = OS.FileSys.openDir path
+ fun doScanDir acc =
+ case OS.FileSys.readDir dir of
+ NONE => (OS.FileSys.closeDir dir; acc)
+ | SOME fname =>
+ (if f fname
+ then doScanDir (fname :: acc)
+ else doScanDir acc)
+ in
+ doScanDir []
+ end
+
+(* Throws Fail if can't init *)
+fun initState (initParams: LspSpec.initializeParams): state =
+ let
+ val rootPath = case #rootUri initParams of
+ NONE => raise Fail "No rootdir found"
+ | SOME a => #path a
+ val optsUrpFile =
+ (SOME (FromJson.asString (FromJson.get "urpfile" (FromJson.get "project" (FromJson.get "urweb" (#initializationOptions initParams))))))
+ handle ex => NONE
+ val foundUrps = scanDir (fn fname => OS.Path.ext fname = SOME "urp") rootPath
+ in
+ { urpPath = case foundUrps of
+ [] => raise Fail ("No .urp files found in path " ^ rootPath)
+ | one :: [] => OS.Path.base (OS.Path.file one)
+ | many => case List.find (fn m => SOME (OS.Path.base (OS.Path.file m)) = optsUrpFile) many of
+ NONE => raise Fail ("Found multiple .urp files in path " ^ rootPath)
+ | SOME f => OS.Path.base (OS.Path.file f)
+ , fileStates = SM.empty
+ }
+ end
+
+fun addSgnToEnv (env: ElabEnv.env) (sgn: Source.sgn_item list) (fileName: string) (addUnprefixed: bool): ElabEnv.env =
+ let
+ val moduleName = C.moduleOf fileName
+ val (sgn, gs) = Elaborate.elabSgn (env, Disjoint.empty) (Source.SgnConst sgn, { file = fileName
+ , first = ErrorMsg.dummyPos
+ , last = ErrorMsg.dummyPos })
+ val () = case gs of
+ [] => ()
+ | _ => (app (fn (_, env, _, c1, c2) =>
+ Print.prefaces "Unresolved"
+ [("c1", ElabPrint.p_con env c1),
+ ("c2", ElabPrint.p_con env c2)]) gs;
+ raise Fail ("Unresolved disjointness constraints in " ^ moduleName ^ " at " ^ fileName)) (* TODO Not sure if this is needed for all signatures or only for Basis *)
+ val (env', n) = ElabEnv.pushStrNamed env moduleName sgn
+ val (_, env') = if addUnprefixed
+ then Elaborate.dopen env' {str = n, strs = [], sgn = sgn}
+ else ([], env')
+ in
+ env'
+ end
+
+fun errorToDiagnostic (err: { span: ErrorMsg.span , message: string }): LspSpec.diagnostic =
+ { range = { start = { line = #line (#first (#span err)) - 1
+ , character = #char (#first (#span err))
+ }
+ , end_ = { line = #line (#last (#span err)) - 1
+ , character = #char (#last (#span err))
+ }
+ }
+ , severity = 1
+ , source = "UrWeb"
+ , message = #message err
+ }
+
+(* TODO FFI modules ? Check compiler.sml -> parse -> parseFfi *)
+(* TODO Optim: cache parsed urp file? *)
+fun elabFile (state: state) (fileName: string): ({ decls: Elab.decl list, envBeforeThisModule: ElabEnv.env} option * LspSpec.diagnostic list) =
+ let
+ val () = if (OS.Path.ext fileName = SOME "ur")
+ then ()
+ else raise Fail ("Can only handle .ur files for now")
+ (* val () = Elaborate.unifyMore := true *)
+ (* To reuse Basis and Top *)
+ val () = Elaborate.incremental := true
+ (* Parsing .urp *)
+ val job = case C.run (C.transform C.parseUrp "parseUrp") (#urpPath state) of
+ NONE => raise LspSpec.LspError (LspSpec.InternalError ("Couldn't parse .urp file at " ^ (#urpPath state)))
+ | SOME a => a
+ val moduleSearchRes =
+ List.foldl
+ (fn (entry, acc) => if #2 acc
+ then acc
+ else
+ if entry ^ ".ur" = fileName
+ then (List.rev (#1 acc), true)
+ else (entry :: #1 acc, false))
+ ([] (* modules before *), false (* module found *))
+ (#ffi job @ #sources job)
+ val modulesBeforeThisFile = #1 moduleSearchRes
+ val () = if #2 moduleSearchRes
+ then ()
+ else raise LspSpec.LspError (LspSpec.InternalError ("Couldn't find file " ^ fileName ^ " referenced in .urp file at " ^ (#urpPath state)))
+ (* Parsing .urs files of previous modules *)
+ val parsedUrss = List.map (fn entry =>
+ if OS.FileSys.access (entry ^ ".urs", [])
+ then case C.run (C.transform C.parseUrs "parseUrs") (entry ^ ".urs") of
+ NONE => raise LspSpec.LspError (LspSpec.InternalError ("Failed to parse .urs file at " ^ entry))
+ | SOME a => { fileName = entry ^ ".urs", parsed = a}
+ else
+ if OS.FileSys.access (entry ^ ".ur", [])
+ then case C.run (C.transform C.parseUrs "parseUrs") (entry ^ ".ur") of
+ NONE => raise LspSpec.LspError (LspSpec.InternalError ("No .urs file found for " ^ entry ^ " and couldn't parse .ur as .urs file"))
+ | SOME a => { fileName = entry ^ ".ur" , parsed = a}
+ else raise LspSpec.LspError (LspSpec.InternalError ("Couldn't find an .ur or .urs file for " ^ entry)))
+ modulesBeforeThisFile
+ (* Parsing Basis and Top *)
+ val basisF = Settings.libFile "basis.urs"
+ val topF = Settings.libFile "top.urs"
+ val topF' = Settings.libFile "top.ur"
+
+ val tm1 = OS.FileSys.modTime topF
+ val tm2 = OS.FileSys.modTime topF'
+
+ val parsedBasisUrs =
+ case C.run (C.transform C.parseUrs "parseUrs") basisF of
+ NONE => raise LspSpec.LspError (LspSpec.InternalError ("Failed to parse basis.urs file at " ^ basisF))
+ | SOME a => a
+ val parsedTopUrs =
+ case C.run (C.transform C.parseUrs "parseUrs") topF of
+ NONE => raise LspSpec.LspError (LspSpec.InternalError ("Failed to parse top.urs file at " ^ topF))
+ | SOME a => a
+ val parsedTopUr =
+ case C.run (C.transform C.parseUr "parseUr") topF' of
+ NONE => raise LspSpec.LspError (LspSpec.InternalError ("Failed to parse top.ur file at " ^ topF'))
+ | SOME a => a
+
+ (* Parsing .ur and .urs of current file *)
+ val (parsedUrs: Source.sgn option) =
+ (if OS.FileSys.access (fileName ^ "s", [])
+ then
+ case C.run (C.transform C.parseUrs "parseUrs") (fileName ^ "s") of
+ NONE => NONE
+ | SOME a => SOME ( Source.SgnConst a
+ , {file = fileName ^ "s", first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos})
+ else
+ NONE) handle ex => NONE
+ val () = ErrorMsg.resetErrors ()
+ val (parsedUrO: (Source.decl list) option) =
+ C.run (C.transform C.parseUr "parseUr") fileName
+ in
+ case parsedUrO of
+ NONE => (* Parse error *) (NONE, List.map errorToDiagnostic (ErrorMsg.readErrorLog ()))
+ | SOME parsedUr =>
+ (* Parsing of .ur succeeded *)
+ let
+ val loc = {file = fileName, first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos}
+ val envBeforeThisModule = ref ElabEnv.empty
+ val res = Elaborate.elabFile
+ parsedBasisUrs tm1 parsedTopUr parsedTopUrs tm2 ElabEnv.empty
+ (* Adding urs's of previous modules to env *)
+ (fn envB =>
+ let
+ val newEnv = List.foldl (fn (sgn, env) => addSgnToEnv env (#parsed sgn) (#fileName sgn) false) envB parsedUrss
+ in
+ (envBeforeThisModule := newEnv; newEnv)
+ end
+ )
+ [( Source.DStr (C.moduleOf fileName, parsedUrs, NONE, (Source.StrConst parsedUr, loc), false)
+ , loc )]
+ (* report back errors (as Diagnostics) *)
+ val errors = ErrorMsg.readErrorLog ()
+ val decls = case List.last res of
+ (Elab.DStr (_, _, _, (Elab.StrConst decls, _)), _) => decls
+ | _ => raise Fail ("Impossible: Source.StrConst did not become Elab.StrConst after elaboration")
+ in
+ (SOME { envBeforeThisModule = !envBeforeThisModule, decls = decls },
+ List.map errorToDiagnostic errors)
+ end
+ end
+
+fun uniq (eq: 'b -> 'b -> bool) (bs: 'b list) =
+ case bs of
+ [] => []
+ | (l as b :: bs') => b :: uniq eq (List.filter (fn a => not (eq a b)) bs')
+
+fun elabFileAndSendDiags (state: state) (toclient: LspSpec.toclient) (documentUri: LspSpec.documentUri): unit =
+ let
+ val fileName = #path documentUri
+ val res = elabFile state fileName
+ fun eq_diag (d1: LspSpec.diagnostic) (d2: LspSpec.diagnostic) = #range d1 = #range d2 andalso #message d1 = #message d2
+ val diags = uniq eq_diag (#2 res)
+ in
+ (case #1 res of
+ NONE => ()
+ | SOME fs =>
+ (State.insertElabRes fileName (#envBeforeThisModule fs) (#decls fs));
+ #publishDiagnostics toclient { uri = documentUri , diagnostics = diags})
+ end
+
+fun scanDir (f: string -> bool) (path: string) =
+ let
+ val dir = OS.FileSys.openDir path
+ fun doScanDir acc =
+ case OS.FileSys.readDir dir of
+ NONE => (OS.FileSys.closeDir dir; acc)
+ | SOME fname =>
+ (if f fname
+ then doScanDir (fname :: acc)
+ else doScanDir acc)
+ in
+ doScanDir []
+ end
+
+fun readFile (fileName: string): string =
+ let
+ val stream = TextIO.openIn fileName
+ fun doReadFile acc =
+ case TextIO.inputLine stream of
+ NONE => acc
+ | SOME str => (if acc = ""
+ then doReadFile str
+ else doReadFile (acc ^ str))
+ val res = doReadFile ""
+ in
+ (TextIO.closeIn stream; res)
+ end
+
+
+(* TODO PERF BIG I couldn't figure out how to print just to a string, so writing to a temp file, then reading it, then deleting it, ... *)
+fun ppToString (pp: Print.PD.pp_desc) (width: int): string =
+ let
+ val tempfile = OS.FileSys.tmpName ()
+ val outStr = TextIO.openOut tempfile
+ val outDev = TextIOPP.openOut {dst = outStr, wid = width}
+ val () = Print.fprint outDev pp
+ val res = readFile tempfile
+ val () = TextIO.closeOut outStr
+ in
+ res
+ end
+
+fun getStringAtCursor
+ (stopAtCursor: bool)
+ (text: string)
+ (pos: LspSpec.position)
+ : string
+ =
+ let
+ val line = List.nth (Substring.fields (fn c => c = #"\n") (Substring.full text), #line pos)
+ val chars = [ (* #".", *) #"(", #")", #"{", #"}", #"[", #"]", #"<", #">", #"-", #"=", #":", #"@"
+ , #" ", #"\n", #"#", #",", #"*", #"\"", #"|", #"&", #"$", #"^", #"+", #";"]
+ val lineUntilCursor = Substring.slice (line, 0, SOME (#character pos))
+ val beforeCursor = Substring.string (Substring.taker (fn c => not (List.exists (fn c' => c = c') chars)) lineUntilCursor)
+ val afterCursor = if stopAtCursor
+ then ""
+ else let
+ val lineAfterCursor = Substring.slice (line, #character pos, NONE)
+ in
+ Substring.string (Substring.takel (fn c => not (List.exists (fn c' => c = c') (#"." :: chars))) lineAfterCursor)
+ end
+ in
+ beforeCursor ^ afterCursor
+ end
+
+fun formatTypeBox (a: P.PD.pp_desc, b: P.PD.pp_desc) =
+ P.PD.hvBox (P.PD.PPS.Rel 0, [a,
+ P.PD.string ": ",
+ P.PD.break {nsp = 0, offset = 2},
+ b])
+
+fun handleHover (state: state) (p: LspSpec.hoverReq): LspSpec.hoverResp LspSpec.result =
+ let
+ val fileName = #path (#uri (#textDocument p))
+ val s = SM.find (#fileStates state, fileName)
+ in
+ case s of
+ NONE => LspSpec.Success NONE
+ | SOME s =>
+ let
+ val searchString = getStringAtCursor false (#text s) (#position p)
+ val env = #envBeforeThisModule s
+ val decls = #decls s
+ val loc = #position p
+ val (env, prefix, found) = GetInfo.findStringInEnv env (Elab.StrConst decls) fileName { line = #line loc + 1
+ , char = #character loc + 1} searchString
+ in
+ case found of
+ NONE => LspSpec.Success NONE
+ | SOME f =>
+ let
+ val desc = case f of
+ GetInfo.FoundStr (x, (_, sgn)) => formatTypeBox (P.PD.string (prefix ^ x), P.PD.string "module")
+ | GetInfo.FoundKind (x, kind) => formatTypeBox (P.PD.string (prefix ^ x), ElabPrint.p_kind env kind)
+ | GetInfo.FoundCon (x, con) => formatTypeBox (P.PD.string (prefix ^ x), ElabPrint.p_con env con)
+ in
+ LspSpec.Success (SOME {contents = ppToString desc 50})
+ end
+ end
+ end
+
+(* TODO IDEA can we use the real parser to figure out what we're typing (exp, con, field, etc) to predict better? *)
+fun handleCompletion (state: state) (p: LspSpec.completionReq) =
+ let
+ val fileName = #path (#uri (#textDocument p))
+ val s = SM.find (#fileStates state, fileName)
+ in
+ case s of
+ NONE => LspSpec.Success { isIncomplete = false, items = []}
+ | SOME s =>
+ let
+ val pos = #position p
+ val searchStr = getStringAtCursor true (#text s) pos
+ val env = #envBeforeThisModule s
+ val decls = #decls s
+ val (env, prefix, foundItems) = GetInfo.matchStringInEnv env (Elab.StrConst decls) fileName { line = #line pos + 1, char = #character pos + 1} searchStr
+ val completions = List.map
+ (fn f => case f of
+ GetInfo.FoundStr (x, _) => {label = prefix ^ x, kind = LspSpec.Module, detail = ""}
+ | GetInfo.FoundKind (x, k) => {label = prefix ^ x, kind = LspSpec.Constructor, detail = ppToString (ElabPrint.p_kind env k) 200}
+ | GetInfo.FoundCon (x, c) => {label = prefix ^ x, kind = LspSpec.Value, detail = ppToString (ElabPrint.p_con env c) 200}
+ )
+ foundItems
+ in
+ LspSpec.Success { isIncomplete = false
+ , items = completions }
+ end
+ end
+
+fun applyContentChange ((c, s): LspSpec.contentChange * string): string =
+ case (#range c, #rangeLength c) of
+ (SOME range, SOME _) =>
+ let
+ val lines = Substring.fields (fn c => c = #"\n") (Substring.full s)
+ val linesBefore = List.take (lines, #line (#start range))
+ val linesAfter = List.drop (lines, #line (#end_ range) + 1)
+ val startLine = List.nth (lines, #line (#start range))
+ val startText = Substring.slice (startLine, 0, SOME (#character (#start range)))
+ val endLine = List.nth (lines, #line (#end_ range))
+ val endText = Substring.triml (#character (#end_ range)) endLine
+ in
+ Substring.concatWith "\n" (linesBefore
+ @ [Substring.full (Substring.concat [startText, Substring.full (#text c), endText])]
+ @ linesAfter)
+ end
+ | _ =>
+ #text c
+
+fun handleDocumentDidChange (state: state) (toclient: LspSpec.toclient) (p: LspSpec.didChangeParams): unit =
+ let
+ val fileName = #path (#uri (#textDocument p))
+ val s = SM.find (#fileStates state, fileName)
+ in
+ case s of
+ NONE =>
+ (debug ("Got change event for file that isn't open: " ^ fileName);
+ (#showMessage toclient) ("Got change event for file that isn't open: " ^ fileName) 1)
+ | SOME s =>
+ State.insertText fileName (List.foldl applyContentChange (#text s) (#contentChanges p))
+ end
+
+fun runInBackground (toclient: LspSpec.toclient) (fileName: string) (f: unit -> unit): unit =
+ BgThread.queueBgTask
+ fileName
+ ((fn () => (f ()
+ handle LspSpec.LspError (LspSpec.InternalError str) => (#showMessage toclient) str 1
+ | LspSpec.LspError LspSpec.ServerNotInitialized => (#showMessage toclient) "Server not initialized" 1
+ | ex => (#showMessage toclient) (General.exnMessage ex) 1
+ ; (#showMessage toclient) ("Done running BG job for " ^ fileName) 3
+ )))
+
+fun handleRequest (requestMessage: LspSpec.message) =
+ case requestMessage of
+ LspSpec.Notification n =>
+ LspSpec.matchNotification
+ n
+ { initialized = fn () => ()
+ , textDocument_didOpen =
+ fn (p, toclient) =>
+ (State.insertText (#path (#uri (#textDocument p))) (#text (#textDocument p));
+ runInBackground
+ toclient
+ (#path (#uri (#textDocument p)))
+ (fn () => State.withState (fn state => elabFileAndSendDiags state toclient (#uri (#textDocument p)))))
+ , textDocument_didChange =
+ fn (p, toclient) =>
+ State.withState (fn state => handleDocumentDidChange state toclient p)
+ , textDocument_didSave =
+ fn (p, toclient) =>
+ runInBackground
+ toclient
+ (#path (#uri (#textDocument p)))
+ (fn () => State.withState (fn state => elabFileAndSendDiags state toclient (#uri (#textDocument p))))
+ , textDocument_didClose =
+ fn (p, toclient) =>
+ State.removeFile (#path (#uri (#textDocument p)))
+ }
+ | LspSpec.RequestMessage m =>
+ (* TODO should error handling here be inside handleMessage? *)
+ LspSpec.matchMessage
+ m
+ { initialize = fn p =>
+ (let val st = initState p
+ in
+ State.init st;
+ LspSpec.Success
+ { capabilities =
+ { hoverProvider = true
+ , completionProvider = SOME { triggerCharacters = ["."]}
+ , textDocumentSync = { openClose = true
+ , change = 2
+ , save = SOME { includeText = false }
+ }}
+ }
+ end)
+ , shutdown = fn () => LspSpec.Success ()
+ , textDocument_hover = fn toclient => State.withState handleHover
+ , textDocument_completion = fn p => State.withState (fn s => handleCompletion s p)
+ }
+
+fun serverLoop () =
+ if not (Option.isSome (TextIO.canInput (TextIO.stdIn, 1))) andalso BgThread.hasBgTasks ()
+ then
+ (* no input waiting -> give control to lower prio thread *)
+ BgThread.runBgTaskForABit ()
+ else
+ let
+ val requestMessage =
+ LspSpec.readRequestFromStdIO ()
+ handle ex => (debug ("Error in reading from stdIn: " ^ General.exnMessage ex) ; raise ex)
+ in
+ handleRequest requestMessage
+ end
+
+fun startServer () = while true do serverLoop ()
+end
diff --git a/src/lspspec.sml b/src/lspspec.sml
new file mode 100644
index 00000000..0d766056
--- /dev/null
+++ b/src/lspspec.sml
@@ -0,0 +1,450 @@
+structure LspSpec = struct
+
+ datatype lspError = InternalError of string
+ | ServerNotInitialized
+ exception LspError of lspError
+
+ fun debug (str: string): unit =
+ (TextIO.output (TextIO.stdErr, str ^ "\n\n"); TextIO.flushOut TextIO.stdErr)
+
+ fun trim (s: substring): substring =
+ Substring.dropr Char.isSpace (Substring.dropl Char.isSpace s)
+
+ fun readHeader (): (string * string) option =
+ let
+ val line = TextIO.inputLine TextIO.stdIn
+ in
+ case line of
+ NONE => OS.Process.exit OS.Process.success
+ | SOME str =>
+ if Substring.isEmpty (trim (Substring.full str))
+ then NONE
+ else
+ let
+ val (key, value) = Substring.splitl (fn c => c <> #":") (Substring.full str)
+ in
+ if Substring.isEmpty (trim value)
+ then raise Fail ("Failed to parse LSP header: Line is not empty but is also not a valid header: " ^ str)
+ else SOME ( Substring.string (trim key)
+ , Substring.string (trim (Substring.dropl (fn c => c = #":") (trim value))))
+ end
+ end
+
+ fun readAllHeaders (): (string * string) list =
+ let
+ fun doReadAllHeaders (l: (string * string) list): (string * string) list =
+ case readHeader () of
+ NONE => l
+ | SOME tup => tup :: doReadAllHeaders l
+
+ in
+ doReadAllHeaders []
+ end
+ datatype message =
+ RequestMessage of { id: Json.json, method: string, params: Json.json}
+ | Notification of { method: string, params: Json.json}
+ fun parseMessage (j: Json.json): message =
+ let
+ val id = SOME (FromJson.get "id" j)
+ handle ex => NONE
+ val method = FromJson.asString (FromJson.get "method" j)
+ val params = FromJson.get "params" j
+ in
+ case id of
+ NONE => Notification {method = method, params = params}
+ | SOME id => RequestMessage {id = id, method = method, params = params}
+ end
+
+ type documentUri =
+ { scheme: string
+ , authority: string
+ , path: string
+ , query: string
+ , fragment: string
+ }
+ fun parseDocumentUri (str: string): documentUri =
+ let
+ val str = Substring.full str
+ val (scheme, rest) = Substring.splitl (fn c => c <> #":") str
+ val (authority, rest) = Substring.splitl (fn c => c <> #"/") (Substring.triml 3 rest (* :// *))
+ val (path, rest) = Substring.splitl (fn c => c <> #"?" orelse c <> #"#") rest
+ val (query, rest) = if Substring.first rest = SOME #"?"
+ then Substring.splitl (fn c => c <> #"#") (Substring.triml 1 rest (* ? *))
+ else (Substring.full "", rest)
+ val fragment = if Substring.first rest = SOME #"#"
+ then (Substring.triml 1 rest (* # *))
+ else Substring.full ""
+
+ in
+ { scheme = Substring.string scheme
+ , authority = Substring.string authority
+ , path = Substring.string path
+ , query = Substring.string query
+ , fragment = Substring.string fragment
+ }
+ end
+ fun printDocumentUri (d: documentUri) =
+ (#scheme d) ^ "://" ^
+ (#authority d) ^
+ (#path d) ^
+ (if #query d <> "" then "?" ^ #query d else "") ^
+ (if #fragment d <> "" then "#" ^ #fragment d else "")
+
+ type textDocumentIdentifier = { uri: documentUri}
+ fun parseTextDocumentIdentifier (j: Json.json): textDocumentIdentifier =
+ { uri = parseDocumentUri (FromJson.asString (FromJson.get "uri" j))}
+
+ type versionedTextDocumentIdentifier =
+ { uri: documentUri
+ , version: int option
+ }
+ fun parseVersionedTextDocumentIdentifier (j: Json.json): versionedTextDocumentIdentifier =
+ { uri = parseDocumentUri (FromJson.asString (FromJson.get "uri" j))
+ , version = FromJson.asOptionalInt (FromJson.get "version" j)
+ }
+
+ type textDocumentItem = {
+ uri: documentUri,
+ languageId: string,
+ version: int, (* The version number of this document (it will increase after each change, including undo/redo). *)
+ text: string
+ }
+ fun parseTextDocumentItem (j: Json.json) =
+ { uri = parseDocumentUri (FromJson.asString (FromJson.get "uri" j))
+ , languageId = FromJson.asString (FromJson.get "languageId" j)
+ , version = FromJson.asInt (FromJson.get "version" j)
+ , text = FromJson.asString (FromJson.get "text" j)
+ }
+
+ type position = { line: int
+ , character: int
+ }
+ fun parsePosition (j: Json.json) =
+ { line = FromJson.asInt (FromJson.get "line" j)
+ , character = FromJson.asInt (FromJson.get "character" j)
+ }
+ fun printPosition (p: position): Json.json = Json.Obj [ ("line", Json.Int (#line p))
+ , ("character", Json.Int (#character p))]
+
+ type range = { start: position
+ , end_: position }
+ fun parseRange (j: Json.json): range =
+ { start = parsePosition (FromJson.get "start" j)
+ , end_ = parsePosition (FromJson.get "end" j)
+ }
+ fun printRange (r: range): Json.json = Json.Obj [ ("start", printPosition (#start r))
+ , ("end", printPosition (#end_ r))]
+
+ fun readRequestFromStdIO (): message =
+ let
+ val headers = readAllHeaders ()
+ val lengthO = List.find (fn (k,v) => k = "Content-Length") headers
+ val request = case lengthO of
+ NONE => raise Fail "No header with Content-Length found"
+ | SOME (k, v) =>
+ case Int.fromString v of
+ NONE => raise Fail ("Couldn't parse content-length from string: " ^ v)
+ | SOME i => TextIO.inputN (TextIO.stdIn, i)
+ val parsed = Json.parse request
+ in
+ parseMessage parsed
+ end
+
+ type hoverReq = { textDocument: textDocumentIdentifier , position: position }
+ type hoverResp = {contents: string} option
+ fun parseHoverReq (params: Json.json): hoverReq =
+ { textDocument = parseTextDocumentIdentifier (FromJson.get "textDocument" params)
+ , position = parsePosition (FromJson.get "position" params)
+ }
+ fun printHoverResponse (resp: hoverResp): Json.json =
+ case resp of
+ NONE => Json.Null
+ | SOME obj => Json.Obj [("contents", Json.String (#contents obj))]
+
+ type didOpenParams = { textDocument: textDocumentItem }
+ fun parseDidOpenParams (params: Json.json): didOpenParams =
+ { textDocument = parseTextDocumentItem (FromJson.get "textDocument" params) }
+
+ type contentChange = { range: range option
+ , rangeLength: int option
+ , text: string }
+ type didChangeParams =
+ { textDocument: versionedTextDocumentIdentifier
+ , contentChanges: contentChange list
+ }
+ fun parseDidChangeParams (params: Json.json): didChangeParams =
+ { textDocument = parseVersionedTextDocumentIdentifier (FromJson.get "textDocument" params)
+ , contentChanges = case FromJson.get "contentChanges" params of
+ Json.Array js =>
+ List.map (fn j => { range = Option.map parseRange (FromJson.getO "range" j)
+ , rangeLength = Option.map FromJson.asInt (FromJson.getO "rangeLength" j)
+ , text = FromJson.asString (FromJson.get "text" j)
+ }
+ ) js
+ | j => raise Fail ("Expected JSON array, got: " ^ Json.print j)
+ }
+
+ type didSaveParams = { textDocument: textDocumentIdentifier }
+ fun parseDidSaveParams (params: Json.json): didSaveParams =
+ { textDocument = parseTextDocumentIdentifier (FromJson.get "textDocument" params)
+ (* , text = ... *)
+ }
+ type didCloseParams = { textDocument: textDocumentIdentifier }
+ fun parseDidCloseParams (params: Json.json): didCloseParams =
+ { textDocument = parseTextDocumentIdentifier (FromJson.get "textDocument" params)
+ }
+ type initializeParams =
+ { rootUri: documentUri option
+ , initializationOptions: Json.json }
+ fun parseInitializeParams (j: Json.json) =
+ { rootUri =
+ Option.map
+ parseDocumentUri
+ (FromJson.asOptionalString (FromJson.get "rootUri" j))
+ , initializationOptions = FromJson.get "initializationOptions" j
+ }
+ type diagnostic = { range: range
+ (* code?: number | string *)
+ , severity: int (* 1 = error, 2 = warning, 3 = info, 4 = hint*)
+ , source: string
+ , message: string
+ (* relatedInformation?: DiagnosticRelatedInformation[]; *)
+ }
+ fun printDiagnostic (d: diagnostic): Json.json =
+ Json.Obj [ ("range", printRange (#range d))
+ , ("severity", Json.Int (#severity d))
+ , ("source", Json.String (#source d))
+ , ("message", Json.String (#message d))
+ ]
+ type publishDiagnosticsParams = { uri: documentUri
+ , diagnostics: diagnostic list
+ }
+ fun printPublishDiagnosticsParams (p: publishDiagnosticsParams): Json.json =
+ Json.Obj [ ("uri", Json.String (printDocumentUri (#uri p)))
+ , ("diagnostics", Json.Array (List.map printDiagnostic (#diagnostics p)))]
+
+ type completionReq =
+ { textDocument: textDocumentIdentifier
+ , position: position
+ , context: { triggerCharacter: string option
+ , triggerKind: int (* 1 = Invoked = typing an identifier or manual invocation or API
+ 2 = TriggerCharacter
+ 3 = TriggerForIncompleteCompletions*)} option
+ }
+ fun parseCompletionReq (j: Json.json): completionReq =
+ { textDocument = parseTextDocumentIdentifier (FromJson.get "textDocument" j)
+ , position = parsePosition (FromJson.get "position" j)
+ , context = case FromJson.getO "context" j of
+ NONE => NONE
+ | SOME ctx => SOME { triggerCharacter = Option.map FromJson.asString (FromJson.getO "triggerCharacter" ctx)
+ , triggerKind = FromJson.asInt (FromJson.get "triggerKind" ctx)
+ }
+ }
+
+ datatype completionItemKind = Text | Method | Function | Constructor | Field | Variable | Class | Interface | Module | Property | Unit | Value | Enum | Keyword | Snippet | Color | File | Reference | Folder | EnumMember | Constant | Struct | Event | Operator | TypeParameter
+ fun completionItemKindToInt (a: completionItemKind) =
+ case a of
+ Text => 1
+ | Method => 2
+ | Function => 3
+ | Constructor => 4
+ | Field => 5
+ | Variable => 6
+ | Class => 7
+ | Interface => 8
+ | Module => 9
+ | Property => 10
+ | Unit => 11
+ | Value => 12
+ | Enum => 13
+ | Keyword => 14
+ | Snippet => 15
+ | Color => 16
+ | File => 17
+ | Reference => 18
+ | Folder => 19
+ | EnumMember => 20
+ | Constant => 21
+ | Struct => 22
+ | Event => 23
+ | Operator => 24
+ | TypeParameter => 25
+
+ type completionItem = { label: string
+ , kind: completionItemKind
+ , detail: string
+ }
+ type completionResp = { isIncomplete: bool
+ , items: completionItem list
+ }
+
+ fun printCompletionItem (a: completionItem): Json.json =
+ Json.Obj [ ("label", Json.String (#label a))
+ , ("kind", Json.Int (completionItemKindToInt (#kind a)))
+ , ("detail", Json.String (#detail a))
+ ]
+ fun printCompletionResp (a: completionResp): Json.json =
+ Json.Obj [ ("isIncomplete", Json.Bool (#isIncomplete a))
+ , (("items", Json.Array (List.map printCompletionItem (#items a))))]
+
+ type initializeResponse = { capabilities:
+ { hoverProvider: bool
+ , completionProvider: {triggerCharacters: string list} option
+ , textDocumentSync:
+ { openClose: bool
+ , change: int (* 0 = None, 1 = Full, 2 = Incremental *)
+ , save: { includeText: bool } option
+ }
+ }}
+ fun printInitializeResponse (res: initializeResponse) =
+ Json.Obj [("capabilities",
+ let
+ val capabilities = #capabilities res
+ in
+ Json.Obj [ ("hoverProvider", Json.Bool (#hoverProvider capabilities))
+ , ("completionProvider", case #completionProvider capabilities of
+ NONE => Json.Null
+ | SOME cp => Json.Obj [("triggerCharacters", Json.Array (List.map Json.String (#triggerCharacters cp)))]
+ )
+ , ("textDocumentSync",
+ let
+ val textDocumentSync = #textDocumentSync capabilities
+ in
+ Json.Obj [ ("openClose", Json.Bool (#openClose textDocumentSync ))
+ , ("change", Json.Int (#change textDocumentSync))
+ , ("save", case #save textDocumentSync of
+ NONE => Json.Null
+ | SOME save => Json.Obj [("includeText", Json.Bool (#includeText save) )])]
+ end
+ )]
+ end
+ )]
+
+ datatype 'a result =
+ Success of 'a
+ | Error of (int * string)
+
+ fun mapResult (f: 'a -> 'b) (a: 'a result): 'b result =
+ case a of
+ Success contents => Success (f contents)
+ | Error e => Error e
+ type toclient = { showMessage: string -> int -> unit
+ , publishDiagnostics: publishDiagnosticsParams -> unit }
+ type messageHandlers =
+ { initialize: initializeParams -> initializeResponse result
+ , shutdown: unit -> unit result
+ , textDocument_hover: toclient -> hoverReq -> hoverResp result
+ , textDocument_completion: completionReq -> completionResp result
+ }
+
+ fun showMessage str typ =
+ let
+ val jsonToPrint = Json.print (Json.Obj [ ("jsonrpc", Json.String "2.0")
+ , ("method", Json.String "window/showMessage")
+ , ("params", Json.Obj [ ("type", Json.Int typ)
+ , ("message", Json.String str)])
+ ])
+ val toPrint = "Content-Length:" ^ Int.toString (String.size jsonToPrint) ^ "\r\n\r\n" ^ jsonToPrint
+ in
+ TextIO.print toPrint
+ end
+ fun publishDiagnostics diags =
+ let
+ val jsonToPrint = Json.print ((Json.Obj [ ("jsonrpc", Json.String "2.0")
+ , ("method", Json.String "textDocument/publishDiagnostics")
+ , ("params", printPublishDiagnosticsParams diags)
+ ]))
+ val toPrint = "Content-Length:" ^ Int.toString (String.size jsonToPrint) ^ "\r\n\r\n" ^ jsonToPrint
+ in
+ TextIO.print toPrint
+ end
+ val toclient: toclient = {showMessage = showMessage, publishDiagnostics = publishDiagnostics}
+
+ fun matchMessage
+ (requestMessage: {id: Json.json, method: string, params: Json.json})
+ (handlers: messageHandlers)
+ : unit =
+ let
+ val result: Json.json result =
+ ((case #method requestMessage of
+ "initialize" =>
+ mapResult
+ printInitializeResponse
+ ((#initialize handlers)
+ (parseInitializeParams (#params requestMessage)))
+ | "textDocument/hover" =>
+ mapResult
+ printHoverResponse
+ ((#textDocument_hover handlers)
+ toclient
+ (parseHoverReq (#params requestMessage)))
+ | "textDocument/completion" =>
+ mapResult
+ printCompletionResp
+ ((#textDocument_completion handlers)
+ (parseCompletionReq (#params requestMessage)))
+ | "shutdown" =>
+ mapResult
+ (fn () => Json.Null)
+ ((#shutdown handlers) ())
+ | "exit" =>
+ OS.Process.exit OS.Process.success
+ | method => (debug ("Method not supported: " ^ method);
+ Error (~32601, "Method not supported: " ^ method)))
+ handle LspError (InternalError str) => Error (~32603, str)
+ | LspError ServerNotInitialized => Error (~32002, "Server not initialized")
+ | ex => Error (~32603, (General.exnMessage ex))
+ )
+ (* val () = (TextIO.output (TextIO.stdErr, "Got result: " ^ (case result of Success _ => "success\n" *)
+ (* | Error _ => "error\n")); TextIO.flushOut TextIO.stdErr) *)
+ in
+ case result of
+ Success j =>
+ let
+ val jsonToPrint =
+ Json.print (Json.Obj [ ("id", #id requestMessage)
+ , ("jsonrpc", Json.String "2.0")
+ , ("result", j)
+ ])
+ val toPrint = "Content-Length:" ^ Int.toString (String.size jsonToPrint) ^ "\r\n\r\n" ^ jsonToPrint
+ in
+ TextIO.print toPrint
+ end
+ | Error (i, err) =>
+ let
+ val jsonToPrint =
+ Json.print (Json.Obj [ ("id", #id requestMessage)
+ , ("jsonrpc", Json.String "2.0")
+ , ("error", Json.Obj [ ("code", Json.Int i)
+ , ("message", Json.String err)
+ ])
+ ])
+ val toPrint = "Content-Length:" ^ Int.toString (String.size jsonToPrint) ^ "\r\n\r\n" ^ jsonToPrint
+ in
+ TextIO.print toPrint
+ end
+ end
+
+ type notificationHandlers =
+ { initialized: unit -> unit
+ , textDocument_didOpen: (didOpenParams * toclient) -> unit
+ , textDocument_didChange: (didChangeParams * toclient) -> unit
+ , textDocument_didSave: (didSaveParams * toclient) -> unit
+ , textDocument_didClose: (didCloseParams * toclient) -> unit
+ }
+ fun matchNotification
+ (notification: {method: string, params: Json.json})
+ (handlers: notificationHandlers)
+ =
+ (case #method notification of
+ "initialized" => (#initialized handlers) ()
+ | "textDocument/didOpen" => (#textDocument_didOpen handlers) (parseDidOpenParams (#params notification), toclient)
+ | "textDocument/didChange" => (#textDocument_didChange handlers) (parseDidChangeParams (#params notification), toclient)
+ | "textDocument/didSave" => (#textDocument_didSave handlers) (parseDidSaveParams (#params notification), toclient)
+ | "textDocument/didClose" => (#textDocument_didClose handlers) (parseDidCloseParams (#params notification), toclient)
+ | m => debug ("Notification method not supported: " ^ m))
+ handle LspError (InternalError str) => showMessage str 1
+ | LspError ServerNotInitialized => showMessage "Server not initialized" 1
+ | ex => showMessage (General.exnMessage ex) 1
+
+end
diff --git a/src/main.mlton.sml b/src/main.mlton.sml
index a6eaa7ea..9042307a 100644
--- a/src/main.mlton.sml
+++ b/src/main.mlton.sml
@@ -247,6 +247,7 @@ fun oneRun args =
NONE),
("moduleOf", ONE ("<file>", printModuleOf),
SOME "print module name of <file> and exit"),
+ ("startLspServer", ZERO Lsp.startServer, SOME "Start Language Server Protocol server"),
("noEmacs", set_true Demo.noEmacs,
NONE),
("limit", TWO ("<class>", "<num>", add_class),
diff --git a/src/mod_db.sig b/src/mod_db.sig
index 8f78f2c2..fb396603 100644
--- a/src/mod_db.sig
+++ b/src/mod_db.sig
@@ -30,12 +30,15 @@
signature MOD_DB = sig
val reset : unit -> unit
- val insert : Elab.decl * Time.time -> unit
+ val insert : Elab.decl * Time.time * bool (* hasErrors *) -> unit
(* Here's a declaration, including the modification timestamp of the file it came from.
* We might invalidate other declarations that depend on this one, if the timestamp has changed. *)
val lookup : Source.decl -> Elab.decl option
+ val lookupModAndDepsIncludingErrored:
+ string -> (Elab.decl * Elab.decl list) option
+
(* Allow undoing to snapshots after failed compilations. *)
val snapshot : unit -> unit
val revert : unit -> unit
diff --git a/src/mod_db.sml b/src/mod_db.sml
index 2d6b285b..c821a0bb 100644
--- a/src/mod_db.sml
+++ b/src/mod_db.sml
@@ -42,7 +42,9 @@ structure IM = IntBinaryMap
type oneMod = {Decl : decl,
When : Time.time,
- Deps : SS.set}
+ Deps : SS.set,
+ HasErrors: bool (* We're saving modules with errors so tooling can find them *)
+ }
val byName = ref (SM.empty : oneMod SM.map)
val byId = ref (IM.empty : string IM.map)
@@ -50,7 +52,39 @@ val byId = ref (IM.empty : string IM.map)
fun reset () = (byName := SM.empty;
byId := IM.empty)
-fun insert (d, tm) =
+(* For debug purposes *)
+fun printByName (bn: oneMod SM.map): unit =
+ (TextIO.print ("Contents of ModDb.byName: \n");
+ List.app (fn tup =>
+ let
+ val name = #1 tup
+ val m = #2 tup
+ val renderedDeps =
+ String.concatWith ", " (SS.listItems (#Deps m))
+ val renderedMod =
+ " " ^ name
+ ^ ". Stored at : " ^ Time.toString (#When m)
+ ^", HasErrors: " ^ Bool.toString (#HasErrors m)
+ ^". Deps: " ^ renderedDeps ^"\n"
+ in
+ TextIO.print renderedMod
+ end)
+ (SM.listItemsi bn))
+
+fun dContainsUndeterminedUnif d =
+ ElabUtil.Decl.exists
+ {kind = fn _ => false,
+ con = fn _ => false,
+ exp = fn e => case e of
+ EUnif (ref NONE) => true
+ | _ => false,
+ sgn_item = fn _ => false,
+ sgn = fn _ => false,
+ str = fn _ => false,
+ decl = fn _ => false}
+ d
+
+fun insert (d, tm, hasErrors) =
let
val xn =
case #1 d of
@@ -62,10 +96,16 @@ fun insert (d, tm) =
NONE => ()
| SOME (x, n) =>
let
+ (* Keep module when it's file didn't change and it was OK before *)
val skipIt =
case SM.find (!byName, x) of
NONE => false
| SOME r => #When r = tm
+ andalso not (#HasErrors r)
+ (* We save results of error'd compiler passes *)
+ (* so modules that still have undetermined unif variables *)
+ (* should not be reused since those are unsuccessfully compiled *)
+ andalso not (dContainsUndeterminedUnif (#Decl r))
in
if skipIt then
()
@@ -73,7 +113,19 @@ fun insert (d, tm) =
let
fun doMod (n', deps) =
case IM.find (!byId, n') of
- NONE => deps
+ NONE =>
+ (
+ (* TextIO.print ("MISSED_DEP: " ^ Int.toString n' ^"\n"); *)
+ deps)
+ (* raise Fail ("ModDb: Trying to make dep tree but couldn't find module " ^ Int.toString n') *)
+ (* I feel like this should throw, but the dependency searching algorithm *)
+ (* is not 100% precise. I encountered problems in json.urs: *)
+ (* datatype r = Rec of M.t r *)
+ (* M is the structure passed to the Recursive functor, so this is not an external dependency *)
+ (* I'm just not sure how to filter these out yet *)
+ (* I still think this should throw: *)
+ (* Trying to add a dep for a module but can't find the dep... *)
+ (* That will always cause a hole in the dependency tree and cause problems down the line *)
| SOME x' =>
SS.union (deps,
SS.add (case SM.find (!byName, x') of
@@ -118,8 +170,11 @@ fun insert (d, tm) =
x,
{Decl = d,
When = tm,
- Deps = deps});
+ Deps = deps,
+ HasErrors = hasErrors
+ });
byId := IM.insert (!byId, n, x)
+ (* printByName (!byName) *)
end
end
end
@@ -130,7 +185,7 @@ fun lookup (d : Source.decl) =
(case SM.find (!byName, x) of
NONE => NONE
| SOME r =>
- if tm = #When r then
+ if tm = #When r andalso not (#HasErrors r) andalso not (dContainsUndeterminedUnif (#Decl r)) then
SOME (#Decl r)
else
NONE)
@@ -138,12 +193,26 @@ fun lookup (d : Source.decl) =
(case SM.find (!byName, x) of
NONE => NONE
| SOME r =>
- if tm = #When r then
+ if tm = #When r andalso not (#HasErrors r) andalso not (dContainsUndeterminedUnif (#Decl r)) then
SOME (#Decl r)
else
NONE)
| _ => NONE
+fun lookupModAndDepsIncludingErrored name =
+ case SM.find (!byName, name) of
+ NONE => NONE
+ | SOME m =>
+ let
+ val deps = SS.listItems (#Deps m)
+ (* Clumsy way of adding Basis and Top without adding doubles *)
+ val deps = List.filter (fn x => x <> "Basis" andalso x <> "Top") deps
+ val deps = ["Basis", "Top"] @ deps
+ val foundDepModules = List.mapPartial (fn d => SM.find (!byName, d)) deps
+ in
+ SOME (#Decl m, List.map (fn a => #Decl a) foundDepModules)
+ end
+
val byNameBackup = ref (!byName)
val byIdBackup = ref (!byId)
diff --git a/src/prefix.cm b/src/prefix.cm
index 2e71d073..eab0bf71 100644
--- a/src/prefix.cm
+++ b/src/prefix.cm
@@ -4,4 +4,6 @@ $/basis.cm
$/smlnj-lib.cm
$smlnj/ml-yacc/ml-yacc-lib.cm
$/pp-lib.cm
+$(SRC)/bg_thread.sig
+$(SRC)/bg_thread.dummy.sml
diff --git a/src/prefix.mlb b/src/prefix.mlb
index 6a510481..13122fcf 100644
--- a/src/prefix.mlb
+++ b/src/prefix.mlb
@@ -3,5 +3,8 @@ local
$(SML_LIB)/smlnj-lib/Util/smlnj-lib.mlb
$(SML_LIB)/mlyacc-lib/mlyacc-lib.mlb
$(SML_LIB)/smlnj-lib/PP/pp-lib.mlb
+ $(SML_LIB)/basis/mlton.mlb
+ $(SRC)/bg_thread.sig
+ $(SRC)/bg_thread.mlton.sml
in
diff --git a/src/search.sig b/src/search.sig
index ac867146..2de85425 100644
--- a/src/search.sig
+++ b/src/search.sig
@@ -59,4 +59,9 @@ signature SEARCH = sig
* ('state11 -> 'state2 -> ('state11 * 'state2, 'abort) result)
-> (('state11 * 'state12) * 'state2, 'abort) result
+ val bindPWithPos :
+ (('state11 * 'state12) * 'state2, 'abort) result
+ * (('state11 * 'state12) -> 'state2 -> ('state11 * 'state2, 'abort) result)
+ -> (('state11 * 'state12) * 'state2, 'abort) result
+
end
diff --git a/src/search.sml b/src/search.sml
index 563496fe..5e4e135f 100644
--- a/src/search.sml
+++ b/src/search.sml
@@ -70,4 +70,12 @@ fun bindP (r, f) =
((x', pos), acc'))
| Return x => Return x
+fun bindPWithPos (r, f) =
+ case r of
+ Continue ((x, pos), acc) =>
+ map (f (x, pos) acc,
+ fn (x', acc') =>
+ ((x', pos), acc'))
+ | Return x => Return x
+
end
diff --git a/src/sources b/src/sources
index 851cdc16..74171365 100644
--- a/src/sources
+++ b/src/sources
@@ -69,6 +69,9 @@ $(SRC)/elab.sml
$(SRC)/elab_util.sig
$(SRC)/elab_util.sml
+$(SRC)/elab_util_pos.sig
+$(SRC)/elab_util_pos.sml
+
$(SRC)/elab_env.sig
$(SRC)/elab_env.sml
@@ -271,6 +274,20 @@ $(SRC)/checknest.sml
$(SRC)/compiler.sig
$(SRC)/compiler.sml
+$(SRC)/getinfo.sig
+$(SRC)/getinfo.sml
+
+$(SRC)/json.sig
+$(SRC)/json.sml
+
+$(SRC)/fromjson.sig
+$(SRC)/fromjson.sml
+
+$(SRC)/lspspec.sml
+
+$(SRC)/lsp.sig
+$(SRC)/lsp.sml
+
$(SRC)/demo.sig
$(SRC)/demo.sml