mise a jour des drivers pour theories/

parent 57068256
......@@ -161,11 +161,11 @@ bin/top: $(CMO)
test: bin/why.byte
mkdir -p output_why3
ocamlrun -bt bin/why.byte -I theories/ --driver lib/drivers/why3.drv \
ocamlrun -bt bin/why.byte -I theories/ --driver drivers/why3.drv \
--output-dir output_why3 src/test.why
bin/why.byte --driver lib/drivers/alt_ergo.drv -I theories/ \
bin/why.byte --driver drivers/alt_ergo.drv -I theories/ \
--output-file - --goal Test.G src/test.why --timeout 3
bin/why.byte --driver lib/drivers/alt_ergo.drv -I theories/ \
bin/why.byte --driver drivers/alt_ergo.drv -I theories/ \
--call --goal Test.G src/test.why --timeout 3
testl: bin/whyl.byte
......
......@@ -66,7 +66,7 @@ echo "=== Type-checking theories ==="
goods theories --type-only
echo ""
echo "=== Checking lib/drivers ==="
drivers lib/drivers --driver
echo "=== Checking drivers ==="
drivers drivers --driver
echo ""
......@@ -31,7 +31,7 @@ theory BuiltIn
end
theory prelude.Int
theory int.Int
prelude "(* this is a prelude for Alt-Ergo arithmetic *)"
......@@ -40,7 +40,6 @@ theory prelude.Int
syntax logic (_+_) "(%1 + %2)"
syntax logic (_-_) "(%1 - %2)"
syntax logic (_*_) "(%1 * %2)"
syntax logic (_/_) "(%1 / %2)"
syntax logic (-_) "(-%1)"
syntax logic (_<=_) "(%1 <= %2)"
......@@ -48,21 +47,21 @@ theory prelude.Int
syntax logic (_>=_) "(%1 >= %2)"
syntax logic (_> _) "(%1 > %2)"
remove prop One_neutral
remove prop Add_assoc
remove prop Add_comm
remove prop Zero_neutral
remove prop Neg
remove prop Mul_comm
remove prop Mul_assoc
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
remove prop CommutativeGroup.Unit_def
remove prop CommutativeGroup.Inv_def
remove prop Assoc.Assoc
remove prop Mul_distr
remove prop Comm.Comm
remove prop Unitary
end
theory algebra.AC
tag cloned logic op "AC"
remove cloned prop Comm
remove cloned prop Assoc
remove cloned prop Comm.Comm
remove cloned prop Assoc.Assoc
end
(*
......
......@@ -48,21 +48,21 @@ theory prelude.Int
syntax logic (_>=_) "(>= %1 %2)"
syntax logic (_> _) "(> %1 %2)"
remove prop One_neutral
remove prop Add_assoc
remove prop Add_comm
remove prop Zero_neutral
remove prop Neg
remove prop Mul_comm
remove prop Mul_assoc
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
remove prop CommutativeGroup.Unit_def
remove prop CommutativeGroup.Inv_def
remove prop Assoc.Assoc
remove prop Mul_distr
remove prop Comm.Comm
remove prop Unitary
end
theory algebra.AC
tag cloned logic op "AC"
remove cloned prop Comm
remove cloned prop Assoc
remove cloned prop Comm.Comm
remove cloned prop Assoc.Assoc
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