# HG changeset patch # User haftmann # Date 1184570943 -7200 # Node ID f5e6932d05002ea097fe05e54a899ba7c42657cd # Parent 6104514a1f5f74a915ef81428a3af7be8188ca96 dropped outer ROOT structure for generated code diff -r 6104514a1f5f -r f5e6932d0500 src/HOL/Complex/ex/ReflectedFerrack.thy --- 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 diff -r 6104514a1f5f -r f5e6932d0500 src/HOL/Extraction/Higman.thy --- 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 \ arbitrary_LT' arbitrary_TT \ 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; diff -r 6104514a1f5f -r f5e6932d0500 src/HOL/Extraction/Pigeonhole.thy --- 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 (\m. m - 1)" + "test n u = pigeonhole n (\m. m - 1)" definition - "test' n = pigeonhole_slow n (\m. m - 1)" + "test' n u = pigeonhole_slow n (\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 diff -r 6104514a1f5f -r f5e6932d0500 src/HOL/Lambda/WeakNorm.thy --- 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 \ int" where "int \ 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); *} diff -r 6104514a1f5f -r f5e6932d0500 src/HOL/ex/Classpackage.thy --- 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