1 /* 2 * foreign.h -- header file for user-defined foreign functions 3 * 4 */ 5 6 /* 7 HOW TO WRITE YOUR OWN C ROUTINE WHICH CAN BE 8 CALLED TO DEMODULATE A TERM DURING OTTER'S DEMODULATION 9 10 The Otter types don't correspond exactly to the C types. In Otter, the 11 types, except `term', are all constants (in the theorem-proving sense), 12 and in C, the types are what you would expect them to be. 13 14 TYPES: 15 - long In C and in Otter, a long integer. 16 - double In C, a double; in Otter, a double surrounded by double quotes. 17 - bool In C, an int; in Otter, $T or $F. 18 - string In C, a pointer to a string; in Otter, any constant. 19 - term An Otter term. 20 21 To include a new function, you have to (1) declare the function, 22 argument types, and result type, (2) insert a call to your function in 23 the Otter code, (3) write your C routine, and (4) remake Otter. 24 The only Otter files you need to change are foreign.h and foreign.c. 25 26 When Otter is demodulating and comes across a 'call' to your function, 27 it will first check the argument types. If they are incorrect (for 28 example a variable is not instantiated) the term will not be 29 rewritten; if the arguments are OK, your C routine will be called, and 30 the result of your C routine will be made into an appropriate Otter 31 term which is the result of the rewriting step. 32 33 (Don't forget that many times you can avoid having to do all of 34 this by just writing your function with demodulators and using 35 existing built in functions. For example, if you need the 36 max of two doubles, you can just use the demodulator 37 float_max(x,y) = $IF($FGT(x,y), x, y). For other examples of 38 programming with demodulators, see eval.in in the Otter test suite. 39 See file demod.c, routine dollar_contract, for the current set 40 of evaluable functions.) 41 42 STEP-BY-STEP INSTRUCTIONS 43 44 0. Say you want to write a function foo that takes 45 a long, a double, and a string as arguments and produces a long, i.e., 46 47 long foo(long n, double x, char *s) 48 49 The Otter-language name must start with $, say $FOO, and you 50 will be evaluating Otter terms like $FOO(32, "-4.5e-10", flag32) 51 52 1. To declare the function and its types, 53 54 (A) In the file foreign.h, #define a symbol, which will be used 55 as an index into a table (see FOO_FUNC in foreign.h). 56 57 (B) In file foreign.c, in routine declare_user_functions, declare 58 the function and its types (look for FOO_FUNC in foreign.c). 59 The types are LONG_TYPE, DOUBLE_TYPE, BOOL_TYPE, STRING_TYPE, 60 and TERM_TYPE. 61 62 2. In file foreign.c, in routine evaluate_user_function, insert a call 63 to your function and a call to translate the result to an Otter 64 term (look for FOO_FUNC in foreign.c). The routines to translate 65 C types to otter terms are long_to_term, double_to_term, bool_to_term, 66 and string_to_term. See foreign.c for examples. 67 68 3. Write your C routine. I have inserted the test routines into 69 foreign.c, but you may wish to organize yours into separate 70 files. (If your routines involve TERM_TYPE, you must 71 #include "header.h".) 72 73 4. Remake Otter; foreign.c is the only Otter file that will need 74 to be recompiled. 75 76 5. Test your new function by using the input file foreign.in. 77 78 79 */ 80 81 #define MAX_USER_ARGS 20 /* maximum arity for user-defined C functions */ 82 83 #define LONG_TYPE 1 /* types for user-defined C functions */ 84 #define DOUBLE_TYPE 2 85 #define BOOL_TYPE 3 86 #define STRING_TYPE 4 87 #define TERM_TYPE 5 88 89 struct user_function { /* entry in table of user-defined functions */ 90 int arity; 91 int arg_types[MAX_USER_ARGS]; 92 int result_type; 93 }; 94 95 #define MAX_USER_FUNCTIONS 100 /* size of table */ 96 97 /* indexes into table of user-defined functions */ 98 99 #define FOO_FUNC 1 100 #define TEST_LONG_FUNC 2 101 #define TEST_DOUBLE_FUNC 3 102 #define TEST_BOOL_FUNC 4 103 #define TEST_STRING_FUNC 5 104 #define TEST_TERM_FUNC 6 105 106