datatype/mutrec/Recftn.sml

3    description of how the function should behave the values of the
7    that compute the return value of the function from the arguments
10    instantiate our recursive function with them, define the functions,
15    there must be at most one function defined for each type (there need
16    not be a function defined for every type). If a function is being
23    first term gives explictly the values of the function on all
24    constructors for each type for which a function is defined, and the
26    the constructors.  The "allelse" works like this: Say a function is
34    right of the = sign is used as the value of the function on terms
39    function being defined, but there is no limit to the number of
160        ftn_dom = <domain type of function>,
163        def = <term defining this case for function>}  *)
255            with the argument of the function. *)
293     (* get_result_typevar destructs function types until it finds that
302        function for a type, then s/he gives a value for each of the
303        constructors for that type, and that only one function is being
309                message = ("only some cases provided for function " ^
323              a dummy function returning one. The domain of the
324              function we're defining is the result type of the
368        We want to create nn, the function that will return a value for
377        so the only recursive function that can be applied to it is
378        varcon_atpat, the function being defined for that type. So we replace
381        If no function is defined for a type, I will create a dummy function
386        defining a function on it and what the domain and range types of
387        such a function would be. lookup_return is the datatype returned by
399     (* get_rec_vars is used when no function is being defined for this type,
400        figures out what vars to abstract over to make a constant function,
445        given in order to make body of return function. It returns
446        the modified term (which will be the body of our function) and
462              recursive calls on this arg since no recursive function
484     (* abstract_over_vars takes as arguments the body of the function
493        into the function or constant (one of a - nn) needed by syntax_rec *)
496     (* no function defined for this type, make the function be
525        function defined for type I (using the order in which the types
526        are given in rec_axiom), and propertyI is, if a function is
528        propertyI says that the function returns one on all inputs. *)
538        (those that refer to types the user isn't defining a function for),
648     (* this function goes through the list, picking out the conjunc(s)
751    function that counts the number of variables and constructors used