From 8270b56efcb2c701832bcea96ac815b224e44576 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Mon, 28 Aug 2023 16:00:06 +0200 Subject: [PATCH] Operators body can now be formulas When cloning a theory, inlined operator definitions must be expressions s.t. their substitution can be done in procedures bodies. --- src/ecCoreFol.ml | 8 ++++++++ src/ecCoreFol.mli | 6 +++++- src/ecDecl.ml | 5 ++--- src/ecDecl.mli | 4 ++-- src/ecEnv.ml | 3 +-- src/ecFol.ml | 1 - src/ecHiGoal.ml | 4 ++-- src/ecInductive.ml | 17 +++++++++-------- src/ecParser.mly | 8 ++++---- src/ecParsetree.ml | 4 ++-- src/ecPrinting.ml | 15 ++++++++------- src/ecReduction.ml | 11 ++++------- src/ecScope.ml | 17 +++++++++-------- src/ecSection.ml | 8 ++++---- src/ecSmt.ml | 5 ++--- src/ecSubst.ml | 16 ++++++++-------- src/ecTheoryReplay.ml | 25 +++++++++++++------------ theories/algebra/Ideal.ec | 2 +- 18 files changed, 84 insertions(+), 75 deletions(-) diff --git a/src/ecCoreFol.ml b/src/ecCoreFol.ml index 094e595a90..a1f621ce7a 100644 --- a/src/ecCoreFol.ml +++ b/src/ecCoreFol.ml @@ -947,6 +947,14 @@ let f_xmul_simpl f1 f2 = let f_xmuli_simpl f1 f2 = f_xmul_simpl (f_N f1) f2 +(* -------------------------------------------------------------------- *) +let f_none (ty : ty) : form = + f_op EcCoreLib.CI_Option.p_none [ty] (toption ty) + +let f_some ({ f_ty = ty } as f : form) : form = + let op = f_op EcCoreLib.CI_Option.p_some [ty] (tfun ty (toption ty)) in + f_app op [f] (toption ty) + (* -------------------------------------------------------------------- *) let cost_map g cost = let calls = diff --git a/src/ecCoreFol.mli b/src/ecCoreFol.mli index 46ebeb1d4e..be97611f92 100644 --- a/src/ecCoreFol.mli +++ b/src/ecCoreFol.mli @@ -337,6 +337,10 @@ val f_int_mul : form -> form -> form val f_int_pow : form -> form -> form val f_int_edivz : form -> form -> form +(* -------------------------------------------------------------------- *) +val f_none : ty -> form +val f_some : form -> form + (* -------------------------------------------------------------------- *) val f_is_inf : form -> form val f_is_int : form -> form @@ -466,7 +470,7 @@ type f_subst = private { fs_freshen : bool; (* true means realloc local *) fs_loc : form Mid.t; fs_esloc : expr Mid.t; - fs_ty : ty_subst; + fs_ty : ty_subst; fs_mem : EcIdent.t Mid.t; fs_memtype : EcMemory.memtype option; (* Only substituted in Fcoe *) fs_mempred : mem_pr Mid.t; (* For predicates over memories, diff --git a/src/ecDecl.ml b/src/ecDecl.ml index 8b0ce32069..aab68b329b 100644 --- a/src/ecDecl.ml +++ b/src/ecDecl.ml @@ -74,7 +74,7 @@ type operator_kind = | OB_nott of notation and opbody = - | OP_Plain of EcTypes.expr * bool (* nosmt? *) + | OP_Plain of EcCoreFol.form * bool (* nosmt? *) | OP_Constr of EcPath.path * int | OP_Record of EcPath.path | OP_Proj of EcPath.path * int * int @@ -294,8 +294,7 @@ let operator_as_prind (op : operator) = | _ -> assert false (* -------------------------------------------------------------------- *) -let axiomatized_op ?(nargs = 0) ?(nosmt = false) path (tparams, bd) lc = - let axbd = EcCoreFol.form_of_expr EcCoreFol.mhr bd in +let axiomatized_op ?(nargs = 0) ?(nosmt = false) path (tparams, axbd) lc = let axbd, axpm = let bdpm = List.map fst tparams in let axpm = List.map EcIdent.fresh bdpm in diff --git a/src/ecDecl.mli b/src/ecDecl.mli index 3ab3ca4034..091273cc19 100644 --- a/src/ecDecl.mli +++ b/src/ecDecl.mli @@ -49,7 +49,7 @@ type operator_kind = | OB_nott of notation and opbody = - | OP_Plain of EcTypes.expr * bool (* nosmt? *) + | OP_Plain of EcCoreFol.form * bool (* nosmt? *) | OP_Constr of EcPath.path * int | OP_Record of EcPath.path | OP_Proj of EcPath.path * int * int @@ -169,7 +169,7 @@ val axiomatized_op : ?nargs: int -> ?nosmt:bool -> EcPath.path - -> (ty_params * expr) + -> (ty_params * form) -> locality -> axiom diff --git a/src/ecEnv.ml b/src/ecEnv.ml index c1fbbaf956..bffdb7f3eb 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -2887,8 +2887,7 @@ module Op = struct let op = oget (by_path_opt p env) in let f = match op.op_kind with - | OB_oper (Some (OP_Plain (e, _))) when force || not op.op_opaque -> - form_of_expr EcCoreFol.mhr e + | OB_oper (Some (OP_Plain (f, _))) | OB_pred (Some (PR_Plain f)) when force || not op.op_opaque -> f | _ -> raise NotReducible diff --git a/src/ecFol.ml b/src/ecFol.ml index 11581cdab8..12d13d5599 100644 --- a/src/ecFol.ml +++ b/src/ecFol.ml @@ -54,7 +54,6 @@ let destr_rint f = | _ -> destr_error "destr_rint" - (* -------------------------------------------------------------------- *) let fop_int_le = f_op CI.CI_Int .p_int_le [] (toarrow [tint ; tint ] tbool) let fop_int_lt = f_op CI.CI_Int .p_int_lt [] (toarrow [tint ; tint ] tbool) diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index aa50c7b1dc..0fa0cec0dc 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -615,8 +615,8 @@ let process_delta ~und_delta ?target (s, o, p) tc = let op = EcEnv.Op.by_path (fst p) env in match op.EcDecl.op_kind with - | EcDecl.OB_oper (Some (EcDecl.OP_Plain (e, _))) -> - (snd p, op.EcDecl.op_tparams, form_of_expr EcFol.mhr e, args, Some (fst p)) + | EcDecl.OB_oper (Some (EcDecl.OP_Plain (f, _))) -> + (snd p, op.EcDecl.op_tparams, f, args, Some (fst p)) | EcDecl.OB_pred (Some (EcDecl.PR_Plain f)) -> (snd p, op.EcDecl.op_tparams, f, args, Some (fst p)) | _ -> diff --git a/src/ecInductive.ml b/src/ecInductive.ml index b915fd713e..2c76fce942 100644 --- a/src/ecInductive.ml +++ b/src/ecInductive.ml @@ -3,6 +3,7 @@ open EcUtils open EcSymbols open EcTypes open EcDecl +open EcCoreFol module EP = EcPath module FL = EcCoreFol @@ -163,7 +164,7 @@ let datatype_projectors (tpath, tparams, { tydt_ctors = ctors }) = let do1 i (cname, cty) = let thv = EcIdent.create "the" in - let the = e_local thv thety in + let the = f_local thv thety in let rty = ttuple cty in let do1 j (_, cty2) = @@ -172,17 +173,17 @@ let datatype_projectors (tpath, tparams, { tydt_ctors = ctors }) = (fun ty -> (EcIdent.create (symbol_of_ty ty), ty)) cty2 in - e_lam lvars + f_lambda + (List.map (fun (x, ty) -> (x, GTty ty)) lvars) (if i = j - then e_some (e_tuple (List.map (curry e_local) lvars)) - else e_none rty) in + then f_some (f_tuple (List.map (curry f_local) lvars)) + else f_none rty) in - - let body = e_match the (List.mapi do1 ctors) (toption rty) in - let body = e_lam [thv, thety] body in + let body = f_match the (List.mapi do1 ctors) (toption rty) in + let body = f_lambda [thv, GTty thety] body in let op = Some (OP_Plain (body, false)) in - let op = mk_op ~opaque:false tparams body.e_ty op `Global in (* FIXME *) + let op = mk_op ~opaque:false tparams body.f_ty op `Global in (* FIXME *) (cname, op) in diff --git a/src/ecParser.mly b/src/ecParser.mly index e212b7dcd6..95fae8eecd 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -24,7 +24,7 @@ let opdef_of_opbody ty b = match b with | None -> PO_abstr ty - | Some (`Expr e ) -> PO_concr (ty, e) + | Some (`Form f ) -> PO_concr (ty, f) | Some (`Case bs) -> PO_case (ty, bs) | Some (`Reft rt) -> PO_reft (ty, rt) @@ -1972,7 +1972,7 @@ operator: po_locality = locality; } } opbody: -| e=expr { `Expr e } +| f=form { `Form f } | bs=opbr+ { `Case bs } opax: @@ -3785,14 +3785,14 @@ clone_override: | OP st=nosmt x=qoident tyvars=bracket(tident*)? p=ptybinding1* sty=ioption(prefix(COLON, loc(type_exp))) - mode=loc(opclmode) e=expr + mode=loc(opclmode) f=form { let ov = { opov_nosmt = st; opov_tyvars = tyvars; opov_args = List.flatten p; opov_retty = odfl (mk_loc mode.pl_loc PTunivar) sty; - opov_body = e; + opov_body = f; } in (x, PTHO_Op (`BySyntax ov, unloc mode)) } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 25212655c0..8cf774a4e9 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -380,7 +380,7 @@ type ptyvardecls = type pop_def = | PO_abstr of pty - | PO_concr of pty * pexpr + | PO_concr of pty * pformula | PO_case of pty * pop_branch list | PO_reft of pty * (psymbol * pformula) @@ -1197,7 +1197,7 @@ and op_override_def = { opov_tyvars : psymbol list option; opov_args : ptybinding list; opov_retty : pty; - opov_body : pexpr; + opov_body : pformula; } and pr_override_def = { diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 15d34526c7..a213820f12 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -2262,21 +2262,22 @@ let pp_opdecl_op (ppe : PPEnv.t) fmt (basename, ts, ty, op) = | None -> Format.fprintf fmt ": %a" (pp_type ppe) ty - | Some (OP_Plain (e, _)) -> + | Some (OP_Plain (f, _)) -> let ((subppe, pp_vds), e, has_vds) = let (vds, e) = - match e.e_node with - | Equant (`ELambda, vds, e) -> (vds, e) - | _ -> ([], e) in - (pp_locbinds ppe ~fv:e.e_fv vds, e, + match f.f_node with + | Fquant (Llambda, vds, f) -> + (List.map (snd_map gty_as_ty) vds, f) + | _ -> ([], f) in + (pp_locbinds ppe ~fv:f.f_fv vds, e, match vds with [] -> false | _ -> true) in if has_vds then Format.fprintf fmt "%t :@ %a =@ %a" pp_vds - (pp_type ppe) e.e_ty (pp_expr subppe) e + (pp_type ppe) f.f_ty (pp_form subppe) f else Format.fprintf fmt ":@ %a =@ %a" - (pp_type ppe) e.e_ty (pp_expr subppe) e + (pp_type ppe) e.f_ty (pp_form subppe) f | Some (OP_Constr (indp, i)) -> Format.fprintf fmt ": %a =@ < %d-th constructor of %a >" diff --git a/src/ecReduction.ml b/src/ecReduction.ml index 28fc44c081..e10b1dd741 100644 --- a/src/ecReduction.ml +++ b/src/ecReduction.ml @@ -2037,15 +2037,12 @@ let check_bindings exn tparams env s bd1 bd2 = let rec conv_oper env ob1 ob2 = match ob1, ob2 with - | OP_Plain(e1,_), OP_Plain(e2,_) -> - Format.eprintf "[W]: ICI1@."; - conv_expr env EcSubst.empty e1 e2 - | OP_Plain({e_node = Eop(p,tys)},_), _ -> - Format.eprintf "[W]: ICI2@."; + | OP_Plain(f1,_), OP_Plain(f2,_) -> + error_body (is_conv (LDecl.init env []) f1 f2) + | OP_Plain({f_node = Fop(p,tys)},_), _ -> let ob1 = get_open_oper env p tys in conv_oper env ob1 ob2 - | _, OP_Plain({e_node = Eop(p,tys)}, _) -> - Format.eprintf "[W]: ICI3@."; + | _, OP_Plain({f_node = Fop(p,tys)}, _) -> let ob2 = get_open_oper env p tys in conv_oper env ob1 ob2 | OP_Constr(p1,i1), OP_Constr(p2,i2) -> diff --git a/src/ecScope.ml b/src/ecScope.ml index 62c87efe2c..867f56c68a 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1147,12 +1147,12 @@ module Op = struct let xs = snd (TT.trans_binding eenv ue op.po_args) in (EcTypes.toarrow (List.map snd xs) codom, `Abstract, []) - | PO_concr (pty, pe) -> + | PO_concr (pty, pf) -> let codom = TT.transty TT.tp_relax eenv ue pty in let env, xs = TT.trans_binding eenv ue op.po_args in - let body = TT.transexpcast env `InOp ue codom pe in - let lam = EcTypes.e_lam xs body in - (lam.EcTypes.e_ty, `Plain lam, []) + let body = TT.trans_form env ue pf codom in + let lam = f_lambda (List.map (fun (x, ty) -> (x, GTty ty)) xs) body in + (lam.f_ty, `Plain lam, []) | PO_case (pty, pbs) -> begin let name = { pl_loc = loc; pl_desc = unloc op.po_name } in @@ -1189,13 +1189,13 @@ module Op = struct let uidmap = EcUnify.UniEnv.close ue in let ts = Tuni.subst uidmap in - let es = e_subst { e_subst_id with es_ty = ts } in + let fs = Fsubst.f_subst (Fsubst.f_subst_init ~sty:ts ()) in let ty = ty_subst ts ty in let tparams = EcUnify.UniEnv.tparams ue in let body = match body with | `Abstract -> None - | `Plain e -> Some (OP_Plain (es e, nosmt)) + | `Plain e -> Some (OP_Plain (fs e, nosmt)) | `Fix opfx -> Some (OP_Fix { opf_args = opfx.EHI.mf_args; @@ -1394,11 +1394,12 @@ module Op = struct (`Det, Sem.translate_e env ret) in let _, aout = Sem.translate_s env cont body.f_body in - let aout = e_lam (List.map2 (fun (_, ty) x -> (x, ty)) params ids) aout in + let aout = form_of_expr mhr aout in (* FIXME: translate to forms directly? *) + let aout = f_lambda (List.map2 (fun (_, ty) x -> (x, GTty ty)) params ids) aout in let opdecl = EcDecl.{ op_tparams = []; - op_ty = aout.e_ty; + op_ty = aout.f_ty; op_kind = OB_oper (Some (OP_Plain (aout, false))); op_loca = op.ppo_locality; op_opaque = false; diff --git a/src/ecSection.ml b/src/ecSection.ml index 23a2bb8dae..d7ff733dea 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -434,7 +434,7 @@ let on_opdecl (cb : cb) (opdecl : operator) = match b with | OP_Constr _ | OP_Record _ | OP_Proj _ -> assert false | OP_TC -> assert false - | OP_Plain (e, _) -> on_expr cb e + | OP_Plain (f, _) -> on_form cb f | OP_Fix f -> let rec on_mpath_branches br = match br with @@ -715,7 +715,7 @@ let tydecl_fv tyd = let op_body_fv body ty = let fv = ty_fv_and_tvar ty in match body with - | OP_Plain (e, _) -> EcIdent.fv_union fv (fv_and_tvar_e e) + | OP_Plain (f, _) -> EcIdent.fv_union fv (fv_and_tvar_f f) | OP_Constr _ | OP_Record _ | OP_Proj _ | OP_TC -> fv | OP_Fix opfix -> let fv = @@ -902,8 +902,8 @@ let generalize_opdecl to_gen prefix (name, operator) = match body with | OP_Constr _ | OP_Record _ | OP_Proj _ -> assert false | OP_TC -> assert false (* ??? *) - | OP_Plain (e,nosmt) -> - OP_Plain (e_lam extra_a e, nosmt) + | OP_Plain (f,nosmt) -> + OP_Plain (f_lambda (List.map (fun (x, ty) -> (x, GTty ty)) extra_a) f, nosmt) | OP_Fix opfix -> let subst = EcSubst.add_opdef EcSubst.empty path tosubst in let nb_extra = List.length extra_a in diff --git a/src/ecSmt.ml b/src/ecSmt.ml index aec3b6a9c6..06126ebe22 100644 --- a/src/ecSmt.ml +++ b/src/ecSmt.ml @@ -1091,7 +1091,6 @@ and create_op ?(body = false) (genv : tenv) p = let decl = match body, op.op_kind with | true, OB_oper (Some (OP_Plain (body, false))) -> - let body = EcFol.form_of_expr EcFol.mhr body in let wparams, wbody = trans_body (genv, lenv) wdom wcodom body in WDecl.create_logic_decl [WDecl.make_ls_defn ls (wextra@wparams) wbody] @@ -1449,8 +1448,8 @@ module Frequency = struct match EcEnv.Op.by_path_opt p env with | Some {op_kind = OB_pred (Some (PR_Plain f)) } -> r_union rs (f_ops unwanted_op f) - | Some {op_kind = OB_oper (Some (OP_Plain (e, false))) } -> - r_union rs (f_ops unwanted_op (form_of_expr mhr e)) + | Some {op_kind = OB_oper (Some (OP_Plain (f, false))) } -> + r_union rs (f_ops unwanted_op f) | Some {op_kind = OB_oper (Some (OP_Fix ({ opf_nosmt = false } as e))) } -> let rec aux rs = function | OPB_Leaf (_, e) -> r_union rs (f_ops unwanted_op (form_of_expr mhr e)) diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 86da049d3f..14f02f0e3e 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -30,7 +30,7 @@ type subst = { sb_flocal : EcCoreFol.form Mid.t; sb_fmem : EcIdent.t Mid.t; sb_tydef : (EcIdent.t list * ty) Mp.t; - sb_def : (EcIdent.t list * [`Expr of expr | `Form of EcCoreFol.form]) Mp.t; + sb_def : (EcIdent.t list * [`Op of expr | `Pred of form]) Mp.t; sb_moddef : EcPath.path Mp.t; } @@ -100,7 +100,7 @@ let subst_mem (s : subst) (m : EcIdent.t) = (* -------------------------------------------------------------------- *) let get_opdef (s : subst) (p : EcPath.path) = match Mp.find_opt p s.sb_def with - | Some (ids, `Expr e) -> Some (ids, e) | _ -> None + | Some (ids, `Op f) -> Some (ids, f) | _ -> None (* -------------------------------------------------------------------- *) let has_opdef (s : subst) (p : EcPath.path) = @@ -112,8 +112,8 @@ let get_def (s : subst) (p : EcPath.path) = | Some (ids, body) -> let body = match body with - | `Expr e -> form_of_expr mhr e - | `Form f -> f in + | `Op e -> form_of_expr mhr e + | `Pred f -> f in Some (ids, body) | None -> None @@ -257,13 +257,13 @@ let add_tydef (s : subst) p (ids, ty) = assert (Mp.find_opt p s.sb_tydef = None); { s with sb_tydef = Mp.add p (ids, ty) s.sb_tydef } -let add_opdef (s : subst) p (ids, e) = +let add_opdef (s : subst) p (ids, f) = assert (Mp.find_opt p s.sb_def = None); - { s with sb_def = Mp.add p (ids, (`Expr e)) s.sb_def } + { s with sb_def = Mp.add p (ids, (`Op f)) s.sb_def } let add_pddef (s : subst) p (ids, f) = assert (Mp.find_opt p s.sb_def = None); - { s with sb_def = Mp.add p (ids, `Form f) s.sb_def } + { s with sb_def = Mp.add p (ids, `Pred f) s.sb_def } let add_moddef (s : subst) ~(src : EcPath.path) ~(dst : EcPath.path) = assert (Mp.find_opt src s.sb_moddef = None); @@ -962,7 +962,7 @@ and subst_notation (s : subst) (nott : notation) = and subst_op_body (s : subst) (bd : opbody) = match bd with | OP_Plain (body, nosmt) -> - OP_Plain (subst_expr s body, nosmt) + OP_Plain (subst_form s body, nosmt) | OP_Constr (p, i) -> OP_Constr (subst_path s p, i) | OP_Record p -> OP_Record (subst_path s p) diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index bd7cf99104..e6a7c1382d 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -132,12 +132,12 @@ let get_open_oper exn env p tys = let rec oper_compatible exn env ob1 ob2 = match ob1, ob2 with - | OP_Plain(e1,_), OP_Plain(e2,_) -> - expr_compatible exn env EcSubst.empty e1 e2 - | OP_Plain({e_node = Eop(p,tys)},_), _ -> + | OP_Plain(f1,_), OP_Plain(f2,_) -> + error_body exn (EcReduction.is_conv (EcEnv.LDecl.init env []) f1 f2) + | OP_Plain({f_node = Fop(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)}, _) -> + | _, OP_Plain({f_node = Fop(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) -> @@ -445,9 +445,9 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) = 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) + let body = EcTyping.trans_form env ue opov.opov_body codom in + let lam = EcFol.f_lambda (List.map (fun (x, ty) -> (x, EcFol.GTty ty)) xs) body in + (lam.f_ty, lam) in begin try ty_compatible env ue @@ -462,7 +462,7 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) = ~loc "this operator body contains free type variables"; let sty = Tuni.subst (EcUnify.UniEnv.close ue) in - let body = e_subst { e_subst_id with es_ty = sty } body in + let body = EcFol.Fsubst.f_subst (EcFol.Fsubst.f_subst_init ~sty ()) body in let ty = ty_subst sty ty in let tparams = EcUnify.UniEnv.tparams ue in let newop = @@ -480,7 +480,7 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) = (match refop.op_kind with | OB_oper (Some (OP_Plain (body, _))) -> body | _ -> assert false) - else EcTypes.e_op p tyargs refop.op_ty in + else EcFol.f_op p tyargs refop.op_ty in let decl = { refop with op_kind = OB_oper (Some (OP_Plain (body, nosmt))); @@ -496,6 +496,7 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) = (newop, subst, x, true) | `Inline _ -> + let body = EcFol.expr_of_form EcFol.mhr body in (* FIXME: error message *) 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) @@ -919,9 +920,9 @@ and replay_instance | 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 + | OB_oper (Some (OP_Plain (f, _))) -> + match f.f_node with + | Fop (r, _) -> Some r | _ -> raise E.InvInstPath in diff --git a/theories/algebra/Ideal.ec b/theories/algebra/Ideal.ec index e572e55599..7b7e62e6f0 100644 --- a/theories/algebra/Ideal.ec +++ b/theories/algebra/Ideal.ec @@ -238,7 +238,7 @@ qed. (* -------------------------------------------------------------------- *) op principal (I : t -> bool) = - exists a : t, forall x, (I x <=> exists b, x = b * a). + exists (a : t), forall x, (I x <=> exists b, x = b * a). lemma principal_ideal I : principal I => ideal I. proof.