Add conversions of num/int/rat/real/word that evaluate expressions us…

…ing Compute

This patch adds conversions of num/int/rat/real/word that use the Compute module to
evaluate expressions.
They are named `*_COMPUTE_CONV` and uses the 'weak' reduction (`Compute.WEAK_CBV_CONV`).
Additionally, an if-then-else expression is configured to be reduced only when the branch is constant.

These new conversions are different from

- `*_RED_CONV` because `*_RED_CONV` cannot
  recursively traverse subexpression (e.g., `NUM_RED_CONV` cannot reduce `` `1 + (2 + 3)` ``)
- Also different from `*_REDUCE_CONV` because `*_REDUCE_CONV` tries to
  recursively reduce every subexpression (e.g.,
  `` `if unknown_cond then 1 + 2 else 3 + 4` ``, `` `\x. x + (1 + 2)` ``).

Library/words.ml

@@ -8171,7 +8171,79 @@ let WORD_RED_CONV =
   (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 = [
+    `word:num->(N)word`,1,CHANGED_CONV WORD_WORD_CONV;
+    `word_saturate:num->(N)word`,1,WORD_SATURATE_CONV;
+    `iword:int->(N)word`,1,WORD_IWORD_CONV;
+    `iword_saturate:int->(N)word`,1,IWORD_SATURATE_CONV;
+    `val:(N)word->num`,1,WORD_VAL_CONV;
+    `ival:(N)word->int`,1,WORD_IVAL_CONV;
+    `bit:num->(N)word->bool`,2,WORD_BIT_CONV;
+    `(=):(N)word->(N)word->bool`,2,WORD_EQ_CONV;
+    `word_ult:(N)word->(N)word->bool`,2,WORD_ULT_CONV;
+    `word_ule:(N)word->(N)word->bool`,2,WORD_ULE_CONV;
+    `word_ugt:(N)word->(N)word->bool`,2,WORD_UGT_CONV;
+    `word_uge:(N)word->(N)word->bool`,2,WORD_UGE_CONV;
+    `word_ilt:(N)word->(N)word->bool`,2,WORD_ILT_CONV;
+    `word_ile:(N)word->(N)word->bool`,2,WORD_ILE_CONV;
+    `word_igt:(N)word->(N)word->bool`,2,WORD_IGT_CONV;
+    `word_ige:(N)word->(N)word->bool`,2,WORD_IGE_CONV;
+    `word_neg:(N)word->(N)word`,1,WORD_NEG_CONV;
+    `word_add:(N)word->(N)word->(N)word`,2,WORD_ADD_CONV;
+    `word_mul:(N)word->(N)word->(N)word`,2,WORD_MUL_CONV;
+    `word_sub:(N)word->(N)word->(N)word`,2,WORD_SUB_CONV;
+    `word_udiv:(N)word->(N)word->(N)word`,2,WORD_UDIV_CONV;
+    `word_umod:(N)word->(N)word->(N)word`,2,WORD_UMOD_CONV;
+    `word_umax:(N)word->(N)word->(N)word`,2,WORD_UMAX_CONV;
+    `word_umin:(N)word->(N)word->(N)word`,2,WORD_UMIN_CONV;
+    `word_imax:(N)word->(N)word->(N)word`,2,WORD_IMAX_CONV;
+    `word_imin:(N)word->(N)word->(N)word`,2,WORD_IMIN_CONV;
+    `word_shl:(N)word->num->(N)word`,2,WORD_SHL_CONV;
+    `word_ushr:(N)word->num->(N)word`,2,WORD_USHR_CONV;
+    `word_ishr:(N)word->num->(N)word`,2,WORD_ISHR_CONV;
+    `word_not:(N)word->(N)word`,1,WORD_NOT_CONV;
+    `word_and:(N)word->(N)word->(N)word`,2,WORD_AND_CONV;
+    `word_or:(N)word->(N)word->(N)word`,2,WORD_OR_CONV;
+    `word_xor:(N)word->(N)word->(N)word`,2,WORD_XOR_CONV;
+    `word_rol:(N)word->num->(N)word`,2,WORD_ROL_CONV;
+    `word_ror:(N)word->num->(N)word`,2,WORD_ROR_CONV;
+    `word_zx:(N)word->(M)word`,1,WORD_ZX_CONV;
+    `word_sx:(N)word->(M)word`,1,WORD_SX_CONV;
+    `word_sxfrom:num->(N)word->(N)word`,2,WORD_SXFROM_CONV;
+    `word_cand:(N)word->(N)word->(N)word`,2,WORD_CAND_CONV;
+    `word_cor:(N)word->(N)word->(N)word`,2,WORD_COR_CONV;
+    `word_join:(N)word->(N)word->(M)word`,2,WORD_JOIN_CONV;
+    `word_subword:(N)word->(num#num)->(M)word`,2,WORD_SUBWORD_CONV;
+    `word_insert:(N)word->(num#num)->(M)word->(K)word`,3,WORD_INSERT_CONV;
+    `word_duplicate:(N)word->(M)word`,1,WORD_DUPLICATE_CONV;
+    `bits_of_word:(N)word->num->bool`,1,WORD_BITS_OF_WORD_CONV;
+    `word_popcount:(N)word->num`,1,WORD_POPCOUNT_CONV;
+    `word_evenparity:(N)word->bool`,1,WORD_EVENPARITY_CONV;
+    `word_oddparity:(N)word->bool`,1,WORD_ODDPARITY_CONV;
+    `word_ctz:(N)word->num`,1,WORD_CTZ_CONV;
+    `word_clz:(N)word->num`,1,WORD_CLZ_CONV;
+    `word_bytereverse:((((N)tybit0)tybit0)tybit0)word->((((N)tybit0)tybit0)tybit0)word`,1,WORD_BYTEREVERSE_CONV;
+    `word_reversefields:num->(N)word->(N)word`,2,WORD_REVERSEFIELDS_CONV;
+    `word_jshl:(N)word->(N)word->(N)word`,2,WORD_JSHL_CONV;
+    `word_jshr:(N)word->(N)word->(N)word`,2,WORD_JSHR_CONV;
+    `word_jushr:(N)word->(N)word->(N)word`,2,WORD_JUSHR_CONV;
+    `word_jrol:(N)word->(N)word->(N)word`,2,WORD_JROL_CONV;
+    `word_jror:(N)word->(N)word->(N)word`,2,WORD_JROR_CONV;
+    `word_jdiv:(N)word->(N)word->(N)word`,2,WORD_JDIV_CONV;
+    `word_jrem:(N)word->(N)word->(N)word`,2,WORD_JREM_CONV
+  ] in
+  fun (compset:Compute.compset):unit ->
+    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.                                       *)

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 ; \

