Commit 3c6c998a authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

accept "\!" and "\?" as function and predicate lambdas

parent a78ff7cc
......@@ -1034,7 +1034,7 @@ let f_neq t1 t2 = f_not (f_app ps_equ [t1; t2])
let fs_func_app =
let ty_a = ty_var (create_tvsymbol (id_fresh "a")) in
let ty_b = ty_var (create_tvsymbol (id_fresh "b")) in
create_fsymbol (id_fresh "infix @") [ty_func ty_a ty_b; ty_a] ty_b
create_fsymbol (id_fresh "infix @!") [ty_func ty_a ty_b; ty_a] ty_b
let ps_pred_app =
let ty_a = ty_var (create_tvsymbol (id_fresh "a")) in
......
......@@ -191,6 +191,10 @@ rule token = parse
{ ASYM_OR }
| "\\"
{ LAMBDA }
| "\\?"
{ PRED }
| "\\!"
{ FUNC }
| "."
{ DOT }
| "|"
......
......@@ -104,7 +104,7 @@
%token AND AS AXIOM CLONE
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL
%token GOAL IF IMPORT IN INDUCTIVE LAMBDA LEMMA
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET LOGIC MATCH META NAMESPACE NOT PROP OR
%token THEN THEORY TRUE TYPE USE WITH
......@@ -113,10 +113,10 @@
%token ARROW ASYM_AND ASYM_OR
%token BACKQUOTE BAR
%token COLON COMMA
%token DOT EQUAL LTGT
%token DOT EQUAL FUNC LAMBDA LTGT
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
%token LRARROW
%token QUOTE
%token PRED QUOTE
%token RIGHTPAR RIGHTSQ
%token UNDERSCORE
......@@ -495,6 +495,8 @@ quant:
| FORALL { PPforall }
| EXISTS { PPexists }
| LAMBDA { PPlambda }
| FUNC { PPfunc }
| PRED { PPpred }
;
/* Triggers */
......
......@@ -28,7 +28,7 @@ type constant = Term.constant
type label = Ident.label
type pp_quant =
| PPforall | PPexists | PPlambda
| PPforall | PPexists | PPlambda | PPfunc | PPpred
type pp_binop =
| PPand | PPor | PPimplies | PPiff
......
......@@ -440,7 +440,7 @@ and dterm_node loc env = function
let env = { env with dvars = Mstr.add x.id ty env.dvars } in
let e1 = dfmla env e1 in
Teps (x, ty, e1), ty
| PPquant (PPlambda, uqu, trl, a) ->
| PPquant ((PPlambda|PPfunc|PPpred) as q, uqu, trl, a) ->
check_quant_linearity uqu;
let uquant env (idl,ty) =
let ty = dty env ty in
......@@ -458,7 +458,13 @@ and dterm_node loc env = function
TRfmla (dfmla env e)
in
let trl = List.map (List.map trigger) trl in
let id, ty, f = match trigger a with
let e = match q with
| PPfunc -> TRterm (dterm env a)
| PPpred -> TRfmla (dfmla env a)
| PPlambda -> trigger a
| _ -> assert false
in
let id, ty, f = match e with
| TRterm t ->
let id = { id = "fc"; id_lab = []; id_loc = loc } in
let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment