Rank.icl 7.38 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 14 15 16 17 18
from Data.Func import $
import Data.Functor
from Data.List import foldr1
import qualified Data.Map as M
import Data.Maybe
import Data.Tuple
19
import System.Process
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
import Text

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

distance :: !RankSettings !CloogleEntry !(Map AnnotationKey Int) !(Maybe TypeRankInfo) -> Int
distance settings entry annots tri = let info = symbolicDistance entry annots tri in toInt $
	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_size       * info.rs_unifier_size +
	settings.rs_used_synonyms      * info.rs_used_synonyms +
	settings.rs_resolved_context   * info.rs_resolved_context +
35 36
	settings.rs_unresolved_context * info.rs_unresolved_context +
	settings.rs_lib_stdenv         * info.rs_lib_stdenv
37 38 39 40 41

symbolicDistance :: !CloogleEntry !(Map AnnotationKey Int) !(Maybe TypeRankInfo) -> RankInformation
symbolicDistance entry annots tri =
	{ rs_ngram_distance     = fromMaybe 0.0 $ toReal <$> 'M'.get NGramDistance annots
	, rs_exact_result       = fromMaybe 0.0 $ toReal <$> 'M'.get ExactResult annots
42 43
	, 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
44 45 46 47
	, rs_unifier_size       = fromMaybe 0.0 $ toReal <$> 'M'.get UnifierSize annots
	, rs_used_synonyms      = case tri of Nothing -> 0.0; Just tri -> toReal $ length tri.tri_used_synonyms
	, rs_resolved_context   = resolved_context
	, rs_unresolved_context = unresolved_context
48
	, rs_lib_stdenv         = if (getLocation entry)=:(Just (Location "StdEnv" _ _ _ _ _)) 1.0 0.0
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
	}
where
	(resolved_context,unresolved_context) = case tri of
		Just {tri_required_context=Just 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)

match :: !UniqueResultIdentifier !CloogleEntry -> Bool
match (mod,name) ce = 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"

68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
findRankSettings :: ![(Request, RankConstraint)] !*CloogleDB !*World
	-> *(!MaybeError String RankSettings, *CloogleDB, !*World)
findRankSettings constraints db w
# (constraints,db) = rankConstraints constraints db
# (z3,w) = runProcessIO "z3" ["-in"] Nothing w
| isError z3 = (Error "Failed to run z3", db, w)
# (z3h,z3io) = fromOk z3
# z3input = join "\n" (constraints ++ ["(check-sat)","(get-model)","(exit)"]) +++ "\n"
# (err,w) = writePipe z3input z3io.stdIn w
| isError err = (Error "Failed to write constraints to z3", db, w)
# (rcode,w) = waitForProcess z3h w
| isError rcode || fromOk rcode <> 0
	= (Error ("z3 failed to compute a model with these constraints:\n" +++ z3input), db, w)
# (out,w) = readPipeBlocking z3io.stdOut w
| isError out = (Error "Failed to read z3 output", db, 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_size       = 0.0
	, rs_used_synonyms      = 0.0
	, rs_resolved_context   = 0.0
	, rs_unresolved_context = 0.0
	, rs_lib_stdenv         = 0.0
	}
= (Ok settings, db, 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_size"       -> {rs & rs_unifier_size      =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

116 117 118 119 120 121 122 123 124 125 126 127 128 129
rankConstraints :: ![(Request, RankConstraint)] !*CloogleDB -> *([String], *CloogleDB)
rankConstraints constraints db
# (constraints,db) = findConstraints constraints db
= (default ++ constraints,db)
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_size       Real)"
		, "(declare-const rs_used_synonyms      Real)"
		, "(declare-const rs_resolved_context   Real)"
		, "(declare-const rs_unresolved_context Real)"
130
		, "(declare-const rs_lib_stdenv         Real)"
131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168
		]

findConstraints :: ![(Request, RankConstraint)] !*CloogleDB -> *([String], *CloogleDB)
findConstraints [(req,LT urid1 urid2):rest] cdb
# (orgsearchtype,allsyns,usedsyns,entries,cdb) = search` req cdb
# (e1,annots1) = case filter (\(e,_) -> match urid1 e) entries of
	[e1:[]] -> e1
	[]      -> abort "no match for URID 1\n"
	_       -> abort "too many matches for URID 1\n"
# (e2,annots2) = case filter (\(e,_) -> match urid2 e) entries of
	[e2:[]] -> e2
	[]      -> abort "no match for URID 2\n"
	_       -> abort "too many matches for URID 2\n"
# (ri1,cdb) = case e1 of
	FunctionEntry fe
		#  (unif,usedsyns,required_context,cdb) = unifyInformation orgsearchtype allsyns usedsyns fe cdb
		-> (symbolicDistance e1 annots1 (Just {tri_used_synonyms=usedsyns,tri_required_context=required_context}), cdb)
	_   -> (symbolicDistance e1 annots1 Nothing, cdb)
# (ri2,cdb) = case e2 of
	FunctionEntry fe
		#  (unif,usedsyns,required_context,cdb) = unifyInformation orgsearchtype allsyns usedsyns fe cdb
		-> (symbolicDistance e2 annots2 (Just {tri_used_synonyms=usedsyns,tri_required_context=required_context}), cdb)
	_   -> (symbolicDistance e2 annots2 Nothing, cdb)
# this = "(assert (< (" +++ formula ri1 +++ ") (" +++ formula ri2 +++ ")))"
# cdb = resetDB cdb
# (rest,cdb) = findConstraints rest cdb
= ([this:rest],cdb)
where
	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_size "       <+ ri.rs_unifier_size
		, "* rs_used_synonyms "      <+ ri.rs_used_synonyms
		, "* rs_resolved_context "   <+ ri.rs_resolved_context
		, "* rs_unresolved_context " <+ ri.rs_unresolved_context
169
		, "* rs_lib_stdenv "         <+ ri.rs_lib_stdenv
170 171 172 173 174 175 176 177
		]
	where
		sum :: [String] -> String
		sum [t] = t
		sum [t:ts]
		# s = sum ts
		= "+ (" +++ t +++ ") (" +++ s +++ ")"
findConstraints [] cdb = ([],cdb)