Rank.dcl 1.78 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
definition module Cloogle.Search.Rank

from Clean.Types import :: TypeDef
from Data.Map import :: Map
from Data.Maybe import :: Maybe

from Cloogle.API import :: Request, :: LocationResult, :: FunctionKind
from Cloogle.DB import :: AnnotationKey, :: CloogleEntry, :: CloogleDB

:: TypeRankInfo =
	{ tri_required_context :: !Maybe [(String, [LocationResult])]
	, tri_used_synonyms    :: ![TypeDef]
	}

/**
 * A rank is computed as the weighted sum of various metrics. The coefficients
 * are given by this record.
 */
:: RankSettings =
	{ rs_ngram_distance     :: !Real //* n-gram distance
	, rs_exact_result       :: !Real //* results with an exact match
	, rs_record_field       :: !Real //* record fields
	, rs_constructor        :: !Real //* constructors
	, rs_unifier_size       :: !Real //* large unifiers
	, rs_used_synonyms      :: !Real //* the number of synonyms required
	, rs_resolved_context   :: !Real //* class contexts with known instances
	, rs_unresolved_context :: !Real //* class contexts without known instances
	}

/**
 * This record is the same as {{`RankSettings`}}, but the members are
 * interpreted as the values rather than the weights.
 */
:: RankInformation :== RankSettings

distance :: !RankSettings !CloogleEntry !(Map AnnotationKey Int) !(Maybe TypeRankInfo) -> Int

symbolicDistance :: !CloogleEntry !(Map AnnotationKey Int) !(Maybe TypeRankInfo) -> RankInformation

:: RankConstraint
	= LT !UniqueResultIdentifier !UniqueResultIdentifier //* arg1 should have lower distance than arg2

/**
 * @representation module name and name of element
 */
:: UniqueResultIdentifier :== (!String, !String)

/**
 * Generate Z3 constraints based on a set of constraints on the order of
 * results for queries.
 */
rankConstraints :: ![(Request, RankConstraint)] !*CloogleDB -> *([String], *CloogleDB)