Extend unification so that Functors work

Need to identify invertible (or cancellable) holes so that we can unify
e.g. ?f Nat with List Nat and get f = List.

src/Core/Unify.idr

@@ -397,7 +397,120 @@ mutual
                 else if post 
                         then postpone loc "Postponing unifyIfEq" env x y
                         else convertError loc env x y
-  
+
+  getArgTypes : Defs -> (fnType : NF vars) -> List (AppInfo, Closure vars) -> 
+                Core (Maybe (List (NF vars)))
+  getArgTypes defs (NBind _ n (Pi _ _ ty) sc) ((_, a) :: as)
+     = do Just scTys <- getArgTypes defs !(sc defs a) as
+               | Nothing => pure Nothing
+          pure (Just (ty :: scTys))
+  getArgTypes _ _ [] = pure (Just [])
+  getArgTypes _ _ _ = pure Nothing
+
+  headsConvert : {auto c : Ref Ctxt Defs} ->
+                 Env Term vars -> 
+                 Maybe (List (NF vars)) -> Maybe (List (NF vars)) ->
+                 Core Bool
+  headsConvert env (Just vs) (Just ns)
+      = case (reverse vs, reverse ns) of
+             (v :: _, n :: _) => 
+                do logNF 10 "Converting" env v
+                   logNF 10 "......with" env n
+                   defs <- get Ctxt
+                   convert defs env v n
+             _ => pure False
+  headsConvert env _ _ 
+      = do log 10 "Nothing to convert"
+           pure True
+
+  unifyInvertible : {auto c : Ref Ctxt Defs} ->
+                    {auto u : Ref UST UState} ->
+                    {vars : _} ->
+                    UnifyMode -> FC -> Env Term vars ->
+                    (metaname : Name) -> (metaref : Int) ->
+                    (margs : List (AppInfo, Closure vars)) ->
+                    (margs' : List (AppInfo, Closure vars)) ->
+                    Maybe ClosedTerm ->
+                    (List (AppInfo, Closure vars) -> NF vars) ->
+                    List (AppInfo, Closure vars) ->
+                    Core UnifyResult
+  unifyInvertible mode fc env mname mref margs margs' nty con args'
+      = do defs <- get Ctxt
+           -- Get the types of the arguments to ensure that the rightmost
+           -- argument types match up
+           Just vty <- lookupTyExact (Resolved mref) (gamma defs)
+                | Nothing => ufail fc ("No such metavariable " ++ show mname)
+           vargTys <- getArgTypes defs !(nf defs env (embed vty)) (margs ++ margs')
+           nargTys <- maybe (pure Nothing)
+                            (\ty => getArgTypes defs !(nf defs env (embed ty)) args')
+                            nty
+           -- If the rightmost arguments have the same type, or we don't
+           -- know the types of the arguments, we'll get on with it.
+           if !(headsConvert env vargTys nargTys)
+              then 
+                -- Unify the rightmost arguments, with the goal of turning the
+                -- hole application into a pattern form
+                case (reverse margs', reverse args') of
+                     ((_, h) :: hargs, (_, f) :: fargs) =>
+                        tryUnify
+                          (do unify mode fc env h f
+                              unify mode fc env 
+                                    (NApp fc (NMeta mname mref margs) (reverse hargs))
+                                    (con (reverse fargs)))
+                          (postpone fc "Postponing hole application [1]" env
+                                (NApp fc (NMeta mname mref margs) margs')
+                                (con args'))
+                     _ => postpone fc "Postponing hole application [2]" env
+                                (NApp fc (NMeta mname mref margs) margs')
+                                (con args')
+              else -- TODO: Cancellable function applications
+                   postpone fc "Postponing hole application [3]" env 
+                            (NApp fc (NMeta mname mref margs) margs') (con args')
+
+  -- Unify a hole application - we have already checked that the hole is
+  -- invertible (i.e. it's a determining argument to a proof search where
+  -- it is a constructor or something else invertible in each case)
+  unifyHoleApp : {auto c : Ref Ctxt Defs} ->
+                 {auto u : Ref UST UState} ->
+                 {vars : _} ->
+                 UnifyMode -> FC -> Env Term vars ->
+                 (metaname : Name) -> (metaref : Int) ->
+                 (margs : List (AppInfo, Closure vars)) ->
+                 (margs' : List (AppInfo, Closure vars)) ->
+                 NF vars ->
+                 Core UnifyResult
+  unifyHoleApp mode loc env mname mref margs margs' (NTCon nfc n t a args')
+      = do defs <- get Ctxt
+           mty <- lookupTyExact n (gamma defs)
+           unifyInvertible mode loc env mname mref margs margs' mty (NTCon nfc n t a) args'
+  unifyHoleApp mode loc env mname mref margs margs' (NDCon nfc n t a args')
+      = do defs <- get Ctxt
+           mty <- lookupTyExact n (gamma defs)
+           unifyInvertible mode loc env mname mref margs margs' mty (NTCon nfc n t a) args'
+  unifyHoleApp mode loc env mname mref margs margs' (NApp nfc (NLocal r idx p) args')
+      = unifyInvertible mode loc env mname mref margs margs' Nothing 
+                        (NApp nfc (NLocal r idx p)) args'
+  unifyHoleApp mode loc env mname mref margs margs' tm@(NApp nfc (NMeta n i margs2) args2')
+      = do defs <- get Ctxt
+           Just mdef <- lookupCtxtExact (Resolved i) (gamma defs)
+                | Nothing => throw (UndefinedName nfc mname)
+           let inv = case definition mdef of
+                          Hole i => i
+                          _ => isPatName n
+           if inv
+              then unifyInvertible mode loc env mname mref margs margs' Nothing
+                                   (NApp nfc (NMeta n i margs2)) args2'
+              else postpone loc "Postponing hole application" env 
+                             (NApp loc (NMeta mname mref margs) margs') tm
+    where
+      isPatName : Name -> Bool
+      isPatName (PV _ _) = True
+      isPatName _ = False
+           
+  unifyHoleApp mode loc env mname mref margs margs' tm
+      = postpone loc "Postponing hole application" env 
+                 (NApp loc (NMeta mname mref margs) margs') tm
+
   unifyPatVar : {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 {vars : _} ->
@@ -469,7 +582,12 @@ mutual
                        pure $ "Unifying: " ++ show mname ++ " " ++ show qargs ++
                               " with " ++ show qtm)
            case !(patternEnv env args) of
-                Nothing => unifyPatVar mode loc env mname mref args tmnf
+                Nothing => 
+                  do Just (Hole inv) <- lookupDefExact (Resolved mref) (gamma defs)
+                        | _ => unifyPatVar mode loc env mname mref args tmnf
+                     if inv
+                        then unifyHoleApp mode loc env mname mref margs margs' tmnf
+                        else unifyPatVar mode loc env mname mref args tmnf
                 Just (newvars ** (locs, submv)) => 
                   do tm <- quote empty env tmnf
                      case shrinkTerm tm submv of

src/TTImp/ProcessDecls.idr

@@ -26,6 +26,10 @@ process eopts nest env (IData fc vis ddef)
     = processData eopts nest env fc vis ddef
 process eopts nest env (IDef fc fname def) 
     = processDef eopts nest env fc fname def
+process eopts nest env (IParameters fc ps decls)
+    = throw (InternalError "Parameters blocks not yet implemented")
+process eopts nest env (IRecord fc vis rec)
+    = throw (InternalError "Records not yet implemented")
 process eopts nest env (INamespace fc ns decls)
     = do oldns <- getNS
          extendNS (reverse ns)

src/TTImp/TTImp.idr

@@ -219,6 +219,31 @@ mutual
     show (MkImpLater fc n tycon)
         = "(%datadecl " ++ show n ++ " " ++ show tycon ++ ")"
 
+  public export
+  data IField : Type where
+       MkIField : FC -> RigCount -> PiInfo -> Name -> RawImp ->
+                  IField
+
+  public export
+  data ImpRecord : Type where
+       MkImpRecord : FC -> (n : Name) ->
+                     (params : List (Name, RawImp)) ->
+                     (conName : Maybe Name) ->
+                     (fields : List IField) ->
+                     ImpRecord
+
+  export
+  Show IField where
+    show (MkIField _ c Explicit n ty) = show n ++ " : " ++ show ty
+    show (MkIField _ c _ n ty) = "{" ++ show n ++ " : " ++ show ty ++ "}"
+
+  export
+  Show ImpRecord where
+    show (MkImpRecord _ n params con fields)
+        = "record " ++ show n ++ " " ++ show params ++ 
+          " " ++ show con ++ "\n\t" ++ 
+          showSep "\n\t" (map show fields) ++ "\n"
+
   public export
   data ImpClause : Type where
        PatClause : FC -> (lhs : RawImp) -> (rhs : RawImp) -> ImpClause 
@@ -239,6 +264,9 @@ mutual
                 ImpTy -> ImpDecl
        IData : FC -> Visibility -> ImpData -> ImpDecl
        IDef : FC -> Name -> List ImpClause -> ImpDecl
+       IParameters : FC -> List (Name, RawImp) ->
+                     List ImpDecl -> ImpDecl 
+       IRecord : FC -> Visibility -> ImpRecord -> ImpDecl
        INamespace : FC -> List String -> List ImpDecl -> ImpDecl 
        IPragma : ({vars : _} -> Ref Ctxt Defs -> 
                   NestedNames vars -> Env Term vars -> Core ()) -> 
@@ -250,6 +278,10 @@ mutual
     show (IClaim _ _ _ _ ty) = show ty
     show (IData _ _ d) = show d
     show (IDef _ n cs) = "(%def " ++ show n ++ " " ++ show cs ++ ")"
+    show (IParameters _ ps ds) 
+        = "parameters " ++ show ps ++ "\n\t" ++
+          showSep "\n\t" (assert_total $ map show ds)
+    show (IRecord _ _ d) = show d
     show (INamespace _ ns decls) 
         = "namespace " ++ show ns ++ 
           showSep "\n" (assert_total $ map show decls)

tests/Main.idr

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

tests/ttimp/basic005/Ambig.yaff

@@ -15,7 +15,7 @@ namespace List
   length (Cons $x $xs) = S (length xs)
 
 namespace Vect
-  data Vect : Nat -> Type -> Type where
+  data Vect : ? -> Type -> Type where
        Nil : Vect Z $a
        Cons : $a -> Vect $k $a -> Vect (S $k) $a
 

tests/ttimp/search004/Functor.yaff

@@ -0,0 +1,73 @@
+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
+
+plus : Nat -> Nat -> Nat
+plus Z $y = y
+plus (S $k) $y = S (plus k y)
+
+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 Functor : (f : ?) -> Type where
+     [noHints, search f]
+     MkFunctor : (map : {0 a, b: Type} -> (a -> b) -> $f a -> $f b) -> 
+                 Functor $f
+
+map : {auto c : Functor $f} -> ($a -> $b) -> $f $a -> $f $b
+map {c = MkFunctor $map_meth} = map_meth
+
+%hint
+ListFunctor : Functor List
+
+mapList : ($a -> $b) -> List $a -> List $b
+mapList $f Nil = Nil
+mapList $f (Cons $x $xs) = Cons (f x) (map f xs)
+
+ListFunctor = MkFunctor mapList
+
+namespace Vect
+    data Vect : ? -> Type -> Type where
+         Nil : Vect Z $a
+         Cons : $a -> Vect $k $a -> Vect (S $k) $a
+
+    %hint
+    VectFunctor : Functor (Vect $n)
+
+    mapVect : ($a -> $b) -> Vect $n $a -> Vect $n $b
+    mapVect $f Nil = Nil
+    mapVect $f (Cons $x $xs) = Cons (f x) (map f xs)
+
+    VectFunctor = MkFunctor mapVect
+
+tryMap : Nat -> Nat -> List Nat
+tryMap $x $y = map (plus x) (Cons y (Cons (S y) Nil))
+
+tryVMap : Nat -> Nat -> Vect ? Nat
+tryVMap $x $y = map (plus x) (Cons y (Cons (S y) Nil))
+
+

tests/ttimp/search004/expected

@@ -0,0 +1,13 @@
+Processing as TTImp
+Written TTC
+Yaffle> (((Main.Cons [Just a = Main.Nat]) (Main.S (Main.S (Main.S Main.Z)))) (((Main.Cons [Just a = Main.Nat]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) (Main.Nil [Just a = Main.Nat])))
+Yaffle> ((((Main.Vect.Cons [Just k = (Main.S Main.Z)]) [Just a = Main.Nat]) (Main.S (Main.S (Main.S Main.Z)))) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Main.Nat]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) (Main.Vect.Nil [Just a = Main.Nat])))
+Yaffle> Bye for now!
+Processing as TTC
+Read 0 holes
+Read 0 guesses
+Read 0 constraints
+Read TTC
+Yaffle> (((Main.Cons [Just a = Main.Nat]) (Main.S (Main.S (Main.S Main.Z)))) (((Main.Cons [Just a = Main.Nat]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) (Main.Nil [Just a = Main.Nat])))
+Yaffle> ((((Main.Vect.Cons [Just k = (Main.S Main.Z)]) [Just a = Main.Nat]) (Main.S (Main.S (Main.S Main.Z)))) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Main.Nat]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) (Main.Vect.Nil [Just a = Main.Nat])))
+Yaffle> Bye for now!

tests/ttimp/search004/input

@@ -0,0 +1,3 @@
+tryMap (S Z) (S (S Z))
+tryVMap (S Z) (S (S Z))
+:q

tests/ttimp/search004/run

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