(* ------------------------------------------------------------------ *) 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 : EcTypes.is_local; ovre_hooks : 'a ovrhooks; } and 'a ovrhooks = { henv : 'a -> EcSection.scenv; hadd_item : 'a -> EcTheory.import -> EcTheory.theory_item_r -> 'a; hthenter : 'a -> thmode -> symbol -> is_local -> '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 let ri = { EcReduction.full_red with delta_p = fun _-> `Force; } in error_body exn (EcReduction.is_conv ~ri:ri (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 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 let env = EcSection.env scenv 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 let item = (Th_type (x, otyd)) in (subst, ops, proofs, ove.ovre_hooks.hadd_item scope import item) | 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 env ue ntyd in let decl = { tyd_params = nargs; tyd_type = `Concrete ntyd; tyd_resolve = otyd.tyd_resolve && (mode = `Alias); tyd_loca = otyd.tyd_loca; } in (decl, ntyd) | `ByPath p -> begin match EcEnv.Ty.by_path_opt p env 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 env).tyd_type with | `Datatype { tydt_ctors = _ } -> let newtparams = List.fst newtyd.tyd_params in let newtparams_ty = List.map tvar newtparams in let newdtype = tconstr np newtparams_ty in let tysubst = EcTypes.Tvar.init (List.fst otyd.tyd_params) newtparams_ty in List.fold_left (fun subst (name, tyargs) -> let np = EcPath.pqoname (EcPath.prefix np) name in let newtyargs = List.map (Tvar.subst tysubst) tyargs in EcSubst.add_opdef subst (xpath ove name) (newtparams, e_op np newtparams_ty (toarrow newtyargs newdtype))) subst octors | _ -> subst end | _, _ -> subst in (subst, x) in let refotyd = EcSubst.subst_tydecl subst otyd in begin try tydecl_compatible env refotyd newtyd with Incompatible err -> clone_error env (CE_TyIncompatible ((snd ove.ovre_prefix, x), err)) end; let scope = match mode with | `Alias -> let item = EcTheory.Th_type (x, newtyd) in ove.ovre_hooks.hadd_item scope import item | `Inline `Keep -> let item = EcTheory.Th_type (x, newtyd) in ove.ovre_hooks.hadd_item scope EcTheory.noimport item | `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 let env = EcSection.env scenv 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.hadd_item scope import (Th_operator (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 env (loc, tp) in let tp = EcTyping.tp_relax in let (ty, body) = 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 env ue (List.map fst reftyvars, refty) (List.map fst (EcUnify.UniEnv.tparams ue), ty) with Incompatible err -> clone_error env (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))) refop.op_loca in (newop, body) | `ByPath p -> begin match EcEnv.Op.by_path_opt p env 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 env (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 env refop newop with Incompatible err -> clone_error env (CE_OpIncompatible ((snd ove.ovre_prefix, x), err)) end; let scope = match opmode with | `Alias -> let item = Th_operator (x, newop) in ove.ovre_hooks.hadd_item scope import item | `Inline `Keep -> let item = Th_operator (x, newop) in ove.ovre_hooks.hadd_item scope EcTheory.noimport item | `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 let env = EcSection.env scenv 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.hadd_item scope import (Th_operator (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 env (loc, tp) in let body = 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 env ue (List.map fst reftyvars, refty) (List.map fst (EcUnify.UniEnv.tparams ue), body.EcFol.f_ty) with Incompatible err -> clone_error env (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; op_loca = refpr.op_loca; } in (newpr, body) | `ByPath p -> begin match EcEnv.Op.by_path_opt p env 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 env (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 env refpr newpr with Incompatible err -> clone_error env (CE_OpIncompatible ((snd ove.ovre_prefix, x), err)) end; let scope = match prmode with | `Alias -> let item = Th_operator (x, newpr) in ove.ovre_hooks.hadd_item scope import item | `Inline `Keep -> let item = Th_operator (x, newpr) in ove.ovre_hooks.hadd_item scope EcTheory.noimport item | `Inline `Clear -> scope in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) and replay_ntd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, 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 item = Th_operator (x, oont) in let scope = ove.ovre_hooks.hadd_item scope import item 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 item = Th_operator (x, oont) in let scope = ove.ovre_hooks.hadd_item scope import item in (subst, ops, proofs, scope) | `Inline `Clear -> (subst, ops, proofs, scope) end (* -------------------------------------------------------------------- *) and replay_axd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, 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.hadd_item scope import (Th_axiom(x, ax)) in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) and replay_scd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, sc) = let subst, x = rename ove subst (`Lemma, x) in let sc = EcSubst.subst_schema subst sc in let item = Th_schema (x, sc) in let scope = ove.ovre_hooks.hadd_item scope import item in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) and replay_modtype (ove : _ ovrenv) (subst, ops, proofs, scope) (import, 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_top_modsig subst modty in let item = Th_modtype (x, modty) in (subst, ops, proofs, ove.ovre_hooks.hadd_item scope import item) | Some { pl_desc = (newname, mode) } -> let env = EcSection.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_modtydef subst ~src:(xpath ove x) ~dst:np in subst, x in let modty = EcSubst.subst_top_modsig subst modty in if not (EcReduction.EqTest.for_msig env modty.tms_sig newmt.tms_sig) then clone_error env (CE_ModTyIncompatible (snd ove.ovre_prefix, x)); let scope = if keep_of_mode mode then let item = Th_modtype (name, newmt) in ove.ovre_hooks.hadd_item scope import item else scope in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) and replay_mod (ove : _ ovrenv) (subst, ops, proofs, scope) (import, (me : top_module_expr)) = match Msym.find_opt me.tme_expr.me_name ove.ovre_ovrd.evc_modexprs with | None -> let subst, name = rename ove subst (`Module, me.tme_expr.me_name) in let me = EcSubst.subst_top_module subst me in let me = { me with tme_expr = { me.tme_expr with me_name = name } } in let item = (Th_module me) in (subst, ops, proofs, ove.ovre_hooks.hadd_item scope import item) | Some { pl_desc = (newname, mode) } -> let name = me.tme_expr.me_name in let env = EcSection.env (ove.ovre_hooks.henv scope) in let mp, (newme, newlc) = 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_moddef subst ~src:(xpath ove name) ~dst:np in let me = EcSubst.subst_top_module substme me in let me = { me with tme_expr = { me.tme_expr with me_name = name } } in let newme = { newme with me_name = name } in let newme = { tme_expr = newme; tme_loca = Option.get newlc; } in if not (EcReduction.EqTest.for_mexpr ~body:false env me.tme_expr newme.tme_expr) then clone_error env (CE_ModIncompatible (snd ove.ovre_prefix, name)); let (subst, _) = match mode with | `Alias -> rename ove subst (`Module, name) | `Inline _ -> substme, EcPath.basename np in let newme = if mode = `Alias || mode = `Inline `Keep then let alias = ME_Alias ( List.length newme.tme_expr.me_params, EcPath.m_apply mp (List.map (fun (id, _) -> EcPath.mident id) newme.tme_expr.me_params) ) in { newme with tme_expr = { newme.tme_expr with me_body = alias } } else newme in let scope = if keep_of_mode mode then ove.ovre_hooks.hadd_item scope import (Th_module newme) else scope in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) and replay_export (ove : _ ovrenv) (subst, ops, proofs, scope) (import, p, lc) = let scenv = ove.ovre_hooks.henv scope in let env = EcSection.env scenv in let p = EcSubst.subst_path subst p in if is_none (EcEnv.Theory.by_path_opt p env) then (subst, ops, proofs, scope) else let scope = ove.ovre_hooks.hadd_item scope import (Th_export (p, lc)) in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) and replay_baserw (ove : _ ovrenv) (subst, ops, proofs, scope) (import, name, lc) = let scope = ove.ovre_hooks.hadd_item scope import (Th_baserw (name, lc)) in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) and replay_addrw (ove : _ ovrenv) (subst, ops, proofs, scope) (import, p, l, lc) = let p = EcSubst.subst_path subst p in let l = List.map (EcSubst.subst_path subst) l in let scope = ove.ovre_hooks.hadd_item scope import (Th_addrw (p, l, lc)) in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) and replay_auto (ove : _ ovrenv) (subst, ops, proofs, scope) (import, lvl, base, ps, lc) = let env = EcSection.env (ove.ovre_hooks.henv scope) in 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 env)) ps in let scope = ove.ovre_hooks.hadd_item scope import (Th_auto (lvl, base, ps, lc)) in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) and replay_reduction (ove : _ ovrenv) (subst, ops, proofs, scope) (import, rules : _ * (EcPath.path * EcTheory.rule_option * EcTheory.rule option) list) = let for1 (p, opts, rule) = let exception Removed in let p = EcSubst.subst_path subst p in (* TODO: A: schema are not replayed for now, but reduction rules can use a schema. Fix this. *) let rule = obind (fun rule -> let env = EcSection.env (ove.ovre_hooks.henv scope) in try if not ( match opts.ur_mode with | `Ax -> is_some (EcEnv.Ax.by_path_opt p env) | `Sc -> is_some (EcEnv.Schema.by_path_opt p env) ) then raise Removed; Some (EcReduction.User.compile ~opts ~prio:rule.rl_prio env opts.ur_mode p) with EcReduction.User.InvalidUserRule _ | Removed -> None) rule in (p, opts, rule) in let rules = List.map for1 rules in let scope = ove.ovre_hooks.hadd_item scope import (Th_reduction rules) in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) and replay_typeclass (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, tc) = let tc = EcSubst.subst_tc subst tc in let scope = ove.ovre_hooks.hadd_item scope import (Th_typeclass (x, tc)) in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) and replay_instance (ove : _ ovrenv) (subst, ops, proofs, scope) (import, (typ, ty), tc, lc) = 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.hadd_item scope import (Th_instance ((typ, ty), tc, lc)) in (subst, ops, proofs, scope) with E.InvInstPath -> (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) item = match item.ti_item with | Th_type (x, otyd) -> replay_tyd ove (subst, ops, proofs, scope) (item.ti_import, x, otyd) | Th_operator (x, ({ op_kind = OB_oper _ } as oopd)) -> replay_opd ove (subst, ops, proofs, scope) (item.ti_import, x, oopd) | Th_operator (x, ({ op_kind = OB_pred _} as oopr)) -> replay_prd ove (subst, ops, proofs, scope) (item.ti_import, x, oopr) | Th_operator (x, ({ op_kind = OB_nott _} as oont)) -> replay_ntd ove (subst, ops, proofs, scope) (item.ti_import, x, oont) | Th_axiom (x, ax) -> replay_axd ove (subst, ops, proofs, scope) (item.ti_import, x, ax) | Th_schema (x, schema) -> replay_scd ove (subst, ops, proofs, scope) (item.ti_import, x, schema) | Th_modtype (x, modty) -> replay_modtype ove (subst, ops, proofs, scope) (item.ti_import, x, modty) | Th_module me -> replay_mod ove (subst, ops, proofs, scope) (item.ti_import, me) | Th_export (p, lc) -> replay_export ove (subst, ops, proofs, scope) (item.ti_import, p, lc) | Th_baserw (x, lc) -> replay_baserw ove (subst, ops, proofs, scope) (item.ti_import, x, lc) | Th_addrw (p, l, lc) -> replay_addrw ove (subst, ops, proofs, scope) (item.ti_import, p, l, lc) | Th_reduction rules -> replay_reduction ove (subst, ops, proofs, scope) (item.ti_import, rules) | Th_auto (lvl, base, ps, lc) -> replay_auto ove (subst, ops, proofs, scope) (item.ti_import, lvl, base, ps, lc) | Th_typeclass (x, tc) -> replay_typeclass ove (subst, ops, proofs, scope) (item.ti_import, x, tc) | Th_instance ((typ, ty), tc, lc) -> replay_instance ove (subst, ops, proofs, scope) (item.ti_import, (typ, ty), tc, lc) | Th_theory (ox, cth) -> begin let thmode = cth.cth_mode in 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 ove.ovre_local in let (subst, ops, proofs, subscope) = List.fold_left (replay1 subove) (subst, ops, proofs, subscope) cth.cth_items 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 ()) ~src:opath ~dst: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 local 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)