Skip to content

Commit

Permalink
Remove "non-import" flags from axioms
Browse files Browse the repository at this point in the history 
In prevision of having a general mechanism for it.
  • Loading branch information
@strub
strub committed Jan 13, 2025
1 parent 1f33371 commit 2d59ffa
Show file tree
Hide file tree
Showing 9 changed files with 90 additions and 103 deletions.
22 changes: 10 additions & 12 deletions src/ecDecl.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -137,13 +137,11 @@ and opopaque = { smt: bool; reduction: bool; }
type axiom_kind = [`Axiom of (Ssym.t * bool) | `Lemma]

type axiom = {
ax_tparams : ty_params;
ax_spec : EcCoreFol.form;
ax_kind : axiom_kind;
ax_loca : locality;
ax_visibility : ax_visibility; }

and ax_visibility = [`Visible | `NoSmt | `Hidden]
ax_tparams : ty_params;
ax_spec : EcCoreFol.form;
ax_kind : axiom_kind;
ax_loca : locality;
ax_smt : bool; }

let is_axiom (x : axiom_kind) = match x with `Axiom _ -> true | _ -> false
let is_lemma (x : axiom_kind) = match x with `Lemma -> true | _ -> false
Expand Down Expand Up @@ -272,11 +270,11 @@ let axiomatized_op ?(nargs = 0) ?(nosmt = false) path (tparams, axbd) lc =
let op = f_app op opargs axbd.f_ty in
let axspec = f_forall args (f_eq op axbd) in

{ ax_tparams = axpm;
ax_spec = axspec;
ax_kind = `Axiom (Ssym.empty, false);
ax_loca = lc;
ax_visibility = if nosmt then `NoSmt else `Visible; }
{ ax_tparams = axpm;
ax_spec = axspec;
ax_kind = `Axiom (Ssym.empty, false);
ax_loca = lc;
ax_smt = not nosmt; }

(* -------------------------------------------------------------------- *)
type typeclass = {
Expand Down
12 changes: 5 additions & 7 deletions src/ecDecl.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -135,15 +135,13 @@ val operator_as_prind : operator -> prind
type axiom_kind = [`Axiom of (Ssym.t * bool) | `Lemma]

type axiom = {
ax_tparams : ty_params;
ax_spec : form;
ax_kind : axiom_kind;
ax_loca : locality;
ax_visibility : ax_visibility;
ax_tparams : ty_params;
ax_spec : form;
ax_kind : axiom_kind;
ax_loca : locality;
ax_smt : bool;
}

and ax_visibility = [`Visible | `NoSmt | `Hidden]

(* -------------------------------------------------------------------- *)
val is_axiom : axiom_kind -> bool
val is_lemma : axiom_kind -> bool
Expand Down
47 changes: 21 additions & 26 deletions src/ecEnv.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -735,11 +735,11 @@ module MC = struct
let axp = EcPath.prefix (Lazy.force mypath) in
let axp = IPPath (EcPath.pqoname axp name) in
let ax =
{ ax_kind = `Lemma;
ax_tparams = tv;
ax_spec = cl;
ax_loca = (snd obj).op_loca;
ax_visibility = `Visible; } in
{ ax_kind = `Lemma;
ax_tparams = tv;
ax_spec = cl;
ax_loca = (snd obj).op_loca;
ax_smt = true; } in
(name, (axp, ax))) ax in

List.fold_left (fun mc -> curry (_up_axiom candup mc)) mc ax
Expand Down Expand Up @@ -791,13 +791,11 @@ module MC = struct
let (schelim, schcase) =
let do1 scheme name =
let scname = Printf.sprintf "%s_%s" x name in
(scname, { ax_tparams = tyd.tyd_params;
ax_spec = scheme;
ax_kind = `Lemma;
ax_loca = loca;
ax_visibility = `NoSmt;
})
in
(scname, { ax_tparams = tyd.tyd_params;
ax_spec = scheme;
ax_kind = `Lemma;
ax_loca = loca;
ax_smt = false; }) in
(do1 schelim "ind", do1 schcase "case")
in

Expand Down Expand Up @@ -836,12 +834,11 @@ module MC = struct

let scheme =
let scname = Printf.sprintf "%s_ind" x in
(scname, { ax_tparams = tyd.tyd_params;
ax_spec = scheme;
ax_kind = `Lemma;
ax_loca = loca;
ax_visibility = `NoSmt;
})
(scname, { ax_tparams = tyd.tyd_params;
ax_spec = scheme;
ax_kind = `Lemma;
ax_loca = loca;
ax_smt = false; })
in

let stname = Printf.sprintf "mk_%s" x in
Expand Down Expand Up @@ -923,11 +920,11 @@ module MC = struct
List.map
(fun (x, ax) ->
let ax = EcSubst.subst_form fsubst ax in
(x, { ax_tparams = [(self, Sp.singleton mypath)];
ax_spec = ax;
ax_kind = `Lemma;
ax_loca = loca;
ax_visibility = `NoSmt; }))
(x, { ax_tparams = [(self, Sp.singleton mypath)];
ax_spec = ax;
ax_kind = `Lemma;
ax_loca = loca;
ax_smt = false; }))
tc.tc_axs
in

