Lines Matching defs:constructors
7 {case_const : term, constructors : term list} option
148 (constructors, colty, res_ty, rows as (((prefix,_),_)::_)) =
164 in part{constrs=constructors, rows=rows, A=[]}
174 (constructors, colty, res_ty, rows as (((prefix:term list,_),_)::_)) =
189 in part{constrs=constructors, rows=rows, A=[]}
223 Boolean literals are the constructors of the bool type.
244 fun case_const_of {case_const : term, constructors : term list} = case_const
245 fun constructors_of {case_const : term, constructors : term list} = constructors
338 fun expand constructors ty ((_,[]), _) = mk_case_fail "expand_var_row"
339 | expand constructors ty (row as ((prefix, p::rst), rhs)) =
346 in map expnd (map fresh constructors) end
393 val constructors = rev (mk_set (rev (filter (not o is_var) col0)))
396 val switch_tm = mk_switch_tm fresh_var u arb constructors
397 val nrows = flatten (map (expandl constructors pty) rows)
398 val subproblems = dividel(constructors, pty, range_ty, nrows)
401 and constructors' = map #constructor subproblems
410 val pat_rect1 = flatten(map2 mk_patl constructors' pat_rect)
418 val {case_const,constructors} =
420 (ERR "mk_case0" ("could not get case constructors for type " ^
424 val nrows = flatten (map (expand constructors pty) rows)
425 val subproblems = divide(constructors, pty, range_ty, nrows)
428 and constructors' = map #constructor subproblems
447 val pat_rect1 = flatten(map2 mk_pat constructors' pat_rect)