src/HOL/Tools/datatype_package.ML
changeset 21045 66d6d1b0ddfa
parent 20820 58693343905f
child 21127 c8e862897d13
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Oct 16 14:07:20 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Oct 16 14:07:21 2006 +0200
     1.3 @@ -167,8 +167,8 @@
     1.4    usually signals a mistake.  But calls the tactic either way!*)
     1.5  fun occs_in_prems tacf vars =
     1.6    SUBGOAL (fn (Bi, i) =>
     1.7 -           (if  exists (fn Free (a, _) => a mem vars)
     1.8 -                      (foldr add_term_frees [] (#2 (strip_context Bi)))
     1.9 +           (if exists (fn (a, _) => member (op =) vars a)
    1.10 +                      (fold Term.add_frees (#2 (strip_context Bi)) [])
    1.11               then warning "Induction variable occurs also among premises!"
    1.12               else ();
    1.13              tacf i));
    1.14 @@ -181,9 +181,9 @@
    1.15  fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x)
    1.16    | prep_var _ = NONE;
    1.17  
    1.18 -fun prep_inst (concl, xs) =	(*exception Library.UnequalLengths *)
    1.19 +fun prep_inst (concl, xs) = (*exception Library.UnequalLengths*)
    1.20    let val vs = InductAttrib.vars_of concl
    1.21 -  in List.mapPartial prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    1.22 +  in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    1.23  
    1.24  in
    1.25  
    1.26 @@ -192,21 +192,21 @@
    1.27    let
    1.28      val (rule, rule_name) =
    1.29        case opt_rule of
    1.30 -	  SOME r => (r, "Induction rule")
    1.31 -	| NONE =>
    1.32 -	    let val tn = find_tname (hd (List.mapPartial I (List.concat varss))) Bi
    1.33 +          SOME r => (r, "Induction rule")
    1.34 +        | NONE =>
    1.35 +            let val tn = find_tname (hd (map_filter I (flat varss))) Bi
    1.36                  val {sign, ...} = Thm.rep_thm state
    1.37 -	    in (#induction (the_datatype sign tn), "Induction rule for type " ^ tn) 
    1.38 -	    end
    1.39 +            in (#induction (the_datatype sign tn), "Induction rule for type " ^ tn) 
    1.40 +            end
    1.41      val concls = HOLogic.dest_concls (Thm.concl_of rule);
    1.42 -    val insts = List.concat (map prep_inst (concls ~~ varss)) handle Library.UnequalLengths =>
    1.43 +    val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
    1.44        error (rule_name ^ " has different numbers of variables");
    1.45    in occs_in_prems (inst_tac insts rule) (map #2 insts) i end)
    1.46    i state;
    1.47  
    1.48  fun induct_tac s =
    1.49    gen_induct_tac Tactic.res_inst_tac'
    1.50 -    (map (Library.single o SOME) (Syntax.read_idents s), NONE);
    1.51 +    (map (single o SOME) (Syntax.read_idents s), NONE);
    1.52  
    1.53  fun induct_thm_tac th s =
    1.54    gen_induct_tac Tactic.res_inst_tac'
    1.55 @@ -273,20 +273,20 @@
    1.56  local
    1.57  
    1.58  fun dt_recs (DtTFree _) = []
    1.59 -  | dt_recs (DtType (_, dts)) = List.concat (map dt_recs dts)
    1.60 +  | dt_recs (DtType (_, dts)) = maps dt_recs dts
    1.61    | dt_recs (DtRec i) = [i];
    1.62  
    1.63  fun dt_cases (descr: descr) (_, args, constrs) =
    1.64    let
    1.65 -    fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
    1.66 -    val bnames = map the_bname (distinct (op =) (List.concat (map dt_recs args)));
    1.67 +    fun the_bname i = Sign.base_name (#1 (the (AList.lookup (op =) descr i)));
    1.68 +    val bnames = map the_bname (distinct (op =) (maps dt_recs args));
    1.69    in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
    1.70  
    1.71  
    1.72  fun induct_cases descr =
    1.73 -  DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
    1.74 +  DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
    1.75  
    1.76 -fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
    1.77 +fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
    1.78  
    1.79  in
    1.80  
    1.81 @@ -294,7 +294,7 @@
    1.82  
    1.83  fun mk_case_names_exhausts descr new =
    1.84    map (RuleCases.case_names o exhaust_cases descr o #1)
    1.85 -    (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr);
    1.86 +    (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
    1.87  
    1.88  end;
    1.89  
    1.90 @@ -306,11 +306,11 @@
    1.91  fun add_rules simps case_thms size_thms rec_thms inject distinct
    1.92                    weak_case_congs cong_att =
    1.93    (snd o PureThy.add_thmss [(("simps", simps), []),
    1.94 -    (("", List.concat case_thms @ size_thms @ 
    1.95 -          List.concat distinct  @ rec_thms), [Simplifier.simp_add]),
    1.96 +    (("", flat case_thms @ size_thms @ 
    1.97 +          flat distinct @ rec_thms), [Simplifier.simp_add]),
    1.98      (("", size_thms @ rec_thms),             [setmp CodegenData.strict_functyp false (RecfunCodegen.add NONE)]),
    1.99 -    (("", List.concat inject),               [iff_add]),
   1.100 -    (("", map name_notE (List.concat distinct)),  [Classical.safe_elim NONE]),
   1.101 +    (("", flat inject),               [iff_add]),
   1.102 +    (("", map name_notE (flat distinct)),  [Classical.safe_elim NONE]),
   1.103      (("", weak_case_congs),                  [cong_att])]);
   1.104  
   1.105  
   1.106 @@ -327,7 +327,7 @@
   1.107        (("", nth inducts i), [PureThy.kind_internal, InductAttrib.induct_type ""]);
   1.108    in
   1.109      thy |> PureThy.add_thms
   1.110 -      (List.concat (map named_rules infos) @
   1.111 +      (maps named_rules infos @
   1.112          map unnamed_rule (length infos upto length inducts - 1)) |> snd
   1.113      |> PureThy.add_thmss [(("inducts", inducts), [])] |> snd
   1.114    end;
   1.115 @@ -396,8 +396,6 @@
   1.116  
   1.117  (**** translation rules for case ****)
   1.118  
   1.119 -fun find_first f = Library.find_first f;
   1.120 -
   1.121  fun case_tr context [t, u] =
   1.122      let
   1.123        val thy = Context.theory_of context;
   1.124 @@ -415,34 +413,34 @@
   1.125        val (cases', default) = (case split_last cases of
   1.126            (cases', (("dummy_pattern", []), t)) => (cases', SOME t)
   1.127          | _ => (cases, NONE))
   1.128 -      fun abstr (Free (x, T), body) = Term.absfree (x, T, body)
   1.129 -        | abstr (Const ("_constrain", _) $ Free (x, T) $ tT, body) =
   1.130 +      fun abstr (Free (x, T)) body = Term.absfree (x, T, body)
   1.131 +        | abstr (Const ("_constrain", _) $ Free (x, T) $ tT) body =
   1.132              Syntax.const Syntax.constrainAbsC $ Term.absfree (x, T, body) $ tT
   1.133 -        | abstr (Const ("Pair", _) $ x $ y, body) =
   1.134 -            Syntax.const "split" $ abstr (x, abstr (y, body))
   1.135 -        | abstr (t, _) = case_error "Illegal pattern" NONE [t];
   1.136 +        | abstr (Const ("Pair", _) $ x $ y) body =
   1.137 +            Syntax.const "split" $ (abstr x o abstr y) body
   1.138 +        | abstr t _ = case_error "Illegal pattern" NONE [t];
   1.139      in case find_first (fn (_, {descr, index, ...}) =>
   1.140 -      exists (equal cname o fst) (#3 (snd (List.nth (descr, index))))) tab of
   1.141 +      exists (equal cname o fst) (#3 (snd (nth descr index)))) tab of
   1.142          NONE => case_error ("Not a datatype constructor: " ^ cname) NONE [u]
   1.143        | SOME (tname, {descr, sorts, case_name, index, ...}) =>
   1.144          let
   1.145            val _ = if exists (equal "dummy_pattern" o fst o fst) cases' then
   1.146              case_error "Illegal occurrence of '_' dummy pattern" (SOME tname) [u] else ();
   1.147 -          val (_, (_, dts, constrs)) = List.nth (descr, index);
   1.148 -          fun find_case (cases, (s, dt)) =
   1.149 +          val (_, (_, dts, constrs)) = nth descr index;
   1.150 +          fun find_case (s, dt) cases =
   1.151              (case find_first (equal s o fst o fst) cases' of
   1.152 -               NONE => (cases, list_abs (map (rpair dummyT)
   1.153 +               NONE => (list_abs (map (rpair dummyT)
   1.154                   (DatatypeProp.make_tnames (map (typ_of_dtyp descr sorts) dt)),
   1.155                   case default of
   1.156                     NONE => (warning ("No clause for constructor " ^ s ^
   1.157                       " in case expression"); Const ("undefined", dummyT))
   1.158 -                 | SOME t => t))
   1.159 +                 | SOME t => t), cases)
   1.160               | SOME (c as ((_, vs), t)) =>
   1.161                   if length dt <> length vs then
   1.162                      case_error ("Wrong number of arguments for constructor " ^ s)
   1.163                        (SOME tname) vs
   1.164 -                 else (cases \ c, foldr abstr t vs))
   1.165 -          val (cases'', fs) = foldl_map find_case (cases', constrs)
   1.166 +                 else (fold_rev abstr vs t, remove (op =) c cases))
   1.167 +          val (fs, cases'') = fold_map find_case constrs cases'
   1.168          in case (cases'', length constrs = length cases', default) of
   1.169              ([], true, SOME _) =>
   1.170                case_error "Extra '_' dummy pattern" (SOME tname) [u]
   1.171 @@ -478,13 +476,12 @@
   1.172        (Sign.extern_const (Context.theory_of context) cname,
   1.173         strip_abs (length dts) t, is_dependent (length dts) t))
   1.174        (constrs ~~ fs);
   1.175 -    fun count_cases (cs, (_, _, true)) = cs
   1.176 -      | count_cases (cs, (cname, (_, body), false)) =
   1.177 -          case AList.lookup (op = : term * term -> bool) cs body
   1.178 -           of NONE => (body, [cname]) :: cs
   1.179 -            | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs;
   1.180 -    val cases' = sort (int_ord o Library.swap o pairself (length o snd))
   1.181 -      (Library.foldl count_cases ([], cases));
   1.182 +    fun count_cases (_, _, true) = I
   1.183 +      | count_cases (cname, (_, body), false) =
   1.184 +          AList.map_default (op = : term * term -> bool)
   1.185 +            (body, []) (cons cname)
   1.186 +    val cases' = sort (int_ord o swap o pairself (length o snd))
   1.187 +      (fold_rev count_cases cases []);
   1.188      fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $
   1.189        list_comb (Syntax.const cname, vs) $ body;
   1.190      fun is_undefined (Const ("undefined", _)) = true
   1.191 @@ -503,13 +500,14 @@
   1.192             else if length cnames = length constrs then
   1.193               [hd cases, ("dummy_pattern", ([], default), false)]
   1.194             else
   1.195 -             filter_out (fn (cname, _, _) => cname mem cnames) cases @
   1.196 +             filter_out (fn (cname, _, _) => member (op =) cnames cname) cases @
   1.197               [("dummy_pattern", ([], default), false)]))
   1.198    end;
   1.199  
   1.200 -fun make_case_tr' case_names descr = List.concat (map
   1.201 -  (fn ((_, (_, _, constrs)), case_name) => map (rpair (case_tr' constrs))
   1.202 -    (NameSpace.accesses' case_name)) (descr ~~ case_names));
   1.203 +fun make_case_tr' case_names descr = maps
   1.204 +  (fn ((_, (_, _, constrs)), case_name) =>
   1.205 +    map (rpair (case_tr' constrs)) (NameSpace.accesses' case_name))
   1.206 +      (descr ~~ case_names);
   1.207  
   1.208  val trfun_setup =
   1.209    Theory.add_advanced_trfuns ([], [("_case_syntax", case_tr)], [], []);
   1.210 @@ -599,9 +597,9 @@
   1.211  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
   1.212      case_names_induct case_names_exhausts thy =
   1.213    let
   1.214 -    val descr' = List.concat descr;
   1.215 +    val descr' = flat descr;
   1.216      val recTs = get_rec_types descr' sorts;
   1.217 -    val used = foldr add_typ_tfree_names [] recTs;
   1.218 +    val used = map fst (fold Term.add_tfreesT recTs []);
   1.219      val newTs = Library.take (length (hd descr), recTs);
   1.220  
   1.221      val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
   1.222 @@ -635,46 +633,44 @@
   1.223  
   1.224      val case_names = map (fn s => (s ^ "_case")) new_type_names;
   1.225  
   1.226 -    val thy2' = thy |>
   1.227 +    val thy2' = thy
   1.228  
   1.229        (** new types **)
   1.230 -
   1.231 -      curry (Library.foldr (fn (((name, mx), tvs), thy') => thy' |>
   1.232 -          TypedefPackage.add_typedecls [(name, tvs, mx)]))
   1.233 -        (types_syntax ~~ tyvars) |>
   1.234 -      add_path flat_names (space_implode "_" new_type_names) |>
   1.235 +      |> fold (fn ((name, mx), tvs) => TypedefPackage.add_typedecls [(name, tvs, mx)])
   1.236 +           (types_syntax ~~ tyvars)
   1.237 +      |> add_path flat_names (space_implode "_" new_type_names)
   1.238  
   1.239        (** primrec combinators **)
   1.240  
   1.241 -      specify_consts (map (fn ((name, T), T') =>
   1.242 -        (name, reccomb_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
   1.243 +      |> specify_consts (map (fn ((name, T), T') =>
   1.244 +           (name, reccomb_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts))
   1.245  
   1.246        (** case combinators **)
   1.247  
   1.248 -      specify_consts (map (fn ((name, T), Ts) =>
   1.249 -        (name, Ts @ [T] ---> freeT, NoSyn)) (case_names ~~ newTs ~~ case_fn_Ts));
   1.250 +      |> specify_consts (map (fn ((name, T), Ts) =>
   1.251 +           (name, Ts @ [T] ---> freeT, NoSyn)) (case_names ~~ newTs ~~ case_fn_Ts));
   1.252  
   1.253      val reccomb_names' = map (Sign.full_name thy2') reccomb_names;
   1.254      val case_names' = map (Sign.full_name thy2') case_names;
   1.255  
   1.256 -    val thy2 = thy2' |>
   1.257 +    val thy2 = thy2'
   1.258  
   1.259        (** size functions **)
   1.260  
   1.261 -      (if no_size then I else specify_consts (map (fn (s, T) =>
   1.262 +      |> (if no_size then I else specify_consts (map (fn (s, T) =>
   1.263          (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   1.264 -          (size_names ~~ Library.drop (length (hd descr), recTs)))) |>
   1.265 +          (size_names ~~ Library.drop (length (hd descr), recTs))))
   1.266  
   1.267        (** constructors **)
   1.268  
   1.269 -      parent_path flat_names |>
   1.270 -      curry (Library.foldr (fn (((((_, (_, _, constrs)), T), tname),
   1.271 -        constr_syntax'), thy') => thy' |>
   1.272 -          add_path flat_names tname |>
   1.273 +      |> parent_path flat_names
   1.274 +      |> fold (fn ((((_, (_, _, constrs)), T), tname),
   1.275 +        constr_syntax') =>
   1.276 +          add_path flat_names tname #>
   1.277              specify_consts (map (fn ((_, cargs), (cname, mx)) =>
   1.278                (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
   1.279 -                (constrs ~~ constr_syntax')) |>
   1.280 -          parent_path flat_names))
   1.281 +                (constrs ~~ constr_syntax')) #>
   1.282 +          parent_path flat_names)
   1.283              (hd descr ~~ newTs ~~ new_type_names ~~ constr_syntax);
   1.284  
   1.285      (**** introduction of axioms ****)
   1.286 @@ -717,7 +713,7 @@
   1.287          exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~
   1.288            nchotomys ~~ case_congs ~~ weak_case_congs);
   1.289  
   1.290 -    val simps = List.concat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.291 +    val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.292      val split_thms = split ~~ split_asm;
   1.293  
   1.294      val thy12 =
   1.295 @@ -775,11 +771,11 @@
   1.296      val (size_thms, thy11) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
   1.297        descr sorts reccomb_names rec_thms thy10;
   1.298  
   1.299 -    val dt_infos = map (make_dt_info (List.concat descr) sorts induct reccomb_names rec_thms)
   1.300 +    val dt_infos = map (make_dt_info (flat descr) sorts induct reccomb_names rec_thms)
   1.301        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
   1.302          casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   1.303  
   1.304 -    val simps = List.concat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.305 +    val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.306  
   1.307      val thy12 =
   1.308        thy11
   1.309 @@ -852,7 +848,7 @@
   1.310      val (case_names_induct, case_names_exhausts) = case RuleCases.get induction
   1.311       of (("1", _) :: _, _) => (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames))
   1.312        | (cases, _) => (RuleCases.case_names (map fst cases),
   1.313 -          replicate (length ((List.filter (fn ((_, (name, _, _))) => member (op =)
   1.314 +          replicate (length ((filter (fn ((_, (name, _, _))) => member (op =)
   1.315              (map #1 dtnames) name) descr)))
   1.316              (RuleCases.case_names (map fst cases)));
   1.317      
   1.318 @@ -892,7 +888,7 @@
   1.319        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
   1.320          map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   1.321  
   1.322 -    val simps = List.concat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.323 +    val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   1.324  
   1.325      val thy11 =
   1.326        thy10
   1.327 @@ -949,12 +945,12 @@
   1.328      val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
   1.329        [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
   1.330  
   1.331 -    fun prep_dt_spec ((dts', constr_syntax, sorts, i), (tvs, tname, mx, constrs)) =
   1.332 +    fun prep_dt_spec (tvs, tname, mx, constrs) (dts', constr_syntax, sorts, i) =
   1.333        let
   1.334 -        fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) =
   1.335 +        fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
   1.336            let
   1.337              val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs);
   1.338 -            val _ = (case foldr add_typ_tfree_names [] cargs' \\ tvs of
   1.339 +            val _ = (case fold (curry add_typ_tfree_names) cargs' [] \\ tvs of
   1.340                  [] => ()
   1.341                | vs => error ("Extra type variables on rhs: " ^ commas vs))
   1.342            in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
   1.343 @@ -966,7 +962,7 @@
   1.344                " of datatype " ^ tname);
   1.345  
   1.346          val (constrs', constr_syntax', sorts') =
   1.347 -          Library.foldl prep_constr (([], [], sorts), constrs)
   1.348 +          fold prep_constr constrs ([], [], sorts)
   1.349  
   1.350        in
   1.351          case duplicates (op =) (map fst constrs') of
   1.352 @@ -978,7 +974,7 @@
   1.353               " in datatype " ^ tname)
   1.354        end;
   1.355  
   1.356 -    val (dts', constr_syntax, sorts', i) = Library.foldl prep_dt_spec (([], [], [], 0), dts);
   1.357 +    val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
   1.358      val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
   1.359      val dt_info = get_datatypes thy;
   1.360      val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
   1.361 @@ -986,7 +982,7 @@
   1.362        if err then error ("Nonemptiness check failed for datatype " ^ s)
   1.363        else raise exn;
   1.364  
   1.365 -    val descr' = List.concat descr;
   1.366 +    val descr' = flat descr;
   1.367      val case_names_induct = mk_case_names_induct descr';
   1.368      val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
   1.369    in