diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-28 15:08:52 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-28 15:08:52 +0000 |
commit | 2a167c9a7796939982fa79b4f5adfc7842c97d0e (patch) | |
tree | 44f3c18fc9bb10bf8b1b28b8abc455c678926baa /plugins/btauto/refl_btauto.ml | |
parent | 65eea15cc3ec4b8316698db10ed02526a7dae4d0 (diff) |
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
Diffstat (limited to 'plugins/btauto/refl_btauto.ml')
-rw-r--r-- | plugins/btauto/refl_btauto.ml | 22 |
1 files changed, 12 insertions, 10 deletions
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|] |