acl2/ml/encodeLib.sml

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