# HG changeset patch # User haftmann # Date 1417804536 -3600 # Node ID a14475f044b2856ddbe7ebb3e8946ea359644bb4 # Parent 788db6d6b8a5f3201fa14e83bcc7197c68d7eebf allow multiple inheritance of targets diff -r 788db6d6b8a5 -r a14475f044b2 src/Doc/Codegen/Adaptation.thy --- a/src/Doc/Codegen/Adaptation.thy Thu Dec 04 16:51:54 2014 +0100 +++ b/src/Doc/Codegen/Adaptation.thy Fri Dec 05 19:35:36 2014 +0100 @@ -2,8 +2,8 @@ imports Setup begin -setup %invisible {* Code_Target.extend_target ("\", ("SML", I)) - #> Code_Target.extend_target ("\", ("Haskell", I)) *} +setup %invisible {* Code_Target.add_derived_target ("\", [("SML", I)]) + #> Code_Target.add_derived_target ("\", [("Haskell", I)]) *} section {* Adaptation to target languages \label{sec:adaptation} *} diff -r 788db6d6b8a5 -r a14475f044b2 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Dec 04 16:51:54 2014 +0100 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Dec 05 19:35:36 2014 +0100 @@ -697,9 +697,9 @@ in -Code_Target.extend_target ("SML_imp", ("SML", imp_program)) -#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) -#> Code_Target.extend_target ("Scala_imp", ("Scala", imp_program)) +Code_Target.add_derived_target ("SML_imp", [("SML", imp_program)]) +#> Code_Target.add_derived_target ("OCaml_imp", [("OCaml", imp_program)]) +#> Code_Target.add_derived_target ("Scala_imp", [("Scala", imp_program)]) end diff -r 788db6d6b8a5 -r a14475f044b2 src/HOL/Quickcheck_Narrowing.thy --- a/src/HOL/Quickcheck_Narrowing.thy Thu Dec 04 16:51:54 2014 +0100 +++ b/src/HOL/Quickcheck_Narrowing.thy Fri Dec 05 19:35:36 2014 +0100 @@ -11,7 +11,7 @@ subsubsection {* Code generation setup *} -setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, I)) *} +setup {* Code_Target.add_derived_target ("Haskell_Quickcheck", [(Code_Haskell.target, I)]) *} code_printing code_module Typerep \ (Haskell_Quickcheck) {* diff -r 788db6d6b8a5 -r a14475f044b2 src/HOL/Quickcheck_Random.thy --- a/src/HOL/Quickcheck_Random.thy Thu Dec 04 16:51:54 2014 +0100 +++ b/src/HOL/Quickcheck_Random.thy Fri Dec 05 19:35:36 2014 +0100 @@ -9,7 +9,7 @@ notation fcomp (infixl "\>" 60) notation scomp (infixl "\\" 60) -setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, I)) *} +setup {* Code_Target.add_derived_target ("Quickcheck", [(Code_Runtime.target, I)]) *} subsection {* Catching Match exceptions *} diff -r 788db6d6b8a5 -r a14475f044b2 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Thu Dec 04 16:51:54 2014 +0100 +++ b/src/Tools/Code/code_haskell.ML Fri Dec 05 19:35:36 2014 +0100 @@ -499,7 +499,7 @@ Toplevel.theory (add_monad target raw_bind))); val setup = - Code_Target.add_target + Code_Target.add_language (target, { serializer = serializer, literals = literals, check = { env_var = "ISABELLE_GHC", make_destination = I, make_command = fn module_name => diff -r 788db6d6b8a5 -r a14475f044b2 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Thu Dec 04 16:51:54 2014 +0100 +++ b/src/Tools/Code/code_ml.ML Fri Dec 05 19:35:36 2014 +0100 @@ -861,13 +861,13 @@ ); val setup = - Code_Target.add_target + Code_Target.add_language (target_SML, { serializer = serializer_sml, literals = literals_sml, check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"), make_command = fn _ => "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } }) - #> Code_Target.add_target + #> Code_Target.add_language (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml, check = { env_var = "ISABELLE_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"), diff -r 788db6d6b8a5 -r a14475f044b2 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Thu Dec 04 16:51:54 2014 +0100 +++ b/src/Tools/Code/code_runtime.ML Fri Dec 05 19:35:36 2014 +0100 @@ -68,7 +68,7 @@ datatype truth = Holds; val _ = Theory.setup - (Code_Target.extend_target (target, (Code_ML.target_SML, I)) + (Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)]) #> Code_Target.set_printings (Type_Constructor (@{type_name prop}, [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))])) #> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds}, diff -r 788db6d6b8a5 -r a14475f044b2 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Thu Dec 04 16:51:54 2014 +0100 +++ b/src/Tools/Code/code_scala.ML Fri Dec 05 19:35:36 2014 +0100 @@ -424,7 +424,7 @@ (** Isar setup **) val setup = - Code_Target.add_target + Code_Target.add_language (target, { serializer = serializer, literals = literals, check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"), diff -r 788db6d6b8a5 -r a14475f044b2 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Dec 04 16:51:54 2014 +0100 +++ b/src/Tools/Code/code_target.ML Fri Dec 05 19:35:36 2014 +0100 @@ -34,12 +34,10 @@ type serializer type literals = Code_Printer.literals - val add_target: string * { serializer: serializer, literals: literals, - check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } } - -> theory -> theory - val extend_target: string * - (string * (Code_Thingol.program -> Code_Thingol.program)) - -> theory -> theory + type language + type ancestry + val add_language: string * language -> theory -> theory + val add_derived_target: string * ancestry -> theory -> theory val assert_target: Proof.context -> string -> string val the_literals: Proof.context -> string -> literals type serialization @@ -208,6 +206,8 @@ fun exists_target thy = Symtab.defined (fst (Targets.get thy)); fun lookup_target_data thy = Symtab.lookup (fst (Targets.get thy)); +fun fold1 f xs = fold f (tl xs) (hd xs); + fun join_ancestry thy target_name = let val the_target_data = the o lookup_target_data thy; @@ -216,8 +216,7 @@ val modifies = rev (map snd ancestry); val modify = fold (curry (op o)) modifies I; val datas = rev (map (snd o the_target_data o fst) ancestry) @ [this_data]; - val data = fold (fn data' => fn data => Code_Printer.merge_data (data, data')) - (tl datas) (hd datas); + val data = fold1 (fn data' => fn data => Code_Printer.merge_data (data, data')) datas; in (modify, (target, data)) end; fun assert_target ctxt target_name = @@ -235,17 +234,26 @@ |> (Targets.map o apfst o Symtab.update) (target_name, (target, Code_Printer.empty_data)) end; -fun add_target (target_name, language) = +fun add_language (target_name, language) = allocate_target target_name { serial = serial (), language = language, ancestry = [] }; -fun extend_target (target_name, (super, modify)) thy = +fun add_derived_target (target_name, initial_ancestry) thy = let - val super_base = case lookup_target_data thy super of - NONE => error ("Unknown code target language: " ^ quote super) - | SOME (super_base, _) => super_base; + val _ = if null initial_ancestry + then error "Must derive from existing target(s)" else (); + fun the_target_data target_name' = case lookup_target_data thy target_name' of + NONE => error ("Unknown code target language: " ^ quote target_name') + | SOME target_data' => target_data'; + val targets = rev (map (fst o the_target_data o fst) initial_ancestry); + val supremum = fold1 (fn target' => fn target => + if #serial target = #serial target' + then target else error "Incompatible targets") targets; + val ancestries = map #ancestry targets @ [initial_ancestry]; + val ancestry = fold1 (fn ancestry' => fn ancestry => + merge_ancestry (ancestry, ancestry')) ancestries; in - allocate_target target_name { serial = #serial super_base, language = #language super_base, - ancestry = (super, modify) :: #ancestry super_base } thy + allocate_target target_name { serial = #serial supremum, language = #language supremum, + ancestry = ancestry } thy end; fun map_data target_name f thy =