summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-01-05 17:50:39 +0000
committerAlasdair Armstrong2018-01-05 17:50:39 +0000
commit90bfc9c8e401e41a2f4616b84976a57f357664df (patch)
treef1ded7f454b4015873afb772d1c149c7f42c342b /src
parentcb796f509c412c4f354e045f7b83f233d8863181 (diff)
Removed legacy parser/lexer and pretty printer
Diffstat (limited to 'src')
-rw-r--r--src/lexer.mll372
-rw-r--r--src/parser.mly1358
-rw-r--r--src/pre_lexer.mll205
-rw-r--r--src/pre_parser.mly94
-rw-r--r--src/pretty_print.ml1
-rw-r--r--src/pretty_print.mli5
-rw-r--r--src/pretty_print_sail.ml536
-rw-r--r--src/process_file.ml35
-rw-r--r--src/process_file.mli1
-rw-r--r--src/sail.ml5
10 files changed, 4 insertions, 2608 deletions
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 <string> Id TyVar TyId
-%token <Nat_big_num.num> Num
-%token <string> String Bin Hex Real
-
-%token <string> Amp At Carrot Div Eq Excl Gt Lt Plus Star Tilde
-%token <string> AmpAmp CarrotCarrot Colon ColonColon EqEq ExclEq ExclExcl
-%token <string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt
-%token <string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar TildeCarrot
-
-%token <string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS
-%token <string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU
-%token <string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarStarUnderS StarStarUnderSi StarUnderS
-%token <string> StarUnderSi StarUnderU StarUnderUi TwoCarrot PlusUnderS MinusUnderS
-
-%token <string> AmpI AtI CarrotI DivI EqI ExclI GtI LtI PlusI StarI TildeI
-%token <string> AmpAmpI CarrotCarrotI ColonColonI EqEqI ExclEqI ExclExclI
-%token <string> GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI
-%token <string> LtEqI LtEqPlusI LtGtI LtLtI LtLtLtI LtPlusI StarStarI TildeCarrotI
-
-%token <string> GtEqUnderSI GtEqUnderSiI GtEqUnderUI GtEqUnderUiI GtGtUnderUI GtUnderSI
-%token <string> GtUnderSiI GtUnderUI GtUnderUiI LtEqUnderSI LtEqUnderSiI LtEqUnderUI
-%token <string> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarStarUnderSI StarStarUnderSiI StarUnderSI
-%token <string> StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI
-
-
-%start file nonempty_exp_list
-%type <Parse_ast.defs> defs
-%type <Parse_ast.atyp> typ
-%type <Parse_ast.pat> pat
-%type <Parse_ast.exp> exp
-%type <Parse_ast.exp list> nonempty_exp_list
-%type <Parse_ast.defs> file
-
-
-%%
-
-id:
- | Id
- { idl (Id($1)) }
- | Tilde
- { idl (Id($1)) }
- | Lparen Deinfix Amp Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix At Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix Carrot Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix Div Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix Quot Rparen
- { idl (DeIid("quot")) }
- | Lparen Deinfix QuotUnderS Rparen
- { idl (DeIid("quot_s")) }
- | Lparen Deinfix Eq Rparen
- { Id_aux(DeIid($3),loc ()) }
- | Lparen Deinfix Excl Lparen
- { idl (DeIid($3)) }
- | Lparen Deinfix Gt Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix Lt Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix GtUnderS Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix LtUnderS Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix Minus Rparen
- { idl (DeIid("-")) }
- | Lparen Deinfix MinusUnderS Rparen
- { idl (DeIid("-_s")) }
- | Lparen Deinfix Mod Rparen
- { idl (DeIid("mod")) }
- | Lparen Deinfix Plus Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix PlusUnderS Rparen
- { idl (DeIid("+_s")) }
- | Lparen Deinfix Star Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix StarUnderS Rparen
- { idl (DeIid("*_s")) }
- | Lparen Deinfix AmpAmp Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix Bar Rparen
- { idl (DeIid("|")) }
- | Lparen Deinfix BarBar Rparen
- { idl (DeIid("||")) }
- | Lparen Deinfix CarrotCarrot Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix Colon Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix ColonColon Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix EqEq Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix ExclEq Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix ExclExcl Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix GtEq Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix GtEqUnderS Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix GtEqPlus Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix GtGt Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix GtGtGt Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix GtPlus Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix HashGtGt Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix HashLtLt Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix LtEq Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix LtEqUnderS Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix LtLt Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix LtLtLt Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix LtPlus Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix StarStar Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix Tilde Rparen
- { idl (DeIid($3)) }
- | Lparen Deinfix TildeCarrot Rparen
- { idl (DeIid($3)) }
-
-tid:
- | TyId
- { (idl (Id($1))) }
-
-tyvar:
- | TyVar
- { (Kid_aux((Var($1)),loc ())) }
-
-tyvars:
- | tyvar
- { [$1] }
- | tyvar tyvars
- { $1 :: $2 }
-
-atomic_kind:
- | TYPE
- { bkloc BK_type }
- | Nat
- { bkloc BK_nat }
- | NatNum
- { bkloc BK_nat }
- | Order
- { bkloc BK_order }
-
-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 <string> Id
-%start file
-%type <string list> 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]
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:19:06 +0000