Commit 9f4bb7d3 authored by Andrei Paskevich's avatar Andrei Paskevich

fix the newly added theories and drivers

parent 0ee8c94c
......@@ -35,13 +35,11 @@ Unset Printing Implicit Defensive.
end
theory HighOrd
syntax type func "(%1 -> %2)"
syntax type pred "(%1 -> bool)"
syntax type (->) "(%1 -> %2)"
syntax function (@) "(%1 %2)"
end
theory Bool
syntax type bool "bool"
syntax function True "true"
......@@ -49,24 +47,17 @@ theory Bool
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 type map "(%1 -> %2)%type"
syntax function get "(%1 %2)"
end
theory map.Const
remove prop Const
end
theory int.Int
prelude "
......@@ -87,16 +78,16 @@ Local Open Scope ring_scope."
syntax predicate (>=) "(%1 >= %2)%R"
syntax predicate (>) "(%1 > %2)%R"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
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
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Comm
remove prop Unitary
remove prop Refl
remove prop Trans
......@@ -113,10 +104,10 @@ theory array.Array
syntax type array "(array %1)"
syntax function get "(get %1 %2)"
syntax function get_unsafe "(get %1 %2)"
syntax function length "(size %1 : int)"
syntax function elts "(get %1)"
syntax function set "(set %1 %2 %3)"
syntax function set_unsafe "(set %1 %2 %3)"
(* does not exist anymore
syntax function make "(make %1 %2)"
*)
......@@ -127,11 +118,11 @@ theory matrix.Matrix
syntax type matrix "(matrix %1)"
syntax function get "(matrix_get %1 %2 %3)"
syntax function get_unsafe "(matrix_get %1 %2 %3)"
syntax function rows "(nrows %1 : int)"
syntax function columns "(ncols %1 : int)"
syntax function elts "(matrix_get_curry %1)"
syntax function set "(matrix_set %1 %2 %3)"
syntax function set_unsafe "(matrix_set %1 %2 %3)"
(* does not exist anymore
syntax function make "(matrix_make %1 %2)"
*)
......
......@@ -54,16 +54,16 @@ theory int.Int
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
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
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Comm
remove prop Unitary
remove prop Refl
remove prop Trans
......@@ -97,16 +97,16 @@ theory real.Real
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
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
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Comm
remove prop Unitary
remove prop Inverse
remove prop Refl
......@@ -148,9 +148,15 @@ theory bool.Bool
syntax function notb "(~ %1)"
end
theory HighOrd
syntax type (->) "(ARRAY %1 OF %2)"
meta "material_type_arg" type (->), 1
syntax function (@) "(%1[%2])"
meta "encoding : lskept" function (@)
end
theory map.Map
syntax type map "(ARRAY %1 OF %2)"
meta "encoding : lskept" function get
meta "encoding : lskept" function set
......
......@@ -19,6 +19,11 @@ theory BuiltIn
syntax predicate (=) "<app><const name=\"HOL.eq\"/>%1%2</app>"
end
theory HighOrd
syntax type (->) "<fun>%1%2</fun>"
syntax function (@) "<app>%1%2</app>"
end
theory Bool
syntax type bool "<type name=\"HOL.bool\"/>"
......@@ -128,19 +133,12 @@ theory option.Option
end
theory map.Map
syntax type map "<fun>%1%2</fun>"
syntax function get "<app>%1%2</app>"
syntax function ([]) "<app>%1%2</app>"
syntax function set "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
syntax function ([<-]) "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
end
theory map.Const
syntax function const "<app><const name=\"_type_constraint_\"><fun>%t0%t0</fun></const><abs name=\"\"><type name=\"dummy\"/>%1</abs></app>"
end
theory set.SetGen
syntax predicate (==) "<app><const name=\"HOL.eq\"/>%1%2</app>"
syntax predicate subset "<app><const name=\"Orderings.ord_class.less_eq\"/>%1%2</app>"
......@@ -185,16 +183,16 @@ theory real.Real
syntax predicate (>=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%2%1</app>"
syntax predicate (>) "<app><const name=\"Orderings.ord_class.less\"/>%2%1</app>"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
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
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Comm
remove prop Unitary
remove prop Refl
remove prop Trans
......
......@@ -26,8 +26,12 @@ theory BuiltIn
syntax predicate (=) "(%1 = %2)"
end
theory HighOrd
syntax type (->) "[%1 -> %2]"
syntax function (@) "%1(%2)"
end
theory map.Map
syntax type map "[%1 -> %2]"
syntax function get "%1(%2)"
syntax function ([]) "%1(%2)"
......@@ -40,11 +44,6 @@ theory map.Map
end
theory map.Const
syntax function const "(LAMBDA (x:%v0): %1)"
remove prop Const
end
theory Bool
syntax type bool "bool"
......
(* Why3 driver for safe prover *)
printer "tptp-fof"
filename "%f-%t-%g.p"
valid "Unsat"
(*
invalid "Completion found"
......@@ -13,3 +10,6 @@ unknown "No Proof Found" ""
fail "Failure.*" "\"\\0\""
*)
time "why3cpulimit time : %s s"
import "tptp.gen"
import "discrimination.gen"
......@@ -43,16 +43,16 @@ theory int.Int
syntax predicate (>=) "$greatereq(%1,%2)"
syntax predicate (>) "$greater(%1,%2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
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
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Comm
remove prop Unitary
remove prop Refl
remove prop Trans
......@@ -80,16 +80,16 @@ theory real.Real
syntax predicate (>=) "$greatereq(%1,%2)"
syntax predicate (>) "$greater(%1,%2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
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
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Comm
remove prop Unitary
remove prop Inverse
remove prop Refl
......@@ -169,16 +169,16 @@ theory tptp.Rat
syntax predicate is_int "$is_int(%1)"
syntax predicate is_rat "$is_rat(%1)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
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
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Comm
remove prop Unitary
remove prop Refl
remove prop Trans
......
......@@ -5,6 +5,7 @@ module Impmap
use import option.Option
use import map.Map
use import map.Const
use import map.MapExt
use export exn.Exn
......
......@@ -227,6 +227,7 @@ end
module Refint63
use import int.Int
use import Int63
use export ref.Ref
......@@ -258,6 +259,7 @@ end
module MinMax63
use import int.Int
use import Int63
let min (x y: int63) : int63
......
......@@ -2,41 +2,43 @@
module Matrix63
use import int.Int
use import mach.int.Int63
use import map.Map as M
type matrix 'a
model { rows: int63; columns: int63; mutable elts: map int (map int 'a) }
invariant { 0 <= to_int self.rows /\ 0 <= to_int self.columns }
type matrix 'a = private {
ghost mutable elts: map int (map int 'a);
rows: int63;
columns: int63
} invariant { 0 <= to_int rows /\ 0 <= to_int columns }
function get (a: matrix 'a) (r c: int) : 'a =
M.get (M.get a.elts r) c
val ghost function get_unsafe (a: matrix 'a) (r c: int) : 'a
ensures { result = M.get (M.get a.elts r) c }
function set (a: matrix 'a) (r c: int) (v: 'a) : matrix 'a =
{ a with elts = M.set a.elts r (M.set (M.get a.elts r) c v) }
val ghost function set_unsafe (a: matrix 'a) (r c: int) (v: 'a) : matrix 'a
ensures {
result.rows = a.rows /\ result.columns = a.columns /\
result.elts = M.set a.elts r (M.set (M.get a.elts r) c v) }
predicate valid_index (a: matrix 'a) (r c: int63) =
0 <= to_int r < to_int a.rows /\ 0 <= to_int c < to_int a.columns
val get (a: matrix 'a) (r c: int63) : 'a
requires { "expl:index in array bounds" valid_index a r c }
ensures { result = get a (to_int r) (to_int c) }
ensures { result = get_unsafe a (to_int r) (to_int c) }
val set (a: matrix 'a) (r c: int63) (v: 'a) : unit
requires { "expl:index in array bounds" valid_index a r c }
writes { a }
ensures { a.elts = M.set (old a.elts) (to_int r)
(M.set (M.get (old a.elts) (to_int r)) (to_int c) v) }
val rows (a: matrix 'a) : int63 ensures { result = a.rows }
val columns (a: matrix 'a) : int63 ensures { result = a.columns }
(M.set (M.get (old a.elts) (to_int r)) (to_int c) v)}
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: matrix 'a) (r c: int63) : 'a
ensures { "expl:index in array bounds" valid_index a r c }
ensures { result = get a (to_int r) (to_int c) }
ensures { result = get_unsafe a (to_int r) (to_int c) }
raises { OutOfBounds -> not (valid_index a r c) }
= if r < of_int 0 || r >= a.rows || c < of_int 0 || c >= a.columns then
raise OutOfBounds;
......@@ -44,8 +46,8 @@ module Matrix63
let defensive_set (a: matrix 'a) (r c: int63) (v: 'a) : unit
ensures { "expl:index in array bounds" valid_index a r c }
ensures { a.elts = M.set (old a.elts)
(to_int r) (M.set (M.get (old a.elts) (to_int r)) (to_int c) v) }
ensures { a.elts = M.set (old a.elts) (to_int r)
(M.set (M.get (old a.elts) (to_int r)) (to_int c) v)}
raises { OutOfBounds -> not (valid_index a r c) /\ a = old a }
= if r < of_int 0 || r >= a.rows || c < of_int 0 || c >= a.columns then
raise OutOfBounds;
......@@ -56,12 +58,12 @@ module Matrix63
ensures { result.rows = r }
ensures { result.columns = c }
ensures { forall i j. 0 <= i < to_int r /\ 0 <= j < to_int c ->
get result i j = v }
get_unsafe result i j = v }
val copy (a: matrix 'a) : matrix 'a
ensures { result.rows = a.rows /\ result.columns = a.columns }
ensures { forall r:int. 0 <= r < to_int result.rows ->
forall c:int. 0 <= c < to_int result.columns ->
get result r c = get a r c }
get_unsafe result r c = get_unsafe a r c }
end
......@@ -196,7 +196,7 @@ theory Reverse
use import Seq
function reverse (s: seq 'a) : seq 'a =
create (length s) (\ i. s[length s - 1 - i])
create (length s) (fun i -> s[length s - 1 - i])
end
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment