Some unifiation infrastructure

src/Core/Context.idr

@@ -160,6 +160,7 @@ public export
 record Defs where
   constructor MkDefs
   gamma : Context GlobalDef
+  currentNS : List String -- namespace for current definitions
 
 export
 clearDefs : Defs -> Core Defs
@@ -171,7 +172,7 @@ export
 initDefs : Core Defs
 initDefs 
     = do gam <- initCtxt
-         pure (MkDefs gam)
+         pure (MkDefs gam ["Main"])
       
 -- Label for context references
 export
@@ -186,3 +187,16 @@ addDef n def
          put Ctxt (record { gamma = gam' } defs)
          pure idx
 
+-- Get the name as it would be defined in the current namespace
+-- i.e. if it doesn't have an explicit namespace already, add it,
+-- otherwise leave it alone
+export
+inCurrentNS : {auto c : Ref Ctxt Defs} ->
+              Name -> Core Name
+inCurrentNS (UN n)
+    = do defs <- get Ctxt
+         pure (NS (currentNS defs) (UN n))
+inCurrentNS n@(MN _ _)
+    = do defs <- get Ctxt
+         pure (NS (currentNS defs) n)
+inCurrentNS n = pure n

src/Core/Env.idr

@@ -3,20 +3,19 @@ module Core.Env
 import Core.TT
 
 -- Environment containing types and values of local variables
-namespace Env
+public export
-  public export
+data Env : (tm : List Name -> Type) -> List Name -> Type where
-  data Env : (tm : List Name -> Type) -> List Name -> Type where
+     Nil : Env tm []
-       Nil : Env tm []
+     (::) : Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)
-       (::) : Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)
 
-  export
+export
-  extend : (x : Name) -> Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)
+extend : (x : Name) -> Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)
-  extend x = (::) {x} 
+extend x = (::) {x} 
 
-  export
+export
-  length : Env tm xs -> Nat
+length : Env tm xs -> Nat
-  length [] = 0
+length [] = 0
-  length (x :: xs) = S (length xs)
+length (x :: xs) = S (length xs)
 
 export
 defined : {vars : _} ->

src/Core/TT.idr

@@ -21,7 +21,7 @@ data NameType : Type where
 
 public export
 data Constant 
-	  = I Int
+    = I Int
     | BI Integer
     | Str String
     | Ch Char
@@ -29,7 +29,7 @@ data Constant
     | WorldVal
 
     | IntType
-		| IntegerType
+    | IntegerType
     | StringType
     | CharType
     | DoubleType

src/Core/Unify.idr

@@ -8,6 +8,8 @@ import Core.TT
 import public Core.UnifyState
 import Core.Value
 
+import Data.IntMap
+
 %default covering
 
 public export
@@ -46,10 +48,81 @@ unify : Unify tm =>
         Core (List Int)
 unify {c} {u} = unifyD c u
 
+ufail : FC -> String -> Core a
+ufail loc msg = throw (GenericMsg loc msg)
+
+convertError : FC -> Env Term vars -> Term vars -> Term vars -> Core a
+convertError loc env x y = throw (CantConvert loc env x y)
+
+convertErrorS : Bool -> FC -> Env Term vars -> Term vars -> Term vars -> Core a
+convertErrorS s loc env x y 
+    = if s then throw (CantConvert loc env y x)
+           else throw (CantConvert loc env x y)
+
+postpone : {auto c : Ref Ctxt Defs} ->
+           {auto u : Ref UST UState} ->
+           FC -> Env Term vars -> NF vars -> NF vars -> Core (List Int)
+postpone loc env x y
+    = do defs <- get Ctxt
+         empty <- clearDefs defs
+         c <- addConstraint (MkConstraint loc env !(quote empty env x) 
+                                                  !(quote empty env y))
+         pure [c]
+
+unifyArgs : (Unify tm, Quote tm) =>
+            {auto c : Ref Ctxt Defs} ->
+            {auto u : Ref UST UState} ->
+            UnifyMode -> FC -> Env Term vars ->
+            List (tm vars) -> List (tm vars) ->
+            Core (List Int)
+unifyArgs mode loc env [] [] = pure []
+unifyArgs mode loc env (cx :: cxs) (cy :: cys)
+    = do constr <- unify mode loc env cx cy
+         case constr of
+              [] => unifyArgs mode loc env cxs cys
+              _ => do cs <- unifyArgs mode loc env cxs cys
+                      -- TODO: Fix this bit! See p59 Ulf's thesis
+--                       c <- addConstraint 
+--                                (MkSeqConstraint loc env 
+--                                    (map (quote gam env) (cx :: cxs))
+--                                    (map (quote gam env) (cy :: cys)))
+                      pure (union constr cs) -- [c]
+unifyArgs mode loc env _ _ = ufail loc ""
+
 mutual
