Add support for symbolic ranking (cloogle-org#215)

Cloogle/DB.icl

@@ -50,9 +50,9 @@ import Cloogle.API
 
 instance == AnnotationKey
 where
-	== NGramDistance NGramDistance = True
-	== UnifierSize UnifierSize = True
-	== _ _ = False
+	== NGramDistance k = k=:NGramDistance
+	== UnifierSize   k = k=:UnifierSize
+	== ExactResult   k = k=:ExactResult
 
 derive gLexOrd AnnotationKey
 instance < AnnotationKey where < a b = (a =?= b) === LT

Cloogle/Search.dcl

@@ -4,9 +4,14 @@ definition module Cloogle.Search
  * Search functions for the Cloogle system
  */
 
+from Clean.Types import :: TypeDef, :: Type, :: Unifier
 from Database.Native import :: NativeDB
-from Cloogle.API import :: Request, :: Result
-from Cloogle.DB import :: CloogleDB, :: AnnotationKey, :: CloogleEntry
+from Data.Map import :: Map
+from Data.Maybe import :: Maybe
+
+from Cloogle.API import :: Request, :: Result, :: LocationResult
+from Cloogle.DB import :: CloogleDB, :: AnnotationKey, :: CloogleEntry, :: FunctionEntry
+from Cloogle.Search.Rank import :: RankSettings
 
 /**
  * Cloogle setting: whether to include language builtins if the Request has
@@ -29,10 +34,21 @@ DEFAULT_INCLUDE_APPS :== False
 /**
  * Search for a request in the type database
  */
-search :: !Request !*CloogleDB -> *([Result], *CloogleDB)
+search :: !RankSettings !Request !*CloogleDB -> *([Result], *CloogleDB)
+
+search` :: !Request !*CloogleDB ->
+	*(!Maybe Type
+	, !(Map String [TypeDef])
+	, ![TypeDef]
+	, ![(!CloogleEntry, !Map AnnotationKey Int)]
+	, !*CloogleDB
+	)
+
+unifyInformation :: !(Maybe Type) !(Map String [TypeDef]) ![TypeDef] !FunctionEntry !*CloogleDB
+	-> *(!Maybe Unifier, ![TypeDef], !Maybe [(!String, ![LocationResult])], !*CloogleDB)
 
 /**
  * Search for a request, and also make suggestions for similar requests with
  * better results.
  */
-searchWithSuggestions :: !Request !*CloogleDB -> *([Result], [(Request,[Result])], *CloogleDB)
+searchWithSuggestions :: !RankSettings !Request !*CloogleDB -> *([Result], [(Request,[Result])], *CloogleDB)

Cloogle/Search/Rank.dcl

+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)

Cloogle/Search/Rank.icl

+implementation module Cloogle.Search.Rank
+
+import StdBool
+import StdInt
+import StdList
+import StdMisc
+import StdReal
+import StdString
+
+import Clean.Types
+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 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 +
+	settings.rs_unresolved_context * info.rs_unresolved_context
+
+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
+	, rs_record_field       = case entry of FunctionEntry {fe_kind=k=:RecordField} -> 1.0; _ -> 0.0
+	, rs_constructor        = case entry of FunctionEntry {fe_kind=k=:Constructor} -> 1.0; _ -> 0.0
+	, 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
+	}
+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"
+
+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)"
+		]
+
+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
+		]
+	where
+		sum :: [String] -> String
+		sum [t] = t
+		sum [t:ts]
+		# s = sum ts
+		= "+ (" +++ t +++ ") (" +++ s +++ ")"
+findConstraints [] cdb = ([],cdb)