https://github.com/EasyCrypt/easycrypt
Tip revision: f7b8664dcf5237042389e655a2e37b09177167f5 authored by Alley Stoughton on 30 June 2021, 15:32:30 UTC
Added Above Threshold and Report Noisy Max examples, which check
Added Above Threshold and Report Noisy Max examples, which check
Tip revision: f7b8664
ecTheoryReplay.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 EcSymbols
open EcUtils
open EcLocation
open EcParsetree
open EcTypes
open EcDecl
open EcModules
open EcTheory
open EcThCloning
module Sp = EcPath.Sp
module Mp = EcPath.Mp
(* ------------------------------------------------------------------ *)
type ovoptions = {
clo_abstract : bool;
}
type 'a ovrenv = {
ovre_ovrd : EcThCloning.evclone;
ovre_rnms : EcThCloning.renaming list;
ovre_ntclr : EcPath.Sp.t;
ovre_opath : EcPath.path;
ovre_npath : EcPath.path;
ovre_prefix : (symbol list) pair;
ovre_glproof : (ptactic_core option * evtags option) list;
ovre_abstract : bool;
ovre_local : bool;
ovre_hooks : 'a ovrhooks;
}
and 'a ovrhooks = {
henv : 'a -> EcEnv.env;
hty : 'a -> ?import:EcTheory.import -> (symbol * tydecl) -> 'a;
hop : 'a -> ?import:EcTheory.import -> (symbol * operator) -> 'a;
hmodty : 'a -> ?import:EcTheory.import -> (symbol * module_sig) -> 'a;
hmod : 'a -> ?import:EcTheory.import -> bool -> module_expr -> 'a;
hax : 'a -> bool -> (symbol * axiom) -> 'a;
hexport : 'a -> EcPath.path -> 'a;
hbaserw : 'a -> symbol -> 'a;
haddrw : 'a -> EcPath.path * EcPath.path list -> 'a;
hauto : 'a -> bool * int * string option * EcPath.path list -> 'a;
htycl : 'a -> symbol * typeclass -> 'a;
hinst : 'a -> (ty_params * ty) * tcinstance -> 'a;
husered : 'a -> (EcPath.path * EcTheory.rule_option * EcTheory.rule option) list -> 'a;
hthenter : 'a -> thmode -> symbol -> 'a;
hthexit : 'a -> [`Full | `ClearOnly | `No] -> 'a;
herr : 'b . ?loc:EcLocation.t -> string -> 'b;
}
(* -------------------------------------------------------------------- *)
let is_inline_mode (mode : clmode) =
match mode with `Inline _ -> true | `Alias -> false
let keep_of_mode (mode : clmode) =
match mode with `Inline `Keep | `Alias -> true | `Inline `Clear -> false
(* -------------------------------------------------------------------- *)
exception Incompatible of incompatible
let tparams_compatible rtyvars ntyvars =
let rlen = List.length rtyvars and nlen = List.length ntyvars in
if rlen <> nlen then
raise (Incompatible (NotSameNumberOfTyParam(rlen,nlen)))
let ty_compatible env ue (rtyvars, rty) (ntyvars, nty) =
tparams_compatible rtyvars ntyvars;
let subst = Tvar.init rtyvars (List.map tvar ntyvars) in
let rty = Tvar.subst subst rty in
try EcUnify.unify env ue rty nty
with EcUnify.UnificationFailure _ ->
raise (Incompatible (DifferentType (rty, nty)))
(* -------------------------------------------------------------------- *)
let error_body exn b = if not b then raise exn
(* -------------------------------------------------------------------- *)
let constr_compatible exn env cs1 cs2 =
error_body exn (List.length cs1 = List.length cs2);
let doit (s1,tys1) (s2,tys2) =
error_body exn (EcSymbols.sym_equal s1 s2);
error_body exn (List.length tys1 = List.length tys2);
List.iter2 (fun ty1 ty2 -> error_body exn (EcReduction.EqTest.for_type env ty1 ty2)) tys1 tys2 in
List.iter2 doit cs1 cs2
let datatype_compatible exn hyps ty1 ty2 =
let env = EcEnv.LDecl.toenv hyps in
constr_compatible exn env ty1.tydt_ctors ty2.tydt_ctors;
error_body exn (EcReduction.is_conv hyps ty1.tydt_schcase ty2.tydt_schcase);
error_body exn (EcReduction.is_conv hyps ty1.tydt_schelim ty2.tydt_schelim)
let record_compatible exn hyps f1 pr1 f2 pr2 =
error_body exn (EcReduction.is_conv hyps f1 f2);
error_body exn (List.length pr1 = List.length pr2);
let env = EcEnv.LDecl.toenv hyps in
let doit (s1,ty1) (s2,ty2) =
error_body exn (EcSymbols.sym_equal s1 s2);
error_body exn (EcReduction.EqTest.for_type env ty1 ty2) in
List.iter2 doit pr1 pr2
let get_open_tydecl hyps p tys =
let tydecl = EcEnv.Ty.by_path p (EcEnv.LDecl.toenv hyps) in
EcSubst.open_tydecl tydecl tys
let rec tybody_compatible exn hyps ty_body1 ty_body2 =
match ty_body1, ty_body2 with
| `Abstract _, `Abstract _ -> () (* FIXME Sp.t *)
| `Concrete ty1 , `Concrete ty2 -> error_body exn (EcReduction.EqTest.for_type (EcEnv.LDecl.toenv hyps) ty1 ty2)
| `Datatype ty1 , `Datatype ty2 -> datatype_compatible exn hyps ty1 ty2
| `Record (f1,pr1), `Record(f2,pr2) -> record_compatible exn hyps f1 pr1 f2 pr2
| _, `Concrete {ty_node = Tconstr(p, tys) } ->
let ty_body2 = get_open_tydecl hyps p tys in
tybody_compatible exn hyps ty_body1 ty_body2
| `Concrete{ty_node = Tconstr(p, tys) }, _ ->
let ty_body1 = get_open_tydecl hyps p tys in
tybody_compatible exn hyps ty_body1 ty_body2
| _, _ -> raise exn (* FIXME should we do more for concrete version other *)
let tydecl_compatible env tyd1 tyd2 =
let params = tyd1.tyd_params in
tparams_compatible params tyd2.tyd_params;
let tparams = List.map (fun (id,_) -> tvar id) params in
let ty_body1 = tyd1.tyd_type in
let ty_body2 = EcSubst.open_tydecl tyd2 tparams in
let exn = Incompatible (TyBody(*tyd1,tyd2*)) in
let hyps = EcEnv.LDecl.init env params in
match ty_body1, ty_body2 with
| `Abstract _, _ -> () (* FIXME Sp.t *)
| _, _ -> tybody_compatible exn hyps ty_body1 ty_body2
(* -------------------------------------------------------------------- *)
let expr_compatible exn env s e1 e2 =
let f1 = EcFol.form_of_expr EcFol.mhr e1 in
let f2 = EcFol.Fsubst.f_subst s (EcFol.form_of_expr EcFol.mhr e2) in
error_body exn (EcReduction.is_conv (EcEnv.LDecl.init env []) f1 f2)
let get_open_oper exn env p tys =
let oper = EcEnv.Op.by_path p env in
let _, okind = EcSubst.open_oper oper tys in
match okind with
| OB_oper (Some ob) -> ob
| _ -> raise exn
let rec oper_compatible exn env ob1 ob2 =
match ob1, ob2 with
| OP_Plain(e1,_), OP_Plain(e2,_) ->
expr_compatible exn env EcFol.Fsubst.f_subst_id e1 e2
| OP_Plain({e_node = Eop(p,tys)},_), _ ->
let ob1 = get_open_oper exn env p tys in
oper_compatible exn env ob1 ob2
| _, OP_Plain({e_node = Eop(p,tys)}, _) ->
let ob2 = get_open_oper exn env p tys in
oper_compatible exn env ob1 ob2
| OP_Constr(p1,i1), OP_Constr(p2,i2) ->
error_body exn (EcPath.p_equal p1 p2 && i1 = i2)
| OP_Record p1, OP_Record p2 ->
error_body exn (EcPath.p_equal p1 p2)
| OP_Proj(p1,i11,i12), OP_Proj(p2,i21,i22) ->
error_body exn (EcPath.p_equal p1 p2 && i11 = i21 && i12 = i22)
| OP_Fix f1, OP_Fix f2 ->
opfix_compatible exn env f1 f2
| OP_TC, OP_TC -> ()
| _, _ -> raise exn
and opfix_compatible exn env f1 f2 =
let s = params_compatible exn env EcFol.Fsubst.f_subst_id f1.opf_args f2.opf_args in
error_body exn (EcReduction.EqTest.for_type env f1.opf_resty f2.opf_resty);
error_body exn (f1.opf_struct = f2.opf_struct);
opbranches_compatible exn env s f1.opf_branches f2.opf_branches
and params_compatible exn env s p1 p2 =
error_body exn (List.length p1 = List.length p2);
let doit s (id1,ty1) (id2,ty2) =
error_body exn (EcReduction.EqTest.for_type env ty1 ty2);
EcFol.Fsubst.f_bind_local s id2 (EcFol.f_local id1 ty1) in
List.fold_left2 doit s p1 p2
and opbranches_compatible exn env s ob1 ob2 =
match ob1, ob2 with
| OPB_Leaf(d1,e1), OPB_Leaf(d2,e2) ->
error_body exn (List.length d1 = List.length d2);
let s =
List.fold_left2 (params_compatible exn env) s d1 d2 in
expr_compatible exn env s e1 e2
| OPB_Branch obs1, OPB_Branch obs2 ->
error_body exn (Parray.length obs1 = Parray.length obs2);
Parray.iter2 (opbranch_compatible exn env s) obs1 obs2
| _, _ -> raise exn
and opbranch_compatible exn env s ob1 ob2 =
error_body exn (EcPath.p_equal (fst ob1.opb_ctor) (fst ob2.opb_ctor));
error_body exn (snd ob1.opb_ctor = snd ob2.opb_ctor);
opbranches_compatible exn env s ob1.opb_sub ob2.opb_sub
let get_open_pred exn env p tys =
let oper = EcEnv.Op.by_path p env in
let _, okind = EcSubst.open_oper oper tys in
match okind with
| OB_pred (Some pb) -> pb
| _ -> raise exn
let rec pred_compatible exn env pb1 pb2 =
match pb1, pb2 with
| PR_Plain f1, PR_Plain f2 -> error_body exn (EcReduction.is_conv (EcEnv.LDecl.init env []) f1 f2)
| PR_Plain {f_node = Fop(p,tys)}, _ ->
let pb1 = get_open_pred exn env p tys in
pred_compatible exn env pb1 pb2
| _, PR_Plain {f_node = Fop(p,tys)} ->
let pb2 = get_open_pred exn env p tys in
pred_compatible exn env pb1 pb2
| PR_Ind pr1, PR_Ind pr2 ->
ind_compatible exn env pr1 pr2
| _, _ -> raise exn
and ind_compatible exn env pi1 pi2 =
let s = params_compatible exn env EcFol.Fsubst.f_subst_id pi1.pri_args pi2.pri_args in
error_body exn (List.length pi1.pri_ctors = List.length pi2.pri_ctors);
List.iter2 (prctor_compatible exn env s) pi1.pri_ctors pi2.pri_ctors
and prctor_compatible exn env s prc1 prc2 =
error_body exn (EcSymbols.sym_equal prc1.prc_ctor prc2.prc_ctor);
let env, s = EcReduction.check_bindings exn env s prc1.prc_bds prc2.prc_bds in
error_body exn (List.length prc1.prc_spec = List.length prc2.prc_spec);
let doit f1 f2 =
error_body exn (EcReduction.is_conv (EcEnv.LDecl.init env []) f1 (EcFol.Fsubst.f_subst s f2)) in
List.iter2 doit prc1.prc_spec prc2.prc_spec
let nott_compatible exn env nb1 nb2 =
let s = params_compatible exn env EcFol.Fsubst.f_subst_id nb1.ont_args nb2.ont_args in
(* We do not check ont_resty because it is redundant *)
expr_compatible exn env s nb1.ont_body nb2.ont_body
let operator_compatible env oper1 oper2 =
let open EcDecl in
let params = oper1.op_tparams in
tparams_compatible oper1.op_tparams oper2.op_tparams;
let oty1, okind1 = oper1.op_ty, oper1.op_kind in
let tparams = List.map (fun (id,_) -> tvar id) params in
let oty2, okind2 = EcSubst.open_oper oper2 tparams in
if not (EcReduction.EqTest.for_type env oty1 oty2) then
raise (Incompatible (DifferentType(oty1, oty2)));
let hyps = EcEnv.LDecl.init env params in
let env = EcEnv.LDecl.toenv hyps in
let exn = Incompatible (OpBody(*oper1,oper2*)) in
match okind1, okind2 with
| OB_oper None , OB_oper _ -> ()
| OB_oper (Some ob1), OB_oper (Some ob2) -> oper_compatible exn env ob1 ob2
| OB_pred None , OB_pred _ -> ()
| OB_pred (Some pb1), OB_pred (Some pb2) -> pred_compatible exn env pb1 pb2
| OB_nott nb1 , OB_nott nb2 -> nott_compatible exn env nb1 nb2
| _ , _ -> raise exn
(* -------------------------------------------------------------------- *)
let check_evtags (tags : evtags) (src : symbol list) =
let module E = struct exception Reject end in
try
let dfl = not (List.exists (fun (mode, _) -> mode = `Include) tags) in
let stt =
List.map (fun src ->
let rec do1 status (mode, dst) =
match mode with
| `Exclude -> if sym_equal src dst then raise E.Reject; status
| `Include -> status || (sym_equal src dst)
in List.fold_left do1 dfl tags)
src
in List.mem true stt
with E.Reject -> false
(* -------------------------------------------------------------------- *)
let xpath ove x =
EcPath.pappend ove.ovre_opath
(EcPath.fromqsymbol (fst ove.ovre_prefix, x))
(* -------------------------------------------------------------------- *)
let xnpath ove x =
EcPath.pappend ove.ovre_npath
(EcPath.fromqsymbol (snd ove.ovre_prefix, x))
(* -------------------------------------------------------------------- *)
let string_of_renaming_kind = function
| `Lemma -> "lemma"
| `Op -> "operator"
| `Pred -> "predicate"
| `Type -> "type"
| `Module -> "module"
| `ModType -> "module type"
| `Theory -> "theory"
(* -------------------------------------------------------------------- *)
let rename ove subst (kind, name) =
try
let newname =
List.find_map
(fun rnm -> EcThCloning.rename rnm (kind, name))
ove.ovre_rnms in
let nameok =
match kind with
| `Lemma | `Type ->
EcIo.is_sym_ident newname
| `Op | `Pred ->
EcIo.is_op_ident newname
| `Module | `ModType | `Theory ->
EcIo.is_mod_ident newname
in
if not nameok then
ove.ovre_hooks.herr
(Format.sprintf
"renamings generated an invalid (%s) name: %s -> %s"
(string_of_renaming_kind kind) name newname);
let subst =
EcSubst.add_path subst
~src:(xpath ove name) ~dst:(xnpath ove newname)
in (subst, newname)
with Not_found -> (subst, name)
(* -------------------------------------------------------------------- *)
let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd) =
let scenv = ove.ovre_hooks.henv scope in
match Msym.find_opt x ove.ovre_ovrd.evc_types with
| None ->
let otyd = EcSubst.subst_tydecl subst otyd in
let subst, x = rename ove subst (`Type, x) in
(subst, ops, proofs, ove.ovre_hooks.hty scope ~import (x, otyd))
| Some { pl_desc = (tydov, mode) } -> begin
let newtyd, body =
match tydov with
| `BySyntax (nargs, ntyd) ->
let nargs = List.map2
(fun (_, tc) x -> (EcIdent.create (unloc x), tc))
otyd.tyd_params nargs in
let ue = EcUnify.UniEnv.create (Some nargs) in
let ntyd = EcTyping.transty EcTyping.tp_tydecl scenv ue ntyd in
let decl =
{ tyd_params = nargs;
tyd_type = `Concrete ntyd;
tyd_resolve = otyd.tyd_resolve && (mode = `Alias); }
in (decl, ntyd)
| `ByPath p -> begin
match EcEnv.Ty.by_path_opt p scenv with
| Some reftyd ->
let tyargs = List.map (fun (x, _) -> EcTypes.tvar x) reftyd.tyd_params in
let body = tconstr p tyargs in
let decl =
{ reftyd with
tyd_type = `Concrete body;
tyd_resolve =otyd.tyd_resolve && (mode = `Alias); } in
(decl, body)
| _ -> assert false
end
in
let subst, x =
match mode with
| `Alias ->
rename ove subst (`Type, x)
| `Inline _ ->
let subst =
EcSubst.add_tydef
subst (xpath ove x) (List.map fst newtyd.tyd_params, body) in
let subst =
(* FIXME: HACK *)
match otyd.tyd_type, body.ty_node with
| `Datatype { tydt_ctors = octors }, Tconstr (np, _) -> begin
match (EcEnv.Ty.by_path np scenv).tyd_type with
| `Datatype { tydt_ctors = _ } ->
List.fold_left (fun subst (name, _) ->
EcSubst.add_path subst
~src:(xpath ove name)
~dst:(EcPath.pqoname (EcPath.prefix np) name))
subst octors
| _ -> subst
end
| _, _ -> subst
in
(subst, x) in
let refotyd = EcSubst.subst_tydecl subst otyd in
begin
try tydecl_compatible scenv refotyd newtyd
with Incompatible err ->
clone_error scenv (CE_TyIncompatible ((snd ove.ovre_prefix, x), err))
end;
let scope =
match mode with
| `Alias ->
ove.ovre_hooks.hty scope ~import (x, newtyd)
| `Inline `Keep ->
ove.ovre_hooks.hty scope ~import:EcTheory.noimport (x, newtyd)
| `Inline `Clear ->
scope
in (subst, ops, proofs, scope)
end
(* -------------------------------------------------------------------- *)
and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) =
let scenv = ove.ovre_hooks.henv scope in
match Msym.find_opt x ove.ovre_ovrd.evc_ops with
| None ->
let (subst, x) = rename ove subst (`Op, x) in
let oopd = EcSubst.subst_op subst oopd in
(subst, ops, proofs, ove.ovre_hooks.hop scope ~import (x, oopd))
| Some { pl_desc = (opov, opmode); pl_loc = loc; } ->
let nosmt =
match opov with
| `BySyntax opov -> opov.opov_nosmt
| `ByPath _ -> false in
if nosmt && is_inline_mode opmode then
ove.ovre_hooks.herr ~loc
("operator overriding with nosmt only makes sense with alias mode");
let refop = EcSubst.subst_op subst oopd in
let (reftyvars, refty) = (refop.op_tparams, refop.op_ty) in
let (newop, subst, x, alias) =
let newop, body =
match opov with
| `BySyntax opov ->
let tp = opov.opov_tyvars |> omap (List.map (fun tv -> (tv, []))) in
let ue = EcTyping.transtyvars scenv (loc, tp) in
let tp = EcTyping.tp_relax in
let (ty, body) =
let env = scenv in
let codom = EcTyping.transty tp env ue opov.opov_retty in
let env, xs = EcTyping.trans_binding env ue opov.opov_args in
let body = EcTyping.transexpcast env `InOp ue codom opov.opov_body in
let lam = EcTypes.e_lam xs body in
(lam.EcTypes.e_ty, lam)
in
begin
try ty_compatible scenv ue
(List.map fst reftyvars, refty)
(List.map fst (EcUnify.UniEnv.tparams ue), ty)
with Incompatible err ->
clone_error scenv (CE_OpIncompatible ((snd ove.ovre_prefix, x), err))
end;
if not (EcUnify.UniEnv.closed ue) then
ove.ovre_hooks.herr
~loc "this operator body contains free type variables";
let uni = EcTypes.Tuni.offun (EcUnify.UniEnv.close ue) in
let body = body |> EcTypes.e_mapty uni in
let ty = uni ty in
let tparams = EcUnify.UniEnv.tparams ue in
let newop =
mk_op
~opaque:false ~clinline:(opmode <> `Alias)
tparams ty (Some (OP_Plain (body, nosmt))) in
(newop, body)
| `ByPath p -> begin
match EcEnv.Op.by_path_opt p scenv with
| Some ({ op_kind = OB_oper _ } as refop) ->
let tyargs = List.map (fun (x, _) -> EcTypes.tvar x) refop.op_tparams in
let body =
if refop.op_clinline then
(match refop.op_kind with
| OB_oper (Some (OP_Plain (body, _))) -> body
| _ -> assert false)
else EcTypes.e_op p tyargs refop.op_ty in
let decl =
{ refop with
op_kind = OB_oper (Some (OP_Plain (body, nosmt)));
op_clinline = (opmode <> `Alias) } in
(decl, body)
| _ -> clone_error scenv (CE_UnkOverride(OVK_Operator, EcPath.toqsymbol p))
end
in
match opmode with
| `Alias ->
let subst, x = rename ove subst (`Op, x) in
(newop, subst, x, true)
| `Inline _ ->
let subst1 = (List.map fst newop.op_tparams, body) in
let subst = EcSubst.add_opdef subst (xpath ove x) subst1
in (newop, subst, x, false)
in
let ops =
let opp = EcPath.fromqsymbol (snd ove.ovre_prefix, x) in
Mp.add opp (newop, alias) ops in
begin
try operator_compatible scenv refop newop
with Incompatible err ->
clone_error scenv (CE_OpIncompatible ((snd ove.ovre_prefix, x), err))
end;
let scope =
match opmode with
| `Alias ->
ove.ovre_hooks.hop scope ~import (x, newop)
| `Inline `Keep ->
ove.ovre_hooks.hop scope ~import:EcTheory.noimport (x, newop)
| `Inline `Clear ->
scope
in (subst, ops, proofs, scope)
(* -------------------------------------------------------------------- *)
and replay_prd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopr) =
let scenv = ove.ovre_hooks.henv scope in
match Msym.find_opt x ove.ovre_ovrd.evc_preds with
| None ->
let subst, x = rename ove subst (`Pred, x) in
let oopr = EcSubst.subst_op subst oopr in
(subst, ops, proofs, ove.ovre_hooks.hop ~import scope (x, oopr))
| Some { pl_desc = (prov, prmode); pl_loc = loc; } ->
let refpr = EcSubst.subst_op subst oopr in
let (reftyvars, refty) =
(refpr.op_tparams, refpr.op_ty)
in
let (newpr, subst, x) =
let newpr, body =
match prov with
| `BySyntax prov ->
let tp = prov.prov_tyvars |> omap (List.map (fun tv -> (tv, []))) in
let ue = EcTyping.transtyvars scenv (loc, tp) in
let body =
let env = scenv in
let env, xs = EcTyping.trans_binding env ue prov.prov_args in
let body = EcTyping.trans_form_opt env ue prov.prov_body None in
let xs = List.map (fun (x, ty) -> x, EcFol.GTty ty) xs in
let lam = EcFol.f_lambda xs body in
lam
in
begin
try
ty_compatible scenv ue
(List.map fst reftyvars, refty)
(List.map fst (EcUnify.UniEnv.tparams ue), body.EcFol.f_ty)
with Incompatible err ->
clone_error scenv
(CE_OpIncompatible ((snd ove.ovre_prefix, x), err))
end;
if not (EcUnify.UniEnv.closed ue) then
ove.ovre_hooks.herr
~loc "this predicate body contains free type variables";
let uni = EcUnify.UniEnv.close ue in
let body = EcFol.Fsubst.uni uni body in
let tparams = EcUnify.UniEnv.tparams ue in
let newpr =
{ op_tparams = tparams;
op_ty = body.EcFol.f_ty;
op_kind = OB_pred (Some (PR_Plain body));
op_opaque = oopr.op_opaque;
op_clinline = prmode <> `Alias; } in
(newpr, body)
| `ByPath p -> begin
match EcEnv.Op.by_path_opt p scenv with
| Some ({ op_kind = OB_pred _ } as refop) ->
let tyargs = List.map (fun (x, _) -> EcTypes.tvar x) refop.op_tparams in
let body =
if refop.op_clinline then
(match refop.op_kind with
| OB_pred (Some (PR_Plain body)) -> body
| _ -> assert false)
else EcFol.f_op p tyargs refop.op_ty in
let newpr =
{ refop with
op_kind = OB_pred (Some (PR_Plain body));
op_clinline = (prmode <> `Alias) ; }
in newpr, body
| _ -> clone_error scenv (CE_UnkOverride(OVK_Predicate, EcPath.toqsymbol p))
end
in
match prmode with
| `Alias ->
let subst, x = rename ove subst (`Pred, x) in
(newpr, subst, x)
| `Inline _ ->
let subst1 = (List.map fst newpr.op_tparams, body) in
let subst = EcSubst.add_pddef subst (xpath ove x) subst1 in
(newpr, subst, x)
in
begin
try operator_compatible scenv refpr newpr
with Incompatible err ->
clone_error scenv (CE_OpIncompatible ((snd ove.ovre_prefix, x), err))
end;
let scope =
match prmode with
| `Alias ->
ove.ovre_hooks.hop scope ~import (x, newpr)
| `Inline `Keep ->
ove.ovre_hooks.hop scope ~import:EcTheory.noimport (x, newpr)
| `Inline `Clear ->
scope
in (subst, ops, proofs, scope)
(* -------------------------------------------------------------------- *)
and replay_ntd (ove : _ ovrenv) (subst, ops, proofs, scope) (x, oont) =
match Msym.find_opt x ove.ovre_ovrd.evc_abbrevs with
| None ->
if EcPath.Sp.mem (xpath ove x) ove.ovre_ntclr then
(subst, ops, proofs, scope)
else
let subst, x = rename ove subst (`Op, x) in
let oont = EcSubst.subst_op subst oont in
let scope = ove.ovre_hooks.hop scope (x, oont) in
(subst, ops, proofs, scope)
| Some { pl_desc = (_, mode) } -> begin
match mode with
| `Alias | `Inline `Keep ->
let subst, x = rename ove subst (`Op, x) in
let oont = EcSubst.subst_op subst oont in
let scope = ove.ovre_hooks.hop scope (x, oont) in
(subst, ops, proofs, scope)
| `Inline `Clear ->
(subst, ops, proofs, scope)
end
(* -------------------------------------------------------------------- *)
and replay_axd (ove : _ ovrenv) (subst, ops, proofs, scope) (x, ax) =
let scenv = ove.ovre_hooks.henv scope in
let subst, x = rename ove subst (`Lemma, x) in
let ax = EcSubst.subst_ax subst ax in
let (ax, proofs, axclear) =
if ove.ovre_abstract then (ax, proofs, false) else
let axclear, tags =
match ax.ax_kind with
| `Lemma -> (false, Ssym.empty)
| `Axiom (tags, axc) -> (axc, tags) in
let doproof =
match Msym.find_opt x (ove.ovre_ovrd.evc_lemmas.ev_bynames) with
| Some (pt, hide) -> Some (pt, hide)
| None when is_axiom ax.ax_kind ->
List.Exceptionless.find_map
(function (pt, None) -> Some (pt, `Alias) | (pt, Some pttags) ->
if check_evtags pttags (Ssym.elements tags) then
Some (pt, `Alias)
else None)
ove.ovre_glproof
| _ -> None
in
match doproof with
| None -> (ax, proofs, false)
| Some (pt, hide) ->
let ax = { ax with
ax_kind = `Lemma;
ax_visibility = if hide <> `Alias then `Hidden else ax.ax_visibility
} in
let axc = { axc_axiom = (x, ax);
axc_path = EcPath.fromqsymbol (snd ove.ovre_prefix, x);
axc_tac = pt;
axc_env = scenv; } in
(ax, axc :: proofs, axclear || hide = `Inline `Clear) in
let scope =
if axclear then scope else
ove.ovre_hooks.hax scope ove.ovre_local (x, ax)
in (subst, ops, proofs, scope)
(* -------------------------------------------------------------------- *)
and replay_modtype
(ove : _ ovrenv) (subst, ops, proofs, scope) (x, modty)
=
match Msym.find_opt x ove.ovre_ovrd.evc_modtypes with
| None ->
let subst, x = rename ove subst (`ModType, x) in
let modty = EcSubst.subst_modsig subst modty in
(subst, ops, proofs, ove.ovre_hooks.hmodty scope (x, modty))
| Some { pl_desc = (newname, mode) } ->
let env = ove.ovre_hooks.henv scope in
let np, newmt = EcEnv.ModTy.lookup (unloc newname) env in
let subst, name =
match mode with
| `Alias -> rename ove subst (`Module, x)
| `Inline _ ->
let subst = EcSubst.add_path subst (xpath ove x) np in
subst, x in
let modty = EcSubst.subst_modsig subst modty in
if not (EcReduction.EqTest.for_msig env modty newmt) then
begin
let ppe = EcPrinting.PPEnv.ofenv env in
Format.eprintf "me = %a@."
(EcPrinting.pp_modsig ppe) (np, modty);
Format.eprintf "me = %a@."
(EcPrinting.pp_modsig ppe) (np, newmt);
clone_error env (CE_ModTyIncompatible (snd ove.ovre_prefix, x));
end;
let scope =
if keep_of_mode mode
then ove.ovre_hooks.hmodty scope (name, newmt)
else scope in
(subst, ops, proofs, scope)
(* -------------------------------------------------------------------- *)
and replay_mod
(ove : _ ovrenv) (subst, ops, proofs, scope) me
=
match Msym.find_opt me.me_name ove.ovre_ovrd.evc_modexprs with
| None ->
let subst, name = rename ove subst (`Module, me.me_name) in
let me = EcSubst.subst_module subst me in
let me = { me with me_name = name } in
(subst, ops, proofs, ove.ovre_hooks.hmod scope ove.ovre_local me)
| Some { pl_desc = (newname, mode) } ->
let name = me.me_name in
let env = ove.ovre_hooks.henv scope in
let mp, newme = EcEnv.Mod.lookup (unloc newname) env in
let np =
match mp.m_top with
| `Concrete (p, None) -> p
| _ -> assert false
in
let substme = EcSubst.add_path subst (xpath ove name) np in
let me = EcSubst.subst_module substme me in
let me = { me with me_name = name; } in
let newme = { newme with me_name = name; } in
if not (EcReduction.EqTest.for_mexpr env me newme) then
begin
let ppe = EcPrinting.PPEnv.ofenv env in
Format.eprintf "me = %a@."
(EcPrinting.pp_modexp ppe) (mp, me);
Format.eprintf "newme = %a@."
(EcPrinting.pp_modexp ppe) (mp, newme);
clone_error env (CE_ModIncompatible (snd ove.ovre_prefix, name))
end;
let (subst, _) =
match mode with
| `Alias ->
rename ove subst (`Module, name)
| `Inline _ ->
substme, EcPath.basename np in
let newme =
if mode = `Alias then
{newme with me_body = ME_Alias (List.length newme.me_sig.mis_params,
mp)}
else newme in
let scope =
if keep_of_mode mode
then ove.ovre_hooks.hmod scope ove.ovre_local newme
else scope in
(subst, ops, proofs, scope)
(* -------------------------------------------------------------------- *)
and replay_export
(ove : _ ovrenv) (subst, ops, proofs, scope) p
=
let scenv = ove.ovre_hooks.henv scope in
let p = EcSubst.subst_path subst p in
if is_none (EcEnv.Theory.by_path_opt p scenv) then
(subst, ops, proofs, scope)
else
let scope = ove.ovre_hooks.hexport scope p in
(subst, ops, proofs, scope)
(* -------------------------------------------------------------------- *)
and replay_baserw
(ove : _ ovrenv) (subst, ops, proofs, scope) name
=
let scope = ove.ovre_hooks.hbaserw scope name in
(subst, ops, proofs, scope)
(* -------------------------------------------------------------------- *)
and replay_addrw
(ove : _ ovrenv) (subst, ops, proofs, scope) (p, l)
=
let p = EcSubst.subst_path subst p in
let l = List.map (EcSubst.subst_path subst) l in
let scope = ove.ovre_hooks.haddrw scope (p, l) in
(subst, ops, proofs, scope)
(* -------------------------------------------------------------------- *)
and replay_auto
(ove : _ ovrenv) (subst, ops, proofs, scope) (lc, lvl, base, ps)
=
let ps = List.map (EcSubst.subst_path subst) ps in
let ps = List.filter (fun p ->
Option.is_some (EcEnv.Ax.by_path_opt p (ove.ovre_hooks.henv scope))
) ps in
let scope = ove.ovre_hooks.hauto scope (lc, lvl, base, ps) in
(subst, ops, proofs, scope)
(* -------------------------------------------------------------------- *)
and replay_reduction
(ove : _ ovrenv) (subst, ops, proofs, scope)
(rules : (EcPath.path * EcTheory.rule_option * EcTheory.rule option) list)
=
let for1 (p, opts, rule) =
let p = EcSubst.subst_path subst p in
let rule =
obind (fun rule ->
try
Some (EcReduction.User.compile
~opts ~prio:rule.rl_prio (ove.ovre_hooks.henv scope) p)
with EcReduction.User.InvalidUserRule _ -> None) rule
in (p, opts, rule) in
let rules = List.map for1 rules in
let scope = ove.ovre_hooks.husered scope rules in
(subst, ops, proofs, scope)
(* -------------------------------------------------------------------- *)
and replay_typeclass
(ove : _ ovrenv) (subst, ops, proofs, scope) (x, tc)
=
let tc = EcSubst.subst_tc subst tc in
let scope = ove.ovre_hooks.htycl scope (x, tc) in
(subst, ops, proofs, scope)
(* -------------------------------------------------------------------- *)
and replay_instance
(ove : _ ovrenv) (subst, ops, proofs, scope) ((typ, ty), tc)
=
let opath = ove.ovre_opath in
let npath = ove.ovre_npath in
let module E = struct exception InvInstPath end in
let forpath (p : EcPath.path) =
match EcPath.getprefix opath p |> omap List.rev with
| None | Some [] -> None
| Some (x::px) ->
let q = EcPath.fromqsymbol (List.rev px, x) in
match Mp.find_opt q ops with
| None ->
Some (EcPath.pappend npath q)
| Some (op, alias) ->
match alias with
| true -> Some (EcPath.pappend npath q)
| false ->
match op.EcDecl.op_kind with
| OB_pred _
| OB_nott _ -> assert false
| OB_oper None -> None
| OB_oper (Some (OP_Constr _))
| OB_oper (Some (OP_Record _))
| OB_oper (Some (OP_Proj _))
| OB_oper (Some (OP_Fix _))
| OB_oper (Some (OP_TC )) ->
Some (EcPath.pappend npath q)
| OB_oper (Some (OP_Plain (e, _))) ->
match e.EcTypes.e_node with
| EcTypes.Eop (r, _) -> Some r
| _ -> raise E.InvInstPath
in
let forpath p = odfl p (forpath p) in
try
let (typ, ty) = EcSubst.subst_genty subst (typ, ty) in
let tc =
let rec doring cr =
{ r_type = EcSubst.subst_ty subst cr.r_type;
r_zero = forpath cr.r_zero;
r_one = forpath cr.r_one;
r_add = forpath cr.r_add;
r_opp = cr.r_opp |> omap forpath;
r_mul = forpath cr.r_mul;
r_exp = cr.r_exp |> omap forpath;
r_sub = cr.r_sub |> omap forpath;
r_embed =
begin match cr.r_embed with
| `Direct -> `Direct
| `Default -> `Default
| `Embed p -> `Embed (forpath p)
end;
r_kind = cr.r_kind; }
and dofield cr =
{ f_ring = doring cr.f_ring;
f_inv = forpath cr.f_inv;
f_div = cr.f_div |> omap forpath; }
in
match tc with
| `Ring cr -> `Ring (doring cr)
| `Field cr -> `Field (dofield cr)
| `General p -> `General (forpath p)
in
let scope = ove.ovre_hooks.hinst scope ((typ, ty), tc) in
(subst, ops, proofs, scope)
with E.InvInstPath ->
(subst, ops, proofs, scope)
(* -------------------------------------------------------------------- *)
and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) item =
match item.cti_item with
| CTh_type (x, otyd) ->
replay_tyd ove (subst, ops, proofs, scope) (item.cti_import, x, otyd)
| CTh_operator (x, ({ op_kind = OB_oper _ } as oopd)) ->
replay_opd ove (subst, ops, proofs, scope) (item.cti_import, x, oopd)
| CTh_operator (x, ({ op_kind = OB_pred _} as oopr)) ->
replay_prd ove (subst, ops, proofs, scope) (item.cti_import, x, oopr)
| CTh_operator (x, ({ op_kind = OB_nott _} as oont)) ->
replay_ntd ove (subst, ops, proofs, scope) (x, oont)
| CTh_axiom (x, ax) ->
replay_axd ove (subst, ops, proofs, scope) (x, ax)
| CTh_modtype (x, modty) ->
replay_modtype ove (subst, ops, proofs, scope) (x, modty)
| CTh_module me ->
replay_mod ove (subst, ops, proofs, scope) me
| CTh_export p ->
replay_export ove (subst, ops, proofs, scope) p
| CTh_baserw x ->
replay_baserw ove (subst, ops, proofs, scope) x
| CTh_addrw (p, l) ->
replay_addrw ove (subst, ops, proofs, scope) (p, l)
| CTh_reduction rules ->
replay_reduction ove (subst, ops, proofs, scope) rules
| CTh_auto (lc, lvl, base, ps) ->
replay_auto ove (subst, ops, proofs, scope) (lc, lvl, base, ps)
| CTh_typeclass (x, tc) ->
replay_typeclass ove (subst, ops, proofs, scope) (x, tc)
| CTh_instance ((typ, ty), tc) ->
replay_instance ove (subst, ops, proofs, scope) ((typ, ty), tc)
| CTh_theory (ox, (cth, thmode)) -> begin
let (subst, x) = rename ove subst (`Theory, ox) in
let subovrds = Msym.find_opt ox ove.ovre_ovrd.evc_ths in
let subovrds = EcUtils.odfl evc_empty subovrds in
let subove = { ove with
ovre_ovrd = subovrds;
ovre_abstract = ove.ovre_abstract || (thmode = `Abstract);
ovre_prefix = (fst ove.ovre_prefix @ [ox], snd ove.ovre_prefix @ [x]);
ovre_glproof =
if List.is_empty subovrds.evc_lemmas.ev_global
then ove.ovre_glproof
else subovrds.evc_lemmas.ev_global; }
in
let (subst, ops, proofs, subscope) =
let subscope = ove.ovre_hooks.hthenter scope thmode x in
let (subst, ops, proofs, subscope) =
List.fold_left (replay1 subove)
(subst, ops, proofs, subscope) cth.cth_struct in
let scope = ove.ovre_hooks.hthexit subscope `Full in
(subst, ops, proofs, scope)
in (subst, ops, proofs, subscope)
end
(* -------------------------------------------------------------------- *)
let replay (hooks : 'a ovrhooks)
~abstract ~local ~incl ~clears ~renames
~opath ~npath ovrds (scope : 'a) (name, items)
=
let subst = EcSubst.add_path EcSubst.empty opath npath in
let ove = {
ovre_ovrd = ovrds;
ovre_rnms = renames;
ovre_ntclr = clears;
ovre_opath = opath;
ovre_npath = npath;
ovre_prefix = ([], []);
ovre_abstract = abstract;
ovre_local = local;
ovre_hooks = hooks;
ovre_glproof = ovrds.evc_lemmas.ev_global;
} in
try
let mode = if abstract then `Abstract else `Concrete in
let scope = if incl then scope else hooks.hthenter scope mode name in
let _, _, proofs, scope =
List.fold_left (replay1 ove)
(subst, Mp.empty, [], scope) items in
let scope = if incl then scope else hooks.hthexit scope `No in
(List.rev proofs, scope)
with EcEnv.DuplicatedBinding x ->
hooks.herr
(Printf.sprintf "name clash for `%s': check your renamings" x)
