idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

Implement postfix dotted application.

Browse Source
This commit is contained in:
Matus Tejiscak 2020-06-20 23:37:09 +02:00 committed by G. Allais
parent c4608745f7
commit 3484510f5a
15 changed files with 57 additions and 107 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/base/Language/Reflection/TT.idr
View File

@ -51,7 +51,6 @@ data Name = UN String -- user defined name
| MN String Int -- machine generated name
| NS (List String) Name -- name in a namespace
| DN String Name -- a name and how to display it
| RF String -- record field name
export
Show Name where
@ -64,7 +63,6 @@ Show Name where
show (UN x) = x
show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
show (DN str y) = str
show (RF n) = "." ++ n
public export
data Count = M0 | M1 | MW

1
src/Compiler/Scheme/Common.idr
View File

@ -36,7 +36,6 @@ schName (UN n) = schString n
schName (MN n i) = schString n ++ "-" ++ show i
schName (PV n d) = "pat--" ++ schName n
schName (DN _ n) = schName n
schName (RF n) = "rf--" ++ schString n
schName (Nested (i, x) n) = "n--" ++ show i ++ "-" ++ show x ++ "-" ++ schName n
schName (CaseBlock x y) = "case--" ++ schString x ++ "-" ++ show y
schName (WithBlock x y) = "with--" ++ schString x ++ "-" ++ show y

2
src/Core/Binary.idr
View File

@ -30,7 +30,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 36
ttcVersion = 37
export
checkTTCVersion : String -> Int -> Int -> Core ()

5
src/Core/Context.idr
View File

@ -1256,8 +1256,6 @@ visibleInAny nss n vis = any (\ns => visibleIn ns n vis) nss
reducibleIn : (nspace : List String) -> Name -> Visibility -> Bool
reducibleIn nspace (NS ns (UN n)) Export = isSuffixOf ns nspace
reducibleIn nspace (NS ns (UN n)) Private = isSuffixOf ns nspace
reducibleIn nspace (NS ns (RF n)) Export = isSuffixOf ns nspace
reducibleIn nspace (NS ns (RF n)) Private = isSuffixOf ns nspace
reducibleIn nspace n _ = True
export
@ -1873,9 +1871,6 @@ inCurrentNS n@(MN _ _)
inCurrentNS n@(DN _ _)
= do defs <- get Ctxt
pure (NS (currentNS defs) n)
inCurrentNS n@(RF _)
= do defs <- get Ctxt
pure (NS (currentNS defs) n)
inCurrentNS n = pure n
export

19
src/Core/Name.idr
View File

