Rank.icl 9.78 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 31
distance :: !RankSettings !CloogleEntry ![Annotation] -> Maybe Real
distance _ _ annots | not (isEmpty [a \\ a=:ExactResult <- annots]) = Nothing
distance settings entry annots = let info = symbolicDistance entry annots in Just $
32 33
	settings.rs_matching_ngrams_q  * info.rs_matching_ngrams_q +
	settings.rs_matching_ngrams_r  * info.rs_matching_ngrams_r +
34 35
	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
	settings.rs_resolved_context   * info.rs_resolved_context +
41 42
	settings.rs_unresolved_context * info.rs_unresolved_context +
	settings.rs_lib_stdenv         * info.rs_lib_stdenv
43

44 45
symbolicDistance :: !CloogleEntry ![Annotation] -> RankInformation
symbolicDistance entry annots =
46 47
	{ 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
48 49
	, 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
50 51 52
	, rs_unifier_n_types    = ntype
	, rs_unifier_n_funcs    = nfunc
	, rs_unifier_n_conss    = ncons
53
	, rs_unifier_n_args     = nargs
54 55
	, rs_resolved_context   = resolved_context
	, rs_unresolved_context = unresolved_context
56
	, rs_lib_stdenv         = if (getLocation entry)=:(Just (Location "StdEnv" _ _ _ _ _)) 1.0 0.0
57 58
	}
where
59 60 61
	(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)
62 63 64 65 66 67 68
	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)

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

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

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

108 109
findRankSettings :: ![(Request, RankConstraint)] !*CloogleDB !*World
	-> *(!MaybeError String RankSettings, *CloogleDB, !*World)
110 111
findRankSettings constraints cdb w
# (constraints,cdb) = rankConstraints constraints cdb
112
# (z3,w) = runProcessIO "z3" ["-in"] Nothing w
113
| isError z3 = (Error "Failed to run z3", cdb, w)
114
# (z3h,z3io) = fromOk z3
115
# z3input = join "\n" (constraints ++ ["(set-option :pp.decimal true)","(check-sat)","(get-model)","(exit)"]) +++ "\n"
116
# (err,w) = writePipe z3input z3io.stdIn w
117
| isError err = (Error "Failed to write constraints to z3", cdb, w)
118 119
# (rcode,w) = waitForProcess z3h w
| isError rcode || fromOk rcode <> 0
120
	= (Error ("z3 failed to compute a model with these constraints:\n" +++ z3input), cdb, w)
121
# (out,w) = readPipeBlocking z3io.stdOut w
122
| isError out = (Error "Failed to read z3 output", cdb, w)
123 124
# out = split "\n" $ fromOk out
# settings = findSettings out
125 126
	{ rs_matching_ngrams_q  = 0.0
	, rs_matching_ngrams_r  = 0.0
127 128
	, rs_record_field       = 0.0
	, rs_constructor        = 0.0
129 130 131
	, rs_unifier_n_types    = 0.0
	, rs_unifier_n_funcs    = 0.0
	, rs_unifier_n_conss    = 0.0
132
	, rs_unifier_n_args     = 0.0
133 134 135 136
	, 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
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
145 146
			"rs_matching_ngrams_q"  -> {rs & rs_matching_ngrams_q =val}
			"rs_matching_ngrams_r"  -> {rs & rs_matching_ngrams_r =val}
147 148
			"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
			"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

160
rankConstraints :: ![(Request, RankConstraint)] !*CloogleDB -> *([String], *CloogleDB)
161
rankConstraints constraints cdb
162
# (constraints,cdb) = findConstraints constraints 'M'.newMap cdb
163
= (default ++ constraints,cdb)
164 165
where
	default =
166 167
		[ "(declare-const rs_matching_ngrams_q  Real)"
		, "(declare-const rs_matching_ngrams_r  Real)"
168 169
		, "(declare-const rs_record_field       Real)"
		, "(declare-const rs_constructor        Real)"
170 171 172
		, "(declare-const rs_unifier_n_types    Real)"
		, "(declare-const rs_unifier_n_funcs    Real)"
		, "(declare-const rs_unifier_n_conss    Real)"
173
		, "(declare-const rs_unifier_n_args     Real)"
174 175
		, "(declare-const rs_resolved_context   Real)"
		, "(declare-const rs_unresolved_context Real)"
176
		, "(declare-const rs_lib_stdenv         Real)"
177 178
		]

179 180 181 182 183 184 185 186 187 188 189 190
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
191 192 193 194
# (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
195 196
# this = "(assert (< (" +++ formula ri1 +++ ") (" +++ formula ri2 +++ ")))"
# cdb = resetDB cdb
197
# (rest,cdb) = findConstraints rest results cdb
198 199
= ([this:rest],cdb)
where
200
	findEntry orgsearchtype allsyns usedsyns urid=:(_,mod,name) entries cdb
201 202 203 204 205 206 207 208 209 210 211 212 213
		= 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")

214 215
	formula :: !RankInformation -> String
	formula ri = sum
216 217
		[ "* rs_matching_ngrams_q "  <+ ri.rs_matching_ngrams_q
		, "* rs_matching_ngrams_r "  <+ ri.rs_matching_ngrams_r
218 219
		, "* rs_record_field "       <+ ri.rs_record_field
		, "* rs_constructor "        <+ ri.rs_constructor
220 221 222
		, "* 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
223
		, "* rs_unifier_n_args "     <+ ri.rs_unifier_n_args
224 225
		, "* rs_resolved_context "   <+ ri.rs_resolved_context
		, "* rs_unresolved_context " <+ ri.rs_unresolved_context
226
		, "* rs_lib_stdenv "         <+ ri.rs_lib_stdenv
227 228 229 230 231 232 233
		]
	where
		sum :: [String] -> String
		sum [t] = t
		sum [t:ts]
		# s = sum ts
		= "+ (" +++ t +++ ") (" +++ s +++ ")"
234
findConstraints [] _ cdb = ([],cdb)