https://github.com/EasyCrypt/easycrypt
Tip revision: a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC
Fix bug w.r.t. _tools presence detection.
Fix bug w.r.t. _tools presence detection.
Tip revision: a79f9ae
ecHiTacticals.ml
(* Copyright (c) - 2012-2014 - IMDEA Software Institute and INRIA
* Distributed under the terms of the CeCILL-B license *)
(* -------------------------------------------------------------------- *)
open EcUtils
open EcLocation
open EcParsetree
open EcFol
open EcCoreGoal
open EcCoreGoal.FApi
open EcHiGoal
module TTC = EcProofTyping
(* -------------------------------------------------------------------- *)
let rec process1_debug (_ttenv : ttenv) (tc : tcenv1) =
FApi.tcenv_of_tcenv1 tc
(* -------------------------------------------------------------------- *)
and process1_by (ttenv : ttenv) (t : ptactic list option) (tc : tcenv1) =
t_onall process_done (process1_seq ttenv (odfl [] t) tc)
(* -------------------------------------------------------------------- *)
and process1_do (ttenv : ttenv) (b, n) (t : ptactic_core) (tc : tcenv1) =
FApi.t_do b n (process1_core ttenv t) tc
(* -------------------------------------------------------------------- *)
and process1_or (ttenv : ttenv) (t1 : ptactic) (t2 : ptactic) (tc : tcenv1) =
let t1 = process1 ttenv t1 in
let t2 = process1 ttenv t2 in
t_or t1 t2 tc
(* -------------------------------------------------------------------- *)
and process1_try (ttenv : ttenv) (t : ptactic_core) (tc : tcenv1) =
FApi.t_try (process1_core ttenv t) tc
(* -------------------------------------------------------------------- *)
and process1_admit (_ : ttenv) (tc : tcenv1) =
(* FIXME: use notifier *)
EcFortune.pick () |> oiter (fun msg -> Printf.printf "[W] %s\n%!" msg);
EcLowGoal.t_admit tc
(* -------------------------------------------------------------------- *)
and process1_idtac (_ : ttenv) (_msg : string option) (tc : tcenv1) =
EcLowGoal.t_id tc
(* -------------------------------------------------------------------- *)
and process1_case (_ : ttenv) gp (tc : tcenv1) =
let form_of_gp () =
match gp with
| [`Form (occ, pf)] -> begin
match occ with
| None -> pf
| Some _ -> tc_error !!tc "cannot specify an occurence selector"
end
| _ -> tc_error !!tc "must give exactly one boolean formula"
in
match (FApi.tc1_goal tc).f_node with
| FbdHoareS _ | FhoareS _ ->
let fp = TTC.tc1_process_phl_formula tc (form_of_gp ()) in
EcPhlCase.t_hl_case fp tc
| FequivS _ ->
let fp = TTC.tc1_process_prhl_formula tc (form_of_gp ()) in
EcPhlCase.t_equiv_case fp tc
| _ -> EcHiGoal.process_case gp tc
(* -------------------------------------------------------------------- *)
and process1_progress (ttenv : ttenv) options t (tc : tcenv1) =
let t = t |> omap (process1_core ttenv) |> odfl EcLowGoal.t_id in
let options =
EcLowGoal.PGOptions.merge
EcLowGoal.PGOptions.default
options
in EcLowGoal.t_progress ~options t tc
(* -------------------------------------------------------------------- *)
and process1_seq (ttenv : ttenv) (ts : ptactic list) (tc : tcenv1) =
let rec aux ts (tc : tcenv) : tcenv =
match ts with
| [] -> tc
| t :: ts -> aux ts (process ttenv t tc)
in
aux ts (tcenv_of_tcenv1 tc)
(* -------------------------------------------------------------------- *)
and process1_logic (ttenv : ttenv) (t : logtactic) (tc : tcenv1) =
let engine = process1_core ttenv in
let tx =
match t with
| Preflexivity -> process_reflexivity
| Passumption -> process_assumption
| Psmt pi -> process_smt ttenv pi
| Pintro pi -> process_intros pi
| Psplit -> process_split
| Pfield st -> process_algebra `Solve `Field st
| Pring st -> process_algebra `Solve `Ring st
| Palg_norm -> EcStrongRing.t_alg_eq
| Pexists fs -> process_exists fs
| Pleft -> process_left
| Pright -> process_right
| Pcongr -> process_congr
| Ptrivial -> process_trivial
| Pelim pe -> process_elim pe
| Papply pe -> process_apply pe
| Pcut (ip, f, t) -> process_cut engine (ip, f, t)
| Pcutdef (ip, f) -> process_cutdef (ip, f)
| Pgeneralize l -> process_generalize l
| Pclear l -> process_clear l
| Prewrite ri -> process_rewrite ttenv ri
| Psubst ri -> process_subst ri
| Psimplify ri -> process_simplify ri
| Pchange pf -> process_change pf
| Ppose (x, o, p) -> process_pose x o p
| _ -> assert false
in
tx tc
(* -------------------------------------------------------------------- *)
and process1_phl (_ : ttenv) (t : phltactic) (tc : tcenv1) =
let (tx : tcenv1 -> tcenv) =
match t with
| Pfun `Def -> EcPhlFun.process_fun_def
| Pfun (`Abs f) -> EcPhlFun.process_fun_abs f
| Pfun (`Upto info) -> EcPhlFun.process_fun_upto info
| Pfun `Code -> EcPhlFun.process_fun_to_code
| Pskip -> EcPhlSkip.t_skip
| Papp (dir, k, phi, f) -> EcPhlApp.process_app dir k phi f
| Pwp wp -> EcPhlWp.t_wp wp
| Psp sp -> EcPhlSp.t_sp sp
| Prcond (side, b, i) -> EcPhlRCond.t_rcond side b i
| Pcond side -> EcPhlCond.process_cond side
| Pwhile (side, info) -> curry3 (EcPhlWhile.process_while side) info
| Pfission info -> EcPhlLoopTx.process_fission info
| Pfusion info -> EcPhlLoopTx.process_fusion info
| Punroll info -> EcPhlLoopTx.process_unroll info
| Psplitwhile info -> EcPhlLoopTx.process_splitwhile info
| Pcall (side, info) -> EcPhlCall.process_call side info
| Pswap sw -> EcPhlSwap.process_swap sw
| Pinline info -> EcPhlInline.process_inline info
| Pcfold info -> EcPhlCodeTx.process_cfold info
| Pkill info -> EcPhlCodeTx.process_kill info
| Palias info -> EcPhlCodeTx.process_alias info
| Pset info -> EcPhlCodeTx.process_set info
| Prnd (side, info) -> EcPhlRnd.process_rnd side info
| Pconseq (nm, info) -> EcPhlConseq.process_conseq nm info
| Phr_exists_elim -> EcPhlExists.t_hr_exists_elim
| Phr_exists_intro fs -> EcPhlExists.process_exists_intro fs
| Pexfalso -> EcPhlAuto.t_exfalso
| Pbydeno (mode, info) -> EcPhlDeno.process_deno mode info
| PPr pr -> EcPhlPr.process_ppr pr
| Pfel (pos, info) -> EcPhlFel.process_fel pos info
| Phoare -> EcPhlBdHoare.t_hoare_bd_hoare
| Pbdhoare_split i -> EcPhlBdHoare.process_bdhoare_split i
| Pprbounded -> EcPhlPr.t_prbounded true
| Psim info -> EcPhlEqobs.process_eqobs_in info
| Ptrans_stmt info -> EcPhlTrans.process_equiv_trans info
| Psymmetry -> EcPhlSym.t_equiv_sym
| Peager_seq infos -> curry3 EcPhlEager.process_seq infos
| Peager_if -> EcPhlEager.process_if
| Peager_while info -> EcPhlEager.process_while info
| Peager_fun_def -> EcPhlEager.process_fun_def
| Peager_fun_abs infos -> curry EcPhlEager.process_fun_abs infos
| Peager_call info -> EcPhlEager.process_call info
| Peager infos -> curry EcPhlEager.process_eager infos
| Pbd_equiv (nm, f1, f2) -> EcPhlConseq.process_bd_equiv nm (f1, f2)
| Pauto -> EcPhlAuto.t_auto
in tx tc
(* -------------------------------------------------------------------- *)
and process_sub (ttenv : ttenv) tts tc =
let count = FApi.tc_count tc in
let ntacs = List.length tts in
if count <> ntacs then
tc_error !$tc "expecting %d tactic(s), got %d" count ntacs;
FApi.t_sub (List.map (process1 ttenv) tts) tc
(* -------------------------------------------------------------------- *)
and process_expect (ttenv : ttenv) (t, n) tc =
if FApi.tc_count tc <> n then
tc_error !$tc "expecting exactly %d subgoal(s)" n;
FApi.t_onall (process1 ttenv t) tc
(* -------------------------------------------------------------------- *)
and process_firsts (ttenv : ttenv) (t, i) tc =
let count = FApi.tc_count tc in
if i > count then
tc_error !$tc "expecting at least %d subgoal(s)" i;
FApi.t_firsts (process1 ttenv t) i tc
(* -------------------------------------------------------------------- *)
and process_lasts (ttenv : ttenv) (t, i) tc =
let count = FApi.tc_count tc in
if i > count then
tc_error !$tc "expecting at least %d subgoal(s)" i;
FApi.t_lasts (process1 ttenv t) i tc
(* -------------------------------------------------------------------- *)
and process_rotate (_ttenv : ttenv) (d, i) tc =
FApi.t_rotate d i tc
(* -------------------------------------------------------------------- *)
and process_chain (ttenv : ttenv) (t : ptactic_chain) (tc : tcenv) =
match t with
| Psubtacs tactics -> process_sub ttenv tactics tc
| Pfirst (t, i) -> process_firsts ttenv (t, i) tc
| Plast (t, i) -> process_lasts ttenv (t, i) tc
| Protate (d, i) -> process_rotate ttenv (d, i) tc
| Pexpect (t, n) -> process_expect ttenv (t, n) tc
(* -------------------------------------------------------------------- *)
and process_core (ttenv : ttenv) (t : ptactic_core) (tc : tcenv) =
let tactic =
match unloc t with
| Pidtac msg -> `One (process1_idtac ttenv msg)
| Padmit -> `One (process1_admit ttenv)
| Plogic t -> `One (process1_logic ttenv t)
| PPhl t -> `One (process1_phl ttenv t)
| Pby t -> `One (process1_by ttenv t)
| Pdo ((b, n), t) -> `One (process1_do ttenv (b, n) t)
| Ptry t -> `One (process1_try ttenv t)
| Por (t1, t2) -> `One (process1_or ttenv t1 t2)
| Pseq ts -> `One (process1_seq ttenv ts)
| Pcase es -> `One (process1_case ttenv es)
| Pprogress (o, t) -> `One (process1_progress ttenv o t)
| Pdebug -> `One (process1_debug ttenv)
| Psubgoal tt -> `All (process_chain ttenv tt)
in
(match tactic with `One t -> t_onall t | `All t -> t) tc
(* -------------------------------------------------------------------- *)
and process (ttenv : ttenv) (t : ptactic) (tc : tcenv) =
let cf =
match unloc t.pt_core with
| Plogic Pintro _
| Plogic (Prewrite _)
| Plogic (Pgeneralize _ )
| Pidtac _ -> true
| _ -> false
in
let tc = process_core ttenv t.pt_core tc in
let tc = EcHiGoal.process_mintros ~cf t.pt_intros tc in
tc
(* -------------------------------------------------------------------- *)
and process1_core (ttenv : ttenv) (t : ptactic_core) (tc : tcenv1) =
process_core ttenv t (tcenv_of_tcenv1 tc)
(* -------------------------------------------------------------------- *)
and process1 (ttenv : ttenv) (t : ptactic) (tc : tcenv1) =
process ttenv t (tcenv_of_tcenv1 tc)
(* -------------------------------------------------------------------- *)
let process (ttenv : ttenv) (t : ptactic list) (pf : proof) =
let tc = tcenv1_of_proof pf in
proof_of_tcenv (process1_seq ttenv t tc)