https://github.com/EasyCrypt/easycrypt
Tip revision: f47fb5394d471bb609b84ab7140bc0164d1fa2a3 authored by Cécile BARITEL-RUET on 26 November 2019, 07:51:24 UTC
better with the files
better with the files
Tip revision: f47fb53
ecCommands.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcUtils
open EcLocation
open EcParsetree
module Sid = EcIdent.Sid
module Mx = EcPath.Mx
(* -------------------------------------------------------------------- *)
exception Restart
(* -------------------------------------------------------------------- *)
type pragma = {
pm_verbose : bool; (* true => display goal after each command *)
pm_g_prall : bool; (* true => display all open goals *)
pm_check : [`Check | `WeakCheck | `Report];
}
let dpragma = {
pm_verbose = true ;
pm_g_prall = false ;
pm_check = `Check;
}
let pragma = ref dpragma
let pragma_verbose (b : bool) =
pragma := { !pragma with pm_verbose = b; }
let pragma_g_prall (b : bool) =
pragma := {!pragma with pm_g_prall = b; }
let pragma_check mode =
pragma := { !pragma with pm_check = mode; }
module Pragmas = struct
let silent = "silent"
let verbose = "verbose"
module Proofs = struct
let check = "Proofs:check"
let weak = "Proofs:weak"
let report = "Proofs:report"
end
module Goals = struct
let printall = "Goals:printall"
let printone = "Goals:printone"
end
end
exception InvalidPragma of string
let apply_pragma (x : string) =
match x with
| x when x = Pragmas.silent -> pragma_verbose false
| x when x = Pragmas.verbose -> pragma_verbose true
| x when x = Pragmas.Proofs.check -> pragma_check `Check
| x when x = Pragmas.Proofs.weak -> pragma_check `WeakCheck
| x when x = Pragmas.Proofs.report -> pragma_check `Report
| x when x = Pragmas.Goals.printone -> pragma_g_prall false
| x when x = Pragmas.Goals.printall -> pragma_g_prall true
| _ -> raise (InvalidPragma x)
(* -------------------------------------------------------------------- *)
module Loader : sig
type loader
type kind = EcLoader.kind
type idx_t = EcLoader.idx_t
val create : unit -> loader
val forsys : loader -> loader
val dup : loader -> loader
val addidir : ?system:bool -> ?recursive:bool -> string -> loader -> unit
val aslist : loader -> ((bool * string) * idx_t) list
val locate : ?onlysys:bool -> string -> loader -> (string * kind) option
val push : string -> loader -> unit
val pop : loader -> string option
val context : loader -> string list
val incontext : string -> loader -> bool
end = struct
type loader = {
(*---*) ld_core : EcLoader.ecloader;
mutable ld_stack : string list;
}
type kind = EcLoader.kind
type idx_t = EcLoader.idx_t
module Path = BatPathGen.OfString
let norm p =
try Path.s (Path.normalize_in_tree (Path.p p))
with Path.Malformed_path -> p
let create () =
{ ld_core = EcLoader.create ();
ld_stack = []; }
let forsys (ld : loader) =
{ ld_core = EcLoader.forsys ld.ld_core;
ld_stack = ld.ld_stack; }
let dup (ld : loader) =
{ ld_core = EcLoader.dup ld.ld_core;
ld_stack = ld.ld_stack; }
let addidir ?system ?recursive (path : string) (ld : loader) =
EcLoader.addidir ?system ?recursive path ld.ld_core
let aslist (ld : loader) =
EcLoader.aslist ld.ld_core
let locate ?onlysys (path : string) (ld : loader) =
EcLoader.locate ?onlysys path ld.ld_core
let push (p : string) (ld : loader) =
ld.ld_stack <- norm p :: ld.ld_stack
let pop (ld : loader) =
match ld.ld_stack with
| [] -> None
| p :: tl -> ld.ld_stack <- tl; Some p
let context (ld : loader) =
ld.ld_stack
let incontext (p : string) (ld : loader) =
List.mem (norm p) ld.ld_stack
end
(* -------------------------------------------------------------------- *)
let process_search scope qs =
EcScope.Search.search scope qs
(* -------------------------------------------------------------------- *)
module HiPrinting = struct
let pr_glob fmt env pm =
let ppe = EcPrinting.PPEnv.ofenv env in
let (p, _) = EcTyping.trans_msymbol env pm in
let us = EcEnv.NormMp.mod_use env p in
Format.fprintf fmt "Globals [# = %d]:@."
(Sid.cardinal us.EcEnv.us_gl);
Sid.iter (fun id ->
Format.fprintf fmt " %s@." (EcIdent.name id))
us.EcEnv.us_gl;
Format.fprintf fmt "@.";
Format.fprintf fmt "Prog. variables [# = %d]:@."
(Mx.cardinal us.EcEnv.us_pv);
List.iter (fun (xp,_) ->
let pv = EcTypes.pv_glob xp in
let ty = EcEnv.Var.by_xpath xp env in
Format.fprintf fmt " @[%a : %a@]@."
(EcPrinting.pp_pv ppe) pv
(EcPrinting.pp_type ppe) ty.EcEnv.vb_type)
(List.rev (Mx.bindings us.EcEnv.us_pv))
let pr_goal fmt scope n =
match EcScope.xgoal scope with
| None | Some { EcScope.puc_active = None} ->
EcScope.hierror "no active proof"
| Some { EcScope.puc_active = Some (puc, _) } -> begin
match puc.EcScope.puc_jdg with
| EcScope.PSNoCheck -> ()
| EcScope.PSCheck pf -> begin
let hds = EcCoreGoal.all_hd_opened pf in
let sz = List.length hds in
let ppe = EcPrinting.PPEnv.ofenv (EcScope.env scope) in
if n > sz then
EcScope.hierror "only %n goal(s) remaining" sz;
if n <= 0 then
EcScope.hierror "goal ID must be positive";
let penv = EcCoreGoal.proofenv_of_proof pf in
let goal = List.nth hds (n-1) in
let goal = EcCoreGoal.FApi.get_pregoal_by_id goal penv in
let goal = (EcEnv.LDecl.tohyps goal.EcCoreGoal.g_hyps,
goal.EcCoreGoal.g_concl) in
Format.fprintf fmt "Printing Goal %d\n\n%!" n;
EcPrinting.pp_goal ppe fmt (goal, `One sz)
end
end
end
(* -------------------------------------------------------------------- *)
let process_pr fmt scope p =
let env = EcScope.env scope in
match p with
| Pr_ty qs -> EcPrinting.ObjectInfo.pr_ty fmt env qs.pl_desc
| Pr_op qs -> EcPrinting.ObjectInfo.pr_op fmt env qs.pl_desc
| Pr_pr qs -> EcPrinting.ObjectInfo.pr_op fmt env qs.pl_desc
| Pr_th qs -> EcPrinting.ObjectInfo.pr_th fmt env qs.pl_desc
| Pr_ax qs -> EcPrinting.ObjectInfo.pr_ax fmt env qs.pl_desc
| Pr_mod qs -> EcPrinting.ObjectInfo.pr_mod fmt env qs.pl_desc
| Pr_mty qs -> EcPrinting.ObjectInfo.pr_mty fmt env qs.pl_desc
| Pr_any qs -> EcPrinting.ObjectInfo.pr_any fmt env qs.pl_desc
| Pr_glob pm -> HiPrinting.pr_glob fmt env pm
| Pr_goal n -> HiPrinting.pr_goal fmt scope n
(* -------------------------------------------------------------------- *)
let check_opname_validity (scope : EcScope.scope) (x : string) =
if EcIo.is_binop x = `Invalid then
EcScope.notify scope `Warning
"operator `%s' cannot be used in prefix mode" x;
if EcIo.is_uniop x = `Invalid then
EcScope.notify scope `Warning
"operator `%s' cannot be used in infix mode" x
(* -------------------------------------------------------------------- *)
let process_print scope p =
process_pr Format.std_formatter scope p
(* -------------------------------------------------------------------- *)
exception Pragma of [`Reset | `Restart]
(* -------------------------------------------------------------------- *)
let rec process_type (scope : EcScope.scope) (tyd : ptydecl located) =
EcScope.check_state `InTop "type" scope;
let tyname = (tyd.pl_desc.pty_tyvars, tyd.pl_desc.pty_name) in
let scope =
match tyd.pl_desc.pty_body with
| PTYD_Abstract bd -> EcScope.Ty.add scope (mk_loc tyd.pl_loc tyname) bd
| PTYD_Alias bd -> EcScope.Ty.define scope (mk_loc tyd.pl_loc tyname) bd
| PTYD_Datatype bd -> EcScope.Ty.add_datatype scope (mk_loc tyd.pl_loc tyname) bd
| PTYD_Record bd -> EcScope.Ty.add_record scope (mk_loc tyd.pl_loc tyname) bd
in
EcScope.notify scope `Info "added type: `%s'" (unloc tyd.pl_desc.pty_name);
scope
(* -------------------------------------------------------------------- *)
and process_types (scope : EcScope.scope) tyds =
List.fold_left process_type scope tyds
(* -------------------------------------------------------------------- *)
and process_typeclass (scope : EcScope.scope) (tcd : ptypeclass located) =
EcScope.check_state `InTop "type class" scope;
let scope = EcScope.Ty.add_class scope tcd in
EcScope.notify scope `Info "added type class: `%s'" (unloc tcd.pl_desc.ptc_name);
scope
(* -------------------------------------------------------------------- *)
and process_tycinst (scope : EcScope.scope) (tci : ptycinstance located) =
EcScope.check_state `InTop "type class instance" scope;
EcScope.Ty.add_instance scope (!pragma).pm_check tci
(* -------------------------------------------------------------------- *)
and process_module (scope : EcScope.scope) m =
EcScope.check_state `InTop "module" scope;
EcScope.Mod.add scope m
(* -------------------------------------------------------------------- *)
and process_declare (scope : EcScope.scope) x =
match x with
| PDCL_Module m -> begin
EcScope.check_state `InTop "module" scope;
EcScope.Mod.declare scope m
end
(* -------------------------------------------------------------------- *)
and process_interface (scope : EcScope.scope) (x, i) =
EcScope.check_state `InTop "interface" scope;
EcScope.ModType.add scope x.pl_desc i
(* -------------------------------------------------------------------- *)
and process_operator (scope : EcScope.scope) (pop : poperator located) =
EcScope.check_state `InTop "operator" scope;
let op, scope = EcScope.Op.add scope pop in
let ppe = EcPrinting.PPEnv.ofenv (EcScope.env scope) in
List.iter
(fun { pl_desc = name } ->
EcScope.notify scope `Info "added operator %s %a"
name (EcPrinting.pp_added_op ppe) op;
check_opname_validity scope name)
(pop.pl_desc.po_name :: pop.pl_desc.po_aliases);
scope
(* -------------------------------------------------------------------- *)
and process_predicate (scope : EcScope.scope) (p : ppredicate located) =
EcScope.check_state `InTop "predicate" scope;
let op, scope = EcScope.Pred.add scope p in
let ppe = EcPrinting.PPEnv.ofenv (EcScope.env scope) in
EcScope.notify scope `Info "added predicate %s %a"
(unloc p.pl_desc.pp_name) (EcPrinting.pp_added_op ppe) op;
check_opname_validity scope (unloc p.pl_desc.pp_name);
scope
(* -------------------------------------------------------------------- *)
and process_notation (scope : EcScope.scope) (n : pnotation located) =
EcScope.check_state `InTop "notation" scope;
let scope = EcScope.Notations.add scope n in
EcScope.notify scope `Info "added notation: `%s'"
(unloc n.pl_desc.nt_name);
scope
(* -------------------------------------------------------------------- *)
and process_abbrev (scope : EcScope.scope) (a : pabbrev located) =
EcScope.check_state `InTop "abbreviation" scope;
let scope = EcScope.Notations.add_abbrev scope a in
EcScope.notify scope `Info "added abbrev.: `%s'"
(unloc a.pl_desc.ab_name);
scope
(* -------------------------------------------------------------------- *)
and process_axiom (scope : EcScope.scope) (ax : paxiom located) =
EcScope.check_state `InTop "axiom" scope;
let (name, scope) = EcScope.Ax.add scope (!pragma).pm_check ax in
name |> EcUtils.oiter
(fun x ->
match (unloc ax).pa_kind with
| PAxiom _ -> EcScope.notify scope `Info "added axiom: `%s'" x
| _ -> EcScope.notify scope `Info "added lemma: `%s'" x);
scope
(* -------------------------------------------------------------------- *)
and process_th_open (scope : EcScope.scope) (abs, name) =
EcScope.check_state `InTop "theory" scope;
EcScope.Theory.enter scope (if abs then `Abstract else `Concrete) name
(* -------------------------------------------------------------------- *)
and process_th_close (scope : EcScope.scope) (clears, name) =
let name = unloc name in
EcScope.check_state `InTop "theory closing" scope;
if (fst (EcScope.name scope)) <> name then
EcScope.hierror
"active theory has name `%s', not `%s'"
(fst (EcScope.name scope)) name;
snd (EcScope.Theory.exit ~clears scope)
(* -------------------------------------------------------------------- *)
and process_th_clear (scope : EcScope.scope) clears =
EcScope.check_state `InTop "theory clear" scope;
EcScope.Theory.add_clears clears scope
(* -------------------------------------------------------------------- *)
and process_th_require1 ld scope (x, io) =
EcScope.check_state `InTop "theory require" scope;
let name = x.pl_desc in
match Loader.locate name ld with
| None ->
EcScope.hierror "cannot locate theory `%s'" name
| Some (filename, kind) ->
if Loader.incontext filename ld then
EcScope.hierror "circular requires involving `%s'" name;
let dirname = Filename.dirname filename in
let subld = Loader.dup ld in
Loader.push filename subld;
Loader.addidir dirname subld;
let loader iscope =
let i_pragma = !pragma in
try
let commands = EcIo.parseall (EcIo.from_file filename) in
let commands = List.fold_left (process_internal subld) iscope commands in
pragma := i_pragma; commands
with e ->
pragma := i_pragma; raise e
in
let kind = match kind with `Ec -> `Concrete | `EcA -> `Abstract in
let scope = EcScope.Theory.require scope (name, kind) loader in
match io with
| None -> scope
| Some `Export -> EcScope.Theory.export scope ([], name)
| Some `Import -> EcScope.Theory.import scope ([], name)
(* -------------------------------------------------------------------- *)
and process_th_require ld scope (xs, io) =
List.fold_left
(fun scope x -> process_th_require1 ld scope (x, io))
scope xs
(* -------------------------------------------------------------------- *)
and process_th_import (scope : EcScope.scope) (names : pqsymbol list) =
EcScope.check_state `InTop "theory import" scope;
List.fold_left EcScope.Theory.import scope (List.map unloc names)
(* -------------------------------------------------------------------- *)
and process_th_export (scope : EcScope.scope) (names : pqsymbol list) =
EcScope.check_state `InTop "theory export" scope;
List.fold_left EcScope.Theory.export scope (List.map unloc names)
(* -------------------------------------------------------------------- *)
and process_th_clone (scope : EcScope.scope) thcl =
EcScope.check_state `InTop "theory cloning" scope;
EcScope.Cloning.clone scope (!pragma).pm_check thcl
(* -------------------------------------------------------------------- *)
and process_sct_open (scope : EcScope.scope) name =
EcScope.check_state `InTop "section opening" scope;
EcScope.Section.enter scope name
(* -------------------------------------------------------------------- *)
and process_sct_close (scope : EcScope.scope) name =
EcScope.check_state `InTop "section closing" scope;
EcScope.Section.exit scope name
(* -------------------------------------------------------------------- *)
and process_tactics (scope : EcScope.scope) t =
let mode = !pragma.pm_check in
match t with
| `Actual t -> snd (EcScope.Tactics.process scope mode t)
| `Proof pm -> EcScope.Tactics.proof scope mode pm.pm_strict
(* -------------------------------------------------------------------- *)
and process_save (scope : EcScope.scope) ed =
let (oname, scope) =
match unloc ed with
| `Qed -> EcScope.Ax.save scope
| `Admit -> EcScope.Ax.admit scope
| `Abort -> (None, EcScope.Ax.abort scope)
in
oname |> EcUtils.oiter
(fun x -> EcScope.notify scope `Info "added lemma: `%s'" x);
scope
(* -------------------------------------------------------------------- *)
and process_realize (scope : EcScope.scope) pr =
let mode = !pragma.pm_check in
let (name, scope) = EcScope.Ax.realize scope mode pr in
name |> EcUtils.oiter
(fun x -> EcScope.notify scope `Info "added lemma: `%s'" x);
scope
(* -------------------------------------------------------------------- *)
and process_proverinfo scope pi =
let scope = EcScope.Prover.process scope pi in
scope
(* -------------------------------------------------------------------- *)
and process_pragma (scope : EcScope.scope) opt =
let pragma_check mode =
match EcScope.goal scope with
| Some { EcScope.puc_mode = Some false } ->
EcScope.hierror "pragma [Proofs:*] in non-strict proof script";
| _ -> pragma_check mode
in
match unloc opt with
| x when x = Pragmas.silent -> pragma_verbose false
| x when x = Pragmas.verbose -> pragma_verbose true
| x when x = Pragmas.Proofs.weak -> pragma_check `WeakCheck
| x when x = Pragmas.Proofs.check -> pragma_check `Check
| x when x = Pragmas.Proofs.report -> pragma_check `Report
| x when x = Pragmas.Goals.printall -> pragma_g_prall true
| x when x = Pragmas.Goals.printone -> pragma_g_prall false
| "noop" -> ()
| "compact" -> Gc.compact ()
| "reset" -> raise (Pragma `Reset)
| "restart" -> raise (Pragma `Restart)
| x -> EcScope.notify scope `Warning "unknown pragma: `%s'" x
(* -------------------------------------------------------------------- *)
and process_option (scope : EcScope.scope) (name, value) =
match value with
| `Bool value -> begin
try EcScope.Options.set scope (unloc name) value
with EcScope.UnknownFlag _ ->
EcScope.hierror "unknown option: %s" (unloc name)
end
| (`Int _) as value ->
let gs = EcEnv.gstate (EcScope.env scope) in
EcGState.setvalue (unloc name) value gs; scope
(* -------------------------------------------------------------------- *)
and process_addrw scope (local, base, names) =
EcScope.Auto.add_rw scope ~local ~base names
(* -------------------------------------------------------------------- *)
and process_hint scope hint =
EcScope.Auto.add_hint scope hint
(* -------------------------------------------------------------------- *)
and process_dump_why3 scope filename =
EcScope.dump_why3 scope filename; scope
(* -------------------------------------------------------------------- *)
and process_dump scope (source, tc) =
let open EcCoreGoal in
let input, (p1, p2) = source.tcd_source in
let goals, scope =
let mode = !pragma.pm_check in
EcScope.Tactics.process scope mode tc
in
let wrerror fname =
EcScope.notify scope `Warning "cannot write `%s'" fname in
let tactic =
try File.read_from_file ~offset:p1 ~length:(p2-p1) input
with Invalid_argument _ -> "(* failed to read back script *)" in
let tactic = Printf.sprintf "%s.\n" (String.strip tactic) in
let ecfname = Printf.sprintf "%s.ec" source.tcd_output in
(try File.write_to_file ~output:ecfname tactic
with Invalid_argument _ -> wrerror ecfname);
goals |> oiter (fun (penv, (hd, hds)) ->
let goals =
List.map
(fun hd -> EcCoreGoal.FApi.get_pregoal_by_id hd penv)
(hd :: hds) in
List.iteri (fun i { g_hyps = hyps; g_concl = concl; } ->
let ecfname = Printf.sprintf "%s.%d.ec" source.tcd_output i in
try
let output = open_out_bin ecfname in
try_finally
(fun () ->
let fbuf = Format.formatter_of_out_channel output in
let ppe = EcPrinting.PPEnv.ofenv (EcEnv.LDecl.toenv hyps) in
source.tcd_width |> oiter (Format.pp_set_margin fbuf);
Format.fprintf fbuf "%a@?" (EcPrinting.pp_goal ppe)
((EcEnv.LDecl.tohyps hyps, concl), `One (-1)))
(fun () -> close_out output)
with Sys_error _ -> wrerror ecfname)
goals);
scope
(* -------------------------------------------------------------------- *)
and process_pattern (scope : EcScope.scope) (_p : pat_stmt) =
scope
(* -------------------------------------------------------------------- *)
and process ?(debug = true) (ld : Loader.loader) (scope : EcScope.scope) g =
let loc = g.pl_loc in
EcGState.tmpset "debug" debug (fun () ->
let scope =
match
match g.pl_desc with
| Gtype t -> `Fct (fun scope -> process_types scope (List.map (mk_loc loc) t))
| Gtypeclass t -> `Fct (fun scope -> process_typeclass scope (mk_loc loc t))
| Gtycinstance t -> `Fct (fun scope -> process_tycinst scope (mk_loc loc t))
| Gmodule m -> `Fct (fun scope -> process_module scope m)
| Gdeclare m -> `Fct (fun scope -> process_declare scope m)
| Ginterface i -> `Fct (fun scope -> process_interface scope i)
| Goperator o -> `Fct (fun scope -> process_operator scope (mk_loc loc o))
| Gpredicate p -> `Fct (fun scope -> process_predicate scope (mk_loc loc p))
| Gnotation n -> `Fct (fun scope -> process_notation scope (mk_loc loc n))
| Gabbrev n -> `Fct (fun scope -> process_abbrev scope (mk_loc loc n))
| Gaxiom a -> `Fct (fun scope -> process_axiom scope (mk_loc loc a))
| GthOpen name -> `Fct (fun scope -> process_th_open scope (snd_map unloc name))
| GthClose info -> `Fct (fun scope -> process_th_close scope info)
| GthClear info -> `Fct (fun scope -> process_th_clear scope info)
| GthRequire name -> `Fct (fun scope -> process_th_require ld scope name)
| GthImport name -> `Fct (fun scope -> process_th_import scope name)
| GthExport name -> `Fct (fun scope -> process_th_export scope name)
| GthClone thcl -> `Fct (fun scope -> process_th_clone scope thcl)
| GsctOpen name -> `Fct (fun scope -> process_sct_open scope name)
| GsctClose name -> `Fct (fun scope -> process_sct_close scope name)
| Gprint p -> `Fct (fun scope -> process_print scope p; scope)
| Gsearch qs -> `Fct (fun scope -> process_search scope qs; scope)
| Gtactics t -> `Fct (fun scope -> process_tactics scope t)
| Gtcdump info -> `Fct (fun scope -> process_dump scope info)
| Grealize p -> `Fct (fun scope -> process_realize scope p)
| Gprover_info pi -> `Fct (fun scope -> process_proverinfo scope pi)
| Gsave ed -> `Fct (fun scope -> process_save scope ed)
| Gpragma opt -> `State (fun scope -> process_pragma scope opt)
| Goption opt -> `Fct (fun scope -> process_option scope opt)
| Gaddrw hint -> `Fct (fun scope -> process_addrw scope hint)
| Ghint hint -> `Fct (fun scope -> process_hint scope hint)
| GdumpWhy3 file -> `Fct (fun scope -> process_dump_why3 scope file)
| Gtest p -> `Fct (fun scope -> process_pattern scope p)
with
| `Fct f -> Some (f scope)
| `State f -> f scope; None
in
scope)
() (EcEnv.gstate (EcScope.env scope))
(* -------------------------------------------------------------------- *)
and process_internal ld scope g =
try odfl scope (process ld scope g.gl_action)
with e -> raise (EcScope.toperror_of_exn ~gloc:(loc g.gl_action) e)
(* -------------------------------------------------------------------- *)
let loader = Loader.create ()
let addidir ?system ?recursive (idir : string) =
Loader.addidir ?system ?recursive idir loader
let loadpath () =
List.map fst (Loader.aslist loader)
(* -------------------------------------------------------------------- *)
type checkmode = {
cm_checkall : bool;
cm_timeout : int;
cm_cpufactor : int;
cm_nprovers : int;
cm_provers : string list option;
cm_profile : bool;
cm_iterate : bool;
}
let initial ~checkmode ~boot =
let checkall = checkmode.cm_checkall in
let profile = checkmode.cm_profile in
let poptions = { EcScope.Prover.empty_options with
EcScope.Prover.po_timeout = Some checkmode.cm_timeout;
EcScope.Prover.po_cpufactor = Some checkmode.cm_cpufactor;
EcScope.Prover.po_nprovers = Some checkmode.cm_nprovers;
EcScope.Prover.po_provers = (checkmode.cm_provers, []);
EcScope.Prover.pl_iterate = Some (checkmode.cm_iterate);
} in
let perv = (mk_loc _dummy EcCoreLib.i_Pervasive, Some `Export) in
let tactics = (mk_loc _dummy "Tactics", Some `Export) in
let prelude = (mk_loc _dummy "Logic", Some `Export) in
let loader = Loader.forsys loader in
let gstate = EcGState.from_flags [("profile", profile)] in
let scope = EcScope.empty gstate in
let scope = process_th_require1 loader scope perv in
let scope = if boot then scope else
List.fold_left (process_th_require1 loader)
scope [tactics; prelude] in
let scope = EcScope.Prover.set_default scope poptions in
let scope = if checkall then EcScope.Prover.full_check scope else scope in
EcScope.freeze scope
(* -------------------------------------------------------------------- *)
type context = {
ct_level : int;
ct_current : EcScope.scope;
ct_root : EcScope.scope;
ct_stack : (EcScope.scope list) option;
}
let context = ref (None : context option)
let rootctxt ?(undo = true) (scope : EcScope.scope) =
{ ct_level = 0;
ct_current = scope;
ct_root = scope;
ct_stack = if undo then Some [] else None; }
(* -------------------------------------------------------------------- *)
let pop_context context =
match context.ct_stack with
| None -> EcScope.hierror "undo stack disabled"
| Some stack ->
assert (not (List.is_empty stack));
{ ct_level = context.ct_level - 1;
ct_root = context.ct_root;
ct_current = List.hd stack;
ct_stack = Some (List.tl stack); }
(* -------------------------------------------------------------------- *)
let push_context scope context =
{ ct_level = context.ct_level + 1;
ct_root = context.ct_root;
ct_current = scope;
ct_stack = context.ct_stack
|> omap (fun st -> context.ct_current :: st); }
(* -------------------------------------------------------------------- *)
let initialize ~restart ~undo ~boot ~checkmode =
assert (restart || EcUtils.is_none !context);
if restart then pragma := dpragma;
context := Some (rootctxt ~undo (initial ~checkmode ~boot))
(* -------------------------------------------------------------------- *)
type notifier = EcGState.loglevel -> string Lazy.t -> unit
let addnotifier (notifier : notifier) =
assert (EcUtils.is_some !context);
let gstate = EcScope.gstate (oget !context).ct_root in
ignore (EcGState.add_notifier notifier gstate)
(* -------------------------------------------------------------------- *)
let current () =
(oget !context).ct_current
(* -------------------------------------------------------------------- *)
let uuid () : int =
(oget !context).ct_level
(* -------------------------------------------------------------------- *)
let mode () : string =
match (!pragma).pm_check with
| `Check -> "check"
| `WeakCheck -> "weakcheck"
| `Report -> "report"
(* -------------------------------------------------------------------- *)
let undo (olduuid : int) =
if olduuid < (uuid ()) then
for i = (uuid ()) - 1 downto olduuid do
context := Some (pop_context (oget !context))
done
(* -------------------------------------------------------------------- *)
let reset () =
context := Some (rootctxt (oget !context).ct_root)
(* -------------------------------------------------------------------- *)
let process ?(timed = false) ?debug (g : global_action located) : float option =
let current = oget !context in
let scope = current.ct_current in
try
let (tdelta, oscope) = EcUtils.timed (process ?debug loader scope) g in
oscope |> oiter (fun scope -> context := Some (push_context scope current));
if timed then
EcScope.notify scope `Info "time: %f" tdelta;
Some tdelta
with
| Pragma `Reset -> reset (); None
| Pragma `Restart -> raise Restart
(* -------------------------------------------------------------------- *)
module S = EcScope
module L = EcBaseLogic
let pp_current_goal ?(all = false) stream =
let scope = current () in
match S.xgoal scope with
| None -> ()
| Some { S.puc_active = None; S.puc_cont = ct } ->
Format.fprintf stream "Remaining lemmas to prove:@\n%!";
List.iter
(fun ((_, ax), p, env) ->
let ppe = EcPrinting.PPEnv.ofenv env in
Format.fprintf stream " %s: %a@\n%!"
(EcPath.tostring p)
(EcPrinting.pp_form ppe) ax.EcDecl.ax_spec)
(fst ct)
| Some { S.puc_active = Some (puc, _) } -> begin
match puc.S.puc_jdg with
| S.PSNoCheck -> ()
| S.PSCheck pf -> begin
let ppe = EcPrinting.PPEnv.ofenv (S.env scope) in
match EcCoreGoal.opened pf with
| None -> Format.fprintf stream "No more goals@\n%!"
| Some (n, g) ->
let get_hc { EcCoreGoal.g_hyps; EcCoreGoal.g_concl } =
(EcEnv.LDecl.tohyps g_hyps, g_concl)
in
if all then
let subgoals = EcCoreGoal.all_opened pf in
let subgoals = odfl [] (List.otail subgoals) in
let subgoals = List.map get_hc subgoals in
EcPrinting.pp_goal ppe stream (get_hc g, `All subgoals)
else
EcPrinting.pp_goal ppe stream (get_hc g, `One n)
end
end
let pp_maybe_current_goal stream =
match (!pragma).pm_verbose with
| true -> pp_current_goal ~all:(!pragma).pm_g_prall stream
| false -> ()