diff --git a/theories/common.elpi b/theories/common.elpi index 5b4b4d0..970d3b1 100644 --- a/theories/common.elpi +++ b/theories/common.elpi @@ -77,13 +77,13 @@ ground-uint {{ Number.UIntDecimal lp:D }} :- !, ground-decimal D. ground-uint {{ Number.UIntHexadecimal lp:D }} :- !, ground-hexadecimal D. pred reduction-pos i:term, o:term. -reduction-pos I O :- coq.reduction.vm.norm I {{ positive }} O, ground-pos O. +reduction-pos I O :- coq.reduction.cbv.norm I O, ground-pos O. pred reduction-N i:term, o:term. -reduction-N I O :- coq.reduction.vm.norm I {{ N }} O, ground-N O. +reduction-N I O :- coq.reduction.cbv.norm I O, ground-N O. pred reduction-Z i:term, o:term. -reduction-Z I O :- coq.reduction.vm.norm I {{ Z }} O, ground-Z O. +reduction-Z I O :- coq.reduction.cbv.norm I O, ground-Z O. pred negb i:bool, o:bool. negb tt ff :- !. diff --git a/theories/lra.elpi b/theories/lra.elpi index 6879b3b..7af6bef 100644 --- a/theories/lra.elpi +++ b/theories/lra.elpi @@ -141,7 +141,7 @@ coqZ->Q tt (coqZneg P) {{ Qmake (-1) lp:P }} :- !. pred quote.nat i:term, o:term, o:coqZ. quote.nat {{ Nat.of_num_uint lp:X }} {{ large_nat_uint lp:X }} Out :- ground-uint X, !, - coq.reduction.vm.norm {{ N.of_num_uint lp:X }} {{ N }} XN, !, + coq.reduction.cbv.norm {{ N.of_num_uint lp:X }} XN, !, coqZ->N Out XN. quote.nat X {{ large_nat_N lp:XN }} Out :- reduction-N {{ N.of_nat lp:X }} XN, !, coqZ->N Out XN. @@ -151,13 +151,13 @@ quote.nat X {{ large_nat_N lp:XN }} Out :- pred quote.int i:term, o:term, o:coqZ. quote.int {{ Posz (Nat.of_num_uint lp:X) }} {{ large_int_Pos lp:X }} Out :- ground-uint X, !, - coq.reduction.vm.norm {{ N.of_num_uint lp:X }} {{ N }} XN, !, coqZ->N Out XN. + coq.reduction.cbv.norm {{ N.of_num_uint lp:X }} XN, !, coqZ->N Out XN. quote.int {{ Posz lp:N }} {{ large_int_Z lp:NZ }} Out :- reduction-Z {{ Z.of_nat lp:N }} NZ, !, coqZ->Z Out NZ. quote.int {{ Negz (Nat.of_num_uint lp:X) }} {{ large_int_Neg lp:X }} (coqZneg P) :- ground-uint X, !, - coq.reduction.vm.norm {{ N.succ_pos (N.of_num_uint lp:X) }} {{ positive }} P. + coq.reduction.cbv.norm {{ N.succ_pos (N.of_num_uint lp:X) }} P. quote.int {{ Negz lp:N }} {{ large_int_Z (Zneg lp:P) }} (coqZneg P) :- reduction-pos {{ N.succ_pos (N.of_nat lp:N) }} P, !. diff --git a/theories/ring.elpi b/theories/ring.elpi index 831b3e8..90bc939 100644 --- a/theories/ring.elpi +++ b/theories/ring.elpi @@ -51,7 +51,7 @@ quote.expr.exp In1 In2 {{ @PEpow Z lp:In1 lp:In2 }} :- !. pred quote.ncstr i:term, o:term, o:term. quote.ncstr {{ Nat.of_num_uint lp:In }} {{ large_nat_uint lp:In }} Out :- ground-uint In, !, - coq.reduction.vm.norm {{ N.of_num_uint lp:In }} {{ N }} Out. + coq.reduction.cbv.norm {{ N.of_num_uint lp:In }} Out. quote.ncstr In {{ large_nat_N lp:Out }} Out :- reduction-N {{ N.of_nat lp:In }} Out. @@ -60,13 +60,13 @@ pred quote.icstr i:term, o:bool, o:term, o:term. quote.icstr {{ Posz (Nat.of_num_uint lp:In) }} tt {{ large_nat_uint lp:In }} Out :- ground-uint In, !, - coq.reduction.vm.norm {{ N.of_num_uint lp:In }} {{ N }} Out. + coq.reduction.cbv.norm {{ N.of_num_uint lp:In }} Out. quote.icstr {{ Negz (Nat.of_num_uint lp:In) }} ff {{ large_nat_uint lp:In }} Out :- ground-uint In, !, - coq.reduction.vm.norm {{ N.of_num_uint lp:In }} {{ N }} Out. + coq.reduction.cbv.norm {{ N.of_num_uint lp:In }} Out. quote.icstr In Pos {{ large_nat_N lp:Out }} Out :- !, - coq.reduction.vm.norm {{ quote_icstr_helper lp:In }} {{ (bool * N)%type }} + coq.reduction.cbv.norm {{ quote_icstr_helper lp:In }} {{ (lp:Pos', lp:Out) }}, !, ((Pos' = {{ true }}, !, Pos = tt); (Pos' = {{ false }}, !, Pos = ff)), !, ground-N Out. @@ -91,7 +91,7 @@ quote.nat R {{ lib:num.nat.S lp:In }} OutM Out VarMap :- !, {quote.expr.constant {{ lib:num.Z.Zpos lp:Out1 }} } Out2 Out). quote.nat _ {{ Nat.of_num_uint lp:X }} {{ NC (large_nat_uint lp:X) }} Out _ :- ground-uint X, !, - coq.reduction.vm.norm {{ Z.of_num_uint lp:X }} {{ Z }} XZ, !, + coq.reduction.cbv.norm {{ Z.of_num_uint lp:X }} XZ, !, quote.expr.constant XZ Out. quote.nat R {{ addn lp:In1 lp:In2 }} {{ NAdd lp:OutM1 lp:OutM2 }} Out VarMap :- !,