@ -12,7 +12,6 @@ data Name : Type where
MN : String -> Int -> Name -- machine generated name
PV : Name -> Int -> Name -- pattern variable name; int is the resolved function id
DN : String -> Name -> Name -- a name and how to display it
RF : String -> Name -- record field name
Nested : (Int, Int) -> Name -> Name -- nested function name
CaseBlock : String -> Int -> Name -- case block nested in (resolved) name
WithBlock : String -> Int -> Name -- with block nested in (resolved) name
@ -41,7 +40,6 @@ userNameRoot : Name -> Maybe String
userNameRoot (NS _ n) = userNameRoot n
userNameRoot (UN n) = Just n
userNameRoot (DN _ n) = userNameRoot n
userNameRoot (RF n) = Just ("." ++ n) -- TMP HACK
userNameRoot _ = Nothing
export
@ -59,7 +57,6 @@ nameRoot (UN n) = n
nameRoot (MN n _) = n
nameRoot (PV n _) = nameRoot n
nameRoot (DN _ n) = nameRoot n
nameRoot (RF n) = n
nameRoot (Nested _ inner) = nameRoot inner
nameRoot (CaseBlock n _) = "$" ++ show n
nameRoot (WithBlock n _) = "$" ++ show n
@ -79,13 +76,11 @@ showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
export
Show Name where
show (NS ns n@(RF _)) = showSep "." (reverse ns) ++ ".(" ++ show n ++ ")"
show (NS ns n) = showSep "." (reverse ns) ++ "." ++ show n
show (UN x) = x
show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}"
show (DN str n) = str
show (RF n) = "." ++ n
show (Nested (outer, idx) inner)
= show outer ++ ":" ++ show idx ++ ":" ++ show inner
show (CaseBlock outer i) = "case block in " ++ outer
@ -99,7 +94,6 @@ Eq Name where
(==) (MN x y) (MN x' y') = y == y' && x == x'
(==) (PV x y) (PV x' y') = x == x' && y == y'
(==) (DN _ n) (DN _ n') = n == n'
(==) (RF n) (RF n') = n == n'
(==) (Nested x y) (Nested x' y') = x == x' && y == y'
(==) (CaseBlock x y) (CaseBlock x' y') = y == y' && x == x'
(==) (WithBlock x y) (WithBlock x' y') = y == y' && x == x'
@ -112,11 +106,10 @@ nameTag (UN _) = 1
nameTag (MN _ _) = 2
nameTag (PV _ _) = 3
nameTag (DN _ _) = 4
nameTag (RF _) = 5
nameTag (Nested _ _) = 6
nameTag (CaseBlock _ _) = 7
nameTag (WithBlock _ _) = 8
nameTag (Resolved _) = 9
nameTag (Nested _ _) = 5
nameTag (CaseBlock _ _) = 6
nameTag (WithBlock _ _) = 7
nameTag (Resolved _) = 8
export
Ord Name where
@ -139,7 +132,6 @@ Ord Name where
GT => GT
LT => LT
compare (DN _ n) (DN _ n') = compare n n'
compare (RF n) (RF n') = compare n n'
compare (Nested x y) (Nested x' y')
= case compare y y' of
EQ => compare x x'
@ -184,9 +176,6 @@ nameEq (DN x t) (DN y t') with (decEq x y)
nameEq (DN y t) (DN y t) | (Yes Refl) | (Just Refl) = Just Refl
nameEq (DN y t) (DN y t') | (Yes Refl) | Nothing = Nothing
nameEq (DN x t) (DN y t') | (No p) = Nothing
nameEq (RF x) (RF y) with (decEq x y)
nameEq (RF y) (RF y) | (Yes Refl) = Just Refl
nameEq (RF x) (RF y) | (No contra) = Nothing
nameEq (Nested x y) (Nested x' y') with (decEq x x')
nameEq (Nested x y) (Nested x' y') | (No p) = Nothing
nameEq (Nested x y) (Nested x y') | (Yes Refl) with (nameEq y y')

6
src/Core/Reflect.idr
View File

@ -232,9 +232,6 @@ Reify Name where
=> do str' <- reify defs !(evalClosure defs str)
n' <- reify defs !(evalClosure defs n)
pure (DN str' n')
(NS _ (UN "RF"), [str])
=> do str' <- reify defs !(evalClosure defs str)
pure (RF str')
_ => cantReify val "Name"
reify defs val = cantReify val "Name"
@ -255,9 +252,6 @@ Reflect Name where
= do str' <- reflect fc defs lhs env str
n' <- reflect fc defs lhs env n
appCon fc defs (reflectiontt "DN") [str', n']
reflect fc defs lhs env (RF x)
= do x' <- reflect fc defs lhs env x
appCon fc defs (reflectiontt "RF") [x']
reflect fc defs lhs env (Resolved i)
= case !(full (gamma defs) (Resolved i)) of
Resolved _ => cantReflect fc "Name"

13
src/Core/TTC.idr
View File

@ -38,10 +38,9 @@ TTC Name where
toBuf b (MN x y) = do tag 2; toBuf b x; toBuf b y
toBuf b (PV x y) = do tag 3; toBuf b x; toBuf b y
toBuf b (DN x y) = do tag 4; toBuf b x; toBuf b y
toBuf b (RF x) = do tag 5; toBuf b x
toBuf b (Nested x y) = do tag 6; toBuf b x; toBuf b y
toBuf b (CaseBlock x y) = do tag 7; toBuf b x; toBuf b y
toBuf b (WithBlock x y) = do tag 8; toBuf b x; toBuf b y
toBuf b (Nested x y) = do tag 5; toBuf b x; toBuf b y
toBuf b (CaseBlock x y) = do tag 6; toBuf b x; toBuf b y
toBuf b (WithBlock x y) = do tag 7; toBuf b x; toBuf b y
toBuf b (Resolved x)
= throw (InternalError ("Can't write resolved name " ++ show x))
@ -62,14 +61,12 @@ TTC Name where
y <- fromBuf b
pure (DN x y)
5 => do x <- fromBuf b
pure (RF x)
6 => do x <- fromBuf b
y <- fromBuf b
pure (Nested x y)
7 => do x <- fromBuf b
6 => do x <- fromBuf b
y <- fromBuf b
pure (CaseBlock x y)
8 => do x <- fromBuf b
7 => do x <- fromBuf b
y <- fromBuf b
pure (WithBlock x y)
_ => corrupt "Name"

1
src/Core/UnifyState.idr
View File

@ -124,7 +124,6 @@ genMVName : {auto c : Ref Ctxt Defs} ->
Name -> Core Name
genMVName (UN str) = genName str
genMVName (MN str _) = genName str
genMVName (RF str) = genName str
genMVName n
= do ust <- get UST
put UST (record { nextName $= (+1) } ust)

10
src/Idris/Desugar.idr
View File

@ -348,12 +348,12 @@ mutual
desugarB side ps (PApp fc (PApp fc (PRef fc (UN "rangeFromThen")) start) n)
desugarB side ps (PUnifyLog fc lvl tm)
= pure $ IUnifyLog fc lvl !(desugarB side ps tm)
desugarB side ps (PRecordFieldAccess fc rec fields)
= desugarB side ps $ foldl (\r, f => PApp fc (PRef fc f) r) rec fields
desugarB side ps (PRecordProjection fc fields)
desugarB side ps (PPostfixApp fc rec projs)
= desugarB side ps $ foldl (\x, proj => PApp fc (PRef fc proj) x) rec projs
desugarB side ps (PPostfixAppPartial fc projs)
= desugarB side ps $
PLam fc top Explicit (PRef fc (MN "rec" 0)) (PImplicit fc) $
foldl (\r, f => PApp fc (PRef fc f) r) (PRef fc (MN "rec" 0)) fields
PLam fc top Explicit (PRef fc (MN "paRoot" 0)) (PImplicit fc) $
foldl (\r, proj => PApp fc (PRef fc proj) r) (PRef fc (MN "paRoot" 0)) projs
desugarB side ps (PWithUnambigNames fc ns rhs)
= IWithUnambigNames fc ns <$> desugarB side ps rhs

17
src/Idris/Parser.idr
View File

@ -337,19 +337,19 @@ mutual
simpleExpr : FileName -> IndentInfo -> Rule PTerm
simpleExpr fname indents
= do
= do -- .y.z
start <- location
recFields <- some recField
projs <- some dotIdent
end <- location
pure $ PRecordProjection (MkFC fname start end) recFields
<|> do
pure $ PPostfixAppPartial (MkFC fname start end) projs
<|> do -- x.y.z
start <- location
root <- simplerExpr fname indents
recFields <- many recField
projs <- many dotIdent
end <- location
pure $ case recFields of
pure $ case projs of
[] => root
fs => PRecordFieldAccess (MkFC fname start end) root recFields
fs => PPostfixApp (MkFC fname start end) root projs
simplerExpr : FileName -> IndentInfo -> Rule PTerm
simplerExpr fname indents
@ -715,13 +715,12 @@ mutual
where
fieldName : Name -> String
fieldName (UN s) = s
fieldName (RF s) = s
fieldName _ = "_impossible"
-- this allows the dotted syntax .field
-- but also the arrowed syntax ->field for compatibility with Idris 1
recFieldCompat : Rule Name
recFieldCompat = recField <|> (symbol "->" *> name)
recFieldCompat = dotIdent <|> (symbol "->" *> name)
rewrite_ : FileName -> IndentInfo -> Rule PTerm
rewrite_ fname indents

28
src/Idris/Syntax.idr
View File

@ -90,10 +90,10 @@ mutual
PRange : FC -> PTerm -> Maybe PTerm -> PTerm -> PTerm
-- A stream range [x,y..]
PRangeStream : FC -> PTerm -> Maybe PTerm -> PTerm
-- record field access (r.x.y)
PRecordFieldAccess : FC -> PTerm -> List Name -> PTerm
-- record projection (.x.y)
PRecordProjection : FC -> List Name -> PTerm
-- r.x.y
PPostfixApp : FC -> PTerm -> List Name -> PTerm
-- .x.y
PPostfixAppPartial : FC -> List Name -> PTerm
-- Debugging
PUnifyLog : FC -> Nat -> PTerm -> PTerm
@ -147,8 +147,8 @@ mutual
getPTermLoc (PRewrite fc _ _) = fc
getPTermLoc (PRange fc _ _ _) = fc
getPTermLoc (PRangeStream fc _ _) = fc
getPTermLoc (PRecordFieldAccess fc _ _) = fc
getPTermLoc (PRecordProjection fc _) = fc
getPTermLoc (PPostfixApp fc _ _) = fc
getPTermLoc (PPostfixAppPartial fc _) = fc
getPTermLoc (PUnifyLog fc _ _) = fc
getPTermLoc (PWithUnambigNames fc _ _) = fc
@ -583,10 +583,10 @@ mutual
showPrec d (PRangeStream _ start (Just next))
= "[" ++ showPrec d start ++ ", " ++ showPrec d next ++ " .. ]"
showPrec d (PUnifyLog _ lvl tm) = showPrec d tm
showPrec d (PRecordFieldAccess fc rec fields)
= showPrec d rec ++ concatMap show fields
showPrec d (PRecordProjection fc fields)
= concatMap show fields
showPrec d (PPostfixApp fc rec fields)
= showPrec d rec ++ concatMap (\n => "." ++ show n) fields
showPrec d (PPostfixAppPartial fc fields)
= concatMap (\n => "." ++ show n) fields
showPrec d (PWithUnambigNames fc ns rhs)
= "with " ++ show ns ++ " " ++ showPrec d rhs
@ -875,11 +875,11 @@ mapPTermM f = goPTerm where
goPTerm (PUnifyLog fc k x) =
PUnifyLog fc k <$> goPTerm x
>>= f
goPTerm (PRecordFieldAccess fc rec fields) =
PRecordFieldAccess fc <$> goPTerm rec <*> pure fields
goPTerm (PPostfixApp fc rec fields) =
PPostfixApp fc <$> goPTerm rec <*> pure fields
>>= f
goPTerm (PRecordProjection fc fields) =
f (PRecordProjection fc fields)
goPTerm (PPostfixAppPartial fc fields) =
f (PPostfixAppPartial fc fields)
goPTerm (PWithUnambigNames fc ns rhs) =
PWithUnambigNames fc ns <$> goPTerm rhs
>>= f

12
src/Parser/Lexer/Source.idr
View File

@ -22,8 +22,8 @@ data Token
-- Identifiers
| HoleIdent String
| Ident String
| DotSepIdent (List String)
| RecordField String
| DotSepIdent (List String) -- ident.ident
| DotIdent String -- .ident
| Symbol String
-- Comments
| Comment String
@ -46,7 +46,7 @@ Show Token where
show (HoleIdent x) = "hole identifier " ++ x
show (Ident x) = "identifier " ++ x
show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (reverse xs)
show (RecordField x) = "record field " ++ x
show (DotIdent x) = "dot+identifier " ++ x
show (Symbol x) = "symbol " ++ x
-- Comments
show (Comment _) = "comment"
@ -110,8 +110,8 @@ docComment = is '|' <+> is '|' <+> is '|' <+> many (isNot '\n')
holeIdent : Lexer
holeIdent = is '?' <+> identNormal
recField : Lexer
recField = is '.' <+> identNormal
dotIdent : Lexer
dotIdent = is '.' <+> identNormal
pragma : Lexer
pragma = is '%' <+> identNormal
@ -208,7 +208,7 @@ rawTokens =
(digits, \x => IntegerLit (cast x)),
(stringLit, \x => StringLit (stripQuotes x)),
(charLit, \x => CharLit (stripQuotes x)),
(recField, \x => RecordField (assert_total $ strTail x)),
(dotIdent, \x => DotIdent (assert_total $ strTail x)),
(namespacedIdent, parseNamespace),
(identNormal, parseIdent),
(pragma, \x => Pragma (assert_total $ strTail x)),

12
src/Parser/Rule/Source.idr
View File

@ -78,11 +78,11 @@ strLit
_ => Nothing)
export
recField : Rule Name
recField
= terminal "Expected record field"
dotIdent : Rule Name
dotIdent
= terminal "Expected dot+identifier"
(\x => case tok x of
RecordField s => Just (RF s)
DotIdent s => Just (UN s)
_ => Nothing)
export
@ -197,12 +197,12 @@ name = opNonNS <|> do
else pure $ NS xs (UN x)
opNonNS : Rule Name
opNonNS = symbol "(" *> (operator <|> recField) <* symbol ")"
opNonNS = symbol "(" *> operator <* symbol ")"
opNS : List String -> Rule Name
opNS ns = do
symbol ".("
n <- (operator <|> recField)
n <- operator
symbol ")"
pure (NS ns n)

19
src/TTImp/ProcessRecord.idr
View File

@ -50,17 +50,13 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
-- Go into new namespace, if there is one, for getters
case newns of
Nothing =>
do elabGetters conName 0 [] RF [] conty -- make dotted projections
when addUndotted $
elabGetters conName 0 [] UN [] conty -- make undotted projections
elabGetters conName 0 [] [] conty -- make undotted projections
Just ns =>
do let cns = currentNS defs
let nns = nestedNS defs
extendNS [ns]
newns <- getNS
elabGetters conName 0 [] RF [] conty -- make dotted projections
when addUndotted $
elabGetters conName 0 [] UN [] conty -- make undotted projections
elabGetters conName 0 [] [] conty -- make undotted projections
defs <- get Ctxt
-- Record that the current namespace is allowed to look
-- at private names in the nested namespace
@ -126,18 +122,17 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
List (Name, RawImp) -> -- names to update in types
-- (for dependent records, where a field's type may depend
-- on an earlier projection)
(String -> Name) ->
Env Term vs -> Term vs ->
Core ()
elabGetters con done upds mkProjName tyenv (Bind bfc n b@(Pi rc imp ty_chk) sc)
elabGetters con done upds tyenv (Bind bfc n b@(Pi rc imp ty_chk) sc)
= if (n `elem` map fst params) || (n `elem` vars)
then elabGetters con
(if imp == Explicit && not (n `elem` vars)
then S done else done)
upds mkProjName (b :: tyenv) sc
upds (b :: tyenv) sc
else
do let fldNameStr = nameRoot n
projNameNS <- inCurrentNS (mkProjName fldNameStr)
projNameNS <- inCurrentNS (UN fldNameStr)
ty <- unelab tyenv ty_chk
let ty' = substNames vars upds ty
@ -178,9 +173,9 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
elabGetters con
(if imp == Explicit
then S done else done)
upds' mkProjName (b :: tyenv) sc
upds' (b :: tyenv) sc
elabGetters con done upds _ _ _ = pure ()
elabGetters con done upds _ _ = pure ()
export
processRecord : {vars : _} ->

17
src/TTImp/TTImp.idr
View File

@ -538,7 +538,6 @@ definedInBlock ns decls =
expandNS : List String -> Name -> Name
expandNS [] n = n
expandNS ns (UN n) = NS ns (UN n)
expandNS ns (RF n) = NS ns (RF n)
expandNS ns n@(MN _ _) = NS ns n
expandNS ns n@(DN _ _) = NS ns n
expandNS ns n = n
@ -556,25 +555,11 @@ definedInBlock ns decls =
fldns' : List String
fldns' = maybe ns (\f => f :: ns) fldns
toRF : Name -> Name
toRF (UN n) = RF n
toRF n = n
fnsUN : List Name
fnsUN = map getFieldName flds
fnsRF : List Name
fnsRF = map toRF fnsUN
-- Depending on %undotted_record_projections,
-- the record may or may not produce undotted projections (fnsUN).
--
-- However, since definedInBlock is pure, we can't check that flag
-- (and it would also be wrong if %undotted_record_projections appears
-- inside the parameter block)
-- so let's just declare all of them and some may go unused.
all : List Name
all = expandNS ns n :: map (expandNS fldns') (fnsRF ++ fnsUN)
all = expandNS ns n :: map (expandNS fldns') fnsUN
defName _ _ = []