1(*****************************************************************************) 2(* Information and trouble shooting guide for encoding to ACL2. *) 3(* *) 4(* Functions are encoded using the translate_..._function functions, and *) 5(* should be used in order of definition. Eg, if the function f calls the *) 6(* function g, then g should be translated before f. Additionally, if *) 7(* f takes as argument a type t, then a 'recognition' function must be *) 8(* generated for t before it can be used. The function, *) 9(* flatten_recognizers is used to do this. *) 10(* *) 11(* Trouble shooting: *) 12(* The trace is registered under 'functionEncodeLib.Trace' and exceptions *) 13(* are best viewed using 'translate_... handle e => Raise e'. *) 14(* *) 15(* The two common reasons for the encoding process to fail are: *) 16(* Missing rewrite: A function that is relied upon by the function *) 17(* being encoded has not been translated yet. *) 18(* In the simplest case this may be solved by translating the *) 19(* missing function, or flattening the recognizer for the required *) 20(* type. If the function may not be translated automatically, *) 21(* then it may be translated by hand and added using: *) 22(* functionEncodeLib.add_standard/conditional_rewrite. *) 23(* Example: *) 24(* If we translate 'DIVMOD' without previously translating *) 25(* 'findq' we get the error: *) 26(* Exception: No rewrite matched the following: *) 27(* Term: nat (findq (1,FST ..., SND ...)) *) 28(* Assumptions: [ [.] *) 29(* Rewrite cannot be applied: This is characterised by a rewrite *) 30(* *nearly* applying in the trace log. *) 31(* In some cases this can be solved by provided an extra theorem. *) 32(* For example, the if the rewrite for DIV fails under the *) 33(* assumptions: *) 34(* [|- ~(a = 0), ... ] ``nat (x DIV a)`` *) 35(* We can solve this by adding the extra theorem: *) 36(* |- ~(a = 0) ==> 0 < a *) 37(* To match the theorem: *) 38(* |- 0 < a ==> (nat (b DIV a) = ...) *) 39(* *) 40(* The translation of under-specified recursive functions (eg. SEG) is *) 41(* particularly troublesome. All constructors in limits must be given *) 42(* in a POSITIVE form, eg: *) 43(* ?x y. argument = x :: y rather than ~(argument = []) *) 44(* For a recursive function we must therefore prove two theorem forms. *) 45(* Firstly, that the limit is correct, and secondly, that it is preserved *) 46(* across recursive calls: *) 47(* 1) : |- a + b <= LENGTH c ==> ~((?n. a = SUC n) /\ (c = [])) *) 48(* 2) : |- (?d. a = SUC d) /\ (b = 0) /\ *) 49(* (?x y. c = x :: y) /\ a + b <= LENGTH c ==> *) 50(* PRE a + 0 <= LENGTH (TL c) *) 51(* Recursive calls are characterised by the limit being applied to *) 52(* destructed arguments (PRE and TL). For a given type, t, these can be *) 53(* found by using the function: *) 54(* get_coding_theorem_precise ``:sexp`` t "destructors" *) 55(* *) 56(*****************************************************************************) 57 58signature acl2encodeLib = 59sig 60 include Abbrev 61 62(*****************************************************************************) 63(* print_all_defs_mbe/standard : *) 64(* Prints all definitions, up until the definition given, to a file. *) 65(* The _mbe version uses the form: *) 66(* (defun f (x) (declare (xargs :guard P)) *) 67(* (must-be-equal (if P body bottom) body)) *) 68(* *) 69(* This has the advantage that functions run must faster. However, ACL2 *) 70(* is occasionally unable to prove termination / verify guards. This will *) 71(* hopefully be resolved soon... *) 72(* *) 73(*****************************************************************************) 74 75 val print_all_defs_mbe : string -> thm -> unit 76 val print_all_defs_standard : string -> thm -> unit 77 78(*****************************************************************************) 79(* set_destructors : thm list -> unit *) 80(* Set the destructors for a given type to the theorems given. *) 81(* These theorems should be of the form: |- D (C a b c...) = b ... *) 82(* *) 83(* This function can be used before or after initialise_type is called. *) 84(* However, if functions are translated using the destructors then the *) 85(* destructors provided, eg. D, MUST have been translated beforehand. *) 86(* *) 87(*****************************************************************************) 88 89 val set_destructors : thm list -> unit 90 91(*****************************************************************************) 92(* initialise_type : *) 93(* Initialises a type so that functions over it can be translated to ACL2 *) 94(* This generates the following functions: *) 95(* map, all : *) 96(* The standard map and all functions, these can be viewed *) 97(* using: polytypicLib.get_source_function_def hol_type "map" *) 98(* encode, decode, detect, fix : *) 99(* These functions form the basis of the translation and may *) 100(* be viewed using: *) 101(* polytypicLib.get_coding_function_def ``:sexp`` *) 102(* hol_type "fix" *) 103(* It also generates a number of theorems for use in the encoding *) 104(* process, for more information see the function definition itself and *) 105(* the function encodeLib.encode_type. *) 106(* *) 107(* Usage: *) 108(* This function should be used to encode types added via hol_datatype. *) 109(* Failure to do so may introduce unexpected errors into the translation *) 110(* process. *) 111(* *) 112(*****************************************************************************) 113 114 val initialise_type : hol_type -> unit 115 116(*****************************************************************************) 117(* translate_simple/conditional/limit_function : *) 118(* These functions translate non-polymorphic definitions that do not use *) 119(* finite cartesian products. The encoding process is as follows: *) 120(* a) Convert to clause form, using *) 121(* functionEncodeLib.clause_to_case *) 122(* b) Define an analogue definition using *) 123(* functionEncodeLib.mk_analogue_definition *) 124(* c) Rewrite the definition using: *) 125(* functionEncodeLib.complete_analogue and *) 126(* functionEncodeLib.PROPAGATE_ENCODERS_CONV *) 127(* *) 128(* Usage: *) 129(* Each function takes an associative list, mapping function constants to *) 130(* names for the translated function. For example: *) 131(* [(``LAST``,"last_translated")] *) 132(* Lists are used throughout to support mutually recursive function *) 133(* definitions. *) 134(* *) 135(* The first of these functions should be used for simple definitions *) 136(* which are fully specified (do not have any missing clauses) and do not *) 137(* rely upon any functions which are not fully specified. *) 138(* *) 139(* The second of these functions should be used when the first fails, *) 140(* for definitions which rely upon under-specified functions, but which *) 141(* are themselves fully specified. Examples of such functions are those *) 142(* relying on DIV, HD, TL etc... *) 143(* The second argument to this function is then a list of helper *) 144(* theorems. For example, if a call to HD is guarded by '~(x = [])`, then *) 145(* since the rewrite (|- (?a b. l = a::b) ==> (encode (HD l) = ...)) *) 146(* relies upon CONS instead, the theorem: *) 147(* |- ~(x = []) ==> (?a b. x = a :: b) *) 148(* should be provided. See the examples in testACL2encoding for more *) 149(* information. *) 150(* *) 151(* The final function should be used for definitions which are under *) 152(* specified. This takes an additional argument specifying the ranges *) 153(* under which the function may be translated, eg: *) 154(* [(``LAST``,[(``\x. (?a b. x = a :: b)``)])] *) 155(* NOTE: The system is designed to work with constructors given *) 156(* POSITIVELY, eg: ?a b. x = a :: b, rather than, ~(x = []). *) 157(* This form (with arguments existentially quantified in an LR *) 158(* fashion) should be used wherever possible. *) 159(* *) 160(*****************************************************************************) 161 162 val translate_simple_function 163 : (term * string) list -> thm -> thm 164 val translate_conditional_function 165 : (term * string) list -> thm list -> thm -> thm 166 val translate_limit_function 167 : (term * string) list -> 168 (term * term list) list -> thm list -> thm -> thm 169 170(*****************************************************************************) 171(* translate_simple/conditional/limit_polymorphic_function : *) 172(* These functions work in exactly the same way as the non-polymorphic *) 173(* varieties, except they take one extra argument: a map fusion theorem *) 174(* for each mutually recursive function involved. *) 175(* *) 176(* For a simple, or conditional, function, only the following form of *) 177(* theorem need be supplied: *) 178(* |- f (map g x) (map h y) ... = map g h (f x y) *) 179(* The 'map' functions are introduced during the encoding of each type, *) 180(* and may be retrieved using polytypicLib.get_source_function_def. This *) 181(* means that such functions may not be encoded until initialise_type *) 182(* has been called. *) 183(* *) 184(* In the case of a limited function, eg. LAST, the fusion theorem can *) 185(* only be of the form: *) 186(* |- (?a b. x = a :: b) ==> (LAST (MAP f x) = f (LAST x)) *) 187(* In this case, we must also supply a fusion theorem for CONS, to the *) 188(* list of theorems: *) 189(* |- (?a b. x = a :: b) ==> (?a b. MAP f x = a :: b) *) 190(* This will be the case with all functions with limit range. *) 191(* *) 192(* Note: For functions which are 'partially' polymorphic, eg. they use *) 193(* a type such as :'a + num, the constant I may be used as the map *) 194(* function for a ground type (eg. num). *) 195(* *) 196(*****************************************************************************) 197 198 val translate_simple_polymorphic_function 199 : (term * string) list -> (term * thm) list -> thm -> thm 200 val translate_conditional_polymorphic_function 201 : (term * string) list -> (term * thm) list -> thm list -> thm -> thm 202 val translate_limit_polymorphic_function 203 : (term * string) list -> 204 (term * thm) list -> (term * term list) list -> thm list -> thm -> thm 205 206(*****************************************************************************) 207(* translate_simple/conditional/limit/recursive_fcp_function : *) 208(* These functions are designed to work with functions that use *) 209(* finite cartesian products or words (see wordsTheory, fcpTheory). *) 210(* *) 211(* The encoding process for such functions is subtly different to that *) 212(* used for standard functions. In this case, a prospective term is found *) 213(* to represent the encoded function, and a function defined to match it *) 214(* using functions in Defn. This means that in the case of recursive *) 215(* definitions, two tactics must be supplied. The first to prove that the *) 216(* definition terminates, and the second to prove the propagation theorem.*) 217(* *) 218(* The first tactic supplied must provide a well-founded relation over *) 219(* sexp that demonstrates that the function terminates. The tactic: *) 220(* ENCODE_WF_REL_TAC : term frag list -> tactic *) 221(* is designed to act as WF_REL_TAC, except the relation is combined with *) 222(* encoding functions to produce a relation over s-expressions. *) 223(* This may be used in conjunction with: *) 224(* FULL_CHOOSE_DETECT : tactic *) 225(* Given the assumption '|- detect x' this tactic replaces 'x' with *) 226(* 'encode y'. Also useful, may be the theorems: *) 227(* polytypicLib.generate_coding_theorem ``:sexp`` *) 228(* "encode_decode_map", "encode_decode", "encode_detect"... *) 229(* *) 230(*****************************************************************************) 231 232 val translate_simple_fcp_function 233 : string -> thm -> thm 234 val translate_conditional_fcp_function 235 : string -> thm list -> thm -> thm 236 val translate_limit_fcp_function 237 : string -> term list -> thm list -> thm -> thm 238 val translate_recursive_fcp_function 239 : string -> term list -> thm list -> thm -> 240 thm list -> tactic -> (thm -> thm -> tactic) -> thm 241 242(*****************************************************************************) 243(* flatten_[fcp]_recognizers : *) 244(* Creates functions to 'recognise' the type, suitable for export to *) 245(* ACL2. This *must* be used before attempting to translate functions *) 246(* that rely on untranslated types. *) 247(* *) 248(* usage: *) 249(* Both functions require a 'naming' function to produce names for *) 250(* recognizers for the types involved. It should be noted that ALL *) 251(* types in [nested] mutual recursion with the type given will have *) 252(* functions defined for them. *) 253(* *) 254(*****************************************************************************) 255 256 val flatten_recognizers 257 : (hol_type -> string) -> hol_type -> thm list 258 val flatten_fcp_recognizers 259 : (hol_type -> string) -> hol_type -> thm list 260 261(*****************************************************************************) 262(* Tactics to assist proof of recursive FCP functions: *) 263(* *) 264(* ENCODE_WF_REL_TAC : *) 265(* Given a goal of the form: ?R. WF R /\ .... and *) 266(* a relation 'R', ENCODE_WF_REL_TAC instantiates the existential in the *) 267(* goal with the term: ``inv_image R encode``. *) 268(* *) 269(* FULL_CHOOSE_DETECT_TAC : *) 270(* A u {detect x} ?- G *) 271(* ------------------------------------- FULL_CHOOSE_DETECT_TAC *) 272(* A[encode x' / x] ?- G [encode x' / x] *) 273(* *) 274(*****************************************************************************) 275 276 val ENCODE_WF_REL_TAC : term frag list -> tactic 277 val FULL_CHOOSE_DETECT_TAC : tactic 278 279(*****************************************************************************) 280(* For a ground term: *) 281(* ONEONE_DECENC_THM t = |- ONEONE (decode_t o encode_t) *) 282(* ONEONE_ENC_THM t = |- ONEONE (encode_t : t -> sexp) *) 283(* *) 284(*****************************************************************************) 285 286 val ONEONE_DECENC_THM : hol_type -> thm 287 val ONEONE_ENC_THM : hol_type -> thm 288 289 val Raise : exn -> 'a 290end