Commit 23ca2d16 authored by Francois Bobot's avatar Francois Bobot

   - Util : Ajout de Creation generique de Set,Map et Hashtbl 
            quand on a un tag et une egalitée physique
   - Hashweak : Implementation de l'idee de Jean-Christophe et Andreï
   - Register : Simplification des types comme demandé par Jean-Christophe
                Mise à jour des fichiers qui en dépendait
   - Theory   : Ajout d'une facilité de création des th_inst
   - Encoding_decorate : Prelude pour l'encodage de Stéphane en utilisant flat_theory d'Andreï
   - Ty : Ajout de Sty, Mty et Hty
   - Main : Reduction de la taille des lignes à 80 colonnes
parent 85b6704d
......@@ -121,14 +121,14 @@ CORE_CMO := ident.cmo ty.cmo term.cmo decl.cmo theory.cmo\
task.cmo pretty.cmo trans.cmo env.cmo register.cmo
CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
UTIL_CMO := pp.cmo loc.cmo util.cmo hashcons.cmo sysutil.cmo
UTIL_CMO := pp.cmo loc.cmo util.cmo hashcons.cmo sysutil.cmo hashweak.cmo
UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))
PARSER_CMO := parser.cmo lexer.cmo denv.cmo typing.cmo
PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
split_conjunction.cmo
split_conjunction.cmo encoding_decorate.cmo
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
DRIVER_CMO := call_provers.cmo dynlink_compat.cmo driver_parser.cmo\
......@@ -454,7 +454,7 @@ jc/jc_ai.ml: jc/jc_annot_inference.ml jc/jc_annot_fail.ml Makefile
############
tags:
find src -name "*.ml*" | grep -v ".svn" | sort -r | xargs \
find src -regex ".*\.ml[^#]*" | grep -v ".svn" | sort -r | xargs \
etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
"--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
"--regex=/and[ \t]+\([^ \t]+\)/\1/" \
......
printer "why3"
filename "%f-%t-%s.why"
transformations
"encoding_decorate"
end
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
end
theory Prelude
type deco
type undeco
type ty
logic sort(ty,undeco) : deco
end
theory Builtin
use import Prelude
type t
logic tty : ty
logic d2t(deco) : t
logic t2u(t) : undeco
axiom Conv : forall x:t[t2u(x)]. d2t(sort(tty,t2u(x)))=x
end
......@@ -26,6 +26,10 @@ type 'a value = env option -> clone option -> 'a
type 'a registered = {mutable value : 'a value;
generate : unit -> 'a value;
tag : int}
type 'a trans_reg = 'a trans registered
type 'a tlist_reg = 'a tlist registered
(*
module HSreg =
struct
......@@ -77,16 +81,11 @@ let store f = store0 unused0 unused0 f
let store_env f = store0 (memo0 env_tag) unused0 f
let store_clone f = store0 (memo0 env_tag) (memo0 cl_tag) f
let apply0 reg = reg.value
let apply0 reg env clone = Trans.apply (reg.value env clone)
let apply_clone reg env clone = apply0 reg (Some env) (Some clone)
let apply_env reg env = apply0 reg (Some env) None
let apply reg = apply0 reg None None
let apply_trans0 reg env clone = Trans.apply (reg.value env clone)
let apply_trans_clone reg env clone = apply_trans0 reg (Some env) (Some clone)
let apply_trans_env reg env = apply_trans0 reg (Some env) None
let apply_trans reg = apply_trans0 reg None None
let clear reg = reg.value<-reg.generate ()
(*
......@@ -102,9 +101,8 @@ let compose0 comp reg1 reg2 =
fun env cl -> comp (reg1 env cl) (reg2 env cl) in
create gen
let compose reg1 reg2 = compose0 (fun f g x -> g (f x)) reg1 reg2
let compose_trans reg1 reg2 = compose0 (fun f g -> Trans.compose f g) reg1 reg2
let compose_trans_l reg1 reg2 = compose0 (fun f g -> Trans.compose_l f g)
let compose reg1 reg2 = compose0 (fun f g -> Trans.compose f g) reg1 reg2
let compose_l reg1 reg2 = compose0 (fun f g -> Trans.compose_l f g)
reg1 reg2
let conv_res conv reg1 =
......@@ -113,6 +111,7 @@ let conv_res conv reg1 =
fun env cl -> conv (reg1 env cl) in
create gen
let singleton reg = conv_res singleton reg
let identity_trans = store (fun () -> identity)
let identity_trans_l = store (fun () -> identity_l)
......@@ -20,41 +20,30 @@ open Env
open Task
open Trans
type 'a registered
type 'a trans_reg
type 'a tlist_reg = 'a list trans_reg
val store : (unit -> 'a) -> 'a registered
val store_env : (unit -> env -> 'a) -> 'a registered
val store_clone : (unit -> env -> clone -> 'a) -> 'a registered
val store : (unit -> 'a trans) -> 'a trans_reg
val store_env : (unit -> env -> 'a trans) -> 'a trans_reg
val store_clone : (unit -> env -> clone -> 'a trans) -> 'a trans_reg
exception ArgumentNeeded
val apply0 : 'a registered -> env option -> clone option -> 'a
val apply_clone : 'a registered -> env -> clone -> 'a
val apply_env : 'a registered -> env -> 'a
val apply : 'a registered -> 'a
val apply_trans0 :
'a trans registered -> env option -> clone option -> task -> 'a
val apply_trans_clone :
'a trans registered -> env -> clone -> task -> 'a
val apply_trans_env :
'a trans registered -> env -> task -> 'a
val apply_trans :
'a trans registered -> task -> 'a
val compose0 :
('a -> 'b -> 'c) -> 'a registered -> 'b registered -> 'c registered
val compose :
('a -> 'b) registered -> ('b -> 'c) registered -> ('a -> 'c) registered
val compose_trans :
task trans registered -> 'a trans registered -> 'a trans registered
val compose_trans_l :
task tlist registered -> 'a tlist registered -> 'a tlist registered
val conv_res : ('a -> 'b) -> 'a registered -> 'b registered
val apply_clone : 'a trans_reg -> env -> clone -> task -> 'a
val apply_env : 'a trans_reg -> env -> task -> 'a
val apply : 'a trans_reg -> task -> 'a
val compose : task trans_reg -> 'a trans_reg -> 'a trans_reg
val compose_l : task tlist_reg -> 'a tlist_reg -> 'a tlist_reg
(*val conv_res : ('a -> 'b) -> 'a registered -> 'b registered
(* Sould be used only with function working in constant time*)
*)
val singleton : 'a trans_reg -> 'a tlist_reg
val clear_all : unit -> unit
val clear : 'a registered -> unit
val clear : 'a trans_reg -> unit
val identity_trans : task trans registered
val identity_trans_l : task tlist registered
val identity_trans : task trans_reg
val identity_trans_l : task tlist_reg
......@@ -43,6 +43,7 @@ type lsymbol = private {
}
val create_lsymbol : preid -> ty list -> ty option -> bool -> lsymbol
(* create_lsymbols preid tyargs tyres is_constr *)
val create_fsymbol : preid -> ty list -> ty -> lsymbol
val create_fconstr : preid -> ty list -> ty -> lsymbol
val create_psymbol : preid -> ty list -> lsymbol
......
......@@ -244,6 +244,23 @@ let empty_inst = {
inst_goal = Spr.empty;
}
let create_inst ~ts ~ls ~lemma ~goal =
let ts =
List.fold_left (fun acc (tso,tsn) -> Mts.add tso tsn acc) Mts.empty ts in
let ls =
List.fold_left (fun acc (lso,lsn) -> Mls.add lso lsn acc) Mls.empty ls in
let make_list = List.fold_left (fun acc lem -> Spr.add lem acc) Spr.empty in
let lemma = make_list lemma in
let goal = make_list goal in
{
inst_ts = ts;
inst_ls = ls;
inst_lemma = lemma;
inst_goal = goal;
}
exception CannotInstantiate of ident
type clones = {
......
......@@ -77,13 +77,17 @@ val get_namespace : theory_uc -> namespace
(** Use and clone *)
type th_inst = {
inst_ts : tysymbol Mts.t;
inst_ts : tysymbol Mts.t; (* old to new *)
inst_ls : lsymbol Mls.t;
inst_lemma : Spr.t;
inst_goal : Spr.t;
}
val empty_inst : th_inst
val create_inst :
ts:(tysymbol * tysymbol) list ->
ls:(lsymbol * lsymbol) list ->
lemma:prsymbol list -> goal:prsymbol list -> th_inst
val use_export : theory_uc -> theory -> theory_uc
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
......
......@@ -56,16 +56,13 @@ and ty_node =
| Tyvar of tvsymbol
| Tyapp of tysymbol * ty list
module Tsym = struct
type t = tysymbol
let equal = (==)
let hash ts = ts.ts_name.id_tag
let compare ts1 ts2 =
Pervasives.compare ts1.ts_name.id_tag ts2.ts_name.id_tag
end
module Sts = Set.Make(Tsym)
module Mts = Map.Make(Tsym)
module Hts = Hashtbl.Make(Tsym)
module Structts = Util.StructMake(struct
type t = tysymbol
let tag x = x.ts_name.id_tag
end)
module Sts = Structts.S
module Mts = Structts.M
module Hts = Structts.H
let mk_ts name args def = {
ts_name = name;
......@@ -93,11 +90,11 @@ module Ty = struct
let tag n ty = { ty with ty_tag = n }
end
module Hty = Hashcons.Make(Ty)
module Hsty = Hashcons.Make(Ty)
let mk_ty n = { ty_node = n; ty_tag = -1 }
let ty_var n = Hty.hashcons (mk_ty (Tyvar n))
let ty_app s tl = Hty.hashcons (mk_ty (Tyapp (s, tl)))
let ty_var n = Hsty.hashcons (mk_ty (Tyvar n))
let ty_app s tl = Hsty.hashcons (mk_ty (Tyapp (s, tl)))
(* generic traversal functions *)
......@@ -193,3 +190,10 @@ let ts_real = create_tysymbol (id_fresh "real") [] None
let ty_int = ty_app ts_int []
let ty_real = ty_app ts_real []
module Structty = Util.StructMake(struct
type t = ty
let tag x = x.ty_tag
end)
module Sty = Structty.S
module Mty = Structty.M
module Hty = Structty.H
......@@ -57,6 +57,7 @@ exception NonLinear
exception UnboundTypeVariable
val create_tysymbol : preid -> tvsymbol list -> ty option -> tysymbol
(* create_tysymbol preid param def *)
val ty_var : tvsymbol -> ty
val ty_app : tysymbol -> ty list -> ty
......@@ -84,3 +85,6 @@ val ts_real : tysymbol
val ty_int : ty
val ty_real : ty
module Sty : Set.S with type elt = ty
module Mty : Map.S with type key = ty
module Hty : Hashtbl.S with type key = ty
......@@ -132,29 +132,31 @@ and driver = {
drv_prover : Call_provers.prover;
drv_prelude : string option;
drv_filename : string option;
drv_transforms : task Trans.tlist registered;
drv_transforms : task tlist_reg;
drv_rules : theory_rules list;
drv_thprelude : string Hid.t;
(* the first is the translation only for this ident, the second is also for representant *)
(* the first is the translation only for this ident, the second is
also for representant *)
drv_theory : (translation * translation) Hid.t;
drv_with_task : translation Hid.t;
}
(*
let print_driver fmt driver =
let print_driver fmt driver =
printf "drv_theory %a@\n"
(Pp.print_iter2 Hid.iter Pp.semi Pp.comma print_ident
(Pp.print_pair print_translation print_translation))
driver.drv_theory
(Pp.print_iter2 Hid.iter Pp.semi Pp.comma print_ident
(Pp.print_pair print_translation print_translation))
driver.drv_theory
*)
(** registering transformation *)
let (transforms : (string, task Trans.tlist registered) Hashtbl.t)
let (transforms : (string, task tlist_reg) Hashtbl.t)
= Hashtbl.create 17
let register_transform_l name transform = Hashtbl.replace transforms name transform
let register_transform name t = register_transform_l name (conv_res Trans.singleton t)
let register_transform_l name transform =
Hashtbl.replace transforms name transform
let register_transform name t = register_transform_l name (singleton t)
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []
(** registering printers *)
......@@ -206,8 +208,13 @@ let check_syntax loc s len =
iter_group regexp_arg_pos
(fun s ->
let i = int_of_string (matched_group 1 s) in
if i=0 then errorm ~loc "invalid indice of argument : the first one is %%1 and not %%0";
if i>len then errorm ~loc "invalid indice of argument \"%%%i\" this logic has only %i argument" i len) s
if i=0
then errorm ~loc
"invalid indice of argument : the first one is %%1 and not %%0";
if i>len
then errorm ~loc
"invalid indice of argument \"%%%i\" this logic has only %i argument"
i len) s
let load_rules env clone driver {thr_name = loc,qualid; thr_rules = trl} =
......@@ -322,7 +329,7 @@ let load_driver file env =
let t =
try Hashtbl.find transforms s
with Not_found -> errorm ~loc "unknown transformation %s" s in
compose_trans_l acc t
compose_l acc t
)
identity_trans_l transformations in
let transforms = trans ltransforms in
......@@ -368,7 +375,8 @@ let syntax_arguments s print fmt l =
(** using drivers *)
let apply_transforms env clone drv = apply_trans_clone drv.drv_transforms env clone
let apply_transforms env clone drv =
apply_clone drv.drv_transforms env clone
let print_task env clone drv fmt task = match drv.drv_printer with
| None -> errorm "no printer"
......
......@@ -37,7 +37,8 @@ type translation =
| Tag of Util.Sstr.t
val query_ident : driver -> ident -> translation
val syntax_arguments : string -> (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
val syntax_arguments : string -> (formatter -> 'a -> unit) ->
formatter -> 'a list -> unit
(* syntax_argument templ print_arg fmt l print in the formatter fmt
the list l using the template templ and the printer print_arg *)
(** registering printers *)
......@@ -46,8 +47,8 @@ type printer = driver -> formatter -> task -> unit
val register_printer : string -> printer -> unit
val register_transform : string -> task trans Register.registered -> unit
val register_transform_l : string -> task tlist Register.registered -> unit
val register_transform : string -> task Register.trans_reg -> unit
val register_transform_l : string -> task Register.tlist_reg -> unit
val list_printers : unit -> string list
val list_transforms : unit -> string list
......
......@@ -81,11 +81,14 @@ let () =
can't be used with --output-file";
"--driver", Arg.String (fun s -> driver := Some s),
"<file> set the driver file";
"--timeout", Arg.Set_int timeout, "set the timeout used when calling provers (0 unlimited, default 10)";
"--timeout", Arg.Set_int timeout, "set the timeout used when calling \
provers (0 unlimited, default 10)";
"--list-printers", Arg.Set list_printers, "list the printers registered";
"--list-transforms", Arg.Set list_transforms, "list the transformation registered";
"--list-transforms", Arg.Set list_transforms, "list the transformation \
registered";
(* "--list-goals", Arg.Set list_goals, "list the goals of the files";*)
"--print-debug", Arg.Set print_debug, "print on stderr the theories of the files given on the commandline"
"--print-debug", Arg.Set print_debug, "print on stderr the theories of \
the files given on the commandline"
]
(fun f -> Queue.push f files)
"usage: why [options] files..."
......@@ -167,7 +170,8 @@ let extract_goals ?filter =
let l = List.rev_map (fun task -> (th,task)) l in
List.rev_append l acc
let file_sanitizer = Ident.sanitizer Ident.char_to_alnumus Ident.char_to_alnumus
let file_sanitizer =
Ident.sanitizer Ident.char_to_alnumus Ident.char_to_alnumus
let do_file env drv filename_printer file =
if !parse_only then begin
......@@ -182,7 +186,8 @@ let do_file env drv filename_printer file =
let m = Typing.read_file env file in
if !print_debug then
eprintf "%a"
(Pp.print_iter2 Mnm.iter Pp.newline Pp.nothing Pp.nothing Pretty.print_theory)
(Pp.print_iter2 Mnm.iter Pp.newline Pp.nothing Pp.nothing
Pretty.print_theory)
m;
if not !type_only then
let drv =
......@@ -197,7 +202,8 @@ let do_file env drv filename_printer file =
Hashtbl.fold
(fun tname goals acc ->
let th = try Mnm.find tname m with Not_found ->
eprintf "File %s : --goal/--goals_of : Unknown theory %s@." file tname; exit 1 in
eprintf "File %s : --goal/--goals_of : Unknown theory %s@."
file tname; exit 1 in
let filter = match goals with
| None -> None
| Some s -> Some
......@@ -213,7 +219,8 @@ let do_file env drv filename_printer file =
let goals = List.fold_left
(fun acc (th,(task,cl)) ->
List.rev_append
(List.map (fun e -> (th,e,cl)) (Driver.apply_transforms env cl drv task)
(List.map (fun e -> (th,e,cl)) (Driver.apply_transforms env cl drv
task)
) acc) [] goals in
(* Pretty-print the goals or call the prover *)
begin
......@@ -254,12 +261,14 @@ let do_file env drv filename_printer file =
let fmt = if file = "-"
then std_formatter
else formatter_of_out_channel (open_out file) in
fprintf fmt "%a\000@?" (Driver.print_task env cl drv) task) goals
fprintf fmt "%a\000@?" (Driver.print_task env cl drv) task)
goals
end;
if !call then
(* we are in the call mode *)
let call (th,task,cl) =
let res = Driver.call_prover ~debug:!debug ?timeout env cl drv task in
let res =
Driver.call_prover ~debug:!debug ?timeout env cl drv task in
printf "%s %s %s : %a@."
file th.th_name.Ident.id_short
((task_goal task).Decl.pr_name).Ident.id_long
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Ident
open Ty
open Term
open Task
open Theory
let why_filename = "encoding_decorate"
(* From Encoding Polymorphism CADE07*)
module Prelude =
struct
(* let create_ty s = ty_app (create_tysymbol (id_fresh s) [] None) [] in
let deco = create_ty "deco" in
let undeco = create_ty "undeco" in
let ty = create_ty "ty" in
let csort = create_fsymbol (id_fresh "csort") [ty;undeco] deco in
*)
(* let spec_conv ts =
let name = ts.ts_name.id_short in
let d2ty = create_fsymbol (id_fresh ("d2"^name)) [deco] (ty_app ts []) in
let ty2u = create_fsymbol (id_fresh (name^"2u")) [(ty_app ts [])] undeco in
let axiom =
let l =
List.fold_left (fun acc ty -> Sty.add ty acc) Sty.empty l
*)
end
type lconv = {d2t : lsymbol;
t2u : lsymbol}
type tenv = {specials : lconv Mts.t;
deco : ty;
undeco : ty;
sort : lsymbol;
ty : ty}
let load_prelude env =
let specials_type = [ts_int;ts_real] in
let prelude = Env.find_theory env [why_filename] "Prelude" in
let sort = Theory.ns_find_ls prelude.th_export ["sort"] in
let ty = ty_app (Theory.ns_find_ts prelude.th_export ["ty"]) [] in
let deco = ty_app (Theory.ns_find_ts prelude.th_export ["deco"]) [] in
let undeco = ty_app (Theory.ns_find_ts prelude.th_export ["undeco"]) [] in
let task = None in
let task = flat_theory task prelude in
let builtin = Env.find_theory env [why_filename] "Builtin" in
let type_t = Theory.ns_find_ts builtin.th_export ["t"] in
let logic_d2t = Theory.ns_find_ls builtin.th_export ["d2t"] in
let logic_t2u = Theory.ns_find_ls builtin.th_export ["t2u"] in
let clone_builtin (task,spmap) ts =
let name = ts.ts_name.id_short in
let th_uc = create_theory (id_fresh ("encoding_decorate_for_"^name)) in
let ty = (ty_app ts []) in
let d2ty = create_fsymbol (id_fresh ("d2"^name)) [deco] ty in
let ty2u = create_fsymbol (id_fresh (name^"2u")) [ty] undeco in
let th_inst = create_inst
~ts:[type_t,ts]
~ls:[logic_d2t,d2ty;logic_t2u,ty2u]
~lemma:[] ~goal:[] in
let lconv = { d2t = d2ty; t2u = ty2u} in
let th_uc = clone_export th_uc builtin th_inst in
let task = flat_theory task (close_theory th_uc) in
task,Mts.add ts lconv spmap
in
let task,specials =
List.fold_left clone_builtin (task,Mts.empty) specials_type in
task,
{ specials = specials;
deco = deco;
undeco = undeco;
ty = ty;
sort = sort}
let decl (tenv:tenv) d = [d]
(* match d.d_node with *)
(* | Dtype t when Mts.mem tenv.specials t -> [d] *)
(* | Dtype t when Mts.mem tenv.specials t -> [d] *)
(* | Dlogic l -> *)
(* let fn = function *)
(* | ls, Some ld -> *)
(* let vl,e = open_ls_defn ld in *)
(* make_ls_defn ls vl (e_map fnT fnF e) *)
(* | ld -> ld *)
(* in *)
(* create_logic_decl (List.map fn l) *)
(* | Dind l -> *)
(* let fn (pr,f) = pr, fnF f in *)
(* let fn (ps,l) = ps, List.map fn l in *)
(* create_ind_decl (List.map fn l) *)
(* | Dprop (k,pr,f) -> *)
(* create_prop_decl k pr (fnF f) *)
let t = Register.store_env
(fun () env ->
let init_task,tenv = load_prelude env in
Trans.decl (decl tenv) init_task)
let () = Driver.register_transform "encoding_decorate" t
......@@ -23,17 +23,17 @@
val t :
isnotinlinedt:(Term.term -> bool) ->
isnotinlinedf:(Term.fmla -> bool) ->
Task.task Trans.trans Register.registered
Task.task Register.trans_reg
(* Inline them all *)
val all : Task.task Trans.trans Register.registered
val all : Task.task Register.trans_reg
(* Inline only the trivial definition :
logic c : t = a
logic f(x : t,...., ) : t = g(y : t2,...) *)
val trivial : Task.task Trans.trans Register.registered
val trivial : Task.task Register.trans_reg
(* Function to use in other transformations if inlining is needed *)
......
......@@ -20,7 +20,7 @@
(* Simplify the recursive type and logic definition *)
val t : Task.task Trans.trans Register.registered
val t : Task.task Register.trans_reg
(* ungroup recursive definition *)
......
module Make (S:Util.Sstruct) =
struct
type 'a t = { ht : (int,'a) Hashtbl.t;
final : S.t -> unit}
let wget w = Weak.get w 0
let wref v =
let w = Weak.create 1 in
Weak.set w 0 (Some v);
w
let create i =
let ht = Hashtbl.create i in
let w = wref ht in
let final x =
match wget w with
| None -> ()
| Some h -> Hashtbl.remove h (S.tag x) in
{ ht = ht; final = final }