Commit efc1378b authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

Coq ssreflect driver (wip)

parent 82e96330
......@@ -2,7 +2,7 @@
prelude "(* This file is generated by Why3's coq-ssreflect driver *)"
prelude "(* Beware! Only edit allowed sections below *)"
printer "coq"
printer "coq-ssr"
filename "%t.v"
valid 0
......@@ -20,11 +20,25 @@ transformation "simplify_formula"
theory BuiltIn
prelude "Require Import ssrwhy3."
prelude "
Require Import ssreflect ssrbool ssrfun ssrnat seq eqtype ssrint.
Require Import ssrint ssrwhy3.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
"
syntax type int "int"
syntax type real "R"
syntax predicate (=) "(%1 = %2)"
end
theory HighOrd
syntax type func "(%1 -> %2)"
syntax type pred "(%1 -> bool)"
syntax function (@) "(%1 %2)"
end
theory Bool
......@@ -54,10 +68,12 @@ end
theory int.Int
prelude "Require Import ssralg ssrnum.
prelude "
Require Import ssralg ssrnum.
Import GRing.Theory Num.Theory.
Local Open Scope ring_scope.
"
Local Open Scope ring_scope."
syntax function zero "0%Z"
syntax function one "1%Z"
......@@ -92,3 +108,15 @@ Local Open Scope ring_scope.
remove prop ZeroLessOne
end
theory array.Array
syntax type array "(array %1)"
syntax function get "(get %1 %2)"
syntax function length "(size %1 : int)"
syntax function elts "(get %1)"
syntax function set "(set %1 %2 %3)"
syntax function make "(make %1 %2)"
end
......@@ -45,33 +45,49 @@ let forget_all () = forget_all iprinter
let tv_set = ref Sid.empty
(* info *)
type info = {
info_syn : syntax_map;
symbol_printers : (string * ident_printer) Mid.t;
realization : bool;
ssreflect: bool;
}
(* type variables *)
let print_tv ~whytypes fmt tv =
let print_tv info ~whytypes fmt tv =
let n = id_unique iprinter tv.tv_name in
fprintf fmt "%s" n;
if whytypes then fprintf fmt " %s_WT" n
if whytypes && not info.ssreflect then fprintf fmt " %s_WT" n
let print_tv_binder ~whytypes ~implicit fmt tv =
let print_tv_binder info ~whytypes ~implicit fmt tv =
tv_set := Sid.add tv.tv_name !tv_set;
let n = id_unique iprinter tv.tv_name in
if implicit then fprintf fmt "{%s:Type}" n else fprintf fmt "(%s:Type)" n;
if whytypes then fprintf fmt " {%s_WT:WhyType %s}" n n
if info.ssreflect then
fprintf fmt "{%s: why3Type}" n
else begin
if implicit then fprintf fmt "{%s:Type}" n else fprintf fmt "(%s:Type)" n;
if whytypes then fprintf fmt " {%s_WT:WhyType %s}" n n
end
let print_tv_binders ~whytypes ~implicit fmt stv =
Stv.iter (fprintf fmt "@ %a" (print_tv_binder ~whytypes ~implicit)) stv
let print_tv_binders info ~whytypes ~implicit fmt stv =
Stv.iter (fprintf fmt "@ %a" (print_tv_binder info ~whytypes ~implicit)) stv
let print_tv_binders_list ~whytypes ~implicit fmt ltv =
List.iter (fprintf fmt "@ %a" (print_tv_binder ~whytypes ~implicit)) ltv
let print_tv_binders_list info ~whytypes ~implicit fmt ltv =
List.iter (fprintf fmt "@ %a" (print_tv_binder info ~whytypes ~implicit)) ltv
let print_params ~whytypes fmt stv =
let print_params info ~whytypes fmt stv =
if Stv.is_empty stv then () else
fprintf fmt "forall%a,@ " (print_tv_binders ~whytypes ~implicit:true) stv
fprintf fmt "forall%a,@ "
(print_tv_binders info ~whytypes ~implicit:true) stv
let print_params_list ~whytypes fmt ltv =
let print_params_list info ~whytypes fmt ltv =
match ltv with
| [] -> ()
| _ -> fprintf fmt "forall%a,@ " (print_tv_binders_list ~whytypes ~implicit:false) ltv
| _ ->
fprintf fmt "forall%a,@ "
(print_tv_binders_list info ~whytypes ~implicit:false) ltv
let forget_tvs () =
Sid.iter (forget_id iprinter) !tv_set;
......@@ -93,14 +109,6 @@ let print_ls fmt ls =
let print_pr fmt pr =
fprintf fmt "%s" (id_unique iprinter pr.pr_name)
(* info *)
type info = {
info_syn : syntax_map;
symbol_printers : (string * ident_printer) Mid.t;
realization : bool;
}
let ls_ty_vars ls =
let ty_vars_args = List.fold_left Ty.ty_freevars Stv.empty ls.ls_args in
let ty_vars_value = Opt.fold Ty.ty_freevars Stv.empty ls.ls_value in
......@@ -129,15 +137,15 @@ let print_pr_real info fmt pr = print_id_real info fmt pr.pr_name
(** Types *)
let print_ts_tv fmt ts =
let print_ts_tv info 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 ~whytypes:false)) ts.ts_args
(print_list space (print_tv info ~whytypes:false)) ts.ts_args
let rec print_ty info fmt ty =
begin match ty.ty_node with
| Tyvar v -> print_tv ~whytypes:false fmt v
| Tyvar v -> print_tv info ~whytypes:false fmt v
| Tyapp (ts, tl) when is_ts_tuple ts ->
begin
match tl with
......@@ -254,7 +262,9 @@ and print_tnode _opl opr info fmt t = match t.t_node with
let number_format = {
Number.long_int_support = true;
Number.extra_leading_zeros_support = true;
Number.dec_int_support = Number.Number_custom "%s%%Z";
Number.dec_int_support =
if info.ssreflect then Number.Number_custom "%s%%:Z"
else Number.Number_custom "%s%%Z";
Number.hex_int_support = Number.Number_unsupported;
Number.oct_int_support = Number.Number_unsupported;
Number.bin_int_support = Number.Number_unsupported;
......@@ -382,7 +392,8 @@ let print_expr info fmt =
let print_constr info ts fmt (cs,_) =
fprintf fmt "@[<hov 4>| %a : %a%a%a@]" print_ls cs
(print_arrow_list (print_ty info)) cs.ls_args
print_ts ts (print_list_pre space (print_tv ~whytypes:false)) ts.ts_args
print_ts ts
(print_list_pre space (print_tv info ~whytypes:false)) ts.ts_args
(*
......@@ -671,23 +682,30 @@ let print_type_decl ~prev info fmt ts =
fprintf fmt "(* Why3 goal *)@\n%s@\n" c
| Some (Axiom _) ->
fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Variable %a : %aType.@]@\n@[<hov 2>Hypothesis %a_WhyType : %aWhyType %a.@]@\nExisting Instance %a_WhyType.@\n@\n"
print_ts ts (print_params_list ~whytypes:false) ts.ts_args
print_ts ts (print_params_list ~whytypes:true) ts.ts_args print_ts_tv ts
print_ts ts
print_ts ts (print_params_list info ~whytypes:false) ts.ts_args
print_ts ts (print_params_list info ~whytypes:true)
ts.ts_args (print_ts_tv info) ts print_ts ts
| _ ->
fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Definition %a : %aType.@]@\n%a@\n"
print_ts ts (print_params_list ~whytypes:false) ts.ts_args
print_ts ts (print_params_list info ~whytypes:false) ts.ts_args
(print_previous_proof None info) prev
else
fprintf fmt "@[<hov 2>Axiom %a : %aType.@]@\n@[<hov 2>Parameter %a_WhyType : %aWhyType %a.@]@\nExisting Instance %a_WhyType.@\n@\n"
print_ts ts (print_params_list ~whytypes:false) ts.ts_args
print_ts ts (print_params_list ~whytypes:true) ts.ts_args print_ts_tv ts
print_ts ts
else begin
fprintf fmt "@[<hov 2>Axiom %a : %aType.@]@\n"
print_ts ts (print_params_list info ~whytypes:false) ts.ts_args;
if not info.ssreflect then begin
fprintf fmt "@[<hov 2>Parameter %a_WhyType : %aWhyType %a.@]@\n"
print_ts ts (print_params_list info ~whytypes:true) ts.ts_args
(print_ts_tv info) ts;
fprintf fmt "Existing Instance %a_WhyType.@\n"
print_ts ts
end;
fprintf fmt "@\n"
end
| Some ty ->
fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>Definition %a%a :=@ %a.@]@\n@\n"
print_ts ts
(print_list_pre space
(print_tv_binder ~whytypes:false ~implicit:false)) ts.ts_args
(print_tv_binder info ~whytypes:false ~implicit:false)) ts.ts_args
(print_ty info) ty
let print_type_decl ~prev info fmt ts =
......@@ -701,18 +719,21 @@ let print_data_decl ~first info fmt ts csl =
else fprintf fmt "@\nwith";
fprintf fmt " %s%a :=@\n@[<hov>%a@]"
name (print_list_pre space
(print_tv_binder ~whytypes:false ~implicit:false)) ts.ts_args
(print_tv_binder info ~whytypes:false ~implicit:false)) ts.ts_args
(print_list newline (print_constr info ts)) csl;
name
let print_data_whytype_and_implicits fmt (name,ts,csl) =
fprintf fmt "@[<hov 2>Axiom %s_WhyType : %aWhyType %a.@]@\nExisting Instance %s_WhyType.@\n"
name (print_params_list ~whytypes:true) ts.ts_args print_ts_tv ts name;
let print_data_whytype_and_implicits info fmt (name,ts,csl) =
if not info.ssreflect then
fprintf fmt "@[<hov 2>Axiom %s_WhyType : %aWhyType %a.@]@\nExisting Instance %s_WhyType.@\n"
name (print_params_list info ~whytypes:true) ts.ts_args
(print_ts_tv info) 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 ~whytypes:false) tv in
let print fmt tv =
fprintf fmt "[%a]" (print_tv info ~whytypes:false) tv in
fprintf fmt "@[<hov 2>Implicit Arguments %a@ [%a].@]@\n"
print_ls cs
(print_list space print) ts.ts_args)
......@@ -733,7 +754,7 @@ let print_data_decls info fmt tl =
if none then () else
begin
fprintf fmt ".@]@\n";
List.iter (print_data_whytype_and_implicits fmt) d
List.iter (print_data_whytype_and_implicits info fmt) d
end
let print_ls_type info fmt = function
......@@ -748,7 +769,7 @@ let print_param_decl ~prev info fmt ls =
fprintf fmt "(* Why3 goal *)@\n%s@\n" c
| Some (Axiom _) ->
fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Variable %a: %a%a%a.@]@\n@\n"
print_ls ls (print_params ~whytypes:true) all_ty_params
print_ls ls (print_params info ~whytypes:true) all_ty_params
(print_arrow_list (print_ty info)) ls.ls_args
(print_ls_type info) ls.ls_value
| (* Some Info *) _ when Mid.mem ls.ls_name info.info_syn ->
......@@ -763,13 +784,13 @@ let print_param_decl ~prev info fmt ls =
List.iter forget_var vl
| _ ->
fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Definition %a: %a%a%a.@]@\n%a@\n"
print_ls ls (print_params ~whytypes:true) all_ty_params
print_ls ls (print_params info ~whytypes:true) all_ty_params
(print_arrow_list (print_ty info)) ls.ls_args
(print_ls_type info) ls.ls_value
(print_previous_proof None info) prev
else
fprintf fmt "@[<hov 2>Parameter %a: %a%a%a.@]@\n@\n"
print_ls ls (print_params ~whytypes:true) all_ty_params
print_ls ls (print_params info ~whytypes:true) all_ty_params
(print_arrow_list (print_ty info)) ls.ls_args
(print_ls_type info) ls.ls_value
......@@ -782,7 +803,7 @@ let print_logic_decl info fmt (ls,ld) =
let vl,e = open_ls_defn ld in
fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>Definition %a%a%a: %a :=@ %a.@]@\n"
print_ls ls
(print_tv_binders ~whytypes:true ~implicit:true) all_ty_params
(print_tv_binders info ~whytypes:true ~implicit:true) all_ty_params
(print_list_pre space (print_vsty info)) vl
(print_ls_type info) ls.ls_value
(print_expr info) e;
......@@ -795,7 +816,7 @@ let print_equivalence_lemma ~prev info fmt name (ls,ld) =
fprintf fmt
"(* Why3 goal *)@\n@[<hov 2>Lemma %s :@ %a%a.@]@\n"
name
(print_params ~whytypes:true) all_ty_params
(print_params info ~whytypes:true) all_ty_params
(print_expr info) def_formula;
fprintf fmt "%a@\n"
(print_previous_proof (Some (all_ty_params,def_formula)) info) prev
......@@ -823,7 +844,7 @@ let print_recursive_decl info fmt (ls,ld) =
let vl,e = open_ls_defn ld in
fprintf fmt "%a%a%a {struct %a}: %a :=@ %a@]"
print_ls ls
(print_tv_binders ~whytypes:true ~implicit:true) all_ty_params
(print_tv_binders info ~whytypes:true ~implicit:true) all_ty_params
(print_list_pre space (print_vsty info)) vl
print_vs (List.nth vl i)
(print_ls_type info) ls.ls_value
......@@ -852,7 +873,8 @@ let print_ind info fmt (pr,f) =
let print_ind_decl info fmt ps bl =
let _, _, all_ty_params = ls_ty_vars ps in
fprintf fmt " %a%a: %aProp :=@ @[<hov>%a@]"
print_ls ps (print_tv_binders ~whytypes:true ~implicit:true) all_ty_params
print_ls ps
(print_tv_binders info ~whytypes:true ~implicit:true) all_ty_params
(print_arrow_list (print_ty info)) ps.ls_args
(print_list newline (print_ind info)) bl
......@@ -885,16 +907,16 @@ let print_prop_decl ~prev info fmt (k,pr,f) =
match prev with
| Some (Axiom _) when stt = "Lemma" ->
fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Hypothesis %a : %a%a.@]@\n@\n"
print_pr pr (print_params ~whytypes:true) params
print_pr pr (print_params info ~whytypes:true) params
(print_fmla info) f
| _ ->
fprintf fmt "(* Why3 goal *)@\n@[<hov 2>%s %a : %a%a.@]@\n%a@\n"
stt print_pr pr (print_params ~whytypes:true) params
stt print_pr pr (print_params info ~whytypes:true) params
(print_fmla info) f
(print_previous_proof (Some (params,f)) info) prev
else
fprintf fmt "@[<hov 2>Axiom %a : %a%a.@]@\n@\n"
print_pr pr (print_params ~whytypes:true) params
print_pr pr (print_params info ~whytypes:true) params
(print_fmla info) f;
forget_tvs ()
......@@ -931,7 +953,7 @@ let print_decl ~old info fmt d =
let print_decls ~old info fmt dl =
fprintf fmt "@\n@[<hov>%a@]" (print_list nothing (print_decl ~old info)) dl
let print_task printer_args realize ?old fmt task =
let print_task printer_args ~realize ~ssreflect ?old fmt task =
(* eprintf "Task:%a@.@." Pretty.print_task task; *)
forget_all ();
print_prelude fmt printer_args.prelude;
......@@ -983,6 +1005,7 @@ let print_task printer_args realize ?old fmt task =
info_syn = get_syntax_map task;
symbol_printers = symbol_printers;
realization = realize;
ssreflect = ssreflect;
}
in
let old = ref (match old with
......@@ -992,10 +1015,10 @@ let print_task printer_args realize ?old fmt task =
output_remaining fmt !old
let print_task_full args ?old fmt task =
print_task args false ?old fmt task
print_task args ~realize:false ~ssreflect:false ?old fmt task
let print_task_real args ?old fmt task =
print_task args true ?old fmt task
print_task args ~realize:true ~ssreflect:false ?old fmt task
let () = register_printer "coq" print_task_full
~desc:"Printer@ for@ the@ Coq@ proof@ assistant@ \
......@@ -1004,6 +1027,13 @@ let () = register_printer "coq-realize" print_task_real
~desc:"Printer@ for@ the@ Coq@ proof@ assistant@ \
(with@ realization@ capabilities)."
let print_task_full_ssr args ?old fmt task =
print_task args ~realize:false ~ssreflect:true ?old fmt task
let () = register_printer "coq-ssr" print_task_full_ssr
~desc:"Printer@ for@ the@ Coq@ proof@ assistant,@ ssreflect@ extension\
(without@ realization@ capabilities)."
(* specific printer for realization of theories *)
(* OBSOLETE
......
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