Fix environments for nested names

This was a slight difference from Blodwen that wasn't accounted for -
there might be lets in the nested environment, so when building the
expanded application type, make sure we go under them
This commit is contained in:
Edwin Brady 2019-06-27 15:25:26 +01:00
parent d053a18977
commit 211de419bb
7 changed files with 150 additions and 1 deletions

View File

@ -103,6 +103,8 @@ getVarType rigc nest env fc x
useVars [] sc = sc
useVars (a :: as) (Bind bfc n (Pi c _ ty) sc)
= Bind bfc n (Let c a ty) (useVars (map weaken as) sc)
useVars as (Bind bfc n (Let c v ty) sc)
= Bind bfc n (Let c v ty) (useVars (map weaken as) sc)
useVars _ sc = sc -- Can't happen?
isHole : NF vars -> Bool

View File

@ -24,7 +24,7 @@ ttimpTests
idrisTests : List String
idrisTests
= ["basic001", "basic002", "basic003", "basic004", "basic005",
"basic006", "basic007",
"basic006", "basic007", "basic008", "basic009",
"coverage001", "coverage002",
"error001", "error002", "error003", "error004", "error005",
"error006",

View File

@ -0,0 +1,24 @@
import Stuff
data IsSuc : Nat -> Type where
Yes : IsSuc (S x)
pred : (x : Nat) -> IsSuc x -> Nat
pred (S x) Yes = x
test1 : Nat -> Nat
test1 x = let y = S (S x) in
case x of
res => pred y ?foo
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect k a -> Vect (S k) a
test2 : Nat -> Nat -> Nat
test2 x@(S Z) y
= case y of
res =>
let fn : Vect (S Z) Nat -> Nat
fn ys = ?bar
in pred x Yes

View File

@ -0,0 +1,102 @@
-- a mini prelude
module Stuff
public export
data Bool = True | False
public export
not : Bool -> Bool
not True = False
not False = True
public export
data Maybe a = Nothing | Just a
infixl 4 &&
public export
(&&) : Bool -> Lazy Bool -> Bool
(&&) True x = x
(&&) False x = False
public export
intToBool : Int -> Bool
intToBool 0 = False
intToBool x = True
public export
ifThenElse : Bool -> Lazy a -> Lazy a -> a
ifThenElse True t e = t
ifThenElse False t e = e
public export
data Nat = Z | S Nat
public export
fromInteger : Integer -> Nat
fromInteger x = ifThenElse (intToBool (prim__eq_Integer x 0))
Z (S (fromInteger (prim__sub_Integer x 1)))
public export
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S k) y = S (plus k y)
infixr 5 ::
public export
data List a = Nil | (::) a (List a)
public export
data Equal : a -> b -> Type where
Refl : {0 x : a} -> Equal x x
public export
data Unit = MkUnit
public export
data Pair : Type -> Type -> Type where
MkPair : {0 a, b : Type} -> (1 x : a) -> (1 y : b) -> Pair a b
public export
fst : {0 a, b : Type} -> (a, b) -> a
fst (x, y) = x
public export
snd : {0 a, b : Type} -> (a, b) -> b
snd (x, y) = y
%pair Pair fst snd
namespace DPair
public export
data DPair : (a : Type) -> (a -> Type) -> Type where
MkDPair : (x : a) -> p x -> DPair a p
fst : DPair a p -> a
fst (MkDPair x y) = x
snd : (x : DPair a p) -> p (fst x)
snd (MkDPair x y) = y
public export
data Unrestricted : Type -> Type where
Un : (x : a) -> Unrestricted a
public export
the : (a : Type) -> a -> a
the _ x = x
public export
id : a -> a
id x = x
public export
data Void : Type where
public export
data Dec : Type -> Type where
Yes : a -> Dec a
No : (a -> Void) -> Dec a

View File

@ -0,0 +1,15 @@
1/2: Building Stuff (Stuff.idr)
2/2: Building LetCase (LetCase.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Main> y : Nat
res : Nat
x : Nat
-------------------------------------
foo : IsSuc (S (S x))
Main> x : Nat
res : Nat
y : Nat
ys : Vect (S Z) Nat
-------------------------------------
bar : Nat
Main> Bye for now!

View File

@ -0,0 +1,3 @@
:t foo
:t bar
:q

3
tests/idris2/basic009/run Executable file
View File

@ -0,0 +1,3 @@
$1 --no-prelude LetCase.idr < input
rm -rf build