Commit aefc8788 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] context by fonction

parent eb0f5249
......@@ -178,7 +178,7 @@ let define_type c t =
end
let parameters f =
if WpContext.is_model_defined () then
if WpContext.is_defined () then
try List.map Lang.F.QED.sort_of_var (Symbol.find f).d_params
with Not_found -> []
else []
......
......@@ -128,15 +128,13 @@ struct
if S.mem x.vname (get_vars ()) then ByValue else
V.param x
(** A memory model context has to be set. *)
let hypotheses () =
let kf = WpContext.get_scope () in
let init = match kf with
| None -> false
| Some f -> WpStrategy.is_main_init f in
let p = ref MemoryContext.empty in
V.iter ?kf ~init (fun vi -> p := MemoryContext.set vi (param vi) !p) ;
MemoryContext.requires !p
let kf,init = match WpContext.get_scope () with
| WpContext.Global -> None,false
| WpContext.Kf f -> Some f, WpStrategy.is_main_init f in
let w = ref MemoryContext.empty in
V.iter ?kf ~init (fun vi -> w := MemoryContext.set vi (param vi) !w) ;
MemoryContext.requires !w
end
......@@ -168,10 +166,10 @@ let is_formal_ptr x =
x.vformal && Cil.isPointerType x.vtype
let refusage_param ~byref ~context x =
let kf = WpContext.get_scope () in
let init = match kf with
| None -> false
| Some f ->
let kf,init = match WpContext.get_scope () with
| WpContext.Global -> None,false
| WpContext.Kf f ->
Some f ,
WpStrategy.is_main_init f ||
Wp_parameters.InitAlias.get () ||
( WpStrategy.isInitConst () &&
......@@ -278,7 +276,7 @@ module COMPILERS = FCMap.Make
if cmp <> 0 then cmp else LogicBuiltins.compare d d'
end)
let instances = ref (COMPILERS.empty : WpContext.t COMPILERS.t)
let instances = ref (COMPILERS.empty : WpContext.model COMPILERS.t)
let instance (s:setup) (d:driver) =
try COMPILERS.find (s,d) !instances
......@@ -286,7 +284,7 @@ let instance (s:setup) (d:driver) =
let id,descr = describe s in
let module CC = (val compiler s.mheap s.mvar) in
let tuning = [configure s d] in
let hypotheses kf = WpContext.on_scope (Some kf) CC.M.hypotheses () in
let hypotheses = CC.M.hypotheses in
let id,descr =
if LogicBuiltins.is_default d then id,descr
else
......
......@@ -40,7 +40,7 @@ val ident : setup -> string
val descr : setup -> string
val compiler : mheap -> mvar -> (module Sigs.Compiler)
val configure : setup -> driver -> WpContext.tuning
val instance : setup -> driver -> WpContext.t
val instance : setup -> driver -> WpContext.model
val default : setup (** ["Var,Typed,Nat,Real"] memory model. *)
val parse :
?default:setup ->
......
......@@ -26,8 +26,8 @@
class type computer =
object
method model : WpContext.t
method lemma : bool
method model : WpContext.model
method add_strategy : WpStrategy.strategy -> unit
method add_lemma : LogicUsage.logic_lemma -> unit
method compute : Wpo.t Bag.t
......
......@@ -26,8 +26,8 @@
class type computer =
object
method model : WpContext.t
method lemma : bool
method model : WpContext.model
method add_strategy : WpStrategy.strategy -> unit
method add_lemma : LogicUsage.logic_lemma -> unit
method compute : Wpo.t Bag.t
......
......@@ -358,7 +358,7 @@ class pane (enabled : GuiConfig.enabled) =
printer#set_target Tactical.Empty ;
strategies#connect None ;
List.iter (fun tactic -> tactic#clear) tactics
| Some(model,tree,sequent,sel) ->
| Some(tree,sequent,sel) ->
strategies#connect (Some (self#strategies sequent)) ;
let select (tactic : GuiTactic.tactic) =
let process = self#apply in
......@@ -366,7 +366,8 @@ class pane (enabled : GuiConfig.enabled) =
let browser = self#browse in
tactic#select ~process ~composer ~browser ~tree sel
in
WpContext.with_model model (List.iter select) tactics ;
let ctxt = ProofEngine.tree_context tree in
WpContext.on_context ctxt (List.iter select) tactics ;
let tgt =
if List.exists (fun tactics -> tactics#targeted) tactics
then sel else Tactical.Empty in
......@@ -470,8 +471,7 @@ class pane (enabled : GuiConfig.enabled) =
self#update_provers (Some wpo) ;
let sequent = printer#sequent in
let select = printer#selection in
let model = wpo.Wpo.po_model in
self#update_tactics (Some(model,proof,sequent,select)) ;
self#update_tactics (Some(proof,sequent,select)) ;
end
| Composer _ | Browser _ -> ()
......@@ -510,9 +510,9 @@ class pane (enabled : GuiConfig.enabled) =
state <- Proof proof ;
printer#restore tgt ;
self#update in
let model = ProofEngine.tree_model proof in
let ctxt = ProofEngine.tree_context proof in
let print = composer#print cc ~quit in
text#printf "%t@." (WpContext.with_model model print) ;
text#printf "%t@." (WpContext.on_context ctxt print) ;
text#hrule ;
text#printf "%t@."
(printer#goal (ProofEngine.head proof)) ;
......@@ -524,9 +524,9 @@ class pane (enabled : GuiConfig.enabled) =
state <- Proof proof ;
printer#restore tgt ;
self#update in
let model = ProofEngine.tree_model proof in
let ctxt = ProofEngine.tree_context proof in
let print = browser#print cc ~quit in
text#printf "%t@." (WpContext.with_model model print) ;
text#printf "%t@." (WpContext.on_context ctxt print) ;
text#hrule ;
text#printf "%t@."
(printer#goal (ProofEngine.head proof)) ;
......
......@@ -143,7 +143,7 @@ class pane (enabled:GuiConfig.enabled) =
let render w =
[`TEXT (Pretty_utils.to_string Wpo.pp_title w)] in
ignore (list#add_column_text ~title:"Goal" [] render) ;
let render w = [`TEXT (Wpo.get_model_name w)] in
let render w = [`TEXT (Wpo.get_model w |> WpContext.MODEL.descr)] in
ignore (list#add_column_text ~title:"Model" [] render) ;
List.iter
self#create_prover
......
......@@ -97,7 +97,7 @@ class popup () =
let setup = Factory.parse (Wp_parameters.Model.get ()) in
let driver = Driver.load_driver () in
let model = Factory.instance setup driver in
WpRTE.generate kf model
WpRTE.generate model kf
method private rte_option
(menu : GMenu.menu GMenu.factory)
......
......@@ -185,8 +185,8 @@ let head t = match t.head with
| None -> t.main
| Some n -> n.goal
let goal n = n.goal
let tree_model t = t.main.Wpo.po_model
let node_model n = n.goal.Wpo.po_model
let tree_context t = Wpo.get_context t.main
let node_context n = Wpo.get_context n.goal
let parent n = n.parent
let title n = n.goal.Wpo.po_name
let tactical n =
......
......@@ -51,8 +51,8 @@ val goto : tree -> position -> unit
val main : tree -> Wpo.t
val head : tree -> Wpo.t
val goal : node -> Wpo.t
val tree_model : tree -> WpContext.t
val node_model : node -> WpContext.t
val tree_context : tree -> WpContext.t
val node_context : node -> WpContext.t
val opened : node -> bool (** not proved *)
val proved : node -> bool (** not opened *)
......
......@@ -30,7 +30,7 @@ type status =
let files : (string,status) Hashtbl.t = Hashtbl.create 32
let filename ?(legacy=false) wpo =
let m = WpContext.get_id wpo.po_model in
let m = WpContext.MODEL.id wpo.po_model in
let d = Wp_parameters.get_session_dir m in
Printf.sprintf "%s/%s.json" d (if legacy then wpo.po_leg else wpo.po_gid)
......
......@@ -655,9 +655,10 @@ let prove_prop wpo ~mode ~axioms ~prop =
let gid = wpo.po_gid in
let leg = wpo.po_leg in
let model = wpo.po_model in
let context = Wpo.get_context wpo in
let script = DISK.file_goal ~pid ~model ~prover:NativeCoq in
let includes , headers , goal =
WpContext.with_model model (assemble_goal ~pid axioms) prop
WpContext.on_context context (assemble_goal ~pid axioms) prop
in
prove_session ~mode {
cw_pid = pid ;
......@@ -673,7 +674,8 @@ let prove_annot wpo vcq ~mode =
Task.todo
begin fun () ->
let prop =
WpContext.with_model wpo.po_model GOAL.compute_proof vcq.VC_Annot.goal in
WpContext.on_context (Wpo.get_context wpo)
GOAL.compute_proof vcq.VC_Annot.goal in
prove_prop wpo ~mode ~axioms:None ~prop
end
......
......@@ -233,7 +233,7 @@ let write_cluster c job =
begin fun fmt ->
Format.fprintf fmt "---------------------------------------------@\n" ;
Format.fprintf fmt "--- File '%s/%s.ergo' @\n"
(WpContext.get_id (WpContext.get_model ())) (cluster_id c) ;
(WpContext.get_context () |> WpContext.S.id) (cluster_id c) ;
Format.fprintf fmt "---------------------------------------------@\n" ;
Command.pp_from_file fmt f ;
end ;
......@@ -472,17 +472,18 @@ let prove_file ~config ~pid ~mode ~file ~lines ~logout ~logerr =
try_prove ~config ~pid ~gui:true ~file ~lines ~logout ~logerr
| r -> Task.return r
let prove_prop ~config ~pid ~mode ~model ~axioms ~prop =
let prove_prop ~config ~pid ~mode ~context ~axioms ~prop =
let prover = NativeAltErgo in
let model = fst context in
let file = DISK.file_goal ~pid ~model ~prover in
let logout = DISK.file_logout ~pid ~model ~prover in
let logerr = DISK.file_logerr ~pid ~model ~prover in
let id = WpPropId.get_propid pid in
let title = Pretty_utils.to_string WpPropId.pretty pid in
let lines = WpContext.with_model model
let lines = WpContext.on_context context
(assemble_goal ~file ~id ~title ~axioms) prop in
if Wp_parameters.has_print_generated () then
WpContext.with_model model (fun () ->
WpContext.on_context context (fun () ->
let goal = cluster ~id ~title () in
Wp_parameters.print_generated (cluster_file goal)
) () ;
......@@ -490,36 +491,36 @@ let prove_prop ~config ~pid ~mode ~model ~axioms ~prop =
then Task.return VCS.no_result
else prove_file ~config ~pid ~mode ~file ~lines ~logout ~logerr
let prove_annot model pid vcq ~config ~mode =
let prove_annot context pid vcq ~config ~mode =
Task.todo
begin fun () ->
let axioms = vcq.VC_Annot.axioms in
let prop = GOAL.compute_proof vcq.VC_Annot.goal in
prove_prop ~pid ~config ~mode ~model ~axioms ~prop
prove_prop ~pid ~config ~mode ~context ~axioms ~prop
end
let prove_lemma model pid vca ~config ~mode =
let prove_lemma context pid vca ~config ~mode =
Task.todo
begin fun () ->
let lemma = vca.Wpo.VC_Lemma.lemma in
let depends = vca.Wpo.VC_Lemma.depends in
let prop = F.p_forall lemma.l_forall lemma.l_lemma in
let axioms = Some(lemma.l_cluster,depends) in
prove_prop ~pid ~config ~mode ~model ~axioms ~prop
prove_prop ~pid ~config ~mode ~context ~axioms ~prop
end
let prove_check model pid vck ~config ~mode =
let prove_check context pid vck ~config ~mode =
Task.todo
begin fun () ->
let prop = vck.VC_Check.goal in
let axioms = None in
prove_prop ~pid ~config ~mode ~model ~axioms ~prop
prove_prop ~pid ~config ~mode ~context ~axioms ~prop
end
let prove ~config ~mode wpo =
let pid = wpo.Wpo.po_pid in
let model = wpo.Wpo.po_model in
let context = Wpo.get_context wpo in
match wpo.Wpo.po_formula with
| Wpo.GoalAnnot vcq -> prove_annot model pid vcq ~config ~mode
| Wpo.GoalLemma vca -> prove_lemma model pid vca ~config ~mode
| Wpo.GoalCheck vck -> prove_check model pid vck ~config ~mode
| Wpo.GoalAnnot vcq -> prove_annot context pid vcq ~config ~mode
| Wpo.GoalLemma vca -> prove_lemma context pid vca ~config ~mode
| Wpo.GoalCheck vck -> prove_check context pid vck ~config ~mode
......@@ -84,8 +84,8 @@ let jfork tree ?node jtactic =
try
let anchor = ProofEngine.anchor tree ?node () in
let goal = ProofEngine.goal anchor in
let model = ProofEngine.node_model anchor in
match WpContext.with_model model (jconfigure console jtactic) goal with
let ctxt = ProofEngine.node_context anchor in
match WpContext.on_context ctxt (jconfigure console jtactic) goal with
| None -> None
| Some (script,process) ->
Some (ProofEngine.fork tree ~anchor script process)
......
......@@ -44,8 +44,8 @@ let fork tree anchor strategy =
~pool:(ProofEngine.pool tree)
~title:strategy.tactical#title in
try
let model = ProofEngine.node_model anchor in
match WpContext.with_model model (configure console) strategy with
let context = ProofEngine.node_context anchor in
match WpContext.on_context context (configure console) strategy with
| None -> None
| Some (script,process) ->
Some (ProofEngine.fork tree ~anchor script process)
......@@ -91,8 +91,8 @@ let search tree ?anchor ?sequent heuristics =
match sequent with
| Some s -> s | None -> snd (Wpo.compute (ProofEngine.goal anchor)) in
let lookup h = try h#search pool#add sequent with Not_found -> () in
WpContext.with_model
(ProofEngine.node_model anchor)
WpContext.on_context
(ProofEngine.node_context anchor)
(List.iter lookup) heuristics ;
first tree ~anchor pool#sort
......
......@@ -652,8 +652,8 @@ class visitor (ctx:context) c =
Log.print_on_output
begin fun fmt ->
Format.fprintf fmt "---------------------------------------------@\n" ;
Format.fprintf fmt "--- Model '%s' Cluster '%s' @\n"
(WpContext.get_id (WpContext.get_model ())) name;
Format.fprintf fmt "--- Context '%s' Cluster '%s' @\n"
(WpContext.get_context () |> WpContext.S.id) name;
Format.fprintf fmt "---------------------------------------------@\n" ;
Why3.Pretty.print_theory fmt th;
end ;
......@@ -1076,7 +1076,7 @@ let prove ?timeout ?steplimit ~prover wpo =
else Task.return VCS.no_result
else call_prover ~timeout ~steplimit prover task wpo
in
WpContext.with_model wpo.Wpo.po_model do_ ()
WpContext.on_context (Wpo.get_context wpo) do_ ()
with exn ->
let bt = Printexc.get_raw_backtrace () in
Wp_parameters.fatal "Error in why3:%a@.%s@."
......
......@@ -62,7 +62,7 @@ class browser ?on_cluster f cluster =
end
let browse f s =
if WpContext.is_model_defined () then
if WpContext.is_defined () then
begin
let main = Definitions.cluster ~id:"browser" () in
let visitor = new browser f main in
......
......@@ -30,6 +30,8 @@ type t = Wpo.t
let get_id = Wpo.get_gid
let get_model = Wpo.get_model
let get_scope = Wpo.get_scope
let get_context = Wpo.get_context
let get_description = Wpo.get_label
let get_property = Wpo.get_property
let get_sequent w = snd (Wpo.compute w)
......@@ -45,7 +47,7 @@ let get_formula po =
| GoalCheck c -> c.VC_Check.goal
| GoalLemma l -> l.VC_Lemma.lemma.Definitions.l_lemma
| GoalAnnot { VC_Annot.goal = g } ->
WpContext.with_model po.po_model Wpo.GOAL.compute_proof g
WpContext.on_context (get_context po) Wpo.GOAL.compute_proof g
let clear = Wpo.clear
let proof = Wpo.goals_of_property
......
......@@ -31,7 +31,9 @@ open VCS
type t (** elementary proof obligation *)
val get_id : t -> string
val get_model : t -> WpContext.t
val get_model : t -> WpContext.model
val get_scope : t -> WpContext.scope
val get_context : t -> WpContext.context
val get_description : t -> string
val get_property : t -> Property.t
val get_result : t -> prover -> result
......
......@@ -1315,7 +1315,7 @@ struct
let provers_wpo =
Bag.map (make_oblig index pid) group.verifs
in
let mid = WpContext.get_id model in
let mid = WpContext.MODEL.id model in
let group =
if is_empty group.trivial then
if Bag.is_empty provers_wpo
......@@ -1361,7 +1361,7 @@ struct
let index = match LogicUsage.section_of_lemma l.lem_name with
| LogicUsage.Toplevel _ -> Wpo.Axiomatic None
| LogicUsage.Axiomatic a -> Wpo.Axiomatic (Some a.ax_name) in
let mid = WpContext.get_id model in
let mid = WpContext.MODEL.id model in
let sid = WpPropId.get_propid id in
let leg = WpPropId.get_legacy id in
let wpo = {
......@@ -1414,12 +1414,12 @@ struct
module VCG = VC(M)
module WP = Calculus.Cfg(VCG)
class wp (m:WpContext.t) =
class wp (model:WpContext.model) =
object
val mutable lemmas : LogicUsage.logic_lemma Bag.t = Bag.empty
val mutable annots : WpStrategy.strategy Bag.t = Bag.empty
method lemma = true
method model = m
method model = model
method add_lemma lemma = lemmas <- Bag.append lemmas lemma
method add_strategy strategy = annots <- Bag.append annots strategy
method compute : Wpo.t Bag.t =
......@@ -1428,41 +1428,39 @@ struct
Lang.F.release () ;
Datatype.String.Set.iter Lang.F.Check.set
(Wp_parameters.QedChecks.get ()) ;
WpContext.on_model m
WpContext.on_context (model,WpContext.Global)
begin fun () ->
WpContext.on_global
(fun () ->
LogicUsage.iter_lemmas VCG.compile_lemma ;
Bag.iter (VCG.prove_lemma collection) lemmas ;
) ;
Bag.iter
(fun strategy ->
let cfg = WpStrategy.cfg_of_strategy strategy in
let kf = WpStrategy.get_kf strategy in
WpContext.on_kf kf
begin fun () ->
let bhv = WpStrategy.get_bhv strategy in
let index = Wpo.Function( kf , bhv ) in
if WpRTE.missing_guards kf m then
Wp_parameters.warning ~current:false ~once:true
"Missing RTE guards" ;
try
let (results,_) = WP.compute cfg strategy in
List.iter (VCG.compile collection index) results
with Warning.Error(source,reason) ->
Wp_parameters.failure
~current:false "From %s: %s" source reason
end
) annots ;
if not (Lang.F.Check.is_set ()) then
begin
Wp_parameters.feedback ~ontty:`Transient "Collecting checks" ;
Bag.iter
(fun w -> ignore (Wpo.reduce w))
!collection ;
Lang.F.Check.iter (add_qed_check collection m) ;
end
end ;
LogicUsage.iter_lemmas VCG.compile_lemma ;
Bag.iter (VCG.prove_lemma collection) lemmas ;
end () ;
Bag.iter
(fun strategy ->
let cfg = WpStrategy.cfg_of_strategy strategy in
let kf = WpStrategy.get_kf strategy in
WpContext.on_context (model,WpContext.Kf kf)
begin fun () ->
let bhv = WpStrategy.get_bhv strategy in
let index = Wpo.Function( kf , bhv ) in
if WpRTE.missing_guards model kf then
Wp_parameters.warning ~current:false ~once:true
"Missing RTE guards" ;
try
let (results,_) = WP.compute cfg strategy in
List.iter (VCG.compile collection index) results
with Warning.Error(source,reason) ->
Wp_parameters.failure
~current:false "From %s: %s" source reason
end ()
) annots ;
if not (Lang.F.Check.is_set ()) then
WpContext.on_context (model,WpContext.Global)
begin fun () ->
Wp_parameters.feedback ~ontty:`Transient "Collecting checks" ;
Bag.iter
(fun w -> ignore (Wpo.reduce w))
!collection ;
Lang.F.Check.iter (add_qed_check collection model) ;
end () ;
lemmas <- Bag.empty ;
annots <- Bag.empty ;
Lang.F.Check.reset () ;
......@@ -1474,7 +1472,7 @@ struct
end
(* Cache because computer functors can not be instantiated twice *)
module COMPUTERS = WpContext.Hash
module COMPUTERS = Hashtbl.Make(WpContext.MODEL)
let computers = COMPUTERS.create 1
let computer setup driver =
......
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