Add symbolic ranking support (#215)

.gitignore

@@ -2,6 +2,7 @@ Clean System Files/
 builddb
 CloogleServer
 *.1
+rank_settings.json
 types.json
 typetree.dot
 cloogle.log

Cloogle @ 196fee32

-Subproject commit 3ba4b6698a71e66aabbc8a2a065f5de8f8d57378
+Subproject commit 196fee3253b2e55d09fc990b371d2672a7b79134

backend/CloogleServer.icl

@@ -29,14 +29,17 @@ import Data.Maybe
 import Data.Tuple
 import System._Posix
 import System.CommandLine
+import System.File
 import System.Options
+import System.Process
 import System.Time
-from Text import class Text(concat,join,toLowerCase), instance Text String, <+
+from Text import class Text(concat,join,split,startsWith,toLowerCase), instance Text String, <+
 import Text.GenJSON
 
 import Cloogle.API
 import Cloogle.DB
 import Cloogle.Search
+import Cloogle.Search.Rank
 
 import Util.SimpleTCPServer
 import Util.Cache
@@ -60,8 +63,8 @@ CACHE_NS_THRESHOLD :== 20000000
 	  , c_page             :: Int
 	  }
 
-derive JSONEncode Kind, Type, RequestCacheKey, TypeRestriction
-derive JSONDecode Kind, Type, RequestCacheKey, TypeRestriction
+derive JSONEncode Kind, Type, RequestCacheKey, TypeRestriction, RankSettings
+derive JSONDecode Kind, Type, RequestCacheKey, TypeRestriction, RankSettings, RankConstraint
 instance toString RequestCacheKey
 where toString rck = toString $ toJSON rck
 
@@ -114,10 +117,11 @@ where
 	unprepareTR (Derivation g t) = Derivation g (unprepare t)
 
 :: Options =
