Skip to content

Rework import mechanism #683

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Rework import mechanism #683

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 15 additions & 18 deletions src/ecDecl.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,9 @@ type ty_params = ty_param list
type ty_pctor = [ `Int of int | `Named of ty_params ]

type tydecl = {
tyd_params : ty_params;
tyd_type : ty_body;
tyd_loca : locality;
tyd_resolve : bool;
tyd_params : ty_params;
tyd_type : ty_body;
tyd_loca : locality;
}

and ty_body = [
Expand Down Expand Up @@ -48,7 +47,7 @@ let tydecl_as_record (td : tydecl) =
match td.tyd_type with `Record x -> Some x | _ -> None

(* -------------------------------------------------------------------- *)
let abs_tydecl ?(resolve = true) ?(tc = Sp.empty) ?(params = `Int 0) lc =
let abs_tydecl ?(tc = Sp.empty) ?(params = `Int 0) lc =
let params =
match params with
| `Named params ->
Expand All @@ -60,7 +59,7 @@ let abs_tydecl ?(resolve = true) ?(tc = Sp.empty) ?(params = `Int 0) lc =
(EcUid.NameGen.bulk ~fmt n)
in

{ tyd_params = params; tyd_type = `Abstract tc; tyd_resolve = resolve; tyd_loca = lc; }
{ tyd_params = params; tyd_type = `Abstract tc; tyd_loca = lc; }

(* -------------------------------------------------------------------- *)
let ty_instanciate (params : ty_params) (args : ty list) (ty : ty) =
Expand Down Expand Up @@ -137,13 +136,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 +269,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
21 changes: 9 additions & 12 deletions src/ecDecl.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,9 @@ type ty_params = ty_param list
type ty_pctor = [ `Int of int | `Named of ty_params ]

type tydecl = {
tyd_params : ty_params;
tyd_type : ty_body;
tyd_loca : locality;
tyd_resolve : bool;
tyd_params : ty_params;
tyd_type : ty_body;
tyd_loca : locality;
}

and ty_body = [
Expand All @@ -36,7 +35,7 @@ val tydecl_as_abstract : tydecl -> Sp.t option
val tydecl_as_datatype : tydecl -> ty_dtype option
val tydecl_as_record : tydecl -> (form * (EcSymbols.symbol * EcTypes.ty) list) option

val abs_tydecl : ?resolve:bool -> ?tc:Sp.t -> ?params:ty_pctor -> locality -> tydecl
val abs_tydecl : ?tc:Sp.t -> ?params:ty_pctor -> locality -> tydecl

val ty_instanciate : ty_params -> ty list -> ty -> ty

Expand Down Expand Up @@ -135,15 +134,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
Loading
Loading