/*
Hermetica Mathematical Tool
Copyright 2009 Hermes T.
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 3 of the License, or
(at your option) any later version.
This program 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. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see .
*/
%{
#include
#include
#include
#include
#include
#include "global_strings.h"
#include "general.h"
#include "h_object.h"
#include "symbols.h"
#include "h_array.h"
#include "h_sequence.h"
#include "h_list.h"
#include "h_string.h"
#include "h_int.h"
#include "operator.h"
#include "pattern.h"
#include "namespace.h"
#include "atom.h"
#include "semtype.h"
#include "subexp.h"
#include "prototype.h"
#include "proof.h"
#include "justification.h"
#include "proofline.h"
#include "memheap.h"
#include "global_h_objects.h"
#include "pattern_walk.h"
#include "parserlib.h"
#include "scanner.h"
#define YYERROR_VERBOSE 1
#define YYENABLE_NLS 1
%}
%union {
char ch;
subexp *subexpression;
h_str *h_string;
h_int *h_number;
operator op;
quantifier qu;
h_list *list;
proofline *pline;
justification *just;
semantic_type *st;
atom *at;
prototype *prot;
pattern *pat;
proof *prf;
symbol_type symbol;
}
%token TOK_STRING TOK_OPENBRACKET TOK_CLOSEBRACKET TOK_OPENSETBRACKET TOK_CLOSESETBRACKET TOK_STICK TOK_COLON TOK_THEREEXISTS TOK_FORALL TOK_SELECTOR TOK_COMMA TOK_OPENSQUAREBRACKET TOK_CLOSESQUAREBRACKET TOK_UNKNOWN TOK_ESCREAM TOK_LAMBDA TOK_DEDUCTION TOK_VAR TOK_CONST TOK_NAMESPACE TOK_NUMSIGN TOK_USE TOK_WITH TOK_EQUALBYDEF TOK_DOT TOK_MACRO TOK_SEMICOLON
%token TOK_NUMBER
%token TOK_CHAR
%token TOK_EMBEDDEDJUST
%token TOK_TEMPLATESYMBOL
%right TOK_LOGICALEQUIVALENCE
%right TOK_IMPLIES
%left TOK_OR
%left TOK_AND
%left TOK_NOT
%right TOK_EQUALS TOK_LESSTHAN TOK_GREATERTHAN TOK_LESSTHANEQUALTO TOK_GREATERTHANEQUALTO TOK_SUPERSET TOK_NONSTRICTSUPERSET TOK_ELEMENTOF TOK_IDENTICAL TOK_SUBSET TOK_NONSTRICTSUBSET TOK_NEQ TOK_NNONSTRICTSUBSET TOK_NNONSTRICTSUPERSET TOK_NSUBSET TOK_NSUPERSET
%left TOK_UNION
%left TOK_INTERSECTION TOK_SETSUBTRACTION
%left TOK_CROSSPRODUCT
%left TOK_PLUS
%left TOK_TIMES TOK_DIV TOK_RINGOPERATOR
%left TOK_HYPHEN
%right TOK_EXPONENT
%right TOK_AT
%type op
%type unit subexp quantifierexp opexp funceval sequence listset pairset tuple lambdaexp
%type quantifier
%type ns_list subexplist atom_list semarglist semarglist2 subexplist2 prooflinelist pattern_list
%type proofline
%type justification usual_justification
%type semtype
%type atom tagged_atom untagged_atom
%type prototype proto_opexp
%type pattern patternunit
%type proof topnode
%glr-parser
%pure-parser
%locations
%%
topnode: proof
{
topnode=$1; //topnode has a refcount of 1 for being
//in memheap
//WE DO NOT! REF THE TOPNODE. DEAL WITH REFCOUNT
//INSTEAD IN proof_fromstring.
//There was an issue where this rule could
//actually fire twice in a single parse
//when there were syntax errors.
//THe result was uncollected garbage
}
;
proof: prooflinelist
{
h_array *linearray;
linearray=h_list_toarray($1,"");
set_pos_from_loc(&@1,(h_object *)linearray);
$$=proof_new(linearray);
UNREF(linearray);
MH_INSERT($$);
}
prooflinelist: proofline
{
$$=h_list_new();
h_list_append($$,(h_object *)$1);
MH_INSERT($$);
//MH_REMOVE($1);
}
| prooflinelist proofline
{
h_list_append($1,(h_object *)$2);
//MH_REMOVE($2);
$$=$1;
}
;
proofline: atom TOK_COLON subexplist TOK_DEDUCTION subexp justification TOK_SEMICOLON
{
//printf("%s\n", "starting parse rule");
h_array *searray=h_list_toarray($3,",");
$$=proofline_step_new($6,$1,searray,$5);
UNREF(searray);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
//MH_REMOVE($5);
//MH_REMOVE($6);
set_pos_from_loc(&@3,(h_object *)searray);
set_pos_from_loc(&@$,(h_object *)$$);
//printf("%s\n", "node parsed");
}
| atom TOK_COLON TOK_DEDUCTION subexp justification TOK_SEMICOLON
{
h_array *emptylist;
emptylist=h_array_new(",");
$$=proofline_step_new($5,$1,emptylist,$4);
UNREF(emptylist);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($4);
//MH_REMOVE($5);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_VAR semtype prototype TOK_SEMICOLON
{
$$=proofline_vardeclaration_new($2,$3);
MH_INSERT($$);
//MH_REMOVE($2);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
//printf("lt %d\n",$$->lt);
//printf("inserted into heap\n");
}
| TOK_CONST semtype prototype TOK_SEMICOLON
{
$$=proofline_constdeclaration_new($2,$3,0);
MH_INSERT($$);
//MH_REMOVE($2);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
//printf("lt %d\n",$$->lt);
//printf("inserted into heap\n");
}
| TOK_CONST semtype prototype TOK_EQUALBYDEF subexp TOK_SEMICOLON
{
$$=proofline_constdeclaration_new($2,$3,$5);
MH_INSERT($$);
//MH_REMOVE($2);
//MH_REMOVE($3);
//MH_REMOVE($5);
set_pos_from_loc(&@$,(h_object *)$$);
//printf("lt %d\n",$$->lt);
//printf("inserted into heap\n");
}
| TOK_USE TOK_NAMESPACE TOK_DOT ns_list TOK_WITH
{scan_pattern();} pattern TOK_SEMICOLON
{
h_array *ns_array;
ns_array=h_list_toarray($4,".");
set_pos_from_loc(&@4,(h_object *)ns_array);
$$=proofline_namespacedeclaration_new(ns_array,$7);
MH_INSERT($$);
if(all_macros_defined($7)){
namespace_stack_add_pattern(parser_ns_stack,$7,ns_array);
}
UNREF(ns_array);
//MH_REMOVE($3);
//MH_REMOVE($6);
set_pos_from_loc(&@$,(h_object *)$$);
scan_normal();
}
| TOK_USE TOK_NAMESPACE TOK_DOT TOK_WITH
{scan_pattern();} pattern TOK_SEMICOLON
{
$$=proofline_namespacedeclaration_new(ROOT_NS,$6);
MH_INSERT($$);
if(all_macros_defined($6)){
namespace_stack_add_pattern(parser_ns_stack,$6,ROOT_NS);
}
//MH_REMOVE($3);
//MH_REMOVE($6);
set_pos_from_loc(&@$,(h_object *)$$);
scan_normal();
}
| TOK_COLON subexplist TOK_DEDUCTION subexp justification TOK_SEMICOLON
{
//printf("%s\n", "starting parse rule");
h_array *searray=h_list_toarray($2,",");
$$=proofline_result_new($5,searray,$4);
UNREF(searray);
MH_INSERT($$);
//MH_REMOVE($3);
//MH_REMOVE($5);
//MH_REMOVE($6);
set_pos_from_loc(&@3,(h_object *)searray);
set_pos_from_loc(&@$,(h_object *)$$);
//printf("%s\n", "node parsed");
}
| TOK_COLON TOK_DEDUCTION subexp justification TOK_SEMICOLON
{
h_array *emptylist;
emptylist=h_array_new(",");
$$=proofline_result_new($4,emptylist,$3);
UNREF(emptylist);
MH_INSERT($$);
//MH_REMOVE($4);
//MH_REMOVE($5);
set_pos_from_loc(&@$,(h_object *)$$);
}
| error TOK_SEMICOLON
{
$$=proofline_parseerror_new();
MH_INSERT($$);
scan_normal();
yyerrok;
}
;
pattern: pattern_list
{
h_array *pat_array=h_list_toarray($1,"");
set_pos_from_loc(&@1,(h_object *)pat_array);
$$=pattern_adjunctionlist_new(pat_array);
UNREF(pat_array);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| pattern TOK_UNION pattern
{
$$=pattern_union_new($1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
pattern_list: pattern_list patternunit
{
h_list_append($1,(h_object *)$2);
$$=$1;
//MH_REMOVE($2);
set_pos_from_loc(&@$,(h_object *)$$);
}
| patternunit
{
$$=h_list_new();
h_list_append($$,(h_object *)$1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
patternunit: TOK_CHAR
{
$$=pattern_char_new($1);
MH_INSERT($$);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_MACRO
{
$$=pattern_macro_new($1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_OPENBRACKET pattern TOK_CLOSEBRACKET
{
$$=$2;
}
| patternunit TOK_PLUS
{
$$=pattern_kleeneplus_new($1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| patternunit TOK_TIMES
{
$$=pattern_kleenestar_new($1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
prototype: atom TOK_OPENBRACKET atom_list TOK_CLOSEBRACKET
{
h_array *at_array=h_list_toarray($3,",");
set_pos_from_loc(&@3,(h_object *)at_array);
$$=prototype_funceval_new($1,at_array);
UNREF(at_array);
MH_INSERT($$);
//MH_REMOVE($3);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom
{
$$=prototype_atom_new($1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| proto_opexp
;
proto_opexp: atom TOK_IMPLIES atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_IMPLIES,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_LESSTHAN atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_LESSTHAN,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_GREATERTHAN atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_GREATERTHAN,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_LESSTHANEQUALTO atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_LESSTHANEQUALTO,
$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_GREATERTHANEQUALTO atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_GREATERTHANEQUALTO,
$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_SUPERSET atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_SUPERSET,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_NONSTRICTSUPERSET atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_NONSTRICTSUPERSET,
$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_SUBSET atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_SUBSET,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_NONSTRICTSUBSET atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_NONSTRICTSUBSET,
$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_ELEMENTOF atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_ELEMENTOF,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_UNION atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_UNION,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_SETSUBTRACTION atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_SETSUBTRACTION,
$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_INTERSECTION atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_INTERSECTION,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_PLUS atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_PLUS,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_CROSSPRODUCT atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_CROSSPRODUCT,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_TIMES atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_TIMES,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_RINGOPERATOR atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_RINGOPERATOR,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_DIV atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_DIV,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_HYPHEN atom
{
$$=prototype_opexpunary_new(&@1,OPERATOR_HYPHEN,$2);
MH_INSERT($$);
//MH_REMOVE($2);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_AT atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_AT,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_EXPONENT atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_EXPONENT,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_LOGICALEQUIVALENCE atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_IFF,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_EQUALS atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_EQUALS,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_NEQ atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_NEQ,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_NNONSTRICTSUBSET atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_NNONSTRICTSUBSET,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_NNONSTRICTSUPERSET atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_NNONSTRICTSUPERSET,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_NSUBSET atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_NSUBSET,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom TOK_NSUPERSET atom
{
$$=prototype_opexpbinary_new(&@2,OPERATOR_NSUPERSET,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
semtype: TOK_NUMBER
{
char *tempstring;
if(h_int_cmp($1,binary_h_int[0])==0){
$$=semantic_type_atom_new(0);
//we can store the location if we have a new one.
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}else if(h_int_cmp($1,binary_h_int[1])==0){
$$=semantic_type_atom_new(1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}else{
$$=semantic_type_error_new();
set_pos_from_loc(&@$,(h_object *)$$);
MH_INSERT($$);
yyerror(&@$,static_string[78]);
YYERROR;
}
}
| semarglist2 TOK_IMPLIES semtype
{
h_array *semarray =h_list_toarray($1,",");
set_pos_from_loc(&@1,(h_object *)semarray);
$$=semantic_type_function_new($3,semarray);
UNREF(semarray);
MH_INSERT($$);
//MH_REMOVE($3);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_OPENBRACKET semtype TOK_CLOSEBRACKET
{
$$=$2;
}
| semtype TOK_IMPLIES semtype
{
h_array *argtypes=h_array_sized_new(1,",");
h_array_add(argtypes,(h_object *)$1);
$$=semantic_type_function_new($3,argtypes);
UNREF(argtypes);
//MH_REMOVE($1);
//MH_REMOVE($3);
MH_INSERT($$);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
semarglist2: TOK_OPENSQUAREBRACKET semarglist TOK_CLOSESQUAREBRACKET
{
$$=$2;
}
semarglist: semtype
{
$$=h_list_new();
h_list_append($$,(h_object *)$1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| semarglist TOK_COMMA semtype
{
$$=$1;
h_list_append($1,(h_object *)$3);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
ns_list: TOK_STRING
{
$$=h_list_new();
h_list_append($$,(h_object *)$1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| ns_list TOK_DOT TOK_STRING
{
h_list_append($1,(h_object *)$3);
$$=$1;
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
//refcounts remain same again...
}
;
justification: usual_justification
| TOK_EMBEDDEDJUST
;
usual_justification: TOK_STRING
{
//printf("%s\n", "starting parse rule for MP");
$$=justification_rule_new($1,0);
MH_INSERT($$);
//MH_REMOVE(
// (h_object *)$1);
set_pos_from_loc(&@$,(h_object *)$$);
//printf("%s\n", "ending parse rule for MP");
}
| TOK_STRING TOK_OPENBRACKET atom_list TOK_CLOSEBRACKET
{
h_array *at_array=h_list_toarray($3,",");
$$=justification_rule_new($1,at_array);
UNREF(at_array);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@3,(h_object *)at_array);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_OPENSETBRACKET setupstack1 proof TOK_CLOSESETBRACKET
{
$$=justification_compound_new($3,0,0);
MH_INSERT($$);
//MH_REMOVE($3);
namespace_stack_pop_top(parser_ns_stack);
parser_contexts_pushed--;
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_OPENSETBRACKET setupstack1 error TOK_CLOSESETBRACKET
{
$$=justification_error_new();
MH_INSERT($$);
namespace_stack_pop_top(parser_ns_stack);
parser_contexts_pushed--;
set_pos_from_loc(&@$,(h_object *)$$);
yyerrok;
}
| TOK_OPENSQUAREBRACKET setupstack2 proof TOK_CLOSESQUAREBRACKET
{
$$=justification_compound_new($3,1,0);
MH_INSERT($$);
//MH_REMOVE($3);
namespace_stack_pop_top(parser_ns_stack);
parser_contexts_pushed--;
set_pos_from_loc(&@$,(h_object *)$$);
namespace_stack_unset_boundary(parser_ns_stack);
}
| TOK_OPENSQUAREBRACKET setupstack2 error TOK_CLOSESQUAREBRACKET
{
$$=justification_error_new();
MH_INSERT($$);
namespace_stack_pop_top(parser_ns_stack);
parser_contexts_pushed--;
set_pos_from_loc(&@$,(h_object *)$$);
namespace_stack_unset_boundary(parser_ns_stack);
yyerrok;
}
;
setupstack1:
{
namespace_stack_push_new_context(parser_ns_stack);
parser_contexts_pushed++;
}
setupstack2: {
namespace_stack_set_boundary(parser_ns_stack);
namespace_stack_push_new_context(parser_ns_stack);
parser_contexts_pushed++;
}
subexp: quantifierexp
| opexp
| funceval
| sequence
| listset
| pairset
| tuple
| lambdaexp
| TOK_OPENBRACKET error TOK_CLOSEBRACKET
{
$$=subexp_error_new();
set_pos_from_loc(&@$,(h_object *)$$);
MH_INSERT($$);
yyerrok;
}
| TOK_OPENBRACKET subexp TOK_CLOSEBRACKET
{
$$=$2;
set_pos_from_loc(&@$,(h_object *)$$);
//this is important because we are changing
//the location info to match the brackets
}
| atom
{
$$=subexp_atom_new($1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
tuple: TOK_OPENBRACKET subexplist2 TOK_CLOSEBRACKET
{
h_array *searray=h_list_toarray($2,",");
set_pos_from_loc(&@2,(h_object *)searray);
$$=subexp_list_new(LIST_TUPLE,searray);
UNREF(searray);
MH_INSERT($$);
//MH_REMOVE($2);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
atom: untagged_atom
| tagged_atom
;
untagged_atom: TOK_NUMSIGN
{
h_array *namespace;
namespace=namespace_stack_get_numberclass(parser_ns_stack);
$$=atom_numberclass_new(namespace);
MH_INSERT($$);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_NUMBER
{
h_array *namespace;
namespace=namespace_stack_get_number(parser_ns_stack,$1);
$$=atom_number_new(namespace,$1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_STRING
{
h_array *namespace;
namespace=namespace_stack_get_name(parser_ns_stack,$1);
$$=atom_name_new(namespace,$1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
//printf("%s %d\n", "LINE IS",@1.first_line);
}
| TOK_OPENBRACKET op TOK_CLOSEBRACKET
{
h_array *namespace;
namespace=namespace_stack_get_operator(parser_ns_stack,$2);
$$=atom_operator_new(namespace,$2);
MH_INSERT($$);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_TEMPLATESYMBOL TOK_OPENBRACKET TOK_CLOSEBRACKET
{
$$=atom_template_new($1,NULL);
MH_INSERT($$);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_TEMPLATESYMBOL TOK_OPENBRACKET subexp TOK_CLOSEBRACKET
{
$$=atom_template_new($1,$3);
MH_INSERT($$);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
tagged_atom: TOK_DOT ns_list TOK_DOT TOK_NUMSIGN
{
h_array *ha=h_list_toarray($2,".");
set_pos_from_loc(&@2,(h_object *)ha);
$$=atom_numberclass_new(ha);
UNREF(ha);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_DOT TOK_NUMSIGN
{
$$=atom_numberclass_new(ROOT_NS);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_DOT ns_list TOK_DOT TOK_NUMBER
{
h_array *ha=h_list_toarray($2,".");
set_pos_from_loc(&@2,(h_object *)ha);
$$=atom_number_new(ha,$4);
UNREF(ha);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_DOT TOK_NUMBER
{
$$=atom_number_new(ROOT_NS,$2);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_DOT ns_list TOK_DOT TOK_STRING
{
h_array *ha=h_list_toarray($2,".");
set_pos_from_loc(&@2,(h_object *)ha);
$$=atom_name_new(ha,$4);
UNREF(ha);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_DOT TOK_STRING
{
$$=atom_name_new(ROOT_NS,$2);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_DOT ns_list TOK_DOT TOK_OPENBRACKET op TOK_CLOSEBRACKET
{
h_array *ha=h_list_toarray($2,".");
set_pos_from_loc(&@2,(h_object *)ha);
$$=atom_operator_new(ha,$5);
UNREF(ha);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_DOT TOK_OPENBRACKET op TOK_CLOSEBRACKET
{
$$=atom_operator_new(ROOT_NS,$3);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
op: TOK_IMPLIES
{
$$=OPERATOR_IMPLIES;
}
| TOK_OR
{
$$=OPERATOR_OR;
}
| TOK_AND
{
$$=OPERATOR_AND;
}
| TOK_NOT
{
$$=OPERATOR_NOT;
}
| TOK_LESSTHAN
{
$$=OPERATOR_LESSTHAN;
}
| TOK_GREATERTHAN
{
$$=OPERATOR_GREATERTHAN;
}
| TOK_LESSTHANEQUALTO
{
$$=OPERATOR_LESSTHANEQUALTO;
}
| TOK_GREATERTHANEQUALTO
{
$$=OPERATOR_GREATERTHANEQUALTO;
}
| TOK_SUPERSET
{
$$=OPERATOR_SUPERSET;
}
| TOK_SUBSET
{
$$=OPERATOR_SUBSET;
}
| TOK_NONSTRICTSUPERSET
{
$$=OPERATOR_NONSTRICTSUPERSET;
}
| TOK_NONSTRICTSUBSET
{
$$=OPERATOR_NONSTRICTSUBSET;
}
| TOK_ELEMENTOF
{
$$=OPERATOR_ELEMENTOF;
}
| TOK_UNION
{
$$=OPERATOR_UNION;
}
| TOK_SETSUBTRACTION
{
$$=OPERATOR_SETSUBTRACTION;
}
| TOK_INTERSECTION
{
$$=OPERATOR_INTERSECTION;
}
| TOK_PLUS
{
$$=OPERATOR_PLUS;
}
| TOK_CROSSPRODUCT
{
$$=OPERATOR_CROSSPRODUCT;
}
| TOK_TIMES
{
$$=OPERATOR_TIMES;
}
| TOK_RINGOPERATOR
{
$$=OPERATOR_RINGOPERATOR;
}
| TOK_DIV
{
$$=OPERATOR_DIV;
}
| TOK_AT
{
$$=OPERATOR_AT;
}
| TOK_EXPONENT
{
$$=OPERATOR_EXPONENT;
}
| TOK_HYPHEN
{
$$=OPERATOR_HYPHEN;
}
| TOK_LOGICALEQUIVALENCE
{
$$=OPERATOR_IFF;
}
| TOK_EQUALS
{
$$=OPERATOR_EQUALS;
}
| TOK_NEQ
{
$$=OPERATOR_NEQ;
}
| TOK_NNONSTRICTSUBSET
{
$$=OPERATOR_NNONSTRICTSUBSET;
}
| TOK_NNONSTRICTSUPERSET
{
$$=OPERATOR_NNONSTRICTSUPERSET;
}
| TOK_NSUBSET
{
$$=OPERATOR_NSUBSET;
}
| TOK_NSUPERSET
{
$$=OPERATOR_NSUPERSET;
}
;
quantifierexp: quantifier atom TOK_OPENBRACKET subexp TOK_CLOSEBRACKET
{
$$=subexp_quantifierexp_new($1,$2,$4);
MH_INSERT($$);
//MH_REMOVE($2);
//MH_REMOVE($4);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
lambdaexp: TOK_LAMBDA atom_list TOK_OPENBRACKET subexp TOK_CLOSEBRACKET
{
h_array *at_array=h_list_toarray($2,",");
set_pos_from_loc(&@2,(h_object *)at_array);
$$=subexp_lambdaexp_new(at_array,$4);
UNREF(at_array);
MH_INSERT($$);
//MH_REMOVE($2);
//MH_REMOVE($4);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
quantifier: TOK_FORALL
{
$$=QUANTIFIER_FORALL;
}
| TOK_THEREEXISTS
{
$$=QUANTIFIER_THEREEXISTS;
}
| TOK_SELECTOR
{
$$=QUANTIFIER_SELECTOR;
}
| TOK_ESCREAM
{
$$=QUANTIFIER_ESCREAM;
}
;
opexp: subexp TOK_LOGICALEQUIVALENCE subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_IFF,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_IMPLIES subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_IMPLIES,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_OR subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_OR,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_AND subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_AND,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_NOT subexp
{
$$=subexp_opexpunary_new(&@1,OPERATOR_NOT,$2);
MH_INSERT($$);
//MH_REMOVE($2);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_EQUALS subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_EQUALS,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_IDENTICAL subexp
{
$$=subexp_equivalence_new_with_loc(&@2,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_LESSTHAN subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_LESSTHAN,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_GREATERTHAN subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_GREATERTHAN,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_LESSTHANEQUALTO subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_LESSTHANEQUALTO,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_GREATERTHANEQUALTO subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_GREATERTHANEQUALTO,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_SUPERSET subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_SUPERSET,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_NONSTRICTSUPERSET subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_NONSTRICTSUPERSET,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_ELEMENTOF subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_ELEMENTOF,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_UNION subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_UNION,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_SETSUBTRACTION subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_SETSUBTRACTION,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_INTERSECTION subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_INTERSECTION,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_PLUS subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_PLUS,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_CROSSPRODUCT subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_CROSSPRODUCT,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_TIMES subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_TIMES,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_RINGOPERATOR subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_RINGOPERATOR,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_DIV subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_DIV,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_HYPHEN subexp
{
$$=subexp_opexpunary_new(&@1,OPERATOR_HYPHEN,$2);
MH_INSERT($$);
//MH_REMOVE($2);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_AT subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_AT,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_EXPONENT subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_EXPONENT,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_NEQ subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_NEQ,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_NNONSTRICTSUBSET subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_NNONSTRICTSUBSET,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_NNONSTRICTSUPERSET subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_NNONSTRICTSUPERSET,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_NONSTRICTSUBSET subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_NONSTRICTSUBSET,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_NSUBSET subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_NSUBSET,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexp TOK_NSUPERSET subexp
{
$$=subexp_opexpbinary_new(&@2,OPERATOR_NSUPERSET,$1,$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
funceval: unit TOK_OPENBRACKET subexplist TOK_CLOSEBRACKET
{
h_array *searray=h_list_toarray($3,",");
set_pos_from_loc(&@3,(h_object *)searray);
//position_pair pos_p;
//position *l_pos=&(pos_p.l_pos);
//position *r_pos=&(pos_p.r_pos);
//l_pos->address@hidden;
//l_pos->address@hidden;
//r_pos->address@hidden;
//r_pos->address@hidden;
//h_object_set_positions((h_object *)$3,&pos_p);
$$=subexp_funceval_new($1,searray);
UNREF(searray);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_OPENBRACKET subexp TOK_CLOSEBRACKET TOK_OPENBRACKET subexplist TOK_CLOSEBRACKET
{
pospair pp;
h_array *searray=h_list_toarray($5,",");
set_pos_from_loc(&@5,(h_object *)searray);
address@hidden;
address@hidden;
address@hidden;
address@hidden;
h_object_set_pospair((h_object *)$2,&pp);
$$=subexp_funceval_new($2,searray);
UNREF(searray);
MH_INSERT($$);
//MH_REMOVE($2);
//MH_REMOVE($5);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
unit: funceval
| sequence
| pairset
| listset
| quantifierexp
| tuple
| lambdaexp
| atom
{
$$=subexp_atom_new($1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
subexplist: subexp
{
$$=h_list_new();
h_list_append($$,(h_object *)$1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexplist TOK_COMMA subexp
{
h_list_append($1,(h_object *)$3);
//MH_REMOVE($3);
$$=$1;
set_pos_from_loc(&@$,(h_object *)$$);
}
;
subexplist2: subexp TOK_COMMA subexp
{
$$=h_list_new();
h_list_append($$,(h_object *)$1);
h_list_append($$,(h_object *)$3);
MH_INSERT($$);
//MH_REMOVE($1);
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
| subexplist2 TOK_COMMA subexp
{
h_list_append($1,(h_object *)$3);
//MH_REMOVE($3);
$$=$1;
set_pos_from_loc(&@$,(h_object *)$$);
}
;
atom_list: atom
{
$$=h_list_new();
h_list_append($$,(h_object *)$1);
MH_INSERT($$);
//MH_REMOVE($1);
set_pos_from_loc(&@$,(h_object *)$$);
}
| atom_list TOK_COMMA atom
{
h_list_append($1,(h_object *)$3);
$$=$1;
//MH_REMOVE($3);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
sequence: TOK_OPENSQUAREBRACKET subexplist TOK_CLOSESQUAREBRACKET
{
h_array *searray=h_list_toarray($2,",");
set_pos_from_loc(&@2,(h_object *)searray);
$$=subexp_list_new(LIST_SEQUENCE,searray);
UNREF(searray);
MH_INSERT($$);
//MH_REMOVE($2);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_OPENSQUAREBRACKET TOK_CLOSESQUAREBRACKET
{
h_array *emptylist=h_array_new(",");
$$=subexp_list_new(LIST_SEQUENCE,emptylist);
UNREF(emptylist);
MH_INSERT($$);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
listset: TOK_OPENSETBRACKET subexplist TOK_CLOSESETBRACKET
{
h_array *searray=h_list_toarray($2,",");
set_pos_from_loc(&@2,(h_object *)searray);
$$=subexp_list_new(LIST_SET,searray);
UNREF(searray);
MH_INSERT($$);
//MH_REMOVE($2);
set_pos_from_loc(&@$,(h_object *)$$);
}
| TOK_OPENSETBRACKET TOK_CLOSESETBRACKET
{
h_array *emptylist=h_array_new(",");
$$=subexp_list_new(LIST_SET,emptylist);
UNREF(emptylist);
MH_INSERT($$);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
pairset: TOK_OPENSETBRACKET atom TOK_STICK subexp TOK_CLOSESETBRACKET
{
$$=subexp_quantifierexp_new(QUANTIFIER_PAIRSET,$2,$4);
MH_INSERT($$);
//MH_REMOVE($2);
//MH_REMOVE($4);
set_pos_from_loc(&@$,(h_object *)$$);
}
;
%%