Commit dea385b4 authored by Francois Bobot's avatar Francois Bobot

- why.el : Ajout d'un debut d'indentation automatique pour le mode de why

  (TODO gestion des commentaires, des match, forall, ...)
   - call_provers : Utilisation de Unix.create_process au lieu de Sys.command
parent 9e1f0bda
......@@ -61,21 +61,24 @@ exception NoCommandlineProvided
(* this should be replaced by a proper use of fork/waitpid() *)
let dirname = Filename.dirname Sys.argv.(0)
let cpulimit_local = Filename.concat dirname "why-cpulimit"
let cpulimit_commands = ["why-cpulimit"; cpulimit_local(* ; "timeout"*)]
let cpulimit = ref (
let cpulimit_commands = ["why-cpulimit"; cpulimit_local ; "timeout"]
let cpulimit = (
let tmp = ref "" in
try
List.iter
(fun s ->
let r = Sys.command (s^" 1 echo") in
if r=0 then (tmp:=s; raise Exit))
(*let r = Sys.command (s^" 1 echo") in
if r=0 then (tmp:=s; raise Exit)*)
let pid = Unix.create_process s [|s;"1";"true"|]
Unix.stdin Unix.stdout Unix.stderr in
match Unix.waitpid [] pid with
| _,Unix.WEXITED 0 -> (tmp:=s; raise Exit)
| _ -> ()
)
cpulimit_commands;
failwith
(List.fold_left
(fun acc s -> acc^" "^s^",")
"need shell command among:"
cpulimit_commands)
with Exit -> !tmp)
failwith ("need shell command among: "^
(String.concat " ," cpulimit_commands))
with Exit -> tmp)
......
......@@ -7,31 +7,31 @@ theory Test
logic id2(x: int) : int = id(x)
logic succ(x:int) : int = id(x+1)
goal G : (forall x:int. x=x) or
(forall x:int. x=x+1)
goal G : (forall x:int.x=x) or
(forall x:int. x=x+1)
goal G2 : forall x:int. let x = 0 + 1 in x = 1
end
theory Test_simplify_array
use import array.Array
goal G : forall x,y:int. forall m: (int,int) t.
select(store(m,y,x),y) = x
use import array.Array
goal G : forall x,y:int. forall m: (int,int) t.
select(store(m,y,x),y) = x
end
theory Test_conjunction
use import int.Int
goal G : forall x:int. x*x=4 -> ((x*x*x=8 or x*x*x = -8) and x*x*2 = 8)
goal G2 : forall x:int. (x+x=4 or x*x=4) -> ((x*x*x=8 or x*x*x = -8) and x*x*2 = 8)
use import int.Int
goal G : forall x:int. x*x=4 -> ((x*x*x=8 or x*x*x = -8) and x*x*2 = 8)
goal G2 : forall x:int. (x+x=4 or x*x=4) -> ((x*x*x=8 or x*x*x = -8) and x*x*2 = 8)
end
theory Split_conj
logic p(x:int)
(*goal G : forall x,y,z:int. ((p(x) -> p(y)) and ((not p(x)) -> p(z))) -> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
(*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) <-> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
(*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) -> (if p(x) then p(y) else p(z))*)
goal G : forall x,y,z:int. (p(x) <-> p(z)) -> (p(x) <-> p(z))
(*goal G : forall x,y,z:int. (p(z) <-> p(x)) -> (((not p(z)) and (not p(x)) or ((p(z)) and (p(x))))) *)
(*goal G : forall x,y,z:int. (p(x) or p(y)) -> p(z)*)
logic p(x:int)
(*goal G : forall x,y,z:int. ((p(x) -> p(y)) and ((not p(x)) -> p(z))) -> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
(*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) <-> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
(*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) -> (if p(x) then p(y) else p(z))*)
goal G : forall x,y,z:int. (p(x) <-> p(z)) -> (p(x) <-> p(z))
(*goal G : forall x,y,z:int. (p(z) <-> p(x)) -> (((not p(z)) and (not p(x)) or ((p(z)) and (p(x))))) *)
(*goal G : forall x,y,z:int. (p(x) or p(y)) -> p(z)*)
end
......@@ -44,7 +44,7 @@ theory TestEnco
logic succ(x:int) : int = id(x+1)
goal G : (forall x:int. x=x) or
(forall x:int. x=x+1)
(forall x:int. x=x+1)
logic p('a ) : 'a mytype
logic p2('a mytype) : 'a
axiom A1 : forall x : 'a mytype. p(p2(x)) = x
......
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