Rank.icl 10.4 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 17
from Data.GenLexOrd import :: LexOrd, generic gLexOrd
import qualified Data.GenLexOrd
18
from Data.List import instance Foldable []
19 20 21
import qualified Data.Map as M
import Data.Maybe
import Data.Tuple
22
import System.Process
23 24 25 26 27 28
import Text

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

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

45 46
symbolicDistance :: !CloogleEntry ![Annotation] -> RankInformation
symbolicDistance entry annots =
47 48
	{ rs_matching_ngrams_q  = case [r \\ MatchingNGramsQuery r <- annots] of [r:_] -> r; _ -> 0.0
	, rs_matching_ngrams_r  = case [r \\ MatchingNGramsResult r <- annots] of [r:_] -> r; _ -> 0.0
49
	, rs_exact_result       = if (isEmpty [a \\ a=:ExactResult <- annots]) 0.0 1.0
50 51
	, 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
52 53 54
	, rs_unifier_n_types    = ntype
	, rs_unifier_n_funcs    = nfunc
	, rs_unifier_n_conss    = ncons
55
	, rs_unifier_n_args     = nargs
56
	, rs_used_synonyms      = case [s \\ UsedSynonyms s <- annots] of [s:_] -> toReal s; _ -> 0.0
57 58
	, rs_resolved_context   = resolved_context
	, rs_unresolved_context = unresolved_context
59
	, rs_lib_stdenv         = if (getLocation entry)=:(Just (Location "StdEnv" _ _ _ _ _)) 1.0 0.0
60 61
	}
where
62 63 64
	(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)
65 66 67 68 69 70 71
	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)

72 73 74
	(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)
75 76 77 78 79 80

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

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

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

167
rankConstraints :: ![(Request, RankConstraint)] !*CloogleDB -> *([String], *CloogleDB)
168
rankConstraints constraints cdb
169
# (constraints,cdb) = findConstraints constraints 'M'.newMap cdb
170
= (default ++ constraints,cdb)
171 172
where
	default =
173 174
		[ "(declare-const rs_matching_ngrams_q  Real)"
		, "(declare-const rs_matching_ngrams_r  Real)"
175 176 177
		, "(declare-const rs_exact_result       Real)"
		, "(declare-const rs_record_field       Real)"
		, "(declare-const rs_constructor        Real)"
178 179 180
		, "(declare-const rs_unifier_n_types    Real)"
		, "(declare-const rs_unifier_n_funcs    Real)"
		, "(declare-const rs_unifier_n_conss    Real)"
181
		, "(declare-const rs_unifier_n_args     Real)"
182 183 184
		, "(declare-const rs_used_synonyms      Real)"
		, "(declare-const rs_resolved_context   Real)"
		, "(declare-const rs_unresolved_context Real)"
185
		, "(declare-const rs_lib_stdenv         Real)"
186 187
		]

188 189 190 191 192 193 194 195 196 197 198 199
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
200 201 202 203
# (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
204 205
# this = "(assert (< (" +++ formula ri1 +++ ") (" +++ formula ri2 +++ ")))"
# cdb = resetDB cdb
206
# (rest,cdb) = findConstraints rest results cdb
207 208
= ([this:rest],cdb)
where
209
	findEntry orgsearchtype allsyns usedsyns urid=:(_,mod,name) entries cdb
210 211 212 213 214 215 216 217 218 219 220 221 222
		= 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")

223 224
	formula :: !RankInformation -> String
	formula ri = sum
225 226
		[ "* rs_matching_ngrams_q "  <+ ri.rs_matching_ngrams_q
		, "* rs_matching_ngrams_r "  <+ ri.rs_matching_ngrams_r
227 228 229
		, "* rs_exact_result "       <+ ri.rs_exact_result
		, "* rs_record_field "       <+ ri.rs_record_field
		, "* rs_constructor "        <+ ri.rs_constructor
230 231 232
		, "* 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
233
		, "* rs_unifier_n_args "     <+ ri.rs_unifier_n_args
234 235 236
		, "* rs_used_synonyms "      <+ ri.rs_used_synonyms
		, "* rs_resolved_context "   <+ ri.rs_resolved_context
		, "* rs_unresolved_context " <+ ri.rs_unresolved_context
237
		, "* rs_lib_stdenv "         <+ ri.rs_lib_stdenv
238 239 240 241 242 243 244
		]
	where
		sum :: [String] -> String
		sum [t] = t
		sum [t:ts]
		# s = sum ts
		= "+ (" +++ t +++ ") (" +++ s +++ ")"
245
findConstraints [] _ cdb = ([],cdb)