Commit 51f20ce0 authored by Francois Bobot's avatar Francois Bobot

ajout de inlining non fonctionnel

parent 5136e7e9
......@@ -100,18 +100,28 @@ doc/version.tex src/version.ml: Version version.sh config.status
# why
#####
CORE_CMO = src/core/name.cmo src/core/ident.cmo src/core/ty.cmo \
src/core/term.cmo src/core/theory.cmo
UTIL_CMO = src/util/pp.cmo src/util/loc.cmo src/util/util.cmo \
src/util/hashcons.cmo
PARSER_CMO = src/parser/parser.cmo src/parser/lexer.cmo src/parser/typing.cmo
CORE_CMO := name.cmo ident.cmo ty.cmo term.cmo theory.cmo
TRANSFORM_CMO = src/transform/transform.cmo src/transform/simplify_recursive_definition.cmo
CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(TRANSFORM_CMO) src/pretty.cmo src/main.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 := transform.cmo simplify_recursive_definition.cmo \
inlining.cmo
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
CMO = $(UTIL_CMO) $(CORE_CMO) src/pretty.cmo $(PARSER_CMO) $(TRANSFORM_CMO) src/main.cmo
CMX = $(CMO:.cmo=.cmx)
bin/why.opt: $(CMX)
echo $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(TRANSFORM_CMO)
$(if $(QUIET),@echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ $^
$(STRIP) $@
......
......@@ -25,7 +25,9 @@ let type_only = ref false
let debug = ref false
let loadpath = ref []
let print_stdout = ref false
let print_simplify_recursive = ref false
let simplify_recursive = ref false
let inlining = ref false
let () =
Arg.parse
["--parse-only", Arg.Set parse_only, "stops after parsing";
......@@ -34,7 +36,8 @@ let () =
"-I", Arg.String (fun s -> loadpath := s :: !loadpath),
"<dir> adds dir to the loadpath";
"--print-stdout", Arg.Set print_stdout, "print the results to stdout";
"--print-simplify-recursive", Arg.Set print_simplify_recursive, "print the results of simplify recursive definition";
"--simplify-recursive", Arg.Set simplify_recursive, "simplify recursive definition";
"--inline", Arg.Set inlining, "inline the definition not recursive";
]
(fun f -> files := f :: !files)
"usage: why [options] files..."
......@@ -59,20 +62,31 @@ let type_file env file =
close_in c;
if !parse_only then env else Typing.add_theories env f
let transform l =
let transform = !simplify_recursive || !inlining in
if !print_stdout && not transform then
List.iter (Pretty.print_theory Format.std_formatter)
(Typing.list_theory l)
else
let l = List.map (fun t -> t.Theory.th_decls) (Typing.list_theory l) in
let l = if !simplify_recursive
then
List.map (fun t -> Transform.apply
Simplify_recursive_definition.t_use t) l
else l in
let l = if !inlining
then
List.map (fun t -> Transform.apply Inlining.t_use t) l
else l in
if !print_stdout then
List.iter (Pretty.print_decl_or_use_list Format.std_formatter) l
let () =
try
let env = Typing.create !loadpath in
let l = List.fold_left type_file env !files in
if !print_stdout then
List.iter (Pretty.print_theory Format.std_formatter)
(Typing.list_theory l);
if !print_simplify_recursive then
List.iter (fun t ->
let de = Transform.apply
Simplify_recursive_definition.t_use t.Theory.th_decls in
(Pp.print_list Pp.newline Pretty.print_decl_or_use)
Format.std_formatter de)
(Typing.list_theory l)
transform l
with e when not !debug ->
eprintf "%a@." report e;
exit 1
......
......@@ -147,6 +147,10 @@ let print_decl_or_use fmt = function
| Decl d -> fprintf fmt "%a" print_decl d
| Use u -> fprintf fmt "use export %a@\n" print_ident u.th_name
let print_decl_or_use_list fmt de =
fprintf fmt "@[<hov>%a@]"
(Pp.print_list Pp.newline print_decl_or_use) de
let print_theory fmt t =
fprintf fmt "@[@[<hov 2>theory %a@\n%a@]@\nend@]@\n@\n" print_ident t.th_name
(print_list newline print_decl_or_use) t.th_decls;
......
......@@ -32,4 +32,6 @@ val print_decl : formatter -> decl -> unit
val print_decl_or_use : formatter -> decl_or_use -> unit
val print_decl_or_use_list : formatter -> decl_or_use list -> unit
val print_theory : formatter -> theory -> unit
......@@ -177,6 +177,7 @@ struct
let f x = LH2.from_list (f (LH1.to_list x)) in
let memo_t = Hashtbl.create 16 in
t (memo f LH1.tag memo_t) (fun () -> Hashtbl.clear memo_t)
end
open Term
......
......@@ -33,7 +33,6 @@ val apply : ('a,'b) t -> 'a list -> 'b list
(* clear the datastructures used to store the memoisation *)
val clear : ('a,'b) t -> unit
module type S =
sig
(* The type of the elements of the list*)
......
......@@ -44,6 +44,24 @@ let print_list_delim start stop sep pr fmt = function
| [] -> ()
| l -> fprintf fmt "%a%a%a" start () (print_list sep pr) l stop ()
let print_iter1 iter sep print fmt l =
let first = ref true in
iter (fun x ->
if !first
then first := false
else sep fmt ();
print fmt x ) l
let print_iter2 iter sep1 sep2 print1 print2 fmt l =
let first = ref true in
iter (fun x y ->
if !first
then first := false
else sep1 fmt ();
print1 fmt x;sep2 fmt (); print2 fmt y) 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 ()
......
......@@ -42,6 +42,22 @@ val print_pair_delim :
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) -> Format.formatter -> 'a * 'b -> unit
val print_iter1 :
(('a -> unit) -> 'b -> unit) ->
(Format.formatter -> unit -> unit) ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'b -> unit
val print_iter2:
(('a -> 'b -> unit) -> 'c -> unit) ->
(Format.formatter -> unit -> unit) ->
(Format.formatter -> unit -> unit) ->
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
Format.formatter -> 'c -> unit
val print_pair :
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) -> Format.formatter -> 'a * 'b -> 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