From d468cde3fc2d695fb9bb985e22067a67c6089bd4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Tuong?=
 <tuong@users.noreply.github.com>
Date: Sun, 2 Jan 2022 11:24:18 -0800
Subject: [PATCH] synchronize with afp-devel

---
 C11-FrontEnd/examples/C1.thy           |  4 ++--
 C11-FrontEnd/src/C_Command.thy         | 12 ++++++------
 C11-FrontEnd/src/C_Parser_Language.thy | 22 ++++++++++++++++++++++
 3 files changed, 30 insertions(+), 8 deletions(-)

diff --git a/C11-FrontEnd/examples/C1.thy b/C11-FrontEnd/examples/C1.thy
index e01ac29c7d7..676f37cc067 100644
--- a/C11-FrontEnd/examples/C1.thy
+++ b/C11-FrontEnd/examples/C1.thy
@@ -48,7 +48,7 @@ text\<open>The following setup just stores the result of the parsed values in th
 ML\<open>
 structure Data_Out = Generic_Data
 (
-  type T = (C_Grammar_Rule.start_happy * C_Antiquote.antiq C_Env.stream) list
+  type T = (C_Grammar_Rule.ast_generic * C_Antiquote.antiq C_Env.stream) list
   val empty = []
   val merge = K empty
 )
@@ -56,7 +56,7 @@ structure Data_Out = Generic_Data
 fun get_module thy =
   let val context = Context.Theory thy
   in (Data_Out.get context 
-      |> map (apfst (C_Grammar_Rule.start_happy1 #> the)), C_Module.Data_In_Env.get context)
+      |> map (apfst (C_Grammar_Rule.get_CTranslUnit #> the)), C_Module.Data_In_Env.get context)
   end
 \<close>
 
diff --git a/C11-FrontEnd/src/C_Command.thy b/C11-FrontEnd/src/C_Command.thy
index 63883e96853..9b830b5d4a3 100644
--- a/C11-FrontEnd/src/C_Command.thy
+++ b/C11-FrontEnd/src/C_Command.thy
@@ -166,14 +166,14 @@ structure Data_In_Env = Generic_Data
 
 structure Data_Accept = Generic_Data
 (
-  type T = C_Grammar_Rule.start_happy -> C_Env.env_lang -> Context.generic -> Context.generic
+  type T = C_Grammar_Rule.ast_generic -> C_Env.env_lang -> Context.generic -> Context.generic
   fun empty _ _ = I
   val merge = #2
 )
 
 structure Data_Term = Generic_Data
 (
-  type T = (C_Grammar_Rule.start_happy -> C_Env.env_lang -> local_theory -> term) Symtab.table
+  type T = (C_Grammar_Rule.ast_generic -> C_Env.env_lang -> local_theory -> term) Symtab.table
   val empty = Symtab.empty
   val merge = #2
 )
@@ -217,10 +217,10 @@ local
 fun map_upd0 key v = Context.theory_map (Data_Term.map (Symtab.update (key, v)))
 fun map_upd key start f = map_upd0 key (f o the o start)
 in
-val map_translation_unit = map_upd key0_translation_unit C_Grammar_Rule.start_happy1
-val map_external_declaration = map_upd key0_external_declaration C_Grammar_Rule.start_happy2
-val map_statement = map_upd key0_statement C_Grammar_Rule.start_happy3
-val map_expression = map_upd key0_expression C_Grammar_Rule.start_happy4
+val map_translation_unit = map_upd key0_translation_unit C_Grammar_Rule.get_CTranslUnit
+val map_external_declaration = map_upd key0_external_declaration C_Grammar_Rule.get_CExtDecl
+val map_statement = map_upd key0_statement C_Grammar_Rule.get_CStat
+val map_expression = map_upd key0_expression C_Grammar_Rule.get_CExpr
 val map_default = map_upd0 key0_default
 end
 
diff --git a/C11-FrontEnd/src/C_Parser_Language.thy b/C11-FrontEnd/src/C_Parser_Language.thy
index 0804ece1448..2850b234700 100644
--- a/C11-FrontEnd/src/C_Parser_Language.thy
+++ b/C11-FrontEnd/src/C_Parser_Language.thy
@@ -872,6 +872,28 @@ subsection \<open>Loading the Generated Grammar (SML signature)\<close>
 
 ML_file "../generated/c_grammar_fun.grm.sig"
 
+ML \<comment> \<open>\<^file>\<open>../generated/c_grammar_fun.grm.sig\<close>\<close>
+(*TODO: the whole part should be maximally generated and integrated in the signature file*)
+\<open>
+structure C_Grammar_Rule = struct
+open C_Grammar_Rule
+
+(* ast_generic is an untyped universe of (some) ast's with the specific lenses put ... get ... *)
+
+type ast_generic = start_happy
+
+val get_CExpr = start_happy4
+val get_CStat = start_happy3
+val get_CExtDecl = start_happy2
+val get_CTranslUnit = start_happy1
+
+fun put_CExpr (x :  C_Grammar_Rule_Lib.CExpr)      = Right (Right (Right (Left x))) : ast_generic
+fun put_CStat (x : C_Grammar_Rule_Lib.CStat)       = Right (Right (Left x))         : ast_generic
+fun put_CExtDecl (x : C_Grammar_Rule_Lib.CExtDecl) = Right (Left x)                 : ast_generic
+fun put_CTranslUnit (x : C_Grammar_Rule_Lib.CTranslUnit) = Left x                   : ast_generic
+end
+\<close>
+
 subsection \<open>Overloading Grammar Rules (Optional Part)\<close>
 
 ML \<comment> \<open>\<^file>\<open>../generated/c_grammar_fun.grm.sml\<close>\<close> \<open>
-- 
GitLab