Rigid unification option for hint solve/exact + print hint

Author: Gustavo2622

src/ecCommands.ml

@@ -2,6 +2,7 @@
 open EcUtils
 open EcLocation
 open EcParsetree
+open EcMaps
 
 module Sid = EcIdent.Sid
 module Mx  = EcPath.Mx
@@ -298,46 +299,6 @@ let process_print_ax (scope : EcScope.scope) =
   let env = EcScope.env scope in
   let ax  = EcEnv.Ax.all ~check:(fun _ ax -> EcDecl.is_axiom ax.ax_kind) env in
 
-  let module Trie : sig
-    type ('a, 'b) t
-
-    val empty : ('a, 'b) t
-    val add : 'a list -> 'b -> ('a, 'b) t -> ('a, 'b) t
-    val iter : ('a list -> 'b list -> unit) -> ('a, 'b) t -> unit
-  end = struct
-    module Map = BatMap
-
-    type ('a, 'b) t =
-      { children : ('a, ('a, 'b) t) Map.t
-      ; value    : 'b list }
-
-    let empty : ('a, 'b) t =
-      { value = []; children = Map.empty; }
-
-    let add (path : 'a list) (value : 'b) (t : ('a, 'b) t) =
-      let rec doit (path : 'a list) (t : ('a, 'b) t) =
-        match path with
-        | [] ->
-          { t with value = value :: t.value }
-        | v :: path ->
-          let children =
-            t.children |> Map.update_stdlib v (fun children ->
-              let subtrie = Option.value ~default:empty children in
-              Some (doit path subtrie)
-            )
-          in { t with children }
-      in doit path t
-
-    let iter (f : 'a list -> 'b list -> unit) (t : ('a, 'b) t) =
-      let rec doit (prefix : 'a list) (t : ('a, 'b) t) =
-        if not (List.is_empty t.value) then
-          f prefix t.value;
-        Map.iter (fun k v -> doit (k :: prefix) v) t.children
-      in
-      
-      doit [] t
-  end in
-
   let ax =
     List.fold_left (fun axs ((p, _) as ax) ->
       Trie.add (EcPath.tolist (oget (EcPath.prefix p))) ax axs
@@ -354,7 +315,6 @@ let process_print_ax (scope : EcScope.scope) =
       | name :: prefix -> (List.rev prefix, name) in
 
     let thpath = EcPath.fromqsymbol thpath in
-
     let ppe = EcPrinting.PPEnv.enter_theory ppe0 thpath in
 
     Format.fprintf fmt
@@ -367,6 +327,41 @@ let process_print_ax (scope : EcScope.scope) =
 
   EcScope.notify scope `Warning "%s" (Buffer.contents buffer)
 
+(* -------------------------------------------------------------------- *)
+let process_print_hint (scope : EcScope.scope) =
+  let env = EcScope.env scope in
+  let ax  = EcEnv.Auto.all env in
+  let ax  = List.map (fun (ir, p) -> (p, (EcEnv.Ax.by_path p env, ir))) ax in
+  let ax =
+    List.fold_left (fun axs ((p, _) as ax) ->
+      Trie.add (EcPath.tolist (oget (EcPath.prefix p))) ax axs
+    ) Trie.empty ax in
+
+  let ppe0 = EcPrinting.PPEnv.ofenv env in
+  let buffer = Buffer.create 0 in
+  let fmt = Format.formatter_of_buffer buffer in
+
+  Trie.iter (fun prefix axs ->
+    let thpath =
+      match prefix with
+      | [] -> assert false
+      | name :: prefix -> (List.rev prefix, name) in
+
+    let thpath = EcPath.fromqsymbol thpath in
+
+    let ppe = EcPrinting.PPEnv.enter_theory ppe0 thpath in
+
+    Format.fprintf fmt
+      "@.========== %a ==========@.@." (EcPrinting.pp_thname ppe0) thpath;
+
+    List.iter (fun (p,  (ax, ir)) ->
+      Format.fprintf fmt "%a%s@." (EcPrinting.pp_axiom ppe) (p, ax) 
+      (if ir then " (irreducible)" else " (reducible)")
+    ) axs
+  ) ax;
+
+  EcScope.notify scope `Warning "%s" (Buffer.contents buffer)
+
 (* -------------------------------------------------------------------- *)
 exception Pragma of [`Reset | `Restart]
 
@@ -735,6 +730,7 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g =
       | GsctClose    name -> `Fct   (fun scope -> process_sct_close  scope  name)
       | Gprint       p    -> `Fct   (fun scope -> process_print      scope  p; scope)
       | Gpaxiom           -> `Fct   (fun scope -> process_print_ax   scope; scope)
+      | Gphint            -> `Fct   (fun scope -> process_print_hint scope; scope)
       | Gsearch      qs   -> `Fct   (fun scope -> process_search     scope  qs; scope)
       | Glocate      x    -> `Fct   (fun scope -> process_locate     scope  x; scope)
       | Gtactics     t    -> `Fct   (fun scope -> process_tactics    scope  t)

src/ecEnv.ml

@@ -181,7 +181,7 @@ type preenv = {
   env_tci      : ((ty_params * ty) * tcinstance) list;
   env_tc       : TC.graph;
   env_rwbase   : Sp.t Mip.t;
-  env_atbase   : (path list Mint.t) Msym.t;
+  env_atbase   : (bool * path) list Mint.t Msym.t; (* maybe rename to atbases? *)
   env_redbase  : mredinfo;
   env_ntbase   : ntbase Mop.t;
   env_modlcs   : Sid.t;                 (* declared modules *)
@@ -221,6 +221,7 @@ and env_notation = ty_params * EcDecl.notation
 
 and ntbase = (path * env_notation) list
 
+
 (* -------------------------------------------------------------------- *)
 type env = preenv
 
@@ -1502,39 +1503,39 @@ end
 module Auto = struct
   let dname : symbol = ""
 
-  let updatedb ~level ?base (ps : path list) (db : (path list Mint.t) Msym.t) =
+  let updatedb ~level ?base (ps : (bool * path) list) (db : (bool * path) list Mint.t Msym.t) =
     let nbase = (odfl dname base) in
-    let ps' = Msym.find_def Mint.empty nbase db in
-    let ps' =
+    let base = Msym.find_def Mint.empty nbase db in
+    let levels =
       let doit x = Some (ofold (fun x ps -> ps @ x) ps x) in
-      Mint.change doit level ps' in
-    Msym.add nbase ps' db
+      Mint.change doit level base in
+    Msym.add nbase levels db
 
-  let add ?(import = import0) ~level ?base (ps : path list) lc (env : env) =
+  let add ?(import = import0) ~level ?base (axioms : (bool * path) list) locality (env : env) =
     let env =
       if import.im_immediate then
         { env with
-            env_atbase = updatedb ?base ~level ps env.env_atbase; }
+            env_atbase = updatedb ?base ~level axioms env.env_atbase; }
       else env
     in
       { env with env_item = mkitem import
-         (Th_auto (level, base, ps, lc)) :: env.env_item; }
+         (Th_auto {level; base; axioms; locality}) :: env.env_item; }
 
-  let add1 ?import ~level ?base (p : path) lc (env : env) =
+  let add1 ?import ~level ?base (p : (bool * path)) lc (env : env) =
     add ?import ?base ~level [p] lc env
 
   let get_core ?base (env : env) =
     Msym.find_def Mint.empty (odfl dname base) env.env_atbase
 
-  let flatten_db (db : path list Mint.t) =
+  let flatten_db (db : (bool * path) list Mint.t) =
     Mint.fold_left (fun ps _ ps' -> ps @ ps') [] db
 
   let get ?base (env : env) =
     flatten_db (get_core ?base env)
 
-  let getall (bases : symbol list) (env : env) =
+  let getall (bases : symbol list) (env : env) : (bool * path) list =
     let dbs = List.map (fun base -> get_core ~base env) bases in
-    let dbs =
+    let dbs = 
       List.fold_left (fun db mi ->
         Mint.union (fun _ sp1 sp2 -> Some (sp1 @ sp2)) db mi)
         Mint.empty dbs
@@ -1543,6 +1544,9 @@ module Auto = struct
   let getx (base : symbol) (env : env) =
     let db = Msym.find_def Mint.empty base env.env_atbase in
     Mint.bindings db
+
+  let all (env : env) : (bool * path) list =
+    Msym.values env.env_atbase |> List.map flatten_db |> List.flatten
 end
 
 (* -------------------------------------------------------------------- *)
@@ -2932,8 +2936,8 @@ module Theory = struct
   (* ------------------------------------------------------------------ *)
   let bind_at_th =
     let for1 _path db = function
-      | Th_auto (level, base, ps, _) ->
-         Some (Auto.updatedb ?base ~level ps db)
+      | Th_auto {level; base; axioms; _} ->
+         Some (Auto.updatedb ?base ~level axioms db)
       | _ -> None
 
     in bind_base_th for1
@@ -3106,9 +3110,9 @@ module Theory = struct
             let ps = List.filter ((not) |- inclear |- oget |- EcPath.prefix) ps in
             if List.is_empty ps then None else Some (Th_addrw (p, ps,lc))
 
-        | Th_auto (lvl, base, ps, lc) ->
-            let ps = List.filter ((not) |- inclear |- oget |- EcPath.prefix) ps in
-            if List.is_empty ps then None else Some (Th_auto (lvl, base, ps, lc))
+        | Th_auto ({axioms} as auto_rl) ->
+            let axioms = List.filter (fun (_b, p) -> ((not) |- inclear |- oget |- EcPath.prefix) p) axioms in
+            if List.is_empty axioms then None else Some (Th_auto {auto_rl with axioms})
 
         | (Th_export (p, _)) as item ->
             if Sp.mem p cleared then None else Some item

src/ecEnv.mli

@@ -413,11 +413,12 @@ end
 (* -------------------------------------------------------------------- *)
 module Auto : sig
   val dname  : symbol
-  val add1   : ?import:import -> level:int -> ?base:symbol -> path -> is_local -> env -> env
-  val add    : ?import:import -> level:int -> ?base:symbol -> path list -> is_local -> env -> env
-  val get    : ?base:symbol -> env -> path list
-  val getall : symbol list -> env -> path list
-  val getx   : symbol -> env ->  (int * path list) list
+  val add1   : ?import:import -> level:int -> ?base:symbol -> (bool * path) -> is_local -> env -> env
+  val add    : ?import:import -> level:int -> ?base:symbol -> (bool * path) list -> is_local -> env -> env
+  val get    : ?base:symbol -> env -> (bool * path) list
+  val getall : symbol list -> env -> (bool * path) list
+  val getx   : symbol -> env -> (int * (bool * path) list) list
+  val all    : env -> (bool * path) list
 end
 
 (* -------------------------------------------------------------------- *)

src/ecLexer.mll

@@ -183,6 +183,7 @@
     "local"       , LOCAL      ;        (* KW: global *)
     "declare"     , DECLARE    ;        (* KW: global *)
     "hint"        , HINT       ;        (* KW: global *)
+    "irreducible" , IRREDUCIBLE;        (* KW: global *)
     "module"      , MODULE     ;        (* KW: global *)
     "of"          , OF         ;        (* KW: global *)
     "const"       , CONST      ;        (* KW: global *)

src/ecLowGoal.ml

@@ -726,7 +726,7 @@ module Apply = struct
 
   exception NoInstance of (bool * reason * PT.pt_env * (form * form))
 
-  let t_apply_bwd_r ?(mode = fmdelta) ?(canview = true) pt (tc : tcenv1) =
+  let t_apply_bwd_r ?(ri = EcReduction.full_compat) ?(mode = fmdelta) ?(canview = true) pt (tc : tcenv1) =
     let ((hyps, concl), pterr) = (FApi.tc1_flat tc, PT.copy pt.ptev_env) in
 
     let noinstance ?(dpe = false) reason =
@@ -736,7 +736,7 @@ module Apply = struct
       match istop && PT.can_concretize pt.PT.ptev_env with
       | true ->
           let ax = PT.concretize_form pt.PT.ptev_env pt.PT.ptev_ax in
-          if   EcReduction.is_conv ~ri:EcReduction.full_compat hyps ax concl
+          if   EcReduction.is_conv ~ri hyps ax concl
           then pt
           else instantiate canview false pt
 
@@ -747,7 +747,7 @@ module Apply = struct
               noinstance `IncompleteInference;
             pt
           with EcMatching.MatchFailure ->
-            match TTC.destruct_product hyps pt.PT.ptev_ax with
+            match TTC.destruct_product ~reduce:(mode.fm_conv) hyps pt.PT.ptev_ax with
             | Some _ ->
                 (* FIXME: add internal marker *)
                 instantiate canview false (PT.apply_pterm_to_hole pt)
@@ -800,15 +800,15 @@ module Apply = struct
 
     t_apply pt tc
 
-  let t_apply_bwd ?mode ?canview pt (tc : tcenv1) =
+  let t_apply_bwd ?(ri : EcReduction.reduction_info option) ?mode ?canview pt (tc : tcenv1) =
     let hyps   = FApi.tc1_hyps tc in
     let pt, ax = LowApply.check `Elim pt (`Hyps (hyps, !!tc)) in
     let ptenv  = ptenv_of_penv hyps !!tc in
     let pt     = { ptev_env = ptenv; ptev_pt = pt; ptev_ax = ax; } in
-    t_apply_bwd_r ?mode ?canview pt tc
+    t_apply_bwd_r ?ri ?mode ?canview pt tc
 
-  let t_apply_bwd_hi ?(dpe = true) ?mode ?canview pt (tc : tcenv1) =
-    try  t_apply_bwd ?mode ?canview pt tc
+  let t_apply_bwd_hi ?(ri : EcReduction.reduction_info option) ?(dpe = true) ?mode ?canview pt (tc : tcenv1) =
+    try  t_apply_bwd ?ri ?mode ?canview pt tc
     with (NoInstance (_, r, pt, f)) ->
       tc_error_exn !!tc (NoInstance (dpe, r, pt, f))
 end
@@ -2506,22 +2506,26 @@ let t_coq
 let t_solve ?(canfail = true) ?(bases = [EcEnv.Auto.dname]) ?(mode = fmdelta) ?(depth = 1) (tc : tcenv1) =
   let bases = EcEnv.Auto.getall bases (FApi.tc1_env tc) in
 
-  let t_apply1 p tc =
 
+  let t_apply1 ((ir, p): bool * path) tc =
+    let ri = if ir then EcReduction.no_red else EcReduction.full_compat in
+    let mode = if ir then fmsearch else mode in
     let pt = PT.pt_of_uglobal !!tc (FApi.tc1_hyps tc) p in
     try
-      Apply.t_apply_bwd_r ~mode ~canview:false pt tc
-    with Apply.NoInstance _ -> t_fail tc in
+      Apply.t_apply_bwd_r ~ri ~mode ~canview:false pt tc
+    with Apply.NoInstance _ -> 
+      t_fail tc 
+  in
 
-  let rec t_apply ctn p tc =
+  let rec t_apply ctn ip tc =
     if   ctn > depth
     then t_fail tc
-    else (t_apply1 p @! t_trivial @! t_solve (ctn + 1) bases) tc
+    else (t_apply1 ip @! t_trivial @! t_solve (ctn + 1) bases) tc
 
   and t_solve ctn bases tc =
     match bases with
     | [] -> t_abort tc
-    | p::bases -> (FApi.t_or (t_apply ctn p) (t_solve ctn bases)) tc in
+    | ip::bases -> (FApi.t_or (t_apply ctn ip) (t_solve ctn bases)) tc in
 
   let t = t_solve 0 bases in
   let t = if canfail then FApi.t_try t else t in

src/ecLowGoal.mli

@@ -134,14 +134,13 @@ module Apply : sig
   exception NoInstance of (bool * reason * pt_env * (form * form))
 
   val t_apply_bwd_r :
-    ?mode:fmoptions -> ?canview:bool -> pt_ev -> FApi.backward
+    ?ri:EcReduction.reduction_info -> ?mode:fmoptions -> ?canview:bool -> pt_ev -> FApi.backward
 
   val t_apply_bwd :
-    ?mode:fmoptions -> ?canview:bool -> proofterm -> FApi.backward
+    ?ri:EcReduction.reduction_info -> ?mode:fmoptions -> ?canview:bool -> proofterm -> FApi.backward
 
   val t_apply_bwd_hi:
-       ?dpe:bool -> ?mode:fmoptions -> ?canview:bool
-    -> proofterm -> FApi.backward
+     ?ri:EcReduction.reduction_info -> ?dpe:bool -> ?mode:fmoptions -> ?canview:bool -> proofterm -> FApi.backward
 end
 
 (* -------------------------------------------------------------------- *)

src/ecMaps.ml

@@ -148,3 +148,44 @@ module Hdint = EHashtbl.Make(DInt)
 (* --------------------------------------------------------------------*)
 module Mstr = Map.Make(String)
 module Sstr = Set.MakeOfMap(Mstr)
+
+(* --------------------------------------------------------------------*)
+module Trie : sig
+  type ('a, 'b) t
+
+  val empty : ('a, 'b) t
+  val add   : 'a list -> 'b -> ('a, 'b) t -> ('a, 'b) t
+  val iter  : ('a list -> 'b list -> unit) -> ('a, 'b) t -> unit
+end = struct
+  module Map = BatMap
+
+  type ('a, 'b) t =
+    { children : ('a, ('a, 'b) t) Map.t
+    ; value    : 'b list }
+
+  let empty : ('a, 'b) t =
+    { value = []; children = Map.empty; }
+
+  let add (path : 'a list) (value : 'b) (t : ('a, 'b) t) =
+    let rec doit (path : 'a list) (t : ('a, 'b) t) =
+      match path with
+      | [] ->
+        { t with value = value :: t.value }
+      | v :: path ->
+        let children =
+          t.children |> Map.update_stdlib v (fun children ->
+            let subtrie = Option.value ~default:empty children in
+            Some (doit path subtrie)
+          )
+        in { t with children }
+    in doit path t
+
+  let iter (f : 'a list -> 'b list -> unit) (t : ('a, 'b) t) =
+    let rec doit (prefix : 'a list) (t : ('a, 'b) t) =
+      if not (List.is_empty t.value) then
+        f prefix t.value;
+      Map.iter (fun k v -> doit (k :: prefix) v) t.children
+    in
+    
+    doit [] t
+end