summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/initial_check.ml14
-rw-r--r--src/lem_interp/interp.lem6
-rw-r--r--src/lexer.mll247
-rw-r--r--src/parser.mly236
-rw-r--r--src/pre_lexer.mll319
-rw-r--r--src/pre_parser.mly86
-rw-r--r--src/pretty_print.ml18
-rw-r--r--src/type_check.mli9
-rw-r--r--src/type_internal.ml8
-rw-r--r--src/type_internal.mli8
10 files changed, 643 insertions, 308 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4d16fef4..772df3e9 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -323,7 +323,7 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
| Parse_ast.E_id(id) -> E_id(to_ast_id id)
| Parse_ast.E_lit(lit) -> E_lit(to_ast_lit lit)
| Parse_ast.E_cast(typ,exp) -> E_cast(to_ast_typ k_env typ, to_ast_exp k_env exp)
- | Parse_ast.E_app(f,args) -> E_app(to_ast_exp k_env f, List.map (to_ast_exp k_env) args)
+ | Parse_ast.E_app(f,args) -> E_app(to_ast_id f, List.map (to_ast_exp k_env) args)
| Parse_ast.E_app_infix(left,op,right) -> E_app_infix(to_ast_exp k_env left, to_ast_id op, to_ast_exp k_env right)
| Parse_ast.E_tuple(exps) -> E_tuple(List.map (to_ast_exp k_env) exps)
| Parse_ast.E_if(e1,e2,e3) -> E_if(to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3)
@@ -351,9 +351,9 @@ and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
LEXP_aux(
(match exp with
| Parse_ast.E_id(id) -> LEXP_id(to_ast_id id)
- | Parse_ast.E_app(Parse_ast.E_aux(f,l'),[exp]) ->
+ | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),[exp]) ->
(match f with
- | Parse_ast.E_id(id) -> LEXP_memory(to_ast_id id,to_ast_exp k_env exp)
+ | Parse_ast.Id(id) -> LEXP_memory(to_ast_id f',to_ast_exp k_env exp)
| _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None)
| Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env vexp, to_ast_exp k_env exp)
| Parse_ast.E_vector_subrange(vexp,exp1,exp2) -> LEXP_vector_range(to_ast_lexp k_env vexp, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
@@ -466,7 +466,11 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de
let id = to_ast_id id in
let key = id_to_string id in
let typq,k_env,_ = to_ast_typquant k_env typq in
- let arms = List.map (fun (atyp,id) -> (to_ast_typ k_env atyp),(to_ast_id id)) arms in (* Add check that all arms have unique names *)
+ let arms = List.map (fun (Parse_ast.Tu_aux(tu,l)) ->
+ match tu with
+ | Parse_ast.Tu_ty_id(atyp,id) -> (Tu_aux(Tu_ty_id ((to_ast_typ k_env atyp),(to_ast_id id)),l))
+ | Parse_ast.Tu_id id -> (Tu_aux(Tu_id(to_ast_id id),l)) )
+ arms in (* Add check that all arms have unique names *)
let td_var = TD_aux(TD_variant(id,to_ast_namescm name_scm_opt,typq,arms,false),(l,None)) in
let typ = (match (typquant_to_quantkinds k_env typq) with
| [ ] -> {k = K_Typ}
@@ -595,7 +599,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
(match !d with
| (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)),dl), false) ->
let typ = to_ast_typ k typ in
- d:= (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms@[typ,arm_id],false),tl)),dl),false);
+ d:= (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms@[Tu_aux(Tu_ty_id (typ,arm_id), l)],false),tl)),dl),false);
(No_def,envs),partial_defs
| _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None
| _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None))
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 2e8af9d3..640f6b1d 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -130,7 +130,7 @@ let rec to_data_constructors (Defs defs) =
| DEF_type t ->
match t with
| TD_variant id _ tq tid_list _ ->
- (List.map (fun (x,y) -> (y,x)) tid_list)++(to_data_constructors (Defs defs))
+ (List.map (fun (Tu_ty_id x y) -> (y,x)) tid_list)++(to_data_constructors (Defs defs))
| _ -> to_data_constructors (Defs defs) end
| _ -> to_data_constructors (Defs defs) end
end
@@ -268,7 +268,7 @@ let rec to_exp v =
E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(List.length vals),[]) vals))
| V_record(ivals) -> E_record(FES_Fexps (List.map (fun (id,value) -> (FE_Fexp id (to_exp value))) ivals) false)
| V_list(vals) -> E_list (List.map to_exp vals)
- | V_ctor id vals -> E_app (E_id id) [to_exp vals]
+ | V_ctor id vals -> E_app id [to_exp vals]
end
val find_type_def : defs -> id -> maybe type_def
@@ -634,7 +634,7 @@ and interp_main t_level l_env l_mem exp =
| E_block(exps) -> interp_block t_level l_env l_env l_mem exps
| E_app f args ->
match (f,t_level) with
- | (E_id(id),(defs,externs,regs,mems,ctors)) ->
+ | (id,(defs,externs,regs,mems,ctors)) ->
(match find_function defs id with
| Just(funcls) ->
resolve_outcome (interp_main t_level l_env l_mem (List_extra.head args))
diff --git a/src/lexer.mll b/src/lexer.mll
index 3843a50b..b9336e2d 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -45,7 +45,7 @@
(**************************************************************************)
{
-open Parser
+open Pre_parser
module M = Map.Make(String)
exception LexError of string * Lexing.position
@@ -58,64 +58,69 @@ let kw_table =
(fun r (x,y) -> M.add x y r)
M.empty
[
- ("and", (fun _ -> And));
- ("as", (fun _ -> As));
- ("bits", (fun _ -> Bits));
- ("by", (fun _ -> By));
- ("case", (fun _ -> Case));
- ("clause", (fun _ -> Clause));
- ("const", (fun _ -> Const));
- ("default", (fun _ -> Default));
- ("effect", (fun _ -> Effect));
- ("Effects", (fun _ -> Effects));
- ("end", (fun _ -> End));
- ("enumerate", (fun _ -> Enumerate));
- ("else", (fun _ -> Else));
- ("extern", (fun _ -> Extern));
- ("false", (fun _ -> False));
- ("forall", (fun _ -> Forall));
- ("foreach", (fun _ -> Foreach));
- ("function", (fun x -> Function_));
- ("if", (fun x -> If_));
- ("in", (fun x -> In));
- ("IN", (fun x -> IN));
- ("let", (fun x -> Let_));
- ("member", (fun x -> Member));
- ("Nat", (fun x -> Nat));
- ("Order", (fun x -> Order));
- ("pure", (fun x -> Pure));
- ("rec", (fun x -> Rec));
- ("register", (fun x -> Register));
+ ("and", (fun _ -> Other));
+ ("as", (fun _ -> Other));
+ ("bits", (fun _ -> Other));
+ ("by", (fun _ -> Other));
+ ("case", (fun _ -> Other));
+ ("clause", (fun _ -> Other));
+ ("const", (fun _ -> Other));
+ ("dec", (fun _ -> Other));
+ ("default", (fun _ -> Other));
+ ("deinfix", (fun _ -> Other));
+ ("effect", (fun _ -> Other));
+ ("Effects", (fun _ -> Other));
+ ("end", (fun _ -> Other));
+ ("enumerate", (fun _ -> Other));
+ ("else", (fun _ -> Other));
+ ("extern", (fun _ -> Other));
+ ("false", (fun _ -> Other));
+ ("forall", (fun _ -> Other));
+ ("foreach", (fun _ -> Other));
+ ("function", (fun x -> Other));
+ ("if", (fun x -> Other));
+ ("in", (fun x -> Other));
+ ("IN", (fun x -> Other));
+ ("Inc", (fun x -> Other));
+ ("let", (fun x -> Other));
+ ("member", (fun x -> Other));
+ ("Nat", (fun x -> Other));
+ ("Order", (fun x -> Other));
+ ("pure", (fun x -> Other));
+ ("rec", (fun x -> Other));
+ ("register", (fun x -> Other));
("scattered", (fun x -> Scattered));
- ("struct", (fun x -> Struct));
- ("switch", (fun x -> Switch));
- ("then", (fun x -> Then));
- ("true", (fun x -> True));
- ("Type", (fun x -> TYPE));
+ ("struct", (fun x -> Other));
+ ("switch", (fun x -> Other));
+ ("then", (fun x -> Other));
+ ("true", (fun x -> Other));
+ ("Type", (fun x -> Other));
("typedef", (fun x -> Typedef));
- ("undefined", (fun x -> Undefined));
- ("union", (fun x -> Union));
- ("with", (fun x -> With));
- ("val", (fun x -> Val));
-
- ("AND", (fun x -> AND));
- ("div", (fun x -> Div_));
- ("EOR", (fun x -> EOR));
- ("mod", (fun x -> Mod));
- ("OR", (fun x -> OR));
- ("quot", (fun x -> Quot));
- ("rem", (fun x -> Rem));
+ ("undefined", (fun x -> Other));
+ ("union", (fun x -> Other));
+ ("with", (fun x -> Other));
+ ("val", (fun x -> Other));
+
+ ("AND", (fun x -> Other));
+ ("div", (fun x -> Other));
+ ("EOR", (fun x -> Other));
+ ("mod", (fun x -> Other));
+ ("OR", (fun x -> Other));
+ ("quot", (fun x -> Other));
+ ("rem", (fun x -> Other));
]
}
let ws = [' ''\t']+
+let lowerletter = ['a'-'z']
+let upperletter = ['A'-'Z']
let letter = ['a'-'z''A'-'Z']
let digit = ['0'-'9']
let binarydigit = ['0'-'1']
let hexdigit = ['0'-'9''A'-'F''a'-'f']
let alphanum = letter|digit
-let startident = letter|'_'
+let startident = lowerletter|'_'
let ident = alphanum|['_''\'']
let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|''~']
let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
@@ -127,84 +132,6 @@ rule token = parse
{ Lexing.new_line lexbuf;
token lexbuf }
- | "&" { (Amp(r"&")) }
- | "@" { (At(r"@")) }
- | "|" { Bar }
- | "^" { (Carrot(r"^")) }
- | ":" { Colon }
- | "," { Comma }
- | "." { Dot }
- | "/" { (Div(r "/")) }
- | "=" { (Eq(r"=")) }
- | "!" { (Excl(r"!")) }
- | ">" { (Gt(r">")) }
- | "-" { Minus }
- | "<" { (Lt(r"<")) }
- | "+" { (Plus(r"+")) }
- | ";" { Semi }
- | "*" { (Star(r"*")) }
- | "~" { (Tilde(r"~")) }
- | "_" { Under }
- | "{" { Lcurly }
- | "}" { Rcurly }
- | "(" { Lparen }
- | "(:" { LparenColon }
- | ")" { Rparen }
- | "[" { Lsquare }
- | "]" { Rsquare }
- | "&&" as i { (AmpAmp(r i)) }
- | "||" { BarBar }
- | "|>" { BarGt }
- | "|]" { BarSquare }
- | "^^" { (CarrotCarrot(r"^^")) }
- | "::" as i { (ColonColon(r i)) }
- | ":=" { ColonEq }
- | ".." { DotDot }
- | "=/=" { (EqDivEq(r"=/=")) }
- | "==" { (EqEq(r"==")) }
- | "!=" { (ExclEq(r"!=")) }
- | "!!" { (ExclExcl(r"!!")) }
- | ">=" { (GtEq(r">=")) }
- | ">=+" { (GtEqPlus(r">=+")) }
- | ">>" { (GtGt(r">>")) }
- | ">>>" { (GtGtGt(r">>>")) }
- | ">+" { (GtPlus(r">+")) }
- | "#>>" { (HashGtGt(r"#>>")) }
- | "#<<" { (HashLtLt(r"#<<")) }
- | "->" { MinusGt }
- | "<=" { (LtEq(r"<=")) }
- | "<=+" { (LtEqPlus(r"<=+")) }
- | "<>" { (LtGt(r"<>")) }
- | "<<" { (LtLt(r"<<")) }
- | "<<<" { (LtLtLt(r"<<<")) }
- | "<+" { (LtPlus(r"<+")) }
- | "**" { (StarStar(r"**")) }
- | "~^" { (TildeCarrot(r"~^")) }
-
- | ">=_s" { (GtEqUnderS(r">=_s")) }
- | ">=_si" { (GtEqUnderSi(r">=_si")) }
- | ">=_u" { (GtEqUnderU(r">=_u")) }
- | ">=_ui" { (GtEqUnderUi(r">=_ui")) }
- | ">>_u" { (GtGtUnderU(r">>_u")) }
- | ">_s" { (GtUnderS(r">_s")) }
- | ">_si" { (GtUnderSi(r">_si")) }
- | ">_u" { (GtUnderU(r">_u")) }
- | ">_ui" { (GtUnderUi(r">_ui")) }
- | "<=_s" { (LtEqUnderS(r"<=_s")) }
- | "<=_si" { (LtEqUnderSi(r"<=_si")) }
- | "<=_u" { (LtEqUnderU(r"<=_u")) }
- | "<=_ui" { (LtEqUnderUi(r"<=_ui")) }
- | "<_s" { (LtUnderS(r"<_s")) }
- | "<_si" { (LtUnderSi(r"<_si")) }
- | "<_u" { (LtUnderU(r"<_u")) }
- | "<_ui" { (LtUnderUi(r"<_ui")) }
- | "**_s" { (StarStarUnderS(r"**_s")) }
- | "**_si" { (StarStarUnderSi(r"**_si")) }
- | "*_u" { (StarUnderU(r"*_u")) }
- | "*_ui" { (StarUnderUi(r"*_ui")) }
- | "2^" { (TwoCarrot(r"2^")) }
-
-
| "(*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
| "*)" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
@@ -212,71 +139,13 @@ rule token = parse
(M.find i kw_table) ()
else
Id(r i) }
- | "&" oper_char+ as i { (AmpI(r i)) }
- | "@" oper_char+ as i { (AtI(r i)) }
- | "^" oper_char+ as i { (CarrotI(r i)) }
- | "/" oper_char+ as i { (DivI(r i)) }
- | "=" oper_char+ as i { (EqI(r i)) }
- | "!" oper_char+ as i { (ExclI(r i)) }
- | ">" oper_char+ as i { (GtI(r i)) }
- | "<" oper_char+ as i { (LtI(r i)) }
- | "+" oper_char+ as i { (PlusI(r i)) }
- | "*" oper_char+ as i { (StarI(r i)) }
- | "~" oper_char+ as i { (TildeI(r i)) }
- | "&&" oper_char+ as i { (AmpAmpI(r i)) }
- | "^^" oper_char+ as i { (CarrotCarrotI(r i)) }
- | "::" oper_char+ as i { (ColonColonI(r i)) }
- | "=/=" oper_char+ as i { (EqDivEqI(r i)) }
- | "==" oper_char+ as i { (EqEqI(r i)) }
- | "!=" oper_char+ as i { (ExclEqI(r i)) }
- | "!!" oper_char+ as i { (ExclExclI(r i)) }
- | ">=" oper_char+ as i { (GtEqI(r i)) }
- | ">=+" oper_char+ as i { (GtEqPlusI(r i)) }
- | ">>" oper_char+ as i { (GtGtI(r i)) }
- | ">>>" oper_char+ as i { (GtGtGtI(r i)) }
- | ">+" oper_char+ as i { (GtPlusI(r i)) }
- | "#>>" oper_char+ as i { (HashGtGt(r i)) }
- | "#<<" oper_char+ as i { (HashLtLt(r i)) }
- | "<=" oper_char+ as i { (LtEqI(r i)) }
- | "<=+" oper_char+ as i { (LtEqPlusI(r i)) }
- | "<<" oper_char+ as i { (LtLtI(r i)) }
- | "<<<" oper_char+ as i { (LtLtLtI(r i)) }
- | "<+" oper_char+ as i { (LtPlusI(r i)) }
- | "**" oper_char+ as i { (StarStarI(r i)) }
- | "~^" oper_char+ as i { (TildeCarrot(r i)) }
-
- | ">=_s" oper_char+ as i { (GtEqUnderSI(r i)) }
- | ">=_si" oper_char+ as i { (GtEqUnderSiI(r i)) }
- | ">=_u" oper_char+ as i { (GtEqUnderUI(r i)) }
- | ">=_ui" oper_char+ as i { (GtEqUnderUiI(r i)) }
- | ">>_u" oper_char+ as i { (GtGtUnderUI(r i)) }
- | ">_s" oper_char+ as i { (GtUnderSI(r i)) }
- | ">_si" oper_char+ as i { (GtUnderSiI(r i)) }
- | ">_u" oper_char+ as i { (GtUnderUI(r i)) }
- | ">_ui" oper_char+ as i { (GtUnderUiI(r i)) }
- | "<=_s" oper_char+ as i { (LtEqUnderSI(r i)) }
- | "<=_si" oper_char+ as i { (LtEqUnderSiI(r i)) }
- | "<=_u" oper_char+ as i { (LtEqUnderUI(r i)) }
- | "<=_ui" oper_char+ as i { (LtEqUnderUiI(r i)) }
- | "<_s" oper_char+ as i { (LtUnderSI(r i)) }
- | "<_si" oper_char+ as i { (LtUnderSiI(r i)) }
- | "<_u" oper_char+ as i { (LtUnderUI(r i)) }
- | "<_ui" oper_char+ as i { (LtUnderUiI(r i)) }
- | "**_s" oper_char+ as i { (StarStarUnderSI(r i)) }
- | "**_si" oper_char+ as i { (StarStarUnderSiI(r i)) }
- | "*_u" oper_char+ as i { (StarUnderUI(r i)) }
- | "*_ui" oper_char+ as i { (StarUnderUiI(r i)) }
- | "2^" oper_char+ as i { (TwoCarrotI(r i)) }
-
- | digit+ as i { (Num(int_of_string i)) }
- | "0b" (binarydigit+ as i) { (Bin(i)) }
- | "0x" (hexdigit+ as i) { (Hex(i)) }
- | '"' { (String(
- string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) }
+ | oper_char+ { Other }
+ | digit+ as i { Other }
+ | '"' { let s =
+ string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf) in
+ Other }
| eof { Eof }
- | _ as c { raise (LexError(
- Printf.sprintf "Unexpected character: %c" c,
- Lexing.lexeme_start_p lexbuf)) }
+ | _ as c { Other }
and comment pos depth = parse
diff --git a/src/parser.mly b/src/parser.mly
index 2ff88944..c5f82508 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -120,9 +120,9 @@ let star = "*"
/*Terminals with no content*/
-%token And As Bits By Case Clause Const Default Dec Effect Effects End Enumerate Else Extern
+%token And As Bits By Case Clause Const Dec Default Deinfix Effect Effects End Enumerate Else Extern
%token False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order Pure Rec Register
-%token Scattered Struct Switch Then True Type TYPE Typedef Undefined Union With Val
+%token Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef Undefined Union With Val
/* Avoid shift/reduce conflict - see right_atomic_exp rule */
%nonassoc Then
@@ -132,11 +132,11 @@ let star = "*"
%token Bar Colon Comma Dot Eof Minus Semi Under
%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare
-%token BarBar BarGt BarSquare DotDot ColonEq ColonGt MinusGt LtBar LparenColon SquareBar
+%token BarBar BarSquare BarBarSquare ColonEq DotDot ColonGt MinusGt LtBar SquareBar SquareBarBar
/*Terminals with content*/
-%token <string> Id TickId
+%token <string> Id TickId TyId
%token <int> Num
%token <string> String Bin Hex
@@ -175,70 +175,74 @@ id:
{ idl (Id($1)) }
| Tilde
{ idl (Id($1)) }
- | LparenColon Amp Rparen
- { idl (DeIid($2)) }
- | LparenColon At Rparen
- { idl (DeIid($2)) }
- | LparenColon Carrot Rparen
- { idl (DeIid($2)) }
- | LparenColon Div Rparen
- { idl (DeIid($2)) }
- | LparenColon Eq Rparen
- { Id_aux(DeIid($2),loc ()) }
- | LparenColon Excl Lparen
- { idl (DeIid($2)) }
- | LparenColon Gt Lparen
- { idl (DeIid($2)) }
- | LparenColon Lt Lparen
- { idl (DeIid($2)) }
- | LparenColon Minus Lparen
+ | Lparen Deinfix Amp Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix At Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Carrot Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Div Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Eq Rparen
+ { Id_aux(DeIid($3),loc ()) }
+ | Lparen Deinfix Excl Lparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Gt Lparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Lt Lparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Minus Lparen
{ idl (DeIid("-")) }
- | LparenColon Plus Rparen
- { idl (DeIid($2)) }
- | LparenColon Star Rparen
- { idl (DeIid($2)) }
- | LparenColon AmpAmp Rparen
- { idl (DeIid($2)) }
- | LparenColon BarBar Rparen
+ | Lparen Deinfix Plus Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Star Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix AmpAmp Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix BarBar Rparen
{ idl (DeIid("||")) }
- | LparenColon CarrotCarrot Rparen
- { idl (DeIid($2)) }
- | LparenColon ColonColon Rparen
- { idl (DeIid($2)) }
- | LparenColon EqDivEq Rparen
- { idl (DeIid($2)) }
- | LparenColon EqEq Rparen
- { idl (DeIid($2)) }
- | LparenColon ExclEq Rparen
- { idl (DeIid($2)) }
- | LparenColon ExclExcl Rparen
- { idl (DeIid($2)) }
- | LparenColon GtEq Rparen
- { idl (DeIid($2)) }
- | LparenColon GtEqPlus Rparen
- { idl (DeIid($2)) }
- | LparenColon GtGt Rparen
- { idl (DeIid($2)) }
- | LparenColon GtGtGt Rparen
- { idl (DeIid($2)) }
- | LparenColon GtPlus Rparen
- { idl (DeIid($2)) }
- | LparenColon HashGtGt Rparen
- { idl (DeIid($2)) }
- | LparenColon HashLtLt Rparen
- { idl (DeIid($2)) }
- | LparenColon LtEq Rparen
- { idl (DeIid($2)) }
- | LparenColon LtLt Rparen
- { idl (DeIid($2)) }
- | LparenColon LtLtLt Rparen
- { idl (DeIid($2)) }
- | LparenColon LtPlus Rparen
- { idl (DeIid($2)) }
- | LparenColon StarStar Rparen
- { idl (DeIid($2)) }
- | LparenColon TildeCarrot Rparen
- { idl (DeIid($2)) }
+ | Lparen Deinfix CarrotCarrot Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix ColonColon Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix EqDivEq Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix EqEq Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix ExclEq Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix ExclExcl Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix GtEq Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix GtEqPlus Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix GtGt Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix GtGtGt Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix GtPlus Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix HashGtGt Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix HashLtLt Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix LtEq Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix LtLt Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix LtLtLt Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix LtPlus Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix StarStar Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix TildeCarrot Rparen
+ { idl (DeIid($3)) }
+
+tid:
+ | TyId
+ { (idl (Id($1))) }
atomic_kind:
| TYPE
@@ -283,7 +287,7 @@ effect_list:
{ $1::$3 }
effect_typ:
- | Effect id
+ | Effect tid
{ tloc (ATyp_efid($2)) }
| Effect Lcurly effect_list Rcurly
{ tloc (ATyp_set($3)) }
@@ -291,7 +295,7 @@ effect_typ:
{ tloc (ATyp_set([])) }
atomic_typ:
- | id
+ | tid
{ tloc (ATyp_id $1) }
| effect_typ
{ $1 }
@@ -299,32 +303,36 @@ atomic_typ:
{ tloc (ATyp_inc) }
| Dec
{ tloc (ATyp_dec) }
- | Lparen typ Rparen
- { $2 }
| SquareBar nexp_typ BarSquare
{ tloc (make_enum_sugar $2) }
| SquareBar nexp_typ Colon nexp_typ BarSquare
{ tloc (make_enum_sugar_bounded $2 $4) }
+ | Lparen typ Rparen
+ { $2 }
vec_typ:
| atomic_typ
{ $1 }
- | atomic_typ Lsquare nexp_typ Rsquare
- { tloc (make_vector_sugar $1 $3) }
- | atomic_typ Lsquare nexp_typ Colon nexp_typ Rsquare
- { tloc (make_vector_sugar_bounded $1 $3 $5) }
+ | tid Lsquare nexp_typ Rsquare
+ { tloc (make_vector_sugar (ATyp_aux ((ATyp_id $1), locn 1 1)) $3) }
+ | tid Lsquare nexp_typ Colon nexp_typ Rsquare
+ { tloc (make_vector_sugar_bounded (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
app_typs:
| vec_typ
{ [$1] }
+ | Num
+ { [tloc (ATyp_constant $1)] }
+ | Num app_typs
+ { (ATyp_aux((ATyp_constant $1),locn 1 1))::$2 }
| vec_typ app_typs
{ $1::$2 }
app_typ:
| vec_typ
{ $1 }
- | id app_typs
- { tloc (ATyp_app($1,$2)) }
+ | tid Lt app_typs Gt
+ { tloc (ATyp_app($1,$3)) }
star_typ_list:
| app_typ
@@ -342,23 +350,23 @@ star_typ:
exp_typ:
| star_typ
{ $1 }
- | Num StarStar typ
- { if (2 = $1)
- then tloc (ATyp_exp($3))
- else raise (Parse_error_locn(loc (), "Only 2 is a valid exponent base in Nats")) }
+ | Num
+ { tloc (ATyp_constant $1) }
+ | TwoStarStar typ
+ { tloc (ATyp_exp($2)) }
nexp_typ:
- | Num
- { tloc (ATyp_constant $1) }
| exp_typ
{ $1 }
- | atomic_typ Plus typ
+ | atomic_typ Plus nexp_typ
{ tloc (ATyp_sum($1,$3)) }
+ | Lparen atomic_typ Plus nexp_typ Rparen
+ { tloc (ATyp_sum($2,$4)) }
typ:
- | nexp_typ
+ | star_typ
{ $1 }
- | star_typ MinusGt atomic_typ effect_typ
+ | star_typ MinusGt typ effect_typ
{ tloc (ATyp_fn($1,$3,$4)) }
lit:
@@ -387,21 +395,25 @@ atomic_pat:
{ ploc P_wild }
| Lparen pat As id Rparen
{ ploc (P_as($2,$4)) }
- | Lt typ Gt atomic_pat
- { ploc (P_typ($2,$4)) }
+ | Lparen Lparen typ Rparen atomic_pat Rparen
+ { ploc (P_typ($3,$5)) }
| id
{ ploc (P_app($1,[])) }
| Lcurly fpats Rcurly
{ ploc (P_record((fst $2, snd $2))) }
- | Lsquare pat Rsquare
- { ploc (P_vector([$2])) }
| Lsquare comma_pats Rsquare
{ ploc (P_vector($2)) }
+ | Lsquare pat Rsquare
+ { ploc (P_vector([$2])) }
| Lsquare npats Rsquare
{ ploc (P_vector_indexed($2)) }
| Lparen comma_pats Rparen
{ ploc (P_tup($2)) }
- | SquareBar comma_pats BarSquare
+ | SquareBarBar BarBarSquare
+ { ploc (P_list([])) }
+ | SquareBarBar pat BarBarSquare
+ { ploc (P_list([$2])) }
+ | SquareBarBar comma_pats BarBarSquare
{ ploc (P_list($2)) }
| Lparen pat Rparen
{ $2 }
@@ -409,10 +421,10 @@ atomic_pat:
app_pat:
| atomic_pat
{ $1 }
- | id Lparen pat Rparen
- { ploc (P_app($1,[$3])) }
| id Lparen comma_pats Rparen
{ ploc (P_app($1,$3)) }
+ | id Lparen pat Rparen
+ { ploc (P_app($1,[$3])) }
pat_colons:
| atomic_pat Colon atomic_pat
@@ -463,7 +475,7 @@ atomic_exp:
{ eloc (E_lit($1)) }
| Lparen exp Rparen
{ $2 }
- | Lt typ Gt atomic_exp
+ | Lparen typ Rparen atomic_exp
{ eloc (E_cast($2,$4)) }
| Lparen comma_exps Rparen
{ eloc (E_tuple($2)) }
@@ -475,7 +487,7 @@ atomic_exp:
{ eloc (E_vector_update($2,$4,$6)) }
| Lsquare exp With atomic_exp Colon atomic_exp Eq exp Rsquare
{ eloc (E_vector_update_subrange($2,$4,$6,$8)) }
- | SquareBar comma_exps BarSquare
+ | SquareBarBar comma_exps BarBarSquare
{ eloc (E_list($2)) }
| Switch exp Lcurly case_exps Rcurly
{ eloc (E_case($2,$4)) }
@@ -498,11 +510,11 @@ app_exp:
| vaccess_exp
{ $1 }
| id Lparen Rparen
- { eloc (E_app((E_aux((E_id $1), locn 1 1)), [eloc (E_lit (lloc L_unit))])) }
+ { eloc (E_app($1, [eloc (E_lit (lloc L_unit))])) }
| id Lparen exp Rparen
- { eloc (E_app((E_aux((E_id $1),locn 1 1)),[ E_aux((E_tuple [$3]),locn 3 3)])) }
+ { eloc (E_app($1,[ E_aux((E_tuple [$3]),locn 3 3)])) }
| id Lparen comma_exps Rparen
- { eloc (E_app((E_aux((E_id $1),locn 1 1)),[E_aux (E_tuple $3,locn 3 3)])) }
+ { eloc (E_app($1,[E_aux (E_tuple $3,locn 3 3)])) }
right_atomic_exp:
| If_ exp Then exp Else exp
@@ -863,15 +875,19 @@ val_spec:
{ vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4)) }
| Val atomic_typ id
{ vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3)) }
+ | Val Extern typquant atomic_typ id
+ { vloc (VS_extern_no_rename (mk_typschm $3 $4 3 4,$5)) }
+ | Val Extern atomic_typ id
+ { vloc (VS_extern_no_rename (mk_typschm (mk_typqn ()) $3 3 3, $4)) }
| Val Extern typquant atomic_typ id Eq String
{ vloc (VS_extern_spec (mk_typschm $3 $4 3 4,$5,$7)) }
| Val Extern atomic_typ id Eq String
{ vloc (VS_extern_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, $6)) }
kinded_id:
- | id
+ | tid
{ kiloc (KOpt_none $1) }
- | kind id
+ | kind tid
{ kiloc (KOpt_kind($1,$2))}
/*kinded_ids:
@@ -924,6 +940,20 @@ c_def_body:
| atomic_typ id Semi c_def_body
{ ($1,$2)::(fst $4), snd $4 }
+union_body:
+ | id
+ { [Tu_aux( Tu_id $1, loc())],false }
+ | atomic_typ id
+ { [Tu_aux( Tu_ty_id ($1,$2), loc())],false }
+ | id Semi
+ { [Tu_aux( Tu_id $1, loc())],true }
+ | atomic_typ id Semi
+ { [Tu_aux( Tu_ty_id ($1,$2),loc())],true }
+ | id Semi union_body
+ { (Tu_aux( Tu_id $1, loc()))::(fst $3), snd $3 }
+ | atomic_typ id Semi union_body
+ { (Tu_aux(Tu_ty_id($1,$2),loc()))::(fst $4), snd $4 }
+
index_range_atomic:
| Num
{ irloc (BF_single($1)) }
@@ -976,13 +1006,13 @@ type_def:
{ tdloc (TD_record($2,mk_namesectn (), $6, fst $8, snd $8)) }
| Typedef id 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 c_def_body Rcurly
+ | Typedef id 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 c_def_body Rcurly
+ | Typedef id 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 c_def_body Rcurly
+ | Typedef id 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 c_def_body Rcurly
+ | Typedef id 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
{ tdloc (TD_enum($2, mk_namesectn (), $6,false)) }
diff --git a/src/pre_lexer.mll b/src/pre_lexer.mll
new file mode 100644
index 00000000..6955c7c3
--- /dev/null
+++ b/src/pre_lexer.mll
@@ -0,0 +1,319 @@
+(**************************************************************************)
+(* Lem *)
+(* *)
+(* Dominic Mulligan, University of Cambridge *)
+(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *)
+(* Gabriel Kerneis, University of Cambridge *)
+(* Kathy Gray, University of Cambridge *)
+(* Peter Boehm, University of Cambridge (while working on Lem) *)
+(* Peter Sewell, University of Cambridge *)
+(* Scott Owens, University of Kent *)
+(* Thomas Tuerk, University of Cambridge *)
+(* *)
+(* The Lem sources are copyright 2010-2013 *)
+(* by the UK authors above and Institut National de Recherche en *)
+(* Informatique et en Automatique (INRIA). *)
+(* *)
+(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *)
+(* are distributed under the license below. The former are distributed *)
+(* under the LGPLv2, as in the LICENSE file. *)
+(* *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in the *)
+(* documentation and/or other materials provided with the distribution. *)
+(* 3. The names of the authors may not be used to endorse or promote *)
+(* products derived from this software without specific prior written *)
+(* permission. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *)
+(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *)
+(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *)
+(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *)
+(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *)
+(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *)
+(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *)
+(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *)
+(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *)
+(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *)
+(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)
+(**************************************************************************)
+
+{
+open Parser
+module M = Map.Make(String)
+exception LexError of string * Lexing.position
+
+let r = fun s -> s (* Ulib.Text.of_latin1 *)
+(* Available as Scanf.unescaped since OCaml 4.0 but 3.12 is still common *)
+let unescaped s = Scanf.sscanf ("\"" ^ s ^ "\"") "%S%!" (fun x -> x)
+
+let kw_table =
+ List.fold_left
+ (fun r (x,y) -> M.add x y r)
+ M.empty
+ [
+ ("and", (fun _ -> And));
+ ("as", (fun _ -> As));
+ ("bits", (fun _ -> Bits));
+ ("by", (fun _ -> By));
+ ("case", (fun _ -> Case));
+ ("clause", (fun _ -> Clause));
+ ("const", (fun _ -> Const));
+ ("dec", (fun _ -> Dec));
+ ("default", (fun _ -> Default));
+ ("deinfix", (fun _ -> Deinfix));
+ ("effect", (fun _ -> Effect));
+ ("Effects", (fun _ -> Effects));
+ ("end", (fun _ -> End));
+ ("enumerate", (fun _ -> Enumerate));
+ ("else", (fun _ -> Else));
+ ("extern", (fun _ -> Extern));
+ ("false", (fun _ -> False));
+ ("forall", (fun _ -> Forall));
+ ("foreach", (fun _ -> Foreach));
+ ("function", (fun x -> Function_));
+ ("if", (fun x -> If_));
+ ("in", (fun x -> In));
+ ("IN", (fun x -> IN));
+ ("Inc", (fun x -> Inc));
+ ("let", (fun x -> Let_));
+ ("member", (fun x -> Member));
+ ("Nat", (fun x -> Nat));
+ ("Order", (fun x -> Order));
+ ("pure", (fun x -> Pure));
+ ("rec", (fun x -> Rec));
+ ("register", (fun x -> Register));
+ ("scattered", (fun x -> Scattered));
+ ("struct", (fun x -> Struct));
+ ("switch", (fun x -> Switch));
+ ("then", (fun x -> Then));
+ ("true", (fun x -> True));
+ ("Type", (fun x -> TYPE));
+ ("typedef", (fun x -> Typedef));
+ ("undefined", (fun x -> Undefined));
+ ("union", (fun x -> Union));
+ ("with", (fun x -> With));
+ ("val", (fun x -> Val));
+
+ ("AND", (fun x -> AND));
+ ("div", (fun x -> Div_));
+ ("EOR", (fun x -> EOR));
+ ("mod", (fun x -> Mod));
+ ("OR", (fun x -> OR));
+ ("quot", (fun x -> Quot));
+ ("rem", (fun x -> Rem));
+]
+
+}
+
+let ws = [' ''\t']+
+let lowerletter = ['a'-'z']
+let upperletter = ['A'-'Z']
+let letter = ['a'-'z''A'-'Z']
+let digit = ['0'-'9']
+let binarydigit = ['0'-'1']
+let hexdigit = ['0'-'9''A'-'F''a'-'f']
+let alphanum = letter|digit
+let startident = lowerletter|'_'
+let ident = alphanum|['_''\'']
+let starttident = upperletter
+let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|''~']
+let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
+
+rule token = parse
+ | ws
+ { token lexbuf }
+ | "\n"
+ { Lexing.new_line lexbuf;
+ token lexbuf }
+
+ | "2**" { TwoStarStar }
+ | "&" { (Amp(r"&")) }
+ | "@" { (At(r"@")) }
+ | "|" { Bar }
+ | "^" { (Carrot(r"^")) }
+ | ":" { Colon }
+ | "," { Comma }
+ | "." { Dot }
+ | "/" { (Div(r "/")) }
+ | "=" { (Eq(r"=")) }
+ | "!" { (Excl(r"!")) }
+ | ">" { (Gt(r">")) }
+ | "-" { Minus }
+ | "<" { (Lt(r"<")) }
+ | "+" { (Plus(r"+")) }
+ | ";" { Semi }
+ | "*" { (Star(r"*")) }
+ | "~" { (Tilde(r"~")) }
+ | "_" { Under }
+ | "{" { Lcurly }
+ | "}" { Rcurly }
+ | "(" { Lparen }
+ | ")" { Rparen }
+ | "[" { Lsquare }
+ | "]" { Rsquare }
+ | "&&" as i { (AmpAmp(r i)) }
+ | "||" { BarBar }
+ | "|]" { BarSquare }
+ | "||]" { BarBarSquare }
+ | "^^" { (CarrotCarrot(r"^^")) }
+ | "::" as i { (ColonColon(r i)) }
+ | ":=" { ColonEq }
+ | ".." { DotDot }
+ | "=/=" { (EqDivEq(r"=/=")) }
+ | "==" { (EqEq(r"==")) }
+ | "!=" { (ExclEq(r"!=")) }
+ | "!!" { (ExclExcl(r"!!")) }
+ | ">=" { (GtEq(r">=")) }
+ | ">=+" { (GtEqPlus(r">=+")) }
+ | ">>" { (GtGt(r">>")) }
+ | ">>>" { (GtGtGt(r">>>")) }
+ | ">+" { (GtPlus(r">+")) }
+ | "#>>" { (HashGtGt(r"#>>")) }
+ | "#<<" { (HashLtLt(r"#<<")) }
+ | "->" { MinusGt }
+ | "<=" { (LtEq(r"<=")) }
+ | "<=+" { (LtEqPlus(r"<=+")) }
+ | "<>" { (LtGt(r"<>")) }
+ | "<<" { (LtLt(r"<<")) }
+ | "<<<" { (LtLtLt(r"<<<")) }
+ | "<+" { (LtPlus(r"<+")) }
+ | "**" { (StarStar(r"**")) }
+ | "~^" { (TildeCarrot(r"~^")) }
+
+ | ">=_s" { (GtEqUnderS(r">=_s")) }
+ | ">=_si" { (GtEqUnderSi(r">=_si")) }
+ | ">=_u" { (GtEqUnderU(r">=_u")) }
+ | ">=_ui" { (GtEqUnderUi(r">=_ui")) }
+ | ">>_u" { (GtGtUnderU(r">>_u")) }
+ | ">_s" { (GtUnderS(r">_s")) }
+ | ">_si" { (GtUnderSi(r">_si")) }
+ | ">_u" { (GtUnderU(r">_u")) }
+ | ">_ui" { (GtUnderUi(r">_ui")) }
+ | "<=_s" { (LtEqUnderS(r"<=_s")) }
+ | "<=_si" { (LtEqUnderSi(r"<=_si")) }
+ | "<=_u" { (LtEqUnderU(r"<=_u")) }
+ | "<=_ui" { (LtEqUnderUi(r"<=_ui")) }
+ | "<_s" { (LtUnderS(r"<_s")) }
+ | "<_si" { (LtUnderSi(r"<_si")) }
+ | "<_u" { (LtUnderU(r"<_u")) }
+ | "<_ui" { (LtUnderUi(r"<_ui")) }
+ | "**_s" { (StarStarUnderS(r"**_s")) }
+ | "**_si" { (StarStarUnderSi(r"**_si")) }
+ | "*_u" { (StarUnderU(r"*_u")) }
+ | "*_ui" { (StarUnderUi(r"*_ui")) }
+ | "2^" { (TwoCarrot(r"2^")) }
+
+
+ | "(*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
+ | "*)" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
+
+ | startident ident* as i { if M.mem i kw_table then
+ (M.find i kw_table) ()
+ else
+ Id(r i) }
+ | starttident ident* as i { if M.mem i kw_table then
+ (M.find i kw_table) ()
+ else
+ TyId(r i) }
+ | "&" oper_char+ as i { (AmpI(r i)) }
+ | "@" oper_char+ as i { (AtI(r i)) }
+ | "^" oper_char+ as i { (CarrotI(r i)) }
+ | "/" oper_char+ as i { (DivI(r i)) }
+ | "=" oper_char+ as i { (EqI(r i)) }
+ | "!" oper_char+ as i { (ExclI(r i)) }
+ | ">" oper_char+ as i { (GtI(r i)) }
+ | "<" oper_char+ as i { (LtI(r i)) }
+ | "+" oper_char+ as i { (PlusI(r i)) }
+ | "*" oper_char+ as i { (StarI(r i)) }
+ | "~" oper_char+ as i { (TildeI(r i)) }
+ | "&&" oper_char+ as i { (AmpAmpI(r i)) }
+ | "^^" oper_char+ as i { (CarrotCarrotI(r i)) }
+ | "::" oper_char+ as i { (ColonColonI(r i)) }
+ | "=/=" oper_char+ as i { (EqDivEqI(r i)) }
+ | "==" oper_char+ as i { (EqEqI(r i)) }
+ | "!=" oper_char+ as i { (ExclEqI(r i)) }
+ | "!!" oper_char+ as i { (ExclExclI(r i)) }
+ | ">=" oper_char+ as i { (GtEqI(r i)) }
+ | ">=+" oper_char+ as i { (GtEqPlusI(r i)) }
+ | ">>" oper_char+ as i { (GtGtI(r i)) }
+ | ">>>" oper_char+ as i { (GtGtGtI(r i)) }
+ | ">+" oper_char+ as i { (GtPlusI(r i)) }
+ | "#>>" oper_char+ as i { (HashGtGt(r i)) }
+ | "#<<" oper_char+ as i { (HashLtLt(r i)) }
+ | "<=" oper_char+ as i { (LtEqI(r i)) }
+ | "<=+" oper_char+ as i { (LtEqPlusI(r i)) }
+ | "<<" oper_char+ as i { (LtLtI(r i)) }
+ | "<<<" oper_char+ as i { (LtLtLtI(r i)) }
+ | "<+" oper_char+ as i { (LtPlusI(r i)) }
+ | "**" oper_char+ as i { (StarStarI(r i)) }
+ | "~^" oper_char+ as i { (TildeCarrot(r i)) }
+
+ | ">=_s" oper_char+ as i { (GtEqUnderSI(r i)) }
+ | ">=_si" oper_char+ as i { (GtEqUnderSiI(r i)) }
+ | ">=_u" oper_char+ as i { (GtEqUnderUI(r i)) }
+ | ">=_ui" oper_char+ as i { (GtEqUnderUiI(r i)) }
+ | ">>_u" oper_char+ as i { (GtGtUnderUI(r i)) }
+ | ">_s" oper_char+ as i { (GtUnderSI(r i)) }
+ | ">_si" oper_char+ as i { (GtUnderSiI(r i)) }
+ | ">_u" oper_char+ as i { (GtUnderUI(r i)) }
+ | ">_ui" oper_char+ as i { (GtUnderUiI(r i)) }
+ | "<=_s" oper_char+ as i { (LtEqUnderSI(r i)) }
+ | "<=_si" oper_char+ as i { (LtEqUnderSiI(r i)) }
+ | "<=_u" oper_char+ as i { (LtEqUnderUI(r i)) }
+ | "<=_ui" oper_char+ as i { (LtEqUnderUiI(r i)) }
+ | "<_s" oper_char+ as i { (LtUnderSI(r i)) }
+ | "<_si" oper_char+ as i { (LtUnderSiI(r i)) }
+ | "<_u" oper_char+ as i { (LtUnderUI(r i)) }
+ | "<_ui" oper_char+ as i { (LtUnderUiI(r i)) }
+ | "**_s" oper_char+ as i { (StarStarUnderSI(r i)) }
+ | "**_si" oper_char+ as i { (StarStarUnderSiI(r i)) }
+ | "*_u" oper_char+ as i { (StarUnderUI(r i)) }
+ | "*_ui" oper_char+ as i { (StarUnderUiI(r i)) }
+ | "2^" oper_char+ as i { (TwoCarrotI(r i)) }
+
+ | digit+ as i { (Num(int_of_string i)) }
+ | "0b" (binarydigit+ as i) { (Bin(i)) }
+ | "0x" (hexdigit+ as i) { (Hex(i)) }
+ | '"' { (String(
+ string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) }
+ | eof { Eof }
+ | _ as c { raise (LexError(
+ Printf.sprintf "Unexpected character: %c" c,
+ Lexing.lexeme_start_p lexbuf)) }
+
+
+and comment pos depth = parse
+ | "(*" { comment pos (depth+1) lexbuf }
+ | "*)" { if depth = 0 then ()
+ else if depth > 0 then comment pos (depth-1) lexbuf
+ else assert false }
+ | "\n" { Lexing.new_line lexbuf;
+ comment pos depth lexbuf }
+ | '"' { ignore(string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf);
+ comment pos depth lexbuf }
+ | _ { comment pos depth lexbuf }
+ | eof { raise (LexError("Unbalanced comment", pos)) }
+
+and string pos b = parse
+ | ([^'"''\n''\\']*'\n' as i) { Lexing.new_line lexbuf;
+ Buffer.add_string b i;
+ string pos b lexbuf }
+ | ([^'"''\n''\\']* as i) { Buffer.add_string b i; string pos b lexbuf }
+ | escape_sequence as i { Buffer.add_string b i; string pos b lexbuf }
+ | '\\' '\n' ws { Lexing.new_line lexbuf; string pos b lexbuf }
+ | '\\' { assert false (*raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+ "illegal backslash escape in string"*) }
+ | '"' { let s = unescaped(Buffer.contents b) in
+ (*try Ulib.UTF8.validate s; s
+ with Ulib.UTF8.Malformed_code ->
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+ "String literal is not valid utf8"))) *) s }
+ | eof { assert false (*raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+ "String literal not terminated")))*) }
diff --git a/src/pre_parser.mly b/src/pre_parser.mly
new file mode 100644
index 00000000..5d56738b
--- /dev/null
+++ b/src/pre_parser.mly
@@ -0,0 +1,86 @@
+/**************************************************************************/
+/* Lem */
+/* */
+/* Dominic Mulligan, University of Cambridge */
+/* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt */
+/* Gabriel Kerneis, University of Cambridge */
+/* Kathy Gray, University of Cambridge */
+/* Peter Boehm, University of Cambridge (while working on Lem) */
+/* Peter Sewell, University of Cambridge */
+/* Scott Owens, University of Kent */
+/* Thomas Tuerk, University of Cambridge */
+/* */
+/* The Lem sources are copyright 2010-2013 */
+/* by the UK authors above and Institut National de Recherche en */
+/* Informatique et en Automatique (INRIA). */
+/* */
+/* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} */
+/* are distributed under the license below. The former are distributed */
+/* under the LGPLv2, as in the LICENSE file. */
+/* */
+/* */
+/* Redistribution and use in source and binary forms, with or without */
+/* modification, are permitted provided that the following conditions */
+/* are met: */
+/* 1. Redistributions of source code must retain the above copyright */
+/* notice, this list of conditions and the following disclaimer. */
+/* 2. Redistributions in binary form must reproduce the above copyright */
+/* notice, this list of conditions and the following disclaimer in the */
+/* documentation and/or other materials provided with the distribution. */
+/* 3. The names of the authors may not be used to endorse or promote */
+/* products derived from this software without specific prior written */
+/* permission. */
+/* */
+/* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS */
+/* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED */
+/* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE */
+/* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY */
+/* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL */
+/* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE */
+/* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS */
+/* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER */
+/* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR */
+/* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN */
+/* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */
+/**************************************************************************/
+
+%{
+
+let r = fun x -> x (* Ulib.Text.of_latin1 *)
+
+%}
+
+/*Terminals with no content*/
+
+%token Scattered Typedef Other Eof
+
+%token <string> Id
+%start file
+%type <list string> file
+
+%%
+
+id:
+ | Id
+ { $1 }
+
+scan:
+ | Typedef id
+ { $2 }
+ | Scattered Typedef id
+ { $3 }
+ | id scan
+ { $2 }
+ | Other scan
+ { $2 }
+
+scan_file:
+ | scan
+ { [$1] }
+ | scan scan_file
+ { $1::$2 }
+
+file:
+ | scan_file Eof
+ { $1 }
+
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 55d09dcb..dd5a792b 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -211,7 +211,7 @@ and pp_exp ppf (E_aux(e,_)) =
| E_id(id) -> pp_id ppf id
| E_lit(lit) -> pp_lit ppf lit
| E_cast(typ,exp) -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "<" pp_typ typ kwd ">" pp_exp exp
- | E_app(f,args) -> fprintf ppf "@[<0>%a %a@]" pp_exp f (list_pp pp_exp pp_exp) args
+ | E_app(f,args) -> fprintf ppf "@[<0>%a %a@]" pp_id f (list_pp pp_exp pp_exp) args
| E_app_infix(l,op,r) -> fprintf ppf "@[<0>%a %a %a@]" pp_exp l pp_id op pp_exp r
| E_tuple(exps) -> fprintf ppf "@[<0>%a %a %a@]" kwd "(" (list_pp pp_comma_exp pp_exp) exps kwd ")"
| E_if(c,t,e) -> fprintf ppf "@[<0> %a %a @[<1> %a %a@] @[<1> %a@ %a@]@]" kwd "if " pp_exp c kwd "then" pp_exp t kwd "else" pp_exp e
@@ -288,8 +288,11 @@ let pp_typdef ppf (TD_aux(td,_)) =
fprintf ppf "@[<0>%a %a %a %a %a %a %a %a@[<1>%a@] %a]@\n"
kwd "typedef" pp_id id pp_namescm nm kwd "=" kwd "const" kwd "struct" pp_typquant typq kwd "{" (list_pp f_pp f_pp) fs kwd "}"
| TD_variant(id,nm,typq,ar,_) ->
- let a_pp ppf (typ,id) =
- fprintf ppf "@[<1>%a %a%a@]" pp_typ typ pp_id id kwd ";" in
+ let a_pp ppf (Tu_aux(typ_u,_)) =
+ match typ_u with
+ | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>%a %a%a@]" pp_typ typ pp_id id kwd ";"
+ | Tu_id(id) -> fprintf ppf "@[<1>%a%a@]" pp_id id kwd ";"
+ in
fprintf ppf "@[<0>%a %a %a %a %a %a %a %a@[<1>%a@] %a]@\n"
kwd "typedef" pp_id id pp_namescm nm kwd "=" kwd "const" kwd "union" pp_typquant typq kwd "{" (list_pp a_pp a_pp) ar kwd "}"
| TD_enum(id,ns,enums,_) ->
@@ -504,7 +507,7 @@ and pp_lem_exp ppf (E_aux(e,_)) =
| E_id(id) -> fprintf ppf "(%a %a)" kwd "E_id" pp_lem_id id
| E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit
| E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp
- | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_exp f (list_pp pp_semi_lem_exp pp_lem_exp) args
+ | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args
| E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r
| E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")"
| E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e
@@ -584,8 +587,11 @@ let pp_lem_typdef ppf (TD_aux(td,_)) =
fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
| TD_variant(id,nm,typq,ar,_) ->
- let a_pp ppf (typ,id) =
- fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
+ let a_pp ppf (Tu_aux(typ_u,_)) =
+ match typ_u with
+ | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_ty_id %a %a)@]" pp_lem_typ typ pp_lem_id id
+ | Tu_id(id) -> fprintf ppf "@[<1>(Tu_id %a)@]" pp_id id
+ in
fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar
| TD_enum(id,ns,enums,_) ->
diff --git a/src/type_check.mli b/src/type_check.mli
new file mode 100644
index 00000000..25992725
--- /dev/null
+++ b/src/type_check.mli
@@ -0,0 +1,9 @@
+open Ast
+open Type_internal
+type kind = Type_internal.kind
+type typ = Type_internal.t
+
+type envs = Nameset.t * kind Envmap.t * typ Envmap.t
+type 'a envs_out = 'a * envs
+
+val check : Nameset.t -> kind Envmap.t -> typ Envmap.t -> tannot defs -> tannot defs
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 8ebb0b69..dabb8100 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -55,6 +55,12 @@ and t_arg =
| TA_eft of effect
| TA_ord of order
+type tag =
+ | Emp
+ | External
+ | Default
+ | Constructor
+
(* Constraints for nexps, plus the location which added the constraint, each nexp is either <= 0 = 0 or >= 0 *)
type nexp_range =
| LtEq of Parse_ast.l * nexp
@@ -62,7 +68,7 @@ type nexp_range =
| GtEq of Parse_ast.l * nexp
| In of Parse_ast.l * nexp * nexp list
-type tannot = (t * nexp_range list) option
+type tannot = (t * tag * nexp_range list) option
let initial_kind_env =
Envmap.from_list [
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 9aa5b9d9..99b82075 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -52,6 +52,12 @@ and t_arg =
| TA_eft of effect
| TA_ord of order
+type tag =
+ | Emp
+ | External
+ | Default
+ | Constructor
+
(* Constraints for nexps, plus the location which added the constraint, each nexp is either <= 0 = 0 or >= 0 *)
type nexp_range =
| LtEq of Parse_ast.l * nexp
@@ -59,6 +65,6 @@ type nexp_range =
| GtEq of Parse_ast.l * nexp
| In of Parse_ast.l * nexp * nexp list
-type tannot = (t * nexp_range list) option
+type tannot = (t * tag * nexp_range list) option
val initial_kind_env : kind Envmap.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:32:02 +0000