Improve auto search to support interfaces

Parser now allows options on data types and functions, and elaborator
processes options so we can set up interfaces

src/Core/AutoSearch.idr

@@ -203,6 +203,7 @@ searchLocalWith {vars} fc rigc defaults depth def top env ((prf, ty) :: rest) ta
              -- We can only use the local if its type is not an unsolved hole
              if !(usableLocal fc defaults env ty)
                 then do
+                   logNF 10 "Trying " env ty
                    ures <- unify InTerm fc env target appTy
                    let [] = constraints ures
                        | _ => throw (CantSolveGoal fc [] top)
@@ -211,7 +212,8 @@ searchLocalWith {vars} fc rigc defaults depth def top env ((prf, ty) :: rest) ta
                    logTermNF 10 "Candidate " env candidate
                    traverse (searchIfHole fc defaults False depth def top env) args
                    pure candidate
-                else throw (CantSolveGoal fc [] top)
+                else do logNF 10 "Can't use " env ty
+                        throw (CantSolveGoal fc [] top)
 
     findPos : Defs -> Term vars -> 
               (Term vars -> Term vars) ->
@@ -364,7 +366,9 @@ searchType {vars} fc rigc defaults depth def top env target
                              sd <- getSearchData fc defaults tyn
                              -- Check determining arguments are okay for 'args' 
                              concreteDets fc defaults env top 0 (detArgs sd) args
-                             tryGroups nty (hintGroups sd)
+                             tryUnify
+                               (searchLocal fc rigc defaults depth def top env nty)
+                               (tryGroups nty (hintGroups sd))
                      else throw (CantSolveGoal fc [] top)
               _ => do logNF 10 "Next target: " env nty
                       searchLocal fc rigc defaults depth def top env nty
@@ -389,11 +393,12 @@ searchType {vars} fc rigc defaults depth def top env target
 --          (defaults : Bool) -> (depth : Nat) ->
 --          (defining : Name) -> (topTy : Term vars) -> Env Term vars -> 
 --          Core (Term vars)
-Core.Unify.search fc rigc defaults depth def top env
+Core.Unify.search fc rigc defaults depth def top_in env
     = do defs <- get Ctxt
+         top <- normaliseScope defs env top_in
          logTerm 10 "Initial target: " top
          tm <- searchType fc rigc defaults depth def 
                           (abstractEnvType fc env top) env 
-                          !(normaliseScope defs env top)
+                          top
          defs <- get Ctxt
          quote defs env tm

src/Core/Value.idr

@@ -75,3 +75,17 @@ mutual
        NErased  : FC -> NF vars
        NType    : FC -> NF vars
 
+export
+getLoc : NF vars -> FC
+getLoc (NBind fc _ _ _) = fc
+getLoc (NApp fc _ _) = fc
+getLoc (NDCon fc _ _ _ _) = fc
+getLoc (NTCon fc _ _ _ _) = fc
+getLoc (NAs fc _ _) = fc
+getLoc (NDelayed fc _ _) = fc
+getLoc (NDelay fc _ _ _) = fc
+getLoc (NForce fc _) = fc
+getLoc (NPrimVal fc _) = fc
+getLoc (NErased fc) = fc
+getLoc (NType fc) = fc
+

src/TTImp/Elab.idr

@@ -73,7 +73,7 @@ elabTermSub defining mode opts nest env env' sub tm ty
          -- Linearity and hole checking.
          -- on the LHS, all holes need to have been solved
          chktm <- case mode of
-              InLHS _ => do checkUserHoles True
+              InLHS _ => do when (not incase) $ checkUserHoles True
                             pure chktm
               -- elsewhere, all unification problems must be
               -- solved, though we defer that if it's a case block since we

src/TTImp/Elab/App.idr

@@ -218,7 +218,7 @@ mutual
              nm <- genMVName x
              empty <- clearDefs defs
              metaty <- quote empty env aty
-             (idx, metaval) <- argVar fc argRig env nm metaty
+             (idx, metaval) <- argVar (getFC arg) argRig env nm metaty
              let fntm = App fc tm appinf metaval
              logNF 10 ("Delaying " ++ show nm ++ " " ++ show arg) env aty
              logTerm 10 "...as" metaval
@@ -235,6 +235,7 @@ mutual
              -- *may* have as patterns in it and we need to retain them.
              -- (As patterns are a bit of a hack but I don't yet see a 
              -- better way that leads to good code...)
