diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/ExtrOcamlZBigInt.v | 18 | ||||
| -rw-r--r-- | plugins/extraction/ExtrOcamlZInt.v | 18 |
2 files changed, 20 insertions, 16 deletions
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v index 322f43850c..fd8ad6d771 100644 --- a/plugins/extraction/ExtrOcamlZBigInt.v +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -36,14 +36,16 @@ Extract Inductive N => "Big.big_int" (** Efficient (but uncertified) versions for usual functions *) -Extract Constant Pplus => "Big.add". -Extract Constant Psucc => "Big.succ". -Extract Constant Ppred => "fun n -> Big.max Big.one (Big.pred n)". -Extract Constant Pminus => "fun n m -> Big.max Big.one (Big.sub n m)". -Extract Constant Pmult => "Big.mult". -Extract Constant Pmin => "Big.min". -Extract Constant Pmax => "Big.max". -Extract Constant Pcompare => +Extract Constant Pos.add => "Big.add". +Extract Constant Pos.succ => "Big.succ". +Extract Constant Pos.pred => "fun n -> Big.max Big.one (Big.pred n)". +Extract Constant Pos.sub => "fun n m -> Big.max Big.one (Big.sub n m)". +Extract Constant Pos.mul => "Big.mult". +Extract Constant Pos.min => "Big.min". +Extract Constant Pos.max => "Big.max". +Extract Constant Pos.compare => + "fun x y -> Big.compare_case Eq Lt Gt x y". +Extract Constant Pos.compare_cont => "fun x y c -> Big.compare_case c Lt Gt x y". Extract Constant Nplus => "Big.add". diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v index 9044b93843..0136957724 100644 --- a/plugins/extraction/ExtrOcamlZInt.v +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -33,14 +33,16 @@ Extract Inductive N => int [ "0" "" ] (** Efficient (but uncertified) versions for usual functions *) -Extract Constant Pplus => "(+)". -Extract Constant Psucc => "succ". -Extract Constant Ppred => "fun n -> max 1 (n-1)". -Extract Constant Pminus => "fun n m -> max 1 (n-m)". -Extract Constant Pmult => "( * )". -Extract Constant Pmin => "min". -Extract Constant Pmax => "max". -Extract Constant Pcompare => +Extract Constant Pos.add => "(+)". +Extract Constant Pos.succ => "succ". +Extract Constant Pos.pred => "fun n -> max 1 (n-1)". +Extract Constant Pos.sub => "fun n m -> max 1 (n-m)". +Extract Constant Pos.mul => "( * )". +Extract Constant Pos.min => "min". +Extract Constant Pos.max => "max". +Extract Constant Pos.compare => + "fun x y -> if x=y then Eq else if x<y then Lt else Gt". +Extract Constant Pos.compare_cont => "fun x y c -> if x=y then c else if x<y then Lt else Gt". |