idris 0.10.2 → 0.10.3
raw patch · 69 files changed
+2125/−516 lines, 69 filesdep +terminal-sizedep −hscurses
Dependencies added: terminal-size
Dependencies removed: hscurses
Files
- CHANGELOG +16/−0
- idris.cabal +17/−9
- libs/base/Control/Monad/State.idr +1/−1
- libs/base/Language/Reflection/Utils.idr +23/−10
- libs/contrib/CFFI.idr +4/−0
- libs/contrib/CFFI/Memory.idr +94/−0
- libs/contrib/CFFI/Types.idr +159/−0
- libs/contrib/Classes/Verified.idr +1/−1
- libs/contrib/contrib.ipkg +3/−1
- libs/effects/Effects.idr +92/−33
- libs/prelude/Builtins.idr +7/−0
- libs/prelude/IO.idr +17/−0
- libs/prelude/Language/Reflection/Elab.idr +44/−3
- libs/pruviloj/Pruviloj/Internals.idr +0/−10
- rts/getline.c +32/−31
- rts/idris_bitstring.c +86/−86
- rts/idris_gc.c +24/−17
- rts/idris_gmp.c +18/−18
- rts/idris_heap.c +105/−5
- rts/idris_heap.h +82/−0
- rts/idris_rts.c +101/−45
- rts/idris_rts.h +52/−13
- src/IRTS/CodegenC.hs +32/−10
- src/IRTS/Lang.hs +9/−7
- src/Idris/AbsSyntax.hs +1/−1
- src/Idris/AbsSyntaxTree.hs +3/−0
- src/Idris/Core/Elaborate.hs +19/−5
- src/Idris/Core/Evaluate.hs +5/−1
- src/Idris/Core/ProofState.hs +12/−4
- src/Idris/Coverage.hs +8/−7
- src/Idris/Elab/Clause.hs +24/−18
- src/Idris/Elab/Data.hs +2/−64
- src/Idris/Elab/Instance.hs +4/−2
- src/Idris/Elab/RunElab.hs +5/−3
- src/Idris/Elab/Term.hs +166/−24
- src/Idris/Elab/Transform.hs +10/−6
- src/Idris/Elab/Type.hs +4/−3
- src/Idris/Elab/Utils.hs +63/−0
- src/Idris/Elab/Value.hs +3/−2
- src/Idris/Interactive.hs +1/−1
- src/Idris/Parser/Expr.hs +1/−1
- src/Idris/Parser/Helpers.hs +22/−26
- src/Idris/Prover.hs +1/−1
- src/Idris/Reflection.hs +19/−3
- src/Util/ScreenSize.hs +2/−20
- stack.yaml +13/−13
- test/Makefile +1/−1
- test/ffi007/expected +1/−0
- test/ffi007/ffi007.c +4/−0
- test/ffi007/ffi007.h +2/−0
- test/ffi007/ffi007.idr +9/−0
- test/ffi008/expected +5/−0
- test/ffi008/ffi008.c +14/−0
- test/ffi008/ffi008.h +17/−0
- test/ffi008/ffi008.idr +48/−0
- test/ffi008/run +4/−0
- test/interactive001/expected +1/−0
- test/meta002/AgdaStyleReflection.idr +0/−7
- test/meta002/DataDef.idr +73/−0
- test/meta002/expected +4/−1
- test/meta002/run +1/−0
- test/primitives006/Data/ByteArray.idr +100/−0
- test/primitives006/Data/Bytes.idr +287/−0
- test/primitives006/array.c +62/−0
- test/primitives006/array.h +18/−0
- test/primitives006/expected +9/−0
- test/primitives006/load-test.idr +48/−0
- test/primitives006/run +6/−0
- test/pruviloj001/pruviloj001.idr +4/−2
CHANGELOG view
@@ -23,6 +23,22 @@ * C function pointers can be called. * Idris can access pointers to C globals. +Effects+-------++* Effects can now be given in any order in effect lists (there is no need+for the ordering to be preserved in sub lists of effects)++Elaborator reflection updates+-----------------------------++* Datatypes can now be defined from elaborator reflection:+ - declareDatatype adds the type constructor declaration to the context+ - defineDatatype adds the constructors to the datatype+ - To declare an inductive-recursive family, declare the types of the+ function and the type constructor before defining the pattern-match+ cases and constructors.+ Minor language changes ----------------------
idris.cabal view
@@ -1,5 +1,5 @@ Name: idris-Version: 0.10.2+Version: 0.10.3 License: BSD3 License-file: LICENSE Author: Edwin Brady@@ -124,6 +124,8 @@ libs/contrib/contrib.ipkg libs/contrib/Makefile+ libs/contrib/*.idr+ libs/contrib/CFFI/*.idr libs/contrib/Classes/*.idr libs/contrib/Control/*.idr libs/contrib/Control/Isomorphism/*.idr@@ -482,6 +484,11 @@ test/ffi007/*.h test/ffi007/run test/ffi007/expected+ test/ffi008/*.idr+ test/ffi008/*.c+ test/ffi008/*.h+ test/ffi008/run+ test/ffi008/expected test/folding001/*.idr test/folding001/run@@ -609,6 +616,14 @@ test/primitives005/*.idr test/primitives005/expected + test/primitives006/run+ test/primitives006/array.c+ test/primitives006/array.h+ test/primitives006/load-test.idr+ test/primitives006/Data/Bytes.idr+ test/primitives006/Data/ByteArray.idr+ test/primitives006/expected+ test/pkg001/run test/pkg001/test.ipkg test/pkg001/*.idr@@ -831,11 +846,6 @@ Default: False manual: True -Flag curses- Description: Use Curses to get the screen width- Default: False- manual: True- -- This flag determines whether to show Git hashes in version strings -- Defaults to True because Hackage is a source release Flag release@@ -994,6 +1004,7 @@ , pretty < 1.2 , process < 1.3 , split < 0.3+ , terminal-size < 0.4 , text >=1.2.1.0 && < 1.3 , time >= 1.4 && < 1.6 , transformers < 0.5@@ -1045,9 +1056,6 @@ build-depends: libffi < 0.2 extra-libraries: gmp cpp-options: -DIDRIS_GMP- if flag(curses)- build-depends: hscurses < 1.5- cpp-options: -DCURSES if flag(freestanding) other-modules: Target_idris cpp-options: -DFREESTANDING
libs/base/Control/Monad/State.idr view
@@ -54,7 +54,7 @@ ||| The State monad. See the MonadState interface State : Type -> Type -> Type-State s a = StateT s Identity a+State = \s, a => StateT s Identity a ||| Unwrap a State monad computation. runState : StateT s Identity a -> s -> (a, s)
libs/base/Language/Reflection/Utils.idr view
@@ -40,17 +40,30 @@ getUName (NS n ns) = getUName n getUName _ = Nothing -total-unApply : TT -> (TT, List TT)-unApply t = unA t []- where unA : TT -> List TT -> (TT, List TT)- unA (App fn arg) args = unA fn (arg::args)- unA tm args = (tm, args)+namespace TT+ total+ unApply : TT -> (TT, List TT)+ unApply t = unA t []+ where unA : TT -> List TT -> (TT, List TT)+ unA (App fn arg) args = unA fn (arg::args)+ unA tm args = (tm, args) -total-mkApp : TT -> List TT -> TT-mkApp tm [] = tm-mkApp tm (a::as) = mkApp (App tm a) as+ total+ mkApp : Foldable f => TT -> f TT -> TT+ mkApp f args = foldl App f args++namespace Raw+ total+ unApply : Raw -> (Raw, List Raw)+ unApply tm = unApply' tm []+ where unApply' : Raw -> List Raw -> (Raw, List Raw)+ unApply' (RApp f x) xs = unApply' f (x::xs)+ unApply' notApp xs = (notApp, xs)++ total+ mkApp : Foldable f => Raw -> f Raw -> Raw+ mkApp f args = foldl RApp f args+ total binderTy : Binder t -> t
+ libs/contrib/CFFI.idr view
@@ -0,0 +1,4 @@+module CFFI++import public CFFI.Types+import public CFFI.Memory
+ libs/contrib/CFFI/Memory.idr view
@@ -0,0 +1,94 @@+||| Machinery for interfacing with C.+module CFFI.Memory++import CFFI.Types+import Data.Vect++%include C "memory.h"++%access public export+%default partial+++data CPtr = CPt Ptr Int++implicit toCPtr : Ptr -> CPtr+toCPtr p = CPt p 0++implicit toPtr : CPtr -> Ptr+toPtr (CPt p 0) = p+toPtr (CPt p o) = prim__ptrOffset p o++||| Import of malloc from the C standard library.+malloc : Int -> IO Ptr+malloc size = foreign FFI_C "malloc" (Int -> IO Ptr) size++||| Import of free from the C standard library.+mfree : Ptr -> IO ()+mfree ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr++||| Allocate enough memory to hold an instance of a C typr+alloc : Composite -> IO CPtr+alloc t = return $ CPt !(malloc (sizeOf t)) 0++||| Free memory allocated with alloc+free : CPtr -> IO ()+free (CPt p _ ) = mfree p++||| Perform an IO action with memory that is freed afterwards+withAlloc : Composite -> (CPtr -> IO ()) -> IO ()+withAlloc t f = do m <- alloc t+ f m+ free m++infixl 1 ~~>+||| Perform an IO action with memory that is freed afterwards+(~~>) : Composite-> (CPtr -> IO ()) -> IO ()+(~~>) = withAlloc++||| Read from memory+peek : (t: CType) -> CPtr -> IO (translate t)+peek I8 (CPt p o) = prim_peek8 p o+peek I16 (CPt p o) = prim_peek16 p o+peek I32 (CPt p o) = prim_peek32 p o+peek I64 (CPt p o) = prim_peek64 p o+peek FLOAT (CPt p o) = prim_peekSingle p o+peek DOUBLE (CPt p o) = prim_peekDouble p o+peek PTR (CPt p o) = prim_peekPtr p o++||| Write to memory+poke : (t : CType) -> CPtr -> translate t -> IO ()+poke I8 (CPt p o) x = do _ <- prim_poke8 p o x+ return ()+poke I16 (CPt p o) x = do _ <- prim_poke16 p o x+ return ()+poke I32 (CPt p o) x = do _ <- prim_poke32 p o x+ return ()+poke I64 (CPt p o) x = do _ <- prim_poke64 p o x+ return ()+poke PTR (CPt p o) x = do _ <- prim_pokePtr p o x+ return ()+poke FLOAT (CPt p o) x = do _ <- prim_pokeSingle p o x+ return ()+poke DOUBLE (CPt p o) x = do _ <- prim_pokeDouble p o x+ return ()++||| Update memory with a function.+update : (t: CType) -> CPtr -> (translate t -> translate t) -> IO ()+update ty cp f = do val <- peek ty cp+ out <- return $ f val+ poke ty cp out++||| Get a pointer to a field in a composite value+field : Composite -> Nat -> CPtr -> CPtr+field arr@(ARRAY n t) i (CPt p o) = CPt p (o + offset arr i)+field un@(UNION xs) i (CPt p o) = CPt p o+field st@(STRUCT xs) i (CPt p o) = CPt p (o + offset st i)+field ps@(PACKEDSTRUCT xs) i (CPt p o) = CPt p (o + offset ps i)+field (T t) Z p = p++infixl 10 #++||| Get a pointer to a field in a composite value+(#) : Composite -> Nat -> CPtr -> CPtr+(#) = field
+ libs/contrib/CFFI/Types.idr view
@@ -0,0 +1,159 @@+||| Types for interfacing with C.+||| This file should be kept free from IO.+module CFFI.Types++import Data.Vect+import Debug.Error++%access public export+%default partial++||| An universe of C types.+data CType = I8 | I16 | I32 | I64 | FLOAT | DOUBLE | PTR++||| Composites of C types+data Composite = T CType | ARRAY Int Composite | STRUCT (List Composite) | UNION (List Composite)+ | PACKEDSTRUCT (List Composite)++||| Implicit conversion of primitive C types to composites+implicit mkComposite : CType -> Composite+mkComposite x = T x++Show CType where+ show I8 = "I8"+ show I16 = "I16"+ show I32 = "I32"+ show I64 = "I64"+ show FLOAT = "FLOAT"+ show DOUBLE = "DOUBLE"+ show PTR = "PTR"++Show Composite where+ show (T ct) = show ct+ show (ARRAY n t) = "ARRAY " ++ show n ++ " " ++ show t+ show (STRUCT xs) = "STRUCT " ++ show xs+ show (UNION xs) = "UNION " ++ show xs+ show (PACKEDSTRUCT xs) = "PACKEDSTRUCT " ++ show xs++||| What Idris type the C type is marshalled to+translate : CType -> Type+translate I8 = Bits8+translate I16 = Bits16+translate I32 = Bits32+translate I64 = Bits64+translate FLOAT = Double+translate DOUBLE = Double+translate PTR = Ptr++mutual+ private+ sizeOfCT : CType -> Int+ sizeOfCT I8 = 1+ sizeOfCT I16 = 2+ sizeOfCT I32 = 4+ sizeOfCT I64 = 8+ sizeOfCT FLOAT = 4+ sizeOfCT DOUBLE = 8+ sizeOfCT PTR = prim__sizeofPtr++ ||| Size of value of the type in bytes+ export+ sizeOf : Composite -> Int+ sizeOf (T ct) = sizeOfCT ct+ sizeOf (ARRAY n t) = n * sizeOf t+ sizeOf (STRUCT xs) = sizeOfStruct xs+ sizeOf (UNION xs) = foldl (\acc, x =>max acc $ sizeOf x) 0 xs+ sizeOf (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOf x) 0 xs++ private+ alignOfCT : CType -> Int+ alignOfCT I8 = 1+ alignOfCT I16 = 2+ alignOfCT I32 = 4+ alignOfCT I64 = prim__sizeofPtr+ alignOfCT FLOAT = 4+ alignOfCT DOUBLE = prim__sizeofPtr+ alignOfCT PTR = prim__sizeofPtr++ ||| Alignment requirement of the type+ export+ alignOf : Composite -> Int+ alignOf (T t) = alignOfCT t+ alignOf (ARRAY n t) = alignOf t+ alignOf (STRUCT xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs+ alignOf (UNION xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs+ alignOf (PACKEDSTRUCT xs) = 1++ private+ pad : Int -> Int -> Int+ pad pos align = let c = pos `mod` align in if c == 0 then 0 else align - c++ private+ nextOffset : Composite -> Int -> Int+ nextOffset ty pos = pos + pad pos (alignOf ty)++ private+ offsetsStruct : List Composite -> List Int+ offsetsStruct xs = offsets' xs 0+ where+ offsets' : List Composite -> Int -> List Int+ offsets' [] _ = []+ offsets' (x::xs) pos = (nextOffset x pos)::(offsets' xs (nextOffset x pos + sizeOf x))++ private+ sizeOfStruct : List Composite -> Int+ sizeOfStruct xs = sizeStruct' xs 0 1+ where+ sizeStruct' : List Composite -> Int -> Int -> Int+ sizeStruct' [] pos maxAlign = pos + (pad pos maxAlign)+ sizeStruct' (x::xs) pos maxAlign = sizeStruct' xs (nextOffset x pos + sizeOf x)+ (max maxAlign (alignOf x))++||| Number of fields in a composite type+export+fields : Composite -> Nat+fields (STRUCT xs) = length xs+fields (PACKEDSTRUCT xs) = length xs+fields (UNION xs) = length xs+fields (ARRAY n _) = toNat n+fields (T _) = 1++private+offsetsPacked : List Composite -> List Int+offsetsPacked xs = offsets' xs [] 0+ where+ offsets' : List Composite -> List Int -> Int -> List Int+ offsets' [] acc _ = reverse acc+ offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)++private+indexOrFail : Nat -> List a -> a+indexOrFail i xs = case index' i xs of+ Just x => x+ Nothing => error "Out of bounds access"++||| The offset of a firld in a composite type+export+offset : Composite -> Nat -> Int+offset (STRUCT xs) i = indexOrFail i (offsetsStruct xs)+offset (PACKEDSTRUCT xs) i = indexOrFail i (offsetsPacked xs)+offset (ARRAY _ t) i = sizeOf t * toIntNat i+offset (T _) _ = 0++||| All offsets of a composite type+export+offsets : Composite -> List Int+offsets (STRUCT xs) = offsetsStruct xs+offsets (PACKEDSTRUCT xs) = offsetsPacked xs+offsets (UNION xs) = replicate (length xs) 0+offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n-1]]+offsets (T _) = [0]++||| The type of a field in a composite type.+export+fieldType : Composite -> Nat -> Composite+fieldType (STRUCT xs@(y::_)) i = indexOrFail i xs+fieldType (PACKEDSTRUCT xs@(y::_)) i = indexOrFail i xs+fieldType (UNION xs@(y::_)) i = indexOrFail i xs+fieldType (ARRAY n t) _ = t+fieldType t _ = t
libs/contrib/Classes/Verified.idr view
@@ -14,7 +14,7 @@ -- and Monoid). interface Functor f => VerifiedFunctor (f : Type -> Type) where- functorIdentity : {a : Type} -> (x : f a) -> map id x = id x+ functorIdentity : {a : Type} -> (x : f a) -> map Basics.id x = Basics.id x functorComposition : {a : Type} -> {b : Type} -> (x : f a) -> (g1 : a -> b) -> (g2 : b -> c) -> map (g2 . g1) x = (map g2 . map g1) x
libs/contrib/contrib.ipkg view
@@ -1,7 +1,9 @@ package contrib opts = "--nobasepkgs --total -i ../prelude -i ../base"-modules = Control.Algebra,+modules = CFFI, CFFI.Types, CFFI.Memory,++ Control.Algebra, Control.Algebra.Lattice, Control.Algebra.VectorSpace, Control.Algebra.NumericInstances, Control.Isomorphism.Primitives,
libs/effects/Effects.idr view
@@ -84,60 +84,119 @@ syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst) -- --------------------------------------- [ Properties and Proof Construction ]+ public export+data SubElem : a -> List a -> Type where+ Z : SubElem a (a :: as)+ S : SubElem a as -> SubElem a (b :: as)+ +public export data SubList : List a -> List a -> Type where- SubNil : SubList [] []- Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)- Drop : SubList xs ys -> SubList xs (x :: ys)+ SubNil : SubList [] xs+ InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys +Uninhabited (SubElem x []) where+ uninhabited Z impossible+ uninhabited (S _) impossible++-- Some useful hints for proof construction in polymorphic programs %hint-subListId : SubList xs xs-subListId {xs = Nil} = SubNil-subListId {xs = x :: xs} = Keep subListId+public export total+dropFirst : SubList xs ys -> SubList xs (x :: ys)+dropFirst SubNil = SubNil+dropFirst (InList el sub) = InList (S el) (dropFirst sub) +%hint+public export total+subListId : (xs : List a) -> SubList xs xs+subListId [] = SubNil+subListId (x :: xs) = InList Z (dropFirst (subListId xs))++public export total+inSuffix : SubElem x ys -> SubList xs ys -> SubElem x (zs ++ ys)+inSuffix {zs = []} el sub = el+inSuffix {zs = (x :: xs)} el sub = S (inSuffix el sub)++%hint+public export total+dropPrefix : SubList xs ys -> SubList xs (zs ++ ys)+dropPrefix SubNil = SubNil+dropPrefix (InList el sub) = InList (inSuffix el sub) (dropPrefix sub)++public export total+inPrefix : SubElem x ys -> SubList xs ys -> SubElem x (ys ++ zs)+inPrefix {zs = []} {ys} el sub+ = rewrite appendNilRightNeutral ys in el+inPrefix {zs = (x :: xs)} Z sub = Z+inPrefix {zs = (x :: xs)} (S y) sub = S (inPrefix y SubNil)++%hint+public export total+dropSuffix : SubList xs ys -> SubList xs (ys ++ zs)+dropSuffix SubNil = SubNil+dropSuffix (InList el sub) = InList (inPrefix el sub) (dropSuffix sub)+ namespace Env public export data Env : (m : Type -> Type) -> List EFFECT -> Type where- Nil : Env m Nil- (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)+ Nil : Env m Nil+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs) -public export-data EffElem : Effect -> Type ->- List EFFECT -> Type where- Here : EffElem x a (MkEff a x :: xs)- There : EffElem x a xs -> EffElem x a (y :: xs)+namespace EffElem+ public export+ data EffElem : Effect -> Type ->+ List EFFECT -> Type where+ Here : EffElem x a (MkEff a x :: xs)+ There : EffElem x a xs -> EffElem x a (y :: xs)+ +total envElem : SubElem x xs -> Env m xs -> Env m [x]+envElem Z (x :: xs) = [x]+envElem (S k) (x :: xs) = envElem k xs ||| make an environment corresponding to a sub-list-private-dropEnv : Env m ys -> SubList xs ys -> Env m xs+total dropEnv : Env m ys -> SubList xs ys -> Env m xs dropEnv [] SubNil = []-dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest-dropEnv (v :: vs) (Drop rest) = dropEnv vs rest+dropEnv [] (InList idx rest) = absurd idx+dropEnv (y::ys) SubNil = []+dropEnv e@(y::ys) (InList idx rest) = + let [x] = envElem idx e+ in x :: dropEnv e rest public export-updateWith : (ys' : List a) -> (xs : List a) ->- SubList ys xs -> List a-updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest-updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest-updateWith [] [] SubNil = []-updateWith (y :: ys) [] SubNil = y :: ys-updateWith [] (x :: xs) (Keep rest) = []+total updateAt : (idx : SubElem x' xs) -> (a:Type) -> List EFFECT -> List EFFECT+updateAt Z a [] = []+updateAt Z a ((MkEff b eff) :: xs) = (MkEff a eff) :: xs+updateAt (S k) a [] = []+updateAt (S k) a (x :: xs) = x :: updateAt k a xs +public export+total updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->+ SubList ys xs -> List EFFECT+updateWith [] xs sl = xs+updateWith (y :: ys) xs SubNil = xs+updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)++public export+total replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->+ Env m (updateAt idx a ys)+replaceEnvAt x Z [] = []+replaceEnvAt x Z (y :: ys) = x :: ys+replaceEnvAt x (S k) [] = []+replaceEnvAt x (S k) (y :: ys) = y :: replaceEnvAt x k ys+ ||| Put things back, replacing old with new in the sub-environment-private-rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->+public export+total rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) -> Env m xs -> Env m (updateWith ys' xs prf)-rebuildEnv [] SubNil env = env-rebuildEnv (x :: xs) SubNil env = x :: xs-rebuildEnv [] (Keep rest) (y :: env) = []-rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env-rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env-+rebuildEnv [] SubNil env = env+rebuildEnv (x :: xs) SubNil env = env+rebuildEnv [] (InList w s) env = env+rebuildEnv (x :: xs) (InList idx rest) env = replaceEnvAt x idx (rebuildEnv xs rest env) -- -------------------------------------------------- [ The Effect EDSL itself ] public export-updateResTy : (val : t) ->+total updateResTy : (val : t) -> (xs : List EFFECT) -> EffElem e a xs -> e t a b -> List EFFECT updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
libs/prelude/Builtins.idr view
@@ -184,6 +184,7 @@ export data Ptr : Type export data ManagedPtr : Type+export data CData : Type %extern prim__readFile : prim__WorldType -> Ptr -> String %extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int@@ -201,6 +202,7 @@ -- primitives for accessing memory. %extern prim__asPtr : ManagedPtr -> Ptr %extern prim__sizeofPtr : Int+%extern prim__ptrOffset : Ptr -> Int -> Ptr %extern prim__peek8 : prim__WorldType -> Ptr -> Int -> Bits8 %extern prim__peek16 : prim__WorldType -> Ptr -> Int -> Bits16 %extern prim__peek32 : prim__WorldType -> Ptr -> Int -> Bits32@@ -213,3 +215,8 @@ %extern prim__peekPtr : prim__WorldType -> Ptr -> Int -> Ptr %extern prim__pokePtr : prim__WorldType -> Ptr -> Int -> Ptr -> Int++%extern prim__peekDouble : prim__WorldType -> Ptr -> Int -> Double+%extern prim__pokeDouble : prim__WorldType -> Ptr -> Int -> Double -> Int+%extern prim__peekSingle : prim__WorldType -> Ptr -> Int -> Double+%extern prim__pokeSingle : prim__WorldType -> Ptr -> Int -> Double -> Int
libs/prelude/IO.idr view
@@ -178,6 +178,7 @@ C_Any : C_Types (Raw a) C_FnT : C_FnTypes t -> C_Types (CFnPtr t) C_IntT : C_IntTypes i -> C_Types i+ C_CData : C_Types CData ||| A descriptor for the C FFI. See the constructors of `C_Types` ||| and `C_IntTypes` for the concrete types that are available.@@ -348,3 +349,19 @@ prim_pokePtr : Ptr -> Int -> Ptr -> IO Int prim_pokePtr ptr offset val = MkIO (\w => prim_io_return ( prim__pokePtr (world w) ptr offset val))++prim_peekDouble : Ptr -> Int -> IO Double+prim_peekDouble ptr offset = MkIO (\w => prim_io_return (prim__peekDouble (world w) ptr offset))++prim_pokeDouble : Ptr -> Int -> Double -> IO Int+prim_pokeDouble ptr offset val = MkIO (\w => prim_io_return (+ prim__pokeDouble (world w) ptr offset val))++||| Single precision floats are marshalled to Doubles+prim_peekSingle : Ptr -> Int -> IO Double+prim_peekSingle ptr offset = MkIO (\w => prim_io_return (prim__peekSingle (world w) ptr offset))++||| Single precision floats are marshalled to Doubles+prim_pokeSingle : Ptr -> Int -> Double -> IO Int+prim_pokeSingle ptr offset val = MkIO (\w => prim_io_return (+ prim__pokeSingle (world w) ptr offset val))
libs/prelude/Language/Reflection/Elab.idr view
@@ -57,11 +57,11 @@ ||| Indices are not uniform TyConIndex FunArg -||| A type declaration+||| A type declaration for a function or datatype record TyDecl where constructor Declare - ||| The name of the function being declared.+ ||| The fully-qualified name of the function or datatype being declared. name : TTName ||| Each argument is in the scope of the names of previous arguments.@@ -83,6 +83,34 @@ clauses : List (FunClause a) +||| A constructor to be associated with a new datatype.+record ConstructorDefn where+ constructor Constructor++ ||| The name of the constructor. The name must _not_ be qualified -+ ||| that is, it should begin with the `UN` or `MN` constructors.+ name : TTName++ ||| The constructor arguments. Idris will infer which arguments are+ ||| datatype parameters.+ arguments : List FunArg++ ||| The specific type constructed by the constructor.+ returnType : Raw+++||| A definition of a datatype to be added during an elaboration script.+record DataDefn where+ constructor DefineDatatype+ ||| The name of the datatype being defined. It must be+ ||| fully-qualified, and it must have been previously declared as a+ ||| datatype.+ name : TTName++ ||| A list of constructors for the datatype.+ constructors : List ConstructorDefn++ data CtorArg = CtorParameter FunArg | CtorField FunArg ||| A reflected datatype definition@@ -151,6 +179,8 @@ Prim__DeclareType : TyDecl -> Elab () Prim__DefineFunction : FunDefn Raw -> Elab ()+ Prim__DeclareDatatype : TyDecl -> Elab ()+ Prim__DefineDatatype : DataDefn -> Elab () Prim__AddInstance : TTName -> TTName -> Elab () Prim__IsTCName : TTName -> Elab Bool @@ -335,7 +365,7 @@ export matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)- matchApply tm argSpec = map snd <$> Prim__Apply tm argSpec+ matchApply tm argSpec = map snd <$> Prim__MatchApply tm argSpec ||| Move the focus to the specified hole. Fails if the hole does not ||| exist.@@ -509,6 +539,17 @@ export defineFunction : FunDefn Raw -> Elab () defineFunction defun = Prim__DefineFunction defun++ ||| Declare a datatype in the global context. This step only+ ||| establishes the type constructor; use `defineDatatype` to give+ ||| it constructors.+ export+ declareDatatype : TyDecl -> Elab ()+ declareDatatype decl = Prim__DeclareDatatype decl++ export+ defineDatatype : DataDefn -> Elab ()+ defineDatatype defn = Prim__DefineDatatype defn ||| Register a new implementation for interface resolution. |||
libs/pruviloj/Pruviloj/Internals.idr view
@@ -26,16 +26,6 @@ updateTyConArgTy f (TyConIndex a) = TyConIndex (record {type = f (type a) } a) -unApply : Raw -> (Raw, List Raw)-unApply tm = unApply' tm []- where unApply' : Raw -> List Raw -> (Raw, List Raw)- unApply' (RApp f x) xs = unApply' f (x::xs)- unApply' notApp xs = (notApp, xs)--mkApp : Raw -> List Raw -> Raw-mkApp f [] = f-mkApp f (x :: xs) = mkApp (RApp f x) xs- ||| Grab the binders from around a term, alpha-converting to make ||| their names unique partial
rts/getline.c view
@@ -38,40 +38,41 @@ ssize_t getdelim(char **buf, size_t *bufsiz, int delimiter, FILE *fp) {- char *ptr, *eptr;--- if (*buf == NULL || *bufsiz == 0) {- *bufsiz = BUFSIZ;- if ((*buf = malloc(*bufsiz)) == NULL)- return -1;- }+ char *ptr, *eptr; - for (ptr = *buf, eptr = *buf + *bufsiz;;) {- int c = fgetc(fp);- if (c == -1) {- if (feof(fp))- return ptr == *buf ? -1 : ptr - *buf;- else- return -1;- }- *ptr++ = c;- if (c == delimiter) {- *ptr = '\0';- return ptr - *buf;+ if (*buf == NULL || *bufsiz == 0) {+ *bufsiz = BUFSIZ;+ if ((*buf = malloc(*bufsiz)) == NULL)+ return -1; }- if (ptr + 2 >= eptr) {- char *nbuf;- size_t nbufsiz = *bufsiz * 2;- ssize_t d = ptr - *buf;- if ((nbuf = realloc(*buf, nbufsiz)) == NULL)- return -1;- *buf = nbuf;- *bufsiz = nbufsiz;- eptr = nbuf + nbufsiz;- ptr = nbuf + d;++ for (ptr = *buf, eptr = *buf + *bufsiz;;) {+ int c = fgetc(fp);+ if (c == -1) {+ if (feof(fp)) {+ *ptr = '\0';+ return ptr - *buf;+ } else {+ return -1;+ }+ }+ *ptr++ = c;+ if (c == delimiter) {+ *ptr = '\0';+ return ptr - *buf;+ }+ if (ptr + 2 >= eptr) {+ char *nbuf;+ size_t nbufsiz = *bufsiz * 2;+ ssize_t d = ptr - *buf;+ if ((nbuf = realloc(*buf, nbufsiz)) == NULL)+ return -1;+ *buf = nbuf;+ *bufsiz = nbufsiz;+ eptr = nbuf + nbufsiz;+ ptr = nbuf + d;+ } }- } } ssize_t
rts/idris_bitstring.c view
@@ -5,7 +5,7 @@ VAL idris_b8CopyForGC(VM *vm, VAL a) { uint8_t A = a->info.bits8; VAL cl = allocate(sizeof(Closure), 1);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = A; return cl; }@@ -13,7 +13,7 @@ VAL idris_b16CopyForGC(VM *vm, VAL a) { uint16_t A = a->info.bits16; VAL cl = allocate(sizeof(Closure), 1);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = A; return cl; }@@ -21,7 +21,7 @@ VAL idris_b32CopyForGC(VM *vm, VAL a) { uint32_t A = a->info.bits32; VAL cl = allocate(sizeof(Closure), 1);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = A; return cl; }@@ -29,7 +29,7 @@ VAL idris_b64CopyForGC(VM *vm, VAL a) { uint64_t A = a->info.bits64; VAL cl = allocate(sizeof(Closure), 1);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = A; return cl; }@@ -37,7 +37,7 @@ VAL idris_b8(VM *vm, VAL a) { uint8_t A = GETINT(a); VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = (uint8_t) A; return cl; }@@ -45,7 +45,7 @@ VAL idris_b16(VM *vm, VAL a) { uint16_t A = GETINT(a); VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = (uint16_t) A; return cl; }@@ -53,7 +53,7 @@ VAL idris_b32(VM *vm, VAL a) { uint32_t A = GETINT(a); VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = (uint32_t) A; return cl; }@@ -61,7 +61,7 @@ VAL idris_b64(VM *vm, VAL a) { uint64_t A = GETINT(a); VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = (uint64_t) A; return cl; }@@ -72,28 +72,28 @@ VAL idris_b8const(VM *vm, uint8_t a) { VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = a; return cl; } VAL idris_b16const(VM *vm, uint16_t a) { VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = a; return cl; } VAL idris_b32const(VM *vm, uint32_t a) { VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = a; return cl; } VAL idris_b64const(VM *vm, uint64_t a) { VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = a; return cl; }@@ -102,7 +102,7 @@ uint8_t A = a->info.bits8; uint8_t B = b->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = A + B; return cl; }@@ -111,7 +111,7 @@ uint8_t A = a->info.bits8; uint8_t B = b->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = A - B; return cl; }@@ -120,7 +120,7 @@ uint8_t A = a->info.bits8; uint8_t B = b->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = A * B; return cl; }@@ -129,7 +129,7 @@ uint8_t A = a->info.bits8; uint8_t B = b->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = A / B; return cl; }@@ -138,7 +138,7 @@ uint8_t A = a->info.bits8; uint8_t B = b->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = (uint8_t) (((int8_t) A) / ((int8_t) B)); return cl; }@@ -147,7 +147,7 @@ uint8_t A = a->info.bits8; uint8_t B = b->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = A % B; return cl; }@@ -156,7 +156,7 @@ uint8_t A = a->info.bits8; uint8_t B = b->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = (uint8_t) (((int8_t) A) % ((int8_t) B)); return cl; }@@ -184,7 +184,7 @@ VAL idris_b8Compl(VM *vm, VAL a) { uint8_t A = a->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = ~ A; return cl; }@@ -193,7 +193,7 @@ uint8_t A = a->info.bits8; uint8_t B = b->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = A & B; return cl; }@@ -202,7 +202,7 @@ uint8_t A = a->info.bits8; uint8_t B = b->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = A | B; return cl; }@@ -211,7 +211,7 @@ uint8_t A = a->info.bits8; uint8_t B = b->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = A ^ B; return cl; }@@ -220,7 +220,7 @@ uint8_t A = a->info.bits8; uint8_t B = b->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = A << B; return cl; }@@ -229,7 +229,7 @@ uint8_t A = a->info.bits8; uint8_t B = b->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = A >> B; return cl; }@@ -238,7 +238,7 @@ uint8_t A = a->info.bits8; uint8_t B = b->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = (uint8_t) (((int8_t) A) >> ((int8_t) B)); return cl; }@@ -247,7 +247,7 @@ uint16_t A = a->info.bits16; uint16_t B = b->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = A + B; return cl; }@@ -256,7 +256,7 @@ uint16_t A = a->info.bits16; uint16_t B = b->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = A - B; return cl; }@@ -265,7 +265,7 @@ uint16_t A = a->info.bits16; uint16_t B = b->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = A * B; return cl; }@@ -274,7 +274,7 @@ uint16_t A = a->info.bits16; uint16_t B = b->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = A / B; return cl; }@@ -283,7 +283,7 @@ uint16_t A = a->info.bits16; uint16_t B = b->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = (uint16_t) (((int16_t) A) / ((int16_t) B)); return cl; }@@ -292,7 +292,7 @@ uint16_t A = a->info.bits16; uint16_t B = b->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = A % B; return cl; }@@ -301,7 +301,7 @@ uint16_t A = a->info.bits16; uint16_t B = b->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = (uint16_t) (((int16_t) A) % ((int16_t) B)); return cl; }@@ -329,7 +329,7 @@ VAL idris_b16Compl(VM *vm, VAL a) { uint16_t A = a->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = ~ A; return cl; }@@ -338,7 +338,7 @@ uint16_t A = a->info.bits16; uint16_t B = b->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = A & B; return cl; }@@ -347,7 +347,7 @@ uint16_t A = a->info.bits16; uint16_t B = b->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = A | B; return cl; }@@ -356,7 +356,7 @@ uint16_t A = a->info.bits16; uint16_t B = b->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = A ^ B; return cl; }@@ -365,7 +365,7 @@ uint16_t A = a->info.bits16; uint16_t B = b->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = A << B; return cl; }@@ -374,7 +374,7 @@ uint16_t A = a->info.bits16; uint16_t B = b->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = A >> B; return cl; }@@ -383,7 +383,7 @@ uint16_t A = a->info.bits16; uint16_t B = b->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = (uint16_t) (((int16_t) A) >> ((int16_t) B)); return cl; }@@ -392,7 +392,7 @@ uint32_t A = a->info.bits32; uint32_t B = b->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = A + B; return cl; }@@ -401,7 +401,7 @@ uint32_t A = a->info.bits32; uint32_t B = b->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = A - B; return cl; }@@ -410,7 +410,7 @@ uint32_t A = a->info.bits32; uint32_t B = b->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = A * B; return cl; }@@ -419,7 +419,7 @@ uint32_t A = a->info.bits32; uint32_t B = b->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = A / B; return cl; }@@ -428,7 +428,7 @@ uint32_t A = a->info.bits32; uint32_t B = b->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = (uint32_t) (((int32_t) A) / ((int32_t) B)); return cl; }@@ -437,7 +437,7 @@ uint32_t A = a->info.bits32; uint32_t B = b->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = A % B; return cl; }@@ -446,7 +446,7 @@ uint32_t A = a->info.bits32; uint32_t B = b->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = (uint32_t) (((int32_t) A) % ((int32_t) B)); return cl; }@@ -474,7 +474,7 @@ VAL idris_b32Compl(VM *vm, VAL a) { uint32_t A = a->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = ~ A; return cl; }@@ -483,7 +483,7 @@ uint32_t A = a->info.bits32; uint32_t B = b->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = A & B; return cl; }@@ -492,7 +492,7 @@ uint32_t A = a->info.bits32; uint32_t B = b->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = A | B; return cl; }@@ -501,7 +501,7 @@ uint32_t A = a->info.bits32; uint32_t B = b->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = A ^ B; return cl; }@@ -510,7 +510,7 @@ uint32_t A = a->info.bits32; uint32_t B = b->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = A << B; return cl; }@@ -519,7 +519,7 @@ uint32_t A = a->info.bits32; uint32_t B = b->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = A >> B; return cl; }@@ -528,7 +528,7 @@ uint32_t A = a->info.bits32; uint32_t B = b->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = (uint32_t) (((int32_t)A) >> ((int32_t)B)); return cl; }@@ -537,7 +537,7 @@ uint64_t A = a->info.bits64; uint64_t B = b->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = A + B; return cl; }@@ -546,7 +546,7 @@ uint64_t A = a->info.bits64; uint64_t B = b->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = A - B; return cl; }@@ -555,7 +555,7 @@ uint64_t A = a->info.bits64; uint64_t B = b->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = A * B; return cl; }@@ -564,7 +564,7 @@ uint64_t A = a->info.bits64; uint64_t B = b->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = A / B; return cl; }@@ -573,7 +573,7 @@ uint64_t A = a->info.bits64; uint64_t B = b->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = (uint64_t) (((int64_t) A) / ((int64_t) B)); return cl; }@@ -582,7 +582,7 @@ uint64_t A = a->info.bits64; uint64_t B = b->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = A % B; return cl; }@@ -591,7 +591,7 @@ uint64_t A = a->info.bits64; uint64_t B = b->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = (uint64_t) (((int64_t) A) % ((int64_t) B)); return cl; }@@ -619,7 +619,7 @@ VAL idris_b64Compl(VM *vm, VAL a) { uint64_t A = a->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = ~ A; return cl; }@@ -628,7 +628,7 @@ uint64_t A = a->info.bits64; uint64_t B = b->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = A & B; return cl; }@@ -637,7 +637,7 @@ uint64_t A = a->info.bits64; uint64_t B = b->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = A | B; return cl; }@@ -646,7 +646,7 @@ uint64_t A = a->info.bits64; uint64_t B = b->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = A ^ B; return cl; }@@ -655,7 +655,7 @@ uint64_t A = a->info.bits64; uint64_t B = b->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = A << B; return cl; }@@ -664,7 +664,7 @@ uint64_t A = a->info.bits64; uint64_t B = b->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = A >> B; return cl; }@@ -673,7 +673,7 @@ uint64_t A = a->info.bits64; uint64_t B = b->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = (uint64_t) (((int64_t) A) >> ((int64_t) B)); return cl; }@@ -681,7 +681,7 @@ VAL idris_b8Z16(VM *vm, VAL a) { uint8_t A = a->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = (uint16_t) A; return cl; }@@ -689,7 +689,7 @@ VAL idris_b8Z32(VM *vm, VAL a) { uint8_t A = a->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = (uint32_t) A; return cl; }@@ -697,7 +697,7 @@ VAL idris_b8Z64(VM *vm, VAL a) { uint8_t A = a->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = (uint64_t) A; return cl; }@@ -705,7 +705,7 @@ VAL idris_b8S16(VM *vm, VAL a) { uint8_t A = a->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = (uint16_t) (int16_t) (int8_t) A; return cl; }@@ -713,7 +713,7 @@ VAL idris_b8S32(VM *vm, VAL a) { uint8_t A = a->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = (uint32_t) (int32_t) (int8_t) A; return cl; }@@ -721,7 +721,7 @@ VAL idris_b8S64(VM *vm, VAL a) { uint8_t A = a->info.bits8; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = (uint64_t) (int64_t) (int8_t) A; return cl; }@@ -729,7 +729,7 @@ VAL idris_b16Z32(VM *vm, VAL a) { uint16_t A = a->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = (uint32_t) A; return cl; }@@ -737,7 +737,7 @@ VAL idris_b16Z64(VM *vm, VAL a) { uint16_t A = a->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = (uint64_t) A; return cl; }@@ -745,7 +745,7 @@ VAL idris_b16S32(VM *vm, VAL a) { uint16_t A = a->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = (uint32_t) (int32_t) (int16_t) A; return cl; }@@ -753,7 +753,7 @@ VAL idris_b16S64(VM *vm, VAL a) { uint16_t A = a->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = (uint64_t) (int64_t) (int16_t) A; return cl; }@@ -761,7 +761,7 @@ VAL idris_b16T8(VM *vm, VAL a) { uint16_t A = a->info.bits16; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = (uint8_t) A; return cl; }@@ -769,7 +769,7 @@ VAL idris_b32Z64(VM *vm, VAL a) { uint32_t A = a->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = (uint64_t) A; return cl; }@@ -777,7 +777,7 @@ VAL idris_b32S64(VM *vm, VAL a) { uint32_t A = a->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl->info.bits64 = (uint64_t) (int64_t) (int32_t) A; return cl; }@@ -785,7 +785,7 @@ VAL idris_b32T8(VM *vm, VAL a) { uint32_t A = a->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = (uint8_t) A; return cl; }@@ -793,7 +793,7 @@ VAL idris_b32T16(VM *vm, VAL a) { uint32_t A = a->info.bits32; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = (uint16_t) A; return cl; }@@ -801,7 +801,7 @@ VAL idris_b64T8(VM *vm, VAL a) { uint64_t A = a->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl->info.bits8 = (uint8_t) A; return cl; }@@ -809,7 +809,7 @@ VAL idris_b64T16(VM *vm, VAL a) { uint64_t A = a->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl->info.bits16 = (uint16_t) A; return cl; }@@ -817,7 +817,7 @@ VAL idris_b64T32(VM *vm, VAL a) { uint64_t A = a->info.bits64; VAL cl = allocate(sizeof(Closure), 0);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl->info.bits32 = (uint32_t) A; return cl; }
rts/idris_gc.c view
@@ -10,7 +10,7 @@ return x; } switch(GETTY(x)) {- case CON:+ case CT_CON: ar = CARITY(x); if (ar == 0 && CTAG(x) < 256) { return x;@@ -21,49 +21,53 @@ } } break;- case FLOAT:+ case CT_FLOAT: cl = MKFLOATc(vm, x->info.f); break;- case STRING:+ case CT_STRING: cl = MKSTRc(vm, x->info.str); break;- case STROFFSET:+ case CT_STROFFSET: cl = MKSTROFFc(vm, x->info.str_offset); break;- case BIGINT:+ case CT_BIGINT: cl = MKBIGMc(vm, x->info.ptr); break;- case PTR:+ case CT_PTR: cl = MKPTRc(vm, x->info.ptr); break;- case MANAGEDPTR:+ case CT_MANAGEDPTR: cl = MKMPTRc(vm, x->info.mptr->data, x->info.mptr->size); break;- case BITS8:+ case CT_BITS8: cl = idris_b8CopyForGC(vm, x); break;- case BITS16:+ case CT_BITS16: cl = idris_b16CopyForGC(vm, x); break;- case BITS32:+ case CT_BITS32: cl = idris_b32CopyForGC(vm, x); break;- case BITS64:+ case CT_BITS64: cl = idris_b64CopyForGC(vm, x); break;- case FWD:+ case CT_FWD: return x->info.ptr;- case RAWDATA:+ case CT_RAWDATA: { size_t size = x->info.size + sizeof(Closure); cl = allocate(size, 0); memcpy(cl, x, size); } break;+ case CT_CDATA:+ cl = MKCDATAc(vm, x->info.c_heap_item);+ c_heap_mark_item(x->info.c_heap_item);+ break; default: break; }- SETTY(x, FWD);+ SETTY(x, CT_FWD); x->info.ptr = cl; return cl; }@@ -76,16 +80,16 @@ while(scan < vm->heap.next) { size_t inc = *((size_t*)scan); VAL heap_item = (VAL)(scan+sizeof(size_t));- // If it's a CON or STROFFSET, copy its arguments+ // If it's a CT_CON or CT_STROFFSET, copy its arguments switch(GETTY(heap_item)) {- case CON:+ case CT_CON: ar = ARITY(heap_item); for(i = 0; i < ar; ++i) { VAL newptr = copy(vm, heap_item->info.c.args[i]); heap_item->info.c.args[i] = newptr; } break;- case STROFFSET:+ case CT_STROFFSET: heap_item->info.str_offset->str = copy(vm, heap_item->info.str_offset->str); break;@@ -132,6 +136,9 @@ if ((vm->heap.next - vm->heap.heap) > vm->heap.size >> 1) { vm->heap.size += vm->heap.growth; }++ // finally, sweep the C heap+ c_heap_sweep(&vm->c_heap); STATS_LEAVE_GC(vm->stats, vm->heap.size, vm->heap.next - vm->heap.heap) HEAP_CHECK(vm)
rts/idris_gmp.c view
@@ -33,7 +33,7 @@ mpz_init(*bigint); mpz_set_str(*bigint, val, 10); - SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl;@@ -50,7 +50,7 @@ mpz_init(*bigint); mpz_set(*bigint, *((mpz_t*)big)); - SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl;@@ -66,7 +66,7 @@ mpz_init_set(*bigint, *((mpz_t*)big)); - SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl;@@ -82,7 +82,7 @@ mpz_init_set_ui(*bigint, val); - SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl;@@ -98,7 +98,7 @@ mpz_init_set_si(*bigint, val); - SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl;@@ -116,14 +116,14 @@ mpz_init(*bigint); mpz_set_si(*bigint, GETINT(x)); - SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl; } else { idris_doneAlloc(); switch(GETTY(x)) {- case FWD:+ case CT_FWD: return GETBIG(vm, x->info.ptr); default: return x;@@ -139,7 +139,7 @@ idris_doneAlloc(); bigint = (mpz_t*)(((char*)cl) + sizeof(Closure)); mpz_add(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));- SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl; }@@ -152,7 +152,7 @@ idris_doneAlloc(); bigint = (mpz_t*)(((char*)cl) + sizeof(Closure)); mpz_sub(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));- SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl; }@@ -165,7 +165,7 @@ idris_doneAlloc(); bigint = (mpz_t*)(((char*)cl) + sizeof(Closure)); mpz_mul(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));- SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl; }@@ -178,7 +178,7 @@ idris_doneAlloc(); bigint = (mpz_t*)(((char*)cl) + sizeof(Closure)); mpz_tdiv_q(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));- SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl; }@@ -191,7 +191,7 @@ idris_doneAlloc(); bigint = (mpz_t*)(((char*)cl) + sizeof(Closure)); mpz_mod(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));- SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl; }@@ -204,7 +204,7 @@ idris_doneAlloc(); bigint = (mpz_t*)(((char*)cl) + sizeof(Closure)); mpz_and(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));- SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl; }@@ -217,7 +217,7 @@ idris_doneAlloc(); bigint = (mpz_t*)(((char*)cl) + sizeof(Closure)); mpz_ior(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));- SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl; }@@ -230,7 +230,7 @@ idris_doneAlloc(); bigint = (mpz_t*)(((char*)cl) + sizeof(Closure)); mpz_mul_2exp(*bigint, GETMPZ(GETBIG(vm,x)), GETINT(y));- SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl; }@@ -244,7 +244,7 @@ idris_doneAlloc(); bigint = (mpz_t*)(((char*)cl) + sizeof(Closure)); mpz_fdiv_q_2exp(*bigint, GETMPZ(GETBIG(vm,x)), GETINT(y));- SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl; }@@ -257,7 +257,7 @@ idris_doneAlloc(); bigint = (mpz_t*)(((char*)cl) + sizeof(Closure)); mpz_fdiv_q_2exp(*bigint, GETMPZ(GETBIG(vm,x)), GETINT(y));- SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl; }@@ -473,7 +473,7 @@ mpz_init_set_d(*bigint, val); - SETTY(cl, BIGINT);+ SETTY(cl, CT_BIGINT); cl -> info.ptr = (void*)bigint; return cl;
rts/idris_heap.c view
@@ -1,12 +1,112 @@ #include "idris_heap.h" #include "idris_rts.h"+#include "idris_gc.h" #include <stdlib.h> #include <stddef.h> #include <stdio.h>+#include <assert.h> +static void c_heap_free_item(CHeap * heap, CHeapItem * item)+{+ assert(item->size <= heap->size);+ heap->size -= item->size; -/* Used for initializing the heap. */+ // fix links+ if (item->next != NULL)+ {+ item->next->prev_next = item->prev_next;+ }+ *(item->prev_next) = item->next;++ // free payload+ item->finalizer(item->data);++ // free item struct+ free(item);+}++CHeapItem * c_heap_create_item(void * data, size_t size, CDataFinalizer * finalizer)+{+ CHeapItem * item = (CHeapItem *) malloc(sizeof(CHeapItem));++ item->data = data;+ item->size = size;+ item->finalizer = finalizer;+ item->is_used = false;+ item->next = NULL;+ item->prev_next = NULL;++ return item;+}++void c_heap_insert_if_needed(VM * vm, CHeap * heap, CHeapItem * item)+{+ if (item->prev_next != NULL) return; // already inserted++ if (heap->first != NULL)+ {+ heap->first->prev_next = &item->next;+ }++ item->prev_next = &heap->first;+ item->next = heap->first;++ heap->first = item;++ // at this point, links are done; let's calculate sizes+ + heap->size += item->size;+ if (heap->size >= heap->gc_trigger_size)+ {+ item->is_used = true; // don't collect what we're inserting+ idris_gc(vm);+ }+}++void c_heap_mark_item(CHeapItem * item)+{+ item->is_used = true;+}++void c_heap_sweep(CHeap * heap)+{+ CHeapItem * p = heap->first;+ while (p != NULL)+ {+ if (p->is_used)+ {+ p->is_used = false;+ p = p->next;+ }+ else+ {+ CHeapItem * unused_item = p;+ p = p->next;++ c_heap_free_item(heap, unused_item);+ }+ }++ heap->gc_trigger_size = C_HEAP_GC_TRIGGER_SIZE(heap->size);+}++void c_heap_init(CHeap * heap)+{+ heap->first = NULL;+ heap->size = 0;+ heap->gc_trigger_size = C_HEAP_GC_TRIGGER_SIZE(heap->size);+}++void c_heap_destroy(CHeap * heap)+{+ while (heap->first != NULL)+ {+ c_heap_free_item(heap, heap->first); // will update heap->first via the backward link+ }+}++/* Used for initializing the FP heap. */ void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old) { char * mem = malloc(heap_size);@@ -86,7 +186,7 @@ VAL heap_item = (VAL)(scan + sizeof(size_t)); switch(GETTY(heap_item)) {- case CON:+ case CT_CON: { int ar = ARITY(heap_item); int i = 0;@@ -107,7 +207,7 @@ if (!(ptr < heap_item)) { fprintf(stderr, "RTS ERROR: heap unidirectionality broken:" \- "<CON %p> <FIELD %p>\n",+ "<CT_CON %p> <FIELD %p>\n", heap_item, ptr); exit(EXIT_FAILURE); }@@ -116,9 +216,9 @@ } break; }- case FWD:+ case CT_FWD: // Check for artifacts after cheney gc.- fprintf(stderr, "RTS ERROR: FWD in working heap.\n");+ fprintf(stderr, "RTS ERROR: CT_FWD in working heap.\n"); exit(EXIT_FAILURE); break; default:
rts/idris_heap.h view
@@ -1,7 +1,89 @@ #ifndef _IDRIS_HEAP_H #define _IDRIS_HEAP_H +#include <stdbool.h> #include <stddef.h>++/* *** C heap ***+ * Objects with finalizers. Mark&sweep-collected.+ *+ * The C heap is implemented as a doubly linked list+ * of pointers coupled with their finalizers.+ */++struct VM;++#define C_HEAP_GC_TRIGGER_SIZE(heap_size) \+ (heap_size < 2048 \+ ? 4096 \+ : 2 * heap_size \+ )++typedef void CDataFinalizer(void *);++typedef struct CHeapItem {+ /// Payload.+ void * data;++ /// Size of the item, in bytes.+ /// This does not have to be a precise size. It is used to assess+ /// whether the heap needs garbage collection.+ size_t size;++ /// Finalizer that will be called on the payload pointer.+ /// Its job is to deallocate all associated resources,+ /// including the memory pointed to by `data` (if any).+ CDataFinalizer * finalizer;++ /// The mark bit set by the FP heap traversal,+ /// cleared by C heap sweep.+ bool is_used;++ /// Next item in the C heap.+ struct CHeapItem * next;++ /// Pointer to the previous next-pointer.+ struct CHeapItem ** prev_next;+} CHeapItem;++typedef struct CHeap {+ /// The first item in the heap. NULL if the heap is empty.+ CHeapItem * first;++ /// Total size of the heap. (Sum of sizes of items.)+ /// This may not be a precise size since individual items'+ /// sizes may be just estimates.+ size_t size;++ /// When heap reaches this size, GC will be triggered.+ size_t gc_trigger_size;+} CHeap;++/// Create a C heap.+void c_heap_init(CHeap * c_heap);++/// Destroy the given C heap. Will not deallocate the given pointer.+/// Will call finalizers & deallocate all blocks in the heap.+void c_heap_destroy(CHeap * c_heap);++/// Insert the given item into the heap if it's not there yet.+/// The VM pointer is needed because this operation may trigger GC.+void c_heap_insert_if_needed(struct VM * vm, CHeap * c_heap, CHeapItem * item);++/// Mark the given item as used.+void c_heap_mark_item(CHeapItem * item);++/// Sweep the C heap, finalizing and freeing unused blocks.+void c_heap_sweep(CHeap * c_heap);++/// Create a C heap item from its payload, size estimate, and finalizer.+/// The size does not have to be precise but it should roughly reflect+/// how big the item is for GC to work effectively.+CHeapItem * c_heap_create_item(void * data, size_t size, CDataFinalizer * finalizer);++/* *** Idris heap **+ * Objects without finalizers. Cheney-collected.+ */ typedef struct { char* next; // Next allocated chunk. Should always (heap <= next < end).
rts/idris_rts.c view
@@ -35,6 +35,8 @@ alloc_heap(&(vm->heap), heap_size, heap_size, NULL); + c_heap_init(&vm->c_heap);+ vm->ret = NULL; vm->reg1 = NULL; #ifdef HAS_PTHREAD@@ -80,6 +82,7 @@ VM* get_vm(void) { #ifdef HAS_PTHREAD+ init_threadkeys(); return pthread_getspecific(vm_key); #else return global_vm;@@ -90,10 +93,17 @@ terminate(vm); } -void init_threadkeys() { #ifdef HAS_PTHREAD+void create_key() { pthread_key_create(&vm_key, (void*)free_key);+} #endif++void init_threadkeys() {+#ifdef HAS_PTHREAD+ static pthread_once_t key_once = PTHREAD_ONCE_INIT;+ pthread_once(&key_once, create_key);+#endif } void init_threaddata(VM *vm) {@@ -116,6 +126,7 @@ #endif free(vm->valstack); free_heap(&(vm->heap));+ c_heap_destroy(&(vm->c_heap)); #ifdef HAS_PTHREAD pthread_mutex_destroy(&(vm -> inbox_lock)); pthread_mutex_destroy(&(vm -> inbox_block));@@ -132,6 +143,17 @@ return stats; } +CData cdata_allocate(size_t size, CDataFinalizer finalizer)+{+ void * data = (void *) malloc(size);+ return cdata_manage(data, size, finalizer);+}++CData cdata_manage(void * data, size_t size, CDataFinalizer finalizer)+{+ return c_heap_create_item(data, size, finalizer);+}+ void idris_requireAlloc(size_t size) { #ifdef HAS_PTHREAD VM* vm = pthread_getspecific(vm_key);@@ -166,7 +188,7 @@ void* idris_alloc(size_t size) { Closure* cl = (Closure*) allocate(sizeof(Closure)+size, 0);- SETTY(cl, RAWDATA);+ SETTY(cl, CT_RAWDATA); cl->info.size = size; return (void*)cl+sizeof(Closure); }@@ -231,7 +253,7 @@ void* allocCon(VM* vm, int arity, int outer) { Closure* cl = allocate(vm, sizeof(Closure) + sizeof(VAL)*arity, outer);- SETTY(cl, CON);+ SETTY(cl, CT_CON); cl -> info.c.arity = arity; // cl -> info.c.tag = 42424242;@@ -242,7 +264,7 @@ VAL MKFLOAT(VM* vm, double val) { Closure* cl = allocate(sizeof(Closure), 0);- SETTY(cl, FLOAT);+ SETTY(cl, CT_FLOAT); cl -> info.f = val; return cl; }@@ -256,7 +278,7 @@ } Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) + sizeof(char)*len, 0);- SETTY(cl, STRING);+ SETTY(cl, CT_STRING); cl -> info.str = (char*)cl + sizeof(Closure); if (str == NULL) { cl->info.str = NULL;@@ -272,9 +294,25 @@ return (root->str->info.str + root->offset); } +VAL MKCDATA(VM* vm, CHeapItem * item) {+ c_heap_insert_if_needed(vm, &vm->c_heap, item);+ Closure* cl = allocate(sizeof(Closure), 0);+ SETTY(cl, CT_CDATA);+ cl->info.c_heap_item = item;+ return cl;+}++VAL MKCDATAc(VM* vm, CHeapItem * item) {+ c_heap_insert_if_needed(vm, &vm->c_heap, item);+ Closure* cl = allocate(sizeof(Closure), 1);+ SETTY(cl, CT_CDATA);+ cl->info.c_heap_item = item;+ return cl;+}+ VAL MKPTR(VM* vm, void* ptr) { Closure* cl = allocate(sizeof(Closure), 0);- SETTY(cl, PTR);+ SETTY(cl, CT_PTR); cl -> info.ptr = ptr; return cl; }@@ -282,7 +320,7 @@ VAL MKMPTR(VM* vm, void* ptr, size_t size) { Closure* cl = allocate(sizeof(Closure) + sizeof(ManagedPtr) + size, 0);- SETTY(cl, MANAGEDPTR);+ SETTY(cl, CT_MANAGEDPTR); cl->info.mptr = (ManagedPtr*)((char*)cl + sizeof(Closure)); cl->info.mptr->data = (char*)cl + sizeof(Closure) + sizeof(ManagedPtr); memcpy(cl->info.mptr->data, ptr, size);@@ -292,7 +330,7 @@ VAL MKFLOATc(VM* vm, double val) { Closure* cl = allocate(sizeof(Closure), 1);- SETTY(cl, FLOAT);+ SETTY(cl, CT_FLOAT); cl -> info.f = val; return cl; }@@ -300,7 +338,7 @@ VAL MKSTRc(VM* vm, char* str) { Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) + sizeof(char)*strlen(str)+1, 1);- SETTY(cl, STRING);+ SETTY(cl, CT_STRING); cl -> info.str = (char*)cl + sizeof(Closure); strcpy(cl -> info.str, str);@@ -309,7 +347,7 @@ VAL MKPTRc(VM* vm, void* ptr) { Closure* cl = allocate(sizeof(Closure), 1);- SETTY(cl, PTR);+ SETTY(cl, CT_PTR); cl -> info.ptr = ptr; return cl; }@@ -317,7 +355,7 @@ VAL MKMPTRc(VM* vm, void* ptr, size_t size) { Closure* cl = allocate(sizeof(Closure) + sizeof(ManagedPtr) + size, 1);- SETTY(cl, MANAGEDPTR);+ SETTY(cl, CT_MANAGEDPTR); cl->info.mptr = (ManagedPtr*)((char*)cl + sizeof(Closure)); cl->info.mptr->data = (char*)cl + sizeof(Closure) + sizeof(ManagedPtr); memcpy(cl->info.mptr->data, ptr, size);@@ -327,28 +365,28 @@ VAL MKB8(VM* vm, uint8_t bits8) { Closure* cl = allocate(sizeof(Closure), 1);- SETTY(cl, BITS8);+ SETTY(cl, CT_BITS8); cl -> info.bits8 = bits8; return cl; } VAL MKB16(VM* vm, uint16_t bits16) { Closure* cl = allocate(sizeof(Closure), 1);- SETTY(cl, BITS16);+ SETTY(cl, CT_BITS16); cl -> info.bits16 = bits16; return cl; } VAL MKB32(VM* vm, uint32_t bits32) { Closure* cl = allocate(sizeof(Closure), 1);- SETTY(cl, BITS32);+ SETTY(cl, CT_BITS32); cl -> info.bits32 = bits32; return cl; } VAL MKB64(VM* vm, uint64_t bits64) { Closure* cl = allocate(sizeof(Closure), 1);- SETTY(cl, BITS64);+ SETTY(cl, CT_BITS64); cl -> info.bits64 = bits64; return cl; }@@ -390,18 +428,18 @@ return; } switch(GETTY(v)) {- case CON:+ case CT_CON: printf("%d[", TAG(v)); for(i = 0; i < ARITY(v); ++i) { dumpVal(v->info.c.args[i]); } printf("] "); break;- case STRING:+ case CT_STRING: printf("STR[%s]", v->info.str); break;- case FWD:- printf("FWD ");+ case CT_FWD:+ printf("CT_FWD "); dumpVal((VAL)(v->info.ptr)); break; default:@@ -434,6 +472,24 @@ return MKINT(0); } +VAL idris_peekDouble(VM* vm, VAL ptr, VAL offset) {+ return MKFLOAT(vm, *(double*)(GETPTR(ptr) + GETINT(offset)));+}++VAL idris_pokeDouble(VAL ptr, VAL offset, VAL data) {+ *(double*)(GETPTR(ptr) + GETINT(offset)) = GETFLOAT(data);+ return MKINT(0);+}++VAL idris_peekSingle(VM* vm, VAL ptr, VAL offset) {+ return MKFLOAT(vm, *(float*)(GETPTR(ptr) + GETINT(offset)));+}++VAL idris_pokeSingle(VAL ptr, VAL offset, VAL data) {+ *(float*)(GETPTR(ptr) + GETINT(offset)) = GETFLOAT(data);+ return MKINT(0);+}+ void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i_int size) { memmove(dest + dest_offset, src + src_offset, size); }@@ -441,7 +497,7 @@ VAL idris_castIntStr(VM* vm, VAL i) { int x = (int) GETINT(i); Closure* cl = allocate(sizeof(Closure) + sizeof(char)*16, 0);- SETTY(cl, STRING);+ SETTY(cl, CT_STRING); cl -> info.str = (char*)cl + sizeof(Closure); sprintf(cl -> info.str, "%d", x); return cl;@@ -452,25 +508,25 @@ ClosureType ty = i->ty; switch (ty) {- case BITS8:+ case CT_BITS8: // max length 8 bit unsigned int str 3 chars (256) cl = allocate(sizeof(Closure) + sizeof(char)*4, 0); cl->info.str = (char*)cl + sizeof(Closure); sprintf(cl->info.str, "%" PRIu8, (uint8_t)i->info.bits8); break;- case BITS16:+ case CT_BITS16: // max length 16 bit unsigned int str 5 chars (65,535) cl = allocate(sizeof(Closure) + sizeof(char)*6, 0); cl->info.str = (char*)cl + sizeof(Closure); sprintf(cl->info.str, "%" PRIu16, (uint16_t)i->info.bits16); break;- case BITS32:+ case CT_BITS32: // max length 32 bit unsigned int str 10 chars (4,294,967,295) cl = allocate(sizeof(Closure) + sizeof(char)*11, 0); cl->info.str = (char*)cl + sizeof(Closure); sprintf(cl->info.str, "%" PRIu32, (uint32_t)i->info.bits32); break;- case BITS64:+ case CT_BITS64: // max length 64 bit unsigned int str 20 chars (18,446,744,073,709,551,615) cl = allocate(sizeof(Closure) + sizeof(char)*21, 0); cl->info.str = (char*)cl + sizeof(Closure);@@ -481,7 +537,7 @@ exit(EXIT_FAILURE); } - SETTY(cl, STRING);+ SETTY(cl, CT_STRING); return cl; } @@ -496,7 +552,7 @@ VAL idris_castFloatStr(VM* vm, VAL i) { Closure* cl = allocate(sizeof(Closure) + sizeof(char)*32, 0);- SETTY(cl, STRING);+ SETTY(cl, CT_STRING); cl -> info.str = (char*)cl + sizeof(Closure); snprintf(cl -> info.str, 32, "%.16g", GETFLOAT(i)); return cl;@@ -512,7 +568,7 @@ // dumpVal(l); // printf("\n"); Closure* cl = allocate(sizeof(Closure) + strlen(ls) + strlen(rs) + 1, 0);- SETTY(cl, STRING);+ SETTY(cl, CT_STRING); cl -> info.str = (char*)cl + sizeof(Closure); strcpy(cl -> info.str, ls); strcat(cl -> info.str, rs);@@ -558,7 +614,7 @@ VAL MKSTROFFc(VM* vm, StrOffset* off) { Closure* cl = allocate(sizeof(Closure) + sizeof(StrOffset), 1);- SETTY(cl, STROFFSET);+ SETTY(cl, CT_STROFFSET); cl->info.str_offset = (StrOffset*)((char*)cl + sizeof(Closure)); cl->info.str_offset->str = off->str;@@ -572,7 +628,7 @@ // gc moves str if (space(vm, sizeof(Closure) + sizeof(StrOffset))) { Closure* cl = allocate(sizeof(Closure) + sizeof(StrOffset), 0);- SETTY(cl, STROFFSET);+ SETTY(cl, CT_STROFFSET); cl->info.str_offset = (StrOffset*)((char*)cl + sizeof(Closure)); int offset = 0;@@ -600,7 +656,7 @@ if ((xval & 0x80) == 0) { // ASCII char Closure* cl = allocate(sizeof(Closure) + strlen(xstr) + 2, 0);- SETTY(cl, STRING);+ SETTY(cl, CT_STRING); cl -> info.str = (char*)cl + sizeof(Closure); cl -> info.str[0] = (char)(GETINT(x)); strcpy(cl -> info.str+1, xstr);@@ -608,7 +664,7 @@ } else { char *init = idris_utf8_fromChar(xval); Closure* cl = allocate(sizeof(Closure) + strlen(init) + strlen(xstr) + 1, 0);- SETTY(cl, STRING);+ SETTY(cl, CT_STRING); cl -> info.str = (char*)cl + sizeof(Closure); strcpy(cl -> info.str, init); strcat(cl -> info.str, xstr);@@ -626,7 +682,7 @@ char *start = idris_utf8_advance(GETSTR(str), GETINT(offset)); char *end = idris_utf8_advance(start, GETINT(length)); Closure* newstr = allocate(sizeof(Closure) + (end - start) +1, 0);- SETTY(newstr, STRING);+ SETTY(newstr, CT_STRING); newstr -> info.str = (char*)newstr + sizeof(Closure); memcpy(newstr -> info.str, start, end - start); *(newstr -> info.str + (end - start) + 1) = '\0';@@ -637,7 +693,7 @@ char *xstr = GETSTR(str); Closure* cl = allocate(sizeof(Closure) + strlen(xstr) + 1, 0);- SETTY(cl, STRING);+ SETTY(cl, CT_STRING); cl->info.str = (char*)cl + sizeof(Closure); idris_utf8_rev(xstr, cl->info.str); return cl;@@ -720,7 +776,7 @@ return x; } switch(GETTY(x)) {- case CON:+ case CT_CON: ar = CARITY(x); if (ar == 0 && CTAG(x) < 256) { // globally allocated cl = x;@@ -734,34 +790,34 @@ } } break;- case FLOAT:+ case CT_FLOAT: cl = MKFLOATc(vm, x->info.f); break;- case STRING:+ case CT_STRING: cl = MKSTRc(vm, x->info.str); break;- case BIGINT:+ case CT_BIGINT: cl = MKBIGMc(vm, x->info.ptr); break;- case PTR:+ case CT_PTR: cl = MKPTRc(vm, x->info.ptr); break;- case MANAGEDPTR:+ case CT_MANAGEDPTR: cl = MKMPTRc(vm, x->info.mptr->data, x->info.mptr->size); break;- case BITS8:+ case CT_BITS8: cl = idris_b8CopyForGC(vm, x); break;- case BITS16:+ case CT_BITS16: cl = idris_b16CopyForGC(vm, x); break;- case BITS32:+ case CT_BITS32: cl = idris_b32CopyForGC(vm, x); break;- case BITS64:+ case CT_BITS64: cl = idris_b64CopyForGC(vm, x); break;- case RAWDATA:+ case CT_RAWDATA: { size_t size = x->info.size + sizeof(Closure); cl = allocate(size, 0);@@ -971,7 +1027,7 @@ nullary_cons = malloc(256 * sizeof(VAL)); for(i = 0; i < 256; ++i) { cl = malloc(sizeof(Closure));- SETTY(cl, CON);+ SETTY(cl, CT_CON); cl->info.c.tag_arity = i << 8; nullary_cons[i] = cl; }
rts/idris_rts.h view
@@ -25,9 +25,9 @@ // Closures typedef enum {- CON, INT, BIGINT, FLOAT, STRING, STROFFSET,- BITS8, BITS16, BITS32, BITS64, UNIT, PTR, FWD,- MANAGEDPTR, RAWDATA+ CT_CON, CT_INT, CT_BIGINT, CT_FLOAT, CT_STRING, CT_STROFFSET,+ CT_BITS8, CT_BITS16, CT_BITS32, CT_BITS64, CT_UNIT, CT_PTR, CT_FWD,+ CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA } ClosureType; typedef struct Closure *VAL;@@ -67,20 +67,21 @@ uint32_t bits32; uint64_t bits64; ManagedPtr* mptr;+ CHeapItem* c_heap_item; size_t size; } info; } Closure; -struct VM_t;+struct VM; struct Msg_t {- struct VM_t* sender;+ struct VM* sender; VAL msg; }; typedef struct Msg_t Msg; -struct VM_t {+struct VM { int active; // 0 if no longer running; keep for message passing // TODO: If we're going to have lots of concurrent threads, // we really need to be cleverer than this!@@ -90,6 +91,7 @@ VAL* valstack_base; VAL* stack_max; + CHeap c_heap; Heap heap; #ifdef HAS_PTHREAD pthread_mutex_t inbox_lock;@@ -110,8 +112,38 @@ VAL reg1; }; -typedef struct VM_t VM;+typedef struct VM VM; ++/* C data interface: allocation on the C heap.+ *+ * Although not enforced in code, CData is meant to be opaque+ * and non-RTS code (such as libraries or C bindings) should+ * access only its (void *) field called "data".+ *+ * Feel free to mutate cd->data; the heap does not care+ * about its particular value. However, keep in mind+ * that it must not break Idris's referential transparency.+ *+ * If you call cdata_allocate or cdata_manage, the resulting+ * CData object *must* be returned from your FFI function so+ * that it is inserted in the C heap. Otherwise the memory+ * will be leaked.+ */++/// C data block. Contains (void * data).+typedef CHeapItem * CData;++/// Allocate memory, returning the corresponding C data block.+CData cdata_allocate(size_t size, CDataFinalizer * finalizer);++/// Wrap a pointer as a C data block.+/// The size should be an estimate of how much memory, in bytes,+/// is associated with the pointer. This estimate need not be absolutely precise+/// but it is necessary for GC to work effectively.+CData cdata_manage(void * data, size_t size, CDataFinalizer * finalizer);++ // Create a new VM VM* init_vm(int stack_size, size_t heap_size, int max_threads);@@ -150,16 +182,17 @@ #define GETPTR(x) (((VAL)(x))->info.ptr) #define GETMPTR(x) (((VAL)(x))->info.mptr->data) #define GETFLOAT(x) (((VAL)(x))->info.f)+#define GETCDATA(x) (((VAL)(x))->info.c_heap_item) #define GETBITS8(x) (((VAL)(x))->info.bits8) #define GETBITS16(x) (((VAL)(x))->info.bits16) #define GETBITS32(x) (((VAL)(x))->info.bits32) #define GETBITS64(x) (((VAL)(x))->info.bits64) -#define TAG(x) (ISINT(x) || x == NULL ? (-1) : ( GETTY(x) == CON ? (x)->info.c.tag_arity >> 8 : (-1)) )-#define ARITY(x) (ISINT(x) || x == NULL ? (-1) : ( GETTY(x) == CON ? (x)->info.c.tag_arity & 0x000000ff : (-1)) )+#define TAG(x) (ISINT(x) || x == NULL ? (-1) : ( GETTY(x) == CT_CON ? (x)->info.c.tag_arity >> 8 : (-1)) )+#define ARITY(x) (ISINT(x) || x == NULL ? (-1) : ( GETTY(x) == CT_CON ? (x)->info.c.tag_arity & 0x000000ff : (-1)) ) -// Already checked it's a CON+// Already checked it's a CT_CON #define CTAG(x) (((x)->info.c.tag_arity) >> 8) #define CARITY(x) ((x)->info.c.tag_arity & 0x000000ff) @@ -179,7 +212,7 @@ #define MKINT(x) ((void*)((x)<<1)+1) #define GETINT(x) ((i_int)(x)>>1) #define ISINT(x) ((((i_int)x)&1) == 1)-#define ISSTR(x) (GETTY(x) == STRING)+#define ISSTR(x) (GETTY(x) == CT_STRING) #define INTOP(op,x,y) MKINT((i_int)((((i_int)x)>>1) op (((i_int)y)>>1))) #define UINTOP(op,x,y) MKINT((i_int)((((uintptr_t)x)>>1) op (((uintptr_t)y)>>1)))@@ -210,6 +243,7 @@ VAL MKB16(VM* vm, uint16_t b); VAL MKB32(VM* vm, uint32_t b); VAL MKB64(VM* vm, uint64_t b);+VAL MKCDATA(VM* vm, CHeapItem * item); // following versions don't take a lock when allocating VAL MKFLOATc(VM* vm, double val);@@ -217,6 +251,7 @@ VAL MKSTRc(VM* vm, char* str); VAL MKPTRc(VM* vm, void* ptr); VAL MKMPTRc(VM* vm, void* ptr, size_t size);+VAL MKCDATAc(VM* vm, CHeapItem * item); char* GETSTROFF(VAL stroff); @@ -248,12 +283,12 @@ #define allocCon(cl, vm, t, a, o) \ cl = allocate(sizeof(Closure) + sizeof(VAL)*a, o); \- SETTY(cl, CON); \+ SETTY(cl, CT_CON); \ cl->info.c.tag_arity = ((t) << 8) | (a); #define updateCon(cl, old, t, a) \ cl = old; \- SETTY(cl, CON); \+ SETTY(cl, CT_CON); \ cl->info.c.tag_arity = ((t) << 8) | (a); #define NULL_CON(x) nullary_cons[x]@@ -313,6 +348,10 @@ VAL idris_peekPtr(VM* vm, VAL ptr, VAL offset); VAL idris_pokePtr(VAL ptr, VAL offset, VAL data);+VAL idris_peekDouble(VM* vm, VAL ptr, VAL offset);+VAL idris_pokeDouble(VAL ptr, VAL offset, VAL data);+VAL idris_peekSingle(VM* vm, VAL ptr, VAL offset);+VAL idris_pokeSingle(VAL ptr, VAL offset, VAL data); // String primitives VAL idris_concat(VM* vm, VAL l, VAL r);
src/IRTS/CodegenC.hs view
@@ -75,6 +75,7 @@ libFlags <- getLibFlags incFlags <- getIncFlags envFlags <- getEnvFlags+ let stackFlag = if isWindows then ["-Wl,--stack,16777216"] else [] let args = [gccDbg dbg] ++ gccFlags iface ++ -- # Any flags defined here which alter the RTS API must also be added to config.mk@@ -85,7 +86,7 @@ (if not iface then libFlags else []) ++ incFlags ++ (if not iface then libs else []) ++- flags +++ flags ++ stackFlag ++ ["-o", out] -- putStrLn (show args) exit <- rawSystem comp args@@ -354,6 +355,7 @@ | c == sUN "C_Float" = FArith ATFloat | c == sUN "C_Ptr" = FPtr | c == sUN "C_MPtr" = FManagedPtr+ | c == sUN "C_CData" = FCData | c == sUN "C_Unit" = FUnit toFType (FApp c [_,ity]) | c == sUN "C_IntT" = FArith (toAType ity)@@ -378,6 +380,7 @@ c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")" c_irts FManagedPtr l x = l ++ "MKMPTR(vm, " ++ x ++ ")" c_irts (FArith ATFloat) l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"+c_irts FCData l x = l ++ "MKCDATA(vm, " ++ x ++ ")" c_irts FAny l x = l ++ x c_irts FFunction l x = error "Return of function from foreign call is not supported" c_irts FFunctionIO l x = error "Return of function from foreign call is not supported"@@ -391,6 +394,7 @@ irts_c FPtr x = "GETPTR(" ++ x ++ ")" irts_c FManagedPtr x = "GETMPTR(" ++ x ++ ")" irts_c (FArith ATFloat) x = "GETFLOAT(" ++ x ++ ")"+irts_c FCData x = "GETCDATA(" ++ x ++ ")" irts_c FAny x = x irts_c FFunctionIO x = wrapped x irts_c FFunction x = wrapped x@@ -649,9 +653,20 @@ = v ++ "idris_peekPtr(vm," ++ creg p ++ "," ++ creg o ++")" doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__pokePtr" = v ++ "idris_pokePtr(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"+doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__pokeDouble"+ = v ++ "idris_pokeDouble(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"+doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peekDouble"+ = v ++ "idris_peekDouble(vm," ++ creg p ++ "," ++ creg o ++")"+doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__pokeSingle"+ = v ++ "idris_pokeSingle(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"+doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peekSingle"+ = v ++ "idris_peekSingle(vm," ++ creg p ++ "," ++ creg o ++")" doOp v (LExternal pk) [] | pk == sUN "prim__sizeofPtr" = v ++ "MKINT(sizeof(void*))"-doOp v (LExternal mpt) [p] | mpt == sUN "prim__asPtr" = v ++ "MKPTR(vm, GETMPTR("++ creg p ++"))"+doOp v (LExternal mpt) [p] | mpt == sUN "prim__asPtr"+ = v ++ "MKPTR(vm, GETMPTR("++ creg p ++"))"+doOp v (LExternal offs) [p, n] | offs == sUN "prim__ptrOffset"+ = v ++ "MKPTR(vm, GETPTR(" ++ creg p ++ ") + GETINT(" ++ creg n ++ "))" doOp _ op args = error $ "doOp not implemented (" ++ show (op, args) ++ ")" @@ -790,19 +805,13 @@ (if ret /= "void" then indent 1 ++ ret ++ " ret;\n" else "") ++ indent 1 ++ "VM* vm = get_vm();\n" ++ indent 1 ++ "if (vm == NULL) {\n" ++- indent 2 ++ "fprintf(stderr, \"No vm available in callback.\");\n" ++- indent 2 ++ "exit(-1);\n" +++ indent 2 ++ "vm = idris_vm();\n" ++ indent 1 ++ "}\n" ++ indent 1 ++ "INITFRAME;\n" ++ indent 1 ++ "RESERVE(" ++ show (len + 1) ++ ");\n" ++ indent 1 ++ "allocCon(REG1, vm, " ++ show tag ++ ",0 , 0);\n" ++ indent 1 ++ "TOP(0) = REG1;\n" ++-- push 1 argList ++- indent 1 ++ "STOREOLD;\n" ++- indent 1 ++ "BASETOP(0);\n" ++- indent 1 ++ "ADDTOP(" ++ show (len + 1) ++ ");\n" ++- indent 1 ++ "CALL(_idris__123_APPLY0_125_);\n" +++ applyArgs argList ++ if ret /= "void" then indent 1 ++ "ret = " ++ irts_c (toFType ft) "RVAL" ++ ";\n" ++ indent 1 ++ "return ret;\n}\n\n"@@ -811,6 +820,19 @@ (ret, ft) = rty desc argList = zip (args desc) [0..] len = length argList++ applyArgs (x:y:xs) = push 1 [x] +++ indent 1 ++ "STOREOLD;\n" +++ indent 1 ++ "BASETOP(0);\n" +++ indent 1 ++ "ADDTOP(2);\n" +++ indent 1 ++ "CALL(_idris__123_APPLY0_125_);\n" +++ indent 1 ++ "TOP(0)=REG1;\n" +++ applyArgs (y:xs)+ applyArgs x = push 1 x +++ indent 1 ++ "STOREOLD;\n" +++ indent 1 ++ "BASETOP(0);\n" +++ indent 1 ++ "ADDTOP(" ++ show (length x + 1) ++ ");\n" +++ indent 1 ++ "CALL(_idris__123_APPLY0_125_);\n" renderArgs [] = "void" renderArgs [((s, _), n)] = s ++ " a" ++ (show n) renderArgs (((s, _), n):xs) = s ++ " a" ++ (show n) ++ ", " ++
src/IRTS/Lang.hs view
@@ -17,10 +17,11 @@ deriving (Show, Eq) -- ASSUMPTION: All variable bindings have unique names here+-- Constructors commented as lifted are not present in the LIR provided to the different backends. data LExp = LV LVar | LApp Bool LExp [LExp] -- True = tail call | LLazyApp Name [LExp] -- True = tail call- | LLazyExp LExp+ | LLazyExp LExp -- lifted out before compiling | LForce LExp -- make sure Exp is evaluted | LLet Name LExp LExp -- name just for pretty printing | LLam [Name] LExp -- lambda, lifted out before compiling@@ -99,6 +100,7 @@ | FUnit | FPtr | FManagedPtr+ | FCData | FAny deriving (Show, Eq) @@ -132,7 +134,7 @@ lname (NS n x) i = NS (lname n i) x lname (UN n) i = MN i n-lname x i = sMN i (show x ++ "_lam")+lname x i = sMN i (showCG x ++ "_lam") liftAll :: [(Name, LDecl)] -> [(Name, LDecl)] liftAll xs = concatMap (\ (x, d) -> lambdaLift x d) xs@@ -215,7 +217,7 @@ -- Keep track of 'updatable' names in the state, i.e. names whose heap -- entry may be reused, along with the arity which was there findUp :: LExp -> State [(Name, Int)] LExp- findUp (LApp t (LV (Glob n)) as) + findUp (LApp t (LV (Glob n)) as) | Just (LConstructor _ i ar) <- lookupCtxtExact n defs, ar == length as = findUp (LCon Nothing i n as)@@ -241,7 +243,7 @@ findUp (LOp o es) = LOp o <$> mapM findUp es findUp (LCase Updatable e@(LV (Glob n)) as) = LCase Updatable e <$> mapM (doUpAlt n) as- findUp (LCase t e as) + findUp (LCase t e as) = LCase t <$> findUp e <*> mapM findUpAlt as findUp t = return t @@ -252,7 +254,7 @@ findUpAlt (LConstCase i rhs) = LConstCase i <$> findUp rhs findUpAlt (LDefaultCase rhs) = LDefaultCase <$> findUp rhs - doUpAlt n (LConCase i t args rhs) + doUpAlt n (LConCase i t args rhs) = do avail <- get put ((n, length args) : avail) rhs' <- findUp rhs@@ -282,7 +284,7 @@ usedIn env (LLam ns e) = usedIn (env \\ ns) e usedIn env (LCon v i n args) = let rest = concatMap (usedIn env) args in case v of- Nothing -> rest + Nothing -> rest Just (Glob n) -> usedArg env n ++ rest usedIn env (LProj t i) = usedIn env t usedIn env (LCase up e alts) = usedIn env e ++ concatMap (usedInA env) alts@@ -329,7 +331,7 @@ Updatable -> "! " fmt [] = "" fmt [alt]- = "\t" ++ ind ++ "| " ++ showAlt env (ind ++ " ") alt + = "\t" ++ ind ++ "| " ++ showAlt env (ind ++ " ") alt fmt (alt:as) = "\t" ++ ind ++ "| " ++ showAlt env (ind ++ ". ") alt ++ "\n" ++ fmt as
src/Idris/AbsSyntax.hs view
@@ -1593,7 +1593,7 @@ -- binding -- Not the function position, but do everything else... implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args- implNamesIn uv t = namesIn uv ist t+ implNamesIn uv t = implicitNamesIn (map fst uv) ist t imps top env ty@(PApp _ f as) = do (decls, ns) <- get
src/Idris/AbsSyntaxTree.hs view
@@ -775,6 +775,9 @@ data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type | RClausesInstrs Name [([(Name, Term)], Term, Term)] | RAddInstance Name Name+ | RDatatypeDeclInstrs Name [PArg]+ | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]+ -- ^ Datatype, constructors -- | For elaborator state data EState = EState {
src/Idris/Core/Elaborate.hs view
@@ -139,13 +139,19 @@ execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux) execElab a e ps = execStateT e (ES (ps, a) "" Nothing) -initElaborator :: Name -> Context -> Ctxt TypeInfo -> Type -> ProofState+initElaborator :: Name -- ^ the name of what's to be elaborated+ -> Context -- ^ the current global context+ -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState+ -> Int -- ^ the value of the idris_name field of IState+ -> Type -- ^ the goal type+ -> ProofState initElaborator = newProof -elaborate :: Context -> Ctxt TypeInfo -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)-elaborate ctxt datatypes n ty d elab = do let ps = initElaborator n ctxt datatypes ty- (a, ES ps' str _) <- runElab d elab ps- return $! (a, str)+elaborate :: Context -> Ctxt TypeInfo -> Int -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)+elaborate ctxt datatypes globalNames n ty d elab =+ do let ps = initElaborator n ctxt datatypes globalNames ty+ (a, ES ps' str _) <- runElab d elab ps+ return $! (a, str) -- | Modify the auxiliary state updateAux :: (aux -> aux) -> Elab' aux ()@@ -209,6 +215,14 @@ set_datatypes :: Ctxt TypeInfo -> Elab' aux () set_datatypes ds = do ES (p, a) logs prev <- get put (ES (p { datatypes = ds }, a) logs prev)++get_global_nextname :: Elab' aux Int+get_global_nextname = do ES (ps, _) _ _ <- get+ return (global_nextname ps)++set_global_nextname :: Int -> Elab' aux ()+set_global_nextname i = do ES (ps, a) logs prev <- get+ put $ ES (ps { global_nextname = i}, a) logs prev -- | get the proof term get_term :: Elab' aux Term
src/Idris/Core/Evaluate.hs view
@@ -13,7 +13,7 @@ lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact, lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal, mapDefCtxt, - lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,+ lookupTotal, lookupTotalExact, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName, Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions, isUniverse) where @@ -1082,6 +1082,10 @@ lookupTotal :: Name -> Context -> [Totality] lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)+ where mkt (d, a, t, m) = t++lookupTotalExact :: Name -> Context -> Maybe Totality+lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt) where mkt (d, a, t, m) = t lookupMetaInformation :: Name -> Context -> [MetaInformation]
src/Idris/Core/ProofState.hs view
@@ -25,7 +25,10 @@ data ProofState = PS { thname :: Name, holes :: [Name], -- ^ holes still to be solved usedns :: [Name], -- ^ used names, don't use again- nextname :: Int, -- ^ name supply+ nextname :: Int, -- ^ name supply, for locally unique names+ global_nextname :: Int, -- ^ a mirror of the global name supply,+ -- for generating things like type tags+ -- in reflection pterm :: ProofTerm, -- ^ current proof term ptype :: Type, -- ^ original goal dontunify :: [Name], -- ^ explicitly given by programmer, leave it@@ -305,11 +308,16 @@ addLog :: Monad m => String -> StateT TState m () addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" }) -newProof :: Name -> Context -> Ctxt TypeInfo -> Type -> ProofState-newProof n ctxt datatypes ty =+newProof :: Name -- ^ the name of what's to be elaborated+ -> Context -- ^ the current global context+ -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState+ -> Int -- ^ the value of the idris_name field of IState+ -> Type -- ^ the goal type+ -> ProofState+newProof n ctxt datatypes globalNames ty = let h = holeName 0 ty' = vToP ty- in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')+ in PS n [h] [] 1 globalNames (mkProofTerm (Bind h (Hole ty') (P Bound h ty'))) ty [] (h, []) [] [] Nothing [] [] [] [] [] []
src/Idris/Coverage.hs view
@@ -334,11 +334,12 @@ x -> return () -- stop if total checkAllCovering _ _ _ _ = return () --- Check if, in a given group of type declarations mut_ns,+-- | Check if, in a given group of type declarations mut_ns, -- the constructor cn : ty is strictly positive, -- and update the context accordingly--checkPositive :: [Name] -> (Name, Type) -> Idris Totality+checkPositive :: [Name] -- ^ the group of type declarations+ -> (Name, Type) -- ^ the constructor+ -> Idris Totality checkPositive mut_ns (cn, ty') = do i <- getIState let ty = delazy' True (normalise (tt_ctxt i) [] ty')@@ -381,8 +382,8 @@ _ -> checkSizeChange n where checkLHS i (P _ fn _)- = case lookupTotal fn (tt_ctxt i) of- [Partial _] -> return (Partial (Other [fn]))+ = case lookupTotalExact fn (tt_ctxt i) of+ Just (Partial _) -> return (Partial (Other [fn])) _ -> Nothing checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a) checkLHS _ _ = Nothing@@ -596,8 +597,8 @@ toJust (n, t) = Just t - getType n = case lookupTy n (tt_ctxt ist) of- [ty] -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist+ getType n = case lookupTyExact n (tt_ctxt ist) of+ Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist isInductive (P _ nty _) (P _ nty' _) = let co = case lookupCtxt nty (idris_datatypes ist) of
src/Idris/Elab/Clause.hs view
@@ -486,14 +486,15 @@ i <- getIState let lhs = addImplPat i lhs_in -- if the LHS type checks, it is possible- case elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState+ case elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState (erun fc (buildTC i info ELHS [] fname (allNamesIn lhs_in) (infTerm lhs))) of- OK (ElabResult lhs' _ _ ctxt' newDecls highlights, _) ->+ OK (ElabResult lhs' _ _ ctxt' newDecls highlights newGName, _) -> do setContext ctxt' processTacticDecls info newDecls sendHighlighting highlights+ updateIState $ \i -> i { idris_name = newGName } let lhs_tm = orderPats (getInferTerm lhs') case recheck ctxt' [] (forget lhs_tm) lhs_tm of OK _ -> return True@@ -587,8 +588,8 @@ logElab 4 ("Fixed parameters: " ++ show params ++ " from " ++ showTmImpls lhs_in ++ "\n" ++ show (fn_ty, fn_is)) - ((ElabResult lhs' dlhs [] ctxt' newDecls highlights, probs, inj), _) <-- tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState+ ((ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, probs, inj), _) <-+ tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState (do res <- errAt "left hand side of " fname Nothing (erun fc (buildTC i info ELHS opts fname (allNamesIn lhs_in)@@ -599,6 +600,7 @@ setContext ctxt' processTacticDecls info newDecls sendHighlighting highlights+ updateIState $ \i -> i { idris_name = newGName } when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs) @@ -670,14 +672,14 @@ logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs ctxt <- getContext -- new context with where block added logElab 5 "STARTING CHECK"- ((rhs', defer, holes, is, probs, ctxt', newDecls, highlights), _) <-- tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patRHS") clhsty initEState+ ((rhs', defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-+ tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patRHS") clhsty initEState (do pbinds ist lhs_tm -- proof search can use explicitly written names mapM_ addPSname (allNamesIn lhs_in) mapM_ setinj (nub (tcparams ++ inj)) setNextName- (ElabResult _ _ is ctxt' newDecls highlights) <-+ (ElabResult _ _ is ctxt' newDecls highlights newGName) <- errAt "right hand side of " fname (Just clhsty) (erun fc (build i winfo ERHS opts fname rhs)) errAt "right hand side of " fname (Just clhsty)@@ -688,10 +690,11 @@ (map fst $ case_decls aux) ctxt tt) [] probs <- get_probs hs <- get_holes- return (tm, ds, hs, is, probs, ctxt', newDecls, highlights))+ return (tm, ds, hs, is, probs, ctxt', newDecls, highlights, newGName)) setContext ctxt' processTacticDecls info newDecls sendHighlighting highlights+ updateIState $ \i -> i { idris_name = newGName } when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs) @@ -838,8 +841,8 @@ propagateParams i params fn_ty (allNamesIn lhs_in) (addImplPat i lhs_in) logElab 2 ("LHS: " ++ show lhs)- (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-- tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState+ (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-+ tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState (errAt "left hand side of with in " fname Nothing (erun fc (buildTC i info ELHS opts fname (allNamesIn lhs_in)@@ -847,6 +850,7 @@ setContext ctxt' processTacticDecls info newDecls sendHighlighting highlights+ updateIState $ \i -> i { idris_name = newGName } ctxt <- getContext let lhs_tm = orderPats (getInferTerm lhs')@@ -860,22 +864,23 @@ let wval = addImplBound i (map fst bargs) wval_in logElab 5 ("Checking " ++ showTmImpls wval) -- Elaborate wval in this context- ((wval', defer, is, ctxt', newDecls, highlights), _) <-- tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")+ ((wval', defer, is, ctxt', newDecls, highlights, newGName), _) <-+ tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "withRHS") (bindTyArgs PVTy bargs infP) initEState (do pbinds i lhs_tm -- proof search can use explicitly written names mapM_ addPSname (allNamesIn lhs_in) setNextName -- TODO: may want where here - see winfo abpve- (ElabResult _ d is ctxt' newDecls highlights) <- errAt "with value in " fname Nothing+ (ElabResult _ d is ctxt' newDecls highlights newGName) <- errAt "with value in " fname Nothing (erun fc (build i info ERHS opts fname (infTerm wval))) erun fc $ psolve lhs_tm tt <- get_term- return (tt, d, is, ctxt', newDecls, highlights))+ return (tt, d, is, ctxt', newDecls, highlights, newGName)) setContext ctxt' processTacticDecls info newDecls sendHighlighting highlights+ updateIState $ \i -> i { idris_name = newGName } def' <- checkDef fc iderr True defer let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'@@ -970,18 +975,19 @@ logElab 5 ("New RHS " ++ showTmImpls rhs) ctxt <- getContext -- New context with block added i <- getIState- ((rhs', defer, is, ctxt', newDecls, highlights), _) <-- tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "wpatRHS") clhsty initEState+ ((rhs', defer, is, ctxt', newDecls, highlights, newGName), _) <-+ tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "wpatRHS") clhsty initEState (do pbinds i lhs_tm setNextName- (ElabResult _ d is ctxt' newDecls highlights) <-+ (ElabResult _ d is ctxt' newDecls highlights newGName) <- erun fc (build i info ERHS opts fname rhs) psolve lhs_tm tt <- get_term- return (tt, d, is, ctxt', newDecls, highlights))+ return (tt, d, is, ctxt', newDecls, highlights, newGName)) setContext ctxt' processTacticDecls info newDecls sendHighlighting highlights+ updateIState $ \i -> i { idris_name = newGName } def' <- checkDef fc iderr True defer let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
src/Idris/Elab/Data.hs view
@@ -90,7 +90,7 @@ ttag <- getName i <- getIState let as = map (const (Left (Msg ""))) (getArgTys cty)- let params = findParams (map snd cons)+ let params = findParams n (map snd cons) logElab 2 $ "Parameters : " ++ show params -- TI contains information about mutually declared types - this will -- be updated when the mutual block is complete@@ -132,13 +132,6 @@ (nfc, AnnName n Nothing Nothing Nothing)) dcons where- setDetaggable :: Name -> Idris ()- setDetaggable n = do- ist <- getIState- let opt = idris_optimisation ist- case lookupCtxt n opt of- [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }- _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt } checkDefinedAs fc n t i = let defined = tclift $ tfail (At fc (AlreadyDefined n))@@ -152,63 +145,8 @@ _ -> defined _ -> defined _ -> defined- -- parameters are names which are unchanged across the structure,- -- which appear exactly once in the return type of a constructor - -- First, find all applications of the constructor, then check over- -- them for repeated arguments - findParams :: [Type] -> [Int]- findParams ts = let allapps = map getDataApp ts- -- do each constructor separately, then merge the results (names- -- may change between constructors)- conParams = map paramPos allapps in- inAll conParams-- inAll :: [[Int]] -> [Int]- inAll [] = []- inAll (x : xs) = filter (\p -> all (\ps -> p `elem` ps) xs) x-- paramPos [] = []- paramPos (args : rest)- = dropNothing $ keepSame (zip [0..] args) rest-- dropNothing [] = []- dropNothing ((x, Nothing) : ts) = dropNothing ts- dropNothing ((x, _) : ts) = x : dropNothing ts-- keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->- [(Int, Maybe Name)]- keepSame as [] = as- keepSame as (args : rest) = keepSame (update as args) rest- where- update [] _ = []- update _ [] = []- update ((n, Just x) : as) (Just x' : args)- | x == x' = (n, Just x) : update as args- update ((n, _) : as) (_ : args) = (n, Nothing) : update as args-- getDataApp :: Type -> [[Maybe Name]]- getDataApp f@(App _ _ _)- | (P _ d _, args) <- unApply f- = if (d == n) then [mParam args args] else []- getDataApp (Bind n (Pi _ t _) sc)- = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)- getDataApp _ = []-- -- keep the arguments which are single names, which don't appear- -- elsewhere-- mParam args [] = []- mParam args (P Bound n _ : rest)- | count n args == 1- = Just n : mParam args rest- where count n [] = 0- count n (t : ts)- | n `elem` freeNames t = 1 + count n ts- | otherwise = count n ts- mParam args (_ : rest) = Nothing : mParam args rest- cname (_, _, n, _, _, _, _) = n -- Abuse of ElabInfo.@@ -263,7 +201,7 @@ where tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc) tyIs con t | (P Bound n' _, _) <- unApply t- = if n' /= tn then + = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con Nothing (Msg ("Type level variable " ++ show n' ++ " is not " ++ show tn)))) else return ()
src/Idris/Elab/Instance.hs view
@@ -186,12 +186,14 @@ ty' <- implicit info syn iname ty' let ty = addImpl [] i ty' ctxt <- getContext- (ElabResult tyT _ _ ctxt' newDecls highlights, _) <-- tclift $ elaborate ctxt (idris_datatypes i) iname (TType (UVal 0)) initEState+ (ElabResult tyT _ _ ctxt' newDecls highlights newGName, _) <-+ tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) iname (TType (UVal 0)) initEState (errAt "type of " iname Nothing (erun fc (build i info ERHS [] iname ty))) setContext ctxt' processTacticDecls info newDecls sendHighlighting highlights+ updateIState $ \i -> i { idris_name = newGName }+ ctxt <- getContext (cty, _) <- recheckC fc id [] tyT let nty = normalise ctxt [] cty
src/Idris/Elab/RunElab.hs view
@@ -32,18 +32,20 @@ mustBeElabScript scriptTy ist <- getIState ctxt <- getContext- (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-- tclift $ elaborate ctxt (idris_datatypes ist) (sMN 0 "toplLevelElab") elabScriptTy initEState+ (ElabResult tyT' defer is ctxt' newDecls highlights newGName, log) <-+ tclift $ elaborate ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "toplLevelElab") elabScriptTy initEState (transformErr RunningElabScript (erun fc (do tm <- runElabAction ist fc [] script ns EState is _ impls highlights <- getAux ctxt <- get_context let ds = [] -- todo log <- getLog- return (ElabResult tm ds (map snd is) ctxt impls highlights))))+ newGName <- get_global_nextname+ return (ElabResult tm ds (map snd is) ctxt impls highlights newGName)))) setContext ctxt' processTacticDecls info newDecls sendHighlighting highlights+ updateIState $ \i -> i { idris_name = newGName }
src/Idris/Elab/Term.hs view
@@ -18,7 +18,7 @@ import Idris.Core.ProofTerm (getProofTerm) import Idris.Core.Typecheck (check, recheck, converts, isType) import Idris.Core.WHNF (whnf)-import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)+import Idris.Coverage (buildSCG, checkDeclTotality, checkPositive, genClauses, recoverableCoverage, validCoverageCase) import Idris.ErrReverse (errReverse) import Idris.Elab.Quasiquote (extractUnquotes) import Idris.Elab.Utils@@ -52,6 +52,9 @@ , resultTyDecls :: [RDeclInstructions] -- ^ Meta-info about the new type declarations , resultHighlighting :: [(FC, OutputAnnotation)]+ -- ^ Saved highlights from elaboration+ , resultName :: Int+ -- ^ The new global name counter } @@ -122,9 +125,10 @@ ctxt <- get_context let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) [] log <- getLog+ g_nextname <- get_global_nextname if log /= ""- then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights)- else return (ElabResult tm ds (map snd is) ctxt impls highlights)+ then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)+ else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname) where pattern = emode == ELHS tydecl = emode == ETyDecl @@ -166,9 +170,10 @@ ctxt <- get_context let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) [] log <- getLog+ g_nextname <- get_global_nextname if (log /= "")- then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights)- else return (ElabResult tm ds (map snd is) ctxt impls highlights)+ then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)+ else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname) where pattern = emode == ELHS -- return whether arguments of the given constructor name can be@@ -1158,9 +1163,10 @@ -- capturing lexically available variables in the quoted term. ctxt <- get_context datatypes <- get_datatypes+ g_nextname <- get_global_nextname saveState updatePS (const .- newProof (sMN 0 "q") ctxt datatypes $+ newProof (sMN 0 "q") ctxt datatypes g_nextname $ P Ref (reflm "TT") Erased) -- Re-add the unquotes, letting Idris infer the (fictional)@@ -1839,11 +1845,74 @@ updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e} return () + checkClosed :: Raw -> Elab' aux (Term, Type) checkClosed tm = do ctxt <- get_context (val, ty) <- lift $ check ctxt [] tm return $! (finalise val, finalise ty) + -- | Add another argument to a Pi+ mkPi :: RFunArg -> Raw -> Raw+ mkPi arg rTy = RBind (argName arg) (Pi Nothing (argTy arg) (RUType AllTypes)) rTy++ mustBeType ctxt tm ty =+ case normaliseAll ctxt [] (finalise ty) of+ UType _ -> return ()+ TType _ -> return ()+ ty' -> lift . tfail . InternalMsg $+ show tm ++ " is not a type: it's " ++ show ty'++ mustNotBeDefined ctxt n =+ case lookupDefExact n ctxt of+ Just _ -> lift . tfail . InternalMsg $+ show n ++ " is already defined."+ Nothing -> return ()++ -- | Prepare a constructor to be added to a datatype being defined here+ prepareConstructor :: Name -> RConstructorDefn -> ElabD (Name, [PArg], Type)+ prepareConstructor tyn (RConstructor cn args resTy) =+ do ctxt <- get_context+ -- ensure the constructor name is not qualified, and+ -- construct a qualified one+ notQualified cn+ let qcn = qualify cn++ -- ensure that the constructor name is not defined already+ mustNotBeDefined ctxt qcn++ -- construct the actual type for the constructor+ let cty = foldr mkPi resTy args+ (checkedTy, ctyTy) <- lift $ check ctxt [] cty+ mustBeType ctxt checkedTy ctyTy++ -- ensure that the constructor builds the right family+ case unApply (getRetTy (normaliseAll ctxt [] (finalise checkedTy))) of+ (P _ n _, _) | n == tyn -> return ()+ t -> lift . tfail . Msg $ "The constructor " ++ show cn +++ " doesn't construct " ++ show tyn +++ " (return type is " ++ show t ++ ")"++ -- add temporary type declaration for constructor (so it can+ -- occur in later constructor types)+ set_context (addTyDecl qcn (DCon 0 0 False) checkedTy ctxt)++ -- Save the implicits for high-level Idris+ let impls = map rFunArgToPArg args++ return (qcn, impls, checkedTy)++ where+ notQualified (NS _ _) = lift . tfail . Msg $ "Constructor names may not be qualified"+ notQualified _ = return ()++ qualify n = case tyn of+ (NS _ ns) -> NS n ns+ _ -> n++ getRetTy :: Type -> Type+ getRetTy (Bind _ (Pi _ _ _) sc) = getRetTy sc+ getRetTy ty = ty+ -- | Do a step in the reflected elaborator monad. The input is the -- step, the output is the (reflected) term returned. runTacTm :: Term -> ElabD Term@@ -2052,20 +2121,10 @@ | n == tacN "Prim__DeclareType", [decl] <- args = do (RDeclare n args res) <- reifyTyDecl decl ctxt <- get_context- let mkPi arg res = RBind (argName arg)- (Pi Nothing (argTy arg) (RUType AllTypes))- res- rty = foldr mkPi res args+ let rty = foldr mkPi res args (checked, ty') <- lift $ check ctxt [] rty- case normaliseAll ctxt [] (finalise ty') of- UType _ -> return ()- TType _ -> return ()- ty'' -> lift . tfail . InternalMsg $- show checked ++ " is not a type: it's " ++ show ty''- case lookupDefExact n ctxt of- Just _ -> lift . tfail . InternalMsg $- show n ++ " is already defined."- Nothing -> return ()+ mustBeType ctxt checked ty'+ mustNotBeDefined ctxt n let decl = TyDecl Ref checked ctxt' = addCtxtDef n decl ctxt set_context ctxt'@@ -2076,11 +2135,46 @@ = do defn <- reifyFunDefn decl defineFunction defn returnUnit+ | n == tacN "Prim__DeclareDatatype", [decl] <- args+ = do RDeclare n args resTy <- reifyTyDecl decl+ ctxt <- get_context+ let tcTy = foldr mkPi resTy args+ (checked, ty') <- lift $ check ctxt [] tcTy+ mustBeType ctxt checked ty'+ mustNotBeDefined ctxt n+ let ctxt' = addTyDecl n (TCon 0 0) checked ctxt+ set_context ctxt'+ updateAux $ \e -> e { new_tyDecls = RDatatypeDeclInstrs n (map rFunArgToPArg args) : new_tyDecls e }+ returnUnit+ | n == tacN "Prim__DefineDatatype", [defn] <- args+ = do RDefineDatatype n ctors <- reifyRDataDefn defn+ ctxt <- get_context+ tyconTy <- case lookupTyExact n ctxt of+ Just t -> return t+ Nothing -> lift . tfail . Msg $ "Type not previously declared"+ datatypes <- get_datatypes+ case lookupCtxtName n datatypes of+ [] -> return ()+ _ -> lift . tfail . Msg $ show n ++ " is already defined as a datatype."+ -- Prepare the constructors+ ctors' <- mapM (prepareConstructor n) ctors+ ttag <- do ES (ps, aux) str prev <- get+ let i = global_nextname ps+ put $ ES (ps { global_nextname = global_nextname ps + 1 },+ aux)+ str+ prev+ return i+ let ctxt' = addDatatype (Data n ttag tyconTy False (map (\(cn, _, cty) -> (cn, cty)) ctors')) ctxt+ set_context ctxt'+ -- the rest happens in a bit+ updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }+ returnUnit | n == tacN "Prim__AddInstance", [cls, inst] <- args = do className <- reifyTTName cls instName <- reifyTTName inst updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :- new_tyDecls e}+ new_tyDecls e } returnUnit | n == tacN "Prim__IsTCName", [n] <- args = do n' <- reifyTTName n@@ -2115,6 +2209,7 @@ aux <- getAux datatypes <- get_datatypes env <- get_env+ g_next <- get_global_nextname (ctxt', ES (p, aux') _ _) <- do (ES (current_p, _) _ _) <- get@@ -2122,13 +2217,15 @@ (do runElabAction ist fc [] script ns ctxt' <- get_context return ctxt')- ((newProof recH ctxt datatypes goalTT)+ ((newProof recH ctxt datatypes g_next goalTT) { nextname = nextname current_p }) set_context ctxt' let tm_out = getProofTerm (pterm p) do (ES (prf, _) s e) <- get- let p' = prf { nextname = nextname p }+ let p' = prf { nextname = nextname p+ , global_nextname = global_nextname p+ } put (ES (p', aux') s e) env' <- get_env (tm, ty, _) <- lift $ recheck ctxt' env (forget tm_out) tm_out@@ -2520,6 +2617,50 @@ let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True, True))) ds in addDeferred ds' _ -> return ()+ RDatatypeDeclInstrs n impls ->+ do addIBC (IBCDef n)+ updateIState $ \i -> i { idris_implicits = addDef n impls (idris_implicits i) }+ addIBC (IBCImp n)++ RDatatypeDefnInstrs tyn tyconTy ctors ->+ do let cn (n, _, _) = n+ cimpls (_, impls, _) = impls+ cty (_, _, t) = t+ addIBC (IBCDef tyn)+ mapM_ (addIBC . IBCDef . cn) ctors+ let params = findParams tyn (map cty ctors)+ let typeInfo = TI (map cn ctors) False [] params []+ -- implicit precondition to IBCData is that idris_datatypes on the IState is populated.+ -- otherwise writing the IBC just fails silently!+ updateIState $ \i -> i { idris_datatypes =+ addDef tyn typeInfo (idris_datatypes i) }+ addIBC (IBCData tyn)+++ ttag <- getName -- from AbsSyntax.hs, really returns a disambiguating Int++ let metainf = DataMI params+ addIBC (IBCMetaInformation tyn metainf)+ updateContext (setMetaInformation tyn metainf)++ for_ ctors $ \(cn, impls, _) ->+ do updateIState $ \i -> i { idris_implicits = addDef cn impls (idris_implicits i) }+ addIBC (IBCImp cn)++ for_ ctors $ \(ctorN, _, _) ->+ do totcheck (NoFC, ctorN)+ ctxt <- tt_ctxt <$> getIState+ case lookupTyExact ctorN ctxt of+ Just cty -> do checkPositive (tyn : map cn ctors) (ctorN, cty)+ return ()+ Nothing -> return ()++ case ctors of+ [ctor] -> do setDetaggable (cn ctor); setDetaggable tyn+ addIBC (IBCOpt (cn ctor)); addIBC (IBCOpt tyn)+ _ -> return ()+ -- TODO: inaccessible+ RAddInstance className instName -> do -- The type class resolution machinery relies on a special logElab 2 $ "Adding elab script instance " ++ show instName ++@@ -2581,13 +2722,14 @@ let lhs = addImplPat ist lhs_in let fc = fileFC "elab_reflected_totality" let tcgen = False -- TODO: later we may support dictionary generation- case elaborate ctxt (idris_datatypes ist) (sMN 0 "refPatLHS") infP initEState+ case elaborate ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "refPatLHS") infP initEState (erun fc (buildTC ist info ELHS [] fname (allNamesIn lhs_in) (infTerm lhs))) of- OK (ElabResult lhs' _ _ _ _ _, _) ->+ OK (ElabResult lhs' _ _ _ _ _ name', _) -> do -- not recursively calling here, because we don't -- want to run infinitely many times let lhs_tm = orderPats (getInferTerm lhs')+ updateIState $ \i -> i { idris_name = name' } case recheck ctxt [] (forget lhs_tm) lhs_tm of OK _ -> return True err -> return False
src/Idris/Elab/Transform.hs view
@@ -54,13 +54,14 @@ i <- getIState let lhs = addImplPat i lhs_in logElab 5 ("Transform LHS input: " ++ showTmImpls lhs)- (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-- tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transLHS") infP initEState+ (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-+ tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transLHS") infP initEState (erun fc (buildTC i info ETransLHS [] (sUN "transform") (allNamesIn lhs_in) (infTerm lhs))) setContext ctxt' processTacticDecls info newDecls sendHighlighting highlights+ updateIState $ \i -> i { idris_name = newGName } let lhs_tm = orderPats (getInferTerm lhs') let lhs_ty = getInferType lhs' let newargs = pvars i lhs_tm@@ -73,18 +74,21 @@ let rhs = addImplBound i (map fst newargs) rhs_in logElab 5 ("Transform RHS input: " ++ showTmImpls rhs) - ((rhs', defer, ctxt', newDecls), _) <-- tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transRHS") clhs_ty initEState+ ((rhs', defer, ctxt', newDecls, newGName), _) <-+ tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transRHS") clhs_ty initEState (do pbinds i lhs_tm setNextName- (ElabResult _ _ _ ctxt' newDecls highlights) <- erun fc (build i info ERHS [] (sUN "transform") rhs)+ (ElabResult _ _ _ ctxt' newDecls highlights newGName) <- erun fc (build i info ERHS [] (sUN "transform") rhs)+ set_global_nextname newGName erun fc $ psolve lhs_tm tt <- get_term let (rhs', defer) = runState (collectDeferred Nothing [] ctxt tt) []- return (rhs', defer, ctxt', newDecls))+ newGName <- get_global_nextname+ return (rhs', defer, ctxt', newDecls, newGName)) setContext ctxt' processTacticDecls info newDecls sendHighlighting highlights+ updateIState $ \i -> i { idris_name = newGName } (crhs_tm_in, crhs_ty) <- recheckC_borrowing False False [] fc id [] rhs' let crhs_tm = renamepats pnames crhs_tm_in
src/Idris/Elab/Type.hs view
@@ -67,12 +67,13 @@ logElab 5 $ show "with methods " ++ show (imp_methods syn) logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty - (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-- tclift $ elaborate ctxt (idris_datatypes i) n (TType (UVal 0)) initEState+ (ElabResult tyT' defer is ctxt' newDecls highlights newGName, log) <-+ tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) n (TType (UVal 0)) initEState (errAt "type of " n Nothing (erun fc (build i info ETyDecl [] n ty))) setContext ctxt' processTacticDecls info newDecls- sendHighlighting highlights+ sendHighlighting highlights + updateIState $ \i -> i { idris_name = newGName } let tyT = patToImp tyT'
src/Idris/Elab/Utils.hs view
@@ -331,4 +331,67 @@ else return () +-- | Find the type constructor arguments that are parameters, given a list of constructor types.+-- Parameters are names which are unchanged across the structure,+-- which appear exactly once in the return type of a constructor+-- First, find all applications of the constructor, then check over+-- them for repeated arguments+findParams :: Name -- ^ the name of the family that we are finding parameters for+ -> [Type] -- ^ the declared constructor types+ -> [Int]+findParams tyn ts =+ let allapps = map getDataApp ts+ -- do each constructor separately, then merge the results (names+ -- may change between constructors)+ conParams = map paramPos allapps+ in inAll conParams + where+ inAll :: [[Int]] -> [Int]+ inAll [] = []+ inAll (x : xs) = filter (\p -> all (\ps -> p `elem` ps) xs) x++ paramPos [] = []+ paramPos (args : rest)+ = dropNothing $ keepSame (zip [0..] args) rest+ dropNothing [] = []+ dropNothing ((x, Nothing) : ts) = dropNothing ts+ dropNothing ((x, _) : ts) = x : dropNothing ts+ keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->+ [(Int, Maybe Name)]+ keepSame as [] = as+ keepSame as (args : rest) = keepSame (update as args) rest+ where+ update [] _ = []+ update _ [] = []+ update ((n, Just x) : as) (Just x' : args)+ | x == x' = (n, Just x) : update as args+ update ((n, _) : as) (_ : args) = (n, Nothing) : update as args+ getDataApp :: Type -> [[Maybe Name]]+ getDataApp f@(App _ _ _)+ | (P _ d _, args) <- unApply f+ = if (d == tyn) then [mParam args args] else []+ getDataApp (Bind n (Pi _ t _) sc)+ = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)+ getDataApp _ = []+ -- keep the arguments which are single names, which don't appear+ -- elsewhere+ mParam args [] = []+ mParam args (P Bound n _ : rest)+ | count n args == 1+ = Just n : mParam args rest+ where count n [] = 0+ count n (t : ts)+ | n `elem` freeNames t = 1 + count n ts+ | otherwise = count n ts+ mParam args (_ : rest) = Nothing : mParam args rest++-- | Mark a name as detaggable in the global state (should be called+-- for type and constructor names of single-constructor datatypes)+setDetaggable :: Name -> Idris ()+setDetaggable n = do+ ist <- getIState+ let opt = idris_optimisation ist+ case lookupCtxt n opt of+ [oi] -> putIState ist { idris_optimisation = addDef n oi { detaggable = True } opt }+ _ -> putIState ist { idris_optimisation = addDef n (Optimise [] True) opt }
src/Idris/Elab/Value.hs view
@@ -64,14 +64,15 @@ -- * elaboration as a Type -- * elaboration as a function a -> b - (ElabResult tm' defer is ctxt' newDecls highlights, _) <-- tclift (elaborate ctxt (idris_datatypes i) (sMN 0 "val") infP initEState+ (ElabResult tm' defer is ctxt' newDecls highlights newGName, _) <-+ tclift (elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "val") infP initEState (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm))) -- Extend the context with new definitions created setContext ctxt' processTacticDecls info newDecls sendHighlighting highlights+ updateIState $ \i -> i { idris_name = newGName } let vtm = orderPats (getInferTerm tm')
src/Idris/Interactive.hs view
@@ -172,7 +172,7 @@ ++ with ++ "\n" ++ unlines rest) runIO $ copyFile fb fn- else iPrintResult with+ else iPrintResult (with ++ "\n") where getIndent s = length (takeWhile isSpace s) -- Replace the given metavariable on the given line with a 'case'
src/Idris/Parser/Expr.hs view
@@ -586,7 +586,7 @@ {- | Parses a disambiguation expression Disamb ::=- '%' 'disamb' NameList Expr+ 'with' NameList Expr ; -} disamb :: SyntaxInfo -> IdrisParser PTerm
src/Idris/Parser/Helpers.hs view
@@ -245,20 +245,20 @@ -- | Idris Style for parsing identifiers/reserved keywords idrisStyle :: MonadicParsing m => IdentifierStyle m-idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier- where _styleName = "Idris"- _styleStart = satisfy isAlpha <|> oneOf "_"- _styleLetter = satisfy isAlphaNum <|> oneOf "_'."- _styleReserved = HS.fromList ["let", "in", "data", "codata", "record", "corecord", "Type",- "do", "dsl", "import", "impossible",- "case", "of", "total", "partial", "mutual",- "infix", "infixl", "infixr", "rewrite",- "where", "with", "syntax", "proof", "postulate",- "using", "namespace", "class", "instance",- "interface", "implementation", "parameters",- "public", "private", "export", "abstract", "implicit",- "quoteGoal", "constructor",- "if", "then", "else"]+idrisStyle = IdentifierStyle {+ _styleName = "Idris"+ , _styleStart = satisfy isAlpha <|> oneOf "_"+ , _styleLetter = satisfy isAlphaNum <|> oneOf "_'."+ , _styleReserved = HS.fromList+ ["let", "in", "data", "codata", "record", "corecord", "Type", "do", "dsl",+ "import", "impossible", "case", "of", "total", "partial", "mutual",+ "infix", "infixl", "infixr", "rewrite", "where", "with", "syntax",+ "proof", "postulate", "using", "namespace", "class", "instance",+ "interface", "implementation", "parameters", "public", "private",+ "export", "abstract", "implicit", "quoteGoal", "constructor", "if",+ "then", "else"]+ , _styleHighlight = Hi.Identifier+ , _styleReservedHighlight = Hi.ReservedIdentifier } char :: MonadicParsing m => Char -> m Char char = Chr.char@@ -293,7 +293,7 @@ -- reserved identifiers never contain line breaks. reservedFC :: MonadicParsing m => String -> m FC reservedFC str = do (FC file (l, c) _) <- getFC- Tok.reserve idrisStyle str+ reserved str return $ FC file (l, c) (l, c + length str) -- | Parse a reserved identfier, highlighting its span as a keyword@@ -308,10 +308,9 @@ notFollowedBy (operatorLetter) <?> ("end of " ++ show name) reservedOpFC :: MonadicParsing m => String -> m FC-reservedOpFC name = token $ try $ do (FC f (l, c) _) <- getFC- string name- notFollowedBy (operatorLetter) <?> ("end of " ++ show name)- return (FC f (l, c) (l, c + length name))+reservedOpFC name = do (FC f (l, c) _) <- getFC+ reservedOp name+ return (FC f (l, c) (l, c + length name)) -- | Parses an identifier as a token identifier :: (MonadicParsing m) => m (String, FC)@@ -393,7 +392,7 @@ commentMarkers = [ "--", "|||" ] invalidOperators :: [String]-invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]+invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!", "@"] -- | Parses an operator operator :: MonadicParsing m => m String@@ -404,12 +403,9 @@ -- | Parses an operator operatorFC :: MonadicParsing m => m (String, FC)-operatorFC = do (op, fc) <- token $ do (FC f (l, c) _) <- getFC- op <- some operatorLetter- return (op, FC f (l, c) (l, c + length op))- when (op `elem` (invalidOperators ++ commentMarkers)) $- fail $ op ++ " is not a valid operator"- return (op, fc)+operatorFC = do (FC f (l, c) _) <- getFC+ op <- operator+ return (op, FC f (l, c) (l, c + length op)) {- * Position helpers -} {- | Get filename from position (returns "(interactive)" when no source file is given) -}
src/Idris/Prover.hs view
@@ -85,7 +85,7 @@ prove :: Bool -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris () prove mode opt ctxt lit n ty- = do ps <- fmap (\ist -> initElaborator n ctxt (idris_datatypes ist) ty) getIState+ = do ps <- fmap (\ist -> initElaborator n ctxt (idris_datatypes ist) (idris_name ist) ty) getIState idemodePutSExp "start-proof-mode" n (tm, prf) <- if mode
src/Idris/Reflection.hs view
@@ -48,6 +48,10 @@ data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RCtorArg], Raw)] deriving Show +data RConstructorDefn = RConstructor Name [RFunArg] Raw++data RDataDefn = RDefineDatatype Name [RConstructorDefn]+ rArgOpts :: RErasure -> [ArgOpt] rArgOpts RErased = [InaccessibleArg] rArgOpts _ = []@@ -963,7 +967,7 @@ Right (TextPart msg) reifyReportPart (App _ (P (DCon _ _ _) n _) ttn) | n == reflm "NamePart" =- case runElab initEState (reifyTTName ttn) (initElaborator (sMN 0 "hole") initContext emptyContext Erased) of+ case runElab initEState (reifyTTName ttn) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of Error e -> Left . InternalMsg $ "could not reify name term " ++ show ttn ++@@ -971,7 +975,7 @@ OK (n', _)-> Right $ NamePart n' reifyReportPart (App _ (P (DCon _ _ _) n _) tm) | n == reflm "TermPart" =- case runElab initEState (reifyTT tm) (initElaborator (sMN 0 "hole") initContext emptyContext Erased) of+ case runElab initEState (reifyTT tm) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of Error e -> Left . InternalMsg $ "could not reify reflected term " ++ show tm ++@@ -979,7 +983,7 @@ OK (tm', _) -> Right $ TermPart tm' reifyReportPart (App _ (P (DCon _ _ _) n _) tm) | n == reflm "RawPart" =- case runElab initEState (reifyRaw tm) (initElaborator (sMN 0 "hole") initContext emptyContext Erased) of+ case runElab initEState (reifyRaw tm) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of Error e -> Left . InternalMsg $ "could not reify reflected raw term " ++ show tm ++@@ -1043,6 +1047,18 @@ | n == tacN "MkImpossibleClause" && t == reflm "Raw" = fmap RMkImpossibleClause $ reifyRaw lhs reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause." reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."++reifyRConstructorDefn :: Term -> ElabD RConstructorDefn+reifyRConstructorDefn (App _ (App _ (App _ (P _ n _) cn) args) retTy)+ | n == tacN "Constructor", Just args' <- unList args+ = RConstructor <$> reifyTTName cn <*> mapM reifyRFunArg args' <*> reifyRaw retTy+reifyRConstructorDefn aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RConstructorDefn"++reifyRDataDefn :: Term -> ElabD RDataDefn+reifyRDataDefn (App _ (App _ (P _ n _) tyn) ctors)+ | n == tacN "DefineDatatype", Just ctors' <- unList ctors+ = RDefineDatatype <$> reifyTTName tyn <*> mapM reifyRConstructorDefn ctors'+reifyRDataDefn aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RDataDefn" envTupleType :: Raw envTupleType
src/Util/ScreenSize.hs view
@@ -1,24 +1,6 @@-{-# LANGUAGE CPP #-} module Util.ScreenSize(getScreenWidth) where -#ifndef CURSES--getScreenWidth :: IO Int-getScreenWidth = return 80--#else--import UI.HSCurses.Curses-import System.IO (hIsTerminalDevice, stdout)+import System.Console.Terminal.Size (size, width) getScreenWidth :: IO Int-getScreenWidth = do term <- hIsTerminalDevice stdout- if term- then do- initScr- refresh- size <- scrSize- endWin- return (snd size)- else return 80-#endif+getScreenWidth = maybe 80 width `fmap` size
stack.yaml view
@@ -1,16 +1,16 @@-resolver: lts-4.2+resolver: lts-5.5+ packages:-- '.'+ - '.'+ flags:- idris:- FFI: true- GMP: True- curses: True-extra-deps: -- annotated-wl-pprint-0.7.0-- cheapskate-0.1.0.4-- hscurses-1.4.2.0-- libffi-0.1+ idris:+ FFI: true+ GMP: true++extra-deps:+ - libffi-0.1+ nix:- enable: false- shell-file: stack-shell.nix+ enable: false+ shell-file: stack-shell.nix
test/Makefile view
@@ -12,7 +12,7 @@ @./runtest $(patsubst %.test,%,$@) -q test_js: runtest- @./runtest without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 basic007 basic011 ffi006 ffi007 primitives005 opts --codegen node+ @./runtest without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 basic007 basic011 ffi006 ffi007 ffi008 primitives005 primitives006 opts --codegen node update: runtest @./runtest all -u
test/ffi007/expected view
@@ -6,3 +6,4 @@ 00000377 I'm dynamic 3 6+7
test/ffi007/ffi007.c view
@@ -28,3 +28,7 @@ callback test_ffi6(void) { return &dynamic_fn; }++void test_mulpar(void (*fn)(int, int)) {+ fn(3,4);+}
test/ffi007/ffi007.h view
@@ -9,3 +9,5 @@ void test_ffi3(void (*cb)(void)); callback test_ffi6(void);++void test_mulpar(void (*fn)(int, int));
test/ffi007/ffi007.idr view
@@ -34,6 +34,14 @@ test7 : Ptr -> Int -> IO Int test7 fnptr i = foreign FFI_C "%dynamic" (Ptr -> Int -> IO Int) fnptr i +adder : Int -> Int -> ()+adder x y = unsafePerformIO $ do+ printLn $ x + y++test8 : IO ()+test8 = foreign FFI_C "test_mulpar" (CFnPtr (Int -> Int -> ()) -> IO ())+ (MkCFnPtr adder)+ main : IO () main = do test@@ -46,4 +54,5 @@ fptr <- test6 i <- test7 fptr 3 printLn i+ test8 return ()
+ test/ffi008/expected view
@@ -0,0 +1,5 @@+True+True+a: 122 b: 0+4+00000010
+ test/ffi008/ffi008.c view
@@ -0,0 +1,14 @@+#include "ffi008.h"+#include <stdio.h>++int size1(void) {+ return sizeof(struct test1);+}++int size2(void) {+ return sizeof(struct test2);+}++void print_mystruct(void) {+ printf("a: %d b: %d\n", mystruct.a, mystruct.b);+}
+ test/ffi008/ffi008.h view
@@ -0,0 +1,17 @@+#include <stdint.h>++struct test1 {+ int8_t a;+ int64_t b;+};++struct test2 {+ int32_t a;+ int16_t b;+};++struct test2 mystruct;++int size1(void);+int size2(void);+void print_mystruct();
+ test/ffi008/ffi008.idr view
@@ -0,0 +1,48 @@+module Main++import CFFI+import Data.Vect++%include C "ffi008.h"++size1 : IO Int+size1 = foreign FFI_C "size1" (IO Int)+++size2 : IO Int+size2 = foreign FFI_C "size2" (IO Int)++mystruct : IO Ptr+mystruct = foreign FFI_C "&mystruct" (IO Ptr)++print_mystruct : IO ()+print_mystruct = foreign FFI_C "print_mystruct" (IO ())++test1 : Composite+test1 = STRUCT [I8, I64]++test2 : Composite+test2 = STRUCT [I32, I16]++test3 : Composite+test3 = STRUCT [DOUBLE, DOUBLE, I8, I64]++test4 : Composite+test4 = PACKEDSTRUCT [I8, I8, I8, I64]+++main : IO ()+main = do+ printLn $ sizeOf test1 == !size1+ printLn $ sizeOf test2 == !size2+ fms <- return $ (test2#0) !mystruct+ poke I32 fms 122+ print_mystruct+ printLn $ fields test3+ withAlloc test2 $ \p => do+ f1 <- return $ (test2 # 0) p+ poke I32 f1 8+ update I32 f1 (* 2)+ print !(peek I32 f1)+ withAlloc PTR $ \p =>+ poke PTR p fms
+ test/ffi008/run view
@@ -0,0 +1,4 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ ffi008.idr -o ffi008 -p contrib --cg-opt "ffi008.c"+./ffi008+rm -f ffi008 *.ibc
test/interactive001/expected view
@@ -6,6 +6,7 @@ f x :: map f xs isElem2 x (y :: ys) with (_) isElem2 x (y :: ys) | with_pat = ?isElem2_rhs+ isElem3 x (x :: ys) | (Yes Refl) = ?isElem3_rhs_3 [] => ?bar_1
test/meta002/AgdaStyleReflection.idr view
@@ -40,13 +40,6 @@ | Constant Const | Ty -unApply : Raw -> (Raw, List Raw)-unApply tm = unApply' tm []- where unApply' : Raw -> List Raw -> (Raw, List Raw)- unApply' (RApp f x) xs = unApply' f (x::xs)- unApply' notApp xs = (notApp, xs)-- implementation Quotable Plicity Raw where quotedTy = `(Plicity) quote Explicit = `(Explicit)
+ test/meta002/DataDef.idr view
@@ -0,0 +1,73 @@+module DataDef++foo : Elab ()+foo = do declareDatatype $ Declare `{{DataDef.N}} [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type)+ defineDatatype $ DefineDatatype `{{DataDef.N}} [+ Constructor `{{MkN}} [MkFunArg `{{x}} `(Nat) Implicit NotErased] (RApp (Var `{{DataDef.N}}) (Var `{{x}})),+ Constructor `{{MkN'}} [MkFunArg `{{x}} `(Nat) Explicit NotErased] (RApp (Var `{{DataDef.N}}) (RApp (Var `{S}) (Var `{{x}})))+ ]+%runElab foo++one : N 1+one = MkN++two : N 2+two = MkN' 1+++-- mutual+-- data U : Type where+-- Base : U+-- Pi : (code : U) -> (el code -> U) -> U+-- el : U -> Type+-- el Base = Bool+-- el (Pi code body) = (x : el code) -> el (body x)++++mkU : Elab ()+mkU = do let U = `{{DataDef.U}}+ let el = `{{DataDef.el}}+ declareDatatype $ Declare U [] `(Type)+ declareType $ Declare el [MkFunArg `{{code}} (Var U) Explicit NotErased] `(Type)+ defineDatatype $ DefineDatatype U [+ Constructor `{{Base}} [] (Var U),+ Constructor `{{Pi}}+ [MkFunArg `{{code}} (Var U) Explicit NotErased,+ MkFunArg `{{body}} `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)) Explicit NotErased]+ (Var U)+ ]+ defineFunction $ DefineFun el [+ MkFunClause (RBind `{{code}} (PVar (Var U))+ (RBind `{{body}} (PVar `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)))+ (RApp (Var el)+ (RApp (RApp (Var `{{DataDef.Pi}})+ (Var `{{code}}))+ (Var `{{body}})))))+ (RBind `{{code}} (PVar (Var U))+ (RBind `{{body}} (PVar `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)))+ (RBind `{{x}} (Pi (RApp (Var el) (Var `{{code}})) `(Type))+ (RApp (Var el) (RApp (Var `{{body}}) (Var `{{x}})))))),+ MkFunClause (RApp (Var el) (Var `{{DataDef.Base}})) `(Bool)++ ]++%runElab mkU++tt : el Base+tt = True++fun : el (Pi Base (\x => if x then Base else Pi Base (const Base)))+fun = \x => (case x of+ False => \y => False+ True => False)+++nope : Elab ()+nope = defineDatatype $ DefineDatatype `{Either} [+ Constructor `{{Middle}} [ MkFunArg `{{x}} `(Type) Implicit NotErased+ , MkFunArg `{{y}} `(Type) Implicit NotErased+ ] `(Either ~(Var `{{x}}) ~(Var `{{y}}))+ ]+%runElab nope+
test/meta002/expected view
@@ -1,9 +1,12 @@+DataDef.idr:72:1-9:+While running an elaboration script, the following error occurred:+Prelude.Either.Either is already defined as a datatype. Tacs.idr:298:15: When checking right hand side of testElab3 with expected type DPair Ty (Tm []) Unifying ty and ARR ty t would lead to infinite value-AgdaStyleReflection.idr:328:5:+AgdaStyleReflection.idr:321:5: When checking right hand side of baz with expected type (Nat, Void)
test/meta002/run view
@@ -1,4 +1,5 @@ #!/usr/bin/env bash+${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 DataDef.idr ${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 Tacs.idr ${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 AgdaStyleReflection.idr # Disabled due to excess memory consumption
+ test/primitives006/Data/ByteArray.idr view
@@ -0,0 +1,100 @@+module Data.ByteArray++%include C "array.h"+%link C "array.o"++%access public export+%default total++namespace Byte+ Byte : Type+ Byte = Bits8++ toInt : Byte -> Int+ toInt = prim__zextB8_Int++ fromInt : Int -> Byte+ fromInt = prim__truncInt_B8++export+record ByteArray where+ constructor BA+ ptr : CData+ sz : Int++-- This needn't be precise; it just needs to be enough to be safe.+export+bytesPerInt : Int+bytesPerInt = 8++export+allocate : Int -> IO ByteArray+allocate sz = do+ ptr <- foreign FFI_C "array_alloc" (Int -> IO CData) sz+ return $ BA ptr sz++export+reallocate : Int -> ByteArray -> IO ()+reallocate newSz (BA ptr sz)+ = foreign FFI_C "array_realloc" (Int -> CData -> IO ()) sz ptr++export+peek : Int -> ByteArray -> IO Byte+peek ofs (BA ptr sz)+ = if (ofs < 0 || ofs >= sz)+ then return 0+ else foreign FFI_C "array_peek" (Int -> CData -> IO Byte) ofs ptr++export+peekInt : Int -> ByteArray -> IO Int+peekInt ofs (BA ptr sz)+ = if (ofs < 0 || ofs+bytesPerInt > sz)+ then return 0+ else foreign FFI_C "array_peek_int" (Int -> CData -> IO Int) ofs ptr++export+poke : Int -> Byte -> ByteArray -> IO ()+poke ofs b (BA ptr sz)+ = if (ofs < 0 || ofs >= sz)+ then return ()+ else foreign FFI_C "array_poke" (Int -> Byte -> CData -> IO ()) ofs b ptr++export+pokeInt : Int -> Int -> ByteArray -> IO ()+pokeInt ofs i (BA ptr sz)+ = if (ofs < 0 || ofs+bytesPerInt > sz)+ then return ()+ else foreign FFI_C "array_poke_int" (Int -> Int -> CData -> IO ()) ofs i ptr++export+copy : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO ()+copy (BA srcPtr srcSz, srcIx) (BA dstPtr dstSz, dstIx) count+ = if (srcIx < 0 || dstIx < 0 || (srcIx+count) > srcSz || (dstIx+count) > dstSz)+ then return ()+ else foreign FFI_C "array_copy" (CData -> Int -> CData -> Int -> Int -> IO ()) srcPtr srcIx dstPtr dstIx count++export+fill : Int -> Int -> Byte -> ByteArray -> IO ()+fill ofs count b (BA ptr sz)+ = if (ofs < 0 || ofs+count > sz)+ then return ()+ else foreign FFI_C "array_fill" (Int -> Int -> Byte -> CData -> IO ()) ofs count b ptr++export+size : ByteArray -> Int+size (BA ptr sz) = sz++export+compare : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO Int+compare (BA ptrL szL, ofsL) (BA ptrR szR, ofsR) count+ = if (ofsL < 0 || ofsL+count > szL || ofsR < 0 || ofsR+count > szR)+ then return 0+ else foreign FFI_C "array_compare" (CData -> Int -> CData -> Int -> Int -> IO Int) ptrL ofsL ptrR ofsR count++export+find : Byte -> ByteArray -> Int -> Int -> IO (Maybe Int)+find b (BA ptr sz) ofs end = do+ ofs <- foreign FFI_C "array_find" (Byte -> CData -> Int -> Int -> IO Int) b ptr ofs end+ if ofs < 0+ then return $ Nothing+ else return $ Just ofs
+ test/primitives006/Data/Bytes.idr view
@@ -0,0 +1,287 @@+module Data.Bytes++import Data.ByteArray as BA++%access public export+%default total++-- Structure of the allocated ByteArray+-- [used_size][.....data.....]+-- used_size is an int and it takes up BA.bytesPerInt bytes+-- at the beginning of the array++export+record Bytes where+ constructor B+ arr : ByteArray+ ofs : Int+ end : Int -- first offset not included in the array++minimalCapacity : Int+minimalCapacity = 16++private+dataOfs : Int+dataOfs = 1 * BA.bytesPerInt++private+allocate : Int -> IO Bytes+allocate capacity = do+ arr <- BA.allocate (BA.bytesPerInt + capacity)+ BA.pokeInt 0 dataOfs arr+ BA.fill dataOfs capacity 0 arr -- zero the array+ return $ B arr dataOfs dataOfs++export+length : Bytes -> Int+length (B arr ofs end) = end - ofs++export+empty : Bytes+empty = unsafePerformIO $ allocate minimalCapacity++export+null : Bytes -> Bool+null (B arr ofs end) = (ofs == end)++%freeze empty++-- factor=1 ~ copy+-- factor=2 ~ grow+private+grow : Int -> Bytes -> IO Bytes+grow factor (B arr ofs end) = do+ maxUsed <- BA.peekInt 0 arr+ let bytesUsed = end - ofs+ let bytesAvailable =+ if maxUsed > end+ then bytesUsed+ else BA.size arr - ofs+ B arr' ofs' end' <- allocate $ (factor*bytesAvailable) `max` minimalCapacity+ BA.copy (arr, ofs) (arr', ofs') bytesUsed+ return $ B arr' ofs' (ofs' + bytesUsed)++%assert_total+export+snoc : Bytes -> Byte -> Bytes+snoc bs@(B arr ofs end) byte+ = if end >= BA.size arr+ then unsafePerformIO $ do -- need more space+ grown <- grow 2 bs+ return $ snoc grown byte+ else unsafePerformIO $ do+ maxUsed <- BA.peekInt 0 arr+ if maxUsed > end+ then do -- someone already took the headroom, need copying+ copy <- grow 2 bs+ return $ snoc copy byte+ else do -- can mutate+ BA.pokeInt 0 (end+1) arr+ BA.poke end byte arr+ return $ B arr ofs (end+1)++infixl 7 |>+export+(|>) : Bytes -> Byte -> Bytes+(|>) = snoc++namespace SnocView+ data SnocView : Type where+ Nil : SnocView+ Snoc : (bs : Bytes) -> (b : Byte) -> SnocView++ export+ snocView : Bytes -> SnocView+ snocView (B arr ofs end) =+ if end == ofs+ then SnocView.Nil+ else unsafePerformIO $ do+ last <- BA.peek (end-1) arr+ return $ SnocView.Snoc (B arr ofs (end-1)) last++namespace ConsView+ data ConsView : Type where+ Nil : ConsView+ Cons : (b : Byte) -> (bs : Bytes) -> ConsView++ export+ consView : Bytes -> ConsView+ consView (B arr ofs end) =+ if end == ofs+ then ConsView.Nil+ else unsafePerformIO $ do+ first <- BA.peek ofs arr+ return $ ConsView.Cons first (B arr (ofs+1) end)++infixr 7 +++%assert_total+export+(++) : Bytes -> Bytes -> Bytes+(++) bsL@(B arrL ofsL endL) bsR@(B arrR ofsR endR)+ = let countR = endR - ofsR in+ if endL + countR > BA.size arrL+ then unsafePerformIO $ do -- need more space+ grown <- grow 2 bsL+ return $ grown ++ bsR+ else unsafePerformIO $ do+ maxUsedL <- BA.peekInt 0 arrL+ if maxUsedL > endL+ then do -- headroom taken+ copyL <- grow 2 bsL+ return $ copyL ++ bsR+ else do -- can mutate+ BA.pokeInt 0 (endL + countR) arrL+ BA.copy (arrR, ofsR) (arrL, endL) countR+ return $ B arrL ofsL (endL + countR)++export+dropPrefix : Int -> Bytes -> Bytes+dropPrefix n (B arr ofs end) = B arr (((ofs + n) `min` end) `max` dataOfs) end++export+takePrefix : Int -> Bytes -> Bytes+takePrefix n (B arr ofs end) = B arr ofs (((ofs + n) `min` end) `max` dataOfs)++export+pack : List Byte -> Bytes+pack = fromList empty+ where+ fromList : Bytes -> List Byte -> Bytes+ fromList bs [] = bs+ fromList bs (x :: xs) = fromList (bs `snoc` x) xs++export+unpack : Bytes -> List Byte+unpack bs with (consView bs)+ | Nil = []+ | Cons x xs = x :: unpack (assert_smaller bs xs)++export+slice : Int -> Int -> Bytes -> Bytes+slice ofs' end' (B arr ofs end)+ = B arr+ (((ofs + ofs') `min` end) `max` dataOfs)+ (((ofs + end') `min` end) `max` dataOfs)++-- Folds with early exit.+-- If Bytes were a Functor, this would be equivalent+-- to a Traversable implementation interpreted in the Either monad.+data Result : Type -> Type where+ Stop : (result : a) -> Result a+ Cont : (acc : a) -> Result a++export+iterateR : (Byte -> a -> Result a) -> a -> Bytes -> a+iterateR f acc bs with (snocView bs)+ | Nil = acc+ | Snoc ys y with (f y acc)+ | Stop result = result+ | Cont acc' = iterateR f acc' (assert_smaller bs ys)++export+iterateL : (a -> Byte -> Result a) -> a -> Bytes -> a+iterateL f acc bs with (consView bs)+ | Nil = acc+ | Cons y ys with (f acc y)+ | Stop result = result+ | Cont acc' = iterateL f acc' (assert_smaller bs ys)++infixl 3 .:+private+(.:) : (a -> b) -> (c -> d -> a) -> (c -> d -> b)+(.:) g f x y = g (f x y)++export+foldr : (Byte -> a -> a) -> a -> Bytes -> a+foldr f = iterateR (Cont .: f)++export+foldl : (a -> Byte -> a) -> a -> Bytes -> a+foldl f = iterateL (Cont .: f)++export+spanLength : (Byte -> Bool) -> Bytes -> Int+spanLength p = iterateL step 0+ where+ step : Int -> Byte -> Result Int+ step n b with (p b)+ | True = Cont (1 + n)+ | False = Stop n++find : Byte -> Bytes -> Maybe Int+find b (B arr ofs end) = unsafePerformIO $ BA.find b arr ofs end++export+splitAt : Int -> Bytes -> (Bytes, Bytes)+splitAt n bs = (takePrefix n bs, dropPrefix n bs)++export+splitOn : Byte -> Bytes -> (Bytes, Bytes)+splitOn b bs with (find b bs)+ | Nothing = (bs, empty)+ | Just ofs = (takePrefix ofs bs, dropPrefix (ofs+1) bs)++export+splitsOn : Byte -> Bytes -> List Bytes+splitsOn b bs with (find b bs)+ | Nothing = [bs]+ | Just ofs = takePrefix ofs bs :: splitsOn b (assert_smaller bs $ dropPrefix (ofs+1) bs)++export+asciiLines : Bytes -> List Bytes+asciiLines = splitsOn 0x0A++export+span : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)+span p bs = splitAt (spanLength p bs) bs++export+break : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)+break p bs = span (not . p) bs++private+cmp : Bytes -> Bytes -> Ordering+cmp (B arrL ofsL endL) (B arrR ofsR endR) = unsafePerformIO $ do+ let countL = endL - ofsL+ let countR = endR - ofsR+ let commonCount = countL `min` countR+ result <- BA.compare (arrL, ofsL) (arrR, ofsR) commonCount+ return $+ if result /= 0+ then i2o result+ else compare countL countR+ where+ i2o : Int -> Ordering+ i2o 0 = EQ+ i2o i = if i < 0 then LT else GT++implementation Eq Bytes where+ xs == ys = (Bytes.cmp xs ys == EQ)++implementation Ord Bytes where+ compare = Bytes.cmp++export+toString : Bytes -> String+toString = foldr (strCons . chr . toInt) ""++export+fromString : String -> Bytes+fromString = foldl (\bs, c => bs |> fromInt (ord c)) empty . unpack++implementation Show Bytes where+ show = ("b" ++) . show . toString++implementation Semigroup Bytes where+ (<+>) = (++)++implementation Monoid Bytes where+ neutral = empty++-- todo:+--+-- make indices Nats+-- Build a ByteString on top of Bytes?+-- migrate to (Bits 8)?+--+-- bidirectional growth?
+ test/primitives006/array.c view
@@ -0,0 +1,62 @@+#include "array.h"+#include <string.h>++int array_find(uint8_t byte, CData array, int ofs, int end)+{+ void * data = array->data + ofs;+ void * result = memchr(data, (int) byte, (size_t) (end - ofs));+ if (result == NULL)+ {+ return -1;+ }+ else+ {+ return (result - data);+ }+}++void array_realloc(int size, CData array)+{+ array->data = realloc(array->data, (size_t) size);+}++CData array_alloc(int size)+{+ return cdata_allocate((size_t) size, free);+}++uint8_t array_peek(int ofs, CData array)+{+ return ((uint8_t *) array->data)[ofs];+}++void array_poke(int ofs, uint8_t byte, CData array)+{+ ((uint8_t *) array->data)[ofs] = byte;+}++int array_peek_int(int ofs, CData array)+{+ return *((int *) (array->data + ofs));+}++void array_poke_int(int ofs, int val, CData array)+{+ *((int *) (array->data + ofs)) = val;+}++void array_copy(CData src, int src_ofs, CData dst, int dst_ofs, int count)+{+ // memmove rather than memcpy in case the areas overlap+ memmove(dst->data + dst_ofs, src->data + src_ofs, count);+}++void array_fill(int ofs, int count, uint8_t byte, CData array)+{+ memset(array->data + ofs, byte, count);+}++int array_compare(CData l, int lofs, CData r, int rofs, int count)+{+ return memcmp(l->data + lofs, r->data + rofs, count);+}
+ test/primitives006/array.h view
@@ -0,0 +1,18 @@+#pragma once++#include <stdint.h>+#include <stddef.h>++#include "idris_rts.h"+++CData array_alloc(int size);+void array_realloc(int size, CData array);+uint8_t array_peek(int ofs, CData array);+int array_peek_int(int ofs, CData array);+void array_poke(int ofs, uint8_t byte, CData array);+void array_poke_int(int ofs, int i, CData array);+void array_copy(CData src, int src_ofs, CData dst, int dst_ofs, int count);+void array_fill(int ofs, int count, uint8_t byte, CData array);+int array_compare(CData l, int lofs, CData r, int rofs, int count);+int array_find(uint8_t byte, CData array, int ofs, int end);
+ test/primitives006/expected view
@@ -0,0 +1,9 @@+1024+("01/8", (145536, 897))+("02/8", (145536, 897))+("03/8", (145536, 897))+("04/8", (145536, 897))+("05/8", (145536, 897))+("06/8", (145536, 897))+("07/8", (145536, 897))+("08/8", (145536, 897))
+ test/primitives006/load-test.idr view
@@ -0,0 +1,48 @@+module Main++import Data.Bytes as B+import Data.ByteArray as BA++-- %flag C "-g3 -ggdb -O0"+%link C "array.o"++initialBuf : Bytes+initialBuf = pack . concat $ replicate 128 block+ where+ block : List Byte+ block = [10,32,1,10,100,32,1,10,255,32,1,10,1,10,255,32,1,10,255,32,1,10,255,32,1,10]++unRLE : Bytes -> Bytes+unRLE = fst . iterateL phi (empty, Nothing)+ where+ phi : (Bytes, Maybe Byte) -> Byte -> Result (Bytes, Maybe Byte)+ phi (bs, Nothing) b = Cont (bs, Just b)+ phi (bs, Just cnt) b = Cont (bs ++ pack (replicate (cast $ prim__zextB8_Int cnt) b), Nothing)++unit : Int -> Byte -> IO ()+unit n b =+ let expanded = unRLE initialBuf+ in let elines = map (flip snoc b) (asciiLines expanded)+ in printLn $ (show b ++ "/" ++ show n, length expanded, length elines)++alloc : Int -> Int -> IO Int+alloc x 0 = return x+alloc x i = do+ -- allocate an array+ arr <- BA.allocate (64 * 1024 * 1024)+ -- write "i" at offset 63M+ BA.pokeInt (63*1024*1024) i arr+ -- read number from offset 63M+ j <- BA.peekInt (63*1024*1024) arr+ -- count matches+ alloc (x + if i == j then 1 else 0) (i - 1)++main : IO ()+main = do+ -- First allocate 1024 64M arrays to break the C heap if there's a bug+ alloc 0 1024 >>= printLn++ -- Then, test Bytes+ traverse_ (unit n . prim__truncInt_B8) [1..n]+ where+ n = 8
+ test/primitives006/run view
@@ -0,0 +1,6 @@+#!/usr/bin/env bash+${CC:-cc} -c -O2 -o array.o array.c $(${IDRIS:-idris} --include)+${IDRIS:-idris} $@ -o load-test load-test.idr --nocolour --warnreach+./load-test+rm -f load-test *.o *.ibc+find -name \*.ibc -delete
test/pruviloj001/pruviloj001.idr view
@@ -12,7 +12,7 @@ auto : Elab () auto = do compute attack- try $ repeatUntilFail intro'+ try intros hs <- map fst <$> getEnv for_ hs $ \ih => try (rewriteWith (Var ih))@@ -23,10 +23,12 @@ partial mush : Elab () mush =- do n <- gensym "j"+ do attack+ n <- gensym "j" intro n try intros ignore $ induction (Var n) `andThen` auto+ solve plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l) plusAssoc = %runElab mush