implementation module Cloogle.Search.Rank import StdArray import StdBool import StdInt import StdList import StdMisc import StdReal import StdString import Clean.Types import Data.Error from Data.Foldable import class Foldable(foldr1) from Data.Func import $ import Data.Functor from Data.GenLexOrd import :: LexOrd, generic gLexOrd import qualified Data.GenLexOrd from Data.List import instance Foldable [] import qualified Data.Map as M import Data.Maybe import Data.Tuple import System.Process import Text import Cloogle.API import Cloogle.DB import Cloogle.Search distance :: !RankSettings !CloogleEntry ![Annotation] -> Real distance settings entry annots = let info = symbolicDistance entry annots in settings.rs_ngram_distance * info.rs_ngram_distance + settings.rs_exact_result * info.rs_exact_result + settings.rs_record_field * info.rs_record_field + settings.rs_constructor * info.rs_constructor + settings.rs_unifier_n_types * info.rs_unifier_n_types + settings.rs_unifier_n_funcs * info.rs_unifier_n_funcs + settings.rs_unifier_n_conss * info.rs_unifier_n_conss + settings.rs_unifier_n_args * info.rs_unifier_n_args + settings.rs_used_synonyms * info.rs_used_synonyms + settings.rs_resolved_context * info.rs_resolved_context + settings.rs_unresolved_context * info.rs_unresolved_context + settings.rs_lib_stdenv * info.rs_lib_stdenv symbolicDistance :: !CloogleEntry ![Annotation] -> RankInformation symbolicDistance entry annots = { rs_ngram_distance = case [d \\ NGramDistance d <- annots] of [d:_] -> toReal d; _ -> 0.0 , rs_exact_result = if (isEmpty [a \\ a=:ExactResult <- annots]) 0.0 1.0 , rs_record_field = if entry=:(FunctionEntry {fe_kind=RecordField}) 1.0 0.0 , rs_constructor = if entry=:(FunctionEntry {fe_kind=Constructor}) 1.0 0.0 , rs_unifier_n_types = ntype , rs_unifier_n_funcs = nfunc , rs_unifier_n_conss = ncons , rs_unifier_n_args = nargs , rs_used_synonyms = case [s \\ UsedSynonyms s <- annots] of [s:_] -> toReal s; _ -> 0.0 , rs_resolved_context = resolved_context , rs_unresolved_context = unresolved_context , rs_lib_stdenv = if (getLocation entry)=:(Just (Location "StdEnv" _ _ _ _ _)) 1.0 0.0 } where (resolved_context,unresolved_context) = case [rc \\ RequiredContext (Just rc) <- annots] of [rc] -> let (res,unres) = context_sizes 0 0 rc in (toReal res,toReal unres) _ -> (0.0,0.0) where context_sizes :: !Int !Int ![(String,[LocationResult])] -> (!Int, !Int) context_sizes res unres [(_,locs):rest] | locs=:[] = context_sizes res (unres+1) rest | otherwise = context_sizes (res+1) unres rest context_sizes res unres [] = (res,unres) (ntype,nfunc,ncons,nargs) = case [unifier_sizes u \\ Unifier u <- annots] of [(nt,nf,nc,na):_] -> (toReal nt,toReal nf,toReal nc,toReal na) _ -> (0.0,0.0,0.0,0.0) /** * @result nr. of Type constructors * @result nr. of Func constructors * @result nr. of Cons constructors */ unifier_sizes :: !Unifier -> (!Int,!Int,!Int,!Int) unifier_sizes unif = count 0 0 0 0 [t \\ (_,t`) <- map fromUnifyingAssignment unif.assignments, t <- subtypes t`] where count :: !Int !Int !Int !Int ![Type] -> (!Int,!Int,!Int,!Int) count nt nf nc na [t:ts] = case t of Type _ as -> count (nt+1) nf nc (na+length as) ts Func _ _ _ -> count nt (nf+1) nc na ts Cons _ as -> count nt nf (nc+1) (na+length as) ts _ -> count nt nf nc na ts count nt nf nc na [] = (nt,nf,nc,na) match :: !UniqueResultIdentifier !CloogleEntry -> Bool match (thing,mod,name) ce | thing <> descriptorName ce = False | otherwise = case getLocation ce of Just (Location _ cemod _ _ _ cename) -> mod == cemod && name == cename Just (Builtin cename _) -> mod == "_builtin" && name == cename _ -> abort "error in match of UniqueResultIdentifier\n" where descriptorName :: !CloogleEntry -> String descriptorName (FunctionEntry _) = "Function" descriptorName (TypeDefEntry _) = "TypeDef" descriptorName (ModuleEntry _) = "Module" descriptorName (ClassEntry _) = "Class" descriptorName (InstanceEntry _) = "Instance" descriptorName (DeriveEntry _) = "Derive" descriptorName (SyntaxEntry _) = "Syntax" descriptorName (ABCInstructionEntry _) = "ABCInstruction" findRankSettings :: ![(Request, RankConstraint)] !*CloogleDB !*World -> *(!MaybeError String RankSettings, *CloogleDB, !*World) findRankSettings constraints cdb w # (constraints,cdb) = rankConstraints constraints cdb # (z3,w) = runProcessIO "z3" ["-in"] Nothing w | isError z3 = (Error "Failed to run z3", cdb, w) # (z3h,z3io) = fromOk z3 # z3input = join "\n" (constraints ++ ["(set-option :pp.decimal true)","(check-sat)","(get-model)","(exit)"]) +++ "\n" # (err,w) = writePipe z3input z3io.stdIn w | isError err = (Error "Failed to write constraints to z3", cdb, w) # (rcode,w) = waitForProcess z3h w | isError rcode || fromOk rcode <> 0 = (Error ("z3 failed to compute a model with these constraints:\n" +++ z3input), cdb, w) # (out,w) = readPipeBlocking z3io.stdOut w | isError out = (Error "Failed to read z3 output", cdb, w) # out = split "\n" $ fromOk out # settings = findSettings out { rs_ngram_distance = 0.0 , rs_exact_result = 0.0 , rs_record_field = 0.0 , rs_constructor = 0.0 , rs_unifier_n_types = 0.0 , rs_unifier_n_funcs = 0.0 , rs_unifier_n_conss = 0.0 , rs_unifier_n_args = 0.0 , rs_used_synonyms = 0.0 , rs_resolved_context = 0.0 , rs_unresolved_context = 0.0 , rs_lib_stdenv = 0.0 } = (Ok settings, cdb, w) where findSettings :: ![String] !RankSettings -> RankSettings findSettings [s:v:ss] rs | startsWith " (define-fun " s # name = s % (14,size s-9) // strip off ' (define-fun ' and ' () Real' # val = toReal {#c \\ c <-: v | isDigit c || c == '.' || c == '-'} # rs = case name of "rs_ngram_distance" -> {rs & rs_ngram_distance =val} "rs_exact_result" -> {rs & rs_exact_result =val} "rs_record_field" -> {rs & rs_record_field =val} "rs_constructor" -> {rs & rs_constructor =val} "rs_unifier_n_types" -> {rs & rs_unifier_n_types =val} "rs_unifier_n_funcs" -> {rs & rs_unifier_n_funcs =val} "rs_unifier_n_conss" -> {rs & rs_unifier_n_conss =val} "rs_unifier_n_args" -> {rs & rs_unifier_n_args =val} "rs_used_synonyms" -> {rs & rs_used_synonyms =val} "rs_resolved_context" -> {rs & rs_resolved_context =val} "rs_unresolved_context" -> {rs & rs_unresolved_context=val} "rs_lib_stdenv" -> {rs & rs_lib_stdenv =val} = findSettings ss rs findSettings [s:ss] rs = findSettings ss rs findSettings [] rs = rs rankConstraints :: ![(Request, RankConstraint)] !*CloogleDB -> *([String], *CloogleDB) rankConstraints constraints cdb # (constraints,cdb) = findConstraints constraints 'M'.newMap cdb = (default ++ constraints,cdb) where default = [ "(declare-const rs_ngram_distance Real)" , "(declare-const rs_exact_result Real)" , "(declare-const rs_record_field Real)" , "(declare-const rs_constructor Real)" , "(declare-const rs_unifier_n_types Real)" , "(declare-const rs_unifier_n_funcs Real)" , "(declare-const rs_unifier_n_conss Real)" , "(declare-const rs_unifier_n_args Real)" , "(declare-const rs_used_synonyms Real)" , "(declare-const rs_resolved_context Real)" , "(declare-const rs_unresolved_context Real)" , "(declare-const rs_lib_stdenv Real)" ] derive gLexOrd Request, Maybe instance < Request where < a b = (gLexOrd{|*|} a b)=:'Data.GenLexOrd'.LT findConstraints :: ![(Request, RankConstraint)] !(Map Request (!Maybe Type,!Map String [TypeDef],![TypeDef],![(!CloogleEntry,![Annotation])])) !*CloogleDB -> *([String], *CloogleDB) findConstraints [(req,LT urid1 urid2):rest] results cdb # (orgsearchtype,allsyns,usedsyns,entries,cdb) = case 'M'.get req results of Just (t,as,us,es) -> (t,as,us,es,cdb) _ -> search` req cdb # results = 'M'.put req (orgsearchtype,allsyns,usedsyns,entries) results # (e1,annots1,cdb) = findEntry orgsearchtype allsyns usedsyns urid1 entries cdb # (e2,annots2,cdb) = findEntry orgsearchtype allsyns usedsyns urid2 entries cdb # ri1 = symbolicDistance e1 annots1 # ri2 = symbolicDistance e2 annots2 # this = "(assert (< (" +++ formula ri1 +++ ") (" +++ formula ri2 +++ ")))" # cdb = resetDB cdb # (rest,cdb) = findConstraints rest results cdb = ([this:rest],cdb) where findEntry orgsearchtype allsyns usedsyns urid=:(_,mod,name) entries cdb = case filter (\(e,_) -> match urid e) entries of [(e1=:FunctionEntry fe,annots):[]] # (unif,usedsyns,required_context,cdb) = unifyInformation orgsearchtype allsyns usedsyns fe cdb # annots = [RequiredContext required_context,UsedSynonyms (length usedsyns):annots] # annots = case unif of Just unif -> [Unifier unif:annots] Nothing -> annots -> (e1,annots,cdb) [(e1,annots):[]] -> (e1,annots,cdb) [] -> abort ("no match for URID " +++ mod +++ "." +++ name +++ "\n") _ -> abort ("too many matches for URID " +++ mod +++ "." +++ name +++ "\n") formula :: !RankInformation -> String formula ri = sum [ "* rs_ngram_distance " <+ ri.rs_ngram_distance , "* rs_exact_result " <+ ri.rs_exact_result , "* rs_record_field " <+ ri.rs_record_field , "* rs_constructor " <+ ri.rs_constructor , "* rs_unifier_n_types " <+ ri.rs_unifier_n_types , "* rs_unifier_n_funcs " <+ ri.rs_unifier_n_funcs , "* rs_unifier_n_conss " <+ ri.rs_unifier_n_conss , "* rs_unifier_n_args " <+ ri.rs_unifier_n_args , "* rs_used_synonyms " <+ ri.rs_used_synonyms , "* rs_resolved_context " <+ ri.rs_resolved_context , "* rs_unresolved_context " <+ ri.rs_unresolved_context , "* rs_lib_stdenv " <+ ri.rs_lib_stdenv ] where sum :: [String] -> String sum [t] = t sum [t:ts] # s = sum ts = "+ (" +++ t +++ ") (" +++ s +++ ")" findConstraints [] _ cdb = ([],cdb)