From d1ff8a903c7c3d6a586f0a4cae1c9320fdff0ecf Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 5 Mar 2025 19:02:57 +0100 Subject: [PATCH] setoid rewrite --- src/ecCommands.ml | 10 ++ src/ecCoreGoal.ml | 12 +- src/ecCoreSubst.ml | 2 +- src/ecEnv.ml | 75 +++++++- src/ecEnv.mli | 15 ++ src/ecHiGoal.ml | 50 ++++-- src/ecHiGoal.mli | 1 + src/ecLexer.mll | 2 + src/ecLowGoal.ml | 36 ++-- src/ecLowGoal.mli | 3 +- src/ecLowPhlGoal.ml | 2 +- src/ecMatching.ml | 392 ++++++++++++++++++++++++++++-------------- src/ecMatching.mli | 74 ++++++-- src/ecMemory.ml | 2 +- src/ecParser.mly | 20 +++ src/ecParsetree.ml | 12 ++ src/ecPrinting.ml | 12 +- src/ecScope.ml | 158 ++++++++++++++++- src/ecScope.mli | 6 + src/ecSection.ml | 12 ++ src/ecSetoid.ml | 56 ++++++ src/ecSetoid.mli | 18 ++ src/ecSmt.ml | 8 +- src/ecSubst.ml | 19 +- src/ecSubst.mli | 1 + src/ecThCloning.ml | 2 + src/ecTheory.ml | 2 + src/ecTheory.mli | 2 + src/ecTheoryReplay.ml | 55 ++++++ src/ecTyping.ml | 8 +- src/ecUtils.ml | 18 +- src/ecUtils.mli | 5 +- tests/setoidrw.ec | 45 +++++ 33 files changed, 928 insertions(+), 207 deletions(-) create mode 100644 src/ecSetoid.ml create mode 100644 src/ecSetoid.mli create mode 100644 tests/setoidrw.ec diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 1f86a41b4a..34ff28acdb 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -682,6 +682,14 @@ and process_addrw scope (local, base, names) = and process_reduction scope name = EcScope.Reduction.add_reduction scope name +(* -------------------------------------------------------------------- *) +and process_relation (scope : EcScope.scope) (rel : prelation) = + EcScope.Setoid.add_relation scope rel + +(* -------------------------------------------------------------------- *) +and process_morphism (scope : EcScope.scope) (mph : pmorphism) = + EcScope.Setoid.add_morphism scope mph + (* -------------------------------------------------------------------- *) and process_hint scope hint = EcScope.Auto.add_hint scope hint @@ -783,6 +791,8 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g = | Goption opt -> `Fct (fun scope -> process_option scope opt) | Gaddrw hint -> `Fct (fun scope -> process_addrw scope hint) | Greduction red -> `Fct (fun scope -> process_reduction scope red) + | Grelation rel -> `Fct (fun scope -> process_relation scope rel) + | Gmorphism mph -> `Fct (fun scope -> process_morphism scope mph) | Ghint hint -> `Fct (fun scope -> process_hint scope hint) | GdumpWhy3 file -> `Fct (fun scope -> process_dump_why3 scope file) with diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 74ff095f5b..561e347f41 100644 --- a/src/ecCoreGoal.ml +++ b/src/ecCoreGoal.ml @@ -508,7 +508,7 @@ module FApi = struct (* ------------------------------------------------------------------ *) let xmutate (tc : tcenv) (vx : 'a) (fp : form list) = - let (tc, hds) = List.map_fold (fun tc fp -> newgoal tc fp) tc fp in + let (tc, hds) = List.fold_left_map (fun tc fp -> newgoal tc fp) tc fp in close tc (VExtern (vx, hds)) (* ------------------------------------------------------------------ *) @@ -518,7 +518,7 @@ module FApi = struct (* ------------------------------------------------------------------ *) let xmutate_hyps (tc : tcenv) (vx : 'a) subgoals = let (tc, hds) = - List.map_fold + List.fold_left_map (fun tc (hyps, fp) -> newgoal tc ~hyps fp) tc subgoals in @@ -564,11 +564,11 @@ module FApi = struct (* ------------------------------------------------------------------ *) let on_sub1i_goals (tt : int -> backward) (hds : handle list) (pe : proofenv) = - let do1 i pe hd = + let do1 pe i hd = let tc = tt i (tcenv1_of_penv hd pe) in assert (tc.tce_tcenv.tce_ctxt = []); (tc_penv tc, tc_opened tc) in - List.mapi_fold do1 pe hds + List.fold_left_mapi do1 pe hds (* ------------------------------------------------------------------ *) let on_sub1_goals (tt : backward) (hds : handle list) (pe : proofenv) = @@ -578,11 +578,11 @@ module FApi = struct let on_sub1i_map_goals (tt : int -> tcenv1 -> 'a * tcenv) (hds : handle list) (pe : proofenv) = - let do1 i pe hd = + let do1 pe i hd = let data, tc = tt i (tcenv1_of_penv hd pe) in assert (tc.tce_tcenv.tce_ctxt = []); (tc_penv tc, (tc_opened tc, data)) in - List.mapi_fold do1 pe hds + List.fold_left_mapi do1 pe hds (* ------------------------------------------------------------------ *) let on_sub1_map_goals diff --git a/src/ecCoreSubst.ml b/src/ecCoreSubst.ml index 7e0253c63c..24612e3a06 100644 --- a/src/ecCoreSubst.ml +++ b/src/ecCoreSubst.ml @@ -600,7 +600,7 @@ module Fsubst = struct (* ------------------------------------------------------------------ *) and add_bindings (s : f_subst) : bindings -> f_subst * bindings = - List.map_fold add_binding s + List.fold_left_map add_binding s (* ------------------------------------------------------------------ *) and add_mod_params (s : f_subst) (params : _) = diff --git a/src/ecEnv.ml b/src/ecEnv.ml index a83045d38d..8f07805c89 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -19,6 +19,7 @@ module Mp = EcPath.Mp module Sid = EcIdent.Sid module Mid = EcIdent.Mid module TC = EcTypeClass +module Sint = EcMaps.Sint module Mint = EcMaps.Mint (* -------------------------------------------------------------------- *) @@ -183,6 +184,7 @@ type preenv = { env_rwbase : Sp.t Mip.t; env_atbase : atbase Msym.t; env_redbase : mredinfo; + env_stdbase : setoid; env_ntbase : ntbase Mop.t; env_modlcs : Sid.t; (* declared modules *) env_item : theory_item list; (* in reverse order *) @@ -225,6 +227,13 @@ and atbase0 = path * [`Rigid | `Default] and atbase = atbase0 list Mint.t +and setoid = setoid1 Mp.t + +and setoid1 = { + spec : path; + morphisms : (path Mint.t) Mp.t; +} + (* -------------------------------------------------------------------- *) type env = preenv @@ -311,6 +320,7 @@ let empty gstate = env_rwbase = Mip.empty; env_atbase = Msym.empty; env_redbase = Mrd.empty; + env_stdbase = Mp.empty; env_ntbase = Mop.empty; env_modlcs = Sid.empty; env_item = []; @@ -611,7 +621,7 @@ module MC = struct let mc = lookup_mc qn env in let objs = odfl [] (mc |> omap (fun mc -> MMsym.all x (proj mc))) in let _, objs = - List.map_fold + List.fold_left_map (fun ps ((p, _) as obj)-> if Sip.mem p ps then (ps, None) @@ -1019,7 +1029,7 @@ module MC = struct in let (mc, submcs) = - List.map_fold mc1_of_module + List.fold_left_map mc1_of_module (empty_mc (if p2 = None then Some me.me_params else None)) me.me_comps @@ -1110,12 +1120,13 @@ module MC = struct (add2mc _up_rwbase x (expath x) mc, None) | Th_export _ | Th_addrw _ | Th_instance _ - | Th_auto _ | Th_reduction _ -> + | Th_auto _ | Th_reduction _ | Th_relation _ + | Th_morphism _ -> (mc, None) in let (mc, submcs) = - List.map_fold mc1_of_theory (empty_mc None) cth.cth_items + List.fold_left_map mc1_of_theory (empty_mc None) cth.cth_items in ((x, mc), List.rev_pmap identity submcs) @@ -1582,6 +1593,35 @@ module Auto = struct Msym.values env.env_atbase |> List.map flatten_db |> List.flatten end +(* -------------------------------------------------------------------- *) +module Setoid = struct + type nonrec setoid1 = setoid1 + + let update_relation_db ((oppath, axpath) : path * path) (db : setoid) = + Mp.add oppath { spec = axpath; morphisms = Mp.empty; } db + + let add_relation ((oppath, axpath) : path * path) (env : env) = + let item = mkitem import0 (Th_relation (oppath, axpath)) in + { env with + env_stdbase = update_relation_db (oppath, axpath) env.env_stdbase; + env_item = item :: env.env_item; } + + let get_relation (env : env) (oppath : path) : setoid1 option = + Mp.find_opt oppath env.env_stdbase + + let update_morphism_db ((rel, op, ax, pos) : path * path * path * int) (db : setoid) = + Mp.change (fun db1 -> + Some { (oget db1) with morphisms = + Mp.change (fun m -> Some (Mint.add pos ax (odfl Mint.empty m))) op (oget db1).morphisms } + ) rel db + + let add_morphism ((rel, op, ax, pos) : path * path * path * int) (env : env) = + let item = mkitem import0 (Th_morphism (rel, op, ax, pos)) in + { env with + env_stdbase = update_morphism_db (rel, op, ax, pos) env.env_stdbase; + env_item = item :: env.env_item; } +end + (* -------------------------------------------------------------------- *) module Fun = struct type t = EcModules.function_ @@ -2975,6 +3015,17 @@ module Theory = struct in bind_base_th for1 + (* ------------------------------------------------------------------ *) + let bind_std_th = + let for1 _path db = function + | Th_relation r -> + Some (Setoid.update_relation_db r db) + | Th_morphism m -> + Some (Setoid.update_morphism_db m db) + | _ -> None + + in bind_base_th for1 + (* ------------------------------------------------------------------ *) let bind_nt_th = let for1 path base = function @@ -3022,12 +3073,14 @@ module Theory = struct let env_tc = bind_tc_th thname env.env_tc items in let env_rwbase = bind_br_th thname env.env_rwbase items in let env_atbase = bind_at_th thname env.env_atbase items in + let env_stdbase = bind_std_th thname env.env_stdbase items in let env_ntbase = bind_nt_th thname env.env_ntbase items in let env_redbase = bind_rd_th thname env.env_redbase items in let env = { env with env_tci ; env_tc ; env_rwbase; - env_atbase; env_ntbase; env_redbase; } + env_atbase; env_stdbase; env_ntbase; + env_redbase; } in add_restr_th thname env items @@ -3088,7 +3141,12 @@ module Theory = struct | Th_baserw (x, _) -> MC.import_rwbase (xpath x) env - | Th_addrw _ | Th_instance _ | Th_auto _ | Th_reduction _ -> + | Th_addrw _ + | Th_instance _ + | Th_auto _ + | Th_reduction _ + | Th_relation _ + | Th_morphism _ -> env in @@ -3105,7 +3163,7 @@ module Theory = struct (* ------------------------------------------------------------------ *) let rec filter clears root cleared items = snd_map (List.pmap identity) - (List.map_fold (filter1 clears root) cleared items) + (List.fold_left_map (filter1 clears root) cleared items) and filter_th clears root cleared items = let mempty = List.exists (EcPath.p_equal root) clears in @@ -3241,6 +3299,7 @@ module Theory = struct env_tc = bind_tc_th thpath env.env_tc cth.cth_items; env_rwbase = bind_br_th thpath env.env_rwbase cth.cth_items; env_atbase = bind_at_th thpath env.env_atbase cth.cth_items; + env_stdbase = bind_std_th thpath env.env_stdbase cth.cth_items; env_ntbase = bind_nt_th thpath env.env_ntbase cth.cth_items; env_redbase = bind_rd_th thpath env.env_redbase cth.cth_items; env_thenvs = Mp.set_union env.env_thenvs compiled.compiled; } @@ -3444,7 +3503,7 @@ module LDecl = struct let do1 hyps s = let id = fresh_id hyps s in (add_local id (LD_var (tbool, None)) hyps, id) - in List.map_fold do1 hyps names + in List.fold_left_map do1 hyps names (* ------------------------------------------------------------------ *) type hyps = { diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 0ed659eb22..b157b7374b 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -413,6 +413,21 @@ module Reduction : sig val get : topsym -> env -> rule list end +(* -------------------------------------------------------------------- *) +type setoid1 = { + spec : path; + morphisms : (path EcMaps.Mint.t) Mp.t; +} + +module Setoid : sig + type nonrec setoid1 = setoid1 + + val add_relation : path * path -> env -> env + val get_relation : env -> path -> setoid1 option + + val add_morphism : path * path * path * int -> env -> env +end + (* -------------------------------------------------------------------- *) module Auto : sig type base0 = path * [`Rigid | `Default] diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index 2ca2e691b1..96d8690bcb 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -249,10 +249,11 @@ module LowRewrite = struct | LRW_IdRewriting | LRW_RPatternNoMatch | LRW_RPatternNoRuleMatch + | LRW_InvalidSetoidContext exception RewriteError of error - let rec find_rewrite_patterns ~inpred (dir : rwside) pt = + let rec find_rewrite_patterns ~inpred (dir : rwside) pt : (pt_ev * rwmode * (form * form)) list = let hyps = pt.PT.ptev_env.PT.pte_hy in let env = LDecl.toenv hyps in let pt = { pt with ptev_ax = snd (PT.concretize pt) } in @@ -270,7 +271,13 @@ module LowRewrite = struct let pt' = apply_pterm_to_arg_r pt' (PVASub pt) in [(pt', `Eq, (f, f_false))] - | _ -> [] + | _ -> begin + try + EcSetoid.as_instance env (destr_op_app ax) + |> Option.map (fun (instance, (f1, f2)) -> (pt, `Setoid instance, (f1, f2))) + |> Option.to_list + with DestrError _ -> [] + end and split ax = match EcFol.sform_of_form ax with @@ -329,7 +336,7 @@ module LowRewrite = struct type rwinfos = rwside * EcFol.form option * EcMatching.occ option let t_rewrite_r ?(mode = `Full) ?target ((s, prw, o) : rwinfos) pt tc = - let hyps, tgfp = FApi.tc1_flat ?target tc in + let env, hyps, tgfp = FApi.tc1_eflat ?target tc in let modes = match mode with @@ -366,7 +373,7 @@ module LowRewrite = struct | PT.FindOccFailure `MatchFailure -> raise (RewriteError LRW_RPatternNoRuleMatch) | PT.FindOccFailure `IncompleteMatch -> - raise (RewriteError LRW_CannotInfer) + raise (RewriteError LRW_CannotInfer) end in if not occmode.k_keyed then begin @@ -376,23 +383,42 @@ module LowRewrite = struct end; let pt = fst (PT.concretize pt) in + + let exception InvalidSetoidContext in + let cpos = + let postcheck (instance : EcSetoid.instance) (lazy ctxt) = + if not (EcSetoid.valid_setoid_context env instance ctxt) then + raise InvalidSetoidContext in + + let postcheck = + match mode with + | `Setoid instance -> postcheck instance + | _ -> fun _ -> () in + try FPosition.select_form + ~postcheck:(fun _ ctxt _ -> postcheck ctxt; true) ~xconv:`AlphaEq ~keyed:occmode.k_keyed hyps o subf tgfp - with InvalidOccurence -> raise (RewriteError (LRW_InvalidOccurence)) + with + | InvalidOccurence -> + raise (RewriteError (LRW_InvalidOccurence)) + | InvalidSetoidContext -> + raise (RewriteError (LRW_InvalidSetoidContext)) in EcLowGoal.t_rewrite ~keyed:occmode.k_keyed ?target ~mode pt (s, Some cpos) tc in let rec do_first = function - | [] -> raise (RewriteError LRW_NothingToRewrite) + | [] -> + raise (RewriteError LRW_NothingToRewrite) + + | [pt, mode, (f1, f2)] -> + for1 (pt, mode, (f1, f2)) - | (pt, mode, (f1, f2)) :: pts -> - try for1 (pt, mode, (f1, f2)) - with RewriteError _ -> - do_first pts + | pt :: pts -> + try do_first [pt] with RewriteError _ -> do_first pts in let pts = find_rewrite_patterns s pt in @@ -590,6 +616,8 @@ let process_rewrite1_core ?mode ?(close = true) ?target (s, p, o) pt tc = tc_error !!tc "r-pattern does not match the goal" | LowRewrite.LRW_RPatternNoRuleMatch -> tc_error !!tc "r-pattern does not match the rewriting rule" + | LowRewrite.LRW_InvalidSetoidContext -> + tc_error !!tc "invalid setoid-rewrite position" (* -------------------------------------------------------------------- *) let process_delta ~und_delta ?target (s, o, p) tc = @@ -2118,7 +2146,7 @@ let process_exists args (tc : tcenv1) = PT.check_pterm_arg pte (x, xty) f arg.ptea_arg in - let _concl, args = List.map_fold for1 (FApi.tc1_goal tc) args in + let _concl, args = List.fold_left_map for1 (FApi.tc1_goal tc) args in if not (PT.can_concretize pte) then tc_error !!tc "cannot infer all placeholders"; diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli index 317163fd6e..b07e1567d4 100644 --- a/src/ecHiGoal.mli +++ b/src/ecHiGoal.mli @@ -41,6 +41,7 @@ module LowRewrite : sig | LRW_IdRewriting | LRW_RPatternNoMatch | LRW_RPatternNoRuleMatch + | LRW_InvalidSetoidContext exception RewriteError of error diff --git a/src/ecLexer.mll b/src/ecLexer.mll index f3552cb5ca..0034f4c1b7 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -191,6 +191,8 @@ "inductive" , INDUCTIVE ; (* KW: global *) "notation" , NOTATION ; (* KW: global *) "abbrev" , ABBREV ; (* KW: global *) + "relation" , RELATION ; (* KW: global *) + "morphism" , MORPHISM ; (* KW: global *) "require" , REQUIRE ; (* KW: global *) "theory" , THEORY ; (* KW: global *) "abstract" , ABSTRACT ; (* KW: global *) diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 88bd20a4f5..573bd593b8 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -1657,7 +1657,7 @@ let t_or_intro_prind ?reduce (side : side) (tc : tcenv1) = (* -------------------------------------------------------------------- *) type rwspec = [`LtoR|`RtoL] * ptnpos option -type rwmode = [`Bool | `Eq] +type rwmode = [`Bool | `Eq | `Setoid of EcSetoid.instance] (* -------------------------------------------------------------------- *) let t_rewrite @@ -1669,24 +1669,26 @@ let t_rewrite let env = LDecl.toenv hyps in let (pt, ax) = LowApply.check `Elim pt (`Tc (tc, target)) in - let (pt, left, right) = + let (left, right), setoid = let doit ax = match sform_of_form ax, mode with - | SFeq (f1, f2), (None | Some `Eq) -> (pt, f1, f2) - | SFiff (f1, f2), (None | Some `Eq) -> (pt, f1, f2) + | SFeq (f1, f2), (None | Some `Eq) -> (f1, f2), None + | SFiff (f1, f2), (None | Some `Eq) -> (f1, f2), None | SFnot f, (None | Some `Bool) when s = `LtoR && donot -> - let ptev_env = ptenv_of_penv hyps (RApi.tc_penv tc) in - let pt = { ptev_env; ptev_pt = pt; ptev_ax = ax } in - let pt' = pt_of_global_r ptev_env LG.p_negeqF [] in - let pt' = apply_pterm_to_arg_r pt' (PVAFormula f) in - let pt' = apply_pterm_to_arg_r pt' (PVASub pt) in - let pt, _ = concretize pt' in - pt, f, f_false + (f, f_false), None | _, (None | Some `Bool) when s = `LtoR && ER.EqTest.for_type env ax.f_ty tbool - -> (pt, ax, f_true) + -> (ax, f_true), None + + | _, Some `Setoid _ (* FIXME: check instance *) -> + let instance, (f1, f2) = + try + oget ~exn:InvalidProofTerm (EcSetoid.as_instance env (destr_op_app ax)) + with DestrError _ -> raise InvalidProofTerm + in + (f1, f2), Some instance | _ -> raise TTC.NoMatch in oget ~exn:InvalidProofTerm (TTC.lazy_destruct hyps doit ax) @@ -1698,7 +1700,12 @@ let t_rewrite | `RtoL -> (right, left ) in - let change f = + let change ctxt f = + setoid |> Option.iter (fun instance -> + if not (EcSetoid.valid_setoid_context env instance (Lazy.force ctxt)) then + raise InvalidProofTerm + ); + if not (EcReduction.is_conv hyps f left) then raise InvalidGoalShape; right in @@ -1708,9 +1715,8 @@ let t_rewrite | None -> FPosition.select_form ?keyed ?xconv hyps None left tgfp | Some pos -> pos in - let tgfp = - try FPosition.map npos change tgfp + try FPosition.map_with_ctxt npos change tgfp with InvalidPosition -> raise InvalidGoalShape in diff --git a/src/ecLowGoal.mli b/src/ecLowGoal.mli index d7f4421ab4..b94f18b864 100644 --- a/src/ecLowGoal.mli +++ b/src/ecLowGoal.mli @@ -18,7 +18,6 @@ exception InvalidProofTerm (* invalid proof term *) type side = [`Left|`Right] type lazyred = [`Full | `NoDelta | `None] - (* -------------------------------------------------------------------- *) val (@!) : FApi.backward -> FApi.backward -> FApi.backward val (@+) : FApi.backward -> FApi.backward list -> FApi.backward @@ -219,7 +218,7 @@ val full_subst_kind : subst_kind val empty_subst_kind : subst_kind type rwspec = [`LtoR|`RtoL] * ptnpos option -type rwmode = [`Bool | `Eq] +type rwmode = [`Bool | `Eq | `Setoid of EcSetoid.instance] val t_rewrite : ?xconv:xconv -> ?keyed:bool -> ?target:ident -> ?mode:rwmode -> ?donot:bool diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 79244af03e..eb627b9a26 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -373,7 +373,7 @@ let add_lv_subst env lv m s = | LvTuple pvs -> let s, ids = - List.map_fold (fun s (pv,t) -> + List.fold_left_map (fun s (pv,t) -> let id = id_of_pv pv m in let s = PVM.add env pv m (f_local id t) s in s, (id,t)) s pvs in diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 8de810498d..640d8acfd7 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -570,7 +570,7 @@ let f_match_core opts hyps (ue, ev) f1 f2 = failure (); let xsubst, bindings = - List.map_fold + List.fold_left_map (fun xsubst x -> let x, xty = (destr_local x, x.f_ty) in let nx = EcIdent.fresh x in @@ -886,8 +886,137 @@ exception InvalidPosition exception InvalidOccurence module FPosition = struct + (* ------------------------------------------------------------------ *) type select = [`Accept of int | `Continue] + (* ------------------------------------------------------------------ *) + type path = int list + + (* ------------------------------------------------------------------ *) + type ctxt1_r = + | CT_AppTop of form list + | CT_AppArg of form * (form list * form list) + | CT_Tuple of form list * form list + | CT_LetVal of lpattern * form + | CT_LetBody of lpattern * form + | CT_Quant of quantif * bindings + | CT_Proj of int + | CT_IfCond of form * form + | CT_IfBranch of form * ([`Then | `Else] * form) + | CT_MatchCond of ty * form list + | CT_MatchBranch of ty * form * (form list * form list) + | CT_PrArgs of { pr_event: form; ctxt: prctxt; } + | CT_PrEvent of { pr_args: form; ctxt: prctxt; } + | CT_HoareFPr of { hf_po: form; ctxt: hoarectxt; } + | CT_HoareFPo of { hf_pr: form; ctxt: hoarectxt; } + | CT_BdHoareFPr of { bhf_po: form; bhf_bd: form; ctxt: bdhoarectxt; } + | CT_BdHoareFPo of { bhf_pr: form; bhf_bd: form; ctxt: bdhoarectxt; } + | CT_BdHoareFBd of { bhf_pr: form; bhf_po: form; ctxt: bdhoarectxt; } + | CT_EHoareFPr of { ehf_po: form; ctxt: ehoarectxt; } + | CT_EHoareFPo of { ehf_pr: form; ctxt: ehoarectxt; } + | CT_EquivFPr of { ef_po: form; ctxt: equivctxt; } + | CT_EquivFPo of { ef_pr: form; ctxt: equivctxt; } + + and ctxt1 = { ctxt: ctxt1_r; ty: ty; } + + and ctxt = ctxt1 list + + and prctxt = { pr_fun: EcPath.xpath; pr_mem: memory; } + and hoarectxt = { hf_f: EcPath.xpath; } + and bdhoarectxt = { bhf_f: EcPath.xpath; bhf_cmp: hoarecmp; } + and ehoarectxt = { ehf_f: EcPath.xpath; } + and equivctxt = { ef_fl: EcPath.xpath; ef_fr: EcPath.xpath; } + + (* ------------------------------------------------------------------ *) + let ctxt_of_path (f : form) (path : path) : ctxt = + let ctxt_of_pr ({ pr_fun; pr_mem; } : pr) : prctxt = + { pr_fun; pr_mem; } + + and ctxt_of_hoare ({ hf_f } : sHoareF) : hoarectxt = + { hf_f } + + and ctxt_of_bdhoare ({ bhf_f; bhf_cmp; } : bdHoareF) : bdhoarectxt = + { bhf_f; bhf_cmp; } + + and ctxt_of_ehoare ({ ehf_f; } : eHoareF) : ehoarectxt = + { ehf_f } + + and ctxt_of_equiv ({ ef_fl; ef_fr; } : equivF) : equivctxt = + { ef_fl; ef_fr; } + + in + + let for1 (f : form) (i : int) = + let f, (ctxt : ctxt1_r) = + match f.f_node, i with + | Fapp (f, fs), 0 -> + f, CT_AppTop fs + + | Fapp (top, fs), i when 0 < i && i <= List.length fs -> + let argsl, f, argsr = List.pivot_at (i - 1) fs in + f, CT_AppArg (top, (argsl, argsr)) + + | Ftuple args, i when 0 <= i && i < List.length args -> + let largs, f, rargs = List.pivot_at i args in + f, CT_Tuple (largs, rargs) + + | Flet (lv, f1, f2), 0 -> f1, CT_LetVal (lv, f2) + | Flet (lv, f1, f2), 1 -> f2, CT_LetVal (lv, f1) + + | Fquant (q, bds, f), 0 -> f, CT_Quant (q, bds) + + | Fproj (f, i), 0 -> f, CT_Proj i + + | Fif (c, f1, f2), 0 -> c, CT_IfCond (f1, f2) + | Fif (c, f1, f2), 1 -> f1, CT_IfBranch (c, (`Then, f2)) + | Fif (c, f1, f2), 2 -> f2, CT_IfBranch (c, (`Then, f1)) + + | Fmatch (c, bs, ty), 0 -> c, CT_MatchCond (ty, bs) + | Fmatch (c, bs, ty), i when 0 < i && i <= List.length bs -> + let bsl, b, bsr = List.pivot_at (i - 1) bs in + b, CT_MatchBranch (ty, c, (bsl, bsr)) + + | Fpr ({ pr_args; pr_event; } as pr), 0 -> + pr_args, CT_PrArgs { pr_event; ctxt = ctxt_of_pr pr } + + | Fpr ({ pr_args; pr_event; } as pr), 1 -> + pr_event, CT_PrEvent { pr_args; ctxt = ctxt_of_pr pr } + + | FhoareF ({ hf_pr; hf_po } as hf), 0 -> + hf_pr, CT_HoareFPr { hf_po; ctxt = ctxt_of_hoare hf } + + | FhoareF ({ hf_pr; hf_po } as hf), 1 -> + hf_po, CT_HoareFPo { hf_pr; ctxt = ctxt_of_hoare hf } + + | FbdHoareF ({ bhf_pr; bhf_po; bhf_bd } as bhf), 0 -> + bhf_po, CT_BdHoareFPo { bhf_pr; bhf_bd; ctxt = ctxt_of_bdhoare bhf } + + | FbdHoareF ({ bhf_pr; bhf_po; bhf_bd } as bhf), 1 -> + bhf_pr, CT_BdHoareFPr { bhf_po; bhf_bd; ctxt = ctxt_of_bdhoare bhf } + + | FbdHoareF ({ bhf_pr; bhf_po; bhf_bd } as bhf), 2 -> + bhf_bd, CT_BdHoareFBd { bhf_pr; bhf_po; ctxt = ctxt_of_bdhoare bhf } + + | FeHoareF ({ ehf_pr; ehf_po } as ehf), 0 -> + ehf_pr, CT_EHoareFPr { ehf_po; ctxt = ctxt_of_ehoare ehf } + + | FeHoareF ({ ehf_pr; ehf_po } as ehf), 1 -> + ehf_po, CT_EHoareFPo { ehf_pr; ctxt = ctxt_of_ehoare ehf } + + | FequivF ({ ef_pr; ef_po } as ef), 0 -> + ef_pr, CT_EquivFPr { ef_po; ctxt = ctxt_of_equiv ef } + + | FequivF ({ ef_pr; ef_po } as ef), 1 -> + ef_po, CT_EquivFPo { ef_pr; ctxt = ctxt_of_equiv ef } + + | _ -> + assert false + + in f, { ctxt; ty = f.f_ty; } + + in + snd (List.fold_left_map for1 f path) + (* ------------------------------------------------------------------ *) let empty : ptnpos = Mint.empty @@ -905,139 +1034,145 @@ module FPosition = struct String.concat ", " items (* ------------------------------------------------------------------ *) - and tostring1 = function + and tostring1 (p : ptnpos1) = + match p with | `Select i when i < 0 -> "-" | `Select i -> Printf.sprintf "-(%d)" i | `Sub p -> tostring p (* ------------------------------------------------------------------ *) - let occurences = - let rec doit1 n p = - match p with - | `Select _ -> n+1 - | `Sub p -> doit n p - - and doit n (ps : ptnpos) = - Mint.fold (fun _ p n -> doit1 n p) ps n - - in - fun p -> doit 0 p + type postcheck = Sid.t -> ctxt lazy_t -> form -> bool (* ------------------------------------------------------------------ *) - let filter ((mode, s) : occ) = - let rec doit1 n p = - match p with - | `Select _ -> begin - match mode with - | `Inclusive -> (n+1, if Sint.mem n s then Some p else None ) - | `Exclusive -> (n+1, if Sint.mem n s then None else Some p) - end + let select_with_ctxt + ?(postcheck : postcheck option) + ?(o : occ option) + (test : Sid.t -> ctxt lazy_t -> form -> select) + (f0 : form) + = + let module T = struct + type t = [ + | `WithCtxt of Sid.t * form list + | `WithSubCtxt of (Sid.t * form) list + ] + end in - | `Sub p -> begin - match doit n p with - | (n, sub) when Mint.is_empty sub -> (n, None) - | (n, sub) -> (n, Some (`Sub sub)) - end + let postcheck = Option.value ~default:(fun _ _ _ -> true) postcheck in + let omode, o = Option.value ~default:(`Exclusive, Sint.empty) o in - and doit n (ps : ptnpos) = - Mint.mapi_filter_fold (fun _ p n -> doit1 n p) ps n + let norm_path (path : path) : path = List.tl (List.rev path) in - in - fun p -> snd (doit 1 p) + let rec doit1 (n : int) (path : path) (vars : Sid.t) (fp : form) : int * (ptnpos1 option) = + let ctxt = lazy (ctxt_of_path f0 (norm_path path)) in - (* ------------------------------------------------------------------ *) - let is_occurences_valid o cpos = - let (min, max) = (Sint.min_elt o, Sint.max_elt o) in - not (min < 1 || max > occurences cpos) + match test vars ctxt fp with + | `Accept i -> begin + let keep = + match omode with + | `Inclusive -> (Sint.mem n o) + | `Exclusive -> not (Sint.mem n o) in - (* ------------------------------------------------------------------ *) - let select ?o test = - let rec doit1 ctxt pos fp = - match test ctxt fp with - | `Accept i -> Some (`Select i) + let keep = keep && postcheck vars ctxt fp in + + n+1, (if keep then Some (`Select i) else None) + end + | `Continue -> begin - let subp = + let n, subp = match fp.f_node with - | Fif (c, f1, f2) -> doit pos (`WithCtxt (ctxt, [c; f1; f2])) - | Fapp (f, fs) -> doit pos (`WithCtxt (ctxt, f :: fs)) - | Ftuple fs -> doit pos (`WithCtxt (ctxt, fs)) + | Fif (c, f1, f2) -> doit n path (`WithCtxt (vars, [c; f1; f2])) + | Fapp (f, fs) -> doit n path (`WithCtxt (vars, f :: fs)) + | Ftuple fs -> doit n path (`WithCtxt (vars, fs)) | Fmatch (b, fs, _) -> - doit pos (`WithCtxt (ctxt, b :: fs)) + doit n path (`WithCtxt (vars, b :: fs)) | Fquant (_, b, f) -> - let ctxt = List.fold_left ((^~) Sid.add) ctxt (List.fst b) in - doit pos (`WithCtxt (ctxt, [f])) + let ctxt = List.fold_left ((^~) Sid.add) vars (List.fst b) in + doit n path (`WithCtxt (ctxt, [f])) | Flet (lp, f1, f2) -> - let subctxt = List.fold_left ((^~) Sid.add) ctxt (lp_ids lp) in - doit pos (`WithSubCtxt [(ctxt, f1); (subctxt, f2)]) + let subctxt = List.fold_left ((^~) Sid.add) vars (lp_ids lp) in + doit n path (`WithSubCtxt [(vars, f1); (subctxt, f2)]) | Fproj (f, _) -> - doit pos (`WithCtxt (ctxt, [f])) + doit n path (`WithCtxt (vars, [f])) | Fpr pr -> - let subctxt = Sid.add pr.pr_mem ctxt in - doit pos (`WithSubCtxt [(ctxt, pr.pr_args); (subctxt, pr.pr_event)]) + let subvars = Sid.add pr.pr_mem vars in + doit n path (`WithSubCtxt [(vars, pr.pr_args); (subvars, pr.pr_event)]) | FhoareF hs -> - doit pos (`WithCtxt (Sid.add EcFol.mhr ctxt, [hs.hf_pr; hs.hf_po])) + doit n path (`WithCtxt (Sid.add EcFol.mhr vars, [hs.hf_pr; hs.hf_po])) - (* TODO: A: From what I undertand, there is an error there: - it should be (subctxt, hs.bhf_bd) *) | FbdHoareF hs -> - let subctxt = Sid.add EcFol.mhr ctxt in - doit pos (`WithSubCtxt ([(subctxt, hs.bhf_pr); - (subctxt, hs.bhf_po); - ( ctxt, hs.bhf_bd)])) + let subvars = Sid.add EcFol.mhr vars in + doit n path (`WithCtxt (subvars, [hs.bhf_pr; hs.bhf_po; hs.bhf_bd])) | FequivF es -> - let ctxt = Sid.add EcFol.mleft ctxt in - let ctxt = Sid.add EcFol.mright ctxt in - doit pos (`WithCtxt (ctxt, [es.ef_pr; es.ef_po])) + let vars = Sid.add EcFol.mleft vars in + let vars = Sid.add EcFol.mright vars in + doit n path (`WithCtxt (vars, [es.ef_pr; es.ef_po])) - | _ -> None + | _ -> n, None in - omap (fun p -> `Sub p) subp + (n, omap (fun p -> `Sub p) subp) end - and doit pos fps = - let fps = + and doit (n : int) (path : path) (fps : T.t) : int * (ptnpos option) = + let n, fps = match fps with | `WithCtxt (ctxt, fps) -> - List.mapi - (fun i fp -> - doit1 ctxt (i::pos) fp |> omap (fun p -> (i, p))) - fps + List.fold_left_mapi + (fun (n : int) (i : int) (fp : form) -> + doit1 n (i :: path) ctxt fp |> snd_map (omap (fun p -> (i, p)))) + n fps | `WithSubCtxt fps -> - List.mapi - (fun i (ctxt, fp) -> - doit1 ctxt (i::pos) fp |> omap (fun p -> (i, p))) - fps + List.fold_left_mapi + (fun (n : int) (i : int) ((ctxt, fp) : Sid.t * form) -> + doit1 n (i :: path) ctxt fp |> snd_map (omap (fun p -> (i, p)))) + n fps in - let fps = List.pmap identity fps in - match fps with - | [] -> None - | _ -> Some (Mint.of_list fps) + let fps = + match List.pmap identity fps with + | [] -> None + | fps -> Some (Mint.of_list fps) in + + (n, fps) in - fun fp -> - let cpos = - match doit [] (`WithCtxt (Sid.empty, [fp])) with - | None -> Mint.empty - | Some p -> p - in - match o with - | None -> cpos - | Some o -> - if not (is_occurences_valid (snd o) cpos) then - raise InvalidOccurence; - filter o cpos + + if not (Sint.is_empty o) && Sint.min_elt o < 1 then + raise InvalidOccurence; + + let n, p = doit 1 [] (`WithCtxt (Sid.empty, [f0])) in + + if not (Sint.is_empty o) && Sint.max_elt o >= n then + raise InvalidOccurence; + + Option.value ~default:empty p (* ------------------------------------------------------------------ *) - let select_form ?(xconv = `Conv) ?(keyed = false) hyps o p target = + let select + ?(postcheck : postcheck option) + ?(o : occ option) + (test : Sid.t -> form -> select) + (f : form) + = + select_with_ctxt ?postcheck ?o (fun vars _ f -> test vars f) f + + (* ------------------------------------------------------------------ *) + let select_form + ?(postcheck : postcheck option) + ?(xconv : EcReduction.xconv = `Conv) + ?(keyed : bool = false) + (hyps : LDecl.hyps) + (o : occ option) + (p : form) + (target : form) + : ptnpos = let na = List.length (snd (EcFol.destr_app p)) in let kmatch key tp = @@ -1058,8 +1193,10 @@ module FPosition = struct | _ -> `NoKey in - let test xconv _ tp = - if not (keycheck tp key) then `Continue else begin + let test xconv _ _ tp = + if not (keycheck tp key) then + `Continue + else begin let (tp, ti) = match tp.f_node with | Fapp (h, hargs) when List.length hargs > na -> @@ -1070,23 +1207,26 @@ module FPosition = struct if EcReduction.xconv xconv hyps p tp then `Accept ti else `Continue end - in select ?o (test xconv) target + in select_with_ctxt ?postcheck ?o (test xconv) target (* ------------------------------------------------------------------ *) - let map (p : ptnpos) (tx : form -> form) (f : form) = - let rec doit1 p fp = + let map_with_ctxt (p : ptnpos) (tx : ctxt Lazy.t -> form -> form) (f0 : form) = + let rec doit1 (path : path) (p : ptnpos1) (fp : form) = + let norm_path (path : path) : path = List.tl (List.rev path) in + match p with - | `Select i when i < 0 -> tx fp + | `Select i when i < 0 -> + tx (lazy (ctxt_of_path f0 (norm_path path))) fp | `Select i -> begin let (f, fs) = EcFol.destr_app fp in if List.length fs < i then raise InvalidPosition; let (fs1, fs2) = List.takedrop i fs in let f' = f_app f fs1 (toarrow (List.map f_ty fs2) fp.f_ty) in - f_app (tx f') fs2 fp.f_ty + f_app (tx (lazy (ctxt_of_path f0 (norm_path path))) f') fs2 fp.f_ty end - | `Sub p -> begin + | `Sub p -> begin match fp.f_node with | Flocal _ -> raise InvalidPosition | Fpvar _ -> raise InvalidPosition @@ -1095,56 +1235,51 @@ module FPosition = struct | Fint _ -> raise InvalidPosition | Fquant (q, b, f) -> - let f' = as_seq1 (doit p [f]) in - f_quant q b f' + f_quant q b (as_seq1 (doit path p [f])) - | Fif (c, f1, f2) -> - let (c', f1', f2') = as_seq3 (doit p [c; f1; f2]) in - f_if c' f1' f2' + | Fif (c, f1, f2) -> + let (c, f1, f2) = as_seq3 (doit path p [c; f1; f2]) in + f_if c f1 f2 | Fmatch (b, fs, ty) -> - let bfs = doit p (b :: fs) in + let bfs = doit path p (b :: fs) in EcCoreFol.f_match (List.hd bfs) (List.tl bfs) ty | Fapp (f, fs) -> begin - match doit p (f :: fs) with + match doit path p (f :: fs) with | [] -> assert false - | f' :: fs' -> - f_app f' fs' (fp.f_ty) + | f :: fs -> f_app f fs (fp.f_ty) end | Ftuple fs -> - let fs' = doit p fs in - f_tuple fs' + f_tuple (doit path p fs) | Fproj (f, i) -> - f_proj (as_seq1 (doit p [f])) i fp.f_ty + f_proj (as_seq1 (doit path p [f])) i fp.f_ty | Flet (lv, f1, f2) -> - let (f1', f2') = as_seq2 (doit p [f1; f2]) in - f_let lv f1' f2' + let (f1, f2) = as_seq2 (doit path p [f1; f2]) in + f_let lv f1 f2 | Fpr pr -> - let (args', event') = as_seq2 (doit p [pr.pr_args; pr.pr_event]) in - f_pr pr.pr_mem pr.pr_fun args' event' + let (args, event) = as_seq2 (doit path p [pr.pr_args; pr.pr_event]) in + f_pr pr.pr_mem pr.pr_fun args event | FhoareF hf -> - let (hf_pr, hf_po) = as_seq2 (doit p [hf.hf_pr; hf.hf_po]) in + let (hf_pr, hf_po) = as_seq2 (doit path p [hf.hf_pr; hf.hf_po]) in f_hoareF_r { hf with hf_pr; hf_po; } | FeHoareF hf -> - let (ehf_pr, ehf_po) = - as_seq2 (doit p [hf.ehf_pr; hf.ehf_po;]) - in + let (ehf_pr, ehf_po) = as_seq2 (doit path p [hf.ehf_pr; hf.ehf_po;]) in f_eHoareF_r { hf with ehf_pr; ehf_po; } | FbdHoareF hf -> - let sub = doit p [hf.bhf_pr; hf.bhf_po; hf.bhf_bd] in + let sub = doit path p [hf.bhf_pr; hf.bhf_po; hf.bhf_bd] in let (bhf_pr, bhf_po, bhf_bd) = as_seq3 sub in f_bdHoareF_r { hf with bhf_pr; bhf_po; bhf_bd; } | FequivF ef -> - let (ef_pr, ef_po) = as_seq2 (doit p [ef.ef_pr; ef.ef_po]) in + let (ef_pr, ef_po) = as_seq2 (doit path p [ef.ef_pr; ef.ef_po]) in f_equivF_r { ef with ef_pr; ef_po; } | FhoareS _ -> raise InvalidPosition @@ -1154,7 +1289,7 @@ module FPosition = struct | FeagerF _ -> raise InvalidPosition end - and doit ps fps = + and doit (path : path) (ps : ptnpos) (fps : form list) = match Mint.is_empty ps with | true -> fps | false -> @@ -1162,12 +1297,17 @@ module FPosition = struct and imax = fst (Mint.max_binding ps) in if imin < 0 || imax >= List.length fps then raise InvalidPosition; - let fps = List.mapi (fun i x -> (x, Mint.find_opt i ps)) fps in - let fps = List.map (function (f, None) -> f | (f, Some p) -> doit1 p f) fps in - fps + fps |> List.mapi (fun i f -> + match Mint.find_opt i ps with + | None -> f + | Some p -> doit1 (i :: path) p f + ) - in - as_seq1 (doit p [f]) + in as_seq1 (doit [] p [f0]) + + (* ------------------------------------------------------------------ *) + let map (p : ptnpos) (tx : form -> form) (f : form) = + map_with_ctxt p (fun _ -> tx) f (* ------------------------------------------------------------------ *) let reroot (root : int list) (p : ptnpos) = diff --git a/src/ecMatching.mli b/src/ecMatching.mli index 552f6f5319..d03d7de5de 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -222,8 +222,47 @@ exception InvalidPosition exception InvalidOccurence module FPosition : sig + open EcMemory + type select = [`Accept of int | `Continue] + (* ------------------------------------------------------------------ *) + type ctxt1_r = + | CT_AppTop of form list + | CT_AppArg of form * (form list * form list) + | CT_Tuple of form list * form list + | CT_LetVal of lpattern * form + | CT_LetBody of lpattern * form + | CT_Quant of quantif * bindings + | CT_Proj of int + | CT_IfCond of form * form + | CT_IfBranch of form * ([`Then | `Else] * form) + | CT_MatchCond of ty * form list + | CT_MatchBranch of ty * form * (form list * form list) + | CT_PrArgs of { pr_event: form; ctxt: prctxt; } + | CT_PrEvent of { pr_args: form; ctxt: prctxt; } + | CT_HoareFPr of { hf_po: form; ctxt: hoarectxt; } + | CT_HoareFPo of { hf_pr: form; ctxt: hoarectxt; } + | CT_BdHoareFPr of { bhf_po: form; bhf_bd: form; ctxt: bdhoarectxt; } + | CT_BdHoareFPo of { bhf_pr: form; bhf_bd: form; ctxt: bdhoarectxt; } + | CT_BdHoareFBd of { bhf_pr: form; bhf_po: form; ctxt: bdhoarectxt; } + | CT_EHoareFPr of { ehf_po: form; ctxt: ehoarectxt; } + | CT_EHoareFPo of { ehf_pr: form; ctxt: ehoarectxt; } + | CT_EquivFPr of { ef_po: form; ctxt: equivctxt; } + | CT_EquivFPo of { ef_pr: form; ctxt: equivctxt; } + + and ctxt1 = { ctxt: ctxt1_r; ty: ty; } + + and ctxt = ctxt1 list + + and prctxt = { pr_fun: EcPath.xpath; pr_mem: memory; } + and hoarectxt = { hf_f: EcPath.xpath; } + and bdhoarectxt = { bhf_f: EcPath.xpath; bhf_cmp: hoarecmp; } + and ehoarectxt = { ehf_f: EcPath.xpath; } + and equivctxt = { ef_fl: EcPath.xpath; ef_fr: EcPath.xpath; } + + type postcheck = Sid.t -> ctxt lazy_t -> form -> bool + val empty : ptnpos val is_empty : ptnpos -> bool @@ -232,16 +271,31 @@ module FPosition : sig val tostring : ptnpos -> string - val select : ?o:occ -> (Sid.t -> form -> select) -> form -> ptnpos - - val select_form : ?xconv:EcReduction.xconv -> ?keyed:bool -> - LDecl.hyps -> occ option -> form -> form -> ptnpos - - val is_occurences_valid : Sint.t -> ptnpos -> bool - - val occurences : ptnpos -> int - - val filter : occ -> ptnpos -> ptnpos + val select_with_ctxt : + ?postcheck:postcheck + -> ?o:occ + -> (Sid.t -> ctxt Lazy.t -> form -> select) + -> form + -> ptnpos + + val select : + ?postcheck:postcheck + -> ?o:occ + -> (Sid.t -> form -> select) + -> form + -> ptnpos + + val select_form : + ?postcheck:(Sid.t -> ctxt lazy_t -> form -> bool) + -> ?xconv:EcReduction.xconv + -> ?keyed:bool + -> LDecl.hyps + -> occ option + -> form + -> form + -> ptnpos + + val map_with_ctxt : ptnpos -> (ctxt Lazy.t -> form -> form) -> form -> form val map : ptnpos -> (form -> form) -> form -> form diff --git a/src/ecMemory.ml b/src/ecMemory.ml index 64571772ca..0256614e32 100644 --- a/src/ecMemory.ml +++ b/src/ecMemory.ml @@ -140,7 +140,7 @@ let bindall_fresh (vs : ovariable list) ((m, Lmt_concrete mt) : memenv) = else x in for_idx 0 in Msym.add name (-1,v.ov_type) m, { v with ov_name = Some name } in - let _, vs = List.map_fold fresh_pv lmt.lmt_proj vs in + let _, vs = List.fold_left_map fresh_pv lmt.lmt_proj vs in let lmt = bindall_lmt vs lmt in (m, Lmt_concrete (Some lmt)), vs diff --git a/src/ecParser.mly b/src/ecParser.mly index 305a6175ed..6adab791d9 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -484,6 +484,7 @@ %token MINUS %token MODPATH %token MODULE +%token MORPHISM %token MOVE %token NE %token NOT @@ -517,6 +518,7 @@ %token RCONDT %token REALIZE %token REFLEX +%token RELATION %token REMOVE %token RENAME %token REPLACE @@ -657,6 +659,8 @@ _lident: | CHECK { "check" } | EDIT { "edit" } | FIX { "fix" } +| RELATION { "relation" } +| MORPHISM { "morphism" } | x=RING { match x with `Eq -> "ringeq" | `Raw -> "ring" } | x=FIELD { match x with `Eq -> "fieldeq" | `Raw -> "field" } @@ -3765,6 +3769,20 @@ user_red_option: (Some ("invalid option: " ^ (unloc x))) } +(* -------------------------------------------------------------------- *) +(* Setoid rewrite *) +relation: +| RELATION name=qident { { + prl_name = name; + } } + +morphism: +| MORPHISM morphism=qoident SLASH position=word LONGARROW relation=qoident { { + prl_morphism = morphism; + prl_position = position; + prl_relation = relation; + } } + (* -------------------------------------------------------------------- *) (* Search pattern *) %inline search: x=sform_h { x } @@ -3795,6 +3813,8 @@ global_action: | notation { Gnotation $1 } | abbreviation { Gabbrev $1 } | reduction { Greduction $1 } +| relation { Grelation $1 } +| morphism { Gmorphism $1 } | axiom { Gaxiom $1 } | tactics_or_prf { Gtactics $1 } | tactic_dump { Gtcdump $1 } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 14db94e182..67b0c98ffb 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -1266,6 +1266,16 @@ type puserred = type threquire = psymbol option * (psymbol * psymbol option) list * [`Import|`Export] option +(* -------------------------------------------------------------------- *) +type prelation = + { prl_name : pqsymbol; } + +(* -------------------------------------------------------------------- *) +type pmorphism = + { prl_morphism : pqsymbol; + prl_position : int; + prl_relation : pqsymbol; } + (* -------------------------------------------------------------------- *) type global_action = | Gmodule of pmodule_def_or_decl @@ -1282,6 +1292,8 @@ type global_action = | Gtycinstance of ptycinstance | Gaddrw of (is_local * pqsymbol * pqsymbol list) | Greduction of puserred + | Grelation of prelation + | Gmorphism of pmorphism | Ghint of phint | Gprint of pprint | Gsearch of pformula list diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 4cfa2f0c28..7854c39501 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -3120,7 +3120,7 @@ module PPGoal = struct let pp_goal1 ?(pphyps = true) ?prpo ?(idx) (ppe : PPEnv.t) fmt (hyps, concl) = let ppe = PPEnv.add_locals ppe (List.map fst hyps.EcBaseLogic.h_tvar) in - let ppe, pps = List.map_fold pre_pp_hyp ppe (List.rev hyps.EcBaseLogic.h_local) in + let ppe, pps = List.fold_left_map pre_pp_hyp ppe (List.rev hyps.EcBaseLogic.h_local) in idx |> oiter (Format.fprintf fmt "Goal #%d@\n"); @@ -3167,7 +3167,7 @@ let pp_hyps (ppe : PPEnv.t) fmt hyps = let hyps = EcEnv.LDecl.tohyps hyps in let ppe = PPEnv.add_locals ppe (List.map fst hyps.EcBaseLogic.h_tvar) in let ppe, pps = - List.map_fold PPGoal.pre_pp_hyp ppe + List.fold_left_map PPGoal.pre_pp_hyp ppe (List.rev hyps.EcBaseLogic.h_local) in begin match hyps.EcBaseLogic.h_tvar with @@ -3543,6 +3543,14 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) = (* FIXME: section we should add the lemma in the reduction *) Format.fprintf fmt "hint simplify." + | EcTheory.Th_relation (oppath, axpath) -> + Format.fprintf fmt "relation %a. (* spec: %a *)" + (pp_opname ppe) oppath (pp_axname ppe) axpath + + | EcTheory.Th_morphism (relpath, oppath, axpath, n) -> + Format.fprintf fmt "morphism %a / %d ==> %a. (* spec: %a *)" + (pp_opname ppe) oppath n (pp_opname ppe) relpath (pp_axname ppe) axpath + | EcTheory.Th_auto { level; base; axioms; locality; } -> Format.fprintf fmt "%ahint solve %d %s : %a." pp_locality locality diff --git a/src/ecScope.ml b/src/ecScope.ml index 17e1b1a4a4..75368672ac 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1781,6 +1781,162 @@ module Reduction = struct { scope with sc_env = EcSection.add_item item scope.sc_env } end +(* -------------------------------------------------------------------- *) +module Setoid = struct + let add_relation (scope as scope0 : scope) (rel : prelation) = + let env = env scope in + let oppath, op = EcEnv.Op.lookup (unloc rel.prl_name) env in + + (* Check that the operator is of the form: ... -> a -> a -> bool *) + begin + let exception InvalidRelTy in + + try + let dom, codom = tyfun_flat op.op_ty in + + if not (EcReduction.EqTest.for_type env codom tbool) then + raise InvalidRelTy; + + match List.rev dom with + | a1 :: a2 :: _ -> + if not (EcReduction.EqTest.for_type env a1 a2) then + raise InvalidRelTy + + | _ -> + raise InvalidRelTy + + with InvalidRelTy -> + hierror ~loc:(loc rel.prl_name) + "the operator must have a type of the form `... -> t -> t -> bool`" + + end; + + (* Check that the operator is an equivalence relation *) + let optp, opty = EcSubst.freshen_type (op.op_tparams, op.op_ty) in + + let dom, codom = tyfun_flat opty in + let nparams = List.length dom - 2 in + let params = List.take nparams dom in + let tyl, tyr = as_seq2 (List.drop nparams dom) in + let params = List.map (fun ty -> (EcIdent.create "x", ty)) params in + + let eqv, _ = EcEnv.Op.lookup ([], "iseqv") env in + let eqv = f_op eqv [tyl] (tfun (toarrow [tyl; tyr] codom) tbool) in + let eqv = + let rel = f_op oppath (List.map (tvar |- fst) optp) opty in + let rel = f_app rel (List.map (fun (x, ty) -> f_local x ty) params) (toarrow [tyl; tyr] codom) in + f_app eqv [rel] tbool in + let eqv = f_forall (List.map (snd_map (fun ty -> GTty ty)) params) eqv in + let eqv = { + ax_tparams = optp; + ax_spec = eqv; + ax_kind = `Lemma; + ax_loca = `Global; + ax_visibility = `Visible; } in + + let axname = Format.sprintf "%s_is_eqv" (EcPath.basename oppath) in + let axpath = EcPath.pqname (path scope) axname in + + let scope = Ax.bind scope (axname, eqv) in + let proof = (None, eqv), axpath, scope0.sc_env in + + (* Add theory item *) + let item = EcTheory.mkitem EcTheory.import0 (Th_relation (oppath, axpath)) in + let scope = { scope with sc_env = EcSection.add_item item scope.sc_env } in + + Ax.add_defer scope [proof] + + let add_morphism (scope as scope0 : scope) (mph : pmorphism) = + (* Check type-level compatibility *) + let env = env scope in + + let mphp, mphop = EcEnv.Op.lookup (unloc mph.prl_morphism) env in + let mph_dom, mph_codom = tyfun_flat mphop.op_ty in + + if not (0 < mph.prl_position && mph.prl_position <= List.length mph_dom) then + hierror ~loc:(loc mph.prl_morphism) "invalid argument position for morphism"; + + let relp, op = EcEnv.Op.lookup (unloc mph.prl_relation) env in + let dom, codom = tyfun_flat op.op_ty in + let nparams = List.length dom - 2 in + let paramsty = List.take nparams dom in + let t1, _ = as_seq2 (List.drop nparams dom) in + + if List.length mphop.op_tparams <> List.length op.op_tparams then + hierror ~loc:(loc mph.prl_morphism) + "the morphism and relation must have compatible type parameters"; + + let tvars = List.map (tvar |- fst) mphop.op_tparams in + let tpsubst = EcCoreSubst.Tvar.init (List.fst op.op_tparams) tvars in + + let othersty, argty = + let largs, arg, rargs = List.pivot_at (mph.prl_position - 1) mph_dom in + (largs @ rargs), arg in + + if not (EcReduction.EqTest.for_type env argty (Tvar.subst tpsubst t1)) then + hierror ~loc:(loc mph.prl_morphism) + "the %d-th argument must be compatible with the equivalence relation" + mph.prl_position; + + (* Construct morphism lemma *) + let params = + List.mapi + (fun i ty -> (EcIdent.create (Format.sprintf "p%d" (i + 1)), Tvar.subst tpsubst ty)) + paramsty in + + let eqv = + let params = List.map (fun (x, ty) -> f_local x ty) params in + fun f1 f2 -> + f_app + (f_op relp tvars (Tvar.subst tpsubst op.op_ty)) + (params @ [f1; f2]) codom in + + let otherargs = + List.mapi + (fun i ty -> (EcIdent.create (Format.sprintf "x_%d" (i + 1)), ty)) + othersty in + + let lothers, rothers = List.split_at (mph.prl_position - 1) otherargs in + + let lothers = List.map (fun (x, ty) -> f_local x ty) lothers in + let rothers = List.map (fun (x, ty) -> f_local x ty) rothers in + + let a1 = EcIdent.create "a1" in + let a2 = EcIdent.create "a2" in + + let concl = eqv (f_local a1 argty) (f_local a2 argty) in + let concl = + let l = f_app (f_op mphp tvars mphop.op_ty) (lothers @ f_local a1 argty :: rothers) mph_codom in + let r = f_app (f_op mphp tvars mphop.op_ty) (lothers @ f_local a2 argty :: rothers) mph_codom in + f_imp concl (eqv l r) in + let concl = + let bindings = params @ otherargs @ [(a1, argty); (a2, argty)] in + let bindings = List.map (fun (x, ty) -> (x, GTty ty)) bindings in + f_forall bindings concl in + + let concl = { + ax_tparams = mphop.op_tparams; + ax_spec = concl; + ax_kind = `Lemma; + ax_loca = `Global; + ax_visibility = `Visible; } in + + let axname = + Format.sprintf + "%s_is_morphism_for_%s_at_%d" + (EcPath.basename mphp) (EcPath.basename relp) (mph.prl_position) in + let axpath = EcPath.pqname (path scope) axname in + + let scope = Ax.bind scope (axname, concl) in + let proof = (None, concl), axpath, scope0.sc_env in + + (* Add theory item *) + let item = EcTheory.mkitem EcTheory.import0 (Th_morphism (relp, mphp, axpath, mph.prl_position)) in + let scope = { scope with sc_env = EcSection.add_item item scope.sc_env } in + + Ax.add_defer scope [proof] +end + (* -------------------------------------------------------------------- *) module Cloning = struct (* ------------------------------------------------------------------ *) @@ -2156,7 +2312,7 @@ module Ty = struct let check_tci_axioms scope mode axs reqs lc = let rmap = Mstr.of_list reqs in let symbs, axs = - List.map_fold + List.fold_left_map (fun m (x, t) -> if not (Mstr.mem (unloc x) rmap) then hierror ~loc:x.pl_loc "invalid axiom name: `%s'" (unloc x); diff --git a/src/ecScope.mli b/src/ecScope.mli index 7b1abcbace..e579f6d7f5 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -245,6 +245,12 @@ module Reduction : sig val add_reduction : scope -> puserred -> scope end +(*-------------------------------------------------------------------- *) +module Setoid : sig + val add_relation : scope -> prelation -> scope + val add_morphism : scope -> pmorphism -> scope +end + (* -------------------------------------------------------------------- *) module Cloning : sig val clone : scope -> Ax.proofmode -> theory_cloning -> scope diff --git a/src/ecSection.ml b/src/ecSection.ml index 3c8257547c..3f5bd5fd2f 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -1016,6 +1016,10 @@ let generalize_addrw to_gen (p, ps, lc) = let generalize_reduction to_gen _rl = to_gen, None +let generalize_relation to_gen _rel = to_gen, None + +let generalize_morphism to_gen _m = to_gen, None + let generalize_auto to_gen auto_rl = if auto_rl.locality = `Local then to_gen, None @@ -1050,6 +1054,8 @@ let rec set_local_item item = | Th_baserw (s,lc) -> Th_baserw (s, set_local lc) | Th_addrw (p,ps,lc) -> Th_addrw (p, ps, set_local lc) | Th_reduction r -> Th_reduction r + | Th_relation r -> Th_relation r + | Th_morphism m -> Th_morphism m | Th_auto auto_rl -> Th_auto {auto_rl with locality=set_local auto_rl.locality} in { item with ti_item = lcitem } @@ -1354,6 +1360,8 @@ let add_item_ (item : theory_item) (scenv:scenv) = | Th_auto auto -> EcEnv.Auto.add ~level:auto.level ?base:auto.base auto.axioms auto.locality env | Th_reduction r -> EcEnv.Reduction.add r env + | Th_relation r -> EcEnv.Setoid.add_relation r env + | Th_morphism m -> EcEnv.Setoid.add_morphism m env | _ -> assert false in { scenv with @@ -1380,6 +1388,8 @@ let rec generalize_th_item (to_gen : to_gen) (prefix : path) (th_item : theory_i | Th_baserw (s,lc) -> generalize_baserw to_gen prefix (s,lc) | Th_addrw (p,ps,lc) -> generalize_addrw to_gen (p, ps, lc) | Th_reduction rl -> generalize_reduction to_gen rl + | Th_relation rel -> generalize_relation to_gen rel + | Th_morphism m -> generalize_morphism to_gen m | Th_auto hints -> generalize_auto to_gen hints in @@ -1502,6 +1512,8 @@ let check_item scenv item = if (locality = `Local && not scenv.sc_insec) then hierror "local hint can only be declared inside section"; | Th_reduction _ -> () + | Th_relation _ -> () + | Th_morphism _ -> () | Th_theory _ -> assert false let rec add_item (item : theory_item) (scenv : scenv) = diff --git a/src/ecSetoid.ml b/src/ecSetoid.ml new file mode 100644 index 0000000000..e9d11a3c47 --- /dev/null +++ b/src/ecSetoid.ml @@ -0,0 +1,56 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcMaps +open EcPath +open EcAst +open EcTypes +open EcFol +open EcEnv +open EcMatching + +(* -------------------------------------------------------------------- *) +type instance = { + relation : path * ty list; + params : form list; +} + +(* -------------------------------------------------------------------- *) +let as_instance (env : env) ((oppath, optyargs), args) = + let exception NotASetoid in + + try + let op = EcEnv.Op.by_path oppath env in + let _rel = oget ~exn:NotASetoid (EcEnv.Setoid.get_relation env oppath) in + + let nparams = List.length (fst (tyfun_flat op.op_ty)) - 2 in + + if List.length args <> nparams + 2 then + raise NotASetoid; + + let f1, f2 = as_seq2 (List.drop nparams args) in + let params = List.take nparams args in + Some ({ relation = (oppath, optyargs); params; }, (f1, f2)) + + with NotASetoid -> None + +(* -------------------------------------------------------------------- *) +let valid_setoid_context (env : env) (instance : instance) (ctxt : FPosition.ctxt) = + let eqvp = fst (instance.relation) in + let eqv = oget (EcEnv.Setoid.get_relation env eqvp) in + + let accept (ineqv : bool) (ctxt1 : FPosition.ctxt1) = + match ctxt1.ctxt with + | CT_AppArg ({ f_node = Fop (p, _)}, (_, rargs)) when List.length rargs < 2 && EcPath.p_equal p eqvp -> + true + | CT_AppArg ({ f_node = Fop (p, _)}, (largs, _)) when ineqv -> begin + match Mp.find_opt p eqv.morphisms with + | None -> + false + | Some mph -> + Mint.mem (1 + List.length largs) mph + end + | _ -> + false in + + List.fold_left accept false ctxt + diff --git a/src/ecSetoid.mli b/src/ecSetoid.mli new file mode 100644 index 0000000000..f0224e8d13 --- /dev/null +++ b/src/ecSetoid.mli @@ -0,0 +1,18 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcPath +open EcAst +open EcEnv +open EcMatching + +(* -------------------------------------------------------------------- *) +type instance = { + relation : path * ty list; + params : form list; +} + +(* -------------------------------------------------------------------- *) +val as_instance : env -> (path * ty list) * form list -> (instance * form pair) option + +(* -------------------------------------------------------------------- *) +val valid_setoid_context : env -> instance -> FPosition.ctxt -> bool diff --git a/src/ecSmt.ml b/src/ecSmt.ml index 6d81016c62..dd553fb8d6 100644 --- a/src/ecSmt.ml +++ b/src/ecSmt.ml @@ -270,7 +270,7 @@ let lenv_of_tparams ts = let tv = WTy.create_tvsymbol (preid id) in { env with le_tv = Mid.add id (WTy.ty_var tv) env.le_tv }, tv in - List.map_fold trans_tv empty_lenv ts + List.fold_left_map trans_tv empty_lenv ts let lenv_of_tparams_for_hyp genv ts = let trans_tv env ((id, _) : ty_param) = (* FIXME: TC HOOK *) @@ -278,7 +278,7 @@ let lenv_of_tparams_for_hyp genv ts = genv.te_task <- WTask.add_ty_decl genv.te_task ts; { env with le_tv = Mid.add id (WTy.ty_app ts []) env.le_tv }, ts in - List.map_fold trans_tv empty_lenv ts + List.fold_left_map trans_tv empty_lenv ts (* -------------------------------------------------------------------- *) let instantiate tparams ~textra targs tres tys = @@ -487,7 +487,7 @@ let trans_binding genv lenv (x, xty) = (* -------------------------------------------------------------------- *) let trans_bindings genv lenv bds = - List.map_fold (trans_binding genv) lenv bds + List.fold_left_map (trans_binding genv) lenv bds (* -------------------------------------------------------------------- *) let trans_lvars genv lenv bds = @@ -981,7 +981,7 @@ and trans_fix (genv, lenv) (wdom, o) = | OPB_Leaf (locals, e) -> let ctors = List.rev ctors in - let lenv, cvs = List.map_fold (trans_lvars genv) lenv locals in + let lenv, cvs = List.fold_left_map (trans_lvars genv) lenv locals in let fe = EcCoreFol.form_of_expr EcCoreFol.mhr e in let we = trans_app (genv, lenv) fe eargs in diff --git a/src/ecSubst.ml b/src/ecSubst.ml index d1b24f4f6f..07c7cd866d 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -678,7 +678,7 @@ and subst_modsig ?params (s : subst) (comps : module_sig) = match comps.mis_params with | [] -> (s, []) | _ -> - List.map_fold + List.fold_left_map (fun (s : subst) (a, aty) -> let a' = EcIdent.fresh a in let decl = (a', subst_modtype s aty) in @@ -687,7 +687,7 @@ and subst_modsig ?params (s : subst) (comps : module_sig) = end | Some params -> - List.map_fold + List.fold_left_map (fun (s : subst) ((a, aty), a') -> let decl = (a', subst_modtype s aty) in add_module s a (EcPath.mident a'), decl) @@ -814,7 +814,7 @@ and subst_module (s : subst) (m : module_expr) = let sbody, me_params = match m.me_params with | [] -> (s, []) | _ -> - List.map_fold + List.fold_left_map (fun (s : subst) (a, aty) -> let a' = EcIdent.fresh a in let decl = (a', subst_modtype s aty) in @@ -928,7 +928,7 @@ and subst_op_body (s : subst) (bd : opbody) = and subst_branches (s : subst) = function | OPB_Leaf (locals, e) -> - let (s, locals) = List.map_fold fresh_elocals s locals in + let (s, locals) = List.fold_left_map fresh_elocals s locals in OPB_Leaf (locals, subst_expr s e) | OPB_Branch bs -> @@ -1075,6 +1075,17 @@ let rec subst_theory_item_r (s : subst) (item : theory_item_r) = List.map (fun (p, opts, _) -> (subst_path s p, opts, None)) rules in Th_reduction rules + | Th_relation (oppath, axpath) -> + let oppath = subst_path s oppath in + let axpath = subst_path s axpath in + Th_relation (oppath, axpath) + + | Th_morphism (relpath, oppath, axpath, pos) -> + let relpath = subst_path s relpath in + let oppath = subst_path s oppath in + let axpath = subst_path s axpath in + Th_morphism (relpath, oppath, axpath, pos) + | Th_auto ({ axioms } as auto_rl) -> Th_auto { auto_rl with axioms = List.map (fst_map (subst_path s)) axioms } diff --git a/src/ecSubst.mli b/src/ecSubst.mli index 8eabb02aeb..9b079a1c5d 100644 --- a/src/ecSubst.mli +++ b/src/ecSubst.mli @@ -36,6 +36,7 @@ val add_elocals : subst -> EcIdent.t list -> expr list -> subst val rename_flocal : subst -> EcIdent.t -> EcIdent.t -> ty -> subst (* -------------------------------------------------------------------- *) +val fresh_tparams : subst -> ty_params -> subst * ty_params val freshen_type : (ty_params * ty) -> (ty_params * ty) (* -------------------------------------------------------------------- *) diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml index 603b52914a..32cec45081 100644 --- a/src/ecThCloning.ml +++ b/src/ecThCloning.ml @@ -456,6 +456,8 @@ end = struct | Th_baserw _ -> (proofs, evc) | Th_addrw _ -> (proofs, evc) | Th_reduction _ -> (proofs, evc) + | Th_relation _ -> (proofs, evc) + | Th_morphism _ -> (proofs, evc) | Th_auto _ -> (proofs, evc) and doit prefix (proofs, evc) dth = diff --git a/src/ecTheory.ml b/src/ecTheory.ml index a329d9318d..8aafec6948 100644 --- a/src/ecTheory.ml +++ b/src/ecTheory.ml @@ -37,6 +37,8 @@ and theory_item_r = | Th_baserw of symbol * is_local | Th_addrw of EcPath.path * EcPath.path list * is_local | Th_reduction of (EcPath.path * rule_option * rule option) list + | Th_relation of (EcPath.path * EcPath.path) + | Th_morphism of (EcPath.path * EcPath.path * EcPath.path * int) | Th_auto of auto_rule and thsource = { diff --git a/src/ecTheory.mli b/src/ecTheory.mli index fb63e85447..966ce3bb6f 100644 --- a/src/ecTheory.mli +++ b/src/ecTheory.mli @@ -34,6 +34,8 @@ and theory_item_r = | Th_addrw of EcPath.path * EcPath.path list * is_local (* reduction rule does not survive to section so no locality *) | Th_reduction of (EcPath.path * rule_option * rule option) list + | Th_relation of (EcPath.path * EcPath.path) + | Th_morphism of (EcPath.path * EcPath.path * EcPath.path * int) | Th_auto of auto_rule and thsource = { diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 283fca0c26..6a809c98fd 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -921,6 +921,55 @@ and replay_reduction (subst, ops, proofs, scope) +(* -------------------------------------------------------------------- *) +and replay_relation (ove : _ ovrenv) (subst, ops, proofs, scope) (import, (oppath, axpath)) = + let exception Removed in + + try + let oppath = EcSubst.subst_path subst oppath in + let axpath = EcSubst.subst_path subst axpath in + + let env = EcSection.env (ove.ovre_hooks.henv scope) in + + if is_none (EcEnv.Op.by_path_opt oppath env) then + raise Removed; + if is_none (EcEnv.Ax.by_path_opt axpath env) then + raise Removed; + + let item = Th_relation (oppath, axpath) in + let scope = ove.ovre_hooks.hadd_item scope import item in + + (subst, ops, proofs, scope) + +with Removed -> + (subst, ops, proofs, scope) + +(* -------------------------------------------------------------------- *) +and replay_morphism (ove : _ ovrenv) (subst, ops, proofs, scope) (import, (relpath, oppath, axpath, position)) = + let exception Removed in + + try + let relpath = EcSubst.subst_path subst relpath in + let oppath = EcSubst.subst_path subst oppath in + let axpath = EcSubst.subst_path subst axpath in + + let env = EcSection.env (ove.ovre_hooks.henv scope) in + + if is_none (EcEnv.Op.by_path_opt relpath env) then + raise Removed; + if is_none (EcEnv.Op.by_path_opt oppath env) then + raise Removed; + if is_none (EcEnv.Ax.by_path_opt axpath env) then + raise Removed; + + let item = Th_morphism (relpath, oppath, axpath, position) in + let scope = ove.ovre_hooks.hadd_item scope import item in + + (subst, ops, proofs, scope) + +with Removed -> + (subst, ops, proofs, scope) + (* -------------------------------------------------------------------- *) and replay_typeclass (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, tc) @@ -1042,6 +1091,12 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) item = | Th_reduction rules -> replay_reduction ove (subst, ops, proofs, scope) (item.ti_import, rules) + | Th_relation (oppath, axpath) -> + replay_relation ove (subst, ops, proofs, scope) (item.ti_import, (oppath, axpath)) + + | Th_morphism (relpath, oppath, axpath, pos) -> + replay_morphism ove (subst, ops, proofs, scope) (item.ti_import, (relpath, oppath, axpath, pos)) + | Th_auto at_base -> replay_auto ove (subst, ops, proofs, scope) (item.ti_import, at_base) diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 1a978db855..32239955a0 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -1199,7 +1199,7 @@ let trans_binding env ue bd = let xs = List.map (fun x -> ident_of_osymbol (unloc x), ty) xs in let env = EcEnv.Var.bind_locals xs env in env, xs in - let env, bd = List.map_fold trans_bd1 env bd in + let env, bd = List.fold_left_map trans_bd1 env bd in let bd = List.flatten bd in env, bd @@ -2830,7 +2830,7 @@ and trans_gbinding env ue decl = let env = EcEnv.Mod.bind_local x mi env in (env, (x, ty)) - in List.map_fold add1 env xs + in List.fold_left_map add1 env xs | PGTY_Mem pmt -> let mt = match pmt with @@ -2842,9 +2842,9 @@ and trans_gbinding env ue decl = let env = EcEnv.Memory.push (x, mt) env in (env, (x, GTmem mt)) - in List.map_fold add1 env xs + in List.fold_left_map add1 env xs - in snd_map List.flatten (List.map_fold trans1 env decl) + in snd_map List.flatten (List.fold_left_map trans1 env decl) (* -------------------------------------------------------------------- *) and trans_form_or_pattern env mode ?mv ?ps ue pf tt = diff --git a/src/ecUtils.ml b/src/ecUtils.ml index 6213d2f966..143c06289a 100644 --- a/src/ecUtils.ml +++ b/src/ecUtils.ml @@ -439,7 +439,7 @@ module List = struct let (a, xs) = doit a xs1 xs2 in (a, x :: xs) - | _, _ -> invalid_arg "List.map_fold2" + | _, _ -> invalid_arg "List.fold_left_map2" in fun a xs1 xs2 -> doit a xs1 xs2 @@ -521,15 +521,15 @@ module List = struct | x :: xs -> aux (ocons (f x) acc) xs in aux [] xs - let mapi_fold f a xs = - let a = ref a in - let xs = List.mapi (fun i b -> - let (a', b') = f i !a b in a := a'; b') - xs - in (!a, xs) + let fold_left_mapi (f : 'a -> int -> 'b -> 'a * 'c) (st : 'a) (s : 'b list) : 'a * 'c list = + let (st, _), s = + fold_left_map + (fun (st, i) v -> let st, v = f st i v in (st, i + 1), v) + (st, 0) s + in (st, s) - let map_fold f a xs = - mapi_fold (fun (_ : int) x -> f x) a xs + let fold_left_map (f : 'a -> 'b -> 'a * 'c) (st : 'a) (xs : 'b list) = + fold_left_mapi (fun (x : 'a) (_ : int) -> f x) st xs let rec fpick (xs : (unit -> 'a option) list) = match xs with diff --git a/src/ecUtils.mli b/src/ecUtils.mli index fe135ee604..4e49a8dc92 100644 --- a/src/ecUtils.mli +++ b/src/ecUtils.mli @@ -289,8 +289,6 @@ module List : sig val fpick : (unit -> 'a option) list -> 'a option val pivot_at : int -> 'a list -> 'a list * 'a * 'a list val find_pivot : ('a -> bool) -> 'a list -> 'a list * 'a * 'a list - val map_fold : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list - val mapi_fold : (int -> 'a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list val pmapi : (int -> 'a -> 'b option) -> 'a list -> 'b list val pmap : ('a -> 'b option) -> 'a list -> 'b list val rev_pmap : ('a -> 'b option) -> 'a list -> 'b list @@ -301,6 +299,9 @@ module List : sig val takedrop_while : ('a -> bool) -> 'a list -> 'a list * 'a list + val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list + val fold_left_mapi : ('a -> int -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list + val fold_left_map_while : ('a -> 'b -> [`Interrupt | `Continue of 'a * 'c]) -> 'a -> 'b list -> 'a * 'c list * 'b list diff --git a/tests/setoidrw.ec b/tests/setoidrw.ec new file mode 100644 index 0000000000..71c570dd67 --- /dev/null +++ b/tests/setoidrw.ec @@ -0,0 +1,45 @@ +require import AllCore. + +inductive iseqv ['a] (e : 'a -> 'a -> bool) = +| IsEqv of + (forall x, e x x) + & (forall x y, e x y => e y x) + & (forall y x z, e x y => e y z => e x z). + +op eqv (i : int) (x y : int) : bool. + +axiom eqvzz (i x : int) : eqv i x x. +axiom eqv_sym (i x y : int) : eqv i x y => eqv i y x. +axiom eqv_trans (i y x z : int) : eqv i x y => eqv i y z => eqv i x z. + +relation eqv. + +realize Top.eqv_is_eqv. +move=> x; split. +- by apply: eqvzz. +- by apply: eqv_sym. +- by apply: eqv_trans. +qed. + +axiom eqv_addl (i t x y) : eqv i x y => eqv i (x + t) (y + t). +axiom eqv_addr (i t x y) : eqv i x y => eqv i (t + x) (t + y). + +morphism CoreInt.add / 1 ==> eqv. + +realize Top.add_is_morphism_for_eqv_at_1. +proof. admitted. + +morphism CoreInt.add / 2 ==> eqv. + +realize Top.add_is_morphism_for_eqv_at_2. +proof. admitted. + +pred p : int. + +lemma foo (i t1 t2 x y : int) : + eqv i x y => p x => eqv i ((x + t2)) ((x + t2)). +proof. +move=> e. +rewrite {2 3}e. + +abort.