Skip to content

Commit

Permalink
merge typing of expressions and formulas
Browse files Browse the repository at this point in the history
  • Loading branch information
@strub
strub committed Dec 16, 2024
1 parent 9eaff01 commit 9d716f0
Show file tree
Hide file tree
Showing 3 changed files with 63 additions and 410 deletions.
158 changes: 3 additions & 155 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 Expand Up @@ -3125,7 +2973,7 @@ interleave_info:
| UNROLL b=boption(FOR) s=side? o=codepos
{ Punroll (s, o, b) }

| SPLITWHILE s=side? o=codepos COLON c=expr %prec prec_tactic
| SPLITWHILE s=side? o=codepos COLON c=expr
{ Psplitwhile (c, s, o) }

| BYPHOARE info=gpterm(conseq)?
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 9d716f0

Please sign in to comment.