+  unifyIfEq : {auto c : Ref Ctxt Defs} ->
+              {auto u : Ref UST UState} ->
+              (postpone : Bool) ->
+              FC -> Env Term vars -> NF vars -> NF vars -> 
+              Core (List Int)
+  unifyIfEq post loc env x y 
+        = do defs <- get Ctxt
+             empty <- clearDefs defs
+             if !(convert defs env x y)
+                then pure []
+                else if post 
+                        then do -- log 10 $ "Postponing constraint (unifyIfEq) " ++
+                                --         show !(quote empty env x) ++ " =?= " ++
+                                --         show !(quote empty env y)
+                                postpone loc env x y
+                        else convertError loc env 
+                                     !(quote empty env x)
+                                     !(quote empty env y)
+
+  unifyNoEta : {auto c : Ref Ctxt Defs} ->
+               {auto u : Ref UST UState} ->
+               UnifyMode -> FC -> Env Term vars ->
+               NF vars -> NF vars ->
+               Core (List Int)
+  unifyNoEta mode loc env x y 
+      = do defs <- get Ctxt
+           empty <- clearDefs defs
+           unifyIfEq False loc env x y
 
   export
   Unify NF where
+    -- TODO: Eta!
+    unifyD _ _ mode loc env tmx tmy = unifyNoEta mode loc env tmx tmy
 
   export
   Unify Term where
@@ -70,3 +143,66 @@ mutual
              -- names won't reduce until they have to
              unify mode loc env !(quote empty env x) !(quote empty env y)
 
+public export
+data SolveMode = Normal -- during elaboration: unifies and searches
+               | Defaults -- unifies and searches for default hints only
+               | LastChance -- as normal, but any failure throws rather than delays
+
+retry : {auto c : Ref Ctxt Defs} ->
+        {auto u : Ref UST UState} ->
+        UnifyMode -> Int -> Core (List Int)
+retry mode c
+    = do ust <- get UST
+         case lookup c (constraints ust) of
+              Nothing => pure []
+              Just Resolved => pure []
+              Just (MkConstraint loc env x y)
+                  => catch (do log 5 $ "Retrying " ++ show x ++ " and " ++ show y
+                               cs <- unify mode loc env x y 
+                               case cs of
+                                 [] => do setConstraint c Resolved
+                                          pure []
+                                 _ => pure cs)
+                       (\err => throw (WhenUnifying loc env x y err)) 
+              Just (MkSeqConstraint loc env xs ys)
+                  => do cs <- unifyArgs mode loc env xs ys
+                        case cs of
+                             [] => do setConstraint c Resolved
+                                      pure []
+                             _ => pure cs
+
+-- Retry the given constraint, return True if progress was made
+retryGuess : {auto c : Ref Ctxt Defs} ->
+             {auto u : Ref UST UState} ->
+             UnifyMode -> (smode : SolveMode) -> (hole : (FC, Name, Int)) ->
+             Core Bool
+retryGuess mode smode (loc, hname, hid)
+    = do defs <- get Ctxt
+         case !(lookupCtxtExact (Resolved hid) (gamma defs)) of
+           Nothing => pure False
+           Just def =>
+             case definition def of
+               Guess tm constraints => 
+                 do cs' <- traverse (retry mode) constraints
+                    case concat cs' of
+                         -- All constraints resolved, so turn into a
+                         -- proper definition and remove it from the
+                         -- hole list
+                         [] => do let gdef = record { definition = Fn tm } def
+                                  addDef (Resolved hid) gdef
+                                  removeGuess hid
+                                  pure True
+                         newcs => do let gdef = record { definition = Guess tm newcs } def
+                                     addDef (Resolved hid) gdef
+                                     pure False
+               _ => pure False
+
+export
+solveConstraints : {auto c : Ref Ctxt Defs} ->
+                   {auto u : Ref UST UState} ->
+                   UnifyMode -> (smode : SolveMode) -> Core ()
+solveConstraints umode smode
+    = do ust <- get UST
+         progress <- traverse (retryGuess umode smode) (guesses ust)
+         when (or (map Delay progress)) $ solveConstraints umode smode
+

