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
This commit is contained in:
Frédéric Tuong 2019-01-10 18:37:56 +00:00
parent 369279e7d1
commit b2db24200a
4 changed files with 56 additions and 46 deletions

View File

@ -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

View File

@ -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 =

View File

@ -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))"

View File

@ -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]"