diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr index 9825df2cf..2d09a4823 100644 --- a/libs/prelude/Prelude.idr +++ b/libs/prelude/Prelude.idr @@ -692,6 +692,9 @@ for = flip traverse -- NATS --- ----------- +%builtinNatZero Z +%builtinNatSucc S + ||| Natural numbers: unbounded, unsigned integers which can be pattern matched. public export data Nat = @@ -702,6 +705,9 @@ data Nat = %name Nat k, j, i +%builtinIntegerToNat integerToNat +%builtinNatToInteger natToInteger + public export integerToNat : Integer -> Nat integerToNat x @@ -709,6 +715,17 @@ integerToNat x then Z else S (assert_total (integerToNat (prim__sub_Integer x 1))) +public export +natToInteger : Nat -> Integer +natToInteger Z = 0 +natToInteger (S k) = 1 + natToInteger k + -- integer (+) may be non-linear in second + -- argument + +%builtinNatAdd plus +%builtinNatSub minus +%builtinNatMul mult + -- Define separately so we can spot the name when optimising Nats ||| Add two natural numbers. ||| @ x the number to case-split on @@ -752,13 +769,6 @@ Ord Nat where compare (S k) Z = GT compare (S j) (S k) = compare j k -public export -natToInteger : Nat -> Integer -natToInteger Z = 0 -natToInteger (S k) = 1 + natToInteger k - -- integer (+) may be non-linear in second - -- argument - ----------- -- PAIRS -- ----------- diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index 23a32a8cb..c7b7ff09a 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -104,9 +104,7 @@ natHackNames : List Name natHackNames = [UN "prim__add_Integer", UN "prim__sub_Integer", - UN "prim__mul_Integer", - NS ["Prelude"] (UN "natToInteger"), - NS ["Prelude"] (UN "integerToNat")] + UN "prim__mul_Integer"] export fastAppend : List String -> String @@ -196,7 +194,8 @@ getCompileData tm = do defs <- get Ctxt sopts <- getSession let ns = getRefs (Resolved (-1)) tm - natHackNames' <- traverse toResolvedNames natHackNames + builtins <- getBuiltins + natHackNames' <- traverse toResolvedNames (natHackNames ++ getDefinedBuiltinNames builtins) -- make an array of Bools to hold which names we've found (quicker -- to check than a NameMap!) asize <- getNextEntry diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index 624e5a800..7bd3b37a0 100644 --- a/src/Compiler/CompileExpr.idr +++ b/src/Compiler/CompileExpr.idr @@ -6,6 +6,7 @@ import Core.Context import Core.Env import Core.Name import Core.Normalise +import Core.Options import Core.TT import Core.Value @@ -136,20 +137,36 @@ mkDropSubst i es rest (x :: xs) -- NOTE: Make sure that names mentioned here are listed in 'natHackNames' in -- Common.idr, so that they get compiled, as they won't be spotted by the -- usual calls to 'getRefs'. -natHack : CExp vars -> CExp vars -natHack (CCon fc (NS ["Prelude"] (UN "Z")) _ []) = CPrimVal fc (BI 0) -natHack (CCon fc (NS ["Prelude"] (UN "S")) _ [k]) - = CApp fc (CRef fc (UN "prim__add_Integer")) [CPrimVal fc (BI 1), k] -natHack (CApp fc (CRef _ (NS ["Prelude"] (UN "natToInteger"))) [k]) = k -natHack (CApp fc (CRef _ (NS ["Prelude"] (UN "integerToNat"))) [k]) = k -natHack (CApp fc (CRef fc' (NS ["Prelude"] (UN "plus"))) args) - = CApp fc (CRef fc' (UN "prim__add_Integer")) args -natHack (CApp fc (CRef fc' (NS ["Prelude"] (UN "mult"))) args) - = CApp fc (CRef fc' (UN "prim__mul_Integer")) args -natHack (CApp fc (CRef fc' (NS ["Nat", "Data"] (UN "minus"))) args) - = CApp fc (CRef fc' (UN "prim__sub_Integer")) args -natHack (CLam fc x exp) = CLam fc x (natHack exp) -natHack t = t +natHack : PrimBuiltinNames -> CExp vars -> CExp vars +natHack primBuiltinNames (CCon fc name t []) + = if Just name == builtinNatZero primBuiltinNames + then CPrimVal fc (BI 0) + else (CCon fc name t []) +natHack primBuiltinNames (CCon fc name t [k]) + = if Just name == builtinNatSucc primBuiltinNames + then CApp fc (CRef fc (UN "prim__add_Integer")) [CPrimVal fc (BI 1), k] + else (CCon fc name t [k]) +natHack primBuiltinNames (CApp fc (CRef fc' name) [k]) + = if Just name == builtinNatToInteger primBuiltinNames + then k + else if Just name == builtinIntegerToNat primBuiltinNames + then k + else (CApp fc (CRef fc' name) [k]) +natHack primBuiltinNames (CApp fc (CRef fc' name) args) + = if Just name == builtinNatAdd primBuiltinNames + then CApp fc (CRef fc' (UN "prim__add_Integer")) args + else if Just name == builtinNatSub primBuiltinNames + then CApp fc (CRef fc' (UN "prim__sub_Integer")) args + else if Just name == builtinNatMul primBuiltinNames + then CApp fc (CRef fc' (UN "prim__mul_Integer")) args + else if Just name == builtinNatDiv primBuiltinNames + then CApp fc (CRef fc' (UN "prim__div_Integer")) args + else if Just name == builtinNatMod primBuiltinNames + then CApp fc (CRef fc' (UN "prim__mod_Integer")) args + else (CApp fc (CRef fc' name) args) + -- TODO: Eq, LT, LTE, GT, GTE +natHack p (CLam fc x exp) = CLam fc x (natHack p exp) +natHack _ t = t isNatCon : Name -> Bool isNatCon (NS ["Prelude"] (UN "Z")) = True @@ -247,15 +264,16 @@ mutual (f, args) => do args' <- traverse (toCExp tags n) args defs <- get Ctxt + builtins <- getBuiltins Arity a <- numArgs defs f | NewTypeBy arity pos => do let res = applyNewType arity pos !(toCExpTm tags n f) args' - pure $ natHack res + pure $ natHack builtins res | EraseArgs arity epos => do let res = eraseConArgs arity epos !(toCExpTm tags n f) args' - pure $ natHack res + pure $ natHack builtins res let res = expandToArity a !(toCExpTm tags n f) args' - pure $ natHack res + pure $ natHack builtins res mutual conCases : {auto c : Ref Ctxt Defs} -> diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index b536d1c9f..7aca25656 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -27,7 +27,7 @@ import Data.Buffer -- TTC files can only be compatible if the version number is the same export ttcVersion : Int -ttcVersion = 23 +ttcVersion = 24 export checkTTCVersion : String -> Int -> Int -> Core () @@ -111,10 +111,23 @@ HasNames e => HasNames (TTCFile e) where fullRW gam (Just (MkRewriteNs e r)) = pure $ Just $ MkRewriteNs !(full gam e) !(full gam r) - fullPrim : Context -> PrimNames -> Core PrimNames - fullPrim gam (MkPrimNs mi ms mc) - = pure $ MkPrimNs !(full gam mi) !(full gam ms) !(full gam mc) + fullPrimCast : Context -> PrimCastNames -> Core PrimCastNames + fullPrimCast gam (MkPrimCastNames i str c) + = pure $ MkPrimCastNames !(full gam i) !(full gam str) !(full gam c) + + fullPrimBuiltin : Context -> PrimBuiltinNames -> Core PrimBuiltinNames + fullPrimBuiltin gam (MkPrimBuiltinNames natZero natSucc natToInteger integerToNat + natAdd natSub natMul natDiv natRem natEq natLT natLTE natGT natGTE) + = pure $ MkPrimBuiltinNames !(full gam natZero) !(full gam natSucc) !(full gam natToInteger) + !(full gam integerToNat) !(full gam natAdd) !(full gam natSub) !(full gam natMul) + !(full gam natDiv) !(full gam natRem) !(full gam natEq) !(full gam natLT) + !(full gam natLTE) !(full gam natGT) !(full gam natGTE) + fullPrim : Context -> PrimNames -> Core PrimNames + fullPrim gam (MkPrimNames primCastNames primBuiltinNames) + = do castNames <- fullPrimCast gam primCastNames + builtinNames <- fullPrimBuiltin gam primBuiltinNames + pure $ MkPrimNames castNames builtinNames -- I don't think we ever actually want to call this, because after we read -- from the file we're going to add them to learn what the resolved names @@ -148,9 +161,23 @@ HasNames e => HasNames (TTCFile e) where resolvedRW gam (Just (MkRewriteNs e r)) = pure $ Just $ MkRewriteNs !(resolved gam e) !(resolved gam r) + resolvedPrimCast : Context -> PrimCastNames -> Core PrimCastNames + resolvedPrimCast gam (MkPrimCastNames i str c) + = pure $ MkPrimCastNames !(resolved gam i) !(resolved gam str) !(resolved gam c) + + resolvedPrimBuiltin : Context -> PrimBuiltinNames -> Core PrimBuiltinNames + resolvedPrimBuiltin gam (MkPrimBuiltinNames natZero natSucc natToInteger integerToNat + natAdd natSub natMul natDiv natRem natEq natLT natLTE natGT natGTE) + = pure $ MkPrimBuiltinNames !(resolved gam natZero) !(resolved gam natSucc) !(resolved gam natToInteger) + !(resolved gam integerToNat) !(resolved gam natAdd) !(resolved gam natSub) !(resolved gam natMul) + !(resolved gam natDiv) !(resolved gam natRem) !(resolved gam natEq) !(resolved gam natLT) + !(resolved gam natLTE) !(resolved gam natGT) !(resolved gam natGTE) + resolvedPrim : Context -> PrimNames -> Core PrimNames - resolvedPrim gam (MkPrimNs mi ms mc) - = pure $ MkPrimNs !(resolved gam mi) !(resolved gam ms) !(resolved gam mc) + resolvedPrim gam (MkPrimNames primCastNames primBuiltinNames) + = do castNames <- resolvedPrimCast gam primCastNames + builtinNames <- resolvedPrimBuiltin gam primBuiltinNames + pure $ MkPrimNames castNames builtinNames asName : List String -> Maybe (List String) -> Name -> Name @@ -320,11 +347,34 @@ updateRewrite r put Ctxt (record { options->rewritenames $= (r <+>) } defs) export -updatePrimNames : PrimNames -> PrimNames -> PrimNames -updatePrimNames p +updatePrimCastNames : PrimCastNames -> PrimCastNames -> PrimCastNames +updatePrimCastNames p = record { fromIntegerName $= ((fromIntegerName p) <+>), fromStringName $= ((fromStringName p) <+>), fromCharName $= ((fromCharName p) <+>) } +export +updatePrimBuiltinNames : PrimBuiltinNames -> PrimBuiltinNames -> PrimBuiltinNames +updatePrimBuiltinNames p + = record { builtinNatZero $= ((builtinNatZero p) <+>), + builtinNatSucc $= ((builtinNatSucc p) <+>), + builtinNatToInteger $= ((builtinNatToInteger p) <+>), + builtinIntegerToNat $= ((builtinIntegerToNat p) <+>), + builtinNatAdd $= ((builtinNatAdd p) <+>), + builtinNatSub $= ((builtinNatSub p) <+>), + builtinNatMul $= ((builtinNatMul p) <+>), + builtinNatDiv $= ((builtinNatDiv p) <+>), + builtinNatMod $= ((builtinNatMod p) <+>), + builtinNatEq $= ((builtinNatEq p) <+>), + builtinNatLT $= ((builtinNatLT p) <+>), + builtinNatLTE $= ((builtinNatLTE p) <+>), + builtinNatGT $= ((builtinNatGT p) <+>), + builtinNatGTE $= ((builtinNatGTE p) <+>) } + +export +updatePrimNames : PrimNames -> PrimNames -> PrimNames +updatePrimNames p + = record { primCastNames $= updatePrimCastNames . primCastNames $ p, + primBuiltinNames $= updatePrimBuiltinNames . primBuiltinNames $ p } export updatePrims : {auto c : Ref Ctxt Defs} -> diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 6080bb733..a50a5d088 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -1982,6 +1982,118 @@ setFromChar n = do defs <- get Ctxt put Ctxt (record { options $= setFromChar n } defs) +export +setBuiltinNatZero : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinNatZero n + = do defs <- get Ctxt + ns <- getNS + put Ctxt (record {options $= setBuiltinNatZero (NS ns n) } defs) + +export +setBuiltinNatSucc : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinNatSucc n + = do defs <- get Ctxt + ns <- getNS + put Ctxt (record {options $= setBuiltinNatSucc (NS ns n) } defs) + +export +setBuiltinNatToInteger : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinNatToInteger n + = do defs <- get Ctxt + ns <- getNS + put Ctxt (record {options $= setBuiltinNatToInteger (NS ns n) } defs) + +export +setBuiltinIntegerToNat : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinIntegerToNat n + = do defs <- get Ctxt + ns <- getNS + put Ctxt (record {options $= setBuiltinIntegerToNat (NS ns n) } defs) + +export +setBuiltinNatAdd : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinNatAdd n + = do defs <- get Ctxt + ns <- getNS + put Ctxt (record {options $= setBuiltinNatAdd (NS ns n) } defs) + +export +setBuiltinNatSub : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinNatSub n + = do defs <- get Ctxt + ns <- getNS + put Ctxt (record {options $= setBuiltinNatSub (NS ns n) } defs) + +export +setBuiltinNatMul : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinNatMul n + = do defs <- get Ctxt + ns <- getNS + put Ctxt (record {options $= setBuiltinNatMul (NS ns n) } defs) + +export +setBuiltinNatDiv : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinNatDiv n + = do defs <- get Ctxt + ns <- getNS + put Ctxt (record {options $= setBuiltinNatDiv (NS ns n) } defs) + +export +setBuiltinNatMod : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinNatMod n + = do defs <- get Ctxt + ns <- getNS + put Ctxt(record {options $= setBuiltinNatMod (NS ns n) } defs) + +export +setBuiltinNatEq : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinNatEq n + = do defs <- get Ctxt + ns <- getNS + put Ctxt(record {options $= setBuiltinNatEq (NS ns n) } defs) + +export +setBuiltinNatLT : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinNatLT n + = do defs <- get Ctxt + ns <- getNS + put Ctxt(record {options $= setBuiltinNatLT (NS ns n) } defs) + +export +setBuiltinNatLTE : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinNatLTE n + = do defs <- get Ctxt + ns <- getNS + put Ctxt(record {options $= setBuiltinNatLTE (NS ns n) } defs) + +export +setBuiltinNatGT : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinNatGT n + = do defs <- get Ctxt + ns <- getNS + put Ctxt(record {options $= setBuiltinNatGT (NS ns n) } defs) + +export +setBuiltinNatGTE : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setBuiltinNatGTE n + = do defs <- get Ctxt + ns <- getNS + put Ctxt(record {options $= setBuiltinNatGTE (NS ns n) } defs) + export addNameDirective : {auto c : Ref Ctxt Defs} -> FC -> Name -> List String -> Core () @@ -2031,26 +2143,36 @@ isEqualTy n Nothing => pure False Just r => pure $ !(getFullName n) == !(getFullName (equalType r)) +-- Get Cast functions from Built-in Types + export fromIntegerName : {auto c : Ref Ctxt Defs} -> Core (Maybe Name) fromIntegerName = do defs <- get Ctxt - pure $ fromIntegerName (primnames (options defs)) + pure . fromIntegerName . primCastNames . primnames . options $ defs export fromStringName : {auto c : Ref Ctxt Defs} -> Core (Maybe Name) fromStringName = do defs <- get Ctxt - pure $ fromStringName (primnames (options defs)) + pure . fromStringName . primCastNames . primnames . options $ defs export fromCharName : {auto c : Ref Ctxt Defs} -> Core (Maybe Name) fromCharName = do defs <- get Ctxt - pure $ fromCharName (primnames (options defs)) + pure . fromCharName . primCastNames . primnames . options $ defs + +-- Get Optimization Hints for some Elemental Types like Nat and their functions + +export +getBuiltins : {auto c : Ref Ctxt Defs} -> Core PrimBuiltinNames +getBuiltins + = do defs <- get Ctxt + pure . primBuiltinNames . primnames . options $ defs export setLogLevel : {auto c : Ref Ctxt Defs} -> diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 1a3d419b0..c4936e039 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -69,12 +69,37 @@ record RewriteNames where rewriteName : Name public export -record PrimNames where - constructor MkPrimNs +record PrimCastNames where + constructor MkPrimCastNames fromIntegerName : Maybe Name fromStringName : Maybe Name fromCharName : Maybe Name +public export +record PrimBuiltinNames where + constructor MkPrimBuiltinNames + -- Naturals + builtinNatZero : Maybe Name + builtinNatSucc : Maybe Name + builtinNatToInteger : Maybe Name + builtinIntegerToNat : Maybe Name + builtinNatAdd : Maybe Name + builtinNatSub : Maybe Name + builtinNatMul : Maybe Name + builtinNatDiv : Maybe Name + builtinNatMod : Maybe Name + builtinNatEq : Maybe Name + builtinNatLT : Maybe Name + builtinNatLTE : Maybe Name + builtinNatGT : Maybe Name + builtinNatGTE : Maybe Name + +public export +record PrimNames where + constructor MkPrimNames + primCastNames : PrimCastNames + primBuiltinNames : PrimBuiltinNames + public export data LangExt = Borrowing -- not yet implemented @@ -142,8 +167,8 @@ pathSep : Char pathSep = if isWindows then ';' else ':' defaultDirs : Dirs -defaultDirs = MkDirs "." Nothing "build" - ("build" ++ dirSep ++ "exec") +defaultDirs = MkDirs "." Nothing "build" + ("build" ++ dirSep ++ "exec") "/usr/local" ["."] [] [] defaultPPrint : PPrinter @@ -156,22 +181,39 @@ defaultSession = MkSessionOpts False False False Chez 0 False False defaultElab : ElabDirectives defaultElab = MkElabDirectives True True PartialOK 3 True +defaultPrimNames : PrimNames +defaultPrimNames = + MkPrimNames + (MkPrimCastNames Nothing Nothing Nothing) + (MkPrimBuiltinNames Nothing Nothing Nothing Nothing Nothing Nothing Nothing + Nothing Nothing Nothing Nothing Nothing Nothing Nothing) + export defaults : Options defaults = MkOptions defaultDirs defaultPPrint defaultSession - defaultElab Nothing Nothing - (MkPrimNs Nothing Nothing Nothing) + defaultElab Nothing Nothing defaultPrimNames [] +-- Getters + +export +getDefinedBuiltinNames : PrimBuiltinNames -> List Name +getDefinedBuiltinNames primBuiltinNames = catMaybes $ + [builtinNatZero, builtinNatSucc, builtinNatToInteger, builtinIntegerToNat, + builtinNatAdd, builtinNatSub, builtinNatMul, builtinNatDiv, builtinNatMod, + builtinNatEq, builtinNatLT, builtinNatLTE, builtinNatGT, builtinNatGTE] <*> [primBuiltinNames] + -- Reset the options which are set by source files export clearNames : Options -> Options clearNames = record { pairnames = Nothing, rewritenames = Nothing, - primnames = MkPrimNs Nothing Nothing Nothing, + primnames = defaultPrimNames, extensions = [] } +-- Setters + export setPair : (pairType : Name) -> (fstn : Name) -> (sndn : Name) -> Options -> Options @@ -183,15 +225,71 @@ setRewrite eq rw = record { rewritenames = Just (MkRewriteNs eq rw) } export setFromInteger : Name -> Options -> Options -setFromInteger n = record { primnames->fromIntegerName = Just n } +setFromInteger n = record { primnames->primCastNames->fromIntegerName = Just n } export setFromString : Name -> Options -> Options -setFromString n = record { primnames->fromStringName = Just n } +setFromString n = record { primnames->primCastNames->fromStringName = Just n } export setFromChar : Name -> Options -> Options -setFromChar n = record { primnames->fromCharName = Just n } +setFromChar n = record { primnames->primCastNames->fromCharName = Just n } + +export +setBuiltinNatZero : Name -> Options -> Options +setBuiltinNatZero n = record { primnames->primBuiltinNames->builtinNatZero = Just n } + +export +setBuiltinNatSucc : Name -> Options -> Options +setBuiltinNatSucc n = record { primnames->primBuiltinNames->builtinNatSucc = Just n } + +export +setBuiltinNatToInteger : Name -> Options -> Options +setBuiltinNatToInteger n = record { primnames->primBuiltinNames->builtinNatToInteger = Just n } + +export +setBuiltinIntegerToNat : Name -> Options -> Options +setBuiltinIntegerToNat n = record { primnames->primBuiltinNames->builtinIntegerToNat = Just n } + +export +setBuiltinNatAdd : Name -> Options -> Options +setBuiltinNatAdd n = record { primnames->primBuiltinNames->builtinNatAdd = Just n } + +export +setBuiltinNatSub : Name -> Options -> Options +setBuiltinNatSub n = record { primnames->primBuiltinNames->builtinNatSub = Just n } + +export +setBuiltinNatMul : Name -> Options -> Options +setBuiltinNatMul n = record { primnames->primBuiltinNames->builtinNatMul = Just n } + +export +setBuiltinNatDiv : Name -> Options -> Options +setBuiltinNatDiv n = record { primnames->primBuiltinNames->builtinNatDiv = Just n } + +export +setBuiltinNatMod : Name -> Options -> Options +setBuiltinNatMod n = record { primnames->primBuiltinNames->builtinNatMod = Just n } + +export +setBuiltinNatEq : Name -> Options -> Options +setBuiltinNatEq n = record { primnames->primBuiltinNames->builtinNatEq = Just n } + +export +setBuiltinNatLT : Name -> Options -> Options +setBuiltinNatLT n = record { primnames->primBuiltinNames->builtinNatLT = Just n } + +export +setBuiltinNatLTE : Name -> Options -> Options +setBuiltinNatLTE n = record { primnames->primBuiltinNames->builtinNatLTE = Just n } + +export +setBuiltinNatGT : Name -> Options -> Options +setBuiltinNatGT n = record { primnames->primBuiltinNames->builtinNatGT = Just n } + +export +setBuiltinNatGTE : Name -> Options -> Options +setBuiltinNatGTE n = record { primnames->primBuiltinNames->builtinNatGTE = Just n } export setExtension : LangExt -> Options -> Options diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index 00c97228b..9ceef3a76 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -749,16 +749,61 @@ TTC RewriteNames where pure (MkRewriteNs ty l) export -TTC PrimNames where +TTC PrimCastNames where toBuf b l = do toBuf b (fromIntegerName l) toBuf b (fromStringName l) toBuf b (fromCharName l) fromBuf b = do i <- fromBuf b - str <- fromBuf b - c <- fromBuf b - pure (MkPrimNs i str c) + str <- fromBuf b + c <- fromBuf b + pure (MkPrimCastNames i str c) + +export +TTC PrimBuiltinNames where + toBuf b l + = do toBuf b (builtinNatZero l) + toBuf b (builtinNatSucc l) + toBuf b (builtinNatToInteger l) + toBuf b (builtinIntegerToNat l) + toBuf b (builtinNatAdd l) + toBuf b (builtinNatSub l) + toBuf b (builtinNatMul l) + toBuf b (builtinNatDiv l) + toBuf b (builtinNatMod l) + toBuf b (builtinNatEq l) + toBuf b (builtinNatLT l) + toBuf b (builtinNatLTE l) + toBuf b (builtinNatGT l) + toBuf b (builtinNatGTE l) + fromBuf b + = do natZero <- fromBuf b + natSucc <- fromBuf b + natToInteger <- fromBuf b + integerToNat <- fromBuf b + natAdd <- fromBuf b + natSub <- fromBuf b + natMul <- fromBuf b + natDiv <- fromBuf b + natMod <- fromBuf b + natEq <- fromBuf b + natLT <- fromBuf b + natLTE <- fromBuf b + natGT <- fromBuf b + natGTE <- fromBuf b + pure (MkPrimBuiltinNames natZero natSucc natToInteger integerToNat + natAdd natSub natMul natDiv natMod natEq natLT natLTE natGT natGTE) + +export +TTC PrimNames where + toBuf b l + = do toBuf b (primCastNames l) + toBuf b (primBuiltinNames l) + fromBuf b + = do castNames <- fromBuf b + builtinNames <- fromBuf b + pure (MkPrimNames castNames builtinNames) export TTC HoleInfo where diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 51eb84a33..83dbb80f0 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -807,9 +807,25 @@ mutual AmbigDepth n => pure [IPragma (\c, nest, env => setAmbigLimit n)] PairNames ty f s => pure [IPragma (\c, nest, env => setPair fc ty f s)] RewriteName eq rw => pure [IPragma (\c, nest, env => setRewrite fc eq rw)] + -- Prim Cast PrimInteger n => pure [IPragma (\c, nest, env => setFromInteger n)] PrimString n => pure [IPragma (\c, nest, env => setFromString n)] PrimChar n => pure [IPragma (\c, nest, env => setFromChar n)] + -- Prim Nat Optimizations + PrimNatZero n => pure [IPragma (\c, nest, env => setBuiltinNatZero n)] + PrimNatSucc n => pure [IPragma (\c, nest, env => setBuiltinNatSucc n)] + PrimNatToInteger n => pure [IPragma (\c, nest, env => setBuiltinNatToInteger n)] + PrimIntegerToNat n => pure [IPragma (\c, nest, env => setBuiltinIntegerToNat n)] + PrimNatAdd n => pure [IPragma (\c, nest, env => setBuiltinNatAdd n)] + PrimNatSub n => pure [IPragma (\c, nest, env => setBuiltinNatSub n)] + PrimNatMul n => pure [IPragma (\c, nest, env => setBuiltinNatMul n)] + PrimNatDiv n => pure [IPragma (\c, nest, env => setBuiltinNatDiv n)] + PrimNatMod n => pure [IPragma (\c, nest, env => setBuiltinNatMod n)] + PrimNatEq n => pure [IPragma (\c, nest, env => setBuiltinNatEq n)] + PrimNatLT n => pure [IPragma (\c, nest, env => setBuiltinNatLT n)] + PrimNatLTE n => pure [IPragma (\c, nest, env => setBuiltinNatLTE n)] + PrimNatGT n => pure [IPragma (\c, nest, env => setBuiltinNatGT n)] + PrimNatGTE n => pure [IPragma (\c, nest, env => setBuiltinNatGTE n)] CGAction cg dir => pure [IPragma (\c, nest, env => addDirective cg dir)] Names n ns => pure [IPragma (\c, nest, env => addNameDirective fc n ns)] StartExpr tm => pure [IPragma (\c, nest, env => throw (InternalError "%start not implemented"))] -- TODO! diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 3a28abc7d..3a23bfec8 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1033,6 +1033,9 @@ directive fname indents rw <- name atEnd indents pure (RewriteName eq rw) + + -- Prim Cast + <|> do pragma "integerLit" n <- name atEnd indents @@ -1045,6 +1048,66 @@ directive fname indents n <- name atEnd indents pure (PrimChar n) + + -- Prim Nat Optimizations + + <|> do pragma "builtinNatZero" + n <- name + atEnd indents + pure (PrimNatZero n) + <|> do pragma "builtinNatSucc" + n <- name + atEnd indents + pure (PrimNatSucc n) + <|> do pragma "builtinNatToInteger" + n <- name + atEnd indents + pure (PrimNatToInteger n) + <|> do pragma "builtinIntegerToNat" + n <- name + atEnd indents + pure (PrimIntegerToNat n) + <|> do pragma "builtinNatAdd" + n <- name + atEnd indents + pure (PrimNatAdd n) + <|> do pragma "builtinNatSub" + n <- name + atEnd indents + pure (PrimNatSub n) + <|> do pragma "builtinNatMul" + n <- name + atEnd indents + pure (PrimNatMul n) + <|> do pragma "builtinNatDiv" + n <- name + atEnd indents + pure (PrimNatDiv n) + <|> do pragma "builtinNatMod" + n <- name + atEnd indents + pure (PrimNatMod n) + <|> do pragma "builtinNatEq" + n <- name + atEnd indents + pure (PrimNatEq n) + <|> do pragma "builtinNatLT" + n <- name + atEnd indents + pure (PrimNatLT n) + <|> do pragma "builtinNatLTE" + n <- name + atEnd indents + pure (PrimNatLTE n) + <|> do pragma "builtinNatGT" + n <- name + atEnd indents + pure (PrimNatGT n) + <|> do pragma "builtinNatGTE" + n <- name + atEnd indents + pure (PrimNatGTE n) + <|> do pragma "name" n <- name ns <- sepBy1 (symbol ",") unqualifiedName diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 9584d56e9..1f7fffa9f 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -158,9 +158,25 @@ mutual AmbigDepth : Nat -> Directive PairNames : Name -> Name -> Name -> Directive RewriteName : Name -> Name -> Directive + -- Prim Casting PrimInteger : Name -> Directive PrimString : Name -> Directive PrimChar : Name -> Directive + -- Prim Nat Optimizations + PrimNatZero : Name -> Directive + PrimNatSucc : Name -> Directive + PrimNatToInteger : Name -> Directive + PrimIntegerToNat : Name -> Directive + PrimNatAdd : Name -> Directive + PrimNatSub : Name -> Directive + PrimNatMul : Name -> Directive + PrimNatDiv : Name -> Directive + PrimNatMod : Name -> Directive + PrimNatEq : Name -> Directive + PrimNatLT : Name -> Directive + PrimNatLTE : Name -> Directive + PrimNatGT : Name -> Directive + PrimNatGTE : Name -> Directive CGAction : String -> String -> Directive Names : Name -> List String -> Directive StartExpr : PTerm -> Directive diff --git a/tests/ideMode/ideMode001/expected b/tests/ideMode/ideMode001/expected index 3270bc4d0..0f7aab0e6 100644 --- a/tests/ideMode/ideMode001/expected +++ b/tests/ideMode/ideMode001/expected @@ -8,7 +8,7 @@ 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1) 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1) 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:249}_[] ?{_:248}_[])")))))) 1) -0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:239} : (Main.Vect n[0] a[1])) -> (({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:735:1--742:1 n[2] m[4]) a[3])))")))))) 1) +0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:239} : (Main.Vect n[0] a[1])) -> (({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:752:1--759:1 n[2] m[4]) a[3])))")))))) 1) 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1) 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1) 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1) diff --git a/tests/ideMode/ideMode003/expected b/tests/ideMode/ideMode003/expected index 0ebd0e1b1..2fd81076b 100644 --- a/tests/ideMode/ideMode003/expected +++ b/tests/ideMode/ideMode003/expected @@ -8,7 +8,7 @@ 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1) 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1) 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:249}_[] ?{_:248}_[])")))))) 1) -0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:239} : (Main.Vect n[0] a[1])) -> (({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:735:1--742:1 n[2] m[4]) a[3])))")))))) 1) +0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:239} : (Main.Vect n[0] a[1])) -> (({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:752:1--759:1 n[2] m[4]) a[3])))")))))) 1) 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1) 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1) 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1) diff --git a/tests/idris2/total006/expected b/tests/idris2/total006/expected index 9671e7a7d..a2b94fca9 100644 --- a/tests/idris2/total006/expected +++ b/tests/idris2/total006/expected @@ -1,6 +1,6 @@ 1/1: Building Total (Total.idr) Main> Main.count is total -Main> Main.badCount is possibly not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:1004:1--1009:1 -> Prelude.map +Main> Main.badCount is possibly not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:1014:1--1019:1 -> Prelude.map Main> Main.process is total Main> Main.badProcess is possibly not terminating due to recursive path Main.badProcess -> Main.badProcess -> Main.badProcess Main> Main.doubleInt is total