Lines Matching defs:constructors
99 (* Label constructors: enc Cn = nat n *)
105 (* Label constructors: dec x = if dnat x = 0 then C0 else .... *)
115 (* Label constructors: dec x = bool (dnat x = 0 \/ ... \/ dnat x = n) *)
125 (* Label constructors: map Li = Li *)
130 (* Label constructors: all Li = T *)
135 (* Label constructors: fix x = x *)
336 fun mk_detect_res_term label rest target t constructors T =
339 mk_detect_constructor rest target b T)) (enumerate 0 constructors))
341 fun mk_detect_term_label (p,x) target t constructors =
347 mk_detect_res_term (mk_comb(dnat,x)) x target t constructors T,
350 fun mk_detect_term_all (p,x) target t constructors =
360 mk_detect_res_term label rest target t constructors (mk_eq(rest,null))),
373 val constructors = constructors_of t' handle e => wrapException "mk_detect_term" e
377 if all (not o can dom_rng o type_of) constructors
378 then mk_detect_term_label (p,x) target t' constructors
380 else if length constructors = 1
381 then mk_detect_term_single (p,x) target t' (hd constructors)
383 else mk_detect_term_all (p,x) target t' constructors
409 fun mk_decode_res_term label rest target t constructors bottom =
412 mk_decode_constructor rest target b)) (enumerate 0 constructors))
414 fun mk_decode_term_label (p,x) target t constructors =
417 val bottom = hd constructors
421 mk_decode_res_term (mk_comb(dnat,x)) x target t constructors bottom,
422 hd (constructors))))
424 fun mk_decode_term_all (p,x) target t constructors =
434 mk_decode_res_term label rest target t constructors bottom),
450 val constructors = constructors_of t' handle e => wrapException "mk_decode_term" e
454 if all (not o can dom_rng o type_of) constructors
455 then mk_decode_term_label (p,x) target t' constructors
457 else if length constructors = 1
458 then mk_decode_term_single (p,x) target t' (hd constructors)
460 else mk_decode_term_all (p,x) target t' constructors
477 fun mk_fix_res_term label all target constructors dead bottom =
480 mk_fix_constructor all target dead a b)) (enumerate 0 constructors))
482 fun mk_fix_term_label x target t constructors =
489 list_mk_cond (map (fn (a,b) => (mk_eq(mk_comb(dnat,x),numLib.term_of_int a),x)) (enumerate 0 constructors))
493 fun mk_fix_term_all (p,x) target t constructors dead =
509 mk_fix_res_term label x target constructors dead bottom),
532 val constructors = constructors_of t'
538 if all (not o can dom_rng o type_of) constructors
539 then mk_fix_term_label x target t' constructors
541 else if length constructors = 1
542 then mk_fix_term_single x target t' (hd constructors) dead
544 else mk_fix_term_all (p,x) target t' constructors dead
587 val constructors = constructors_of t'
590 if all (not o can dom_rng o type_of) constructors
591 then mk_encode_term_label target t' constructors
593 else if length constructors = 1
594 then mk_encode_term_single target t' (hd constructors)
596 else mk_encode_term_all target t' constructors