store all encountered constructors in the environment

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13536 3260e6d1-4efc-4170-b0a7-36055960796d

Citadelle/src/compiler/core/Floor1_haskabelle.thy

@@ -101,56 +101,62 @@ fun hsk_term and
 
 definition "hsk_stmt version names app_end =
  (let b = \<lambda>s. Term_basic [s] in
-  concat o map
+  map_prod concat concat o L.split o map
    (\<lambda> Meta_HKB.Datatype l \<Rightarrow>
         let l_data = L.map (map_prod (hsk_typespec names) (L.map (map_prod (hsk_name names) (L.map (hsk_type names))))) l
           ; l_data' = concat (L.map (L.map (\<lambda>(s, _). (s, gen_zero s)) o snd) l_data) in
-        O.datatype (Datatype version (L.map (map_prod id (L.map (map_prod gen_zero id))) l_data))
-        # (* For each constructor, we additionally generate an alias definition, for it to be used
-             in the SML code generated part as an alternative of the SML generated constructor:
-             its type will be not curried (whereas the SML type of the constructor will be). *)
-          L.map (\<lambda>(s, s'). O.definition (Definition (Term_rewrite (b s) \<open>=\<close> (b s')))) l_data'
-    | TypeSynonym [(t0, t1)] \<Rightarrow> [O.type_synonym (Type_synonym (hsk_typespec names t0) (hsk_type names t1))]
+        ( O.datatype (Datatype version (L.map (map_prod id (L.map (map_prod gen_zero id))) l_data))
+          # (* For each constructor, we additionally generate an alias definition, for it to be used
+               in the SML code generated part as an alternative of the SML generated constructor:
+               its type will be not curried (whereas the SML type of the constructor will be). *)
+            L.map (\<lambda>(s, s'). O.definition (Definition (Term_rewrite (b s) \<open>=\<close> (b s')))) l_data'
+        , L.map fst l_data')
+    | TypeSynonym [(t0, t1)] \<Rightarrow> ([O.type_synonym (Type_synonym (hsk_typespec names t0) (hsk_type names t1))], [])
     | Function (Function_Stmt Meta_HKB.Definition [t] [((lhs_n, lhs_arg), rhs)]) \<Rightarrow>
         let s_empty = b \<open>v\<close>
           ; T_string = Term_string'
           ; hsk_term = hsk_term \<lparr> lex_list_cons = \<open>#\<close>, lex_bool_false = \<open>False\<close>, lex_string = (\<lambda>s. if s \<triangleq> \<open>\<close> then s_empty else T_string s) \<rparr> names in
-        [(O.definition o Definition)
-          (Term_rewrite (Term_app (hsk_name'' names lhs_n) (map hsk_term lhs_arg))
-                        \<open>=\<close>
-                        (let t = Term_parenthesis (Term_let [(s_empty, T_string \<open>\<close>)] (hsk_term rhs)) in
-                         case app_end of Gen_apply_hol f \<Rightarrow> Term_app f [t]
-                                       | _ \<Rightarrow> t))]
+        ( [(O.definition o Definition)
+            (Term_rewrite (Term_app (hsk_name'' names lhs_n) (map hsk_term lhs_arg))
+                          \<open>=\<close>
+                          (let t = Term_parenthesis (Term_let [(s_empty, T_string \<open>\<close>)] (hsk_term rhs)) in
+                           case app_end of Gen_apply_hol f \<Rightarrow> Term_app f [t]
+                                         | _ \<Rightarrow> t))]
+        , [])
     | Meta_HKB.SML (Function_Stmt Meta_HKB.Definition [t] [((lhs_n, lhs_arg), rhs)]) \<Rightarrow>
         let s_empty = b \<open>v\<close>
           ; f_content = b \<open>content\<close>
           ; T_string = Term_string'' f_content
           ; hsk_term = hsk_term \<lparr> lex_list_cons = \<open>::\<close>, lex_bool_false = \<open>false\<close>, lex_string = (\<lambda>s. if s \<triangleq> \<open>\<close> then s_empty else T_string s) \<rparr> names in
