Commit ab636c11 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

First attempt at printer

parent 8ed16ca6
This diff is collapsed.
......@@ -8,4 +8,20 @@
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open Format
open Pp
open Ident
open Ty
open Term
open Decl
open Printer
open Theory
open Stdlib
type name_tables = {
namespace : Theory.namespace;
unique_names : string Mid.t;
th: theory_uc;
}
val build_name_tables : Task.task -> name_tables
......@@ -12,6 +12,14 @@ type _ trans_typ =
| Tterm : 'a trans_typ -> (term -> 'a) trans_typ
| Tformula : 'a trans_typ -> (term -> 'a) trans_typ
let type_ptree ~as_fmla t task =
(* Simply build th_uc at the same time by rebuilding the declarations with unique names ??? *)
let tables = Why3printer.build_name_tables task in
let th_uc = tables.th in
if as_fmla
then Typing.type_fmla th_uc (fun _ -> None) t
else Typing.type_term th_uc (fun _ -> None) t
(*** term argument parsed in the context of the task ***)
let type_ptree ~as_fmla t task =
let used_ths = Task.used_theories task in
......
......@@ -421,14 +421,20 @@ let print_position (s: session) (cursor: proof_zipper) fmt: unit =
let print_position_p s cursor fmt _ = print_position s cursor fmt
let task_driver =
let d = Filename.concat (Whyconf.datadir main)
(Filename.concat "drivers" "why3_itp.drv")
in
Driver.load_driver env d []
(* Print current goal or nearest next goal if we are not on a goal *)
let test_print_goal fmt _args =
(* temporary : get the first goal *)
let id = nearest_goal () in
let task = Session_itp.get_task cont.Controller_itp.controller_session id in
fprintf fmt "@[====================== Task =====================@\n%a@]@."
Pretty.print_task
(* (Driver.print_task ~cntexample:false task_driver) *)
(*Pretty.print_task*)
(Driver.print_task ~cntexample:false task_driver)
task
(* Execute f and then print the goal *)
......@@ -464,12 +470,6 @@ let apply_transform fmt args =
(*******)
let task_driver =
let d = Filename.concat (Whyconf.datadir main)
(Filename.concat "drivers" "why3_itp.drv")
in
Driver.load_driver env d []
let test_save_session _fmt args =
match args with
| file :: _ ->
......@@ -570,6 +570,10 @@ let commands =
"gr", "get to the goal right", then_print (move_to_goal_ret_p zipper_right);
"gl", "get to the goal left", then_print (move_to_goal_ret_p zipper_left);
"pcur", "print tree rooted at current position", (print_position_p cont.controller_session zipper);
"test", "test register known_map", (fun _ _ -> ignore (
let id = nearest_goal () in
let task = get_task cont.controller_session id in
Why3printer.build_name_tables task));
"zu", "navigation up, parent", (fun _ _ -> ignore (zipper_up ()));
"zd", "navigation down, left child", (fun _ _ -> ignore (zipper_down ()));
"zl", "navigation left, left brother", (fun _ _ -> ignore (zipper_left ()));
......
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