acl2/ml/functionEncodeLib.sml

259 fun wrap e = wrapException "conditionize_rewrite" e
277                handle e => wrap e
285    handle e => wrap e
1769 fun wrap s = wrapException ("clause_to_case_list" ^ s)
1779                        handle e => wrap "" e
1782                        handle e => wrap "" e
1786                         handle e => wrap " (outermost)" e
1791                     handle e => wrap "" e
1850 fun wrap e = wrapException "mk_func_case_thm" e
1853 let     val c = TypeBase.case_const_of t handle e => wrap e
1854         val case_def = TypeBase.case_def_of t  handle e => wrap e
1858                         handle e => wrap e
1860                    handle e => wrap e
1863                       mk_comb(case_term,xvar)))  handle e => wrap e
1868         handle e => wrap e
1892 fun wrap e = wrapException "general_lambda" e
1895                     handle e => wrap e
1899         val vars = map2 (curry mk_var) names types handle e => wrap e
1900         val pairs = map list_mk_pair (compn terms vars) handle e => wrap e
1904         list_mk_pabs (pairs,list_mk_comb(out,butlast vars)) handle e => wrap e
1909 fun wrap e = wrapException "general_lambda_propagation_term" e
1914 let     val gterm = general_lambda term handle e => wrap e
2025 fun wrap e = wrapException "mk_affirmation_theorems" e
2037 let val nchotomy = SPEC_ALL (TypeBase.nchotomy_of t) handle e => wrap e
2351 fun wrap e = wrapException "mk_case_propagation_theorem" e
2361         handle e => wrap e
2377                        (enumerate 0 constructors) vars) handle e => wrap e
2379                       handle e => wrap e
2384                      handle e => wrap e;
2388                      handle e => wrap e;
2392                      handle e => wrap e;
2393     val case_term1 = rator (lhs (concl (hd ordered))) handle e => wrap e
2395                      handle e => wrap e
2398                     normalized results handle e => wrap e
2399     val case_defs = map (INST inst) normalized handle e => wrap e
2400     val case_term = rator (lhs (concl (hd case_defs))) handle e => wrap e
2403                handle e => wrap e
3373     fun wrap e = (remove () ; wrapException "encode_until_recursive" e)
3377         (enumerate 0 new_rewrites) handle e => wrap e
3379     ((encode_until funcs AE term handle e => wrap e)
3626 let fun wrap e = wrapException "create_abstract_recognizers" e
3631                 handle e => wrap e
3647                            handle e => wrap e
3654     handle e => wrap e