Skip to content

Commit

Permalink
Merge typing of expressions and formulas
Browse files Browse the repository at this point in the history 
This is a step forward removing expressions from EasyCrypt.

This commit removes all parsing and typing code specific to
expressions. Expressions are now parsed as formulas, utilizing the
formula type checker instead of an expression-specific type
checker. If a formula does not represent a valid expression, it is the
type checker's responsibility to raise a meaningful error message.
  • Loading branch information
@strub
strub committed Dec 19, 2024
1 parent fd573d0 commit 13acf05
Show file tree
Hide file tree
Showing 5 changed files with 116 additions and 445 deletions.
156 changes: 2 additions & 154 deletions src/ecParser.mly
View file
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) }

(* -------------------------------------------------------------------- *)
bdident_:
Expand Down
80 changes: 31 additions & 49 deletions src/ecParsetree.ml
View file
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

and pformula = pformula_r located

and pformula_r =
| PFhole
Expand Down
Loading

0 comments on commit 13acf05

Please sign in to comment.