Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merge typing of expressions and formulas #671

Merged
merged 1 commit into from
Dec 19, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
156 changes: 2 additions & 154 deletions src/ecParser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -39,21 +39,9 @@
in
try Some (nm, unloc name) with E.Invalid -> None

let mk_peid_symb loc s ti =
mk_loc loc (PEident (pqsymb_of_symb loc s, ti))

let mk_pfid_symb loc s ti =
mk_loc loc (PFident (pqsymb_of_symb loc s, ti))

let peapp_symb loc s ti es =
PEapp (mk_peid_symb loc s ti, es)

let peget loc ti e1 e2 =
peapp_symb loc EcCoreLib.s_get ti [e1;e2]

let peset loc ti e1 e2 e3 =
peapp_symb loc EcCoreLib.s_set ti [e1;e2;e3]

let pfapp_symb loc s ti es =
PFapp(mk_pfid_symb loc s ti, es)

Expand All @@ -63,15 +51,6 @@
let pfset loc ti e1 e2 e3 =
pfapp_symb loc EcCoreLib.s_set ti [e1;e2;e3]

let pe_nil loc ti =
mk_peid_symb loc EcCoreLib.s_nil ti

let pe_cons loc ti e1 e2 =
mk_loc loc (peapp_symb loc EcCoreLib.s_cons ti [e1; e2])

let pelist loc ti (es : pexpr list) : pexpr =
List.fold_right (fun e1 e2 -> pe_cons loc ti e1 e2) es (pe_nil loc ti)

let pf_nil loc ti =
mk_pfid_symb loc EcCoreLib.s_nil ti

Expand Down Expand Up @@ -917,139 +896,8 @@ tyvar_annot:
| LTCOLON k=loc(tyvar_annot) GT { k }

(* -------------------------------------------------------------------- *)
%inline sexpr: x=loc(sexpr_u) { x }
%inline expr: x=loc( expr_u) { x }

sexpr_u:
| e=sexpr PCENT p=uqident
{ PEscope (p, e) }

| e=sexpr p=loc(prefix(PCENT, _lident))
{ if unloc p = "top" then
PEscope (pqsymb_of_symb p.pl_loc "<top>", e)
else
let p = lmap (fun x -> "%" ^ x) p in
PEapp (mk_loc (loc p) (PEident (pqsymb_of_psymb p, None)), [e]) }

| LPAREN e=expr COLONTILD ty=loc(type_exp) RPAREN
{ PEcast (e, ty) }

| n=uint
{ PEint n }

| d=DECIMAL
{ PEdecimal d }

| x=qoident ti=tvars_app?
{ PEident (x, ti) }

| op=loc(numop) ti=tvars_app?
{ peapp_symb op.pl_loc op.pl_desc ti [] }

| se=sexpr DLBRACKET ti=tvars_app? e=loc(plist1(expr, COMMA)) RBRACKET
{ let e = List.reduce1 (fun _ -> lmap (fun x -> PEtuple x) e) (unloc e) in
peget (EcLocation.make $startpos $endpos) ti se e }

| se=sexpr DLBRACKET ti=tvars_app? e1=loc(plist1(expr, COMMA)) LARROW e2=expr RBRACKET
{ let e1 = List.reduce1 (fun _ -> lmap (fun x -> PEtuple x) e1) (unloc e1) in
peset (EcLocation.make $startpos $endpos) ti se e1 e2 }

| TICKPIPE ti=tvars_app? e=expr PIPE
{ peapp_symb e.pl_loc EcCoreLib.s_abs ti [e] }

| LBRACKET ti=tvars_app? es=loc(plist0(expr, SEMICOLON)) RBRACKET
{ unloc (pelist es.pl_loc ti es.pl_desc) }

| LBRACKET ti=tvars_app? e1=expr op=loc(DOTDOT) e2=expr RBRACKET
{ let id =
PEident (mk_loc op.pl_loc EcCoreLib.s_dinter, ti)
in
PEapp(mk_loc op.pl_loc id, [e1; e2]) }

| LPAREN es=plist0(expr, COMMA) RPAREN
{ PEtuple es }

| r=loc(RBOOL)
{ PEident (mk_loc r.pl_loc EcCoreLib.s_dbool, None) }

| LPBRACE fields=rlist1(expr_field, SEMICOLON) SEMICOLON? RPBRACE
{ PErecord (None, fields) }

| LPBRACE b=sexpr WITH fields=rlist1(expr_field, SEMICOLON) SEMICOLON? RPBRACE
{ PErecord (Some b, fields) }

| e=sexpr DOTTICK x=qident
{ PEproj (e, x) }

| e=sexpr DOTTICK n=loc(word)
{ if n.pl_desc = 0 then
parse_error n.pl_loc (Some "tuple projection start at 1");
PEproji(e,n.pl_desc - 1) }

expr_u:
| e=sexpr_u { e }

| e=sexpr args=sexpr+
{ PEapp (e, args) }

| op=loc(uniop) ti=tvars_app? e=expr
{ peapp_symb op.pl_loc op.pl_desc ti [e] }

| e=expr_chained_orderings %prec prec_below_order
{ fst e }

| e1=expr op=loc(binop) ti=tvars_app? e2=expr
{ peapp_symb op.pl_loc op.pl_desc ti [e1; e2] }

| c=expr QUESTION e1=expr COLON e2=expr %prec LOP2
{ PEif (c, e1, e2) }

| IF c=expr THEN e1=expr ELSE e2=expr
{ PEif (c, e1, e2) }

| MATCH e=expr WITH
PIPE? bs=plist0(p=mcptn(sbinop) IMPL be=expr { (p, be) }, PIPE)
END
{ PEmatch (e, bs) }

