program extraction (WIP)

parent db97f181
......@@ -119,6 +119,12 @@ tools
- Maybe : make something generic for the dialog box with memory.
OCaml extraction
----------------
- allow other realizations for arithmetic, such as Zarith or GMP
(currently this is Num)
provers
-------
......
......@@ -44,6 +44,7 @@ bads () {
drivers () {
for f in $1/*.drv; do
if [ $f = "drivers/ocaml.drv" ]; then continue; fi
echo -n " "$f"... "
# running Why
if ! echo "theory Test goal G : 1=2 end" | $pgm -F why --driver $f - > /dev/null 2>&1; then
......
filename "%f_%t.ml"
theory BuiltIn
syntax type int "Num.num"
syntax predicate (=) "(%1 = %2)"
end
theory option.Option
syntax type option "(%1 option)"
syntax function None "None"
syntax function Some "(Some %1)"
end
theory Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
end
theory bool.Bool
syntax function andb "(%1 && %2)"
syntax function orb "(%1 || %2)"
(* syntax function xorb "(xorb %1 %2)" *)
syntax function notb "(not %1)"
(* syntax function implb "(implb %1)" *)
end
theory list.List
syntax type list "%1 list"
syntax function Nil "[]"
syntax function Cons "(%1 :: %2)"
end
theory int.Int
syntax function zero "(Num.num_of_int 0)"
syntax function one "(Num.num_of_int 1)"
syntax function (+) "(Num.add_num %1 %2)"
syntax function (-) "(Num.sub_num %1 %2)"
syntax function (*) "(Num.mult_num %1 %2)"
syntax function (-_) "(Num.minus_num %1)"
syntax predicate (<=) "(Num.le_num %1 %2)"
syntax predicate (<) "(Num.lt_num %1 %2)"
syntax predicate (>=) "(Num.ge_num %1 %2)"
syntax predicate (>) "(Num.gt_num %1 %2)"
end
theory int.Abs
syntax function abs "(Num.abs_num %1)"
end
theory int.MinMax
syntax function min "(Num.min_num %1 %2)"
syntax function max "(Num.max_num %1 %2)"
end
(* Note: documentation for Num says ``Euclidean division'' but this is
rather a computer division *)
theory int.ComputerDivision
syntax function div "(Num.quo_num %1 %2)"
syntax function mod "(Num.mod_num %1 %2)"
end
......@@ -251,14 +251,11 @@ let get_syntax_map task =
let sm = Task.on_meta meta_remove_prop sm_add_pr sm task in
sm
(*
let get_syntax_map_of_theory theory =
let sm = Mid.empty in
let sm = Theory.on_meta meta_syntax_type sm_add_ts sm theory in
let sm = Theory.on_meta meta_syntax_logic sm_add_ls sm theory in
let sm = Theory.on_meta meta_remove_prop sm_add_pr sm theory in
sm
*)
let add_syntax_map td sm = match td.td_node with
| Meta (m, args) when meta_equal m meta_syntax_type -> sm_add_ts sm args
| Meta (m, args) when meta_equal m meta_syntax_logic -> sm_add_ls sm args
| Meta (m, args) when meta_equal m meta_remove_prop -> sm_add_pr sm args
| _ -> sm
let query_syntax sm id = Mid.find_opt id sm
......
......@@ -60,9 +60,8 @@ type syntax_map = string Mid.t
(* [syntax_map] maps the idents of removed props to "" *)
val get_syntax_map : task -> syntax_map
(*
val get_syntax_map_of_theory : theory -> syntax_map
*)
val add_syntax_map : tdecl -> syntax_map -> syntax_map
(* interprets a declaration as a syntax rule, if any *)
val query_syntax : syntax_map -> ident -> string option
......
......@@ -199,6 +199,10 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
drv_tag = !driver_tag
}
let syntax_map drv =
let addth _ (_,tds) acc = Stdecl.fold Printer.add_syntax_map tds acc in
Mid.fold addth drv.drv_meta Mid.empty
(** apply drivers *)
exception UnknownSpec of string
......
......@@ -84,3 +84,7 @@ val prove_task_prepared :
?inplace : bool ->
driver -> Task.task -> Call_provers.pre_prover_call
(** Traverse all metas from a driver *)
val syntax_map: driver -> Printer.syntax_map
......@@ -523,15 +523,16 @@ let do_local_theory env drv fname m (tname,_,t,glist) =
let extract_to ?fname th extract =
let dir = match !opt_output with Some dir -> dir | None -> assert false in
let fname = match fname, th.th_path with
let _fname = match fname, th.th_path with
| Some fname, _ ->
let fname = Filename.basename fname in
(try Filename.chop_extension fname with _ -> fname)
| None, [] -> assert false
| None, path -> List.hd (List.rev path)
in
let mname = fname ^ "__" ^ th.th_name.Ident.id_string ^ ".ml" in
let mname = String.uncapitalize mname in
(* FIXME: use fname to forge the OCaml filename *)
let mname = (* fname ^ "__" ^ *) th.th_name.Ident.id_string ^ ".ml" in
(* let mname = String.uncapitalize mname in *)
let file = Filename.concat dir mname in
let old =
if Sys.file_exists file then begin
......@@ -543,48 +544,50 @@ let extract_to ?fname th extract =
extract file ?old (formatter_of_out_channel cout);
close_out cout
let do_extract_theory _env ?fname tname th _glist =
let extract fname ?old _fmt = ignore (old);
Debug.dprintf Mlw_ocaml.debug "extract theory %s to file %s@." tname fname
let do_extract_theory env ?fname tname th =
let extract fname ?old fmt = ignore (old);
Debug.dprintf Mlw_ocaml.debug "extract theory %s to file %s@." tname fname;
Mlw_ocaml.extract_theory env ?old fmt th
in
extract_to ?fname th extract
let do_extract_module _env ?fname tname m _glist =
let extract fname ?old _fmt = ignore (old);
Debug.dprintf Mlw_ocaml.debug "extract module %s to file %s@." tname fname
let do_extract_module env ?fname tname m =
let extract fname ?old fmt = ignore (old);
Debug.dprintf Mlw_ocaml.debug "extract module %s to file %s@." tname fname;
Mlw_ocaml.extract_module env ?old fmt m
in
extract_to ?fname m.Mlw_module.mod_theory extract
let do_global_extract env (tname,p,t,glist) =
let do_global_extract env (tname,p,t,_) =
try
let lib = Mlw_main.library_of_env env in
let mm, thm = Env.read_lib_file lib p in
try
let m = Mstr.find t mm in
do_extract_module env tname m glist
do_extract_module env tname m
with Not_found ->
let th = Mstr.find t thm in
do_extract_theory env tname th glist
do_extract_theory env tname th
with Env.LibFileNotFound _ | Not_found -> try
let format = Util.def_option "why" !opt_parser in
let th = Env.read_theory ~format env p t in
do_extract_theory env tname th glist
do_extract_theory env tname th
with Env.LibFileNotFound _ | Env.TheoryNotFound _ ->
eprintf "Theory/module '%s' not found.@." tname;
exit 1
let do_extract_theory_from env fname m (tname,_,t,glist) =
let do_extract_theory_from env fname m (tname,_,t,_) =
let th = try Mstr.find t m with Not_found ->
eprintf "Theory '%s' not found in file '%s'.@." tname fname;
exit 1
in
do_extract_theory env ~fname tname th glist
do_extract_theory env ~fname tname th
let do_extract_module_from env fname mm thm (tname,_,t,glist) =
let do_extract_module_from env fname mm thm (tname,_,t,_) =
try
let m = Mstr.find t mm in do_extract_module env ~fname tname m glist
let m = Mstr.find t mm in do_extract_module env ~fname tname m
with Not_found -> try
let th = Mstr.find t thm in do_extract_theory env ~fname tname th glist
let th = Mstr.find t thm in do_extract_theory env ~fname tname th
with Not_found ->
eprintf "Theory/module '%s' not found in file '%s'.@." tname fname;
exit 1
......@@ -594,19 +597,17 @@ let do_local_extract env fname cin tlist =
let lib = Mlw_main.library_of_env env in
let mm, thm = Mlw_main.read_channel lib [] fname cin in
if Queue.is_empty tlist then begin
let glist = Queue.create () in
let do_m t m thm =
do_extract_module env ~fname t m glist; Mstr.remove t thm in
do_extract_module env ~fname t m; Mstr.remove t thm in
let thm = Mstr.fold do_m mm thm in
Mstr.iter (fun t th -> do_extract_theory env ~fname t th glist) thm
Mstr.iter (fun t th -> do_extract_theory env ~fname t th) thm
end else
Queue.iter (do_extract_module_from env fname mm thm) tlist
end else begin
let m = Env.read_channel ?format:!opt_parser env fname cin in
if Queue.is_empty tlist then
let glist = Queue.create () in
let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
let do_th _ (t,th) = do_extract_theory env ~fname t th glist in
let do_th _ (t,th) = do_extract_theory env ~fname t th in
Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
else
Queue.iter (do_extract_theory_from env fname m) tlist
......
......@@ -27,8 +27,10 @@ open Ty
open Term
open Decl
open Theory
open Printer
open Mlw_expr
open Mlw_decl
open Mlw_module
let debug =
Debug.register_info_flag
......@@ -70,6 +72,21 @@ let forget_all () =
forget_all tprinter;
forget_all pprinter
(* info *)
type info = {
info_syn: syntax_map;
current_theory: string;
known_map: Decl.known_map;
(* symbol_printers : (string * ident_printer) Mid.t; *)
}
let is_constructor info ls = match Mid.find ls.ls_name info.known_map with
| { d_node = Ddata dl } ->
let constr (_,csl) = List.exists (fun (cs,_) -> ls_equal cs ls) csl in
List.exists constr dl
| _ -> false
(* type variables always start with a quote *)
let print_tv fmt tv =
fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
......@@ -86,75 +103,73 @@ let print_ident fmt id =
let s = id_unique iprinter id in
fprintf fmt "%s" s
let extract_op ls =
let s = ls.ls_name.id_string in
let len = String.length s in
if len < 7 then None else
let inf = String.sub s 0 6 in
if inf = "infix " then Some (String.sub s 6 (len - 6)) else
let prf = String.sub s 0 7 in
if prf = "prefix " then Some (String.sub s 7 (len - 7)) else
None
(* pretty-print infix and prefix logic symbols *)
let extract_op ls =
let s = ls.ls_name.id_string in
let len = String.length s in
if len < 7 then None else
let inf = String.sub s 0 6 in
if inf = "infix " then Some (String.sub s 6 (len - 6)) else
let prf = String.sub s 0 7 in
if prf = "prefix " then Some (String.sub s 7 (len - 7)) else
None
let tight_op s = let c = String.sub s 0 1 in c = "!" || c = "?"
let escape_op s =
let s = Str.replace_first (Str.regexp "^\\*.") " \\0" s in
let s = Str.replace_first (Str.regexp ".\\*$") "\\0 " s in
s
let print_ls fmt ls =
if ls.ls_name.id_string = "mixfix []" then fprintf fmt "([])" else
if ls.ls_name.id_string = "mixfix [<-]" then fprintf fmt "([<-])" else
match extract_op ls with
| Some s -> fprintf fmt "(%s)" (escape_op s)
| None -> fprintf fmt "%s" (id_unique iprinter ls.ls_name)
let print_cs fmt ls =
let sanitizer = String.capitalize in
fprintf fmt "%s" (id_unique iprinter ~sanitizer ls.ls_name)
let print_ts fmt ts =
fprintf fmt "%s" (id_unique tprinter ts.ts_name)
let print_path = print_list dot pp_print_string
let print_qident ~sanitizer info fmt id =
let s = id_unique ~sanitizer iprinter id in
try
let _lp, t, _p = Theory.restore_path id in
(* fprintf fmt "%a/%s/%a" print_path lp t print_path p *)
if t = info.current_theory then
fprintf fmt "%s" s
else
fprintf fmt "%s.%s" t s
with Not_found ->
fprintf fmt "%s" s
let print_lident = print_qident ~sanitizer:String.uncapitalize
let print_uident = print_qident ~sanitizer:String.capitalize
let print_ls info fmt ls = print_lident info fmt ls.ls_name
let print_cs info fmt ls = print_uident info fmt ls.ls_name
let print_ts info fmt ts = print_lident info fmt ts.ts_name
let print_path_id fmt = function
| [], id -> print_ident fmt id
| p , id -> fprintf fmt "%a.%a" print_path p print_ident id
let print_theory_name fmt th = print_path_id fmt (th.th_path, th.th_name)
let print_module_name fmt m = print_theory_name fmt m.mod_theory
let to_be_implemented fmt s =
fprintf fmt "failwith \"to be implemented\" (* %s *)" s
let tbi s = "failwith \"to be implemented\" (* " ^^ s ^^ " *)"
(** Types *)
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
let star fmt () = fprintf fmt " *@ "
let rec print_ty_node inn fmt ty = match ty.ty_node with
let rec print_ty_node inn info fmt ty = match ty.ty_node with
| Tyvar v ->
print_tv fmt v
| Tyapp (ts, []) when is_ts_tuple ts ->
fprintf fmt "unit"
| Tyapp (ts, tl) when is_ts_tuple ts ->
fprintf fmt "(%a)" (print_list star (print_ty_node false)) tl
| Tyapp (ts, []) ->
print_ts fmt ts
fprintf fmt "(%a)" (print_list star (print_ty_node false info)) tl
| Tyapp (ts, tl) ->
fprintf fmt (protect_on inn "(%a)@ %a")
(print_list comma (print_ty_node false)) tl print_ts ts
begin match query_syntax info.info_syn ts.ts_name with
| Some s -> syntax_arguments s (print_ty_node true info) fmt tl
| None ->
begin match tl with
| [] ->
print_ts info fmt ts
| [ty] ->
fprintf fmt (protect_on inn "%a@ %a")
(print_ty_node true info) ty (print_ts info) ts
| _ ->
fprintf fmt (protect_on inn "(%a)@ %a")
(print_list comma (print_ty_node false info)) tl
(print_ts info) ts
end
end
let print_ty = print_ty_node false
let print_vsty fmt v =
fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
let print_vsty info fmt v =
fprintf fmt "%a:@ %a" print_vs v (print_ty info) v.vs_ty
let print_tv_arg = print_tv
let print_tv_args fmt = function
......@@ -162,41 +177,41 @@ let print_tv_args fmt = function
| [tv] -> fprintf fmt "%a@ " print_tv_arg tv
| tvl -> fprintf fmt "(%a)@ " (print_list comma print_tv_arg) tvl
let print_ty_arg fmt ty = fprintf fmt "%a" (print_ty_node true) ty
let print_vs_arg fmt vs = fprintf fmt "(%a)" print_vsty vs
let print_ty_arg info fmt ty = fprintf fmt "%a" (print_ty_node true info) ty
let print_vs_arg info fmt vs = fprintf fmt "(%a)" (print_vsty info) vs
(* FIXME: print projections! *)
let print_constr ty fmt (cs,_) =
let print_constr info ty fmt (cs,_) =
let ty_val = of_option cs.ls_value in
let m = ty_match Mtv.empty ty_val ty in
let tl = List.map (ty_inst m) cs.ls_args in
match tl with
| [] ->
fprintf fmt "@[<hov 4>| %a@]" print_cs cs
fprintf fmt "@[<hov 4>| %a@]" (print_cs info) cs
| _ ->
fprintf fmt "@[<hov 4>| %a of %a@]" print_cs cs
(print_list star print_ty_arg) tl
fprintf fmt "@[<hov 4>| %a of %a@]" (print_cs info) cs
(print_list star (print_ty_arg info)) tl
let print_type_decl fmt ts = match ts.ts_def with
let print_type_decl info fmt ts = match ts.ts_def with
| None ->
fprintf fmt "@[<hov 2>type %a%a@]"
print_tv_args ts.ts_args print_ts ts
print_tv_args ts.ts_args (print_ts info) ts
| Some ty ->
fprintf fmt "@[<hov 2>type %a%a =@ %a@]"
print_tv_args ts.ts_args print_ts ts print_ty ty
print_tv_args ts.ts_args (print_ts info) ts (print_ty info) ty
let print_type_decl fmt ts =
print_type_decl fmt ts; forget_tvs ()
let print_type_decl info fmt ts =
print_type_decl info fmt ts; forget_tvs ()
let print_data_decl fst fmt (ts,csl) =
let print_data_decl info fst fmt (ts,csl) =
let ty = ty_app ts (List.map ty_var ts.ts_args) in
fprintf fmt "@[<hov 2>%s %a%a =@\n@[<hov>%a@]@]"
(if fst then "type" else "and")
print_tv_args ts.ts_args print_ts ts
(print_list newline (print_constr ty)) csl
print_tv_args ts.ts_args (print_ts info) ts
(print_list newline (print_constr info ty)) csl
let print_data_decl first fmt d =
print_data_decl first fmt d; forget_tvs ()
let print_data_decl first info fmt d =
print_data_decl first info fmt d; forget_tvs ()
(** Inductive *)
......@@ -205,16 +220,16 @@ let name_args l =
let mk ty = incr r; create_vsymbol (id_fresh "x") ty in
List.map mk l
let print_ind_decl fst fmt (ps,_) =
let print_ind_decl info fst fmt (ps,_) =
let vars = name_args ps.ls_args in
fprintf fmt "@[<hov 2>%s %a %a : bool =@ @[<hov>%a@]@]"
(if fst then "let rec" else "and") print_ls ps
(print_list space print_vs_arg) vars
(if fst then "let rec" else "and") (print_ls info) ps
(print_list space (print_vs_arg info)) vars
to_be_implemented "inductive";
forget_vars vars
let print_ind_decl first fmt d =
print_ind_decl first fmt d; forget_tvs ()
let print_ind_decl first info fmt d =
print_ind_decl first info fmt d; forget_tvs ()
(** Functions/Predicates *)
......@@ -242,7 +257,14 @@ let rec is_exec_term t = match t.t_node with
and is_exec_branch b =
let _, t = t_open_branch b in is_exec_term t
let print_const = Pretty.print_const
let print_const fmt = function
| ConstInt (IConstDecimal s) -> fprintf fmt "(Num.num_of_string \"%s\")" s
| ConstInt (IConstHexa s) -> fprintf fmt (tbi "0x%s") s
| ConstInt (IConstOctal s) -> fprintf fmt (tbi "0o%s") s
| ConstInt (IConstBinary s) -> fprintf fmt (tbi "0b%s") s
| ConstReal (RConstDecimal (i,f,None)) -> fprintf fmt (tbi "%s.%s") i f
| ConstReal (RConstDecimal (i,f,Some e)) -> fprintf fmt (tbi "%s.%se%s") i f e
| ConstReal (RConstHexa (i,f,e)) -> fprintf fmt (tbi "0x%s.%sp%s") i f e
(* can the type of a value be derived from the type of the arguments? *)
let unambig_fs fs =
......@@ -259,25 +281,27 @@ let unambig_fs fs =
(** Patterns, terms, and formulas *)
let rec print_pat_node pri fmt p = match p.pat_node with
let rec print_pat_node pri info fmt p = match p.pat_node with
| Term.Pwild ->
fprintf fmt "_"
| Term.Pvar v ->
print_vs fmt v
| Term.Pas (p, v) ->
fprintf fmt (protect_on (pri > 1) "%a as %a")
(print_pat_node 1) p print_vs v
(print_pat_node 1 info) p print_vs v
| Term.Por (p, q) ->
fprintf fmt (protect_on (pri > 0) "%a | %a")
(print_pat_node 0) p (print_pat_node 0) q
(print_pat_node 0 info) p (print_pat_node 0 info) q
| Term.Papp (cs, pl) when is_fs_tuple cs ->
fprintf fmt "(%a)"
(print_list comma (print_pat_node 1)) pl
| Term.Papp (cs, []) ->
print_cs fmt cs
(print_list comma (print_pat_node 1 info)) pl
| Term.Papp (cs, pl) ->
fprintf fmt (protect_on (pri > 1) "%a@ (%a)")
print_cs cs (print_list comma (print_pat_node 2)) pl
begin match query_syntax info.info_syn cs.ls_name with
| Some s -> syntax_arguments s (print_pat_node 0 info) fmt pl
| None when pl = [] -> print_cs info fmt cs
| _ -> fprintf fmt (protect_on (pri > 1) "%a@ (%a)")
(print_cs info) cs (print_list comma (print_pat_node 2 info)) pl
end
let print_pat = print_pat_node 0
......@@ -293,57 +317,54 @@ let prio_binop = function
| Timplies -> 1
| Tiff -> 1
let rec print_term fmt t =
print_lterm 0 fmt t
and print_lterm pri fmt t =
print_tnode pri fmt t
and print_app pri ls fmt tl = match extract_op ls, tl with
| _, [] ->
print_ls fmt ls
| Some s, [t1] when tight_op s ->
fprintf fmt (protect_on (pri > 7) "%s%a")
s (print_lterm 7) t1
| Some s, [t1] ->
fprintf fmt (protect_on (pri > 4) "%s %a")
s (print_lterm 5) t1
| Some s, [t1;t2] ->
fprintf fmt (protect_on (pri > 4) "@[<hov 1>%a %s@ %a@]")
(print_lterm 5) t1 s (print_lterm 5) t2
| _, [t1;t2] when ls.ls_name.id_string = "mixfix []" ->
fprintf fmt (protect_on (pri > 6) "%a[%a]")
(print_lterm 6) t1 print_term t2
| _, [t1;t2;t3] when ls.ls_name.id_string = "mixfix [<-]" ->
fprintf fmt (protect_on (pri > 6) "%a[%a <- %a]")
(print_lterm 6) t1 (print_lterm 5) t2 (print_lterm 5) t3
| _, tl ->
let rec print_term info fmt t =
print_lterm 0 info fmt t
and print_lterm pri info fmt t =
print_tnode pri info fmt t
and print_app pri ls info fmt tl =
let isc = is_constructor info ls in
let print = if isc then print_cs else print_ls in
match tl with
| [] ->
print info fmt ls
| [t1] ->
fprintf fmt (protect_on (pri > 4) "%a %a")
(print info) ls (print_lterm 5 info) t1
| tl when isc ->
fprintf fmt (protect_on (pri > 5) "@[<hov 1>%a@ (%a)@]")
(print_cs info) ls (print_list comma (print_lterm 6 info)) tl
| tl ->
fprintf fmt (protect_on (pri > 5) "@[<hov 1>%a@ %a@]")
print_ls ls (print_list space (print_lterm 6)) tl
(print_ls info) ls (print_list space (print_lterm 6 info)) tl
and print_tnode pri fmt t = match t.t_node with
and print_tnode pri info fmt t = match t.t_node with
| Tvar v ->
print_vs fmt v
| Tconst c ->
print_const fmt c
| Tapp (fs, tl) when is_fs_tuple fs ->
fprintf fmt "(%a)" (print_list comma print_term) tl
| Tapp (fs, tl) when unambig_fs fs ->
print_app pri fs fmt tl
fprintf fmt "(%a)" (print_list comma (print_term info)) tl
| Tapp (fs, tl) ->
fprintf fmt (protect_on (pri > 0) "%a:%a")
(print_app 5 fs) tl print_ty (t_type t)
begin match query_syntax info.info_syn fs.ls_name with
| Some s -> syntax_arguments s (print_term info) fmt tl
| None when unambig_fs fs -> print_app pri fs info fmt tl