From 2a167c9a7796939982fa79b4f5adfc7842c97d0e Mon Sep 17 00:00:00 2001 From: ppedrot Date: Thu, 28 Jun 2012 15:08:52 +0000 Subject: Replace nat indices with positive one in Btauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15499 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/btauto/refl_btauto.ml | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) (limited to 'plugins/btauto/refl_btauto.ml') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 0f89f348e..caa6eac2e 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -34,18 +34,20 @@ module CoqList = struct end -module CoqNat = struct - let path = ["Init"; "Datatypes"] - let typ = get_constant path "nat" - let _S = get_constant path "S" - let _O = get_constant path "O" +module CoqPositive = struct + let path = ["Numbers"; "BinNums"] + let typ = get_constant path "positive" + let _xH = get_constant path "xH" + let _xO = get_constant path "xO" + let _xI = get_constant path "xI" (* A coq nat from an int *) let rec of_int n = - if n <= 0 then Lazy.force _O + if n <= 1 then Lazy.force _xH else - let ans = of_int (pred n) in - lapp _S [|ans|] + let ans = of_int (n / 2) in + if n mod 2 = 0 then lapp _xO [|ans|] + else lapp _xI [|ans|] end @@ -70,7 +72,7 @@ module Env = struct let () = incr off in i - let empty () = (ConstrHashtbl.create 16, ref 0) + let empty () = (ConstrHashtbl.create 16, ref 1) let to_list (env, _) = (* we need to get an ordered list *) @@ -159,7 +161,7 @@ module Btauto = struct let soundness = get_constant ["btauto"; "Reflect"] "reduce_poly_of_formula_sound_alt" let rec convert = function - | Bool.Var n -> lapp f_var [|CoqNat.of_int n|] + | Bool.Var n -> lapp f_var [|CoqPositive.of_int n|] | Bool.Const true -> Lazy.force f_top | Bool.Const false -> Lazy.force f_btm | Bool.Andb (b1, b2) -> lapp f_cnj [|convert b1; convert b2|] -- cgit v1.2.3