Commit e4eaa5ca authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add a constraint on each type variable stating that the type is inhabited in Coq.

parent 23875720
......@@ -880,7 +880,7 @@ COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
endif
COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_FP)
COQLIBS_FILES = lib/coq/BuiltIn $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_FP)
COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
......@@ -897,6 +897,7 @@ COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
drivers/coq-realizations.aux: Makefile
$(if $(QUIET),@echo 'Generate $@' &&) \
(echo "(* generated automatically at compilation time *)"; \
echo 'theory BuiltIn meta "realized" "BuiltIn", "" end'; \
for f in $(COQLIBS_INT_FILES); do \
echo 'theory int.'"$$f"' meta "realized" "int.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_REAL_FILES); do \
......@@ -912,6 +913,7 @@ opt byte: $(COQVO)
install_no_local::
mkdir -p $(LIBDIR)/why3/coq
mkdir -p $(LIBDIR)/why3/coq/int
cp lib/coq/BuiltIn.vo $(LIBDIR)/why3/coq/
cp $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
mkdir -p $(LIBDIR)/why3/coq/real
cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
......@@ -926,8 +928,10 @@ endif
install_local: $(COQVO) drivers/coq-realizations.aux
ifneq "$(MAKECMDGOALS)" "clean"
ifneq "$(MAKECMDGOALS)" "update-coq"
include $(COQVD)
endif
endif
depend: $(COQVD)
......
......@@ -21,11 +21,8 @@ transformation "simplify_formula"
theory BuiltIn
prelude "Require Import ZArith."
prelude "Require Import Rbase."
prelude "Require Import BuiltIn."
syntax type int "Z"
syntax type real "R"
syntax predicate (=) "(%1 = %2)"
end
......
Require Export ZArith.
Require Export Rbase.
Class WhyType T := why_inhabitant : T.
Notation int := Z.
Global Instance int_WhyType : WhyType int.
exact Z0.
Qed.
Notation real := R.
Global Instance real_WhyType : WhyType real.
exact R0.
Qed.
Global Instance tuple_WhyType : forall T {T' : WhyType T} U {U' : WhyType U}, WhyType (T * U).
now split.
Qed.
Global Instance unit_WhyType : WhyType unit.
exact tt.
Qed.
Global Instance bool_WhyType : WhyType bool.
exact false.
Qed.
......@@ -64,12 +64,12 @@ let print_tv fmt tv =
let print_tv_binder fmt tv =
tv_set := Sid.add tv.tv_name !tv_set;
let n = id_unique iprinter tv.tv_name in
fprintf fmt "(%s:Type)" n
fprintf fmt "(%s:Type) {%s_WT:WhyType %s}" n n n
let print_implicit_tv_binder fmt tv =
tv_set := Sid.add tv.tv_name !tv_set;
let n = id_unique iprinter tv.tv_name in
fprintf fmt "{%s:Type}" n
fprintf fmt "{%s:Type} {%s_WT:WhyType %s}" n n n
let print_ne_params fmt stv =
Stv.iter
......@@ -137,6 +137,12 @@ let print_pr_real info fmt pr = print_id_real info fmt pr.pr_name
(** Types *)
let print_ts_tv fmt ts =
match ts.ts_args with
| [] -> fprintf fmt "%a" print_ts ts
| _ -> fprintf fmt "(%a %a)" print_ts ts
(print_list space print_tv) ts.ts_args
let rec print_ty info fmt ty = match ty.ty_node with
| Tyvar v -> print_tv fmt v
| Tyapp (ts, tl) when is_ts_tuple ts ->
......@@ -618,8 +624,10 @@ let print_type_decl ~prev info fmt ts =
print_ts ts print_params_list ts.ts_args
(print_previous_proof None) prev
else
fprintf fmt "@[<hov 2>Parameter %a : %aType.@]@\n@\n"
fprintf fmt "@[<hov 2>Parameter %a : %aType.@]@\n@[<hov 2>Axiom %a_WhyType : %aWhyType %a.@]@\nExisting Instance %a_WhyType.@\n@\n"
print_ts ts print_params_list ts.ts_args
print_ts ts print_params_list ts.ts_args print_ts_tv ts
print_ts ts
| Some ty ->
fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>Definition %a %a :=@ %a.@]@\n@\n"
print_ts ts (print_list space print_tv_binder) ts.ts_args
......@@ -635,14 +643,16 @@ let print_data_decl info fmt (ts,csl) =
fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>Inductive %s %a :=@\n@[<hov>%a@].@]@\n"
name (print_list space print_tv_binder) ts.ts_args
(print_list newline (print_constr info ts)) csl;
fprintf fmt "@[<hov 2>Axiom %s_WhyType : %aWhyType %a.@]@\nExisting Instance %s_WhyType.@\n"
name print_params_list ts.ts_args print_ts_tv ts name;
List.iter
(fun (cs,_) ->
let _, _, all_ty_params = ls_ty_vars cs in
if not (Stv.is_empty all_ty_params) then
let print fmt tv = fprintf fmt "[%a]" print_tv tv in
fprintf fmt "Implicit Arguments %a [%a].@\n"
print_ls cs
(print_list space print) ts.ts_args)
let print fmt tv = fprintf fmt "[%a]@ [%a_WT]" print_tv tv print_tv tv in
fprintf fmt "@[<hov 2>Implicit Arguments %a@ [%a].@]@\n"
print_ls cs
(print_list space print) ts.ts_args)
csl;
fprintf fmt "@\n"
......
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