coq-ssreflect.drv 2.82 KB
Newer Older
1 2 3 4

prelude "(* This file is generated by Why3's coq-ssreflect driver *)"
prelude "(* Beware! Only edit allowed sections below    *)"

5
printer "coq-ssr"
6 7 8 9 10 11 12 13 14 15
filename "%t.v"

valid 0
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"

transformation "inline_trivial"
transformation "eliminate_non_struct_recursion"
transformation "eliminate_if"
Quentin Garchery's avatar
Quentin Garchery committed
16
transformation "eliminate_literal"
17 18 19 20 21 22 23
transformation "eliminate_non_lambda_set_epsilon"
transformation "eliminate_projections"
transformation "simplify_formula"


theory BuiltIn

24 25 26 27 28 29 30
  prelude "
Require Import ssreflect ssrbool ssrfun ssrnat seq eqtype ssrint.
Require Import ssrint ssrwhy3.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
"
31 32 33 34

  syntax type int "int"
  syntax type real "R"
  syntax predicate  (=)   "(%1 = %2)"
35 36 37

end

38 39 40 41
theory Unit
  syntax type unit "unit"
end

42
theory HighOrd
43
  syntax type (->) "(%1 -> %2)"
44
  syntax function (@)  "(%1 %2)"
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
end

theory Bool
  syntax type bool   "bool"

  syntax function True  "true"
  syntax function False "false"
end

theory bool.Bool
  syntax function andb  "(Init.Datatypes.andb %1 %2)"
  syntax function orb   "(Init.Datatypes.orb %1 %2)"
  syntax function xorb  "(Init.Datatypes.xorb %1 %2)"
  syntax function notb  "(Init.Datatypes.negb %1)"
  syntax function implb "(Init.Datatypes.implb %1 %2)"
end

theory map.Map
  syntax function get "(%1 %2)"
MARCHE Claude's avatar
MARCHE Claude committed
64
end
65 66 67

theory int.Int

68 69
  prelude "
Require Import ssralg ssrnum.
70
Import GRing.Theory Num.Theory.
71 72
Local Open Scope ring_scope."

73 74
  syntax function zero "0%:Z"
  syntax function one  "1%:Z"
75

76 77 78 79
  syntax function (+)  "(%1 + %2)%R"
  syntax function (-)  "(%1 - %2)%R"
  syntax function ( * )  "(%1 * %2)%R"
  syntax function (-_) "(-%1)%R"
80

81 82 83 84
  syntax predicate (<=) "(%1 <= %2)%R"
  syntax predicate (<)  "(%1 < %2)%R"
  syntax predicate (>=) "(%1 >= %2)%R"
  syntax predicate (>)  "(%1 > %2)%R"
85

86 87 88 89 90 91 92
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
93 94
  remove prop Mul_distr_l
  remove prop Mul_distr_r
95
  remove prop Comm
96 97 98 99 100 101 102 103 104 105 106
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
  remove prop ZeroLessOne

end
107 108 109 110 111

theory array.Array

  syntax type array "(array %1)"

112
  syntax function ([]) "(get %1 %2)"
113 114
  syntax function length "(size %1 : int)"
  syntax function elts "(get %1)"
115
(* does not exist anymore
116
  syntax function make "(make %1 %2)"
117
*)
118 119

end
120 121 122 123 124 125 126

theory matrix.Matrix

  syntax type matrix "(matrix %1)"

  syntax function rows "(nrows %1 : int)"
  syntax function columns "(ncols %1 : int)"
127
  syntax function elts "(matrix_get_curry %1)"
128
(* does not exist anymore
129
  syntax function make "(matrix_make %1 %2)"
130
*)
131 132

end