cime-terms.opp.exp 3.29 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201
%{

  open Gen_terms
  open Term_syntax
  open User_signatures
  open Finite_orderings

%}
%start equation_eof
%start equation_set_eof
%start order_constraint_eof
%start precedence_eof
%start rule_set_eof
%start status_eof
%start term_eof
%token <Variables.var_id> VAR_IDENT
%token SEMICOLON
%token RL_LEX
%token OPENPAR
%token MUL
%token LR_LEX
%token EOF
%token COMMA
%token CLOSEPAR
%token ARROW
%token OR
%token AND
%token NOT
%token NE
%token LT
%token LE
%token GT
%token GE
%token EQ
%token <string> INFIX_IDENT
%token <string> POSTFIX_IDENT
%token <string> PREFIX_IDENT
%left OR 
%left AND 
%nonassoc NOT 
%nonassoc NE LT LE GT GE EQ 
%left INFIX_IDENT 
%nonassoc POSTFIX_IDENT 
%nonassoc PREFIX_IDENT 
%type <(string Gen_terms.term * string Gen_terms.term)> equation_eof
%type <(string Gen_terms.term * string Gen_terms.term) list> equation_set_eof
%type <string Order_constraints.formula> order_constraint_eof
%type <string Finite_orderings.precedence list> precedence_eof
%type <(string Gen_terms.term * string Gen_terms.term) list> rule_set_eof
%type <(string * Rpo.rpo_status) list > status_eof
%type <string Gen_terms.term> term_eof
%%

term_eof:
| term EOF
    { $1 }

term:
| VAR_IDENT
    { make_var_term $1 }
| PREFIX_IDENT
    { !check_make_term $1 [] }
| PREFIX_IDENT term
    { !check_make_term $1 [$2] }
| PREFIX_IDENT OPENPAR term COMMA term_list CLOSEPAR %prec POSTFIX_IDENT
    { !check_make_term $1 ($3::$5) }
| term POSTFIX_IDENT
    { !check_make_term $2 [$1] }
| OPENPAR term COMMA term_list CLOSEPAR POSTFIX_IDENT
    { !check_make_term $6 ($2::$4) }
| term INFIX_IDENT term
    { !check_make_term $2 [$1;$3] }
| OPENPAR term CLOSEPAR
    { $2 }

term_list:
| term
    { [$1] }
| term COMMA term_list
    { $1 :: $3 }

equation_set_eof:
| equation_set EOF
    { $1 }

equation_set:
| 
    { []   }
| equation
    { [$1] }
| equation SEMICOLON equation_set
    { $1::$3 }

equation_eof:
| equation EOF
    { $1 }

equation:
| term EQ term
    { ($1,$3) }

rule_set_eof:
| rule_set EOF
    { $1 }

rule_set:
| 
    { []   }
| rule
    { [$1] }
| rule SEMICOLON rule_set
    { $1::$3 }

rule:
| term ARROW term
    { ($1,$3) }

order_constraint_eof:
| formula EOF
    { $1 }

formula:
| term comp term
    { Order_constraints.Atom($1,$2,$3) }
| formula AND formula
    { Order_constraints.conj $1 $3 }
| formula OR formula
    { Order_constraints.disj $1 $3 }
| NOT formula
    { Order_constraints.Not($2) }
| OPENPAR formula CLOSEPAR
    { $2 }

comp:
| EQ
    { Order_constraints.Eq }
| GT
    { Order_constraints.Gt }
| LT
    { Order_constraints.Lt }
| GE
    { Order_constraints.Ge }
| LE
    { Order_constraints.Le }
| NE
    { Order_constraints.Ne }

precedence_eof:
| precedence EOF
    { $1 }

precedence:
| 
    { [] }
| ordered_list
    { [$1] }
| ordered_list COMMA precedence
    { $1::$3 }

ordered_list:
| ident
    { One($1) }
| ident EQ ordered_list
    { Eq($1,$3) }
| ident GT ordered_list
    { Gt($1,$3) }
| ident LT ordered_list
    { Lt($1,$3) }

ident:
| PREFIX_IDENT
    { $1 }
| POSTFIX_IDENT
    { $1 }
| INFIX_IDENT
    { $1 }

status_eof:
| status EOF
    { $1 }

status:
| 
    { [] }
| symbol_status
    { [$1] }
| symbol_status SEMICOLON status
    { $1::$3 }

symbol_status:
| ident MUL
    { ($1,Rpo.Multiset) }
| ident LR_LEX
    { ($1,Rpo.Lr_lexico) }
| ident RL_LEX
    { ($1,Rpo.Rl_lexico) }

%%