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