diff options
| -rw-r--r-- | src/_tags | 2 | ||||
| -rw-r--r-- | src/initial_check.ml | 2 | ||||
| -rw-r--r-- | src/lexer2.mll | 356 | ||||
| -rw-r--r-- | src/parser2.mly | 1350 | ||||
| -rw-r--r-- | src/process_file.ml | 9 | ||||
| -rw-r--r-- | src/process_file.mli | 2 | ||||
| -rw-r--r-- | src/sail.ml | 8 | ||||
| -rw-r--r-- | src/type_check.ml | 103 | ||||
| -rw-r--r-- | src/type_check.mli | 2 | ||||
| -rw-r--r-- | test/typecheck/pass/exint.sail | 22 |
10 files changed, 1816 insertions, 40 deletions
@@ -1,4 +1,4 @@ -true: -traverse, debug +true: -traverse, debug, use_menhir <**/*.ml>: bin_annot, annot <lem_interp> or <test>: include <sail.{byte,native}>: use_pprint, use_nums, use_unix diff --git a/src/initial_check.ml b/src/initial_check.ml index 728056ab..9d295dda 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -302,7 +302,7 @@ and to_ast_typ_arg (k_env : kind Envmap.t) (def_ord : order) (kind : kind) (arg | K_Nat -> Typ_arg_nexp (to_ast_nexp k_env arg) | K_Ord -> Typ_arg_order (to_ast_order k_env def_ord arg) | K_Efct -> Typ_arg_effect (to_ast_effects k_env arg) - | _ -> raise (Reporting_basic.err_unreachable l "To_ast_typ_arg received Lam kind or infer kind")), + | _ -> raise (Reporting_basic.err_unreachable l ("To_ast_typ_arg received Lam kind or infer kind: " ^ kind_to_string kind))), l) and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint = diff --git a/src/lexer2.mll b/src/lexer2.mll new file mode 100644 index 00000000..561adcfd --- /dev/null +++ b/src/lexer2.mll @@ -0,0 +1,356 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* 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. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``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 AUTHOR OR *) +(* CONTRIBUTORS 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 Parser2 +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)); + ("alias", (fun _ -> Alias)); + ("as", (fun _ -> As)); + ("assert", (fun _ -> Assert)); + ("bitzero", (fun _ -> Bitzero)); + ("bitone", (fun _ -> Bitone)); + ("bits", (fun _ -> Bits)); + ("by", (fun _ -> By)); + ("case", (fun _ -> Case)); + ("clause", (fun _ -> Clause)); + ("const", (fun _ -> Const)); + ("dec", (fun _ -> Dec)); + ("def", (fun _ -> Def)); + ("default", (fun _ -> Default)); + ("deinfix", (fun _ -> Deinfix)); + ("effect", (fun _ -> Effect)); + ("Effect", (fun _ -> EFFECT)); + ("end", (fun _ -> End)); + ("enumerate", (fun _ -> Enumerate)); + ("else", (fun _ -> Else)); + ("exit", (fun _ -> Exit)); + ("extern", (fun _ -> Extern)); + ("cast", (fun _ -> Cast)); + ("false", (fun _ -> False)); + ("forall", (fun _ -> Forall)); + ("exist", (fun _ -> Exist)); + ("foreach", (fun _ -> Foreach)); + ("function", (fun x -> Function_)); + ("overload", (fun _ -> Overload)); + ("if", (fun x -> If_)); + ("in", (fun x -> In)); + ("inc", (fun _ -> Inc)); + ("IN", (fun x -> IN)); + ("let", (fun x -> Let_)); + ("member", (fun x -> Member)); + ("Nat", (fun x -> Nat)); + ("Num", (fun x -> NatNum)); + ("Order", (fun x -> Order)); + ("pure", (fun x -> Pure)); + ("rec", (fun x -> Rec)); + ("register", (fun x -> Register)); + ("return", (fun x -> Return)); + ("scattered", (fun x -> Scattered)); + ("sizeof", (fun x -> Sizeof)); + ("constraint", (fun x -> Constraint)); + ("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)); + ("when", (fun x -> When)); + ("val", (fun x -> Val)); + + ("div", (fun x -> Div_)); + ("mod", (fun x -> Mod)); + ("mod_s", (fun x -> ModUnderS)); + ("quot", (fun x -> Quot)); + ("quot_s", (fun x -> QuotUnderS)); + ("rem", (fun x -> Rem)); + + ("barr", (fun x -> Barr)); + ("depend", (fun x -> Depend)); + ("rreg", (fun x -> Rreg)); + ("wreg", (fun x -> Wreg)); + ("rmem", (fun x -> Rmem)); + ("rmemt", (fun x -> Rmemt)); + ("wmem", (fun x -> Wmem)); + ("wmv", (fun x -> Wmv)); + ("wmvt", (fun x -> Wmvt)); + ("eamem", (fun x -> Eamem)); + ("exmem", (fun x -> Exmem)); + ("undef", (fun x -> Undef)); + ("unspec", (fun x -> Unspec)); + ("nondet", (fun x -> Nondet)); + ("escape", (fun x -> Escape)); + +] + +let default_type_names = ["bool";"unit";"vector";"range";"list";"bit";"nat"; "int"; "real"; + "uint8";"uint16";"uint32";"uint64";"atom";"implicit";"string";"option"] +let custom_type_names : string list ref = ref [] + +} + +let ws = [' ''\t']+ +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 ident = alphanum|['_''\''] +let tyvar_start = '\'' +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 } + + | "&" { (Amp(r"&")) } + | "@" { (At(r"@")) } + | "|" { Bar } + | "^" { (Carrot(r"^")) } + | ":" { Colon(r ":") } + | "," { Comma } + | "." { Dot } + | "=" { (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 } + | "||]" { BarBarSquare } + | "|]" { BarSquare } + | "^^" { (CarrotCarrot(r"^^")) } + | "::" as i { (ColonColon(r i)) } + | ":=" { ColonEq } + | ":>" { ColonGt } + | ":]" { ColonSquare } + | ".." { DotDot } + | "==" { (EqEq(r"==")) } + | "!=" { (ExclEq(r"!=")) } + | "!!" { (ExclExcl(r"!!")) } + | ">=" { (GtEq(r">=")) } + | ">=+" { (GtEqPlus(r">=+")) } + | ">>" { (GtGt(r">>")) } + | ">>>" { (GtGtGt(r">>>")) } + | ">+" { (GtPlus(r">+")) } + | "#>>" { (HashGtGt(r"#>>")) } + | "#<<" { (HashLtLt(r"#<<")) } + | "->" { MinusGt } + | "<:" { LtColon } + | "<=" { (LtEq(r"<=")) } + | "<=+" { (LtEqPlus(r"<=+")) } + | "<>" { (LtGt(r"<>")) } + | "<<" { (LtLt(r"<<")) } + | "<<<" { (LtLtLt(r"<<<")) } + | "<+" { (LtPlus(r"<+")) } + | "**" { (StarStar(r"**")) } + | "[|" { SquareBar } + | "[||" { SquareBarBar } + | "[:" { SquareColon } + | "~^" { (TildeCarrot(r"~^")) } + + | "+_s" { (PlusUnderS(r"+_s")) } + | "-_s" { (MinusUnderS(r"-_s")) } + | ">=_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" { (StarUnderS(r"*_s")) } + | "**_s" { (StarStarUnderS(r"**_s")) } + | "**_si" { (StarStarUnderSi(r"**_si")) } + | "*_u" { (StarUnderU(r"*_u")) } + | "*_ui" { (StarUnderUi(r"*_ui")) } + | "2^" { (TwoCarrot(r"2^")) } + | "2**" { TwoStarStar } + + + | "(*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf } + | "*)" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) } + + | tyvar_start startident ident* as i { TyVar(r i) } + | startident ident* as i { if M.mem i kw_table then + (M.find i kw_table) () + else if + List.mem i default_type_names || + List.mem i !custom_type_names then + TyId(r i) + 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 { (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 i1) "." (digit+ as i2) { (Real (i1 ^ "." ^ i2)) } + | "-" (digit* as i1) "." (digit+ as i2) { (Real ("-" ^ i1 ^ "." ^ i2)) } + | digit+ as i { (Num(int_of_string 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/parser2.mly b/src/parser2.mly new file mode 100644 index 00000000..d6da6e63 --- /dev/null +++ b/src/parser2.mly @@ -0,0 +1,1350 @@ +/**************************************************************************/ +/* Sail */ +/* */ +/* Copyright (c) 2013-2017 */ +/* Kathyrn Gray */ +/* Shaked Flur */ +/* Stephen Kell */ +/* Gabriel Kerneis */ +/* Robert Norton-Wright */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the University of Cambridge Computer */ +/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ +/* (REMS) project, funded by EPSRC grant EP/K008528/1. */ +/* */ +/* 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. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``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 AUTHOR OR */ +/* CONTRIBUTORS 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 *) + +open Parse_ast + +let loc () = Range(Parsing.symbol_start_pos(),Parsing.symbol_end_pos()) +let locn m n = Range(Parsing.rhs_start_pos m,Parsing.rhs_end_pos n) + +let idl i = Id_aux(i, loc()) + +let efl e = BE_aux(e, loc()) + +let ploc p = P_aux(p,loc ()) +let eloc e = E_aux(e,loc ()) +let peloc pe = Pat_aux(pe,loc ()) +let lbloc lb = LB_aux(lb,loc ()) + +let bkloc k = BK_aux(k,loc ()) +let kloc k = K_aux(k,loc ()) +let kiloc ki = KOpt_aux(ki,loc ()) +let tloc t = ATyp_aux(t,loc ()) +let tlocl t l1 l2 = ATyp_aux(t,locn l1 l2) +let lloc l = L_aux(l,loc ()) +let ploc p = P_aux(p,loc ()) +let fploc p = FP_aux(p,loc ()) + +let funclloc f = FCL_aux(f,loc ()) +let typql t = TypQ_aux(t, loc()) +let irloc r = BF_aux(r, loc()) +let defloc df = DT_aux(df, loc()) + +let tdloc td = TD_aux(td, loc()) +let kdloc kd = KD_aux(kd, loc()) +let funloc fn = FD_aux(fn, loc()) +let vloc v = VS_aux(v, loc ()) +let sdloc sd = SD_aux(sd, loc ()) +let dloc d = d + +let mk_typschm tq t s e = TypSchm_aux((TypSchm_ts(tq,t)),(locn s e)) +let mk_rec i = (Rec_aux((Rec_rec), locn i i)) +let mk_recn _ = (Rec_aux((Rec_nonrec), Unknown)) +let mk_typqn _ = (TypQ_aux(TypQ_no_forall,Unknown)) +let mk_tannot tq t s e = Typ_annot_opt_aux(Typ_annot_opt_some(tq,t),(locn s e)) +let mk_tannotn _ = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown) +let mk_eannot e i = Effect_opt_aux((Effect_opt_effect(e)),(locn i i)) +let mk_eannotn _ = Effect_opt_aux(Effect_opt_pure,Unknown) +let mk_namesectn _ = Name_sect_aux(Name_sect_none,Unknown) + +let make_range_sugar_bounded typ1 typ2 = + ATyp_app(Id_aux(Id("range"),Unknown),[typ1; typ2;]) +let make_range_sugar typ1 = + make_range_sugar_bounded (ATyp_aux(ATyp_constant(0), Unknown)) typ1 +let make_atom_sugar typ1 = + ATyp_app(Id_aux(Id("atom"),Unknown),[typ1]) + +let make_r bot top = + match bot,top with + | ATyp_aux(ATyp_constant b,_),ATyp_aux(ATyp_constant t,l) -> + ATyp_aux(ATyp_constant ((t-b)+1),l) + | bot,(ATyp_aux(_,l) as top) -> + ATyp_aux((ATyp_sum ((ATyp_aux (ATyp_sum (top, ATyp_aux(ATyp_constant 1,Unknown)), Unknown)), + (ATyp_aux ((ATyp_neg bot),Unknown)))), l) + +let make_vector_sugar_bounded order_set is_inc name typ typ1 typ2 = + let (rise,ord,name) = + if order_set + then if is_inc + then (make_r typ1 typ2,ATyp_inc,name) + else (make_r typ2 typ1,ATyp_dec,name) + else if name = "vector" + then (typ2, ATyp_default_ord,"vector_sugar_tb") (* rise not calculated, but top and bottom came from specification *) + else (typ2, ATyp_default_ord,"vector_sugar_r") (* rise and base not calculated, rise only from specification *) in + ATyp_app(Id_aux(Id(name),Unknown),[typ1;rise;ATyp_aux(ord,Unknown);typ]) +let make_vector_sugar order_set is_inc typ typ1 = + let zero = (ATyp_aux(ATyp_constant 0,Unknown)) in + let (typ1,typ2) = match (order_set,is_inc,typ1) with + | (true,true,ATyp_aux(ATyp_constant t,l)) -> zero,ATyp_aux(ATyp_constant (t-1),l) + | (true,true,ATyp_aux(_, l)) -> zero,ATyp_aux (ATyp_sum (typ1, + ATyp_aux(ATyp_neg(ATyp_aux(ATyp_constant 1,Unknown)), Unknown)), l) + | (true,false,_) -> typ1,zero + | (false,_,_) -> zero,typ1 in + make_vector_sugar_bounded order_set is_inc "vector_sugar_r" typ typ1 typ2 + +%} + +/*Terminals with no content*/ + +%token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Def Default Deinfix Effect EFFECT End +%token Enumerate Else Exit Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Nat NatNum Order Cast +%token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef +%token Undefined Union With When Val Constraint +%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape + + +/* Avoid shift/reduce conflict - see right_atomic_exp rule */ +%nonassoc Then +%nonassoc Else + +%token Div_ Mod ModUnderS Quot Rem QuotUnderS + +%token Bar Comma Dot Eof Minus Semi Under +%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare +%token BarBar BarSquare BarBarSquare ColonEq ColonGt ColonSquare DotDot +%token MinusGt LtBar LtColon SquareBar SquareBarBar SquareColon + +/*Terminals with content*/ + +%token <string> Id TyVar TyId +%token <int> Num +%token <string> String Bin Hex Real + +%token <string> Amp At Carrot Div Eq Excl Gt Lt Plus Star Tilde +%token <string> AmpAmp CarrotCarrot Colon ColonColon EqEq ExclEq ExclExcl +%token <string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt +%token <string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar TildeCarrot + +%token <string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS +%token <string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU +%token <string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarStarUnderS StarStarUnderSi StarUnderS +%token <string> StarUnderSi StarUnderU StarUnderUi TwoCarrot PlusUnderS MinusUnderS + +%token <string> AmpI AtI CarrotI DivI EqI ExclI GtI LtI PlusI StarI TildeI +%token <string> AmpAmpI CarrotCarrotI ColonColonI EqEqI ExclEqI ExclExclI +%token <string> GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI +%token <string> LtEqI LtEqPlusI LtGtI LtLtI LtLtLtI LtPlusI StarStarI TildeCarrotI + +%token <string> GtEqUnderSI GtEqUnderSiI GtEqUnderUI GtEqUnderUiI GtGtUnderUI GtUnderSI +%token <string> GtUnderSiI GtUnderUI GtUnderUiI LtEqUnderSI LtEqUnderSiI LtEqUnderUI +%token <string> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarStarUnderSI StarStarUnderSiI StarUnderSI +%token <string> StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI + + +%start file nonempty_exp_list +%type <Parse_ast.defs> defs +%type <Parse_ast.atyp> typ +%type <Parse_ast.pat> pat +%type <Parse_ast.exp> exp +%type <Parse_ast.exp list> nonempty_exp_list +%type <Parse_ast.defs> file + + +%% + +id: + | Id + { idl (Id($1)) } + | Tilde + { idl (Id($1)) } + | 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 Quot Rparen + { idl (DeIid("quot")) } + | Lparen Deinfix QuotUnderS Rparen + { idl (DeIid("quot_s")) } + | Lparen Deinfix Eq Rparen + { Id_aux(DeIid($3),loc ()) } + | Lparen Deinfix Excl Lparen + { idl (DeIid($3)) } + | Lparen Deinfix Gt Rparen + { idl (DeIid($3)) } + | Lparen Deinfix Lt Rparen + { idl (DeIid($3)) } + | Lparen Deinfix GtUnderS Rparen + { idl (DeIid($3)) } + | Lparen Deinfix LtUnderS Rparen + { idl (DeIid($3)) } + | Lparen Deinfix Minus Rparen + { idl (DeIid("-")) } + | Lparen Deinfix MinusUnderS Rparen + { idl (DeIid("-_s")) } + | Lparen Deinfix Mod Rparen + { idl (DeIid("mod")) } + | Lparen Deinfix Plus Rparen + { idl (DeIid($3)) } + | Lparen Deinfix PlusUnderS Rparen + { idl (DeIid("+_s")) } + | Lparen Deinfix Star Rparen + { idl (DeIid($3)) } + | Lparen Deinfix StarUnderS Rparen + { idl (DeIid("*_s")) } + | Lparen Deinfix AmpAmp Rparen + { idl (DeIid($3)) } + | Lparen Deinfix Bar Rparen + { idl (DeIid("|")) } + | Lparen Deinfix BarBar Rparen + { idl (DeIid("||")) } + | Lparen Deinfix CarrotCarrot Rparen + { idl (DeIid($3)) } + | Lparen Deinfix Colon Rparen + { idl (DeIid($3)) } + | Lparen Deinfix ColonColon 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 GtEqUnderS 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 LtEqUnderS 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 Tilde Rparen + { idl (DeIid($3)) } + | Lparen Deinfix TildeCarrot Rparen + { idl (DeIid($3)) } + +tid: + | TyId + { (idl (Id($1))) } + +tyvar: + | TyVar + { (Kid_aux((Var($1)),loc ())) } + +tyvars: + | tyvar + { [$1] } + | tyvar tyvars + { $1 :: $2 } + +atomic_kind: + | TYPE + { bkloc BK_type } + | Nat + { bkloc BK_nat } + | NatNum + { bkloc BK_nat } + | Order + { bkloc BK_order } + | EFFECT + { bkloc BK_effect } + +kind_help: + | atomic_kind + { [ $1 ] } + | atomic_kind MinusGt kind_help + { $1::$3 } + +kind: + | kind_help + { K_aux(K_kind($1), loc ()) } + +effect: + | Barr + { efl BE_barr } + | Depend + { efl BE_depend } + | Rreg + { efl BE_rreg } + | Wreg + { efl BE_wreg } + | Rmem + { efl BE_rmem } + | Rmemt + { efl BE_rmemt } + | Wmem + { efl BE_wmem } + | Wmv + { efl BE_wmv } + | Wmvt + { efl BE_wmvt } + | Eamem + { efl BE_eamem } + | Exmem + { efl BE_exmem } + | Undef + { efl BE_undef } + | Unspec + { efl BE_unspec } + | Nondet + { efl BE_nondet } + | Escape + { efl BE_escape } + +effect_list: + | effect + { [$1] } + | effect Comma effect_list + { $1::$3 } + +effect_typ: + | Lcurly effect_list Rcurly + { tloc (ATyp_set($2)) } + | Pure + { tloc (ATyp_set([])) } + +vec_typ: + | tid Lsquare nexp_typ Rsquare + { tloc (make_vector_sugar false false (ATyp_aux ((ATyp_id $1), locn 1 1)) $3) } + | tid Lsquare nexp_typ Colon nexp_typ Rsquare + { tloc (make_vector_sugar_bounded false false "vector" (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) } + | tid Lsquare nexp_typ LtColon nexp_typ Rsquare + { tloc (make_vector_sugar_bounded true true "vector" (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) } + | tid Lsquare nexp_typ ColonGt nexp_typ Rsquare + { tloc (make_vector_sugar_bounded true false "vector" (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) } + | tyvar Lsquare nexp_typ Rsquare + { tloc (make_vector_sugar false false (ATyp_aux ((ATyp_var $1), locn 1 1)) $3) } + | tyvar Lsquare nexp_typ Colon nexp_typ Rsquare + { tloc (make_vector_sugar_bounded false false "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) } + | tyvar Lsquare nexp_typ LtColon nexp_typ Rsquare + { tloc (make_vector_sugar_bounded true true "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) } + | tyvar Lsquare nexp_typ ColonGt nexp_typ Rsquare + { tloc (make_vector_sugar_bounded true false "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) } + +app_typs: + | atomic_typ + { [$1] } + | atomic_typ Comma app_typs + { $1::$3 } + +atomic_typ: + | vec_typ + { $1 } + | range_typ + { $1 } + | nexp_typ + { $1 } + | Inc + { tloc (ATyp_inc) } + | Dec + { tloc (ATyp_dec) } + | tid Lt app_typs Gt + { tloc (ATyp_app($1,$3)) } + | Register Lt app_typs Gt + { tloc (ATyp_app(Id_aux(Id "register", locn 1 1),$3)) } + +range_typ: + | SquareBar nexp_typ BarSquare + { tloc (make_range_sugar $2) } + | SquareBar nexp_typ Colon nexp_typ BarSquare + { tloc (make_range_sugar_bounded $2 $4) } + | SquareColon nexp_typ ColonSquare + { tloc (make_atom_sugar $2) } + +nexp_typ: + | nexp_typ Plus nexp_typ2 + { tloc (ATyp_sum ($1, $3)) } + | nexp_typ Minus nexp_typ2 + { tloc (ATyp_minus ($1, $3)) } + | Minus nexp_typ2 + { tloc (ATyp_neg $2) } + | nexp_typ2 + { $1 } + +nexp_typ2: + | nexp_typ2 Star nexp_typ3 + { tloc (ATyp_times ($1, $3)) } + | nexp_typ3 + { $1 } + +nexp_typ3: + | TwoStarStar nexp_typ4 + { tloc (ATyp_exp $2) } + | nexp_typ4 + { $1 } + +nexp_typ4: + | Num + { tlocl (ATyp_constant $1) 1 1 } + | tid + { tloc (ATyp_id $1) } + | Lcurly id Rcurly + { tloc (ATyp_id $2) } + | tyvar + { tloc (ATyp_var $1) } + | Lparen exist_typ Rparen + { $2 } + +tup_typ_list: + | atomic_typ Comma atomic_typ + { [$1;$3] } + | atomic_typ Comma tup_typ_list + { $1::$3 } + +tup_typ: + | atomic_typ + { $1 } + | Lparen tup_typ_list Rparen + { tloc (ATyp_tup $2) } + +exist_typ: + | Exist tyvars Comma nexp_constraint Dot tup_typ + { tloc (ATyp_exist ($2, $4, $6)) } + | Exist tyvars Dot tup_typ + { tloc (ATyp_exist ($2, NC_aux (NC_true, loc ()), $4)) } + | tup_typ + { $1 } + +typ: + | exist_typ + { $1 } + | tup_typ MinusGt exist_typ Effect effect_typ + { tloc (ATyp_fn($1,$3,$5)) } + +lit: + | True + { lloc L_true } + | False + { lloc L_false } + | Num + { lloc (L_num $1) } + | String + { lloc (L_string $1) } + | Lparen Rparen + { lloc L_unit } + | Bin + { lloc (L_bin $1) } + | Hex + { lloc (L_hex $1) } + | Real + { lloc (L_real $1) } + | Undefined + { lloc L_undef } + | Bitzero + { lloc L_zero } + | Bitone + { lloc L_one } + +atomic_pat: + | lit + { ploc (P_lit $1) } + | Under + { ploc P_wild } + | Lparen pat As id Rparen + { ploc (P_as($2,$4)) } + | Lparen exist_typ Rparen atomic_pat + { ploc (P_typ($2,$4)) } + | id + { ploc (P_app($1,[])) } + | Lcurly fpats Rcurly + { ploc (P_record((fst $2, snd $2))) } + | Lsquare comma_pats Rsquare + { ploc (P_vector($2)) } + | Lsquare pat Rsquare + { ploc (P_vector([$2])) } + | Lsquare Rsquare + { ploc (P_vector []) } + | Lsquare npats Rsquare + { ploc (P_vector_indexed($2)) } + | Lparen comma_pats Rparen + { ploc (P_tup($2)) } + | SquareBarBar BarBarSquare + { ploc (P_list([])) } + | SquareBarBar pat BarBarSquare + { ploc (P_list([$2])) } + | SquareBarBar comma_pats BarBarSquare + { ploc (P_list($2)) } + | atomic_pat ColonColon pat + { ploc (P_cons ($1, $3)) } + | Lparen pat Rparen + { $2 } + +app_pat: + | atomic_pat + { $1 } + | 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 + { ([$1;$3]) } + | atomic_pat Colon pat_colons + { ($1::$3) } + +pat: + | app_pat + { $1 } + | pat_colons + { ploc (P_vector_concat($1)) } + +comma_pats: + | atomic_pat Comma atomic_pat + { [$1;$3] } + | atomic_pat Comma comma_pats + { $1::$3 } + +fpat: + | id Eq pat + { fploc (FP_Fpat($1,$3)) } + +fpats: + | fpat + { ([$1], false) } + | fpat Semi + { ([$1], true) } + | fpat Semi fpats + { ($1::fst $3, snd $3) } + +npat: + | Num Eq pat + { ($1,$3) } + +npats: + | npat + { [$1] } + | npat Comma npats + { ($1::$3) } + +atomic_exp: + | Lcurly semi_exps Rcurly + { eloc (E_block $2) } + | Nondet Lcurly semi_exps Rcurly + { eloc (E_nondet $3) } + | id + { eloc (E_id($1)) } + | lit + { eloc (E_lit($1)) } + | Lparen exp Rparen + { $2 } + | Lparen exist_typ Rparen atomic_exp + { eloc (E_cast($2,$4)) } + | Lparen comma_exps Rparen + { eloc (E_tuple($2)) } + | Lcurly exp With semi_exps Rcurly + { eloc (E_record_update($2,$4)) } + | Lsquare Rsquare + { eloc (E_vector([])) } + | Lsquare exp Rsquare + { eloc (E_vector([$2])) } + | Lsquare comma_exps Rsquare + { eloc (E_vector($2)) } + | Lsquare comma_exps Semi Default Eq exp Rsquare + { eloc (E_vector_indexed($2,(Def_val_aux(Def_val_dec $6, locn 3 6)))) } + | Lsquare exp With atomic_exp Eq exp Rsquare + { 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)) } + | SquareBarBar BarBarSquare + { eloc (E_list []) } + | SquareBarBar exp BarBarSquare + { eloc (E_list [$2]) } + | SquareBarBar comma_exps BarBarSquare + { eloc (E_list($2)) } + | Switch exp Lcurly case_exps Rcurly + { eloc (E_case($2,$4)) } + | Sizeof atomic_typ + { eloc (E_sizeof($2)) } + | Constraint Lparen nexp_constraint Rparen + { eloc (E_constraint $3) } + | Exit atomic_exp + { eloc (E_exit $2) } + | Return atomic_exp + { eloc (E_return $2) } + | Assert Lparen exp Comma exp Rparen + { eloc (E_assert ($3,$5)) } + +field_exp: + | atomic_exp + { $1 } + | atomic_exp Dot id + { eloc (E_field($1,$3)) } + +vaccess_exp: + | field_exp + { $1 } + | atomic_exp Lsquare exp Rsquare + { eloc (E_vector_access($1,$3)) } + | atomic_exp Lsquare exp DotDot exp Rsquare + { eloc (E_vector_subrange($1,$3,$5)) } + +app_exp: + | vaccess_exp + { $1 } + | id Lparen Rparen + { eloc (E_app($1, [eloc (E_lit (lloc L_unit))])) } + /* we wrap into a tuple here, but this is unwrapped in initial_check.ml */ + | id Lparen exp Rparen + { eloc (E_app($1,[ E_aux((E_tuple [$3]),locn 3 3)])) } + | id Lparen comma_exps Rparen + { eloc (E_app($1,[E_aux (E_tuple $3,locn 3 3)])) } + +right_atomic_exp: + | If_ exp Then exp Else exp + { eloc (E_if($2,$4,$6)) } + | If_ exp Then exp + { eloc (E_if($2,$4, eloc (E_lit(lloc L_unit)))) } + | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp In typ Rparen exp + { if $4 <> "from" then + raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop")); + if $6 <> "to" then + raise (Parse_error_locn ((loc ()),"Missing \"to\" in foreach loop")); + eloc (E_for($3,$5,$7,$9,$11,$13)) } + | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp Rparen exp + { if $4 <> "from" then + raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop")); + if $6 <> "to" && $6 <> "downto" then + raise (Parse_error_locn ((loc ()),"Missing \"to\" or \"downto\" in foreach loop")); + let order = + if $6 = "to" + then ATyp_aux(ATyp_inc,(locn 6 6)) + else ATyp_aux(ATyp_dec,(locn 6 6)) in + eloc (E_for($3,$5,$7,$9,order,$11)) } + | Foreach Lparen id Id atomic_exp Id atomic_exp Rparen exp + { if $4 <> "from" then + raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop")); + if $6 <> "to" && $6 <> "downto" then + raise (Parse_error_locn ((loc ()),"Missing \"to\" or \"downto\" in foreach loop")); + let step = eloc (E_lit(lloc (L_num 1))) in + let ord = + if $6 = "to" + then ATyp_aux(ATyp_inc,(locn 6 6)) + else ATyp_aux(ATyp_dec,(locn 6 6)) in + eloc (E_for($3,$5,$7,step,ord,$9)) } + | letbind In exp + { eloc (E_let($1,$3)) } + +starstar_exp: + | app_exp + { $1 } + | starstar_exp StarStar app_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + +/* this is where we diverge from the non-right_atomic path; + here we go directly to right_atomic whereas the other one + goes through app_exp, vaccess_exp and field_exp too. */ +starstar_right_atomic_exp: + | right_atomic_exp + { $1 } + | starstar_exp StarStar right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + +star_exp: + | starstar_exp + { $1 } + | star_exp Star starstar_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | star_exp Div starstar_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | star_exp Div_ starstar_exp + { eloc (E_app_infix($1,Id_aux(Id("div"), locn 2 2), $3)) } + | star_exp Quot starstar_exp + { eloc (E_app_infix($1,Id_aux(Id("quot"), locn 2 2), $3)) } + | star_exp QuotUnderS starstar_exp + { eloc (E_app_infix($1,Id_aux(Id("quot_s"), locn 2 2), $3)) } + | star_exp Rem starstar_exp + { eloc (E_app_infix($1,Id_aux(Id("rem"), locn 2 2), $3)) } + | star_exp Mod starstar_exp + { eloc (E_app_infix($1,Id_aux(Id("mod"), locn 2 2), $3)) } + | star_exp ModUnderS starstar_exp + { eloc (E_app_infix($1,Id_aux(Id("mod_s"), locn 2 2), $3)) } + | star_exp StarUnderS starstar_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | star_exp StarUnderSi starstar_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | star_exp StarUnderU starstar_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | star_exp StarUnderUi starstar_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + +star_right_atomic_exp: + | starstar_right_atomic_exp + { $1 } + | star_exp Star starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | star_exp Div starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | star_exp Div_ starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id("div"), locn 2 2), $3)) } + | star_exp Quot starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id("quot"), locn 2 2), $3)) } + | star_exp QuotUnderS starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id("quot_s"), locn 2 2), $3)) } + | star_exp Rem starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id("rem"), locn 2 2), $3)) } + | star_exp Mod starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id("mod"), locn 2 2), $3)) } + | star_exp ModUnderS starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id("mod_s"), locn 2 2), $3)) } + | star_exp StarUnderS starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | star_exp StarUnderSi starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | star_exp StarUnderU starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | star_exp StarUnderUi starstar_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + +plus_exp: + | star_exp + { $1 } + | plus_exp Plus star_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | plus_exp PlusUnderS star_exp + { eloc (E_app_infix($1, Id_aux(Id($2), locn 2 2), $3)) } + | plus_exp Minus star_exp + { eloc (E_app_infix($1,Id_aux(Id("-"), locn 2 2), $3)) } + | plus_exp MinusUnderS star_exp + { eloc (E_app_infix($1,Id_aux(Id("-_s"),locn 2 2), $3)) } + +plus_right_atomic_exp: + | star_right_atomic_exp + { $1 } + | plus_exp Plus star_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | plus_exp Minus star_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id("-"), locn 2 2), $3)) } + | plus_exp PlusUnderS star_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | plus_exp MinusUnderS star_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id("-_s"), locn 2 2), $3)) } + +shift_exp: + | plus_exp + { $1 } + | shift_exp GtGt plus_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | shift_exp GtGtGt plus_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | shift_exp LtLt plus_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | shift_exp LtLtLt plus_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + +shift_right_atomic_exp: + | plus_right_atomic_exp + { $1 } + | shift_exp GtGt plus_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | shift_exp GtGtGt plus_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | shift_exp LtLt plus_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | shift_exp LtLtLt plus_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + + +cons_exp: + | shift_exp + { $1 } + | shift_exp ColonColon cons_exp + { eloc (E_cons($1,$3)) } + | shift_exp Colon cons_exp + { eloc (E_vector_append($1, $3)) } + +cons_right_atomic_exp: + | shift_right_atomic_exp + { $1 } + | shift_exp ColonColon cons_right_atomic_exp + { eloc (E_cons($1,$3)) } + | shift_exp Colon cons_right_atomic_exp + { eloc (E_vector_append($1, $3)) } + +at_exp: + | cons_exp + { $1 } + | cons_exp At at_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | cons_exp CarrotCarrot at_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | cons_exp Carrot at_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | cons_exp TildeCarrot at_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + +at_right_atomic_exp: + | cons_right_atomic_exp + { $1 } + | cons_exp At at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | cons_exp CarrotCarrot at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | cons_exp Carrot at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | cons_exp TildeCarrot at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + +eq_exp: + | at_exp + { $1 } + /* XXX check for consistency */ + | eq_exp Eq at_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp EqEq at_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp ExclEq at_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp GtEq at_exp + { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp GtEqUnderS at_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp GtEqUnderU at_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp Gt at_exp + { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp GtUnderS at_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp GtUnderU at_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp LtEq at_exp + { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp LtEqUnderS at_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp Lt at_exp + { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp LtUnderS at_exp + { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp LtUnderSi at_exp + { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp LtUnderU at_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + /* XXX assignement should not have the same precedence as equal, + otherwise a := b > c requires extra parens... */ + | eq_exp ColonEq at_exp + { eloc (E_assign($1,$3)) } + +eq_right_atomic_exp: + | at_right_atomic_exp + { $1 } + | eq_exp Eq at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp EqEq at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp ExclEq at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp GtEq at_right_atomic_exp + { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp GtEqUnderS at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp GtEqUnderU at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp Gt at_right_atomic_exp + { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp GtUnderS at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp GtUnderU at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp LtEq at_right_atomic_exp + { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp LtEqUnderS at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp Lt at_right_atomic_exp + { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp LtUnderS at_right_atomic_exp + { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp LtUnderSi at_right_atomic_exp + { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp LtUnderU at_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp ColonEq at_right_atomic_exp + { eloc (E_assign($1,$3)) } + +and_exp: + | eq_exp + { $1 } + | eq_exp Amp and_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp AmpAmp and_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + +and_right_atomic_exp: + | eq_right_atomic_exp + { $1 } + | eq_exp Amp and_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + | eq_exp AmpAmp and_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) } + +or_exp: + | and_exp + { $1 } + | and_exp Bar or_exp + { eloc (E_app_infix($1,Id_aux(Id("|"), locn 2 2), $3)) } + | and_exp BarBar or_exp + { eloc (E_app_infix($1,Id_aux(Id("||"), locn 2 2), $3)) } + +or_right_atomic_exp: + | and_right_atomic_exp + { $1 } + | and_exp Bar or_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id("|"), locn 2 2), $3)) } + | and_exp BarBar or_right_atomic_exp + { eloc (E_app_infix($1,Id_aux(Id("||"), locn 2 2), $3)) } + +exp: + | or_exp + { $1 } + | or_right_atomic_exp + { $1 } + +comma_exps: + | exp Comma exp + { [$1;$3] } + | exp Comma comma_exps + { $1::$3 } + +semi_exps_help: + | exp + { [$1] } + | exp Semi + { [$1] } + | exp Semi semi_exps_help + { $1::$3 } + +semi_exps: + | + { [] } + | semi_exps_help + { $1 } + +case_exp: + | Case patsexp + { $2 } + +case_exps: + | case_exp + { [$1] } + | case_exp case_exps + { $1::$2 } + +patsexp: + | atomic_pat MinusGt exp + { peloc (Pat_exp($1,$3)) } + | atomic_pat When exp MinusGt exp + { peloc (Pat_when ($1, $3, $5)) } + +letbind: + | Let_ atomic_pat Eq exp + { lbloc (LB_val_implicit($2,$4)) } + | Let_ typquant atomic_typ atomic_pat Eq exp + { lbloc (LB_val_explicit((mk_typschm $2 $3 2 3),$4,$6)) } +/* This introduces one shift reduce conflict, that basically points out that an atomic_pat with a type declared is the Same as this + | Let_ Lparen typ Rparen atomic_pat Eq exp + { assert false (* lbloc (LB_val_explicit((mk_typschm (mk_typqn ()) $2 2 2),$3,$5)) *)} */ + +funcl: + | id atomic_pat Eq exp + { funclloc (FCL_Funcl($1,$2,$4)) } + +funcl_ands: + | funcl + { [$1] } + | funcl And funcl_ands + { $1::$3 } + +/* This causes ambiguity because without a type quantifier it's unclear whether the first id is a function name or a type name for the optional types.*/ +fun_def: + | Function_ Rec typquant typ Effect effect_typ funcl_ands + { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $6 6, $7)) } + | Function_ Rec typquant typ funcl_ands + { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) } + | Function_ Rec typ Effect effect_typ funcl_ands + { funloc (FD_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $5 5, $6)) } + | Function_ Rec Effect effect_typ funcl_ands + { funloc (FD_function(mk_rec 2,mk_tannotn (), mk_eannot $4 4, $5)) } + | Function_ Rec typ funcl_ands + { funloc (FD_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) } + | Function_ Rec funcl_ands + { funloc (FD_function(mk_rec 2, mk_tannotn (), mk_eannotn (), $3)) } + | Function_ typquant typ Effect effect_typ funcl_ands + { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannot $5 5, $6)) } + | Function_ typquant typ funcl_ands + { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) } + | Function_ typ Effect effect_typ funcl_ands + { funloc (FD_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $4 4, $5)) } + | Function_ Effect effect_typ funcl_ands + { funloc (FD_function(mk_recn (),mk_tannotn (), mk_eannot $3 3, $4)) } + | Function_ typ funcl_ands + { funloc (FD_function(mk_recn (),mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) } + | Function_ funcl_ands + { funloc (FD_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) } + + +val_spec: + | Val typquant typ id + { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4)) } + | Val typ id + { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3)) } + | Val Cast typquant typ id + { vloc (VS_cast_spec (mk_typschm $3 $4 3 4,$5)) } + | Val Cast typ id + { vloc (VS_cast_spec (mk_typschm (mk_typqn ()) $3 3 3, $4)) } + | Val Extern typquant typ id + { vloc (VS_extern_no_rename (mk_typschm $3 $4 3 4,$5)) } + | Val Extern typ id + { vloc (VS_extern_no_rename (mk_typschm (mk_typqn ()) $3 3 3, $4)) } + | Val Extern typquant typ id Eq String + { vloc (VS_extern_spec (mk_typschm $3 $4 3 4,$5,$7)) } + | Val Extern typ id Eq String + { vloc (VS_extern_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, $6)) } + +kinded_id: + | tyvar + { kiloc (KOpt_none $1) } + | kind tyvar + { kiloc (KOpt_kind($1,$2))} + +/*kinded_ids: + | kinded_id + { [$1] } + | kinded_id kinded_ids + { $1::$2 }*/ + +nums: + | Num + { [$1] } + | Num Comma nums + { $1::$3 } + +nexp_constraint: + | nexp_constraint1 + { $1 } + | nexp_constraint1 Bar nexp_constraint + { NC_aux (NC_or ($1, $3), loc ()) } + +nexp_constraint1: + | nexp_constraint2 + { $1 } + | nexp_constraint2 Amp nexp_constraint1 + { NC_aux (NC_and ($1, $3), loc ()) } + +nexp_constraint2: + | nexp_typ Eq nexp_typ + { NC_aux(NC_fixed($1,$3), loc () ) } + | nexp_typ ExclEq nexp_typ + { NC_aux (NC_not_equal ($1, $3), loc ()) } + | nexp_typ GtEq nexp_typ + { NC_aux(NC_bounded_ge($1,$3), loc () ) } + | nexp_typ LtEq nexp_typ + { NC_aux(NC_bounded_le($1,$3), loc () ) } + | tyvar In Lcurly nums Rcurly + { NC_aux(NC_nat_set_bounded($1,$4), loc ()) } + | tyvar IN Lcurly nums Rcurly + { NC_aux(NC_nat_set_bounded($1,$4), loc ()) } + | True + { NC_aux (NC_true, loc ()) } + | False + { NC_aux (NC_false, loc ()) } + | Lparen nexp_constraint Rparen + { $2 } + +id_constraint: + | nexp_constraint + { QI_aux((QI_const $1), loc())} + | kinded_id + { QI_aux((QI_id $1), loc()) } + +id_constraints: + | id_constraint + { [$1] } + | id_constraint Comma id_constraints + { $1::$3 } + +typquant: + | Forall id_constraints Dot + { typql(TypQ_tq($2)) } + +name_sect: + | Lsquare Id Eq String Rsquare + { + if $2 <> "name" then + raise (Parse_error_locn ((loc ()),"Unexpected id \""^$2^"\" in name_sect (should be \"name\")")); + Name_sect_aux(Name_sect_some($4), loc ()) } + +c_def_body: + | typ id + { [($1,$2)],false } + | typ id Semi + { [($1,$2)],true } + | typ id Semi c_def_body + { ($1,$2)::(fst $4), snd $4 } + +union_body: + | id + { [Tu_aux( Tu_id $1, loc())],false } + | typ id + { [Tu_aux( Tu_ty_id ($1,$2), loc())],false } + | id Semi + { [Tu_aux( Tu_id $1, loc())],true } + | 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 } + | 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)) } + | Num DotDot Num + { irloc (BF_range($1,$3)) } + | Lparen index_range Rparen + { $2 } + +enum_body: + | id + { [$1] } + | id Semi + { [$1] } + | id Semi enum_body + { $1::$3 } + +index_range: + | index_range_atomic + { $1 } + | index_range_atomic Comma index_range + { irloc(BF_concat($1,$3)) } + +r_id_def: + | index_range Colon id + { $1,$3 } + +r_def_body: + | r_id_def + { [$1] } + | r_id_def Semi + { [$1] } + | r_id_def Semi r_def_body + { $1::$3 } + +type_def: + | Typedef tid name_sect Eq typquant typ + { tdloc (TD_abbrev($2,$3,mk_typschm $5 $6 5 6)) } + | Typedef tid name_sect Eq typ + { tdloc (TD_abbrev($2,$3,mk_typschm (mk_typqn ()) $5 5 5)) } + | Typedef tid Eq typquant typ + { tdloc (TD_abbrev($2,mk_namesectn (), mk_typschm $4 $5 4 5))} + | 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 tid name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly + { tdloc (TD_record($2,$3,$7,fst $9, snd $9)) } + | Typedef tid name_sect Eq Const Struct Lcurly c_def_body Rcurly + { tdloc (TD_record($2,$3,(mk_typqn ()), fst $8, snd $8)) } + | Typedef tid Eq Const Struct typquant Lcurly c_def_body Rcurly + { tdloc (TD_record($2,mk_namesectn (), $6, fst $8, snd $8)) } + | Typedef tid Eq Const Struct Lcurly c_def_body Rcurly + { tdloc (TD_record($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) } + | Typedef tid name_sect Eq Const Union typquant Lcurly union_body Rcurly + { tdloc (TD_variant($2,$3, $7, fst $9, snd $9)) } + | Typedef tid Eq Const Union typquant Lcurly union_body Rcurly + { tdloc (TD_variant($2,mk_namesectn (), $6, fst $8, snd $8)) } + | Typedef tid name_sect Eq Const Union Lcurly union_body Rcurly + { tdloc (TD_variant($2, $3, mk_typqn (), fst $8, snd $8)) } + | Typedef tid Eq Const Union Lcurly union_body Rcurly + { tdloc (TD_variant($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) } + | Typedef tid Eq Enumerate Lcurly enum_body Rcurly + { tdloc (TD_enum($2, mk_namesectn (), $6,false)) } + | Typedef tid name_sect Eq Enumerate Lcurly enum_body Rcurly + { tdloc (TD_enum($2,$3,$7,false)) } + | Typedef tid Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly + { tdloc (TD_register($2, $7, $9, $12)) } + +default_typ: + | Default atomic_kind tyvar + { defloc (DT_kind($2,$3)) } + | Default atomic_kind Inc + { defloc (DT_order($2, tloc (ATyp_inc))) } + | Default atomic_kind Dec + { defloc (DT_order($2, tloc (ATyp_dec))) } + | Default typquant typ id + { defloc (DT_typ((mk_typschm $2 $3 2 3),$4)) } + | Default typ id + { defloc (DT_typ((mk_typschm (mk_typqn ()) $2 2 2),$3)) } + +scattered_def: + | Function_ Rec typquant typ Effect effect_typ id + { sdloc (SD_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $6 6, $7)) } + | Function_ Rec typ Effect effect_typ id + { sdloc (SD_scattered_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $5 5, $6)) } + | Function_ Rec typquant typ id + { sdloc (SD_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) } + | Function_ Rec Effect effect_typ id + { sdloc (SD_scattered_function (mk_rec 2, mk_tannotn (), mk_eannot $4 4, $5)) } + | Function_ Rec typ id + { sdloc (SD_scattered_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) } + | Function_ Rec id + { sdloc (SD_scattered_function(mk_rec 2,mk_tannotn (), mk_eannotn (),$3)) } + | Function_ typquant typ Effect effect_typ id + { sdloc (SD_scattered_function(mk_recn (),mk_tannot $2 $3 2 3, mk_eannot $5 5, $6)) } + | Function_ typ Effect effect_typ id + { sdloc (SD_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $4 4, $5)) } + | Function_ typquant typ id + { sdloc (SD_scattered_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannotn (), $4)) } + | Function_ Effect effect_typ id + { sdloc (SD_scattered_function(mk_recn (), mk_tannotn (), mk_eannot $3 3, $4)) } + | Function_ typ id + { 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 tid name_sect Eq Const Union typquant + { sdloc (SD_scattered_variant($2,$3,$7)) } + | Typedef tid Eq Const Union typquant + { sdloc (SD_scattered_variant($2,(mk_namesectn ()),$6)) } + | Typedef tid name_sect Eq Const Union + { sdloc (SD_scattered_variant($2,$3,mk_typqn ())) } + | Typedef tid Eq Const Union + { sdloc (SD_scattered_variant($2,mk_namesectn (),mk_typqn ())) } + +ktype_def: + | Def kind tid name_sect Eq typquant typ + { kdloc (KD_abbrev($2,$3,$4,mk_typschm $6 $7 6 7)) } + | Def kind tid name_sect Eq typ + { kdloc (KD_abbrev($2,$3,$4,mk_typschm (mk_typqn ()) $6 6 6)) } + | Def kind tid Eq typquant typ + { kdloc (KD_abbrev($2,$3,mk_namesectn (), mk_typschm $5 $6 5 6)) } + | Def kind tid Eq typ + { kdloc (KD_abbrev($2,$3,mk_namesectn (),mk_typschm (mk_typqn ()) $5 5 5)) } + | Def kind tid Eq Num + { kdloc (KD_abbrev($2,$3,mk_namesectn (),mk_typschm (mk_typqn ()) (tlocl (ATyp_constant $5) 5 5) 5 5)) } + | Def kind tid name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly + { kdloc (KD_record($2,$3,$4,$8,fst $10, snd $10)) } + | Def kind tid name_sect Eq Const Struct Lcurly c_def_body Rcurly + { kdloc (KD_record($2,$3,$4,(mk_typqn ()), fst $9, snd $9)) } + | Def kind tid Eq Const Struct typquant Lcurly c_def_body Rcurly + { kdloc (KD_record($2,$3,mk_namesectn (), $7, fst $9, snd $9)) } + | Def kind tid Eq Const Struct Lcurly c_def_body Rcurly + { kdloc (KD_record($2,$3, mk_namesectn (), mk_typqn (), fst $8, snd $8)) } + | Def kind tid name_sect Eq Const Union typquant Lcurly union_body Rcurly + { kdloc (KD_variant($2,$3,$4, $8, fst $10, snd $10)) } + | Def kind tid Eq Const Union typquant Lcurly union_body Rcurly + { kdloc (KD_variant($2,$3,mk_namesectn (), $7, fst $9, snd $9)) } + | Def kind tid name_sect Eq Const Union Lcurly union_body Rcurly + { kdloc (KD_variant($2, $3,$4, mk_typqn (), fst $9, snd $9)) } + | Def kind tid Eq Const Union Lcurly union_body Rcurly + { kdloc (KD_variant($2,$3, mk_namesectn (), mk_typqn (), fst $8, snd $8)) } + | Def kind tid Eq Enumerate Lcurly enum_body Rcurly + { kdloc (KD_enum($2,$3, mk_namesectn (), $7,false)) } + | Def kind tid name_sect Eq Enumerate Lcurly enum_body Rcurly + { kdloc (KD_enum($2,$3,$4,$8,false)) } + | Def kind tid Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly + { kdloc (KD_register($2,$3, $8, $10, $13)) } + + +def: + | type_def + { dloc (DEF_type($1)) } + | ktype_def + { dloc (DEF_kind($1)) } + | fun_def + { dloc (DEF_fundef($1)) } + | letbind + { dloc (DEF_val($1)) } + | val_spec + { dloc (DEF_spec($1)) } + | default_typ + { dloc (DEF_default($1)) } + | Overload id Lsquare enum_body Rsquare + { dloc (DEF_overload($2,$4)) } + | Register typ id + { dloc (DEF_reg_dec(DEC_aux(DEC_reg($2,$3),loc ()))) } + | Register Alias id Eq exp + { dloc (DEF_reg_dec(DEC_aux(DEC_alias($3,$5),loc ()))) } + | Register Alias typ id Eq exp + { dloc (DEF_reg_dec(DEC_aux(DEC_typ_alias($3,$4,$6), loc ()))) } + | Scattered scattered_def + { dloc (DEF_scattered $2) } + | Function_ Clause funcl + { dloc (DEF_scattered (sdloc (SD_scattered_funcl($3)))) } + | Union tid Member typ id + { dloc (DEF_scattered (sdloc (SD_scattered_unioncl($2,Tu_aux(Tu_ty_id($4,$5), locn 4 5))))) } + | 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 + { [$1] } + | def defs_help + { $1::$2 } + +defs: + | defs_help + { (Defs $1) } + +file: + | defs Eof + { $1 } + +nonempty_exp_list: + | semi_exps_help Eof { $1 } + diff --git a/src/process_file.ml b/src/process_file.ml index c9a4f178..91262ce9 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -40,6 +40,8 @@ (* SUCH DAMAGE. *) (**************************************************************************) +let opt_new_parser = ref false + type out_type = | Lem_ast_out | Lem_out of string option @@ -71,7 +73,11 @@ let parse_file (f : string) : Parse_ast.defs = close_in in_chan; let lexbuf, in_chan = get_lexbuf f in try - let ast = Parser.file Lexer.token lexbuf in + let ast = + if !opt_new_parser + then Parser2.file Lexer2.token lexbuf + else Parser.file Lexer.token lexbuf + in close_in in_chan; ast with | Parsing.Parse_error -> @@ -90,7 +96,6 @@ let load_file order env f = let ast = convert_ast order (parse_file f) in Type_check.check env ast -let opt_new_typecheck = ref false let opt_just_check = ref false let opt_ddump_tc_ast = ref false let opt_dno_cast = ref false diff --git a/src/process_file.mli b/src/process_file.mli index 9907b743..1cf710bc 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -51,7 +51,7 @@ val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val load_file_no_check : Ast.order -> string -> unit Ast.defs val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t -val opt_new_typecheck : bool ref +val opt_new_parser : bool ref val opt_just_check : bool ref val opt_ddump_tc_ast : bool ref val opt_dno_cast : bool ref diff --git a/src/sail.ml b/src/sail.ml index c7c14a67..d03060dc 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -88,11 +88,11 @@ let options = Arg.align ([ | [fname;line;var] -> opt_mono_split := ((fname,int_of_string line),var)::!opt_mono_split | _ -> raise (Arg.Bad (s ^ " not of form <filename>:<line>:<variable>"))), "<filename>:<line>:<variable> to case split for monomorphisation"); - ( "-new_typecheck", - Arg.Set opt_new_typecheck, - " (experimental) use new typechecker with Z3 constraint solving"); + ( "-new_parser", + Arg.Set Process_file.opt_new_parser, + " (experimental) use new parser"); ( "-just_check", - Arg.Tuple [Arg.Set opt_new_typecheck; Arg.Set opt_just_check], + Arg.Set opt_just_check, " (experimental) terminate immediately after typechecking, implies -new_typecheck"); ( "-ddump_tc_ast", Arg.Set opt_ddump_tc_ast, diff --git a/src/type_check.ml b/src/type_check.ml index ff65c453..bd2db570 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -133,8 +133,11 @@ let unit_typ = mk_id_typ (mk_id "unit") let bit_typ = mk_id_typ (mk_id "bit") let real_typ = mk_id_typ (mk_id "real") let app_typ id args = mk_typ (Typ_app (id, args)) -let atom_typ nexp = mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))])) -let range_typ nexp1 nexp2 = mk_typ (Typ_app (mk_id "range", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp1)); mk_typ_arg (Typ_arg_nexp (nexp_simp nexp2))])) +let atom_typ nexp = + mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))])) +let range_typ nexp1 nexp2 = + mk_typ (Typ_app (mk_id "range", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp1)); + mk_typ_arg (Typ_arg_nexp (nexp_simp nexp2))])) let bool_typ = mk_id_typ (mk_id "bool") let string_typ = mk_id_typ (mk_id "string") let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)])) @@ -175,7 +178,6 @@ let nc_false = mk_nc NC_false let mk_lit l = E_aux (E_lit (L_aux (l, Parse_ast.Unknown)), (Parse_ast.Unknown, ())) -(* FIXME: Can now negate all n_constraints *) let rec nc_negate (NC_aux (nc, _)) = match nc with | NC_bounded_ge (n1, n2) -> nc_lt n1 n2 @@ -232,6 +234,18 @@ let quant_items : typquant -> quant_item list = function | TypQ_aux (TypQ_tq qis, _) -> qis | TypQ_aux (TypQ_no_forall, _) -> [] +let quant_split typq = + let qi_kopt = function + | QI_aux (QI_id kopt, _) -> [kopt] + | _ -> [] + in + let qi_nc = function + | QI_aux (QI_const nc, _) -> [nc] + | _ -> [] + in + let qis = quant_items typq in + List.concat (List.map qi_kopt qis), List.concat (List.map qi_nc qis) + let kopt_kid (KOpt_aux (kopt_aux, _)) = match kopt_aux with | KOpt_none kid | KOpt_kind (_, kid) -> kid @@ -405,8 +419,8 @@ module Env : sig val add_typ_var : kid -> base_kind_aux -> t -> t val get_ret_typ : t -> typ option val add_ret_typ : typ -> t -> t - val add_typ_synonym : id -> (typ_arg list -> typ) -> t -> t - val get_typ_synonym : id -> t -> typ_arg list -> typ + val add_typ_synonym : id -> (t -> typ_arg list -> typ) -> t -> t + val get_typ_synonym : id -> t -> t -> typ_arg list -> typ val add_overloads : id -> id list -> t -> t val get_overloads : id -> t -> id list val get_default_order : t -> order @@ -433,7 +447,7 @@ end = struct regtyps : (int * int * (index_range * id) list) Bindings.t; variants : (typquant * type_union list) Bindings.t; typ_vars : base_kind_aux KBindings.t; - typ_synonyms : (typ_arg list -> typ) Bindings.t; + typ_synonyms : (t -> typ_arg list -> typ) Bindings.t; overloads : (id list) Bindings.t; flow : (typ -> typ) Bindings.t; enums : IdSet.t Bindings.t; @@ -831,7 +845,7 @@ end = struct begin try let synonym = Bindings.find id env.typ_synonyms in - expand_synonyms env (synonym args) + expand_synonyms env (synonym env args) with | Not_found -> Typ_aux (Typ_app (id, List.map (expand_synonyms_arg env) args), l) end @@ -839,7 +853,7 @@ end = struct begin try let synonym = Bindings.find id env.typ_synonyms in - expand_synonyms env (synonym []) + expand_synonyms env (synonym env []) with | Not_found -> Typ_aux (Typ_id id, l) end @@ -912,7 +926,7 @@ let lvector_typ env l typ = let initial_env = Env.empty - |> Env.add_typ_synonym (mk_id "atom") (fun args -> mk_typ (Typ_app (mk_id "range", args @ args))) + |> Env.add_typ_synonym (mk_id "atom") (fun _ args -> mk_typ (Typ_app (mk_id "range", args @ args))) let ex_counter = ref 0 @@ -952,6 +966,12 @@ let destruct_vector_typ env typ = (* 3. Subtyping and constraint solving *) (**************************************************************************) +let rec simp_typ (Typ_aux (typ_aux, l)) = Typ_aux (simp_typ_aux typ_aux, l) +and simp_typ_aux = function + | Typ_exist (kids1, nc1, Typ_aux (Typ_exist (kids2, nc2, typ), _)) -> + Typ_exist (kids1 @ kids2, nc_and nc1 nc2, typ) + | typ_aux -> typ_aux + let order_eq (Ord_aux (ord_aux1, _)) (Ord_aux (ord_aux2, _)) = match ord_aux1, ord_aux2 with | Ord_inc, Ord_inc -> true @@ -971,7 +991,6 @@ type tnf = | Tnf_tup of tnf list | Tnf_index_sort of index_sort | Tnf_app of id * tnf_arg list - | Tnf_exist of kid list * n_constraint * tnf and tnf_arg = | Tnf_arg_nexp of nexp | Tnf_arg_typ of tnf @@ -987,8 +1006,6 @@ let rec string_of_tnf = function | Tnf_index_sort IS_int -> "INT" | Tnf_index_sort (IS_prop (kid, props)) -> "{" ^ string_of_kid kid ^ " | " ^ string_of_list " & " (fun (n1, n2) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2) props ^ "}" - | Tnf_exist (kids, nc, tnf) -> - "exist " ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_tnf tnf and string_of_tnf_arg = function | Tnf_arg_nexp n -> string_of_nexp n | Tnf_arg_typ tnf -> string_of_tnf tnf @@ -1003,7 +1020,7 @@ let rec normalize_typ env (Typ_aux (typ, l)) = let kid = Env.fresh_kid env in Tnf_index_sort (IS_prop (kid, [(nconstant 0, nvar kid)])) | Typ_id v -> begin - try normalize_typ env (Env.get_typ_synonym v env []) with + try normalize_typ env (Env.get_typ_synonym v env env []) with | Not_found -> Tnf_id v end | Typ_var kid -> Tnf_var kid @@ -1016,10 +1033,10 @@ let rec normalize_typ env (Typ_aux (typ, l)) = Tnf_app (vector, List.map (normalize_typ_arg env) args) | Typ_app (id, args) -> begin - try normalize_typ env (Env.get_typ_synonym id env args) with + try normalize_typ env (Env.get_typ_synonym id env env args) with | Not_found -> Tnf_app (id, List.map (normalize_typ_arg env) args) end - | Typ_exist (kids, nc, typ) -> Tnf_exist (kids, nc, normalize_typ env typ) + | Typ_exist (kids, nc, typ) -> typ_error l "Cannot normalise existential type" | Typ_fn _ -> typ_error l ("Cannot normalize function type " ^ string_of_typ (Typ_aux (typ, l))) and normalize_typ_arg env (Typ_arg_aux (typ_arg, _)) = match typ_arg with @@ -1168,10 +1185,6 @@ let rec subtyp_tnf env tnf1 tnf2 = | Constraint.Unknown [] -> typ_debug "sat"; false | Constraint.Unknown _ -> typ_debug "unknown"; false end - | Tnf_exist (kids, nc, tnf1), _ -> - let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in - let env = Env.add_constraint nc env in - subtyp_tnf env tnf1 tnf2 | _, _ -> false and tnf_args_eq env arg1 arg2 = @@ -1457,9 +1470,13 @@ let uv_nexp_constraint env (kid, uvar) = | U_nexp nexp -> Env.add_constraint (nc_eq (nvar kid) nexp) env | _ -> env -let subtyp l env typ1 typ2 = - match destructure_exist env typ2 with - | Some (kids, nc, typ2) -> +let rec subtyp l env typ1 typ2 = + match destructure_exist env typ1, destructure_exist env typ2 with + | Some (kids, nc, typ1), _ -> + let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in + let env = Env.add_constraint nc env in + subtyp l env typ1 typ2 + | _, Some (kids, nc, typ2) -> let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in let unifiers, existential_kids, existential_nc = try unify l env typ2 typ1 with @@ -1475,7 +1492,7 @@ let subtyp l env typ1 typ2 = in if prove env nc then () else typ_error l ("Could not show " ^ string_of_typ typ1 ^ " is a subset of existential " ^ string_of_typ typ2) - | None -> + | _, None -> if subtyp_tnf env (normalize_typ env typ1) (normalize_typ env typ2) then () else typ_error l (string_of_typ typ1 @@ -1719,6 +1736,8 @@ let rec match_typ env typ1 typ2 = let Typ_aux (typ1_aux, _) = Env.expand_synonyms env typ1 in let Typ_aux (typ2_aux, _) = Env.expand_synonyms env typ2 in match typ1_aux, typ2_aux with + | Typ_exist (_, _, typ1), _ -> match_typ env typ1 typ2 + | _, Typ_exist (_, _, typ2) -> match_typ env typ1 typ2 | Typ_wild, Typ_wild -> true | _, Typ_var kid2 -> true | Typ_id v1, Typ_id v2 when Id.compare v1 v2 = 0 -> true @@ -1915,7 +1934,7 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ = in begin try - typ_debug "PERFORMING TYPE COERCION"; + typ_debug ("PERFORMING TYPE COERCION: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ); subtyp l env (typ_of annotated_exp) typ; annotated_exp with | Type_error (_, m) when Env.allow_casts env -> @@ -2482,9 +2501,9 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = end | (utyps, (typ :: typs)), (uargs, ((n, arg) :: args)) -> begin - typ_debug ("INSTANTIATE: " ^ string_of_exp arg ^ " with " ^ string_of_typ typ ^ " NF " ^ string_of_tnf (normalize_typ env typ)); + typ_debug ("INSTANTIATE: " ^ string_of_exp arg ^ " with " ^ string_of_typ typ); let iarg = irule infer_exp env arg in - typ_debug ("INFER: " ^ string_of_exp arg ^ " type " ^ string_of_typ (typ_of iarg) ^ " NF " ^ string_of_tnf (normalize_typ env (typ_of iarg))); + typ_debug ("INFER: " ^ string_of_exp arg ^ " type " ^ string_of_typ (typ_of iarg)); try let iarg, (unifiers, ex_kids, ex_nc) (* FIXME *) = type_coercion_unify env iarg typ in typ_debug (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers)); @@ -2557,12 +2576,12 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = typ_debug ("Existentials: " ^ string_of_list ", " string_of_kid existentials); typ_debug ("Existential constraints: " ^ string_of_list ", " string_of_n_constraint ex_constraints); - let nc_true = nc_eq (nconstant 0) (nconstant 0) in let typ_ret = - if KidSet.is_empty (KidSet.inter (typ_frees typ_ret) (KidSet.of_list existentials)) - then typ_ret + if KidSet.is_empty (KidSet.of_list existentials) + then (typ_debug "Returning Existential"; typ_ret) else mk_typ (Typ_exist (existentials, List.fold_left nc_and nc_true ex_constraints, typ_ret)) in + let typ_ret = simp_typ typ_ret in let exp = annot_exp (E_app (f, xs_reordered)) typ_ret eff in typ_debug ("RETURNING: " ^ string_of_typ (typ_of exp)); match ret_ctx_typ with @@ -2940,11 +2959,35 @@ let check_type_union env variant typq (Tu_aux (tu, l)) = | Tu_id v -> Env.add_union_id v (typq, ret_typ) env | Tu_ty_id (typ, v) -> Env.add_val_spec v (typq, mk_typ (Typ_fn (typ, ret_typ, no_effect))) env +let mk_synonym typq typ = + let kopts, ncs = quant_split typq in + let rec subst_args kopts args = + match kopts, args with + | kopt :: kopts, Typ_arg_aux (Typ_arg_nexp arg, _) :: args when is_nat_kopt kopt -> + let typ, ncs = subst_args kopts args in + typ_subst_nexp (kopt_kid kopt) (unaux_nexp arg) typ, + List.map (nc_subst_nexp (kopt_kid kopt) (unaux_nexp arg)) ncs + | kopt :: kopts, Typ_arg_aux (Typ_arg_typ arg, _) :: args when is_typ_kopt kopt -> + let typ, ncs = subst_args kopts args in + typ_subst_typ (kopt_kid kopt) (unaux_typ arg) typ, ncs + | kopt :: kopts, Typ_arg_aux (Typ_arg_order arg, _) :: args when is_order_kopt kopt -> + let typ, ncs = subst_args kopts args in + typ_subst_order (kopt_kid kopt) (unaux_order arg) typ, ncs + | [], [] -> typ, ncs + | _, Typ_arg_aux (_, l) :: _ -> typ_error l "Synonym applied to bad arguments" + | _, _ -> typ_error Parse_ast.Unknown "Synonym applied to bad arguments" + in + fun env args -> + let typ, ncs = subst_args kopts args in + if List.for_all (prove env) ncs + then typ + else typ_error Parse_ast.Unknown "Could not prove constraints in type synonym" + let check_typedef env (TD_aux (tdef, (l, _))) = let td_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented Typedef") in match tdef with | TD_abbrev(id, nmscm, (TypSchm_aux (TypSchm_ts (typq, typ), _))) -> - [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (fun _ -> typ) env + [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (mk_synonym typq typ) env | TD_record(id, nmscm, typq, fields, _) -> [DEF_type (TD_aux (tdef, (l, None)))], Env.add_record id typq fields env | TD_variant(id, nmscm, typq, arms, _) -> diff --git a/src/type_check.mli b/src/type_check.mli index ce66aba3..de825d06 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -97,7 +97,7 @@ module Env : sig any exceptions. *) val get_ret_typ : t -> typ option - val get_typ_synonym : id -> t -> typ_arg list -> typ + val get_typ_synonym : id -> t -> (t -> typ_arg list -> typ) val get_overloads : id -> t -> id list diff --git a/test/typecheck/pass/exint.sail b/test/typecheck/pass/exint.sail new file mode 100644 index 00000000..dfe51eb9 --- /dev/null +++ b/test/typecheck/pass/exint.sail @@ -0,0 +1,22 @@ + +typedef Int = exist 'n. [:'n:] + +val ([:'n:], [:'m:]) -> exist 'o, 'o = 'n + 'm. [:'o:] effect pure add + +val ([:'n:], [:'m:]) -> exist 'o, 'o = 'n * 'm. [:'o:] effect pure mult + +overload (deinfix +) [add] + +overload (deinfix * ) [mult] + +let x = 3 + 4 + +let y = x + x * x + +let ([:7 * 8:]) z = y + +typedef Range = forall Num 'n, Num 'm, 'n <= 'm. exist 'o, 'n <= 'o & 'o <= 'm. [:'o:] + +let (Range<3,4>) a = 3 + +let (Range<2,5>) b = a + 1
\ No newline at end of file |