Commit cc79baa8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Move Coq realizations from a .ml file to a driver file.

Note that the file is still generated at compilation time.

The "realized" meta takes two arguments. The first one is the path+name of
the theory, the second one is the translation of it for the target prover.
The meta is supposed to be put into a printer file, so there is no
ambiguity on the target. The second argument can be left empty if it can be
inferred from the first one.

Note that the first argument is not really satisfactory, since it is
redundant with the theory part of the driver. Moreover, its handling is a
bit crude: it does not take into account rich qualifiers and it does not
generate proper error messages if it does not match the theory.
parent d65e0492
......@@ -111,7 +111,7 @@ plugins: plugins.@OCAMLBEST@
LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
src/parser/parser.mli src/parser/parser.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml \
src/driver/driver_lexer.ml src/coq_config.ml
src/driver/driver_lexer.ml
LIB_UTIL = stdlib exn_printer debug pp loc print_tree print_number \
cmdline hashweak hashcons util sysutil rc plugin
......@@ -138,7 +138,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq simplify gappa \
cvc3 yices
LIBMODULES = src/config src/coq_config \
LIBMODULES = src/config \
$(addprefix src/util/, $(LIB_UTIL)) \
$(addprefix src/core/, $(LIB_CORE)) \
$(addprefix src/parser/, $(LIB_PARSER)) \
......@@ -856,16 +856,15 @@ COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
%.vo: %.v
$(COQC) -R lib/coq Why3 $<
src/coq_config.ml:
echo "let realized_theories = [" > $@
for f in $(COQLIBS_INT_FILES); do echo ' ["int"; "'"$$f"'"];'; done >> $@
for f in $(COQLIBS_REAL_FILES); do echo ' ["real"; "'"$$f"'"];'; done >> $@
drivers/coq-realizations.aux:
echo "(* generated automatically at compilation time *)" > $@
for f in $(COQLIBS_INT_FILES); do echo 'theory int.'"$$f"' meta "realized" "int.'"$$f"'", "" end'; done >> $@
for f in $(COQLIBS_REAL_FILES); do echo 'theory real.'"$$f"' meta "realized" "real.'"$$f"'", "" end'; done >> $@
ifeq (@enable_coq_fp_libs@,yes)
for f in $(COQLIBS_FP_FILES); do echo ' ["floating_point"; "'"$$f"'"];'; done >> $@
for f in $(COQLIBS_FP_FILES); do echo 'theory floating_point.'"$$f"' meta "realized" "floating_point.'"$$f"'", "" end'; done >> $@
endif
echo "]" >> $@
all: $(COQVO)
opt byte: $(COQVO)
install_no_local::
mkdir -p $(LIBDIR)/why3/coq
......@@ -877,8 +876,9 @@ ifeq (@enable_coq_fp_libs@,yes)
mkdir -p $(LIBDIR)/why3/coq/floating_point
cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
endif
cp drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
install_local: $(COQVO)
install_local: $(COQVO) drivers/coq-realizations.aux
include .depend.coq-libs
......@@ -893,11 +893,16 @@ clean::
else
src/coq_config.ml:
echo "let realized_theories = []" > $@
drivers/coq-realizations.aux:
echo "(* generated automatically at compilation time *)" > $@
endif
opt byte: drivers/coq-realizations.aux
clean::
rm -f drivers/coq-realizations.aux
########
# Tptp2why
########
......
......@@ -280,3 +280,6 @@ theory real.Trigonometry
remove prop Sin_pi2
end
(* this file has an extension .aux rather than .gen since it should not be distributed *)
import "coq-realizations.aux"
......@@ -171,6 +171,7 @@ exception KnownLogicSyntax of lsymbol
let meta_syntax_type = register_meta "syntax_type" [MTtysymbol; MTstring]
let meta_syntax_logic = register_meta "syntax_logic" [MTlsymbol; MTstring]
let meta_remove_prop = register_meta "remove_prop" [MTprsymbol]
let meta_realized = register_meta "realized" [MTstring; MTstring]
let syntax_type ts s =
check_syntax s (List.length ts.ts_args);
......
......@@ -48,6 +48,7 @@ val print_prelude_for_theory : theory -> prelude_map pp
val meta_syntax_type : meta
val meta_syntax_logic : meta
val meta_remove_prop : meta
val meta_realized : meta
val syntax_type : tysymbol -> string -> tdecl
val syntax_logic : lsymbol -> string -> tdecl
......
......@@ -32,10 +32,12 @@ let black_list =
[ "at"; "cofix"; "exists2"; "fix"; "IF"; "left"; "mod"; "Prop";
"return"; "right"; "Set"; "Type"; "using"; "where"; ]
let iprinter =
let fresh_printer () =
let isanitize = sanitizer char_to_alpha char_to_alnumus in
create_ident_printer black_list ~sanitizer:isanitize
let iprinter = fresh_printer ()
let forget_all () = forget_all iprinter
let tv_set = ref Sid.empty
......@@ -102,7 +104,7 @@ let print_pr fmt pr =
type info = {
info_syn : syntax_map;
symbol_printers : (Theory.theory * ident_printer) Mid.t;
symbol_printers : (string * ident_printer) Mid.t;
realization : bool;
}
......@@ -111,12 +113,10 @@ let print_path = print_list (constant_string ".") string
let print_id fmt id = string fmt (id_unique iprinter id)
let print_id_real info fmt id =
try let th,ipr = Mid.find id info.symbol_printers in
fprintf fmt "%a.%s.%s"
print_path th.Theory.th_path
th.Theory.th_name.id_string
(id_unique ipr id)
with Not_found -> print_id fmt id
try
let path,ipr = Mid.find id info.symbol_printers in
fprintf fmt "%s.%s" path (id_unique ipr id)
with Not_found -> print_id fmt id
let print_ls_real info fmt ls = print_id_real info fmt ls.ls_name
let print_ts_real info fmt ts = print_id_real info fmt ts.ts_name
......@@ -677,53 +677,45 @@ let print_decl ~old info fmt d = match d.d_node with
let print_decls ~old info fmt dl =
fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl ~old info)) dl
let init_printer th =
let isanitize = sanitizer char_to_alpha char_to_alnumus in
let pr = create_ident_printer black_list ~sanitizer:isanitize in
Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
pr
(* TODO: add a driver meta and make lookup for realized theories a bit
more efficient *)
let realized_theories = Coq_config.realized_theories
let print_task _env pr thpr realize ?old fmt task =
let print_task env pr thpr realize ?old fmt task =
forget_all ();
print_prelude fmt pr;
print_th_prelude task fmt thpr;
let symbol_printers,decls =
let used = Task.used_theories task in
let used = Mid.filter (fun _ th -> List.mem (th.Theory.th_path@[th.Theory.th_name.id_string]) realized_theories) used in
(* 2 cases: goal is clone T with [] or goal is a real goal *)
let used = match task with
| None -> assert false
| Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
Sid.iter
(fun id -> ignore (id_unique iprinter id))
th.Theory.th_local;
Mid.remove th.Theory.th_name used
| _ -> used
in
(*
(* output the Require commands *)
List.iter
(fprintf fmt "Add Rec LoadPath \"%s\".@\n")
(Env.get_loadpath env);
*)
Mid.iter
(fun id th -> fprintf fmt "Require %a.%s.@\n"
print_path th.Theory.th_path id.id_string)
used;
let symbols = Task.used_symbols used in
(* build the printers for each theories *)
let printers = Mid.map init_printer used in
let decls = Task.local_decls task symbols in
let symbols =
Mid.map (fun th -> (th,Mid.find th.Theory.th_name printers))
symbols
in
symbols, decls
in
(* find theories that are both used and realized from metas *)
let realized_theories =
Task.on_meta meta_realized (fun mid args ->
match args with
| [Theory.MAstr s1; Theory.MAstr s2] ->
(* TODO: do not split string; in fact, do not even use a string argument *)
let f,id = let l = split_string_rev s1 '.' in List.rev (List.tl l),List.hd l in
let th = Env.find_theory env f id in
Mid.add th.Theory.th_name (th, if s2 = "" then s1 else s2) mid
| _ -> assert false
) Mid.empty task in
(* 2 cases: goal is clone T with [] or goal is a real goal *)
let realized_theories =
match task with
| None -> assert false
| Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
Mid.remove th.Theory.th_name realized_theories
| _ -> realized_theories in
let realized_theories' =
Mid.map (fun (th,s) -> fprintf fmt "Require %s.@\n" s; th) realized_theories in
let realized_symbols = Task.used_symbols realized_theories' in
let local_decls = Task.local_decls task realized_symbols in
(* associate a special printer to each symbol in a realized theory *)
let symbol_printers =
let printers =
Mid.map (fun th ->
let pr = fresh_printer () in
Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
pr
) realized_theories' in
Mid.map (fun th ->
(snd (Mid.find th.Theory.th_name realized_theories),
Mid.find th.Theory.th_name printers)
) realized_symbols in
let info = {
info_syn = get_syntax_map task;
symbol_printers = symbol_printers;
......@@ -734,7 +726,7 @@ let print_task _env pr thpr realize ?old fmt task =
| None -> None
| Some ch -> Some(ref NoWhere,ch)
in
print_decls ~old info fmt decls
print_decls ~old info fmt local_decls
let print_task_full env pr thpr ?old fmt task =
print_task env pr thpr false ?old fmt task
......
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