Expand Down Expand Up @@ -3025,9 +3022,7 @@ module Theory = struct
MC.import_operator (xpath x) op env
| Th_axiom (x, ax) ->
if ax.ax_visibility <> `Hidden
then MC.import_axiom (xpath x) ax env
else env
MC.import_axiom (xpath x) ax env
| Th_modtype (x, mty) ->
MC.import_modty (xpath x) mty env
Expand Down
7 changes: 3 additions & 4 deletions src/ecPrinting.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2506,10 +2506,9 @@ let pp_axiom ?(long=false) (ppe : PPEnv.t) fmt (x, ax) =

let pp_decl fmt () =
let vs =
match ax.ax_visibility with
| `Visible -> []
| `NoSmt -> ["nosmt"]
| `Hidden -> ["(* hidden *)"] in
match ax.ax_smt with
| true -> []
| false -> ["nosmt"] in


Format.fprintf fmt "@[<hov 2>%a %t%t:@ %t.@]"
Expand Down
82 changes: 41 additions & 41 deletions src/ecScope.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -305,8 +305,8 @@ and proof_state =
PSNoCheck | PSCheck of EcCoreGoal.proof

and pucflags = {
puc_visibility : EcDecl.ax_visibility;
puc_local : bool;
puc_smt : bool;
puc_local : bool;
}

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -888,11 +888,11 @@ module Ax = struct
| PAxiom tags -> `Axiom (Ssym.of_list (List.map unloc tags), false)
| _ -> `Lemma

