Implement OCaml API + Add regression

.github/workflows/regression-tests.yml

@@ -0,0 +1,14 @@
+name: Regression Tests
+
+on:
+  push:
+    branches: [master]
+  pull_request:
+    branches: [master]
+
+jobs:
+  test:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - run: ./test.sh

.gitignore

@@ -31,4 +31,8 @@ cake-x64-64.tar.gz
 cake-x64-64
 cake
 config_enc_str.txt
-checkpoint
+checkpoint
+
+candle_boot.ml
+types.txt
+candle_insulate.ml

Help/UNIFY_ACCEPT_TAC.hlp

@@ -1,6 +1,6 @@
 \DOC UNIFY_ACCEPT_TAC
 
-\TYPE {UNIFY_ACCEPT_TAC : term list -> thm -> 'a * term -> ('b list * instantiation) * 'c list * (instantiation -> 'd list -> thm)}
+\TYPE {UNIFY_ACCEPT_TAC : term list -> thm_tactic}
 
 \SYNOPSIS
 Unify free variables in theorem and metavariables in goal to accept theorem.
@@ -75,6 +75,6 @@ in the remaining goal, which we can solve easily:
 Terminating proof search when using metavariables. Used in {ITAUT_TAC}
 
 \SEEALSO
-ACCEPT_TAC, ITAUT, ITAUT_TAC, MATCH_ACCEPT_TAC.
+ACCEPT_TAC, ITAUT, ITAUT_TAC, MATCH_ACCEPT_TAC, UNIFY_REFL_TAC.
 
 \ENDDOC

Help/UNIFY_REFL_TAC.hlp

@@ -0,0 +1,57 @@
+\DOC UNIFY_REFL_TAC
+
+\TYPE {UNIFY_REFL_TAC : tactic}
+
+\SYNOPSIS
+Unify term(s) and metavariable(s) in the equality of the goal.
+
+\DESCRIBE
+Given a goal {_ ?- x = y} where {y} is a metavariable, the tactic
+{UNIFY_REFL_TAC} attempts to unify {y} with {x}.
+If {y} is function application {f a b c} and {f} is a metavariable,
+{UNIFY_REFL_TAC} attemps to unify {f} with {\a b c. x} (the number of arguments
+can vary).
+
+\FAILURE
+Fails if no unification will work.
+
+\EXAMPLE
+{
+  # g `?x. 1 = x`;;
+  ...
+
+  # e META_EXISTS_TAC;;
+	val it : goalstack = 1 subgoal (1 total)
+
+	`1 = x`
+
+	# e UNIFY_REFL_TAC;;
+
+	val it : goalstack = No subgoals
+}
+\noindent If the RHS is function application:
+{
+	# g `?f. y + z = f y z`;;
+	...
+
+	# e (META_EXISTS_TAC THEN UNIFY_REFL_TAC);;
+	val it : goalstack = No subgoals
+}
+\noindent The arguments to {f} can be constants, but {UNIFY_REFL_TAC} will
+print a warning.
+{
+	# g `?f. y + 1 = f y 0`;;
+	...
+
+	# e (META_EXISTS_TAC THEN UNIFY_REFL_TAC);;
+	UNIFY_REFL_TAC: warning: this isn't var: 0
+	val it : goalstack = No subgoals
+}
+
+\USES
+Terminating proof search when using metavariables.
+
+\SEEALSO
+UNIFY_ACCEPT_TAC
+
+\ENDDOC

Library/calc_real.ml

@@ -1725,7 +1725,9 @@ let ELIMINATE_DEF =
 (* Overall conversion.                                                       *)
 (* ------------------------------------------------------------------------- *)
 
-let realcalc_cache = ref [];;
+type realcalc =
+  ((num * num) ref * (num -> num)) * ((num * thm) ref * (num -> thm))
+let realcalc_cache = ref ([] : (term * realcalc) list)
 
 let REALCALC_CONV,thm_eval,raw_eval,thm_wrap =
   let a_tm = `a:real` and n_tm = `n:num` and n'_tm = `n':num`
@@ -2095,7 +2097,7 @@ let REALCALC_CONV,thm_eval,raw_eval,thm_wrap =
       let ax0 = abs_num x0 in
       let r = log2(ax0) -/ num 1 in
       let get_ek(acc) =
-        if r < num 0 then
+        if r </ num 0 then
           let p = find_msd rfn in
           let e = acc +/ p +/ num 1 in
           let k = e +/ p in e,k
@@ -2170,7 +2172,7 @@ let REALCALC_CONV,thm_eval,raw_eval,thm_wrap =
         and q = log2(abs_num(raw_eval rfn2 s)) in
         let k = q +/ r +/ num 1
         and l = p +/ s +/ num 1 in
-        if p =/ num 0 && q = num 0 then
+        if p =/ num 0 && q =/ num 0 then
           if k </ l then k +/ num 1,l else k,l +/ num 1
         else k,l in
       let raw_fn acc =