acl2/ml/encodeLib.sml

55                 ("Could not find bottom values for all sub-types of "
129 (*     Makes a full all function for the given type:                         *)
130 (*     Label constructors: all Li = T                                        *)
131 (*     Otherwise         : all (C a0 .. an) = (all0 # .. # alln) (a0,..,an)  *)
201 fun mk_all_string t = "all" ^ (get_type_string t)
256               (get_source_function_const t "all") t
322                  (C exists_source_function_precise "all")
377         if      all (not o can dom_rng o type_of) constructors
454         if      all (not o can dom_rng o type_of) constructors
466 fun mk_fix_constructor_ns all target C =
470         mk_comb(get_fix_function target (list_mk_prod (num::list)),all)
472 fun mk_fix_constructor all target dead n C =
474                 then mk_fix_constructor_ns all target C
477 fun mk_fix_res_term label all target constructors dead bottom =
480                         mk_fix_constructor all target dead a b)) (enumerate 0 constructors))
538     if all (not o can dom_rng o type_of) constructors
590     if all (not o can dom_rng o type_of) constructors
814 let     val _ = if exists_source_function t "all" then
818                 ("Generating all function for: " ^ type_to_string t ^ "\n")
821                         "all"
825                                 (PURE_REWRITE_CONV [get_source_function_def (mk_prod(alpha,beta)) "all"])))) x
870 (*     ?- (detect f o encode g) = all (f o g)                                *)
876 (*     ?- all (K T) = K T                                                    *)
1006         val all = check_function get_all_function t
1011         val sub = map2 (curry op|->) (free_vars_lr all) (map2 (curry combinSyntax.mk_o) det_vars enc_vars)
1014         list_mk_forall(enc_vars,mk_eq((curry combinSyntax.mk_o) det enc,subst sub all)))
1465 (*        APP_ALL_CONV : |- (all (C a b)) = (all a) /\ (all b)               *)
1498         val def = get_source_function_def t "all"
1522         val all_rwr =   if all (not o can dom_rng o type_of) cs then
1530         val first_decode = if all (not o can dom_rng o type_of) cs then
1558         val pair_all = get_source_function_def (mk_prod(alpha,beta)) "all"
1565         val all_rwr =   if all (not o can dom_rng o type_of) cs then
1572                         if all (not o can dom_rng o type_of) cs then
1633 in      if all (not o can dom_rng o type_of) cs then ALL_TAC
1673         val all_defs = mapfilter (C get_source_function_def "all") (all_types t)
1679                 ASM_REWRITE_TAC (get_source_function_def (mk_prod(alpha,beta)) "all"::thms) THEN
1899         val def = get_source_function_def t "all"
1900         val pair_def = get_source_function_def (mk_prod(alpha,beta)) "all"
2006                 "all"
2010                         (PURE_REWRITE_CONV [get_source_function_def (mk_prod(alpha,beta)) "all"])))) x
2078                 "all" "all_id"
2122                 (check_source_rule_use "all" "all_id")
2169         val _ = generate_source_function "all" t