From 80e7bb6165a5ad6517b35f301228f56b58eef39c Mon Sep 17 00:00:00 2001 From: FrigoEU Date: Wed, 31 Jul 2019 15:13:18 +0200 Subject: first iteration of "typeOf" command --- src/compiler.sig | 1 + src/compiler.sml | 187 +++++++++++ src/elab_util_pos.sig | 63 ++++ src/elab_util_pos.sml | 910 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/main.mlton.sml | 6 + src/mod_db.sig | 2 + src/mod_db.sml | 9 + src/search.sig | 5 + src/search.sml | 8 + src/sources | 3 + 10 files changed, 1194 insertions(+) create mode 100644 src/elab_util_pos.sig create mode 100644 src/elab_util_pos.sml diff --git a/src/compiler.sig b/src/compiler.sig index 6ed2f9a6..7f724b0f 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -215,6 +215,7 @@ signature COMPILER = sig val addModuleRoot : string * string -> unit val moduleOf : string -> string + val typeOf : string -> Print.PD.pp_desc val setStop : string -> unit (* Stop compilation after this phase. *) diff --git a/src/compiler.sml b/src/compiler.sml index 0aba3a40..46a035ee 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -1781,4 +1781,191 @@ fun moduleOf fname = end end +fun isPosIn row col span = + let + val start = #first span + val end_ = #last span + in + ((#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 foundStuff = + Kind of Elab.kind + | Con of Elab.con + | Exp of Elab.exp + | Sgn_item of Elab.sgn_item + | Sgn of Elab.sgn + | Str of Elab.str + | Decl of Elab.decl + +fun getSpan (f: foundStuff * ElabEnv.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 getTypeAt file row col = + if not (!Elaborate.incremental) + then Print.PD.string "ERROR: urweb daemon is needed to use typeOf command" + else + case ModDb.lookupForTooling (moduleOf file) of + NONE => Print.PD.string ("ERROR: No module found: " ^ moduleOf file) + | SOME (decl, deps) => + let + (* TODO Top is not always found as a dep *) + val () = ElabUtilPos.mliftConInCon := ElabEnv.mliftConInCon + (* Adding dependencies to environment *) + val env = List.foldl (fn (d, e) => ElabEnv.declBinds e d) + ElabEnv.empty + deps + (* Adding previous declarations to environment *) + val env = + case #1 decl of + Elab.DStr (name, _, sgn, str) => + (case #1 str of + Elab.StrConst decls => + List.foldl + (fn (d, e) => ElabEnv.declBinds e d) + env + decls + | _ => env) + | Elab.DFfiStr _ => env + | _ => env + (* Look for item under cursor *) + val (atPosition, env) = + ElabUtilPos.Decl.foldB + { kind = fn (env, (k, span), acc) => + if isPosIn row col span andalso isSmallerThan span (getSpan acc) + then (Kind (k, span), env) + else acc , + con = fn (env, (k, span), acc) => + if isPosIn row col span andalso isSmallerThan span (getSpan acc) + then (Con (k, span), env) + else acc, + exp = fn (env, (k, span), acc) => + if isPosIn row col span andalso isSmallerThan span (getSpan acc) + then (Exp (k, span), env) + else acc, + sgn_item = fn (env, (k, span), acc) => + if isPosIn row col span andalso isSmallerThan span (getSpan acc) + then (Sgn_item (k, span), env) + else acc, + sgn = fn (env, (k, span), acc) => + if isPosIn row col span andalso isSmallerThan span (getSpan acc) + then (Sgn (k, span), env) + else acc, + str = fn (env, (k, span), acc) => + if isPosIn row col span andalso isSmallerThan span (getSpan acc) + then (Str (k, span), env) + else acc, + decl = fn (env, (k, span), acc) => + if isPosIn row col span andalso isSmallerThan span (getSpan acc) + then (Decl (k, span), env) + else acc, + bind = fn (env, binder) => + case binder of + ElabUtilPos.Decl.RelK x => + ElabEnv.pushKRel env x + | ElabUtilPos.Decl.RelC (x, k) => + ElabEnv.pushCRel env x k + | ElabUtilPos.Decl.NamedC (x, n, k, co) => + ElabEnv.pushCNamedAs env x n k co + | ElabUtilPos.Decl.RelE (x, c) => + ElabEnv.pushERel env x c + | ElabUtilPos.Decl.NamedE (x, c) => + #1 (ElabEnv.pushENamed env x c) + | ElabUtilPos.Decl.Str (x, n, sgn) => + #1 (ElabEnv.pushStrNamed env x sgn) + | ElabUtilPos.Decl.Sgn (x, n, sgn) => + #1 (ElabEnv.pushSgnNamed env x sgn) + } + env + (Decl (#1 decl, { file = file + , first = { line = 0, char = 0} + , last = { line = 99999, char = 0} }) + , env) + decl + in + case atPosition of + Kind k => + Print.box [Print.PD.string "Not implemented yet, KIND: ", ElabPrint.p_kind env k] + | Con c => + Print.box [Print.PD.string "Not implemented yet, CON: ", ElabPrint.p_con env c] + | Exp (Elab.EPrim p, _) => + Print.box [Prim.p_t p, + Print.PD.string ": ", + Print.PD.string (case p of + Prim.Int _ => "int" + | Prim.Float _ => "float" + | Prim.String _ => "string" + | Prim.Char _ => "char")] + | Exp (Elab.ERel n, _) => + ((let val found = ElabEnv.lookupERel env n + in + + Print.box [ Print.PD.string (#1 found) + , Print.PD.string ": " + , ElabPrint.p_con env (#2 found)] + end) + handle ElabEnv.UnboundRel _ => Print.PD.string ("UNBOUND_REL" ^ Int.toString n)) + | Exp (Elab.ENamed n, _) => + ((let val found = ElabEnv.lookupENamed env n + in + Print.box [ Print.PD.string (#1 found) + , Print.PD.string ": " + , ElabPrint.p_con env (#2 found)] + end) + handle ElabEnv.UnboundNamed _ => Print.PD.string ("UNBOUND_NAMED" ^ Int.toString n)) + | Exp (Elab.EModProj ( m1 (* number (= "name") of top level module *) + , ms (* names of submodules - possibly none *) + , x (* identifier *)), loc) => + (let + val (m1name, m1sgn) = ElabEnv.lookupStrNamed env m1 + val (str, sgn) = foldl (fn (m, (str, sgn)) => + case ElabEnv.projectStr env {sgn = sgn, str = str, field = m} of + NONE => raise Fail ("Couldn't find Structure: " ^ m) + | SOME sgn => ((Elab.StrProj (str, m), loc), sgn)) + ((Elab.StrVar m1, loc), m1sgn) + ms + val t = case ElabEnv.projectVal env {sgn = sgn, str = str, field = x} of + NONE => raise Fail ("Couldn't find identifier: " ^ x) + | SOME t => t + in + Print.box [ Print.p_list_sep (Print.PD.string ".") Print.PD.string (m1name :: ms @ [x]) + , Print.PD.string ": " + , ElabPrint.p_con env t + ] + end + handle ElabEnv.UnboundNamed _ => Print.PD.string ("Module not found: " ^ Int.toString m1)) + | Exp e => Print.box [Print.PD.string "Not implemented yet, EXP: ", ElabPrint.p_exp env e] + | Sgn_item si => Print.box [Print.PD.string "Not implemented yet, SGN_ITEM: ", ElabPrint.p_sgn_item env si] + | Sgn s => Print.box [Print.PD.string "Not implemented yet, SGN: ", ElabPrint.p_sgn env s] + | Str s => Print.box [Print.PD.string "Not implemented yet, STR: ", ElabPrint.p_str env s] + | Decl d => Print.box [Print.PD.string "Not implemented yet, DECL: ", ElabPrint.p_decl env d] + end + + +fun typeOf 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) => + Print.box [getTypeAt file row col, Print.PD.string "\n"] + | _ => Print.PD.string "ERROR: Wrong typeOf input format, should be ") + | _ => Print.PD.string "ERROR: Wrong typeOf input format, should be " end diff --git a/src/elab_util_pos.sig b/src/elab_util_pos.sig new file mode 100644 index 00000000..f616f7f3 --- /dev/null +++ b/src/elab_util_pos.sig @@ -0,0 +1,63 @@ +(* 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. + *) + +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/main.mlton.sml b/src/main.mlton.sml index cb7c8a77..8e70e398 100644 --- a/src/main.mlton.sml +++ b/src/main.mlton.sml @@ -139,6 +139,10 @@ fun oneRun args = fun printModuleOf fname = print_and_exit (Compiler.moduleOf fname) () + fun typeOf loc = + (Print.print (Compiler.typeOf loc); + raise Code OS.Process.success) + fun add_class (class, num) = case Int.fromString num of NONE => raise Fail ("Invalid limit number '" ^ num ^ "'") @@ -245,6 +249,8 @@ fun oneRun args = NONE), ("moduleOf", ONE ("", printModuleOf), SOME "print module name of and exit"), + ("typeOf", ONE ("", typeOf), + SOME "print type of expression at and exit"), ("noEmacs", set_true Demo.noEmacs, NONE), ("limit", TWO ("", "", add_class), diff --git a/src/mod_db.sig b/src/mod_db.sig index c45fd203..40cd52e2 100644 --- a/src/mod_db.sig +++ b/src/mod_db.sig @@ -36,6 +36,8 @@ signature MOD_DB = sig val lookup : Source.decl -> Elab.decl option + val lookupForTooling : 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 de428570..fdf6d5ab 100644 --- a/src/mod_db.sml +++ b/src/mod_db.sml @@ -207,6 +207,15 @@ fun lookup (d : Source.decl) = NONE) | _ => NONE +fun lookupForTooling name = + case SM.find (!byName, name) of + NONE => NONE + | SOME m => + SOME (#Decl m, List.map (fn a => #Decl a) + (List.mapPartial + (fn d => SM.find (!byName, d)) + (SS.listItems (#Deps m)))) + 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..e25ccd2e 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 -- cgit v1.2.3