datatype/mutrec/MutRecDef.sml

73  arg_info for a constructor.
122  for each of its argument types (i.e. is th constructor closed in the current
123  world).  If we find such a constructor, it is a witness, and so we put it
160 fun change_entry {name,arg_info} = {constructor = "JOINT_"^name,
188  of a constructor for that type.  The list is given the order in which the
190  constructor description given with the type name is tthe information
242    and constants, one for each constructor of the joint type, that compute
257  e0, f1, f2, ...).  Each of these functions corresponds to a constructor.
260  recursive types in the arguments to the constructor, next the constructor
261  arguments of non-recursive type, and last the constructor arguments of
271    representing the arguments to the constructor the return function
272    is for. We build up the being_defined & existing constructor arg lists
277  Base Case: We are through looking at the constructor arguments.  Return the
341     (* if constructor has no args, the return "function" is just a constant *)
344     (* if the constructor has args, get variables (and numbers) to
346        to correspond to arguments of the constructor *)
514 (* mk_constructor_app makes a constructor and creates variables of the
516    returns the applied constructor and list of vars that were created. *)
535         val constructor = mk_var {Name = name, Ty = constructor_type}
547         mk_c_app constructor dom_ty_list 1 []
550 (* apply_constructor takes a constructor name, the args it's to be applied
552    constant for the constructor and applies it *)
597 (* the joint constructor must be applied to the variables returned by
605    defines one constructor for the type with name tyname *)
797  Base Case: We are through looking at the constructor arguments.  Return the