+             logTerm 5 ("Solving " ++ show metaval ++ " with") argv
              ok <- solveIfUndefined env metaval argv
              when (not ok) $
                 do res <- convert fc elabinfo env (gnf env metaval)

src/TTImp/Parser.idr

@@ -50,8 +50,8 @@ atom fname
          end <- location
          pure (IHole (MkFC fname start end) x)
 
-visibility : EmptyRule Visibility
-visibility
+visOption : Rule Visibility
+visOption
     = do keyword "public"
          keyword "export"
          pure Public
@@ -59,8 +59,59 @@ visibility
          pure Export
   <|> do keyword "private"
          pure Private
+
+visibility : EmptyRule Visibility
+visibility
+    = visOption
   <|> pure Private
 
+fnOpt : Rule FnOpt
+fnOpt
+    = do keyword "partial"
+         pure PartialOK
+  <|> do keyword "total"
+         pure Total
+  <|> do keyword "covering"
+         pure Covering
+
+fnDirectOpt : Rule FnOpt
+fnDirectOpt
+    = do exactIdent "hint"
+         pure (Hint True)
+  <|> do exactIdent "chaser"
+         pure (Hint False)
+  <|> do exactIdent "globalhint"
+         pure (GlobalHint True)
+  <|> do exactIdent "defaulthint"
+         pure (GlobalHint False)
+  <|> do exactIdent "inline"
+         pure Inline
+  <|> do exactIdent "extern"
+         pure ExternFn
+
+visOpt : Rule (Either Visibility FnOpt)
+visOpt
+    = do vis <- visOption
+         pure (Left vis)
+  <|> do tot <- fnOpt
+         pure (Right tot)
+  <|> do symbol "%"
+         opt <- fnDirectOpt
+         pure (Right opt)
+
+getVisibility : Maybe Visibility -> List (Either Visibility FnOpt) -> 
+                EmptyRule Visibility
+getVisibility Nothing [] = pure Private
+getVisibility (Just vis) [] = pure vis
+getVisibility Nothing (Left x :: xs) = getVisibility (Just x) xs
+getVisibility (Just vis) (Left x :: xs)
+   = fatalError "Multiple visibility modifiers"
+getVisibility v (_ :: xs) = getVisibility v xs
+
+getRight : Either a b -> Maybe b
+getRight (Left _) = Nothing
+getRight (Right v) = Just v
+
 bindSymbol : Rule PiInfo
 bindSymbol
     = do symbol "->"
@@ -404,6 +455,14 @@ clause fname indents
          lhs <- expr fname indents
          parseRHS fname indents start lhs
 
+dataOpt : Rule DataOpt
+dataOpt
+    = do exactIdent "noHints"
+         pure NoHints
+  <|> do exactIdent "search"
+         ns <- some name
+         pure (SearchBy ns)
+
 dataDecl : FileName -> IndentInfo -> Rule ImpData
 dataDecl fname indents
     = do start <- location
@@ -412,9 +471,13 @@ dataDecl fname indents
          symbol ":"
          ty <- expr fname indents
          keyword "where"
+         opts <- option [] (do symbol "["
+                               dopts <- sepBy1 (symbol ",") dataOpt
+                               symbol "]"
+                               pure dopts)
          cs <- block (tyDecl fname)
          end <- location
-         pure (MkImpData (MkFC fname start end) n ty [] cs)
+         pure (MkImpData (MkFC fname start end) n ty opts cs)
 
 namespaceDecl : Rule (List String)
 namespaceDecl
@@ -452,10 +515,12 @@ topDecl fname indents
          end <- location
          pure (INamespace (MkFC fname start end) ns ds)
   <|> do start <- location
-         vis <- visibility
+         visOpts <- many visOpt
+         vis <- getVisibility Nothing visOpts
+         let opts = mapMaybe getRight visOpts
          claim <- tyDecl fname indents
          end <- location
-         pure (IClaim (MkFC fname start end) RigW vis [] claim)
+         pure (IClaim (MkFC fname start end) RigW vis opts claim)
   <|> do symbol "%"; commit
          directive fname indents
   <|> clause fname indents

src/TTImp/ProcessType.idr

@@ -6,11 +6,43 @@ import Core.Env
 import Core.Normalise
 import Core.TT
 import Core.UnifyState
+import Core.Value
 
 import TTImp.Elab.Check
 import TTImp.Elab
 import TTImp.TTImp
 
