Add 'last chance' unification and tweak guesses

Idris 1 will fill in the last metavariables by matching rather than
unification, as a convenience. I still think this is okay, even if it's
a bit hacky, because it's a huge convenience and doesn't affect other
unification problems.

Also abstract over lets in guesses, like in delayed elaborators, to
avoid any difficulties when linearity checking and to make sure that let
bound things don't get reevaluated.

This is enough to get the Chapter 6 TypeDD tests working

TypeDD.md

@@ -62,7 +62,14 @@ In `Loops.idr` and `ReadNum.idr` add `import Data.Strings` and change `cast` to
 Chapter 6
 ---------
 
-TODO
+In `DataStore.idr` and `DataStoreHoles.idr`, add `import Data.Strings` and
+`import System.REPL`
+In `DataStore.idr`, the `schema` argument to `display` is required for
+matching, so change the type to:
+
+    display : {schema : _} -> SchemaType schema -> String
+
+In `TypeFuns.idr` add `import Data.Strings`
 
 Chapter 7
 ---------

src/Core/Unify.idr

@@ -18,13 +18,13 @@ import Data.List.Views
 public export
 data UnifyMode = InLHS
                | InTerm
-               | InDot
+               | InMatch
                | InSearch
 
 Eq UnifyMode where
    InLHS == InLHS = True
    InTerm == InTerm = True
-   InDot == InDot = True
+   InMatch == InMatch = True
    InSearch == InSearch = True
    _ == _ = False
 
@@ -756,14 +756,14 @@ mutual
       = if hdx == hdy
            then unifyArgs InSearch loc env xargs yargs
            else unifyApp False InSearch loc env xfc fx xargs (NApp yfc fy yargs)
-  doUnifyBothApps InDot loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
+  doUnifyBothApps InMatch loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
       = if hdx == hdy
            then do logC 5 (do defs <- get Ctxt
                               xs <- traverse (quote defs env) xargs
                               ys <- traverse (quote defs env) yargs
-                              pure ("Unifying dot pattern args " ++ show xs ++ " " ++ show ys))
-                   unifyArgs InDot loc env xargs yargs
-           else unifyApp False InDot loc env xfc fx xargs (NApp yfc fy yargs)
+                              pure ("Matching args " ++ show xs ++ " " ++ show ys))
+                   unifyArgs InMatch loc env xargs yargs
+           else unifyApp False InMatch loc env xfc fx xargs (NApp yfc fy yargs)
   doUnifyBothApps mode loc env xfc fx ax yfc fy ay
       = unifyApp False mode loc env xfc fx ax (NApp yfc fy ay)
 
@@ -1090,7 +1090,10 @@ retryGuess mode smode (hid, (loc, hname))
                                                  throw !(normaliseErr err)
                                              _ => pure False) -- Postpone again
                Guess tm constrs => 
-                 do cs' <- traverse (retry mode) constrs
+                 do let umode = case smode of
+                                     LastChance => InMatch
+                                     _ => mode
+                    cs' <- traverse (retry umode) constrs
                     let csAll = unionAll cs'
                     case constraints csAll of
                          -- All constraints resolved, so turn into a
@@ -1154,7 +1157,7 @@ checkDots
              -- A dot is okay if the constraint is solvable *without solving
              -- any additional holes*
              catch
