alt-ergo

Makefile.in

@@ -138,7 +138,7 @@ bin/top: $(CMO)
 
 test: bin/why.byte
 	ocamlrun -bt bin/why.byte --print-stdout -I lib/prelude/ src/test.why
-	bin/why.byte --alt-ergo -I lib/prelude/ src/test.why
+#	bin/why.byte --alt-ergo -I lib/prelude/ src/test.why
 
 # graphical interface
 #####################

lib/prelude/math.why

+
+theory RingStructure
+  type t
+  logic zero : t
+  logic (_+_)(t, t) : t
+  logic (-_)(t) : t
+  logic (_*_)(t, t) : t
+
+  axiom Add_assoc:    forall x,y,z:t. x + (y + z) = (x + y) + z
+  axiom Add_comm:     forall x,y:t. x + y = y + x
+  axiom Zero_neutral: forall x:t. x + zero = x
+  axiom Neg:          forall x:t. x + -x = zero
+  axiom Mul_assoc:    forall x,y,z:t. x * (y * z) = (x * y) * z
+  axiom Mul_distr:    forall x,y,z:t. x * (y + z) = x * y + x * z
+end
+

lib/prelude/prelude.why

@@ -14,15 +14,13 @@ theory Int
   logic (_/_) (int, int) : int
   logic (_%_) (int, int) : int
 
+  logic zero : int = 0
   logic (-_)(int) : int
   
   (* ring structure *)
-  axiom Add_assoc:    forall x,y,z:int. x + (y + z) = (x + y) + z
-  axiom Add_comm:     forall x,y:int. x + y = y + x
-  axiom Zero_neutral: forall x:int. x + 0 = x
-  axiom Neg:          forall x:int. x + -x = 0
-  axiom Mul_assoc:    forall x,y,z:int. x * (y * z) = (x * y) * z
-  axiom Mul_distr:    forall x,y,z:int. x * (y + z) = x * y + x * z
+  clone export math.RingStructure with 
+     type t = int, logic zero = zero, 
+     logic (_+_) = (_+_), logic (_*_) = (_*_), logic (-_) = (-_)
 
   (* int is a unitary, communtative ring *)
   axiom Mul_comm:     forall x,y:int. x * y = y * x

src/main.ml

@@ -76,19 +76,27 @@ let type_file env file =
   close_in c;
   if !parse_only then env else Typing.add_theories env f
 
+let extract_goals th =
+  let ctx = Context.use_export Context.empty_context th in
+  assert false
+
 let transform l =
   let l = Typing.list_theory l in
   if !print_stdout && not transform then 
     List.iter (Pretty.print_theory Format.std_formatter) l
-  else if !alt_ergo then
-    List.iter (fun th -> Alt_ergo.print_context std_formatter th.th_ctxt) l
-   else 
+  else if !alt_ergo then match l with
+    | th :: _ -> begin match extract_goals th with
+	| g :: _ -> Alt_ergo.print_goal std_formatter g
+	| [] -> ()
+      end	
+    | [] -> ()
+  else 
     let l = List.map (fun t -> t,Transform.apply Flatten.t t.th_ctxt)
       l in
     let l = if !simplify_recursive 
     then 
       List.map (fun (t,dl) -> t,Transform.apply 
-                     Simplify_recursive_definition.t dl) l
+                  Simplify_recursive_definition.t dl) l
     else l in
     let l = if !inlining
     then

src/output/alt_ergo.ml

@@ -6,20 +6,10 @@ open Ty
 open Term
 open Theory
 
-let ident_table = Hid.create 5003
-
-let fresh_ident =
-  let ident_count = ref 0 in
-  fun () -> incr ident_count; "x" ^ string_of_int !ident_count
+let ident_printer = create_printer ()
 
 let print_ident fmt id =
-  let s = 
-    try 
-      Hid.find ident_table id
-    with Not_found -> 
-      let s = fresh_ident () in Hid.add ident_table id s; s
-  in
-  pp_print_string fmt s
+  fprintf fmt "%s" (id_unique ident_printer id)
 
 let rec print_type fmt ty = match ty.ty_node with
   | Tyvar id -> 
@@ -143,3 +133,7 @@ let print_context fmt ctxt =
   let decls = Context.get_decls ctxt in
   print_list newline2 print_decl fmt decls
 
+
+let print_goal fmt (id, f, ctxt) =
+  print_context fmt ctxt;
+  fprintf fmt "@[<hov 2>goal %a : %a@]" print_ident id print_fmla f

src/output/alt_ergo.mli

 
 open Format
+open Ident
 open Term
 open Theory
 
@@ -8,3 +9,5 @@ val print_term : formatter -> term -> unit
 val print_fmla : formatter -> fmla -> unit
 
 val print_context : formatter -> context -> unit
+
+val print_goal : formatter -> ident * fmla * context -> unit

src/test.why

@@ -2,52 +2,9 @@
 (* test file *)
 
 theory Test1
-  type t
-  logic (_+_)(t,t) : t
-end
-
-theory Test2
-  logic f(int, int) : int
-  clone export Test1 with type t = int, logic (_+_) = f
-  axiom Ax : 1+1 = f(1,1)
-end
-
-theory ThA
-    type 'a t = None | Some ('a)
-    type s
-    logic c : s
-end
-
-theory ThB
-    use export prelude.List
-    clone ThA with type s = int
-end
-
-theory ThC
-end
-
-theory RingStructure
-  type t
-  logic zero : t
-  logic (_+_)(t, t) : t
-  logic (-_)(t) : t
-  logic (_*_)(t, t) : t
-
-  axiom Add_assoc:    forall x,y,z:t. x + (y + z) = (x + y) + z
-  axiom Add_comm:     forall x,y:t. x + y = y + x
-  axiom Zero_neutral: forall x:t. x + zero = x
-  axiom Neg:          forall x:t. x + -x = zero
-  axiom Mul_assoc:    forall x,y,z:t. x * (y * z) = (x * y) * z
-  axiom Mul_distr:    forall x,y,z:t. x * (y + z) = x * y + x * z
-end
-
-theory IntRing
-  type t
-  logic c0 : t
-  logic add(t, t) : t
-  logic neg(t) : t
-  logic mul(t, t) : t
-  (*clone export RingStructure with type t = t*)
+  use import prelude.Int
+  axiom Ax : forall x :int. x=1 and forall x:int. x=2
+  logic g(x: int) : int = x+2
 end
 
 theory Test