sortie alt-ergo

Makefile.in

@@ -117,7 +117,7 @@ TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
 	flatten.cmo
 TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
 
-OUTPUT_CMO := alt_ergo.cmo why3.cmo
+OUTPUT_CMO := print_real.cmo alt_ergo.cmo why3.cmo
 OUTPUT_CMO := $(addprefix src/output/,$(OUTPUT_CMO))
 
 CMO = $(UTIL_CMO) $(CORE_CMO) src/pretty.cmo $(PARSER_CMO)	\
@@ -126,22 +126,23 @@ CMX = $(CMO:.cmo=.cmx)
 
 bin/why.opt: $(CMX) 
 	echo $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(TRANSFORM_CMO)
-	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ $^
+	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ nums.cmxa $^
 	$(STRIP) $@
 
 bin/why.byte: $(CMO) 
-	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -o $@ $^
+	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -o $@ nums.cma $^
 
 bin/why.static: $(CMX) src/why.cmx 
-	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) -cclib -static $(OFLAGS) -o $@ $^ 
+	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) -cclib -static $(OFLAGS) -o $@ nums.cmxa $^ 
 	$(STRIP) $@
 
 bin/top: $(CMO)
-	ocamlmktop $(BFLAGS) -o $@ $^
+	ocamlmktop $(BFLAGS) -o $@ nums.cma $^
 
 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 > ergo.why
+	timeout 3 alt-ergo ergo.why
 
 # graphical interface
 #####################

src/main.ml

@@ -46,6 +46,7 @@ let () =
     "usage: why [options] files..."
 
 let in_emacs = Sys.getenv "TERM" = "dumb"
