Rank.icl

implementation module Cloogle.Search.Rank

import StdArray
import StdBool
import StdInt
import StdList
import StdMisc
import StdReal
import StdString

import Clean.Types
import Data.Error
from Data.Func import $
import Data.Functor
from Data.List import foldr1
import qualified Data.Map as M
import Data.Maybe
import Data.Tuple
import System.Process
import Text

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

distance :: !RankSettings !CloogleEntry ![Annotation] -> Int
distance settings entry annots = let info = symbolicDistance entry annots 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_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 +
	settings.rs_used_synonyms      * info.rs_used_synonyms +
	settings.rs_resolved_context   * info.rs_resolved_context +
	settings.rs_unresolved_context * info.rs_unresolved_context +
	settings.rs_lib_stdenv         * info.rs_lib_stdenv

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
	, 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
	, rs_unifier_n_types    = ntype
	, rs_unifier_n_funcs    = nfunc
	, rs_unifier_n_conss    = ncons
	, rs_used_synonyms      = case [s \\ UsedSynonyms s <- annots] of [s:_] -> toReal s; _ -> 0.0
	, rs_resolved_context   = resolved_context
	, rs_unresolved_context = unresolved_context
	, rs_lib_stdenv         = if (getLocation entry)=:(Just (Location "StdEnv" _ _ _ _ _)) 1.0 0.0
	}
where
	(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)
	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)

	(ntype,nfunc,ncons) = case [unifier_sizes u \\ Unifier u <- annots] of
		[(nt,nf,nc):_] -> (toReal nt,toReal nf,toReal nc)
		_              -> (0.0,0.0,0.0)

	/**
	 * @result nr. of Type constructors
	 * @result nr. of Func constructors
	 * @result nr. of Cons constructors
	 */
	unifier_sizes :: !Unifier -> (!Int,!Int,!Int)
	unifier_sizes unif
	= count 0 0 0 [t \\ (_,t`) <- map fromUnifyingAssignment unif.assignments, t <- subtypes t`]
	where
		count :: !Int !Int !Int ![Type] -> (!Int,!Int,!Int)
		count nt nf nc [t:ts] = case t of
			Type _ _   -> count (nt+1) nf     nc     ts
			Func _ _ _ -> count nt     (nf+1) nc     ts
			Cons _ _   -> count nt     nf     (nc+1) ts
			_          -> count nt     nf     nc     ts
		count nt nf nc [] = (nt,nf,nc)

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"

findRankSettings :: ![(Request, RankConstraint)] !*CloogleDB !*World
	-> *(!MaybeError String RankSettings, *CloogleDB, !*World)
findRankSettings constraints cdb w
# (constraints,cdb) = rankConstraints constraints cdb
# (z3,w) = runProcessIO "z3" ["-in"] Nothing w
| isError z3 = (Error "Failed to run z3", cdb, 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", cdb, w)
# (rcode,w) = waitForProcess z3h w
| isError rcode || fromOk rcode <> 0
	= (Error ("z3 failed to compute a model with these constraints:\n" +++ z3input), cdb, w)
# (out,w) = readPipeBlocking z3io.stdOut w
| isError out = (Error "Failed to read z3 output", cdb, 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_n_types    = 0.0
	, rs_unifier_n_funcs    = 0.0
	, rs_unifier_n_conss    = 0.0
	, rs_used_synonyms      = 0.0
	, rs_resolved_context   = 0.0
	, rs_unresolved_context = 0.0
	, rs_lib_stdenv         = 0.0
	}
= (Ok settings, cdb, 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_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}
			"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

rankConstraints :: ![(Request, RankConstraint)] !*CloogleDB -> *([String], *CloogleDB)
rankConstraints constraints cdb
# (constraints,cdb) = findConstraints constraints cdb
= (default ++ constraints,cdb)
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_n_types    Real)"
		, "(declare-const rs_unifier_n_funcs    Real)"
		, "(declare-const rs_unifier_n_conss    Real)"
		, "(declare-const rs_used_synonyms      Real)"
		, "(declare-const rs_resolved_context   Real)"
		, "(declare-const rs_unresolved_context Real)"
		, "(declare-const rs_lib_stdenv         Real)"
		]

findConstraints :: ![(Request, RankConstraint)] !*CloogleDB -> *([String], *CloogleDB)
findConstraints [(req,LT urid1 urid2):rest] cdb
# (orgsearchtype,allsyns,usedsyns,entries,cdb) = search` req cdb
# (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
# this = "(assert (< (" +++ formula ri1 +++ ") (" +++ formula ri2 +++ ")))"
# cdb = resetDB cdb
# (rest,cdb) = findConstraints rest cdb
= ([this:rest],cdb)
where
	findEntry orgsearchtype allsyns usedsyns urid=:(mod,name) entries cdb
		= 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")

	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_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
		, "* rs_used_synonyms "      <+ ri.rs_used_synonyms
		, "* rs_resolved_context "   <+ ri.rs_resolved_context
		, "* rs_unresolved_context " <+ ri.rs_unresolved_context
		, "* rs_lib_stdenv "         <+ ri.rs_lib_stdenv
		]
	where
		sum :: [String] -> String
		sum [t] = t
		sum [t:ts]
		# s = sum ts
		= "+ (" +++ t +++ ") (" +++ s +++ ")"
findConstraints [] cdb = ([],cdb)