+getRetTy : Defs -> NF [] -> Core Name
+getRetTy defs (NBind fc _ (Pi _ _ _) sc)
+    = getRetTy defs !(sc defs (toClosure defaultOpts [] (Erased fc)))
+getRetTy defs (NTCon _ n _ _ _) = pure n
+getRetTy defs ty
+    = throw (GenericMsg (getLoc ty) 
+             "Can only add hints for concrete return types")
+
+processFnOpt : {auto c : Ref Ctxt Defs} ->
+               FC -> Name -> FnOpt -> Core ()
+processFnOpt fc ndef Inline 
+    = setFlag fc ndef Inline
+processFnOpt fc ndef (Hint d)
+    = do defs <- get Ctxt
+         Just ty <- lookupTyExact ndef (gamma defs)
+              | Nothing => throw (UndefinedName fc ndef)
+         target <- getRetTy defs !(nf defs [] ty)
+         addHintFor fc target ndef d
+processFnOpt fc ndef (GlobalHint a)
+    = addGlobalHint ndef a
+processFnOpt fc ndef ExternFn
+    = setFlag fc ndef Inline -- if externally defined, inline when compiling
+processFnOpt fc ndef Invertible
+    = setFlag fc ndef Invertible
+processFnOpt fc ndef Total
+    = setFlag fc ndef (SetTotal Total)
+processFnOpt fc ndef Covering
+    = setFlag fc ndef (SetTotal CoveringOnly)
+processFnOpt fc ndef PartialOK
+    = setFlag fc ndef (SetTotal PartialOK)
+
 export
 processType : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
@@ -38,5 +70,8 @@ processType eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
          -- level check so don't set the flag.
          when (not (InCase `elem` eopts)) $ setLinearCheck idx True
 
+         log 1 $ "Setting options for " ++ show n ++ ": " ++ show opts
+         traverse (processFnOpt fc (Resolved idx)) opts
+
          -- TODO: Interface hash and saving
          pure ()

src/TTImp/TTImp.idr

@@ -149,11 +149,41 @@ mutual
   public export
   data FnOpt : Type where
        Inline : FnOpt
+       -- Flag means the hint is a direct hint, not a function which might
+       -- find the result (e.g. chasing parent interface dictionaries)
+       Hint : Bool -> FnOpt
+       -- flag means always use this in search. If not set, it is only
+       -- used as a hint if all else fails (i.e. a default)
+       GlobalHint : Bool -> FnOpt
+       ExternFn : FnOpt
+       -- assume safe to cancel arguments in unification
+       Invertible : FnOpt
+       Total : FnOpt
+       Covering : FnOpt
+       PartialOK : FnOpt
+
+  export
+  Show FnOpt where
+    show Inline = "%inline"
+    show (Hint t) = "%hint " ++ show t
+    show (GlobalHint t) = "%globalhint " ++ show t
+    show ExternFn = "%extern"
+    show Invertible = "%invertible"
+    show Total = "total"
+    show Covering = "covering"
+    show PartialOK = "partial"
 
   export
   Eq FnOpt where
-    (==) Inline Inline = True
-    (==) _ _ = False
+    Inline == Inline = True
+    (Hint x) == (Hint y) = x == y
+    (GlobalHint x) == (GlobalHint y) = x == y
+    ExternFn == ExternFn = True
+    Invertible == Invertible = True
+    Total == Total = True
+    Covering == Covering = True
+    PartialOK == PartialOK = True
+    _ == _ = False
 
   public export
   data ImpTy : Type where

tests/Main.idr

@@ -14,7 +14,7 @@ ttimpTests
        "nest001", "nest002",
        "perf001", "perf002", "perf003",
        "qtt001", "qtt002", "qtt003",
-       "search001", "search002"]
+       "search001", "search002", "search003"]
 
 chdir : String -> IO Bool
 chdir dir 

tests/ttimp/search003/FakeTC.yaff

