Commit 75a68951 authored by Andrei Paskevich's avatar Andrei Paskevich

Dterm, Dexpr: binary functional appplcation

Finally, it is simpler to treat "higher-order" applications
in Dterm and Dexpr, since we can analyze the dtypes.
parent 5b04269b
......@@ -161,6 +161,7 @@ and dterm_node =
| DTgvar of vsymbol
| DTconst of Number.constant
| DTapp of lsymbol * dterm list
| DTfapp of dterm * dterm
| DTif of dterm * dterm * dterm
| DTlet of dterm * preid * dterm
| DTcase of dterm * (dpattern * dterm) list
......@@ -280,6 +281,11 @@ let dterm ?loc node =
let dtyl, dty = specialize_ls ls in
dty_unify_app ls dterm_expected_type dtl dtyl;
dty
| DTfapp (dt1,dt2) ->
let dtyl, dty = specialize_ls fs_func_app in
(* TODO: better error messages based on dt1 *)
dty_unify_app fs_func_app dterm_expected_type [dt1;dt2] dtyl;
dty
| DTif (df,dt1,dt2) ->
dfmla_expected_type df;
dexpr_expected_type dt2 dt1.dt_dty;
......@@ -436,6 +442,8 @@ and try_term strict keep_loc uloc env prop dty node =
| DTapp (ls,dtl) ->
t_app ls (List.map (get env false) dtl)
(Opt.map (term_ty_of_dty ~strict) dty)
| DTfapp (dt1,dt2) ->
t_func_app (get env false dt1) (get env false dt2)
| DTlet (dt,id,df) ->
let prop = prop || dty = None in
let t = get env false dt in
......
......@@ -49,6 +49,7 @@ and dterm_node =
| DTgvar of vsymbol
| DTconst of Number.constant
| DTapp of lsymbol * dterm list
| DTfapp of dterm * dterm
| DTif of dterm * dterm * dterm
| DTlet of dterm * preid * dterm
| DTcase of dterm * (dpattern * dterm) list
......
......@@ -191,38 +191,41 @@ let chainable_op uc op =
type global_vs = Ptree.qualid -> vsymbol option
let rec dterm uc (gvars: global_vs) denv {pp_desc = desc; pp_loc = loc} =
let pterm denv pp = dterm uc gvars denv pp in
let highord_app e1 e2 =
DTapp (fs_func_app, [Dterm.dterm ~loc e1; pterm denv e2]) in
let highord_app e1 el = List.fold_left highord_app e1 el in
let qualid_app q el = match gvars q with
let rec dterm uc gvars denv {pp_desc = desc; pp_loc = loc} =
let func_app loc e el =
let app (loc, e) e1 = Loc.join loc e1.pp_loc,
DTfapp (Dterm.dterm ~loc e, dterm uc gvars denv e1) in
snd (List.fold_left app (loc, e) el)
in
let rec take loc al l el = match l, el with
| (_::l), (e::el) ->
take (Loc.join loc e.pp_loc) (dterm uc gvars denv e :: al) l el
| _, _ -> loc, List.rev al, el
in
let qualid_app loc q el = match gvars q with
| Some vs ->
highord_app (DTgvar vs) el
func_app loc (DTgvar vs) el
| None ->
let ls = find_lsymbol uc q in
let rec take al l el = match l, el with
| (_::l), (e::el) -> take (pterm denv e :: al) l el
| _, _ -> List.rev al, el in
let al, el = take [] ls.ls_args el in
highord_app (DTapp (ls,al)) el
let loc, al, el = take loc [] ls.ls_args el in
func_app loc (DTapp (ls,al)) el
in
let qualid_app q el = match q with
let qualid_app loc q el = match q with
| Qident {id = n} ->
(match denv_get_opt denv n with
| Some dt -> highord_app dt el
| None -> qualid_app q el)
| _ -> qualid_app q el
| Some d -> func_app loc d el
| None -> qualid_app loc q el)
| _ -> qualid_app loc q el
in
Dterm.dterm ~loc (match desc with
| PPvar x ->
qualid_app x []
| PPapp (x, tl) ->
qualid_app x tl
| PPvar q ->
qualid_app loc q []
| PPapp (q, tl) ->
qualid_app (qloc q) q tl
| PPhoapp (e1, e2) ->
DTapp (fs_func_app, [pterm denv e1; pterm denv e2])
DTfapp (dterm uc gvars denv e1, dterm uc gvars denv e2)
| PPtuple tl ->
let tl = List.map (pterm denv) tl in
let tl = List.map (dterm uc gvars denv) tl in
DTapp (fs_tuple (List.length tl), tl)
| PPinfix (e12, op2, e3)
| PPinnfix (e12, op2, e3) ->
......@@ -243,41 +246,41 @@ let rec dterm uc (gvars: global_vs) denv {pp_desc = desc; pp_loc = loc} =
| [] -> assert false in
let rec get_chain e12 acc = match e12.pp_desc with
| PPinfix (e1, op1, e2) when chainable_op uc op1 ->
get_chain e1 ((op1, pterm denv e2) :: acc)
get_chain e1 ((op1, dterm uc gvars denv e2) :: acc)
| _ -> e12, acc in
let ch = [op2, pterm denv e3] in
let ch = [op2, dterm uc gvars denv e3] in
let e1, ch = if chainable_op uc op2
then get_chain e12 ch else e12, ch in
make_chain (pterm denv e1) ch
make_chain (dterm uc gvars denv e1) ch
| PPconst c ->
DTconst c
| PPlet (x, e1, e2) ->
let id = create_user_id x in
let e1 = pterm denv e1 in
let e1 = dterm uc gvars denv e1 in
let denv = denv_add_let denv e1 id in
let e2 = pterm denv e2 in
let e2 = dterm uc gvars denv e2 in
DTlet (e1, id, e2)
| PPmatch (e1, bl) ->
let e1 = pterm denv e1 in
let e1 = dterm uc gvars denv e1 in
let branch (p, e) =
let p = dpattern uc p in
let denv = denv_add_pat denv p in
p, pterm denv e in
p, dterm uc gvars denv e in
DTcase (e1, List.map branch bl)
| PPif (e1, e2, e3) ->
let e1 = pterm denv e1 in
let e2 = pterm denv e2 in
let e3 = pterm denv e3 in
let e1 = dterm uc gvars denv e1 in
let e2 = dterm uc gvars denv e2 in
let e3 = dterm uc gvars denv e3 in
DTif (e1, e2, e3)
| PPtrue ->
DTtrue
| PPfalse ->
DTfalse
| PPunop (PPnot, e1) ->
DTnot (pterm denv e1)
DTnot (dterm uc gvars denv e1)
| PPbinop (e1, op, e2) ->
let e1 = pterm denv e1 in
let e2 = pterm denv e2 in
let e1 = dterm uc gvars denv e1 in
let e2 = dterm uc gvars denv e2 in
let op = match op with
| PPand -> Tand
| PPor -> Tor
......@@ -287,8 +290,9 @@ let rec dterm uc (gvars: global_vs) denv {pp_desc = desc; pp_loc = loc} =
| PPquant (q, uqu, trl, e1) ->
let qvl = List.map (quant_var uc) uqu in
let denv = denv_add_quant denv qvl in
let trl = List.map (List.map (pterm denv)) trl in
let e1 = pterm denv e1 in
let dterm e = dterm uc gvars denv e in
let trl = List.map (List.map dterm) trl in
let e1 = dterm e1 in
begin match q with
| PPforall -> DTquant (Tforall, qvl, trl, e1)
| PPexists -> DTquant (Texists, qvl, trl, e1)
......@@ -304,23 +308,23 @@ let rec dterm uc (gvars: global_vs) denv {pp_desc = desc; pp_loc = loc} =
end
| PPrecord fl ->
let get_val cs pj = function
| Some e -> pterm denv e
| Some e -> dterm uc gvars denv e
| None -> Loc.error ~loc (RecordFieldMissing (cs,pj)) in
let cs, fl = parse_record ~loc uc get_val fl in
DTapp (cs, fl)
| PPupdate (e1, fl) ->
let e1 = pterm denv e1 in
let e1 = dterm uc gvars denv e1 in
let get_val _ pj = function
| Some e -> pterm denv e
| Some e -> dterm uc gvars denv e
| None -> Dterm.dterm ~loc (DTapp (pj,[e1])) in
let cs, fl = parse_record ~loc uc get_val fl in
DTapp (cs, fl)
| PPnamed (Lpos uloc, e1) ->
DTuloc (pterm denv e1, uloc)
DTuloc (dterm uc gvars denv e1, uloc)
| PPnamed (Lstr lab, e1) ->
DTlabel (pterm denv e1, Slab.singleton lab)
DTlabel (dterm uc gvars denv e1, Slab.singleton lab)
| PPcast (e1, ty) ->
DTcast (pterm denv e1, ty_of_pty uc ty))
DTcast (dterm uc gvars denv e1, ty_of_pty uc ty))
(** Export for program parsing *)
......
......@@ -386,7 +386,7 @@ and dexpr_node =
| DEgpsym of psymbol
| DEplapp of plsymbol * dexpr list
| DElsapp of lsymbol * dexpr list
| DEapply of dexpr * dexpr list
| DEapply of dexpr * dexpr
| DEconst of Number.constant
| DEval of dval_decl * dexpr
| DElet of dlet_defn * dexpr
......@@ -623,16 +623,13 @@ let dexpr ?loc node =
let argl, res = specialize_ls ls in
dity_unify_app ls dexpr_expected_type del argl;
[], res
| DEapply (de,del) ->
let argl, res = de.de_dvty in
let rec down del al = match del, al with
| de::del, dity::al -> dexpr_expected_type de dity; down del al
| [], _ -> al
| _ when argl = [] -> Loc.errorm
"This expression is not a function and cannot be applied"
| _ -> Loc.errorm
"This function is applied to too many arguments" in
down del argl, res
| DEapply ({de_dvty = (dity::argl, res)}, de2) ->
dexpr_expected_type de2 dity;
argl, res
| DEapply (de1, de2) -> (* TODO: better error messages *)
let argl, res = specialize_ls fs_func_app in
dity_unify_app fs_func_app dexpr_expected_type [de1;de2] argl;
[], res
| DEconst (Number.ConstInt _) ->
[], dity_int
| DEconst (Number.ConstReal _) ->
......@@ -1113,18 +1110,14 @@ and try_expr keep_loc uloc env (argl,res) node =
e_plapp pl (List.map2 get_gh pl.pl_args del) (ity_of_dity res)
| DElsapp (ls,del) ->
e_lapp ls (List.map (get env) del) (ity_of_dity res)
| DEapply (de,del) ->
let rec ghostify_args del = function
| VTvalue _ -> assert (del = []); []
| VTarrow a ->
let rec args del al = match del, al with
| de::del, {pv_ghost = gh}::al ->
e_ghostify gh (get env de) :: args del al
| [], _ -> []
| _, [] -> ghostify_args del a.aty_result in
args del a.aty_args in
let e = get env de in
e_app e (ghostify_args del e.e_vty)
| DEapply ({de_dvty = (_::_, _)} as de1,de2) ->
let e1 = get env de1 in
let gh = match e1.e_vty with
| VTarrow {aty_args = pv::_} -> pv.pv_ghost
| _ -> assert false in
e_app e1 [e_ghostify gh (get env de2)]
| DEapply (de1,de2) ->
e_lapp fs_func_app [get env de1; get env de2] (ity_of_dity res)
| DEconst c ->
e_const c
| DEval (vald,de) ->
......
......@@ -102,7 +102,7 @@ and dexpr_node =
| DEgpsym of psymbol
| DEplapp of plsymbol * dexpr list
| DElsapp of lsymbol * dexpr list
| DEapply of dexpr * dexpr list
| DEapply of dexpr * dexpr
| DEconst of Number.constant
| DEval of dval_decl * dexpr
| DElet of dlet_defn * dexpr
......
......@@ -585,7 +585,8 @@ let rec e_app_flatten e pv = match e.e_node with
will be rejected, since local_get_ref is instantiated to
the region introduced (reset) by create_ref. Is it bad? *)
let e_app = List.fold_left (fun e -> on_value (e_app_flatten e))
let e_app e1 e2 = on_value (fun pv -> e_app_flatten e1 pv) e2
let e_app e1 el = List.fold_left e_app e1 el
let e_plapp pls el ity =
if pls.pl_hidden then raise (HiddenPLS pls);
......
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