diff --git a/libs/base/Language/Reflection/TT.idr b/libs/base/Language/Reflection/TT.idr index ffe19422d..f5169e038 100644 --- a/libs/base/Language/Reflection/TT.idr +++ b/libs/base/Language/Reflection/TT.idr @@ -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 diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index c35c7cca8..77c708b7f 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/src/Compiler/Scheme/Common.idr @@ -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 diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 1e03b9b71..a077b01d1 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -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 () diff --git a/src/Core/Context.idr b/src/Core/Context.idr index ca05fa5f8..d57386c30 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -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 diff --git a/src/Core/Name.idr b/src/Core/Name.idr index 7ebee3ac2..7249d2c2b 100644 --- a/src/Core/Name.idr +++ b/src/Core/Name.idr @@ -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') diff --git a/src/Core/Reflect.idr b/src/Core/Reflect.idr index 43cebef65..de10c4554 100644 --- a/src/Core/Reflect.idr +++ b/src/Core/Reflect.idr @@ -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" diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index a02c4f4c2..ef195e404 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -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" diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index de2493f10..20745870c 100644 --- a/src/Core/UnifyState.idr +++ b/src/Core/UnifyState.idr @@ -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) diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 90816f0b4..aca91bb55 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -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 diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index d158baf6e..ac58418b6 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -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 diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 148768039..b1ea5bef6 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -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 diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index 1d15357a1..3e0995774 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -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)), diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr index 3c898c829..0c80af3bb 100644 --- a/src/Parser/Rule/Source.idr +++ b/src/Parser/Rule/Source.idr @@ -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) diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr index 6edc98ceb..d1e0956ca 100644 --- a/src/TTImp/ProcessRecord.idr +++ b/src/TTImp/ProcessRecord.idr @@ -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 : _} -> diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 8988822d6..6c4a49fdc 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -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 _ _ = []