{"header":{"message":"add c-ffi-gen parser","description":null,"timestamp":"2026-06-13T19:51:41.62367671Z","authors":[{}]},"hash":"KGCNLVNLYDSCJX4HKWDNJZO5IKHXMKTSWC7FUG4AALXTKFTACA5AC","authors":[{"login":"tzemanovic","key":"2WjXWEKKcZxUNwKcbgp8p6mbzkx1SozR6nmaqfuDQgdk"}],"deps":{"hashes":[["KGCNLVNLYDSCJX4HKWDNJZO5IKHXMKTSWC7FUG4AALXTKFTACA5AC","add c-ffi-gen parser"],["AA",null],["E2AEJUMECGGGDZDGCRNX6XECOYBSJRQHG3CUHFS7Y37YBUOAOGWQC",""]],"deps":["E2AEJUMECGGGDZDGCRNX6XECOYBSJRQHG3CUHFS7Y37YBUOAOGWQC"],"known":[]},"hunks":[{"FileAdd":{"meta":{"basename":"c-ffi-gen","metadata":576},"context":[{"change":2,"pos":1}],"contents":[]}},{"FileAdd":{"meta":{"basename":"test","metadata":576},"context":[{"change":0,"pos":1}],"contents":[]}},{"FileAdd":{"meta":{"basename":"test.ipkg","metadata":0},"context":[{"change":0,"pos":24}],"contents":[{"Add":"package c-ffi-gen-test"},{"Add":"version = 0.1.0"},{"Add":"authors = \"Tom\\225\\353 Zemanovi\\269\""},{"Add":"-- maintainers ="},{"Add":"-- license ="},{"Add":"-- brief ="},{"Add":"-- readme ="},{"Add":"-- homepage ="},{"Add":"-- sourceloc ="},{"Add":"-- bugtracker ="},{"Add":""},{"Add":"-- the Idris2 version required (e.g. langversion >= 0.5.1)"},{"Add":"-- langversion"},{"Add":""},{"Add":"-- packages to add to search path"},{"Add":"depends = c-ffi-gen"},{"Add":""},{"Add":"-- modules to install"},{"Add":"-- modules ="},{"Add":""},{"Add":"-- main file (i.e. file to load at REPL)"},{"Add":"main = Main"},{"Add":""},{"Add":"-- name of executable"},{"Add":"executable = \"c-ffi-gen-test\""},{"Add":"-- opts ="},{"Add":"sourcedir = \"src\""},{"Add":"-- builddir ="},{"Add":"-- outputdir ="},{"Add":""},{"Add":"-- script to run before building"},{"Add":"-- prebuild ="},{"Add":""},{"Add":"-- script to run after building"},{"Add":"-- postbuild ="},{"Add":""},{"Add":"-- script to run after building, before installing"},{"Add":"-- preinstall ="},{"Add":""},{"Add":"-- script to run after installing"},{"Add":"-- postinstall ="},{"Add":""},{"Add":"-- script to run before cleaning"},{"Add":"-- preclean ="},{"Add":""},{"Add":"-- script to run after cleaning"},{"Add":"-- postclean ="}]}},{"FileAdd":{"meta":{"basename":"src","metadata":576},"context":[{"change":0,"pos":24}],"contents":[]}},{"FileAdd":{"meta":{"basename":"Main.idr","metadata":0},"context":[{"change":0,"pos":895}],"contents":[{"Add":"module Main"},{"Add":""},{"Add":"main : IO ()"},{"Add":"main = putStrLn \"Test successful!\""}]}},{"FileAdd":{"meta":{"basename":"src","metadata":576},"context":[{"change":0,"pos":1}],"contents":[]}},{"FileAdd":{"meta":{"basename":"Main.idr","metadata":0},"context":[{"change":0,"pos":1009}],"contents":[{"Add":"module Main"},{"Add":""},{"Add":"import Derive.Prelude"},{"Add":"import Text.FC"},{"Add":"import Text.Lex"},{"Add":"import Text.Parse"},{"Add":"import System"},{"Add":"import System.File"},{"Add":""},{"Add":"%default total"},{"Add":"%language ElabReflection"},{"Add":""},{"Add":"--------------------------------------------------------------------------------"},{"Add":"-- Lexing"},{"Add":"--------------------------------------------------------------------------------"},{"Add":""},{"Add":"data Keyword : Type where"},{"Add":" KEnum : Keyword"},{"Add":" KTypedef : Keyword"},{"Add":" KStruct : Keyword"},{"Add":" KUnion : Keyword"},{"Add":" KConst : Keyword"},{"Add":"%runElab derive \"Keyword\" [Show,Eq]"},{"Add":""},{"Add":"data CPrim : Type where"},{"Add":" CVoid : CPrim"},{"Add":" CBool : CPrim"},{"Add":" CSize : CPrim"},{"Add":" CUint8 : CPrim"},{"Add":" CUint16 : CPrim"},{"Add":" CUint32 : CPrim"},{"Add":" CUint64 : CPrim"},{"Add":" CInt8 : CPrim"},{"Add":" CInt16 : CPrim"},{"Add":" CInt32 : CPrim"},{"Add":" CInt64 : CPrim"},{"Add":"%runElab derive \"CPrim\" [Show,Eq]"},{"Add":""},{"Add":"data Token : Type where"},{"Add":" TIgnored : String -> Token"},{"Add":" TKeyword : Keyword -> Token"},{"Add":" TCPrim : CPrim -> Token"},{"Add":" TSym : Char -> Token"},{"Add":" TIntVal : Int -> Token"},{"Add":" TName : String -> Token"},{"Add":"%runElab derive \"Token\" [Show,Eq]"},{"Add":""},{"Add":"export"},{"Add":"Interpolation Token where"},{"Add":" interpolate (TIgnored x) = show x"},{"Add":" interpolate (TKeyword x) = show x"},{"Add":" interpolate (TCPrim x) = \"'\\{show x}'\""},{"Add":" interpolate (TSym x) = show x"},{"Add":" interpolate (TIntVal x) = show x"},{"Add":" interpolate (TName x) = x"},{"Add":""},{"Add":"%inline"},{"Add":"fromChar : Char -> Token"},{"Add":"fromChar = TSym"},{"Add":""},{"Add":"isIdentifierChar : Char -> Bool"},{"Add":"isIdentifierChar c = isAlpha c || isDigit c || c == '_'"},{"Add":""},{"Add":"identifier : Lexer"},{"Add":"identifier = preds isIdentifierChar"},{"Add":""},{"Add":"tokenMap : TokenMap Token"},{"Add":"tokenMap ="},{"Add":" -- Symbols - implicit conversions `fromChar`"},{"Add":" [ (is '{', const '{')"},{"Add":" , (is '}', const '}')"},{"Add":" , (is '(', const '(')"},{"Add":" , (is ')', const ')')"},{"Add":" , (is ',', const ',')"},{"Add":" , (is ';', const ';')"},{"Add":" , (is '=', const '=')"},{"Add":" , (is '*', const '*')"},{"Add":""},{"Add":" -- Keywords"},{"Add":" , (exact \"enum\", const $ TKeyword KEnum)"},{"Add":" , (exact \"typedef\", const $ TKeyword KTypedef)"},{"Add":" , (exact \"struct\", const $ TKeyword KStruct)"},{"Add":" , (exact \"union\", const $ TKeyword KUnion)"},{"Add":" , (exact \"const\", const $ TKeyword KConst)"},{"Add":""},{"Add":" -- Types"},{"Add":" , (exact \"void\", const $ TCPrim CVoid)"},{"Add":" , (exact \"bool\", const $ TCPrim CBool)"},{"Add":" , (exact \"size_t\", const $ TCPrim CSize)"},{"Add":" , (exact \"uint8_t\", const $ TCPrim CUint8)"},{"Add":" , (exact \"uint16_t\", const $ TCPrim CUint16)"},{"Add":" , (exact \"uint32_t\", const $ TCPrim CUint32)"},{"Add":" , (exact \"uint64_t\", const $ TCPrim CUint64)"},{"Add":" , (exact \"int8_t\", const $ TCPrim CInt8)"},{"Add":" , (exact \"int16_t\", const $ TCPrim CInt16)"},{"Add":" , (exact \"int32_t\", const $ TCPrim CInt32)"},{"Add":" , (exact \"int64_t\", const $ TCPrim CInt64)"},{"Add":" , (preds isDigit, TIntVal . cast {to = Int} . cast {to = String})"},{"Add":" , (identifier, TName . cast {to = String})"},{"Add":""},{"Add":" -- Ignores. These are lexed, but filtered out before parsing"},{"Add":" , (spaces, const $ TIgnored \" \")"},{"Add":" -- - ignore comments"},{"Add":" , (surround (exact \"/**\") (exact \"*/\") any, TIgnored . cast {to = String})"},{"Add":" , (surround (exact \"/*\") (exact \"*/\") (non newline), TIgnored . cast {to = String})"},{"Add":" -- - ignore include pragmas"},{"Add":" , (exact \"#include\" <+> manyTillNewline, TIgnored . cast {to = String})"},{"Add":" ]"},{"Add":""},{"Add":"tokenize : String -> Either (ParseError Void) (List $ Bounded Token)"},{"Add":"tokenize s ="},{"Add":" mapFst (toParseError Virtual s) $ lexManual (first tokenMap) s"},{"Add":""},{"Add":""},{"Add":"--------------------------------------------------------------------------------"},{"Add":"-- Parsing"},{"Add":"--------------------------------------------------------------------------------"},{"Add":""},{"Add":"data CType : Type where"},{"Add":" CTypePrim : CPrim -> CType"},{"Add":" CTypeCustom : String -> CType"},{"Add":"%runElab derive \"CType\" [Show,Eq]"},{"Add":""},{"Add":"data TypeModifier : Type where"},{"Add":" Pointer : TypeModifier"},{"Add":"%runElab derive \"TypeModifier\" [Show,Eq]"},{"Add":""},{"Add":"record Field where"},{"Add":" constructor MkField"},{"Add":" type : CType"},{"Add":" modifier : Maybe TypeModifier"},{"Add":" name : String"},{"Add":"%runElab derive \"Field\" [Show,Eq]"},{"Add":""},{"Add":"record Struct where"},{"Add":" constructor MkStruct"},{"Add":" ||| Inlined structs may be anonymous"},{"Add":" name : Maybe String"},{"Add":" fields : List1 Field"},{"Add":"%runElab derive \"Struct\" [Show,Eq]"},{"Add":""},{"Add":"record Enum where"},{"Add":" constructor MkEnum"},{"Add":" name : String"},{"Add":" -- Each case has an assigned unique int value."},{"Add":" -- This is optional in which case it's an enumeration following the"},{"Add":" -- order of declarations."},{"Add":" cases : List1 (String, Int)"},{"Add":"%runElab derive \"Enum\" [Show,Eq]"},{"Add":""},{"Add":"data UnionCase : Type where"},{"Add":" ||| Single type and name"},{"Add":" UnionCaseSingle : CType -> String -> UnionCase"},{"Add":" ||| Inlined struct"},{"Add":" UnionCaseStruct : Struct -> UnionCase"},{"Add":"%runElab derive \"UnionCase\" [Show,Eq]"},{"Add":""},{"Add":"record Union where"},{"Add":" constructor MkUnion"},{"Add":" name : String"},{"Add":" cases : List1 UnionCase"},{"Add":"%runElab derive \"Union\" [Show,Eq]"},{"Add":""},{"Add":"data TypedefType : Type where"},{"Add":" ||| C primitive type."},{"Add":" TypedefCPrim : CPrim -> TypedefType"},{"Add":" ||| Inlined union definition."},{"Add":" TypedefUnion : Union -> TypedefType"},{"Add":" ||| Inlined struct definition."},{"Add":" TypedefStructInline : Struct -> TypedefType"},{"Add":" ||| Struct alias."},{"Add":" ||| First `String` is the target name, second is the name of the typedef"},{"Add":" TypedefStructAlias : String -> TypedefType"},{"Add":" ||| Opaque pointer."},{"Add":" TypedefOpaquePointer : TypedefType"},{"Add":"%runElab derive \"TypedefType\" [Show,Eq]"},{"Add":""},{"Add":"record Typedef where"},{"Add":" constructor MkTypedef"},{"Add":" type : TypedefType"},{"Add":" name : String"},{"Add":"%runElab derive \"Typedef\" [Show,Eq]"},{"Add":""},{"Add":"record ReturnType where"},{"Add":" constructor MkReturnType"},{"Add":" type : CType"},{"Add":" modifier : Maybe TypeModifier"},{"Add":"%runElab derive \"ReturnType\" [Show,Eq]"},{"Add":""},{"Add":"record PtrArgType where"},{"Add":" constructor MkPtrArgType"},{"Add":" type : CType"},{"Add":" modifier : Maybe TypeModifier"},{"Add":"%runElab derive \"PtrArgType\" [Show,Eq]"},{"Add":""},{"Add":"data FnPtrArg: Type where"},{"Add":" FPAVoid : FnPtrArg"},{"Add":" FPAField : PtrArgType -> FnPtrArg"},{"Add":"%runElab derive \"FnPtrArg\" [Show,Eq]"},{"Add":""},{"Add":"||| Function arg that is a function pointer"},{"Add":"record FnArgFnPtr where"},{"Add":" constructor MkFnArgFnPtr"},{"Add":" returnType : ReturnType"},{"Add":" name : String"},{"Add":" args : List1 FnPtrArg"},{"Add":"%runElab derive \"FnArgFnPtr\" [Show,Eq]"},{"Add":""},{"Add":"data FnArg: Type where"},{"Add":" FAVoid : FnArg"},{"Add":" FAField : Field -> FnArg"},{"Add":" FAFnPtr : FnArgFnPtr -> FnArg"},{"Add":"%runElab derive \"FnArg\" [Show,Eq]"},{"Add":""},{"Add":"record Fn where"},{"Add":" constructor MkFn"},{"Add":" returnType : ReturnType"},{"Add":" returnTypeModifier : Maybe TypeModifier"},{"Add":" name : String"},{"Add":" args : List1 FnArg"},{"Add":"%runElab derive \"Fn\" [Show,Eq]"},{"Add":""},{"Add":"||| Only parsing typedefs, structs, enums, unions and functions. Everything else is ignored."},{"Add":"data Def : Type where"},{"Add":" DTypedef : Typedef -> Def"},{"Add":" DStruct : Struct -> Def"},{"Add":" DEnum : Enum -> Def"},{"Add":" DUnion : Union -> Def"},{"Add":" DFn : Fn -> Def"},{"Add":"%runElab derive \"Def\" [Show,Eq]"},{"Add":""},{"Add":"Defs : Type"},{"Add":"Defs = List1 Def"},{"Add":""},{"Add":"public export"},{"Add":"data ParseErr : Type where"},{"Add":" ExpectedString : ParseErr"},{"Add":"%runElab derive \"ParseErr\" [Show,Eq]"},{"Add":""},{"Add":"export"},{"Add":"Interpolation ParseErr where"},{"Add":" interpolate ExpectedString = \"Expected string literal\""},{"Add":""},{"Add":"0 Rule : Bool -> Type -> Type"},{"Add":"Rule b t = Grammar b () Token ParseErr t"},{"Add":""},{"Add":"ignored : Rule True ()"},{"Add":"ignored = terminal $ \\case (TIgnored _) => Just (); _ => Nothing"},{"Add":""},{"Add":"name : Rule True String"},{"Add":"name = terminal $ \\case (TName name) => Just name; _ => Nothing"},{"Add":""},{"Add":"cPrim : Rule True CPrim"},{"Add":"cPrim = terminal $ \\case (TCPrim prim) => Just prim; _ => Nothing"},{"Add":""},{"Add":"cType : Rule True CType"},{"Add":"cType = (CTypePrim <$> cPrim) <|> (CTypeCustom <$> name)"},{"Add":""},{"Add":"intValue : Rule True Int"},{"Add":"intValue = terminal $ \\case (TIntVal val) => Just val; _ => Nothing"},{"Add":""},{"Add":"constKeyword : Rule True ()"},{"Add":"constKeyword = terminal $ \\case TKeyword KConst => Just (); _ => Nothing"},{"Add":""},{"Add":"unionKeyword : Rule True ()"},{"Add":"unionKeyword = terminal $ \\case TKeyword KUnion => Just (); _ => Nothing"},{"Add":""},{"Add":"structKeyword : Rule True ()"},{"Add":"structKeyword = terminal $ \\case TKeyword KStruct => Just (); _ => Nothing"},{"Add":""},{"Add":"typeModifier : Rule False (Maybe TypeModifier)"},{"Add":"typeModifier = optional (const Pointer <$> is '*')"},{"Add":""},{"Add":"field : Rule True Field"},{"Add":"field = MkField"},{"Add":" <$> ("},{"Add":" optional constKeyword *>"},{"Add":" (optional ("},{"Add":" -- Fields using union type are prefixed with \"union\""},{"Add":" unionKeyword"},{"Add":" -- Fields using struct type are prefixed with \"struct\""},{"Add":" <|> structKeyword"},{"Add":" ))"},{"Add":" *> cType"},{"Add":" )"},{"Add":" <*> typeModifier"},{"Add":" <*> name"},{"Add":""},{"Add":"struct : Rule True Struct"},{"Add":"struct ="},{"Add":" (const MkStruct <$> structKeyword)"},{"Add":" <*> (optional name)"},{"Add":" <*> (between (is '{') (is '}') (endBy1 (is ';') field))"},{"Add":""},{"Add":"unionCase : Rule True UnionCase"},{"Add":"unionCase ="},{"Add":" (UnionCaseStruct <$> struct) <|> (UnionCaseSingle <$> cType <*> name)"},{"Add":""},{"Add":"union : Rule True Union"},{"Add":"union ="},{"Add":" (const MkUnion <$> unionKeyword)"},{"Add":" <*> name"},{"Add":" <*> (between (is '{') (is '}') (endBy1 (is ';') unionCase))"},{"Add":""},{"Add":"typedefExtStruct : Rule True String"},{"Add":"typedefExtStruct ="},{"Add":" structKeyword *> name"},{"Add":""},{"Add":"data TypedefStructKind : Type where"},{"Add":" TSKInline : List1 Field -> TypedefStructKind"},{"Add":" TSKAlias : TypedefStructKind"},{"Add":""},{"Add":"typedefStruct : Rule True TypedefType"},{"Add":"typedefStruct ="},{"Add":" conv <$>"},{"Add":" (structKeyword *> name)"},{"Add":" <*> ("},{"Add":" (TSKInline <$>"},{"Add":" (between (is '{') (is '}') (endBy1 (is ';') field))"},{"Add":" )"},{"Add":" <|> (pure TSKAlias)"},{"Add":" )"},{"Add":" where"},{"Add":" conv : String -> TypedefStructKind -> TypedefType"},{"Add":" conv aName kind = case kind of"},{"Add":" TSKInline fields => TypedefStructInline $ MkStruct (Just aName) fields"},{"Add":" TSKAlias => TypedefStructAlias aName"},{"Add":""},{"Add":"typedefOpaquePointer : Rule True TypedefType"},{"Add":"typedefOpaquePointer = const TypedefOpaquePointer <$> (name <* (is '*'))"},{"Add":""},{"Add":"typedefType : Rule True TypedefType"},{"Add":"typedefType ="},{"Add":" (TypedefCPrim <$> cPrim)"},{"Add":" <|> (TypedefUnion <$> union)"},{"Add":" <|> typedefStruct"},{"Add":" <|> typedefOpaquePointer"},{"Add":""},{"Add":"typedef : Rule True Def"},{"Add":"typedef = DTypedef <$>"},{"Add":" ( (terminal $ \\case"},{"Add":" TKeyword KTypedef => Just MkTypedef"},{"Add":" _ => Nothing)"},{"Add":" <*> typedefType"},{"Add":" <*> name"},{"Add":" <* (is ';')"},{"Add":" )"},{"Add":""},{"Add":"-- Assign int value if missing following the order of the list"},{"Add":"enumerate : List1 (a, Maybe Int) -> List1 (a, Int)"},{"Add":"enumerate list ="},{"Add":" let"},{"Add":" len = length list"},{"Add":" ixs = 0 ::: iterateN (pred len) (\\n => n + 1) 1"},{"Add":" in zipWith (\\(a, maybeN), n => (a, maybe n id maybeN)) list ixs"},{"Add":""},{"Add":"enum : Rule True Def"},{"Add":"enum = DEnum <$>"},{"Add":" ((terminal $ \\case"},{"Add":" (TKeyword KEnum) => Just MkEnum"},{"Add":" _ => Nothing)"},{"Add":" <*> name"},{"Add":" <*> ("},{"Add":" enumerate <$> between (is '{') (is '}')"},{"Add":" (endBy1 (is ',')"},{"Add":" -- A case name with an optional value assignment"},{"Add":" (MkPair <$> name <*> (optional ((is '=') *> intValue)))"},{"Add":" )"},{"Add":" )"},{"Add":" <* (is ';')"},{"Add":" )"},{"Add":""},{"Add":"structDef : Rule True Def"},{"Add":"structDef = DStruct <$> struct"},{"Add":""},{"Add":"unionDef : Rule True Def"},{"Add":"unionDef = DUnion <$> union"},{"Add":""},{"Add":"returnType : Rule True ReturnType"},{"Add":"returnType = MkReturnType"},{"Add":" <$> ("},{"Add":" -- optional constKeyword *>"},{"Add":" (optional ("},{"Add":" unionKeyword"},{"Add":" <|> structKeyword"},{"Add":" ))"},{"Add":" *> cType"},{"Add":" )"},{"Add":" <*> typeModifier"},{"Add":""},{"Add":"void : Rule True ()"},{"Add":"void = is (TCPrim CVoid)"},{"Add":""},{"Add":"fnPtrArgType : Rule True PtrArgType"},{"Add":"fnPtrArgType = MkPtrArgType"},{"Add":" <$> ("},{"Add":" optional constKeyword *>"},{"Add":" (optional ("},{"Add":" -- Types using union type are prefixed with \"union\""},{"Add":" unionKeyword"},{"Add":" -- Types using struct type are prefixed with \"struct\""},{"Add":" <|> structKeyword"},{"Add":" ))"},{"Add":" *> cType"},{"Add":" )"},{"Add":" <*> typeModifier"},{"Add":""},{"Add":"fnPtrArg : Rule True FnPtrArg"},{"Add":"fnPtrArg ="},{"Add":" (const FPAVoid <$> void)"},{"Add":" <|> (FPAField <$> fnPtrArgType)"},{"Add":""},{"Add":"data FnArgKind : Type where"},{"Add":" FAKField : String -> FnArgKind"},{"Add":" FAKFnPtr : String -> List1 FnPtrArg -> FnArgKind"},{"Add":""},{"Add":"fnArg : Rule True FnArg"},{"Add":"fnArg ="},{"Add":" (const FAVoid <$> void)"},{"Add":" <|> (conv <$> ("},{"Add":" optional constKeyword *>"},{"Add":" (optional ("},{"Add":" -- Fields using union type are prefixed with \"union\""},{"Add":" unionKeyword"},{"Add":" -- Fields using struct type are prefixed with \"struct\""},{"Add":" <|> structKeyword"},{"Add":" ))"},{"Add":" *> cType"},{"Add":" )"},{"Add":" <*> typeModifier"},{"Add":" <*> ("},{"Add":" (FAKField <$> name)"},{"Add":" <|> ((FAKFnPtr <$>"},{"Add":" (between (is '(') (is ')') (is '*' *> name)))"},{"Add":" <*> (between (is '(') (is ')') (sepBy1 (is ',') fnPtrArg))"},{"Add":" )"},{"Add":" )"},{"Add":" )"},{"Add":" where"},{"Add":" conv : CType -> Maybe TypeModifier -> FnArgKind -> FnArg"},{"Add":" conv cType modifier kind = case kind of"},{"Add":" FAKField name => FAField $ MkField cType modifier name"},{"Add":" FAKFnPtr name args => FAFnPtr $ MkFnArgFnPtr (MkReturnType cType modifier) name args"},{"Add":""},{"Add":"fnArgs : Rule True (List1 FnArg)"},{"Add":"fnArgs ="},{"Add":" (between (is '(') (is ')')"},{"Add":" (sepBy1 (is ',') fnArg)"},{"Add":" )"},{"Add":""},{"Add":"fn : Rule True Def"},{"Add":"fn = DFn <$>"},{"Add":" ((MkFn <$> returnType)"},{"Add":" <*> typeModifier"},{"Add":" <*> name"},{"Add":" <*> fnArgs"},{"Add":" <* (is ';')"},{"Add":" )"},{"Add":""},{"Add":"def : Rule True Def"},{"Add":"def = typedef <|> fn <|> structDef <|> enum <|> unionDef"},{"Add":""},{"Add":"-- `Defs` parser"},{"Add":"defs : Rule True Defs"},{"Add":"defs = afterMany ignored $ some def"},{"Add":""},{"Add":"parse : String -> Either (List1 (ParseError ParseErr)) Defs"},{"Add":"parse s = case tokenize s of"},{"Add":" Left err => Left (singleton $ {error $= fromVoid} err)"},{"Add":"-- TODO filter out ignored tokens"},{"Add":" Right toks =>"},{"Add":" let toks = filter ((\\case TIgnored _ => False; _ => True) . val) toks"},{"Add":" in case parse defs () toks of"},{"Add":" Left es => Left (toParseError Virtual s <$> es)"},{"Add":" Right ((),res,[]) => Right res"},{"Add":" Right ((),res,(x::xs)) =>"},{"Add":" Left (singleton $ toParseError Virtual s $ Expected [] . interpolate <$> x)"},{"Add":""},{"Add":"--------------------------------------------------------------------------------"},{"Add":"-- CLI"},{"Add":"--------------------------------------------------------------------------------"},{"Add":""},{"Add":"lexAndPrint : String -> IO ()"},{"Add":"lexAndPrint s = putStrLn $ either interpolate show (tokenize s)"},{"Add":""},{"Add":"parseAndPrint : String -> IO ()"},{"Add":"parseAndPrint s ="},{"Add":" case parse s of"},{"Add":" Left xs => traverse_ (putStrLn . interpolate) xs"},{"Add":" Right v => printLn v"},{"Add":""},{"Add":"main : IO ()"},{"Add":"main = do"},{"Add":" Right input <- assert_total $ fRead stdin"},{"Add":" | Left err => do"},{"Add":" ignore $ fPutStrLn stderr $ \"Error: Expected input from stdin, failed with: \" ++ show err"},{"Add":" exitWith (ExitFailure 1)"},{"Add":" -- lexAndPrint input"},{"Add":" parseAndPrint input"}]}},{"FileAdd":{"meta":{"basename":"pack.toml","metadata":0},"context":[{"change":0,"pos":1}],"contents":[{"Add":"[custom.all.c-ffi-gen]"},{"Add":"type = \"local\""},{"Add":"path = \".\""},{"Add":"ipkg = \"c-ffi-gen.ipkg\""},{"Add":"test = \"test/test.ipkg\""},{"Add":""},{"Add":"[custom.all.c-ffi-gen-test]"},{"Add":"type = \"local\""},{"Add":"path = \"test\""},{"Add":"ipkg = \"test.ipkg\""}]}},{"FileAdd":{"meta":{"basename":"c-ffi-gen.ipkg","metadata":0},"context":[{"change":0,"pos":1}],"contents":[{"Add":"package c-ffi-gen"},{"Add":"version = 0.1.0"},{"Add":"authors = \"Tomáš Zemanovič\""},{"Add":"-- maintainers ="},{"Add":"license = \"BSD-3-Clause\""},{"Add":"brief = \"Generate Idris C FFI code from a C header file\""},{"Add":"-- readme ="},{"Add":"-- homepage ="},{"Add":"-- sourceloc ="},{"Add":"-- bugtracker ="},{"Add":""},{"Add":"-- the Idris2 version required (e.g. langversion >= 0.5.1)"},{"Add":"-- langversion"},{"Add":""},{"Add":"-- packages to add to search path"},{"Add":"depends"},{"Add":" = elab-util"},{"Add":" , parser"},{"Add":""},{"Add":"-- modules to install"},{"Add":"-- modules ="},{"Add":""},{"Add":"-- main file (i.e. file to load at REPL)"},{"Add":"main = Main"},{"Add":""},{"Add":"-- name of executable"},{"Add":"executable = \"c-ffi-gen\""},{"Add":"-- opts ="},{"Add":"sourcedir = \"src\""},{"Add":"-- builddir ="},{"Add":"-- outputdir ="},{"Add":""},{"Add":"-- script to run before building"},{"Add":"-- prebuild ="},{"Add":""},{"Add":"-- script to run after building"},{"Add":"-- postbuild ="},{"Add":""},{"Add":"-- script to run after building, before installing"},{"Add":"-- preinstall ="},{"Add":""},{"Add":"-- script to run after installing"},{"Add":"-- postinstall ="},{"Add":""},{"Add":"-- script to run before cleaning"},{"Add":"-- preclean ="},{"Add":""},{"Add":"-- script to run after cleaning"},{"Add":"-- postclean ="}]}}],"owner":"tzemanovic","repo":"idris2-window","token":"tFmoZQaseznEEOWJrvmuPtAYqqwUOyd8kMXS0MeJ5gk=","login":null}

…

Dependencies

Change contents