| LET p=lpattern EQ e1=expr IN e2=expr
{ PElet (p, (e1, None), e2) }

| LET p=lpattern COLON ty=loc(type_exp) EQ e1=expr IN e2=expr
{ PElet (p, (e1, Some ty), e2) }

| r=loc(RBOOL) TILD e=sexpr
{ let id = PEident(mk_loc r.pl_loc EcCoreLib.s_dbitstring, None) in
let loc = EcLocation.make $startpos $endpos in
PEapp (mk_loc loc id, [e]) }

| FUN pd=ptybindings IMPL e=expr
| FUN pd=ptybindings COMMA e=expr { PElambda (pd, e) }

| FORALL pd=ptybindings COMMA e=expr { PEforall (pd, e) }
| EXIST pd=ptybindings COMMA e=expr { PEexists (pd, e) }

expr_field:
| x=qident EQ e=expr
{ { rf_name = x ; rf_tvi = None; rf_value = e; } }

expr_ordering:
| e1=expr op=loc(ordering_op) ti=tvars_app? e2=expr
{ (op, ti, e1, e2) }

expr_chained_orderings:
| e=expr_ordering
{ let (op, ti, e1, e2) = e in
(peapp_symb op.pl_loc (unloc op) ti [e1; e2], e2) }

| e1=loc(expr_chained_orderings) op=loc(ordering_op) ti=tvars_app? e2=expr
{ let (lce1, (e1, le)) = (e1.pl_loc, unloc e1) in
let loc = EcLocation.make $startpos $endpos in
(peapp_symb loc "&&" None
[EcLocation.mk_loc lce1 e1;
EcLocation.mk_loc loc
(peapp_symb op.pl_loc (unloc op) ti [le; e2])],
e2) }
%inline sexpr: f=sform { mk_loc f.pl_loc (Expr f) }
%inline expr: f=form { mk_loc f.pl_loc (Expr f) }
strub marked this conversation as resolved.
Show resolved Hide resolved

(* -------------------------------------------------------------------- *)
bdident_:
Expand Down
80 changes: 31 additions & 49 deletions src/ecParsetree.ml
Original file line number Diff line number Diff line change
Expand Up @@ -65,60 +65,12 @@ type ppattern =
type ptybinding = osymbol list * pty
and ptybindings = ptybinding list

and pexpr_r =
| PEcast of pexpr * pty (* type cast *)
| PEint of zint (* int. literal *)
| PEdecimal of (zint * (int * zint)) (* dec. literal *)
| PEident of pqsymbol * ptyannot option (* symbol *)
| PEapp of pexpr * pexpr list (* op. application *)
| PElet of plpattern * pexpr_wty * pexpr (* let binding *)
| PEtuple of pexpr list (* tuple constructor *)
| PEif of pexpr * pexpr * pexpr (* _ ? _ : _ *)
| PEmatch of pexpr * (ppattern * pexpr) list (* match *)
| PEforall of ptybindings * pexpr (* forall quant. *)
| PEexists of ptybindings * pexpr (* exists quant. *)
| PElambda of ptybindings * pexpr (* lambda abstraction *)
| PErecord of pexpr option * pexpr rfield list (* record *)
| PEproj of pexpr * pqsymbol (* projection *)
| PEproji of pexpr * int (* tuple projection *)
| PEscope of pqsymbol * pexpr (* scope selection *)

and pexpr = pexpr_r located
and pexpr_wty = pexpr * pty option

and 'a rfield = {
rf_name : pqsymbol;
rf_tvi : ptyannot option;
rf_value : 'a;
}

(* -------------------------------------------------------------------- *)
type plvalue_r =
| PLvSymbol of pqsymbol
| PLvTuple of pqsymbol list
| PLvMap of pqsymbol * ptyannot option * pexpr list

and plvalue = plvalue_r located

type pinstr_r =
| PSident of psymbol
| PSasgn of plvalue * pexpr
| PSrnd of plvalue * pexpr
| PScall of plvalue option * pgamepath * (pexpr list) located
| PSif of pscond * pscond list * pstmt
| PSwhile of pscond
| PSmatch of pexpr * psmatch
| PSassert of pexpr

and psmatch = [
| `Full of (ppattern * pstmt) list
| `If of (ppattern * pstmt) * pstmt option
]

and pscond = pexpr * pstmt
and pinstr = pinstr_r located
and pstmt = pinstr list

(* -------------------------------------------------------------------- *)
type is_local = [ `Local | `Global]

Expand Down Expand Up @@ -170,7 +122,37 @@ type glob_or_var =
| GVglob of pmsymbol located * pqsymbol list
| GVvar of pqsymbol

type pformula = pformula_r located
(* -------------------------------------------------------------------- *)
type plvalue_r =
| PLvSymbol of pqsymbol
| PLvTuple of pqsymbol list
| PLvMap of pqsymbol * ptyannot option * pexpr list

and plvalue = plvalue_r located

and pinstr_r =
| PSident of psymbol
| PSasgn of plvalue * pexpr
| PSrnd of plvalue * pexpr
| PScall of plvalue option * pgamepath * (pexpr list) located
| PSif of pscond * pscond list * pstmt
| PSwhile of pscond
| PSmatch of pexpr * psmatch
| PSassert of pexpr

and psmatch = [
| `Full of (ppattern * pstmt) list
| `If of (ppattern * pstmt) * pstmt option
]

and pscond = pexpr * pstmt
and pinstr = pinstr_r located
and pstmt = pinstr list

and pexpr = pexpr_r located
and pexpr_r = Expr of pformula
strub marked this conversation as resolved.
Show resolved Hide resolved

and pformula = pformula_r located

and pformula_r =
| PFhole
Expand Down
Loading