Rank.icl 10 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 33 34
	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 +
35 36 37
	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 +
38
	settings.rs_unifier_n_args     * info.rs_unifier_n_args +
39 40
	settings.rs_used_synonyms      * info.rs_used_synonyms +
	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 46 47
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
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
	, rs_used_synonyms      = case [s \\ UsedSynonyms s <- annots] of [s:_] -> toReal s; _ -> 0.0
55 56
	, rs_resolved_context   = resolved_context
	, rs_unresolved_context = unresolved_context
57
	, rs_lib_stdenv         = if (getLocation entry)=:(Just (Location "StdEnv" _ _ _ _ _)) 1.0 0.0
58 59
	}
where
60 61 62
	(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)
63 64 65 66 67 68 69
	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)

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

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

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

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

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

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

218 219 220 221 222 223
	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
224 225 226
		, "* 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
227
		, "* rs_unifier_n_args "     <+ ri.rs_unifier_n_args
228 229 230
		, "* rs_used_synonyms "      <+ ri.rs_used_synonyms
		, "* rs_resolved_context "   <+ ri.rs_resolved_context
		, "* rs_unresolved_context " <+ ri.rs_unresolved_context
231
		, "* rs_lib_stdenv "         <+ ri.rs_lib_stdenv
232 233 234 235 236 237 238
		]
	where
		sum :: [String] -> String
		sum [t] = t
		sum [t:ts]
		# s = sum ts
		= "+ (" +++ t +++ ") (" +++ s +++ ")"
239
findConstraints [] _ cdb = ([],cdb)