sortie alt-ergo (en cours)

parent b93ee249
......@@ -51,7 +51,8 @@ OCAMLBEST= @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
CAMLP4 = @CAMLP4O@
INCLUDES = -I src/core -I src/util -I src/parser -I src/transform -I src
INCLUDES = -I src/core -I src/util -I src/parser -I src/output \
-I src/transform -I src
BFLAGS = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@
# no -warn-error because some do not compile all files (e.g. those linked to APRON)
OFLAGS = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@
......@@ -101,24 +102,23 @@ doc/version.tex src/version.ml: Version version.sh config.status
#####
CORE_CMO := name.cmo ident.cmo ty.cmo term.cmo theory.cmo transform.cmo
CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
UTIL_CMO := pp.cmo loc.cmo util.cmo hashcons.cmo
UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))
PARSER_CMO := parser.cmo lexer.cmo typing.cmo
PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
flatten.cmo
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
OUTPUT_CMO := alt_ergo.cmo
OUTPUT_CMO := $(addprefix src/output/,$(OUTPUT_CMO))
CMO = $(UTIL_CMO) $(CORE_CMO) src/pretty.cmo $(PARSER_CMO) \
$(TRANSFORM_CMO) src/main.cmo
$(TRANSFORM_CMO) $(OUTPUT_CMO) src/main.cmo
CMX = $(CMO:.cmo=.cmx)
bin/why.opt: $(CMX)
......@@ -138,6 +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
# graphical interface
#####################
......
......@@ -18,6 +18,7 @@
(**************************************************************************)
open Format
open Theory
let files = ref []
let parse_only = ref false
......@@ -28,6 +29,7 @@ let print_stdout = ref false
let simplify_recursive = ref false
let inlining = ref false
let transform = ref false
let alt_ergo = ref false
let () =
Arg.parse
......@@ -40,6 +42,7 @@ let () =
"--simplify-recursive", Arg.Set simplify_recursive, "simplify recursive definition";
"--inline", Arg.Set inlining, "inline the definition not recursive";
"--transform", Arg.Set transform, "transform the goal (--inline,and --simplify-recursive set it) ";
"--alt-ergo", Arg.Set alt_ergo, "output for Alt-Ergo on stdout";
]
(fun f -> files := f :: !files)
"usage: why [options] files..."
......@@ -70,8 +73,10 @@ 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
let l = List.map (fun t -> t,Transform.apply Flatten.t t.Theory.th_ctxt)
let l = List.map (fun t -> t,Transform.apply Flatten.t t.th_ctxt)
l in
let l = if !simplify_recursive
then
......@@ -85,7 +90,7 @@ let transform l =
if !print_stdout then
List.iter (fun (t,dl) ->
Format.printf "@[@[<hov 2>theory %a@\n%a@]@\nend@]@\n@\n@?"
Pretty.print_ident t.Theory.th_name
Pretty.print_ident t.th_name
Pretty.print_context dl
) l
......
open Format
open Pp
open Ident
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 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
let rec print_type fmt ty = match ty.ty_node with
| Tyvar id ->
fprintf fmt "'%a" print_ident id
| Tyapp (ts, []) ->
print_ident fmt ts.ts_name
| Tyapp (ts, [ty]) ->
fprintf fmt "%a %a" print_type ty print_ident ts.ts_name
| Tyapp (ts, tyl) ->
fprintf fmt "(%a) %a"
(print_list comma print_type) tyl print_ident ts.ts_name
let rec print_term fmt t = match t.t_node with
| Tbvar _ ->
assert false
| Tconst (ConstInt s) ->
fprintf fmt "%s" s
| Tconst (ConstReal _) ->
assert false (*TODO*)
| Tvar { vs_name = id } | Tapp ({ ls_name = id }, []) ->
print_ident fmt id
| Tapp (ls, tl) ->
fprintf fmt "%a(%a)"
print_ident ls.ls_name (print_list comma print_term) tl
| Tlet (t1, tb) ->
let v, t2 = t_open_bound tb in
fprintf fmt "@[(let %a = %a@ in %a)@]" print_ident v.vs_name
print_term t1 print_term t2
| Tcase _ ->
assert false
| Teps _ ->
assert false
let rec print_fmla fmt f = match f.f_node with
| Fapp ({ ls_name = id }, []) ->
print_ident fmt id
| Fapp (ls, [t1; t2]) when ls == ps_equ ->
fprintf fmt "(%a = %a)" print_term t1 print_term t2
| Fapp (ls, tl) ->
fprintf fmt "%a(%a)"
print_ident ls.ls_name (print_list comma print_term) tl
| Fquant (Fforall, fq) ->
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
in
fprintf fmt "@[<hov2>(%a%a.@ %a)@]" (print_list dot forall) vl
(print_list alt print_triggers) tl print_fmla f
| 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) ->
fprintf fmt "(%a or %a)" print_fmla f1 print_fmla f2
| Fbinop (Fimplies, f1, f2) ->
fprintf fmt "(%a -> %a)" print_fmla f1 print_fmla f2
| Fbinop (Fiff, f1, f2) ->
fprintf fmt "(%a <-> %a)" print_fmla f1 print_fmla f2
| Fnot f ->
fprintf fmt "(not %a)" print_fmla f
| Ftrue ->
fprintf fmt "true"
| Ffalse ->
fprintf fmt "false"
| Fif (f1, f2, f3) ->
fprintf fmt "((%a and %a) or (not %a and %a))"
print_fmla f1 print_fmla f2 print_fmla f1 print_fmla f3
| Flet _ ->
assert false
| Fcase _ ->
assert false
and print_trigger fmt = function
| TrTerm t -> print_term fmt t
| TrFmla f -> print_fmla fmt f
and print_triggers fmt tl = print_list comma print_trigger fmt tl
let print_logic_binder fmt v =
fprintf fmt "%a: %a" print_ident v.vs_name print_type v.vs_ty
let print_type_decl fmt = function
| ts, Tabstract ->
fprintf fmt "type %a" print_ident ts.ts_name
| _, Talgebraic _ ->
assert false
let print_logic_decl fmt = function
| Lfunction (ls, None) ->
let tyl = ls.ls_args in
let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
fprintf fmt "@[<hov 2>logic %a : %a -> %a@]@\n" print_ident ls.ls_name
(print_list comma print_type) tyl print_type ty
| Lfunction (ls, Some defn) ->
let id = ls.ls_name in
let _, vl, t = open_fs_defn defn in
let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
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
| Lpredicate _ ->
assert false (*TODO*)
| Linductive _ ->
assert false
let print_decl fmt d = match d.d_node with
| Dtype dl ->
print_list newline print_type_decl fmt dl
| Dlogic dl ->
print_list newline print_logic_decl fmt dl
| Dprop (Paxiom, id, f) ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n" print_ident id print_fmla f
| Dprop (Pgoal, id, f) ->
fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n" print_ident id print_fmla f
| Dprop (Plemma, _, _) ->
assert false
| Duse _ | Dclone _ ->
()
let print_context fmt ctxt =
let decls = Context.get_decls ctxt in
print_list newline2 print_decl fmt decls
open Format
open Term
open Theory
val print_term : formatter -> term -> unit
val print_fmla : formatter -> fmla -> unit
val print_context : formatter -> context -> unit
......@@ -65,6 +65,7 @@ let print_iter2 iter sep1 sep2 print1 print2 fmt l =
let print_pair_delim start sep stop pr1 pr2 fmt (a,b) =
fprintf fmt "%a%a%a%a%a" start () pr1 a sep () pr2 b stop ()
let dot fmt () = fprintf fmt ".@ "
let comma fmt () = fprintf fmt ",@ "
let simple_comma fmt () = fprintf fmt ", "
let underscore fmt () = fprintf fmt "_"
......
......@@ -64,6 +64,7 @@ val space : formatter -> unit -> unit
val alt : formatter -> unit -> unit
val newline : formatter -> unit -> unit
val newline2 : formatter -> unit -> unit
val dot : formatter -> unit -> unit
val comma : formatter -> unit -> unit
val simple_comma : formatter -> unit -> unit
val semi : formatter -> unit -> unit
......
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