acl2/ml/functionEncodeLib.sml

16 (*        derivation of function type for encode/decode et al...             *)
33 (*        encoding boundaries (eg. decode (encode x)). The suggested fix is  *)
116 (*     a) (encode : t -> target) x    where encode is a valid encoder        *)
174 (*                (Q0 ==> encode a0 = A0) /\ ... /\ (Qm ==> encode am = Am)  *)
175 (*                ==> (encode (F a0 ... an) = F A0 ... Am)                   *)
191          "      (Q0 ==> encode a0 = A0) /\\ ... /\\ (Qm ==> encode am = Am)\n" ^
192          "      ==> (encode (F a0 ... an) = F A0 ... Am)\n" ^
258      "\nis not of the form: |- P ==> (encode a = b) or |- encode a = b")
348 (*             !x. detect x ==> encode (decode x) = x                        *)
350 (*           |- !x. detect x ==> encode (decode x) = x                       *)
352 (*             !x. decode (encode x) = x                                     *)
354 (*           |- !x. decode (encode x) = x                                    *)
356 (*             !x. detect (encode x)                                         *)
358 (*           |- !x. detect (encode x)                                        *)
528 (*     |- !a. decode (encode a) = a                                          *)
533 (*     |- !a. detect a ==> encode (decode a) = a                             *)
538 (*     |- !a. detect (encode a)                                              *)
544                         "Not a term of the form: \"!a. decode (encode a) = a\""
563 val err = mkStandardExn "dest_decenc" "Not a term of the form: \"!a. detect a ==> encode (decode a) = a\""
568         val (encode,decoded_term) = with_exn (dest_comb o lhs) body2 err
573         val _ = with_exn (match_term encode) (gen_encode_function target t) err
588 val err = mkStandardExn "dest_encdet" "Not a term of the form: \"!a. detect (encode a)\""
842 "      (Q0 ==> encode a0 = A0) /\\ ... /\\ (Qm ==> encode am = Am) ==>\n" ^
843 "      (encode (F a0 ... an) = F A0 ... Am)"))
934 (*     'n L ==> encode x = X' and, provided L is null, derives the theorem:  *)
935 (*     [encode x = X] |- detect X  and appends it, and the theorem:          *)
936 (*     [encode x = X] |- encode x = X to the list of assumptions A.          *)
1033              " ie. it has antecedents: \"(encode (f X) = Y) ..." ^
1034              " /\\ (encode (g Y) = X)\""))
1038   "      (Q0 ==> encode a0 = A0) /\\ ... /\\ (Qm ==> encode am = Am)\n" ^
1039   "      ==> (encode (F a0 ... an) = F A0 ... Am)\n" ^
1237 (*        A |- encode Y = y  --> A |- Y = decode y                           *)
1305 (*    PROPAGATE_ENCODERS_CONV (assumptions,extras) ``encode M``              *)
2211 (*     encode 'encode_type f g A' seperately. This is because the final      *)
2238 (*             bool ((FST o decode_pair decode_num I o encode .. x)) = i)    *)
2244 let val encoders = CONJUNCTS (get_coding_function_def target t "encode")
2268 let val encoders = CONJUNCTS (get_coding_function_def target t "encode")
2404     val enc = mk_var("encode",mk_vartype "'out" --> mk_vartype "'target")
2434     val enc = mk_var("encode",type_of (lhs (concl thm)) --> gen_tyvar())
2452     val encoder = mk_var("encode",alpha --> gen_tyvar());
2501 (* Add rewrites to encode constructors, case theorems, and encoding of       *)
2503 (*      |- encode (C x y z) = cons 0 (encode x) (encode y) (encode z)        *)
2506 (*      |- (!x. f0' (f0 x) = x) /\ (encode f0 f1 ... x = X) /\               *)
2509 (*      |- detect a ==> (encode (decode a) = a)                              *)
2527                       (get_coding_function_def target t "encode"))
2623 (*    If a statement is of the form: encode (decode x) or encode (case ...)  *)
2638                                  "Not a term: encode (decode x)"))
2662 (*        encode (if (detect a /\ detect b /\                                *)
2668 (*    [D] |- P a b ... ==> (encode (f a b) = <f> (encode a) (encode b))      *)
2677  "Definition is not of the form: \"|- !a b. f a b ... = encode (...)\"";
2840 (*        encode (if (detect a /\ detect b /\                                *)
2846 (*     [D] |- P a b /\ ... ==> (encode (f a b) = <f> (encode a) (encode b)) *)
3050 (*                              (encode (f a b) = <f> (encode a) (encode b)) *)
3054 (*           |- P a b ==> (encode (f a b) = <f> (encode a) (encode b))       *)
3109                         "Rewrite is not of the form: |- !a... encode (f a..) =")
3163 (*               |- (?a. x = SUC a) ==> (encode (PRE a) = ...)               *)
4129                ("Could not encode the value: " ^ term_to_string x));