edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-29 15:52:29 +03:00
Code Issues Projects Releases Wiki Activity

Allow type annotations on lets

Browse Source 
Fixes #87
This commit is contained in:
Edwin Brady 2020-02-01 12:17:54 +00:00
parent 284a3ded69
commit 4fed357fb4
7 changed files with 63 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/Idris/Desugar.idr
View File

@ -386,18 +386,20 @@ mutual
(Implicit fc False)
(PatClause fc bpat rest'
:: alts')))
expandDo side ps topfc (DoLet fc n rig tm :: rest)
expandDo side ps topfc (DoLet fc n rig ty tm :: rest)
= do tm' <- desugar side ps tm
ty' <- desugar side ps ty
rest' <- expandDo side ps topfc rest
pure $ ILet fc rig n (Implicit fc False) tm' rest'
expandDo side ps topfc (DoLetPat fc pat tm alts :: rest)
pure $ ILet fc rig n ty' tm' rest'
expandDo side ps topfc (DoLetPat fc pat ty tm alts :: rest)
= do pat' <- desugar LHS ps pat
ty' <- desugar side ps ty
(newps, bpat) <- bindNames False pat'
tm' <- desugar side ps tm
alts' <- traverse (desugarClause ps True) alts
let ps' = newps ++ ps
rest' <- expandDo side ps' topfc rest
pure $ ICase fc tm' (Implicit fc False)
pure $ ICase fc tm' ty'
(PatClause fc bpat rest'
:: alts')
expandDo side ps topfc (DoLetLocal fc decls :: rest)

26
src/Idris/Parser.idr
View File

@ -488,40 +488,44 @@ mutual
= PLam fc rig Explicit pat ty (bindAll fc rest scope)
letBinder : FileName -> IndentInfo ->
Rule (FilePos, FilePos, RigCount, PTerm, PTerm, List PClause)
Rule (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause)
letBinder fname indents
= do start <- location
rigc <- multiplicity
pat <- expr plhs fname indents
tyend <- location
ty <- option (PImplicit (MkFC fname start tyend))
(do symbol ":"
typeExpr (pnoeq pdef) fname indents)
symbol "="
val <- expr pnowith fname indents
alts <- block (patAlt fname)
end <- location
rig <- getMult rigc
pure (start, end, rig, pat, val, alts)
pure (start, end, rig, pat, ty, val, alts)
buildLets : FileName ->
List (FilePos, FilePos, RigCount, PTerm, PTerm, List PClause) ->
List (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause) ->
PTerm -> PTerm
buildLets fname [] sc = sc
buildLets fname ((start, end, rig, pat, val, alts) :: rest) sc
buildLets fname ((start, end, rig, pat, ty, val, alts) :: rest) sc
= let fc = MkFC fname start end in
PLet fc rig pat (PImplicit fc) val
PLet fc rig pat ty val
(buildLets fname rest sc) alts
buildDoLets : FileName ->
List (FilePos, FilePos, RigCount, PTerm, PTerm, List PClause) ->
List (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause) ->
List PDo
buildDoLets fname [] = []
buildDoLets fname ((start, end, rig, PRef fc' (UN n), val, []) :: rest)
buildDoLets fname ((start, end, rig, PRef fc' (UN n), ty, val, []) :: rest)
= let fc = MkFC fname start end in
if lowerFirst n
then DoLet fc (UN n) rig val :: buildDoLets fname rest
else DoLetPat fc (PRef fc' (UN n)) val []
then DoLet fc (UN n) rig ty val :: buildDoLets fname rest
else DoLetPat fc (PRef fc' (UN n)) ty val []
:: buildDoLets fname rest
buildDoLets fname ((start, end, rig, pat, val, alts) :: rest)
buildDoLets fname ((start, end, rig, pat, ty, val, alts) :: rest)
= let fc = MkFC fname start end in
DoLetPat fc pat val alts :: buildDoLets fname rest
DoLetPat fc pat ty val alts :: buildDoLets fname rest
let_ : FileName -> IndentInfo -> Rule PTerm
let_ fname indents

12
src/Idris/Syntax.idr
View File

@ -106,8 +106,8 @@ mutual
DoExp : FC -> PTerm -> PDo
DoBind : FC -> Name -> PTerm -> PDo
DoBindPat : FC -> PTerm -> PTerm -> List PClause -> PDo
DoLet : FC -> Name -> RigCount -> PTerm -> PDo
DoLetPat : FC -> PTerm -> PTerm -> List PClause -> PDo
DoLet : FC -> Name -> RigCount -> PTerm -> PTerm -> PDo
DoLetPat : FC -> PTerm -> PTerm -> PTerm -> List PClause -> PDo
DoLetLocal : FC -> List PDecl -> PDo
DoRewrite : FC -> PTerm -> PDo
@ -116,8 +116,8 @@ mutual
getLoc (DoExp fc _) = fc
getLoc (DoBind fc _ _) = fc
getLoc (DoBindPat fc _ _ _) = fc
getLoc (DoLet fc _ _ _) = fc
getLoc (DoLetPat fc _ _ _) = fc
getLoc (DoLet fc _ _ _ _) = fc
getLoc (DoLetPat fc _ _ _ _) = fc
getLoc (DoLetLocal fc _) = fc
getLoc (DoRewrite fc _) = fc
@ -348,8 +348,8 @@ mutual
showDo (DoBind _ n tm) = show n ++ " <- " ++ show tm
showDo (DoBindPat _ l tm alts)
= show l ++ " <- " ++ show tm ++ concatMap showAlt alts
showDo (DoLet _ l rig tm) = "let " ++ show l ++ " = " ++ show tm
showDo (DoLetPat _ l tm alts)
showDo (DoLet _ l rig _ tm) = "let " ++ show l ++ " = " ++ show tm
showDo (DoLetPat _ l _ tm alts)
= "let " ++ show l ++ " = " ++ show tm ++ concatMap showAlt alts
showDo (DoLetLocal _ ds)
-- We'll never see this when displaying a normal form...

2
tests/Main.idr
View File

@ -29,7 +29,7 @@ idrisTests
"basic016", "basic017", "basic018", "basic019", "basic020",
"basic021", "basic022", "basic023", "basic024", "basic025",
"basic026", "basic027", "basic028", "basic029", "basic030",
"basic031", "basic032", "basic033",
"basic031", "basic032", "basic033", "basic034",
"coverage001", "coverage002", "coverage003", "coverage004",
"error001", "error002", "error003", "error004", "error005",
"error006", "error007", "error008", "error009", "error010",

7
tests/idris2/basic034/expected Normal file
View File

@ -0,0 +1,7 @@
1/1: Building lets (lets.idr)
lets.idr:22:39--23:14:While processing right hand side of Main.dolet2 at lets.idr:21:1--26:1:
When unifying Maybe Int and Maybe String
Mismatch between:
Int
and
String

25
tests/idris2/basic034/lets.idr Normal file
View File

@ -0,0 +1,25 @@
data A : Type where
The : Type -> A
U : A -> Type
U (The x) = x
works : (a : A) -> (H : U a) -> (let q = H in Nat)
works a h = 0
fails : (a : A) -> (H : U a) -> (let q : U a = H in Nat)
fails a h = 0
dolet : Maybe Int -> Maybe Int -> Maybe Int
dolet x y
= do let Just x' : Maybe Int = x
| Nothing => Nothing
y' <- y
pure (x' + y')
dolet2 : Maybe Int -> Maybe Int -> Maybe Int
dolet2 x y
= do let Just x' : Maybe String = x
| Nothing => Nothing
y' <- y
pure (x' + y')

3
tests/idris2/basic034/run Normal file
View File

@ -0,0 +1,3 @@
$1 --check lets.idr
rm -rf build