-        (O.ML o SML o SML_top)
-          [SML_val_fun
-             (Some Sval)
-             (hol_to_sml (Term_rewrite (Term_app (hsk_name'' names lhs_n) (map hsk_term lhs_arg))
-                                       \<open>=\<close>
-                                       (let t = Term_parenthesis (Term_let [ (f_content, term_binop \<open>o\<close> (map b [\<open>SS_base\<close>, \<open>ST\<close>, \<open>Input.source_content\<close>]))
-                                                                           , (s_empty, T_string \<open>\<close>)]
-                                                                           (hsk_term rhs)) in
-                                        case app_end of Gen_apply_sml f \<Rightarrow> Term_app f [t]
-                                                      | Gen_apply_sml_cmd f _ \<Rightarrow> Term_app f [t]
-                                                      | _ \<Rightarrow> t)))]
-        # (case app_end of Gen_apply_sml_cmd _ s \<Rightarrow>
-                            [(META_all_meta_embedding o META_generic o OclGeneric) s]
-                         | _ \<Rightarrow> [])
-    | _ \<Rightarrow> []))"
+        ( (O.ML o SML o SML_top)
+            [SML_val_fun
+               (Some Sval)
+               (hol_to_sml (Term_rewrite (Term_app (hsk_name'' names lhs_n) (map hsk_term lhs_arg))
+                                         \<open>=\<close>
+                                         (let t = Term_parenthesis (Term_let [ (f_content, term_binop \<open>o\<close> (map b [\<open>SS_base\<close>, \<open>ST\<close>, \<open>Input.source_content\<close>]))
+                                                                             , (s_empty, T_string \<open>\<close>)]
+                                                                             (hsk_term rhs)) in
+                                          case app_end of Gen_apply_sml f \<Rightarrow> Term_app f [t]
+                                                        | Gen_apply_sml_cmd f _ \<Rightarrow> Term_app f [t]
+                                                        | _ \<Rightarrow> t)))]
+          # (case app_end of Gen_apply_sml_cmd _ s \<Rightarrow>
+                              [(META_all_meta_embedding o META_generic o OclGeneric) s]
+                           | _ \<Rightarrow> [])
+        , [])
+    | _ \<Rightarrow> ([], [])))"
 
-definition "print_haskell = (\<lambda> IsaUnit version l_name app_end name_new (l_mod, b_concat) \<Rightarrow>
-  Pair (List.bind (if b_concat then l_mod else [last l_mod])
-                  (\<lambda> Module (ThyName name_old) _ m _ \<Rightarrow>
-                       hsk_stmt (case map_prod id nat_of_natural version of (False, _) \<Rightarrow> Datatype_new
-                                                                          | (True, 0) \<Rightarrow> Datatype_old
-                                                                          | (True, Suc 0) \<Rightarrow> Datatype_old_atomic
-                                                                          | (True, Suc (Suc 0)) \<Rightarrow> Datatype_old_atomic_sub)
-                                ((name_old, Some name_new) # l_name)
-                                app_end
-                                m)))"
+definition "print_haskell = (\<lambda> IsaUnit version l_name app_end name_new (l_mod, b_concat) \<Rightarrow> \<lambda>env.
+  (map_prod concat ((\<lambda>l1. D_hsk_constr_update (\<lambda>l0. l0 @ l1) env) o L.map String.to_String\<^sub>b\<^sub>a\<^sub>s\<^sub>e o concat)
+   o L.split
+   o map
+    (\<lambda> Module (ThyName name_old) _ m _ \<Rightarrow>
+         hsk_stmt (case map_prod id nat_of_natural version of (False, _) \<Rightarrow> Datatype_new
+                                                            | (True, 0) \<Rightarrow> Datatype_old
+                                                            | (True, Suc 0) \<Rightarrow> Datatype_old_atomic
+                                                            | (True, Suc (Suc 0)) \<Rightarrow> Datatype_old_atomic_sub)
+                  ((name_old, Some name_new) # l_name)
+                  app_end
+                  m))
+    (if b_concat then l_mod else [last l_mod]))"
 
 end

Citadelle/src/compiler/meta/Meta_META.thy

@@ -144,6 +144,7 @@ record compiler_env_config =  D_output_disable_thy :: bool
                               D_ocl_accessor :: " string\<^sub>b\<^sub>a\<^sub>s\<^sub>e (* name of the constant added *) list (* pre *)
                                                 \<times> string\<^sub>b\<^sub>a\<^sub>s\<^sub>e (* name of the constant added *) list (* post *)"
                               D_ocl_HO_type :: "(string\<^sub>b\<^sub>a\<^sub>s\<^sub>e (* raw HOL name (as key for rbt) *)) list"
+                              D_hsk_constr :: "(string\<^sub>b\<^sub>a\<^sub>s\<^sub>e (* name of the constant added *)) list"
                               D_output_sorry_dirty :: "generation_lemma_mode option \<times> bool (* dirty *)" (* Some Gen_sorry or None and {dirty}: activate sorry mode for skipping proofs *)
 
 subsection\<open>Operations of Fold, Map, ..., on the Meta-Model\<close>
@@ -181,7 +182,7 @@ definition "compiler_env_config_empty output_disable_thy output_header_thy oid_s
     oid_start
     (0, 0)
     design_analysis
-    None [] [] [] False False ([], []) []
+    None [] [] [] False False ([], []) [] []
     sorry_dirty"
 
 definition "compiler_env_config_reset_no_env env =

