allow multiple inheritance of targets
authorhaftmann
Fri Dec 05 19:35:36 2014 +0100 (2014-12-05)
changeset 59104a14475f044b2
parent 59103 788db6d6b8a5
child 59105 18d4e100c267
child 59107 48429ad6d0c8
allow multiple inheritance of targets
src/Doc/Codegen/Adaptation.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Quickcheck_Random.thy
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Doc/Codegen/Adaptation.thy	Thu Dec 04 16:51:54 2014 +0100
     1.2 +++ b/src/Doc/Codegen/Adaptation.thy	Fri Dec 05 19:35:36 2014 +0100
     1.3 @@ -2,8 +2,8 @@
     1.4  imports Setup
     1.5  begin
     1.6  
     1.7 -setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", I))
     1.8 -  #> Code_Target.extend_target ("\<SMLdummy>", ("Haskell", I)) *}
     1.9 +setup %invisible {* Code_Target.add_derived_target ("\<SML>", [("SML", I)])
    1.10 +  #> Code_Target.add_derived_target ("\<SMLdummy>", [("Haskell", I)]) *}
    1.11  
    1.12  section {* Adaptation to target languages \label{sec:adaptation} *}
    1.13  
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Dec 04 16:51:54 2014 +0100
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Dec 05 19:35:36 2014 +0100
     2.3 @@ -697,9 +697,9 @@
     2.4  
     2.5  in
     2.6  
     2.7 -Code_Target.extend_target ("SML_imp", ("SML", imp_program))
     2.8 -#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
     2.9 -#> Code_Target.extend_target ("Scala_imp", ("Scala", imp_program))
    2.10 +Code_Target.add_derived_target ("SML_imp", [("SML", imp_program)])
    2.11 +#> Code_Target.add_derived_target ("OCaml_imp", [("OCaml", imp_program)])
    2.12 +#> Code_Target.add_derived_target ("Scala_imp", [("Scala", imp_program)])
    2.13  
    2.14  end
    2.15  
     3.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Dec 04 16:51:54 2014 +0100
     3.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Dec 05 19:35:36 2014 +0100
     3.3 @@ -11,7 +11,7 @@
     3.4  
     3.5  subsubsection {* Code generation setup *}
     3.6  
     3.7 -setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, I)) *}
     3.8 +setup {* Code_Target.add_derived_target ("Haskell_Quickcheck", [(Code_Haskell.target, I)]) *}
     3.9  
    3.10  code_printing
    3.11    code_module Typerep \<rightharpoonup> (Haskell_Quickcheck) {*
     4.1 --- a/src/HOL/Quickcheck_Random.thy	Thu Dec 04 16:51:54 2014 +0100
     4.2 +++ b/src/HOL/Quickcheck_Random.thy	Fri Dec 05 19:35:36 2014 +0100
     4.3 @@ -9,7 +9,7 @@
     4.4  notation fcomp (infixl "\<circ>>" 60)
     4.5  notation scomp (infixl "\<circ>\<rightarrow>" 60)
     4.6  
     4.7 -setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, I)) *}
     4.8 +setup {* Code_Target.add_derived_target ("Quickcheck", [(Code_Runtime.target, I)]) *}
     4.9  
    4.10  subsection {* Catching Match exceptions *}
    4.11  
     5.1 --- a/src/Tools/Code/code_haskell.ML	Thu Dec 04 16:51:54 2014 +0100
     5.2 +++ b/src/Tools/Code/code_haskell.ML	Fri Dec 05 19:35:36 2014 +0100
     5.3 @@ -499,7 +499,7 @@
     5.4        Toplevel.theory (add_monad target raw_bind)));
     5.5  
     5.6  val setup =
     5.7 -  Code_Target.add_target
     5.8 +  Code_Target.add_language
     5.9      (target, { serializer = serializer, literals = literals,
    5.10        check = { env_var = "ISABELLE_GHC", make_destination = I,
    5.11          make_command = fn module_name =>
     6.1 --- a/src/Tools/Code/code_ml.ML	Thu Dec 04 16:51:54 2014 +0100
     6.2 +++ b/src/Tools/Code/code_ml.ML	Fri Dec 05 19:35:36 2014 +0100
     6.3 @@ -861,13 +861,13 @@
     6.4    );
     6.5  
     6.6  val setup =
     6.7 -  Code_Target.add_target
     6.8 +  Code_Target.add_language
     6.9      (target_SML, { serializer = serializer_sml, literals = literals_sml,
    6.10        check = { env_var = "ISABELLE_PROCESS",
    6.11          make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
    6.12          make_command = fn _ =>
    6.13            "\"$ISABELLE_PROCESS\" -r -q -e 'datatype ref = datatype Unsynchronized.ref; use \"ROOT.ML\" handle _ => exit 1' Pure" } })
    6.14 -  #> Code_Target.add_target
    6.15 +  #> Code_Target.add_language
    6.16      (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
    6.17        check = { env_var = "ISABELLE_OCAML",
    6.18          make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
     7.1 --- a/src/Tools/Code/code_runtime.ML	Thu Dec 04 16:51:54 2014 +0100
     7.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Dec 05 19:35:36 2014 +0100
     7.3 @@ -68,7 +68,7 @@
     7.4  datatype truth = Holds;
     7.5  
     7.6  val _ = Theory.setup
     7.7 -  (Code_Target.extend_target (target, (Code_ML.target_SML, I))
     7.8 +  (Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)])
     7.9    #> Code_Target.set_printings (Type_Constructor (@{type_name prop},
    7.10      [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
    7.11    #> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds},
     8.1 --- a/src/Tools/Code/code_scala.ML	Thu Dec 04 16:51:54 2014 +0100
     8.2 +++ b/src/Tools/Code/code_scala.ML	Fri Dec 05 19:35:36 2014 +0100
     8.3 @@ -424,7 +424,7 @@
     8.4  (** Isar setup **)
     8.5  
     8.6  val setup =
     8.7 -  Code_Target.add_target
     8.8 +  Code_Target.add_language
     8.9      (target, { serializer = serializer, literals = literals,
    8.10        check = { env_var = "SCALA_HOME",
    8.11          make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
     9.1 --- a/src/Tools/Code/code_target.ML	Thu Dec 04 16:51:54 2014 +0100
     9.2 +++ b/src/Tools/Code/code_target.ML	Fri Dec 05 19:35:36 2014 +0100
     9.3 @@ -34,12 +34,10 @@
     9.4  
     9.5    type serializer
     9.6    type literals = Code_Printer.literals
     9.7 -  val add_target: string * { serializer: serializer, literals: literals,
     9.8 -    check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }
     9.9 -    -> theory -> theory
    9.10 -  val extend_target: string *
    9.11 -      (string * (Code_Thingol.program -> Code_Thingol.program))
    9.12 -    -> theory -> theory
    9.13 +  type language
    9.14 +  type ancestry
    9.15 +  val add_language: string * language -> theory -> theory
    9.16 +  val add_derived_target: string * ancestry -> theory -> theory
    9.17    val assert_target: Proof.context -> string -> string
    9.18    val the_literals: Proof.context -> string -> literals
    9.19    type serialization
    9.20 @@ -208,6 +206,8 @@
    9.21  fun exists_target thy = Symtab.defined (fst (Targets.get thy));
    9.22  fun lookup_target_data thy = Symtab.lookup (fst (Targets.get thy));
    9.23  
    9.24 +fun fold1 f xs = fold f (tl xs) (hd xs);
    9.25 +
    9.26  fun join_ancestry thy target_name =
    9.27    let
    9.28      val the_target_data = the o lookup_target_data thy;
    9.29 @@ -216,8 +216,7 @@
    9.30      val modifies = rev (map snd ancestry);
    9.31      val modify = fold (curry (op o)) modifies I;
    9.32      val datas = rev (map (snd o the_target_data o fst) ancestry) @ [this_data];
    9.33 -    val data = fold (fn data' => fn data => Code_Printer.merge_data (data, data'))
    9.34 -      (tl datas) (hd datas);
    9.35 +    val data = fold1 (fn data' => fn data => Code_Printer.merge_data (data, data')) datas;
    9.36    in (modify, (target, data)) end;
    9.37  
    9.38  fun assert_target ctxt target_name =
    9.39 @@ -235,17 +234,26 @@
    9.40      |> (Targets.map o apfst o Symtab.update) (target_name, (target, Code_Printer.empty_data))  
    9.41    end;
    9.42  
    9.43 -fun add_target (target_name, language) =
    9.44 +fun add_language (target_name, language) =
    9.45    allocate_target target_name { serial = serial (), language = language, ancestry = [] };
    9.46  
    9.47 -fun extend_target (target_name, (super, modify)) thy =
    9.48 +fun add_derived_target (target_name, initial_ancestry) thy =
    9.49    let
    9.50 -    val super_base = case lookup_target_data thy super of
    9.51 -      NONE => error ("Unknown code target language: " ^ quote super)
    9.52 -    | SOME (super_base, _) => super_base;
    9.53 +    val _ = if null initial_ancestry
    9.54 +      then error "Must derive from existing target(s)" else ();
    9.55 +    fun the_target_data target_name' = case lookup_target_data thy target_name' of
    9.56 +      NONE => error ("Unknown code target language: " ^ quote target_name')
    9.57 +    | SOME target_data' => target_data';
    9.58 +    val targets = rev (map (fst o the_target_data o fst) initial_ancestry);
    9.59 +    val supremum = fold1 (fn target' => fn target =>
    9.60 +      if #serial target = #serial target'
    9.61 +      then target else error "Incompatible targets") targets;
    9.62 +    val ancestries = map #ancestry targets @ [initial_ancestry];
    9.63 +    val ancestry = fold1 (fn ancestry' => fn ancestry =>
    9.64 +      merge_ancestry (ancestry, ancestry')) ancestries;
    9.65    in
    9.66 -    allocate_target target_name { serial = #serial super_base, language = #language super_base,
    9.67 -      ancestry = (super, modify) :: #ancestry super_base } thy 
    9.68 +    allocate_target target_name { serial = #serial supremum, language = #language supremum,
    9.69 +      ancestry = ancestry } thy 
    9.70    end;
    9.71    
    9.72  fun map_data target_name f thy =