Commit 72714897 authored by Andrei Paskevich's avatar Andrei Paskevich

Mlw: support Epure in the surface language (with type inference)

The current syntax is "{| <term> |}", which is shorter than
"pure { <term> }", and does not require a keyword. Better
alternatives are welcome.

As for type inference, we infer the type pf the term under Epure
without binding destructible type variables in the program.
In particular,
  let ghost fn x = {| x + 1 |}
will not typecheck. Indeed, even if we detect that the result
is [int], the type of the formal parameter [x[ is not inferred
in the process, and thus stays at ['xi].

Another problem is related to the fact that variable and function
namespaces are not yet separated when we perform type inference.
Thus both fuctions
  let ghost fn (x: int) = let x a = a in {| x + 5 |}
and
  let ghost fn (x: int) = let x a = a in {| x 5 |}
will not typecheck, since the type of [x] is ['a -> 'a] when
we infer the type for the Epure term, but it becomes [int],
when we construct the final program expression. Probably,
the only reasonable solution is to keep variables and
functions in the same namespace, so that [x] simply can
not be used in annotations after being redefined as a
program function.
parent 9d21ee47
......@@ -29,6 +29,36 @@ let dty_fresh = let i = ref 0 in fun () -> Dvar (ref (Dind (incr i; !i)))
let dty_of_ty ty = Duty ty
let dty_var tv = Duty (ty_var tv)
let rec dty_app ts dtl =
try
let tl = List.map (function Duty ty -> ty | _ -> raise Exit) dtl in
Duty (ty_app ts tl)
with Exit -> match ts.ts_def with
| Alias ty ->
let sbs = try List.fold_right2 Mtv.add ts.ts_args dtl Mtv.empty with
| Invalid_argument _ -> raise (BadTypeArity (ts, List.length dtl)) in
let rec inst ty = match ty.ty_node with
| Tyapp (ts,tl) -> dty_app ts (List.map inst tl)
| Tyvar v -> Mtv.find v sbs in
inst ty
| NoDef | Range _ | Float _ ->
if List.length ts.ts_args <> List.length dtl then
raise (BadTypeArity (ts, List.length dtl));
Dapp (ts, dtl)
let dty_fold fnS fnV fnI dty =
let rec on_ty ty = match ty.ty_node with
| Tyapp (s, tl) -> fnS s (List.map on_ty tl)
| Tyvar v -> fnV v in
let rec on_dty = function
| Dvar { contents = Dind i } -> fnI i
| Dvar { contents = Dval dty } -> on_dty dty
| Dapp (s, dtl) -> fnS s (List.map on_dty dtl)
| Duty ty -> on_ty ty in
on_dty dty
exception UndefinedTypeVar of tvsymbol
let rec ty_of_dty ~strict = function
......
......@@ -22,6 +22,17 @@ val dty_fresh : unit -> dty
val dty_of_ty : ty -> dty
val dty_var : tvsymbol -> dty
val dty_app : tysymbol -> dty list -> dty
val dty_match : dty -> ty -> unit (* raises Exit on failure *)
val dty_unify : dty -> dty -> unit (* raises Exit on failure *)
val dty_bool : dty
val dty_fold : (tysymbol -> 'a list -> 'a) ->
(tvsymbol -> 'a) -> (int -> 'a) -> dty -> 'a
(** Patterns, terms, and formulas *)
type dpattern = private {
......
......@@ -126,25 +126,27 @@ let rec dity_unify_weak d1 d2 = match d1,d2 with
List.iter2 dity_unify_weak dl1 dl2
| _ -> raise Exit
let dity_app_fresh s dl =
let mv = List.fold_right2 Mtv.add s.its_ts.ts_args dl Mtv.empty in
let hr = Hreg.create 3 in
let rec ity_inst ity = match ity.ity_node with
| Ityreg r -> reg_inst r
| Ityvar (v, false) -> Mtv.find v mv
| Ityvar (v, true) -> dity_pur (Mtv.find v mv)
| Ityapp (s,tl,rl) -> app_map ity_inst s tl rl
and reg_inst ({reg_its = s; reg_args = tl; reg_regs = rl} as r) =
try Hreg.find hr r with Not_found ->
let d = dity_reg (app_map ity_inst s tl rl) in
Hreg.replace hr r d; d in
Dapp (s, dl, List.map reg_inst s.its_regions)
let rec dity_refresh = function
| Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))}
| Durg (d,_) -> dity_refresh d
| Dutv _ as d -> d
| Dvar {contents = Dtvs _} -> dity_fresh ()
| Dapp (s,dl,_) ->
let dl = List.map dity_refresh dl in
let mv = List.fold_right2 Mtv.add s.its_ts.ts_args dl Mtv.empty in
let hr = Hreg.create 3 in
let rec ity_inst ity = match ity.ity_node with
| Ityreg r -> reg_inst r
| Ityvar (v, false) -> Mtv.find v mv
| Ityvar (v, true) -> dity_pur (Mtv.find v mv)
| Ityapp (s,tl,rl) -> app_map ity_inst s tl rl
and reg_inst ({reg_its = s; reg_args = tl; reg_regs = rl} as r) =
try Hreg.find hr r with Not_found ->
let d = dity_reg (app_map ity_inst s tl rl) in
Hreg.replace hr r d; d in
let d = Dapp (s, dl, List.map reg_inst s.its_regions) in
let d = dity_app_fresh s (List.map dity_refresh dl) in
if its_immutable s then d else dity_reg d
let rec dity_unify_asym d1 d2 = match d1,d2 with
......@@ -423,7 +425,7 @@ and dexpr_node =
| DEraise of xsymbol * dexpr
| DEghost of dexpr
| DEassert of assertion_kind * term later
| DEpure of term later
| DEpure of term later * dity
| DEabsurd
| DEtrue
| DEfalse
......@@ -536,6 +538,28 @@ let denv_get denv n =
let denv_get_opt denv n =
Opt.map (mk_node n) (Mstr.find_opt n denv.locals)
let denv_pure denv get_dty =
let ht = Htv.create 3 in
let hi = Hint.create 3 in
let rec fold = function
| Dvar {contents = (Dval d|Dpur d|Dsim (d,_)|Dreg (d,_))}
| Durg (d,_) -> fold d
| Dvar {contents = Dtvs v} as d ->
begin try fst (Htv.find ht v) with Not_found ->
let f = Dterm.dty_fresh () in Htv.add ht v (f,d); f end
| Dapp (s,dl,_) -> Dterm.dty_app s.its_ts (List.map fold dl)
| Dutv v -> Dterm.dty_var v in
let pure_denv = Mstr.mapi (fun n (_, dvty) ->
Dterm.DTvar (n, fold (dity_of_dvty dvty))) denv.locals in
let dty = get_dty pure_denv in
Htv.iter (fun v (f,_) ->
try Dterm.dty_match f (ty_var v) with Exit -> ()) ht;
let fnS s dl = dity_app_fresh (restore_its s) dl in
let fnV v = try snd (Htv.find ht v) with Not_found -> Dutv v in
let fnI i = try Hint.find hi i with Not_found ->
let d = dity_fresh () in Hint.add hi i d; d in
dity_pur (Dterm.dty_fold fnS fnV fnI dty)
(** Unification tools *)
let dity_unify_app ls fn (l1: 'a list) (l2: dity list) =
......@@ -727,7 +751,8 @@ let dexpr ?loc node =
de.de_dvty
| DEassert _ ->
dvty_unit
| DEpure _
| DEpure (_, dity) ->
[], dity
| DEabsurd ->
[], dity_fresh ()
| DEtrue
......@@ -1265,7 +1290,7 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
e_ghostify true (expr uloc {env with ghs = true} de)
| DEassert (ak,f) ->
e_assert ak (create_assert (get_later env f))
| DEpure t ->
| DEpure (t, _) ->
e_pure (get_later env t)
| DEabsurd ->
e_absurd (ity_of_dity res)
......
......@@ -23,12 +23,13 @@ val dity_fresh : unit -> dity
val dity_of_ity : ity -> dity
val dity_int : dity
val dity_int : dity
val dity_real : dity
val dity_bool : dity
val dity_unit : dity
type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
(** Patterns *)
type dpattern = private {
......@@ -114,7 +115,7 @@ and dexpr_node =
| DEraise of xsymbol * dexpr
| DEghost of dexpr
| DEassert of assertion_kind * term later
| DEpure of term later
| DEpure of term later * dity
| DEabsurd
| DEtrue
| DEfalse
......@@ -150,6 +151,8 @@ val denv_get_opt : denv -> string -> dexpr_node option
val denv_contents : denv -> (Ty.Stv.t option * dvty) Mstr.t
val denv_pure : denv -> (Dterm.denv -> Dterm.dty) -> dity
(** Constructors *)
val dpattern : ?loc:Loc.position -> dpattern_node -> dpattern
......
......@@ -182,6 +182,10 @@ rule token = parse
{ LEFTBRC }
| "}"
{ RIGHTBRC }
| "{|"
{ LEFTPURE }
| "|}"
{ RIGHTPURE }
| ":"
{ COLON }
| ";"
......
......@@ -153,7 +153,7 @@
(* program symbols *)
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
%token AMPAMP BARBAR LEFTBRC RIGHTBRC LEFTPURE RIGHTPURE SEMICOLON
(* Precedences *)
......@@ -811,6 +811,7 @@ expr_sub:
| LEFTPAR comma_list2(expr) RIGHTPAR { Etuple $2 }
| LEFTBRC field_list1(expr) RIGHTBRC { Erecord $2 }
| LEFTBRC expr_arg WITH field_list1(expr) RIGHTBRC { Eupdate ($2, $4) }
| LEFTPURE term RIGHTPURE { Epure $2 }
| expr_dot DOT lqualid_rich { Eidapp ($3, [$1]) }
| expr_arg LEFTSQ expr RIGHTSQ
{ Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
......
......@@ -139,6 +139,7 @@ and expr_desc =
| Enot of expr
| Ematch of expr * (pattern * expr) list
| Eabsurd
| Epure of term
| Eraise of qualid * expr option
| Etry of expr * (qualid * pattern option * expr) list
| Efor of ident * expr * Expr.for_direction * expr * invariant * expr
......
......@@ -739,8 +739,16 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
| Ptree.Eghost e1 ->
DEghost (dexpr muc denv e1)
| Ptree.Eabsurd -> DEabsurd
| Ptree.Eassert (ak, lexpr) ->
DEassert (ak, dassert muc lexpr)
| Ptree.Epure t ->
let get_term lvm old = type_term muc lvm old t in
let gvars _at q = try match find_prog_symbol muc q with
| PV v -> Some v | _ -> None with _ -> None in
let get_dty pure_denv =
let dt = dterm muc.muc_theory gvars None pure_denv t in
match dt.dt_dty with Some dty -> dty | None -> dty_bool in
DEpure (get_term, denv_pure denv get_dty)
| Ptree.Eassert (ak, f) ->
DEassert (ak, dassert muc f)
| Ptree.Emark (id, e1) ->
DEmark (create_user_id id, dexpr muc denv e1)
| Ptree.Enamed (Lpos uloc, e1) ->
......
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