aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/boot/fe/ast.ml21
-rw-r--r--src/boot/fe/item.ml7
-rw-r--r--src/boot/fe/lexer.mll2
-rw-r--r--src/boot/fe/pexp.ml5
-rw-r--r--src/boot/fe/token.ml6
-rw-r--r--src/comp/front/ast.rs5
-rw-r--r--src/comp/front/lexer.rs2
-rw-r--r--src/comp/front/parser.rs14
-rw-r--r--src/comp/front/token.rs6
-rw-r--r--src/lib/map.rs4
10 files changed, 4 insertions, 68 deletions
diff --git a/src/boot/fe/ast.ml b/src/boot/fe/ast.ml
index c2387c5a..26c3b7c1 100644
--- a/src/boot/fe/ast.ml
+++ b/src/boot/fe/ast.ml
@@ -37,11 +37,6 @@ type layer =
| LAYER_gc
;;
-type opacity =
- OPA_transparent
- | OPA_abstract
-;;
-
type mutability =
MUT_mutable
| MUT_immutable
@@ -720,22 +715,6 @@ and fmt_layer_qual
fmt_layer ff s;
if s <> LAYER_value then fmt ff " ";
-and fmt_opacity
- (ff:Format.formatter)
- (opa:opacity)
- : unit =
- match opa with
- OPA_transparent -> ()
- | OPA_abstract -> fmt ff "abs"
-
-and fmt_opacity_qual
- (ff:Format.formatter)
- (op:opacity)
- : unit =
- fmt_opacity ff op;
- if op <> OPA_transparent then fmt ff " ";
-
-
and fmt_ty_fn
(ff:Format.formatter)
(ident_and_params:(ident * ty_param array) option)
diff --git a/src/boot/fe/item.ml b/src/boot/fe/item.ml
index df300b19..6b232e7e 100644
--- a/src/boot/fe/item.ml
+++ b/src/boot/fe/item.ml
@@ -609,8 +609,7 @@ and parse_stmts_including_none (ps:pstate) : Ast.stmt array =
spans ps stmts apos (Ast.STMT_join lval)
- | STATE | GC
- | ABS | NATIVE
+ | STATE | GC | NATIVE
| MOD | OBJ | TAG | TYPE | FN | USE ->
let items = ctxt "stmt: decl" parse_mod_item ps in
let bpos = lexpos ps in
@@ -695,7 +694,6 @@ and parse_stmts_including_none (ps:pstate) : Ast.stmt array =
and parse_ty_param (iref:int ref) (ps:pstate) : Ast.ty_param identified =
let apos = lexpos ps in
- let _ = Pexp.parse_opacity ps in
let s = Pexp.parse_layer ps in
let ident = Pexp.parse_ident ps in
let i = !iref in
@@ -990,9 +988,8 @@ and parse_mod_item (ps:pstate)
match peek ps with
- STATE | GC | ABS
+ STATE | GC
| TYPE | OBJ | TAG | FN | ITER ->
- let _ = Pexp.parse_opacity ps in
let layer = Pexp.parse_layer ps in
begin
match peek ps with
diff --git a/src/boot/fe/lexer.mll b/src/boot/fe/lexer.mll
index 5cf73166..b375b874 100644
--- a/src/boot/fe/lexer.mll
+++ b/src/boot/fe/lexer.mll
@@ -95,8 +95,6 @@
("claim", CLAIM);
("prove", PROVE);
- ("abs", ABS);
-
("state", STATE);
("gc", GC);
diff --git a/src/boot/fe/pexp.ml b/src/boot/fe/pexp.ml
index 5310f6df..ed36926d 100644
--- a/src/boot/fe/pexp.ml
+++ b/src/boot/fe/pexp.ml
@@ -140,11 +140,6 @@ and parse_optional_trailing_constrs (ps:pstate) : Ast.constrs =
COLON -> (bump ps; parse_constrs ps)
| _ -> [| |]
-and parse_opacity (ps:pstate) : Ast.opacity =
- match peek ps with
- ABS -> bump ps; Ast.OPA_abstract
- | _ -> Ast.OPA_transparent
-
and parse_layer (ps:pstate) : Ast.layer =
match peek ps with
STATE -> bump ps; Ast.LAYER_state
diff --git a/src/boot/fe/token.ml b/src/boot/fe/token.ml
index 7f4665c2..0b157983 100644
--- a/src/boot/fe/token.ml
+++ b/src/boot/fe/token.ml
@@ -80,9 +80,6 @@ type token =
| CLAIM
| PROVE
- (* Opacity keywords *)
- | ABS
-
(* Layer keywords *)
| STATE
| GC
@@ -243,9 +240,6 @@ let rec string_of_tok t =
| CLAIM -> "claim"
| PROVE -> "prove"
- (* Opacity keywords *)
- | ABS -> "abs"
-
(* Layer keywords *)
| STATE -> "state"
| GC -> "gc"
diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs
index 7ec5e20a..882b70a4 100644
--- a/src/comp/front/ast.rs
+++ b/src/comp/front/ast.rs
@@ -119,11 +119,6 @@ tag mutability {
maybe_mut;
}
-tag opacity {
- op_abstract;
- op_transparent;
-}
-
tag layer {
layer_value;
layer_state;
diff --git a/src/comp/front/lexer.rs b/src/comp/front/lexer.rs
index 3a9eb1ed..3659af1c 100644
--- a/src/comp/front/lexer.rs
+++ b/src/comp/front/lexer.rs
@@ -130,8 +130,6 @@ fn keyword_table() -> std.map.hashmap[str, token.token] {
keywords.insert("claim", token.CLAIM);
keywords.insert("prove", token.PROVE);
- keywords.insert("abs", token.ABS);
-
keywords.insert("state", token.STATE);
keywords.insert("gc", token.GC);
diff --git a/src/comp/front/parser.rs b/src/comp/front/parser.rs
index 3ed74abc..30d0ffbc 100644
--- a/src/comp/front/parser.rs
+++ b/src/comp/front/parser.rs
@@ -1951,7 +1951,6 @@ fn parse_item_native_fn(parser p) -> @ast.native_item {
}
fn parse_native_item(parser p) -> @ast.native_item {
- let ast.opacity opa = parse_opacity(p);
let ast.layer lyr = parse_layer(p);
alt (p.peek()) {
case (token.TYPE) {
@@ -2106,18 +2105,6 @@ fn parse_item_tag(parser p) -> @ast.item {
ret @spanned(lo, hi, item);
}
-fn parse_opacity(parser p) -> ast.opacity {
- alt (p.peek()) {
- case (token.ABS) {
- p.bump();
- ret ast.op_abstract;
- }
- case (_) {
- ret ast.op_transparent;
- }
- }
- fail;
-}
fn parse_layer(parser p) -> ast.layer {
alt (p.peek()) {
@@ -2167,7 +2154,6 @@ fn peeking_at_item(parser p) -> bool {
}
fn parse_item(parser p) -> @ast.item {
- let ast.opacity opa = parse_opacity(p);
let ast.layer lyr = parse_layer(p);
alt (p.peek()) {
diff --git a/src/comp/front/token.rs b/src/comp/front/token.rs
index cdc6b503..f367bcc6 100644
--- a/src/comp/front/token.rs
+++ b/src/comp/front/token.rs
@@ -93,9 +93,6 @@ tag token {
CLAIM;
PROVE;
- /* Opacity keywords */
- ABS;
-
/* Layer keywords */
STATE;
GC;
@@ -265,9 +262,6 @@ fn to_str(token t) -> str {
case (CLAIM) { ret "claim"; }
case (PROVE) { ret "prove"; }
- /* Opacity keywords */
- case (ABS) { ret "abs"; }
-
/* Layer keywords */
case (STATE) { ret "state"; }
case (GC) { ret "gc"; }
diff --git a/src/lib/map.rs b/src/lib/map.rs
index 91d0a56a..2c530f5b 100644
--- a/src/lib/map.rs
+++ b/src/lib/map.rs
@@ -6,7 +6,7 @@
type hashfn[K] = fn(&K) -> uint;
type eqfn[K] = fn(&K, &K) -> bool;
-abs state type hashmap[K, V] = state obj {
+state type hashmap[K, V] = state obj {
fn size() -> uint;
fn insert(&K key, &V val) -> bool;
fn contains_key(&K key) -> bool;
@@ -241,5 +241,5 @@ fn mk_hashmap[K, V](&hashfn[K] hasher, &eqfn[K] eqer) -> hashmap[K, V] {
// indent-tabs-mode: nil
// c-basic-offset: 4
// buffer-file-coding-system: utf-8-unix
-// compile-command: "make -k -C .. 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
+// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
// End:
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 10:06:49 +0000