datatype/mutrec/Recftn.sml

6    constants, one for each constructor of the mutually recursive types,
8    of the constructor and the return values of applications of (possibly
9    other) mutually recursive functions to the constructor args. We then
18    value for each constructor for the type, except as descibed below in
28    atpat) and the case for a constructor is missing (for example,
32    constructor applied to appropriate arguments (here, (SCONatpat sc)) is
35    constructed with that constructor. If there is a variable "arg" with
37    the =), this will be replaced by the constructor applied to arguments
131     (* decompose takes as arguments a term that is a constructor applied
133        off the rest of the args, returning the constructor by itself
144        the constructor associated with it, the arguments of the constructor,
145        and the type the constructor will construct *)
161        constructor = <constructor this case covers>,
162        args = <constructor args>,
171          constructor = con, args = args, def = rhs}
181     fun same_cons constructor {cons,cons_args,result_type}=
182         (#Name(dest_const constructor) = #Name(dest_const cons))
183     fun find_ty_subst {constructor,args,def,ftn,ftn_dom} =
185            (#cons(Lib.first (same_cons constructor) gen_cons_data))
186            constructor)
190  *  fun find_ty_subst {constructor,args,def,ftn,ftn_dom} =
191  *      #2(Match.match_term constructor
192  *         (#cons(Lib.first (same_cons constructor) gen_cons_data)))
226        definition for this constructor. If finds exactly one, returns
236        found (ie, we matched against a constructor rather than an
238        found the constructor, or the information from an "allelse"
243        getting an exact constructor match. *)
245                  (def_datum as {ftn, ftn_dom, constructor,
248             if constructor = cons then
251            if so, the constructor is the one we're looking for
253            with the applied constructor substituted for the
257             andalso (is_var constructor)
258             andalso (#Name (dest_var constructor) = "allelse") then
266                    constructor = cons, args = cons_args,
276             constructor for our type *)
282               (* that constructor only appeared once *)
284               (* constructor appeared more than once in def *)
288                    message = ("constructor " ^ (term_name cons) ^
325              constructor it's operating on *)
328                | SOME {args, constructor, def, ftn, ftn_dom} =>
340                | SOME {args, constructor, def, ftn, ftn_dom} =>
363        that compute return values for each constructor, ie, the a-nn in
376        type atpat (since it's the second arg to constructor CONpat), and
422     (* sort_cons_args is used to sort the constructor args into
427        of the constructor. Within those sorts, however, earlier
428        constructor args are earlier in the lists. The list returned is
504       | create_return_fun (SOME {ftn, ftn_dom, constructor, args, def},
594        I want the conjunct itself, the constructor and the conjunct
595        refers to, and the type of the constructor *)
600         val (constructor, _) = decompose (cons_and_args, [])
602         {cons = constructor, cons_range = return_type, conj = conjunct}
613        associated with the constructor field of an item in def_data,
616     fun get_conj_for_cons ({constructor, ftn, ftn_dom, args, def},
620             if constructor = cons then
627          message = ("illegal constructor " ^ (term_name constructor) ^
635     fun get_conjs_for_allelse ({constructor, ftn, ftn_dom, args, def},
656     fun mk_Qtm_body ((datum as {ftn, ftn_dom, constructor, args, def})
659     if is_var constructor then
660         if #Name (dest_var constructor) = "allelse" then
670                       (term_name constructor) ^