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