datatype/mutrec/MutRecDef.sml

33 fun MUT_REC_ERR {function,message} = HOL_ERR{origin_structure = "MutRecDef",
34                                              origin_function = function,
46          | _ => raise MUT_REC_ERR {function = "dest_fun",
47                                    message = "Not a function type"})
53          | _ => raise MUT_REC_ERR {function = "dest_prod",
60          | _ => raise MUT_REC_ERR{function = "dest_sum",
116     else Raise (MUT_REC_ERR {function = "find_witnesses",
165         raise MUT_REC_ERR{function="type_num",
235 (* Our next goal is to define a function (called joint_name^"_select",
236    I'll refer to it as the joint select function) that, given an item in
243    return values for the joint select function; I'll refer to them
259  gotten by recursively applying the function being defined) for each each of
266    need to create the return functions for our joint select function.
268    the recursive calls to the joint select function, the number terms will
271    representing the arguments to the constructor the return function
341     (* if constructor has no args, the return "function" is just a constant *)
357                our return function will be just a constant giving the
377 (* fn_lemma says there exists a unique function satisfying the
378    desired properties of our joint selection function *)
386 (* define our joint_select function *)
394 (* make a constant for our joint select function *)
572         | NONE => raise MUT_REC_ERR{function = "mk_case",
575 (* get_abs returns the abstraction function associated with type of tyname *)
581                 {function = "get_abs", message = "no abs for " ^ tyname}
586 (* get_rep returns the representation function associated with tyname *)
592                 {function = "get_rep", message = "no rep for " ^ tyname}
667         raise MUT_REC_ERR{function = "get_sum_type", message = "No types!?!"}
703             {function = "mk_rights", message = "Impossible"}
719             {function = "get_ins_outs", message = "Impossible - No type names"}
722             {function = "get_ins_outs", message = "Impossible - No types"}
777  need to create the return functions for our joint mutual recursion function.
783  recursive call to the joint function, the plain_vars are the vars
827                | NONE => raise MUT_REC_ERR{function = "mk_case",
1018                | NONE => raise MUT_REC_ERR{function = "mk_case",
1028                | NONE => raise MUT_REC_ERR{function = "mk_case",
1120                 | NONE => raise MUT_REC_ERR{function = "",
1126                 | NONE => raise MUT_REC_ERR{function = "",
1149                | NONE => raise MUT_REC_ERR{function = "",
1164                 | NONE => raise MUT_REC_ERR{function = "",
1198   | map3 f _ _ _ = raise MUT_REC_ERR{function = "map3",
1249                   | NONE => raise MUT_REC_ERR{function = "",