src/HOL/Tools/datatype_aux.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4  fun message s = if !quiet_mode then () else writeln s;
     1.5  
     1.6  (* FIXME: move to library ? *)
     1.7 -fun foldl1 f (x::xs) = foldl f (x, xs);
     1.8 +fun foldl1 f (x::xs) = Library.foldl f (x, xs);
     1.9  
    1.10  fun add_path flat_names s = if flat_names then I else Theory.add_path s;
    1.11  fun parent_path flat_names = if flat_names then I else Theory.parent_path;
    1.12 @@ -108,7 +108,7 @@
    1.13  
    1.14  
    1.15  fun cong_tac i st = (case Logic.strip_assums_concl
    1.16 -  (nth_elem (i - 1, prems_of st)) of
    1.17 +  (List.nth (prems_of st, i - 1)) of
    1.18      _ $ (_ $ (f $ x) $ (g $ y)) =>
    1.19        let
    1.20          val cong' = lift_rule (st, i) cong;
    1.21 @@ -128,7 +128,7 @@
    1.22    let
    1.23      val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
    1.24      val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
    1.25 -      (Logic.strip_imp_concl (nth_elem (i - 1, prems_of st))));
    1.26 +      (Logic.strip_imp_concl (List.nth (prems_of st, i - 1))));
    1.27      val getP = if can HOLogic.dest_imp (hd ts) then
    1.28        (apfst SOME) o HOLogic.dest_imp else pair NONE;
    1.29      fun abstr (t1, t2) = (case t1 of
    1.30 @@ -148,14 +148,14 @@
    1.31  fun exh_tac exh_thm_of i state =
    1.32    let
    1.33      val sg = Thm.sign_of_thm state;
    1.34 -    val prem = nth_elem (i - 1, prems_of state);
    1.35 +    val prem = List.nth (prems_of state, i - 1);
    1.36      val params = Logic.strip_params prem;
    1.37      val (_, Type (tname, _)) = hd (rev params);
    1.38      val exhaustion = lift_rule (state, i) (exh_thm_of tname);
    1.39      val prem' = hd (prems_of exhaustion);
    1.40      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
    1.41      val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),
    1.42 -      cterm_of sg (foldr (fn ((_, T), t) => Abs ("z", T, t))
    1.43 +      cterm_of sg (Library.foldr (fn ((_, T), t) => Abs ("z", T, t))
    1.44          (params, Bound 0)))] exhaustion
    1.45    in compose_tac (false, exhaustion', nprems_of exhaustion) i state
    1.46    end;
    1.47 @@ -228,7 +228,7 @@
    1.48  
    1.49  fun name_of_typ (Type (s, Ts)) =
    1.50        let val s' = Sign.base_name s
    1.51 -      in space_implode "_" (filter (not o equal "") (map name_of_typ Ts) @
    1.52 +      in space_implode "_" (List.filter (not o equal "") (map name_of_typ Ts) @
    1.53          [if Syntax.is_identifier s' then s' else "x"])
    1.54        end
    1.55    | name_of_typ _ = "";
    1.56 @@ -242,9 +242,9 @@
    1.57               DtRec (find_index (curry op = tname o fst) new_dts)
    1.58             else error ("Illegal occurence of recursive type " ^ tname));
    1.59  
    1.60 -fun typ_of_dtyp descr sorts (DtTFree a) = TFree (a, the (assoc (sorts, a)))
    1.61 +fun typ_of_dtyp descr sorts (DtTFree a) = TFree (a, valOf (assoc (sorts, a)))
    1.62    | typ_of_dtyp descr sorts (DtRec i) =
    1.63 -      let val (s, ds, _) = the (assoc (descr, i))
    1.64 +      let val (s, ds, _) = valOf (assoc (descr, i))
    1.65        in Type (s, map (typ_of_dtyp descr sorts) ds) end
    1.66    | typ_of_dtyp descr sorts (DtType (s, ds)) =
    1.67        Type (s, map (typ_of_dtyp descr sorts) ds);
    1.68 @@ -252,8 +252,8 @@
    1.69  (* find all non-recursive types in datatype description *)
    1.70  
    1.71  fun get_nonrec_types descr sorts =
    1.72 -  map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
    1.73 -    foldl (fn (Ts', (_, cargs)) =>
    1.74 +  map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
    1.75 +    Library.foldl (fn (Ts', (_, cargs)) =>
    1.76        filter_out is_rec_type cargs union Ts') (Ts, constrs)) ([], descr));
    1.77  
    1.78  (* get all recursive types in datatype description *)
    1.79 @@ -264,22 +264,22 @@
    1.80  (* get all branching types *)
    1.81  
    1.82  fun get_branching_types descr sorts =
    1.83 -  map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
    1.84 -    foldl (fn (Ts', (_, cargs)) => foldr op union (map (fst o strip_dtyp)
    1.85 +  map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
    1.86 +    Library.foldl (fn (Ts', (_, cargs)) => Library.foldr op union (map (fst o strip_dtyp)
    1.87        cargs, Ts')) (Ts, constrs)) ([], descr));
    1.88  
    1.89 -fun get_arities descr = foldl (fn (is, (_, (_, _, constrs))) =>
    1.90 -  foldl (fn (is', (_, cargs)) => map (length o fst o strip_dtyp)
    1.91 -    (filter is_rec_type cargs) union is') (is, constrs)) ([], descr);
    1.92 +fun get_arities descr = Library.foldl (fn (is, (_, (_, _, constrs))) =>
    1.93 +  Library.foldl (fn (is', (_, cargs)) => map (length o fst o strip_dtyp)
    1.94 +    (List.filter is_rec_type cargs) union is') (is, constrs)) ([], descr);
    1.95  
    1.96  (* nonemptiness check for datatypes *)
    1.97  
    1.98  fun check_nonempty descr =
    1.99    let
   1.100 -    val descr' = flat descr;
   1.101 +    val descr' = List.concat descr;
   1.102      fun is_nonempty_dt is i =
   1.103        let
   1.104 -        val (_, _, constrs) = the (assoc (descr', i));
   1.105 +        val (_, _, constrs) = valOf (assoc (descr', i));
   1.106          fun arg_nonempty (_, DtRec i) = if i mem is then false
   1.107                else is_nonempty_dt (i::is) i
   1.108            | arg_nonempty _ = true;
   1.109 @@ -303,8 +303,8 @@
   1.110           NONE => typ_error T (tname ^ " is not a datatype - can't use it in\
   1.111             \ nested recursion")
   1.112         | (SOME {index, descr, ...}) =>
   1.113 -           let val (_, vars, _) = the (assoc (descr, index));
   1.114 -               val subst = ((map dest_DtTFree vars) ~~ dts) handle LIST _ =>
   1.115 +           let val (_, vars, _) = valOf (assoc (descr, index));
   1.116 +               val subst = ((map dest_DtTFree vars) ~~ dts) handle UnequalLengths =>
   1.117                   typ_error T ("Type constructor " ^ tname ^ " used with wrong\
   1.118                    \ number of arguments")
   1.119             in (i + index, map (fn (j, (tn, args, cs)) => (i + j,
   1.120 @@ -333,18 +333,18 @@
   1.121      (* unfold a constructor *)
   1.122  
   1.123      fun unfold_constr ((i, constrs, descrs), (cname, cargs)) =
   1.124 -      let val (i', cargs', descrs') = foldl unfold_arg ((i, [], descrs), cargs)
   1.125 +      let val (i', cargs', descrs') = Library.foldl unfold_arg ((i, [], descrs), cargs)
   1.126        in (i', constrs @ [(cname, cargs')], descrs') end;
   1.127  
   1.128      (* unfold a single datatype *)
   1.129  
   1.130      fun unfold_datatype ((i, dtypes, descrs), (j, (tname, tvars, constrs))) =
   1.131        let val (i', constrs', descrs') =
   1.132 -        foldl unfold_constr ((i, [], descrs), constrs)
   1.133 +        Library.foldl unfold_constr ((i, [], descrs), constrs)
   1.134        in (i', dtypes @ [(j, (tname, tvars, constrs'))], descrs')
   1.135        end;
   1.136  
   1.137 -    val (i', descr', descrs) = foldl unfold_datatype ((i, [],[]), descr);
   1.138 +    val (i', descr', descrs) = Library.foldl unfold_datatype ((i, [],[]), descr);
   1.139  
   1.140    in (descr' :: descrs, i') end;
   1.141