Revision 0014c65d3e5c46422f6d031123e58ac070d686e7 authored by François Dupressoir on 27 April 2016, 13:20:53 UTC, committed by François Dupressoir on 27 April 2016, 15:06:22 UTC
Some discussion need to be had: - Should we bring everything back to bitstrings? octetstrings? - Should we get rid of those blasted Arrays? (Yes)
1 parent 8db4a56
ecPhlExists.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2016 - Inria
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcUtils
open EcFol
open EcEnv
open EcCoreGoal
open EcLowGoal
open EcLowPhlGoal
module TTC = EcProofTyping
let get_to_gens fs =
let do_id f =
let id =
match f.f_node with
| Fpvar (pv, m) -> id_of_pv pv m
| Fglob (mp, m) -> id_of_mp mp m
| _ -> EcIdent.create "f" in
id, f in
List.map do_id fs
(* -------------------------------------------------------------------- *)
let t_hr_exists_elim_r tc =
let pre = tc1_get_pre tc in
let bd, pre = destr_exists_prenex pre in
(* FIXME: check that bd is not bound in the post *)
let concl = f_forall bd (set_pre ~pre (FApi.tc1_goal tc)) in
FApi.xmutate1 tc `HlExists [concl]
(* -------------------------------------------------------------------- *)
let t_hr_exists_intro_r fs tc =
let hyps = FApi.tc1_hyps tc in
let concl = FApi.tc1_goal tc in
let pre = tc1_get_pre tc in
let post = tc1_get_post tc in
let side = is_equivS concl || is_equivF concl in
let gen = get_to_gens fs in
let eqs = List.map (fun (id, f) -> f_eq (f_local id f.f_ty) f) gen in
let bd = List.map (fun (id, f) -> (id, GTty f.f_ty)) gen in
let pre = f_exists bd (f_and (f_ands eqs) pre) in
let h = LDecl.fresh_id hyps "h" in
let ms, subst =
match side with
| true ->
let ml, mr = as_seq2 (LDecl.fresh_ids hyps ["&ml"; "&mr"]) in
let s = Fsubst.f_subst_id in
let s = Fsubst.f_bind_mem s mleft ml in
let s = Fsubst.f_bind_mem s mright mr in
([ml; mr], s)
| false ->
let m = LDecl.fresh_id hyps "&m" in
let s = Fsubst.f_subst_id in
let s = Fsubst.f_bind_mem s mhr m in
([m], s)
in
let args =
let do1 (_, f) = PAFormula (Fsubst.f_subst subst f) in
List.map do1 gen
in
let tactic =
FApi.t_seqsub (EcPhlConseq.t_conseq pre post)
[ FApi.t_seqs [
t_intros_i (ms@[h]);
t_exists_intro_s args;
t_apply_hyp h;
];
t_logic_trivial;
t_id]
in
FApi.t_internal tactic tc
(* -------------------------------------------------------------------- *)
let t_hr_exists_elim = FApi.t_low0 "hr-exists-elim" t_hr_exists_elim_r
let t_hr_exists_intro = FApi.t_low1 "hr-exists-intro" t_hr_exists_intro_r
(* -------------------------------------------------------------------- *)
let process_exists_intro fs tc =
let (hyps, concl) = FApi.tc1_flat tc in
let penv =
match concl.f_node with
| FhoareF hf -> fst (LDecl.hoareF hf.hf_f hyps)
| FhoareS hs -> LDecl.push_active hs.hs_m hyps
| FbdHoareF bhf -> fst (LDecl.hoareF bhf.bhf_f hyps)
| FbdHoareS bhs -> LDecl.push_active bhs.bhs_m hyps
| FequivF ef -> fst (LDecl.equivF ef.ef_fl ef.ef_fr hyps)
| FequivS es -> LDecl.push_all [es.es_ml; es.es_mr] hyps
| _ -> tc_error_noXhl ~kinds:hlkinds_Xhl !!tc
in
let fs =
List.map
(fun f -> TTC.pf_process_form_opt !!tc penv None f)
fs
in
t_hr_exists_intro fs tc
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...