Commit 3a4ee4f1 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

ITP: make tables for printing and parsing

parent ab636c11
......@@ -51,6 +51,8 @@ val find_qualid :
type global_vs = Ptree.qualid -> vsymbol option
val type_term_in_namespace : namespace -> global_vs -> Ptree.term -> term
val type_term : theory_uc -> global_vs -> Ptree.term -> term
val type_fmla : theory_uc -> global_vs -> Ptree.term -> term
......
......@@ -20,159 +20,13 @@ open Decl
open Printer
open Theory
let iprinter,aprinter,tprinter,pprinter,fresh_printer =
let bl = ["theory"; "type"; "function"; "predicate"; "inductive";
"axiom"; "lemma"; "goal"; "use"; "clone"; "prop"; "meta";
"namespace"; "import"; "export"; "end";
"forall"; "exists"; "not"; "true"; "false"; "if"; "then"; "else";
"let"; "in"; "match"; "with"; "as"; "epsilon" ] in
let isanitize = sanitizer char_to_alpha char_to_alnumus in
let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
create_ident_printer bl ~sanitizer:isanitize,
create_ident_printer bl ~sanitizer:lsanitize,
create_ident_printer bl ~sanitizer:lsanitize,
create_ident_printer bl ~sanitizer:isanitize,
fun () -> create_ident_printer bl ~sanitizer:isanitize
open Stdlib
type name_tables = {
namespace : Theory.namespace;
unique_names : string Mid.t;
th: theory_uc;
}
(* Use symb to encapsulate ids into correct categories of symbols *)
type symb =
| Ts of tysymbol
| Ls of lsymbol
| Pr of prsymbol
(* [add_unsafe s id tables] Add (s, id) to tables without any checking. *)
let add_unsafe (s: string) (id: symb) (tables: name_tables) : name_tables =
match id with
| Ts ty ->
{namespace = {tables.namespace with ns_ts = Mstr.add s ty tables.namespace.ns_ts};
unique_names = Mid.add ty.ts_name s tables.unique_names;
th = tables.th}
| Ls ls ->
{namespace = {tables.namespace with ns_ls = Mstr.add s ls tables.namespace.ns_ls};
unique_names = Mid.add ls.ls_name s tables.unique_names;
th = tables.th}
| Pr pr ->
{namespace = {tables.namespace with ns_pr = Mstr.add s pr tables.namespace.ns_pr};
unique_names = Mid.add pr.pr_name s tables.unique_names;
th = tables.th}
(* Adds symbols that are introduced to a constrictor *)
let constructor_add (cl: constructor list) (printer: ident_printer) tables : name_tables =
List.fold_left
(fun tables (c: constructor) ->
let id = (fst c).ls_name in
let s = id_unique printer id in
add_unsafe s (Ls (fst c)) tables)
tables
cl
(* Add symbols that are introduced by an inductive *)
let ind_decl_add il printer tables =
List.fold_left
(fun tables ((pr, t): prsymbol * term) ->
let id = pr.pr_name in
let s = id_unique printer id in
add_unsafe s (Pr pr) tables)
il
tables
(* [add d printer tables] Adds all new declaration of symbol inside d to tables.
It uses printer to give them a unique name and also register these new names in printer *)
let add (d: decl) (printer: ident_printer) (tables: name_tables): name_tables =
let tables = {tables with th = Theory.add_decl ~warn:false tables.th d} in
match d.d_node with
| Dtype ty ->
(* only current symbol is new in the declaration (see create_ty_decl) *)
let id = ty.ts_name in
let s = id_unique printer id in
add_unsafe s (Ts ty) tables
| Ddata dl ->
(* first part is new. Also only first part of each constructor seem new
(see create_data_decl) *)
List.fold_left
(fun tables (dd: data_decl) ->
let id = (fst dd).ts_name in
let s = id_unique printer id in
let tables = add_unsafe s (Ts (fst dd)) tables in
constructor_add (snd dd) printer tables)
tables
dl
| Dparam ls ->
(* Only one lsymbol which is new *)
let id = ls.ls_name in
let s = id_unique printer id in
add_unsafe s (Ls ls) tables
| Dlogic lsd ->
(* Only first part of logic_decl is new (see create_logic) *)
List.fold_left
(fun tables (l: logic_decl) ->
let id = (fst l).ls_name in
let s = id_unique printer id in
add_unsafe s (Ls (fst l)) tables)
tables
lsd
| Dind (is, il) ->
(* Every symbol is new except symbol inside terms (see create_ind_decl) *)
List.fold_left
(fun tables (ind: ind_decl) ->
let id = (fst ind).ls_name in
let s = id_unique printer id in
let tables = add_unsafe s (Ls (fst ind)) tables in
ind_decl_add tables printer (snd ind))
tables
il
| Dprop (_, pr, _) ->
(* Only pr is new in Dprop (see create_prop_decl) *)
let id = pr.pr_name in
let s = id_unique printer id in
add_unsafe s (Pr pr) tables
let build_name_tables task : name_tables =
(*
TODO:
- simply use [km = Task.task_known task] as the set of identifiers
to insert in the tables
- only one printer (do not attempt te rebuild qualified idents)
- use syntax_map from why3_itp driver
- to build the namespace, do a match on the decl associated with the id
in [km]
| Dtype -> tysymbol
| Ddata | Dparam | Dlogic | Dind -> lsymbol
| Dprop -> prsymbol
TODO: use the result of this function in
- a new variant of a printer in this file
- use the namespace to type the terms
(change the code in parser/typing.ml to use namespace
instead of theory_uc)
*)
let tables = {namespace = empty_ns; unique_names = Mid.empty; th = Theory.create_theory (Ident.id_fresh "dummy")} in
let km = Task.task_known task in
let pr = fresh_printer () in
Mid.fold
(fun _id d tables ->
(* TODO optimization. We may check if id is already there to not explore twice the same
declaration ? *)
add d pr tables)
km
tables
open Args_wrapper
let id_unique tables id =
try
Mid.find id tables.unique_names
with Not_found ->
(Format.printf "Table is not complete %s !@." id.id_string; id.id_string) (* Everything must be here *)
id_unique tables.printer id
(*
let forget_tvs () =
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* 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
......@@ -2,6 +2,158 @@ open Task
open Ty
open Term
open Trans
open Ident
open Theory
open Decl
let fresh_printer =
let bl = ["theory"; "type"; "function"; "predicate"; "inductive";
"axiom"; "lemma"; "goal"; "use"; "clone"; "prop"; "meta";
"namespace"; "import"; "export"; "end";
"forall"; "exists"; "not"; "true"; "false"; "if"; "then"; "else";
"let"; "in"; "match"; "with"; "as"; "epsilon" ] in
let isanitize = sanitizer char_to_alpha char_to_alnumus in
fun () -> create_ident_printer bl ~sanitizer:isanitize
open Stdlib
type name_tables = {
namespace : namespace;
unique_names : string Mid.t;
printer : ident_printer;
}
(* Use symb to encapsulate ids into correct categories of symbols *)
type symb =
| Ts of tysymbol
| Ls of lsymbol
| Pr of prsymbol
(* [add_unsafe s id tables] Add (s, id) to tables without any checking. *)
let add_unsafe (s: string) (id: symb) (tables: name_tables) : name_tables =
match id with
| Ts ty ->
{tables with
namespace = {tables.namespace with ns_ts = Mstr.add s ty tables.namespace.ns_ts};
unique_names = Mid.add ty.ts_name s tables.unique_names;
}
| Ls ls ->
{tables with
namespace = {tables.namespace with ns_ls = Mstr.add s ls tables.namespace.ns_ls};
unique_names = Mid.add ls.ls_name s tables.unique_names}
| Pr pr ->
{tables with
namespace = {tables.namespace with ns_pr = Mstr.add s pr tables.namespace.ns_pr};
unique_names = Mid.add pr.pr_name s tables.unique_names}
(* Adds symbols that are introduced to a constructor *)
let constructor_add (cl: constructor list) tables : name_tables =
(* TODO: add also the projections *)
List.fold_left
(fun tables (c: constructor) ->
let id = (fst c).ls_name in
let s = id_unique tables.printer id in
add_unsafe s (Ls (fst c)) tables)
tables
cl
(* Add symbols that are introduced by an inductive *)
let ind_decl_add il tables =
List.fold_left
(fun tables ((pr, _): prsymbol * term) ->
let id = pr.pr_name in
let s = id_unique tables.printer id in
add_unsafe s (Pr pr) tables)
il
tables
(* [add d printer tables] Adds all new declaration of symbol inside d to tables.
It uses printer to give them a unique name and also register these new names in printer *)
let add (d: decl) (tables: name_tables): name_tables =
match d.d_node with
| Dtype ty ->
(* only current symbol is new in the declaration (see create_ty_decl) *)
let id = ty.ts_name in
let s = id_unique tables.printer id in
add_unsafe s (Ts ty) tables
| Ddata dl ->
(* first part is new. Also only first part of each constructor seem new
(see create_data_decl) *)
List.fold_left
(fun tables (dd: data_decl) ->
let id = (fst dd).ts_name in
let s = id_unique tables.printer id in
let tables = add_unsafe s (Ts (fst dd)) tables in
constructor_add (snd dd) tables)
tables
dl
| Dparam ls ->
(* Only one lsymbol which is new *)
let id = ls.ls_name in
let s = id_unique tables.printer id in
add_unsafe s (Ls ls) tables
| Dlogic lsd ->
(* Only first part of logic_decl is new (see create_logic) *)
List.fold_left
(fun tables ((ls,_): logic_decl) ->
let id = ls.ls_name in
let s = id_unique tables.printer id in
add_unsafe s (Ls ls) tables)
tables
lsd
| Dind (_is, il) ->
(* Every symbol is new except symbol inside terms (see create_ind_decl) *)
List.fold_left
(fun tables ((ls,ind): ind_decl) ->
let id = ls.ls_name in
let s = id_unique tables.printer id in
let tables = add_unsafe s (Ls ls) tables in
ind_decl_add tables ind)
tables
il
| Dprop (_, pr, _) ->
(* Only pr is new in Dprop (see create_prop_decl) *)
let id = pr.pr_name in
let s = id_unique tables.printer id in
add_unsafe s (Pr pr) tables
let build_name_tables task : name_tables =
(*
TODO:
- simply use [km = Task.task_known task] as the set of identifiers
to insert in the tables
- only one printer (do not attempt te rebuild qualified idents)
- use syntax_map from why3_itp driver
- to build the namespace, do a match on the decl associated with the id
in [km]
| Dtype -> tysymbol
| Ddata | Dparam | Dlogic | Dind -> lsymbol
| Dprop -> prsymbol
TODO: use the result of this function in
- a new variant of a printer in this file
- use the namespace to type the terms
(change the code in parser/typing.ml to use namespace
instead of theory_uc)
*)
let pr = fresh_printer () in
let tables = {
namespace = empty_ns; unique_names = Mid.empty ; printer = pr } in
let km = Task.task_known task in
Mid.fold
(fun _id d tables ->
(* TODO optimization. We may check if id is already there to not explore twice the same
declaration ? *)
add d tables)
km
tables
(************* wrapper *************)
type _ trans_typ =
| Ttrans : (task -> task list) trans_typ
......@@ -14,11 +166,13 @@ type _ 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
let tables = build_name_tables task in
failwith "todo"
(* 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 =
......
open Ident
open Theory
open Task
(** Pre-processing of tasks, to build unique names for all declared
identifiers of a task.*)
type name_tables = {
namespace : Theory.namespace;
unique_names : string Mid.t;
printer : ident_printer;
}
val build_name_tables : Task.task -> name_tables
type _ trans_typ =
| Ttrans : (task -> task list) trans_typ
| Tint : 'a trans_typ -> (int -> 'a) trans_typ
......@@ -10,4 +23,8 @@ type _ trans_typ =
| Tterm : 'a trans_typ -> (Term.term -> 'a) trans_typ
| Tformula : 'a trans_typ -> (Term.term -> 'a) trans_typ
val wrap : 'a trans_typ -> 'a -> Trans.trans_with_args
(** wrap arguments of transformations, turning string arguments into
arguments of proper types. arguments of type term of formula are
parsed and typed, name resolution using the given name_tables. *)
val wrap : (* name_tables -> *) 'a trans_typ -> 'a -> Trans.trans_with_args
......@@ -570,10 +570,16 @@ 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));
"test", "test register known_map",
(fun _ _ ->
try
let id = nearest_goal () in
let task = get_task cont.controller_session id in
let _ = Args_wrapper.build_name_tables task in
()
with e when not (Debug.test_flag Debug.stack_trace) ->
Format.eprintf
"@[Exception raised :@ %a@.@]" Exn_printer.exn_printer e);
"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