Commit 336ea66d authored by Martin Clochard's avatar Martin Clochard

discriminate: change way to configure the transformation

This commit enable the possibility to change discriminate
behavior from Why3 source files. The 4 metas that configure
the transformation:


can now be configured from source files (actually they could
before, but their value was overriden by the drivers).

The behavior in absence of annotation can be specified from
drivers using the 4 new configuration metas:


They behave as their non-default counterparts, except they
have lower precedence. This avoid the forementioned
overriding problem.
parent 3c3019a6
theory BuiltIn
meta "select_inst" "goal"
meta "select_lskept" "goal"
meta "select_lsinst" "goal"
meta "select_kept" "all"
meta "select_inst_default" "goal"
meta "select_lskept_default" "goal"
meta "select_lsinst_default" "goal"
meta "select_kept_default" "all"
......@@ -356,21 +356,26 @@ exception IllegalFlagTrans of meta
type ('a,'b) flag_trans = ('a -> 'b trans) Hstr.t
let on_flag m ft def arg =
let on_flag_find m ft s = try Hstr.find ft s with
| Not_found -> let l = Hstr.fold (fun s _ l -> s :: l) ft [] in
raise (UnknownFlagTrans (m,s,l))
let on_flag_gen m ft def_name def arg =
on_meta_excl m (fun alo ->
let s = match alo with
| None -> def
| Some [MAstr s] -> s
let t, tr_name = match alo with
| None -> def, Printf.sprintf "%s %s" m.meta_name def_name
| Some [MAstr s] ->
on_flag_find m ft s, Printf.sprintf "%s : %s" m.meta_name s
| _ -> raise (IllegalFlagTrans m)
let t = try Hstr.find ft s with
| Not_found ->
let l = Hstr.fold (fun s _ l -> s :: l) ft [] in
raise (UnknownFlagTrans (m,s,l))
let tr_name = Printf.sprintf "%s : %s" m.meta_name s in
named tr_name (t arg))
let on_flag m ft def arg =
let tdef x = on_flag_find m ft def x in
on_flag_gen m ft (Printf.sprintf ": %s" def) tdef arg
let on_flag_t m ft def arg = on_flag_gen m ft "(default)" def arg
let () = Exn_printer.register (fun fmt exn -> match exn with
| KnownTrans s ->
Format.fprintf fmt "Transformation '%s' is already registered" s
......@@ -95,6 +95,8 @@ val on_flag : meta -> ('a,'b) flag_trans -> string -> 'a -> 'b trans
does not have a requested association. Raises [IllegalFlagTrans] if
the type of [m] is not [[MTstring]]. *)
val on_flag_t : meta -> ('a,'b) flag_trans -> ('a -> 'b trans) -> 'a -> 'b trans
(** Debug Transformations *)
val print_meta : Debug.flag -> meta -> task trans
......@@ -55,6 +55,18 @@ let meta_select_lsinst = register_meta_excl "select_lsinst" [MTstring]
- all: @[mark@ every@ monomorphic@ instance@ in@ the@ task.@]\
let meta_select_inst_default =
register_meta_excl "select_inst_default" [MTstring]
~desc:"Default@ setting@ for@ select_inst"
let meta_select_lskept_default =
register_meta_excl "select_lskept_default" [MTstring]
~desc:"Default@ setting@ for@ select_lskept"
let meta_select_lsinst_default =
register_meta_excl "select_lsinst_default" [MTstring]
~desc:"Default@ setting@ for@ select_lsinst"
module OHTy = OrderedHashed(struct
type t = ty
let tag = ty_hash
......@@ -294,9 +306,14 @@ let clear_metas = Trans.fold (fun hd task ->
| _ -> add_tdecl task hd.task_decl) None
let select_lsinst env =
let inst = Trans.on_flag meta_select_inst ft_select_inst "none" env in
let lskept = Trans.on_flag meta_select_lskept ft_select_lskept "none" env in
let lsinst = Trans.on_flag meta_select_lsinst ft_select_lsinst "none" env in
let select m1 m2 ft =
Trans.on_flag_t m1 ft (Trans.on_flag m2 ft "none") env in
let inst =
select meta_select_inst meta_select_inst_default ft_select_inst in
let lskept =
select meta_select_lskept meta_select_lskept_default ft_select_lskept in
let lsinst =
select meta_select_lsinst meta_select_lsinst_default ft_select_lsinst in
let trans task =
let inst = Trans.apply inst task in
let lskept = Trans.apply lskept task in
......@@ -23,6 +23,10 @@ let meta_select_kept = register_meta_excl "select_kept" [MTstring]
- all: @[mark@ every@ closed@ type@ in@ the@ task.@]\
let meta_select_kept_default =
register_meta_excl "select_kept_default" [MTstring]
~desc:"Default@ setting@ for@ select_kept"
let meta_enco_kept = register_meta_excl "enco_kept" [MTstring]
~desc:"Specify@ the@ type@ protection@ transformation:@; \
......@@ -52,7 +56,8 @@ let ft_enco_kept = ((Hstr.create 17) : (Env.env,task) Trans.flag_trans)
let ft_enco_poly = ((Hstr.create 17) : (Env.env,task) Trans.flag_trans)
let select_kept def env =
let select = Trans.on_flag meta_select_kept ft_select_kept def env in
let def = Trans.on_flag meta_select_kept_default ft_select_kept def in
let select = Trans.on_flag_t meta_select_kept ft_select_kept def env in
let trans task =
let add ty acc = create_meta Libencoding.meta_kept [MAty ty] :: acc in
let decls = Sty.fold add (Trans.apply select task) [] 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