From 44135941afd71321b08f2c47dfcc58c4f4803102 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Sun, 21 Mar 2010 17:19:41 +0000 Subject: [PATCH] parsing epsilon expressions --- src/parser/lexer.mll | 9 +------ src/parser/parser.mly | 60 +++++++++++++++++++------------------------ src/parser/ptree.mli | 2 +- src/parser/typing.ml | 17 +++++++++--- 4 files changed, 42 insertions(+), 46 deletions(-) diff --git a/src/parser/lexer.mll b/src/parser/lexer.mll index 71f7955c0..2bedc481a 100644 --- a/src/parser/lexer.mll +++ b/src/parser/lexer.mll @@ -49,6 +49,7 @@ "clone", CLONE; "else", ELSE; "end", END; + "epsilon", EPSILON; "exists", EXISTS; "export", EXPORT; "false", FALSE; @@ -161,8 +162,6 @@ rule token = parse { LEFTPAR } | ")" { RIGHTPAR } - | "!" - { BANG } | ":" { COLON } | "->" @@ -177,18 +176,12 @@ rule token = parse { OP2 (String.make 1 c) } | "*" | "/" | "%" as c { OP3 (String.make 1 c) } - | "@" - { AT } | "." { DOT } | "[" { LEFTSQ } | "]" { RIGHTSQ } - | "{" - { LEFTB } - | "}" - { RIGHTB } | "|" { BAR } | "\"" diff --git a/src/parser/parser.mly b/src/parser/parser.mly index 79537c6ad..c819acde7 100644 --- a/src/parser/parser.mly +++ b/src/parser/parser.mly @@ -54,25 +54,21 @@ /* keywords */ -%token AND AS AXIOM -%token CLONE -%token ELSE END EXISTS EXPORT FALSE FORALL -%token GOAL -%token IF IMPORT IN INDUCTIVE LEMMA -%token LET LOGIC MATCH -%token NAMESPACE NOT OR -%token THEN THEORY TRUE TYPE -%token USE WITH +%token AND AS AXIOM CLONE +%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL +%token GOAL IF IMPORT IN INDUCTIVE LEMMA +%token LET LOGIC MATCH NAMESPACE NOT OR +%token THEN THEORY TRUE TYPE USE WITH /* symbols */ -%token ARROW AT -%token BANG BAR +%token ARROW +%token BAR %token COLON COMMA %token DOT EQUAL -%token LEFTB LEFTPAR LEFTSQ +%token LEFTPAR LEFTSQ %token LRARROW -%token QUOTE RIGHTB +%token QUOTE %token RIGHTPAR RIGHTSQ %token UNDERSCORE @@ -81,30 +77,25 @@ /* Precedences */ -%left LEFTB - -%left COLON - -%left IN +%nonassoc prec_decls +%nonassoc LOGIC TYPE INDUCTIVE -%left ELSE +%nonassoc COLON +%nonassoc ELSE +%nonassoc IN +%nonassoc DOT -%right prec_named -%right prec_quant +%nonassoc prec_named %right ARROW LRARROW %right OR %right AND -%right NOT -%right prec_if +%nonassoc NOT %left EQUAL OP0 %left OP1 %left OP2 %left OP3 -%right unary_op -%left LEFTSQ - -%nonassoc prec_decls -%nonassoc LOGIC TYPE INDUCTIVE +%nonassoc prefix_op +%nonassoc postfix_op /* Entry points */ @@ -385,11 +376,11 @@ lexpr: | lexpr OP3 lexpr { let id = { id = infix $2; id_loc = loc_i 2 } in mk_pp (PPapp (Qident id, [$1; $3])) } -| any_op lexpr %prec unary_op +| any_op lexpr %prec prefix_op { let id = { id = prefix $1; id_loc = loc_i 2 } in mk_pp (PPapp (Qident id, [$2])) } /* -| lexpr any_op %prec unary_op +| lexpr any_op %prec postfix_op { let id = { id = postfix $2; id_loc = loc_i 2 } in mk_pp (PPapp (Qident id, [$1])) } */ @@ -397,11 +388,11 @@ lexpr: { mk_pp (PPvar $1) } | qualid LEFTPAR list1_lexpr_sep_comma RIGHTPAR { mk_pp (PPapp ($1, $3)) } -| IF lexpr THEN lexpr ELSE lexpr %prec prec_if +| IF lexpr THEN lexpr ELSE lexpr { mk_pp (PPif ($2, $4, $6)) } -| FORALL list1_uquant_sep_comma triggers DOT lexpr %prec prec_quant +| FORALL list1_uquant_sep_comma triggers DOT lexpr { mk_pp (PPquant (PPforall, $2, $3, $5)) } -| EXISTS list1_uquant_sep_comma triggers DOT lexpr %prec prec_quant +| EXISTS list1_uquant_sep_comma triggers DOT lexpr { mk_pp (PPquant (PPexists, $2, $3, $5)) } | INTEGER { mk_pp (PPconst (Term.ConstInt $1)) } @@ -419,6 +410,8 @@ lexpr: { mk_pp (PPlet ($2, $4, $6)) } | MATCH list1_lexpr_sep_comma WITH bar_ match_cases END { mk_pp (PPmatch ($2, $5)) } +| EPSILON lident COLON primitive_type DOT lexpr + { mk_pp (PPeps ($2, $4, $6)) } | lexpr COLON primitive_type { mk_pp (PPcast ($1, $3)) } ; @@ -449,6 +442,7 @@ pattern: | uqualid { mk_pat (PPpapp ($1, [])) } | uqualid LEFTPAR list1_pat_sep_comma RIGHTPAR { mk_pat (PPpapp ($1, $3)) } | pattern AS lident { mk_pat (PPpas ($1,$3)) } +| LEFTPAR pattern RIGHTPAR { $2 } ; triggers: diff --git a/src/parser/ptree.mli b/src/parser/ptree.mli index b6effd18d..2ef4da764 100644 --- a/src/parser/ptree.mli +++ b/src/parser/ptree.mli @@ -72,7 +72,7 @@ and pp_desc = | PPquant of pp_quant * uquant list * lexpr list list * lexpr | PPnamed of string * lexpr | PPlet of ident * lexpr * lexpr -(* | PPeps of ident * lexpr *) + | PPeps of ident * pty * lexpr | PPmatch of lexpr list * (pattern list * lexpr) list | PPcast of lexpr * pty diff --git a/src/parser/typing.ml b/src/parser/typing.ml index eafd6f9b9..21b7d6114 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -266,7 +266,7 @@ and dterm_node = | Tlet of dterm * string * dterm | Tmatch of dterm list * (dpattern list * dterm) list | Tnamed of string * dterm - | Teps of string * dfmla + | Teps of string * dty * dfmla and dfmla = | Fapp of lsymbol * dterm list @@ -413,6 +413,11 @@ and dterm_node loc env = function let ty = dty env ty in if not (unify e1.dt_ty ty) then term_expected_type ~loc e1.dt_ty ty; e1.dt_node, ty + | PPeps ({id=x}, ty, e1) -> + let ty = dty env ty in + let env = { env with dvars = Mstr.add x ty env.dvars } in + let e1 = dfmla env e1 in + Teps (x, ty, e1), ty | PPquant _ | PPif _ | PPprefix _ | PPinfix _ | PPfalse | PPtrue -> error ~loc TermExpected @@ -474,7 +479,7 @@ and dfmla env e = match e.pp_desc with Fnamed (x, f1) | PPvar x -> Fvar (snd (find_prop x env.uc)) - | PPconst _ | PPcast _ -> + | PPeps _ | PPconst _ | PPcast _ -> error ~loc:e.pp_loc PredicateExpected and dpat_list env tl pl = @@ -551,8 +556,12 @@ let rec term env t = match t.dt_node with | Tnamed (x, e1) -> let e1 = term env e1 in t_label_add x e1 - | Teps _ -> - assert false (*TODO*) + | Teps (x, ty, e1) -> + let ty = ty_of_dty ty in + let v = create_vsymbol (id_fresh x) ty in + let env = Mstr.add x v env in + let e1 = fmla env e1 in + t_eps v e1 and fmla env = function | Ftrue -> -- GitLab