calc_int.ml

@@ -390,3 +390,26 @@ let REAL_INT_RED_CONV =
   REWRITES_CONV gconv_net;;
 
 let REAL_INT_REDUCE_CONV = DEPTH_CONV REAL_INT_RED_CONV;;
+
+let real_int_compute_add_convs =
+  let convlist = [
+    `<=`,2,REAL_INT_LE_CONV;
+    `<`,2,REAL_INT_LT_CONV;
+    `>=`,2,REAL_INT_GE_CONV;
+    `>`,2,REAL_INT_GT_CONV;
+    `(=):real->real->bool`,2,REAL_INT_EQ_CONV;
+    `--`,1,CHANGED_CONV REAL_INT_NEG_CONV;
+    `abs`,1,REAL_INT_ABS_CONV;
+    `+`,2,REAL_INT_ADD_CONV;
+    `-`,2,REAL_INT_SUB_CONV;
+    `*`,2,REAL_INT_MUL_CONV;
+    `pow`,2,REAL_INT_POW_CONV
+  ] in
+  fun (compset:Compute.compset):unit ->
+    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;;

calc_num.ml

@@ -1475,6 +1475,36 @@ let NUM_RED_CONV =
 
 let NUM_REDUCE_CONV = DEPTH_CONV NUM_RED_CONV;;
 
+let num_compute_add_convs =
+  let convlist = [
+    `SUC`,1,NUM_SUC_CONV;
+    `PRE`,1,NUM_PRE_CONV;
+    `FACT`,1,NUM_FACT_CONV;
+    `<`,2,NUM_LT_CONV;
+    `<=`,2,NUM_LE_CONV;
+    `>`,2,NUM_GT_CONV;
+    `>=`,2,NUM_GE_CONV;
+    `(=):num->num->bool`,2,NUM_EQ_CONV;
+    `EVEN`,1,NUM_EVEN_CONV;
+    `ODD`,1,NUM_ODD_CONV;
+    `+`,2,NUM_ADD_CONV;
+    `-`,2,NUM_SUB_CONV;
+    `*`,2,NUM_MULT_CONV;
+    `EXP`,2,NUM_EXP_CONV;
+    `DIV`,2,NUM_DIV_CONV;
+    `MOD`,2,NUM_MOD_CONV;
+    `MAX`,2,NUM_MAX_CONV;
+    `MIN`,2,NUM_MIN_CONV
+  ] in
+  fun (compset:Compute.compset):unit ->
+    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;;
 
 (* ------------------------------------------------------------------------- *)

