Commit 10568fd0 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Coq output: fixed implicit arguments of inductive definitions

parent 719d6335
......@@ -106,6 +106,12 @@ type info = {
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
(ty_vars_args, ty_vars_value, Stv.union ty_vars_args ty_vars_value)
(* unused printing function
let print_path = print_list (constant_string ".") string
*)
......@@ -118,7 +124,22 @@ let print_id_real info fmt id =
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 lsymbols_under_definition = ref Sls.empty
let print_ls_real info fmt ls =
if Sls.mem ls !lsymbols_under_definition then
let _,_,l = ls_ty_vars ls in
if Stv.is_empty l then
print_id_real info fmt ls.ls_name
else
begin
fprintf fmt "(@@%a" (print_id_real info) ls.ls_name;
Stv.iter (fun _ -> fprintf fmt " _ _") l;
fprintf fmt ")"
end
else
print_id_real info fmt ls.ls_name
let print_ts_real info fmt ts = print_id_real info fmt ts.ts_name
(* unused printing function
let print_pr_real info fmt pr = print_id_real info fmt pr.pr_name
......@@ -152,14 +173,14 @@ let rec print_whytype info fmt ty =
begin
match tl with
| [] -> fprintf fmt "%a_WhyType" (print_ts_real info) ts
| l -> fprintf fmt "(@@%a_WhyType@ %a)"
| l -> fprintf fmt "(@@%a_WhyType@ %a)"
(print_ts_real info) ts
(print_list space (print_ty ~whytypes:true info)) l
end
end
end
and print_ty ?(whytypes=false) info fmt ty =
and print_ty ?(whytypes=false) info fmt ty =
begin match ty.ty_node with
| Tyvar v -> print_tv fmt v
| Tyapp (ts, tl) when is_ts_tuple ts ->
......@@ -400,11 +421,6 @@ let print_constr info ts fmt (cs,_) =
(print_arrow_list (print_ty info)) l
print_ts ts (print_list_pre space print_tv) ts.ts_args
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
(ty_vars_args, ty_vars_value, Stv.union ty_vars_args ty_vars_value)
(*
copy of old user scripts
......@@ -423,7 +439,7 @@ type statement =
exception StringValue of string
let read_generated_name =
let def = Str.regexp "\\(Definition\\|Fixpoint\\|Inductive\\)[ ]+\\([^ :(.]+\\)" in
let def = Str.regexp "\\(Definition\\|Fixpoint\\|Inductive\\|CoInductive\\)[ ]+\\([^ :(.]+\\)" in
fun ch ->
try
while true do
......@@ -724,8 +740,8 @@ let print_data_whytype_and_implicits fmt (name,ts,csl) =
(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]@ [%a_WT]"
(print_tv ~whytypes:false) tv (print_tv ~whytypes:false) tv
let print fmt tv = fprintf fmt "[%a]@ [%a_WT]"
(print_tv ~whytypes:false) tv (print_tv ~whytypes:false) tv
in
fprintf fmt "@[<hov 2>Implicit Arguments %a@ [%a].@]@\n"
print_ls cs
......@@ -871,12 +887,14 @@ let print_ind info fmt (pr,f) =
let print_ind_decl info s fmt (ps,bl) =
let _, _, all_ty_params = ls_ty_vars ps in
fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>%s %a%a : %a -> Prop :=@ @[<hov>%a@].@]@\n"
lsymbols_under_definition := Sls.add ps Sls.empty;
fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>%s %a %a: %a -> Prop :=@ @[<hov>%a@].@]@\n"
(match s with Ind -> "Inductive" | Coind -> "CoInductive")
print_ls ps print_implicit_params all_ty_params
(print_arrow_list (print_ty info)) ps.ls_args
(print_list newline (print_ind info)) bl;
fprintf fmt "@\n"
fprintf fmt "@\n";
lsymbols_under_definition := Sls.empty
let print_ind_decl info s fmt d =
if not (Mid.mem (fst d).ls_name info.info_syn) then
......
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