-	{ port         :: !Int
-	, reload_cache :: !Bool
-	, test_file    :: !Maybe FilePath
-	, test_options :: ![TestOption]
+	{ port                      :: !Int
+	, reload_cache              :: !Bool
+	, rank_settings_constraints :: !Maybe FilePath
+	, test_file                 :: !Maybe FilePath
+	, test_options              :: ![TestOption]
 	}
 
 :: TestOption = NoUnify
@@ -125,10 +129,11 @@ where
 instance zero Options
 where
 	zero =
-		{ port         = 31215
-		, reload_cache = False
-		, test_file    = Nothing
-		, test_options = []
+		{ port                      = 31215
+		, reload_cache              = False
+		, rank_settings_constraints = Nothing
+		, test_file                 = Nothing
+		, test_options              = []
 		}
 
 optionDescription :: Option Options
@@ -145,6 +150,11 @@ optionDescription = WithHelp True $ Options
 		"--reload-cache"
 		(\opts -> Ok {opts & reload_cache=True})
 		"Reload the cache in the background"
+	, Option
+		"--rank-settings-constraints"
+		(\file opts -> Ok {opts & rank_settings_constraints=Just file})
+		"FILE"
+		"Output symbolic rank constraints in Z3 format based on test cases in FILE"
 	, Option
 		"--test"
 		(\file opts -> Ok {opts & test_file=Just file})
@@ -169,24 +179,21 @@ Start w
 #! (_,f,w) = fopen "types.json" FReadText w
 #! (db,f) = openDB f
 #! (ok,db) = isJustU db
-| not ok
-	# (io,w) = stdio w
-	# io = io <<< "Could not open database\n"
-	# (_,w) = fclose io w
-	= w
+| not ok = errexit "Could not open database\n" -1 w
+#! (_,w) = fclose f w
 #! db = hyperstrict (fromJust db)
+| isJust opts.rank_settings_constraints = computeRankConstraints (fromJust opts.rank_settings_constraints) db w
+#! (f,w) = readFile "rank_settings.json" w
+# rsets = fromJSON $ fromString $ fromOk f
+| isError f || isNothing rsets = errexit "Could not open rank settings\n" -1 w
+#! rsets = fromJust rsets
 | isJust opts.test_file
 	# (ok,f,w) = fopen (fromJust opts.test_file) FReadText w
-	| not ok
-		# (io,w) = stdio w
-		# io = io <<< "Could not open test file\n"
-		# (_,w) = fclose io w
-		= w
-	= test opts.test_options f db w
-#! (db,w) = if opts.reload_cache (doInBackground reloadCache) id (db,w)
-#! (_,w) = fclose f w
+	| not ok = errexit "Could not open test file\n" -1 w
+	= test opts.test_options rsets f db w
+#! (db,w) = if opts.reload_cache (doInBackground (reloadCache rsets)) id (db,w)
 = serve
-	{ handler           = handle
+	{ handler           = handle rsets
 	, logger            = Just log
 	, port              = opts.Options.port
 	, connect_timeout   = Just 3600000 // 1h
@@ -198,13 +205,16 @@ where
 	# (ok,w) = mlockall (MCL_CURRENT bitor MCL_FUTURE) w
 	| ok = w
 	# (err,w) = errno w
-	# (io,w) = stdio w
-	# io = io <<< "Could not lock memory (" <<< err <<< "); process may get swapped out\n"
-	= snd $ fclose io w
+	= snd $ fclose (stderr <<< "Could not lock memory (" <<< err <<< "); process may get swapped out\n") w
+
+errexit :: !String !Int !*World -> *World
+errexit msg rcode w
+# (_,w) = fclose (stderr <<< msg) w
+= setReturnCode rcode w
 
-handle :: !(Maybe Request) !*CloogleDB !*World -> *(!Response, !(!Maybe CacheKey, !MicroSeconds), !*CloogleDB, !*World)
-handle Nothing db w = (err InvalidInput "Couldn't parse input", (Nothing,0), db, w)
-handle (Just request=:{unify,name,page}) db w
+handle :: !RankSettings !(Maybe Request) !*CloogleDB !*World -> *(!Response, !(!Maybe CacheKey, !MicroSeconds), !*CloogleDB, !*World)
+handle _ Nothing db w = (err InvalidInput "Couldn't parse input", (Nothing,0), db, w)
+handle rsets (Just request=:{unify,name,page}) db w
 	#! (start,w) = nsTime w
 	//Check cache
 	#! (key,db) = toRequestCacheKey db request
@@ -222,7 +232,7 @@ handle (Just request=:{unify,name,page}) db w
 		= respond start Nothing (err InvalidInput "Empty query") db w
 	// Results
 	#! drop_n = fromJust (page <|> pure 0) * MAX_RESULTS
-	#! (res,suggs,db) = searchWithSuggestions request db
+	#! (res,suggs,db) = searchWithSuggestions rsets request db
 	#! suggs = if (isEmpty suggs) Nothing (Just suggs)
 	#! results = drop drop_n res
 	#! more = max 0 (length results - MAX_RESULTS)
@@ -271,8 +281,8 @@ where
 			}
 		(give,keep) = splitAt MAX_RESULTS results
 
-reloadCache :: !*(!*CloogleDB, !*World) -> *(!*CloogleDB, !*World)
-reloadCache (db,w)
+reloadCache :: !RankSettings !*(!*CloogleDB, !*World) -> *(!*CloogleDB, !*World)
+reloadCache rsets (db,w)
 # (ks,w) = allCacheKeys LongTerm w
 = loop ks db w
 where
@@ -280,7 +290,7 @@ where
 	loop [] db w = (db,w)
 	loop [k:ks] db w
 	# w = removeFromCache LongTerm k w
-	# (_,_,db,w) = handle (Just $ fromRequestCacheKey k) db w
+	# (_,_,db,w) = handle rsets (Just $ fromRequestCacheKey k) db w
 	# db = resetDB db
 	= loop ks db w
 
@@ -291,8 +301,8 @@ doInBackground f w
 | pid > 0   = w // Parent: return directly
 | otherwise = snd $ exit 0 $ f w // Child: do function
 
-test :: ![TestOption] !*File !*CloogleDB !*World -> *World
-test opts queries db w
+test :: ![TestOption] !RankSettings !*File !*CloogleDB !*World -> *World
+test opts rsets queries db w
 # (e,queries) = fend queries
 | e = w
 # (qstring,queries) = freadline queries
@@ -300,17 +310,71 @@ test opts queries db w
 # q = parseSingleLineRequest qstring
 | isError q
 	# w = snd $ fclose (stderr <<< "Warning: could not parse '" <<< qstring <<< "'; " <<< fromError q <<< "\n") w
-	= test opts queries db w
+	= test opts rsets queries db w
 # q = fromOk q
 | excluded opts q
-	= test opts queries db w
-# (_,_,db,w) = handle (Just q) db w
-= test opts queries db w
+	= test opts rsets queries db w
+# (_,_,db,w) = handle rsets (Just q) db w
+= test opts rsets queries db w
 where
 	excluded :: ![TestOption] !Request -> Bool
 	excluded []           _ = False
 	excluded [NoUnify:os] r = isJust r.unify || excluded os r
 
+computeRankConstraints :: !FilePath !*CloogleDB !*World -> *World
+computeRankConstraints constraintfile db w
+#! (f,w) = readFile constraintfile w
+# constraints = fromJSON $ fromString $ fromOk f
+| isError f || isNothing constraints = errexit "Could not open rank settings constraints\n" -1 w
+# constraints = fromJust constraints
+# (constraints,db) = rankConstraints constraints db
+# (z3,w) = runProcessIO "z3" ["-in"] Nothing w
+| isError z3 = errexit "Failed to run z3\n" -1 w
+# (z3h,z3io) = fromOk z3
+# z3input = join "\n" (constraints ++ ["(check-sat)","(get-model)","(exit)"]) +++ "\n"
+# (err,w) = writePipe z3input z3io.stdIn w
+| isError err = errexit "Failed to write constraints to z3\n" -1 w
+# (rcode,w) = waitForProcess z3h w
+| isError rcode || fromOk rcode <> 0
+	= errexit
+		("z3 failed to compute a model with these constraints:\n" +++ z3input)
+		-1 w
+# (out,w) = readPipeBlocking z3io.stdOut w
+| isError out = errexit "Failed to read z3 output\n" -1 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
+	}
+# (io,w) = stdio w
+# io = io <<< jsonPrettyPrint (toJSON settings) <<< "\n"
+# (_,w) = fclose io w
+= 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 (v % (4,size v-2))
+		# 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}
+		= findSettings ss rs
+	findSettings [s:ss] rs = findSettings ss rs
+	findSettings [] rs = rs
+
 :: LogMemory =
 	{ mem_ip         :: IPAddress
 	, mem_time_start :: Tm

backend/build.sh

 #!/bin/bash
-set -e
+set -ev
 
 install_clean.sh 'base lib-platform lib-tcpip' 2018-10-30
 
-PACKAGES="patch jq unzip"
+PACKAGES="patch jq unzip z3"
 apt-get update -qq
 apt-get install -qq $PACKAGES --no-install-recommends
 
@@ -11,8 +11,8 @@ make clean CloogleServer builddb
 
 if [ ! -f libs.json ]; then ln -s ../libs.json; fi
 ../util/fetch_libs.sh /opt/clean/lib
-echo "./builddb > types.json"
 ./builddb > types.json
+./CloogleServer --rank-settings-constraints rank_settings_constraints.json > rank_settings.json
 
 rm -rf \
 	Cloogle \

backend/rank_settings_constraints.json

+[ [{"name":"toInt"},          ["LT",["StdOverloaded","toInt"],   ["StdChar","digitToInt"]]]
+, [{"unify":"Char -> Int"},   ["LT",["StdChar","digitToInt"],    ["StdOverloaded","toInt"]]]
+, [{"unify":"Int -> String"}, ["LT",["StdOverloaded","fromInt"], ["StdOverloaded","one"]]]
+]

frontend/banners.json

@@ -29,5 +29,11 @@
 		"text": "<b>SoccerFun</b> users: be aware that to search for things in SoccerFun you need to enable '<b>include apps</b>' in the advanced search options.",
 		"from": "Thu, 4 Oct 2018 00:00:00 UTC",
 		"until": "Thu, 25 Oct 2018 00:00:00 UTC"
+	},
+	{
+		"id": "new-ranking",
+		"text": "Cloogle uses a <a href='https://gitlab.science.ru.nl/cloogle/cloogle-org/merge_requests/216' target='_blank'>new ranking function</a> which needs to learn from its mistakes. Please <a href='https://gitlab.science.ru.nl/cloogle/cloogle-org/issues/new' target='_blank'>report</a> any issues you see.",
+		"from": "Thu, 15 Nov 2018 00:00:00 UTC",
+		"until": "Thu, 29 Nov 2018 00:00:00 UTC"
 	}
 ]

util/update.sh

@@ -89,6 +89,7 @@ if [[ "$RELEASE_DIRECTORY" != "" ]]; then
 	sed 's/\x1b\[[0-9;]*m//g' /tmp/cloogle-build.log \
 		| sed -n '/^\.\/builddb /{:a;n;/^Execution: /{p;b};p;ba}' \
 		> "$THIS_RELEASE/build-log.txt"
+	timeout -k 10 10 sudo docker-compose exec -T backend cat rank_settings.json > "$THIS_RELEASE/rank_settings.json"
 	timeout -k 10 10 sudo docker-compose exec -T backend cat types.json > "$THIS_RELEASE/types.json"
 	timeout -k 10 10 sudo docker-compose exec -T backend cat typetree.dot > "$THIS_RELEASE/typetree.dot"
 fi