drivers/coq-ssreflect.drv

   1
   2 prelude "(* This file is generated by Why3's coq-ssreflect driver *)"
   3 prelude "(* Beware! Only edit allowed sections below    *)"
   4
   5 printer "coq-ssr"
   6 filename "%t.v"
   7
   8 valid 0
   9 unknown "Error: \\(.*\\)$" "\\1"
  10 fail "Syntax error: \\(.*\\)$" "\\1"
  11 time "why3cpulimit time : %s s"
  12
  13 (* Performed introductions depending on whether counterexamples are
  14    requested, as said by the meta "get_counterexmp". When this meta
  15    set, this transformation introduces the model variables that are
  16    still embedded in the goal. When it is not set, it removes all
  17    these unused-ce-related variables, even in the context.  *)
  18 transformation "counterexamples_dependent_intros"
  19
  20 transformation "inline_trivial"
  21 transformation "eliminate_non_struct_recursion"
  22 transformation "eliminate_if"
  23 transformation "eliminate_literal"
  24 transformation "eliminate_non_lambda_set_epsilon"
  25 transformation "eliminate_projections"
  26 transformation "simplify_formula"
  27
  28
  29 theory BuiltIn
  30
  31   prelude "\n\
  32 Require Import ssreflect ssrbool ssrfun ssrnat seq eqtype ssrint.\n\
  33 Require Import ssrint ssrwhy3.\n\
  34 Set Implicit Arguments.\n\
  35 Unset Strict Implicit.\n\
  36 Unset Printing Implicit Defensive.\n\
  37 "
  38
  39   syntax type int "int"
  40   syntax type real "R"
  41   syntax predicate  (=)   "(%1 = %2)"
  42
  43 end
  44
  45 theory Unit
  46   syntax type unit "unit"
  47 end
  48
  49 theory HighOrd
  50   syntax type (->) "(%1 -> %2)"
  51   syntax function (@)  "(%1 %2)"
  52 end
  53
  54 theory Bool
  55   syntax type bool   "bool"
  56
  57   syntax function True  "true"
  58   syntax function False "false"
  59 end
  60
  61 theory bool.Bool
  62   syntax function andb  "(Init.Datatypes.andb %1 %2)"
  63   syntax function orb   "(Init.Datatypes.orb %1 %2)"
  64   syntax function xorb  "(Init.Datatypes.xorb %1 %2)"
  65   syntax function notb  "(Init.Datatypes.negb %1)"
  66   syntax function implb "(Init.Datatypes.implb %1 %2)"
  67 end
  68
  69 theory map.Map
  70   syntax function get "(%1 %2)"
  71 end
  72
  73 theory int.Int
  74
  75   prelude "\n\
  76 Require Import ssralg ssrnum.\n\
  77 Import GRing.Theory Num.Theory.\n\
  78 Local Open Scope ring_scope."
  79
  80   syntax function zero "0%:Z"
  81   syntax function one  "1%:Z"
  82
  83   syntax function (+)  "(%1 + %2)%R"
  84   syntax function (-)  "(%1 - %2)%R"
  85   syntax function ( * )  "(%1 * %2)%R"
  86   syntax function (-_) "(-%1)%R"
  87
  88   syntax predicate (<=) "(%1 <= %2)%R"
  89   syntax predicate (<)  "(%1 < %2)%R"
  90   syntax predicate (>=) "(%1 >= %2)%R"
  91   syntax predicate (>)  "(%1 > %2)%R"
  92
  93   remove prop MulComm.Comm
  94   remove prop MulAssoc.Assoc
  95   remove prop Unit_def_l
  96   remove prop Unit_def_r
  97   remove prop Inv_def_l
  98   remove prop Inv_def_r
  99   remove prop Assoc
 100   remove prop Mul_distr_l
 101   remove prop Mul_distr_r
 102   remove prop Comm
 103   remove prop Unitary
 104   remove prop Refl
 105   remove prop Trans
 106   remove prop Antisymm
 107   remove prop Total
 108   remove prop NonTrivialRing
 109   remove prop CompatOrderAdd
 110   remove prop CompatOrderMult
 111   remove prop ZeroLessOne
 112
 113 end
 114
 115 theory array.Array
 116
 117   syntax type array "(array %1)"
 118
 119   syntax function ([]) "(get %1 %2)"
 120   syntax function length "(size %1 : int)"
 121   syntax function elts "(get %1)"
 122 (* does not exist anymore
 123   syntax function make "(make %1 %2)"
 124 *)
 125
 126 end
 127
 128 theory matrix.Matrix
 129
 130   syntax type matrix "(matrix %1)"
 131
 132   syntax function rows "(nrows %1 : int)"
 133   syntax function columns "(ncols %1 : int)"
 134   syntax function elts "(matrix_get_curry %1)"
 135 (* does not exist anymore
 136   syntax function make "(matrix_make %1 %2)"
 137 *)
 138
 139 end