Skip to content

Commit

Permalink
Rigid unification option for hint solve/exact + print hint
Browse files Browse the repository at this point in the history
  • Loading branch information
@Gustavo2622 @strub
Gustavo2622 authored and strub committed Jan 13, 2025
1 parent 2c4a5e1 commit 2fe6a42
Show file tree
Hide file tree
Showing 16 changed files with 251 additions and 174 deletions.
158 changes: 71 additions & 87 deletions src/ecCommands.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
open EcUtils
open EcLocation
open EcParsetree
open EcMaps

module Sid = EcIdent.Sid
module Mx = EcPath.Mx
Expand Down Expand Up @@ -226,6 +227,7 @@ module HiPrinting = struct
pv


(* -------------------------------------------------------------------- *)
let pr_goal fmt scope n =
match EcScope.xgoal scope with
| None | Some { EcScope.puc_active = None} ->
Expand Down Expand Up @@ -255,10 +257,76 @@ module HiPrinting = struct
fmt (goal, `One sz)
end
end

(* -------------------------------------------------------------------- *)
let pr_axioms (fmt : Format.formatter) (env : EcEnv.env) =
let ax = EcEnv.Ax.all ~check:(fun _ ax -> EcDecl.is_axiom ax.ax_kind) env 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

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 ax ->
Format.fprintf fmt "%a@." (EcPrinting.pp_axiom ppe) ax
) axs
) ax

(* -------------------------------------------------------------------- *)
let pr_hint (fmt : Format.formatter) (env : EcEnv.env) =
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

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
end

(* -------------------------------------------------------------------- *)
let process_pr fmt scope p =
let check_opname_validity (scope : EcScope.scope) (x : string) =
if EcIo.is_binop x = `Invalid then
EcScope.notify scope `Warning
"operator `%s' cannot be used in prefix mode" x;
if EcIo.is_uniop x = `Invalid then
EcScope.notify scope `Warning
"operator `%s' cannot be used in infix mode" x

(* -------------------------------------------------------------------- *)
let process_print ?(fmt = Format.std_formatter) (scope : EcScope.scope) (p : pprint) =
let env = EcScope.env scope in

match p with
Expand All @@ -280,92 +348,9 @@ let process_pr fmt scope p =
| Pr_glob pm -> HiPrinting.pr_glob fmt env pm
| Pr_goal n -> HiPrinting.pr_goal fmt scope n

(* -------------------------------------------------------------------- *)
let check_opname_validity (scope : EcScope.scope) (x : string) =
if EcIo.is_binop x = `Invalid then
EcScope.notify scope `Warning
"operator `%s' cannot be used in prefix mode" x;
if EcIo.is_uniop x = `Invalid then
EcScope.notify scope `Warning
"operator `%s' cannot be used in infix mode" x

(* -------------------------------------------------------------------- *)
let process_print scope p =
process_pr Format.std_formatter scope p

(* -------------------------------------------------------------------- *)
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
) 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 ax ->
Format.fprintf fmt "%a@." (EcPrinting.pp_axiom ppe) ax
) axs
) ax;
| Pr_axioms -> HiPrinting.pr_axioms fmt env

EcScope.notify scope `Warning "%s" (Buffer.contents buffer)
| Pr_hint -> HiPrinting.pr_hint fmt env

(* -------------------------------------------------------------------- *)
exception Pragma of [`Reset | `Restart]
Expand Down Expand Up @@ -734,7 +719,6 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g =
| GsctOpen name -> `Fct (fun scope -> process_sct_open scope name)
| 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)
| 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)
Expand Down
40 changes: 22 additions & 18 deletions src/ecEnv.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down Expand Up @@ -221,6 +221,7 @@ and env_notation = ty_params * EcDecl.notation

and ntbase = (path * env_notation) list


(* -------------------------------------------------------------------- *)
type env = preenv

Expand Down Expand Up @@ -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
Expand All @@ -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
(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
11 changes: 6 additions & 5 deletions src/ecEnv.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

(* -------------------------------------------------------------------- *)
Expand Down
1 change: 1 addition & 0 deletions src/ecLexer.mll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down
Loading

0 comments on commit 2fe6a42

Please sign in to comment.