1.1 --- a/src/HOL/HOL.thy Thu Aug 26 11:33:36 2010 +0200
1.2 +++ b/src/HOL/HOL.thy Thu Aug 26 13:44:50 2010 +0200
1.3 @@ -1924,7 +1924,7 @@
1.4 (Haskell "True" and "False" and "not"
1.5 and infixl 3 "&&" and infixl 2 "||"
1.6 and "!(if (_)/ then (_)/ else (_))")
1.7 - (Scala "true" and "false" and "'!/ _"
1.8 + (Scala "true" and "false" and "'! _"
1.9 and infixl 3 "&&" and infixl 1 "||"
1.10 and "!(if ((_))/ (_)/ else (_))")
1.11
2.1 --- a/src/HOL/Imperative_HOL/Array.thy Thu Aug 26 11:33:36 2010 +0200
2.2 +++ b/src/HOL/Imperative_HOL/Array.thy Thu Aug 26 13:44:50 2010 +0200
2.3 @@ -484,11 +484,11 @@
2.4
2.5 code_type array (Scala "!collection.mutable.ArraySeq[_]")
2.6 code_const Array (Scala "!error(\"bare Array\")")
2.7 -code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
2.8 -code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
2.9 -code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
2.10 -code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
2.11 -code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
2.12 -code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
2.13 +code_const Array.new' (Scala "('_: Unit)/ => / Heap.Array.alloc((_))((_))")
2.14 +code_const Array.make' (Scala "('_: Unit)/ =>/ Heap.Array.make((_))((_))")
2.15 +code_const Array.len' (Scala "('_: Unit)/ =>/ Heap.Array.len((_))")
2.16 +code_const Array.nth' (Scala "('_: Unit)/ =>/ Heap.Array.nth((_), (_))")
2.17 +code_const Array.upd' (Scala "('_: Unit)/ =>/ Heap.Array.upd((_), (_), (_))")
2.18 +code_const Array.freeze (Scala "('_: Unit)/ =>/ Heap.Array.freeze((_))")
2.19
2.20 end
3.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Aug 26 11:33:36 2010 +0200
3.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Aug 26 13:44:50 2010 +0200
3.3 @@ -478,7 +478,6 @@
3.4
3.5 code_include Scala "Heap"
3.6 {*import collection.mutable.ArraySeq
3.7 -import Natural._
3.8
3.9 def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
3.10
3.11 @@ -487,24 +486,33 @@
3.12 }
3.13
3.14 object Ref {
3.15 - def apply[A](x: A): Ref[A] = new Ref[A](x)
3.16 - def lookup[A](r: Ref[A]): A = r.value
3.17 - def update[A](r: Ref[A], x: A): Unit = { r.value = x }
3.18 + def apply[A](x: A): Ref[A] =
3.19 + new Ref[A](x)
3.20 + def lookup[A](r: Ref[A]): A =
3.21 + r.value
3.22 + def update[A](r: Ref[A], x: A): Unit =
3.23 + { r.value = x }
3.24 }
3.25
3.26 object Array {
3.27 - def alloc[A](n: Natural)(x: A): ArraySeq[A] = ArraySeq.fill(n.as_Int)(x)
3.28 - def make[A](n: Natural)(f: Natural => A): ArraySeq[A] = ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k)))
3.29 - def len[A](a: ArraySeq[A]): Natural = Natural(a.length)
3.30 - def nth[A](a: ArraySeq[A], n: Natural): A = a(n.as_Int)
3.31 - def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit = a.update(n.as_Int, x)
3.32 - def freeze[A](a: ArraySeq[A]): List[A] = a.toList
3.33 + def alloc[A](n: Natural.Nat)(x: A): ArraySeq[A] =
3.34 + ArraySeq.fill(n.as_Int)(x)
3.35 + def make[A](n: Natural.Nat)(f: Natural.Nat => A): ArraySeq[A] =
3.36 + ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural.Nat(k)))
3.37 + def len[A](a: ArraySeq[A]): Natural.Nat =
3.38 + Natural.Nat(a.length)
3.39 + def nth[A](a: ArraySeq[A], n: Natural.Nat): A =
3.40 + a(n.as_Int)
3.41 + def upd[A](a: ArraySeq[A], n: Natural.Nat, x: A): Unit =
3.42 + a.update(n.as_Int, x)
3.43 + def freeze[A](a: ArraySeq[A]): List[A] =
3.44 + a.toList
3.45 }*}
3.46
3.47 code_reserved Scala bind Ref Array
3.48
3.49 code_type Heap (Scala "Unit/ =>/ _")
3.50 -code_const bind (Scala "bind")
3.51 +code_const bind (Scala "Heap.bind")
3.52 code_const return (Scala "('_: Unit)/ =>/ _")
3.53 code_const Heap_Monad.raise' (Scala "!error((_))")
3.54
4.1 --- a/src/HOL/Imperative_HOL/Ref.thy Thu Aug 26 11:33:36 2010 +0200
4.2 +++ b/src/HOL/Imperative_HOL/Ref.thy Thu Aug 26 13:44:50 2010 +0200
4.3 @@ -306,10 +306,10 @@
4.4
4.5 text {* Scala *}
4.6
4.7 -code_type ref (Scala "!Ref[_]")
4.8 +code_type ref (Scala "!Heap.Ref[_]")
4.9 code_const Ref (Scala "!error(\"bare Ref\")")
4.10 -code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
4.11 -code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
4.12 -code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
4.13 +code_const ref' (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
4.14 +code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.Ref.lookup((_))")
4.15 +code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.Ref.update((_), (_))")
4.16
4.17 end
5.1 --- a/src/HOL/Library/Code_Integer.thy Thu Aug 26 11:33:36 2010 +0200
5.2 +++ b/src/HOL/Library/Code_Integer.thy Thu Aug 26 13:44:50 2010 +0200
5.3 @@ -51,14 +51,14 @@
5.4 (SML "IntInf.- ((_), 1)")
5.5 (OCaml "Big'_int.pred'_big'_int")
5.6 (Haskell "!(_/ -/ 1)")
5.7 - (Scala "!(_/ -/ 1)")
5.8 + (Scala "!(_ -/ 1)")
5.9 (Eval "!(_/ -/ 1)")
5.10
5.11 code_const Int.succ
5.12 (SML "IntInf.+ ((_), 1)")
5.13 (OCaml "Big'_int.succ'_big'_int")
5.14 (Haskell "!(_/ +/ 1)")
5.15 - (Scala "!(_/ +/ 1)")
5.16 + (Scala "!(_ +/ 1)")
5.17 (Eval "!(_/ +/ 1)")
5.18
5.19 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
6.1 --- a/src/HOL/Library/Code_Natural.thy Thu Aug 26 11:33:36 2010 +0200
6.2 +++ b/src/HOL/Library/Code_Natural.thy Thu Aug 26 13:44:50 2010 +0200
6.3 @@ -54,48 +54,48 @@
6.4
6.5 code_reserved Haskell Natural
6.6
6.7 -code_include Scala "Natural" {*
6.8 -import scala.Math
6.9 +code_include Scala "Natural"
6.10 +{*import scala.Math
6.11
6.12 -object Natural {
6.13 +object Nat {
6.14
6.15 - def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
6.16 - def apply(numeral: Int): Natural = Natural(BigInt(numeral))
6.17 - def apply(numeral: String): Natural = Natural(BigInt(numeral))
6.18 + def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
6.19 + def apply(numeral: Int): Nat = Nat(BigInt(numeral))
6.20 + def apply(numeral: String): Nat = Nat(BigInt(numeral))
6.21
6.22 }
6.23
6.24 -class Natural private(private val value: BigInt) {
6.25 +class Nat private(private val value: BigInt) {
6.26
6.27 override def hashCode(): Int = this.value.hashCode()
6.28
6.29 override def equals(that: Any): Boolean = that match {
6.30 - case that: Natural => this equals that
6.31 + case that: Nat => this equals that
6.32 case _ => false
6.33 }
6.34
6.35 override def toString(): String = this.value.toString
6.36
6.37 - def equals(that: Natural): Boolean = this.value == that.value
6.38 + def equals(that: Nat): Boolean = this.value == that.value
6.39
6.40 def as_BigInt: BigInt = this.value
6.41 def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
6.42 this.value.intValue
6.43 else error("Int value out of range: " + this.value.toString)
6.44
6.45 - def +(that: Natural): Natural = new Natural(this.value + that.value)
6.46 - def -(that: Natural): Natural = Natural(this.value - that.value)
6.47 - def *(that: Natural): Natural = new Natural(this.value * that.value)
6.48 + def +(that: Nat): Nat = new Nat(this.value + that.value)
6.49 + def -(that: Nat): Nat = Nat(this.value - that.value)
6.50 + def *(that: Nat): Nat = new Nat(this.value * that.value)
6.51
6.52 - def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
6.53 + def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
6.54 else {
6.55 val (k, l) = this.value /% that.value
6.56 - (new Natural(k), new Natural(l))
6.57 + (new Nat(k), new Nat(l))
6.58 }
6.59
6.60 - def <=(that: Natural): Boolean = this.value <= that.value
6.61 + def <=(that: Nat): Boolean = this.value <= that.value
6.62
6.63 - def <(that: Natural): Boolean = this.value < that.value
6.64 + def <(that: Nat): Boolean = this.value < that.value
6.65
6.66 }
6.67 *}
6.68 @@ -104,7 +104,7 @@
6.69
6.70 code_type code_numeral
6.71 (Haskell "Natural.Natural")
6.72 - (Scala "Natural")
6.73 + (Scala "Natural.Nat")
6.74
6.75 setup {*
6.76 fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
7.1 --- a/src/HOL/Library/Efficient_Nat.thy Thu Aug 26 11:33:36 2010 +0200
7.2 +++ b/src/HOL/Library/Efficient_Nat.thy Thu Aug 26 13:44:50 2010 +0200
7.3 @@ -242,8 +242,8 @@
7.4 and @{typ int}.
7.5 *}
7.6
7.7 -code_include Haskell "Nat" {*
7.8 -newtype Nat = Nat Integer deriving (Eq, Show, Read);
7.9 +code_include Haskell "Nat"
7.10 +{*newtype Nat = Nat Integer deriving (Eq, Show, Read);
7.11
7.12 instance Num Nat where {
7.13 fromInteger k = Nat (if k >= 0 then k else 0);
7.14 @@ -280,8 +280,8 @@
7.15
7.16 code_reserved Haskell Nat
7.17
7.18 -code_include Scala "Nat" {*
7.19 -import scala.Math
7.20 +code_include Scala "Nat"
7.21 +{*import scala.Math
7.22
7.23 object Nat {
7.24
7.25 @@ -330,7 +330,7 @@
7.26
7.27 code_type nat
7.28 (Haskell "Nat.Nat")
7.29 - (Scala "Nat")
7.30 + (Scala "Nat.Nat")
7.31
7.32 code_instance nat :: eq
7.33 (Haskell -)
7.34 @@ -397,7 +397,7 @@
7.35
7.36 code_const int and nat
7.37 (Haskell "toInteger" and "fromInteger")
7.38 - (Scala "!_.as'_BigInt" and "Nat")
7.39 + (Scala "!_.as'_BigInt" and "Nat.Nat")
7.40
7.41 text {* Conversion from and to code numerals. *}
7.42
7.43 @@ -405,14 +405,14 @@
7.44 (SML "IntInf.toInt")
7.45 (OCaml "_")
7.46 (Haskell "!(fromInteger/ ./ toInteger)")
7.47 - (Scala "!Natural(_.as'_BigInt)")
7.48 + (Scala "!Natural.Nat(_.as'_BigInt)")
7.49 (Eval "_")
7.50
7.51 code_const Code_Numeral.nat_of
7.52 (SML "IntInf.fromInt")
7.53 (OCaml "_")
7.54 (Haskell "!(fromInteger/ ./ toInteger)")
7.55 - (Scala "!Nat(_.as'_BigInt)")
7.56 + (Scala "!Nat.Nat(_.as'_BigInt)")
7.57 (Eval "_")
7.58
7.59 text {* Using target language arithmetic operations whenever appropriate *}
8.1 --- a/src/HOL/ex/Numeral.thy Thu Aug 26 11:33:36 2010 +0200
8.2 +++ b/src/HOL/ex/Numeral.thy Thu Aug 26 13:44:50 2010 +0200
8.3 @@ -1033,14 +1033,14 @@
8.4 (SML "IntInf.- ((_), 1)")
8.5 (OCaml "Big'_int.pred'_big'_int")
8.6 (Haskell "!(_/ -/ 1)")
8.7 - (Scala "!(_/ -/ 1)")
8.8 + (Scala "!(_ -/ 1)")
8.9 (Eval "!(_/ -/ 1)")
8.10
8.11 code_const Int.succ
8.12 (SML "IntInf.+ ((_), 1)")
8.13 (OCaml "Big'_int.succ'_big'_int")
8.14 (Haskell "!(_/ +/ 1)")
8.15 - (Scala "!(_/ +/ 1)")
8.16 + (Scala "!(_ +/ 1)")
8.17 (Eval "!(_/ +/ 1)")
8.18
8.19 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
9.1 --- a/src/Tools/Code/code_haskell.ML Thu Aug 26 11:33:36 2010 +0200
9.2 +++ b/src/Tools/Code/code_haskell.ML Thu Aug 26 13:44:50 2010 +0200
9.3 @@ -344,11 +344,9 @@
9.4 contr_classparam_typs
9.5 (if string_classes then deriving_show else K false);
9.6 fun print_module name content =
9.7 - (name, Pretty.chunks [
9.8 + (name, Pretty.chunks2 [
9.9 str ("module " ^ name ^ " where {"),
9.10 - str "",
9.11 content,
9.12 - str "",
9.13 str "}"
9.14 ]);
9.15 fun serialize_module1 (module_name', (deps, (stmts, _))) =
10.1 --- a/src/Tools/Code/code_scala.ML Thu Aug 26 11:33:36 2010 +0200
10.2 +++ b/src/Tools/Code/code_scala.ML Thu Aug 26 13:44:50 2010 +0200
10.3 @@ -135,7 +135,7 @@
10.4 fun print_context tyvars vs name = applify "[" "]"
10.5 (fn (v, sort) => (Pretty.block o map str)
10.6 (lookup_tyvar tyvars v :: maps (fn sort => [": ", deresolve sort]) sort))
10.7 - NOBR ((str o deresolve) name) vs;
10.8 + NOBR ((str o deresolve_base) name) vs;
10.9 fun print_defhead tyvars vars name vs params tys ty =
10.10 Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
10.11 constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
10.12 @@ -194,7 +194,8 @@
10.13 str "match", str "{"], str "}")
10.14 (map print_clause eqs)
10.15 end;
10.16 - val print_method = (str o Library.enclose "`" "+`" o deresolve_base);
10.17 + val print_method = str o Library.enclose "`" "`" o space_implode "+"
10.18 + o fst o split_last o Long_Name.explode;
10.19 fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
10.20 print_def name (vs, ty) (filter (snd o snd) raw_eqs)
10.21 | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
10.22 @@ -240,7 +241,7 @@
10.23 in
10.24 concat [str "def", constraint (Pretty.block [applify "(" ")"
10.25 (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
10.26 - (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
10.27 + (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_base classparam))
10.28 (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
10.29 add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
10.30 applify "(" ")" (str o lookup_var vars) NOBR
10.31 @@ -281,67 +282,143 @@
10.32 end;
10.33 in print_stmt end;
10.34
10.35 +local
10.36 +
10.37 +(* hierarchical module name space *)
10.38 +
10.39 +datatype node =
10.40 + Dummy
10.41 + | Stmt of Code_Thingol.stmt
10.42 + | Module of ((Name.context * Name.context) * Name.context) * (string list * (string * node) Graph.T);
10.43 +
10.44 +in
10.45 +
10.46 fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
10.47 let
10.48 - val the_module_name = the_default "Program" module_name;
10.49 - val module_alias = K (SOME the_module_name);
10.50 - val reserved = Name.make_context reserved;
10.51 - fun prepare_stmt (name, stmt) (nsps, stmts) =
10.52 +
10.53 + (* building module name hierarchy *)
10.54 + val module_alias = if is_some module_name then K module_name else raw_module_alias;
10.55 + fun alias_fragments name = case module_alias name
10.56 + of SOME name' => Long_Name.explode name'
10.57 + | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
10.58 + (Long_Name.explode name);
10.59 + val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
10.60 + val fragments_tab = fold (fn name => Symtab.update
10.61 + (name, alias_fragments name)) module_names Symtab.empty;
10.62 + val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab);
10.63 +
10.64 + (* building empty module hierarchy *)
10.65 + val empty_module = (((reserved, reserved), reserved), ([], Graph.empty));
10.66 + fun map_module f (Module content) = Module (f content);
10.67 + fun declare_module name_fragement ((nsp_class, nsp_object), nsp_common) =
10.68 let
10.69 - val (_, base) = Code_Printer.dest_name name;
10.70 - val mk_name_stmt = yield_singleton Name.variants;
10.71 - fun add_class ((nsp_class, nsp_object), nsp_common) =
10.72 + val declare = Name.declare name_fragement;
10.73 + in ((declare nsp_class, declare nsp_object), declare nsp_common) end;
10.74 + fun ensure_module name_fragement (nsps, (implicits, nodes)) =
10.75 + if can (Graph.get_node nodes) name_fragement then (nsps, (implicits, nodes))
10.76 + else
10.77 + (nsps |> declare_module name_fragement, (implicits,
10.78 + nodes |> Graph.new_node (name_fragement, (name_fragement, Module empty_module))));
10.79 + fun allocate_module [] = I
10.80 + | allocate_module (name_fragment :: name_fragments) =
10.81 + ensure_module name_fragment
10.82 + #> (apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
10.83 + val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
10.84 + fragments_tab empty_module;
10.85 + fun change_module [] = I
10.86 + | change_module (name_fragment :: name_fragments) =
10.87 + apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module
10.88 + o change_module name_fragments;
10.89 +
10.90 + (* statement declaration *)
10.91 + fun namify_class base ((nsp_class, nsp_object), nsp_common) =
10.92 + let
10.93 + val (base', nsp_class') = yield_singleton Name.variants base nsp_class
10.94 + in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
10.95 + fun namify_object base ((nsp_class, nsp_object), nsp_common) =
10.96 + let
10.97 + val (base', nsp_object') = yield_singleton Name.variants base nsp_object
10.98 + in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
10.99 + fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
10.100 + let
10.101 + val (base', nsp_common') =
10.102 + yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
10.103 + in
10.104 + (base',
10.105 + ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
10.106 + end;
10.107 + fun declare_stmt name stmt =
10.108 + let
10.109 + val (name_fragments, base) = dest_name name;
10.110 + val namify = case stmt
10.111 + of Code_Thingol.Fun _ => namify_object
10.112 + | Code_Thingol.Datatype _ => namify_class
10.113 + | Code_Thingol.Datatypecons _ => namify_common true
10.114 + | Code_Thingol.Class _ => namify_class
10.115 + | Code_Thingol.Classrel _ => namify_object
10.116 + | Code_Thingol.Classparam _ => namify_object
10.117 + | Code_Thingol.Classinst _ => namify_common false;
10.118 + val stmt' = case stmt
10.119 + of Code_Thingol.Datatypecons _ => Dummy
10.120 + | Code_Thingol.Classrel _ => Dummy
10.121 + | Code_Thingol.Classparam _ => Dummy
10.122 + | _ => Stmt stmt;
10.123 + fun is_classinst stmt = case stmt
10.124 + of Code_Thingol.Classinst _ => true
10.125 + | _ => false;
10.126 + val implicit_deps = filter (is_classinst o Graph.get_node program)
10.127 + (Graph.imm_succs program name);
10.128 + fun declaration (nsps, (implicits, nodes)) =
10.129 let
10.130 - val (base', nsp_class') = mk_name_stmt base nsp_class
10.131 - in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
10.132 - fun add_object ((nsp_class, nsp_object), nsp_common) =
10.133 - let
10.134 - val (base', nsp_object') = mk_name_stmt base nsp_object
10.135 - in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
10.136 - fun add_common upper ((nsp_class, nsp_object), nsp_common) =
10.137 - let
10.138 - val (base', nsp_common') =
10.139 - mk_name_stmt (if upper then first_upper base else base) nsp_common
10.140 - in
10.141 - (base',
10.142 - ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
10.143 - end;
10.144 - val add_name = case stmt
10.145 - of Code_Thingol.Fun _ => add_object
10.146 - | Code_Thingol.Datatype _ => add_class
10.147 - | Code_Thingol.Datatypecons _ => add_common true
10.148 - | Code_Thingol.Class _ => add_class
10.149 - | Code_Thingol.Classrel _ => add_object
10.150 - | Code_Thingol.Classparam _ => add_object
10.151 - | Code_Thingol.Classinst _ => add_common false;
10.152 - fun add_stmt base' = case stmt
10.153 - of Code_Thingol.Datatypecons _ => cons (name, (base', NONE))
10.154 - | Code_Thingol.Classrel _ => cons (name, (base', NONE))
10.155 - | Code_Thingol.Classparam _ => cons (name, (base', NONE))
10.156 - | _ => cons (name, (base', SOME stmt));
10.157 - in
10.158 - nsps
10.159 - |> add_name
10.160 - |-> (fn base' => rpair (add_stmt base' stmts))
10.161 - end;
10.162 - val stmts = AList.make (Graph.get_node program) (Graph.strong_conn program |> flat)
10.163 - |> filter_out (Code_Thingol.is_case o snd);
10.164 - val (_, sca_program) = fold prepare_stmt stmts (((reserved, reserved), reserved), []);
10.165 - fun deresolver name = (fst o the o AList.lookup (op =) sca_program) name
10.166 - handle Option => error ("Unknown statement name: " ^ labelled_name name);
10.167 - in (deresolver, (the_module_name, sca_program)) end;
10.168 + val (base', nsps') = namify base nsps;
10.169 + val implicits' = union (op =) implicit_deps implicits;
10.170 + val nodes' = Graph.new_node (name, (base', stmt')) nodes;
10.171 + in (nsps', (implicits', nodes')) end;
10.172 + in change_module name_fragments declaration end;
10.173 +
10.174 + (* dependencies *)
10.175 + fun add_dependency name name' =
10.176 + let
10.177 + val (name_fragments, base) = dest_name name;
10.178 + val (name_fragments', base') = dest_name name';
10.179 + val (name_fragments_common, (diff, diff')) =
10.180 + chop_prefix (op =) (name_fragments, name_fragments');
10.181 + val dep = if null diff then (name, name') else (hd diff, hd diff')
10.182 + in (change_module name_fragments_common o apsnd o apsnd) (Graph.add_edge dep) end;
10.183 +
10.184 + (* producing program *)
10.185 + val (_, (_, sca_program)) = empty_program
10.186 + |> Graph.fold (fn (name, (stmt, _)) => declare_stmt name stmt) program
10.187 + |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
10.188 +
10.189 + (* deresolving *)
10.190 + fun deresolve name =
10.191 + let
10.192 + val (name_fragments, _) = dest_name name;
10.193 + val nodes = fold (fn name_fragement => fn nodes => case Graph.get_node nodes name_fragement
10.194 + of (_, Module (_, (_, nodes))) => nodes) name_fragments sca_program;
10.195 + val (base', _) = Graph.get_node nodes name;
10.196 + in Long_Name.implode (name_fragments @ [base']) end
10.197 + handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name);
10.198 +
10.199 + in (deresolve, sca_program) end;
10.200
10.201 fun serialize_scala raw_module_name labelled_name
10.202 raw_reserved includes raw_module_alias
10.203 _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
10.204 program stmt_names destination =
10.205 let
10.206 +
10.207 + (* generic nonsense *)
10.208 val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
10.209 val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
10.210 +
10.211 + (* preprocess program *)
10.212 val reserved = fold (insert (op =) o fst) includes raw_reserved;
10.213 - val (deresolver, (the_module_name, sca_program)) = scala_program_of_program labelled_name
10.214 - module_name reserved raw_module_alias program;
10.215 - val reserved = make_vars reserved;
10.216 + val (deresolve, sca_program) = scala_program_of_program labelled_name
10.217 + module_name (Name.make_context reserved) raw_module_alias program;
10.218 +
10.219 + (* print statements *)
10.220 fun lookup_constr tyco constr = case Graph.get_node program tyco
10.221 of Code_Thingol.Datatype (_, (_, constrs)) =>
10.222 the (AList.lookup (op = o apsnd fst) constrs constr);
10.223 @@ -359,44 +436,43 @@
10.224 of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
10.225 | _ => false;
10.226 val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
10.227 - reserved args_num is_singleton_constr deresolver;
10.228 - fun print_module name imports content =
10.229 - (name, Pretty.chunks (
10.230 - str ("object " ^ name ^ " {")
10.231 - :: (if null imports then []
10.232 - else str "" :: map (fn name => str ("import " ^ name ^ "._")) imports)
10.233 - @ [str "",
10.234 - content,
10.235 - str "",
10.236 - str "}"]
10.237 - ));
10.238 - fun serialize_module the_module_name sca_program =
10.239 - let
10.240 - val content = Pretty.chunks2 (map_filter
10.241 - (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
10.242 - | (_, (_, NONE)) => NONE) sca_program);
10.243 - in print_module the_module_name (map fst includes) content end;
10.244 - fun check_destination destination =
10.245 - (File.check destination; destination);
10.246 - fun write_module destination (modlname, content) =
10.247 - let
10.248 - val filename = case modlname
10.249 - of "" => Path.explode "Main.scala"
10.250 - | _ => (Path.ext "scala" o Path.explode o implode o separate "/"
10.251 - o Long_Name.explode) modlname;
10.252 - val pathname = Path.append destination filename;
10.253 - val _ = File.mkdir_leaf (Path.dir pathname);
10.254 - in File.write pathname (code_of_pretty content) end
10.255 + (make_vars reserved) args_num is_singleton_constr deresolve;
10.256 +
10.257 + (* print nodes *)
10.258 + fun print_implicits [] = NONE
10.259 + | print_implicits implicits = (SOME o Pretty.block)
10.260 + (str "import /*implicits*/" :: Pretty.brk 1 :: Pretty.commas (map (str o deresolve) implicits));
10.261 + fun print_module base implicits p = Pretty.chunks2
10.262 + ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
10.263 + @ [p, str ("} /* object " ^ base ^ " */")]);
10.264 + fun print_node (_, Dummy) = NONE
10.265 + | print_node (name, Stmt stmt) = if null presentation_stmt_names
10.266 + orelse member (op =) presentation_stmt_names name
10.267 + then SOME (print_stmt (name, stmt))
10.268 + else NONE
10.269 + | print_node (name, Module (_, (implicits, nodes))) = if null presentation_stmt_names
10.270 + then case print_nodes nodes
10.271 + of NONE => NONE
10.272 + | SOME p => SOME (print_module (Long_Name.base_name name) implicits p)
10.273 + else print_nodes nodes
10.274 + and print_nodes nodes = let
10.275 + val ps = map_filter (fn name => print_node (name,
10.276 + snd (Graph.get_node nodes name)))
10.277 + ((rev o flat o Graph.strong_conn) nodes);
10.278 + in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
10.279 +
10.280 + (* serialization *)
10.281 + val p_includes = if null presentation_stmt_names
10.282 + then map (fn (base, p) => print_module base [] p) includes else [];
10.283 + val p = Pretty.chunks2 (p_includes @ the_list (print_nodes sca_program));
10.284 in
10.285 Code_Target.mk_serialization target
10.286 - (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
10.287 - (write_module (check_destination file)))
10.288 - (rpair [] o cat_lines o map (code_of_pretty o snd))
10.289 - (map (fn (name, content) => print_module name [] content) includes
10.290 - @| serialize_module the_module_name sca_program)
10.291 - destination
10.292 + (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
10.293 + (rpair [] o code_of_pretty) p destination
10.294 end;
10.295
10.296 +end; (*local*)
10.297 +
10.298 val literals = let
10.299 fun char_scala c = if c = "'" then "\\'"
10.300 else if c = "\"" then "\\\""
10.301 @@ -412,8 +488,8 @@
10.302 literal_char = Library.enclose "'" "'" o char_scala,
10.303 literal_string = quote o translate_string char_scala,
10.304 literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
10.305 - literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
10.306 - literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
10.307 + literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
10.308 + literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
10.309 literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
10.310 literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
10.311 infix_cons = (6, "::")
10.312 @@ -429,10 +505,10 @@
10.313 val setup =
10.314 Code_Target.add_target
10.315 (target, { serializer = isar_serializer, literals = literals,
10.316 - check = { env_var = "SCALA_HOME", make_destination = I,
10.317 + check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
10.318 make_command = fn scala_home => fn p => fn _ =>
10.319 "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
10.320 - ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
10.321 + ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " " ^ File.shell_path p } })
10.322 #> Code_Target.add_syntax_tyco target "fun"
10.323 (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
10.324 brackify_infix (1, R) fxy (