src/Core/UnifyState.idr

@@ -37,9 +37,11 @@ record UState where
   guesses : List (FC, Name, Int) -- Names which will be defined when constraints solved
   constraints : IntMap Constraint -- map for finding constraints by ID
   nextName : Int
+  nextConstraint : Int
 
+export
 initUState : UState
-initUState = MkUState [] [] empty 0
+initUState = MkUState [] [] empty 0 0
 
 export
 data UST : Type where
@@ -64,6 +66,45 @@ addGuessName fc n i
     = do ust <- get UST
          put UST (record { guesses $= ((fc, n, i) ::)  } ust)
 
+export
+removeHole : {auto u : Ref UST UState} ->
+             Int -> Core ()
+removeHole n
+    = do ust <- get UST
+         put UST (record { holes $= filter (\ (fc, x, i) => i /= n) } ust)
+
+export
+removeGuess : {auto u : Ref UST UState} ->
+              Int -> Core ()
+removeGuess n
+    = do ust <- get UST
+         put UST (record { guesses $= filter (\ (fc, x, i) => i /= n) } ust)
+
+export
+getHoles : {auto u : Ref UST UState} ->
+           Core (List (FC, Name, Int))
+getHoles
+    = do ust <- get UST
+         pure (holes ust)
+
+export
+setConstraint : {auto u : Ref UST UState} ->
+                Int -> Constraint -> Core ()
+setConstraint cid c
+    = do ust <- get UST
+         put UST (record { constraints $= insert cid c } ust)
+
+export
+addConstraint : {auto u : Ref UST UState} ->
+                {auto c : Ref Ctxt Defs} ->
+                Constraint -> Core Int
+addConstraint constr
+    = do ust <- get UST
+         let cid = nextConstraint ust
+         put UST (record { constraints $= insert cid constr,
+                           nextConstraint = cid+1 } ust)
+         pure cid
+
 mkConstantAppArgs : Bool -> FC -> Env Term vars -> 
                     (wkns : List Name) ->
                     List (Term (wkns ++ (vars ++ done)))

src/TTImp/Elab/App.idr

@@ -111,7 +111,7 @@ mutual
            defs <- get Ctxt
            case expty of
                 NBind tfc' x' (Pi rigb' Implicit aty') sc'
-                   => checkExp rig env fc tm (glueBack defs env ty) (Just expty_in)
+                   => checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)
                 _ => makeImplicit rig elabinfo env fc tm x aty sc [] [] (Just expty_in)
   checkAppWith rig elabinfo env fc tm ty@(NBind tfc x (Pi rigb AutoImplicit aty) sc)
                [] [] (Just expty_in)
@@ -119,7 +119,7 @@ mutual
            defs <- get Ctxt
            case expty of
                 NBind tfc' x' (Pi rigb' AutoImplicit aty') sc'
