From 90bfc9c8e401e41a2f4616b84976a57f357664df Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 5 Jan 2018 17:50:39 +0000 Subject: Removed legacy parser/lexer and pretty printer --- src/lexer.mll | 372 ------------- src/parser.mly | 1358 ---------------------------------------------- src/pre_lexer.mll | 205 ------- src/pre_parser.mly | 94 ---- src/pretty_print.ml | 1 - src/pretty_print.mli | 5 - src/pretty_print_sail.ml | 536 ------------------ src/process_file.ml | 35 +- src/process_file.mli | 1 - src/sail.ml | 5 +- 10 files changed, 4 insertions(+), 2608 deletions(-) delete mode 100644 src/lexer.mll delete mode 100644 src/parser.mly delete mode 100644 src/pre_lexer.mll delete mode 100644 src/pre_parser.mly delete mode 100644 src/pretty_print_sail.ml (limited to 'src') diff --git a/src/lexer.mll b/src/lexer.mll deleted file mode 100644 index 814e645e..00000000 --- a/src/lexer.mll +++ /dev/null @@ -1,372 +0,0 @@ -(**************************************************************************) -(* Sail *) -(* *) -(* Copyright (c) 2013-2017 *) -(* Kathyrn Gray *) -(* Shaked Flur *) -(* Stephen Kell *) -(* Gabriel Kerneis *) -(* Robert Norton-Wright *) -(* Christopher Pulte *) -(* Peter Sewell *) -(* Alasdair Armstrong *) -(* Brian Campbell *) -(* Thomas Bauereiss *) -(* Anthony Fox *) -(* Jon French *) -(* Dominic Mulligan *) -(* Stephen Kell *) -(* Mark Wassell *) -(* *) -(* 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 Parser -module Big_int = Nat_big_num -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)); - ("try", (fun _ -> Try)); - ("catch", (fun _ -> Catch)); - ("throw", (fun _ -> Throw)); - ("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)); - ("repeat", (fun x -> Repeat)); - ("until", (fun x -> Until)); - ("while", (fun x -> While)); - ("do", (fun x -> Do)); - ("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(Big_int.of_string i)) } - | "-" digit+ as i { (Num(Big_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/parser.mly b/src/parser.mly deleted file mode 100644 index d2a5933a..00000000 --- a/src/parser.mly +++ /dev/null @@ -1,1358 +0,0 @@ -/**************************************************************************/ -/* Sail */ -/* */ -/* Copyright (c) 2013-2017 */ -/* Kathyrn Gray */ -/* Shaked Flur */ -/* Stephen Kell */ -/* Gabriel Kerneis */ -/* Robert Norton-Wright */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alasdair Armstrong */ -/* Brian Campbell */ -/* Thomas Bauereiss */ -/* Anthony Fox */ -/* Jon French */ -/* Dominic Mulligan */ -/* Stephen Kell */ -/* Mark Wassell */ -/* */ -/* 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 *) - -module Big_int = Nat_big_num -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 id_of_kid = function - | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l) - -let idl i = Id_aux(i, loc()) - -let string_of_id = function - | Id_aux (Id str, _) -> str - | Id_aux (DeIid str, _) -> str - -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(Big_int.zero), 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 (Big_int.add (Big_int.sub t b) (Big_int.of_int 1)),l) - | bot,(ATyp_aux(_,l) as top) -> - ATyp_aux((ATyp_sum ((ATyp_aux (ATyp_sum (top, ATyp_aux(ATyp_constant (Big_int.of_int 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 Big_int.zero,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 (Big_int.sub t (Big_int.of_int 1)),l) - | (true,true,ATyp_aux(_, l)) -> zero,ATyp_aux (ATyp_sum (typ1, - ATyp_aux(ATyp_neg(ATyp_aux(ATyp_constant (Big_int.of_int 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 Try Catch Throw -%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape -%token While Do Repeat Until - - -/* 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 Id TyVar TyId -%token Num -%token String Bin Hex Real - -%token Amp At Carrot Div Eq Excl Gt Lt Plus Star Tilde -%token AmpAmp CarrotCarrot Colon ColonColon EqEq ExclEq ExclExcl -%token GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt -%token LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar TildeCarrot - -%token GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS -%token GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU -%token LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarStarUnderS StarStarUnderSi StarUnderS -%token StarUnderSi StarUnderU StarUnderUi TwoCarrot PlusUnderS MinusUnderS - -%token AmpI AtI CarrotI DivI EqI ExclI GtI LtI PlusI StarI TildeI -%token AmpAmpI CarrotCarrotI ColonColonI EqEqI ExclEqI ExclExclI -%token GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI -%token LtEqI LtEqPlusI LtGtI LtLtI LtLtLtI LtPlusI StarStarI TildeCarrotI - -%token GtEqUnderSI GtEqUnderSiI GtEqUnderUI GtEqUnderUiI GtGtUnderUI GtUnderSI -%token GtUnderSiI GtUnderUI GtUnderUiI LtEqUnderSI LtEqUnderSiI LtEqUnderUI -%token LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarStarUnderSI StarStarUnderSiI StarUnderSI -%token StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI - - -%start file nonempty_exp_list -%type defs -%type typ -%type pat -%type exp -%type nonempty_exp_list -%type 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 } - -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,[])) } - | tyvar - { ploc (P_var (ploc (P_id (id_of_kid $1)), $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 []) } - | Lparen comma_pats Rparen - { ploc (P_tup($2)) } - | SquareBarBar BarBarSquare - { ploc (P_list([])) } - | SquareBarBar pat BarBarSquare - { ploc (P_list([$2])) } - | SquareBarBar semi_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 } - -semi_pats: - | atomic_pat Semi atomic_pat - { [$1;$3] } - | atomic_pat Semi semi_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 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)) } - | Try exp Catch Lcurly case_exps Rcurly - { eloc (E_try ($2, $5)) } - | Sizeof atomic_typ - { eloc (E_sizeof($2)) } - | Constraint Lparen nexp_constraint Rparen - { eloc (E_constraint $3) } - | Throw atomic_exp - { eloc (E_throw $2) } - | 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 (Big_int.of_int 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)) } - | While exp Do exp - { eloc (E_loop (While, $2, $4)) } - | 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($2,$4)) } - -patsexp_funcl: - | atomic_pat Eq exp - { peloc (Pat_exp($1,$3)) } - | Lparen atomic_pat When exp Rparen Eq exp - { peloc (Pat_when ($2, $4, $7)) } - -funcl: - | id patsexp_funcl - { funclloc (FCL_Funcl($1,$2)) } - -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, (fun _ -> None), false)) } - | Val typ id - { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3, (fun _ -> None), false)) } - | Val Cast typquant typ id - { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, (fun _ -> None), true)) } - | Val Cast typ id - { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, (fun _ -> None), true)) } - | Val Extern typquant typ id - { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, (fun _ -> Some (string_of_id $5)), false)) } - | Val Extern typ id - { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, (fun _ -> Some (string_of_id $4)), false)) } - | Val Extern typquant typ id Eq String - { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, (fun _ -> Some $7), false)) } - | Val Extern typ id Eq String - { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, (fun _ -> Some $6), false)) } - | Val Cast Extern typquant typ id - { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, (fun _ -> Some (string_of_id $6)), true)) } - | Val Cast Extern typ id - { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4, $5, (fun _ -> Some (string_of_id $5)), true)) } - | Val Cast Extern typquant typ id Eq String - { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, (fun _ -> Some $8), true)) } - | Val Cast Extern typ id Eq String - { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4,$5, (fun _ -> Some $7), true)) } - -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_equal($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_set($1,$4), loc ()) } - | tyvar IN Lcurly nums Rcurly - { NC_aux(NC_set($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)) } - -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: - | 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/pre_lexer.mll b/src/pre_lexer.mll deleted file mode 100644 index 3c308b99..00000000 --- a/src/pre_lexer.mll +++ /dev/null @@ -1,205 +0,0 @@ -(**************************************************************************) -(* Sail *) -(* *) -(* Copyright (c) 2013-2017 *) -(* Kathyrn Gray *) -(* Shaked Flur *) -(* Stephen Kell *) -(* Gabriel Kerneis *) -(* Robert Norton-Wright *) -(* Christopher Pulte *) -(* Peter Sewell *) -(* Alasdair Armstrong *) -(* Brian Campbell *) -(* Thomas Bauereiss *) -(* Anthony Fox *) -(* Jon French *) -(* Dominic Mulligan *) -(* Stephen Kell *) -(* Mark Wassell *) -(* *) -(* 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 Pre_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 _ -> 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)); - ("return", (fun x -> Other)); - ("scattered", (fun x -> Other)); - ("struct", (fun x -> Other)); - ("sizeof", (fun x -> Other)); - ("switch", (fun x -> Other)); - ("then", (fun x -> Other)); - ("true", (fun x -> Other)); - ("Type", (fun x -> Other)); - ("typedef", (fun x -> Typedef)); - ("def", (fun x -> Def)); - ("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 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 } - - | "2**" | "&" | "@" | "|" | "^" | ":" | "," | "." | "/" | "=" | "!" | ">" | "-" | "<" | - "+" | ";" | "*" | "~" | "_" | "{" | "}" | "(" | ")" | "[" | "]" | "&&" | "||" | "|]" | "||]" | - "^^" | "::" | ":>" | ":=" | ".." | "=/=" | "==" | "!=" | "!!" | ">=" | ">=+" | ">>" | ">>>" | ">+" | - "#>>" | "#<<" | "->" | "<:" | "<=" | "<=+" | "<>" | "<<" | "<<<" | "<+" | "**" | "~^" | ">=_s" | - ">=_si" | ">=_u" | ">=_ui" | ">>_u" | ">_s" | ">_si" | ">_u" | ">_ui" | "<=_s" | "<=_si" | - "<=_u" | "<=_ui" | "<_s" | "<_si" | "<_u" | "<_ui" | "**_s" | "**_si" | "*_u" | "*_ui"| "2^" { Other } - - - | "(*" { 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) } - | tyvar_start startident ident* { Other } - | "&" oper_char+ | "@" oper_char+ | "^" oper_char+ | "/" oper_char+ | "=" oper_char+ | - "!" oper_char+ | ">" oper_char+ | "<" oper_char+ | "+" oper_char+ | "*" oper_char+ | - "~" oper_char+ | "&&" oper_char+ | "^^" oper_char+| "::" oper_char+| "=/=" oper_char+ | - "==" oper_char+ | "!=" oper_char+ | "!!" oper_char+ | ">=" oper_char+ | ">=+" oper_char+ | - ">>" oper_char+ | ">>>" oper_char+ | ">+" oper_char+ | "#>>" oper_char+ | "#<<" oper_char+ | - "<=" oper_char+ | "<=+" oper_char+ | "<<" oper_char+ | "<<<" oper_char+ | "<+" oper_char+ | - "**" oper_char+ | "~^" oper_char+ | ">=_s" oper_char+ | ">=_si" oper_char+ | ">=_u" oper_char+ | - ">=_ui" oper_char+ | ">>_u" oper_char+ | ">_s" oper_char+ | ">_si" oper_char+| ">_u" oper_char+ | - ">_ui" oper_char+ | "<=_s" oper_char+ | "<=_si" oper_char+ | "<=_u" oper_char+ | "<=_ui" oper_char+ | - "<_s" oper_char+ | "<_si" oper_char+ | "<_u" oper_char+ | "<_ui" oper_char+ | "**_s" oper_char+ | - "**_si" oper_char+ | "*_u" oper_char+ | "*_ui" oper_char+ | "2^" oper_char+ { Other } - | digit+ { Other } - | "0b" (binarydigit+) { Other } - | "0x" (hexdigit+) { Other } - | '"' { let _ = 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)) } - - -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 deleted file mode 100644 index 0b4833a1..00000000 --- a/src/pre_parser.mly +++ /dev/null @@ -1,94 +0,0 @@ -/**************************************************************************/ -/* Sail */ -/* */ -/* Copyright (c) 2013-2017 */ -/* Kathyrn Gray */ -/* Shaked Flur */ -/* Stephen Kell */ -/* Gabriel Kerneis */ -/* Robert Norton-Wright */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alasdair Armstrong */ -/* Brian Campbell */ -/* Thomas Bauereiss */ -/* Anthony Fox */ -/* Jon French */ -/* Dominic Mulligan */ -/* Stephen Kell */ -/* Mark Wassell */ -/* */ -/* 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 *) - -%} - -/*Terminals with no content*/ - -%token Scattered Typedef Def Other Eof - -%token Id -%start file -%type file - -%% - -id_found: - | Typedef Id - { $2 } - | Def Other Id - { $3 } - -skip: - | Scattered - { () } - | Id - { () } - | Other - { () } - -scan_file: - | id_found Eof - { [$1] } - | skip Eof - { [] } - | id_found scan_file - { $1::$2 } - | skip scan_file - { $2 } - -file: - | scan_file - { $1 } - diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 8047ff32..8f0c0386 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -49,5 +49,4 @@ (**************************************************************************) include Pretty_print_lem_ast -include Pretty_print_sail include Pretty_print_lem diff --git a/src/pretty_print.mli b/src/pretty_print.mli index d411815f..c685e0a4 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -51,11 +51,6 @@ open Ast open Type_check -(* Prints the defs following source syntax *) -val pp_defs : out_channel -> 'a defs -> unit -val pp_exp : Buffer.t -> 'a exp -> unit -val pat_to_string : 'a pat -> string - (* Prints on formatter the defs as Lem Ast nodes *) val pp_lem_defs : Format.formatter -> tannot defs -> unit val pp_defs_lem : bool -> bool -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml deleted file mode 100644 index 38b9e134..00000000 --- a/src/pretty_print_sail.ml +++ /dev/null @@ -1,536 +0,0 @@ -(**************************************************************************) -(* Sail *) -(* *) -(* Copyright (c) 2013-2017 *) -(* Kathyrn Gray *) -(* Shaked Flur *) -(* Stephen Kell *) -(* Gabriel Kerneis *) -(* Robert Norton-Wright *) -(* Christopher Pulte *) -(* Peter Sewell *) -(* Alasdair Armstrong *) -(* Brian Campbell *) -(* Thomas Bauereiss *) -(* Anthony Fox *) -(* Jon French *) -(* Dominic Mulligan *) -(* Stephen Kell *) -(* Mark Wassell *) -(* *) -(* 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 Ast -open Ast_util -open PPrint -open Pretty_print_common - -(**************************************************************************** - * PPrint-based source-to-source pretty printer -****************************************************************************) - -let doc_bkind (BK_aux(k,_)) = - string (match k with - | BK_type -> "Type" - | BK_nat -> "Nat" - | BK_order -> "Order") - -let doc_kind (K_aux(K_kind(klst),_)) = - separate_map (spaces arrow) doc_bkind klst - -let doc_qi (QI_aux(qi,_)) = match qi with - | QI_const n_const -> doc_nexp_constraint n_const - | QI_id(KOpt_aux(ki,_)) -> - match ki with - | KOpt_none v -> doc_var v - | KOpt_kind(k,v) -> separate space [doc_kind k; doc_var v] - -(* typ_doc is the doc for the type being quantified *) -let doc_typquant (TypQ_aux(tq,_)) typ_doc = match tq with - | TypQ_no_forall -> typ_doc - | TypQ_tq [] -> typ_doc - | TypQ_tq qlist -> - (* include trailing break because the caller doesn't know if tq is empty *) - doc_op dot - (separate space [string "forall"; separate_map comma_sp doc_qi qlist]) - typ_doc - -let doc_typscm (TypSchm_aux(TypSchm_ts(tq,t),_)) = - (doc_typquant tq (doc_typ t)) - -let doc_typscm_atomic (TypSchm_aux(TypSchm_ts(tq,t),_)) = - (doc_typquant tq (doc_atomic_typ t)) - -let doc_lit (L_aux(l,_)) = - utf8string (match l with - | L_unit -> "()" - | L_zero -> "bitzero" - | L_one -> "bitone" - | L_true -> "true" - | L_false -> "false" - | L_num i -> Big_int.to_string i - | L_hex n -> "0x" ^ n - | L_bin n -> "0b" ^ n - | L_real r -> r - | L_undef -> "undefined" - | L_string s -> "\"" ^ String.escaped s ^ "\"") - -let doc_pat, doc_atomic_pat = - let rec pat pa = pat_colons pa - and pat_colons ((P_aux(p,l)) as pa) = match p with - (* XXX add leading indentation if not flat - we need to define our own - * combinator for that *) - | P_vector_concat pats -> separate_map (space ^^ colon ^^ break 1) atomic_pat pats - | _ -> app_pat pa - and app_pat ((P_aux(p,l)) as pa) = match p with - | P_app(id, ((_ :: _) as pats)) -> doc_unop (doc_id id) (parens (separate_map comma_sp atomic_pat pats)) - | _ -> atomic_pat pa - and atomic_pat ((P_aux(p,(l,annot))) as pa) = match p with - | P_lit lit -> doc_lit lit - | P_wild -> underscore - | P_id id -> doc_id id - | P_var (P_aux (P_id id, _), kid) when Id.compare (id_of_kid kid) id == 0 -> - doc_var kid - | P_var(p,kid) -> parens (separate space [pat p; string "as"; doc_var kid]) - | P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id id]) - | P_typ(typ,p) -> separate space [parens (doc_typ typ); atomic_pat p] - | P_app(id,[]) -> doc_id id - | P_record(fpats,_) -> braces (separate_map semi_sp fpat fpats) - | P_vector pats -> brackets (separate_map comma_sp atomic_pat pats) - | P_tup pats -> parens (separate_map comma_sp atomic_pat pats) - | P_list pats -> squarebarbars (separate_map semi_sp atomic_pat pats) - | P_cons (pat1, pat2) -> separate space [atomic_pat pat1; coloncolon; pat pat2] - | P_app(_, _ :: _) | P_vector_concat _ -> - group (parens (pat pa)) - and fpat (FP_aux(FP_Fpat(id,fpat),_)) = doc_op equals (doc_id id) (pat fpat) - and npat (i,p) = doc_op equals (doc_int i) (pat p) - - (* expose doc_pat and doc_atomic_pat *) - in pat, atomic_pat - -let doc_exp, doc_let = - let rec exp e = group (or_exp e) - and or_exp ((E_aux(e,_)) as expr) = match e with - | E_app_infix(l,(Id_aux(Id ("|" | "||"),_) as op),r) -> - doc_op (doc_id op) (and_exp l) (or_exp r) - | _ -> and_exp expr - and and_exp ((E_aux(e,_)) as expr) = match e with - | E_app_infix(l,(Id_aux(Id ("&" | "&&"),_) as op),r) -> - doc_op (doc_id op) (eq_exp l) (and_exp r) - | _ -> eq_exp expr - and eq_exp ((E_aux(e,_)) as expr) = match e with - | E_app_infix(l,(Id_aux(Id ( - (* XXX this is not very consistent - is the parser bogus here? *) - "=" | "==" | "!=" - | ">=" | ">=_s" | ">=_u" | ">" | ">_s" | ">_u" - | "<=" | "<=_s" | "<" | "<_s" | "<_si" | "<_u" - ),_) as op),r) -> - doc_op (doc_id op) (eq_exp l) (at_exp r) - (* XXX assignment should not have the same precedence as equal etc. *) - | E_assign(le,exp) -> doc_op coloneq (doc_lexp le) (at_exp exp) - | _ -> at_exp expr - and at_exp ((E_aux(e,_)) as expr) = match e with - | E_app_infix(l,(Id_aux(Id ("@" | "^^" | "^" | "~^"),_) as op),r) -> - doc_op (doc_id op) (cons_exp l) (at_exp r) - | _ -> cons_exp expr - and cons_exp ((E_aux(e,_)) as expr) = match e with - | E_vector_append(l,r) -> - doc_op colon (shift_exp l) (cons_exp r) - | E_cons(l,r) -> - doc_op coloncolon (shift_exp l) (cons_exp r) - | _ -> shift_exp expr - and shift_exp ((E_aux(e,_)) as expr) = match e with - | E_app_infix(l,(Id_aux(Id (">>" | ">>>" | "<<" | "<<<"),_) as op),r) -> - doc_op (doc_id op) (shift_exp l) (plus_exp r) - | _ -> plus_exp expr - and plus_exp ((E_aux(e,_)) as expr) = match e with - | E_app_infix(l,(Id_aux(Id ("+" | "-" | "+_s" | "-_s"),_) as op),r) -> - doc_op (doc_id op) (plus_exp l) (star_exp r) - | _ -> star_exp expr - and star_exp ((E_aux(e,_)) as expr) = match e with - | E_app_infix(l,(Id_aux(Id ( - "*" | "/" - | "div" | "quot" | "quot_s" | "rem" | "mod" - | "*_s" | "*_si" | "*_u" | "*_ui"),_) as op),r) -> - doc_op (doc_id op) (star_exp l) (starstar_exp r) - | _ -> starstar_exp expr - and starstar_exp ((E_aux(e,_)) as expr) = match e with - | E_app_infix(l,(Id_aux(Id "**",_) as op),r) -> - doc_op (doc_id op) (starstar_exp l) (app_exp r) - | E_if _ | E_for _ | E_loop _ | E_let _ - | E_var _ | E_internal_plet _ -> right_atomic_exp expr - | _ -> app_exp expr - and right_atomic_exp ((E_aux(e,_)) as expr) = match e with - (* Special case: omit "else ()" when the else branch is empty. *) - | E_if(c,t,E_aux(E_block [], _)) -> - string "if" ^^ space ^^ group (exp c) ^/^ - string "then" ^^ space ^^ group (exp t) - | E_if(c,t,e) -> - string "if" ^^ space ^^ group (exp c) ^/^ - string "then" ^^ space ^^ group (exp t) ^/^ - string "else" ^^ space ^^ group (exp e) - | E_loop (While, c, e) -> - separate space [string "while"; atomic_exp c; string "do"] ^/^ - exp e - | E_loop (Until, c, e) -> - (string "repeat" - ^/^ exp e) - ^/^ (string "until" ^^ space ^^ atomic_exp c) - | E_for(id,exp1,exp2,exp3,order,exp4) -> - string "foreach" ^^ space ^^ - group (parens ( - separate (break 1) [ - doc_id id; - string "from " ^^ atomic_exp exp1; - string "to " ^^ atomic_exp exp2; - string "by " ^^ atomic_exp exp3; - string "in " ^^ doc_ord order - ] - )) ^/^ - exp exp4 - | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e) - | E_var (lexp, exp1, exp2) -> - let le = - prefix 2 1 - (separate space [string "internal_let"; doc_lexp lexp; equals]) - (exp exp1) in - doc_op (string "in") le (exp exp2) - | E_internal_plet (pat, exp1, exp2) -> - let le = - prefix 2 1 - (separate space [string "internal_plet"; doc_pat pat; equals]) - (exp exp1) in - doc_op (string "in") le (exp exp2) - | _ -> group (parens (exp expr)) - and app_exp ((E_aux(e,_)) as expr) = match e with - | E_app(f,args) -> - (doc_id f) ^^ (parens (separate_map comma exp args)) - | _ -> vaccess_exp expr - and vaccess_exp ((E_aux(e,_)) as expr) = match e with - | E_vector_access(v,e) -> - atomic_exp v ^^ brackets (exp e) - | E_vector_subrange(v,e1,e2) -> - atomic_exp v ^^ brackets (doc_op dotdot (exp e1) (exp e2)) - | _ -> field_exp expr - and field_exp ((E_aux(e,_)) as expr) = match e with - | E_field(fexp,id) -> atomic_exp fexp ^^ dot ^^ doc_id id - | _ -> atomic_exp expr - and atomic_exp ((E_aux(e,_)) as expr) = match e with - (* Special case: an empty block is equivalent to unit, but { } would - * be parsed as a struct. *) - | E_block [] -> string "()" - | E_block exps -> - let exps_doc = separate_map (semi ^^ hardline) exp exps in - surround 2 1 lbrace exps_doc rbrace - | E_nondet exps -> - let exps_doc = separate_map (semi ^^ hardline) exp exps in - string "nondet" ^^ space ^^ (surround 2 1 lbrace exps_doc rbrace) - | E_comment s -> string ("(*" ^ s ^ "*) ()") - | E_comment_struc e -> string "(*" ^^ exp e ^^ string "*) ()" - | E_id id -> doc_id id - | E_lit lit -> doc_lit lit - | E_cast(typ,e) -> prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp e)) - (* - | E_internal_cast((_,NoTyp),e) -> atomic_exp e - | E_internal_cast((_,Base((_,t),_,_,_,_,bindings)), (E_aux(_,(_,eannot)) as e)) -> - (match t.t,eannot with - (* XXX I don't understand why we can hide the internal cast here - AAA Because an internal cast between vectors is only generated to reset the base access; - the type checker generates far more than are needed and they're pruned off here, after constraint resolution *) - | Tapp("vector",[TA_nexp n1;_;_;_]),Base((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_,_,_) - when nexp_eq n1 n2 -> atomic_exp e - | _ -> prefix 2 1 (parens (doc_typ (t_to_typ t))) (group (atomic_exp e))) - *) - | E_tuple exps -> - parens (separate_map comma exp exps) - | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> - (* XXX E_record is not handled by parser currently - AAA The parser can't handle E_record due to ambiguity with blocks; initial_check looks for blocks that are all field assignments and converts *) - braces (separate_map semi_sp doc_fexp fexps) - | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> - braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps)) - | E_vector exps -> - let default_print _ = brackets (separate_map comma exp exps) in - (match exps with - | [] -> default_print () - | E_aux(e,_)::es -> - (match e with - | E_lit (L_aux(L_one, _)) | E_lit (L_aux(L_zero, _)) -> - utf8string - ("0b" ^ - (List.fold_right (fun (E_aux( e,_)) rst -> - (match e with - | E_lit(L_aux(l, _)) -> - ((match l with | L_one -> "1" | L_zero -> "0" | L_undef -> "u" | _ -> assert false) ^ rst) - | _ -> assert false)) exps "")) - | _ -> default_print ())) - | E_vector_update(v,e1,e2) -> - brackets (doc_op (string "with") (exp v) (doc_op equals (atomic_exp e1) (exp e2))) - | E_vector_update_subrange(v,e1,e2,e3) -> - brackets ( - doc_op (string "with") (exp v) - (doc_op equals (atomic_exp e1 ^^ colon ^^ atomic_exp e2) (exp e3))) - | E_list exps -> - squarebarbars (separate_map comma exp exps) - | E_try(e,pexps) -> - let opening = separate space [string "try"; exp e; string "catch"; lbrace] in - let cases = separate_map (break 1) doc_case pexps in - surround 2 1 opening cases rbrace - | E_case(e,pexps) -> - let opening = separate space [string "switch"; exp e; lbrace] in - let cases = separate_map (break 1) doc_case pexps in - surround 2 1 opening cases rbrace - | E_sizeof n -> - parens (separate space [string "sizeof"; doc_nexp n]) - | E_constraint nc -> - string "constraint" ^^ parens (doc_nexp_constraint nc) - | E_exit e -> - separate space [string "exit"; atomic_exp e;] - | E_throw e -> - separate space [string "throw"; atomic_exp e;] - | E_return e -> - separate space [string "return"; atomic_exp e;] - | E_assert(c,m) -> - separate space [string "assert"; parens (separate comma [exp c; exp m])] - (* adding parens and loop for lower precedence *) - | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _) - | E_cons (_, _)|E_field (_, _)|E_assign (_, _) - | E_if _ | E_for _ | E_loop _ | E_let _ - | E_var _ | E_internal_plet _ - | E_vector_append _ - | E_app_infix (_, - (* for every app_infix operator caught at a higher precedence, - * we need to wrap around with parens *) - (Id_aux(Id("|" | "||" - | "&" | "&&" - | "=" | "==" | "!=" - | ">=" | ">=_s" | ">=_u" | ">" | ">_s" | ">_u" - | "<=" | "<=_s" | "<" | "<_s" | "<_si" | "<_u" - | "@" | "^^" | "^" | "~^" - | ">>" | ">>>" | "<<" | "<<<" - | "+" | "-" | "+_s" | "-_s" - | "*" | "/" - | "div" | "quot" | "quot_s" | "rem" | "mod" - | "*_s" | "*_si" | "*_u" | "*_ui" - | "**"), _)) - , _) -> - group (parens (exp expr)) - (* XXX default precedence for app_infix? *) - | E_app_infix(l,op,r) -> - failwith ("unexpected app_infix operator " ^ (pp_format_id op)) - (* doc_op (doc_id op) (exp l) (exp r) *) - | E_internal_return exp1 -> - separate space [string "internal_return"; exp exp1] - | _ -> failwith ("Cannot print: " ^ Ast_util.string_of_exp expr) - and let_exp (LB_aux(lb,_)) = match lb with - | LB_val(pat,e) -> - prefix 2 1 - (separate space [string "let"; doc_atomic_pat pat; equals]) - (atomic_exp e) - - and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id id) (exp e) - - and doc_case (Pat_aux (pexp, _)) = - match pexp with - | Pat_exp(pat, e) -> - doc_op arrow (separate space [string "case"; doc_atomic_pat pat]) (group (exp e)) - | Pat_when(pat, guard, e) -> - doc_op arrow (separate space [string "case"; doc_atomic_pat pat; string "when"; exp guard]) (group (exp e)) - - (* lexps are parsed as eq_exp - we need to duplicate the precedence - * structure for them *) - and doc_lexp le = app_lexp le - and app_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with - | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma exp args) - | _ -> vaccess_lexp le - and vaccess_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with - | LEXP_vector(v,e) -> atomic_lexp v ^^ brackets (exp e) - | LEXP_vector_range(v,e1,e2) -> - atomic_lexp v ^^ brackets (exp e1 ^^ dotdot ^^ exp e2) - | _ -> field_lexp le - and field_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with - | LEXP_field(v,id) -> atomic_lexp v ^^ dot ^^ doc_id id - | _ -> atomic_lexp le - and atomic_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with - | LEXP_id id -> doc_id id - | LEXP_cast(typ,id) -> prefix 2 1 (parens (doc_typ typ)) (doc_id id) - | LEXP_memory _ | LEXP_vector _ | LEXP_vector_range _ - | LEXP_field _ -> group (parens (doc_lexp le)) - | LEXP_tup tups -> parens (separate_map comma doc_lexp tups) - - (* expose doc_exp and doc_let *) - in exp, let_exp - -let doc_default (DT_aux(df,_)) = match df with - | DT_kind(bk,v) -> separate space [string "default"; doc_bkind bk; doc_var v] - | DT_typ(ts,id) -> separate space [string "default"; doc_typscm ts; doc_id id] - | DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord] - -let doc_spec (VS_aux (VS_val_spec (ts, id, ext_opt, is_cast), _)) = - let cast_pp = if is_cast then [string "cast"] else [] in - (* This sail syntax only supports a single extern name, so just use the ocaml version *) - let extern_kwd_pp, id_pp = match ext_opt "ocaml" with - | Some ext -> [string "extern"], doc_op equals (doc_id id) (dquotes (string (ext))) - | None -> [], doc_id id - in - separate space ([string "val"] @ cast_pp @ extern_kwd_pp @ [doc_typscm ts] @ [id_pp]) - -let doc_namescm (Name_sect_aux(ns,_)) = match ns with - | Name_sect_none -> empty - (* include leading space because the caller doesn't know if ns is - * empty, and trailing break already added by the following equals *) - | Name_sect_some s -> space ^^ brackets (doc_op equals (string "name") (dquotes (string s))) - -let doc_type_union (Tu_aux(typ_u,_)) = match typ_u with - | Tu_ty_id(typ,id) -> separate space [doc_typ typ; doc_id id] - | Tu_id id -> doc_id id - -let doc_typdef (TD_aux(td,_)) = match td with - | TD_abbrev(id,nm,typschm) -> - doc_op equals (concat [string "typedef"; space; doc_id id; doc_namescm nm]) (doc_typscm typschm) - | TD_record(id,nm,typq,fs,_) -> - let f_pp (typ,id) = concat [doc_typ typ; space; doc_id id; semi] in - let fs_doc = group (separate_map (break 1) f_pp fs) in - doc_op equals - (concat [string "typedef"; space; doc_id id; doc_namescm nm]) - (string "const struct" ^^ space ^^ doc_typquant typq (braces fs_doc)) - | TD_variant(id,nm,typq,ar,_) -> - let ar_doc = group (separate_map (semi ^^ break 1) doc_type_union ar) in - doc_op equals - (concat [string "typedef"; space; doc_id id; doc_namescm nm]) - (string "const union" ^^ space ^^ doc_typquant typq (braces ar_doc)) - | TD_enum(id,nm,enums,_) -> - let enums_doc = group (separate_map (semi ^^ break 1) doc_id enums) in - doc_op equals - (concat [string "typedef"; space; doc_id id; doc_namescm nm]) - (string "enumerate" ^^ space ^^ braces enums_doc) - -let doc_kindef (KD_aux(kd,_)) = match kd with - | KD_nabbrev(kind,id,nm,n) -> - doc_op equals (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm]) (doc_nexp n) - -let doc_rec (Rec_aux(r,_)) = match r with - | Rec_nonrec -> empty - (* include trailing space because caller doesn't know if we return - * empty *) - | Rec_rec -> space ^^ string "rec" - -let doc_tannot_opt (Typ_annot_opt_aux(t,_)) = match t with - | Typ_annot_opt_some(tq,typ) -> space ^^ doc_typquant tq (doc_typ typ) - | Typ_annot_opt_none -> empty - -let doc_effects_opt (Effect_opt_aux(e,_)) = match e with - | Effect_opt_pure -> string "pure" - | Effect_opt_effect e -> doc_effects e - -let doc_funcl (FCL_aux(FCL_Funcl(id,pexp),_)) = - match pexp with - | Pat_aux (Pat_exp (pat,exp),_) -> - group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp exp)) - | Pat_aux (Pat_when (pat,wh,exp),_) -> - group (doc_op equals (doc_id id ^^ space ^^ parens (separate space [doc_atomic_pat pat; string "when"; doc_exp wh])) - (doc_exp exp)) - -let doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),_)) = - match fcls with - | [] -> failwith "FD_function with empty function list" - | _ -> - let sep = hardline ^^ string "and" ^^ space in - let clauses = separate_map sep doc_funcl fcls in - separate space ([string "function" ^^ doc_rec r ^^ doc_tannot_opt typa]@ - (match efa with - | Effect_opt_aux (Effect_opt_pure,_) -> [] - | _ -> [string "effect"; - doc_effects_opt efa;]) - @[clauses]) - -let doc_alias (AL_aux (alspec,_)) = - match alspec with - | AL_subreg((RI_aux (RI_id id,_)),subid) -> doc_id id ^^ dot ^^ doc_id subid - | AL_bit((RI_aux (RI_id id,_)),ac) -> doc_id id ^^ brackets (doc_exp ac) - | AL_slice((RI_aux (RI_id id,_)),b,e) -> doc_id id ^^ brackets (doc_op dotdot (doc_exp b) (doc_exp e)) - | AL_concat((RI_aux (RI_id f,_)),(RI_aux (RI_id s,_))) -> doc_op colon (doc_id f) (doc_id s) - -let doc_dec (DEC_aux (reg,_)) = - match reg with - | DEC_reg(typ,id) -> separate space [string "register"; doc_typ typ; doc_id id] - | DEC_alias(id,alspec) -> - doc_op equals (string "register alias" ^^ space ^^ doc_id id) (doc_alias alspec) - | DEC_typ_alias(typ,id,alspec) -> - doc_op equals (string "register alias" ^^ space ^^ doc_typ typ) (doc_alias alspec) - -let doc_scattered (SD_aux (sdef, _)) = match sdef with - | SD_scattered_function (r, typa, efa, id) -> - separate space ([ - string "scattered function"; - doc_rec r ^^ doc_tannot_opt typa;]@ - (match efa with - | Effect_opt_aux (Effect_opt_pure,_) -> [] - | _ -> [string "effect"; doc_effects_opt efa;]) - @[doc_id id]) - | SD_scattered_variant (id, ns, tq) -> - doc_op equals - (string "scattered typedef" ^^ space ^^ doc_id id ^^ doc_namescm ns) - (string "const union" ^^ space ^^ (doc_typquant tq empty)) - | SD_scattered_funcl funcl -> - string "function clause" ^^ space ^^ doc_funcl funcl - | SD_scattered_unioncl (id, tu) -> - separate space [string "union"; doc_id id; - string "member"; doc_type_union tu] - | SD_scattered_end id -> string "end" ^^ space ^^ doc_id id - -let rec doc_def def = group (match def with - | DEF_default df -> doc_default df - | DEF_spec v_spec -> doc_spec v_spec - | DEF_type t_def -> doc_typdef t_def - | DEF_kind k_def -> doc_kindef k_def - | DEF_fundef f_def -> doc_fundef f_def - | DEF_val lbind -> doc_let lbind - | DEF_reg_dec dec -> doc_dec dec - | DEF_scattered sdef -> doc_scattered sdef - | DEF_overload (id, ids) -> - let ids_doc = group (separate_map (semi ^^ break 1) doc_id ids) in - string "overload" ^^ space ^^ doc_id id ^^ space ^^ brackets ids_doc - | DEF_comm (DC_comm s) -> comment (string s) - | DEF_comm (DC_comm_struct d) -> comment (doc_def d) - | DEF_fixity _ -> empty - | DEF_internal_mutrec _ -> failwith "Cannot print internal mutrec" - ) ^^ hardline - -let doc_defs (Defs(defs)) = - separate_map hardline doc_def defs - -let pp_defs f d = print f (doc_defs d) -let pp_exp b e = to_buf b (doc_exp e) -let pat_to_string p = - let b = Buffer.create 20 in - to_buf b (doc_pat p); - Buffer.contents b diff --git a/src/process_file.ml b/src/process_file.ml index 8c00d37b..116eeb0b 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -48,7 +48,6 @@ (* SUCH DAMAGE. *) (**************************************************************************) -let opt_new_parser = ref false let opt_lem_sequential = ref false let opt_lem_mwords = ref false @@ -66,43 +65,15 @@ let get_lexbuf f = lexbuf, in_chan let parse_file (f : string) : Parse_ast.defs = - if not !opt_new_parser - then - let scanbuf, in_chan = get_lexbuf f in - let type_names = - try - Pre_parser.file Pre_lexer.token scanbuf - with - | Parsing.Parse_error -> - let pos = Lexing.lexeme_start_p scanbuf in - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "pre"))) - | Parse_ast.Parse_error_locn(l,m) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))) - | Lexer.LexError(s,p) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) - in - close_in in_chan; - Lexer.custom_type_names := !Lexer.custom_type_names @ type_names - else (); - let lexbuf, in_chan = get_lexbuf f in try - let ast = - if !opt_new_parser - then Parser2.file Lexer2.token lexbuf - else Parser.file Lexer.token lexbuf - in + let ast = Parser2.file Lexer2.token lexbuf in close_in in_chan; ast with | Parser2.Error -> let pos = Lexing.lexeme_start_p lexbuf in raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "no information"))) - | Parsing.Parse_error -> - let pos = Lexing.lexeme_start_p lexbuf in - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main"))) - | Parse_ast.Parse_error_locn(l,m) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))) - | Lexer.LexError(s,p) -> + | Lexer2.LexError(s,p) -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) let convert_ast (order : Ast.order) (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast order defs @@ -132,7 +103,7 @@ let opt_auto_mono = ref false let monomorphise_ast locs type_env ast = let ast = Monomorphise.monomorphise (!opt_lem_mwords) (!opt_auto_mono) (!opt_dmono_analysis) locs type_env ast in - let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in + let () = if !opt_ddump_raw_mono_ast then Pretty_print_sail2.pp_defs stdout ast else () in let ienv = Type_check.Env.no_casts Type_check.initial_env in Type_check.check ienv ast diff --git a/src/process_file.mli b/src/process_file.mli index 86e8fb05..ee021e61 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -63,7 +63,6 @@ val rewrite_ast_check : 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_parser : bool ref val opt_lem_sequential : bool ref val opt_lem_mwords : bool ref val opt_just_check : bool ref diff --git a/src/sail.ml b/src/sail.ml index d4e2526e..fdcaa15c 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -118,9 +118,6 @@ let options = Arg.align ([ ( "-no_effects", Arg.Set Type_check.opt_no_effects, " (experimental) turn off effect checking"); - ( "-new_parser", - Arg.Set Process_file.opt_new_parser, - " (experimental) use new parser"); ( "-convert", Arg.Set opt_convert, " (experimental) convert sail to new syntax for use with -new_parser"); @@ -224,7 +221,7 @@ let main() = () else ()); (if !(opt_print_verbose) - then ((Pretty_print.pp_defs stdout) ast) + then ((Pretty_print_sail2.pp_defs stdout) ast) else ()); (if !(opt_print_lem_ast) then output "" Lem_ast_out [out_name,ast] -- cgit v1.2.3