mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-24 21:34:36 +03:00
Delay case elaboration
This helps a few things because it delays elaboration of the block until as much as possible is known about its type. Also added a few libraries.
This commit is contained in:
Edwin Brady
parent
5eec46f6ce
commit
e526badfe2
@ -99,3 +99,9 @@ data NonEmpty : (xs : List a) -> Type where
|
||||
export
|
||||
Uninhabited (NonEmpty []) where
|
||||
uninhabited IsNonEmpty impossible
|
||||
|
||||
||| Convert any Foldable structure to a list.
|
||||
export
|
||||
toList : Foldable t => t a -> List a
|
||||
toList = foldr (::) []
|
||||
|
||||
|
||||
@ -25,3 +25,33 @@ isItJust : (v : Maybe a) -> Dec (IsJust v)
|
||||
isItJust (Just x) = Yes ItIsJust
|
||||
isItJust Nothing = No absurd
|
||||
|
||||
||| Convert a `Maybe a` value to an `a` value by providing a default `a` value
|
||||
||| in the case that the `Maybe` value is `Nothing`.
|
||||
public export
|
||||
fromMaybe : (Lazy a) -> Maybe a -> a
|
||||
fromMaybe def Nothing = def
|
||||
fromMaybe def (Just j) = j
|
||||
|
||||
||| Returns `Just` the given value if the conditional is `True`
|
||||
||| and `Nothing` if the conditional is `False`.
|
||||
public export
|
||||
toMaybe : Bool -> Lazy a -> Maybe a
|
||||
toMaybe True j = Just j
|
||||
toMaybe False j = Nothing
|
||||
|
||||
export
|
||||
justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y
|
||||
justInjective Refl = Refl
|
||||
|
||||
||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case
|
||||
||| that the `Maybe` value is `Nothing`.
|
||||
public export
|
||||
lowerMaybe : Monoid a => Maybe a -> a
|
||||
lowerMaybe Nothing = neutral
|
||||
lowerMaybe (Just x) = x
|
||||
|
||||
||| Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise.
|
||||
export
|
||||
raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a
|
||||
raiseToMaybe x = if x == neutral then Nothing else Just x
|
||||
|
||||
|
||||
@ -232,6 +232,25 @@ lcm _ Z = Z
|
||||
lcm Z _ = Z
|
||||
lcm a (S b) = divNat (a * (S b)) (gcd a (S b))
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- An informative comparison view
|
||||
--------------------------------------------------------------------------------
|
||||
public export
|
||||
data CmpNat : Nat -> Nat -> Type where
|
||||
CmpLT : (y : _) -> CmpNat x (x + S y)
|
||||
CmpEQ : CmpNat x x
|
||||
CmpGT : (x : _) -> CmpNat (y + S x) y
|
||||
|
||||
export
|
||||
total cmp : (x, y : Nat) -> CmpNat x y
|
||||
cmp Z Z = CmpEQ
|
||||
cmp Z (S k) = CmpLT _
|
||||
cmp (S k) Z = CmpGT _
|
||||
cmp (S x) (S y) with (cmp x y)
|
||||
cmp (S x) (S (x + (S k))) | CmpLT k = CmpLT k
|
||||
cmp (S x) (S x) | CmpEQ = CmpEQ
|
||||
cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k
|
||||
|
||||
-- Proofs on +
|
||||
|
||||
export
|
||||
@ -397,3 +416,5 @@ multOneRightNeutral (S left) =
|
||||
let inductiveHypothesis = multOneRightNeutral left in
|
||||
rewrite inductiveHypothesis in
|
||||
Refl
|
||||
|
||||
|
||||
|
||||
@ -4,6 +4,8 @@ import Data.List
|
||||
import Data.Nat
|
||||
import public Data.Fin
|
||||
|
||||
import Decidable.Equality
|
||||
|
||||
public export
|
||||
data Vect : (len : Nat) -> (elem : Type) -> Type where
|
||||
||| Empty vector
|
||||
@ -566,5 +568,252 @@ public export
|
||||
elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
|
||||
elemIndices = elemIndicesBy (==)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Filters
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| Find all elements of a vector that satisfy some test
|
||||
|||
|
||||
||| ```idris example
|
||||
||| filter (< 3) (fromList [1,2,3,4])
|
||||
||| ```
|
||||
filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
|
||||
filter p [] = ( _ ** [] )
|
||||
filter p (x::xs) =
|
||||
let (_ ** tail) = filter p xs
|
||||
in if p x then
|
||||
(_ ** x::tail)
|
||||
else
|
||||
(_ ** tail)
|
||||
|
||||
||| Make the elements of some vector unique by some test
|
||||
|||
|
||||
||| ```idris example
|
||||
||| nubBy (==) (fromList [1,2,2,3,4,4])
|
||||
||| ```
|
||||
-- nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
|
||||
-- nubBy = nubBy' []
|
||||
-- where
|
||||
-- nubBy' : forall len . Vect m elem -> (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
|
||||
-- nubBy' acc p [] = (_ ** [])
|
||||
-- nubBy' acc p (x::xs) with (elemBy p x acc)
|
||||
-- nubBy' acc p (x :: xs) | True = nubBy' acc p xs
|
||||
-- nubBy' acc p (x :: xs) | False with (nubBy' (x::acc) p xs)
|
||||
-- nubBy' acc p (x :: xs) | False | (_ ** tail) = (_ ** x::tail)
|
||||
--
|
||||
-- ||| Make the elements of some vector unique by the default Boolean equality
|
||||
-- |||
|
||||
-- ||| ```idris example
|
||||
-- ||| nub (fromList [1,2,2,3,4,4])
|
||||
-- ||| ```
|
||||
-- nub : Eq elem => Vect len elem -> (p ** Vect p elem)
|
||||
-- nub = nubBy (==)
|
||||
|
||||
||| Delete first element from list according to some test
|
||||
|||
|
||||
||| ```idris example
|
||||
||| deleteBy (<) 3 (fromList [1,2,2,3,4,4])
|
||||
||| ```
|
||||
deleteBy : {len : _} -> -- needed for the dependent pair
|
||||
(elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
|
||||
deleteBy _ _ [] = (_ ** [])
|
||||
deleteBy eq x (y::ys) =
|
||||
let (len ** zs) = deleteBy eq x ys
|
||||
in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
|
||||
|
||||
||| Delete first element from list equal to the given one
|
||||
|||
|
||||
||| ```idris example
|
||||
||| delete 2 (fromList [1,2,2,3,4,4])
|
||||
||| ```
|
||||
delete : {len : _} ->
|
||||
Eq elem => elem -> Vect len elem -> (p ** Vect p elem)
|
||||
delete = deleteBy (==)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Splitting and breaking lists
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| A tuple where the first element is a `Vect` of the `n` first elements and
|
||||
||| the second element is a `Vect` of the remaining elements of the original.
|
||||
||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),
|
||||
||| but is more efficient.
|
||||
|||
|
||||
||| @ n the index to split at
|
||||
||| @ xs the `Vect` to split in two
|
||||
|||
|
||||
||| ```idris example
|
||||
||| splitAt 2 (fromList [1,2,3,4])
|
||||
||| ```
|
||||
splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
|
||||
splitAt Z xs = ([], xs)
|
||||
splitAt (S k) (x :: xs) with (splitAt k {m} xs)
|
||||
splitAt (S k) (x :: xs) | (tk, dr) = (x :: tk, dr)
|
||||
|
||||
||| A tuple where the first element is a `Vect` of the `n` elements passing given test
|
||||
||| and the second element is a `Vect` of the remaining elements of the original.
|
||||
|||
|
||||
||| ```idris example
|
||||
||| partition (== 2) (fromList [1,2,3,2,4])
|
||||
||| ```
|
||||
partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
|
||||
partition p [] = ((_ ** []), (_ ** []))
|
||||
partition p (x::xs) =
|
||||
let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in
|
||||
if p x then
|
||||
((S leftLen ** x::lefts), (rightLen ** rights))
|
||||
else
|
||||
((leftLen ** lefts), (S rightLen ** x::rights))
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Predicates
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| Verify vector prefix
|
||||
|||
|
||||
||| ```idris example
|
||||
||| isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])
|
||||
||| ```
|
||||
isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
|
||||
isPrefixOfBy p [] right = True
|
||||
isPrefixOfBy p left [] = False
|
||||
isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
|
||||
|
||||
||| Verify vector prefix
|
||||
|||
|
||||
||| ```idris example
|
||||
||| isPrefixOf (fromList [1,2]) (fromList [1,2,3,4])
|
||||
||| ```
|
||||
isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
|
||||
isPrefixOf = isPrefixOfBy (==)
|
||||
|
||||
||| Verify vector suffix
|
||||
|||
|
||||
||| ```idris example
|
||||
||| isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])
|
||||
||| ```
|
||||
isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
|
||||
isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
|
||||
|
||||
||| Verify vector suffix
|
||||
|||
|
||||
||| ```idris example
|
||||
||| isSuffixOf (fromList [3,4]) (fromList [1,2,3,4])
|
||||
||| ```
|
||||
isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
|
||||
isSuffixOf = isSuffixOfBy (==)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Conversions
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| Convert Maybe type into Vect
|
||||
|||
|
||||
||| ```idris example
|
||||
||| maybeToVect (Just 2)
|
||||
||| ```
|
||||
maybeToVect : Maybe elem -> (p ** Vect p elem)
|
||||
maybeToVect Nothing = (_ ** [])
|
||||
maybeToVect (Just j) = (_ ** [j])
|
||||
|
||||
||| Convert first element of Vect (if exists) into Maybe.
|
||||
|||
|
||||
||| ```idris example
|
||||
||| vectToMaybe [2]
|
||||
||| ```
|
||||
vectToMaybe : Vect len elem -> Maybe elem
|
||||
vectToMaybe [] = Nothing
|
||||
vectToMaybe (x::xs) = Just x
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Misc
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| Filter out Nothings from Vect
|
||||
|||
|
||||
||| ```idris example
|
||||
||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
|
||||
||| ```
|
||||
catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
|
||||
catMaybes [] = (_ ** [])
|
||||
catMaybes (Nothing::xs) = catMaybes xs
|
||||
catMaybes ((Just j)::xs) =
|
||||
let (_ ** tail) = catMaybes xs
|
||||
in (_ ** j::tail)
|
||||
|
||||
||| Get diagonal elements
|
||||
|||
|
||||
||| ```idris example
|
||||
||| diag [[1,2,3], [4,5,6], [7,8,9]]
|
||||
||| ```
|
||||
diag : Vect len (Vect len elem) -> Vect len elem
|
||||
diag [] = []
|
||||
diag ((x::xs)::xss) = x :: diag (map tail xss)
|
||||
|
||||
range : {len : Nat} -> Vect len (Fin len)
|
||||
range {len=Z} = []
|
||||
range {len=S _} = FZ :: map FS range
|
||||
|
||||
||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
|
||||
|||
|
||||
||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).
|
||||
|||
|
||||
||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
|
||||
|||
|
||||
||| ```idris example
|
||||
||| transpose [[1,2], [3,4], [5,6], [7,8]]
|
||||
||| ```
|
||||
transpose : {n : _} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
|
||||
transpose [] = replicate _ [] -- = [| [] |]
|
||||
transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Applicative/Monad/Traversable
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- implementation Applicative (Vect k) where
|
||||
-- pure = replicate _
|
||||
-- fs <*> vs = zipWith apply fs vs
|
||||
--
|
||||
-- ||| This monad is different from the List monad, (>>=)
|
||||
-- ||| uses the diagonal.
|
||||
-- implementation Monad (Vect len) where
|
||||
-- m >>= f = diag (map f m)
|
||||
--
|
||||
-- implementation Traversable (Vect n) where
|
||||
-- traverse f [] = pure []
|
||||
-- traverse f (x :: xs) = pure (::) <*> (f x) <*> (traverse f xs)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Show
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
export
|
||||
implementation Show elem => Show (Vect len elem) where
|
||||
show = show . toList
|
||||
|
||||
-- Some convenience functions for testing lengths
|
||||
|
||||
-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we
|
||||
-- only know we don't know how to make a Vect n a, not that one can't exist.
|
||||
export
|
||||
exactLength : {m : Nat} -> -- expected at run-time
|
||||
(len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
|
||||
exactLength {m} len xs with (decEq m len)
|
||||
exactLength {m = m} m xs | (Yes Refl) = Just xs
|
||||
exactLength {m = m} len xs | (No contra) = Nothing
|
||||
|
||||
||| If the given Vect is at least the required length, return a Vect with
|
||||
||| at least that length in its type, otherwise return Nothing
|
||||
||| @len the required length
|
||||
||| @xs the vector with the desired length
|
||||
-- overLength : {m : Nat} -> -- expected at run-time
|
||||
-- (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a)
|
||||
-- overLength {m} n xs with (cmp m n)
|
||||
-- overLength {m = m} (plus m (S y)) xs | (CmpLT y) = Nothing
|
||||
-- overLength {m = m} m xs | CmpEQ
|
||||
-- = Just (0 ** xs)
|
||||
-- overLength {m = plus n (S x)} n xs | (CmpGT x)
|
||||
-- = Just (S x ** rewrite plusCommutative (S x) n in xs)
|
||||
|
||||
|
||||
|
||||
@ -1,5 +1,8 @@
|
||||
module Decidable.Equality
|
||||
|
||||
import Data.Maybe
|
||||
import Data.Nat
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Decidable equality
|
||||
--------------------------------------------------------------------------------
|
||||
@ -30,8 +33,57 @@ decEqSelfIsYes {x} with (decEq x x)
|
||||
--- Unit
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
export
|
||||
implementation DecEq () where
|
||||
decEq () () = Yes Refl
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Booleans
|
||||
--------------------------------------------------------------------------------
|
||||
total trueNotFalse : True = False -> Void
|
||||
trueNotFalse Refl impossible
|
||||
|
||||
export
|
||||
implementation DecEq Bool where
|
||||
decEq True True = Yes Refl
|
||||
decEq False False = Yes Refl
|
||||
decEq True False = No trueNotFalse
|
||||
decEq False True = No (negEqSym trueNotFalse)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Nat
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
total ZnotS : Z = S n -> Void
|
||||
ZnotS Refl impossible
|
||||
|
||||
export
|
||||
implementation DecEq Nat where
|
||||
decEq Z Z = Yes Refl
|
||||
decEq Z (S _) = No ZnotS
|
||||
decEq (S _) Z = No (negEqSym ZnotS)
|
||||
decEq (S n) (S m) with (decEq n m)
|
||||
decEq (S n) (S m) | Yes p = Yes $ cong S p
|
||||
decEq (S n) (S m) | No p = No $ \h : (S n = S m) => p $ succInjective n m h
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Maybe
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
total nothingNotJust : {x : t} -> (Nothing {ty = t} = Just x) -> Void
|
||||
nothingNotJust Refl impossible
|
||||
|
||||
export
|
||||
implementation (DecEq t) => DecEq (Maybe t) where
|
||||
decEq Nothing Nothing = Yes Refl
|
||||
decEq (Just x') (Just y') with (decEq x' y')
|
||||
decEq (Just x') (Just y') | Yes p = Yes $ cong Just p
|
||||
decEq (Just x') (Just y') | No p
|
||||
= No $ \h : Just x' = Just y' => p $ justInjective h
|
||||
decEq Nothing (Just _) = No nothingNotJust
|
||||
decEq (Just _) Nothing = No (negEqSym nothingNotJust)
|
||||
|
||||
-- TODO: Primitives and other prelude data types
|
||||
|
||||
|
||||
|
||||
|
||||
@ -35,17 +35,10 @@ snd (x, y) = y
|
||||
|
||||
namespace DPair
|
||||
public export
|
||||
data DPair : (a : Type) -> (a -> Type) -> Type where
|
||||
MkDPair : {0 a : Type} -> {0 p : a -> Type} ->
|
||||
(1 x : a) -> (1 y : p x)-> DPair a p
|
||||
|
||||
public export
|
||||
fst : DPair a p -> a
|
||||
fst (MkDPair x y) = x
|
||||
|
||||
public export
|
||||
snd : (x : DPair a p) -> p (fst x)
|
||||
snd (MkDPair x y) = y
|
||||
record DPair a (p : a -> Type) where
|
||||
constructor MkDPair
|
||||
fst : a
|
||||
snd : p fst
|
||||
|
||||
-- The empty type
|
||||
|
||||
|
||||
@ -592,7 +592,7 @@ dumpHole lvl hole
|
||||
++ if inj then " (Invertible)" else ""
|
||||
(BySearch _ _ _, ty) =>
|
||||
log lvl $ "Search " ++ show hole ++ " : " ++
|
||||
show !(normaliseHoles defs [] ty)
|
||||
show !(toFullNames !(normaliseHoles defs [] ty))
|
||||
(PMDef _ args t _ _, ty) =>
|
||||
log 4 $ "Solved: " ++ show hole ++ " : " ++
|
||||
show !(normalise defs [] ty) ++
|
||||
|
||||
@ -89,6 +89,9 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty
|
||||
oldhs <- if not incase
|
||||
then saveHoles
|
||||
else pure empty
|
||||
ust <- get UST
|
||||
let olddelayed = delayedElab ust
|
||||
put UST (record { delayedElab = [] } ust)
|
||||
|
||||
defs <- get Ctxt
|
||||
e <- newRef EST (initEStateSub defining env' sub)
|
||||
@ -108,8 +111,10 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty
|
||||
catch (retryDelayed (delayedElab ust))
|
||||
(\err =>
|
||||
do ust <- get UST
|
||||
put UST (record { delayedElab = [] } ust)
|
||||
put UST (record { delayedElab = olddelayed } ust)
|
||||
throw err)
|
||||
ust <- get UST
|
||||
put UST (record { delayedElab = olddelayed } ust)
|
||||
-- As long as we're not in a case block, finish off constraint solving
|
||||
when (not incase) $
|
||||
-- resolve any default hints
|
||||
|
||||
@ -252,10 +252,10 @@ checkAlternative rig elabinfo nest env fc (UniqueDefault def) alts mexpected
|
||||
let solvemode = case elabMode elabinfo of
|
||||
InLHS c => InLHS
|
||||
_ => InTerm
|
||||
solveConstraints solvemode Normal
|
||||
delayOnFailure fc rig env expected ambiguous $
|
||||
(\delayed =>
|
||||
do defs <- get Ctxt
|
||||
do solveConstraints solvemode Normal
|
||||
defs <- get Ctxt
|
||||
alts' <- pruneByType !(getNF expected) alts
|
||||
if delayed -- use the default if there's still ambiguity
|
||||
then try
|
||||
@ -278,10 +278,10 @@ checkAlternative rig elabinfo nest env fc uniq alts mexpected
|
||||
let solvemode = case elabMode elabinfo of
|
||||
InLHS c => InLHS
|
||||
_ => InTerm
|
||||
solveConstraints solvemode Normal
|
||||
delayOnFailure fc rig env expected ambiguous $
|
||||
(\delayed =>
|
||||
do defs <- get Ctxt
|
||||
do solveConstraints solvemode Normal
|
||||
defs <- get Ctxt
|
||||
alts' <- pruneByType !(getNF expected) alts
|
||||
exp <- getTerm expected
|
||||
-- If we don't know the target type on the first attempt,
|
||||
|
||||
@ -10,6 +10,7 @@ import Core.TT
|
||||
import Core.Value
|
||||
|
||||
import TTImp.Elab.Check
|
||||
import TTImp.Elab.Delayed
|
||||
import TTImp.Elab.ImplicitBind
|
||||
import TTImp.TTImp
|
||||
|
||||
@ -418,26 +419,27 @@ checkCase : {vars : _} ->
|
||||
Maybe (Glued vars) ->
|
||||
Core (Term vars, Glued vars)
|
||||
checkCase rig elabinfo nest env fc scr scrty_exp alts exp
|
||||
= do (scrtyv, scrtyt) <- check Rig0 elabinfo nest env scrty_exp
|
||||
(Just (gType fc))
|
||||
|
||||
logTerm 10 "Expected scrutinee type" scrtyv
|
||||
-- Try checking at the given multiplicity; if that doesn't work,
|
||||
-- try checking at Rig1 (meaning that we're using a linear variable
|
||||
-- so the scrutinee should be linear)
|
||||
(scrtm_in, gscrty, caseRig) <- handle
|
||||
(do c <- check RigW elabinfo nest env scr (Just (gnf env scrtyv))
|
||||
pure (fst c, snd c, RigW))
|
||||
(\err => case err of
|
||||
LinearMisuse _ _ Rig1 _
|
||||
=> do c <- check Rig1 elabinfo nest env scr
|
||||
(Just (gnf env scrtyv))
|
||||
pure (fst c, snd c, Rig1)
|
||||
e => throw e)
|
||||
scrty <- getTerm gscrty
|
||||
logTermNF 5 "Scrutinee type" env scrty
|
||||
checkConcrete !(getNF gscrty)
|
||||
caseBlock rig elabinfo fc nest env scr scrtm_in scrty caseRig alts exp
|
||||
= delayElab fc rig env exp $
|
||||
do (scrtyv, scrtyt) <- check Rig0 elabinfo nest env scrty_exp
|
||||
(Just (gType fc))
|
||||
|
||||
logTerm 10 "Expected scrutinee type" scrtyv
|
||||
-- Try checking at the given multiplicity; if that doesn't work,
|
||||
-- try checking at Rig1 (meaning that we're using a linear variable
|
||||
-- so the scrutinee should be linear)
|
||||
(scrtm_in, gscrty, caseRig) <- handle
|
||||
(do c <- check RigW elabinfo nest env scr (Just (gnf env scrtyv))
|
||||
pure (fst c, snd c, RigW))
|
||||
(\err => case err of
|
||||
LinearMisuse _ _ Rig1 _
|
||||
=> do c <- check Rig1 elabinfo nest env scr
|
||||
(Just (gnf env scrtyv))
|
||||
pure (fst c, snd c, Rig1)
|
||||
e => throw e)
|
||||
scrty <- getTerm gscrty
|
||||
logTermNF 5 "Scrutinee type" env scrty
|
||||
checkConcrete !(getNF gscrty)
|
||||
caseBlock rig elabinfo fc nest env scr scrtm_in scrty caseRig alts exp
|
||||
where
|
||||
-- For the moment, throw an error if we haven't been able to work out
|
||||
-- the type of the case scrutinee, because we'll need it to build the
|
||||
|
||||
@ -425,7 +425,7 @@ successful ((tm, elab) :: elabs)
|
||||
put MD md
|
||||
put Ctxt defs
|
||||
elabs' <- successful elabs
|
||||
pure (Left (tm, err) :: elabs'))
|
||||
pure (Left (tm, !(normaliseErr err)) :: elabs'))
|
||||
|
||||
export
|
||||
exactlyOne : {vars : _} ->
|
||||
|
||||
@ -75,6 +75,41 @@ delayOnFailure fc rig env expected pred elab
|
||||
pure (dtm, expected)
|
||||
else throw err)
|
||||
|
||||
export
|
||||
delayElab : {auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
FC -> RigCount -> Env Term vars ->
|
||||
(expected : Maybe (Glued vars)) ->
|
||||
Core (Term vars, Glued vars) ->
|
||||
Core (Term vars, Glued vars)
|
||||
delayElab {vars} fc rig env exp elab
|
||||
= do est <- get EST
|
||||
nm <- genName "delayed"
|
||||
expected <- mkExpected exp
|
||||
(ci, dtm) <- newDelayed fc Rig1 env nm !(getTerm expected)
|
||||
logGlueNF 5 ("Postponing elaborator " ++ show nm ++
|
||||
" for") env expected
|
||||
ust <- get UST
|
||||
put UST (record { delayedElab $=
|
||||
((ci, mkClosedElab fc env
|
||||
(do est <- get EST
|
||||
put EST (record { allowDelay = False } est)
|
||||
tm <- elab
|
||||
est <- get EST
|
||||
put EST (record { allowDelay = True } est)
|
||||
pure tm)) :: ) }
|
||||
ust)
|
||||
pure (dtm, expected)
|
||||
where
|
||||
mkExpected : Maybe (Glued vars) -> Core (Glued vars)
|
||||
mkExpected (Just ty) = pure ty
|
||||
mkExpected Nothing
|
||||
= do nm <- genName "delayTy"
|
||||
ty <- metaVar fc Rig0 env nm (TType fc)
|
||||
pure (gnf env ty)
|
||||
|
||||
export
|
||||
retryDelayed : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
|
||||
@ -1,6 +1,8 @@
|
||||
1/1: Building CaseInf (CaseInf.idr)
|
||||
CaseInf.idr:6:17--6:24:While processing right hand side of Main.test3bad at CaseInf.idr:6:1--9:1:
|
||||
Can't infer type for case scrutinee
|
||||
Ambiguous elaboration. Possible correct results:
|
||||
Builtin.Pair (Prelude.fromInteger 1) (Prelude.fromInteger 2)
|
||||
Builtin.MkPair (Prelude.fromInteger 1) (Prelude.fromInteger 2)
|
||||
Welcome to Idris 2 version 0.0. Enjoy yourself!
|
||||
Main> S (S (S Z))
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:17} Main.Nat (%pi Rig1 Explicit Just ws ((Main.Vect {k:17}) a) (%pi RigW Explicit Nothing a (%pi Rig1 Explicit Just zs ((Main.Vect (Main.S {k:17})) a) (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S (Main.S {k:17}))) m)) a))))))))))
|
||||
Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just n Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:44} Main.Nat (%pi Rig1 Explicit Just zs ((Main.Vect {k:44}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:44})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:44})) m)) a))))))))))))))
|
||||
Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just n Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:72} Main.Nat (%pi Rig0 Explicit Just zs ((Main.Vect {k:72}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:72})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:72}) a) ((Main.Vect ((Main.plus (Main.S {k:72})) m)) a)))))))))))))))
|
||||
Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just n Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:45} Main.Nat (%pi Rig1 Explicit Just zs ((Main.Vect {k:45}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:45})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:45})) m)) a))))))))))))))
|
||||
Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just n Main.Nat (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just xs ((Main.Vect n) a) (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:74} Main.Nat (%pi Rig0 Explicit Just zs ((Main.Vect {k:74}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:74})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:74}) a) ((Main.Vect ((Main.plus (Main.S {k:74})) m)) a)))))))))))))))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
Loading…
Reference in New Issue
Block a user