Skip to content

GitLab

why3
why3
Commit 4379970a authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

syntax rules, metas, and preludes are cloned 

remove the keyword "cloned" from drivers, since it becomes
the default and only behaviour (the same for prelude strings).

Also, remove obsolete Printer.print_prelude_for_theory.
parent 385bdf8c
Hide whitespace changes
Inline Side-by-side
Showing with 56 additions and 80 deletions
drivers/alt_ergo_bare.drv
View file @ 4379970a
......@@ -144,14 +144,7 @@ theory Tuple0
end
theory algebra.AC
meta cloned AC function op
remove cloned prop Comm.Comm
remove cloned prop Assoc
meta AC function op
remove prop Comm.Comm
remove prop Assoc
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
drivers/z3_smtv1.drv
View file @ 4379970a
......@@ -121,7 +121,7 @@ theory Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
meta cloned "encoding_decorate : kept" type bool
meta "encoding_decorate : kept" type bool
end
theory bool.Bool
syntax function andb "(and %1 %2)"
......
src/core/printer.ml
View file @ 4379970a
......@@ -171,23 +171,29 @@ let print_prelude fmt pl =
print_list nothing println fmt pl
let print_prelude_of_theories th_used fmt pm =
List.iter (fun th ->
let prel = Mid.find_def [] th.th_name pm in
print_prelude fmt prel) th_used
let ht = Hid.create 5 in
List.iter (fun { th_name = id } ->
if not (Hid.mem ht id) then begin
print_prelude fmt (Mid.find_def [] id pm);
Hid.add ht id () end) th_used
let print_th_prelude task fmt pm =
let th_used = task_fold (fun acc -> function
| { td_node = Clone (th,sm) } when is_empty_sm sm -> th::acc
| { td_node = Clone (th,_) } -> th::acc
| _ -> acc) [] task
in
print_prelude_of_theories th_used fmt pm
(*
let print_prelude_for_theory th fmt pm =
let th_used = List.fold_left (fun acc -> function
| { td_node = Clone (th,sm) } when is_empty_sm sm -> th::acc
| _ -> acc) [] th.th_decls
let rec get_th_used acc th = List.fold_left (fun acc -> function
| { td_node = Use th } -> th :: get_th_used acc th
| { td_node = Clone (th,_) } -> th::acc
| _ -> acc) acc th.th_decls
in
let th_used = List.rev (get_th_used [] th) in
print_prelude_of_theories th_used fmt pm
*)
exception KnownTypeSyntax of tysymbol
exception KnownLogicSyntax of lsymbol
......
src/core/printer.mli
View file @ 4379970a
......@@ -37,7 +37,6 @@ val list_printers : unit -> (string * Pp.formatted) list
val print_prelude : prelude pp
val print_th_prelude : task -> prelude_map pp
val print_prelude_for_theory : theory -> prelude_map pp
val meta_syntax_type : meta
val meta_syntax_logic : meta
......
src/driver/driver.ml
View file @ 4379970a
......@@ -32,7 +32,6 @@ type driver = {
drv_thprelude : prelude_map;
drv_blacklist : string list;
drv_meta : (theory * Stdecl.t) Mid.t;
drv_meta_cl : (theory * Stdecl.t) Mid.t;
drv_regexps : (Str.regexp * prover_answer) list;
drv_timeregexps : Call_provers.timeregexp list;
drv_exitcodes : (int * prover_answer) list;
......@@ -111,7 +110,6 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
let thprelude = ref Mid.empty in
let meta = ref Mid.empty in
let meta_cl = ref Mid.empty in
let qualid = ref [] in
let find_pr th (loc,q) = try ns_find_pr th.th_export q
......@@ -137,19 +135,19 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
| Rprelude s ->
let l = Mid.find_def [] th.th_name !thprelude in
thprelude := Mid.add th.th_name (s::l) !thprelude
| Rsyntaxts (c,q,s) ->
| Rsyntaxts (q,s) ->
let td = syntax_type (find_ts th q) s in
add_meta th td (if c then meta_cl else meta)
| Rsyntaxfs (c,q,s) ->
add_meta th td meta
| Rsyntaxfs (q,s) ->
let td = syntax_logic (find_fs th q) s in
add_meta th td (if c then meta_cl else meta)
| Rsyntaxps (c,q,s) ->
add_meta th td meta
| Rsyntaxps (q,s) ->
let td = syntax_logic (find_ps th q) s in
add_meta th td (if c then meta_cl else meta)
| Rremovepr (c,q) ->
add_meta th td meta
| Rremovepr (q) ->
let td = remove_prop (find_pr th q) in
add_meta th td (if c then meta_cl else meta)
| Rmeta (c,s,al) ->
add_meta th td meta
| Rmeta (s,al) ->
let rec ty_of_pty = function
| PTyvar x ->
Ty.ty_var (Typing.create_user_tv x)
......@@ -171,7 +169,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
in
let m = lookup_meta s in
let td = create_meta m (List.map convert al) in
add_meta th td (if c then meta_cl else meta)
add_meta th td meta
in
let add_local th (loc,rule) =
try add_local th rule with e -> raise (Loc.Located (loc,e))
......@@ -198,7 +196,6 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
drv_thprelude = Mid.map List.rev !thprelude;
drv_blacklist = Queue.fold (fun l s -> s :: l) [] blacklist;
drv_meta = !meta;
drv_meta_cl = !meta_cl;
drv_regexps = List.rev !regexps;
drv_timeregexps = List.rev !timeregexps;
drv_exitcodes = List.rev !exitcodes;
......@@ -258,15 +255,6 @@ let update_task drv task_orig =
| Some { task_decl = g ; task_prev = t } -> t,g
| None -> raise Task.GoalNotFound
in
let task =
Mid.fold (fun _ (th,s) task ->
if Task.on_used_theory th task_orig then
Stdecl.fold (fun tdm task ->
add_tdecl task tdm
) s task
else task
) drv.drv_meta task
in
let task =
Mid.fold (fun _ (th,s) task ->
Task.on_theory th (fun task sm ->
......@@ -274,7 +262,7 @@ let update_task drv task_orig =
add_tdecl task (clone_meta tdm sm)
) s task
) task task_orig
) drv.drv_meta_cl task
) drv.drv_meta task
in
add_tdecl task goal
......
src/driver/driver_ast.ml
View file @ 4379970a
......@@ -13,8 +13,6 @@ type loc = Loc.position
type qualid = loc * string list
type cloned = bool
type pty =
| PTyvar of string
| PTyapp of qualid * pty list
......@@ -30,11 +28,11 @@ type metarg =
type th_rule =
| Rprelude of string
| Rsyntaxts of cloned * qualid * string
| Rsyntaxfs of cloned * qualid * string
| Rsyntaxps of cloned * qualid * string
| Rremovepr of cloned * qualid
| Rmeta of cloned * string * metarg list
| Rsyntaxts of qualid * string
| Rsyntaxfs of qualid * string
| Rsyntaxps of qualid * string
| Rremovepr of qualid
| Rmeta of string * metarg list
type theory_rules = {
thr_name : qualid;
......@@ -43,8 +41,8 @@ type theory_rules = {
type mo_rule =
| MRtheory of th_rule
| MRexception of cloned * qualid * string
| MRval of cloned * qualid * string
| MRexception of qualid * string
| MRval of qualid * string
type module_rules = {
mor_name : qualid;
......
src/driver/driver_lexer.mll
View file @ 4379970a
......@@ -30,7 +30,6 @@
"syntax", SYNTAX;
"remove", REMOVE;
"meta", META;
"cloned", CLONED;
"prelude", PRELUDE;
"printer", PRINTER;
"valid", VALID;
......
src/driver/driver_parser.mly
View file @ 4379970a
......@@ -27,7 +27,7 @@
%token <string> OPERATOR
%token THEORY END SYNTAX REMOVE META PRELUDE PRINTER
%token VALID INVALID TIMEOUT OUTOFMEMORY UNKNOWN FAIL TIME
%token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT QUOTE EOF
%token UNDERSCORE LEFTPAR RIGHTPAR DOT QUOTE EOF
%token BLACKLIST
%token MODULE EXCEPTION VAL
%token FUNCTION PREDICATE TYPE PROP FILENAME TRANSFORM PLUGIN
......@@ -89,14 +89,14 @@ list0_trule:
;
trule:
| PRELUDE STRING { Rprelude ($2) }
| SYNTAX cloned TYPE qualid STRING { Rsyntaxts ($2, $4, $5) }
| SYNTAX cloned CONSTANT qualid STRING { Rsyntaxfs ($2, $4, $5) }
| SYNTAX cloned FUNCTION qualid STRING { Rsyntaxfs ($2, $4, $5) }
| SYNTAX cloned PREDICATE qualid STRING { Rsyntaxps ($2, $4, $5) }
| REMOVE cloned PROP qualid { Rremovepr ($2, $4) }
| META cloned ident meta_args { Rmeta ($2, $3, $4) }
| META cloned STRING meta_args { Rmeta ($2, $3, $4) }
| PRELUDE STRING { Rprelude ($2) }
| SYNTAX TYPE qualid STRING { Rsyntaxts ($3, $4) }
| SYNTAX CONSTANT qualid STRING { Rsyntaxfs ($3, $4) }
| SYNTAX FUNCTION qualid STRING { Rsyntaxfs ($3, $4) }
| SYNTAX PREDICATE qualid STRING { Rsyntaxps ($3, $4) }
| REMOVE PROP qualid { Rremovepr ($3) }
| META ident meta_args { Rmeta ($2, $3) }
| META STRING meta_args { Rmeta ($2, $3) }
;
meta_args:
......@@ -113,11 +113,6 @@ meta_arg:
| INTEGER { PMAint $1 }
;
cloned:
| /* epsilon */ { false }
| CLONED { true }
;
tqualid:
| ident { loc (), [$1] }
| ident DOT tqualid { loc (), ($1 :: snd $3) }
......@@ -133,9 +128,6 @@ ident:
| IDENT { $1 }
| SYNTAX { "syntax" }
| REMOVE { "remove" }
/*
| CLONED { "cloned" }
*/
| PRELUDE { "prelude" }
| PRINTER { "printer" }
| VALID { "valid" }
......@@ -218,7 +210,8 @@ file_extract:
;
list0_global_theory_module:
| /* epsilon */ { { fe_global = []; fe_th_rules = []; fe_mo_rules = [] } }
| /* epsilon */
{ { fe_global = []; fe_th_rules = []; fe_mo_rules = [] } }
| global_extract list0_global_theory_module
{ {$2 with fe_global = (loc_i 1, $1) :: ($2.fe_global)} }
| theory list0_global_theory_module
......@@ -244,8 +237,8 @@ list0_mrule:
;
mrule:
| trule { MRtheory $1 }
| SYNTAX cloned EXCEPTION qualid STRING { MRexception ($2, $4, $5) }
| SYNTAX cloned VAL qualid STRING { MRval ($2, $4, $5) }
| trule { MRtheory $1 }
| SYNTAX EXCEPTION qualid STRING { MRexception ($3, $4) }
| SYNTAX VAL qualid STRING { MRval ($3, $4) }
;
src/whyml/mlw_driver.ml
View file @ 4379970a
......@@ -100,21 +100,21 @@ let load_driver lib file extra_files =
| Rprelude s ->
let l = Mid.find_def [] th.th_name !thprelude in
thprelude := Mid.add th.th_name (s::l) !thprelude
| Rsyntaxts (_,q,s) ->
| Rsyntaxts (q,s) ->
let ts = find_ts th q in
check_syntax_type ts s;
add_syntax ts.ts_name s
| Rsyntaxfs (_,q,s) ->
| Rsyntaxfs (q,s) ->
let fs = find_fs th q in
check_syntax_logic fs s;
add_syntax fs.ls_name s
| Rsyntaxps (_,q,s) ->
| Rsyntaxps (q,s) ->
let ps = find_ps th q in
check_syntax_logic ps s;
add_syntax ps.ls_name s
| Rremovepr (_,q) ->
| Rremovepr (q) ->
ignore (find_pr th q)
| Rmeta (_,s,al) ->
| Rmeta (s,al) ->
let rec ty_of_pty = function
| PTyvar x ->
Ty.ty_var (Typing.create_user_tv x)
......@@ -153,10 +153,10 @@ let load_driver lib file extra_files =
in
let add_local_module loc m = function
| MRtheory trule -> add_local m.mod_theory (loc,trule)
| MRexception (_,q,s) ->
| MRexception (q,s) ->
let xs = find_xs m q in
add_syntax xs.xs_name s
| MRval (_,q,s) ->
| MRval (q,s) ->
let id = find_val m q in
add_syntax id s
in
......
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