Save hints to TTC files

And process them on loading. We record that hints need saving out when
adding them, and clear that list unless we happen to be reexporting the
thing we've just read (import public).

src/Core/Binary.idr

@@ -145,6 +145,7 @@ readTTCFile modns as r b
            defs <- fromBuf r b
            autohs <- fromBuf r b
            typehs <- fromBuf r b
+--            coreLift $ putStrLn ("Hints: " ++ show typehs)
 --            coreLift $ putStrLn $ "Read " ++ show (length (map fullname defs)) ++ " defs"
            imp <- fromBuf r b
            nextv <- fromBuf r b
@@ -192,8 +193,8 @@ writeToTTC extradata fname
                               (toList (guesses ust)) 
                               (toList (constraints ust))
                               gdefs
-                              (toList (autoHints defs))
-                              (typeHints defs)
+                              (saveAutoHints defs)
+                              (saveTypeHints defs)
                               (imported defs)
                               (nextName ust)
                               (currentNS defs)
@@ -214,6 +215,14 @@ addGlobalDef modns as def
          addDef (asName modns as n) def
          pure ()
 
+addTypeHint : {auto c : Ref Ctxt Defs} ->
+              FC -> (Name, Name, Bool) -> Core ()
+addTypeHint fc (tyn, hintn, d) = addHintFor fc tyn hintn d
+
+addAutoHint : {auto c : Ref Ctxt Defs} ->
+              (Name, Bool) -> Core ()
+addAutoHint (hintn, d) = addGlobalHint hintn d
+
 -- Add definitions from a binary file to the current context
 -- Returns the "extra" section of the file (user defined data), the interface
 -- hash and the list of additional TTCs that need importing
@@ -247,8 +256,11 @@ readFromTTC loc reexp fname modNS importAs
          ttc <- readTTCFile modNS as r bin
          traverse (addGlobalDef modNS as) (context ttc)
          setNS (currentNS ttc)
-         -- TODO: Set up typeHints and autoHints properly
+         -- Set up typeHints and autoHints based on the loaded data
+         traverse_ (addTypeHint loc) (typeHints ttc)
+         traverse_ addAutoHint (autoHints ttc)
          -- TODO: Set up pair/rewrite etc names, name directives
+         when (not reexp) clearSavedHints
          resetFirstEntry
 
          -- Finally, update the unification state with the holes from the

src/Core/Context.idr

@@ -464,7 +464,7 @@ record Defs where
   openHints : NameMap ()
      -- ^ currently open global hints; just for the rest of this module (not exported)
      -- and prioritised
-  typeHints : List (Name, Name, Bool)
+  saveTypeHints : List (Name, Name, Bool)
      -- ^ a mapping from type names to hints (and a flag setting whether it's 
      -- a "direct" hint). Direct hints are searched first (as part of a group)
      -- the indirect hints. Indirect hints, in practice, are used to find
@@ -472,6 +472,7 @@ record Defs where
      -- tried to find a direct result via a constructor or a top level hint.
      -- We don't look up anything in here, it's merely for saving out to TTC.
      -- We save the hints in the 'GlobalDef' itself for faster lookup.
+  saveAutoHints : List (Name, Bool)
   ifaceHash : Int
   importHashes : List (List String, Int)
      -- ^ interface hashes of imported modules
@@ -493,7 +494,7 @@ initDefs : Core Defs
 initDefs 
     = do gam <- initCtxt
          pure (MkDefs gam ["Main"] defaults empty 100 
-                      empty empty [] 5381 [] [] [])
+                      empty empty [] [] 5381 [] [] [])
       
 -- Label for context references
 export
@@ -794,6 +795,9 @@ addHintFor fc tyn hintn_in direct
          Just (TCon t a ps dets cons hs) <- lookupDefExact tyn (gamma defs)
               | _ => throw (GenericMsg fc (show tyn ++ " is not a type constructor"))
          updateDef tyn (const (Just (TCon t a ps dets cons ((hintn, direct) :: hs))))
+         defs <- get Ctxt
+         put Ctxt (record { saveTypeHints $= ((tyn, hintn, direct) :: )
+                          } defs)
 
 export
 addGlobalHint : {auto c : Ref Ctxt Defs} ->
@@ -806,7 +810,8 @@ addGlobalHint hintn_in isdef
                     _ => case getNameID hintn_in (gamma defs) of
                               Nothing => hintn_in
                               Just idx => Resolved idx
-         put Ctxt (record { autoHints $= insert hintn isdef } defs)
+         put Ctxt (record { autoHints $= insert hintn isdef,
+                            saveAutoHints $= ((hintn, isdef) ::) } defs)
 
 export
 addOpenHint : {auto c : Ref Ctxt Defs} -> Name -> Core ()
@@ -820,6 +825,13 @@ addOpenHint hintn_in
                               Just idx => Resolved idx
          put Ctxt (record { openHints $= insert hintn () } defs)
 
+export
+clearSavedHints : {auto c : Ref Ctxt Defs} -> Core ()
+clearSavedHints
+    = do defs <- get Ctxt
+         put Ctxt (record { saveTypeHints = [],
+                            saveAutoHints = [] } defs)
+
 -- Set the default namespace for new definitions
 export
 setNS : {auto c : Ref Ctxt Defs} ->

src/TTImp/ProcessData.idr

@@ -141,7 +141,7 @@ processData eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
 
          traverse_ (processDataOpt fc (Resolved tidx)) opts
          when (not (NoHints `elem` opts)) $
-              traverse_ (\x => addHintFor fc n x True) (map conName cons)
+              traverse_ (\x => addHintFor fc (Resolved tidx) x True) (map conName cons)
 
          -- TODO: Interface hash
          

tests/ttimp/basic008/expected

@@ -3,3 +3,11 @@ Written TTC
 Yaffle> 94
 Yaffle> 94
 Yaffle> Bye for now!
+Processing as TTC
+Read 0 holes
+Read 0 guesses
+Read 0 constraints
+Read TTC
+Yaffle> 94
+Yaffle> 94
+Yaffle> Bye for now!

tests/ttimp/basic008/run

@@ -1,3 +1,4 @@
 $1 Auto.yaff < input
+$1 build/Auto.ttc < input
 
 rm -rf build