https://github.com/EasyCrypt/easycrypt
Revision 36f7f5a29ef730b23ec3b2a96e76e387e90ea0e5 authored by Alley Stoughton on 21 February 2018, 22:32:02 UTC, committed by Pierre-Yves Strub on 26 February 2018, 15:04:53 UTC
The elements of prover [...] have one of the following forms, where s is a string: s (add s to the use-only list) +s (add include s to the include/exclude list) -s (add exclude s to the include/exclude list) The include/exclude list is ordered, so that later instructions can supersede earlier ones. The use-only list was not ordered, but now is. The relative order of the use-only and include/exclude lists is irrelevant, so that, e.g., prover ["Z3" +"Alt-Ergo"] and prover [+"Alt-Ergo" "Z3"] are equivalent. The semantics is that the use-only list is first interpreted (if it's empty, one starts with the current provers as the base), and only then are the instructions of the include/exclude list applied to it, in order. There was already the special use-only instruction "ALL". Now, there is also the use-only instruction "CLEAR", which clears the use-only list, but may be superseded by the use-only instructions that follow. Examples (assuming "Z3" and "Alt-Ergo" are only known provers): prover []. (* a no-op *) prover [+"Z3"] (* adds just "Z3" to whatever current provers are *) prover [-"Z3"] (* removes just "Z3" from whatever current provers are *) prover ["ALL"] (* results in "Z3", "Alt-Ergo" *) prover ["CLEAR"] (* results in nothing *) prover ["CLEAR" +"Z3"] (* results in just "Z3" *) prover [+"Z3" "CLEAR"] (* results in just "Z3" *) prover ["CLEAR" "Z3"] (* result in just "Z3" *) prover ["Z3" "CLEAR"] (* results in nothing *) prover [-"Z3" "ALL"] (* results in "Alt-Ergo" *) prover [+"Z3" "ALL" -"Z3"] (* results in "Alt-Ergo" *) prover [-"Z3" "ALL" +"Z3"] (* results in "Z3", "Alt-Ergo" *)
1 parent 5115c89
Tip revision: 36f7f5a29ef730b23ec3b2a96e76e387e90ea0e5 authored by Alley Stoughton on 21 February 2018, 22:32:02 UTC
Added clean way to clear the list of current provers.
Added clean way to clear the list of current provers.
Tip revision: 36f7f5a
ecHiPredicates.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 EcSymbols
open EcLocation
open EcTypes
open EcCoreFol
open EcParsetree
open EcDecl
module TT = EcTyping
(* -------------------------------------------------------------------- *)
type tperror =
| TPE_Typing of EcTyping.tyerror
| TPE_TyNotClosed
| TPE_DuplicatedConstr of symbol
exception TransPredError of EcLocation.t * EcEnv.env * tperror
let tperror loc env e = raise (TransPredError (loc, env, e))
(* -------------------------------------------------------------------- *)
let close_pr_body (uni : EcUnify.uidmap) (body : prbody) =
let fsubst = EcFol.Fsubst.uni_subst uni in
let tsubst = Tuni.offun uni in
match body with
| PR_Plain body ->
PR_Plain (Fsubst.f_subst fsubst body)
| PR_Ind pri ->
let for1 ctor =
{ prc_ctor = ctor.prc_ctor;
prc_bds = List.map (snd_map (Fsubst.gty_subst fsubst)) ctor.prc_bds;
prc_spec = List.map (Fsubst.f_subst fsubst) ctor.prc_spec; } in
PR_Ind
{ pri_args = List.map (snd_map tsubst) pri.pri_args;
pri_ctors = List.map for1 pri.pri_ctors; }
(* -------------------------------------------------------------------- *)
let trans_preddecl_r (env : EcEnv.env) (pr : ppredicate located) =
let pr = pr.pl_desc and loc = pr.pl_loc in
let ue = TT.transtyvars env (loc, pr.pp_tyvars) in
let tp = TT.tp_relax in
let dom, body =
match pr.pp_def with
| PPabstr ptys ->
(List.map (TT.transty tp env ue) ptys, None)
| PPconcr (bd, pe) ->
let env, xs = TT.trans_binding env ue bd in
let body = TT.trans_prop env ue pe in
let dom = List.map snd xs in
let xs = List.map (fun (x,ty) -> x, EcFol.GTty ty) xs in
let lam = EcFol.f_lambda xs body in
(dom, Some (PR_Plain lam))
| PPind (bd, pi) ->
Msym.odup unloc (List.map (fun c -> c.pic_name) pi) |>
oiter (fun (_, x) ->
tperror x.pl_loc env (TPE_DuplicatedConstr (unloc x)));
let env, xs = TT.trans_binding env ue bd in
let for1 ctor =
let env, bs = TT.trans_gbinding env ue ctor.pic_bds in
let fs = List.map (TT.trans_prop env ue) ctor.pic_spec in
{ prc_ctor = unloc ctor.pic_name;
prc_bds = bs; prc_spec = fs; } in
let prind = { pri_args = xs; pri_ctors = List.map for1 pi; } in
(List.map snd xs, Some (PR_Ind prind))
in
if not (EcUnify.UniEnv.closed ue) then
tperror loc env TPE_TyNotClosed;
let uni = EcUnify.UniEnv.close ue in
let tparams = EcUnify.UniEnv.tparams ue in
let body = body |> omap (close_pr_body uni) in
let dom = List.map (Tuni.offun uni) dom in
EcDecl.mk_pred tparams dom body
(* -------------------------------------------------------------------- *)
let trans_preddecl (env : EcEnv.env) (pr : ppredicate located) =
try trans_preddecl_r env pr
with TT.TyError (loc, env, e) -> tperror loc env (TPE_Typing e)
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...