https://github.com/EasyCrypt/easycrypt
Tip revision: 03fd7f2c77df23d8f806e8b05d08b20b36f5d9d6 authored by Pierre-Yves Strub on 10 October 2017, 09:04:16 UTC
compile with up-to-date toolchain
compile with up-to-date toolchain
Tip revision: 03fd7f2
ecPhlTAuto.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2016 - Inria
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcFol
open EcCoreGoal
open EcLowPhlGoal
(* -------------------------------------------------------------------- *)
let t_hoare_true_r tc =
match (FApi.tc1_goal tc).f_node with
| FhoareF hf when f_equal hf.hf_po f_true ->
FApi.xmutate1 tc `HoareTrue []
| FhoareS hs when f_equal hs.hs_po f_true ->
FApi.xmutate1 tc `HoareTrue []
| FmuhoareF hf when
f_equal (snd (open_mu_binding (FApi.tc1_env tc) hf.muhf_po)) f_true ->
FApi.xmutate1 tc `HoareTrue []
| FmuhoareS hs when
f_equal (snd (open_mu_binding (FApi.tc1_env tc) hs.muh_po)) f_true ->
FApi.xmutate1 tc `HoareTrue []
| _ ->
tc_error !!tc
"the conclusion is not of the form %s"
"hoare[_ : _ ==> true]"
let t_hoare_true = FApi.t_low0 "hoare-true" t_hoare_true_r
(* -------------------------------------------------------------------- *)
let t_core_exfalso_r tc =
let pre = tc1_get_pre tc in
if not (f_equal pre f_false) then
tc_error !!tc "pre-condition is not `false'";
FApi.xmutate1 tc `ExFalso []
let t_core_exfalso = FApi.t_low0 "core-exfalso" t_core_exfalso_r