Theory C_Ast
chapter ‹Annex I: The Commented Sources of Isabelle/C›
section ‹Core Language: An Abstract Syntax Tree Definition (C Language without Annotations)›
theory C_Ast
imports Main
begin
subsection ‹Loading the Generated AST›
text ‹ The abstract syntax tree of the C language considered in the Isabelle/C project is
arbitrary, but it must already come with a grammar making the connection with a default AST, so that
both the grammar and AST can be imported to SML.⁋‹Additionally, the grammar and AST
must both have a free licence --- compatible with the Isabelle AFP, for them to be publishable
there.› The Haskell Language.C project fulfills this property: see for instance
🌐‹http://hackage.haskell.org/package/language-c› and
🌐‹https://github.com/visq/language-c/blob/master/src/Language/C/Syntax/AST.hs›,
where its AST is being imported in the present theory file 🗏‹C_Ast.thy›, whereas
its grammar will be later in 🗏‹C_Parser_Language.thy›
(🗏‹C_Parser_Language.thy› depends on 🗏‹C_Ast.thy›). The AST
importation is based on a modified version of Haskabelle, which generates the C AST from Haskell to
an ML file. ›
ML ‹
val fresh_ident0 =
let val i = Synchronized.var "counter for new identifier" 38 in
fn () => Int.toString (Synchronized.change_result i (fn i => (i, i + 1)))
end
›
ML
‹
structure CodeType = struct
type mlInt = string
type 'a mlMonad = 'a option
end
structure CodeConst = struct
structure Monad = struct
val bind = fn
NONE => (fn _ => NONE)
| SOME a => fn f => f a
val return = SOME
end
structure Printf = struct
local
fun sprintf s l =
case String.fields (fn #"%" => true | _ => false) s of
[] => ""
| [x] => x
| x :: xs =>
let fun aux acc l_pat l_s =
case l_pat of
[] => rev acc
| x :: xs => aux (String.extract (x, 1, NONE) :: hd l_s :: acc) xs (tl l_s) in
String.concat (x :: aux [] xs l)
end
in
fun sprintf0 s_pat = s_pat
fun sprintf1 s_pat s1 = sprintf s_pat [s1]
fun sprintf2 s_pat s1 s2 = sprintf s_pat [s1, s2]
fun sprintf3 s_pat s1 s2 s3 = sprintf s_pat [s1, s2, s3]
fun sprintf4 s_pat s1 s2 s3 s4 = sprintf s_pat [s1, s2, s3, s4]
fun sprintf5 s_pat s1 s2 s3 s4 s5 = sprintf s_pat [s1, s2, s3, s4, s5]
end
end
structure String = struct
val concat = String.concatWith
end
structure Sys = struct
val isDirectory2 = SOME o File.is_dir o Path.explode handle ERROR _ => K NONE
end
structure To = struct
fun nat f = Int.toString o f
end
fun outFile1 _ _ = tap (fn _ => warning "not implemented") NONE
fun outStand1 f = outFile1 f ""
end
›
ML_file ‹../generated/c_ast.ML›
text ‹ Note that the purpose of 🗀‹../generated› is to host any generated
files of the Isabelle/C project. It contains among others:
▪ 🗏‹../generated/c_ast.ML› representing the Abstract Syntax Tree of C,
which has just been loaded.
▪ 🗏‹../generated/c_grammar_fun.grm› is a generated file not used by the
project, except for further generating 🗏‹../generated/c_grammar_fun.grm.sig›
and 🗏‹../generated/c_grammar_fun.grm.sml›. Its physical presence in the
directory is actually not necessary, but has been kept for informative documentation purposes. It
represents the basis point of our SML grammar file, generated by an initial Haskell grammar file
(namely
🌐‹https://github.com/visq/language-c/blob/master/src/Language/C/Parser/Parser.y›)
using a modified version of Happy.
▪ 🗏‹../generated/c_grammar_fun.grm.sig› and
🗏‹../generated/c_grammar_fun.grm.sml› are the two files generated from
🗏‹../generated/c_grammar_fun.grm› with a modified version of ML-Yacc. This
last comes from MLton source in 🗀‹../../src_ext/mlton›, see for example
🗀‹../../src_ext/mlton/mlyacc›.
›
text ‹ For the case of 🗏‹../generated/c_ast.ML›, it is actually not
mandatory to have a ``physical'' representation of the file in 🗀‹../generated›:
it could be generated ``on-the-fly'' with ⬚‹code_reflect› and immediately
loaded: Citadelle has an option to choose between the two
tasks~\cite{DBLP:journals/afp/TuongW15}.⁋‹🌐‹https://gitlab.lisn.upsaclay.fr/frederictuong/isabelle_contrib/-/tree/master/Citadelle/src/compiler›››
text ‹ After loading the AST, it is possible in Citadelle to do various meta-programming
renaming, such as the one depicted in the next command. Actually, its content is explicitly included
here by hand since we decided to manually load the AST using the above
⬚‹ML_file› command. (Otherwise, one can automatically execute the overall
generation and renaming tasks in Citadelle without resorting to a manual copying-pasting.)›
ML ‹
structure C_Ast =
struct
val Position = C_Ast.position
val NoPosition = C_Ast.noPosition
val BuiltinPosition = C_Ast.builtinPosition
val InternalPosition = C_Ast.internalPosition
val Name = C_Ast.name
val OnlyPos = C_Ast.onlyPos
val NodeInfo = C_Ast.nodeInfo
val AnonymousRef = C_Ast.anonymousRef
val NamedRef = C_Ast.namedRef
val CChar = C_Ast.cChar val CChars = C_Ast.cChars
val DecRepr = C_Ast.decRepr val HexRepr = C_Ast.hexRepr
val OctalRepr = C_Ast.octalRepr
val FlagUnsigned = C_Ast.flagUnsigned
val FlagLong = C_Ast.flagLong
val FlagLongLong = C_Ast.flagLongLong
val FlagImag = C_Ast.flagImag
val CFloat = C_Ast.cFloat
val Flags = C_Ast.flags
val CInteger = C_Ast.cInteger
val CAssignOp = C_Ast.cAssignOp
val CMulAssOp = C_Ast.cMulAssOp
val CDivAssOp = C_Ast.cDivAssOp
val CRmdAssOp = C_Ast.cRmdAssOp
val CAddAssOp = C_Ast.cAddAssOp
val CSubAssOp = C_Ast.cSubAssOp
val CShlAssOp = C_Ast.cShlAssOp
val CShrAssOp = C_Ast.cShrAssOp
val CAndAssOp = C_Ast.cAndAssOp
val CXorAssOp = C_Ast.cXorAssOp
val COrAssOp = C_Ast.cOrAssOp
val CMulOp = C_Ast.cMulOp
val CDivOp = C_Ast.cDivOp
val CRmdOp = C_Ast.cRmdOp
val CAddOp = C_Ast.cAddOp
val CSubOp = C_Ast.cSubOp
val CShlOp = C_Ast.cShlOp
val CShrOp = C_Ast.cShrOp
val CLeOp = C_Ast.cLeOp
val CGrOp = C_Ast.cGrOp
val CLeqOp = C_Ast.cLeqOp
val CGeqOp = C_Ast.cGeqOp
val CEqOp = C_Ast.cEqOp
val CNeqOp = C_Ast.cNeqOp
val CAndOp = C_Ast.cAndOp
val CXorOp = C_Ast.cXorOp
val COrOp = C_Ast.cOrOp
val CLndOp = C_Ast.cLndOp
val CLorOp = C_Ast.cLorOp
val CPreIncOp = C_Ast.cPreIncOp
val CPreDecOp = C_Ast.cPreDecOp
val CPostIncOp = C_Ast.cPostIncOp
val CPostDecOp = C_Ast.cPostDecOp
val CAdrOp = C_Ast.cAdrOp
val CIndOp = C_Ast.cIndOp
val CPlusOp = C_Ast.cPlusOp
val CMinOp = C_Ast.cMinOp
val CCompOp = C_Ast.cCompOp
val CNegOp = C_Ast.cNegOp
val CAuto = C_Ast.cAuto
val CRegister = C_Ast.cRegister
val CStatic = C_Ast.cStatic
val CExtern = C_Ast.cExtern
val CTypedef = C_Ast.cTypedef
val CThread = C_Ast.cThread
val CInlineQual = C_Ast.cInlineQual
val CNoreturnQual = C_Ast.cNoreturnQual
val CStructTag = C_Ast.cStructTag
val CUnionTag = C_Ast.cUnionTag
val CIntConst = C_Ast.cIntConst
val CCharConst = C_Ast.cCharConst
val CFloatConst = C_Ast.cFloatConst
val CStrConst = C_Ast.cStrConst
val CStrLit = C_Ast.cStrLit
val CFunDef = C_Ast.cFunDef
val CDecl = C_Ast.cDecl
val CStaticAssert = C_Ast.cStaticAssert
val CDeclr = C_Ast.cDeclr
val CPtrDeclr = C_Ast.cPtrDeclr
val CArrDeclr = C_Ast.cArrDeclr
val CFunDeclr = C_Ast.cFunDeclr
val CNoArrSize = C_Ast.cNoArrSize
val CArrSize = C_Ast.cArrSize
val CLabel = C_Ast.cLabel
val CCase = C_Ast.cCase
val CCases = C_Ast.cCases
val CDefault = C_Ast.cDefault
val CExpr = C_Ast.cExpr
val CCompound = C_Ast.cCompound
val CIf = C_Ast.cIf
val CSwitch = C_Ast.cSwitch
val CWhile = C_Ast.cWhile
val CFor = C_Ast.cFor
val CGoto = C_Ast.cGoto
val CGotoPtr = C_Ast.cGotoPtr
val CCont = C_Ast.cCont
val CBreak = C_Ast.cBreak
val CReturn = C_Ast.cReturn
val CAsm = C_Ast.cAsm
val CAsmStmt = C_Ast.cAsmStmt
val CAsmOperand = C_Ast.cAsmOperand
val CBlockStmt = C_Ast.cBlockStmt
val CBlockDecl = C_Ast.cBlockDecl
val CNestedFunDef = C_Ast.cNestedFunDef
val CStorageSpec = C_Ast.cStorageSpec
val CTypeSpec = C_Ast.cTypeSpec
val CTypeQual = C_Ast.cTypeQual
val CFunSpec = C_Ast.cFunSpec
val CAlignSpec = C_Ast.cAlignSpec
val CVoidType = C_Ast.cVoidType
val CCharType = C_Ast.cCharType
val CShortType = C_Ast.cShortType
val CIntType = C_Ast.cIntType
val CLongType = C_Ast.cLongType
val CFloatType = C_Ast.cFloatType
val CDoubleType = C_Ast.cDoubleType
val CSignedType = C_Ast.cSignedType
val CUnsigType = C_Ast.cUnsigType
val CBoolType = C_Ast.cBoolType
val CComplexType = C_Ast.cComplexType
val CInt128Type = C_Ast.cInt128Type
val CSUType = C_Ast.cSUType
val CEnumType = C_Ast.cEnumType
val CTypeDef = C_Ast.cTypeDef
val CTypeOfExpr = C_Ast.cTypeOfExpr
val CTypeOfType = C_Ast.cTypeOfType
val CAtomicType = C_Ast.cAtomicType
val CConstQual = C_Ast.cConstQual
val CVolatQual = C_Ast.cVolatQual
val CRestrQual = C_Ast.cRestrQual
val CAtomicQual = C_Ast.cAtomicQual
val CAttrQual = C_Ast.cAttrQual
val CNullableQual = C_Ast.cNullableQual
val CNonnullQual = C_Ast.cNonnullQual
val CAlignAsType = C_Ast.cAlignAsType
val CAlignAsExpr = C_Ast.cAlignAsExpr
val CStruct = C_Ast.cStruct
val CEnum = C_Ast.cEnum
val CInitExpr = C_Ast.cInitExpr
val CInitList = C_Ast.cInitList
val CArrDesig = C_Ast.cArrDesig
val CMemberDesig = C_Ast.cMemberDesig
val CRangeDesig = C_Ast.cRangeDesig
val CAttr = C_Ast.cAttr
val CComma = C_Ast.cComma
val CAssign = C_Ast.cAssign
val CCond = C_Ast.cCond
val CBinary = C_Ast.cBinary
val CCast = C_Ast.cCast
val CUnary = C_Ast.cUnary
val CSizeofExpr = C_Ast.cSizeofExpr
val CSizeofType = C_Ast.cSizeofType
val CAlignofExpr = C_Ast.cAlignofExpr
val CAlignofType = C_Ast.cAlignofType
val CComplexReal = C_Ast.cComplexReal
val CComplexImag = C_Ast.cComplexImag
val CIndex = C_Ast.cIndex
val CCall = C_Ast.cCall
val CMember = C_Ast.cMember
val CVar = C_Ast.cVar
val CConst = C_Ast.cConst
val CCompoundLit = C_Ast.cCompoundLit
val CGenericSelection = C_Ast.cGenericSelection
val CStatExpr = C_Ast.cStatExpr
val CLabAddrExpr = C_Ast.cLabAddrExpr
val CBuiltinExpr = C_Ast.cBuiltinExpr
val CBuiltinVaArg = C_Ast.cBuiltinVaArg
val CBuiltinOffsetOf = C_Ast.cBuiltinOffsetOf
val CBuiltinTypesCompatible = C_Ast.cBuiltinTypesCompatible
val CDeclExt = C_Ast.cDeclExt
val CFDefExt = C_Ast.cFDefExt
val CAsmExt = C_Ast.cAsmExt
val CTranslUnit = C_Ast.cTranslUnit
open C_Ast
end
›
subsection ‹Basic Aliases and Initialization of the Haskell Library›
ML ‹
structure C_Ast =
struct
type class_Pos = Position.T * Position.T
type NodeInfo = C_Ast.nodeInfo
type CStorageSpec = NodeInfo C_Ast.cStorageSpecifier
type CFunSpec = NodeInfo C_Ast.cFunctionSpecifier
type CConst = NodeInfo C_Ast.cConstant
type 'a CInitializerList = ('a C_Ast.cPartDesignator List.list * 'a C_Ast.cInitializer) List.list
type CTranslUnit = NodeInfo C_Ast.cTranslationUnit
type CExtDecl = NodeInfo C_Ast.cExternalDeclaration
type CFunDef = NodeInfo C_Ast.cFunctionDef
type CDecl = NodeInfo C_Ast.cDeclaration
type CDeclr = NodeInfo C_Ast.cDeclarator
type CDerivedDeclr = NodeInfo C_Ast.cDerivedDeclarator
type CArrSize = NodeInfo C_Ast.cArraySize
type CStat = NodeInfo C_Ast.cStatement
type CAsmStmt = NodeInfo C_Ast.cAssemblyStatement
type CAsmOperand = NodeInfo C_Ast.cAssemblyOperand
type CBlockItem = NodeInfo C_Ast.cCompoundBlockItem
type CDeclSpec = NodeInfo C_Ast.cDeclarationSpecifier
type CTypeSpec = NodeInfo C_Ast.cTypeSpecifier
type CTypeQual = NodeInfo C_Ast.cTypeQualifier
type CAlignSpec = NodeInfo C_Ast.cAlignmentSpecifier
type CStructUnion = NodeInfo C_Ast.cStructureUnion
type CEnum = NodeInfo C_Ast.cEnumeration
type CInit = NodeInfo C_Ast.cInitializer
type CInitList = NodeInfo CInitializerList
type CDesignator = NodeInfo C_Ast.cPartDesignator
type CAttr = NodeInfo C_Ast.cAttribute
type CExpr = NodeInfo C_Ast.cExpression
type CBuiltin = NodeInfo C_Ast.cBuiltinThing
type CStrLit = NodeInfo C_Ast.cStringLiteral
type ClangCVersion = C_Ast.clangCVersion
type Ident = C_Ast.ident
type Position = C_Ast.positiona
type PosLength = Position * int
type Name = C_Ast.namea
type Bool = bool
type CString = C_Ast.cString
type CChar = C_Ast.cChar
type CInteger = C_Ast.cInteger
type CFloat = C_Ast.cFloat
type CStructTag = C_Ast.cStructTag
type CUnaryOp = C_Ast.cUnaryOp
type 'a CStringLiteral = 'a C_Ast.cStringLiteral
type 'a CConstant = 'a C_Ast.cConstant
type ('a, 'b) Either = ('a, 'b) C_Ast.either
type CIntRepr = C_Ast.cIntRepr
type CIntFlag = C_Ast.cIntFlag
type CAssignOp = C_Ast.cAssignOp
type Comment = C_Ast.comment
type 'a Reversed = 'a
datatype CDeclrR = CDeclrR0 of C_Ast.ident C_Ast.optiona
* NodeInfo C_Ast.cDerivedDeclarator list Reversed
* NodeInfo C_Ast.cStringLiteral C_Ast.optiona
* NodeInfo C_Ast.cAttribute list
* NodeInfo
type 'a Maybe = 'a C_Ast.optiona
datatype 'a Located = Located of 'a * (Position * (Position * int))
fun CDeclrR ide l s a n = CDeclrR0 (ide, l, s, a, n)
val reverse = rev
val Nothing = C_Ast.None
val Just = C_Ast.Some
val False = false
val True = true
val Ident = C_Ast.Ident0
val CDecl_flat = fn l1 => C_Ast.CDecl l1 o map (fn (a, b, c) => ((a, b), c))
fun flat3 (a, b, c) = ((a, b), c)
fun maybe def f = fn C_Ast.None => def | C_Ast.Some x => f x
val Reversed = I
val From_string =
C_Ast.SS_base
o C_Ast.ST
o implode
o map (fn s =>
if Symbol.is_char s then s
else if Symbol.is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s
else s)
o Symbol.explode
val From_char_hd = hd o C_Ast.explode
val Namea = C_Ast.name
open C_Ast
fun flip f b a = f a b
open Basic_Library
end
›
section‹A General C11-AST iterator.›
ML‹val ABR_STRING_SPY = Unsynchronized.ref (C_Ast.SS_base(C_Ast.ST ""));›
ML‹
signature C11_AST_LIB =
sig
val fold_either: ('a -> 'b -> 'c) -> ('d -> 'b -> 'c) -> ('a, 'd) C_Ast.either -> 'b -> 'c
val fold_optiona: ('a -> 'b -> 'b) -> 'a C_Ast.optiona -> 'b -> 'b
datatype data = data_bool of bool | data_int of int
| data_string of string | data_absstring of string
| data_nodeInfo of C_Ast.nodeInfo
type node_content = { tag : string,
sub_tag : string,
args : data list }
val toString_cBinaryOp : C_Ast.cBinaryOp -> string
val toString_cIntFlag : C_Ast.cIntFlag -> string
val toString_cIntRepr : C_Ast.cIntRepr -> string
val toString_cUnaryOp : C_Ast.cUnaryOp -> string
val toString_cAssignOp : C_Ast.cAssignOp -> string
val toString_abr_string: C_Ast.abr_string -> string
val toString_abr_string_2: C_Ast.abr_string -> string
val toPos_positiona : C_Ast.positiona -> Position.T list
val decode_positions : string -> Position.T list
val encode_positions : Position.T list -> string
val toString_nodeinfo : C_Ast.nodeInfo -> string
val toString_node_content : node_content -> string
val id_of_node_content : node_content -> string
val get_abr_string_from_Ident_string:string -> C_Ast.abr_string
val fold_ident: 'a -> (node_content -> 'a -> 'b -> 'c) -> C_Ast.ident -> 'b -> 'c
val fold_cInteger: (node_content -> 'a -> 'b) -> C_Ast.cInteger -> 'a -> 'b
val fold_cConstant: (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cConstant -> 'b -> 'b
val fold_cStringLiteral: (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cStringLiteral -> 'b -> 'b
val fold_cArraySize: 'a -> ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cArraySize -> 'b -> 'b
val fold_cAttribute: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cAttribute -> 'b -> 'b
val fold_cBuiltinThing: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cBuiltinThing -> 'b -> 'b
val fold_cCompoundBlockItem: 'a -> ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b)
-> 'a C_Ast.cCompoundBlockItem -> 'b -> 'b
val fold_cDeclaration: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cDeclaration -> 'b -> 'b
val fold_cDeclarationSpecifier: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b)
-> 'a C_Ast.cDeclarationSpecifier -> 'b -> 'b
val fold_cDeclarator: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cDeclarator -> 'b -> 'b
val fold_cDerivedDeclarator: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b)
-> 'a C_Ast.cDerivedDeclarator -> 'b -> 'b
val fold_cEnumeration: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cEnumeration -> 'b -> 'b
val fold_cExpression: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cExpression -> 'b -> 'b
val fold_cInitializer: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cInitializer -> 'b -> 'b
val fold_cPartDesignator: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cPartDesignator -> 'b -> 'b
val fold_cStatement: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cStatement -> 'b -> 'b
val fold_cStructureUnion : ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cStructureUnion -> 'b -> 'b
val fold_cTypeQualifier: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cTypeQualifier -> 'b -> 'b
val fold_cTypeSpecifier: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cTypeSpecifier -> 'b -> 'b
val fold_cExternalDeclaration: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cExternalDeclaration -> 'b -> 'b
val fold_cTranslationUnit: ('b -> 'b -> 'b) -> (node_content -> 'a -> 'b -> 'b) -> 'a C_Ast.cTranslationUnit -> 'b -> 'b
datatype 'a C11_Ast =
mk_cInteger of C_Ast.cInteger
| mk_cConstant of 'a C_Ast.cConstant
| mk_cStringLiteral of 'a C_Ast.cStringLiteral
| mk_cArraySize of 'a C_Ast.cArraySize
| mk_cAttribute of 'a C_Ast.cAttribute
| mk_cBuiltinThing of 'a C_Ast.cBuiltinThing
| mk_cCompoundBlockItem of 'a C_Ast.cCompoundBlockItem
| mk_cDeclaration of 'a C_Ast.cDeclaration
| mk_cDeclarationSpecifier of 'a C_Ast.cDeclarationSpecifier
| mk_cDeclarator of 'a C_Ast.cDeclarator
| mk_cDerivedDeclarator of 'a C_Ast.cDerivedDeclarator
| mk_cEnumeration of 'a C_Ast.cEnumeration
| mk_cExpression of 'a C_Ast.cExpression
| mk_cInitializer of 'a C_Ast.cInitializer
| mk_cPartDesignator of 'a C_Ast.cPartDesignator
| mk_cStatement of 'a C_Ast.cStatement
| mk_cStructureUnion of 'a C_Ast.cStructureUnion
| mk_cTypeQualifier of 'a C_Ast.cTypeQualifier
| mk_cTypeSpecifier of 'a C_Ast.cTypeSpecifier
| mk_cStructTag of C_Ast.cStructTag
| mk_cUnaryOp of C_Ast.cUnaryOp
| mk_cAssignOp of C_Ast.cAssignOp
| mk_cBinaryOp of C_Ast.cBinaryOp
| mk_cIntFlag of C_Ast.cIntFlag
| mk_cIntRepr of C_Ast.cIntRepr
| mk_cExternalDeclaration of 'a C_Ast.cExternalDeclaration
| mk_cTranslationUnit of 'a C_Ast.cTranslationUnit
end
structure C11_Ast_Lib : C11_AST_LIB =
struct
local open C_Ast in
datatype data = data_bool of bool | data_int of int
| data_string of string | data_absstring of string
| data_nodeInfo of C_Ast.nodeInfo
type node_content = { tag : string,
sub_tag : string,
args : data list }
fun TT s = { tag = s, sub_tag = "", args = [] }
fun TTT s t = { tag = s, sub_tag = t, args = [] }
fun ({ tag,sub_tag,args} #>> S) = { tag = tag, sub_tag = sub_tag, args = args @ S }
fun fold_optiona _ None st = st | fold_optiona g (Some a) st = g a st;
fun fold_either g1 _ (Left a) st = g1 a st
|fold_either _ g2 (Right a) st = g2 a st
fun toString_cStructTag (X:C_Ast.cStructTag) = @{make_string} X
fun toString_cIntFlag (X:C_Ast.cIntFlag) = @{make_string} X
fun toString_cIntRepr (X:C_Ast.cIntRepr) = @{make_string} X
fun toString_cUnaryOp (X:C_Ast.cUnaryOp) = @{make_string} X
fun toString_cAssignOp (X:C_Ast.cAssignOp) = @{make_string} X
fun toString_cBinaryOp (X:C_Ast.cBinaryOp) = @{make_string} X
fun toString_cIntFlag (X:C_Ast.cIntFlag) = @{make_string} X
fun toString_cIntRepr (X:C_Ast.cIntRepr) = @{make_string} X
val encode_positions =
let fun conv ({line = line,
offset = offset,
end_offset = end_offset,
props = {file = file, id = id, label = label}} : Thread_Position.T)
= ((line, offset, end_offset), (file,id,label))
in map (Position.dest #> conv)
#> let open XML.Encode in list (pair (triple int int int) (triple string string string)) end
#> YXML.string_of_body
end
val decode_positions=
let
fun snd ((a,b)) = b
fun conv ((line, offset, end_offset), properties) =
{line = line, offset = offset, end_offset = end_offset,
props = {id=snd(hd properties), label="", file=""}}
in (YXML.parse_body
#> let open XML.Decode in list (pair (triple int int int) (properties)) end
#> map (conv #> Position.make))
end
fun dark_matter x = XML.content_of (YXML.parse_body x)
val toString_abr_string_2 = C_Ast.meta_of_logic
local
val ST_tok = hd(ML_Lex.read_source ‹C_Ast.ST›)
val STa_tok = hd(ML_Lex.read_source ‹C_Ast.STa›)
val SS_base_tok = hd(ML_Lex.read_source ‹C_Ast.SS_base›)
val String_concatWith_tok = hd(ML_Lex.read_source ‹C_Ast.String_concatWith›)
fun eval ctxt pos ml =
ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos ml
handle ERROR msg => error (msg ^ Position.here pos);
fun convert_to_long_ML_ids (Antiquote.Text A) = (case ML_Lex.content_of A of
"ST" => ST_tok
|"STa" => STa_tok
|"SS_base" => SS_base_tok
|"String_concatWith" => String_concatWith_tok
| _ => Antiquote.Text A)
|convert_to_long_ML_ids X = X
in
fun get_abr_string_from_Ident_string XX =
let val txt00 ="(ABR_STRING_SPY := ("^XML.content_of (YXML.parse_body XX)^"))";
val ml00' = map convert_to_long_ML_ids (ML_Lex.read_source (Input.string txt00))
val t = eval @{context} @{here} ml00';
in !ABR_STRING_SPY end
end;
fun toString_abr_string (C_Ast.SS_base (C_Ast.ST txt)) = txt
| toString_abr_string (C_Ast.SS_base (C_Ast.STa txt)) = @{make_string} txt
| toString_abr_string (C_Ast.String_concatWith (a,S) ) =
String.concatWith (toString_abr_string a) (map toString_abr_string S)
fun toPos_positiona (C_Ast.Position0(i, str,j,k)) = decode_positions(toString_abr_string str)
| toPos_positiona C_Ast.NoPosition0 = []
| toPos_positiona C_Ast.BuiltinPosition0 = []
| toPos_positiona C_Ast.InternalPosition0 = []
fun toString_nodeinfo (C_Ast.NodeInfo0 (positiona, (positiona', i), namea)) =
let val p1 = toPos_positiona positiona;
val p2 = toPos_positiona positiona';
val C_Ast.Name0 X = namea;
in "<"^ @{make_string} p1 ^ " : " ^ @{make_string} p2 ^"::" ^ Int.toString X ^ ">"
end
|toString_nodeinfo (C_Ast.OnlyPos0 (positiona, (positiona', i))) =
let val p1 = toPos_positiona positiona;
val p2 = toPos_positiona positiona';
in "<"^ @{make_string} p1 ^ " : " ^ @{make_string} p2 ^">"
end;
fun id_of_node_content {args = (data_string S)::_::data_nodeInfo S'::[], sub_tag = _, tag = _} =
(toString_abr_string o get_abr_string_from_Ident_string)(S)
fun toString_node_content
{args = (data_string S)::_::data_nodeInfo S'::[],
sub_tag = STAG,
tag = TAG}
= ("TAG:"^TAG^":"^STAG^":"^ (toString_abr_string o get_abr_string_from_Ident_string)(S)^
"<:>"^toString_nodeinfo S'^"<:>");
fun toString_Chara (Chara(b1,b2,b3,b4,b5,b6,b7,b8)) =
let val v1 = (b1 ? (K 0)) (128)
val v2 = (b2 ? (K 0)) (64)
val v3 = (b3 ? (K 0)) (32)
val v4 = (b4 ? (K 0)) (16)
val v5 = (b5 ? (K 0)) (8)
val v6 = (b6 ? (K 0)) (4)
val v7 = (b7 ? (K 0)) (2)
val v8 = (b8 ? (K 0)) (1)
in String.implode[Char.chr(v1+v2+v3+v4+v5+v6+v7+v8)] end
fun fold_cInteger g' (CInteger0 (i: int, r: cIntRepr, rfl:cIntFlag flags)) st =
st |> g'(TT "CInteger0"
#>> [data_int i,
data_string (@{make_string} r),
data_string (@{make_string} rfl)])
fun fold_cChar g' (CChar0(c : char, b:bool)) st =
st |> g' (TT"CChar0"
#>> [data_string (toString_Chara c),data_bool (b)])
| fold_cChar g' (CChars0(cs : char list, b:bool)) st =
let val cs' = cs |> map toString_Chara
|> String.concat
in st |> g' (TT"CChars0" #>> [data_string cs',data_bool b]) end
fun fold_cFloat g' (CFloat0 (bstr: abr_string)) st =
st |> g' (TT"CFloat0"#>> [data_string (@{make_string} bstr)])
fun fold_cString g' (CString0 (bstr: abr_string, b: bool)) st =
st |> g' (TT"CString0"#>> [data_string (@{make_string} bstr), data_bool b])
fun fold_cConstant g ast st =
case ast of
(CIntConst0 (i: cInteger, a)) => st |> fold_cInteger (fn x=>g x a) i
|> g (TT"CIntConst0") a
|(CCharConst0 (c : cChar, a)) => st |> fold_cChar (fn x=>g x a) c
|> g (TT"CCharConst0") a
|(CFloatConst0 (f : cFloat, a)) => st |> fold_cFloat (fn x=>g x a) f
|> g (TT"CFloatConst0") a
|(CStrConst0 (s : cString, a))=> st |> fold_cString (fn x=>g x a) s
|> g (TT"CStrConst0") a
fun fold_ident a g (Ident0(bstr : abr_string, i : int, ni: nodeInfo )) st =
st |> g (TT "Ident0"
#>> [data_string (@{make_string} bstr),
data_int i,
data_nodeInfo ni
]) a
fun fold_cStringLiteral g (CStrLit0(cs:cString, a)) st = st |> fold_cString (fn x=>g x a) cs
|> g (TT"CStrLit0") a
fun fold_cTypeSpecifier grp g ast st =
case ast of
(CAtomicType0 (decl : 'a cDeclaration, a)) =>
st |> fold_cDeclaration grp g decl |> g (TT"CAtomicType0") a
| (CBoolType0 a) => st |> g (TT"CBoolType0") a
| (CCharType0 a) => st |> g (TT"CCharType0") a
| (CComplexType0 a) => st |> g (TT"CComplexType0") a
| (CDoubleType0 a) => st |> g (TT"CDoubleType0") a
| (CEnumType0(e: 'a cEnumeration, a)) =>
st |> fold_cEnumeration grp g e |> g (TT"CEnumType0") a
| (CFloatType0 a) => st |> g (TT"CFloatType0") a
| (CInt128Type0 a) => st |> g (TT"CInt128Type0") a
| (CIntType0 a) => st |> g (TT"CIntType0") a
| (CLongType0 a) => st |> g (TT"CLongType0") a
| (CSUType0 (su: 'a cStructureUnion, a)) =>
st |> fold_cStructureUnion grp g su |> g (TT"CSUType0") a
| (CShortType0 a) => st |> g (TT"CShortType0") a
| (CSignedType0 a) => st |> g (TT"CSignedType0") a
| (CTypeDef0 (id:ident, a)) =>
st |> fold_ident a g id |> g (TT"CTypeDef0") a
| (CTypeOfExpr0 (ex: 'a cExpression, a)) =>
st |> fold_cExpression grp g ex |> g (TT"CTypeOfExpr0") a
| (CTypeOfType0 (decl: 'a cDeclaration, a)) =>
st |> fold_cDeclaration grp g decl |> g (TT"CTypeOfType0") a
| (CUnsigType0 a) => st |> g (TT"CUnsigType0") a
| (CVoidType0 a) => st |> g (TT"CVoidType0") a
and fold_cTypeQualifier grp g ast st =
case ast of
(CAtomicQual0 a) => g (TT"CAtomicQual0") a st
| (CAttrQual0 (CAttr0 (id,eL:'a cExpression list, a))) =>
st |> fold_ident a g id
|> fold(fold_cExpression grp g) eL
|> g (TT"CAttrQual0") a
| (CConstQual0 a) => st |> g (TT"CConstQual0") a
| (CNonnullQual0 a) => st |> g (TT"CNonnullQual0") a
| (CNullableQual0 a) => st |> g (TT"CNullableQual0") a
| (CRestrQual0 a) => st |> g (TT"CRestrQual0") a
| (CVolatQual0 a) => st |> g (TT"CVolatQual0") a
and fold_cStatement grp g ast st =
case ast of
(CLabel0(id:ident, s:'a cStatement, aL: 'a cAttribute list, a)) =>
st |> fold_ident a g id
|> fold_cStatement grp g s
|> fold(fold_cAttribute grp g) aL
|> g (TT"CLabel0") a
| (CCase0(ex: 'a cExpression, stmt: 'a cStatement, a)) =>
st |> fold_cExpression grp g ex
|> fold_cStatement grp g stmt
|> g (TT"CCase0") a
| (CCases0(ex1: 'a cExpression, ex2: 'a cExpression, stmt:'a cStatement, a)) =>
st |> fold_cExpression grp g ex1
|> fold_cExpression grp g ex2
|> fold_cStatement grp g stmt
|> g (TT"CCases0") a
| (CDefault0(stmt:'a cStatement, a)) =>
st |> fold_cStatement grp g stmt
|> g (TT"CDefault0") a
| (CExpr0(ex_opt:'a cExpression optiona, a)) =>
st |> fold_optiona (fold_cExpression grp g) ex_opt
|> g (TT"CExpr0") a
| (CCompound0(idS : ident list,
cbiS: 'a cCompoundBlockItem list, a)) =>
st |> fold(fold_ident a g) idS
|> (fn st' => ((grp st') o (fold(fold_cCompoundBlockItem a grp g) cbiS)) st')
|> g (TT"CCompound0") a
| (CIf0(ex1:'a cExpression,stmt: 'a cStatement,
stmt_opt: 'a cStatement optiona, a)) =>
st |> fold_cExpression grp g ex1
|> fold_cStatement grp g stmt
|> fold_optiona (fold_cStatement grp g) stmt_opt
|> g (TT"CIf0") a
| (CSwitch0(ex1:'a cExpression, stmt: 'a cStatement, a)) =>
st |> fold_cExpression grp g ex1
|> fold_cStatement grp g stmt
|> g (TT"CSwitch0") a
| (CWhile0(ex1:'a cExpression, stmt: 'a cStatement, b: bool, a)) =>
st |> fold_cExpression grp g ex1
|> fold_cStatement grp g stmt
|> g (TT"CWhile0" #>> [data_bool b]) a
| (CFor0(ex0:('a cExpression optiona, 'a cDeclaration) either,
ex1_opt: 'a cExpression optiona, ex2_opt: 'a cExpression optiona,
stmt: 'a cStatement, a)) =>
st |> fold_either (fold_optiona (fold_cExpression grp g))
(fold_cDeclaration grp g) ex0
|> fold_optiona (fold_cExpression grp g) ex1_opt
|> fold_optiona (fold_cExpression grp g) ex2_opt
|> fold_cStatement grp g stmt
|> g (TT"CFor0") a
| (CGoto0(id: ident, a)) =>
st |> fold_ident a g id
|> g (TT"CGoto0") a
| (CGotoPtr0(ex1:'a cExpression, a)) =>
st |> fold_cExpression grp g ex1 |> g (TT"CGotoPtr0") a
| (CCont0 a) => st |> g (TT"CCont0") a
| (CBreak0 a) => st |> g (TT"CBreak0") a
| (CReturn0 (ex:'a cExpression optiona,a)) =>
st |> fold_optiona (fold_cExpression grp g) ex |> g (TT"CReturn0") a
| (CAsm0(_: 'a cAssemblyStatement, a)) => st |> g (TT"CAsm0") a
and fold_cExpression grp g ast st =
case ast of
(CComma0 (eL:'a cExpression list, a)) =>
st |> fold(fold_cExpression grp g) eL |> g (TT"CComma0") a
| (CAssign0(aop:cAssignOp, ex1:'a cExpression, ex2:'a cExpression,a)) =>
st |> fold_cExpression grp g ex1
|> fold_cExpression grp g ex2
|> g (TTT"CAssign0" (toString_cAssignOp aop)) a
| (CCond0( ex1:'a cExpression, ex2opt: 'a cExpression optiona,
ex3: 'a cExpression,a)) =>
st |> fold_cExpression grp g ex1
|> fold_optiona (fold_cExpression grp g) ex2opt
|> fold_cExpression grp g ex3 |> g (TT"CCond0") a
| (CBinary0(bop: cBinaryOp, ex1: 'a cExpression,ex2: 'a cExpression, a)) =>
st |> fold_cExpression grp g ex1
|> fold_cExpression grp g ex2
|> g (TTT"CBinary0"(toString_cBinaryOp bop)) a
| (CCast0(decl:'a cDeclaration, ex: 'a cExpression, a)) =>
st |> fold_cExpression grp g ex
|> fold_cDeclaration grp g decl
|> g (TT"CCast0") a
| (CUnary0(unop:cUnaryOp, ex: 'a cExpression, a)) =>
st |> fold_cExpression grp g ex
|> g (TT("CUnary0 "^toString_cUnaryOp unop)) a
| (CSizeofExpr0(ex:'a cExpression, a)) =>
st |> fold_cExpression grp g ex |> g (TT"CSizeofExpr0") a
| (CSizeofType0(decl:'a cDeclaration,a)) =>
st |> fold_cDeclaration grp g decl |> g (TT"CSizeofType0") a
| (CAlignofExpr0(ex:'a cExpression, a)) =>
st |> fold_cExpression grp g ex |> g (TT"CAlignofExpr0") a
| (CAlignofType0(decl:'a cDeclaration, a)) =>
st |> fold_cDeclaration grp g decl |> g (TT"CAlignofType0") a
| (CComplexReal0(ex:'a cExpression, a)) =>
st |> fold_cExpression grp g ex |> g (TT"CComplexReal0") a
| (CComplexImag0(ex:'a cExpression, a)) =>
st |> fold_cExpression grp g ex |> g (TT"CComplexImag0") a
| (CIndex0(ex1:'a cExpression, ex2: 'a cExpression, a)) =>
st |> fold_cExpression grp g ex1
|> fold_cExpression grp g ex2
|> g (TT"CIndex0") a
| (CCall0(ex:'a cExpression, argS: 'a cExpression list, a)) =>
st |> fold_cExpression grp g ex
|> fold (fold_cExpression grp g) argS
|> g (TT"CCall0") a
| (CMember0(ex:'a cExpression, id:ident, b, a)) =>
st |> fold_cExpression grp g ex
|> fold_ident a g id
|> g (TT"CMember0"#>> [data_bool b]) a
| (CVar0(id:ident,a)) => st |> fold_ident a g id |> g (TT"CVar0") a
| (CConst0(cc:'a cConstant)) => st |> fold_cConstant g cc
| (CCompoundLit0(decl:'a cDeclaration,eqn:('a cPartDesignator list*'a cInitializer)list,a))=>
st |> fold(fn(S,init) =>
fn st => st |> fold(fold_cPartDesignator grp g) S
|> fold_cInitializer grp g init) eqn
|> fold_cDeclaration grp g decl
|> g (TT"CCompoundLit0") a
| (CGenericSelection0(ex:'a cExpression,eqn:('a cDeclaration optiona*'a cExpression)list,a))=>
st |> fold_cExpression grp g ex
|> fold (fn (d,ex) =>
fn st => st |> fold_optiona (fold_cDeclaration grp g) d
|> fold_cExpression grp g ex) eqn
|> g (TT"CGenericSelection0") a
| (CStatExpr0(stmt: 'a cStatement,a)) =>
st |> fold_cStatement grp g stmt |> g (TT"CStatExpr0") a
| (CLabAddrExpr0(id:ident,a)) =>
st |> fold_ident a g id |> g (TT"CLabAddrExpr0") a
| (CBuiltinExpr0(X: 'a cBuiltinThing)) => st |> fold_cBuiltinThing grp g X
and fold_cDeclaration grp g ast st =
case ast of
(CDecl0(dsS:'a cDeclarationSpecifier list,
mkS:(('a cDeclarator optiona*'a cInitializer optiona)*'a cExpression optiona)list,a)) =>
st |> fold(fold_cDeclarationSpecifier grp g) dsS
|> fold(fn ((d_o, init_o),ex_opt) =>
fn st => st |> fold_optiona(fold_cDeclarator grp g) d_o
|> fold_optiona(fold_cInitializer grp g) init_o
|> fold_optiona(fold_cExpression grp g) ex_opt) mkS
|> g (TT"CDecl0") a
| (CStaticAssert0(ex:'a cExpression, slit: 'a cStringLiteral, a)) =>
st |> fold_cExpression grp g ex
|> fold_cStringLiteral g slit
|> g (TT"CStaticAssert0") a
and fold_cBuiltinThing grp g (CBuiltinVaArg0(ex:'a cExpression,decl: 'a cDeclaration,a)) st =
st |> fold_cExpression grp g ex
|> fold_cDeclaration grp g decl
|> g (TT"CBuiltinVaArg0") a
| fold_cBuiltinThing grp g (CBuiltinOffsetOf0(d: 'a cDeclaration, _: 'a cPartDesignator list, a)) st =
st |> fold_cDeclaration grp g d
|> g (TT"CBuiltinOffsetOf0") a
| fold_cBuiltinThing grp g (CBuiltinTypesCompatible0 (d1: 'a cDeclaration, d2: 'a cDeclaration,a)) st=
st |> fold_cDeclaration grp g d1
|> fold_cDeclaration grp g d2
|> g (TT"CBuiltinTypesCompatible0") a
and fold_cInitializer grp g (CInitExpr0(ex: 'a cExpression, a)) st =
st |> fold_cExpression grp g ex |> g (TT"CInitExpr0") a
| fold_cInitializer grp g (CInitList0 (mms: ('a cPartDesignator list * 'a cInitializer) list,a)) st =
st |> fold(fn (a,b) =>
fn st => st|> fold(fold_cPartDesignator grp g) a
|> fold_cInitializer grp g b) mms
|> g (TT"CInitList0") a
and fold_cPartDesignator grp g (CArrDesig0(ex: 'a cExpression, a)) st =
st |> fold_cExpression grp g ex |> g (TT"CArrDesig0") a
| fold_cPartDesignator grp g (CMemberDesig0(id: ident, a)) st =
st |> fold_ident a g id |> g (TT"CMemberDesig0") a
| fold_cPartDesignator grp g (CRangeDesig0(ex1: 'a cExpression, ex2: 'a cExpression, a)) st =
st |> fold_cExpression grp g ex1
|> fold_cExpression grp g ex2
|> g (TT"CRangeDesig0") a
and fold_cAttribute grp g (CAttr0(id: ident, exS: 'a cExpression list, a)) st =
st |> fold_ident a g id
|> fold(fold_cExpression grp g) exS
|> g (TT"CAttr0") a
and fold_cEnumeration grp g (CEnum0 (ident_opt: ident optiona,
exS_opt: ((ident * 'a cExpression optiona) list) optiona,
attrS: 'a cAttribute list, a)) st =
st |> fold_optiona(fold_ident a g) ident_opt
|> fold_optiona(fold(
fn (id,ex_o) =>
fn st => st |> fold_ident a g id
|> fold_optiona (fold_cExpression grp g) ex_o))
exS_opt
|> fold(fold_cAttribute grp g) attrS
|> g (TT"CEnum0") a
and fold_cArraySize a grp g (CNoArrSize0 (b: bool)) st =
st |> g (TT "CNoArrSize0" #>> [data_bool b]) a
| fold_cArraySize a grp g (CArrSize0 (b:bool, ex : 'a cExpression)) st =
st |> fold_cExpression grp g ex
|> g (TT "CNoArrSize0" #>> [data_bool b]) a
and fold_cDerivedDeclarator grp g (CPtrDeclr0 (tqS: 'a cTypeQualifier list , a)) st =
st |> fold(fold_cTypeQualifier grp g) tqS
|> g (TT"CPtrDeclr0") a
| fold_cDerivedDeclarator grp g (CArrDeclr0 (tqS:'a cTypeQualifier list, aS: 'a cArraySize,a)) st =
st |> fold(fold_cTypeQualifier grp g) tqS
|> fold_cArraySize a grp g aS
|> g (TT"CArrDeclr0") a
| fold_cDerivedDeclarator grp g (CFunDeclr0 (decl_alt: (ident list,
('a cDeclaration list * bool)) either,
aS: 'a cAttribute list, a)) st =
st |> fold_either
(fold(fold_ident a g))
(fn (declS,b) =>
fn st => st |> fold (fold_cDeclaration grp g) declS
|> g (TTT "CFunDeclr0""decl_alt-Right"
#>> [data_bool b]) a) decl_alt
|> fold(fold_cAttribute grp g) aS
|> g (TT"CFunDeclr0") a
and fold_cDeclarationSpecifier grp g ast st =
case ast of
(CStorageSpec0(CAuto0 a)) => st |> g (TTT"CStorageSpec0" "CAuto0") a
| (CStorageSpec0(CRegister0 a)) => st |> g (TTT"CStorageSpec0" "CRegister0") a
| (CStorageSpec0(CStatic0 a)) => st |> g (TTT"CStorageSpec0" "CStatic0") a
| (CStorageSpec0(CExtern0 a)) => st |> g (TTT"CStorageSpec0" "CExtern0") a
| (CStorageSpec0(CTypedef0 a)) => st |> g (TTT"CStorageSpec0" "CTypedef0") a
| (CStorageSpec0(CThread0 a)) => st |> g (TTT"CStorageSpec0" "CThread0") a
| (CTypeSpec0(CVoidType0 a)) => st |> g (TTT"CTypeSpec0""CVoidType0") a
| (CTypeSpec0(CCharType0 a)) => st |> g (TTT"CTypeSpec0""CCharType0") a
| (CTypeSpec0(CShortType0 a)) => st |> g (TTT"TCTypeSpec0""CShortType0") a
| (CTypeSpec0(CIntType0 a)) => st |> g (TTT"CTypeSpec0""CIntType0") a
| (CTypeSpec0(CLongType0 a)) => st |> g (TTT"CTypeSpec0""CLongType0") a
| (CTypeSpec0(CFloatType0 a)) => st |> g (TTT"CTypeSpec0""CFloatType0") a
| (CTypeSpec0(CDoubleType0 a)) => st |> g (TTT"CTypeSpec0""CDoubleType0") a
| (CTypeSpec0(CSignedType0 a)) => st |> g (TTT"CTypeSpec0""CSignedType0") a
| (CTypeSpec0(CUnsigType0 a)) => st |> g (TTT"CTypeSpec0""CUnsigType0") a
| (CTypeSpec0(CBoolType0 a)) => st |> g (TTT"CTypeSpec0""CBoolType0") a
| (CTypeQual0(x:'a cTypeQualifier)) => st |> fold_cTypeQualifier grp g x
| (CFunSpec0(CInlineQual0 a)) => st |> g (TTT"CFunSpec0""CInlineQual0") a
| (CFunSpec0(CNoreturnQual0 a)) => st |> g (TTT"CFunSpec0""CNoreturnQual0") a
| (CAlignSpec0(CAlignAsType0(decl,a))) => st |> fold_cDeclaration grp g decl
|> g (TTT"CAlignSpec0""CAlignAsType0") a
| (CAlignSpec0(CAlignAsExpr0(ex,a)))=> st |> fold_cExpression grp g ex
|> g (TTT"CAlignSpec0""CAlignAsType0") a
and fold_cDeclarator grp g (CDeclr0(id_opt: ident optiona,
declS: 'a cDerivedDeclarator list,
sl_opt: 'a cStringLiteral optiona,
attrS: 'a cAttribute list, a)) st =
st |> fold_optiona(fold_ident a g) id_opt
|> fold (fold_cDerivedDeclarator grp g) declS
|> fold_optiona(fold_cStringLiteral g) sl_opt
|> fold(fold_cAttribute grp g) attrS
|> g (TT"CDeclr0") a
and fold_cFunctionDef grp g (CFunDef0(dspecS: 'a cDeclarationSpecifier list,
dclr: 'a cDeclarator,
declsS: 'a cDeclaration list,
stmt: 'a cStatement, a)) st =
st |> fold(fold_cDeclarationSpecifier grp g) dspecS
|> fold_cDeclarator grp g dclr
|> fold(fold_cDeclaration grp g) declsS
|> fold_cStatement grp g stmt
|> g (TT"CFunDef0") a
and fold_cCompoundBlockItem a grp g ast st =
case ast of
(CBlockStmt0 (stmt: 'a cStatement)) =>
st |> fold_cStatement grp g stmt
|> g (TT"CBlockStmt0") a
| (CBlockDecl0 (decl : 'a cDeclaration)) =>
st |> fold_cDeclaration grp g decl
|> g (TT"CBlockDecl0") a
| (CNestedFunDef0(fdef : 'a cFunctionDef)) =>
st |> fold_cFunctionDef grp g fdef
|> g (TT"CNestedFunDef0") a
and fold_cStructureUnion grp g (CStruct0( ct : cStructTag, id_a: ident optiona,
declS_opt : ('a cDeclaration list) optiona,
aS: 'a cAttribute list, a)) st =
st |> fold_optiona (fold_ident a g) id_a
|> fold_optiona (fold(fold_cDeclaration grp g)) declS_opt
|> fold(fold_cAttribute grp g) aS
|> g (TTT "CStruct0" (toString_cStructTag ct)) a
and fold_cExternalDeclaration grp g ast st =
case ast of
(CDeclExt0(cd : 'a cDeclaration)) => st |> fold_cDeclaration grp g cd
| (CFDefExt0(fd : 'a cFunctionDef)) => st |> fold_cFunctionDef grp g fd
| (CAsmExt0( _ : 'a cStringLiteral, _ : 'a)) => error"Inline assembler not supprted"
and fold_cTranslationUnit grp g (CTranslUnit0 (ceL : 'a cExternalDeclaration list, a : 'a)) st =
st |> fold(fold_cExternalDeclaration grp g) ceL
|> g (TT"CTranslUnit0") a
datatype 'a C11_Ast =
mk_cInteger of C_Ast.cInteger
| mk_cStructTag of C_Ast.cStructTag
| mk_cUnaryOp of C_Ast.cUnaryOp
| mk_cAssignOp of C_Ast.cAssignOp
| mk_cBinaryOp of C_Ast.cBinaryOp
| mk_cIntFlag of C_Ast.cIntFlag
| mk_cIntRepr of C_Ast.cIntRepr
| mk_cConstant of 'a C_Ast.cConstant
| mk_cStringLiteral of 'a C_Ast.cStringLiteral
| mk_cArraySize of 'a C_Ast.cArraySize
| mk_cAttribute of 'a C_Ast.cAttribute
| mk_cBuiltinThing of 'a C_Ast.cBuiltinThing
| mk_cCompoundBlockItem of 'a C_Ast.cCompoundBlockItem
| mk_cDeclaration of 'a C_Ast.cDeclaration
| mk_cDeclarationSpecifier of 'a C_Ast.cDeclarationSpecifier
| mk_cDeclarator of 'a C_Ast.cDeclarator
| mk_cDerivedDeclarator of 'a C_Ast.cDerivedDeclarator
| mk_cEnumeration of 'a C_Ast.cEnumeration
| mk_cExpression of 'a C_Ast.cExpression
| mk_cInitializer of 'a C_Ast.cInitializer
| mk_cPartDesignator of 'a C_Ast.cPartDesignator
| mk_cStatement of 'a C_Ast.cStatement
| mk_cStructureUnion of 'a C_Ast.cStructureUnion
| mk_cTypeQualifier of 'a C_Ast.cTypeQualifier
| mk_cTypeSpecifier of 'a C_Ast.cTypeSpecifier
| mk_cExternalDeclaration of 'a C_Ast.cExternalDeclaration
| mk_cTranslationUnit of 'a C_Ast.cTranslationUnit
end
end
›
end