slightly improved hylo.

C11-BackEnds/AutoCorres_wrapper/examples/GCD_Fred_CAS.thy

@@ -221,6 +221,7 @@ val bbb = get_anno_data (Context.Proof @{context})
 \<close>
 
 
+
 ML\<open>
 val get_anno_data = C_Module'.Annotation_Data.get ;
 val blocks = Inttab.keys o get_anno_data;
@@ -276,10 +277,13 @@ val ([C_Ast.CDecl0 Y5,C_Ast.CDecl0 Y5'],false) =Y4;
 val (Y6,Y6',Y6'') = Y5
 
 val [C_Ast.CTypeSpec0 Y7] = Y6
-val  C_Ast.CIntType0 (C_Ast.NodeInfo0 Y8) = Y7
-open C_Ast;
+val  C_Ast.CIntType0 (C_Ast.NodeInfo0 Y8) = Y7\<close>
+
+
+(* HINT *)
+ML\<open>@{make_string} Y8\<close>
+
 
-\<close>
 
 ML\<open>
 
@@ -290,7 +294,16 @@ val S = map C11_Ast_Lib.toString_nodeinfo nodes;
 
 \<close>
 
+ML\<open>open String\<close>
 ML\<open>
+val sep = String.fields (fn x => x = #" ") 
+val identS = fold(C11_Ast_Lib.fold_cDerivedDeclarator 
+                 (fn key => fn a => fn S => if String.isPrefix "Ident0" key 
+                                            then (sep key) :: S else S)) 
+                 params 
+                 []
+
+
 
 \<close>
 

C11-FrontEnd/src/C_Ast.thy

@@ -329,70 +329,21 @@ 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 CStructTag0 = "CStructTag0"
-   |toString_cStructTag CUnionTag0  = "CUnionTag0"
-
-fun toString_cIntFlag FlagUnsigned0 = "FlagUnsigned0"
-  | toString_cIntFlag FlagLong0     = "FlagLong0"
-  | toString_cIntFlag FlagLongLong0 = "FlagLongLong0"
-  | toString_cIntFlag FlagImag0     = "FlagImag0"
-
-fun toString_cIntRepr DecRepr0      = "DecRepr0"
-  | toString_cIntRepr HexRepr0      = "HexRepr0"
-  | toString_cIntRepr OctalRepr0    = "OctalRepr0"
-
-
-fun toString_cUnaryOp CPreIncOp0    = "CPreIncOp0"
-  | toString_cUnaryOp CPreDecOp0    = "CPreDecOp0"
-  | toString_cUnaryOp CPostIncOp0   = "CPostIncOp0"
-  | toString_cUnaryOp CPostDecOp0   = "CPostDecOp0"
-  | toString_cUnaryOp CAdrOp0       = "CAdrOp0"
-  | toString_cUnaryOp CIndOp0       = "CIndOp0"
-  | toString_cUnaryOp CPlusOp0      = "CPlusOp0"
-  | toString_cUnaryOp CMinOp0       = "CMinOp0"
-  | toString_cUnaryOp CCompOp0      = "CCompOp0"
-  | toString_cUnaryOp CNegOp0       = "CNegOp0"
-                                    
-fun toString_cAssignOp CAssignOp0   = "CAssignOp0"
-  | toString_cAssignOp CMulAssOp0   = "CMulAssOp0"
-  | toString_cAssignOp CDivAssOp0   = "CDivAssOp0"
-  | toString_cAssignOp CRmdAssOp0   = "CRmdAssOp0"
-  | toString_cAssignOp CAddAssOp0   = "CAddAssOp0"
-  | toString_cAssignOp CSubAssOp0   = "CSubAssOp0"
-  | toString_cAssignOp CShlAssOp0   = "CShlAssOp0"
-  | toString_cAssignOp CShrAssOp0   = "CShrAssOp0"
-  | toString_cAssignOp CAndAssOp0   = "CAndAssOp0"
-  | toString_cAssignOp CXorAssOp0   = "CXorAssOp0"
-  | toString_cAssignOp COrAssOp0    = "COrAssOp0"
-
-fun toString_cBinaryOp CMulOp0      = "CMulOp0"
-  | toString_cBinaryOp CDivOp0      = "CDivOp0"
-  | toString_cBinaryOp CRmdOp0      = "CRmdOp0"
-  | toString_cBinaryOp CAddOp0      = "CAddOp0"
-  | toString_cBinaryOp CSubOp0      = "CSubOp0"
-  | toString_cBinaryOp CShlOp0      = "CShlOp0"
-  | toString_cBinaryOp CShrOp0      = "CShrOp0"
-  | toString_cBinaryOp CLeOp0       = "CLeOp0"
-  | toString_cBinaryOp CGrOp0       = "CGrOp0"
-  | toString_cBinaryOp CLeqOp0      = "CLeqOp0"
-  | toString_cBinaryOp CGeqOp0      = "CGeqOp0"
-  | toString_cBinaryOp CEqOp0       = "CEqOp0"
-  | toString_cBinaryOp CNeqOp0      = "CNeqOp0"
-  | toString_cBinaryOp CAndOp0      = "CAndOp0"
-  | toString_cBinaryOp CXorOp0      = "CXorOp0"
-  | toString_cBinaryOp COrOp0       = "COrOp0"
-  | toString_cBinaryOp CLndOp0      = "CLndOp0"
-  | toString_cBinaryOp CLorOp0      = "CLorOp0"
-
-fun toString_cIntFlag FlagUnsigned0 = "FlagUnsigned0"
-  | toString_cIntFlag FlagLong0     = "FlagLong0"
-  | toString_cIntFlag FlagLongLong0 = "FlagLongLong0"
-  | toString_cIntFlag FlagImag0     = "FlagImag0"
-
-fun toString_cIntRepr DecRepr0      = "DecRepr0"
-  | toString_cIntRepr HexRepr0      = "HexRepr0"
-  | toString_cIntRepr OctalRepr0    = "OctalRepr0"
-
+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
 
 fun dark_matter x = XML.content_of (YXML.parse_body x)
 
@@ -442,8 +393,13 @@ fun fold_cConstant g (CIntConst0 (i: cInteger, a))  st = st |> fold_cInteger (fn
   | fold_cConstant g (CStrConst0 (s : cString, a))  st = st |> fold_cString (fn x=>g x a) s
                                                             |> g "CStrConst0" a
 
-fun fold_ident a g (Ident0(_: abr_string, _ : int, _: nodeInfo (* ignored here !!! *))) st = 
-                         st |> g "Ident0" a
+fun fold_ident a g (Ident0(astr : abr_string, i : int, _: nodeInfo (* ignored here !!! *))) st = 
+                   let val ss = @{make_string} astr
+                       val i =  @{make_string} i
+                       val suffix = " "^ss^" "^i
+                   in
+                         st |> g ("Ident0"^suffix) a
+                   end
     (* there could be done much much more !!! *)
     (* that ident contains nodeinfo instead of 'a is an error in my view. *)