src/parser.mly

   1 (* Goalfile parser
   2  * Copyright (C) 2019 Richard W.M. Jones
   3  * Copyright (C) 2019 Red Hat Inc.
   4  *
   5  * This program is free software; you can redistribute it and/or modify
   6  * it under the terms of the GNU General Public License as published by
   7  * the Free Software Foundation; either version 2 of the License, or
   8  * (at your option) any later version.
   9  *
  10  * This program is distributed in the hope that it will be useful,
  11  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  12  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  13  * GNU General Public License for more details.
  14  *
  15  * You should have received a copy of the GNU General Public License along
  16  * with this program; if not, write to the Free Software Foundation, Inc.,
  17  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  18  *)
  19
  20 %{
  21 open Utils
  22 open Printf
  23
  24 (* There are several circular dependencies between the lexer
  25  * (caused by includes) and eval.  These references break
  26  * the circular dependencies.  They are initialized when
  27  * the program starts, hence are never really None.
  28  *)
  29 let lexer_read = ref None
  30 let eval_substitute = ref None
  31
  32 let find_on_include_path filename =
  33   if not (Filename.is_implicit filename) then filename
  34   else (
  35     let rec loop = function
  36       | [] -> filename
  37       | inc :: incs ->
  38          let path = inc // filename in
  39          if Sys.file_exists path then path else loop incs
  40     in
  41     loop (Cmdline.includes ())
  42   )
  43
  44 let do_include env loc filename optflag file =
  45   let eval_substitute =
  46     match !eval_substitute with None -> assert false | Some f -> f in
  47   let filename = eval_substitute env loc filename in
  48   let filename = find_on_include_path filename in
  49   if optflag && not (Sys.file_exists filename) then env
  50   else (
  51     let fp = open_in filename in
  52     let lexbuf = Lexing.from_channel fp in
  53     lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename };
  54     let lexer_read =
  55       match !lexer_read with None -> assert false | Some r -> r in
  56     let env' = file lexer_read lexbuf in
  57     close_in fp;
  58     Ast.Env.merge env env'
  59   )
  60 %}
  61
  62 (* Tokens. *)
  63 %token <Ast.code> CODE
  64 %token COLON
  65 %token COMMA
  66 %token EQUALS
  67 %token EOF
  68 %token EXPRESSION
  69 %token FUNCTION
  70 %token GOAL
  71 %token <string> ID
  72 %token INCLUDE
  73 %token LEFT_ARRAY
  74 %token LEFT_PAREN
  75 %token LET
  76 %token OPTINCLUDE
  77 %token PURE
  78 %token RETURNING
  79 %token RIGHT_ARRAY
  80 %token RIGHT_PAREN
  81 %token SEMICOLON
  82 %token <Ast.substs> STRING
  83 %token STRING_KEYWORD
  84 %token STRINGS
  85 %token <string> PRED
  86 %token PREDICATE
  87
  88 (* Start nonterminals. *)
  89 %start <Ast.expr Ast.Env.t> file
  90 %start <Ast.expr> expr_only
  91 %%
  92
  93 file:
  94     | stmts EOF  { $1 }
  95     ;
  96
  97 stmts:
  98     | (* none *) { Ast.Env.empty }
  99     | stmts INCLUDE STRING option(SEMICOLON)
 100     { do_include $1 $loc $3 false file }
 101     | stmts OPTINCLUDE STRING option(SEMICOLON)
 102     { do_include $1 $loc $3 true file }
 103     | stmts stmt option(SEMICOLON)
 104     { let name, expr = $2 in Ast.Env.add name expr $1 }
 105     ;
 106
 107 stmt:
 108     | option(goal_stmt) patterns COLON barelist option(CODE)
 109     { let name, params =
 110         match $1 with
 111         | None ->
 112            sprintf "_goal@%d" $startpos.pos_lnum, []
 113         | Some x -> x in
 114       name, Ast.EGoalDefn ($loc, (params, $2, $4, $5))
 115     }
 116     | goal_stmt CODE
 117     {
 118       let name, params = $1 in
 119       name, Ast.EGoalDefn ($loc, (params, [], [], Some $2))
 120     }
 121     | GOAL ID
 122     {
 123       $2, Ast.EGoalDefn ($loc, ([], [], [], None))
 124     }
 125     | option(PURE) FUNCTION ID params_decl return_decl EQUALS CODE
 126     {
 127       $3, Ast.EFuncDefn ($loc, ($4, $5, $1 <> None, $7))
 128     }
 129     | PREDICATE PRED params_decl EQUALS CODE
 130     {
 131       $2, Ast.EPredDefn ($loc, ($3, $5))
 132     }
 133     | LET ID EQUALS expr { $2, $4 }
 134     ;
 135
 136 goal_stmt:
 137     | GOAL ID option(params_decl) EQUALS
 138     { $2, match $3 with None -> [] | Some ps -> ps }
 139     ;
 140 params_decl:
 141     | LEFT_PAREN separated_list(COMMA, param_decl) RIGHT_PAREN { $2 }
 142     ;
 143 param_decl:
 144     | ID         { $1 }
 145 return_decl:
 146     |            { RetExpr }
 147     | RETURNING EXPRESSION { RetExpr }
 148     | RETURNING STRINGS { RetStrings }
 149     | RETURNING STRING_KEYWORD { RetString }
 150
 151 patterns:
 152     | separated_list(COMMA, pattern) { $1 }
 153     ;
 154 pattern:
 155     | STRING     { Ast.PPred ($loc, "is-file", [$1]) }
 156     | PRED pattern_params { Ast.PPred ($loc, $1, $2) }
 157     ;
 158 pattern_params:
 159     | LEFT_PAREN separated_list(COMMA, pattern_param) RIGHT_PAREN { $2 }
 160     ;
 161 pattern_param:
 162     | STRING     { $1 }
 163     ;
 164
 165 expr:
 166     | ID params  { Ast.ECall ($loc, $1, $2) }
 167     | ID         { Ast.EVar ($loc, $1) }
 168     | PRED params { Ast.EPredCtor ($loc, $1, $2) }
 169     | STRING     { Ast.ESubsts ($loc, $1) }
 170     | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
 171     ;
 172 barelist:
 173     | right_flexible_list(COMMA, expr) { $1 }
 174     ;
 175 params:
 176     | LEFT_PAREN separated_list(COMMA, expr) RIGHT_PAREN { $2 }
 177     ;
 178
 179 (* This is used by Parse.parse_expr where we have to parse
 180  * a standalone string (eg. from the command line).
 181  *)
 182 expr_only:
 183     | expr EOF   { $1 }
 184     ;
 185
 186 (* http://gallium.inria.fr/blog/lr-lists/ *)
 187 right_flexible_list(delim, X):
 188     | (* nothing *) { [] }
 189     | x = X { [x] }
 190     | x = X delim xs = right_flexible_list(delim, X) { x :: xs }