<commit_before>/**************************************************************************/
/*                                                                        */
/*  Copyright (C) 2010-                                                   */
/*    <NAME>                                                      */
/*    <NAME>                                           */
/*    <NAME>                                                      */
/*    <NAME>                                                    */
/*                                                                        */
/*  This software is free software; you can redistribute it and/or        */
/*  modify it under the terms of the GNU Library General Public           */
/*  License version 2.1, with the special exception on linking            */
/*  described in file LICENSE.                                            */
/*                                                                        */
/*  This software is distributed in the hope that it will be useful,      */
/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  */
/*                                                                        */
/**************************************************************************/

%{

  open Ptree
  open Parsing

  let loc () = (symbol_start_pos (), symbol_end_pos ())
  let loc_i i = (rhs_start_pos i, rhs_end_pos i)
  let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)

  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
  let mk_pp d = mk_ppl (loc ()) d
  let mk_pp_i i d = mk_ppl (loc_i i) d

  let mk_pat p = { pat_loc = loc (); pat_desc = p }

  let infix_ppl loc a i b = mk_ppl loc (PPbinop (a, i, b))
  let infix_pp a i b = infix_ppl (loc ()) a i b

  let prefix_ppl loc p a = mk_ppl loc (PPunop (p, a))
  let prefix_pp p a = prefix_ppl (loc ()) p a

  let infix s = "infix " ^ s
  let prefix s = "prefix " ^ s

  let () = Exn_printer.register
    (fun fmt exn -> match exn with
      | Parsing.Parse_error -> Format.fprintf fmt "syntax error"
      | _ -> raise exn
    )

%}

/* Tokens */

%token <string> LIDENT UIDENT
%token <string> INTEGER
%token <string> OP1 OP2 OP3 OP4 OPPREF
%token <Ptree.real_constant> FLOAT
%token <string> STRING

/* keywords */

%token AND AS AXIOM CLONE
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET LOGIC MATCH META NAMESPACE NOT PROP OR
%token THEN THEORY TRUE TYPE USE WITH

/* symbols */

%token ARROW
%token BAR
%token COLON COMMA
%token DOT EQUAL
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
%token LRARROW
%token QUOTE
%token RIGHTPAR RIGHTSQ
%token UNDERSCORE

%token EOF


/* Precedences */

%nonassoc prec_decls
%nonassoc LOGIC TYPE INDUCTIVE

%nonassoc DOT ELSE IN
%nonassoc COLON

%nonassoc prec_named
%right ARROW LRARROW
%right OR
%right AND
%nonassoc NOT
%left EQUAL OP1
%left OP2
%left OP3
%left OP4
%nonassoc prefix_op
%nonassoc OPPREF

/* Entry points */

%type <Ptree.lexpr> lexpr
%start lexpr
%type <Ptree.decl list> list0_decl
%start list0_decl
%type <Ptree.logic_file> logic_file
%start logic_file
%%

/* File, theory, declaration */

logic_file:
| list1_theory EOF  { $1 }
| EOF               { [] }
;

list1_theory:
| theory                { [$1] }
| theory list1_theory   { $1 :: $2 }
;

theory:
| THEORY uident list0_decl END
   { { pt_loc = loc (); pt_name = $2; pt_decl = $3 } }
;

list0_decl:
| /* epsilon */    { [] }
| decl list0_decl  { $1 :: $2 }
;

decl:
| list1_type_decl
    { TypeDecl $1 }
| list1_logic_decl
    { LogicDecl $1 }
| list1_inductive_decl
    { IndDecl $1 }
| AXIOM uident COLON lexpr
    { PropDecl (loc (), Kaxiom, $2, $4) }
| LEMMA uident COLON lexpr
    { PropDecl (loc (), Klemma, $2, $4) }
| GOAL uident COLON lexpr
    { PropDecl (loc (), Kgoal, $2, $4) }
| USE use
    { UseClone (loc (), $2, None) }
| CLONE use clone_subst
    { UseClone (loc (), $2, Some $3) }
| NAMESPACE uident list0_decl END
    { Namespace (loc (), false, Some $2, $3) }
| NAMESPACE UNDERSCORE list0_decl END
    { Namespace (loc (), false, None, $3) }
| NAMESPACE IMPORT uident list0_decl END
    { Namespace (loc (), true, Some $3, $4) }
| NAMESPACE IMPORT UNDERSCORE list0_decl END
    { Namespace (loc (), true, None, $4) }
| META ident list1_meta_arg_sep_comma
    { Meta (loc (), $2, $3) }
;

/* Use and clone */

use:
| imp_exp tqualid
    { { use_theory = $2; use_as = None; use_imp_exp = $1 } }
| imp_exp tqualid AS uident
    { { use_theory = $2; use_as = Some (Some $4); use_imp_exp = $1 } }
| imp_exp tqualid AS UNDERSCORE
    { { use_theory = $2; use_as = Some None; use_imp_exp = $1 } }
;

imp_exp:
| IMPORT        { Import }
| EXPORT        { Export }
| /* epsilon */ { Nothing }
;

