diff --git a/easycrypt.project b/easycrypt.project index f59238299..1373f9bfc 100644 --- a/easycrypt.project +++ b/easycrypt.project @@ -2,3 +2,5 @@ provers = Alt-Ergo@2.4 provers = CVC5@1.0 provers = Z3@4.12 + +rdirs = Jasmin:../jasmin/eclib diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 6b0e8f4fa..480c141e5 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -298,75 +298,125 @@ 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 ppe0 = EcPrinting.PPEnv.ofenv env in + let buffer = Buffer.create 0 in + let fmt = Format.formatter_of_buffer buffer 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 + EcPrinting.pp_by_theory ppe0 (EcPrinting.pp_axiom) fmt ax; + + EcScope.notify scope `Warning "%s" (Buffer.contents buffer) +(* -------------------------------------------------------------------- *) +let process_print_hint_solve (scope : EcScope.scope) = + let env = EcScope.env scope in + let hint_solve = EcEnv.Auto.all env in + let hint_solve = List.map (fun (ir, p) -> (p, (EcEnv.Ax.by_path p env, ir))) hint_solve 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 pp_hint_solve ppe fmt = (fun (p, (hint_solve, ir)) -> + Format.fprintf fmt "%a%s" (EcPrinting.pp_axiom ppe) (p, hint_solve) + (if ir then " (irreducible)" else " (reducible)") + ) + in + + EcPrinting.pp_by_theory ppe0 pp_hint_solve fmt hint_solve; - let thpath = EcPath.fromqsymbol thpath in + EcScope.notify scope `Warning "%s" (Buffer.contents buffer) - let ppe = EcPrinting.PPEnv.enter_theory ppe0 thpath in +let process_print_hint_rewrite (scope : EcScope.scope) = + let env = EcScope.env scope in + let hint_rewrite = EcEnv.BaseRw.all env in + + let ppe0 = EcPrinting.PPEnv.ofenv env in + let buffer = Buffer.create 0 in + let fmt = Format.formatter_of_buffer buffer in - Format.fprintf fmt - "@.========== %a ==========@.@." (EcPrinting.pp_thname ppe0) thpath; + let pp_hint_rewrite _ppe fmt = (fun (p, sp) -> + let elems = EcPath.Sp.ntr_elements sp in + if List.is_empty elems then + Format.fprintf fmt "%s (empty)@." (EcPath.tostring p) + else + Format.fprintf fmt "%s = @.@[%a@]@." (EcPath.tostring p) + (EcPrinting.pp_list "@." (fun fmt p -> + Format.fprintf fmt "%s" (EcPath.tostring p))) + (EcPath.Sp.ntr_elements sp) + ) + in + + EcPrinting.pp_by_theory ppe0 pp_hint_rewrite fmt hint_rewrite; - List.iter (fun ax -> - Format.fprintf fmt "%a@." (EcPrinting.pp_axiom ppe) ax - ) axs - ) ax; + EcScope.notify scope `Warning "%s" (Buffer.contents buffer) + +let process_print_hint_simplify (scope : EcScope.scope) = + let env = EcScope.env scope in + let open EcTheory in + let (hint_simplify: (EcEnv.Reduction.topsym * rule list) list) = EcEnv.Reduction.all env in + let hint_simplify = List.filter_map (fun (ts, rl) -> + match ts with + | `Path p -> Some (p, rl) + | _ -> None + ) hint_simplify + in + + let ppe0 = EcPrinting.PPEnv.ofenv env in + let buffer = Buffer.create 0 in + let fmt = Format.formatter_of_buffer buffer in + + let rec pp_rule_pattern ppe fmt (rl_pt: rule_pattern) = + match rl_pt with + | Rule (trp, rp_list) -> pp_rule ppe fmt trp rp_list + | Int z -> Format.fprintf fmt "%s" (EcBigInt.to_string z) + | Var v -> Format.fprintf fmt "%s" (EcIdent.name v) + + and pp_rule_patterns ppe fmt (rl_pts: rule_pattern list) = + match rl_pts with + | [] -> () + | rl_pts -> Format.fprintf fmt "(%a)" (EcPrinting.pp_list "," (pp_rule_pattern ppe)) rl_pts + + and pp_rule ppe fmt trp rl_pts = + match trp with + | `Tuple -> Format.fprintf fmt "tuple%a" (pp_rule_patterns ppe) rl_pts + | `Op (p, _) -> Format.fprintf fmt "%a%a" (EcPrinting.pp_opname ppe) p (pp_rule_patterns ppe) rl_pts + | `Proj i -> if List.is_empty rl_pts then () else + Format.fprintf fmt "%a`%d" (pp_rule_patterns ppe) rl_pts i + in + + let pp_hint_simplify ppe fmt = (fun (p, (rls : rule list)) -> + Format.fprintf fmt "%s:@.@[%a@]" (EcPath.tostring p) + (EcPrinting.pp_list "@." (fun fmt rl -> + Format.fprintf fmt "Conditions: %a@.Target: %a@.Pattern: %a@." + (EcPrinting.pp_list "," (EcPrinting.pp_form ppe)) rl.rl_cond + (EcPrinting.pp_form ppe) rl.rl_tg + (pp_rule_pattern ppe) rl.rl_ptn + )) + rls + ) + in + + EcPrinting.pp_by_theory ppe0 pp_hint_simplify fmt hint_simplify; EcScope.notify scope `Warning "%s" (Buffer.contents buffer) +let process_print_hint (scope: EcScope.scope) (ph: pprinthint) = + if ph.solve then begin + EcScope.notify scope `Warning "Solve hints:@."; + process_print_hint_solve scope + end else (); + + if ph.simplify then begin + EcScope.notify scope `Warning "Simplify hints:@."; + process_print_hint_simplify scope + end else (); + + if ph.rewrite then begin + EcScope.notify scope `Warning "Rewrite hints:@."; + process_print_hint_rewrite scope + end else () + + (* -------------------------------------------------------------------- *) exception Pragma of [`Reset | `Restart] @@ -735,6 +785,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 ph -> `Fct (fun scope -> process_print_hint scope ph; 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) diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml index a8187a70e..41a9cfe48 100644 --- a/src/ecCorePrinting.ml +++ b/src/ecCorePrinting.ml @@ -55,6 +55,8 @@ module type PrinterAPI = sig val pp_axname : PPEnv.t -> path pp val pp_tcname : PPEnv.t -> path pp val pp_thname : PPEnv.t -> path pp + (* FIXME: where should this go? *) + val pp_by_theory : PPEnv.t -> (PPEnv.t -> (EcPath.path * 'a) pp) -> ((EcPath.path * 'a) list) pp val pp_mem : PPEnv.t -> EcIdent.t pp val pp_memtype : PPEnv.t -> EcMemory.memtype pp diff --git a/src/ecEnv.ml b/src/ecEnv.ml index 34662c4b0..03421af05 100644 --- a/src/ecEnv.ml +++ b/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 @@ -1444,6 +1445,10 @@ module BaseRw = struct (omap (fun s -> List.fold_left (fun s r -> Sp.add r s) s l)) (IPPath p) env.env_rwbase; env_item = mkitem import (Th_addrw (p, l, lc)) :: env.env_item; } + + let all env = + List.map (fun (IPPath p, sp) -> (p, sp)) @@ + Mip.bindings env.env_rwbase end (* -------------------------------------------------------------------- *) @@ -1496,45 +1501,51 @@ module Reduction = struct Mrd.find_opt p env.env_redbase |> omap (fun x -> Lazy.force x.ri_list) |> odfl [] + + (* FIXME: handle other cases, right now only used for print hint *) + let all env = + List.map (fun (ts, mr) -> + (ts, Lazy.force mr.ri_list)) + (Mrd.bindings env.env_redbase) 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 +1554,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 +2946,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 +3120,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 diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 0e8712174..e8d267e21 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -398,6 +398,8 @@ module BaseRw : sig val add : ?import:import -> symbol -> is_local -> env -> env val addto : ?import:import -> path -> path list -> is_local -> env -> env + + val all : env -> (path * Sp.t) list end (* -------------------------------------------------------------------- *) @@ -408,16 +410,19 @@ module Reduction : sig val add1 : path * rule_option * rule option -> env -> env val add : ?import:import -> (path * rule_option * rule option) list -> env -> env val get : topsym -> env -> rule list + + val all : env -> (topsym * rule list) list 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 (* -------------------------------------------------------------------- *) diff --git a/src/ecLexer.mll b/src/ecLexer.mll index c1225b072..73baa8c0f 100644 --- a/src/ecLexer.mll +++ b/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 *) diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 003bf07a9..fdb735bf3 100644 --- a/src/ecLowGoal.ml +++ b/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 diff --git a/src/ecLowGoal.mli b/src/ecLowGoal.mli index 093f14424..b9107b8dc 100644 --- a/src/ecLowGoal.mli +++ b/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 (* -------------------------------------------------------------------- *) diff --git a/src/ecParser.mly b/src/ecParser.mly index 71dfbc9b2..29b9962ba 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -134,6 +134,9 @@ fp_head = FPCut (None, None); fp_args = []; }) info + let mk_print_hint (simplify) (solve) (rewrite) = + {simplify; solve; rewrite} + (* ------------------------------------------------------------------ *) let locality_as_local (lc : locality located) = match unloc lc with @@ -482,6 +485,7 @@ %token INTERLEAVE %token INSTANCE %token IOTA +%token IRREDUCIBLE %token IS %token KILL %token LARROW @@ -3763,9 +3767,15 @@ print: | REWRITE qs=qident { Pr_db (`Rewrite qs) } | SOLVE qs=ident { Pr_db (`Solve qs) } +%inline phint: +| { mk_print_hint true true true } +| SIMPLIFY { mk_print_hint true false false } +| SOLVE { mk_print_hint false true false } +| REWRITE { mk_print_hint false false true } + coq_info: | { None } -| CHECK { Some EcProvers.Check } +| CHECK { Some EcProvers.Check } | EDIT { Some EcProvers.Edit } | FIX { Some EcProvers.Fix } @@ -3817,14 +3827,30 @@ addrw: | local=is_local HINT REWRITE p=lqident COLON l=lqident* { (local, p, l) } + + (* FIXME: fix integration of irreducible optional keyword *) hint: | local=is_local HINT EXACT base=lident? COLON l=qident* { { ht_local = local; ht_prio = 0; - ht_base = base ; ht_names = l; } } + ht_base = base ; ht_names = l; + ht_irreducible = false; } } | local=is_local HINT SOLVE i=word base=lident? COLON l=qident* { { ht_local = local; ht_prio = i; - ht_base = base ; ht_names = l; } } + ht_base = base ; ht_names = l; + ht_irreducible = false; } } + +| local=is_local HINT IRREDUCIBLE EXACT base=lident? COLON l=qident* + { { ht_local = local; ht_prio = 0; + ht_base = base ; ht_names = l; + ht_irreducible = true; } } + +| local=is_local HINT IRREDUCIBLE SOLVE i=word base=lident? COLON l=qident* + { { ht_local = local; ht_prio = i; + ht_base = base ; ht_names = l; + ht_irreducible = true; } } + + (* -------------------------------------------------------------------- *) (* User reduction *) @@ -3888,6 +3914,7 @@ global_action: | x=loc(proofend) { Gsave x } | PRINT p=print { Gprint p } | PRINT AXIOM { Gpaxiom } +| PRINT HINT ph=phint { Gphint ph } | SEARCH x=search+ { Gsearch x } | LOCATE x=qident { Glocate x } | WHY3 x=STRING { GdumpWhy3 x } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 53eda26b8..4fea65c3c 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -1123,6 +1123,12 @@ type pprint = | Pr_goal of int | Pr_db of [`Rewrite of pqsymbol | `Solve of psymbol] +type pprinthint = + { rewrite : bool + ; simplify : bool + ; solve : bool + } + (* -------------------------------------------------------------------- *) type renaming_kind = | RNty @@ -1234,6 +1240,7 @@ type phint = { ht_prio : int; ht_base : psymbol option; ht_names : pqsymbol list; + ht_irreducible : bool; } (* -------------------------------------------------------------------- *) @@ -1264,6 +1271,7 @@ type global_action = | Ghint of phint | Gprint of pprint | Gpaxiom + | Gphint of pprinthint | Gsearch of pformula list | Glocate of pqsymbol | GthOpen of (is_local * bool * psymbol) diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 9b5232c5b..1119b1e0d 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -476,10 +476,84 @@ let pp_rwname ppe fmt p = let pp_axname ppe fmt p = Format.fprintf fmt "%a" EcSymbols.pp_qsymbol (PPEnv.ax_symb ppe p) +let pp_axhnt ppe fmt (b, p) = + Format.fprintf fmt "%a%s" (pp_axname ppe) p (if b then " (irreducible)" else "") + (* -------------------------------------------------------------------- *) let pp_thname ppe fmt p = EcSymbols.pp_qsymbol fmt (PPEnv.th_symb ppe p) +(* -------------------------------------------------------------------- *) +let pp_by_theory + (ppe0: PPEnv.t) + (pp: PPEnv.t -> (EcPath.path * 'a) pp) + (fmt: Format.formatter) + (xs: (EcPath.path * 'a) list) += + 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 tr = + List.fold_left (fun tr ((p, _) as x) -> + Trie.add (EcPath.tolist (oget (EcPath.prefix p))) x tr + ) Trie.empty xs + in + + Trie.iter (fun prefix xs -> + let thpath = + match prefix with + | [] -> assert false + | name :: prefix -> (List.rev prefix, name) in + + let thpath = EcPath.fromqsymbol thpath in + + let ppe = PPEnv.enter_theory ppe0 thpath in + + Format.fprintf fmt + "@.========== %a ==========@.@." (pp_thname ppe0) thpath; + + List.iter (fun x -> + Format.fprintf fmt "%a@." (pp ppe) x + ) xs + ) tr + (* -------------------------------------------------------------------- *) let pp_funname (ppe : PPEnv.t) fmt p = Format.fprintf fmt "%a.%s" (pp_topmod ppe) p.P.x_top p.P.x_sub @@ -2890,23 +2964,27 @@ let pp_rwbase ppe fmt (p, rws) = (pp_rwname ppe) p (pp_list ", " (pp_axname ppe)) (Sp.elements rws) (* -------------------------------------------------------------------- *) -let pp_solvedb ppe fmt db = +let pp_solvedb ppe fmt (db: (int * (bool * P.path) list) list) = List.iter (fun (lvl, ps) -> Format.fprintf fmt "[%3d] %a\n%!" - lvl (pp_list ", " (pp_axname ppe)) ps) + lvl + (pp_list ", " (pp_axhnt ppe)) + ps) db; let lemmas = List.flatten (List.map snd db) in - let lemmas = List.pmap (fun p -> + let lemmas = List.pmap (fun (ir, p) -> let ax = EcEnv.Ax.by_path_opt p ppe.PPEnv.ppe_env in - (omap (fun ax -> (p, ax)) ax)) + (omap (fun ax -> ((p, ax), ir)) ax)) lemmas in + (* FIXME: maybe integrate irreducible print into pp_axiom *) if not (List.is_empty lemmas) then begin Format.fprintf fmt "\n%!"; List.iter - (fun ax -> Format.fprintf fmt "%a\n\n%!" (pp_axiom ppe) ax) + (fun (ax, ir) -> Format.fprintf fmt "%a%s\n\n%!" (pp_axiom ppe) ax + (if ir then " (irreducible)" else "")) lemmas end @@ -3391,11 +3469,11 @@ 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_auto (lvl, base, p, lc) -> + | EcTheory.Th_auto { level; base; axioms; locality} -> Format.fprintf fmt "%ahint solve %d %s : %a." - pp_locality lc - lvl (odfl "" base) - (pp_list "@ " (pp_axname ppe)) p + pp_locality locality + level (odfl "" base) + (pp_list "@ " (pp_axhnt ppe)) axioms (* -------------------------------------------------------------------- *) let pp_stmt_with_nums (ppe : PPEnv.t) fmt stmt = diff --git a/src/ecScope.ml b/src/ecScope.ml index b17295a4d..9ab43c4bd 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -796,8 +796,8 @@ module Auto = struct let item = EcTheory.mkitem EcTheory.import0 (Th_addrw (base, l, local)) in { scope with sc_env = EcSection.add_item item scope.sc_env } - let bind_hint scope ~local ~level ?base names = - let item = EcTheory.mkitem EcTheory.import0 (Th_auto (level, base, names, local)) in + let bind_hint scope ~local ~level ?base axioms = + let item = EcTheory.mkitem EcTheory.import0 (Th_auto { level; base; axioms; locality=local} ) in { scope with sc_env = EcSection.add_item item scope.sc_env } let add_hint scope hint = @@ -806,6 +806,7 @@ module Auto = struct let names = List.map (fun l -> EcEnv.Ax.lookup_path (unloc l) env) hint.ht_names in + let names = List.map (fun p -> (hint.ht_irreducible, p)) names in bind_hint scope ~local:hint.ht_local ~level:hint.ht_prio ?base names end @@ -1287,7 +1288,7 @@ module Op = struct List.fold_left (fun scope base -> - Auto.bind_hint ~local:(local_of_locality lc) ~level:0 ~base scope [axpath]) + Auto.bind_hint ~local:(local_of_locality lc) ~level:0 ~base scope [(false, axpath)]) scope bases in diff --git a/src/ecSection.ml b/src/ecSection.ml index 127040f6b..074f10c6f 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -1016,12 +1016,12 @@ let generalize_addrw to_gen (p, ps, lc) = let generalize_reduction to_gen _rl = to_gen, None -let generalize_auto to_gen (n,s,ps,lc) = - if lc = `Local then to_gen, None +let generalize_auto to_gen auto_rl = + if auto_rl.locality = `Local then to_gen, None else - let ps = List.filter (fun p -> to_keep to_gen (`Ax p)) ps in - if ps = [] then to_gen, None - else to_gen, Some (Th_auto (n,s,ps,lc)) + let axioms = List.filter (fun (_b, p) -> to_keep to_gen (`Ax p)) auto_rl.axioms in + if axioms = [] then to_gen, None + else to_gen, Some (Th_auto {auto_rl with axioms}) (* --------------------------------------------------------------- *) let get_locality scenv = scenv.sc_loca @@ -1046,7 +1046,7 @@ 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_auto (i,s,p,lc) -> Th_auto (i, s, p, set_local lc) + | Th_auto auto_rl -> Th_auto {auto_rl with locality=set_local auto_rl.locality} in { item with ti_item = lcitem } @@ -1337,19 +1337,20 @@ let add_item_ (item : theory_item) (scenv:scenv) = let env = scenv.sc_env in let env = match item.ti_item with - | Th_type (s,tyd) -> EcEnv.Ty.bind s tyd env - | Th_operator (s,op) -> EcEnv.Op.bind s op env - | Th_axiom (s, ax) -> EcEnv.Ax.bind s ax env - | Th_modtype (s, ms) -> EcEnv.ModTy.bind s ms env - | Th_module me -> EcEnv.Mod.bind me.tme_expr.me_name me env - | Th_typeclass(s,tc) -> EcEnv.TypeClass.bind s tc env - | Th_export (p, lc) -> EcEnv.Theory.export p lc env - | Th_instance (tys,i,lc) -> EcEnv.TypeClass.add_instance tys i lc env - | Th_baserw (s,lc) -> EcEnv.BaseRw.add s lc env - | Th_addrw (p,ps,lc) -> EcEnv.BaseRw.addto p ps lc env - | Th_auto (level, base, ps, lc) -> EcEnv.Auto.add ~level ?base ps lc env - | Th_reduction r -> EcEnv.Reduction.add r env - | _ -> assert false + | Th_type (s,tyd) -> EcEnv.Ty.bind s tyd env + | Th_operator (s,op) -> EcEnv.Op.bind s op env + | Th_axiom (s, ax) -> EcEnv.Ax.bind s ax env + | Th_modtype (s, ms) -> EcEnv.ModTy.bind s ms env + | Th_module me -> EcEnv.Mod.bind me.tme_expr.me_name me env + | Th_typeclass(s,tc) -> EcEnv.TypeClass.bind s tc env + | Th_export (p, lc) -> EcEnv.Theory.export p lc env + | Th_instance (tys,i,lc) -> EcEnv.TypeClass.add_instance tys i lc env + | Th_baserw (s,lc) -> EcEnv.BaseRw.add s lc env + | Th_addrw (p,ps,lc) -> EcEnv.BaseRw.addto p ps lc env + | Th_auto {level; base; + axioms; locality;} -> EcEnv.Auto.add ~level ?base axioms locality env + | Th_reduction r -> EcEnv.Reduction.add r env + | _ -> assert false in { scenv with sc_env = env; @@ -1493,8 +1494,8 @@ let check_item scenv item = | Th_addrw (_,_,lc) -> if (lc = `Local && not scenv.sc_insec) then hierror "local hint rewrite can only be declared inside section"; - | Th_auto (_, _, _, lc) -> - if (lc = `Local && not scenv.sc_insec) then + | Th_auto {locality} -> + if (locality = `Local && not scenv.sc_insec) then hierror "local hint can only be declared inside section"; | Th_reduction _ -> () | Th_theory _ -> assert false diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 977f7e365..5c62dadb0 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -1075,8 +1075,8 @@ 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_auto (lvl, base, ps, lc) -> - Th_auto (lvl, base, List.map (subst_path s) ps, lc) + | Th_auto ({axioms} as auto_rl) -> + Th_auto {auto_rl with axioms = List.map (fun (b, a) -> (b, (subst_path s a))) axioms} (* -------------------------------------------------------------------- *) and subst_theory (s : subst) (items : theory) = diff --git a/src/ecTheory.ml b/src/ecTheory.ml index 0d39c8d21..0e9eaca48 100644 --- a/src/ecTheory.ml +++ b/src/ecTheory.ml @@ -37,7 +37,7 @@ 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_auto of (int * symbol option * path list * is_local) + | Th_auto of auto_rule and thsource = { ths_base : EcPath.path; @@ -75,6 +75,13 @@ and rule_option = { ur_eqtrue : bool; } +and auto_rule = { + level : int; + base : symbol option; + axioms : (bool * path) list; + locality: is_local; +} + let mkitem (import : import) (item : theory_item_r) = { ti_import = import; ti_item = item; } diff --git a/src/ecTheory.mli b/src/ecTheory.mli index 472928561..70cda9300 100644 --- a/src/ecTheory.mli +++ b/src/ecTheory.mli @@ -34,7 +34,7 @@ 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_auto of (int * symbol option * path list * is_local) + | Th_auto of auto_rule and thsource = { ths_base : EcPath.path; @@ -72,6 +72,13 @@ and rule_option = { ur_eqtrue : bool; } +and auto_rule = { + level : int; + base : symbol option; + axioms : (bool * path) list; + locality: is_local; +} + val mkitem : import -> theory_item_r -> theory_item (* -------------------------------------------------------------------- *) diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 227aaee34..a2d476cb5 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -825,12 +825,12 @@ and replay_addrw (* -------------------------------------------------------------------- *) and replay_auto - (ove : _ ovrenv) (subst, ops, proofs, scope) (import, lvl, base, ps, lc) + (ove : _ ovrenv) (subst, ops, proofs, scope) (import, at_base) = let env = EcSection.env (ove.ovre_hooks.henv scope) in - let ps = List.map (EcSubst.subst_path subst) ps in - let ps = List.filter (fun p -> Option.is_some (EcEnv.Ax.by_path_opt p env)) ps in - let scope = ove.ovre_hooks.hadd_item scope import (Th_auto (lvl, base, ps, lc)) in + let axioms = List.map (fun (ir, p) -> (ir, EcSubst.subst_path subst p)) at_base.axioms in + let axioms = List.filter (fun (_ir, p) -> Option.is_some (EcEnv.Ax.by_path_opt p env)) axioms in + let scope = ove.ovre_hooks.hadd_item scope import (Th_auto {at_base with axioms}) in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) @@ -981,8 +981,8 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) item = | Th_reduction rules -> replay_reduction ove (subst, ops, proofs, scope) (item.ti_import, rules) - | Th_auto (lvl, base, ps, lc) -> - replay_auto ove (subst, ops, proofs, scope) (item.ti_import, lvl, base, ps, lc) + | Th_auto at_base -> + replay_auto ove (subst, ops, proofs, scope) (item.ti_import, at_base) | Th_typeclass (x, tc) -> replay_typeclass ove (subst, ops, proofs, scope) (item.ti_import, x, tc)