Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dropped outer ROOT structure for generated code
authorhaftmann
Mon, 16 Jul 2007 09:29:03 +0200
changeset 23810 f5e6932d0500
parent 23809 6104514a1f5f
child 23811 b18557301bf9
dropped outer ROOT structure for generated code
src/HOL/Complex/ex/ReflectedFerrack.thy file | annotate | diff | comparison | revisions
src/HOL/Extraction/Higman.thy file | annotate | diff | comparison | revisions
src/HOL/Extraction/Pigeonhole.thy file | annotate | diff | comparison | revisions
src/HOL/Lambda/WeakNorm.thy file | annotate | diff | comparison | revisions
src/HOL/ex/Classpackage.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Jul 16 09:29:02 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Jul 16 09:29:03 2007 +0200
@@ -1993,16 +1993,14 @@
   "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
     (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
 
-code_gen linrqe ferrack_test in SML
-
-ML {* structure Ferrack = struct open ROOT end *}
+code_gen linrqe ferrack_test in SML to Ferrack
 
 (*code_module Ferrack
   contains
     linrqe = linrqe
     test = ferrack_test*)
 
-ML {* Ferrack.ReflectedFerrack.ferrack_test () *}
+ML {* Ferrack.ferrack_test () *}
 
 use "linreif.ML"
 oracle linr_oracle ("term") = ReflectedFerrack.linrqe_oracle
--- a/src/HOL/Extraction/Higman.thy	Mon Jul 16 09:29:02 2007 +0200
+++ b/src/HOL/Extraction/Higman.thy	Mon Jul 16 09:29:03 2007 +0200
@@ -409,12 +409,11 @@
   arbitrary_LT \<equiv> arbitrary_LT'
   arbitrary_TT \<equiv> arbitrary_TT'
 
-code_gen higman_idx in SML
+code_gen higman_idx in SML to Higman
 
 ML {*
 local
-  open ROOT.Higman
-  open ROOT.Nat
+  open Higman
 in
 
 val a = 16807.0;
--- a/src/HOL/Extraction/Pigeonhole.thy	Mon Jul 16 09:29:02 2007 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy	Mon Jul 16 09:29:03 2007 +0200
@@ -285,9 +285,9 @@
 *}
 
 definition
-  "test n = pigeonhole n (\<lambda>m. m - 1)"
+  "test n u = pigeonhole n (\<lambda>m. m - 1)"
 definition
-  "test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
+  "test' n u = pigeonhole_slow n (\<lambda>m. m - 1)"
 definition
   "test'' u = pigeonhole 8 (op ! [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
 
@@ -309,30 +309,30 @@
   test' = test'
   test'' = test''
 
-code_gen test test' test'' in SML
+code_gen test test' test'' in SML to PH2
 
-ML "timeit (fn () => PH.test 10)"
-ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
+ML "timeit (PH.test 10)"
+ML "timeit (PH2.test 10)"
 
-ML "timeit (fn () => PH.test' 10)"
-ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"
+ML "timeit (PH.test' 10)"
+ML "timeit (PH2.test' 10)"
 
-ML "timeit (fn () => PH.test 20)"
-ML "timeit (fn () => ROOT.Pigeonhole.test 20)"
+ML "timeit (PH.test 20)"
+ML "timeit (PH2.test 20)"
 
-ML "timeit (fn () => PH.test' 20)"
-ML "timeit (fn () => ROOT.Pigeonhole.test' 20)"
+ML "timeit (PH.test' 20)"
+ML "timeit (PH2.test' 20)"
 
-ML "timeit (fn () => PH.test 25)"
-ML "timeit (fn () => ROOT.Pigeonhole.test 25)"
+ML "timeit (PH.test 25)"
+ML "timeit (PH2.test 25)"
 
-ML "timeit (fn () => PH.test' 25)"
-ML "timeit (fn () => ROOT.Pigeonhole.test' 25)"
+ML "timeit (PH.test' 25)"
+ML "timeit (PH2.test' 25)"
 
-ML "timeit (fn () => PH.test 500)"
-ML "timeit (fn () => ROOT.Pigeonhole.test 500)"
+ML "timeit (PH.test 500)"
+ML "timeit (PH2.test 500)"
 
 ML "timeit PH.test''"
-ML "timeit ROOT.Pigeonhole.test''"
+ML "timeit PH2.test''"
 
 end
--- a/src/HOL/Lambda/WeakNorm.thy	Mon Jul 16 09:29:02 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Mon Jul 16 09:29:03 2007 +0200
@@ -581,34 +581,29 @@
   int :: "nat \<Rightarrow> int" where
   "int \<equiv> of_nat"
 
-code_gen type_NF nat int in SML
+code_gen type_NF nat int in SML to Norm
 
 ML {*
-structure Norm = ROOT.WeakNorm;
-structure Type = ROOT.Type;
-structure Lambda = ROOT.Lambda;
-structure Nat = ROOT.Nat;
-
-val nat_of_int = ROOT.Integer.nat o IntInf.fromInt;
-val int_of_nat = IntInf.toInt o ROOT.WeakNorm.int;
+val nat_of_int = Norm.nat o IntInf.fromInt;
+val int_of_nat = IntInf.toInt o Norm.int;
 
 fun dBtype_of_typ (Type ("fun", [T, U])) =
-      Type.Fun (dBtype_of_typ T, dBtype_of_typ U)
+      Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)
   | dBtype_of_typ (TFree (s, _)) = (case explode s of
-        ["'", a] => Type.Atom (nat_of_int (ord a - 97))
+        ["'", a] => Norm.Atom (nat_of_int (ord a - 97))
       | _ => error "dBtype_of_typ: variable name")
   | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
 
-fun dB_of_term (Bound i) = Lambda.Var (nat_of_int i)
-  | dB_of_term (t $ u) = Lambda.App (dB_of_term t, dB_of_term u)
-  | dB_of_term (Abs (_, _, t)) = Lambda.Abs (dB_of_term t)
+fun dB_of_term (Bound i) = Norm.Var (nat_of_int i)
+  | dB_of_term (t $ u) = Norm.App (dB_of_term t, dB_of_term u)
+  | dB_of_term (Abs (_, _, t)) = Norm.Abs (dB_of_term t)
   | dB_of_term _ = error "dB_of_term: bad term";
 
-fun term_of_dB Ts (Type ("fun", [T, U])) (Lambda.Abs dBt) =
+fun term_of_dB Ts (Type ("fun", [T, U])) (Norm.Abs dBt) =
       Abs ("x", T, term_of_dB (T :: Ts) U dBt)
   | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
-and term_of_dB' Ts (Lambda.Var n) = Bound (int_of_nat n)
-  | term_of_dB' Ts (Lambda.App (dBt, dBu)) =
+and term_of_dB' Ts (Norm.Var n) = Bound (int_of_nat n)
+  | term_of_dB' Ts (Norm.App (dBt, dBu)) =
       let val t = term_of_dB' Ts dBt
       in case fastype_of1 (Ts, t) of
           Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu
@@ -617,17 +612,17 @@
   | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
 
 fun typing_of_term Ts e (Bound i) =
-      Norm.Var (e, nat_of_int i, dBtype_of_typ (nth Ts i))
+      Norm.Vara (e, nat_of_int i, dBtype_of_typ (nth Ts i))
   | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
-        Type ("fun", [T, U]) => Norm.Appa (e, dB_of_term t,
+        Type ("fun", [T, U]) => Norm.Appaa (e, dB_of_term t,
           dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
           typing_of_term Ts e t, typing_of_term Ts e u)
       | _ => error "typing_of_term: function type expected")
   | typing_of_term Ts e (Abs (s, T, t)) =
       let val dBT = dBtype_of_typ T
-      in Norm.Absa (e, dBT, dB_of_term t,
+      in Norm.Absaa (e, dBT, dB_of_term t,
         dBtype_of_typ (fastype_of1 (T :: Ts, t)),
-        typing_of_term (T :: Ts) (Type.shift e Nat.Zero_nat dBT) t)
+        typing_of_term (T :: Ts) (Norm.shift e Norm.Zero_nat dBT) t)
       end
   | typing_of_term _ _ _ = error "typing_of_term: bad term";
 
@@ -636,11 +631,11 @@
 
 ML {*
 val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
-val (dB1, _) = ROOT.WeakNorm.type_NF (typing_of_term [] dummyf (term_of ct1));
+val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
 val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
 
 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
-val (dB2, _) = ROOT.WeakNorm.type_NF (typing_of_term [] dummyf (term_of ct2));
+val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
 val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
 *}
 
--- a/src/HOL/ex/Classpackage.thy	Mon Jul 16 09:29:02 2007 +0200
+++ b/src/HOL/ex/Classpackage.thy	Mon Jul 16 09:29:03 2007 +0200
@@ -338,6 +338,8 @@
 definition "x2 = X (1::int) 2 3"
 definition "y2 = Y (1::int) 2 3"
 
-code_gen x1 x2 y2 in SML in OCaml file - in Haskell file -
+code_gen x1 x2 y2 in SML to Classpackage
+  in OCaml file -
+  in Haskell file -
 
 end
isabelle