Added code generator setup.
authorberghofe
Fri Aug 31 16:28:26 2001 +0200 (2001-08-31)
changeset 115330c0d2332e8f0
parent 11532 da74db1373ea
child 11534 0494d0347f18
Added code generator setup.
src/HOL/Main.thy
src/HOL/Recdef.thy
     1.1 --- a/src/HOL/Main.thy	Fri Aug 31 16:27:43 2001 +0200
     1.2 +++ b/src/HOL/Main.thy	Fri Aug 31 16:28:26 2001 +0200
     1.3 @@ -15,4 +15,28 @@
     1.4  lemmas rev_induct [case_names Nil snoc] = rev_induct
     1.5    and rev_cases [case_names Nil snoc] = rev_exhaust
     1.6  
     1.7 +(** configuration of code generator **)
     1.8 +
     1.9 +types_code
    1.10 +  "bool"  ("bool")
    1.11 +  "*"     ("prod")
    1.12 +  "list"  ("list")
    1.13 +
    1.14 +consts_code
    1.15 +  "op ="    ("(_ =/ _)")
    1.16 +
    1.17 +  "True"    ("true")
    1.18 +  "False"   ("false")
    1.19 +  "Not"     ("not")
    1.20 +  "op |"    ("(_ orelse/ _)")
    1.21 +  "op &"    ("(_ andalso/ _)")
    1.22 +  "If"      ("(if _/ then _/ else _)")
    1.23 +
    1.24 +  "Pair"    ("(_,/ _)")
    1.25 +  "fst"     ("fst")
    1.26 +  "snd"     ("snd")
    1.27 +
    1.28 +  "Nil"     ("[]")
    1.29 +  "Cons"    ("(_ ::/ _)")
    1.30 +  
    1.31  end
     2.1 --- a/src/HOL/Recdef.thy	Fri Aug 31 16:27:43 2001 +0200
     2.2 +++ b/src/HOL/Recdef.thy	Fri Aug 31 16:28:26 2001 +0200
     2.3 @@ -15,7 +15,9 @@
     2.4    ("../TFL/thry.ML")
     2.5    ("../TFL/tfl.ML")
     2.6    ("../TFL/post.ML")
     2.7 -  ("Tools/recdef_package.ML"):
     2.8 +  ("Tools/recdef_package.ML")
     2.9 +  ("Tools/basic_codegen.ML")
    2.10 +  ("Tools/inductive_codegen.ML"):
    2.11  
    2.12  lemma tfl_eq_True: "(x = True) --> x"
    2.13    by blast
    2.14 @@ -50,7 +52,11 @@
    2.15  use "../TFL/tfl.ML"
    2.16  use "../TFL/post.ML"
    2.17  use "Tools/recdef_package.ML"
    2.18 +use "Tools/basic_codegen.ML"
    2.19 +use "Tools/inductive_codegen.ML"
    2.20  setup RecdefPackage.setup
    2.21 +setup BasicCodegen.setup
    2.22 +setup InductiveCodegen.setup
    2.23  
    2.24  lemmas [recdef_simp] =
    2.25    inv_image_def