/*

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 <http://www.gnu.org/licenses/>.
*/


%{
#include <config.h>
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include <gtk/gtk.h>
#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 <h_string> 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 <h_number> TOK_NUMBER
%token <ch>TOK_CHAR
%token <just>TOK_EMBEDDEDJUST
%token <symbol>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>op
%type <subexpression> unit subexp quantifierexp opexp funceval sequence listset pairset tuple lambdaexp
%type <qu>quantifier
%type <list>ns_list subexplist atom_list semarglist semarglist2 subexplist2 prooflinelist pattern_list
%type <pline>proofline
%type <just>justification usual_justification
%type <st>semtype
%type <at>atom tagged_atom untagged_atom
%type <prot>prototype proto_opexp
%type <pat>pattern patternunit
%type <prf>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 *)$$);
             }
;



%%