+
 let transformation = 
   Transform.conv_map
     (Transform.compose
@@ -74,6 +75,7 @@ let rec report fmt = function
         fprintf fmt "anomaly:@\n%s" (Printexc.to_string e)
       else 
         fprintf fmt "anomaly: %s" (Printexc.to_string e)
+
 let type_file env file =
   let c = open_in file in
   let lb = Lexing.from_channel c in
@@ -91,16 +93,15 @@ let transform env l =
       (Typing.list_theory l) in
   let l = Transform.apply transformation l in
   if !print_stdout then 
-    List.iter (fun (t,ctxt) -> Why3.print_context_th std_formatter t.th_name ctxt) l
+    List.iter 
+      (fun (t,ctxt) -> Why3.print_context_th std_formatter t.th_name ctxt) l
   else if !alt_ergo then match l with
     | (_,ctxt) :: _ -> begin match extract_goals ctxt with
 	| g :: _ -> Alt_ergo.print_goal env std_formatter g
-	| [] -> ()
+	| [] -> eprintf "no goal@."
       end	
     | [] -> ()
 
-	
-
 let () =
   try
     let env = Typing.create !loadpath in

src/output/alt_ergo.ml

@@ -57,16 +57,15 @@ let rec print_fmla fmt f = match f.f_node with
   | Fapp (ls, tl) ->
       fprintf fmt "%a(%a)" 
 	print_ident ls.ls_name (print_list comma print_term) tl
-  | Fquant (Fforall, fq) ->
+  | Fquant (q, fq) ->
+      let q = match q with Fforall -> "forall" | Fexists -> "exists" in
       let vl, tl, f = f_open_quant fq in
       let forall fmt v = 
-	fprintf fmt "forall %a:%a" print_ident v.vs_name print_type v.vs_ty
+	fprintf fmt "%s %a:%a" q print_ident v.vs_name print_type v.vs_ty
       in
       fprintf fmt "@[<hov2>(%a%a.@ %a)@]" (print_list dot forall) vl
         (print_list alt print_triggers) tl print_fmla f;
       List.iter forget_var vl
-  | Fquant (Fexists, fq) ->
-      assert false (*TODO*)
   | Fbinop (Fand, f1, f2) ->
       fprintf fmt "(%a and %a)" print_fmla f1 print_fmla f2
   | Fbinop (For, f1, f2) ->
@@ -123,8 +122,14 @@ let print_logic_decl env ctxt fmt = function
       fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n" print_ident id
         (print_list comma print_logic_binder) vl print_type ty print_term t;
       List.iter forget_var vl
-  | Lpredicate _ ->
-      assert false (*TODO*)
+  | Lpredicate (ls, None) ->
+      fprintf fmt "@[<hov 2>logic %a : %a -> prop@]"
+	print_ident ls.ls_name (print_list comma print_type) ls.ls_args
+  | Lpredicate (ls, Some fd) ->
+      let _,vl,f = open_ps_defn fd in
+      fprintf fmt "@[<hov 2>predicate %a(%a) = %a@]"
+	print_ident ls.ls_name 
+        (print_list comma print_logic_binder) vl print_fmla f
 
 let print_decl env ctxt fmt d = match d.d_node with
   | Dtype dl ->
@@ -154,4 +159,4 @@ let print_context env fmt ctxt =
 
 let print_goal env fmt (id, f, ctxt) =
   print_context env fmt ctxt;
-  fprintf fmt "@\n@[<hov 2>goal %a : %a@]" print_ident id print_fmla f
+  fprintf fmt "@\n@[<hov 2>goal %a : %a@]@\n" print_ident id print_fmla f

src/output/print_real.ml

+
+open Format
+open Big_int
+open Term
+
+let print_decimal_no_exponent fmt ~prefix_div = function
+  | "","0",_ | "0","",_ | "0","0",_ -> 
+      fprintf fmt "0.0"
+  | "",f, None -> 
+      fprintf fmt "0.%s" f
+  | i,"", None -> 
+      fprintf fmt "%s.0" i
+  | i,f, None ->
+      fprintf fmt "%s.%s" i f      
+  | i,f, Some e ->
+      let e = (int_of_string e) - String.length f in
+      if e = 0 then
+	fprintf fmt "%s%s" i f
+      else 
+        let op,s =
+          if e > 0 then "*",(String.make e '0')
+          else "/",(String.make (-e) '0')
+        in
+        if prefix_div then
+	  fprintf fmt "(%s %s%s.0 1%s.0)" op i f s
+        else
+	  fprintf fmt "(%s%s %s.0 1%s.0)" i f op s
+
+
+let num0 = Num.Int 0
+let num10 = Num.Int 10
+let num16 = Num.Int 16
+
+let decnumber s =
+  let r = ref num0 in
+  for i=0 to String.length s - 1 do
+    r := Num.add_num (Num.mult_num num10 !r) 
+      (Num.num_of_int (Char.code s.[i] - Char.code '0'))
+  done;
+  !r
+    
+let hexnumber s =
+  let r = ref num0 in
+  for i=0 to String.length s - 1 do
+    let c = s.[i] in
+    let v = 
+      match c with
+	| '0'..'9' -> Char.code c - Char.code '0'
+	| 'a'..'f' -> Char.code c - Char.code 'a' + 10
+	| 'A'..'F' -> Char.code c - Char.code 'A' + 10
+	| _ -> assert false
+    in
+    r := Num.add_num (Num.mult_num num16 !r) (Num.num_of_int v)
+  done;
+  !r
+    
+let print_hexa fmt i f e =
+  let mant = hexnumber (i^f) in
+  let v =
+    if e=""
+    then mant
+    else
+      if String.get e 0 = '-' then
+	Num.div_num mant 
+	  (Num.power_num (Num.Int 2) 
+	     (decnumber (String.sub e 1 (String.length e - 1))))
+      else
+	
+	Num.mult_num mant 
+	  (Num.power_num (Num.Int 2) (decnumber e))
+  in
+  let v = 
+    Num.div_num v 
+      (Num.power_num (Num.Int 16) (Num.num_of_int (String.length f))) 
+  in
+  let i = Num.floor_num v in
+  let f = ref (Num.sub_num v i) in
+  if Num.eq_num !f num0 then
+    fprintf fmt "%s.0" (Num.string_of_num i)
+  else
+    begin
+      fprintf fmt "%s." (Num.string_of_num i);
+      while not (Num.eq_num !f num0) do
+	f := Num.mult_num !f num10;
+	let i =  Num.floor_num !f in
+	fprintf fmt "%s" (Num.string_of_num i);
+	f := Num.sub_num !f i
+      done
+    end
+(*
+  Format.fprintf fmt ";;;; %s@\n" (Num.string_of_num v)
+*)
+
+let print_no_exponent fmt ~prefix_div = function
+  | RConstDecimal (i, f, e) -> print_decimal_no_exponent fmt ~prefix_div (i,f,e)
+  | RConstHexa (i, f, e) -> print_hexa fmt i f e 
+
+let hexa_to_decimal s =
+  let n = String.length s in
+  let rec compute acc i =
+    if i = n then 
+      acc 
+    else 
+      compute (add_int_big_int 
+		  (match s.[i] with 
+		    | '0'..'9' as c -> Char.code c - Char.code '0'
+		    | 'A'..'F' as c -> 10 + Char.code c - Char.code 'A'
+		    | 'a'..'f' as c -> 10 + Char.code c - Char.code 'a'
+		    | _ -> assert false)
+		  (mult_int_big_int 16 acc)) (i+1)
+  in
+  string_of_big_int (compute zero_big_int 0)
+
+let power2 n =
+  string_of_big_int (power_int_positive_int 2 n)
+
+let print_with_integers exp0_fmt exp_pos_fmt exp_neg_fmt fmt = function
+  | RConstDecimal (i, f, e) -> 
+      let f = if f = "0" then "" else f in
+      let e = 
+	(match e with None -> 0 | Some e -> int_of_string e) - 
+	String.length f 
+      in
+      if e = 0 then
+	fprintf fmt exp0_fmt (i ^ f)
+      else if e > 0 then
+	fprintf fmt exp_pos_fmt (i ^ f) ("1" ^ String.make e '0')
+      else
+	fprintf fmt exp_neg_fmt (i ^ f) ("1" ^ String.make (-e) '0')
+  | RConstHexa (i, f, e) -> 
+      let f = if f = "0" then "" else f in
+      let dec = hexa_to_decimal (i ^ f) in
+      let e = int_of_string e - 4 * String.length f in
+      if e = 0 then
+	fprintf fmt exp0_fmt dec
+      else if e > 0 then
+	fprintf fmt exp_pos_fmt dec (power2 e)
+      else
+	fprintf fmt exp_neg_fmt dec (power2 (-e))
+      
+
+let print fmt = function
+  | RConstDecimal (i, f,None) -> 
+      fprintf fmt "%s.%s" i f 
+  | RConstDecimal (i, f, Some e) -> 
+      fprintf fmt "%s.%se%s" i f e
+  | RConstHexa (i, f, e) -> 
+      fprintf fmt "0x%s.%sp%s" i f e
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../.. byte"
+End: 
+*)

src/output/print_real.mli

+
+open Format
+
+val print : formatter -> Term.real_constant -> unit

src/test.why

 
 (* test file *)
 
-theory Test1
-  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
-  use graph.Path
-  use import prelude.List
-  axiom Ax : forall l:int list. l=l
+  use import prelude.Int
+  logic id(x: int) : int = x
+  logic even(x: int) = 2*(x/2) = x
+  goal G : forall x:int. even(4) 
 end
 
 (*