src/HOL/Tools/datatype_package.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -125,15 +125,15 @@
     1.4  
     1.5  fun constrs_of_sg sg tname = (case datatype_info_sg sg tname of
     1.6     SOME {index, descr, ...} =>
     1.7 -     let val (_, _, constrs) = the (assoc (descr, index))
     1.8 -     in SOME (map (fn (cname, _) => Const (cname, the (Sign.const_type sg cname))) constrs)
     1.9 +     let val (_, _, constrs) = valOf (assoc (descr, index))
    1.10 +     in SOME (map (fn (cname, _) => Const (cname, valOf (Sign.const_type sg cname))) constrs)
    1.11       end
    1.12   | _ => NONE);
    1.13  
    1.14  val constrs_of = constrs_of_sg o Theory.sign_of;
    1.15  
    1.16  fun case_const_of thy tname = (case datatype_info thy tname of
    1.17 -   SOME {case_name, ...} => SOME (Const (case_name, the (Sign.const_type
    1.18 +   SOME {case_name, ...} => SOME (Const (case_name, valOf (Sign.const_type
    1.19       (Theory.sign_of thy) case_name)))
    1.20   | _ => NONE);
    1.21  
    1.22 @@ -169,7 +169,7 @@
    1.23  fun occs_in_prems tacf vars =
    1.24    SUBGOAL (fn (Bi, i) =>
    1.25             (if  exists (fn Free (a, _) => a mem vars)
    1.26 -                      (foldr add_term_frees (#2 (strip_context Bi), []))
    1.27 +                      (Library.foldr add_term_frees (#2 (strip_context Bi), []))
    1.28               then warning "Induction variable occurs also among premises!"
    1.29               else ();
    1.30              tacf i));
    1.31 @@ -182,9 +182,9 @@
    1.32  fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x)
    1.33    | prep_var _ = NONE;
    1.34  
    1.35 -fun prep_inst (concl, xs) =	(*exception LIST*)
    1.36 +fun prep_inst (concl, xs) =	(*exception UnequalLengths *)
    1.37    let val vs = InductAttrib.vars_of concl
    1.38 -  in mapfilter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    1.39 +  in List.mapPartial prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    1.40  
    1.41  in
    1.42  
    1.43 @@ -196,11 +196,11 @@
    1.44        (case opt_rule of
    1.45          SOME r => (r, "Induction rule")
    1.46        | NONE =>
    1.47 -          let val tn = find_tname (hd (mapfilter I (flat varss))) Bi
    1.48 +          let val tn = find_tname (hd (List.mapPartial I (List.concat varss))) Bi
    1.49            in (#induction (datatype_info_sg_err sign tn), "Induction rule for type " ^ tn) end);
    1.50  
    1.51      val concls = HOLogic.dest_concls (Thm.concl_of rule);
    1.52 -    val insts = flat (map prep_inst (concls ~~ varss)) handle LIST _ =>
    1.53 +    val insts = List.concat (map prep_inst (concls ~~ varss)) handle UnequalLengths =>
    1.54        error (rule_name ^ " has different numbers of variables");
    1.55    in occs_in_prems (inst_tac insts rule) (map #2 insts) i state end;
    1.56  
    1.57 @@ -272,20 +272,20 @@
    1.58  local
    1.59  
    1.60  fun dt_recs (DtTFree _) = []
    1.61 -  | dt_recs (DtType (_, dts)) = flat (map dt_recs dts)
    1.62 +  | dt_recs (DtType (_, dts)) = List.concat (map dt_recs dts)
    1.63    | dt_recs (DtRec i) = [i];
    1.64  
    1.65  fun dt_cases (descr: descr) (_, args, constrs) =
    1.66    let
    1.67 -    fun the_bname i = Sign.base_name (#1 (the (assoc (descr, i))));
    1.68 -    val bnames = map the_bname (distinct (flat (map dt_recs args)));
    1.69 +    fun the_bname i = Sign.base_name (#1 (valOf (assoc (descr, i))));
    1.70 +    val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
    1.71    in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
    1.72  
    1.73  
    1.74  fun induct_cases descr =
    1.75 -  DatatypeProp.indexify_names (flat (map (dt_cases descr) (map #2 descr)));
    1.76 +  DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
    1.77  
    1.78 -fun exhaust_cases descr i = dt_cases descr (the (assoc (descr, i)));
    1.79 +fun exhaust_cases descr i = dt_cases descr (valOf (assoc (descr, i)));
    1.80  
    1.81  in
    1.82  
    1.83 @@ -293,18 +293,18 @@
    1.84  
    1.85  fun mk_case_names_exhausts descr new =
    1.86    map (RuleCases.case_names o exhaust_cases descr o #1)
    1.87 -    (filter (fn ((_, (name, _, _))) => name mem_string new) descr);
    1.88 +    (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr);
    1.89  
    1.90  end;
    1.91  
    1.92  fun add_rules simps case_thms size_thms rec_thms inject distinct
    1.93                    weak_case_congs cong_att =
    1.94    (#1 o PureThy.add_thmss [(("simps", simps), []),
    1.95 -    (("", flat case_thms @ size_thms @ 
    1.96 -          flat distinct  @ rec_thms), [Simplifier.simp_add_global]),
    1.97 +    (("", List.concat case_thms @ size_thms @ 
    1.98 +          List.concat distinct  @ rec_thms), [Simplifier.simp_add_global]),
    1.99      (("", size_thms @ rec_thms), [RecfunCodegen.add]),
   1.100 -    (("", flat inject),               [iff_add_global]),
   1.101 -    (("", flat distinct RL [notE]),   [Classical.safe_elim_global]),
   1.102 +    (("", List.concat inject),               [iff_add_global]),
   1.103 +    (("", List.concat distinct RL [notE]),   [Classical.safe_elim_global]),
   1.104      (("", weak_case_congs),           [cong_att])]);
   1.105  
   1.106  
   1.107 @@ -325,7 +325,7 @@
   1.108         (("", exhaustion), [InductAttrib.cases_type_global name])];
   1.109      fun unnamed_rule i =
   1.110        (("", proj i induction), [InductAttrib.induct_type_global ""]);
   1.111 -    val rules = flat (map named_rules infos) @ map unnamed_rule (length infos upto n - 1);
   1.112 +    val rules = List.concat (map named_rules infos) @ map unnamed_rule (length infos upto n - 1);
   1.113    in #1 o PureThy.add_thms rules end;
   1.114  
   1.115  
   1.116 @@ -393,7 +393,7 @@
   1.117  fun case_tr sg [t, u] =
   1.118      let
   1.119        fun case_error s name ts = raise TERM ("Error in case expression" ^
   1.120 -        if_none (apsome (curry op ^ " for datatype ") name) "" ^ ":\n" ^ s, ts);
   1.121 +        getOpt (Option.map (curry op ^ " for datatype ") name, "") ^ ":\n" ^ s, ts);
   1.122        fun dest_case1 (Const ("_case1", _) $ t $ u) = (case strip_comb t of
   1.123              (Const (s, _), ts) => (Sign.intern_const sg s, ts)
   1.124            | (Free (s, _), ts) => (Sign.intern_const sg s, ts)
   1.125 @@ -413,13 +413,13 @@
   1.126              Syntax.const "split" $ abstr (x, abstr (y, body))
   1.127          | abstr (t, _) = case_error "Illegal pattern" NONE [t];
   1.128      in case find_first (fn (_, {descr, index, ...}) =>
   1.129 -      exists (equal cname o fst) (#3 (snd (nth_elem (index, descr))))) tab of
   1.130 +      exists (equal cname o fst) (#3 (snd (List.nth (descr, index))))) tab of
   1.131          NONE => case_error ("Not a datatype constructor: " ^ cname) NONE [u]
   1.132        | SOME (tname, {descr, case_name, index, ...}) =>
   1.133          let
   1.134            val _ = if exists (equal "dummy_pattern" o fst o fst) cases' then
   1.135              case_error "Illegal occurrence of '_' dummy pattern" (SOME tname) [u] else ();
   1.136 -          val (_, (_, dts, constrs)) = nth_elem (index, descr);
   1.137 +          val (_, (_, dts, constrs)) = List.nth (descr, index);
   1.138            val sorts = map (rpair [] o dest_DtTFree) dts;
   1.139            fun find_case (cases, (s, dt)) =
   1.140              (case find_first (equal s o fst o fst) cases' of
   1.141 @@ -431,7 +431,7 @@
   1.142                   if length dt <> length vs then
   1.143                      case_error ("Wrong number of arguments for constructor " ^ s)
   1.144                        (SOME tname) vs
   1.145 -                 else (cases \ c, foldr abstr (vs, t)))
   1.146 +                 else (cases \ c, Library.foldr abstr (vs, t)))
   1.147            val (cases'', fs) = foldl_map find_case (cases', constrs)
   1.148          in case (cases'', length constrs = length cases', default) of
   1.149              ([], true, SOME _) =>
   1.150 @@ -473,7 +473,7 @@
   1.151            NONE => (body, [cname]) :: cs
   1.152          | SOME cnames => overwrite (cs, (body, cnames @ [cname])));
   1.153      val cases' = sort (int_ord o Library.swap o pairself (length o snd))
   1.154 -      (foldl count_cases ([], cases));
   1.155 +      (Library.foldl count_cases ([], cases));
   1.156      fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $
   1.157        list_comb (Syntax.const cname, vs) $ body;
   1.158    in
   1.159 @@ -490,7 +490,7 @@
   1.160               [("dummy_pattern", ([], default), false)]))
   1.161    end;
   1.162  
   1.163 -fun make_case_tr' case_names descr = flat (map
   1.164 +fun make_case_tr' case_names descr = List.concat (map
   1.165    (fn ((_, (_, _, constrs)), case_name) => map (rpair (case_tr' constrs))
   1.166      (NameSpace.accesses' case_name)) (descr ~~ case_names));
   1.167  
   1.168 @@ -542,7 +542,7 @@
   1.169  (********************* axiomatic introduction of datatypes ********************)
   1.170  
   1.171  fun add_and_get_axioms_atts label tnames attss ts thy =
   1.172 -  foldr (fn (((tname, atts), t), (thy', axs)) =>
   1.173 +  Library.foldr (fn (((tname, atts), t), (thy', axs)) =>
   1.174      let
   1.175        val (thy'', [ax]) = thy' |>
   1.176          Theory.add_path tname |>
   1.177 @@ -554,7 +554,7 @@
   1.178    add_and_get_axioms_atts label tnames (replicate (length tnames) []);
   1.179  
   1.180  fun add_and_get_axiomss label tnames tss thy =
   1.181 -  foldr (fn ((tname, ts), (thy', axss)) =>
   1.182 +  Library.foldr (fn ((tname, ts), (thy', axss)) =>
   1.183      let
   1.184        val (thy'', [axs]) = thy' |>
   1.185          Theory.add_path tname |>
   1.186 @@ -565,10 +565,10 @@
   1.187  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
   1.188      case_names_induct case_names_exhausts thy =
   1.189    let
   1.190 -    val descr' = flat descr;
   1.191 +    val descr' = List.concat descr;
   1.192      val recTs = get_rec_types descr' sorts;
   1.193 -    val used = foldr add_typ_tfree_names (recTs, []);
   1.194 -    val newTs = take (length (hd descr), recTs);
   1.195 +    val used = Library.foldr add_typ_tfree_names (recTs, []);
   1.196 +    val newTs = Library.take (length (hd descr), recTs);
   1.197  
   1.198      val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
   1.199        (fn dt => is_rec_type dt andalso not (null (fst (strip_dtyp dt))))
   1.200 @@ -591,7 +591,7 @@
   1.201          (1 upto (length descr')));
   1.202  
   1.203      val size_names = DatatypeProp.indexify_names
   1.204 -      (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs)));
   1.205 +      (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs)));
   1.206  
   1.207      val freeT = TFree (variant used "'t", HOLogic.typeS);
   1.208      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   1.209 @@ -605,7 +605,7 @@
   1.210  
   1.211        (** new types **)
   1.212  
   1.213 -      curry (foldr (fn (((name, mx), tvs), thy') => thy' |>
   1.214 +      curry (Library.foldr (fn (((name, mx), tvs), thy') => thy' |>
   1.215            TypedefPackage.add_typedecls [(name, tvs, mx)]))
   1.216          (types_syntax ~~ tyvars) |>
   1.217        add_path flat_names (space_implode "_" new_type_names) |>
   1.218 @@ -631,12 +631,12 @@
   1.219  
   1.220        (if no_size then I else Theory.add_consts_i (map (fn (s, T) =>
   1.221          (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   1.222 -          (size_names ~~ drop (length (hd descr), recTs)))) |>
   1.223 +          (size_names ~~ Library.drop (length (hd descr), recTs)))) |>
   1.224  
   1.225        (** constructors **)
   1.226  
   1.227        parent_path flat_names |>
   1.228 -      curry (foldr (fn (((((_, (_, _, constrs)), T), tname),
   1.229 +      curry (Library.foldr (fn (((((_, (_, _, constrs)), T), tname),
   1.230          constr_syntax'), thy') => thy' |>
   1.231            add_path flat_names tname |>
   1.232              Theory.add_consts_i (map (fn ((_, cargs), (cname, mx)) =>
   1.233 @@ -686,7 +686,7 @@
   1.234          exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~
   1.235            nchotomys ~~ case_congs ~~ weak_case_congs);
   1.236  
   1.237 -    val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.238 +    val simps = List.concat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.239      val split_thms = split ~~ split_asm;
   1.240  
   1.241      val thy12 = thy11 |>
   1.242 @@ -694,7 +694,7 @@
   1.243        Theory.add_path (space_implode "_" new_type_names) |>
   1.244        add_rules simps case_thms size_thms rec_thms inject distinct
   1.245                  weak_case_congs Simplifier.cong_add_global |> 
   1.246 -      put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   1.247 +      put_datatypes (Library.foldr Symtab.update (dt_infos, dt_info)) |>
   1.248        add_cases_induct dt_infos induct |>
   1.249        Theory.parent_path |>
   1.250        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
   1.251 @@ -741,18 +741,18 @@
   1.252      val (thy11, size_thms) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
   1.253        descr sorts reccomb_names rec_thms thy10;
   1.254  
   1.255 -    val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms)
   1.256 +    val dt_infos = map (make_dt_info (List.concat descr) induct reccomb_names rec_thms)
   1.257        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
   1.258          casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   1.259  
   1.260 -    val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.261 +    val simps = List.concat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.262  
   1.263      val thy12 = thy11 |>
   1.264        Theory.add_advanced_trfuns ([], [], make_case_tr' case_names (hd descr), []) |>
   1.265        Theory.add_path (space_implode "_" new_type_names) |>
   1.266        add_rules simps case_thms size_thms rec_thms inject distinct
   1.267                  weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
   1.268 -      put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   1.269 +      put_datatypes (Library.foldr Symtab.update (dt_infos, dt_info)) |>
   1.270        add_cases_induct dt_infos induct |>
   1.271        Theory.parent_path |>
   1.272        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
   1.273 @@ -778,7 +778,7 @@
   1.274      val _ = Theory.requires thy0 "Inductive" "datatype representations";
   1.275  
   1.276      fun app_thmss srcs thy = foldl_map (fn (thy, x) => apply_theorems x thy) (thy, srcs);
   1.277 -    fun app_thm src thy = apsnd Library.hd (apply_theorems [src] thy);
   1.278 +    fun app_thm src thy = apsnd hd (apply_theorems [src] thy);
   1.279  
   1.280      val (((thy1, induction), inject), distinct) = thy0
   1.281        |> app_thmss raw_distinct
   1.282 @@ -796,7 +796,7 @@
   1.283        | get_typ t = err t;
   1.284  
   1.285      val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induction')));
   1.286 -    val new_type_names = if_none alt_names (map fst dtnames);
   1.287 +    val new_type_names = getOpt (alt_names, map fst dtnames);
   1.288  
   1.289      fun get_constr t = (case Logic.strip_assums_concl t of
   1.290          _ $ (_ $ t') => (case head_of t' of
   1.291 @@ -854,13 +854,13 @@
   1.292        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
   1.293          map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   1.294  
   1.295 -    val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.296 +    val simps = List.concat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.297  
   1.298      val thy11 = thy10 |>
   1.299        Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
   1.300        add_rules simps case_thms size_thms rec_thms inject distinct
   1.301                  weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
   1.302 -      put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   1.303 +      put_datatypes (Library.foldr Symtab.update (dt_infos, dt_info)) |>
   1.304        add_cases_induct dt_infos induction' |>
   1.305        Theory.parent_path |>
   1.306        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
   1.307 @@ -915,8 +915,8 @@
   1.308        let
   1.309          fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) =
   1.310            let
   1.311 -            val (cargs', sorts'') = foldl (prep_typ sign) (([], sorts'), cargs);
   1.312 -            val _ = (case foldr add_typ_tfree_names (cargs', []) \\ tvs of
   1.313 +            val (cargs', sorts'') = Library.foldl (prep_typ sign) (([], sorts'), cargs);
   1.314 +            val _ = (case Library.foldr add_typ_tfree_names (cargs', []) \\ tvs of
   1.315                  [] => ()
   1.316                | vs => error ("Extra type variables on rhs: " ^ commas vs))
   1.317            in (constrs @ [((if flat_names then Sign.full_name sign else
   1.318 @@ -928,7 +928,7 @@
   1.319                " of datatype " ^ tname);
   1.320  
   1.321          val (constrs', constr_syntax', sorts') =
   1.322 -          foldl prep_constr (([], [], sorts), constrs)
   1.323 +          Library.foldl prep_constr (([], [], sorts), constrs)
   1.324  
   1.325        in
   1.326          case duplicates (map fst constrs') of
   1.327 @@ -940,7 +940,7 @@
   1.328               " in datatype " ^ tname)
   1.329        end;
   1.330  
   1.331 -    val (dts', constr_syntax, sorts', i) = foldl prep_dt_spec (([], [], [], 0), dts);
   1.332 +    val (dts', constr_syntax, sorts', i) = Library.foldl prep_dt_spec (([], [], [], 0), dts);
   1.333      val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
   1.334      val dt_info = get_datatypes thy;
   1.335      val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
   1.336 @@ -948,7 +948,7 @@
   1.337        if err then error ("NONEmptiness check failed for datatype " ^ s)
   1.338        else raise exn;
   1.339  
   1.340 -    val descr' = flat descr;
   1.341 +    val descr' = List.concat descr;
   1.342      val case_names_induct = mk_case_names_induct descr';
   1.343      val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
   1.344    in