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 (* This is initialized with Lexer.read once the program
  25  * starts.  Doing this avoids a circular dependency caused
  26  * by include files.
  27  *)
  28 let lexer_read = ref None
  29
  30 let find_on_include_path filename =
  31   if not (Filename.is_implicit filename) then filename
  32   else (
  33     let rec loop = function
  34       | [] -> filename
  35       | inc :: incs ->
  36          let path = inc // filename in
  37          if Sys.file_exists path then path else loop incs
  38     in
  39     loop Cmdline.includes
  40   )
  41
  42 let do_include env loc filename optflag file =
  43   let filename = Ast.substitute env loc filename in
  44   let filename = find_on_include_path filename in
  45   if optflag && not (Sys.file_exists filename) then env
  46   else (
  47     let fp = open_in filename in
  48     let lexbuf = Lexing.from_channel fp in
  49     lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename };
  50     let reader =
  51       match !lexer_read with None -> assert false | Some r -> r in
  52     let env' = file reader lexbuf in
  53     close_in fp;
  54     Ast.Env.merge env env'
  55   )
  56 %}
  57
  58 (* Tokens. *)
  59 %token <Ast.substs> CODE
  60 %token COLON
  61 %token COMMA
  62 %token EQUALS
  63 %token EOF
  64 %token GOAL
  65 %token <string> ID
  66 %token INCLUDE
  67 %token LEFT_ARRAY
  68 %token LEFT_PAREN
  69 %token LET
  70 %token OPTINCLUDE
  71 %token RIGHT_ARRAY
  72 %token RIGHT_PAREN
  73 %token <Ast.substs> STRING
  74 %token <string> TACTIC
  75 %token TACTIC_KEYWORD
  76
  77 (* Start nonterminals. *)
  78 %start <Ast.expr Ast.Env.t> file
  79 %start <Ast.expr> expr
  80 %%
  81
  82 file:
  83     | stmts EOF  { $1 }
  84     ;
  85
  86 stmts:
  87     | (* none *) { Ast.Env.empty }
  88     | stmts INCLUDE STRING
  89     { do_include $1 $loc $3 false file }
  90     | stmts OPTINCLUDE STRING
  91     { do_include $1 $loc $3 true file }
  92     | stmts stmt  { let name, expr = $2 in Ast.Env.add name expr $1 }
  93     ;
  94
  95 stmt:
  96     | option(goal_stmt) patterns COLON barelist option(CODE)
  97     { let name, params =
  98         match $1 with
  99         | None ->
 100            sprintf "_goal@%d" $startpos.pos_lnum, []
 101         | Some x -> x in
 102       name, Ast.EGoalDefn ($loc, (params, $2, $4, $5))
 103     }
 104     | goal_stmt CODE
 105     {
 106       let name, params = $1 in
 107       name, Ast.EGoalDefn ($loc, (params, [], [], Some $2))
 108     }
 109     | TACTIC_KEYWORD TACTIC params_decl EQUALS CODE
 110     {
 111       $2, Ast.ETacticDefn ($loc, ($3, $5))
 112     }
 113     | LET ID EQUALS expr { $2, $4 }
 114     ;
 115
 116 goal_stmt:
 117     | GOAL ID option(params_decl) EQUALS
 118     { $2, match $3 with None -> [] | Some ps -> ps }
 119     ;
 120 params_decl:
 121     | LEFT_PAREN separated_list(COMMA, param_decl) RIGHT_PAREN { $2 }
 122     ;
 123 param_decl:
 124     | ID         { $1 }
 125
 126 patterns:
 127     | separated_list(COMMA, pattern) { $1 }
 128     ;
 129 pattern:
 130     | STRING     { Ast.PTactic ($loc, "*file", [$1]) }
 131     | ID pattern_params { Ast.PTactic ($loc, $1, $2) }
 132     ;
 133 pattern_params:
 134     | LEFT_PAREN separated_list(COMMA, pattern_param) RIGHT_PAREN { $2 }
 135     ;
 136 pattern_param:
 137     | STRING     { $1 }
 138     ;
 139
 140 expr:
 141     | ID params  { Ast.ECallGoal ($loc, $1, $2) }
 142     | ID         { Ast.EVar ($loc, $1) }
 143     | TACTIC params { Ast.ETacticConstructor ($loc, $1, $2) }
 144     | STRING     { Ast.ESubsts ($loc, $1) }
 145     | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
 146     ;
 147 barelist:
 148     | separated_list(COMMA, expr) { $1 }
 149     ;
 150 params:
 151     | LEFT_PAREN separated_list(COMMA, expr) RIGHT_PAREN { $2 }
 152     ;