Rank.icl 9.53 KB
Newer Older
1 2
implementation module Cloogle.Search.Rank

3
import StdArray
4 5 6 7 8 9 10 11
import StdBool
import StdInt
import StdList
import StdMisc
import StdReal
import StdString

import Clean.Types
12
import Data.Error
13
from Data.Foldable import class Foldable(foldr1)
14 15
from Data.Func import $
import Data.Functor
16
from Data.List import instance Foldable []
17 18 19
import qualified Data.Map as M
import Data.Maybe
import Data.Tuple
20
import System.Process
21 22 23 24 25 26
import Text

import Cloogle.API
import Cloogle.DB
import Cloogle.Search

27 28
distance :: !RankSettings !CloogleEntry ![Annotation] -> Real
distance settings entry annots = let info = symbolicDistance entry annots in
29 30 31 32
	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 +
33 34 35
	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 +
36
	settings.rs_unifier_n_args     * info.rs_unifier_n_args +
37 38
	settings.rs_used_synonyms      * info.rs_used_synonyms +
	settings.rs_resolved_context   * info.rs_resolved_context +
39 40
	settings.rs_unresolved_context * info.rs_unresolved_context +
	settings.rs_lib_stdenv         * info.rs_lib_stdenv
41

42 43 44 45
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
46 47
	, 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
48 49 50
	, rs_unifier_n_types    = ntype
	, rs_unifier_n_funcs    = nfunc
	, rs_unifier_n_conss    = ncons
51
	, rs_unifier_n_args     = nargs
52
	, rs_used_synonyms      = case [s \\ UsedSynonyms s <- annots] of [s:_] -> toReal s; _ -> 0.0
53 54
	, rs_resolved_context   = resolved_context
	, rs_unresolved_context = unresolved_context
55
	, rs_lib_stdenv         = if (getLocation entry)=:(Just (Location "StdEnv" _ _ _ _ _)) 1.0 0.0
56 57
	}
where
58 59 60
	(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)
61 62 63 64 65 66 67
	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)

68 69 70
	(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)
71 72 73 74 75 76

	/**
	 * @result nr. of Type constructors
	 * @result nr. of Func constructors
	 * @result nr. of Cons constructors
	 */
77
	unifier_sizes :: !Unifier -> (!Int,!Int,!Int,!Int)
78
	unifier_sizes unif
79
	= count 0 0 0 0 [t \\ (_,t`) <- map fromUnifyingAssignment unif.assignments, t <- subtypes t`]
80
	where
81 82 83 84 85 86 87
		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)
88

89
match :: !UniqueResultIdentifier !CloogleEntry -> Bool
90 91 92
match (thing,mod,name) ce
| thing <> descriptorName ce = False
| otherwise = case getLocation ce of
93 94 95
	Just (Location _ cemod _ _ _ cename) -> mod == cemod && name == cename
	Just (Builtin cename _)              -> mod == "_builtin" && name == cename
	_                                    -> abort "error in match of UniqueResultIdentifier\n"
96 97 98 99 100 101 102 103 104 105
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"
106

107 108
findRankSettings :: ![(Request, RankConstraint)] !*CloogleDB !*World
	-> *(!MaybeError String RankSettings, *CloogleDB, !*World)
109 110
findRankSettings constraints cdb w
# (constraints,cdb) = rankConstraints constraints cdb
111
# (z3,w) = runProcessIO "z3" ["-in"] Nothing w
112
| isError z3 = (Error "Failed to run z3", cdb, w)
113
# (z3h,z3io) = fromOk z3
114
# z3input = join "\n" (constraints ++ ["(set-option :pp.decimal true)","(check-sat)","(get-model)","(exit)"]) +++ "\n"
115
# (err,w) = writePipe z3input z3io.stdIn w
116
| isError err = (Error "Failed to write constraints to z3", cdb, w)
117 118
# (rcode,w) = waitForProcess z3h w
| isError rcode || fromOk rcode <> 0
119
	= (Error ("z3 failed to compute a model with these constraints:\n" +++ z3input), cdb, w)
120
# (out,w) = readPipeBlocking z3io.stdOut w
121
| isError out = (Error "Failed to read z3 output", cdb, w)
122 123 124 125 126 127
# 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
128 129 130
	, rs_unifier_n_types    = 0.0
	, rs_unifier_n_funcs    = 0.0
	, rs_unifier_n_conss    = 0.0
131
	, rs_unifier_n_args     = 0.0
132 133 134 135 136
	, rs_used_synonyms      = 0.0
	, rs_resolved_context   = 0.0
	, rs_unresolved_context = 0.0
	, rs_lib_stdenv         = 0.0
	}
137
= (Ok settings, cdb, w)
138 139 140 141 142 143 144 145 146 147 148
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}
149 150 151
			"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}
152
			"rs_unifier_n_args"     -> {rs & rs_unifier_n_args    =val}
153 154 155 156 157 158 159 160
			"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

161
rankConstraints :: ![(Request, RankConstraint)] !*CloogleDB -> *([String], *CloogleDB)
162 163 164
rankConstraints constraints cdb
# (constraints,cdb) = findConstraints constraints cdb
= (default ++ constraints,cdb)
165 166 167 168 169 170
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)"
171 172 173
		, "(declare-const rs_unifier_n_types    Real)"
		, "(declare-const rs_unifier_n_funcs    Real)"
		, "(declare-const rs_unifier_n_conss    Real)"
174
		, "(declare-const rs_unifier_n_args     Real)"
175 176 177
		, "(declare-const rs_used_synonyms      Real)"
		, "(declare-const rs_resolved_context   Real)"
		, "(declare-const rs_unresolved_context Real)"
178
		, "(declare-const rs_lib_stdenv         Real)"
179 180 181 182 183
		]

findConstraints :: ![(Request, RankConstraint)] !*CloogleDB -> *([String], *CloogleDB)
findConstraints [(req,LT urid1 urid2):rest] cdb
# (orgsearchtype,allsyns,usedsyns,entries,cdb) = search` req cdb
184 185 186 187
# (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
188 189 190 191 192
# this = "(assert (< (" +++ formula ri1 +++ ") (" +++ formula ri2 +++ ")))"
# cdb = resetDB cdb
# (rest,cdb) = findConstraints rest cdb
= ([this:rest],cdb)
where
193
	findEntry orgsearchtype allsyns usedsyns urid=:(_,mod,name) entries cdb
194 195 196 197 198 199 200 201 202 203 204 205 206
		= 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")

207 208 209 210 211 212
	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
213 214 215
		, "* 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
216
		, "* rs_unifier_n_args "     <+ ri.rs_unifier_n_args
217 218 219
		, "* rs_used_synonyms "      <+ ri.rs_used_synonyms
		, "* rs_resolved_context "   <+ ri.rs_resolved_context
		, "* rs_unresolved_context " <+ ri.rs_unresolved_context
220
		, "* rs_lib_stdenv "         <+ ri.rs_lib_stdenv
221 222 223 224 225 226 227 228
		]
	where
		sum :: [String] -> String
		sum [t] = t
		sum [t:ts]
		# s = sum ts
		= "+ (" +++ t +++ ") (" +++ s +++ ")"
findConstraints [] cdb = ([],cdb)