diff options
| author | Alasdair Armstrong | 2017-10-06 17:56:30 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-10-06 17:56:30 +0100 |
| commit | d3604c52e19e4e71965b5d96d6fab879bac7effc (patch) | |
| tree | ef79450d7038ae70072d8fb155442a778cfdc14d /src | |
| parent | 6e4573f9a1ace7cba38d0cecb95b4dfe95c73c71 (diff) | |
Remove BK_effect constructor
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast.ml | 1 | ||||
| -rw-r--r-- | src/ast_util.ml | 1 | ||||
| -rw-r--r-- | src/initial_check.ml | 1 | ||||
| -rw-r--r-- | src/parse_ast.ml | 1 | ||||
| -rw-r--r-- | src/parser.mly | 2 | ||||
| -rw-r--r-- | src/pretty_print_lem_ast.ml | 3 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 3 |
7 files changed, 2 insertions, 10 deletions
@@ -57,7 +57,6 @@ base_kind_aux = (* base kind *) BK_type (* kind of types *) | BK_nat (* kind of natural number size expressions *) | BK_order (* kind of vector order specifications *) - | BK_effect (* kind of effect sets *) type diff --git a/src/ast_util.ml b/src/ast_util.ml index ecff4ff4..2db41ce6 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -340,7 +340,6 @@ let string_of_base_kind_aux = function | BK_type -> "Type" | BK_nat -> "Nat" | BK_order -> "Order" - | BK_effect -> "Effect" let string_of_base_kind (BK_aux (bk, _)) = string_of_base_kind_aux bk diff --git a/src/initial_check.ml b/src/initial_check.ml index efda0da1..36b6478e 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -128,7 +128,6 @@ let to_ast_base_kind (Parse_ast.BK_aux(k,l')) = | Parse_ast.BK_type -> BK_aux(BK_type,l'), { k = K_Typ} | Parse_ast.BK_nat -> BK_aux(BK_nat,l'), { k = K_Nat } | Parse_ast.BK_order -> BK_aux(BK_order,l'), { k = K_Ord } - | Parse_ast.BK_effect -> BK_aux(BK_effect,l'), { k = K_Efct } let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst),l)) : (Ast.kind * kind) = match klst with diff --git a/src/parse_ast.ml b/src/parse_ast.ml index f38c2d3d..9532b858 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -64,7 +64,6 @@ base_kind_aux = (* base kind *) BK_type (* kind of types *) | BK_nat (* kind of natural number size expressions *) | BK_order (* kind of vector order specifications *) - | BK_effect (* kind of effect sets *) type diff --git a/src/parser.mly b/src/parser.mly index a415801e..df4a273d 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -309,8 +309,6 @@ atomic_kind: { bkloc BK_nat } | Order { bkloc BK_order } - | EFFECT - { bkloc BK_effect } kind_help: | atomic_kind diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index 2c9cf83c..2e464a08 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -133,8 +133,7 @@ let pp_format_bkind_lem (BK_aux(k,l)) = (match k with | BK_type -> "BK_type" | BK_nat -> "BK_nat" - | BK_order -> "BK_order" - | BK_effect -> "BK_effect") ^ " " ^ + | BK_order -> "BK_order") ^ " " ^ (pp_format_l_lem l) ^ ")" let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk) diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index ce887f72..99263bc7 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -53,8 +53,7 @@ let doc_bkind (BK_aux(k,_)) = string (match k with | BK_type -> "Type" | BK_nat -> "Nat" - | BK_order -> "Order" - | BK_effect -> "Effect") + | BK_order -> "Order") let doc_kind (K_aux(K_kind(klst),_)) = separate_map (spaces arrow) doc_bkind klst |