calc_rat.ml

@@ -409,6 +409,34 @@ let REAL_RAT_RED_CONV =
 
 let REAL_RAT_REDUCE_CONV = DEPTH_CONV REAL_RAT_RED_CONV;;
 
+let real_rat_compute_add_convs =
+  let convlist = [
+    `<=`,2,REAL_RAT_LE_CONV;
+    `<`,2,REAL_RAT_LT_CONV;
+    `>=`,2,REAL_RAT_GE_CONV;
+    `>`,2,REAL_RAT_GT_CONV;
+    `(=):real->real->bool`,2,REAL_RAT_EQ_CONV;
+    `--`,1,CHANGED_CONV REAL_RAT_NEG_CONV;
+    `real_sgn`,1,REAL_RAT_SGN_CONV;
+    `abs`,1,REAL_RAT_ABS_CONV;
+    `inv`,1,REAL_RAT_INV_CONV;
+    `+`,2,REAL_RAT_ADD_CONV;
+    `-`,2,REAL_RAT_SUB_CONV;
+    `*`,2,REAL_RAT_MUL_CONV;
+    `/`,2,CHANGED_CONV REAL_RAT_DIV_CONV;
+    `pow`,2,REAL_RAT_POW_CONV;
+    `max`,2,REAL_RAT_MAX_CONV;
+    `min`,2,REAL_RAT_MIN_CONV
+  ] in
+  fun (compset:Compute.compset):unit ->
+    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.                          *)
 (* ------------------------------------------------------------------------- *)

int.ml

@@ -1823,6 +1823,34 @@ let INT_RED_CONV =
 
 let INT_REDUCE_CONV = DEPTH_CONV INT_RED_CONV;;
 
+let int_compute_add_convs =
+  let convlist = [
+    `<=`,2,INT_LE_CONV;
+    `<`,2,INT_LT_CONV;
+    `>=`,2,INT_GE_CONV;
+    `>`,2,INT_GT_CONV;
+    `(=):int->int->bool`,2,INT_EQ_CONV;
+    `--`,1,CHANGED_CONV INT_NEG_CONV;
+    `int_sgn`,1,INT_SGN_CONV;
+    `abs`,1,INT_ABS_CONV;
+    `+`,2,INT_ADD_CONV;
+    `-`,2,INT_SUB_CONV;
+    `*`,2,INT_MUL_CONV;
+    `div`,2,INT_DIV_CONV;
+    `rem`,2,INT_REM_CONV;
+    `pow`,2,INT_POW_CONV;
+    `max`,2,INT_MAX_CONV;
+    `min`,2,INT_MIN_CONV
+  ] in
+  fun (compset:Compute.compset):unit ->
+    itlist (fun newc () -> Compute.add_conv newc compset) convlist ();;
+
+let INT_COMPUTE_CONV =
+  let cs = Compute.bool_compset () in
+  Compute.set_skip cs `COND: bool -> A -> A -> A` (Some 1);
+  int_compute_add_convs cs;
+  Compute.WEAK_CBV_CONV cs;;
+
 (* ------------------------------------------------------------------------- *)
 (* Integer analogs of the usual even/odd combining theorems EVEN_ADD etc.    *)
 (* ------------------------------------------------------------------------- *)

unit_tests.ml

@@ -11,3 +11,19 @@ assert (`F` = `false`);;
 assert (`!(x:A). P x` = `forall (x:A). P x`);;
 assert (`?(x:A). P x` = `exists (x:A). P x`);;
 assert (`?!(x:A). P x` = `existsunique (x:A). P x`);;
+
+(* ------------------------------------------------------------------------- *)
+(* Test COMPUTE_CONVs.                                                       *)
+(* ------------------------------------------------------------------------- *)
+
+assert (rhs (concl (NUM_COMPUTE_CONV `if x then 1 + 2 else 3 + 4`))
+              = `if x then 1 + 2 else 3 + 4`);;
+assert (rhs (concl (NUM_COMPUTE_CONV `if true then 1 + 2 else 3 + 4`))
+              = `3`);;
+assert (rhs (concl (NUM_COMPUTE_CONV `\x. x + (1 + 2)`))
+        = `\x. x + (1 + 2)`);;
+assert (rhs (concl (NUM_COMPUTE_CONV `(\x. x + (1 + 2)) (3 + 4)`))
+        = `10`);;
+(* Arguments are reduced when the fn is a constant. *)
+assert (rhs (concl (NUM_COMPUTE_CONV `(unknown_fn:num->num) (1+2)`))
+        = `(unknown_fn:num->num) 3`);;