Commit 55b108ab authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

actually add the ocamlyacc file

parent 0459a044
/**************************************************************************/
/* */
/* Copyright (C) 2010-2011 */
/* François Bobot */
/* Jean-Christophe Filliâtre */
/* Claude Marché */
/* Andrei Paskevich */
/* */
/* 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 Parsing
open Tptp_ast
let loc () = (symbol_start_pos (), symbol_end_pos ())
let floc () = Loc.extract (loc ())
let loc_i i = (rhs_start_pos i, rhs_end_pos i)
let floc_i i = Loc.extract (loc_i i)
let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
let floc_ij i j = Loc.extract (loc_ij i j)
let mk_ty n = { ty_node = n ; ty_loc = floc () }
let mk_term n = { t_node = n ; t_loc = floc () }
let mk_formula n = { f_node = n ; f_loc = floc () }
let mk_binding n = { b_node = n ; b_loc = floc () }
let () = Exn_printer.register (fun fmt exn -> match exn with
| Parsing.Parse_error -> Format.fprintf fmt "syntax error"
| _ -> raise exn)
%}
/* tokens */
%token <string> LWORD UWORD DWORD
%token <string> SINGLE_QUOTED DISTINCT_OBJECT
%token <num_integer> INTNUM
%token <num_rational> RATNUM
%token <num_real> REALNUM
/* keywords */
%token ASSUMPTION AXIOM CNF CONJECTURE DEFINITION FOF
%token HYPOTHESIS INCLUDE LEMMA NEGATED_CONJECTURE TFF
%token THEOREM TYPE
/* symbols */
%token DOT COMMA COLON LEFTPAR RIGHTPAR LEFTSQ RIGHTSQ
%token LONGARROW LARROW RARROW LRARROW NLRARROW NAMP NBAR
%token TILDE EQUAL NEQUAL STAR GT PI BANG QUES
%token SLASH_STAR_SLASH EOF
/* entry points */
%type <tptp_file> tptp_file
%start tptp_file
%%
tptp_file:
| list0_input EOF { $1 }
;
list0_input:
| /* epsilon */ { [] }
| input list0_input { $1 :: $2 }
;
input:
| kind LEFTPAR name COMMA role COMMA top_formula annotation RIGHTPAR DOT
{ Formula ($1, $3, $5, $7, floc ()) }
| INCLUDE LEFTPAR SINGLE_QUOTED formula_selection RIGHTPAR DOT
{ Include ($3, $4, floc ()) }
;
kind:
| TFF { TFF }
| FOF { FOF }
| CNF { CNF }
;
role:
| AXIOM { Axiom }
| HYPOTHESIS { Hypothesis }
| DEFINITION { Definition }
| ASSUMPTION { Assumption }
| LEMMA { Lemma }
| THEOREM { Theorem }
| CONJECTURE { Conjecture }
| NEGATED_CONJECTURE { Negated_conjecture }
| TYPE { Type }
| LWORD { Unknown $1 }
;
top_formula:
| logic_formula { $1 }
| typed_atom { $1 }
| sequent { $1 }
;
/* typed_atom */
typed_atom:
| untyped_atom COLON top_type { TypedAtom ($1,$3) }
| LEFTPAR typed_atom RIGHTPAR { $2 }
;
untyped_atom:
| atomic_word { $1 }
/*
| DDWORD { $1 }
*/
;
top_type:
| atomic_type { [],[],$1 }
| mapping_type { let l,r = $1 in [],l,r }
| quantified_type { $1 }
;
quantified_type:
| PI LEFTSQ varlist RIGHTSQ COLON monotype { let l,r = $6 in $3,l,r }
| LEFTPAR quantified_type RIGHTPAR { $2 }
;
monotype:
| atomic_type { [],$1 }
| LEFTPAR mapping_type RIGHTPAR { $2 }
;
mapping_type:
| unitary_type GT atomic_type { $1,$2 }
| LEFTPAR mapping_type RIGHTPAR { $2 }
;
unitary_type:
| atomic_type { [1] }
| LEFTPAR xprod_type RIGHTPAR { $2 }
;
xprod_type:
| atomic_type STAR atomic_type { [$1;$2] }
| xprod_type STAR atomic_type { $1 @ [$2] }
| LEFTPAR xprod_type RIGHTPAR { $2 }
;
/* atomic type */
atomic_type:
| variable { mk_ty (TVar $1) }
| atomic_word { mk_ty (TConstr ($1,[])) }
| atomic_word LEFTPAR list1_atomic_type RIGHTPAR { mk_ty (TConstr ($1,$3)) }
| defined_type { mk_ty (TDef $1) }
;
list1_atomic_type:
| atomic_type { [$1] }
| atomic_type COMMA list1_atomic_type { $1 :: $3 }
;
defined_type
/* sequent */
sequent:
| tuple LONGARROW tuple { Sequent ($1,$3) }
| LEFTPAR sequent RIGHTPAR { $2 }
;
tuple:
| LEFTSQ RIGHTSQ { [] }
| LEFTSQ list1_logic_formula RIGHTSQ { $2 }
;
list1_logic_formula:
| logic_formula { [$1] }
| logic_formula COMMA list1_logic_formula { $1 :: $3 }
;
/* misc */
number:
| INTNUM { Nint $1 }
| RATNUM { Nrat $1 }
| REALNUM { Nreal $1 }
;
atomic_word:
| LWORD { $1 }
| SINGLE_QUOTED { $1 }
;
/* TODO: add support for annotations */
annotation:
| /* epsilon */ { () }
;
formula_selection:
| /* epsilon */ { [] }
| COMMA LEFTSQ list1_name RIGHTSQ { $3 }
;
list1_name:
| name { [$1] }
| name COMMA list1_name { $1 :: $3 }
;
name:
| atomic_word { $1 }
| INTNUM { $1 }
;
%
/* File, theory, namespace */
list0_theory:
| /* epsilon */ { () }
| theory list0_theory { () }
;
theory_head:
| THEORY uident labels { Incremental.open_theory (add_lab $2 $3) }
;
theory:
| theory_head list0_decl END { Incremental.close_theory (floc_i 1) }
;
list0_decl:
| /* epsilon */ { () }
| new_decl list0_decl { () }
;
new_decl:
| decl
{ Incremental.new_decl $1 }
| namespace_head namespace_import namespace_name list0_decl END
{ Incremental.close_namespace (floc_i 3) $2 $3 }
;
namespace_head:
| NAMESPACE { Incremental.open_namespace () }
;
namespace_import:
| /* epsilon */ { false }
| IMPORT { true }
;
namespace_name:
| uident { Some $1 }
| UNDERSCORE { None }
;
/* Declaration */
decl:
| TYPE list1_type_decl
{ TypeDecl $2 }
| FUNCTION list1_logic_decl_function
{ LogicDecl $2 }
| PREDICATE list1_logic_decl_predicate
{ LogicDecl $2 }
| INDUCTIVE list1_inductive_decl
{ IndDecl $2 }
| AXIOM ident labels COLON lexpr
{ PropDecl (floc (), Kaxiom, add_lab $2 $3, $5) }
| LEMMA ident labels COLON lexpr
{ PropDecl (floc (), Klemma, add_lab $2 $3, $5) }
| GOAL ident labels COLON lexpr
{ PropDecl (floc (), Kgoal, add_lab $2 $3, $5) }
| USE use
{ UseClone (floc (), $2, None) }
| CLONE use clone_subst
{ UseClone (floc (), $2, Some $3) }
| META sident list1_meta_arg_sep_comma
{ Meta (floc (), $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:
| /* epsilon */ { [] }
| WITH list1_comma_subst { $2 }
;
list1_comma_subst:
| subst { [$1] }
| subst COMMA list1_comma_subst { $1 :: $3 }
;
subst:
| NAMESPACE ns EQUAL ns { CSns ($2, $4) }
| TYPE qualid EQUAL qualid { CStsym ($2, $4) }
| FUNCTION qualid EQUAL qualid { CSfsym ($2, $4) }
| PREDICATE qualid EQUAL qualid { CSpsym ($2, $4) }
| LEMMA qualid { CSlemma $2 }
| GOAL qualid { CSgoal $2 }
;
ns:
| uqualid { Some $1 }
| DOT { None }
;
/* Meta args */
list1_meta_arg_sep_comma:
| meta_arg { [$1] }
| meta_arg COMMA list1_meta_arg_sep_comma { $1 :: $3 }
;
meta_arg:
| TYPE qualid { PMAts $2 }
| FUNCTION qualid { PMAfs $2 }
| PREDICATE qualid { PMAps $2 }
| PROP qualid { PMApr $2 }
| STRING { PMAstr $1 }
| INTEGER { PMAint (small_integer $1) }
;
/* Type declarations */
list1_type_decl:
| type_decl { [$1] }
| type_decl WITH list1_type_decl { $1 :: $3 }
;
type_decl:
| lident labels type_args typedefn
{ let model, def = $4 in
{ td_loc = floc (); td_ident = add_lab $1 $2;
td_params = $3; td_model = model; td_def = def } }
;
type_args:
| /* epsilon */ { [] }
| type_var labels type_args { add_lab $1 $2 :: $3 }
;
typedefn:
| /* epsilon */ { false, TDabstract }
| equal_model primitive_type { $1, TDalias $2 }
| equal_model typecases { $1, TDalgebraic $2 }
| equal_model BAR typecases { $1, TDalgebraic $3 }
| equal_model record_type { $1, TDrecord $2 }
;
equal_model:
| EQUAL { false }
| MODEL { true }
;
record_type:
| LEFTREC list1_record_field opt_semicolon RIGHTREC { List.rev $2 }
;
list1_record_field:
| record_field { [$1] }
| list1_record_field SEMICOLON record_field { $3 :: $1 }
;
record_field:
| opt_mutable lident labels COLON primitive_type
{ floc (), $1, add_lab $2 $3, $5 }
;
typecases:
| typecase { [$1] }
| typecase BAR typecases { $1::$3 }
;
typecase:
| uident labels params { (floc (), add_lab $1 $2, $3) }
;
/* Logic declarations */
list1_logic_decl_function:
| logic_decl_function { [$1] }
| logic_decl_function WITH list1_logic_decl { $1 :: $3 }
;
list1_logic_decl_predicate:
| logic_decl_predicate { [$1] }
| logic_decl_predicate WITH list1_logic_decl { $1 :: $3 }
;
list1_logic_decl:
| logic_decl { [$1] }
| logic_decl WITH list1_logic_decl { $1 :: $3 }
;
logic_decl_function:
| lident_rich labels params COLON primitive_type logic_def_option
{ { ld_loc = floc (); ld_ident = add_lab $1 $2;
ld_params = $3; ld_type = Some $5; ld_def = $6 } }
;
logic_decl_predicate:
| lident_rich labels params logic_def_option
{ { ld_loc = floc (); ld_ident = add_lab $1 $2;
ld_params = $3; ld_type = None; ld_def = $4 } }
;
logic_decl:
| lident_rich labels params logic_type_option logic_def_option
{ { ld_loc = floc (); ld_ident = add_lab $1 $2;
ld_params = $3; ld_type = $4; ld_def = $5 } }
;
logic_type_option:
| /* epsilon */ { None }
| COLON primitive_type { Some $2 }
;
logic_def_option:
| /* epsilon */ { None }
| EQUAL lexpr { Some $2 }
;
/* Inductive declarations */
list1_inductive_decl:
| inductive_decl { [$1] }
| inductive_decl WITH list1_inductive_decl { $1 :: $3 }
;
inductive_decl:
| lident_rich labels params inddefn
{ { in_loc = floc (); in_ident = add_lab $1 $2;
in_params = $3; in_def = $4 } }
;
inddefn:
| /* epsilon */ { [] }
| EQUAL bar_ indcases { $3 }
;
indcases:
| indcase { [$1] }
| indcase BAR indcases { $1::$3 }
;
indcase:
| ident labels COLON lexpr { (floc (), add_lab $1 $2, $4) }
;
/* Type expressions */
primitive_type:
| primitive_type_arg { $1 }
| lqualid primitive_type_args { PPTtyapp ($2, $1) }
;
primitive_type_non_lident:
| primitive_type_arg_non_lident { $1 }
| uqualid DOT lident primitive_type_args { PPTtyapp ($4, Qdot ($1, $3)) }
;
primitive_type_args:
| primitive_type_arg { [$1] }
| primitive_type_arg primitive_type_args { $1 :: $2 }
;
primitive_type_arg:
| lident { PPTtyapp ([], Qident $1) }
| primitive_type_arg_non_lident { $1 }
;
primitive_type_arg_non_lident:
| uqualid DOT lident
{ PPTtyapp ([], Qdot ($1, $3)) }
| type_var
{ PPTtyvar $1 }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
{ PPTtuple ($2 :: $4) }
| LEFTPAR RIGHTPAR
{ PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
{ $2 }
;
list1_primitive_type_sep_comma:
| primitive_type { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;
type_var:
| QUOTE lident { $2 }
;
/* Logic expressions */
lexpr:
| lexpr ARROW lexpr
{ infix_pp $1 PPimplies $3 }
| lexpr LRARROW lexpr
{ infix_pp $1 PPiff $3 }
| lexpr OR lexpr
{ infix_pp $1 PPor $3 }
| lexpr BARBAR lexpr
{ mk_pp (PPnamed (Lstr Term.asym_label, infix_pp $1 PPor $3)) }
| lexpr AND lexpr
{ infix_pp $1 PPand $3 }
| lexpr AMPAMP lexpr
{ mk_pp (PPnamed (Lstr Term.asym_label, infix_pp $1 PPand $3)) }
| NOT lexpr
{ prefix_pp PPnot $2 }
| lexpr EQUAL lexpr
{ mk_l_infix $1 "=" $3 }
| lexpr LTGT lexpr
{ prefix_pp PPnot (mk_l_infix $1 "=" $3) }
| lexpr OP1 lexpr
{ mk_l_infix $1 $2 $3 }
| lexpr OP2 lexpr
{ mk_l_infix $1 $2 $3 }
| lexpr OP3 lexpr
{ mk_l_infix $1 $2 $3 }
| lexpr OP4 lexpr
{ mk_l_infix $1 $2 $3 }
| prefix_op lexpr %prec prec_prefix_op
{ mk_l_prefix $1 $2 }
| qualid list1_lexpr_arg
{ mk_pp (PPapp ($1, $2)) }
| IF lexpr THEN lexpr ELSE lexpr
{ mk_pp (PPif ($2, $4, $6)) }
| quant list1_param_var_sep_comma triggers DOT lexpr
{ mk_pp (PPquant ($1, $2, $3, $5)) }
| label lexpr %prec prec_named
{ mk_pp (PPnamed ($1, $2)) }
| LET pattern EQUAL lexpr IN lexpr
{ match $2.pat_desc with
| PPpvar id -> mk_pp (PPlet (id, $4, $6))
| _ -> mk_pp (PPmatch ($4, [$2, $6])) }
| MATCH lexpr WITH bar_ match_cases END
{ mk_pp (PPmatch ($2, $5)) }
| MATCH lexpr COMMA list1_lexpr_sep_comma WITH bar_ match_cases END
{ mk_pp (PPmatch (mk_pp (PPtuple ($2::$4)), $7)) }
| EPSILON lident labels COLON primitive_type DOT lexpr
{ mk_pp (PPeps (add_lab $2 $3, $5, $7)) }
| lexpr COLON primitive_type
{ mk_pp (PPcast ($1, $3)) }
| lexpr_arg
{ $1 }
;
list1_field_value:
| field_value { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;
field_value:
| lqualid EQUAL lexpr { $1, $3 }
;
list1_lexpr_arg:
| lexpr_arg { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
;
constant:
| INTEGER { Term.ConstInt $1 }
| FLOAT { Term.ConstReal $1 }
;
lexpr_arg:
| qualid { mk_pp (PPvar $1) }
| constant { mk_pp (PPconst $1) }
| TRUE { mk_pp PPtrue }
| FALSE { mk_pp PPfalse }
| OPPREF lexpr_arg { mk_l_prefix $1 $2 }
| lexpr_sub { $1 }
| QUOTE uident { mk_pp (PPvar (Qident (quote $2))) }
;
lexpr_dot:
| lqualid_copy { mk_pp (PPvar $1) }
| OPPREF lexpr_dot { mk_l_prefix $1 $2 }
| lexpr_sub { $1 }
;
lexpr_sub:
| lexpr_dot DOT lqualid_rich
{ mk_pp (PPapp ($3, [$1])) }
| LEFTPAR lexpr RIGHTPAR
{ $2 }