Citadelle/src/compiler/meta/Parser_META.thy

@@ -64,6 +64,7 @@ definition "compiler_env_config_rec0 f env = f
   (D_output_auto_bootstrap env)
   (D_ocl_accessor env)
   (D_ocl_HO_type env)
+  (D_hsk_constr env)
   (D_output_sorry_dirty env)"
 
 definition "compiler_env_config_rec f env = compiler_env_config_rec0 f env
@@ -71,19 +72,19 @@ definition "compiler_env_config_rec f env = compiler_env_config_rec0 f env
 
 (* *)
 
-lemma [code]: "compiler_env_config.extend = (\<lambda>env v. compiler_env_config_rec0 (co14 (\<lambda>f. f v) compiler_env_config_ext) env)"
+lemma [code]: "compiler_env_config.extend = (\<lambda>env v. compiler_env_config_rec0 (co15 (\<lambda>f. f v) compiler_env_config_ext) env)"
 by(intro ext, simp add: compiler_env_config_rec0_def
                         compiler_env_config.extend_def
-                        co14_def K_def)
-lemma [code]: "compiler_env_config.make = co14 (\<lambda>f. f ()) compiler_env_config_ext"
+                        co15_def K_def)
+lemma [code]: "compiler_env_config.make = co15 (\<lambda>f. f ()) compiler_env_config_ext"
 by(intro ext, simp add: compiler_env_config.make_def
-                        co14_def)
-lemma [code]: "compiler_env_config.truncate = compiler_env_config_rec (co14 K compiler_env_config.make)"
+                        co15_def)
+lemma [code]: "compiler_env_config.truncate = compiler_env_config_rec (co15 K compiler_env_config.make)"
 by(intro ext, simp add: compiler_env_config_rec0_def
                         compiler_env_config_rec_def
                         compiler_env_config.truncate_def
                         compiler_env_config.make_def
-                        co14_def K_def)
+                        co15_def K_def)
 
 subsection\<open>Main\<close>
 
@@ -129,7 +130,7 @@ definition "of_generation_lemma_mode a b = rec_generation_lemma_mode
   (b \<open>Gen_no_dirty\<close>)"
 
 definition "of_compiler_env_config a b f = compiler_env_config_rec
-  (ap15 a (b (ext \<open>compiler_env_config_ext\<close>))
+  (ap16 a (b (ext \<open>compiler_env_config_ext\<close>))
     (of_bool b)
     (of_option a b (of_pair a b (of_string a b) (of_pair a b (of_list a b (of_string a b)) (of_string a b))))
     (of_internal_oids a b)
@@ -143,6 +144,7 @@ definition "of_compiler_env_config a b f = compiler_env_config_rec
     (of_bool b)
     (of_pair a b (of_list a b (of_string\<^sub>b\<^sub>a\<^sub>s\<^sub>e a b)) (of_list a b (of_string\<^sub>b\<^sub>a\<^sub>s\<^sub>e a b)))
     (of_list a b (of_string\<^sub>b\<^sub>a\<^sub>s\<^sub>e a b))
+    (of_list a b (of_string\<^sub>b\<^sub>a\<^sub>s\<^sub>e a b))
     (of_pair a b (of_option a b (of_generation_lemma_mode a b)) (of_bool b))
     (f a b))"
 

Citadelle/src/compiler_generic/meta_isabelle/Parser_init.thy

@@ -80,6 +80,7 @@ definition "ap12 a v0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 v1 v2 v3 v4 v5 v6 v
 definition "ap13 a v0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 = a v0 [f1 v1, f2 v2, f3 v3, f4 v4, f5 v5, f6 v6, f7 v7, f8 v8, f9 v9, f10 v10, f11 v11, f12 v12, f13 v13]"
 definition "ap14 a v0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 = a v0 [f1 v1, f2 v2, f3 v3, f4 v4, f5 v5, f6 v6, f7 v7, f8 v8, f9 v9, f10 v10, f11 v11, f12 v12, f13 v13, f14 v14]"
 definition "ap15 a v0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 = a v0 [f1 v1, f2 v2, f3 v3, f4 v4, f5 v5, f6 v6, f7 v7, f8 v8, f9 v9, f10 v10, f11 v11, f12 v12, f13 v13, f14 v14, f15 v15]"
+definition "ap16 a v0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 = a v0 [f1 v1, f2 v2, f3 v3, f4 v4, f5 v5, f6 v6, f7 v7, f8 v8, f9 v9, f10 v10, f11 v11, f12 v12, f13 v13, f14 v14, f15 v15, f16 v16]"
 
 definition "ar1 a v0 z = a v0 [z]"
 definition "ar2 a v0 f1 v1 z = a v0 [f1 v1, z]"