Lines Matching defs:constructor
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