alt_ergo.drv 1.28 KB
Newer Older
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
1 2 3

(* Why driver for Alt-Ergo *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4 5 6
prelude "(* this is a prelude for Alt-Ergo*)"

printer "alt-ergo"
Francois Bobot's avatar
Francois Bobot committed
7
filename "%f-%t-%s.mlw"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8
call_on_file  "alt-ergo %s"
9

Francois Bobot's avatar
Francois Bobot committed
10 11 12
valid "Valid"
invalid "Invalid"
unknown "I don't know" "Unknown"
13
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
Francois Bobot's avatar
Francois Bobot committed
14

15 16
(* À discuter *)
transformations
Francois Bobot's avatar
Francois Bobot committed
17
  "simplify_recursive_definition"      
18
  "inline_trivial"
Francois Bobot's avatar
Francois Bobot committed
19
end
20

21 22

theory BuiltIn
23 24
  syntax type int "int"
  syntax type real "real"
25

Francois Bobot's avatar
Francois Bobot committed
26
  syntax logic (_=_) "(%1 = %2)"
27

Francois Bobot's avatar
Francois Bobot committed
28
  syntax logic (_<>_) "(%1 = %2)"
29 30 31 32

end


Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
33 34
theory prelude.Int

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
35
  prelude "(* this is a prelude for Alt-Ergo arithmetic *)"
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
36

37
  syntax logic zero "0"
38

39 40 41 42 43
  syntax logic (_+_) "(%1 + %2)"
  syntax logic (_-_) "(%1 - %2)"
  syntax logic (_*_) "(%1 * %2)"
  syntax logic (_/_) "(%1 / %2)"
  syntax logic (-_)  "(-%1)"
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
44

45 46 47 48
  syntax logic (_<=_) "(%1 <= %2)"
  syntax logic (_< _) "(%1 <  %2)"
  syntax logic (_>=_) "(%1 >= %2)"
  syntax logic (_> _) "(%1 >  %2)"
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
49

50
  remove prop One_neutral
51 52 53 54 55 56 57 58
  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 Mul_distr

Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
59 60
end

61
theory algebra.AC
62 63 64
  tag cloned logic op "AC"
  remove cloned prop Comm
  remove cloned prop Assoc
65 66
end

Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
67 68 69 70 71 72
(*
Local Variables: 
mode: why
compile-command: "make -C ../.. bench"
End: 
*)