Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

alt_ergo.drv 1.07 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 7 8
prelude "(* this is a prelude for Alt-Ergo*)"

printer "alt-ergo"

call_on_file  "alt-ergo %s"
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
9

10 11

theory BuiltIn
12 13
  syntax type int "int"
  syntax type real "real"
14 15 16 17 18 19 20 21 22

  syntax logic (_=_) "(%1 = %1)"

 (* inutile car  "<>" devient "not =" *)
  syntax logic (_<>_) "(%1 = %1)"

end


Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
23 24
theory prelude.Int

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

27
  syntax logic zero "0"
28

29 30 31 32 33
  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
34

35 36 37 38
  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
39

40
  remove prop One_neutral
41 42 43 44 45 46 47 48
  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
49 50
end

51
theory algebra.AC
52 53 54
  tag logic cloned op "AC"
  remove prop cloned Comm
  remove prop cloned Assoc
55 56
end

Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
57 58 59 60 61 62
(*
Local Variables: 
mode: why
compile-command: "make -C ../.. bench"
End: 
*)