compile.hl

(* Make sure that load_path contains a path to eval_compile.hl *)
(* load_path := "path to eval_*.hl" :: !load_path *)
needs "eval_compile.hl";;

(*****************************************************************************)
(* Basic usage                                                               *)
(*****************************************************************************)

(* The compiler workflow is the following: 
  1) a database with equational theorems is created;
  2) some or all rules from this database are compiled
     into OCaml code which can be saved in a file.
  Several optimizations are available. *)

(* Let's create an empty database *)
let db = empty_db "first";;

(* The only argument of empty_db is the name of a new database *)

(* Theorems are added with add_thms *)
add_thms db [
  "ARITH_MULT", ARITH_MULT, [];
  "ARITH_SUC", ARITH_SUC, [];
  "ARITH_ADD", ARITH_ADD, [];
];;

(* The first argument of add_thms is a database. The second argument
is a list of theorems. Each element of this list is a triple:
the OCaml name of a theorem, a theorem itself, a list of constants for
manual instantiation of types (will be explained later). *)

(* add_thms mutates the db but it also returns db. So it is convenient
to combine two steps above as follows *)
let db = add_thms (empty_db "first") [
  "ARITH_MULT", ARITH_MULT, [];
  "ARITH_SUC", ARITH_SUC, [];
  "ARITH_ADD", ARITH_ADD, [];
];;

(* Now we can compile and save compilation results in a file *)
(* Note: it may be necessary to change the name and/or path of 
the output file on your machine *)
write_rules_names db "examples/out_first.hl" ["SUC"; "+"; "*"];;

(* We can load the created file *)
loadt "examples/out_first.hl";;

(* Compiled functions are called "f_..." where ... is a name of the corresponding
constants. Some names are not supported by OCaml so they are modified.
For instance, "+" becomes "ADD", "*" becomes "MUL", etc. *)

(* Returns |- SUC 30 = 31 *)
f_SUC `30` None;;
(* Returns |- 23 + 44 = 67 *)
f_ADD `23` `44` None;;
(* Returns |- 23 * 33 = 759 *)
f_MUL `23` `33` None;;

(* Compiled rules are invoked with terms as arguments and they return equational
theorems. The last argument of compiled rules is an optional theorem.
This argument is important for implementing tail call elimination for
tail recursive definitions. It is enough to call compiled rules with None to
get final results. *)

(* Compiled rules only accept terms which are in normalized forms which are 
recognized by underlying equational theorems *)

(* Failure: No match *)
f_SUC `1 + 2` None;;
(* This argument is acceptable *)
f_SUC `BIT0 (BIT1 _0)` None;;
(* This also works *)
f_SUC `BIT0 n` None;;
(* And this fails because f_SUC recursively calls itself for `n` *)
f_SUC `BIT1 n` None;;

(* write_rules_names compiles rules corresponding to the given constant
names and saves compiled code in a file. 
All compiled rules are written in the same order as in the list of 
constant names. The rule for "+" depends on the rule for "SUC" so "+" 
must follow "SUC" in the list of names.
It may be difficult to keep track of dependencies manually. Moreover,
some rules are mutually recursive and it is impossible to specify
a linear order for such rules.
So it is recommended to use a special function for computing
dependencies before compiling and writing results into a file. *)

(* Add ARITH_GE and ARITH_GT which are mutually recursive *)
add_thms db [
  "ARITH_GE", ARITH_GE, [];
  "ARITH_GT", ARITH_GT, [];
];;

(* We can try to use write_rules_names *)
write_rules_names db "examples/out_first.hl" [">"; ">="; "SUC"];;

(* But the output file cannot be loaded: f_GT calls f_GE which is
defined later in the same file *)
loadt "examples/out_first.hl";;

(* One solution is to use a more general function write_rules_consts *)
write_rules_consts db "examples/out_first.hl" [[`>`; `>=`]; [`SUC`]];;

(* This function takes a list of lists of constants. Constants which belong to
the same inner list are combined together and yield mutually recursive 
functions. *)
loadt "examples/out_first.hl";;
f_GE `4` `4` None;;
f_GT `4` `4` None;;

(* But it is still difficult to keep track of all dependencies. So it
is better to compute all dependencies automatically and then call
write_rules_consts *)
let consts = dependencies db `a > b /\ a >= SUC b`;;
write_rules_consts db "examples/out_first.hl" consts;;
loadt "examples/out_first.hl";;
f_GE `5` `6` None;;

(* The function "dependencies" takes a database and a term as arguments.
The term must contain all constants for which dependencies are computed.
This function returns a list of lists of constants which is accepted
by write_rules_consts. *)

(* write_rules_consts (and write_rules_names) has an optional argument
"term". This argument may be used to compile and evaluate a single
term. *)

write_rules_consts db "examples/out_first.hl" consts ~term:`3 > 4`;;
loadt "examples/out_first.hl";;
(* The term evaluation is in the variable "result" *)
result;;

(* It is also possible to associate custom functions with constants in
a database. For example, let's add a function for computing factorials. *)

set_rule db `FACT`;;

(* Now we need to define a function called f_FACT *)
let f_FACT =
  let op = `FACT` in
  fun n opt_th -> trans_opt opt_th (NUM_FACT_CONV (mk_comb (op, n)));;

(* We have used the predefined function trans_opt which performs the
standard TRANS rule if the first argument is not None. *)

let tm = `FACT (10 + 10)`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_first.hl" consts ~term:tm;;
loadt "examples/out_first.hl";;
result;;

(* We can give a different name to our predefined function using the optional
argument "name" of "set_rule" *)
let db = add_thms (empty_db "first") [
  "ARITH_MULT", ARITH_MULT, [];
  "ARITH_SUC", ARITH_SUC, [];
  "ARITH_ADD", ARITH_ADD, [];
];;

set_rule db `FACT` ~name:"factorial";;
let factorial = f_FACT;;

let tm = `FACT (10 + 10)`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_first.hl" consts ~term:tm;;
loadt "examples/out_first.hl";;
result;;
factorial `30` None;;

(* We can load a predefined database which contains arithmetic operations
for natural numbers (implemented with standard conversions NUM_..._CONV) and
equality operations for natural numbers, pairs, lists, and optional types *)

needs "eval_default_db.hl";;
let db = default_db "default";;
let tm = `([SOME (FACT 5)] = [NONE]), 300 DIV 4 + 300 MOD 4`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_first.hl" consts ~term:tm;;
loadt "examples/out_first.hl";;
result;;

(*****************************************************************************)
(* Functional arguments and type instantiations                              *)
(*****************************************************************************)

(* It is possible to have polymorphic definitions *)
let db = add_thms (empty_db "second") [
  "ARITH_SUC", ARITH_SUC, [];
  "MAP", MAP, [];
];;

let tm = `MAP SUC [1;SUC 2;3]`;;
write_rules_names db "examples/out_2.hl" ["SUC"; "MAP"] ~term:tm;;
loadt "examples/out_2.hl";;
result;;

(* The function f_MAP is polymorphic and it takes one functional argument.
Functional arguments are pairs of a term and a function. Terms specify
head symbols of the corresponding operations. *)
f_MAP (`SUC`, f_SUC) `[1]` None;;
f_MAP (`SUC`, f_SUC) `[]:(num)list` None;;
f_MAP (`MAP SUC`, f_MAP (`SUC`, f_SUC)) `[[1; 2]; [3; 4]; []]` None;;

(* We can restrict our definitions to particular types only *)
let db = add_thms (empty_db "second") [
  "ARITH_SUC", ARITH_SUC, [];
  "MAP", MAP, [`MAP:(num->num)->(num)list->(num)list`];
];;

let tm = `MAP SUC [1;SUC 2;3]`;;
write_rules_names db "examples/out_2.hl" ["SUC"; "MAP"] ~term:tm;;
loadt "examples/out_2.hl";;

(* Now the MAP function is called f_MAP_num_num and we can use it only
with `:num->num` and `:(num)list` arguments *)
f_MAP_num_num (`SUC`, f_SUC) `[1]` None;;

(* The advantage of f_MAP_num_num is that it is faster than the polymorphic
f_MAP function. It is also possible to produce both restricted and
polymorphic functions. *)
let db = add_thms (empty_db "second") [
  "ARITH_SUC", ARITH_SUC, [];
  "MAP", MAP, [`MAP:(A->B)->(A)list->(B)list`; `MAP:(num->num)->(num)list->(num)list`];
];;

write_rules_names db "examples/out_2.hl" ["SUC"; "MAP"] ~term:tm;;
loadt "examples/out_2.hl";;
result;;

(* Note that the term tm = `MAP SUC [1;SUC 2;3]` is evaluated with
f_MAP_num_num *)
f_MAP (`MAP SUC`, f_MAP (`SUC`, f_SUC)) `[[1; 2]; [3; 4]; []]` None;;
f_MAP (`SUC`, f_SUC) `[1]` None;;
f_MAP_num_num (`SUC`, f_SUC) `[1]` None;;

(* It may be very difficult to select appropriate type instantiations
for all terms in a database. We again can use the function "dependencies"
to compute all required type instantiations automatically. *)
let tm = `MAP (MAP SUC) [[1; 2]; [3; 4]]`;;
let consts = dependencies db tm;;
(* Note that "consts" has two entries for `MAP` with different types. *)
(* The function "dependencies" mutates the database and now the database has
entries for MAP with specific types. *)

write_rules_consts db "examples/out_2.hl" consts ~term:tm;;
loadt "examples/out_2.hl";;
result;;

(* There are two functions for evaluating MAP: f_MAP_num_num and
f_MAP_num_list_num_list *)

(* It is possible to suppress automatic type instantiation when
calling the "dependencies" function *)

let db = add_thms (empty_db "second") [
  "ARITH_SUC", ARITH_SUC, [];
  "MAP", MAP, [];
];;

let consts = dependencies db tm ~inst_types:false;;
write_rules_consts db "examples/out_2.hl" consts ~term:tm;;
(* Now there is only one polymorphic f_MAP *)
loadt "examples/out_2.hl";;
result;;

(* In rare cases it is still necessary to provide types explicitly in
add_thms. Consider the following database with theorems for (=). *)

let db = add_thms (empty_db "eq") [
  "ARITH_EQ", ARITH_EQ, [];
  "PAIR_EQ", PAIR_EQ, [];
  "ARITH_SUC", ARITH_SUC, [];
  "MAP", MAP, [];
];;

let tm = `MAP ((=) (3, 4)) [(1,2); (3,4); (3,SUC 3)]`;;
let consts = dependencies db tm;;

(* We add an automatic call counter for (=) for a demonstration.
Call counters and other extra parameters will be explained later. *)
set_extra_for_names db (Extra_counter 0) ["="];;

write_rules_consts db "examples/out_eq.hl" consts ~term:tm;;
reset_all_counters();;
loadt "examples/out_eq.hl";;
result;;
(* f_EQ_num: 21, f_EQ_num_num: 3 *)
get_all_counters();;

(* One disadvantage of produced definitions is that both ARITH_EQ and PAIR_EQ
need to do quite a lot of work to prove that structurely equal terms are
indeed equal (f_EQ_num is called 21 times). It is much simpler to prove 
structural equality with reflexivity. *)

(* Let's add a reflexivity theorem. Note that it must be added
before ARITH_EQ and PAIR_EQ because compiled definitions will match
all cases in the same order as they are defined in a database. *)
let EQ_REFL' = EQT_INTRO (SPEC_ALL EQ_REFL);;

let db = add_thms (empty_db "eq") [
  "EQ_REFL'", EQ_REFL', [];
  "ARITH_EQ", ARITH_EQ, [];
  "PAIR_EQ", PAIR_EQ, [];
  "ARITH_SUC", ARITH_SUC, [];
  "MAP", MAP, [];
];;

(* Unfortunately, this does not work because "dependencies" assumes that
it is enough to have EQ_REFL' rule only to compare pairs of numbers. *)
let consts = dependencies db tm;;
write_rules_consts db "examples/out_eq.hl" consts ~term:tm;;
loadt "examples/out_eq.hl";;

(* It is necessary to instantiate types of both EQ_REFL' and PAIR_EQ to
get the desired result *)

let db = add_thms (empty_db "eq") [
  "EQ_REFL'", EQ_REFL', [`(=):num#num->num#num->bool`; `(=):num->num->bool`];
  "ARITH_EQ", ARITH_EQ, [];
  "PAIR_EQ", PAIR_EQ, [`(=):num#num->num#num->bool`];
  "ARITH_SUC", ARITH_SUC, [];
  "MAP", MAP, [];
];;

let consts = dependencies db tm;;
set_extra_for_names db (Extra_counter 0) ["="];;
write_rules_consts db "examples/out_eq.hl" consts ~term:tm;;
reset_all_counters();;
loadt "examples/out_eq.hl";;
result;;
(* f_EQ_num: 3, f_EQ_num_num: 3 *)
get_all_counters();;

(*****************************************************************************)
(* Abstractions                                                              *)
(*****************************************************************************)

(* Both simple and generalized abstractions are supported *)

let abs_def = new_definition `abs_def s = MAP (\(x, y). x + y) s`;;
let abs_def2 = new_definition `abs_def2 s = MAP (\(x, y). [x; y]) s`;;
let abs_def3 = new_definition `abs_def3 z s = MAP (\(x, y). [x; y; z]) s`;;

let db = add_thms (empty_db "abs") [
  "abs_def", abs_def, [];
  "abs_def2", abs_def2, [];
  "abs_def3", abs_def3, [];
  "ARITH_SUC", ARITH_SUC, [];
  "ARITH_ADD", ARITH_ADD, [];
  "MAP", MAP, [];
];;

let tm = `abs_def [1,2; 3,4]`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_abs.hl" consts ~term:tm;;
loadt "examples/out_abs.hl";;
result;;

let tm = `abs_def2 [1,2; 3,4]`;;
let consts = dependencies db tm ~inst_types:false;;
write_rules_consts db "examples/out_abs.hl" consts ~term:tm;;
loadt "examples/out_abs.hl";;
result;;

let tm = `abs_def3 0 [1,2; 3,4]`;;
let consts = dependencies db tm ~inst_types:false;;
write_rules_consts db "examples/out_abs.hl" consts ~term:tm;;
loadt "examples/out_abs.hl";;
result;;

let tm = `MAP (\x. CONS x [1]) [1;2;3]`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_abs.hl" consts ~term:tm;;
loadt "examples/out_abs.hl";;
result;;

(* "match" is also supported *)
let match_map = define 
  `match_map f xs = 
    match xs with 
    | [] -> [] 
    | CONS x xs -> CONS (f x) (match_map f xs)`;;

add_thms db ["match_map", match_map, []];;

let tm = `match_map (\x. CONS x [1]) [1;2;3]`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_abs.hl" consts ~term:tm;;
loadt "examples/out_abs.hl";;
result;;

(* "let" is not supported directly (it may change in future versions)
but it is easy to replace "let" with abstractions. *)
let let_def = define `let_def x = let t = SUC x in t + t`;;
let let_def' = PURE_REWRITE_RULE[LET_DEF; LET_END_DEF] let_def;;

add_thms db ["let_def'", let_def', []];;
let tm = `let_def 30`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_abs.hl" consts ~term:tm;;
loadt "examples/out_abs.hl";;
result;;

(* For this simple definition it is better to expand let completely and
eliminate abstractions. The compiled definition will compute `SUC x` only once. *)
let let_def'' = REWRITE_RULE[LET_DEF; LET_END_DEF] let_def;;

let db = add_thms (empty_db "let") [
  "let_def''", let_def'', [];
  "ARITH_SUC", ARITH_SUC, [];
  "ARITH_ADD", ARITH_ADD, [];
];;
let tm = `let_def 30`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_abs.hl" consts ~term:tm;;
loadt "examples/out_abs.hl";;
result;;

(* Abstractions can be automatically eliminated. Abstractions
slow down evaluations because the INST primitive inference rule
has to consider possible variable captures for abstractions. *)

let db = add_thms (empty_db "abs" ~eliminate_abs:true) [
  "abs_def", abs_def, [];
  "abs_def2", abs_def2, [];
  "abs_def3", abs_def3, [];
  "ARITH_SUC", ARITH_SUC, [];
  "ARITH_ADD", ARITH_ADD, [];
  "MAP", MAP, [];
];;

let tm = `abs_def2 [1,2; 3,4]`;;
let consts = dependencies db tm ~inst_types:false;;
(* Note that consts contains a special constant `$1`. This constant corresponds
to a new automatically produced definition which eliminated the abstraction in
abs_def2. *)
write_rules_consts db "examples/out_abs.hl" consts ~term:tm;;
loadt "examples/out_abs.hl";;
result;;

let tm = `abs_def3 0 [1,2; 3,4]`;;
let consts = dependencies db tm ~inst_types:false;;
write_rules_consts db "examples/out_abs.hl" consts ~term:tm;;
loadt "examples/out_abs.hl";;
result;;

(* Abstractions are not eliminated in terms *)
let tm = `MAP (\x. CONS x [1]) [1;2;3]`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_abs.hl" consts ~term:tm;;
loadt "examples/out_abs.hl";;
result;;

(*****************************************************************************)
(* Short-circuit evaluations                                                 *)
(*****************************************************************************)

(* The second argument of /\ and \/ is evaluated only when the first
argument is T for /\ and F for \/. Also only one branch of 
"if" is evaluated. *)

let inf_bool = define `(inf_bool n):bool = inf_bool (SUC n)`;;

let db = add_thms (empty_db "lazy") [
  "ARITH_EQ", ARITH_EQ, [];
  "ARITH_SUC", ARITH_SUC, [];
  "MAP", MAP, [];
  "ALL", ALL, [];
  "inf_bool", inf_bool, [];
];;

let tm = `MAP (\x. if x = 3 then inf_bool 0 else F) [1;2]`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_lazy.hl" consts ~term:tm;;
loadt "examples/out_lazy.hl";;
result;;

let tm = `ALL (\x. x = 3 /\ inf_bool 0) [1;3;3]`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_lazy.hl" consts ~term:tm;;
loadt "examples/out_lazy.hl";;
result;;

let tm = `ALL (\x. x = 3 \/ inf_bool 0) [3;3;3]`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_lazy.hl" consts ~term:tm;;
loadt "examples/out_lazy.hl";;
result;;

(*****************************************************************************)
(* Extra parameters and memoization                                           *)
(*****************************************************************************)

(* It is possible to specify global preprocessing operations for theorems
in a database. There are two preprocessing steps: rewritings with
some theorems and applying some rules. *)

(* Suppose we want to eliminate "let" definitions for all theorems in
our database. Then we can rewrite all theorems with LET_DEF and LET_END_DEF. *)

let let_def = define `let_def x = let t = SUC x in t + t`;;

let db = empty_db "extra";;

add_extra_rewrite db ("LET_DEF", LET_DEF);;
add_extra_rewrite db ("LET_END_DEF", LET_END_DEF);;

(* Note that preprocessing steps are applied when theorems are added
to a database and when compiled definitions are loaded. So it is important
to define preprocessing steps before adding theorems to a database. Also
all preprocessing theorems and conversions must be available when 
the compiled definitions are loaded. *)

add_thms db [
  "ARITH_SUC", ARITH_SUC, [];
  "ARITH_ADD", ARITH_ADD, [];
  "let_def", let_def, [];
];;

let tm = `let_def 3`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_extra.hl" consts ~term:tm;;
loadt "examples/out_extra.hl";;

(* Alternatively we may eliminate "let" completely with let_CONV *)

let db = empty_db "extra";;
add_extra_rule db ("CONV_RULE (DEPTH_CONV let_CONV)", CONV_RULE (DEPTH_CONV let_CONV));;

add_thms db [
  "ARITH_SUC", ARITH_SUC, [];
  "ARITH_ADD", ARITH_ADD, [];
  "let_def", let_def, [];
];;

let tm = `let_def 3`;;
let consts = dependencies db tm;;
write_rules_consts db "examples/out_extra.hl" consts ~term:tm;;
loadt "examples/out_extra.hl";;

(* We can associate extra parameters with each constant in a database.
These parameters are used for adding extra features to the generated code. *)

(* We can generate call counters for specific functions. 
These counters can be used to track how many times a given function is invoked. *)

(* Extra_counter takes one integer argument: if this argument is greater than 0
then the counter value is printed during the evaluation process when the counter
value is divisble by this argument. *)
set_extra_for_all db (Extra_counter 0);;
set_extra_for_names db (Extra_counter 10) ["SUC"];;

write_rules_names db "examples/out_extra.hl" ["SUC"; "+"];;
loadt "examples/out_extra.hl";;

(* It is recommended to reset all counters before evaluation *)
reset_all_counters();;
f_ADD `65535` `1023` None;;
get_counter "f_SUC";;
get_all_counters();;

(* We can improve performance of some functions if we memoize their results.
Different memoization implementations are available: standard Hashtbl,
associative arrays which always have a constant number of entries, and
LRU associative arrays which also have a constant number of entries. *)

let fib = define `fib n = if n < 2 then n else fib (n - 1) + fib (n - 2)`;;

let db = add_thms (empty_db "extra") [
  "ARITH_EQ", ARITH_EQ, [];
  "ARITH_PRE", ARITH_PRE, [];
  "ARITH_LE", ARITH_LE, [];
  "ARITH_LT", ARITH_LT, [];
  "ARITH_SUB", ARITH_SUB, [];
  "ARITH_SUC", ARITH_SUC, [];
  "ARITH_ADD", ARITH_ADD, [];
  "fib", fib, [];
];;

let consts = dependencies db `fib 10`;;
write_rules_consts db "examples/out_extra.hl" consts;;
loadt "examples/out_extra.hl";;

(* Very slow *)
f_fib `25` None;;

set_extra_for_consts db (Extra_memo Hashtbl_memo) [`fib`];;
write_rules_consts db "examples/out_extra.hl" consts;;
loadt "examples/out_extra.hl";;

(* Very fast *)
clear_all_memos();;

f_fib `25` None;;
f_fib `100` None;;

(* We could also use:
Extra_memo (Assoc_memo 1000)
Extra_memo (Assoc_lru (1000, 2))
1000 here is the size of the corresponding associative array.
*)

(* Note that memoized functions are not tail recursive *)

(* If we want to discover which functions should be memoized it may be useful
to add Extra_arg_list to all functions in order to record all calls with all
arguments. *)

let db = add_thms (empty_db "extra") [
  "ARITH_EQ", ARITH_EQ, [];
  "ARITH_PRE", ARITH_PRE, [];
  "ARITH_LE", ARITH_LE, [];
  "ARITH_LT", ARITH_LT, [];
  "ARITH_SUB", ARITH_SUB, [];
  "ARITH_SUC", ARITH_SUC, [];
  "ARITH_ADD", ARITH_ADD, [];
  "fib", fib, [];
];;

set_extra_for_all db Extra_arg_list;;
let consts = dependencies db `fib 10`;;
write_rules_consts db "examples/out_extra.hl" consts;;
loadt "examples/out_extra.hl";;

clear_arg_lists();;
f_fib `15` None;;

all_arg_lists();;

let args = !(create_arg_list "f_fib") |> map hd;;
(* 1973 *)
length args;;
(* 16 *)
length (setify_terms args);;

(* It is obvious that a function which is called 1973 times with only 16
different arguments must be memoized. *)

(* There are some useful functions for analyzing lists of arguments *)

(* Compute frequencies of all elements in a list and sort them 
from most to less frequent *)
freqs args;;

(* Returns a pair: a number between 0 and 1 which measures the proportion
of repeated arguments (0 - all unique, 1 - all repeated) and the number
of all arguments. *)
analyze_arg_list !(create_arg_list "f_fib");;

(* Applies analyze_arg_list to all lists of arguments *)
analyze_arg_lists();;

(* If we call a function with bad arguments we do not get an informative
error message by default *)
f_fib `BIT0 (BIT1 _0)` None;;

(* We can compile functions with better error messages by setting the global
flag generate_eval_errors *)
generate_eval_errors := true;;
write_rules_consts db "examples/out_extra.hl" consts;;
loadt "examples/out_extra.hl";;

f_fib `BIT0 (BIT1 _0)` None;;

(* Now we can see that the function f_EQ_num cannot evaluate arguments
`BIT0 (BIT1 _0)` and `0` *)

(* Note that when generate_eval_errors := true then all functions are
not tail recursive *)

generate_eval_errors := false;;

(*****************************************************************************)
(* Limitations                                                               *)
(*****************************************************************************)

(* The main limitation of the current version of the evaluation tool is that
it cannot produce code for functions which return other functions. The following
constructions are also not allowed: `(if x = 2 then SUC else PRE) 3`. Rators
should not reduce to functions. Functions cannot be passed inside lists, pairs
or any other structures: `MAP (\f. f 3) [SUC; PRE]`. *)

(* This limitations may be removed in later versions of the evaluation tool. *)

(* "match" without elimination of abstractions is only supported when it is
a top level operation. *)