clone_subst:<commit_msg>In a .why a meta can be an ident or a string<commit_after>/**************************************************************************/
/*                                                                        */
/*  Copyright (C) 2010-                                                   */
/*    <NAME>                                                      */
/*    <NAME>                                           */
/*    <NAME>                                                      */
/*    <NAME>                                                    */
/*                                                                        */
/*  This software is free software; you can redistribute it and/or        */
/*  modify it under the terms of the GNU Library General Public           */
/*  License version 2.1, with the special exception on linking            */
/*  described in file LICENSE.                                            */
/*                                                                        */
/*  This software is distributed in the hope that it will be useful,      */
/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  */
/*                                                                        */
/**************************************************************************/

%{

  open Ptree
  open Parsing

  let loc () = (symbol_start_pos (), symbol_end_pos ())
  let loc_i i = (rhs_start_pos i, rhs_end_pos i)
  let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)

  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
  let mk_pp d = mk_ppl (loc ()) d
  let mk_pp_i i d = mk_ppl (loc_i i) d

  let mk_pat p = { pat_loc = loc (); pat_desc = p }

  let infix_ppl loc a i b = mk_ppl loc (PPbinop (a, i, b))
  let infix_pp a i b = infix_ppl (loc ()) a i b

  let prefix_ppl loc p a = mk_ppl loc (PPunop (p, a))
  let prefix_pp p a = prefix_ppl (loc ()) p a

  let infix s = "infix " ^ s
  let prefix s = "prefix " ^ s

  let () = Exn_printer.register
    (fun fmt exn -> match exn with
      | Parsing.Parse_error -> Format.fprintf fmt "syntax error"
      | _ -> raise exn
    )

%}

/* Tokens */

%token <string> LIDENT UIDENT
%token <string> INTEGER
%token <string> OP1 OP2 OP3 OP4 OPPREF
%token <Ptree.real_constant> FLOAT
%token <string> STRING

/* keywords */

%token AND AS AXIOM CLONE
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET LOGIC MATCH META NAMESPACE NOT PROP OR
%token THEN THEORY TRUE TYPE USE WITH

/* symbols */

%token ARROW
%token BAR
%token COLON COMMA
%token DOT EQUAL
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
%token LRARROW
%token QUOTE
%token RIGHTPAR RIGHTSQ
%token UNDERSCORE

%token EOF


/* Precedences */

%nonassoc prec_decls
%nonassoc LOGIC TYPE INDUCTIVE

%nonassoc DOT ELSE IN
%nonassoc COLON

%nonassoc prec_named
%right ARROW LRARROW
%right OR
%right AND
%nonassoc NOT
%left EQUAL OP1
%left OP2
%left OP3
%left OP4
%nonassoc prefix_op
%nonassoc OPPREF

/* Entry points */

%type <Ptree.lexpr> lexpr
%start lexpr
%type <Ptree.decl list> list0_decl
%start list0_decl
%type <Ptree.logic_file> logic_file
%start logic_file
%%

/* File, theory, declaration */

logic_file:
| list1_theory EOF  { $1 }
| EOF               { [] }
;

list1_theory:
| theory                { [$1] }
| theory list1_theory   { $1 :: $2 }
;

theory:
| THEORY uident list0_decl END
   { { pt_loc = loc (); pt_name = $2; pt_decl = $3 } }
;

list0_decl:
| /* epsilon */    { [] }
| decl list0_decl  { $1 :: $2 }
;

decl:
| list1_type_decl
    { TypeDecl $1 }
| list1_logic_decl
    { LogicDecl $1 }
| list1_inductive_decl
    { IndDecl $1 }
| AXIOM uident COLON lexpr
    { PropDecl (loc (), Kaxiom, $2, $4) }
| LEMMA uident COLON lexpr
    { PropDecl (loc (), Klemma, $2, $4) }
| GOAL uident COLON lexpr
    { PropDecl (loc (), Kgoal, $2, $4) }
| USE use
    { UseClone (loc (), $2, None) }
| CLONE use clone_subst
    { UseClone (loc (), $2, Some $3) }
| NAMESPACE uident list0_decl END
    { Namespace (loc (), false, Some $2, $3) }
| NAMESPACE UNDERSCORE list0_decl END
    { Namespace (loc (), false, None, $3) }
| NAMESPACE IMPORT uident list0_decl END
    { Namespace (loc (), true, Some $3, $4) }
| NAMESPACE IMPORT UNDERSCORE list0_decl END
    { Namespace (loc (), true, None, $4) }
| META ident list1_meta_arg_sep_comma
    { Meta (loc (), $2, $3) }
| META STRING list1_meta_arg_sep_comma
    { Meta (loc (), { id = $2; id_loc = loc_i 2 }, $3) }
;

/* Use and clone */

use:
| imp_exp tqualid
    { { use_theory = $2; use_as = None; use_imp_exp = $1 } }
| imp_exp tqualid AS uident
    { { use_theory = $2; use_as = Some (Some $4); use_imp_exp = $1 } }
| imp_exp tqualid AS UNDERSCORE
    { { use_theory = $2; use_as = Some None; use_imp_exp = $1 } }
;

imp_exp:
| IMPORT        { Import }
| EXPORT        { Export }
| /* epsilon */ { Nothing }
;

clone_subst:
{'fraction_non_alphanumeric': 0.13853389224005724, 'fraction_numerical': 0.013700030671710458, 'mean_word_length': 1.951719975859988, 'pattern_counts': {'":': 0, '<': 27, '<?xml version=': 0, '>': 33, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 48, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1963703', 'n_tokens_mistral': 3347, 'n_tokens_neox': 3199, 'n_words': 1021}