liquid-fixpoint-0.3.0.0: external/fixpoint/fixParse.mly
%{
module A = Ast
module So = A.Sort
module Sy = A.Symbol
module E = A.Expression
module P = A.Predicate
module H = A.Horn
module Su = A.Subst
module C = FixConstraint
module Co = Constants
open FixMisc.Ops
(*
*
%token <string> Tycon
| (capital)letdig* { Tycon (Lexing.lexeme lexbuf) }
| Tycon { So.t_app (So.tycon $1) [] }
| Tycon tyconargsne { So.t_app (So.tycon $1) $2 }
*)
(* | Id { So.t_ptr (So.Loc $1) }
(*
pExprs:
LPAREN RPAREN { [] }
| LPAREN expr RPAREN { [$2] }
| LPAREN exprsCommaNe RPAREN { $2 }
;
exprsCommaNe:
expr { [$1] }
| expr COMMA exprsCommaNe { $1 :: $3 }
;
*)
*)
let parse_error msg =
Errorline.error (symbol_start ()) msg
let create_qual name vv = Qualifier.create (Sy.of_string name) (Sy.of_string vv)
let set_ibind, get_ibind =
let bindt = Hashtbl.create 37 in
( (fun (i, x, t) -> Hashtbl.replace bindt i (x, t))
, (fun i -> try Hashtbl.find bindt i with Not_found -> assertf "Unknown binding: %d\n" i)
)
let env_of_ibindings is =
is |> FixMisc.sort_and_compact
|> FixMisc.map get_ibind
|> C.env_of_ordered_bindings
%}
%token <string> Id
%token <int> Num
%token <float> Real
%token <string> StringLit
%token TVAR
%token TAG ID
%token BEXP
%token TRUE FALSE
%token UNDERSCORE
%token LPAREN RPAREN LB RB LC RC
%token EQ NE GT GE LT LE UEQ UNE
%token AND OR NOT NOTWORD IMPL IFF IFFWORD FORALL SEMI COMMA COLON MID
%token EOF
%token MOD
%token PLUS
%token MINUS
%token TIMES
%token DIV
%token DOL QM DOT ASGN
%token OBJ REAL INT NUM PTR LFUN BOOL UNINT FUNC LIT FRAC
%token SRT AXM CON CST WF SOL QUL KUT BIND ADP DDP
%token ENV GRD LHS RHS REF
%right IFF IFFWORD
%right IMPL
%left PLUS
%left MINUS
%left DIV
%left TIMES
%left DOT
%right NOT
%start defs
%start sols
%start reft
%type <FixConfig.deft list> defs
%type <FixConfig.deft> def
%type <FixConfig.solbind list> sols
%type <So.t list> sorts, sortsne
%type <So.t> sort
%type <(Sy.t * So.t) list> binds, bindsne
%type <A.pred list> preds, predsne
%type <A.pred> pred
%type <A.expr list> exprs, exprsne
%type <A.expr> expr
%type <C.t> cstr
%type <C.envt> env
%type <FixConstraint.reft> reft
%type <C.refa list> refas, refasne
%type <C.refa> refa
%type <Su.t> subs
%%
defs:
{ [] }
| def defs { $1 :: $2 }
;
qual:
Id LPAREN Id COLON sort RPAREN COLON pred { create_qual $1 $3 $5 [] $8 }
| Id LPAREN Id RPAREN COLON pred { create_qual $1 $3 So.t_int [] $6 }
| Id LPAREN Id COLON sort qbindsne RPAREN COLON pred { create_qual $1 $3 $5 $6 $9 }
;
qbindsne:
COMMA bind { [$2] }
| COMMA bind qbindsne { $2 :: $3 }
;
def:
SRT COLON sort { FixConfig.Srt $3 }
| AXM COLON pred { FixConfig.Axm $3 }
| CST COLON cstr { FixConfig.Cst $3 }
| CON Id COLON sort { FixConfig.Con (Sy.of_string $2, $4) }
| WF COLON wf { FixConfig.Wfc $3 }
| sol { FixConfig.Sol $1 }
| QUL qual { FixConfig.Qul $2 }
| KUT kvid { FixConfig.Kut $2 }
| dep { FixConfig.Dep $1 }
| BIND Num Id COLON reft { let (i, x, r) = ($2, Sy.of_string $3, $5)
>> set_ibind
in FixConfig.IBind (i,x,r) }
;
sorts:
LB RB { [] }
| LB sortsne RB { $2 }
;
sortsne:
sort { [$1] }
| sort SEMI sortsne { $1 :: $3 }
;
tyconargsne:
| bsort { [$1] }
| bsort tyconargsne { $1 :: $2 }
;
sort:
| bsort { $1 }
| Id tyconargsne { So.t_app (So.tycon $1) $2 }
| LB sort RB { So.t_app (So.tycon "List") [$2] }
;
bsort:
| INT { So.t_int }
| REAL { So.t_real }
| BOOL { So.t_bool }
| PTR { So.t_ptr (So.Lvar 0) }
| PTR LPAREN LFUN RPAREN { So.t_ptr (So.LFun) }
| PTR LPAREN Num RPAREN { So.t_ptr (So.Lvar $3) }
| PTR LPAREN Id RPAREN { So.t_ptr (So.Loc $3) }
| OBJ { So.t_obj }
| NUM { So.t_num }
| FRAC { So.t_frac }
| TVAR LPAREN Num RPAREN { So.t_generic $3 }
| FUNC LPAREN sorts RPAREN { So.t_func 0 $3 }
| FUNC LPAREN Num COMMA sorts RPAREN { So.t_func $3 $5 }
| Id { let s = $1 in
if !Co.gen_qual_sorts || FixMisc.stringIsLower s then
So.t_ptr (So.Loc s) (* tyvar *)
else
So.t_app (So.tycon s) [] (* tycon *)
}
| LPAREN sort RPAREN { $2 }
| LB RB { So.t_app (So.tycon "List") [] }
;
binds:
LB RB { [] }
| LB bindsne RB { $2 }
;
bindsne:
bind { [$1] }
| bind SEMI bindsne { $1::$3 }
;
bind:
Id COLON sort { ((Sy.of_string $1), $3) }
;
rels:
LB RB { [] }
| LB relsne RB { $2 }
;
relsne:
rel { [$1]}
| rel SEMI relsne { $1 :: $3}
;
rel:
EQ { A.Eq }
| NE { A.Ne }
| UEQ { A.Ueq }
| UNE { A.Une }
| GT { A.Gt }
| GE { A.Ge }
| LT { A.Lt }
| LE { A.Le }
;
preds:
LB RB { [] }
| LB predsne RB { $2 }
;
predsne:
pred { [$1] }
| pred SEMI predsne { $1 :: $3 }
;
pred:
TRUE { A.pTrue }
| FALSE { A.pFalse }
| BEXP expr { A.pBexp $2 }
| QM expr { A.pBexp $2 }
| Id LPAREN argsne RPAREN { A.pBexp (A.eApp ((Sy.of_string $1), $3)) }
| AND preds { A.pAnd ($2) }
| OR preds { A.pOr ($2) }
| NOT pred { A.pNot ($2) }
| NOTWORD pred { A.pNot ($2) }
| LPAREN pred AND pred RPAREN { A.pAnd [$2; $4] }
| LPAREN pred OR pred RPAREN { A.pOr [$2; $4] }
| expr rel expr { A.pAtom ($1, $2, $3) }
| expr rels expr { A.pMAtom ($1, $2, $3) }
| FORALL binds DOT pred { A.pForall ($2, $4) }
| pred IMPL pred { A.pImp ($1, $3) }
| pred IFF pred { A.pIff ($1, $3) }
| pred IFFWORD pred { A.pIff ($1, $3) }
| LPAREN pred RPAREN { $2 }
;
argsne:
expr { [$1] }
| expr COMMA argsne { $1::$3 }
;
exprs:
LB RB { [] }
| LB exprsne RB { $2 }
;
exprsne:
expr { [$1] }
| expr SEMI exprsne { $1 :: $3 }
;
expr:
Id { A.eVar (Sy.of_string $1) }
| con { A.eCon $1 }
| exprs { A.eMExp $1 }
| LPAREN expr MOD expr RPAREN { A.eMod ($2, $4) }
| MINUS expr { A.eBin (A.zero, A.Minus, $2) }
| expr op expr { A.eBin ($1, $2, $3) }
| expr ops expr { A.eMBin ($1, $2, $3) }
| Id LPAREN exprs RPAREN { A.eApp ((Sy.of_string $1), $3) }
| Id Id { A.eApp ((Sy.of_string $1), [A.eVar (Sy.of_string $2)]) }
| LPAREN pred QM expr COLON expr RPAREN { A.eIte ($2,$4,$6) }
| expr DOT Id { A.eFld ((Sy.of_string $3), $1) }
| LPAREN expr COLON sort RPAREN { A.eCst ($2, $4) }
| LPAREN expr RPAREN { $2 }
;
op:
| PLUS { A.Plus }
| MINUS { A.Minus }
| TIMES { A.Times }
| DIV { A.Div }
;
ops:
LB RB { [] }
| LB opsne RB { $2 }
;
opsne:
op { [$1] }
| op SEMI opsne { $1 :: $3 }
;
con:
| Real { (A.Constant.Real $1) }
| Num { (A.Constant.Int $1) }
| MINUS Num { (A.Constant.Int (-1 * $2)) }
| MINUS Real { (A.Constant.Real (-. $2)) }
| LIT StringLit sort { (A.Constant.Lit ($2, $3)) }
;
cons:
LB RB { [] }
| LB consne RB { $2 }
;
consne:
con { [$1] }
| con SEMI consne { $1 :: $3 }
;
wf:
ENV env REF reft { C.make_wf $2 $4 None }
| ENV env REF reft ID Num { C.make_wf $2 $4 (Some $6) }
;
tagsne:
Num { [$1] }
| Num SEMI tagsne { $1 :: $3 }
;
tag:
| LB tagsne RB { ($2, "") }
;
dep:
| ADP COLON tag IMPL tag {C.make_dep true (Some $3) (Some $5) }
| DDP COLON tag IMPL tag {C.make_dep false (Some $3) (Some $5) }
| DDP COLON TIMES IMPL tag {C.make_dep false None (Some $5) }
| DDP COLON tag IMPL TIMES {C.make_dep false (Some $3) None }
;
info:
ID Num { ((Some $2), ([],"")) }
| TAG tag { (None , $2)}
| ID Num TAG tag { ((Some $2), $4) }
;
cstr:
| ENV env GRD pred LHS reft RHS reft { C.make_t $2 $4 $6 $8 None ([],"") }
| ENV env GRD pred LHS reft RHS reft info { C.make_t $2 $4 $6 $8 (fst $9) (snd $9)}
;
env:
LB RB { C.env_of_bindings [] }
| LB envne RB { C.env_of_bindings $2 }
| LB ienvne RB { env_of_ibindings $2 }
;
ienvne:
Num { [$1] }
| Num SEMI ienvne { $1 :: $3 }
;
envne:
rbind { [$1] }
| rbind SEMI envne { $1 :: $3 }
;
rbind:
Id COLON reft { (Sy.of_string $1, $3) }
;
ibind:
Num Id COLON reft { ($1, Sy.of_string $2, $4) }
;
reft:
LC Id COLON sort MID refas RC { ((Sy.of_string $2), $4, $6) }
;
refas:
LB RB { [] }
| LB refasne RB { $2 }
;
refasne:
refa { [$1] }
| refa SEMI refasne { $1 :: $3 }
;
kvid:
DOL Id { Sy.of_string $2 }
| Id { Sy.of_string $1 }
;
refa:
| kvid subs { C.Kvar ($2, $1) }
| pred { C.Conc $1 }
;
subs:
{ Su.empty }
| LB Id ASGN expr RB subs { Su.extend $6 ((Sy.of_string $2), $4) }
;
npred:
LPAREN pred COMMA Id LPAREN argsne RPAREN RPAREN { ((* $2, *) (Sy.of_string $4, $6)) }
;
npreds:
LB RB { [] }
| LB npredsne RB { $2 }
;
npredsne:
npred { [$1] }
| npred SEMI npredsne { $1 :: $3 }
;
sol:
SOL COLON Id ASGN npreds { ((Sy.of_string $3), $5) }
sols:
{ [] }
| sol sols { $1 :: $2 }