mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-23 21:02:07 +03:00
Implement pragma for declaring nat optimizations
Co-authored-by: MarcelineVQ <marcythevq@gmail.com>
This commit is contained in:
Fabián Heredia Montiel
parent
7edef68739
commit
a8e099b770
@ -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 --
|
||||
-----------
|
||||
|
||||
@ -164,9 +164,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
|
||||
@ -257,7 +255,8 @@ getCompileData phase tm_in
|
||||
sopts <- getSession
|
||||
let ns = getRefs (Resolved (-1)) tm_in
|
||||
tm <- toFullNames tm_in
|
||||
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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -129,20 +130,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
|
||||
@ -269,16 +286,17 @@ mutual
|
||||
(f, args) =>
|
||||
do args' <- traverse (toCExp n) args
|
||||
defs <- get Ctxt
|
||||
builtins <- getBuiltins
|
||||
f' <- toCExpTm n f
|
||||
Arity a <- numArgs defs f
|
||||
| NewTypeBy arity pos =>
|
||||
do let res = applyNewType arity pos f' args'
|
||||
pure $ natHack res
|
||||
pure $ natHack builtins res
|
||||
| EraseArgs arity epos =>
|
||||
do let res = eraseConArgs arity epos f' args'
|
||||
pure $ natHack res
|
||||
pure $ natHack builtins res
|
||||
let res = expandToArity a f' args'
|
||||
pure $ natHack res
|
||||
pure $ natHack builtins res
|
||||
|
||||
mutual
|
||||
conCases : {auto c : Ref Ctxt Defs} ->
|
||||
|
||||
@ -27,7 +27,7 @@ import Data.Buffer
|
||||
-- TTC files can only be compatible if the version number is the same
|
||||
export
|
||||
ttcVersion : Int
|
||||
ttcVersion = 26
|
||||
ttcVersion = 27
|
||||
|
||||
export
|
||||
checkTTCVersion : String -> Int -> Int -> Core ()
|
||||
@ -117,10 +117,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
|
||||
@ -155,9 +168,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
|
||||
@ -331,11 +358,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} ->
|
||||
|
||||
@ -2031,6 +2031,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 ()
|
||||
@ -2080,26 +2192,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} ->
|
||||
|
||||
@ -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
|
||||
|
||||
@ -751,16 +751,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
|
||||
|
||||
@ -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!
|
||||
|
||||
@ -1035,6 +1035,9 @@ directive fname indents
|
||||
rw <- name
|
||||
atEnd indents
|
||||
pure (RewriteName eq rw)
|
||||
|
||||
-- Prim Cast
|
||||
|
||||
<|> do pragma "integerLit"
|
||||
n <- name
|
||||
atEnd indents
|
||||
@ -1047,6 +1050,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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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 ?{_:265}_[] ?{_:264}_[])")))))) 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 ?{_:254}_[] ?{_:253}_[])")))))) 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:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (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:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (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)
|
||||
|
||||
@ -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 ?{_:265}_[] ?{_:264}_[])")))))) 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 ?{_:254}_[] ?{_:253}_[])")))))) 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:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (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:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (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)
|
||||
|
||||
@ -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
|
||||
|
||||
Loading…
Reference in New Issue
Block a user