src/HOL/Tools/hologic.ML
changeset 37389 09467cdfa198
parent 37387 3581483cca6c
child 37591 d3daea901123
     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