1.1 --- a/src/HOL/Tools/hologic.ML Tue Jun 08 16:37:22 2010 +0200
1.2 +++ b/src/HOL/Tools/hologic.ML Thu Jun 10 12:24:01 2010 +0200
1.3 @@ -289,42 +289,42 @@
1.4
1.5 (* prod *)
1.6
1.7 -fun mk_prodT (T1, T2) = Type ("*", [T1, T2]);
1.8 +fun mk_prodT (T1, T2) = Type ("Product_Type.*", [T1, T2]);
1.9
1.10 -fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
1.11 +fun dest_prodT (Type ("Product_Type.*", [T1, T2])) = (T1, T2)
1.12 | dest_prodT T = raise TYPE ("dest_prodT", [T], []);
1.13
1.14 -fun pair_const T1 T2 = Const ("Pair", [T1, T2] ---> mk_prodT (T1, T2));
1.15 +fun pair_const T1 T2 = Const ("Product_Type.Pair", [T1, T2] ---> mk_prodT (T1, T2));
1.16
1.17 fun mk_prod (t1, t2) =
1.18 let val T1 = fastype_of t1 and T2 = fastype_of t2 in
1.19 pair_const T1 T2 $ t1 $ t2
1.20 end;
1.21
1.22 -fun dest_prod (Const ("Pair", _) $ t1 $ t2) = (t1, t2)
1.23 +fun dest_prod (Const ("Product_Type.Pair", _) $ t1 $ t2) = (t1, t2)
1.24 | dest_prod t = raise TERM ("dest_prod", [t]);
1.25
1.26 fun mk_fst p =
1.27 let val pT = fastype_of p in
1.28 - Const ("fst", pT --> fst (dest_prodT pT)) $ p
1.29 + Const ("Product_Type.fst", pT --> fst (dest_prodT pT)) $ p
1.30 end;
1.31
1.32 fun mk_snd p =
1.33 let val pT = fastype_of p in
1.34 - Const ("snd", pT --> snd (dest_prodT pT)) $ p
1.35 + Const ("Product_Type.snd", pT --> snd (dest_prodT pT)) $ p
1.36 end;
1.37
1.38 fun split_const (A, B, C) =
1.39 - Const ("split", (A --> B --> C) --> mk_prodT (A, B) --> C);
1.40 + Const ("Product_Type.split", (A --> B --> C) --> mk_prodT (A, B) --> C);
1.41
1.42 fun mk_split t =
1.43 (case Term.fastype_of t of
1.44 T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
1.45 - Const ("split", T --> mk_prodT (A, B) --> C) $ t
1.46 + Const ("Product_Type.split", T --> mk_prodT (A, B) --> C) $ t
1.47 | _ => raise TERM ("mk_split: bad body type", [t]));
1.48
1.49 (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
1.50 -fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
1.51 +fun flatten_tupleT (Type ("Product_Type.*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
1.52 | flatten_tupleT T = [T];
1.53
1.54
1.55 @@ -334,14 +334,14 @@
1.56 | mk_tupleT Ts = foldr1 mk_prodT Ts;
1.57
1.58 fun strip_tupleT (Type ("Product_Type.unit", [])) = []
1.59 - | strip_tupleT (Type ("*", [T1, T2])) = T1 :: strip_tupleT T2
1.60 + | strip_tupleT (Type ("Product_Type.*", [T1, T2])) = T1 :: strip_tupleT T2
1.61 | strip_tupleT T = [T];
1.62
1.63 fun mk_tuple [] = unit
1.64 | mk_tuple ts = foldr1 mk_prod ts;
1.65
1.66 fun strip_tuple (Const ("Product_Type.Unity", _)) = []
1.67 - | strip_tuple (Const ("Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
1.68 + | strip_tuple (Const ("Product_Type.Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
1.69 | strip_tuple t = [t];
1.70
1.71
1.72 @@ -367,14 +367,14 @@
1.73 fun strip_ptupleT ps =
1.74 let
1.75 fun factors p T = if member (op =) ps p then (case T of
1.76 - Type ("*", [T1, T2]) =>
1.77 + Type ("Product_Type.*", [T1, T2]) =>
1.78 factors (1::p) T1 @ factors (2::p) T2
1.79 | _ => ptuple_err "strip_ptupleT") else [T]
1.80 in factors [] end;
1.81
1.82 val flat_tupleT_paths =
1.83 let
1.84 - fun factors p (Type ("*", [T1, T2])) =
1.85 + fun factors p (Type ("Product_Type.*", [T1, T2])) =
1.86 p :: factors (1::p) T1 @ factors (2::p) T2
1.87 | factors p _ = []
1.88 in factors [] end;
1.89 @@ -383,7 +383,7 @@
1.90 let
1.91 fun mk p T ts =
1.92 if member (op =) ps p then (case T of
1.93 - Type ("*", [T1, T2]) =>
1.94 + Type ("Product_Type.*", [T1, T2]) =>
1.95 let
1.96 val (t, ts') = mk (1::p) T1 ts;
1.97 val (u, ts'') = mk (2::p) T2 ts'
1.98 @@ -395,14 +395,14 @@
1.99 fun strip_ptuple ps =
1.100 let
1.101 fun dest p t = if member (op =) ps p then (case t of
1.102 - Const ("Pair", _) $ t $ u =>
1.103 + Const ("Product_Type.Pair", _) $ t $ u =>
1.104 dest (1::p) t @ dest (2::p) u
1.105 | _ => ptuple_err "strip_ptuple") else [t]
1.106 in dest [] end;
1.107
1.108 val flat_tuple_paths =
1.109 let
1.110 - fun factors p (Const ("Pair", _) $ t $ u) =
1.111 + fun factors p (Const ("Product_Type.Pair", _) $ t $ u) =
1.112 p :: factors (1::p) t @ factors (2::p) u
1.113 | factors p _ = []
1.114 in factors [] end;
1.115 @@ -414,7 +414,7 @@
1.116 let
1.117 fun ap ((p, T) :: pTs) =
1.118 if member (op =) ps p then (case T of
1.119 - Type ("*", [T1, T2]) =>
1.120 + Type ("Product_Type.*", [T1, T2]) =>
1.121 split_const (T1, T2, map snd pTs ---> T3) $
1.122 ap ((1::p, T1) :: (2::p, T2) :: pTs)
1.123 | _ => ptuple_err "mk_psplits")
1.124 @@ -427,7 +427,7 @@
1.125 val strip_psplits =
1.126 let
1.127 fun strip [] qs Ts t = (t, rev Ts, qs)
1.128 - | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
1.129 + | strip (p :: ps) qs Ts (Const ("Product_Type.split", _) $ t) =
1.130 strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
1.131 | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
1.132 | strip (p :: ps) qs Ts t = strip ps qs