-                   => checkExp rig env fc tm (glueBack defs env ty) (Just expty_in)
+                   => checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)
                 _ => makeAutoImplicit rig elabinfo env fc tm x aty sc [] [] (Just expty_in)
 
   -- Check next auto implicit argument
@@ -164,7 +164,7 @@ mutual
 
   checkAppWith rig elabinfo env fc tm ty [] [] expty 
       = do defs <- get Ctxt
-           checkExp rig env fc tm (glueBack defs env ty) expty
+           checkExp rig elabinfo env fc tm (glueBack defs env ty) expty
   checkAppWith rig elabinfo env fc tm ty [] impargs expty 
       = throw (InvalidImplicits fc env (map fst impargs) tm)
   checkAppWith {vars} rig elabinfo env fc tm ty (arg :: expargs) impargs expty 

src/TTImp/Elab/Binders.idr

@@ -31,7 +31,7 @@ checkPi rig elabinfo env fc rigf info n argTy retTy expTy
          (scopev, scopet) <- 
             inScope (\e' => 
               check {e=e'} Rig0 (nextLevel elabinfo) env' retTy (Just (gType fc)))
-         checkExp rig env fc (Bind fc n (Pi rigf info tyv) scopev) (gType fc) expTy
+         checkExp rig elabinfo env fc (Bind fc n (Pi rigf info tyv) scopev) (gType fc) expTy
 
 findLamRig : {auto c : Ref Ctxt Defs} ->
              Maybe (Glued vars) -> Core RigCount
@@ -84,7 +84,7 @@ checkLambda rig_in elabinfo env fc rigl info n argTy scope (Just expty_in)
                        inScope (\e' =>
                           check {e=e'} rig (nextLevel elabinfo) env' scope 
                                 (Just (gnf defs env' (renameTop n psc))))
-                    checkExp rig env fc 
+                    checkExp rig elabinfo env fc 
                              (Bind fc n (Lam rigb info tyv) scopev)
                              (gnf defs env 
                                   (Bind fc n (Pi rigb info tyv) !(getTerm scopet)))

src/TTImp/Elab/Check.idr

@@ -7,11 +7,15 @@ import Core.Core
 import Core.Env
 import Core.Normalise
 import Core.Unify
+import Core.UnifyState
 import Core.TT
 import Core.Value
 
 import TTImp.TTImp
 
+public export
+data ElabMode = InType | InLHS RigCount | InExpr
+
 -- Current elaboration state (preserved/updated throughout elaboration)
 public export
 record EState (vars : List Name) where
@@ -48,6 +52,7 @@ inScope {e} elab
 public export
 record ElabInfo where
   constructor MkElabInfo
+  elabMode : ElabMode
   level : Nat
 
 export
@@ -95,8 +100,26 @@ convert : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           {auto e : Ref EST (EState vars)} ->
-          FC -> Env Term vars -> NF vars -> NF vars ->
+          FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars ->
           Core (List Int)
+convert fc elabinfo env x y
+    = let umode : UnifyMode
+                = case elabMode elabinfo of
+                       InLHS _ => InLHS
+                       _ => InTerm in
+          catch (do hs <- getHoles
+                    vs <- unify umode fc env !(getNF x) !(getNF y)
+                    hs' <- getHoles
+                    when (isNil vs && length hs' < length hs) $
+                      solveConstraints umode Normal
+                    pure vs)
+                (\err => do xtm <- getTerm x
+                            ytm <- getTerm y
+                            -- See if we can improve the error message by
+                            -- resolving any more constraints
+                            catch (solveConstraints umode Normal)
+                                  (\err => pure ())
+                            throw (WhenUnifying fc env xtm ytm err))
 
 -- Check whether the type we got for the given type matches the expected
 -- type.
@@ -108,12 +131,12 @@ checkExp : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            {auto e : Ref EST (EState vars)} ->
-           RigCount -> Env Term vars -> FC ->
+           RigCount -> ElabInfo -> Env Term vars -> FC ->
            (term : Term vars) -> 
            (got : Glued vars) -> (expected : Maybe (Glued vars)) -> 
            Core (Term vars, Glued vars)
-checkExp rig env fc tm got (Just exp) 
+checkExp rig elabinfo env fc tm got (Just exp) 
-    = do constr <- convert fc env !(getNF got) !(getNF exp)
+    = do constr <- convert fc elabinfo env got exp
          case constr of
               [] => pure (tm, got)
               cs => do defs <- get Ctxt
@@ -121,4 +144,4 @@ checkExp rig env fc tm got (Just exp)
                        cty <- getTerm exp
                        ctm <- newConstant fc rig env tm cty cs
                        pure (ctm, exp)
-checkExp rig env fc tm got Nothing = pure (tm, got)
+checkExp rig elabinfo env fc tm got Nothing = pure (tm, got)

src/TTImp/Elab/Term.idr

@@ -48,7 +48,7 @@ checkTerm rig elabinfo env (IImplicitApp fc fn nm arg) exp
 checkTerm rig elabinfo env (IPrimVal fc c) exp 
     = ?checkTerm_rhs_6
 checkTerm rig elabinfo env (IType fc) exp 
-    = checkExp rig env fc (TType fc) (gType fc) exp
+    = checkExp rig elabinfo env fc (TType fc) (gType fc) exp
 checkTerm rig elabinfo env (Implicit fc) (Just gexpty)
     = do nm <- genName "imp"
          expty <- getTerm gexpty

src/TTImp/ProcessDecls.idr

@@ -2,10 +2,24 @@ module TTImp.ProcessDecls
 
 import Core.Context
 import Core.Core
+import Core.Env
+import Core.UnifyState
 
 import TTImp.Elab.Term
 import TTImp.TTImp
 
-export
 processDecl : {auto c : Ref Ctxt Defs} ->
-              ImpDecl -> Core ()
+              {auto u : Ref UST UState} ->
+              Env Term vars -> ImpDecl -> Core ()
+processDecl env (IClaim fc rig vis opts ty) 
+    = ?processDecl_rhs_1
+processDecl env (IData fc vis ddef) = ?processDecl_rhs_2
+processDecl env (IDef fc fname def) = ?processDecl_rhs_3
+
+export
+processDecls : {auto c : Ref Ctxt Defs} ->
+               {auto u : Ref UST UState} ->
+               Env Term vars -> List ImpDecl -> Core ()
+processDecls env decls
+    = do traverse (processDecl env) decls
+         pure ()

src/Yaffle/Main.idr

@@ -2,22 +2,37 @@ module Main
 
 import Parser.Support
 
+import Core.Context
+import Core.Env
 import Core.TT
+import Core.UnifyState
+
 import TTImp.TTImp
 import TTImp.Parser
+import TTImp.ProcessDecls
 
 import System
 
+coreMain : String -> Core ()
+coreMain fname
+    = do Right tti <- coreLift $ parseFile fname
+                                (do decls <- prog fname
+                                    eoi
+                                    pure decls)
+             | Left err => do coreLift $ printLn err
+                              coreLift $ exitWith (ExitFailure 1)
+         coreLift $ putStrLn "Parsed okay"
+         
+         defs <- initDefs
+         c <- newRef Ctxt defs
+         u <- newRef UST initUState
+         processDecls [] tti
+
 main : IO ()
 main
     = do [_, fname] <- getArgs
              | _ => do putStrLn "Usage: yaffle [input file]"
                        exitWith (ExitFailure 1)
-         Right tti <- parseFile fname
+         coreRun defaultOpts (coreMain fname)
-                                (do decls <- prog fname
+               (\err : Error => putStrLn ("Uncaught error: " ++ show err))
-                                    eoi
+               (\res => pure ())
-                                    pure decls)
-             | Left err => do printLn err
-                              exitWith (ExitFailure 1)
-         putStrLn "Parsed okay"
-         putStrLn (showSep "\n" (map show tti))