-               (do cs <- unify InDot fc env x y
+               (do cs <- unify InMatch fc env x y
                    defs <- get Ctxt
                    Just ndef <- lookupDefExact n (gamma defs)
                         | Nothing => throw (UndefinedName fc n)

src/Core/UnifyState.idr

@@ -383,8 +383,8 @@ newMeta fc r env n ty cyc = newMetaLets fc r env n ty cyc False
 
 mkConstant : FC -> Env Term vars -> Term vars -> ClosedTerm
 mkConstant fc [] tm = tm
-mkConstant {vars = x :: _} fc (Let c val ty :: env) tm
-    = mkConstant fc env (Bind fc x (Let c val ty) tm)
+-- mkConstant {vars = x :: _} fc (Let c val ty :: env) tm
+--     = mkConstant fc env (Bind fc x (Let c val ty) tm)
 mkConstant {vars = x :: _} fc (b :: env) tm 
     = let ty = binderType b in
           mkConstant fc env (Bind fc x (Lam (multiplicity b) Explicit ty) tm)
@@ -401,7 +401,7 @@ newConstant : {auto u : Ref UST UState} ->
               Core (Term vars)
 newConstant {vars} fc rig env tm ty constrs
     = do let def = mkConstant fc env tm
-         let defty = abstractEnvType fc env ty
+         let defty = abstractFullEnvType fc env ty
          cn <- genName "postpone"
          let guess = newDef fc cn rig [] defty Public (Guess def constrs)
          log 5 $ "Adding new constant " ++ show (cn, fc, rig)
@@ -411,7 +411,7 @@ newConstant {vars} fc rig env tm ty constrs
          pure (Meta fc cn idx envArgs)
   where
     envArgs : List (Term vars)
-    envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in
+    envArgs = let args = reverse (mkConstantAppArgs {done = []} True fc env []) in
                   rewrite sym (appendNilRightNeutral vars) in args
 
 -- Create a new search with the given name and return type,

src/Idris/REPL.idr

@@ -456,7 +456,7 @@ process Edit
               Nothing => do coreLift $ putStrLn "No file loaded"
                             pure True
               Just f =>
-                do let line = maybe "" (\i => " +" ++ show i) (errorLine opts)
+                do let line = maybe "" (\i => " +" ++ show (i + 1)) (errorLine opts)
                    coreLift $ system (editor opts ++ " " ++ f ++ line)
                    loadMainFile f
                    pure True

tests/Main.idr

@@ -47,7 +47,8 @@ idrisTests
 
 typeddTests : List String
 typeddTests
-   = ["chapter01", "chapter02", "chapter03", "chapter04", "chapter05"]
+   = ["chapter01", "chapter02", "chapter03", "chapter04", "chapter05",
+      "chapter06"]
 
 chezTests : List String
 chezTests

tests/typedd-book/chapter06/Adder.idr

@@ -0,0 +1,8 @@
+AdderType : (numargs : Nat) -> Type -> Type
+AdderType Z numType = numType
+AdderType (S k) numType = (next : numType) -> AdderType k numType
+
+adder : Num numType =>
+        (numargs : Nat) -> numType -> AdderType numargs numType
+adder Z acc = acc
+adder (S k) acc = \next => adder k (next + acc)

tests/typedd-book/chapter06/DataStore.idr

@@ -0,0 +1,130 @@
+module Main
+
+import Data.List
+import Data.Strings
+import Data.Vect
+import System.REPL
+
+infixr 5 .+.
+
+data Schema = SString | SInt | (.+.) Schema Schema
+
+SchemaType : Schema -> Type
+SchemaType SString = String
+SchemaType SInt = Int
+SchemaType (x .+. y) = (SchemaType x, SchemaType y)
+
+record DataStore where
+  constructor MkData
+  schema : Schema
+  size : Nat
+  items : Vect size (SchemaType schema)
+
+addToStore : (store : DataStore) -> SchemaType (schema store) -> DataStore
+addToStore (MkData schema size store) newitem = MkData schema _ (addToData store)
+  where
+    addToData : Vect oldsize (SchemaType schema) -> Vect (S oldsize) (SchemaType schema)
+    addToData [] = [newitem]
+    addToData (x :: xs) = x :: addToData xs
+
+setSchema : (store : DataStore) -> Schema -> Maybe DataStore
+setSchema store schema = case size store of
+                              Z => Just (MkData schema _ [])
+                              S k => Nothing
+
+data Command : Schema -> Type where
+     SetSchema : Schema -> Command schema
+     Add : SchemaType schema -> Command schema
+     Get : Integer -> Command schema
+     Quit : Command schema
+
+
+parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
+parsePrefix SString input = getQuoted (unpack input)
+  where
+    getQuoted : List Char -> Maybe (String, String)
+    getQuoted ('"' :: xs)
+        = case span (/= '"') xs of
+               (quoted, '"' :: rest) => Just (pack quoted, ltrim (pack rest))
+               _ => Nothing
+    getQuoted _ = Nothing
+
+parsePrefix SInt input = case span isDigit input of
+                              ("", rest) => Nothing
+                              (num, rest) => Just (cast num, ltrim rest)
+parsePrefix (schemal .+. schemar) input
+    = case parsePrefix schemal input of
+           Nothing => Nothing
+           Just (l_val, input') =>
+                case parsePrefix schemar input' of
+                     Nothing => Nothing
+                     Just (r_val, input'') => Just ((l_val, r_val), input'')
+
+parseBySchema : (schema : Schema) -> String -> Maybe (SchemaType schema)
+parseBySchema schema x = case parsePrefix schema x of
+                              Nothing => Nothing
+                              Just (res, "") => Just res
+                              Just _ => Nothing
+
+parseSchema : List String -> Maybe Schema
+parseSchema ("String" :: xs)
+    = case xs of
+           [] => Just SString
+           _ => case parseSchema xs of
+                     Nothing => Nothing
+                     Just xs_sch => Just (SString .+. xs_sch)
+parseSchema ("Int" :: xs)
+    = case xs of
+           [] => Just SInt
+           _ => case parseSchema xs of
+                     Nothing => Nothing
+                     Just xs_sch => Just (SInt .+. xs_sch)
+parseSchema _ = Nothing
+
+parseCommand : (schema : Schema) -> String -> String -> Maybe (Command schema)
+parseCommand schema "add" rest = case parseBySchema schema rest of
+                                      Nothing => Nothing
+                                      Just restok => Just (Add restok)
+parseCommand schema "get" val = case all isDigit (unpack val) of
+                                    False => Nothing
+                                    True => Just (Get (cast val))
+parseCommand schema "quit" "" = Just Quit
+parseCommand schema "schema" rest
+    = case parseSchema (words rest) of
+           Nothing => Nothing
+           Just schemaok => Just (SetSchema schemaok)
+parseCommand _ _ _ = Nothing
+
+parse : (schema : Schema) -> (input : String) -> Maybe (Command schema)
+parse schema input = case span (/= ' ') input of
+                          (cmd, args) => parseCommand schema cmd (ltrim args)
+
+display : {schema : _} -> SchemaType schema -> String
+display {schema = SString} item = show item
+display {schema = SInt} item = show item
+display {schema = (y .+. z)} (iteml, itemr) = display iteml ++ ", " ++
+                                              display itemr
+
+getEntry : (pos : Integer) -> (store : DataStore) ->
+           Maybe (String, DataStore)
+getEntry pos store
+    = let store_items = items store in
+          case integerToFin pos (size store) of
+               Nothing => Just ("Out of range\n", store)
+               Just id => Just (display (index id (items store)) ++ "\n", store)
+
+processInput : DataStore -> String -> Maybe (String, DataStore)
+processInput store input
+    = case parse (schema store) input of
+           Nothing => Just ("Invalid command\n", store)
+           Just (Add item) =>
+              Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
+           Just (SetSchema schema') =>
+              case setSchema store schema' of
+                   Nothing => Just ("Can't update schema when entries in store\n", store)
+                   Just store' => Just ("OK\n", store')
+           Just (Get pos) => getEntry pos store
+           Just Quit => Nothing
+
+main : IO ()
+main = replWith (MkData (SString .+. SString .+. SInt) _ []) "Command: " processInput

tests/typedd-book/chapter06/DataStoreHoles.idr

@@ -0,0 +1,64 @@
+module Main
+
+import Data.Strings
+import Data.Vect
+import System.REPL
+
+infixr 5 .+.
+
+data Schema = SString | SInt | (.+.) Schema Schema
+
+SchemaType : Schema -> Type
+SchemaType SString = String
+SchemaType SInt = Int
+SchemaType (x .+. y) = (SchemaType x, SchemaType y)
+
+record DataStore where
+  constructor MkData
+  schema : Schema
+  size : Nat
+  items : Vect size (SchemaType schema)
+
+addToStore : (d : DataStore) -> SchemaType (schema d) -> DataStore
+addToStore (MkData schema size store) newitem = MkData schema _ (addToData store)
+  where
+    addToData : Vect oldsize (SchemaType schema) -> Vect (S oldsize) (SchemaType schema)
+    addToData [] = [newitem]
+    addToData (x :: xs) = x :: addToData xs
+
+data Command : Schema -> Type where
+     Add : SchemaType schema -> Command schema
+     Get : Integer -> Command schema
+     Quit : Command schema
+
+parseCommand : String -> String -> Maybe (Command schema)
+parseCommand "add" rest = Just (Add (?parseBySchema rest))
+parseCommand "get" val = case all isDigit (unpack val) of
+                              False => Nothing
+                              True => Just (Get (cast val))
+parseCommand "quit" "" = Just Quit
+parseCommand _ _ = Nothing
+
+parse : (schema : Schema) -> (input : String) -> Maybe (Command schema)
+parse schema input = case span (/= ' ') input of
+                          (cmd, args) => parseCommand cmd (ltrim args)
+
+getEntry : (pos : Integer) -> (store : DataStore) ->
+           Maybe (String, DataStore)
+getEntry pos store
+    = let store_items = items store in
+          case integerToFin pos (size store) of
+               Nothing => Just ("Out of range\n", store)
+               Just id => Just (?display (index id (items store)) ++ "\n", store)
+
+processInput : DataStore -> String -> Maybe (String, DataStore)
+processInput store input
+    = case parse (schema store) input of
+           Nothing => Just ("Invalid command\n", store)
+           Just (Add item) =>
+              Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
+           Just (Get pos) => getEntry pos store
+           Just Quit => Nothing
+
+main : IO ()
+main = replWith (MkData SString _ []) "Command: " processInput

tests/typedd-book/chapter06/Maybe.idr

@@ -0,0 +1,16 @@
+maybeAdd : Maybe Int -> Maybe Int -> Maybe Int
+maybeAdd x y = case x of
+                    Nothing => Nothing
+                    Just x_val => case y of
+                                       Nothing => Nothing
+                                       Just y_val => Just (x_val + y_val)
+
+maybeAdd' : Maybe Int -> Maybe Int -> Maybe Int
+maybeAdd' x y = x >>= \x_val =>
+                y >>= \y_val =>
+                Just (x_val + y_val)
+
+maybeAdd'' : Maybe Int -> Maybe Int -> Maybe Int
+maybeAdd'' x y = do x_val <- x
+                    y_val <- y
+                    Just (x_val + y_val)

tests/typedd-book/chapter06/Printf.idr

@@ -0,0 +1,28 @@
+data Format = Number Format
+            | Str Format
+            | Lit String Format
+            | End
+
+PrintfType : Format -> Type
+PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
+PrintfType (Str fmt) = (str : String) -> PrintfType fmt
+PrintfType (Lit str fmt) = PrintfType fmt
+PrintfType End = String
+
+printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
+printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
+printfFmt (Str fmt) acc = \str => printfFmt fmt (acc ++ str)
+printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit)
+printfFmt End acc = acc
+
+toFormat : (xs : List Char) -> Format
+toFormat [] = End
+toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
+toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
+toFormat ('%' :: chars) = Lit "%" (toFormat chars)
+toFormat (c :: chars) = case toFormat chars of
+                             Lit lit chars' => Lit (strCons c lit) chars'
+                             fmt => Lit (strCons c "") fmt
+
+printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
+printf fmt = printfFmt _ ""

tests/typedd-book/chapter06/TypeFuns.idr

@@ -0,0 +1,20 @@
+import Data.Strings
+import Data.Vect
+
+StringOrInt : Bool -> Type
+StringOrInt False = String
+StringOrInt True = Int
+
+getStringOrInt : (isInt : Bool) -> StringOrInt isInt
+getStringOrInt False = "Ninety four"
+getStringOrInt True = 94
+
+valToString : (isInt : Bool) -> StringOrInt isInt -> String
+valToString False y = trim y
+valToString True y = cast y
+
+valToString' : (isInt : Bool) -> (case isInt of
+                                       False => String
+                                       True => Int) -> String
+valToString' False y = trim y
+valToString' True y = cast y

tests/typedd-book/chapter06/TypeSynonyms.idr

@@ -0,0 +1,16 @@
+import Data.Vect
+
+tri : Vect 3 (Double, Double)
+tri = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]
+
+Position : Type
+Position = (Double, Double)
+
+tri' : Vect 3 Position
+tri' = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]
+
+Polygon : Nat -> Type
+Polygon n = Vect n Position
+
+tri'' : Polygon 3
+tri'' = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]

tests/typedd-book/chapter06/expected

@@ -0,0 +1,7 @@
+1/1: Building Adder (Adder.idr)
+1/1: Building DataStore (DataStore.idr)
+1/1: Building DataStoreHoles (DataStoreHoles.idr)
+1/1: Building Maybe (Maybe.idr)
+1/1: Building Printf (Printf.idr)
+1/1: Building TypeFuns (TypeFuns.idr)
+1/1: Building TypeSynonyms (TypeSynonyms.idr)

tests/typedd-book/chapter06/run

@@ -0,0 +1,9 @@
+$1 Adder.idr --check
+$1 DataStore.idr --check
+$1 DataStoreHoles.idr --check
+$1 Maybe.idr --check
+$1 Printf.idr --check
+$1 TypeFuns.idr --check
+$1 TypeSynonyms.idr --check
+
+rm -rf build