Commit 357c21dd authored by Andrei Paskevich's avatar Andrei Paskevich

- restore the interface and implementation of Pretty

- copy the code of Pretty to Why3 to prepare it for Driver
- move goal_of_ctxt to Transform, where it belongs 
- comment out the unused "extract_goals" in Transform
- comment out the debugging printing in Theory, use Pretty
- in use_export, put the Duse declaration after the copied
  declarations, not before
parent d49c181b
...@@ -68,9 +68,10 @@ let id_derive_long sh ln id = create_ident sh ln (Derived id) ...@@ -68,9 +68,10 @@ let id_derive_long sh ln id = create_ident sh ln (Derived id)
let id_clone id = create_ident id.id_short id.id_long (Derived id) let id_clone id = create_ident id.id_short id.id_long (Derived id)
let id_dup id = { id with id_tag = -1 } let id_dup id = { id with id_tag = -1 }
(* Utils *) let rec id_derived_from i1 i2 = i1 == i2 ||
let rec derived_from i1 i2 = (match i1.id_origin with
i1 == i2 || (match i1.id_origin with Derived i3 -> derived_from i1 i2 | _ -> false) | Derived i3 -> id_derived_from i3 i2
| _ -> false)
(** Unique names for pretty printing *) (** Unique names for pretty printing *)
......
...@@ -59,10 +59,8 @@ val id_clone : ident -> preid ...@@ -59,10 +59,8 @@ val id_clone : ident -> preid
(* create a duplicate pre-ident *) (* create a duplicate pre-ident *)
val id_dup : ident -> preid val id_dup : ident -> preid
(* Utils *) (* id_derived_from i1 i2 <=> i1 is derived from i2 *)
val derived_from : ident -> ident -> bool val id_derived_from : ident -> ident -> bool
(* derived_from i1 i2 is true if i1 is derived from i2 *)
(** Unique persistent names for pretty printing *) (** Unique persistent names for pretty printing *)
...@@ -79,7 +77,8 @@ val id_unique : ...@@ -79,7 +77,8 @@ val id_unique :
(* forget an ident *) (* forget an ident *)
val forget_id : ident_printer -> ident -> unit val forget_id : ident_printer -> ident -> unit
(* forget all the idents *)
(* forget all idents *)
val forget_all : ident_printer -> unit val forget_all : ident_printer -> unit
(* generic sanitizer taking a separate encoder for the first letter *) (* generic sanitizer taking a separate encoder for the first letter *)
......
This diff is collapsed.
...@@ -23,55 +23,36 @@ open Ty ...@@ -23,55 +23,36 @@ open Ty
open Term open Term
open Theory open Theory
val printer : unit -> ident_printer val forget_all : unit -> unit (* flush id_unique *)
val forget_tvs : unit -> unit (* flush id_unique for type vars *)
val forget_var : vsymbol -> unit (* flush id_unique for a variable *)
val forget_tvs : ?printer:ident_printer -> unit -> unit val print_tv : formatter -> tvsymbol -> unit (* type variable *)
(* flush id_unique for type vars *) val print_vs : formatter -> vsymbol -> unit (* variable *)
val forget_var : ?printer:ident_printer -> vsymbol -> unit
(* flush id_unique for a variable *) val print_ts : formatter -> tysymbol -> unit (* type symbol *)
val print_ls : formatter -> lsymbol -> unit (* logic symbol *)
val print_pr : formatter -> prop -> unit (* proposition name *)
val print_ty : formatter -> ty -> unit (* type *)
val print_vsty : formatter -> vsymbol -> unit (* variable : type *)
val print_id : ?printer:ident_printer -> (* ident *)
formatter -> ident -> unit
val print_tv : ?printer:ident_printer -> (* type variable *)
formatter -> tvsymbol -> unit
val print_ts : ?printer:ident_printer -> (* type symbol *)
formatter -> tysymbol -> unit
val print_ty : ?printer:ident_printer -> (* type *)
formatter -> ty -> unit
val print_vs : ?printer:ident_printer -> (* variable *)
formatter -> vsymbol -> unit
val print_vsty : ?printer:ident_printer -> (* variable : type *)
formatter -> vsymbol -> unit
val print_ls : ?printer:ident_printer -> (* logic symbol *)
formatter -> lsymbol -> unit
val print_const : formatter -> constant -> unit (* int/real constant *) val print_const : formatter -> constant -> unit (* int/real constant *)
val print_pat : ?printer:ident_printer -> (* pattern *) val print_pat : formatter -> pattern -> unit (* pattern *)
formatter -> pattern -> unit val print_term : formatter -> term -> unit (* term *)
val print_term : ?printer:ident_printer -> (* term *) val print_fmla : formatter -> fmla -> unit (* formula *)
formatter -> term -> unit
val print_fmla : ?printer:ident_printer -> (* formula *)
formatter -> fmla -> unit
val print_type_decl : ?printer:ident_printer -> val print_type_decl : formatter -> ty_decl -> unit
formatter -> ty_decl -> unit val print_logic_decl : formatter -> logic_decl -> unit
val print_logic_decl : ?printer:ident_printer -> val print_ind_decl : formatter -> ind_decl -> unit
formatter -> logic_decl -> unit
val print_ind_decl : ?printer:ident_printer ->
formatter -> ind_decl -> unit
val print_pkind : formatter -> prop_kind -> unit val print_pkind : formatter -> prop_kind -> unit
val print_prop : ?printer:ident_printer -> val print_prop : formatter -> prop -> unit
formatter -> prop -> unit
val print_decl : ?printer:ident_printer -> val print_decl : formatter -> decl -> unit
formatter -> decl -> unit val print_decls : formatter -> decl list -> unit
val print_decls : ?printer:ident_printer -> val print_context : formatter -> context -> unit
formatter -> decl list -> unit val print_theory : formatter -> theory -> unit
val print_context : ?printer:ident_printer ->
formatter -> context -> unit
val print_theory : ?printer:ident_printer ->
formatter -> theory -> unit
val print_named_context : ?printer:ident_printer -> val print_named_context : formatter -> string -> context -> unit
formatter -> string -> context -> unit
...@@ -314,7 +314,7 @@ let create_logic_decl ldl = ...@@ -314,7 +314,7 @@ let create_logic_decl ldl =
module Ctxt = struct module Ctxt = struct
type t = context type t = context
let equal a b = let equal a b =
a.ctxt_env == b.ctxt_env && a.ctxt_env == b.ctxt_env &&
a.ctxt_decl == b.ctxt_decl && a.ctxt_decl == b.ctxt_decl &&
match a.ctxt_prev, b.ctxt_prev with match a.ctxt_prev, b.ctxt_prev with
...@@ -376,14 +376,14 @@ let builtin_theory env = ...@@ -376,14 +376,14 @@ let builtin_theory env =
(** Environments *) (** Environments *)
let create_env = let create_env =
let r = ref 0 in let r = ref 0 in
fun retrieve -> fun retrieve ->
incr r; incr r;
let env = let env = {
{ env_retrieve = retrieve; env_retrieve = retrieve;
env_memo = Hashtbl.create 17; env_memo = Hashtbl.create 17;
env_tag = !r; } env_tag = !r }
in in
let builtin = builtin_theory env in let builtin = builtin_theory env in
let m = Mnm.add builtin.th_name.id_short builtin Mnm.empty in let m = Mnm.add builtin.th_name.id_short builtin Mnm.empty in
...@@ -393,7 +393,7 @@ let create_env = ...@@ -393,7 +393,7 @@ let create_env =
exception TheoryNotFound of string list * string exception TheoryNotFound of string list * string
let find_theory env sl s = let find_theory env sl s =
let m = let m =
try try
Hashtbl.find env.env_memo sl Hashtbl.find env.env_memo sl
with Not_found -> with Not_found ->
...@@ -402,8 +402,8 @@ let find_theory env sl s = ...@@ -402,8 +402,8 @@ let find_theory env sl s =
Hashtbl.replace env.env_memo sl m; Hashtbl.replace env.env_memo sl m;
m m
in in
try Mnm.find s m try Mnm.find s m
with Not_found -> raise (TheoryNotFound (sl, s)) with Not_found -> raise (TheoryNotFound (sl, s))
(** Context constructors and utilities *) (** Context constructors and utilities *)
...@@ -564,8 +564,7 @@ module Context = struct ...@@ -564,8 +564,7 @@ module Context = struct
let rec use_export hide ctxt th = let rec use_export hide ctxt th =
let d = create_use_decl th in let d = create_use_decl th in
try try
let kn = add_known th.th_name d ctxt.ctxt_known in ignore (add_known th.th_name d ctxt.ctxt_known);
let ctxt = push_decl ctxt kn d in
let add_decl ctxt d = match d.d_node with let add_decl ctxt d = match d.d_node with
| Duse th -> use_export true ctxt th | Duse th -> use_export true ctxt th
| Dprop (Pgoal,_) when hide -> ctxt | Dprop (Pgoal,_) when hide -> ctxt
...@@ -574,7 +573,9 @@ module Context = struct ...@@ -574,7 +573,9 @@ module Context = struct
| _ -> add_decl ctxt d | _ -> add_decl ctxt d
in in
let decls = get_decls th.th_ctxt in let decls = get_decls th.th_ctxt in
List.fold_left add_decl ctxt decls let ctxt = List.fold_left add_decl ctxt decls in
let kn = add_known th.th_name d ctxt.ctxt_known in
push_decl ctxt kn d
with DejaVu -> with DejaVu ->
ctxt ctxt
...@@ -819,7 +820,7 @@ module TheoryUC = struct ...@@ -819,7 +820,7 @@ module TheoryUC = struct
(* Manage theories *) (* Manage theories *)
let create_theory env n = let create_theory env n =
let builtin = find_theory env [] builtin_name in let builtin = find_theory env [] builtin_name in
{ uc_name = n; { uc_name = n;
uc_ctxt = builtin.th_ctxt; uc_ctxt = builtin.th_ctxt;
...@@ -933,6 +934,7 @@ module TheoryUC = struct ...@@ -933,6 +934,7 @@ module TheoryUC = struct
end end
(*
(** Debugging *) (** Debugging *)
let print_ident = let print_ident =
...@@ -969,3 +971,4 @@ let goal_of_ctxt ctxt = ...@@ -969,3 +971,4 @@ let goal_of_ctxt ctxt =
match ctxt.ctxt_decl.d_node with match ctxt.ctxt_decl.d_node with
| Dprop (Pgoal,pr) -> pr | Dprop (Pgoal,pr) -> pr
| _ -> raise NotGoalContext | _ -> raise NotGoalContext
*)
...@@ -212,6 +212,7 @@ end ...@@ -212,6 +212,7 @@ end
val builtin_name : string val builtin_name : string
(*
(** Debugging *) (** Debugging *)
val print_ident : Format.formatter -> ident -> unit val print_ident : Format.formatter -> ident -> unit
...@@ -222,6 +223,7 @@ val print_th : Format.formatter -> theory -> unit ...@@ -222,6 +223,7 @@ val print_th : Format.formatter -> theory -> unit
(* Utils *) (* Utils *)
exception NotGoalContext exception NotGoalContext
val goal_of_ctxt : context -> prop val goal_of_ctxt : context -> prop
(* goal_of_ctxt ctxt return the goal of a goal context (* goal_of_ctxt ctxt return the goal of a goal context
the ctxt must end with a goal.*) the ctxt must end with a goal.*)
*)
...@@ -20,6 +20,7 @@ ...@@ -20,6 +20,7 @@
open Format open Format
open Theory open Theory
open Driver open Driver
open Transform
let files = Queue.create () let files = Queue.create ()
let parse_only = ref false let parse_only = ref false
...@@ -183,7 +184,7 @@ let do_file env drv filename_printer file = ...@@ -183,7 +184,7 @@ let do_file env drv filename_printer file =
List.filter (fun (_,ctxt) -> List.filter (fun (_,ctxt) ->
match ctxt.ctxt_decl.d_node with match ctxt.ctxt_decl.d_node with
| Dprop (_,{pr_name = pr_name}) -> | Dprop (_,{pr_name = pr_name}) ->
Ident.derived_from pr_name pr.pr_name Ident.id_derived_from pr_name pr.pr_name
| _ -> assert false) goals in | _ -> assert false) goals in
(* Apply transformations *) (* Apply transformations *)
let goals = List.map let goals = List.map
......
...@@ -134,12 +134,13 @@ and driver = { ...@@ -134,12 +134,13 @@ and driver = {
drv_with_ctxt : translation Hid.t; drv_with_ctxt : translation Hid.t;
} }
(*
let print_driver fmt driver = let print_driver fmt driver =
printf "drv_theory %a@\n" printf "drv_theory %a@\n"
(Pp.print_iter2 Hid.iter Pp.semi Pp.comma print_ident (Pp.print_iter2 Hid.iter Pp.semi Pp.comma print_ident
(Pp.print_pair print_translation print_translation)) (Pp.print_pair print_translation print_translation))
driver.drv_theory driver.drv_theory
*)
(** registering transformation *) (** registering transformation *)
...@@ -373,7 +374,7 @@ let filename_of_goal drv ident_printer filename theory_name ctxt = ...@@ -373,7 +374,7 @@ let filename_of_goal drv ident_printer filename theory_name ctxt =
match drv.drv_filename with match drv.drv_filename with
| None -> errorm "no filename syntax given" | None -> errorm "no filename syntax given"
| Some f -> | Some f ->
let pr_name = (goal_of_ctxt ctxt).pr_name in let pr_name = (Transform.goal_of_ctxt ctxt).pr_name in
let repl_fun s = let repl_fun s =
let i = matched_group 1 s in let i = matched_group 1 s in
match i with match i with
......
This diff is collapsed.
...@@ -16,4 +16,3 @@ ...@@ -16,4 +16,3 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *) (* *)
(**************************************************************************) (**************************************************************************)
(* test file *) (* test file *)
theory ThA
type test
logic test (test : test) : test
goal Test : forall test : test . forall test : test . test(test) <> test
end
theory Test theory Test
use import prelude.Int use import prelude.Int
logic id(x: int) : int = x logic id(x: int) : int = x
......
...@@ -33,8 +33,6 @@ let conv_res f c = ...@@ -33,8 +33,6 @@ let conv_res f c =
{ all = (fun x -> c (f.all x)); { all = (fun x -> c (f.all x));
clear = f.clear; } clear = f.clear; }
exception CompositionOfIncompatibleTranformation
let compose f g = let compose f g =
{ all = (fun x -> g.all (f.all x)); { all = (fun x -> g.all (f.all x));
clear = (fun () -> f.clear (); g.clear ()); } clear = (fun () -> f.clear (); g.clear ()); }
...@@ -147,6 +145,14 @@ let split_goals = ...@@ -147,6 +145,14 @@ let split_goals =
let g = fold_env f (fun env -> init_context env, []) in let g = fold_env f (fun env -> init_context env, []) in
conv_res g snd conv_res g snd
exception NotGoalContext
let goal_of_ctxt ctxt =
match ctxt.ctxt_decl.d_node with
| Dprop (Pgoal,pr) -> pr
| _ -> raise NotGoalContext
(*
let extract_goals () = let extract_goals () =
let f ctxt0 (ctxt,l) = let f ctxt0 (ctxt,l) =
let decl = ctxt0.ctxt_decl in let decl = ctxt0.ctxt_decl in
...@@ -161,11 +167,13 @@ let extract_goals () = ...@@ -161,11 +167,13 @@ let extract_goals () =
in in
let g = fold_env f (fun env -> init_context env, []) in let g = fold_env f (fun env -> init_context env, []) in
conv_res g snd conv_res g snd
*)
let identity = let identity =
{ all = (fun x -> x); { all = (fun x -> x);
clear = (fun () -> ()); } clear = (fun () -> ()); }
(*
let cloned_from_ts env ctxt l s ls1 = let cloned_from_ts env ctxt l s ls1 =
assert false (*TODO*) assert false (*TODO*)
(* try *) (* try *)
...@@ -190,4 +198,4 @@ let cloned_from_pr env ctxt l s pr1 = ...@@ -190,4 +198,4 @@ let cloned_from_pr env ctxt l s pr1 =
(* let pr2 = Mnm.find s th.th_export.ns_pr in *) (* let pr2 = Mnm.find s th.th_export.ns_pr in *)
(* Context_utils.cloned_from ctxt pr1.pr_name pr2.pr_name *) (* Context_utils.cloned_from ctxt pr1.pr_name pr2.pr_name *)
(* with Loc.Located _ -> assert false *) (* with Loc.Located _ -> assert false *)
*)
...@@ -28,7 +28,6 @@ open Theory ...@@ -28,7 +28,6 @@ open Theory
type 'a t type 'a t
type ctxt_t = context t type ctxt_t = context t
exception CompositionOfIncompatibleTranformation
(* compose two transformations, the underlying datastructures for (* compose two transformations, the underlying datastructures for
the memoisation are shared *) the memoisation are shared *)
val compose : context t -> 'a t -> 'a t val compose : context t -> 'a t -> 'a t
...@@ -86,4 +85,9 @@ val fold_context_of_decl: ...@@ -86,4 +85,9 @@ val fold_context_of_decl:
val split_goals : context list t val split_goals : context list t
exception NotGoalContext
val goal_of_ctxt : context -> prop
(* goal_of_ctxt ctxts return the goal of a goal context
the ctxt must end with a goal.*)
val identity : context t val identity : context t
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