From 9f99b67e3009f0a40a0a14cde3201f2d7839efbd Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 5 Jan 2018 17:56:53 +0000 Subject: Moved parser, lexer and pretty printer to correct locations. --- src/initial_check.ml | 6 +- src/interpreter.ml | 2 +- src/isail.ml | 2 +- src/lexer.mll | 300 +++++++++++ src/lexer2.mll | 300 ----------- src/myocamlbuild.ml | 6 - src/parser.mly | 1233 +++++++++++++++++++++++++++++++++++++++++++++ src/parser2.mly | 1233 --------------------------------------------- src/pretty_print_sail.ml | 540 ++++++++++++++++++++ src/pretty_print_sail2.ml | 540 -------------------- src/process_file.ml | 12 +- src/sail.ml | 6 +- src/spec_analysis.ml | 2 +- 13 files changed, 2088 insertions(+), 2094 deletions(-) create mode 100644 src/lexer.mll delete mode 100644 src/lexer2.mll create mode 100644 src/parser.mly delete mode 100644 src/parser2.mly create mode 100644 src/pretty_print_sail.ml delete mode 100644 src/pretty_print_sail2.ml (limited to 'src') diff --git a/src/initial_check.ml b/src/initial_check.ml index 52ed1da1..4e466596 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -956,11 +956,11 @@ let initial_kind_env = ] let exp_of_string order str = - let exp = Parser2.exp_eof Lexer2.token (Lexing.from_string str) in + let exp = Parser.exp_eof Lexer.token (Lexing.from_string str) in to_ast_exp initial_kind_env order exp let typschm_of_string order str = - let typschm = Parser2.typschm_eof Lexer2.token (Lexing.from_string str) in + let typschm = Parser.typschm_eof Lexer.token (Lexing.from_string str) in let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in typschm @@ -1098,5 +1098,5 @@ let process_ast order defs = end let ast_of_def_string order str = - let def = Parser2.def_eof Lexer2.token (Lexing.from_string str) in + let def = Parser.def_eof Lexer.token (Lexing.from_string str) in process_ast order (Defs [def]) diff --git a/src/interpreter.ml b/src/interpreter.ml index 7e84f5c7..7a4b6b33 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -510,7 +510,7 @@ let rec eval_frame ast = function print_endline ("Returning value: " ^ string_of_value (value_of_exp v) |> Util.cyan |> Util.clear); Step (stack_string head, (stack_state head, snd state), stack_cont head (value_of_exp v), stack') | Pure exp', _ -> - let out' = Pretty_print_sail2.to_string (Pretty_print_sail2.doc_exp exp') in + let out' = Pretty_print_sail.to_string (Pretty_print_sail.doc_exp exp') in Step (out', state, step exp', stack) | Yield (Call(id, vals, cont)), _ -> print_endline ("Calling " ^ string_of_id id |> Util.cyan |> Util.clear); diff --git a/src/isail.ml b/src/isail.ml index c56fc69f..5452b7a9 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -53,7 +53,7 @@ open Sail open Ast open Ast_util open Interpreter -open Pretty_print_sail2 +open Pretty_print_sail type mode = | Evaluation of frame diff --git a/src/lexer.mll b/src/lexer.mll new file mode 100644 index 00000000..ccbe12a5 --- /dev/null +++ b/src/lexer.mll @@ -0,0 +1,300 @@ +(**************************************************************************) +(* 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 +open Parse_ast +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 mk_operator prec n op = + match prec, n with + | Infix, 0 -> Op0 op + | Infix, 1 -> Op1 op + | Infix, 2 -> Op2 op + | Infix, 3 -> Op3 op + | Infix, 4 -> Op4 op + | Infix, 5 -> Op5 op + | Infix, 6 -> Op6 op + | Infix, 7 -> Op7 op + | Infix, 8 -> Op8 op + | Infix, 9 -> Op9 op + | InfixL, 0 -> Op0l op + | InfixL, 1 -> Op1l op + | InfixL, 2 -> Op2l op + | InfixL, 3 -> Op3l op + | InfixL, 4 -> Op4l op + | InfixL, 5 -> Op5l op + | InfixL, 6 -> Op6l op + | InfixL, 7 -> Op7l op + | InfixL, 8 -> Op8l op + | InfixL, 9 -> Op9l op + | InfixR, 0 -> Op0r op + | InfixR, 1 -> Op1r op + | InfixR, 2 -> Op2r op + | InfixR, 3 -> Op3r op + | InfixR, 4 -> Op4r op + | InfixR, 5 -> Op5r op + | InfixR, 6 -> Op6r op + | InfixR, 7 -> Op7r op + | InfixR, 8 -> Op8r op + | InfixR, 9 -> Op9r op + | _, _ -> assert false + +let operators = ref M.empty + +let kw_table = + List.fold_left + (fun r (x,y) -> M.add x y r) + M.empty + [ + ("and", (fun _ -> And)); + ("as", (fun _ -> As)); + ("assert", (fun _ -> Assert)); + ("bitzero", (fun _ -> Bitzero)); + ("bitone", (fun _ -> Bitone)); + ("by", (fun _ -> By)); + ("match", (fun _ -> Match)); + ("clause", (fun _ -> Clause)); + ("dec", (fun _ -> Dec)); + ("operator", (fun _ -> Op)); + ("default", (fun _ -> Default)); + ("effect", (fun _ -> Effect)); + ("end", (fun _ -> End)); + ("enum", (fun _ -> Enum)); + ("else", (fun _ -> Else)); + ("exit", (fun _ -> Exit)); + ("cast", (fun _ -> Cast)); + ("false", (fun _ -> False)); + ("forall", (fun _ -> Forall)); + ("foreach", (fun _ -> Foreach)); + ("function", (fun x -> Function_)); + ("overload", (fun _ -> Overload)); + ("throw", (fun _ -> Throw)); + ("try", (fun _ -> Try)); + ("catch", (fun _ -> Catch)); + ("if", (fun x -> If_)); + ("in", (fun x -> In)); + ("inc", (fun _ -> Inc)); + ("let", (fun x -> Let_)); + ("var", (fun _ -> Var)); + ("ref", (fun _ -> Ref)); + ("record", (fun _ -> Record)); + ("Int", (fun x -> Int)); + ("Order", (fun x -> Order)); + ("pure", (fun x -> Pure)); + ("register", (fun x -> Register)); + ("return", (fun x -> Return)); + ("scattered", (fun x -> Scattered)); + ("sizeof", (fun x -> Sizeof)); + ("constraint", (fun x -> Constraint)); + ("struct", (fun x -> Struct)); + ("then", (fun x -> Then)); + ("true", (fun x -> True)); + ("Type", (fun x -> TYPE)); + ("type", (fun x -> Typedef)); + ("undefined", (fun x -> Undefined)); + ("union", (fun x -> Union)); + ("newtype", (fun x -> Newtype)); + ("with", (fun x -> With)); + ("val", (fun x -> Val)); + ("repeat", (fun _ -> Repeat)); + ("until", (fun _ -> Until)); + ("while", (fun _ -> While)); + ("do", (fun _ -> Do)); + ("mutual", (fun _ -> Mutual)); + ("bitfield", (fun _ -> Bitfield)); + + ("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 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 operator = (oper_char+ ('_' ident)?) +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 "@") } + | "2" ws "^" { TwoCaret } + | "^" { (Caret(r"^")) } + | ":" { Colon(r ":") } + | "," { Comma } + | ".." { DotDot } + | "." { Dot } + | "==" as op + { try M.find op !operators + with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) } + | "=" { (Eq(r"=")) } + | ">" { (Gt(r">")) } + | "-" { Minus } + | "<" { (Lt(r"<")) } + | "+" { (Plus(r"+")) } + | ";" { Semi } + | "*" { (Star(r"*")) } + | "_" { Under } + | "[|" { LsquareBar } + | "|]" { RsquareBar } + | "{|" { LcurlyBar } + | "|}" { RcurlyBar } + | "|" { Bar } + | "{" { Lcurly } + | "}" { Rcurly } + | "()" { Unit(r"()") } + | "(" { Lparen } + | ")" { Rparen } + | "[" { Lsquare } + | "]" { Rsquare } + | "!=" { (ExclEq(r"!=")) } + | ">=" { (GtEq(r">=")) } + | "->" { MinusGt } + | "=>" { EqGt(r "=>") } + | "<=" { (LtEq(r"<=")) } + | "/*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf } + | "*/" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) } + | "infix" ws (digit as p) ws (operator as op) + { operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators; + Fixity (Infix, Big_int.of_string (Char.escaped p), op) } + | "infixl" ws (digit as p) ws (operator as op) + { operators := M.add op (mk_operator InfixL (int_of_string (Char.escaped p)) op) !operators; + Fixity (InfixL, Big_int.of_string (Char.escaped p), op) } + | "infixr" ws (digit as p) ws (operator as op) + { operators := M.add op (mk_operator InfixR (int_of_string (Char.escaped p)) op) !operators; + Fixity (InfixR, Big_int.of_string (Char.escaped p), op) } + | operator as op + { try M.find op !operators + with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) } + | tyvar_start startident ident* as i { TyVar(r i) } + | "~" { Id(r"~") } + | 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) } + | (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/lexer2.mll b/src/lexer2.mll deleted file mode 100644 index 3a1f7066..00000000 --- a/src/lexer2.mll +++ /dev/null @@ -1,300 +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 Parser2 -module Big_int = Nat_big_num -open Parse_ast -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 mk_operator prec n op = - match prec, n with - | Infix, 0 -> Op0 op - | Infix, 1 -> Op1 op - | Infix, 2 -> Op2 op - | Infix, 3 -> Op3 op - | Infix, 4 -> Op4 op - | Infix, 5 -> Op5 op - | Infix, 6 -> Op6 op - | Infix, 7 -> Op7 op - | Infix, 8 -> Op8 op - | Infix, 9 -> Op9 op - | InfixL, 0 -> Op0l op - | InfixL, 1 -> Op1l op - | InfixL, 2 -> Op2l op - | InfixL, 3 -> Op3l op - | InfixL, 4 -> Op4l op - | InfixL, 5 -> Op5l op - | InfixL, 6 -> Op6l op - | InfixL, 7 -> Op7l op - | InfixL, 8 -> Op8l op - | InfixL, 9 -> Op9l op - | InfixR, 0 -> Op0r op - | InfixR, 1 -> Op1r op - | InfixR, 2 -> Op2r op - | InfixR, 3 -> Op3r op - | InfixR, 4 -> Op4r op - | InfixR, 5 -> Op5r op - | InfixR, 6 -> Op6r op - | InfixR, 7 -> Op7r op - | InfixR, 8 -> Op8r op - | InfixR, 9 -> Op9r op - | _, _ -> assert false - -let operators = ref M.empty - -let kw_table = - List.fold_left - (fun r (x,y) -> M.add x y r) - M.empty - [ - ("and", (fun _ -> And)); - ("as", (fun _ -> As)); - ("assert", (fun _ -> Assert)); - ("bitzero", (fun _ -> Bitzero)); - ("bitone", (fun _ -> Bitone)); - ("by", (fun _ -> By)); - ("match", (fun _ -> Match)); - ("clause", (fun _ -> Clause)); - ("dec", (fun _ -> Dec)); - ("operator", (fun _ -> Op)); - ("default", (fun _ -> Default)); - ("effect", (fun _ -> Effect)); - ("end", (fun _ -> End)); - ("enum", (fun _ -> Enum)); - ("else", (fun _ -> Else)); - ("exit", (fun _ -> Exit)); - ("cast", (fun _ -> Cast)); - ("false", (fun _ -> False)); - ("forall", (fun _ -> Forall)); - ("foreach", (fun _ -> Foreach)); - ("function", (fun x -> Function_)); - ("overload", (fun _ -> Overload)); - ("throw", (fun _ -> Throw)); - ("try", (fun _ -> Try)); - ("catch", (fun _ -> Catch)); - ("if", (fun x -> If_)); - ("in", (fun x -> In)); - ("inc", (fun _ -> Inc)); - ("let", (fun x -> Let_)); - ("var", (fun _ -> Var)); - ("ref", (fun _ -> Ref)); - ("record", (fun _ -> Record)); - ("Int", (fun x -> Int)); - ("Order", (fun x -> Order)); - ("pure", (fun x -> Pure)); - ("register", (fun x -> Register)); - ("return", (fun x -> Return)); - ("scattered", (fun x -> Scattered)); - ("sizeof", (fun x -> Sizeof)); - ("constraint", (fun x -> Constraint)); - ("struct", (fun x -> Struct)); - ("then", (fun x -> Then)); - ("true", (fun x -> True)); - ("Type", (fun x -> TYPE)); - ("type", (fun x -> Typedef)); - ("undefined", (fun x -> Undefined)); - ("union", (fun x -> Union)); - ("newtype", (fun x -> Newtype)); - ("with", (fun x -> With)); - ("val", (fun x -> Val)); - ("repeat", (fun _ -> Repeat)); - ("until", (fun _ -> Until)); - ("while", (fun _ -> While)); - ("do", (fun _ -> Do)); - ("mutual", (fun _ -> Mutual)); - ("bitfield", (fun _ -> Bitfield)); - - ("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 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 operator = (oper_char+ ('_' ident)?) -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 "@") } - | "2" ws "^" { TwoCaret } - | "^" { (Caret(r"^")) } - | ":" { Colon(r ":") } - | "," { Comma } - | ".." { DotDot } - | "." { Dot } - | "==" as op - { try M.find op !operators - with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) } - | "=" { (Eq(r"=")) } - | ">" { (Gt(r">")) } - | "-" { Minus } - | "<" { (Lt(r"<")) } - | "+" { (Plus(r"+")) } - | ";" { Semi } - | "*" { (Star(r"*")) } - | "_" { Under } - | "[|" { LsquareBar } - | "|]" { RsquareBar } - | "{|" { LcurlyBar } - | "|}" { RcurlyBar } - | "|" { Bar } - | "{" { Lcurly } - | "}" { Rcurly } - | "()" { Unit(r"()") } - | "(" { Lparen } - | ")" { Rparen } - | "[" { Lsquare } - | "]" { Rsquare } - | "!=" { (ExclEq(r"!=")) } - | ">=" { (GtEq(r">=")) } - | "->" { MinusGt } - | "=>" { EqGt(r "=>") } - | "<=" { (LtEq(r"<=")) } - | "/*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf } - | "*/" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) } - | "infix" ws (digit as p) ws (operator as op) - { operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators; - Fixity (Infix, Big_int.of_string (Char.escaped p), op) } - | "infixl" ws (digit as p) ws (operator as op) - { operators := M.add op (mk_operator InfixL (int_of_string (Char.escaped p)) op) !operators; - Fixity (InfixL, Big_int.of_string (Char.escaped p), op) } - | "infixr" ws (digit as p) ws (operator as op) - { operators := M.add op (mk_operator InfixR (int_of_string (Char.escaped p)) op) !operators; - Fixity (InfixR, Big_int.of_string (Char.escaped p), op) } - | operator as op - { try M.find op !operators - with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) } - | tyvar_start startident ident* as i { TyVar(r i) } - | "~" { Id(r"~") } - | 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) } - | (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/myocamlbuild.ml b/src/myocamlbuild.ml index d912c965..1babc1c9 100644 --- a/src/myocamlbuild.ml +++ b/src/myocamlbuild.ml @@ -109,11 +109,5 @@ dispatch begin function mv (basename (env "%.lem")) (dirname (env "%.lem")) ]); - rule "old parser" - ~insert:(`top) - ~prods: ["parser.ml"; "parser.mli"] - ~dep: "parser.mly" - (fun env builder -> Cmd(S[V"OCAMLYACC"; T(tags_of_pathname "parser.mly"++"ocaml"++"parser"++"ocamlyacc"); Px "parser.mly"])); - | _ -> () end ;; diff --git a/src/parser.mly b/src/parser.mly new file mode 100644 index 00000000..7af70687 --- /dev/null +++ b/src/parser.mly @@ -0,0 +1,1233 @@ +/**************************************************************************/ +/* 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 n m = Range (n, m) + +let default_opt x = function + | None -> x + | Some y -> y + +let assoc_opt key assocs = + try Some (List.assoc key assocs) with + | Not_found -> None + +let string_of_id = function + | Id_aux (Id str, _) -> str + | Id_aux (DeIid str, _) -> str + +let prepend_id str1 = function + | Id_aux (Id str2, loc) -> Id_aux (Id (str1 ^ str2), loc) + | _ -> assert false + +let mk_id i n m = Id_aux (i, loc n m) +let mk_kid str n m = Kid_aux (Var str, loc n m) + +let id_of_kid = function + | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l) + +let deinfix = function + | (Id_aux (Id v, l)) -> Id_aux (DeIid v, l) + | (Id_aux (DeIid v, l)) -> Id_aux (Id v, l) + +let mk_effect e n m = BE_aux (e, loc n m) +let mk_typ t n m = ATyp_aux (t, loc n m) +let mk_pat p n m = P_aux (p, loc n m) +let mk_pexp p n m = Pat_aux (p, loc n m) +let mk_exp e n m = E_aux (e, loc n m) +let mk_lit l n m = L_aux (l, loc n m) +let mk_lit_exp l n m = mk_exp (E_lit (mk_lit l n m)) n m +let mk_typschm tq t n m = TypSchm_aux (TypSchm_ts (tq, t), loc n m) +let mk_nc nc n m = NC_aux (nc, loc n m) +let mk_sd s n m = SD_aux (s, loc n m) +let mk_ir r n m = BF_aux (r, loc n m) + +let mk_funcl f n m = FCL_aux (f, loc n m) +let mk_fun fn n m = FD_aux (fn, loc n m) +let mk_td t n m = TD_aux (t, loc n m) +let mk_vs v n m = VS_aux (v, loc n m) +let mk_reg_dec d n m = DEC_aux (d, loc n m) +let mk_default d n m = DT_aux (d, loc n m) + +let qi_id_of_kopt (KOpt_aux (kopt_aux, l) as kopt) = QI_aux (QI_id kopt, l) + +let mk_recn = (Rec_aux((Rec_nonrec), Unknown)) +let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown)) +let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown) +let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown) +let mk_namesectn = Name_sect_aux(Name_sect_none,Unknown) + +type lchain = + LC_lt +| LC_lteq +| LC_nexp of atyp + +let rec desugar_lchain chain s e = + match chain with + | [LC_nexp n1; LC_lteq; LC_nexp n2] -> + mk_nc (NC_bounded_le (n1, n2)) s e + | [LC_nexp n1; LC_lt; LC_nexp n2] -> + mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e, n2)) s e + | (LC_nexp n1 :: LC_lteq :: LC_nexp n2 :: chain) -> + let nc1 = mk_nc (NC_bounded_le (n1, n2)) s e in + mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e + | (LC_nexp n1 :: LC_lt :: LC_nexp n2 :: chain) -> + let nc1 = mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e, n2)) s e in + mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e + | _ -> assert false + +type rchain = + RC_gt +| RC_gteq +| RC_nexp of atyp + +let rec desugar_rchain chain s e = + match chain with + | [RC_nexp n1; RC_gteq; RC_nexp n2] -> + mk_nc (NC_bounded_ge (n1, n2)) s e + | [RC_nexp n1; RC_gt; RC_nexp n2] -> + mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e)) s e + | (RC_nexp n1 :: RC_gteq :: RC_nexp n2 :: chain) -> + let nc1 = mk_nc (NC_bounded_ge (n1, n2)) s e in + mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e + | (RC_nexp n1 :: RC_gt :: RC_nexp n2 :: chain) -> + let nc1 = mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e)) s e in + mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e + | _ -> assert false + +%} + +/*Terminals with no content*/ + +%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op +%token Enum Else False Forall Foreach Overload Function_ If_ In Inc Let_ Int Order Cast +%token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef +%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield +%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape +%token Repeat Until While Do Record Mutual Var Ref + +%nonassoc Then +%nonassoc Else + +%token Bar Comma Dot Eof Minus Semi Under DotDot +%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar LsquareBar RsquareBar +%token MinusGt + +/*Terminals with content*/ + +%token Id TyVar +%token Num +%token String Bin Hex Real + +%token Amp At Caret Eq Gt Lt Plus Star EqGt Unit +%token Colon ExclEq +%token GtEq +%token LtEq + +%token Op0 Op1 Op2 Op3 Op4 Op5 Op6 Op7 Op8 Op9 +%token Op0l Op1l Op2l Op3l Op4l Op5l Op6l Op7l Op8l Op9l +%token Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r + +%token Fixity + +%start file +%start typschm_eof +%start exp_eof +%start def_eof +%type typschm_eof +%type exp_eof +%type def_eof +%type file + +%% + +id: + | Id { mk_id (Id $1) $startpos $endpos } + + | Op Op0 { mk_id (DeIid $2) $startpos $endpos } + | Op Op1 { mk_id (DeIid $2) $startpos $endpos } + | Op Op2 { mk_id (DeIid $2) $startpos $endpos } + | Op Op3 { mk_id (DeIid $2) $startpos $endpos } + | Op Op4 { mk_id (DeIid $2) $startpos $endpos } + | Op Op5 { mk_id (DeIid $2) $startpos $endpos } + | Op Op6 { mk_id (DeIid $2) $startpos $endpos } + | Op Op7 { mk_id (DeIid $2) $startpos $endpos } + | Op Op8 { mk_id (DeIid $2) $startpos $endpos } + | Op Op9 { mk_id (DeIid $2) $startpos $endpos } + + | Op Op0l { mk_id (DeIid $2) $startpos $endpos } + | Op Op1l { mk_id (DeIid $2) $startpos $endpos } + | Op Op2l { mk_id (DeIid $2) $startpos $endpos } + | Op Op3l { mk_id (DeIid $2) $startpos $endpos } + | Op Op4l { mk_id (DeIid $2) $startpos $endpos } + | Op Op5l { mk_id (DeIid $2) $startpos $endpos } + | Op Op6l { mk_id (DeIid $2) $startpos $endpos } + | Op Op7l { mk_id (DeIid $2) $startpos $endpos } + | Op Op8l { mk_id (DeIid $2) $startpos $endpos } + | Op Op9l { mk_id (DeIid $2) $startpos $endpos } + + | Op Op0r { mk_id (DeIid $2) $startpos $endpos } + | Op Op1r { mk_id (DeIid $2) $startpos $endpos } + | Op Op2r { mk_id (DeIid $2) $startpos $endpos } + | Op Op3r { mk_id (DeIid $2) $startpos $endpos } + | Op Op4r { mk_id (DeIid $2) $startpos $endpos } + | Op Op5r { mk_id (DeIid $2) $startpos $endpos } + | Op Op6r { mk_id (DeIid $2) $startpos $endpos } + | Op Op7r { mk_id (DeIid $2) $startpos $endpos } + | Op Op8r { mk_id (DeIid $2) $startpos $endpos } + | Op Op9r { mk_id (DeIid $2) $startpos $endpos } + + | Op Plus { mk_id (DeIid "+") $startpos $endpos } + | Op Minus { mk_id (DeIid "-") $startpos $endpos } + | Op Star { mk_id (DeIid "*") $startpos $endpos } + | Op ExclEq { mk_id (DeIid "!=") $startpos $endpos } + | Op Lt { mk_id (DeIid "<") $startpos $endpos } + | Op Gt { mk_id (DeIid ">") $startpos $endpos } + | Op LtEq { mk_id (DeIid "<=") $startpos $endpos } + | Op GtEq { mk_id (DeIid ">=") $startpos $endpos } + | Op Amp { mk_id (DeIid "&") $startpos $endpos } + | Op Bar { mk_id (DeIid "|") $startpos $endpos } + | Op Caret { mk_id (DeIid "^") $startpos $endpos } + +op0: Op0 { mk_id (Id $1) $startpos $endpos } +op1: Op1 { mk_id (Id $1) $startpos $endpos } +op2: Op2 { mk_id (Id $1) $startpos $endpos } +op3: Op3 { mk_id (Id $1) $startpos $endpos } +op4: Op4 { mk_id (Id $1) $startpos $endpos } +op5: Op5 { mk_id (Id $1) $startpos $endpos } +op6: Op6 { mk_id (Id $1) $startpos $endpos } +op7: Op7 { mk_id (Id $1) $startpos $endpos } +op8: Op8 { mk_id (Id $1) $startpos $endpos } +op9: Op9 { mk_id (Id $1) $startpos $endpos } + +op0l: Op0l { mk_id (Id $1) $startpos $endpos } +op1l: Op1l { mk_id (Id $1) $startpos $endpos } +op2l: Op2l { mk_id (Id $1) $startpos $endpos } +op3l: Op3l { mk_id (Id $1) $startpos $endpos } +op4l: Op4l { mk_id (Id $1) $startpos $endpos } +op5l: Op5l { mk_id (Id $1) $startpos $endpos } +op6l: Op6l { mk_id (Id $1) $startpos $endpos } +op7l: Op7l { mk_id (Id $1) $startpos $endpos } +op8l: Op8l { mk_id (Id $1) $startpos $endpos } +op9l: Op9l { mk_id (Id $1) $startpos $endpos } + +op0r: Op0r { mk_id (Id $1) $startpos $endpos } +op1r: Op1r { mk_id (Id $1) $startpos $endpos } +op2r: Op2r { mk_id (Id $1) $startpos $endpos } +op3r: Op3r { mk_id (Id $1) $startpos $endpos } +op4r: Op4r { mk_id (Id $1) $startpos $endpos } +op5r: Op5r { mk_id (Id $1) $startpos $endpos } +op6r: Op6r { mk_id (Id $1) $startpos $endpos } +op7r: Op7r { mk_id (Id $1) $startpos $endpos } +op8r: Op8r { mk_id (Id $1) $startpos $endpos } +op9r: Op9r { mk_id (Id $1) $startpos $endpos } + +id_list: + | id + { [$1] } + | id Comma id_list + { $1 :: $3 } + +kid: + | TyVar + { mk_kid $1 $startpos $endpos } + +kid_list: + | kid + { [$1] } + | kid kid_list + { $1 :: $2 } + +nc: + | nc Bar nc_and + { mk_nc (NC_or ($1, $3)) $startpos $endpos } + | nc_and + { $1 } + +nc_and: + | nc_and Amp atomic_nc + { mk_nc (NC_and ($1, $3)) $startpos $endpos } + | atomic_nc + { $1 } + +atomic_nc: + | True + { mk_nc NC_true $startpos $endpos } + | False + { mk_nc NC_false $startpos $endpos } + | typ Eq typ + { mk_nc (NC_equal ($1, $3)) $startpos $endpos } + | typ ExclEq typ + { mk_nc (NC_not_equal ($1, $3)) $startpos $endpos } + | nc_lchain + { desugar_lchain $1 $startpos $endpos } + | nc_rchain + { desugar_rchain $1 $startpos $endpos } + | Lparen nc Rparen + { $2 } + | kid In Lcurly num_list Rcurly + { mk_nc (NC_set ($1, $4)) $startpos $endpos } + +num_list: + | Num + { [$1] } + | Num Comma num_list + { $1 :: $3 } + +nc_lchain: + | typ LtEq typ + { [LC_nexp $1; LC_lteq; LC_nexp $3] } + | typ Lt typ + { [LC_nexp $1; LC_lt; LC_nexp $3] } + | typ LtEq nc_lchain + { LC_nexp $1 :: LC_lteq :: $3 } + | typ Lt nc_lchain + { LC_nexp $1 :: LC_lt :: $3 } + +nc_rchain: + | typ GtEq typ + { [RC_nexp $1; RC_gteq; RC_nexp $3] } + | typ Gt typ + { [RC_nexp $1; RC_gt; RC_nexp $3] } + | typ GtEq nc_rchain + { RC_nexp $1 :: RC_gteq :: $3 } + | typ Gt nc_rchain + { RC_nexp $1 :: RC_gt :: $3 } + +typ: + | typ0 + { $1 } + +/* The following implements all nine levels of user-defined precedence for +operators in types, with both left, right and non-associative operators */ + +typ0: + | typ1 op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ0l op0l typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ1 op0r typ0r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ1 { $1 } +typ0l: + | typ1 op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ0l op0l typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ1 { $1 } +typ0r: + | typ1 op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ1 op0r typ0r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ1 { $1 } + +typ1: + | typ2 op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ1l op1l typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ2 op1r typ1r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ2 { $1 } +typ1l: + | typ2 op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ1l op1l typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ2 { $1 } +typ1r: + | typ2 op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ2 op1r typ1r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ2 { $1 } + +typ2: + | typ3 op2 typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ2l op2l typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ3 op2r typ2r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ3 { $1 } +typ2l: + | typ3 op2 typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ2l op2l typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ3 { $1 } +typ2r: + | typ3 op2 typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ3 op2r typ2r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ3 { $1 } + +typ3: + | typ4 op3 typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ3l op3l typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ4 op3r typ3r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ4 { $1 } +typ3l: + | typ4 op3 typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ3l op3l typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ4 { $1 } +typ3r: + | typ4 op3 typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ4 op3r typ3r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ4 { $1 } + +typ4: + | typ5 op4 typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ4l op4l typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ5 op4r typ4r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ5 { $1 } +typ4l: + | typ5 op4 typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ4l op4l typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ5 { $1 } +typ4r: + | typ5 op4 typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ5 op4r typ4r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ5 { $1 } + +typ5: + | typ6 op5 typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ5l op5l typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ6 op5r typ5r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ6 { $1 } +typ5l: + | typ6 op5 typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ5l op5l typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ6 { $1 } +typ5r: + | typ6 op5 typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ6 op5r typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ6 { $1 } + +typ6: + | typ7 op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ6l op6l typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ7 op6r typ6r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ6l Plus typ7 { mk_typ (ATyp_sum ($1, $3)) $startpos $endpos } + | typ6l Minus typ7 { mk_typ (ATyp_minus ($1, $3)) $startpos $endpos } + | typ7 { $1 } +typ6l: + | typ7 op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ6l op6l typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ6l Plus typ7 { mk_typ (ATyp_sum ($1, $3)) $startpos $endpos } + | typ6l Minus typ7 { mk_typ (ATyp_minus ($1, $3)) $startpos $endpos } + | typ7 { $1 } +typ6r: + | typ7 op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ7 op6r typ6r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ7 { $1 } + +typ7: + | typ8 op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ7l op7l typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ8 op7r typ7r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ7l Star typ8 { mk_typ (ATyp_times ($1, $3)) $startpos $endpos } + | typ8 { $1 } +typ7l: + | typ8 op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ7l op7l typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ7l Star typ8 { mk_typ (ATyp_times ($1, $3)) $startpos $endpos } + | typ8 { $1 } +typ7r: + | typ8 op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ8 op7r typ7r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ8 { $1 } + +typ8: + | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos } + | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos} + | typ9 { $1 } +typ8l: + | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos } + | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos} + | typ9 { $1 } +typ8r: + | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos } + | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos} + | typ9 { $1 } + +typ9: + | atomic_typ op9 atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ9l op9l atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | atomic_typ op9r typ9r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | atomic_typ { $1 } +typ9l: + | atomic_typ op9 atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | typ9l op9l atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | atomic_typ { $1 } +typ9r: + | atomic_typ op9 atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | atomic_typ op9r typ9r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } + | atomic_typ { $1 } + +atomic_typ: + | id + { mk_typ (ATyp_id $1) $startpos $endpos } + | kid + { mk_typ (ATyp_var $1) $startpos $endpos } + | Num + { mk_typ (ATyp_constant $1) $startpos $endpos } + | Dec + { mk_typ ATyp_dec $startpos $endpos } + | Inc + { mk_typ ATyp_inc $startpos $endpos } + | id Lparen typ_list Rparen + { mk_typ (ATyp_app ($1, $3)) $startpos $endpos } + | Register Lparen typ Rparen + { let register_id = mk_id (Id "register") $startpos($1) $endpos($1) in + mk_typ (ATyp_app (register_id, [$3])) $startpos $endpos } + | Ref Lparen typ Rparen + { let ref_id = mk_id (Id "ref") $startpos($1) $endpos($1) in + mk_typ (ATyp_app (ref_id, [$3])) $startpos $endpos } + | Lparen typ Rparen + { $2 } + | Lparen typ Comma typ_list Rparen + { mk_typ (ATyp_tup ($2 :: $4)) $startpos $endpos } + | LcurlyBar num_list RcurlyBar + { let v = mk_kid "n" $startpos $endpos in + let atom_id = mk_id (Id "atom") $startpos $endpos in + let atom_of_v = mk_typ (ATyp_app (atom_id, [mk_typ (ATyp_var v) $startpos $endpos])) $startpos $endpos in + mk_typ (ATyp_exist ([v], NC_aux (NC_set (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos } + | Lcurly kid_list Dot typ Rcurly + { mk_typ (ATyp_exist ($2, NC_aux (NC_true, loc $startpos $endpos), $4)) $startpos $endpos } + | Lcurly kid_list Comma nc Dot typ Rcurly + { mk_typ (ATyp_exist ($2, $4, $6)) $startpos $endpos } + +typ_list: + | typ + { [$1] } + | typ Comma typ_list + { $1 :: $3 } + +base_kind: + | Int + { BK_aux (BK_nat, loc $startpos $endpos) } + | TYPE + { BK_aux (BK_type, loc $startpos $endpos) } + | Order + { BK_aux (BK_order, loc $startpos $endpos) } + +kind: + | base_kind + { K_aux (K_kind [$1], loc $startpos $endpos) } + +kopt: + | Lparen kid Colon kind Rparen + { KOpt_aux (KOpt_kind ($4, $2), loc $startpos $endpos) } + | kid + { KOpt_aux (KOpt_none $1, loc $startpos $endpos) } + +kopt_list: + | kopt + { [$1] } + | kopt kopt_list + { $1 :: $2 } + +typquant: + | kopt_list Comma nc + { let qi_nc = QI_aux (QI_const $3, loc $startpos($3) $endpos($3)) in + TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1 @ [qi_nc]), loc $startpos $endpos) } + | kopt_list + { TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1), loc $startpos $endpos) } + +effect: + | Barr + { mk_effect BE_barr $startpos $endpos } + | Depend + { mk_effect BE_depend $startpos $endpos } + | Rreg + { mk_effect BE_rreg $startpos $endpos } + | Wreg + { mk_effect BE_wreg $startpos $endpos } + | Rmem + { mk_effect BE_rmem $startpos $endpos } + | Rmemt + { mk_effect BE_rmemt $startpos $endpos } + | Wmem + { mk_effect BE_wmem $startpos $endpos } + | Wmv + { mk_effect BE_wmv $startpos $endpos } + | Wmvt + { mk_effect BE_wmvt $startpos $endpos } + | Eamem + { mk_effect BE_eamem $startpos $endpos } + | Exmem + { mk_effect BE_exmem $startpos $endpos } + | Undef + { mk_effect BE_undef $startpos $endpos } + | Unspec + { mk_effect BE_unspec $startpos $endpos } + | Nondet + { mk_effect BE_nondet $startpos $endpos } + | Escape + { mk_effect BE_escape $startpos $endpos } + +effect_list: + | effect + { [$1] } + | effect Comma effect_list + { $1::$3 } + +effect_set: + | Lcurly effect_list Rcurly + { mk_typ (ATyp_set $2) $startpos $endpos } + | Pure + { mk_typ (ATyp_set []) $startpos $endpos } + +typschm: + | typ MinusGt typ + { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_fn ($1, $3, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos } + | Forall typquant Dot typ MinusGt typ + { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos } + | typ MinusGt typ Effect effect_set + { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_fn ($1, $3, $5)) s e) s e) $startpos $endpos } + | Forall typquant Dot typ MinusGt typ Effect effect_set + { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, $8)) s e) s e) $startpos $endpos } + +typschm_eof: + | typschm Eof + { $1 } + +pat1: + | atomic_pat + { $1 } + | atomic_pat At pat_concat + { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos } + +pat_concat: + | atomic_pat + { [$1] } + | atomic_pat At pat_concat + { $1 :: $3 } + +pat: + | pat1 + { $1 } + | pat1 As id + { mk_pat (P_as ($1, $3)) $startpos $endpos } + | pat1 As kid + { mk_pat (P_var ($1, $3)) $startpos $endpos } + +pat_list: + | pat + { [$1] } + | pat Comma pat_list + { $1 :: $3 } + +atomic_pat: + | Under + { mk_pat (P_wild) $startpos $endpos } + | lit + { mk_pat (P_lit $1) $startpos $endpos } + | id + { mk_pat (P_id $1) $startpos $endpos } + | kid + { mk_pat (P_var (mk_pat (P_id (id_of_kid $1)) $startpos $endpos, $1)) $startpos $endpos } + | id Lparen pat_list Rparen + { mk_pat (P_app ($1, $3)) $startpos $endpos } + | atomic_pat Colon typ + { mk_pat (P_typ ($3, $1)) $startpos $endpos } + | Lparen pat Rparen + { $2 } + | Lparen pat Comma pat_list Rparen + { mk_pat (P_tup ($2 :: $4)) $startpos $endpos } + | Lsquare pat_list Rsquare + { mk_pat (P_vector $2) $startpos $endpos } + +lit: + | True + { mk_lit L_true $startpos $endpos } + | False + { mk_lit L_false $startpos $endpos } + | Unit + { mk_lit L_unit $startpos $endpos } + | Num + { mk_lit (L_num $1) $startpos $endpos } + | Undefined + { mk_lit L_undef $startpos $endpos } + | Bitzero + { mk_lit L_zero $startpos $endpos } + | Bitone + { mk_lit L_one $startpos $endpos } + | Bin + { mk_lit (L_bin $1) $startpos $endpos } + | Hex + { mk_lit (L_hex $1) $startpos $endpos } + | String + { mk_lit (L_string $1) $startpos $endpos } + | Real + { mk_lit (L_real $1) $startpos $endpos } + +exp_eof: + | exp Eof + { $1 } + +exp: + | exp0 + { $1 } + | atomic_exp Eq exp + { mk_exp (E_assign ($1, $3)) $startpos $endpos } + | Let_ letbind In exp + { mk_exp (E_let ($2, $4)) $startpos $endpos } + | Var atomic_exp Eq exp In exp + { mk_exp (E_var ($2, $4, $6)) $startpos $endpos } + | Star atomic_exp + { mk_exp (E_deref $2) $startpos $endpos } + | Lcurly block Rcurly + { mk_exp (E_block $2) $startpos $endpos } + | Return exp + { mk_exp (E_return $2) $startpos $endpos } + | Throw exp + { mk_exp (E_throw $2) $startpos $endpos } + | If_ exp Then exp Else exp + { mk_exp (E_if ($2, $4, $6)) $startpos $endpos } + | If_ exp Then exp + { mk_exp (E_if ($2, $4, mk_lit_exp L_unit $endpos($4) $endpos($4))) $startpos $endpos } + | Match exp Lcurly case_list Rcurly + { mk_exp (E_case ($2, $4)) $startpos $endpos } + | Try exp Catch Lcurly case_list Rcurly + { mk_exp (E_try ($2, $5)) $startpos $endpos } + | 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 $startpos $endpos,"Missing \"from\" in foreach loop")); + if $6 <> "to" then + raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" in foreach loop")); + mk_exp (E_for ($3, $5, $7, $9, $11, $13)) $startpos $endpos } + | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp Rparen exp + { if $4 <> "from" then + raise (Parse_error_locn (loc $startpos $endpos,"Missing \"from\" in foreach loop")); + if $6 <> "to" && $6 <> "downto" then + raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" or \"downto\" in foreach loop")); + let order = + if $6 = "to" + then ATyp_aux(ATyp_inc,loc $startpos($6) $endpos($6)) + else ATyp_aux(ATyp_dec,loc $startpos($6) $endpos($6)) + in + mk_exp (E_for ($3, $5, $7, $9, order, $11)) $startpos $endpos } + | Foreach Lparen id Id atomic_exp Id atomic_exp Rparen exp + { if $4 <> "from" then + raise (Parse_error_locn (loc $startpos $endpos,"Missing \"from\" in foreach loop")); + if $6 <> "to" && $6 <> "downto" then + raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" or \"downto\" in foreach loop")); + let step = mk_lit_exp (L_num (Big_int.of_int 1)) $startpos $endpos in + let ord = + if $6 = "to" + then ATyp_aux(ATyp_inc,loc $startpos($6) $endpos($6)) + else ATyp_aux(ATyp_dec,loc $startpos($6) $endpos($6)) + in + mk_exp (E_for ($3, $5, $7, step, ord, $9)) $startpos $endpos } + | Repeat exp Until exp + { mk_exp (E_loop (Until, $4, $2)) $startpos $endpos } + | While exp Do exp + { mk_exp (E_loop (While, $2, $4)) $startpos $endpos } + +/* The following implements all nine levels of user-defined precedence for +operators in expressions, with both left, right and non-associative operators */ + +exp0: + | exp1 op0 exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp0l op0l exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp1 op0r exp0r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp1 { $1 } +exp0l: + | exp1 op0 exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp0l op0l exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp1 { $1 } +exp0r: + | exp1 op0 exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp1 op0r exp0r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp1 { $1 } + +exp1: + | exp2 op1 exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp1l op1l exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp2 op1r exp1r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp2 { $1 } +exp1l: + | exp2 op1 exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp1l op1l exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp2 { $1 } +exp1r: + | exp2 op1 exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp2 op1r exp1r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp2 { $1 } + +exp2: + | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp2l op2l exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp3 { $1 } +exp2l: + | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp2l op2l exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp3 { $1 } +exp2r: + | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp3 { $1 } + +exp3: + | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp3l op3l exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp4 { $1 } +exp3l: + | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp3l op3l exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp4 { $1 } +exp3r: + | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp4 { $1 } + +exp4: + | exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp5 Lt exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp5 Gt exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp5 LtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<=") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp5 GtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">=") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp5 ExclEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "!=") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp4l op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp5 op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp5 { $1 } +exp4l: + | exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp4l op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp5 { $1 } +exp4r: + | exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp5 op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp5 { $1 } + +exp5: + | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp5l op5l exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp6 op5r exp5r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp6 At exp5r { mk_exp (E_vector_append ($1, $3)) $startpos $endpos } + | exp6 { $1 } +exp5l: + | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp5l op5l exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp6 { $1 } +exp5r: + | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp6 op5r exp5r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp6 At exp5r { mk_exp (E_vector_append ($1, $3)) $startpos $endpos } + | exp6 { $1 } + +exp6: + | exp7 op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp6l op6l exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp7 op6r exp6r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp6l Plus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "+") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp6l Minus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "-") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp7 { $1 } +exp6l: + | exp7 op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp6l op6l exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp6l Plus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "+") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp6l Minus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "-") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp7 { $1 } +exp6r: + | exp7 op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp7 op6r exp6r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp7 { $1 } + +exp7: + | exp8 op7 exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp7l op7l exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp8 op7r exp7r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp7l Star exp8 { mk_exp (E_app_infix ($1, mk_id (Id "*") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp8 { $1 } +exp7l: + | exp8 op7 exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp7l op7l exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp7l Star exp8 { mk_exp (E_app_infix ($1, mk_id (Id "*") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | exp8 { $1 } +exp7r: + | exp8 op7 exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp8 op7r exp7r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp8 { $1 } + +exp8: + | exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp8l op8l exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp9 op8r exp8r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp9 Caret exp8r { mk_exp (E_app_infix ($1, mk_id (Id "^") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos } + | exp9 { $1 } +exp8l: + | exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp8l op8l exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos } + | exp9 { $1 } +exp8r: + | exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp9 op8r exp8r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp9 Caret exp8r { mk_exp (E_app_infix ($1, mk_id (Id "^") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos } + | exp9 { $1 } + +exp9: + | atomic_exp op9 atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp9l op9l atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | atomic_exp op9r exp9r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | atomic_exp { $1 } +exp9l: + | atomic_exp op9 atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | exp9l op9l atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | atomic_exp { $1 } +exp9r: + | atomic_exp op9 atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | atomic_exp op9r exp9r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } + | atomic_exp { $1 } + +case: + | pat EqGt exp + { mk_pexp (Pat_exp ($1, $3)) $startpos $endpos } + | pat If_ exp EqGt exp + { mk_pexp (Pat_when ($1, $3, $5)) $startpos $endpos } + +case_list: + | case + { [$1] } + | case Comma case_list + { $1 :: $3 } + +block: + | exp + { [$1] } + | Let_ letbind Semi block + { [mk_exp (E_let ($2, mk_exp (E_block $4) $startpos($4) $endpos)) $startpos $endpos] } + | Var atomic_exp Eq exp Semi block + { [mk_exp (E_var ($2, $4, mk_exp (E_block $6) $startpos($6) $endpos)) $startpos $endpos] } + | exp Semi /* Allow trailing semicolon in block */ + { [$1] } + | exp Semi block + { $1 :: $3 } + +%inline letbind: + | pat Eq exp + { LB_aux (LB_val ($1, $3), loc $startpos $endpos) } + +atomic_exp: + | atomic_exp Colon atomic_typ + { mk_exp (E_cast ($3, $1)) $startpos $endpos } + | lit + { mk_exp (E_lit $1) $startpos $endpos } + | id MinusGt id Unit + { mk_exp (E_app (prepend_id "_mod_" $3, [mk_exp (E_ref $1) $startpos($1) $endpos($1)])) $startpos $endpos } + | id MinusGt id Lparen exp_list Rparen + { mk_exp (E_app (prepend_id "_mod_" $3, mk_exp (E_ref $1) $startpos($1) $endpos($1) :: $5)) $startpos $endpos } + | atomic_exp Dot id Unit + { mk_exp (E_app (prepend_id "_mod_" $3, [$1])) $startpos $endpos } + | atomic_exp Dot id Lparen exp_list Rparen + { mk_exp (E_app (prepend_id "_mod_" $3, $1 :: $5)) $startpos $endpos } + | atomic_exp Dot id + { mk_exp (E_field ($1, $3)) $startpos $endpos } + | id + { mk_exp (E_id $1) $startpos $endpos } + | kid + { mk_exp (E_sizeof (mk_typ (ATyp_var $1) $startpos $endpos)) $startpos $endpos } + | Ref id + { mk_exp (E_ref $2) $startpos $endpos } + | id Unit + { mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos } + | id Lparen exp_list Rparen + { mk_exp (E_app ($1, $3)) $startpos $endpos } + | Exit Lparen exp Rparen + { mk_exp (E_exit $3) $startpos $endpos } + | Sizeof Lparen typ Rparen + { mk_exp (E_sizeof $3) $startpos $endpos } + | Constraint Lparen nc Rparen + { mk_exp (E_constraint $3) $startpos $endpos } + | Assert Lparen exp Rparen + { mk_exp (E_assert ($3, mk_lit_exp (L_string "") $startpos($4) $endpos($4))) $startpos $endpos } + | Assert Lparen exp Comma exp Rparen + { mk_exp (E_assert ($3, $5)) $startpos $endpos } + | atomic_exp Lsquare exp Rsquare + { mk_exp (E_vector_access ($1, $3)) $startpos $endpos } + | atomic_exp Lsquare exp DotDot exp Rsquare + { mk_exp (E_vector_subrange ($1, $3, $5)) $startpos $endpos } + | Record Lcurly fexp_exp_list Rcurly + { mk_exp (E_record $3) $startpos $endpos } + | Lcurly exp With fexp_exp_list Rcurly + { mk_exp (E_record_update ($2, $4)) $startpos $endpos } + | Lsquare exp_list Rsquare + { mk_exp (E_vector $2) $startpos $endpos } + | Lsquare exp With atomic_exp Eq exp Rsquare + { mk_exp (E_vector_update ($2, $4, $6)) $startpos $endpos } + | Lsquare exp With atomic_exp DotDot atomic_exp Eq exp Rsquare + { mk_exp (E_vector_update_subrange ($2, $4, $6, $8)) $startpos $endpos } + | LsquareBar exp_list RsquareBar + { mk_exp (E_list $2) $startpos $endpos } + | Lparen exp Rparen + { $2 } + | Lparen exp Comma exp_list Rparen + { mk_exp (E_tuple ($2 :: $4)) $startpos $endpos } + +fexp_exp: + | atomic_exp Eq exp + { mk_exp (E_app_infix ($1, mk_id (Id "=") $startpos($2) $endpos($2), $3)) $startpos $endpos } + +fexp_exp_list: + | fexp_exp + { [$1] } + | fexp_exp Comma fexp_exp_list + { $1 :: $3 } + +exp_list: + | exp + { [$1] } + | exp Comma exp_list + { $1 :: $3 } + +funcl_patexp: + | pat Eq exp + { mk_pexp (Pat_exp ($1, $3)) $startpos $endpos } + | Lparen pat If_ exp Rparen Eq exp + { mk_pexp (Pat_when ($2, $4, $7)) $startpos $endpos } + +funcl: + | id funcl_patexp + { mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos } + +funcls: + | id funcl_patexp + { [mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos] } + | id funcl_patexp And funcls + { mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos :: $4 } + +index_range: + | Num + { mk_ir (BF_single $1) $startpos $endpos } + | Num DotDot Num + { mk_ir (BF_range ($1, $3)) $startpos $endpos } + +r_id_def: + | id Colon index_range + { $1, $3 } + +r_def_body: + | r_id_def + { [$1] } + | r_id_def Comma + { [$1] } + | r_id_def Comma r_def_body + { $1 :: $3 } + +type_def: + | Typedef id typquant Eq typ + { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm $3 $5 $startpos($3) $endpos)) $startpos $endpos } + | Typedef id Eq typ + { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm mk_typqn $4 $startpos($4) $endpos)) $startpos $endpos } + | Struct id Eq Lcurly struct_fields Rcurly + { mk_td (TD_record ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos } + | Struct id typquant Eq Lcurly struct_fields Rcurly + { mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos } + | Enum id Eq enum_bar + { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos } + | Enum id Eq Lcurly enum Rcurly + { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos } + | Newtype id Eq type_union + { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), [$4], false)) $startpos $endpos } + | Newtype id typquant Eq type_union + { mk_td (TD_variant ($2, mk_namesectn, $3, [$5], false)) $startpos $endpos } + | Union id Eq Lcurly type_unions Rcurly + { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos } + | Union id typquant Eq Lcurly type_unions Rcurly + { mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos } + | Bitfield id Colon typ Eq Lcurly r_def_body Rcurly + { mk_td (TD_bitfield ($2, $4, $7)) $startpos $endpos } + +enum_bar: + | id + { [$1] } + | id Bar enum_bar + { $1 :: $3 } + +enum: + | id + { [$1] } + | id Comma enum + { $1 :: $3 } + +struct_field: + | id Colon typ + { ($3, $1) } + +struct_fields: + | struct_field + { [$1] } + | struct_field Comma + { [$1] } + | struct_field Comma struct_fields + { $1 :: $3 } + +type_union: + | id Colon typ + { Tu_aux (Tu_ty_id ($3, $1), loc $startpos $endpos) } + | id + { Tu_aux (Tu_id $1, loc $startpos $endpos) } + +type_unions: + | type_union + { [$1] } + | type_union Comma + { [$1] } + | type_union Comma type_unions + { $1 :: $3 } + +fun_def: + | Function_ funcls + { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos } + +fun_def_list: + | fun_def + { [$1] } + | fun_def fun_def_list + { $1 :: $2 } + +let_def: + | Let_ letbind + { $2 } + +externs: + | id Colon String + { [(string_of_id $1, $3)] } + | id Colon String Comma externs + { (string_of_id $1, $3) :: $5 } + +val_spec_def: + | Val id Colon typschm + { mk_vs (VS_val_spec ($4, $2, (fun _ -> None), false)) $startpos $endpos } + | Val Cast id Colon typschm + { mk_vs (VS_val_spec ($5, $3, (fun _ -> None), true)) $startpos $endpos } + | Val id Eq String Colon typschm + { mk_vs (VS_val_spec ($6, $2, (fun _ -> Some $4), false)) $startpos $endpos } + | Val Cast id Eq String Colon typschm + { mk_vs (VS_val_spec ($7, $3, (fun _ -> Some $5), true)) $startpos $endpos } + | Val String Colon typschm + { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), (fun _ -> Some $2), false)) $startpos $endpos } + | Val Cast String Colon typschm + { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), (fun _ -> Some $3), true)) $startpos $endpos } + | Val id Eq Lcurly externs Rcurly Colon typschm + { mk_vs (VS_val_spec ($8, $2, (fun backend -> (assoc_opt backend $5)), false)) $startpos $endpos } + | Val Cast id Eq Lcurly externs Rcurly Colon typschm + { mk_vs (VS_val_spec ($9, $3, (fun backend -> (assoc_opt backend $6)), true)) $startpos $endpos } + +register_def: + | Register id Colon typ + { mk_reg_dec (DEC_reg ($4, $2)) $startpos $endpos } + +default_def: + | Default base_kind Inc + { mk_default (DT_order ($2, mk_typ ATyp_inc $startpos($3) $endpos)) $startpos $endpos } + | Default base_kind Dec + { mk_default (DT_order ($2, mk_typ ATyp_dec $startpos($3) $endpos)) $startpos $endpos } + +scattered_def: + | Union id typquant + { mk_sd (SD_scattered_variant($2, mk_namesectn, $3)) $startpos $endpos } + | Union id + { mk_sd (SD_scattered_variant($2, mk_namesectn, mk_typqn)) $startpos $endpos } + | Function_ id + { mk_sd (SD_scattered_function(mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos } + +def: + | fun_def + { DEF_fundef $1 } + | Fixity + { let (prec, n, op) = $1 in DEF_fixity (prec, n, Id_aux (Id op, loc $startpos $endpos)) } + | val_spec_def + { DEF_spec $1 } + | type_def + { DEF_type $1 } + | let_def + { DEF_val $1 } + | register_def + { DEF_reg_dec $1 } + | Overload id Eq Lcurly id_list Rcurly + { DEF_overload ($2, $5) } + | Overload id Eq enum_bar + { DEF_overload ($2, $4) } + | Scattered scattered_def + { DEF_scattered $2 } + | Function_ Clause funcl + { DEF_scattered (mk_sd (SD_scattered_funcl $3) $startpos $endpos) } + | Union Clause id Eq type_union + { DEF_scattered (mk_sd (SD_scattered_unioncl ($3, $5)) $startpos $endpos) } + | End id + { DEF_scattered (mk_sd (SD_scattered_end $2) $startpos $endpos) } + | default_def + { DEF_default $1 } + | Mutual Lcurly fun_def_list Rcurly + { DEF_internal_mutrec $3 } + +defs_list: + | def + { [$1] } + | def defs_list + { $1::$2 } + +def_eof: + | def Eof + { $1 } + +defs: + | defs_list + { (Defs $1) } + +file: + | defs Eof + { $1 } diff --git a/src/parser2.mly b/src/parser2.mly deleted file mode 100644 index 7af70687..00000000 --- a/src/parser2.mly +++ /dev/null @@ -1,1233 +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 n m = Range (n, m) - -let default_opt x = function - | None -> x - | Some y -> y - -let assoc_opt key assocs = - try Some (List.assoc key assocs) with - | Not_found -> None - -let string_of_id = function - | Id_aux (Id str, _) -> str - | Id_aux (DeIid str, _) -> str - -let prepend_id str1 = function - | Id_aux (Id str2, loc) -> Id_aux (Id (str1 ^ str2), loc) - | _ -> assert false - -let mk_id i n m = Id_aux (i, loc n m) -let mk_kid str n m = Kid_aux (Var str, loc n m) - -let id_of_kid = function - | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l) - -let deinfix = function - | (Id_aux (Id v, l)) -> Id_aux (DeIid v, l) - | (Id_aux (DeIid v, l)) -> Id_aux (Id v, l) - -let mk_effect e n m = BE_aux (e, loc n m) -let mk_typ t n m = ATyp_aux (t, loc n m) -let mk_pat p n m = P_aux (p, loc n m) -let mk_pexp p n m = Pat_aux (p, loc n m) -let mk_exp e n m = E_aux (e, loc n m) -let mk_lit l n m = L_aux (l, loc n m) -let mk_lit_exp l n m = mk_exp (E_lit (mk_lit l n m)) n m -let mk_typschm tq t n m = TypSchm_aux (TypSchm_ts (tq, t), loc n m) -let mk_nc nc n m = NC_aux (nc, loc n m) -let mk_sd s n m = SD_aux (s, loc n m) -let mk_ir r n m = BF_aux (r, loc n m) - -let mk_funcl f n m = FCL_aux (f, loc n m) -let mk_fun fn n m = FD_aux (fn, loc n m) -let mk_td t n m = TD_aux (t, loc n m) -let mk_vs v n m = VS_aux (v, loc n m) -let mk_reg_dec d n m = DEC_aux (d, loc n m) -let mk_default d n m = DT_aux (d, loc n m) - -let qi_id_of_kopt (KOpt_aux (kopt_aux, l) as kopt) = QI_aux (QI_id kopt, l) - -let mk_recn = (Rec_aux((Rec_nonrec), Unknown)) -let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown)) -let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown) -let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown) -let mk_namesectn = Name_sect_aux(Name_sect_none,Unknown) - -type lchain = - LC_lt -| LC_lteq -| LC_nexp of atyp - -let rec desugar_lchain chain s e = - match chain with - | [LC_nexp n1; LC_lteq; LC_nexp n2] -> - mk_nc (NC_bounded_le (n1, n2)) s e - | [LC_nexp n1; LC_lt; LC_nexp n2] -> - mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e, n2)) s e - | (LC_nexp n1 :: LC_lteq :: LC_nexp n2 :: chain) -> - let nc1 = mk_nc (NC_bounded_le (n1, n2)) s e in - mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e - | (LC_nexp n1 :: LC_lt :: LC_nexp n2 :: chain) -> - let nc1 = mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e, n2)) s e in - mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e - | _ -> assert false - -type rchain = - RC_gt -| RC_gteq -| RC_nexp of atyp - -let rec desugar_rchain chain s e = - match chain with - | [RC_nexp n1; RC_gteq; RC_nexp n2] -> - mk_nc (NC_bounded_ge (n1, n2)) s e - | [RC_nexp n1; RC_gt; RC_nexp n2] -> - mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e)) s e - | (RC_nexp n1 :: RC_gteq :: RC_nexp n2 :: chain) -> - let nc1 = mk_nc (NC_bounded_ge (n1, n2)) s e in - mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e - | (RC_nexp n1 :: RC_gt :: RC_nexp n2 :: chain) -> - let nc1 = mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e)) s e in - mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e - | _ -> assert false - -%} - -/*Terminals with no content*/ - -%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op -%token Enum Else False Forall Foreach Overload Function_ If_ In Inc Let_ Int Order Cast -%token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef -%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield -%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape -%token Repeat Until While Do Record Mutual Var Ref - -%nonassoc Then -%nonassoc Else - -%token Bar Comma Dot Eof Minus Semi Under DotDot -%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar LsquareBar RsquareBar -%token MinusGt - -/*Terminals with content*/ - -%token Id TyVar -%token Num -%token String Bin Hex Real - -%token Amp At Caret Eq Gt Lt Plus Star EqGt Unit -%token Colon ExclEq -%token GtEq -%token LtEq - -%token Op0 Op1 Op2 Op3 Op4 Op5 Op6 Op7 Op8 Op9 -%token Op0l Op1l Op2l Op3l Op4l Op5l Op6l Op7l Op8l Op9l -%token Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r - -%token Fixity - -%start file -%start typschm_eof -%start exp_eof -%start def_eof -%type typschm_eof -%type exp_eof -%type def_eof -%type file - -%% - -id: - | Id { mk_id (Id $1) $startpos $endpos } - - | Op Op0 { mk_id (DeIid $2) $startpos $endpos } - | Op Op1 { mk_id (DeIid $2) $startpos $endpos } - | Op Op2 { mk_id (DeIid $2) $startpos $endpos } - | Op Op3 { mk_id (DeIid $2) $startpos $endpos } - | Op Op4 { mk_id (DeIid $2) $startpos $endpos } - | Op Op5 { mk_id (DeIid $2) $startpos $endpos } - | Op Op6 { mk_id (DeIid $2) $startpos $endpos } - | Op Op7 { mk_id (DeIid $2) $startpos $endpos } - | Op Op8 { mk_id (DeIid $2) $startpos $endpos } - | Op Op9 { mk_id (DeIid $2) $startpos $endpos } - - | Op Op0l { mk_id (DeIid $2) $startpos $endpos } - | Op Op1l { mk_id (DeIid $2) $startpos $endpos } - | Op Op2l { mk_id (DeIid $2) $startpos $endpos } - | Op Op3l { mk_id (DeIid $2) $startpos $endpos } - | Op Op4l { mk_id (DeIid $2) $startpos $endpos } - | Op Op5l { mk_id (DeIid $2) $startpos $endpos } - | Op Op6l { mk_id (DeIid $2) $startpos $endpos } - | Op Op7l { mk_id (DeIid $2) $startpos $endpos } - | Op Op8l { mk_id (DeIid $2) $startpos $endpos } - | Op Op9l { mk_id (DeIid $2) $startpos $endpos } - - | Op Op0r { mk_id (DeIid $2) $startpos $endpos } - | Op Op1r { mk_id (DeIid $2) $startpos $endpos } - | Op Op2r { mk_id (DeIid $2) $startpos $endpos } - | Op Op3r { mk_id (DeIid $2) $startpos $endpos } - | Op Op4r { mk_id (DeIid $2) $startpos $endpos } - | Op Op5r { mk_id (DeIid $2) $startpos $endpos } - | Op Op6r { mk_id (DeIid $2) $startpos $endpos } - | Op Op7r { mk_id (DeIid $2) $startpos $endpos } - | Op Op8r { mk_id (DeIid $2) $startpos $endpos } - | Op Op9r { mk_id (DeIid $2) $startpos $endpos } - - | Op Plus { mk_id (DeIid "+") $startpos $endpos } - | Op Minus { mk_id (DeIid "-") $startpos $endpos } - | Op Star { mk_id (DeIid "*") $startpos $endpos } - | Op ExclEq { mk_id (DeIid "!=") $startpos $endpos } - | Op Lt { mk_id (DeIid "<") $startpos $endpos } - | Op Gt { mk_id (DeIid ">") $startpos $endpos } - | Op LtEq { mk_id (DeIid "<=") $startpos $endpos } - | Op GtEq { mk_id (DeIid ">=") $startpos $endpos } - | Op Amp { mk_id (DeIid "&") $startpos $endpos } - | Op Bar { mk_id (DeIid "|") $startpos $endpos } - | Op Caret { mk_id (DeIid "^") $startpos $endpos } - -op0: Op0 { mk_id (Id $1) $startpos $endpos } -op1: Op1 { mk_id (Id $1) $startpos $endpos } -op2: Op2 { mk_id (Id $1) $startpos $endpos } -op3: Op3 { mk_id (Id $1) $startpos $endpos } -op4: Op4 { mk_id (Id $1) $startpos $endpos } -op5: Op5 { mk_id (Id $1) $startpos $endpos } -op6: Op6 { mk_id (Id $1) $startpos $endpos } -op7: Op7 { mk_id (Id $1) $startpos $endpos } -op8: Op8 { mk_id (Id $1) $startpos $endpos } -op9: Op9 { mk_id (Id $1) $startpos $endpos } - -op0l: Op0l { mk_id (Id $1) $startpos $endpos } -op1l: Op1l { mk_id (Id $1) $startpos $endpos } -op2l: Op2l { mk_id (Id $1) $startpos $endpos } -op3l: Op3l { mk_id (Id $1) $startpos $endpos } -op4l: Op4l { mk_id (Id $1) $startpos $endpos } -op5l: Op5l { mk_id (Id $1) $startpos $endpos } -op6l: Op6l { mk_id (Id $1) $startpos $endpos } -op7l: Op7l { mk_id (Id $1) $startpos $endpos } -op8l: Op8l { mk_id (Id $1) $startpos $endpos } -op9l: Op9l { mk_id (Id $1) $startpos $endpos } - -op0r: Op0r { mk_id (Id $1) $startpos $endpos } -op1r: Op1r { mk_id (Id $1) $startpos $endpos } -op2r: Op2r { mk_id (Id $1) $startpos $endpos } -op3r: Op3r { mk_id (Id $1) $startpos $endpos } -op4r: Op4r { mk_id (Id $1) $startpos $endpos } -op5r: Op5r { mk_id (Id $1) $startpos $endpos } -op6r: Op6r { mk_id (Id $1) $startpos $endpos } -op7r: Op7r { mk_id (Id $1) $startpos $endpos } -op8r: Op8r { mk_id (Id $1) $startpos $endpos } -op9r: Op9r { mk_id (Id $1) $startpos $endpos } - -id_list: - | id - { [$1] } - | id Comma id_list - { $1 :: $3 } - -kid: - | TyVar - { mk_kid $1 $startpos $endpos } - -kid_list: - | kid - { [$1] } - | kid kid_list - { $1 :: $2 } - -nc: - | nc Bar nc_and - { mk_nc (NC_or ($1, $3)) $startpos $endpos } - | nc_and - { $1 } - -nc_and: - | nc_and Amp atomic_nc - { mk_nc (NC_and ($1, $3)) $startpos $endpos } - | atomic_nc - { $1 } - -atomic_nc: - | True - { mk_nc NC_true $startpos $endpos } - | False - { mk_nc NC_false $startpos $endpos } - | typ Eq typ - { mk_nc (NC_equal ($1, $3)) $startpos $endpos } - | typ ExclEq typ - { mk_nc (NC_not_equal ($1, $3)) $startpos $endpos } - | nc_lchain - { desugar_lchain $1 $startpos $endpos } - | nc_rchain - { desugar_rchain $1 $startpos $endpos } - | Lparen nc Rparen - { $2 } - | kid In Lcurly num_list Rcurly - { mk_nc (NC_set ($1, $4)) $startpos $endpos } - -num_list: - | Num - { [$1] } - | Num Comma num_list - { $1 :: $3 } - -nc_lchain: - | typ LtEq typ - { [LC_nexp $1; LC_lteq; LC_nexp $3] } - | typ Lt typ - { [LC_nexp $1; LC_lt; LC_nexp $3] } - | typ LtEq nc_lchain - { LC_nexp $1 :: LC_lteq :: $3 } - | typ Lt nc_lchain - { LC_nexp $1 :: LC_lt :: $3 } - -nc_rchain: - | typ GtEq typ - { [RC_nexp $1; RC_gteq; RC_nexp $3] } - | typ Gt typ - { [RC_nexp $1; RC_gt; RC_nexp $3] } - | typ GtEq nc_rchain - { RC_nexp $1 :: RC_gteq :: $3 } - | typ Gt nc_rchain - { RC_nexp $1 :: RC_gt :: $3 } - -typ: - | typ0 - { $1 } - -/* The following implements all nine levels of user-defined precedence for -operators in types, with both left, right and non-associative operators */ - -typ0: - | typ1 op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ0l op0l typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ1 op0r typ0r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ1 { $1 } -typ0l: - | typ1 op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ0l op0l typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ1 { $1 } -typ0r: - | typ1 op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ1 op0r typ0r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ1 { $1 } - -typ1: - | typ2 op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ1l op1l typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ2 op1r typ1r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ2 { $1 } -typ1l: - | typ2 op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ1l op1l typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ2 { $1 } -typ1r: - | typ2 op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ2 op1r typ1r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ2 { $1 } - -typ2: - | typ3 op2 typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ2l op2l typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ3 op2r typ2r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ3 { $1 } -typ2l: - | typ3 op2 typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ2l op2l typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ3 { $1 } -typ2r: - | typ3 op2 typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ3 op2r typ2r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ3 { $1 } - -typ3: - | typ4 op3 typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ3l op3l typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ4 op3r typ3r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ4 { $1 } -typ3l: - | typ4 op3 typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ3l op3l typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ4 { $1 } -typ3r: - | typ4 op3 typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ4 op3r typ3r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ4 { $1 } - -typ4: - | typ5 op4 typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ4l op4l typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ5 op4r typ4r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ5 { $1 } -typ4l: - | typ5 op4 typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ4l op4l typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ5 { $1 } -typ4r: - | typ5 op4 typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ5 op4r typ4r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ5 { $1 } - -typ5: - | typ6 op5 typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ5l op5l typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ6 op5r typ5r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ6 { $1 } -typ5l: - | typ6 op5 typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ5l op5l typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ6 { $1 } -typ5r: - | typ6 op5 typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ6 op5r typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ6 { $1 } - -typ6: - | typ7 op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ6l op6l typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ7 op6r typ6r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ6l Plus typ7 { mk_typ (ATyp_sum ($1, $3)) $startpos $endpos } - | typ6l Minus typ7 { mk_typ (ATyp_minus ($1, $3)) $startpos $endpos } - | typ7 { $1 } -typ6l: - | typ7 op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ6l op6l typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ6l Plus typ7 { mk_typ (ATyp_sum ($1, $3)) $startpos $endpos } - | typ6l Minus typ7 { mk_typ (ATyp_minus ($1, $3)) $startpos $endpos } - | typ7 { $1 } -typ6r: - | typ7 op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ7 op6r typ6r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ7 { $1 } - -typ7: - | typ8 op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ7l op7l typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ8 op7r typ7r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ7l Star typ8 { mk_typ (ATyp_times ($1, $3)) $startpos $endpos } - | typ8 { $1 } -typ7l: - | typ8 op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ7l op7l typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ7l Star typ8 { mk_typ (ATyp_times ($1, $3)) $startpos $endpos } - | typ8 { $1 } -typ7r: - | typ8 op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ8 op7r typ7r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ8 { $1 } - -typ8: - | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos } - | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos} - | typ9 { $1 } -typ8l: - | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos } - | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos} - | typ9 { $1 } -typ8r: - | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos } - | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos} - | typ9 { $1 } - -typ9: - | atomic_typ op9 atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ9l op9l atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | atomic_typ op9r typ9r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | atomic_typ { $1 } -typ9l: - | atomic_typ op9 atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | typ9l op9l atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | atomic_typ { $1 } -typ9r: - | atomic_typ op9 atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | atomic_typ op9r typ9r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos } - | atomic_typ { $1 } - -atomic_typ: - | id - { mk_typ (ATyp_id $1) $startpos $endpos } - | kid - { mk_typ (ATyp_var $1) $startpos $endpos } - | Num - { mk_typ (ATyp_constant $1) $startpos $endpos } - | Dec - { mk_typ ATyp_dec $startpos $endpos } - | Inc - { mk_typ ATyp_inc $startpos $endpos } - | id Lparen typ_list Rparen - { mk_typ (ATyp_app ($1, $3)) $startpos $endpos } - | Register Lparen typ Rparen - { let register_id = mk_id (Id "register") $startpos($1) $endpos($1) in - mk_typ (ATyp_app (register_id, [$3])) $startpos $endpos } - | Ref Lparen typ Rparen - { let ref_id = mk_id (Id "ref") $startpos($1) $endpos($1) in - mk_typ (ATyp_app (ref_id, [$3])) $startpos $endpos } - | Lparen typ Rparen - { $2 } - | Lparen typ Comma typ_list Rparen - { mk_typ (ATyp_tup ($2 :: $4)) $startpos $endpos } - | LcurlyBar num_list RcurlyBar - { let v = mk_kid "n" $startpos $endpos in - let atom_id = mk_id (Id "atom") $startpos $endpos in - let atom_of_v = mk_typ (ATyp_app (atom_id, [mk_typ (ATyp_var v) $startpos $endpos])) $startpos $endpos in - mk_typ (ATyp_exist ([v], NC_aux (NC_set (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos } - | Lcurly kid_list Dot typ Rcurly - { mk_typ (ATyp_exist ($2, NC_aux (NC_true, loc $startpos $endpos), $4)) $startpos $endpos } - | Lcurly kid_list Comma nc Dot typ Rcurly - { mk_typ (ATyp_exist ($2, $4, $6)) $startpos $endpos } - -typ_list: - | typ - { [$1] } - | typ Comma typ_list - { $1 :: $3 } - -base_kind: - | Int - { BK_aux (BK_nat, loc $startpos $endpos) } - | TYPE - { BK_aux (BK_type, loc $startpos $endpos) } - | Order - { BK_aux (BK_order, loc $startpos $endpos) } - -kind: - | base_kind - { K_aux (K_kind [$1], loc $startpos $endpos) } - -kopt: - | Lparen kid Colon kind Rparen - { KOpt_aux (KOpt_kind ($4, $2), loc $startpos $endpos) } - | kid - { KOpt_aux (KOpt_none $1, loc $startpos $endpos) } - -kopt_list: - | kopt - { [$1] } - | kopt kopt_list - { $1 :: $2 } - -typquant: - | kopt_list Comma nc - { let qi_nc = QI_aux (QI_const $3, loc $startpos($3) $endpos($3)) in - TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1 @ [qi_nc]), loc $startpos $endpos) } - | kopt_list - { TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1), loc $startpos $endpos) } - -effect: - | Barr - { mk_effect BE_barr $startpos $endpos } - | Depend - { mk_effect BE_depend $startpos $endpos } - | Rreg - { mk_effect BE_rreg $startpos $endpos } - | Wreg - { mk_effect BE_wreg $startpos $endpos } - | Rmem - { mk_effect BE_rmem $startpos $endpos } - | Rmemt - { mk_effect BE_rmemt $startpos $endpos } - | Wmem - { mk_effect BE_wmem $startpos $endpos } - | Wmv - { mk_effect BE_wmv $startpos $endpos } - | Wmvt - { mk_effect BE_wmvt $startpos $endpos } - | Eamem - { mk_effect BE_eamem $startpos $endpos } - | Exmem - { mk_effect BE_exmem $startpos $endpos } - | Undef - { mk_effect BE_undef $startpos $endpos } - | Unspec - { mk_effect BE_unspec $startpos $endpos } - | Nondet - { mk_effect BE_nondet $startpos $endpos } - | Escape - { mk_effect BE_escape $startpos $endpos } - -effect_list: - | effect - { [$1] } - | effect Comma effect_list - { $1::$3 } - -effect_set: - | Lcurly effect_list Rcurly - { mk_typ (ATyp_set $2) $startpos $endpos } - | Pure - { mk_typ (ATyp_set []) $startpos $endpos } - -typschm: - | typ MinusGt typ - { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_fn ($1, $3, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos } - | Forall typquant Dot typ MinusGt typ - { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos } - | typ MinusGt typ Effect effect_set - { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_fn ($1, $3, $5)) s e) s e) $startpos $endpos } - | Forall typquant Dot typ MinusGt typ Effect effect_set - { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, $8)) s e) s e) $startpos $endpos } - -typschm_eof: - | typschm Eof - { $1 } - -pat1: - | atomic_pat - { $1 } - | atomic_pat At pat_concat - { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos } - -pat_concat: - | atomic_pat - { [$1] } - | atomic_pat At pat_concat - { $1 :: $3 } - -pat: - | pat1 - { $1 } - | pat1 As id - { mk_pat (P_as ($1, $3)) $startpos $endpos } - | pat1 As kid - { mk_pat (P_var ($1, $3)) $startpos $endpos } - -pat_list: - | pat - { [$1] } - | pat Comma pat_list - { $1 :: $3 } - -atomic_pat: - | Under - { mk_pat (P_wild) $startpos $endpos } - | lit - { mk_pat (P_lit $1) $startpos $endpos } - | id - { mk_pat (P_id $1) $startpos $endpos } - | kid - { mk_pat (P_var (mk_pat (P_id (id_of_kid $1)) $startpos $endpos, $1)) $startpos $endpos } - | id Lparen pat_list Rparen - { mk_pat (P_app ($1, $3)) $startpos $endpos } - | atomic_pat Colon typ - { mk_pat (P_typ ($3, $1)) $startpos $endpos } - | Lparen pat Rparen - { $2 } - | Lparen pat Comma pat_list Rparen - { mk_pat (P_tup ($2 :: $4)) $startpos $endpos } - | Lsquare pat_list Rsquare - { mk_pat (P_vector $2) $startpos $endpos } - -lit: - | True - { mk_lit L_true $startpos $endpos } - | False - { mk_lit L_false $startpos $endpos } - | Unit - { mk_lit L_unit $startpos $endpos } - | Num - { mk_lit (L_num $1) $startpos $endpos } - | Undefined - { mk_lit L_undef $startpos $endpos } - | Bitzero - { mk_lit L_zero $startpos $endpos } - | Bitone - { mk_lit L_one $startpos $endpos } - | Bin - { mk_lit (L_bin $1) $startpos $endpos } - | Hex - { mk_lit (L_hex $1) $startpos $endpos } - | String - { mk_lit (L_string $1) $startpos $endpos } - | Real - { mk_lit (L_real $1) $startpos $endpos } - -exp_eof: - | exp Eof - { $1 } - -exp: - | exp0 - { $1 } - | atomic_exp Eq exp - { mk_exp (E_assign ($1, $3)) $startpos $endpos } - | Let_ letbind In exp - { mk_exp (E_let ($2, $4)) $startpos $endpos } - | Var atomic_exp Eq exp In exp - { mk_exp (E_var ($2, $4, $6)) $startpos $endpos } - | Star atomic_exp - { mk_exp (E_deref $2) $startpos $endpos } - | Lcurly block Rcurly - { mk_exp (E_block $2) $startpos $endpos } - | Return exp - { mk_exp (E_return $2) $startpos $endpos } - | Throw exp - { mk_exp (E_throw $2) $startpos $endpos } - | If_ exp Then exp Else exp - { mk_exp (E_if ($2, $4, $6)) $startpos $endpos } - | If_ exp Then exp - { mk_exp (E_if ($2, $4, mk_lit_exp L_unit $endpos($4) $endpos($4))) $startpos $endpos } - | Match exp Lcurly case_list Rcurly - { mk_exp (E_case ($2, $4)) $startpos $endpos } - | Try exp Catch Lcurly case_list Rcurly - { mk_exp (E_try ($2, $5)) $startpos $endpos } - | 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 $startpos $endpos,"Missing \"from\" in foreach loop")); - if $6 <> "to" then - raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" in foreach loop")); - mk_exp (E_for ($3, $5, $7, $9, $11, $13)) $startpos $endpos } - | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp Rparen exp - { if $4 <> "from" then - raise (Parse_error_locn (loc $startpos $endpos,"Missing \"from\" in foreach loop")); - if $6 <> "to" && $6 <> "downto" then - raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" or \"downto\" in foreach loop")); - let order = - if $6 = "to" - then ATyp_aux(ATyp_inc,loc $startpos($6) $endpos($6)) - else ATyp_aux(ATyp_dec,loc $startpos($6) $endpos($6)) - in - mk_exp (E_for ($3, $5, $7, $9, order, $11)) $startpos $endpos } - | Foreach Lparen id Id atomic_exp Id atomic_exp Rparen exp - { if $4 <> "from" then - raise (Parse_error_locn (loc $startpos $endpos,"Missing \"from\" in foreach loop")); - if $6 <> "to" && $6 <> "downto" then - raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" or \"downto\" in foreach loop")); - let step = mk_lit_exp (L_num (Big_int.of_int 1)) $startpos $endpos in - let ord = - if $6 = "to" - then ATyp_aux(ATyp_inc,loc $startpos($6) $endpos($6)) - else ATyp_aux(ATyp_dec,loc $startpos($6) $endpos($6)) - in - mk_exp (E_for ($3, $5, $7, step, ord, $9)) $startpos $endpos } - | Repeat exp Until exp - { mk_exp (E_loop (Until, $4, $2)) $startpos $endpos } - | While exp Do exp - { mk_exp (E_loop (While, $2, $4)) $startpos $endpos } - -/* The following implements all nine levels of user-defined precedence for -operators in expressions, with both left, right and non-associative operators */ - -exp0: - | exp1 op0 exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp0l op0l exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp1 op0r exp0r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp1 { $1 } -exp0l: - | exp1 op0 exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp0l op0l exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp1 { $1 } -exp0r: - | exp1 op0 exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp1 op0r exp0r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp1 { $1 } - -exp1: - | exp2 op1 exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp1l op1l exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp2 op1r exp1r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp2 { $1 } -exp1l: - | exp2 op1 exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp1l op1l exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp2 { $1 } -exp1r: - | exp2 op1 exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp2 op1r exp1r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp2 { $1 } - -exp2: - | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp2l op2l exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp3 { $1 } -exp2l: - | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp2l op2l exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp3 { $1 } -exp2r: - | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp3 { $1 } - -exp3: - | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp3l op3l exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp4 { $1 } -exp3l: - | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp3l op3l exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp4 { $1 } -exp3r: - | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp4 { $1 } - -exp4: - | exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp5 Lt exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp5 Gt exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp5 LtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<=") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp5 GtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">=") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp5 ExclEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "!=") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp4l op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp5 op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp5 { $1 } -exp4l: - | exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp4l op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp5 { $1 } -exp4r: - | exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp5 op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp5 { $1 } - -exp5: - | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp5l op5l exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp6 op5r exp5r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp6 At exp5r { mk_exp (E_vector_append ($1, $3)) $startpos $endpos } - | exp6 { $1 } -exp5l: - | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp5l op5l exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp6 { $1 } -exp5r: - | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp6 op5r exp5r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp6 At exp5r { mk_exp (E_vector_append ($1, $3)) $startpos $endpos } - | exp6 { $1 } - -exp6: - | exp7 op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp6l op6l exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp7 op6r exp6r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp6l Plus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "+") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp6l Minus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "-") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp7 { $1 } -exp6l: - | exp7 op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp6l op6l exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp6l Plus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "+") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp6l Minus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "-") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp7 { $1 } -exp6r: - | exp7 op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp7 op6r exp6r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp7 { $1 } - -exp7: - | exp8 op7 exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp7l op7l exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp8 op7r exp7r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp7l Star exp8 { mk_exp (E_app_infix ($1, mk_id (Id "*") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp8 { $1 } -exp7l: - | exp8 op7 exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp7l op7l exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp7l Star exp8 { mk_exp (E_app_infix ($1, mk_id (Id "*") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | exp8 { $1 } -exp7r: - | exp8 op7 exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp8 op7r exp7r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp8 { $1 } - -exp8: - | exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp8l op8l exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp9 op8r exp8r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp9 Caret exp8r { mk_exp (E_app_infix ($1, mk_id (Id "^") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos } - | exp9 { $1 } -exp8l: - | exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp8l op8l exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos } - | exp9 { $1 } -exp8r: - | exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp9 op8r exp8r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp9 Caret exp8r { mk_exp (E_app_infix ($1, mk_id (Id "^") $startpos($2) $endpos($2), $3)) $startpos $endpos } - | TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos } - | exp9 { $1 } - -exp9: - | atomic_exp op9 atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp9l op9l atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | atomic_exp op9r exp9r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | atomic_exp { $1 } -exp9l: - | atomic_exp op9 atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | exp9l op9l atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | atomic_exp { $1 } -exp9r: - | atomic_exp op9 atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | atomic_exp op9r exp9r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos } - | atomic_exp { $1 } - -case: - | pat EqGt exp - { mk_pexp (Pat_exp ($1, $3)) $startpos $endpos } - | pat If_ exp EqGt exp - { mk_pexp (Pat_when ($1, $3, $5)) $startpos $endpos } - -case_list: - | case - { [$1] } - | case Comma case_list - { $1 :: $3 } - -block: - | exp - { [$1] } - | Let_ letbind Semi block - { [mk_exp (E_let ($2, mk_exp (E_block $4) $startpos($4) $endpos)) $startpos $endpos] } - | Var atomic_exp Eq exp Semi block - { [mk_exp (E_var ($2, $4, mk_exp (E_block $6) $startpos($6) $endpos)) $startpos $endpos] } - | exp Semi /* Allow trailing semicolon in block */ - { [$1] } - | exp Semi block - { $1 :: $3 } - -%inline letbind: - | pat Eq exp - { LB_aux (LB_val ($1, $3), loc $startpos $endpos) } - -atomic_exp: - | atomic_exp Colon atomic_typ - { mk_exp (E_cast ($3, $1)) $startpos $endpos } - | lit - { mk_exp (E_lit $1) $startpos $endpos } - | id MinusGt id Unit - { mk_exp (E_app (prepend_id "_mod_" $3, [mk_exp (E_ref $1) $startpos($1) $endpos($1)])) $startpos $endpos } - | id MinusGt id Lparen exp_list Rparen - { mk_exp (E_app (prepend_id "_mod_" $3, mk_exp (E_ref $1) $startpos($1) $endpos($1) :: $5)) $startpos $endpos } - | atomic_exp Dot id Unit - { mk_exp (E_app (prepend_id "_mod_" $3, [$1])) $startpos $endpos } - | atomic_exp Dot id Lparen exp_list Rparen - { mk_exp (E_app (prepend_id "_mod_" $3, $1 :: $5)) $startpos $endpos } - | atomic_exp Dot id - { mk_exp (E_field ($1, $3)) $startpos $endpos } - | id - { mk_exp (E_id $1) $startpos $endpos } - | kid - { mk_exp (E_sizeof (mk_typ (ATyp_var $1) $startpos $endpos)) $startpos $endpos } - | Ref id - { mk_exp (E_ref $2) $startpos $endpos } - | id Unit - { mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos } - | id Lparen exp_list Rparen - { mk_exp (E_app ($1, $3)) $startpos $endpos } - | Exit Lparen exp Rparen - { mk_exp (E_exit $3) $startpos $endpos } - | Sizeof Lparen typ Rparen - { mk_exp (E_sizeof $3) $startpos $endpos } - | Constraint Lparen nc Rparen - { mk_exp (E_constraint $3) $startpos $endpos } - | Assert Lparen exp Rparen - { mk_exp (E_assert ($3, mk_lit_exp (L_string "") $startpos($4) $endpos($4))) $startpos $endpos } - | Assert Lparen exp Comma exp Rparen - { mk_exp (E_assert ($3, $5)) $startpos $endpos } - | atomic_exp Lsquare exp Rsquare - { mk_exp (E_vector_access ($1, $3)) $startpos $endpos } - | atomic_exp Lsquare exp DotDot exp Rsquare - { mk_exp (E_vector_subrange ($1, $3, $5)) $startpos $endpos } - | Record Lcurly fexp_exp_list Rcurly - { mk_exp (E_record $3) $startpos $endpos } - | Lcurly exp With fexp_exp_list Rcurly - { mk_exp (E_record_update ($2, $4)) $startpos $endpos } - | Lsquare exp_list Rsquare - { mk_exp (E_vector $2) $startpos $endpos } - | Lsquare exp With atomic_exp Eq exp Rsquare - { mk_exp (E_vector_update ($2, $4, $6)) $startpos $endpos } - | Lsquare exp With atomic_exp DotDot atomic_exp Eq exp Rsquare - { mk_exp (E_vector_update_subrange ($2, $4, $6, $8)) $startpos $endpos } - | LsquareBar exp_list RsquareBar - { mk_exp (E_list $2) $startpos $endpos } - | Lparen exp Rparen - { $2 } - | Lparen exp Comma exp_list Rparen - { mk_exp (E_tuple ($2 :: $4)) $startpos $endpos } - -fexp_exp: - | atomic_exp Eq exp - { mk_exp (E_app_infix ($1, mk_id (Id "=") $startpos($2) $endpos($2), $3)) $startpos $endpos } - -fexp_exp_list: - | fexp_exp - { [$1] } - | fexp_exp Comma fexp_exp_list - { $1 :: $3 } - -exp_list: - | exp - { [$1] } - | exp Comma exp_list - { $1 :: $3 } - -funcl_patexp: - | pat Eq exp - { mk_pexp (Pat_exp ($1, $3)) $startpos $endpos } - | Lparen pat If_ exp Rparen Eq exp - { mk_pexp (Pat_when ($2, $4, $7)) $startpos $endpos } - -funcl: - | id funcl_patexp - { mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos } - -funcls: - | id funcl_patexp - { [mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos] } - | id funcl_patexp And funcls - { mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos :: $4 } - -index_range: - | Num - { mk_ir (BF_single $1) $startpos $endpos } - | Num DotDot Num - { mk_ir (BF_range ($1, $3)) $startpos $endpos } - -r_id_def: - | id Colon index_range - { $1, $3 } - -r_def_body: - | r_id_def - { [$1] } - | r_id_def Comma - { [$1] } - | r_id_def Comma r_def_body - { $1 :: $3 } - -type_def: - | Typedef id typquant Eq typ - { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm $3 $5 $startpos($3) $endpos)) $startpos $endpos } - | Typedef id Eq typ - { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm mk_typqn $4 $startpos($4) $endpos)) $startpos $endpos } - | Struct id Eq Lcurly struct_fields Rcurly - { mk_td (TD_record ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos } - | Struct id typquant Eq Lcurly struct_fields Rcurly - { mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos } - | Enum id Eq enum_bar - { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos } - | Enum id Eq Lcurly enum Rcurly - { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos } - | Newtype id Eq type_union - { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), [$4], false)) $startpos $endpos } - | Newtype id typquant Eq type_union - { mk_td (TD_variant ($2, mk_namesectn, $3, [$5], false)) $startpos $endpos } - | Union id Eq Lcurly type_unions Rcurly - { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos } - | Union id typquant Eq Lcurly type_unions Rcurly - { mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos } - | Bitfield id Colon typ Eq Lcurly r_def_body Rcurly - { mk_td (TD_bitfield ($2, $4, $7)) $startpos $endpos } - -enum_bar: - | id - { [$1] } - | id Bar enum_bar - { $1 :: $3 } - -enum: - | id - { [$1] } - | id Comma enum - { $1 :: $3 } - -struct_field: - | id Colon typ - { ($3, $1) } - -struct_fields: - | struct_field - { [$1] } - | struct_field Comma - { [$1] } - | struct_field Comma struct_fields - { $1 :: $3 } - -type_union: - | id Colon typ - { Tu_aux (Tu_ty_id ($3, $1), loc $startpos $endpos) } - | id - { Tu_aux (Tu_id $1, loc $startpos $endpos) } - -type_unions: - | type_union - { [$1] } - | type_union Comma - { [$1] } - | type_union Comma type_unions - { $1 :: $3 } - -fun_def: - | Function_ funcls - { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos } - -fun_def_list: - | fun_def - { [$1] } - | fun_def fun_def_list - { $1 :: $2 } - -let_def: - | Let_ letbind - { $2 } - -externs: - | id Colon String - { [(string_of_id $1, $3)] } - | id Colon String Comma externs - { (string_of_id $1, $3) :: $5 } - -val_spec_def: - | Val id Colon typschm - { mk_vs (VS_val_spec ($4, $2, (fun _ -> None), false)) $startpos $endpos } - | Val Cast id Colon typschm - { mk_vs (VS_val_spec ($5, $3, (fun _ -> None), true)) $startpos $endpos } - | Val id Eq String Colon typschm - { mk_vs (VS_val_spec ($6, $2, (fun _ -> Some $4), false)) $startpos $endpos } - | Val Cast id Eq String Colon typschm - { mk_vs (VS_val_spec ($7, $3, (fun _ -> Some $5), true)) $startpos $endpos } - | Val String Colon typschm - { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), (fun _ -> Some $2), false)) $startpos $endpos } - | Val Cast String Colon typschm - { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), (fun _ -> Some $3), true)) $startpos $endpos } - | Val id Eq Lcurly externs Rcurly Colon typschm - { mk_vs (VS_val_spec ($8, $2, (fun backend -> (assoc_opt backend $5)), false)) $startpos $endpos } - | Val Cast id Eq Lcurly externs Rcurly Colon typschm - { mk_vs (VS_val_spec ($9, $3, (fun backend -> (assoc_opt backend $6)), true)) $startpos $endpos } - -register_def: - | Register id Colon typ - { mk_reg_dec (DEC_reg ($4, $2)) $startpos $endpos } - -default_def: - | Default base_kind Inc - { mk_default (DT_order ($2, mk_typ ATyp_inc $startpos($3) $endpos)) $startpos $endpos } - | Default base_kind Dec - { mk_default (DT_order ($2, mk_typ ATyp_dec $startpos($3) $endpos)) $startpos $endpos } - -scattered_def: - | Union id typquant - { mk_sd (SD_scattered_variant($2, mk_namesectn, $3)) $startpos $endpos } - | Union id - { mk_sd (SD_scattered_variant($2, mk_namesectn, mk_typqn)) $startpos $endpos } - | Function_ id - { mk_sd (SD_scattered_function(mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos } - -def: - | fun_def - { DEF_fundef $1 } - | Fixity - { let (prec, n, op) = $1 in DEF_fixity (prec, n, Id_aux (Id op, loc $startpos $endpos)) } - | val_spec_def - { DEF_spec $1 } - | type_def - { DEF_type $1 } - | let_def - { DEF_val $1 } - | register_def - { DEF_reg_dec $1 } - | Overload id Eq Lcurly id_list Rcurly - { DEF_overload ($2, $5) } - | Overload id Eq enum_bar - { DEF_overload ($2, $4) } - | Scattered scattered_def - { DEF_scattered $2 } - | Function_ Clause funcl - { DEF_scattered (mk_sd (SD_scattered_funcl $3) $startpos $endpos) } - | Union Clause id Eq type_union - { DEF_scattered (mk_sd (SD_scattered_unioncl ($3, $5)) $startpos $endpos) } - | End id - { DEF_scattered (mk_sd (SD_scattered_end $2) $startpos $endpos) } - | default_def - { DEF_default $1 } - | Mutual Lcurly fun_def_list Rcurly - { DEF_internal_mutrec $3 } - -defs_list: - | def - { [$1] } - | def defs_list - { $1::$2 } - -def_eof: - | def Eof - { $1 } - -defs: - | defs_list - { (Defs $1) } - -file: - | defs Eof - { $1 } diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml new file mode 100644 index 00000000..930da39c --- /dev/null +++ b/src/pretty_print_sail.ml @@ -0,0 +1,540 @@ +(**************************************************************************) +(* 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 + +module Big_int = Nat_big_num + +let doc_op symb a b = infix 2 1 symb a b + +let doc_id (Id_aux (id_aux, _)) = + string (match id_aux with + | Id v -> v + | DeIid op -> "operator " ^ op) + +let doc_kid kid = string (Ast_util.string_of_kid kid) + +let doc_int n = string (Big_int.to_string n) + +let doc_ord (Ord_aux(o,_)) = match o with + | Ord_var v -> doc_kid v + | Ord_inc -> string "inc" + | Ord_dec -> string "dec" + +let rec doc_nexp = + let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) = + match n_aux with + | Nexp_constant c -> string (Big_int.to_string c) + | Nexp_id id -> doc_id id + | Nexp_var kid -> doc_kid kid + | _ -> parens (nexp0 nexp) + and nexp0 (Nexp_aux (n_aux, _) as nexp) = + match n_aux with + | Nexp_sum (n1, Nexp_aux (Nexp_neg n2, _)) | Nexp_minus (n1, n2) -> + separate space [nexp0 n1; string "-"; nexp1 n2] + | Nexp_sum (n1, Nexp_aux (Nexp_constant c, _)) when Big_int.less c Big_int.zero -> + separate space [nexp0 n1; string "-"; doc_int (Big_int.abs c)] + | Nexp_sum (n1, n2) -> separate space [nexp0 n1; string "+"; nexp1 n2] + | _ -> nexp1 nexp + and nexp1 (Nexp_aux (n_aux, _) as nexp) = + match n_aux with + | Nexp_times (n1, n2) -> separate space [nexp1 n1; string "*"; nexp2 n2] + | _ -> nexp2 nexp + and nexp2 (Nexp_aux (n_aux, _) as nexp) = + match n_aux with + | Nexp_neg n -> separate space [string "-"; atomic_nexp n] + | Nexp_exp n -> separate space [string "2"; string "^"; atomic_nexp n] + | _ -> atomic_nexp nexp + in + nexp0 + +let doc_nc = + let nc_op op n1 n2 = separate space [doc_nexp n1; string op; doc_nexp n2] in + let rec atomic_nc (NC_aux (nc_aux, _) as nc) = + match nc_aux with + | NC_true -> string "true" + | NC_false -> string "false" + | NC_equal (n1, n2) -> nc_op "=" n1 n2 + | NC_not_equal (n1, n2) -> nc_op "!=" n1 n2 + | NC_bounded_ge (n1, n2) -> nc_op ">=" n1 n2 + | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2 + | NC_set (kid, ints) -> + separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)] + | _ -> parens (nc0 nc) + and nc0 (NC_aux (nc_aux, _) as nc) = + match nc_aux with + | NC_or (c1, c2) -> separate space [nc0 c1; string "|"; nc1 c2] + | _ -> nc1 nc + and nc1 (NC_aux (nc_aux, _) as nc) = + match nc_aux with + | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2] + | _ -> atomic_nc nc + in + nc0 + +let rec doc_typ (Typ_aux (typ_aux, _)) = + match typ_aux with + | Typ_id id -> doc_id id + | Typ_app (id, []) -> doc_id id + | Typ_app (Id_aux (DeIid str, _), [x; y]) -> + separate space [doc_typ_arg x; doc_typ_arg y] + (* + | Typ_app (id, [_; len; _; Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]) when Id.compare (mk_id "vector") id == 0 && Id.compare (mk_id "bit") tid == 0-> + string "bits" ^^ parens (doc_typ_arg len) + *) + | Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs) + | Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs) + | Typ_var kid -> doc_kid kid + (* Resugar set types like {|1, 2, 3|} *) + | Typ_exist ([kid1], NC_aux (NC_set (kid2, ints), _), Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _)) + when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 && Id.compare (mk_id "atom") id == 0 -> + enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints) + | Typ_exist (kids, nc, typ) -> + braces (separate_map space doc_kid kids ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ) + | Typ_fn (typ1, typ2, Effect_aux (Effect_set [], _)) -> + separate space [doc_typ typ1; string "->"; doc_typ typ2] + | Typ_fn (typ1, typ2, Effect_aux (Effect_set effs, _)) -> + let ocaml_eff = braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs)) in + separate space [doc_typ typ1; string "->"; doc_typ typ2; string "effect"; ocaml_eff] +and doc_typ_arg (Typ_arg_aux (ta_aux, _)) = + match ta_aux with + | Typ_arg_typ typ -> doc_typ typ + | Typ_arg_nexp nexp -> doc_nexp nexp + | Typ_arg_order o -> doc_ord o + +let doc_quants quants = + let doc_qi_kopt (QI_aux (qi_aux, _)) = + match qi_aux with + | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid] + | QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])] + | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])] + | QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])] + | QI_const nc -> [] + in + let qi_nc (QI_aux (qi_aux, _)) = + match qi_aux with + | QI_const nc -> [nc] + | _ -> [] + in + let kdoc = separate space (List.concat (List.map doc_qi_kopt quants)) in + let ncs = List.concat (List.map qi_nc quants) in + match ncs with + | [] -> kdoc + | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc + | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs) + + + +let doc_binding (TypQ_aux (tq_aux, _), typ) = + match tq_aux with + | TypQ_no_forall -> doc_typ typ + | TypQ_tq [] -> doc_typ typ + | TypQ_tq qs -> + string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ typ + +let doc_typschm (TypSchm_aux (TypSchm_ts (typq, typ), _)) = doc_binding (typq, typ) + +let doc_typschm_typ (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = doc_typ typ + +let doc_typschm_quants (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = + match tq_aux with + | TypQ_no_forall -> None + | TypQ_tq [] -> None + | TypQ_tq qs -> Some (doc_quants qs) + +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 rec doc_pat (P_aux (p_aux, _) as pat) = + match p_aux with + | P_id id -> doc_id id + | P_tup pats -> lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen + | P_typ (typ, pat) -> separate space [doc_pat pat; colon; doc_typ typ] + | P_lit lit -> doc_lit lit + (* P_var short form sugar *) + | P_var (P_aux (P_id id, _), kid) when Id.compare (id_of_kid kid) id == 0 -> + doc_kid kid + | P_var (pat, kid) -> separate space [doc_pat pat; string "as"; doc_kid kid] + | P_vector pats -> brackets (separate_map (comma ^^ space) doc_pat pats) + | P_vector_concat pats -> separate_map (space ^^ string "@" ^^ space) doc_pat pats + | P_wild -> string "_" + | P_as (pat, id) -> separate space [doc_pat pat; string "as"; doc_id id] + | P_app (id, pats) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_pat pats) + | _ -> string (string_of_pat pat) + +(* if_block_x is true if x should be printed like a block, i.e. with + newlines. Blocks are automatically printed as blocks, so this + returns false for them. *) +let if_block_then (E_aux (e_aux, _)) = + match e_aux with + | E_assign _ | E_if _ -> true + | _ -> false + +let if_block_else (E_aux (e_aux, _)) = + match e_aux with + | E_assign _ -> true + | _ -> false + +let fixities = + let fixities' = + List.fold_left + (fun r (x, y) -> Bindings.add x y r) + Bindings.empty + [ + (mk_id "^", (InfixR, 8)); + (mk_id "*", (InfixL, 7)); + (mk_id "+", (InfixL, 6)); + (mk_id "-", (InfixL, 6)); + (mk_id "!=", (Infix, 4)); + (mk_id ">", (Infix, 4)); + (mk_id "<", (Infix, 4)); + (mk_id ">=", (Infix, 4)); + (mk_id "<=", (Infix, 4)); + (mk_id "&", (InfixR, 3)); + (mk_id "|", (InfixR, 2)); + ] + in + ref (fixities' : (prec * int) Bindings.t) + +let rec doc_exp (E_aux (e_aux, _) as exp) = + match e_aux with + | E_block [] -> string "()" + | E_block [exp] -> doc_exp exp + | E_block exps -> surround 2 0 lbrace (doc_block exps) rbrace + | E_nondet exps -> assert false + (* This is mostly for the -convert option *) + | E_app_infix (x, id, y) when Id.compare (mk_id "quot") id == 0 -> + separate space [doc_atomic_exp x; string "/"; doc_atomic_exp y] + | E_app_infix _ -> doc_infix 0 exp + | E_tuple exps -> parens (separate_map (comma ^^ space) doc_exp exps) + + (* Various rules to try to format if blocks nicely based on content *) + | E_if (if_exp, then_exp, else_exp) when if_block_then then_exp && if_block_else else_exp -> + (separate space [string "if"; doc_exp if_exp; string "then"] ^//^ doc_exp then_exp) + ^/^ (string "else" ^//^ doc_exp else_exp) + | E_if (if_exp, then_exp, (E_aux (E_if _, _) as else_exp)) when if_block_then then_exp -> + (separate space [string "if"; doc_exp if_exp; string "then"] ^//^ doc_exp then_exp) + ^/^ (string "else" ^^ space ^^ doc_exp else_exp) + | E_if (if_exp, then_exp, else_exp) when if_block_else else_exp -> + (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp]) + ^^ space ^^ (string "else" ^//^ doc_exp else_exp) + | E_if (if_exp, then_exp, else_exp) when if_block_then then_exp -> + (separate space [string "if"; doc_exp if_exp; string "then"] ^//^ doc_exp then_exp) + ^/^ (string "else" ^^ space ^^ doc_exp else_exp) + | E_if (if_exp, then_exp, else_exp) -> + group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp; string "else"; doc_exp else_exp]) + + | E_list exps -> string "[|" ^^ separate_map (comma ^^ space) doc_exp exps ^^ string "|]" + | E_cons (exp1, exp2) -> string "E_cons" + | E_record fexps -> separate space [string "record"; string "{"; doc_fexps fexps; string "}"] + | E_loop (While, cond, exp) -> + separate space [string "while"; doc_exp cond; string "do"; doc_exp exp] + | E_loop (Until, cond, exp) -> + separate space [string "repeat"; doc_exp exp; string "until"; doc_exp cond] + | E_record_update (exp, fexps) -> + separate space [string "{"; doc_exp exp; string "with"; doc_fexps fexps; string "}"] + | E_vector_append (exp1, exp2) -> separate space [doc_atomic_exp exp1; string "@"; doc_atomic_exp exp2] + | E_case (exp, pexps) -> + separate space [string "match"; doc_exp exp; doc_pexps pexps] + | E_let (LB_aux (LB_val (pat, binding), _), exp) -> + separate space [string "let"; doc_pat pat; equals; doc_exp binding; string "in"; doc_exp exp] + | E_internal_plet (pat, exp1, exp2) -> + let le = + prefix 2 1 + (separate space [string "internal_plet"; doc_pat pat; equals]) + (doc_exp exp1) in + doc_op (string "in") le (doc_exp exp2) + | E_var (lexp, binding, exp) -> + separate space [string "var"; doc_lexp lexp; equals; doc_exp binding; string "in"; doc_exp exp] + | E_assign (lexp, exp) -> + separate space [doc_lexp lexp; equals; doc_exp exp] + | E_for (id, exp1, exp2, exp3, order, exp4) -> + begin + let header = + string "foreach" ^^ space ^^ + group (parens (separate (break 1) + [ doc_id id; + string "from " ^^ doc_atomic_exp exp1; + string "to " ^^ doc_atomic_exp exp2; + string "by " ^^ doc_atomic_exp exp3; + string "in " ^^ doc_ord order ])) + in + match exp4 with + | E_aux (E_block [_], _) -> header ^//^ doc_exp exp4 + | E_aux (E_block _, _) -> header ^^ space ^^ doc_exp exp4 + | _ -> header ^//^ doc_exp exp4 + end + (* Resugar an assert with an empty message *) + | E_throw exp -> string "throw" ^^ parens (doc_exp exp) + | E_try (exp, pexps) -> + separate space [string "try"; doc_exp exp; string "catch"; doc_pexps pexps] + | E_return exp -> string "return" ^^ parens (doc_exp exp) + | E_internal_return exp -> string "internal_return" ^^ parens (doc_exp exp) + | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 -> + separate space [string "2"; string "^"; doc_atomic_exp exp] + | _ -> doc_atomic_exp exp +and doc_infix n (E_aux (e_aux, _) as exp) = + match e_aux with + | E_app_infix (l, op, r) when n < 10 -> + begin + try + match Bindings.find op !fixities with + | (Infix, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r] + | (Infix, m) when m < n -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]) + | (InfixL, m) when m >= n -> separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r] + | (InfixL, m) when m < n -> parens (separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r]) + | (InfixR, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r] + | (InfixR, m) when m < n -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r]) + | _ -> assert false + with + | Not_found -> + separate space [doc_atomic_exp l; doc_id op; doc_atomic_exp r] + end + | _ -> doc_atomic_exp exp +and doc_atomic_exp (E_aux (e_aux, _) as exp) = + match e_aux with + | E_cast (typ, exp) -> + separate space [doc_atomic_exp exp; colon; doc_typ typ] + | E_lit lit -> doc_lit lit + | E_id id -> doc_id id + | E_ref id -> string "ref" ^^ space ^^ doc_id id + | E_field (exp, id) -> doc_atomic_exp exp ^^ dot ^^ doc_id id + | E_sizeof (Nexp_aux (Nexp_var kid, _)) -> doc_kid kid + | E_sizeof nexp -> string "sizeof" ^^ parens (doc_nexp nexp) + (* Format a function with a unit argument as f() rather than f(()) *) + | E_app (id, [E_aux (E_lit (L_aux (L_unit, _)), _)]) -> doc_id id ^^ string "()" + | E_app (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps) + | E_constraint nc -> string "constraint" ^^ parens (doc_nc nc) + | E_assert (exp1, E_aux (E_lit (L_aux (L_string "", _)), _)) -> string "assert" ^^ parens (doc_exp exp1) + | E_assert (exp1, exp2) -> string "assert" ^^ parens (doc_exp exp1 ^^ comma ^^ space ^^ doc_exp exp2) + | E_exit exp -> string "exit" ^^ parens (doc_exp exp) + | E_vector_access (exp1, exp2) -> doc_atomic_exp exp1 ^^ brackets (doc_exp exp2) + | E_vector_subrange (exp1, exp2, exp3) -> doc_atomic_exp exp1 ^^ brackets (separate space [doc_exp exp2; string ".."; doc_exp exp3]) + | E_vector exps -> brackets (separate_map (comma ^^ space) doc_exp exps) + | E_vector_update (exp1, exp2, exp3) -> + brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; equals; doc_exp exp3]) + | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> + brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4]) + | E_internal_value v -> string (Value.string_of_value v |> Util.green |> Util.clear) + | _ -> parens (doc_exp exp) +and doc_fexps (FES_aux (FES_Fexps (fexps, _), _)) = + separate_map (comma ^^ space) doc_fexp fexps +and doc_fexp (FE_aux (FE_Fexp (id, exp), _)) = + separate space [doc_id id; equals; doc_exp exp] +and doc_block = function + | [] -> string "()" + | [E_aux (E_let (LB_aux (LB_val (pat, binding), _), E_aux (E_block exps, _)), _)] -> + separate space [string "let"; doc_pat pat; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps + | [E_aux (E_var (lexp, binding, E_aux (E_block exps, _)), _)] -> + separate space [string "var"; doc_lexp lexp; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps + | [exp] -> doc_exp exp + | exp :: exps -> doc_exp exp ^^ semi ^^ hardline ^^ doc_block exps +and doc_lexp (LEXP_aux (l_aux, _) as lexp) = + match l_aux with + | LEXP_cast (typ, id) -> separate space [doc_id id; colon; doc_typ typ] + | _ -> doc_atomic_lexp lexp +and doc_atomic_lexp (LEXP_aux (l_aux, _) as lexp) = + match l_aux with + | LEXP_id id -> doc_id id + | LEXP_deref exp -> lparen ^^ string "*" ^^ doc_atomic_exp exp ^^ rparen + | LEXP_tup lexps -> lparen ^^ separate_map (comma ^^ space) doc_lexp lexps ^^ rparen + | LEXP_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id + | LEXP_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp) + | LEXP_vector_range (lexp, exp1, exp2) -> doc_atomic_lexp lexp ^^ brackets (separate space [doc_exp exp1; string ".."; doc_exp exp2]) + | LEXP_memory (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps) + | _ -> parens (doc_lexp lexp) +and doc_pexps pexps = surround 2 0 lbrace (separate_map (comma ^^ hardline) doc_pexp pexps) rbrace +and doc_pexp (Pat_aux (pat_aux, _)) = + match pat_aux with + | Pat_exp (pat, exp) -> separate space [doc_pat pat; string "=>"; doc_exp exp] + | Pat_when (pat, wh, exp) -> + separate space [doc_pat pat; string "if"; doc_exp wh; string "=>"; doc_exp exp] +and doc_letbind (LB_aux (lb_aux, _)) = + match lb_aux with + | LB_val (pat, exp) -> + separate space [doc_pat pat; equals; doc_exp exp] + +let doc_funcl funcl = string "FUNCL" + +let doc_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp,_)), _)) = + match pexp with + | Pat_exp (pat,exp) -> + group (separate space [doc_id id; doc_pat pat; equals; doc_exp exp]) + | Pat_when (pat,wh,exp) -> + group (separate space [doc_id id; parens (separate space [doc_pat pat; string "if"; doc_exp wh]); string "="; doc_exp exp]) + +let doc_default (DT_aux(df,_)) = match df with + | DT_kind(bk,v) -> string "DT_kind" (* separate space [string "default"; doc_bkind bk; doc_var v] *) + | DT_typ(ts,id) -> separate space [string "default"; doc_typschm ts; doc_id id] + | DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord] + +let doc_fundef (FD_aux (FD_function (r, typa, efa, funcls), _)) = + match funcls with + | [] -> failwith "Empty function list" + | _ -> + let sep = hardline ^^ string "and" ^^ space in + let clauses = separate_map sep doc_funcl funcls in + string "function" ^^ space ^^ clauses + +let doc_dec (DEC_aux (reg,_)) = + match reg with + | DEC_reg (typ, id) -> separate space [string "register"; doc_id id; colon; doc_typ typ] + | DEC_alias(id,alspec) -> string "ALIAS" + | DEC_typ_alias(typ,id,alspec) -> string "ALIAS" + +let doc_field (typ, id) = + separate space [doc_id id; colon; doc_typ typ] + +let doc_union (Tu_aux (tu, l)) = match tu with + | Tu_id id -> doc_id id + | Tu_ty_id (typ, id) -> separate space [doc_id id; colon; doc_typ typ] + +let doc_typdef (TD_aux(td,_)) = match td with + | TD_abbrev (id, _, typschm) -> + begin + match doc_typschm_quants typschm with + | Some qdoc -> + doc_op equals (concat [string "type"; space; doc_id id; space; qdoc]) (doc_typschm_typ typschm) + | None -> + doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm) + end + | TD_enum (id, _, ids, _) -> + separate space [string "enum"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace] + | TD_record (id, _, TypQ_aux (TypQ_no_forall, _), fields, _) | TD_record (id, _, TypQ_aux (TypQ_tq [], _), fields, _) -> + separate space [string "struct"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace] + | TD_record (id, _, TypQ_aux (TypQ_tq qs, _), fields, _) -> + separate space [string "struct"; doc_id id; doc_quants qs; equals; + surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace] + | TD_variant (id, _, TypQ_aux (TypQ_no_forall, _), unions, _) | TD_variant (id, _, TypQ_aux (TypQ_tq [], _), unions, _) -> + separate space [string "union"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace] + | TD_variant (id, _, TypQ_aux (TypQ_tq qs, _), unions, _) -> + separate space [string "union"; doc_id id; doc_quants qs; equals; + surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace] + | _ -> string "TYPEDEF" + +let doc_spec (VS_aux(v,_)) = + let doc_extern ext = + let doc_backend b = Util.option_map (fun id -> string (b ^ ":") ^^ space ^^ + utf8string ("\"" ^ String.escaped id ^ "\"")) (ext b) in + let docs = Util.option_these (List.map doc_backend ["ocaml"; "lem"]) in + if docs = [] then empty else equals ^^ space ^^ braces (separate (comma ^^ space) docs) + in + match v with + | VS_val_spec(ts,id,ext,is_cast) -> + string "val" ^^ space + ^^ (if is_cast then (string "cast" ^^ space) else empty) + ^^ doc_id id ^^ space + ^^ doc_extern ext + ^^ colon ^^ space + ^^ doc_typschm ts + +let doc_prec = function + | Infix -> string "infix" + | InfixL -> string "infixl" + | InfixR -> string "infixr" + +let doc_kind_def (KD_aux (KD_nabbrev (_, id, _, nexp), _)) = + separate space [string "integer"; doc_id id; equals; doc_nexp nexp] + +let rec doc_scattered (SD_aux (sd_aux, _)) = + match sd_aux with + | SD_scattered_function (_, _, _, id) -> + string "scattered" ^^ space ^^ string "function" ^^ space ^^ doc_id id + | SD_scattered_funcl funcl -> + string "function" ^^ space ^^ string "clause" ^^ space ^^ doc_funcl funcl + | SD_scattered_end id -> + string "end" ^^ space ^^ doc_id id + | _ -> string "SCATTERED" + +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_kind_def k_def + | DEF_fundef f_def -> doc_fundef f_def + | DEF_val lbind -> string "let" ^^ space ^^ doc_letbind lbind + | DEF_internal_mutrec fundefs -> + (string "mutual {" ^//^ separate_map (hardline ^^ hardline) doc_fundef fundefs) + ^^ hardline ^^ string "}" + | DEF_reg_dec dec -> doc_dec dec + | DEF_scattered sdef -> doc_scattered sdef + | DEF_fixity (prec, n, id) -> + fixities := Bindings.add id (prec, Big_int.to_int n) !fixities; + separate space [doc_prec prec; doc_int n; doc_id id] + | DEF_overload (id, ids) -> + separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace] + | DEF_comm (DC_comm s) -> string "TOPLEVEL" + | DEF_comm (DC_comm_struct d) -> string "TOPLEVEL" + ) ^^ hardline + +let doc_defs (Defs(defs)) = + separate_map hardline doc_def defs + +let pp_defs f d = ToChannel.pretty 1. 80 f (doc_defs d) + +let pretty_sail f doc = ToChannel.pretty 1. 120 f doc + +let to_string doc = + let b = Buffer.create 120 in + ToBuffer.pretty 1. 120 b doc; + Buffer.contents b diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml deleted file mode 100644 index 930da39c..00000000 --- a/src/pretty_print_sail2.ml +++ /dev/null @@ -1,540 +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 - -module Big_int = Nat_big_num - -let doc_op symb a b = infix 2 1 symb a b - -let doc_id (Id_aux (id_aux, _)) = - string (match id_aux with - | Id v -> v - | DeIid op -> "operator " ^ op) - -let doc_kid kid = string (Ast_util.string_of_kid kid) - -let doc_int n = string (Big_int.to_string n) - -let doc_ord (Ord_aux(o,_)) = match o with - | Ord_var v -> doc_kid v - | Ord_inc -> string "inc" - | Ord_dec -> string "dec" - -let rec doc_nexp = - let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) = - match n_aux with - | Nexp_constant c -> string (Big_int.to_string c) - | Nexp_id id -> doc_id id - | Nexp_var kid -> doc_kid kid - | _ -> parens (nexp0 nexp) - and nexp0 (Nexp_aux (n_aux, _) as nexp) = - match n_aux with - | Nexp_sum (n1, Nexp_aux (Nexp_neg n2, _)) | Nexp_minus (n1, n2) -> - separate space [nexp0 n1; string "-"; nexp1 n2] - | Nexp_sum (n1, Nexp_aux (Nexp_constant c, _)) when Big_int.less c Big_int.zero -> - separate space [nexp0 n1; string "-"; doc_int (Big_int.abs c)] - | Nexp_sum (n1, n2) -> separate space [nexp0 n1; string "+"; nexp1 n2] - | _ -> nexp1 nexp - and nexp1 (Nexp_aux (n_aux, _) as nexp) = - match n_aux with - | Nexp_times (n1, n2) -> separate space [nexp1 n1; string "*"; nexp2 n2] - | _ -> nexp2 nexp - and nexp2 (Nexp_aux (n_aux, _) as nexp) = - match n_aux with - | Nexp_neg n -> separate space [string "-"; atomic_nexp n] - | Nexp_exp n -> separate space [string "2"; string "^"; atomic_nexp n] - | _ -> atomic_nexp nexp - in - nexp0 - -let doc_nc = - let nc_op op n1 n2 = separate space [doc_nexp n1; string op; doc_nexp n2] in - let rec atomic_nc (NC_aux (nc_aux, _) as nc) = - match nc_aux with - | NC_true -> string "true" - | NC_false -> string "false" - | NC_equal (n1, n2) -> nc_op "=" n1 n2 - | NC_not_equal (n1, n2) -> nc_op "!=" n1 n2 - | NC_bounded_ge (n1, n2) -> nc_op ">=" n1 n2 - | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2 - | NC_set (kid, ints) -> - separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)] - | _ -> parens (nc0 nc) - and nc0 (NC_aux (nc_aux, _) as nc) = - match nc_aux with - | NC_or (c1, c2) -> separate space [nc0 c1; string "|"; nc1 c2] - | _ -> nc1 nc - and nc1 (NC_aux (nc_aux, _) as nc) = - match nc_aux with - | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2] - | _ -> atomic_nc nc - in - nc0 - -let rec doc_typ (Typ_aux (typ_aux, _)) = - match typ_aux with - | Typ_id id -> doc_id id - | Typ_app (id, []) -> doc_id id - | Typ_app (Id_aux (DeIid str, _), [x; y]) -> - separate space [doc_typ_arg x; doc_typ_arg y] - (* - | Typ_app (id, [_; len; _; Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]) when Id.compare (mk_id "vector") id == 0 && Id.compare (mk_id "bit") tid == 0-> - string "bits" ^^ parens (doc_typ_arg len) - *) - | Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs) - | Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs) - | Typ_var kid -> doc_kid kid - (* Resugar set types like {|1, 2, 3|} *) - | Typ_exist ([kid1], NC_aux (NC_set (kid2, ints), _), Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _)) - when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 && Id.compare (mk_id "atom") id == 0 -> - enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints) - | Typ_exist (kids, nc, typ) -> - braces (separate_map space doc_kid kids ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ) - | Typ_fn (typ1, typ2, Effect_aux (Effect_set [], _)) -> - separate space [doc_typ typ1; string "->"; doc_typ typ2] - | Typ_fn (typ1, typ2, Effect_aux (Effect_set effs, _)) -> - let ocaml_eff = braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs)) in - separate space [doc_typ typ1; string "->"; doc_typ typ2; string "effect"; ocaml_eff] -and doc_typ_arg (Typ_arg_aux (ta_aux, _)) = - match ta_aux with - | Typ_arg_typ typ -> doc_typ typ - | Typ_arg_nexp nexp -> doc_nexp nexp - | Typ_arg_order o -> doc_ord o - -let doc_quants quants = - let doc_qi_kopt (QI_aux (qi_aux, _)) = - match qi_aux with - | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid] - | QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])] - | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])] - | QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])] - | QI_const nc -> [] - in - let qi_nc (QI_aux (qi_aux, _)) = - match qi_aux with - | QI_const nc -> [nc] - | _ -> [] - in - let kdoc = separate space (List.concat (List.map doc_qi_kopt quants)) in - let ncs = List.concat (List.map qi_nc quants) in - match ncs with - | [] -> kdoc - | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc - | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs) - - - -let doc_binding (TypQ_aux (tq_aux, _), typ) = - match tq_aux with - | TypQ_no_forall -> doc_typ typ - | TypQ_tq [] -> doc_typ typ - | TypQ_tq qs -> - string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ typ - -let doc_typschm (TypSchm_aux (TypSchm_ts (typq, typ), _)) = doc_binding (typq, typ) - -let doc_typschm_typ (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = doc_typ typ - -let doc_typschm_quants (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = - match tq_aux with - | TypQ_no_forall -> None - | TypQ_tq [] -> None - | TypQ_tq qs -> Some (doc_quants qs) - -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 rec doc_pat (P_aux (p_aux, _) as pat) = - match p_aux with - | P_id id -> doc_id id - | P_tup pats -> lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen - | P_typ (typ, pat) -> separate space [doc_pat pat; colon; doc_typ typ] - | P_lit lit -> doc_lit lit - (* P_var short form sugar *) - | P_var (P_aux (P_id id, _), kid) when Id.compare (id_of_kid kid) id == 0 -> - doc_kid kid - | P_var (pat, kid) -> separate space [doc_pat pat; string "as"; doc_kid kid] - | P_vector pats -> brackets (separate_map (comma ^^ space) doc_pat pats) - | P_vector_concat pats -> separate_map (space ^^ string "@" ^^ space) doc_pat pats - | P_wild -> string "_" - | P_as (pat, id) -> separate space [doc_pat pat; string "as"; doc_id id] - | P_app (id, pats) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_pat pats) - | _ -> string (string_of_pat pat) - -(* if_block_x is true if x should be printed like a block, i.e. with - newlines. Blocks are automatically printed as blocks, so this - returns false for them. *) -let if_block_then (E_aux (e_aux, _)) = - match e_aux with - | E_assign _ | E_if _ -> true - | _ -> false - -let if_block_else (E_aux (e_aux, _)) = - match e_aux with - | E_assign _ -> true - | _ -> false - -let fixities = - let fixities' = - List.fold_left - (fun r (x, y) -> Bindings.add x y r) - Bindings.empty - [ - (mk_id "^", (InfixR, 8)); - (mk_id "*", (InfixL, 7)); - (mk_id "+", (InfixL, 6)); - (mk_id "-", (InfixL, 6)); - (mk_id "!=", (Infix, 4)); - (mk_id ">", (Infix, 4)); - (mk_id "<", (Infix, 4)); - (mk_id ">=", (Infix, 4)); - (mk_id "<=", (Infix, 4)); - (mk_id "&", (InfixR, 3)); - (mk_id "|", (InfixR, 2)); - ] - in - ref (fixities' : (prec * int) Bindings.t) - -let rec doc_exp (E_aux (e_aux, _) as exp) = - match e_aux with - | E_block [] -> string "()" - | E_block [exp] -> doc_exp exp - | E_block exps -> surround 2 0 lbrace (doc_block exps) rbrace - | E_nondet exps -> assert false - (* This is mostly for the -convert option *) - | E_app_infix (x, id, y) when Id.compare (mk_id "quot") id == 0 -> - separate space [doc_atomic_exp x; string "/"; doc_atomic_exp y] - | E_app_infix _ -> doc_infix 0 exp - | E_tuple exps -> parens (separate_map (comma ^^ space) doc_exp exps) - - (* Various rules to try to format if blocks nicely based on content *) - | E_if (if_exp, then_exp, else_exp) when if_block_then then_exp && if_block_else else_exp -> - (separate space [string "if"; doc_exp if_exp; string "then"] ^//^ doc_exp then_exp) - ^/^ (string "else" ^//^ doc_exp else_exp) - | E_if (if_exp, then_exp, (E_aux (E_if _, _) as else_exp)) when if_block_then then_exp -> - (separate space [string "if"; doc_exp if_exp; string "then"] ^//^ doc_exp then_exp) - ^/^ (string "else" ^^ space ^^ doc_exp else_exp) - | E_if (if_exp, then_exp, else_exp) when if_block_else else_exp -> - (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp]) - ^^ space ^^ (string "else" ^//^ doc_exp else_exp) - | E_if (if_exp, then_exp, else_exp) when if_block_then then_exp -> - (separate space [string "if"; doc_exp if_exp; string "then"] ^//^ doc_exp then_exp) - ^/^ (string "else" ^^ space ^^ doc_exp else_exp) - | E_if (if_exp, then_exp, else_exp) -> - group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp; string "else"; doc_exp else_exp]) - - | E_list exps -> string "[|" ^^ separate_map (comma ^^ space) doc_exp exps ^^ string "|]" - | E_cons (exp1, exp2) -> string "E_cons" - | E_record fexps -> separate space [string "record"; string "{"; doc_fexps fexps; string "}"] - | E_loop (While, cond, exp) -> - separate space [string "while"; doc_exp cond; string "do"; doc_exp exp] - | E_loop (Until, cond, exp) -> - separate space [string "repeat"; doc_exp exp; string "until"; doc_exp cond] - | E_record_update (exp, fexps) -> - separate space [string "{"; doc_exp exp; string "with"; doc_fexps fexps; string "}"] - | E_vector_append (exp1, exp2) -> separate space [doc_atomic_exp exp1; string "@"; doc_atomic_exp exp2] - | E_case (exp, pexps) -> - separate space [string "match"; doc_exp exp; doc_pexps pexps] - | E_let (LB_aux (LB_val (pat, binding), _), exp) -> - separate space [string "let"; doc_pat pat; equals; doc_exp binding; string "in"; doc_exp exp] - | E_internal_plet (pat, exp1, exp2) -> - let le = - prefix 2 1 - (separate space [string "internal_plet"; doc_pat pat; equals]) - (doc_exp exp1) in - doc_op (string "in") le (doc_exp exp2) - | E_var (lexp, binding, exp) -> - separate space [string "var"; doc_lexp lexp; equals; doc_exp binding; string "in"; doc_exp exp] - | E_assign (lexp, exp) -> - separate space [doc_lexp lexp; equals; doc_exp exp] - | E_for (id, exp1, exp2, exp3, order, exp4) -> - begin - let header = - string "foreach" ^^ space ^^ - group (parens (separate (break 1) - [ doc_id id; - string "from " ^^ doc_atomic_exp exp1; - string "to " ^^ doc_atomic_exp exp2; - string "by " ^^ doc_atomic_exp exp3; - string "in " ^^ doc_ord order ])) - in - match exp4 with - | E_aux (E_block [_], _) -> header ^//^ doc_exp exp4 - | E_aux (E_block _, _) -> header ^^ space ^^ doc_exp exp4 - | _ -> header ^//^ doc_exp exp4 - end - (* Resugar an assert with an empty message *) - | E_throw exp -> string "throw" ^^ parens (doc_exp exp) - | E_try (exp, pexps) -> - separate space [string "try"; doc_exp exp; string "catch"; doc_pexps pexps] - | E_return exp -> string "return" ^^ parens (doc_exp exp) - | E_internal_return exp -> string "internal_return" ^^ parens (doc_exp exp) - | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 -> - separate space [string "2"; string "^"; doc_atomic_exp exp] - | _ -> doc_atomic_exp exp -and doc_infix n (E_aux (e_aux, _) as exp) = - match e_aux with - | E_app_infix (l, op, r) when n < 10 -> - begin - try - match Bindings.find op !fixities with - | (Infix, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r] - | (Infix, m) when m < n -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]) - | (InfixL, m) when m >= n -> separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r] - | (InfixL, m) when m < n -> parens (separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r]) - | (InfixR, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r] - | (InfixR, m) when m < n -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r]) - | _ -> assert false - with - | Not_found -> - separate space [doc_atomic_exp l; doc_id op; doc_atomic_exp r] - end - | _ -> doc_atomic_exp exp -and doc_atomic_exp (E_aux (e_aux, _) as exp) = - match e_aux with - | E_cast (typ, exp) -> - separate space [doc_atomic_exp exp; colon; doc_typ typ] - | E_lit lit -> doc_lit lit - | E_id id -> doc_id id - | E_ref id -> string "ref" ^^ space ^^ doc_id id - | E_field (exp, id) -> doc_atomic_exp exp ^^ dot ^^ doc_id id - | E_sizeof (Nexp_aux (Nexp_var kid, _)) -> doc_kid kid - | E_sizeof nexp -> string "sizeof" ^^ parens (doc_nexp nexp) - (* Format a function with a unit argument as f() rather than f(()) *) - | E_app (id, [E_aux (E_lit (L_aux (L_unit, _)), _)]) -> doc_id id ^^ string "()" - | E_app (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps) - | E_constraint nc -> string "constraint" ^^ parens (doc_nc nc) - | E_assert (exp1, E_aux (E_lit (L_aux (L_string "", _)), _)) -> string "assert" ^^ parens (doc_exp exp1) - | E_assert (exp1, exp2) -> string "assert" ^^ parens (doc_exp exp1 ^^ comma ^^ space ^^ doc_exp exp2) - | E_exit exp -> string "exit" ^^ parens (doc_exp exp) - | E_vector_access (exp1, exp2) -> doc_atomic_exp exp1 ^^ brackets (doc_exp exp2) - | E_vector_subrange (exp1, exp2, exp3) -> doc_atomic_exp exp1 ^^ brackets (separate space [doc_exp exp2; string ".."; doc_exp exp3]) - | E_vector exps -> brackets (separate_map (comma ^^ space) doc_exp exps) - | E_vector_update (exp1, exp2, exp3) -> - brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; equals; doc_exp exp3]) - | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> - brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4]) - | E_internal_value v -> string (Value.string_of_value v |> Util.green |> Util.clear) - | _ -> parens (doc_exp exp) -and doc_fexps (FES_aux (FES_Fexps (fexps, _), _)) = - separate_map (comma ^^ space) doc_fexp fexps -and doc_fexp (FE_aux (FE_Fexp (id, exp), _)) = - separate space [doc_id id; equals; doc_exp exp] -and doc_block = function - | [] -> string "()" - | [E_aux (E_let (LB_aux (LB_val (pat, binding), _), E_aux (E_block exps, _)), _)] -> - separate space [string "let"; doc_pat pat; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps - | [E_aux (E_var (lexp, binding, E_aux (E_block exps, _)), _)] -> - separate space [string "var"; doc_lexp lexp; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps - | [exp] -> doc_exp exp - | exp :: exps -> doc_exp exp ^^ semi ^^ hardline ^^ doc_block exps -and doc_lexp (LEXP_aux (l_aux, _) as lexp) = - match l_aux with - | LEXP_cast (typ, id) -> separate space [doc_id id; colon; doc_typ typ] - | _ -> doc_atomic_lexp lexp -and doc_atomic_lexp (LEXP_aux (l_aux, _) as lexp) = - match l_aux with - | LEXP_id id -> doc_id id - | LEXP_deref exp -> lparen ^^ string "*" ^^ doc_atomic_exp exp ^^ rparen - | LEXP_tup lexps -> lparen ^^ separate_map (comma ^^ space) doc_lexp lexps ^^ rparen - | LEXP_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id - | LEXP_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp) - | LEXP_vector_range (lexp, exp1, exp2) -> doc_atomic_lexp lexp ^^ brackets (separate space [doc_exp exp1; string ".."; doc_exp exp2]) - | LEXP_memory (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps) - | _ -> parens (doc_lexp lexp) -and doc_pexps pexps = surround 2 0 lbrace (separate_map (comma ^^ hardline) doc_pexp pexps) rbrace -and doc_pexp (Pat_aux (pat_aux, _)) = - match pat_aux with - | Pat_exp (pat, exp) -> separate space [doc_pat pat; string "=>"; doc_exp exp] - | Pat_when (pat, wh, exp) -> - separate space [doc_pat pat; string "if"; doc_exp wh; string "=>"; doc_exp exp] -and doc_letbind (LB_aux (lb_aux, _)) = - match lb_aux with - | LB_val (pat, exp) -> - separate space [doc_pat pat; equals; doc_exp exp] - -let doc_funcl funcl = string "FUNCL" - -let doc_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp,_)), _)) = - match pexp with - | Pat_exp (pat,exp) -> - group (separate space [doc_id id; doc_pat pat; equals; doc_exp exp]) - | Pat_when (pat,wh,exp) -> - group (separate space [doc_id id; parens (separate space [doc_pat pat; string "if"; doc_exp wh]); string "="; doc_exp exp]) - -let doc_default (DT_aux(df,_)) = match df with - | DT_kind(bk,v) -> string "DT_kind" (* separate space [string "default"; doc_bkind bk; doc_var v] *) - | DT_typ(ts,id) -> separate space [string "default"; doc_typschm ts; doc_id id] - | DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord] - -let doc_fundef (FD_aux (FD_function (r, typa, efa, funcls), _)) = - match funcls with - | [] -> failwith "Empty function list" - | _ -> - let sep = hardline ^^ string "and" ^^ space in - let clauses = separate_map sep doc_funcl funcls in - string "function" ^^ space ^^ clauses - -let doc_dec (DEC_aux (reg,_)) = - match reg with - | DEC_reg (typ, id) -> separate space [string "register"; doc_id id; colon; doc_typ typ] - | DEC_alias(id,alspec) -> string "ALIAS" - | DEC_typ_alias(typ,id,alspec) -> string "ALIAS" - -let doc_field (typ, id) = - separate space [doc_id id; colon; doc_typ typ] - -let doc_union (Tu_aux (tu, l)) = match tu with - | Tu_id id -> doc_id id - | Tu_ty_id (typ, id) -> separate space [doc_id id; colon; doc_typ typ] - -let doc_typdef (TD_aux(td,_)) = match td with - | TD_abbrev (id, _, typschm) -> - begin - match doc_typschm_quants typschm with - | Some qdoc -> - doc_op equals (concat [string "type"; space; doc_id id; space; qdoc]) (doc_typschm_typ typschm) - | None -> - doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm) - end - | TD_enum (id, _, ids, _) -> - separate space [string "enum"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace] - | TD_record (id, _, TypQ_aux (TypQ_no_forall, _), fields, _) | TD_record (id, _, TypQ_aux (TypQ_tq [], _), fields, _) -> - separate space [string "struct"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace] - | TD_record (id, _, TypQ_aux (TypQ_tq qs, _), fields, _) -> - separate space [string "struct"; doc_id id; doc_quants qs; equals; - surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace] - | TD_variant (id, _, TypQ_aux (TypQ_no_forall, _), unions, _) | TD_variant (id, _, TypQ_aux (TypQ_tq [], _), unions, _) -> - separate space [string "union"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace] - | TD_variant (id, _, TypQ_aux (TypQ_tq qs, _), unions, _) -> - separate space [string "union"; doc_id id; doc_quants qs; equals; - surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace] - | _ -> string "TYPEDEF" - -let doc_spec (VS_aux(v,_)) = - let doc_extern ext = - let doc_backend b = Util.option_map (fun id -> string (b ^ ":") ^^ space ^^ - utf8string ("\"" ^ String.escaped id ^ "\"")) (ext b) in - let docs = Util.option_these (List.map doc_backend ["ocaml"; "lem"]) in - if docs = [] then empty else equals ^^ space ^^ braces (separate (comma ^^ space) docs) - in - match v with - | VS_val_spec(ts,id,ext,is_cast) -> - string "val" ^^ space - ^^ (if is_cast then (string "cast" ^^ space) else empty) - ^^ doc_id id ^^ space - ^^ doc_extern ext - ^^ colon ^^ space - ^^ doc_typschm ts - -let doc_prec = function - | Infix -> string "infix" - | InfixL -> string "infixl" - | InfixR -> string "infixr" - -let doc_kind_def (KD_aux (KD_nabbrev (_, id, _, nexp), _)) = - separate space [string "integer"; doc_id id; equals; doc_nexp nexp] - -let rec doc_scattered (SD_aux (sd_aux, _)) = - match sd_aux with - | SD_scattered_function (_, _, _, id) -> - string "scattered" ^^ space ^^ string "function" ^^ space ^^ doc_id id - | SD_scattered_funcl funcl -> - string "function" ^^ space ^^ string "clause" ^^ space ^^ doc_funcl funcl - | SD_scattered_end id -> - string "end" ^^ space ^^ doc_id id - | _ -> string "SCATTERED" - -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_kind_def k_def - | DEF_fundef f_def -> doc_fundef f_def - | DEF_val lbind -> string "let" ^^ space ^^ doc_letbind lbind - | DEF_internal_mutrec fundefs -> - (string "mutual {" ^//^ separate_map (hardline ^^ hardline) doc_fundef fundefs) - ^^ hardline ^^ string "}" - | DEF_reg_dec dec -> doc_dec dec - | DEF_scattered sdef -> doc_scattered sdef - | DEF_fixity (prec, n, id) -> - fixities := Bindings.add id (prec, Big_int.to_int n) !fixities; - separate space [doc_prec prec; doc_int n; doc_id id] - | DEF_overload (id, ids) -> - separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace] - | DEF_comm (DC_comm s) -> string "TOPLEVEL" - | DEF_comm (DC_comm_struct d) -> string "TOPLEVEL" - ) ^^ hardline - -let doc_defs (Defs(defs)) = - separate_map hardline doc_def defs - -let pp_defs f d = ToChannel.pretty 1. 80 f (doc_defs d) - -let pretty_sail f doc = ToChannel.pretty 1. 120 f doc - -let to_string doc = - let b = Buffer.create 120 in - ToBuffer.pretty 1. 120 b doc; - Buffer.contents b diff --git a/src/process_file.ml b/src/process_file.ml index 116eeb0b..7a4f71e3 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -67,13 +67,13 @@ let get_lexbuf f = let parse_file (f : string) : Parse_ast.defs = let lexbuf, in_chan = get_lexbuf f in try - let ast = Parser2.file Lexer2.token lexbuf in + let ast = Parser.file Lexer.token lexbuf in close_in in_chan; ast with - | Parser2.Error -> + | Parser.Error -> let pos = Lexing.lexeme_start_p lexbuf in raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "no information"))) - | Lexer2.LexError(s,p) -> + | Lexer.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 @@ -92,7 +92,7 @@ let opt_dno_cast = ref false let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t = let ienv = if !opt_dno_cast then Type_check.Env.no_casts Type_check.initial_env else Type_check.initial_env in let ast, env = Type_check.check ienv defs in - let () = if !opt_ddump_tc_ast then Pretty_print_sail2.pp_defs stdout ast else () in + let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_defs stdout ast else () in let () = if !opt_just_check then exit 0 else () in (ast, env) @@ -103,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_sail2.pp_defs stdout ast else () in + let () = if !opt_ddump_raw_mono_ast then Pretty_print_sail.pp_defs stdout ast else () in let ienv = Type_check.Env.no_casts Type_check.initial_env in Type_check.check ienv ast @@ -191,7 +191,7 @@ let rewrite_step defs (name,rewriter) = let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in (* output "" Lem_ast_out [filename, defs]; *) let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted filename in - Pretty_print_sail2.pp_defs ot defs; + Pretty_print_sail.pp_defs ot defs; close_output_with_check ext_ot; opt_ddump_rewrite_ast := Some (f, i + 1) end diff --git a/src/sail.ml b/src/sail.ml index fdcaa15c..974885c6 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -186,7 +186,7 @@ let main() = let ast = convert_ast Ast_util.inc_ord ast in if !opt_convert - then (Pretty_print_sail2.pp_defs stdout ast; exit 0) + then (Pretty_print_sail.pp_defs stdout ast; exit 0) else (); let (ast, type_envs) = check_ast ast in @@ -221,7 +221,7 @@ let main() = () else ()); (if !(opt_print_verbose) - then ((Pretty_print_sail2.pp_defs stdout) ast) + then ((Pretty_print_sail.pp_defs stdout) ast) else ()); (if !(opt_print_lem_ast) then output "" Lem_ast_out [out_name,ast] @@ -229,7 +229,7 @@ let main() = (if !(opt_print_sil) then let ast = rewrite_ast_sil ast in - Pretty_print_sail2.pp_defs stdout ast + Pretty_print_sail.pp_defs stdout ast else ()); (if !(opt_print_ocaml) then diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 3d3b13e3..96f6e546 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -625,7 +625,7 @@ let merge_mutrecs defs = | DEF_fundef fundef -> fundef :: fundefs | DEF_internal_mutrec fundefs' -> fundefs' @ fundefs | _ -> - (* let _ = Pretty_print_sail2.pp_defs stderr (Defs [def]) in *) + (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) raise (Reporting_basic.err_unreachable (def_loc def) "Trying to merge non-function definition with mutually recursive functions") in (* let _ = Printf.eprintf " - Merging %s (using %s)\n" (set_to_string binds') (set_to_string uses') in *) -- cgit v1.2.3