setoid rewrite

Author: strub

src/ecCommands.ml

@@ -687,6 +687,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
@@ -789,6 +797,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

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

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 : _) =

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_albase   : path Mp.t;             (* theory aliases   *)
   env_modlcs   : Sid.t;                 (* declared modules *)
@@ -226,6 +228,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
 
@@ -312,6 +321,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_albase   = Mp.empty;
     env_modlcs   = Sid.empty;
@@ -613,7 +623,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)
@@ -1018,7 +1028,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
@@ -1113,12 +1123,13 @@ module MC = struct
           (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)
 
@@ -1566,6 +1577,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 ~import:true (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 ~import:true (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_
@@ -2974,6 +3014,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
@@ -3021,12 +3072,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
 
@@ -3086,7 +3139,12 @@ module Theory = struct
         | Th_alias (name, path) ->
             rebind_alias name path env
 
-        | Th_addrw _ | Th_instance _ | Th_auto _ | Th_reduction _ ->
+        | Th_addrw _
+        | Th_instance _
+        | Th_auto _
+        | Th_reduction _
+        | Th_relation _
+        | Th_morphism _ ->
             env
 
       in
@@ -3103,7 +3161,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
@@ -3239,6 +3297,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; }
@@ -3442,7 +3501,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 = {

src/ecEnv.mli

@@ -416,6 +416,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]

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
@@ -596,6 +622,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 =
@@ -2139,7 +2167,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";