src/HOL/Tools/refute.ML
changeset 33968 f94fb13ecbb3
parent 33955 fff6f11b1f09
child 34017 ef2776c89799
     1.1 --- a/src/HOL/Tools/refute.ML	Mon Nov 30 11:42:48 2009 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Nov 30 11:42:49 2009 +0100
     1.3 @@ -406,12 +406,12 @@
     1.4  (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
     1.5  (* ------------------------------------------------------------------------- *)
     1.6  
     1.7 -  fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
     1.8 +  fun typ_of_dtyp descr typ_assoc (Datatype_Aux.DtTFree a) =
     1.9      (* replace a 'DtTFree' variable by the associated type *)
    1.10 -    the (AList.lookup (op =) typ_assoc (DatatypeAux.DtTFree a))
    1.11 -    | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
    1.12 +    the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a))
    1.13 +    | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, ds)) =
    1.14      Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.15 -    | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
    1.16 +    | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) =
    1.17      let
    1.18        val (s, ds, _) = the (AList.lookup (op =) descr i)
    1.19      in
    1.20 @@ -946,7 +946,7 @@
    1.21              (* sanity check: every element in 'dtyps' must be a *)
    1.22              (* 'DtTFree'                                        *)
    1.23              val _ = if Library.exists (fn d =>
    1.24 -              case d of DatatypeAux.DtTFree _ => false | _ => true) typs then
    1.25 +              case d of Datatype_Aux.DtTFree _ => false | _ => true) typs then
    1.26                raise REFUTE ("ground_types", "datatype argument (for type "
    1.27                  ^ Syntax.string_of_typ_global thy T ^ ") is not a variable")
    1.28              else ()
    1.29 @@ -958,11 +958,11 @@
    1.30                val dT = typ_of_dtyp descr typ_assoc d
    1.31              in
    1.32                case d of
    1.33 -                DatatypeAux.DtTFree _ =>
    1.34 +                Datatype_Aux.DtTFree _ =>
    1.35                  collect_types dT acc
    1.36 -              | DatatypeAux.DtType (_, ds) =>
    1.37 +              | Datatype_Aux.DtType (_, ds) =>
    1.38                  collect_types dT (fold_rev collect_dtyp ds acc)
    1.39 -              | DatatypeAux.DtRec i =>
    1.40 +              | Datatype_Aux.DtRec i =>
    1.41                  if dT mem acc then
    1.42                    acc  (* prevent infinite recursion *)
    1.43                  else
    1.44 @@ -971,7 +971,7 @@
    1.45                      (* if the current type is a recursive IDT (i.e. a depth *)
    1.46                      (* is required), add it to 'acc'                        *)
    1.47                      val acc_dT = if Library.exists (fn (_, ds) =>
    1.48 -                      Library.exists DatatypeAux.is_rec_type ds) dconstrs then
    1.49 +                      Library.exists Datatype_Aux.is_rec_type ds) dconstrs then
    1.50                          insert (op =) dT acc
    1.51                        else acc
    1.52                      (* collect argument types *)
    1.53 @@ -985,7 +985,7 @@
    1.54            in
    1.55              (* argument types 'Ts' could be added here, but they are also *)
    1.56              (* added by 'collect_dtyp' automatically                      *)
    1.57 -            collect_dtyp (DatatypeAux.DtRec index) acc
    1.58 +            collect_dtyp (Datatype_Aux.DtRec index) acc
    1.59            end
    1.60          | NONE =>
    1.61            (* not an inductive datatype, e.g. defined via "typedef" or *)
    1.62 @@ -1157,7 +1157,7 @@
    1.63              in
    1.64                (* recursive datatype? *)
    1.65                Library.exists (fn (_, ds) =>
    1.66 -                Library.exists DatatypeAux.is_rec_type ds) constrs
    1.67 +                Library.exists Datatype_Aux.is_rec_type ds) constrs
    1.68              end
    1.69            | NONE => false)
    1.70          | _ => false) types
    1.71 @@ -1952,7 +1952,7 @@
    1.72                val typ_assoc           = dtyps ~~ Ts
    1.73                (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
    1.74                val _ = if Library.exists (fn d =>
    1.75 -                  case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
    1.76 +                  case d of Datatype_Aux.DtTFree _ => false | _ => true) dtyps
    1.77                  then
    1.78                    raise REFUTE ("IDT_interpreter",
    1.79                      "datatype argument (for type "
    1.80 @@ -2076,7 +2076,7 @@
    1.81                val typ_assoc           = dtyps ~~ Ts
    1.82                (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
    1.83                val _ = if Library.exists (fn d =>
    1.84 -                  case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
    1.85 +                  case d of Datatype_Aux.DtTFree _ => false | _ => true) dtyps
    1.86                  then
    1.87                    raise REFUTE ("IDT_constructor_interpreter",
    1.88                      "datatype argument (for type "
    1.89 @@ -2135,7 +2135,7 @@
    1.90                val typ_assoc           = dtyps ~~ Ts'
    1.91                (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
    1.92                val _ = if Library.exists (fn d =>
    1.93 -                  case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
    1.94 +                  case d of Datatype_Aux.DtTFree _ => false | _ => true) dtyps
    1.95                  then
    1.96                    raise REFUTE ("IDT_constructor_interpreter",
    1.97                      "datatype argument (for type "
    1.98 @@ -2350,7 +2350,7 @@
    1.99                    (* sanity check: every element in 'dtyps' must be a *)
   1.100                    (*               'DtTFree'                          *)
   1.101                    val _ = if Library.exists (fn d =>
   1.102 -                    case d of DatatypeAux.DtTFree _ => false
   1.103 +                    case d of Datatype_Aux.DtTFree _ => false
   1.104                              | _ => true) dtyps
   1.105                      then
   1.106                        raise REFUTE ("IDT_recursion_interpreter",
   1.107 @@ -2372,10 +2372,10 @@
   1.108                      (case AList.lookup op= acc d of
   1.109                        NONE =>
   1.110                        (case d of
   1.111 -                        DatatypeAux.DtTFree _ =>
   1.112 +                        Datatype_Aux.DtTFree _ =>
   1.113                          (* add the association, proceed *)
   1.114                          rec_typ_assoc ((d, T)::acc) xs
   1.115 -                      | DatatypeAux.DtType (s, ds) =>
   1.116 +                      | Datatype_Aux.DtType (s, ds) =>
   1.117                          let
   1.118                            val (s', Ts) = dest_Type T
   1.119                          in
   1.120 @@ -2385,7 +2385,7 @@
   1.121                              raise REFUTE ("IDT_recursion_interpreter",
   1.122                                "DtType/Type mismatch")
   1.123                          end
   1.124 -                      | DatatypeAux.DtRec i =>
   1.125 +                      | Datatype_Aux.DtRec i =>
   1.126                          let
   1.127                            val (_, ds, _) = the (AList.lookup (op =) descr i)
   1.128                            val (_, Ts)    = dest_Type T
   1.129 @@ -2401,7 +2401,7 @@
   1.130                          raise REFUTE ("IDT_recursion_interpreter",
   1.131                            "different type associations for the same dtyp"))
   1.132                    val typ_assoc = filter
   1.133 -                    (fn (DatatypeAux.DtTFree _, _) => true | (_, _) => false)
   1.134 +                    (fn (Datatype_Aux.DtTFree _, _) => true | (_, _) => false)
   1.135                      (rec_typ_assoc []
   1.136                        (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
   1.137                    (* sanity check: typ_assoc must associate types to the   *)
   1.138 @@ -2417,7 +2417,7 @@
   1.139                    val mc_intrs = map (fn (idx, (_, _, cs)) =>
   1.140                      let
   1.141                        val c_return_typ = typ_of_dtyp descr typ_assoc
   1.142 -                        (DatatypeAux.DtRec idx)
   1.143 +                        (Datatype_Aux.DtRec idx)
   1.144                      in
   1.145                        (idx, map (fn (cname, cargs) =>
   1.146                          (#1 o interpret thy (typs, []) {maxvars=0,
   1.147 @@ -2471,7 +2471,7 @@
   1.148                    val _ = map (fn (idx, intrs) =>
   1.149                      let
   1.150                        val T = typ_of_dtyp descr typ_assoc
   1.151 -                        (DatatypeAux.DtRec idx)
   1.152 +                        (Datatype_Aux.DtRec idx)
   1.153                      in
   1.154                        if length intrs <> size_of_type thy (typs, []) T then
   1.155                          raise REFUTE ("IDT_recursion_interpreter",
   1.156 @@ -2552,7 +2552,7 @@
   1.157                          val (_, _, constrs) = the (AList.lookup (op =) descr idx)
   1.158                          val (_, dtyps)      = List.nth (constrs, c)
   1.159                          val rec_dtyps_args  = filter
   1.160 -                          (DatatypeAux.is_rec_type o fst) (dtyps ~~ args)
   1.161 +                          (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args)
   1.162                          (* map those indices to interpretations *)
   1.163                          val rec_dtyps_intrs = map (fn (dtyp, arg) =>
   1.164                            let
   1.165 @@ -2565,18 +2565,18 @@
   1.166                          (* takes the dtyp and interpretation of an element, *)
   1.167                          (* and computes the interpretation for the          *)
   1.168                          (* corresponding recursive argument                 *)
   1.169 -                        fun rec_intr (DatatypeAux.DtRec i) (Leaf xs) =
   1.170 +                        fun rec_intr (Datatype_Aux.DtRec i) (Leaf xs) =
   1.171                            (* recursive argument is "rec_i params elem" *)
   1.172                            compute_array_entry i (find_index (fn x => x = True) xs)
   1.173 -                          | rec_intr (DatatypeAux.DtRec _) (Node _) =
   1.174 +                          | rec_intr (Datatype_Aux.DtRec _) (Node _) =
   1.175                            raise REFUTE ("IDT_recursion_interpreter",
   1.176                              "interpretation for IDT is a node")
   1.177 -                          | rec_intr (DatatypeAux.DtType ("fun", [dt1, dt2]))
   1.178 +                          | rec_intr (Datatype_Aux.DtType ("fun", [dt1, dt2]))
   1.179                              (Node xs) =
   1.180                            (* recursive argument is something like     *)
   1.181                            (* "\<lambda>x::dt1. rec_? params (elem x)" *)
   1.182                            Node (map (rec_intr dt2) xs)
   1.183 -                          | rec_intr (DatatypeAux.DtType ("fun", [_, _]))
   1.184 +                          | rec_intr (Datatype_Aux.DtType ("fun", [_, _]))
   1.185                              (Leaf _) =
   1.186                            raise REFUTE ("IDT_recursion_interpreter",
   1.187                              "interpretation for function dtyp is a leaf")
   1.188 @@ -3169,7 +3169,7 @@
   1.189            val typ_assoc           = dtyps ~~ Ts
   1.190            (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   1.191            val _ = if Library.exists (fn d =>
   1.192 -              case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
   1.193 +              case d of Datatype_Aux.DtTFree _ => false | _ => true) dtyps
   1.194              then
   1.195                raise REFUTE ("IDT_printer", "datatype argument (for type " ^
   1.196                  Syntax.string_of_typ_global thy (Type (s, Ts)) ^ ") is not a variable")