@@ -0,0 +1,133 @@
+data Bool : Type where
+     False : Bool
+     True : Bool
+
+not : Bool -> Bool
+not False = True
+not True = False
+
+data Nat : Type where
+     Z : Nat
+     S : Nat -> Nat
+
+data List : Type -> Type where
+     Nil : List $a
+     Cons : $a -> List $a -> List $a
+
+data Maybe : Type -> Type where
+     Nothing : Maybe $a
+     Just : $a -> Maybe $a
+
+data Pair : Type -> Type -> Type where
+     MkPair : $a -> $b -> Pair $a $b
+
+fst : {0 a, b : _} -> Pair a b -> a
+fst (MkPair $x _) = x
+
+snd : {0 a, b : _} -> Pair a b -> b
+snd (MkPair _ $y) = y
+
+%pair Pair fst snd
+
+data Show : (a : Type) -> Type where
+     [noHints, search a]
+     MkShow : (showFn : $a -> String) -> Show $a
+
+show : {auto c : Show $a} -> $a -> String
+show {c = MkShow $show'} $x = show' x
+
+showNat : Nat -> String
+showNat Z = "Z"
+showNat (S $k) = "s" -- (showNat k)
+
+%hint
+ShowNat : Show Nat
+ShowNat = MkShow showNat
+
+%hint
+ShowBool : Show Bool
+ShowBool = MkShow (\b : Bool => case b of
+                                     True => "True"
+                                     False => "False")
+
+data Eq : (a : Type) -> Type where
+     [noHints, search a]
+     MkEq : (eq : $a -> $a -> Bool) -> (neq : $a -> $a -> Bool) -> Eq $a
+
+-- Signatures
+eq : {auto c : Eq $a} -> $a -> $a -> Bool
+neq : {auto c : Eq $a} -> $a -> $a -> Bool
+
+-- Top level method bodies
+eq {c = MkEq $eq' $neq'} $x $y = eq' x y
+neq {c = MkEq $eq' $neq'} $x $y = neq' x y
+
+-- Default definitions
+defaultEq : {auto c : Eq $a} -> $a -> $a -> Bool
+defaultEq $x $y = not (neq x y)
+
+defaultNotEq : {auto c : Eq $a} -> $a -> $a -> Bool
+defaultNotEq $x $y = not (eq x y)
+
+-- e.g. Nat
+
+-- Instance type
+%hint
+EqNat : Eq Nat
+
+-- Method bodies
+
+eqNat : Nat -> Nat -> Bool
+eqNat Z Z = True
+eqNat (S $j) (S $k) = eq j k
+eqNat _ _ = False
+
+-- Rest of instance
+EqNat = MkEq eqNat (\x, y => not (eqNat x y))
+
+%hint
+EqMaybe : {auto c : Eq $a} -> Eq (Maybe $a)
+
+eqMaybe : {auto c : Eq $a} -> Maybe $a -> Maybe $a -> Bool
+eqMaybe Nothing Nothing = True
+eqMaybe (Just $x) (Just $y) = eq x y
+eqMaybe _ _ = False
+
+EqMaybe = MkEq eqMaybe (\x, y => not (eqMaybe x y))
+
+public export
+data Compare : Type where
+     LT : Compare
+     EQ : Compare
+     GT : Compare
+
+public export
+data Ord : (a : Type) -> Type where
+     MkOrd : {auto eqc : Eq $a} ->
+             (cmp : $a -> $a -> Compare) -> Ord $a
+
+%chaser
+findEq :  Ord $a -> Eq $a
+findEq (MkOrd _) = %search
+
+cmp : {auto c : Ord $a} -> $a -> $a -> Compare
+cmp {c = MkOrd $cmp'} $x $y = cmp' x y
+
+cmpNat : Nat -> Nat -> Compare
+cmpNat Z Z = EQ
+cmpNat Z (S $k) = LT
+cmpNat (S $k) Z = GT
+cmpNat (S $x) (S $y) = cmpNat x y
+
+%hint
+ordNat : Ord Nat
+ordNat = MkOrd cmpNat
+
+testEq : {auto c : Ord $a} -> $a -> $a -> Bool
+testEq $x $y = eq x y
+
+testThings : {auto c : Pair (Show $a) (Ord $a)} -> $a -> $a -> 
+             Pair String Bool
+testThings $x $y = MkPair (show x) (eq x y)
+
+

tests/ttimp/search003/expected

@@ -0,0 +1,15 @@
+Processing as TTImp
+Written TTC
+Yaffle> Main.True
+Yaffle> "True"
+Yaffle> ((((Main.MkPair [Just b = Main.Bool]) [Just a = String]) "Z") Main.False)
+Yaffle> Bye for now!
+Processing as TTC
+Read 0 holes
+Read 0 guesses
+Read 0 constraints
+Read TTC
+Yaffle> Main.True
+Yaffle> "True"
+Yaffle> ((((Main.MkPair [Just b = Main.Bool]) [Just a = String]) "Z") Main.False)
+Yaffle> Bye for now!

tests/ttimp/search003/input

@@ -0,0 +1,4 @@
+eq (S (S Z)) (S (S Z))
+show True
+testThings Z (S (S (S Z)))
+:q

tests/ttimp/search003/run

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