Commit 9ebe7ff1 authored by Andrei Paskevich's avatar Andrei Paskevich

Parser: distinguish "let f x = ..." from "let f = fun x -> ..."

parent b0bdadcd
......@@ -131,9 +131,7 @@ let d : pdecl =
let p = mk_lexpr (PPinfix(c6p7,mk_ident "infix =",c42)) in
mk_expr(Eassert(Aassert,p))
in
let triple = body, spec in
let lambda = mk_expr(Efun(args,triple)) in
Dlet(mk_ident "f",Gnone,lambda)
Dfun(mk_ident "f",Gnone,(args,None,body,spec))
let () =
try t.new_pdecl Loc.dummy_position d
......
......@@ -39,9 +39,6 @@ end
let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
let mk_pp d = mk_ppl (floc ()) d
(* dead code
let mk_pp_i i d = mk_ppl (floc_i i) d
*)
let mk_pat p = { pat_loc = floc (); pat_desc = p }
let infix_ppl loc a i b = mk_ppl loc (PPbinop (a, i, b))
......@@ -84,13 +81,8 @@ end
| _ -> raise exn)
let mk_expr d = { expr_loc = floc (); expr_desc = d }
let mk_expr_i i d = { expr_loc = floc_i i; expr_desc = d }
let cast_body c e = match c with
| Some pt -> { e with expr_desc = Ecast (e, pt) }
| None -> e
let rec mk_apply f a =
let mk_apply f a =
let loc = Loc.join f.expr_loc a.expr_loc in
{ expr_loc = loc; expr_desc = Eapply (f,a) }
......@@ -1089,13 +1081,13 @@ new_ns_mo:
pdecl:
| LET top_ghost lident_rich labels EQUAL fun_expr
{ Dlet (add_lab $3 $4, $2, $6) }
{ Dfun (add_lab $3 $4, $2, $6) }
| LET top_ghost lident_rich labels fun_defn
{ Dlet (add_lab $3 $4, $2, $5) }
{ Dfun (add_lab $3 $4, $2, $5) }
| LET REC list1_rec_defn
{ Dletrec $3 }
{ Drec $3 }
| VAL top_ghost lident_rich labels type_v
{ Dparam (add_lab $3 $4, $2, $5) }
{ Dval (add_lab $3 $4, $2, $5) }
| EXCEPTION uident labels
{ Dexn (add_lab $2 $3, ty_unit ()) }
| EXCEPTION uident labels primitive_type
......@@ -1139,17 +1131,17 @@ list1_rec_defn:
rec_defn:
| top_ghost lident_rich labels list1_binder opt_cast spec EQUAL spec expr
{ floc (), add_lab $2 $3, $1, $4, (cast_body $5 $9, spec_union $6 $8) }
{ add_lab $2 $3, $1, ($4, $5, $9, spec_union $6 $8) }
;
fun_defn:
| list1_binder opt_cast spec EQUAL spec expr
{ mk_expr_i 6 (Efun ($1, (cast_body $2 $6, spec_union $3 $5))) }
{ ($1, $2, $6, spec_union $3 $5) }
;
fun_expr:
| FUN list1_binder spec ARROW spec expr %prec prec_fun
{ mk_expr (Efun ($2, ($6, spec_union $3 $5))) }
{ ($2, None, $6, spec_union $3 $5) }
;
expr:
......@@ -1210,13 +1202,13 @@ expr:
{ $5 with expr_desc = Ecast ($5, PPTtuple []) }, $7))
| _ -> mk_expr (Ematch ({ $5 with expr_desc = Eghost $5 }, [$3, $7])) }
| LET lident labels fun_defn IN expr
{ mk_expr (Elet (add_lab $2 $3, Gnone, $4, $6)) }
{ mk_expr (Efun (add_lab $2 $3, Gnone, $4, $6)) }
| LET lident_op_id labels fun_defn IN expr
{ mk_expr (Elet (add_lab $2 $3, Gnone, $4, $6)) }
{ mk_expr (Efun (add_lab $2 $3, Gnone, $4, $6)) }
| LET GHOST lident labels fun_defn IN expr
{ mk_expr (Elet (add_lab $3 $4, Gghost, $5, $7)) }
{ mk_expr (Efun (add_lab $3 $4, Gghost, $5, $7)) }
| LET GHOST lident_op_id labels fun_defn IN expr
{ mk_expr (Elet (add_lab $3 $4, Gghost, $5, $7)) }
{ mk_expr (Efun (add_lab $3 $4, Gghost, $5, $7)) }
| LET lident_op_id labels EQUAL expr IN expr
{ mk_expr (Elet (add_lab $2 $3, Gnone, $5, $7)) }
| LET GHOST lident_op_id labels EQUAL expr IN expr
......@@ -1224,11 +1216,11 @@ expr:
| LET LEMMA lident_rich labels EQUAL expr IN expr
{ mk_expr (Elet (add_lab $3 $4, Glemma, $6, $8)) }
| LET LEMMA lident_rich labels fun_defn IN expr
{ mk_expr (Elet (add_lab $3 $4, Glemma, $5, $7)) }
{ mk_expr (Efun (add_lab $3 $4, Glemma, $5, $7)) }
| LET REC list1_rec_defn IN expr
{ mk_expr (Eletrec ($3, $5)) }
{ mk_expr (Erec ($3, $5)) }
| fun_expr
{ $1 }
{ mk_expr (Elam $1) }
| MATCH expr WITH bar_ program_match_cases END
{ mk_expr (Ematch ($2, $5)) }
| MATCH expr COMMA list1_expr_sep_comma WITH bar_ program_match_cases END
......
......@@ -222,9 +222,10 @@ and expr_desc =
| Eapply of expr * expr
| Einfix of expr * ident * expr
| Einnfix of expr * ident * expr
| Efun of binder list * triple
| Elet of ident * top_ghost * expr * expr
| Eletrec of letrec list * expr
| Efun of ident * top_ghost * lambda * expr
| Erec of fundef list * expr
| Elam of lambda
| Etuple of expr list
| Erecord of (qualid * expr) list
| Eupdate of expr * (qualid * expr) list
......@@ -246,17 +247,18 @@ and expr_desc =
| Ecast of expr * pty
| Eany of type_c
| Eghost of expr
| Eabstract of triple
| Eabstract of expr * spec
| Enamed of label * expr
and letrec = loc * ident * top_ghost * binder list * triple
and fundef = ident * top_ghost * lambda
and triple = expr * spec
and lambda = binder list * pty option * expr * spec
type pdecl =
| Dval of ident * top_ghost * type_v
| Dlet of ident * top_ghost * expr
| Dletrec of letrec list
| Dparam of ident * top_ghost * type_v
| Dfun of ident * top_ghost * lambda
| Drec of fundef list
| Dexn of ident * pty
(* incremental parsing *)
......
......@@ -553,13 +553,22 @@ and de_desc denv loc = function
| _ -> add_mono id e1.de_type denv in
let e2 = dexpr denv e2 in
DElet (id, gh, e1, e2), e2.de_type
| Ptree.Eletrec (fdl, e1) ->
| Ptree.Efun (id, gh, lam, e2) ->
let id, gh = add_lemma_label ~top:false id gh in
let e1 = dexpr denv {expr_desc = Ptree.Elam lam; expr_loc = id.id_loc} in
let denv = add_poly id e1.de_type denv in
let e2 = dexpr denv e2 in
DElet (id, gh, e1, e2), e2.de_type
| Ptree.Erec (fdl, e1) ->
let fdl = dletrec ~top:false denv fdl in
let add_one denv (id,_,dvty,_,_) = add_poly id dvty denv in
let denv = List.fold_left add_one denv fdl in
let e1 = dexpr denv e1 in
DEletrec (fdl, e1), e1.de_type
| Ptree.Efun (bl, tr) ->
| Ptree.Elam (bl, pty, e1, sp) ->
let tr = match pty with
| Some pty -> { e1 with expr_desc = Ptree.Ecast (e1, pty) }, sp
| None -> e1, sp in
let denv, bl, tyl = dbinders denv (pass_opacity tr bl) in
let tr, (argl, res) = dtriple denv tr in
DEfun (bl, tr), (tyl @ argl, res)
......@@ -727,9 +736,8 @@ and de_desc denv loc = function
and dletrec ~top denv fdl =
let tvars = denv.tvars in
(* add all functions into the environment *)
let add_one denv (_,id,_,bl,tr) =
let _,argl,tyl = dbinders denv (pass_opacity tr bl) in
let rpty = find_top_pty (fst tr) in
let add_one denv (id,_,(bl,rpty,_,_)) =
let _,argl,tyl = dbinders denv bl in
let dvty = tyl, match rpty with
| Some pty -> dity_of_pty denv pty
| None -> create_type_variable () in
......@@ -740,18 +748,21 @@ and dletrec ~top denv fdl =
denv, (argl, dvty, freetvs) in
let denv, dvtyl = Lists.map_fold_left add_one denv fdl in
(* then type-check the bodies *)
let type_one (loc,id,gh,bl,tr) (argl,((tyl,tyv) as dvty),freetvs) =
let type_one (id,gh,(bl,pty,e1,sp)) (argl,((tyl,tyv) as dvty),freetvs) =
let tr = match pty with
| Some pty -> { e1 with expr_desc = Ptree.Ecast (e1, pty) }, sp
| None -> e1, sp in
let add denv (_,id,_,_) dity = match id with
| Some id -> add_var id dity denv
| None -> denv in
let denv = List.fold_left2 add denv bl tyl in
let id, gh = add_lemma_label ~top id gh in
let tr, (badl, res) = dtriple denv tr in
if badl <> [] then Loc.errorm ~loc
if badl <> [] then Loc.errorm ~loc:e1.expr_loc
"The body of a recursive function must be a first-order value";
unify_loc unify loc tyv res;
unify_loc unify e1.expr_loc tyv res;
let freenow = free_user_vars tvars dvty in
if not (Stv.subset freetvs freenow) then Loc.errorm ~loc
if not (Stv.subset freetvs freenow) then Loc.errorm ~loc:e1.expr_loc
"This function is expected to be polymorphic in type variable %a"
Pretty.print_tv (Stv.choose (Stv.diff freetvs freenow));
id, gh, dvty, argl, tr in
......@@ -1942,7 +1953,18 @@ let add_pdecl ~wp loc uc = function
let def = create_let_defn (Typing.create_user_id id) e in
create_let_decl def in
add_pdecl_with_tuples ~wp uc pd
| Dletrec fdl ->
| Dfun (id, gh, lam) ->
let id, gh = add_lemma_label ~top:true id gh in
let e = {expr_desc = Ptree.Elam lam; expr_loc = loc} in
let e = dexpr (create_denv uc) e in
let uc = flush_tuples uc in
let pd = match e.de_desc with
| DEfun (bl, tr) ->
let fd = expr_fun (create_lenv uc) id gh bl tr in
create_rec_decl [fd]
| _ -> assert false in
add_pdecl_with_tuples ~wp uc pd
| Drec fdl ->
let fdl = dletrec ~top:true (create_denv uc) fdl in
let uc = flush_tuples uc in
let fdl = expr_rec (create_lenv uc) fdl in
......@@ -1953,7 +1975,7 @@ let add_pdecl ~wp loc uc = function
let xs = create_xsymbol (Typing.create_user_id id) ity in
let pd = create_exn_decl xs in
add_pdecl_with_tuples ~wp uc pd
| Dparam (id, gh, tyv) ->
| Dval (id, gh, tyv) ->
let id, gh = add_lemma_label ~top:true id gh in
let tyv, _ = dtype_v (create_denv uc) tyv in
let uc = flush_tuples uc in
......
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