diff options
Diffstat (limited to 'src/getinfo.sml')
-rw-r--r-- | src/getinfo.sml | 304 |
1 files changed, 304 insertions, 0 deletions
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 |