in { ax_tparams = tparams;
ax_spec = concl;
ax_kind = kind;
ax_loca = ax.pa_locality;
ax_visibility = `Visible; }
in { ax_tparams = tparams;
ax_spec = concl;
ax_kind = kind;
ax_loca = ax.pa_locality;
ax_smt = true; }
in

match ax.pa_kind with
Expand All @@ -904,7 +904,7 @@ module Ax = struct
| `Global -> false in

let check = Check_mode.check scope.sc_options in
let pucflags = { puc_visibility = axd.ax_visibility; puc_local = local; } in
let pucflags = { puc_smt = axd.ax_smt; puc_local = local; } in
let pucflags = (([], None), pucflags) in

match tc with
Expand Down Expand Up @@ -1058,7 +1058,7 @@ module Ax = struct
in
doit [] (fst puc.puc_cont)
in
let pucflags = { puc_visibility = ax.ax_visibility; puc_local = false; } in
let pucflags = { puc_smt = ax.ax_smt; puc_local = false; } in
let pucflags = ((proofs, snd puc.puc_cont), pucflags) in
let check = Check_mode.check scope.sc_options in

Expand Down Expand Up @@ -1218,11 +1218,11 @@ module Op = struct
(Tvar.f_subst ~freshen:true bdpm (List.map EcTypes.tvar axpm) ax,
List.combine axpm (List.map snd tparams)) in
let ax =
{ ax_tparams = axpm;
ax_spec = ax;
ax_kind = `Axiom (Ssym.empty, false);
ax_loca = lc;
ax_visibility = `Visible; }
{ ax_tparams = axpm;
ax_spec = ax;
ax_kind = `Axiom (Ssym.empty, false);
ax_loca = lc;
ax_smt = true; }
in Ax.bind scope (unloc rname, ax))
scope refts
in
Expand Down Expand Up @@ -1271,11 +1271,11 @@ module Op = struct
let ax = EcFol.f_forall (List.map (snd_map gtty) bds) ax in

let ax =
{ ax_tparams = List.map (fun ty -> (ty, Sp.empty)) nparams;
ax_spec = ax;
ax_kind = `Axiom (Ssym.empty, false);
ax_loca = lc;
ax_visibility = `Visible; } in
{ ax_tparams = List.map (fun ty -> (ty, Sp.empty)) nparams;
ax_spec = ax;
ax_kind = `Axiom (Ssym.empty, false);
ax_loca = lc;
ax_smt = true; } in

let scope, axname =
let axname = Printf.sprintf "%s_%s" (unloc op.po_name) suffix in
Expand Down Expand Up @@ -1394,11 +1394,11 @@ module Op = struct
in

let prax = EcDecl.{
ax_tparams = [];
ax_spec = prax;
ax_kind = `Lemma;
ax_loca = op.ppo_locality;
ax_visibility = `Visible;
ax_tparams = [];
ax_spec = prax;
ax_kind = `Lemma;
ax_loca = op.ppo_locality;
ax_smt = true;
} in

Ax.bind scope (unloc op.ppo_name ^ "_opsem", prax) in
Expand Down Expand Up @@ -1427,11 +1427,11 @@ module Op = struct
in

let prax = EcDecl.{
ax_tparams = [];
ax_spec = hax;
ax_kind = `Lemma;
ax_loca = op.ppo_locality;
ax_visibility = `Visible;
ax_tparams = [];
ax_spec = hax;
ax_kind = `Lemma;
ax_loca = op.ppo_locality;
ax_smt = true;
} in

Ax.bind scope (unloc op.ppo_name ^ "_opsem_det", prax)
Expand Down Expand Up @@ -1751,11 +1751,11 @@ module Ty = struct
(fun (x, req) ->
if not (Mstr.mem x symbs) then
let ax = {
ax_tparams = [];
ax_spec = req;
ax_kind = `Lemma;
ax_loca = lc;
ax_visibility = `NoSmt;
ax_tparams = [];
ax_spec = req;
ax_kind = `Lemma;
ax_loca = lc;
ax_smt = false;
} in Some ((None, ax), EcPath.psymbol x, scope.sc_env)
else None)
reqs in
Expand All @@ -1766,14 +1766,14 @@ module Ty = struct
let t = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]) } in
let t = { pt_core = t; pt_intros = []; } in
let ax = {
ax_tparams = [];
ax_spec = f;
ax_kind = `Lemma;
ax_visibility = `NoSmt;
ax_loca = lc;
ax_tparams = [];
ax_spec = f;
ax_kind = `Lemma;
ax_smt = false;
ax_loca = lc;
} in

let pucflags = { puc_visibility = `Visible; puc_local = false; } in
let pucflags = { puc_smt = true; puc_local = false; } in
let pucflags = (([], None), pucflags) in
let check = Check_mode.check scope.sc_options in

Expand Down Expand Up @@ -2273,7 +2273,7 @@ module Cloning = struct
let t = { pt_core = t; pt_intros = []; } in
let (x, ax) = axc.C.axc_axiom in

let pucflags = { puc_visibility = `Visible; puc_local = false; } in
let pucflags = { puc_smt = true; puc_local = false; } in
let pucflags = (([], None), pucflags) in
let check = Check_mode.check scope.sc_options in

Expand Down
4 changes: 2 additions & 2 deletions src/ecScope.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,8 +50,8 @@ and proof_state =
PSNoCheck | PSCheck of EcCoreGoal.proof

and pucflags = {
puc_visibility : EcDecl.ax_visibility;
puc_local : bool;
puc_smt : bool;
puc_local : bool;
}

(* -------------------------------------------------------------------- *)
Expand Down
4 changes: 2 additions & 2 deletions src/ecSmt.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1540,7 +1540,7 @@ let init_relevant env pi rs =
let push e r = r := e :: !r in
let do1 p ax =
let wanted = wanted_ax p in
if wanted || (ax.ax_visibility = `Visible && not (unwanted_ax p)) then begin
if wanted || (ax.ax_smt && not (unwanted_ax p)) then begin
Frequency.add fr ax.ax_spec;
let used = Frequency.f_ops unwanted_ops ax.ax_spec in
let paxu = (p,ax), used in
Expand Down Expand Up @@ -1631,7 +1631,7 @@ let init hyps concl =
let select env pi hyps concl execute_task =
if pi.P.pr_all then
let init_select p ax =
ax.ax_visibility = `Visible && not (P.Hints.mem p pi.P.pr_unwanted) in
ax.ax_smt && not (P.Hints.mem p pi.P.pr_unwanted) in
(execute_task (EcEnv.Ax.all ~check:init_select env) = Some true)
else
let rs = Frequency.f_ops_goal unwanted_ops hyps.h_local concl in
Expand Down
10 changes: 5 additions & 5 deletions src/ecSubst.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -976,11 +976,11 @@ let subst_ax (s : subst) (ax : axiom) =
let s, tparams = fresh_tparams s ax.ax_tparams in
let spec = subst_form s ax.ax_spec in

{ ax_tparams = tparams;
ax_spec = spec;
ax_kind = ax.ax_kind;
ax_loca = ax.ax_loca;
ax_visibility = ax.ax_visibility; }
{ ax_tparams = tparams;
ax_spec = spec;
ax_kind = ax.ax_kind;
ax_loca = ax.ax_loca;
ax_smt = ax.ax_smt; }

(* -------------------------------------------------------------------- *)
let fresh_scparam (s : subst) ((x, ty) : EcIdent.t * ty) =
Expand Down
5 changes: 1 addition & 4 deletions src/ecTheoryReplay.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -692,10 +692,7 @@ and replay_axd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, ax) =
| Some (pt, hide, explicit) ->
if explicit && not (EcDecl.is_axiom ax.ax_kind) then
clone_error (EcSection.env scenv) (CE_ProofForLemma (snd ove.ovre_prefix, x));
let ax = { ax with
ax_kind = `Lemma;
ax_visibility = if hide <> `Alias then `Hidden else ax.ax_visibility
} in
let ax = { ax with ax_kind = `Lemma } in
let axc = { axc_axiom = (x, ax);
axc_path = EcPath.fromqsymbol (snd ove.ovre_prefix, x);
axc_tac = pt;
Expand Down

0 comments on commit 2d59ffa

Please sign in to comment.