Merge pull request #119 from aqjune-aws/reduce_conv

Add conversions of num/int/rat/real/word that evaluate expressions using Compute
jrh13 · Nov 20, 2024 · 4eef6f6 · 4eef6f6
2 parents 9eccc5e + 7915d48
commit 4eef6f6
Show file tree

Hide file tree

Showing 8 changed files with 215 additions and 121 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -34,6 +34,7 @@ jobs:
 
       - name: Run
         run: |
+          set -e
           cd hol-light
           eval $(opam env)
           make
@@ -58,6 +59,7 @@ jobs:
 
       - name: Run
         run: |
+          set -e
           cd hol-light
           make switch
           eval $(opam env)
@@ -69,6 +71,7 @@ jobs:
 
       - name: Run (HOLLIGHT_USE_MODULE=1)
         run: |
+          set -e
           cd hol-light
           eval $(opam env)
           make clean

diff --git a/Library/words.ml b/Library/words.ml
@@ -8101,77 +8101,92 @@ let WORD_JREM_CONV =
   RAND_CONV (LAND_CONV WORD_JDIV_CONV THENC WORD_MUL_CONV) THENC
   WORD_SUB_CONV;;
 
+let word_red_conv_list =
+ [`word(NUMERAL n):N word`,CHANGED_CONV WORD_WORD_CONV;
+  `word_saturate(NUMERAL n):N word`,WORD_SATURATE_CONV;
+  `iword i:N word`,WORD_IWORD_CONV;
+  `iword_saturate(n):N word`,IWORD_SATURATE_CONV;
+  `val(w:N word)`,WORD_VAL_CONV;
+  `ival(w:N word)`,WORD_IVAL_CONV;
+  `bit (NUMERAL k) (word(NUMERAL n):N word)`,WORD_BIT_CONV;
+  `word(NUMERAL m):N word = word(NUMERAL n)`,WORD_EQ_CONV;
+  `word_ult (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_ULT_CONV;
+  `word_ule (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_ULE_CONV;
+  `word_ugt (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_UGT_CONV;
+  `word_uge (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_UGE_CONV;
+  `word_ilt (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_ILT_CONV;
+  `word_ile (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_ILE_CONV;
+  `word_igt (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_IGT_CONV;
+  `word_ige (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_IGE_CONV;
+  `word_neg (word(NUMERAL n):N word)`,WORD_NEG_CONV;
+  `word_add (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_ADD_CONV;
+  `word_mul (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_MUL_CONV;
+  `word_sub (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_SUB_CONV;
+  `word_udiv (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_UDIV_CONV;
+  `word_umod (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_UMOD_CONV;
+  `word_umax (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_UMAX_CONV;
+  `word_umin (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_UMIN_CONV;
+  `word_imax (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_IMAX_CONV;
+  `word_imin (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_IMIN_CONV;
+  `word_shl (word(NUMERAL m):N word) (NUMERAL n)`,WORD_SHL_CONV;
+  `word_ushr (word(NUMERAL m):N word) (NUMERAL n)`,WORD_USHR_CONV;
+  `word_ishr (word(NUMERAL m):N word) (NUMERAL n)`,WORD_ISHR_CONV;
+  `word_not (word(NUMERAL n):N word)`,WORD_NOT_CONV;
+  `word_and (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_AND_CONV;
+  `word_or (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_OR_CONV;
+  `word_xor (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_XOR_CONV;
+  `word_rol (word(NUMERAL m):N word) (NUMERAL n)`,WORD_ROL_CONV;
+  `word_ror (word(NUMERAL m):N word) (NUMERAL n)`,WORD_ROR_CONV;
+  `word_zx (word(NUMERAL n):N word)`,WORD_ZX_CONV;
+  `word_sx (word(NUMERAL n):N word)`,WORD_SX_CONV;
+  `word_sxfrom (NUMERAL m) (word(NUMERAL n):N word)`,WORD_SXFROM_CONV;
+  `word_cand (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_CAND_CONV;
+  `word_cor (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_COR_CONV;
+  `word_join (word(NUMERAL m):M word) (word(NUMERAL n):N word)`,
+              WORD_JOIN_CONV;
+  `word_subword (word(NUMERAL m):M word) (NUMERAL p,NUMERAL q):N word`,
+              WORD_SUBWORD_CONV;
+  `word_insert (word(NUMERAL m):M word) (NUMERAL p,NUMERAL q)
+               (word(NUMERAL n):N word):P word`,
+              WORD_INSERT_CONV;
+  `word_duplicate (word(NUMERAL m):M word):N word`,WORD_DUPLICATE_CONV;
+  `bits_of_word (word(NUMERAL n):N word)`,WORD_BITS_OF_WORD_CONV;
+  `word_popcount (word(NUMERAL n):N word)`,WORD_POPCOUNT_CONV;
+  `word_evenparity (word(NUMERAL n):N word)`,WORD_EVENPARITY_CONV;
+  `word_oddparity (word(NUMERAL n):N word)`,WORD_ODDPARITY_CONV;
+  `word_ctz (word(NUMERAL n):N word)`,WORD_CTZ_CONV;
+  `word_clz (word(NUMERAL n):N word)`,WORD_CLZ_CONV;
+  `word_bytereverse (word(NUMERAL n):((((N)tybit0)tybit0)tybit0)word)`,
+              WORD_BYTEREVERSE_CONV;
+  `word_reversefields (NUMERAL b) (word(NUMERAL n):N word)`,
+              WORD_REVERSEFIELDS_CONV;
+  `word_jshl (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JSHL_CONV;
+  `word_jshr (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JSHR_CONV;
+  `word_jushr (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JUSHR_CONV;
+  `word_jrol (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JROL_CONV;
+  `word_jror (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JROR_CONV;
+  `word_jdiv (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JDIV_CONV;
+  `word_jrem (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JREM_CONV];;
+
 let WORD_RED_CONV =
-  let gconv_net = itlist (uncurry net_of_conv)
-   [`word(NUMERAL n):N word`,CHANGED_CONV WORD_WORD_CONV;
-    `word_saturate(NUMERAL n):N word`,WORD_SATURATE_CONV;
-    `iword i:N word`,WORD_IWORD_CONV;
-    `iword_saturate(n):N word`,IWORD_SATURATE_CONV;
-    `val(w:N word)`,WORD_VAL_CONV;
-    `ival(w:N word)`,WORD_IVAL_CONV;
-    `bit (NUMERAL k) (word(NUMERAL n):N word)`,WORD_BIT_CONV;
-    `word(NUMERAL m):N word = word(NUMERAL n)`,WORD_EQ_CONV;
-    `word_ult (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_ULT_CONV;
-    `word_ule (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_ULE_CONV;
-    `word_ugt (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_UGT_CONV;
-    `word_uge (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_UGE_CONV;
-    `word_ilt (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_ILT_CONV;
-    `word_ile (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_ILE_CONV;
-    `word_igt (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_IGT_CONV;
-    `word_ige (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_IGE_CONV;
-    `word_neg (word(NUMERAL n):N word)`,WORD_NEG_CONV;
-    `word_add (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_ADD_CONV;
-    `word_mul (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_MUL_CONV;
-    `word_sub (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_SUB_CONV;
-    `word_udiv (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_UDIV_CONV;
-    `word_umod (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_UMOD_CONV;
-    `word_umax (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_UMAX_CONV;
-    `word_umin (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_UMIN_CONV;
-    `word_imax (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_IMAX_CONV;
-    `word_imin (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_IMIN_CONV;
-    `word_shl (word(NUMERAL m):N word) (NUMERAL n)`,WORD_SHL_CONV;
-    `word_ushr (word(NUMERAL m):N word) (NUMERAL n)`,WORD_USHR_CONV;
-    `word_ishr (word(NUMERAL m):N word) (NUMERAL n)`,WORD_ISHR_CONV;
-    `word_not (word(NUMERAL n):N word)`,WORD_NOT_CONV;
-    `word_and (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_AND_CONV;
-    `word_or (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_OR_CONV;
-    `word_xor (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_XOR_CONV;
-    `word_rol (word(NUMERAL m):N word) (NUMERAL n)`,WORD_ROL_CONV;
-    `word_ror (word(NUMERAL m):N word) (NUMERAL n)`,WORD_ROR_CONV;
-    `word_zx (word(NUMERAL n):N word)`,WORD_ZX_CONV;
-    `word_sx (word(NUMERAL n):N word)`,WORD_SX_CONV;
-    `word_sxfrom (NUMERAL m) (word(NUMERAL n):N word)`,WORD_SXFROM_CONV;
-    `word_cand (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_CAND_CONV;
-    `word_cor (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_COR_CONV;
-    `word_join (word(NUMERAL m):M word) (word(NUMERAL n):N word)`,
-                WORD_JOIN_CONV;
-    `word_subword (word(NUMERAL m):M word) (NUMERAL p,NUMERAL q):N word`,
-                WORD_SUBWORD_CONV;
-    `word_insert (word(NUMERAL m):M word) (NUMERAL p,NUMERAL q)
-                 (word(NUMERAL n):N word):P word`,
-                WORD_INSERT_CONV;
-    `word_duplicate (word(NUMERAL m):M word):N word`,WORD_DUPLICATE_CONV;
-    `bits_of_word (word(NUMERAL n):N word)`,WORD_BITS_OF_WORD_CONV;
-    `word_popcount (word(NUMERAL n):N word)`,WORD_POPCOUNT_CONV;
-    `word_evenparity (word(NUMERAL n):N word)`,WORD_EVENPARITY_CONV;
-    `word_oddparity (word(NUMERAL n):N word)`,WORD_ODDPARITY_CONV;
-    `word_ctz (word(NUMERAL n):N word)`,WORD_CTZ_CONV;
-    `word_clz (word(NUMERAL n):N word)`,WORD_CLZ_CONV;
-    `word_bytereverse (word(NUMERAL n):((((N)tybit0)tybit0)tybit0)word)`,
-                WORD_BYTEREVERSE_CONV;
-    `word_reversefields (NUMERAL b) (word(NUMERAL n):N word)`,
-                WORD_REVERSEFIELDS_CONV;
-    `word_jshl (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JSHL_CONV;
-    `word_jshr (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JSHR_CONV;
-    `word_jushr (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JUSHR_CONV;
-    `word_jrol (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JROL_CONV;
-    `word_jror (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JROR_CONV;
-    `word_jdiv (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JDIV_CONV;
-    `word_jrem (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JREM_CONV]
-  (basic_net()) in
+  let gconv_net = itlist (uncurry net_of_conv) word_red_conv_list (basic_net()) in
   REWRITES_CONV gconv_net;;
 
-let WORD_REDUCE_CONV = DEPTH_CONV WORD_RED_CONV;;
+let WORD_REDUCE_CONV =
+  DEPTH_CONV WORD_RED_CONV;;
+
+let word_compute_add_convs =
+  let convlist = map (fun pat,the_conv ->
+    let c,args = strip_comb pat in (c,length args,the_conv))
+    word_red_conv_list in
+  fun (compset:Compute.compset) ->
+    itlist (fun newc () -> Compute.add_conv newc compset) convlist ();;
+
+let WORD_COMPUTE_CONV =
+  let cs = Compute.bool_compset () in
+  Compute.set_skip cs `COND: bool -> A -> A -> A` (Some 1);
+  word_compute_add_convs cs;
+  Compute.WEAK_CBV_CONV cs;;
 
 (* ------------------------------------------------------------------------- *)
 (* Alternative returning signed words.                                       *)

diff --git a/Makefile b/Makefile
@@ -20,7 +20,7 @@ HOLSRC=system.ml lib.ml fusion.ml basics.ml nets.ml preterm.ml          \
        parser.ml printer.ml equal.ml bool.ml drule.ml tactics.ml        \
        itab.ml simp.ml theorems.ml ind_defs.ml class.ml trivia.ml       \
        canon.ml meson.ml firstorder.ml metis.ml thecops.ml quot.ml      \
-       impconv.ml recursion.ml pair.ml                                  \
+       impconv.ml recursion.ml pair.ml compute.ml                       \
        nums.ml arith.ml wf.ml calc_num.ml normalizer.ml grobner.ml      \
        ind_types.ml lists.ml realax.ml calc_int.ml realarith.ml         \
        real.ml calc_rat.ml int.ml sets.ml iterate.ml cart.ml define.ml  \
@@ -135,7 +135,7 @@ hol_loader.cmo: hol_loader.ml ; \
 hol_loader.cmx: hol_loader.ml ; \
         ocamlopt -verbose -c hol_loader.ml -o hol_loader.cmx
 
-hol_lib_inlined.ml: hol_lib.ml inline_load.ml ; \
+hol_lib_inlined.ml: ${HOLSRC} inline_load.ml ; \
         HOLLIGHT_DIR="`pwd`" ocaml inline_load.ml hol_lib.ml hol_lib_inlined.ml -omit-prelude
 
 hol_lib.cmo: pa_j.cmo hol_lib_inlined.ml hol_loader.cmo bignum.cmo ; \

diff --git a/calc_int.ml b/calc_int.ml
@@ -373,20 +373,35 @@ let REAL_INT_ABS_CONV =
     REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_NUM]) in
   GEN_REWRITE_CONV I [pth];;
 
+let real_int_red_conv_list = 
+  [`x <= y`,REAL_INT_LE_CONV;
+   `x < y`,REAL_INT_LT_CONV;
+   `x >= y`,REAL_INT_GE_CONV;
+   `x > y`,REAL_INT_GT_CONV;
+   `x:real = y`,REAL_INT_EQ_CONV;
+   `--x`,CHANGED_CONV REAL_INT_NEG_CONV;
+   `abs(x)`,REAL_INT_ABS_CONV;
+   `x + y`,REAL_INT_ADD_CONV;
+   `x - y`,REAL_INT_SUB_CONV;
+   `x * y`,REAL_INT_MUL_CONV;
+   `x pow n`,REAL_INT_POW_CONV];;
+
 let REAL_INT_RED_CONV =
-  let gconv_net = itlist (uncurry net_of_conv)
-    [`x <= y`,REAL_INT_LE_CONV;
-     `x < y`,REAL_INT_LT_CONV;
-     `x >= y`,REAL_INT_GE_CONV;
-     `x > y`,REAL_INT_GT_CONV;
-     `x:real = y`,REAL_INT_EQ_CONV;
-     `--x`,CHANGED_CONV REAL_INT_NEG_CONV;
-     `abs(x)`,REAL_INT_ABS_CONV;
-     `x + y`,REAL_INT_ADD_CONV;
-     `x - y`,REAL_INT_SUB_CONV;
-     `x * y`,REAL_INT_MUL_CONV;
-     `x pow n`,REAL_INT_POW_CONV]
+  let gconv_net = itlist (uncurry net_of_conv) real_int_red_conv_list
     (basic_net()) in
   REWRITES_CONV gconv_net;;
 
 let REAL_INT_REDUCE_CONV = DEPTH_CONV REAL_INT_RED_CONV;;
+
+let real_int_compute_add_convs =
+  let convlist = map (fun pat,the_conv ->
+    let c,args = strip_comb pat in (c,length args,the_conv))
+    real_int_red_conv_list in
+  fun (compset:Compute.compset) ->
+    itlist (fun newc () -> Compute.add_conv newc compset) convlist ();;
+
+let REAL_INT_COMPUTE_CONV =
+  let cs = Compute.bool_compset () in
+  Compute.set_skip cs `COND: bool -> A -> A -> A` (Some 1);
+  real_int_compute_add_convs cs;
+  Compute.WEAK_CBV_CONV cs;;
diff --git a/calc_num.ml b/calc_num.ml
@@ -1450,31 +1450,46 @@ let NUM_REL_CONV =
     (basic_net()) in
   REWRITES_CONV gconv_net;;
 
+let num_red_conv_list =
+  [`SUC(NUMERAL n)`,NUM_SUC_CONV;
+   `PRE(NUMERAL n)`,NUM_PRE_CONV;
+   `FACT(NUMERAL n)`,NUM_FACT_CONV;
+   `NUMERAL m < NUMERAL n`,NUM_LT_CONV;
+   `NUMERAL m <= NUMERAL n`,NUM_LE_CONV;
+   `NUMERAL m > NUMERAL n`,NUM_GT_CONV;
+   `NUMERAL m >= NUMERAL n`,NUM_GE_CONV;
+   `NUMERAL m = NUMERAL n`,NUM_EQ_CONV;
+   `EVEN(NUMERAL n)`,NUM_EVEN_CONV;
+   `ODD(NUMERAL n)`,NUM_ODD_CONV;
+   `NUMERAL m + NUMERAL n`,NUM_ADD_CONV;
+   `NUMERAL m - NUMERAL n`,NUM_SUB_CONV;
+   `NUMERAL m * NUMERAL n`,NUM_MULT_CONV;
+   `(NUMERAL m) EXP (NUMERAL n)`,NUM_EXP_CONV;
+   `(NUMERAL m) DIV (NUMERAL n)`,NUM_DIV_CONV;
+   `(NUMERAL m) MOD (NUMERAL n)`,NUM_MOD_CONV;
+   `MAX (NUMERAL m) (NUMERAL n)`,NUM_MAX_CONV;
+   `MIN (NUMERAL m) (NUMERAL n)`,NUM_MIN_CONV];;
+
 let NUM_RED_CONV =
-  let gconv_net = itlist (uncurry net_of_conv)
-    [`SUC(NUMERAL n)`,NUM_SUC_CONV;
-     `PRE(NUMERAL n)`,NUM_PRE_CONV;
-     `FACT(NUMERAL n)`,NUM_FACT_CONV;
-     `NUMERAL m < NUMERAL n`,NUM_LT_CONV;
-     `NUMERAL m <= NUMERAL n`,NUM_LE_CONV;
-     `NUMERAL m > NUMERAL n`,NUM_GT_CONV;
-     `NUMERAL m >= NUMERAL n`,NUM_GE_CONV;
-     `NUMERAL m = NUMERAL n`,NUM_EQ_CONV;
-     `EVEN(NUMERAL n)`,NUM_EVEN_CONV;
-     `ODD(NUMERAL n)`,NUM_ODD_CONV;
-     `NUMERAL m + NUMERAL n`,NUM_ADD_CONV;
-     `NUMERAL m - NUMERAL n`,NUM_SUB_CONV;
-     `NUMERAL m * NUMERAL n`,NUM_MULT_CONV;
-     `(NUMERAL m) EXP (NUMERAL n)`,NUM_EXP_CONV;
-     `(NUMERAL m) DIV (NUMERAL n)`,NUM_DIV_CONV;
-     `(NUMERAL m) MOD (NUMERAL n)`,NUM_MOD_CONV;
-     `MAX (NUMERAL m) (NUMERAL n)`,NUM_MAX_CONV;
-     `MIN (NUMERAL m) (NUMERAL n)`,NUM_MIN_CONV]
+  let gconv_net = itlist (uncurry net_of_conv) num_red_conv_list
     (basic_net()) in
   REWRITES_CONV gconv_net;;
 
 let NUM_REDUCE_CONV = DEPTH_CONV NUM_RED_CONV;;
 
+let num_compute_add_convs =
+  let convlist = map (fun pat,the_conv ->
+    let c,args = strip_comb pat in (c,length args,the_conv))
+    num_red_conv_list in
+  fun (compset:Compute.compset) ->
+    itlist (fun newc () -> Compute.add_conv newc compset) convlist ();;
+
+let NUM_COMPUTE_CONV =
+  let cs = Compute.bool_compset () in
+  Compute.set_skip cs `COND: bool -> A -> A -> A` (Some 1);
+  num_compute_add_convs cs;
+  Compute.WEAK_CBV_CONV cs;;
+
 let NUM_REDUCE_TAC = CONV_TAC NUM_REDUCE_CONV;;
 
 (* ------------------------------------------------------------------------- *)

diff --git a/calc_rat.ml b/calc_rat.ml
@@ -386,29 +386,44 @@ let REAL_RAT_MIN_CONV =
 (* Everything.                                                               *)
 (* ------------------------------------------------------------------------- *)
 
+let real_rat_red_conv_list =
+  [`x <= y`,REAL_RAT_LE_CONV;
+   `x < y`,REAL_RAT_LT_CONV;
+   `x >= y`,REAL_RAT_GE_CONV;
+   `x > y`,REAL_RAT_GT_CONV;
+   `x:real = y`,REAL_RAT_EQ_CONV;
+   `--x`,CHANGED_CONV REAL_RAT_NEG_CONV;
+   `real_sgn(x)`,REAL_RAT_SGN_CONV;
+   `abs(x)`,REAL_RAT_ABS_CONV;
+   `inv(x)`,REAL_RAT_INV_CONV;
+   `x + y`,REAL_RAT_ADD_CONV;
+   `x - y`,REAL_RAT_SUB_CONV;
+   `x * y`,REAL_RAT_MUL_CONV;
+   `x / y`,CHANGED_CONV REAL_RAT_DIV_CONV;
+   `x pow n`,REAL_RAT_POW_CONV;
+   `max x y`,REAL_RAT_MAX_CONV;
+   `min x y`,REAL_RAT_MIN_CONV];;
+
 let REAL_RAT_RED_CONV =
-  let gconv_net = itlist (uncurry net_of_conv)
-    [`x <= y`,REAL_RAT_LE_CONV;
-     `x < y`,REAL_RAT_LT_CONV;
-     `x >= y`,REAL_RAT_GE_CONV;
-     `x > y`,REAL_RAT_GT_CONV;
-     `x:real = y`,REAL_RAT_EQ_CONV;
-     `--x`,CHANGED_CONV REAL_RAT_NEG_CONV;
-     `real_sgn(x)`,REAL_RAT_SGN_CONV;
-     `abs(x)`,REAL_RAT_ABS_CONV;
-     `inv(x)`,REAL_RAT_INV_CONV;
-     `x + y`,REAL_RAT_ADD_CONV;
-     `x - y`,REAL_RAT_SUB_CONV;
-     `x * y`,REAL_RAT_MUL_CONV;
-     `x / y`,CHANGED_CONV REAL_RAT_DIV_CONV;
-     `x pow n`,REAL_RAT_POW_CONV;
-     `max x y`,REAL_RAT_MAX_CONV;
-     `min x y`,REAL_RAT_MIN_CONV]
+  let gconv_net = itlist (uncurry net_of_conv) real_rat_red_conv_list
     (basic_net()) in
   REWRITES_CONV gconv_net;;
 
 let REAL_RAT_REDUCE_CONV = DEPTH_CONV REAL_RAT_RED_CONV;;
 
+let real_rat_compute_add_convs =
+  let convlist = map (fun pat,the_conv ->
+    let c,args = strip_comb pat in (c,length args,the_conv))
+    real_rat_red_conv_list in
+  fun (compset:Compute.compset) ->
+    itlist (fun newc () -> Compute.add_conv newc compset) convlist ();;
+
+let REAL_RAT_COMPUTE_CONV =
+  let cs = Compute.bool_compset () in
+  Compute.set_skip cs `COND: bool -> A -> A -> A` (Some 1);
+  real_rat_compute_add_convs cs;
+  Compute.WEAK_CBV_CONV cs;;
+
 (* ------------------------------------------------------------------------- *)
 (* Real normalizer dealing with rational constants.                          *)
 (* ------------------------------------------------------------------------- *)