summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/initial_check.ml4
-rw-r--r--src/parser.mly44
-rw-r--r--src/pre_lexer.mll2
-rw-r--r--src/pre_parser.mly14
-rw-r--r--src/test/run_tests.ml2
-rw-r--r--src/test/test1.sail4
-rw-r--r--src/type_check.ml2
7 files changed, 36 insertions, 36 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 7a4cc413..29bedd12 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -90,7 +90,7 @@ let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ =
| K_Typ -> Typ_id id
| K_infer -> k.k <- K_Typ; Typ_id id
| _ -> typ_error l "Required an identifier with kind Type, encountered " (Some id) None (Some k))
- | None -> typ_error l "Encountered an unbound identifier" (Some id) None None)
+ | None -> typ_error l "Encountered an unbound type identifier" (Some id) None None)
| Parse_ast.ATyp_var(v) ->
let v = to_ast_var v in
let mk = Envmap.apply k_env (var_to_string v) in
@@ -621,7 +621,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
let typq, k_env',_ = to_ast_typquant k_env typquant in
(match (def_in_progress id partial_defs) with
| None -> let partial_def = ref ((DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,None))),(l,None))),false) in
- (Def_place_holder(id,l),envs),(id,(partial_def,k_env'))::partial_defs
+ (Def_place_holder(id,l),(names,Envmap.insert k_env ((id_to_string id),{k=K_Typ}),t_env)),(id,(partial_def,k_env'))::partial_defs
| Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None)
| Parse_ast.SD_scattered_unioncl(id,tu) ->
let id = to_ast_id id in
diff --git a/src/parser.mly b/src/parser.mly
index 5779b3b4..bf77ffaf 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1000,36 +1000,36 @@ r_def_body:
{ $1::$3 }
type_def:
- | Typedef id name_sect Eq typquant typ
+ | Typedef tid name_sect Eq typquant typ
{ tdloc (TD_abbrev($2,$3,mk_typschm $5 $6 5 6)) }
- | Typedef id name_sect Eq typ
+ | Typedef tid name_sect Eq typ
{ tdloc (TD_abbrev($2,$3,mk_typschm (mk_typqn ()) $5 5 5)) }
- | Typedef id Eq typquant typ
+ | Typedef tid Eq typquant typ
{ tdloc (TD_abbrev($2,mk_namesectn (), mk_typschm $4 $5 4 5))}
- | Typedef id Eq typ
+ | Typedef tid Eq typ
{ tdloc (TD_abbrev($2,mk_namesectn (),mk_typschm (mk_typqn ()) $4 4 4)) }
/* The below adds 4 shift/reduce conflicts. Due to c_def_body and confusions in id id and parens */
- | Typedef id name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly
+ | Typedef tid name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly
{ tdloc (TD_record($2,$3,$7,fst $9, snd $9)) }
- | Typedef id name_sect Eq Const Struct Lcurly c_def_body Rcurly
+ | Typedef tid name_sect Eq Const Struct Lcurly c_def_body Rcurly
{ tdloc (TD_record($2,$3,(mk_typqn ()), fst $8, snd $8)) }
- | Typedef id Eq Const Struct typquant Lcurly c_def_body Rcurly
+ | Typedef tid Eq Const Struct typquant Lcurly c_def_body Rcurly
{ tdloc (TD_record($2,mk_namesectn (), $6, fst $8, snd $8)) }
- | Typedef id Eq Const Struct Lcurly c_def_body Rcurly
+ | Typedef tid Eq Const Struct Lcurly c_def_body Rcurly
{ tdloc (TD_record($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) }
- | Typedef id name_sect Eq Const Union typquant Lcurly union_body Rcurly
+ | Typedef tid name_sect Eq Const Union typquant Lcurly union_body Rcurly
{ tdloc (TD_variant($2,$3, $7, fst $9, snd $9)) }
- | Typedef id Eq Const Union typquant Lcurly union_body Rcurly
+ | Typedef tid Eq Const Union typquant Lcurly union_body Rcurly
{ tdloc (TD_variant($2,mk_namesectn (), $6, fst $8, snd $8)) }
- | Typedef id name_sect Eq Const Union Lcurly union_body Rcurly
+ | Typedef tid name_sect Eq Const Union Lcurly union_body Rcurly
{ tdloc (TD_variant($2, $3, mk_typqn (), fst $8, snd $8)) }
- | Typedef id Eq Const Union Lcurly union_body Rcurly
+ | Typedef tid Eq Const Union Lcurly union_body Rcurly
{ tdloc (TD_variant($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) }
- | Typedef id Eq Enumerate Lcurly enum_body Rcurly
+ | Typedef tid Eq Enumerate Lcurly enum_body Rcurly
{ tdloc (TD_enum($2, mk_namesectn (), $6,false)) }
- | Typedef id name_sect Eq Enumerate Lcurly enum_body Rcurly
+ | Typedef tid name_sect Eq Enumerate Lcurly enum_body Rcurly
{ tdloc (TD_enum($2,$3,$7,false)) }
- | Typedef id Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly
+ | Typedef tid Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly
{ tdloc (TD_register($2, $7, $9, $12)) }
@@ -1066,13 +1066,13 @@ scattered_def:
{ sdloc (SD_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
| Function_ id
{ sdloc (SD_scattered_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
- | Typedef id name_sect Eq Const Union typquant
+ | Typedef tid name_sect Eq Const Union typquant
{ sdloc (SD_scattered_variant($2,$3,$7)) }
- | Typedef id Eq Const Union typquant
+ | Typedef tid Eq Const Union typquant
{ sdloc (SD_scattered_variant($2,(mk_namesectn ()),$6)) }
- | Typedef id name_sect Eq Const Union
+ | Typedef tid name_sect Eq Const Union
{ sdloc (SD_scattered_variant($2,$3,mk_typqn ())) }
- | Typedef id Eq Const Union
+ | Typedef tid Eq Const Union
{ sdloc (SD_scattered_variant($2,mk_namesectn (),mk_typqn ())) }
def:
@@ -1092,12 +1092,14 @@ def:
{ dloc (DEF_scattered $2) }
| Function_ Clause funcl
{ dloc (DEF_scattered (sdloc (SD_scattered_funcl($3)))) }
- | Union id Member typ id
+ | Union tid Member typ id
{ dloc (DEF_scattered (sdloc (SD_scattered_unioncl($2,Tu_aux(Tu_ty_id($4,$5), locn 4 5))))) }
- | Union id Member id
+ | Union tid Member id
{ dloc (DEF_scattered (sdloc (SD_scattered_unioncl($2,Tu_aux(Tu_id($4), locn 4 4))))) }
| End id
{ dloc (DEF_scattered (sdloc (SD_scattered_end($2)))) }
+ | End tid
+ { dloc (DEF_scattered (sdloc (SD_scattered_end($2)))) }
defs_help:
| def
diff --git a/src/pre_lexer.mll b/src/pre_lexer.mll
index ae336f0f..5f55cc72 100644
--- a/src/pre_lexer.mll
+++ b/src/pre_lexer.mll
@@ -95,7 +95,7 @@ let kw_table =
("then", (fun x -> Other));
("true", (fun x -> Other));
("Type", (fun x -> Other));
- ("typedef", (fun x -> Other));
+ ("typedef", (fun x -> Typedef));
("undefined", (fun x -> Other));
("union", (fun x -> Other));
("with", (fun x -> Other));
diff --git a/src/pre_parser.mly b/src/pre_parser.mly
index e9c38ebd..9aceb371 100644
--- a/src/pre_parser.mly
+++ b/src/pre_parser.mly
@@ -60,26 +60,22 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *)
%%
-id:
- | Id
- { $1 }
-
id_found:
- | Typedef id
+ | Typedef Id
{ $2 }
skip:
| Scattered
{ () }
- | id
+ | Id
{ () }
| Other
{ () }
scan_file:
- | id_found
+ | id_found Eof
{ [$1] }
- | skip
+ | skip Eof
{ [] }
| id_found scan_file
{ $1::$2 }
@@ -87,6 +83,6 @@ scan_file:
{ $2 }
file:
- | scan_file Eof
+ | scan_file
{ $1 }
diff --git a/src/test/run_tests.ml b/src/test/run_tests.ml
index ddad139a..3720e5e2 100644
--- a/src/test/run_tests.ml
+++ b/src/test/run_tests.ml
@@ -4,7 +4,7 @@ let tests = [
"test3", Test3.defs;
"pattern", Pattern.defs;
"vectors", Vectors.defs;
- "power", Power.defs;
+(* "power", Power.defs;*)
] ;;
let run_all () = List.iter Run_interp.run tests ;;
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 0cb592d8..d75206fd 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -14,8 +14,8 @@ let bit v = bitzero
let ( bit [ 32 ] ) v1 = 0b101
(* scattered function definition and union definition *)
-scattered function unit f
scattered typedef ast = const union
+scattered function unit f
union ast member bit * bit * bit A
function clause f ( A (a,b,c) ) = ()
@@ -26,8 +26,8 @@ function clause f ( B (a,b) ) = ()
union ast member bit C
function clause f ( C (a) ) = ()
-end f
end ast
+end f
function bit sw s = switch s { case 0 -> bitzero }
diff --git a/src/type_check.ml b/src/type_check.ml
index d8bdec28..45ac1382 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -405,7 +405,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
let t',cs = type_consistent l d_env t expect_t in
let (e',u,t_env,cs') = check_exp envs t' e in
(e',t',t_env,cs@cs')
+
| E_app(id,parms) ->
+ (*TODO add a tuple arg to store the function effects in, for eventual checking*)
let i = id_to_string id in
(match Envmap.apply t_env i with
| Some(Some(tp,Enum,cs)) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 16:29:48 +0000