Commit 1586788e authored by MARCHE Claude's avatar MARCHE Claude

Reorganized driver files for Alt-Ergo

parent 53768698
(* Driver for the most recent version of Alt-Ergo *) (* Driver for Alt-Ergo version >= 0.95 *)
import "alt_ergo_bare.drv" import "alt_ergo_common.drv"
theory BuiltIn theory BuiltIn
meta "eliminate_algebraic" "keep_enums" meta "eliminate_algebraic" "keep_enums"
......
(* Driver for Alt-Ergo version <= 0.92 *) (* Driver for Alt-Ergo version <= 0.92 *)
import "alt_ergo_bare.drv" import "alt_ergo_common.drv"
theory BuiltIn theory BuiltIn
meta "printer_option" "no_type_cast" meta "printer_option" "no_type_cast"
......
...@@ -4,7 +4,7 @@ ...@@ -4,7 +4,7 @@
- maps - maps
*) *)
import "alt_ergo_bare.drv" import "alt_ergo_common.drv"
theory BuiltIn theory BuiltIn
meta "eliminate_algebraic" "keep_enums" meta "eliminate_algebraic" "keep_enums"
......
...@@ -4,10 +4,22 @@ ...@@ -4,10 +4,22 @@
- Euclidean division - Euclidean division
*) *)
import "alt_ergo_0.93.drv" import "alt_ergo_common.drv"
theory BuiltIn theory BuiltIn
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs" meta "eliminate_algebraic" "keep_recs"
meta "printer_option" "no_type_cast"
end
theory map.Map
syntax type map "(%1,%2) farray"
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
remove prop Select_eq
remove prop Select_neq
end end
theory int.EuclideanDivision theory int.EuclideanDivision
......
(* Why driver for Alt-Ergo *) (* Why drivers for Alt-Ergo: common part *)
prelude "(* this is a prelude for Alt-Ergo*)" prelude "(* this is the prelude for Alt-Ergo, any versions *)"
printer "alt-ergo" printer "alt-ergo"
filename "%f-%t-%g.why" filename "%f-%t-%g.why"
......
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