summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elab_util_pos.sig66
-rw-r--r--src/elab_util_pos.sml910
-rw-r--r--src/elaborate.sig6
-rw-r--r--src/elaborate.sml23
-rw-r--r--src/elisp/urweb-mode.el27
-rw-r--r--src/errormsg.sig5
-rw-r--r--src/errormsg.sml21
-rw-r--r--src/getinfo.sig31
-rw-r--r--src/getinfo.sml270
-rw-r--r--src/main.mlton.sml6
-rw-r--r--src/mod_db.sig5
-rw-r--r--src/mod_db.sml81
-rw-r--r--src/search.sig5
-rw-r--r--src/search.sml8
-rw-r--r--src/sources6
15 files changed, 1452 insertions, 18 deletions
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..03359814 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -47,4 +47,10 @@ 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)
+
end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 9718ccad..d5e190fa 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)
@@ -4757,6 +4763,8 @@ fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env
fun elabFile basis basis_tm topStr topSgn top_tm env 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), _)) =>
@@ -5121,11 +5129,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..4cf8b50a 100644
--- a/src/errormsg.sig
+++ b/src/errormsg.sig
@@ -48,6 +48,11 @@ 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
diff --git a/src/errormsg.sml b/src/errormsg.sml
index 8f3c93b1..eee20768 100644
--- a/src/errormsg.sml
+++ b/src/errormsg.sml
@@ -88,12 +88,31 @@ fun spanOf (pos1, pos2) = {file = !file,
val errors = ref false
+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 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, ":");
diff --git a/src/getinfo.sig b/src/getinfo.sig
new file mode 100644
index 00000000..317b7e79
--- /dev/null
+++ b/src/getinfo.sig
@@ -0,0 +1,31 @@
+(* 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
+ val getInfo: string (* file:row:col *) -> Print.PD.pp_desc
+end
+
diff --git a/src/getinfo.sml b/src/getinfo.sml
new file mode 100644
index 00000000..37c50928
--- /dev/null
+++ b/src/getinfo.sml
@@ -0,0 +1,270 @@
+(* 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
+structure P = Print
+
+fun isPosIn file row col span =
+ let
+ val start = #first span
+ val end_ = #last span
+ in
+ String.isSuffix file (#file span)
+ andalso
+ (#line start < row orelse
+ #line start = row andalso #char start <= col)
+ andalso
+ (#line end_ > row orelse
+ #line end_ = row andalso #char end_ >= col)
+
+ 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 * E.env) =
+ case #1 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 getInfo' file row col =
+ if not (!Elaborate.incremental)
+ then P.PD.string "ERROR: urweb daemon is needed to use typeOf command"
+ else
+ case ModDb.lookupModAndDepsIncludingErrored (Compiler.moduleOf file) of
+ NONE => P.PD.string ("ERROR: No module found: " ^ Compiler.moduleOf file)
+ | SOME (modDecl, deps) =>
+ let
+ val () = U.mliftConInCon := E.mliftConInCon
+
+ (* Adding signature of dependencies to environment *)
+ val env = List.foldl (fn (d, e) => E.declBinds e d) E.empty deps
+
+ (* Adding previous declarations in file to environment *)
+ (* "open <mod>" statements are already translated during elaboration *)
+ (* They get added to the env here "unprefixed" *)
+ val env =
+ case #1 modDecl of
+ L.DStr (name, _, sgn, str) =>
+ (case #1 str of
+ L.StrConst decls =>
+ List.foldl (fn (d, env) =>
+ if #line (#first (#2 d)) <= row
+ andalso #char (#first (#2 d)) <= col
+ then E.declBinds env d
+ else env) env decls
+ | _ => env)
+ | L.DFfiStr _ => env
+ | _ => env
+
+ (* Basis and Top need to be added to the env explicitly *)
+ val env =
+ case ModDb.lookupModAndDepsIncludingErrored "Top" of
+ NONE => raise Fail "ERROR: Top module not found in ModDb"
+ | SOME ((L.DStr (_, top_n, topSgn, topStr), _), _) =>
+ #2 (Elaborate.dopen env {str = top_n, strs = [], sgn = topSgn})
+ | _ => raise Fail "ERROR: Impossible"
+ val env =
+ case ModDb.lookupModAndDepsIncludingErrored "Basis" of
+ NONE => raise Fail "ERROR: Top module not found in ModDb"
+ | SOME ((L.DFfiStr (_, basis_n, sgn), _), _) =>
+ #2 (Elaborate.dopen env {str = basis_n, strs = [], sgn = sgn})
+ | _ => raise Fail "ERROR: Impossible"
+
+ (* Just use ElabPrint functions. *)
+ (* These are better for compiler error message, but it's better than nothing *)
+ fun printLiterally {span = span, item = item, env = env} =
+ P.box [ case item of
+ Kind k => P.box [P.PD.string "KIND: ", ElabPrint.p_kind env k]
+ | Con c => P.box [P.PD.string "CON: ", ElabPrint.p_con env c]
+ | Exp e => P.box [P.PD.string "EXP: ", ElabPrint.p_exp env e]
+ | Sgn_item si => P.box [P.PD.string "SGN_ITEM: ", ElabPrint.p_sgn_item env si]
+ | Sgn s => P.box [P.PD.string "SGN: ", ElabPrint.p_sgn env s]
+ | Str s => P.box [P.PD.string "STR: ", ElabPrint.p_str env s]
+ | Decl d => P.box [P.PD.string "DECL: ", ElabPrint.p_decl env d]
+ ]
+
+ (* TODO We lose some really useful information, like eg. inferred parameters, *)
+ (* which we do have in the actual items (L.Decl, L.Exp, etc) *)
+ (* but not when we do a lookup into the Env *)
+ (* TODO Rename? *)
+ fun printGoodPart env f span =
+ (case f of
+ Exp (L.EPrim p, _) =>
+ SOME (P.box [Prim.p_t p,
+ P.PD.string ": ",
+ P.PD.string (case p of
+ Prim.Int _ => "int"
+ | Prim.Float _ => "float"
+ | Prim.String _ => "string"
+ | Prim.Char _ => "char")])
+ | Exp (L.ERel n, _) =>
+ SOME ((let val found = E.lookupERel env n
+ in
+ P.box [ P.PD.string (#1 found)
+ , P.PD.string ": "
+ , ElabPrint.p_con env (#2 found)]
+ end)
+ handle E.UnboundRel _ => P.PD.string ("UNBOUND_REL" ^ Int.toString n))
+ | Exp (L.ENamed n, _) =>
+ SOME ((let val found = E.lookupENamed env n
+ in
+ P.box [ P.PD.string (#1 found)
+ , P.PD.string ": "
+ , ElabPrint.p_con env (#2 found)]
+ end)
+ handle E.UnboundNamed _ => P.PD.string ("UNBOUND_NAMED" ^ Int.toString n))
+ | Exp (L.EModProj ( m1 (* number (= "name") of top level module *)
+ , ms (* names of submodules - possibly none *)
+ , x (* identifier *)), loc) =>
+ SOME (let
+ val (m1name, m1sgn) = E.lookupStrNamed env m1
+ val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+ case E.projectStr env {sgn = sgn, str = str, field = m} of
+ NONE => raise Fail ("Couldn't find Structure: " ^ m)
+ | SOME sgn => ((L.StrProj (str, m), loc), sgn))
+ ((L.StrVar m1, loc), m1sgn)
+ ms
+ val t = case E.projectVal env {sgn = sgn, str = str, field = x} of
+ NONE => raise Fail ("Couldn't find identifier: " ^ x)
+ | SOME t => t
+ in
+ P.box [ P.p_list_sep (P.PD.string ".") P.PD.string (m1name :: ms @ [x])
+ , P.PD.string ": "
+ , ElabPrint.p_con env t
+ ]
+ end
+ handle E.UnboundNamed _ => P.PD.string ("Module not found: " ^ Int.toString m1))
+ | Exp e => NONE
+ | Kind k => NONE
+ | Con c => NONE
+ | Sgn_item si => NONE
+ | Sgn s => NONE
+ | Str s => NONE
+ | Decl d => NONE)
+
+ fun add env item span acc =
+ if not (isPosIn file row col span)
+ then
+ acc
+ else
+ let
+ val smallest =
+ if isSmallerThan span (#span (#smallest acc))
+ then {span = span, item = item, env = env}
+ else #smallest acc
+ val smallestgoodpart =
+ case #smallestgoodpart acc of
+ NONE =>
+ (case printGoodPart env item span of
+ NONE => NONE
+ | SOME desc => SOME (desc, span))
+ | SOME (desc', span') =>
+ if isSmallerThan span span'
+ then
+ (case printGoodPart env item span of
+ NONE => SOME (desc', span')
+ | SOME desc => SOME (desc, span))
+ else SOME (desc', span')
+ in
+ {smallest = smallest, smallestgoodpart = smallestgoodpart}
+ end
+
+ (* Look for item at input position *)
+ (* We're looking for two things simultaneously: *)
+ (* 1. The "smallest" part, ie. the one of which the source span is the smallest *)
+ (* 2. The "smallestgoodpart" part, ie. the one of which the source span is the smallest AND has a special case in printGoodPart *)
+ (* If we end up with a smallestgoodpart, we'll show that one since that one is probably more useful *)
+ (* TODO source spans of XML and SQL sources are weird and you end *)
+ (* up with eg: a span from eg 1-5 and another from 2-6, makes no sense? *)
+ (* That's one of the reasons why we're searching for the two things mentioned above *)
+ val result =
+ U.Decl.foldB
+ { kind = fn (env, (k, span), acc) => add env (Kind (k, span)) span acc,
+ con = fn (env, (k, span), acc) => add env (Con (k, span)) span acc,
+ exp = fn (env, (k, span), acc) => add env (Exp (k, span)) span acc,
+ sgn_item = fn (env, (k, span), acc) => add env (Sgn_item (k, span)) span acc,
+ sgn = fn (env, (k, span), acc) => add env (Sgn (k, span)) span acc,
+ str = fn (env, (k, span), acc) => add env (Str (k, span)) span acc,
+ decl = fn (env, (k, span), acc) => add env (Decl (k, span)) span 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
+ { smallestgoodpart = NONE
+ , smallest = { item = Decl (#1 modDecl, { file = file
+ , first = { line = 0, char = 0}
+ , last = { line = 99999, char = 0} })
+ , span = { file = file
+ , first = { line = 0, char = 0}
+ , last = { line = 99999, char = 0} }
+ , env = env }
+ }
+ modDecl
+ in
+ case #smallestgoodpart result of
+ NONE => printLiterally (#smallest result)
+ | SOME (desc, span) => desc
+ end
+
+fun getInfo loc =
+ case String.tokens (fn ch => ch = #":") loc of
+ file :: rowStr :: colStr :: nil =>
+ (case (Int.fromString rowStr, Int.fromString colStr) of
+ (SOME row, SOME col) => getInfo' file row col
+ | _ => P.PD.string "ERROR: Wrong typeOf input format, should be <file:row:col>")
+ | _ => P.PD.string "ERROR: Wrong typeOf input format, should be <file:row:col>"
+end
diff --git a/src/main.mlton.sml b/src/main.mlton.sml
index a6eaa7ea..7f8540f2 100644
--- a/src/main.mlton.sml
+++ b/src/main.mlton.sml
@@ -141,6 +141,10 @@ fun oneRun args =
fun printModuleOf fname =
print_and_exit (Compiler.moduleOf fname) ()
+ fun getInfo loc =
+ (Print.print (GetInfo.getInfo loc);
+ raise Code OS.Process.success)
+
fun add_class (class, num) =
case Int.fromString num of
NONE => raise Fail ("Invalid limit number '" ^ num ^ "'")
@@ -247,6 +251,8 @@ fun oneRun args =
NONE),
("moduleOf", ONE ("<file>", printModuleOf),
SOME "print module name of <file> and exit"),
+ ("getInfo", ONE ("<file:row:col>", getInfo),
+ SOME "print info of expression at <file:row:col> and exit"),
("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/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..20d77483 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,9 @@ $(SRC)/checknest.sml
$(SRC)/compiler.sig
$(SRC)/compiler.sml
+$(SRC)/getinfo.sig
+$(SRC)/getinfo.sml
+
$(SRC)/demo.sig
$(SRC)/demo.sml
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 06:25:24 +0000