dexpr.ml 45.9 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10 11 12 13 14 15 16 17 18 19 20 21
(********************************************************************)

open Stdlib
open Ident
open Ty
open Term
open Ity
open Expr

(** Program types *)

type dity =
Andrei Paskevich's avatar
Andrei Paskevich committed
22 23 24 25
  | Dutv of tvsymbol          (* undestructible "user" type variable *)
  | Dvar of dvar ref          (* destructible "fresh" type variable *)
  | Durg of ity * dity        (* undestructible "user" region, for global refs *)
  | Dreg of dvar ref * dity   (* destructible "fresh" region *)
26 27 28
  | Dapp of itysymbol * dity list * dity list

and dvar =
Andrei Paskevich's avatar
Andrei Paskevich committed
29 30 31 32 33 34 35
  | Dtvs of tvsymbol          (* unassigned fresh type variable *)
  | Dval of dity              (* destructive binding *)

(* In Dapp, the second dity list only contains Dreg's and Durg's.
   In Dreg and Durg, the dity field is a Dapp of the region's type.
   In Dreg, the dvar field leads to another Dreg or Durg.
   In Durg, the ity field is an Ityreg. *)
36 37 38

type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)

Andrei Paskevich's avatar
Andrei Paskevich committed
39
let dity_of_dvty (argl,res) =
40
  List.fold_right (fun a d -> Dapp (its_func, [a;d], [])) argl res
Andrei Paskevich's avatar
Andrei Paskevich committed
41

42 43
let dvar_fresh n = ref (Dtvs (create_tvsymbol (id_fresh n)))

Andrei Paskevich's avatar
Andrei Paskevich committed
44
let dreg_fresh dity = Dreg (dvar_fresh "rho", dity)
45 46 47 48

let dity_of_ity ity =
  let hr = Hreg.create 3 in
  let rec dity ity = match ity.ity_node with
49 50
    | Ityapp (s,tl,rl) -> Dapp (s, List.map dity tl, List.map dity rl)
    | Ityvar (v,_) -> Dutv v
51 52 53 54
    | Ityreg r -> dreg r
  and dreg reg =
    try Hreg.find hr reg with Not_found ->
    let {reg_its = s; reg_args = tl; reg_regs = rl} = reg in
55
    let d = Dapp (s, List.map dity tl, List.map dity rl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
56
    let r = dreg_fresh d in Hreg.add hr reg r; r in
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71
  dity ity

let rec ity_of_dity = function
  | Dvar ({contents = Dval d})
  | Dreg ({contents = Dval d}, _) ->
      ity_of_dity d
  | Dvar r ->
      let v = create_tvsymbol (id_fresh "xi") in
      r := Dval (Dutv v); ity_var v
  | Dreg (r, d) ->
      let ity = ity_of_dity d in
      r := Dval (Durg (ity, d)); ity
  | Dutv v -> ity_var v
  | Durg (ity,_) -> ity
  | Dapp (s,tl,rl) ->
72
      ity_app s (List.map ity_of_dity tl) (List.map ity_of_dity rl)
73 74 75 76 77 78

(** Destructive type unification *)

let rec occur_check v = function
  | Dvar {contents = Dval d} | Dreg (_,d) | Durg (_,d) -> occur_check v d
  | Dvar {contents = Dtvs u} | Dutv u -> if tv_equal u v then raise Exit
79
  | Dapp (_,dl,_) -> List.iter (occur_check v) dl
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95

let rec dity_unify d1 d2 = match d1,d2 with
  | Dvar {contents = Dval d1}, d2
  | d1, Dvar {contents = Dval d2}
  | Durg (_,d1), Durg (_,d2) | Durg (_,d1), Dreg (_,d2)
  | Dreg (_,d1), Durg (_,d2) | Dreg (_,d1), Dreg (_,d2) ->
      dity_unify d1 d2
  | Dvar {contents = Dtvs u},
    Dvar {contents = Dtvs v} when tv_equal u v ->
      ()
  | Dvar ({contents = Dtvs v} as r), d
  | d, Dvar ({contents = Dtvs v} as r) ->
      occur_check v d;
      r := Dval d
  | Dutv u, Dutv v when tv_equal u v ->
      ()
96
  | Dapp (s1,dl1,_), Dapp (s2,dl2,_) when its_equal s1 s2 ->
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113
      List.iter2 dity_unify dl1 dl2
  | _ -> raise Exit

(** Reunify regions *)

let dtvs_queue : dvar ref Queue.t = Queue.create ()

let unify_queue : (dity * dity) Queue.t = Queue.create ()

let dity_fresh () =
  let r = dvar_fresh "mu" in
  Queue.add r dtvs_queue;
  Dvar r

let rec dity_refresh ht = function
  | Dreg ({contents = Dtvs v},d) ->
      begin try Htv.find ht v with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
114
      let r = dreg_fresh (dity_refresh ht d) in
115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
      Htv.add ht v r; r end
  | Dreg _ -> assert false
  | Dapp (s,dl,rl) -> Dapp (s, List.map (dity_refresh ht) dl,
                               List.map (dity_refresh ht) rl)
  | Dvar {contents = Dval d} -> dity_refresh (Htv.create 3) d
  |(Dvar {contents = Dtvs _} | Dutv _ | Durg _) as d -> d

let dity_refresh d = dity_refresh (Htv.create 3) d

let dity_unify_weak = dity_unify

let dity_unify d1 d2 = dity_unify d1 d2; Queue.add (d1,d2) unify_queue

let rec reunify d1 d2 = match d1,d2 with
  | Dvar {contents = Dval d1}, d2
  | d1, Dvar {contents = Dval d2}
  | Dreg ({contents = Dval d1},_), d2
  | d1, Dreg ({contents = Dval d2},_) ->
      reunify d1 d2
  | Dvar _, Dvar _ | Dutv _, Dutv _ | Durg _, Durg _ ->
      ()
  | Dreg ({contents = Dtvs u},_),
    Dreg ({contents = Dtvs v},_) when tv_equal u v ->
      ()
  | Dreg (r, d1), (Dreg (_, d2) as d)
  | Dreg (r, d1), (Durg (_, d2) as d)
  | (Durg (_, d1) as d), Dreg (r, d2) ->
      reunify d1 d2;
      r := Dval d
  | Dapp (_,dl1,rl1), Dapp (_,dl2,rl2) ->
      List.iter2 reunify dl1 dl2;
      List.iter2 reunify rl1 rl2
  | _ -> assert false

let reunify_regions () =
  Queue.iter (fun r -> match !r with
    | Dval d -> r := Dval (dity_refresh d)
    | Dtvs _ -> ()) dtvs_queue;
  Queue.clear dtvs_queue;
  Queue.iter (fun (d1,d2) -> reunify d1 d2) unify_queue;
  Queue.clear unify_queue

(** Built-in types *)

159 160 161 162
let dity_int  = Dapp (its_int,  [], [])
let dity_real = Dapp (its_real, [], [])
let dity_bool = Dapp (its_bool, [], [])
let dity_unit = Dapp (its_unit, [], [])
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193

let dvty_int  = [], dity_int
let dvty_real = [], dity_real
let dvty_bool = [], dity_bool
let dvty_unit = [], dity_unit

(** Pretty-printing *)

let rprinter =
  let sanitizer = Ident.sanitizer Ident.char_to_lalpha Ident.char_to_alnumus in
  Ident.create_ident_printer [] ~sanitizer

let print_args pr fmt tl = if tl <> [] then
  Format.fprintf fmt "@ %a" (Pp.print_list Pp.space pr) tl

let print_regs pr fmt rl = if rl <> [] then
  Format.fprintf fmt "@ <%a>" (Pp.print_list Pp.comma pr) rl

let protect_on x s = if x then "(" ^^ s ^^ ")" else s

let rec print_dity pri fmt = function
  | Dvar {contents = Dval d}
  | Dreg ({contents = Dval d},_) ->
      print_dity pri fmt d
  | Dvar {contents = Dtvs v}
  | Dutv v ->
      Pretty.print_tv fmt v
  | Dreg ({contents = Dtvs v},d) ->
      Format.fprintf fmt (protect_on (pri > 1) "%a@ @@%s")
        (print_dity 0) d (Ident.id_unique rprinter v.tv_name)
  | Durg (ity,d) ->
194 195
      let reg_of_ity = function
        | {ity_node = Ityreg reg} -> reg | _ -> assert false in
196 197
      Format.fprintf fmt (protect_on (pri > 1) "%a@ @@%s")
        (print_dity 0) d (Ident.id_unique rprinter (reg_of_ity ity).reg_name)
198
  | Dapp (s,[t1;t2],[]) when its_equal s its_func ->
199 200
      Format.fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
        (print_dity 1) t1 (print_dity 0) t2
201
  | Dapp (s,tl,[]) when is_ts_tuple s.its_ts ->
202 203 204 205 206
      Format.fprintf fmt "(%a)" (Pp.print_list Pp.comma (print_dity 0)) tl
  | Dapp (s,tl,rl) ->
      Format.fprintf fmt (protect_on (pri > 1) "%a%a%a")
        Pretty.print_ts s.its_ts (print_args (print_dity 2)) tl
          (print_regs (print_dity 0)) rl
207
(*
208 209 210
  | Dpur (s,tl) ->
      Format.fprintf fmt (protect_on (pri > 1 && tl <> []) "{%a}%a")
        Pretty.print_ts s.its_ts (print_args (print_dity 2)) tl
211
*)
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230

let print_dity fmt d = print_dity 0 fmt d

(* Specialization of symbols *)

let specialize_scheme tvs (argl,res) =
  let hv = Htv.create 3 and hr = Htv.create 3 in
  let rec spec_dity = function
    | Durg _ as d -> d
    | Dvar {contents = Dval d} | Dreg ({contents = Dval d},_) -> spec_dity d
    | Dvar {contents = Dtvs v} | Dutv v as d -> get_tv v d
    | Dreg ({contents = Dtvs v},d) -> get_reg v d
    | Dapp (s,dl,rl) -> Dapp (s, List.map spec_dity dl, List.map spec_dity rl)
  and get_tv v d = try Htv.find hv v with Not_found ->
    let nd = dity_fresh () in
    (* can't return d, might differ in regions *)
    if not (Stv.mem v tvs) then dity_unify_weak nd d;
    Htv.add hv v nd; nd
  and get_reg v d = try Htv.find hr v with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
231
    let r = dreg_fresh (spec_dity d) in
232 233 234 235 236 237
    Htv.add hr v r; r in
  List.map spec_dity argl, spec_dity res

let spec_ity hv hr frz ity =
  let rec dity ity = match ity.ity_node with
    | Ityreg r -> dreg r
238 239
    | Ityvar (v,_) -> if Mtv.mem v frz.isb_var then Dutv v else get_tv v
    | Ityapp (s,tl,rl) -> Dapp (s, List.map dity tl, List.map dity rl)
240 241 242 243
  and get_tv v = try Htv.find hv v with Not_found ->
    let nd = dity_fresh () in Htv.add hv v nd; nd
  and dreg reg = try Hreg.find hr reg with Not_found ->
    let {reg_its = s; reg_args = tl; reg_regs = rl} = reg in
244
    let d = Dapp (s, List.map dity tl, List.map dity rl) in
245
    let r = if Mreg.mem reg frz.isb_reg then
Andrei Paskevich's avatar
Andrei Paskevich committed
246
      Durg (ity_reg reg, d) else dreg_fresh d in
247 248 249
    Hreg.add hr reg r; r in
  dity ity

Andrei Paskevich's avatar
Andrei Paskevich committed
250
let specialize_pv {pv_ity = ity} =
251 252
  spec_ity (Htv.create 3) (Hreg.create 3) (ity_freeze isb_empty ity) ity

Andrei Paskevich's avatar
Andrei Paskevich committed
253
let specialize_xs {xs_ity = ity} =
254 255
  spec_ity (Htv.create 3) (Hreg.create 3) (ity_freeze isb_empty ity) ity

256
let specialize_rs {rs_cty = cty} =
257 258 259 260
  let hv = Htv.create 3 and hr = Hreg.create 3 in
  let spec ity = spec_ity hv hr cty.cty_freeze ity in
  List.map (fun v -> spec v.pv_ity) cty.cty_args, spec cty.cty_result

261 262 263
let specialize_ls {ls_args = args; ls_value = res} =
  let hv = Htv.create 3 and hr = Hreg.create 3 in
  let rec ity ty = match ty.ty_node with
264
    | Tyapp (s,tl) -> ity_app (restore_its s) (List.map ity tl) []
265 266 267 268
    | Tyvar v -> ity_var v in
  let spec ty = spec_ity hv hr isb_empty (ity ty) in
  List.map spec args, Opt.fold (Util.const spec) dity_bool res

269 270 271
(** Patterns *)

type dpattern = {
Andrei Paskevich's avatar
Andrei Paskevich committed
272
  dp_pat  : pre_pattern;
273 274 275 276 277 278 279 280
  dp_dity : dity;
  dp_vars : dity Mstr.t;
  dp_loc  : Loc.position option;
}

type dpattern_node =
  | DPwild
  | DPvar  of preid
281
  | DPapp  of rsymbol * dpattern list
282 283 284 285 286 287 288 289
  | DPor   of dpattern * dpattern
  | DPas   of dpattern * preid
  | DPcast of dpattern * ity

(** Specifications *)

type ghost = bool

Andrei Paskevich's avatar
Andrei Paskevich committed
290
type dbinder = preid option * ghost * dity
291

292 293 294
type register_old = pvsymbol -> string -> pvsymbol

type 'a later = pvsymbol Mstr.t -> register_old -> 'a
295 296 297 298 299 300
  (* specification terms are parsed and typechecked after the program
     expressions, when the types of locally bound program variables are
     already established. *)

type dspec_final = {
  ds_pre     : term list;
301 302 303
  ds_post    : (pvsymbol * term) list;
  ds_xpost   : (pvsymbol * term) list Mexn.t;
  ds_reads   : pvsymbol list;
304 305
  ds_writes  : term list;
  ds_diverge : bool;
306
  ds_checkrw : bool;
307 308
}

309
type dspec = ity -> dspec_final
310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
  (* Computation specification is also parametrized by the result type.
     All vsymbols in the postcondition clauses in the [ds_post] field
     must have this type. All vsymbols in the exceptional postcondition
     clauses must have the type of the corresponding exception. *)

(** Expressions *)

type dinvariant = term list

type dexpr = {
  de_node : dexpr_node;
  de_dvty : dvty;
  de_loc  : Loc.position option;
}

and dexpr_node =
  | DEvar of string * dvty
327 328
  | DEpv of pvsymbol
  | DErs of rsymbol
329
  | DEls of lsymbol
330
  | DEconst of Number.constant
331
  | DEapp of dexpr * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
332
  | DEfun of dbinder list * dspec later * dexpr
333
  | DEany of dbinder list * dspec later * dity
334 335
  | DElet of dlet_defn * dexpr
  | DErec of drec_defn * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
336
  | DEnot of dexpr
337 338
  | DEand of dexpr * dexpr
  | DEor of dexpr * dexpr
339 340
  | DEif of dexpr * dexpr * dexpr
  | DEcase of dexpr * (dpattern * dexpr) list
341
  | DEassign of (dexpr * rsymbol * dexpr) list
342
  | DEwhile of dexpr * dinvariant later * variant list later * dexpr
343
  | DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
344 345 346
  | DEtry of dexpr * (xsymbol * dpattern * dexpr) list
  | DEraise of xsymbol * dexpr
  | DEghost of dexpr
347
  | DEassert of assertion_kind * term later
Andrei Paskevich's avatar
Andrei Paskevich committed
348 349 350 351
  | DEpure of term later
  | DEabsurd
  | DEtrue
  | DEfalse
352 353 354 355 356
  | DEmark of preid * dexpr
  | DEcast of dexpr * ity
  | DEuloc of dexpr * Loc.position
  | DElabel of dexpr * Slab.t

357
and dlet_defn = preid * ghost * rs_kind * dexpr
358 359 360

and drec_defn = { fds : dfun_defn list }

361
and dfun_defn = preid * ghost * rs_kind *
362
  dbinder list * dspec later * variant list later * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
363

364 365 366 367 368 369 370 371 372
(** Environment *)

type denv = {
  frozen : dity list;
  locals : (Stv.t option * dvty) Mstr.t;
}

let denv_empty = { frozen = []; locals = Mstr.empty }

Andrei Paskevich's avatar
Andrei Paskevich committed
373 374
let is_frozen frozen v =
  try List.iter (occur_check v) frozen; false with Exit -> true
375 376 377

let freeze_dvty frozen (argl,res) =
  let rec add l = function
Andrei Paskevich's avatar
Andrei Paskevich committed
378
    | Dreg (_,d) | Durg (_,d)
379 380 381
    | Dvar { contents = Dval d } -> add l d
    | Dvar { contents = Dtvs _ } as d -> d :: l
    | Dutv _ as d -> d :: l
382
    | Dapp (_,tl,_) -> List.fold_left add l tl in
383 384 385 386
  List.fold_left add (add frozen res) argl

let free_vars frozen (argl,res) =
  let rec add s = function
Andrei Paskevich's avatar
Andrei Paskevich committed
387
    | Dreg (_,d) | Durg (_,d)
388
    | Dvar { contents = Dval d } -> add s d
Andrei Paskevich's avatar
Andrei Paskevich committed
389 390
    | Dvar { contents = Dtvs v }
    | Dutv v -> if is_frozen frozen v then s else Stv.add v s
391
    | Dapp (_,tl,_) -> List.fold_left add s tl in
392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413
  List.fold_left add (add Stv.empty res) argl

let denv_add_mono { frozen = frozen; locals = locals } id dvty =
  let locals = Mstr.add id.pre_name (None, dvty) locals in
  { frozen = freeze_dvty frozen dvty; locals = locals }

let denv_add_poly { frozen = frozen; locals = locals } id dvty =
  let ftvs = free_vars frozen dvty in
  let locals = Mstr.add id.pre_name (Some ftvs, dvty) locals in
  { frozen = frozen; locals = locals }

let denv_add_rec_mono { frozen = frozen; locals = locals } id dvty =
  let locals = Mstr.add id.pre_name (Some Stv.empty, dvty) locals in
  { frozen = freeze_dvty frozen dvty; locals = locals }

let denv_add_rec_poly { frozen = frozen; locals = locals } frozen0 id dvty =
  let ftvs = free_vars frozen0 dvty in
  let locals = Mstr.add id.pre_name (Some ftvs, dvty) locals in
  { frozen = frozen; locals = locals }

let denv_add_rec denv frozen0 id ((argl,res) as dvty) =
  let rec is_explicit = function
Andrei Paskevich's avatar
Andrei Paskevich committed
414
    | Dreg (_,d) | Durg (_,d)
415 416
    | Dvar { contents = Dval d } -> is_explicit d
    | Dvar { contents = Dtvs _ } -> false
Andrei Paskevich's avatar
Andrei Paskevich committed
417
    | Dutv _ -> true
418
    | Dapp (_,tl,_) -> List.for_all is_explicit tl in
419 420 421 422 423 424
  if List.for_all is_explicit argl && is_explicit res
  then denv_add_rec_poly denv frozen0 id dvty
  else denv_add_rec_mono denv id dvty

let denv_add_var denv id dity = denv_add_mono denv id ([], dity)

Andrei Paskevich's avatar
Andrei Paskevich committed
425
let denv_add_let denv (id,_,_,({de_dvty = dvty} as de)) =
426 427 428
  if fst dvty = [] then denv_add_mono denv id dvty else
  let rec is_value de = match de.de_node with
    | DEghost de | DEuloc (de,_) | DElabel (de,_) -> is_value de
429
    | DEvar _ | DErs _ | DEfun _ | DEany _ -> true
430 431 432 433 434 435
    | _ -> false in
  if is_value de
  then denv_add_poly denv id dvty
  else denv_add_mono denv id dvty

let denv_add_args { frozen = frozen; locals = locals } bl =
Andrei Paskevich's avatar
Andrei Paskevich committed
436 437
  let l = List.fold_left (fun l (_,_,t) -> t::l) frozen bl in
  let add s (id,_,t) = match id with
438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474
    | Some {pre_name = n} ->
        Mstr.add_new (Dterm.DuplicateVar n) n (None, ([],t)) s
    | None -> s in
  let s = List.fold_left add Mstr.empty bl in
  { frozen = l; locals = Mstr.set_union s locals }

let denv_add_pat { frozen = frozen; locals = locals } dp =
  let l = Mstr.fold (fun _ t l -> t::l) dp.dp_vars frozen in
  let s = Mstr.map (fun t -> None, ([], t)) dp.dp_vars in
  { frozen = l; locals = Mstr.set_union s locals }

let mk_node n = function
  | Some tvs, dvty -> DEvar (n, specialize_scheme tvs dvty)
  | None,     dvty -> DEvar (n, dvty)

let denv_get denv n =
  mk_node n (Mstr.find_exn (Dterm.UnboundVar n) n denv.locals)

let denv_get_opt denv n =
  Opt.map (mk_node n) (Mstr.find_opt n denv.locals)

(** Unification tools *)

let dity_unify_app ls fn (l1: 'a list) (l2: dity list) =
  try List.iter2 fn l1 l2 with Invalid_argument _ ->
    raise (BadArity (ls, List.length l1))

let dpat_expected_type {dp_dity = dp_dity; dp_loc = loc} dity =
  try dity_unify dp_dity dity with Exit -> Loc.errorm ?loc
    "This pattern has type %a,@ but is expected to have type %a"
    print_dity dp_dity print_dity dity

let dpat_expected_type_weak {dp_dity = dp_dity; dp_loc = loc} dity =
  try dity_unify_weak dp_dity dity with Exit -> Loc.errorm ?loc
    "This pattern has type %a,@ but is expected to have type %a"
    print_dity dp_dity print_dity dity

Andrei Paskevich's avatar
Andrei Paskevich committed
475 476
let dexpr_expected_type {de_dvty = dvty; de_loc = loc} dity =
  let res = dity_of_dvty dvty in
477 478 479 480
  try dity_unify res dity with Exit -> Loc.errorm ?loc
    "This expression has type %a,@ but is expected to have type %a"
    print_dity res print_dity dity

Andrei Paskevich's avatar
Andrei Paskevich committed
481 482
let dexpr_expected_type_weak {de_dvty = dvty; de_loc = loc} dity =
  let res = dity_of_dvty dvty in
483 484 485 486 487 488
  try dity_unify_weak res dity with Exit -> Loc.errorm ?loc
    "This expression has type %a,@ but is expected to have type %a"
    print_dity res print_dity dity

(** Generation of letrec blocks *)

489 490
type pre_fun_defn = preid * ghost * rs_kind * dbinder list *
  dity * (denv -> dspec later * variant list later * dexpr)
491 492 493 494

exception DupId of preid

let drec_defn denv0 prel =
Andrei Paskevich's avatar
Andrei Paskevich committed
495 496
  if prel = [] then invalid_arg "Dexpr.drec_defn: empty function list";
  let add s (id,_,_,_,_,_) = Sstr.add_new (DupId id) id.pre_name s in
497 498
  let _ = try List.fold_left add Sstr.empty prel with DupId id ->
    Loc.errorm ?loc:id.pre_loc "duplicate function name %s" id.pre_name in
Andrei Paskevich's avatar
Andrei Paskevich committed
499 500 501
  let add denv (id,_,_,bl,res,_) =
    if bl = [] then invalid_arg "Dexpr.drec_defn: empty argument list";
    let argl = List.map (fun (_,_,t) -> t) bl in
502 503
    denv_add_rec denv denv0.frozen id (argl,res) in
  let denv1 = List.fold_left add denv0 prel in
Andrei Paskevich's avatar
Andrei Paskevich committed
504
  let parse (id,gh,pk,bl,res,pre) =
505
    let dsp, dvl, de = pre (denv_add_args denv1 bl) in
506
    dexpr_expected_type_weak de res;
507
    (id,gh,pk,bl,dsp,dvl,de) in
508
  let fdl = List.map parse prel in
509
  let add denv (id,_,_,bl,_,_,{de_dvty = dvty}) =
Andrei Paskevich's avatar
Andrei Paskevich committed
510
    (* just in case we linked some polymorphic type var to the outer context *)
511 512 513 514 515 516 517
    let check tv = if is_frozen denv0.frozen tv then Loc.errorm ?loc:id.pre_loc
      "This function is expected to be polymorphic in type variable %a"
      Pretty.print_tv tv in
    begin match Mstr.find_opt id.pre_name denv1.locals with
    | Some (Some tvs, _) -> Stv.iter check tvs
    | Some (None, _) | None -> assert false
    end;
Andrei Paskevich's avatar
Andrei Paskevich committed
518 519
    let argl = List.map (fun (_,_,t) -> t) bl in
    denv_add_poly denv id (argl, dity_of_dvty dvty) in
520 521 522 523 524 525 526 527 528 529 530 531 532
  List.fold_left add denv0 fdl, { fds = fdl }

(** Constructors *)

let dpattern ?loc node =
  let mk_dpat pre dity vars =
    { dp_pat = pre; dp_dity = dity; dp_vars = vars; dp_loc = loc } in
  let dpat = function
    | DPwild ->
        mk_dpat PPwild (dity_fresh ()) Mstr.empty
    | DPvar id ->
        let dity = dity_fresh () in
        mk_dpat (PPvar id) dity (Mstr.singleton id.pre_name dity)
533 534
    | DPapp ({rs_logic = RLls ls} as rs, dpl) when ls.ls_constr > 0 ->
        let argl, res = specialize_rs rs in
535 536 537 538 539
        dity_unify_app ls dpat_expected_type dpl argl;
        let join n _ _ = raise (Dterm.DuplicateVar n) in
        let add acc dp = Mstr.union join acc dp.dp_vars in
        let vars = List.fold_left add Mstr.empty dpl in
        let ppl = List.map (fun dp -> dp.dp_pat) dpl in
540 541 542
        mk_dpat (PPapp (rs, ppl)) res vars
    | DPapp (rs,_) ->
        raise (ConstructorExpected rs);
543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563
    | DPor (dp1,dp2) ->
        dpat_expected_type dp2 dp1.dp_dity;
        let join n dity1 dity2 = try dity_unify dity1 dity2; Some dity1
          with Exit -> Loc.errorm ?loc
            "Variable %s has type %a,@ but is expected to have type %a"
            n print_dity dity1 print_dity dity2 in
        let vars = Mstr.union join dp1.dp_vars dp2.dp_vars in
        mk_dpat (PPor (dp1.dp_pat, dp2.dp_pat)) dp1.dp_dity vars
    | DPas (dp, ({pre_name = n} as id)) ->
        let { dp_pat = pat; dp_dity = dity; dp_vars = vars } = dp in
        let vars = Mstr.add_new (Dterm.DuplicateVar n) n dity vars in
        mk_dpat (PPas (pat, id)) dity vars
    | DPcast (dp, ity) ->
        dpat_expected_type_weak dp (dity_of_ity ity);
        dp
  in
  Loc.try1 ?loc dpat node

let dexpr ?loc node =
  let get_dvty = function
    | DEvar (_,dvty) ->
564
        dvty
565
    | DEpv pv ->
566
        [], specialize_pv pv
567
    | DErs rs ->
568
        specialize_rs rs
569 570
    | DEls ls ->
        specialize_ls ls
571
    | DEconst (Number.ConstInt _) ->
572
        dvty_int
573
    | DEconst (Number.ConstReal _) ->
574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593
        dvty_real
    | DEapp ({de_dvty = (arg::argl, res)}, de2) ->
        dexpr_expected_type de2 arg;
        argl, res
    | DEapp ({de_dvty = ([],res)} as de1, de2) ->
        let f,a,r = match specialize_rs rs_func_app with
          | [f;a],r -> f,a,r | _ -> assert false in
        begin try dity_unify res f with Exit ->
          let rec down n de = match de.de_node with
            | DEapp (de,_) -> down (succ n) de
            | _ when n = 0 -> Loc.errorm ?loc:de.de_loc
                "This expression has type %a,@ it cannot be applied"
                print_dity (dity_of_dvty de.de_dvty)
            | _ -> Loc.errorm ?loc:de.de_loc
                "This expression has type %a,@ but is applied to %d arguments"
                print_dity (dity_of_dvty de.de_dvty) (succ n) in
          down 0 de1
        end;
        dexpr_expected_type de2 a;
        [], r
594
    | DEfun (bl,_,de) ->
595
        List.map (fun (_,_,t) -> t) bl, dity_of_dvty de.de_dvty
596
    | DEany (bl,_,res) ->
597
        List.map (fun (_,_,t) -> t) bl, res
598 599
    | DElet (_,de)
    | DErec (_,de) ->
600
        de.de_dvty
601 602
    | DEnot de ->
        dexpr_expected_type de dity_bool;
603 604 605
        dvty_bool
    | DEand (de1,de2)
    | DEor (de1,de2) ->
606 607
        dexpr_expected_type de1 dity_bool;
        dexpr_expected_type de2 dity_bool;
608
        dvty_bool
609 610 611 612 613
    | DEif (de1,de2,de3) ->
        let res = dity_fresh () in
        dexpr_expected_type de1 dity_bool;
        dexpr_expected_type de2 res;
        dexpr_expected_type de3 res;
614
        [], res
615
    | DEcase (_,[]) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
616
        invalid_arg "Dexpr.dexpr: empty branch list in DEcase"
617 618 619 620
    | DEcase (de,bl) ->
        let ety = dity_fresh () in
        let res = dity_fresh () in
        dexpr_expected_type de ety;
621
        List.iter (fun (dp,de) ->
622
          dpat_expected_type dp ety;
623
          dexpr_expected_type de res) bl;
624
        [], res
625
    | DEassign al ->
626 627 628
        List.iter (fun (de1,rs,de2) ->
          let argl, res = specialize_rs rs in
          let ls = match rs.rs_logic with RLls ls -> ls
629 630 631
            | _ -> invalid_arg "Dexpr.dexpr: not a field" in
          dity_unify_app ls dexpr_expected_type [de1] argl;
          dexpr_expected_type_weak de2 res) al;
632 633
        dvty_unit
    | DEwhile (de1,_,_,de2) ->
634
        dexpr_expected_type de1 dity_bool;
635
        dexpr_expected_type de2 dity_unit;
636
        dvty_unit
637 638 639 640
    | DEfor (_,de_from,_,de_to,_,de) ->
        dexpr_expected_type de_from dity_int;
        dexpr_expected_type de_to dity_int;
        dexpr_expected_type de dity_unit;
641
        dvty_unit
642
    | DEtry (_,[]) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
643
        invalid_arg "Dexpr.dexpr: empty branch list in DEtry"
644 645 646
    | DEtry (de,bl) ->
        let res = dity_fresh () in
        dexpr_expected_type de res;
647 648 649
        List.iter (fun (xs,dp,de) ->
          dpat_expected_type dp (specialize_xs xs);
          dexpr_expected_type de res) bl;
650
        [], res
651 652
    | DEraise (xs,de) ->
        dexpr_expected_type de (specialize_xs xs);
653
        [], dity_fresh ()
654
    | DEghost de ->
655
        de.de_dvty
656
    | DEassert _ ->
657
        dvty_unit
658 659
    | DEpure _
    | DEabsurd ->
660
        [], dity_fresh ()
661 662
    | DEtrue
    | DEfalse ->
663
        dvty_bool
664 665
    | DEcast (de,ity) ->
        dexpr_expected_type_weak de (dity_of_ity ity);
666
        de.de_dvty
667
    | DEmark (_,de)
668 669
    | DEuloc (de,_)
    | DElabel (de,_) ->
670 671 672
        de.de_dvty in
  let dvty = Loc.try1 ?loc get_dvty node in
  { de_node = node; de_dvty = dvty; de_loc = loc }
673 674 675 676 677 678 679

(** Final stage *)

(** Binders *)

let binders bl =
  let sn = ref Sstr.empty in
680
  let binder (id, ghost, dity) =
681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697
    let id = match id with
      | Some ({pre_name = n} as id) ->
          let exn = match id.pre_loc with
            | Some loc -> Loc.Located (loc, Dterm.DuplicateVar n)
            | None -> Dterm.DuplicateVar n in
          sn := Sstr.add_new exn n !sn; id
      | None -> id_fresh "_" in
    create_pvsymbol id ~ghost (ity_of_dity dity) in
  List.map binder bl

(** Specifications *)

let to_fmla f = match f.t_ty with
  | None -> f
  | Some ty when ty_equal ty ty_bool -> t_equ f t_bool_true
  | _ -> Loc.error ?loc:f.t_loc Dterm.FmlaExpected

698 699 700 701
let create_assert = to_fmla

let create_invariant pl = List.map to_fmla pl

702 703
let create_post ity ql = List.map (fun (v,f) ->
  ity_equal_check ity v.pv_ity; Ity.create_post v.pv_vs (to_fmla f)) ql
704

705
let create_xpost xql = Mexn.mapi (fun xs ql -> create_post xs.xs_ity ql) xql
706 707 708

(** User effects *)

709 710 711 712 713 714
let rec effect_of_term t =
  let quit () = Loc.errorm ?loc:t.t_loc "unsupported effect expression" in
  match t.t_node with
  | Tapp (fs, [ta]) ->
      let v, ity, fa = effect_of_term ta in
      let ity = match fa with
715
        | Some {rs_cty = {cty_args = [arg]; cty_result = res}} ->
716 717 718
            ity_full_inst (ity_match isb_empty arg.pv_ity ity) res
        | Some _ -> assert false
        | None -> ity in
719
      begin try match ity.ity_node, restore_rs fs with
Andrei Paskevich's avatar
Andrei Paskevich committed
720 721
        | Ityreg {reg_its = ts}, ({rs_field = Some f} as rs)
          when List.exists (pv_equal f) ts.its_mfields -> v, ity, Some rs
722
        | _, {rs_cty={cty_args=[arg]; cty_result=res; cty_freeze=frz}} ->
723 724 725 726 727 728
            v, ity_full_inst (ity_match frz arg.pv_ity ity) res, None
        | _ -> quit () with Not_found -> quit () end
  | Tvar v ->
      let v = try restore_pv v with Not_found -> quit () in
      v, v.pv_ity, None
  | _ -> quit ()
729 730

let effect_of_dspec dsp =
731
  let pvs = Spv.of_list dsp.ds_reads in
732
  let add_write (l,eff) t = match effect_of_term t with
733 734
    | v, {ity_node = Ityreg reg}, fd ->
        let fs = match fd with
735
          | Some fd -> Spv.singleton (Opt.get fd.rs_field)
736
          | None -> Spv.of_list reg.reg_its.its_mfields in
737 738 739
        let rd = Spv.singleton v and wr = Mreg.singleton reg fs in
        let e = Loc.try2 ?loc:t.t_loc eff_write rd wr in
        (e,t)::l, eff_union_par eff e
740
    | _ ->
741
        Loc.errorm ?loc:t.t_loc "mutable expression expected" in
742 743 744 745
  let wl, eff = List.fold_left add_write ([], eff_read pvs) dsp.ds_writes in
  let eff = Mexn.fold (fun xs _ eff -> eff_raise eff xs) dsp.ds_xpost eff in
  let eff = if dsp.ds_diverge then eff_diverge eff else eff in
  wl, eff
746

747 748
(* TODO: add warnings for empty postconditions (anywhere)
    and empty exceptional postconditions (toplevel). *)
Andrei Paskevich's avatar
Andrei Paskevich committed
749
let check_spec dsp ecty e =
750 751 752
  let bad_write weff eff = not (Mreg.submap (fun _ s1 s2 -> Spv.subset s1 s2)
                                            weff.eff_writes eff.eff_writes) in
  let bad_raise xeff eff = not (Sexn.subset xeff.eff_raises eff.eff_raises) in
753
  (* computed effect vs user effect *)
Andrei Paskevich's avatar
Andrei Paskevich committed
754
  let check_rwd = dsp.ds_checkrw in
755
  let uwrl, ue = effect_of_dspec dsp in
756 757
  let ucty = create_cty ecty.cty_args ecty.cty_pre ecty.cty_post
    ecty.cty_xpost ecty.cty_oldies ue ecty.cty_result in
758 759
  let ueff = ucty.cty_effect and eeff = ecty.cty_effect in
  let urds = ueff.eff_reads and erds = eeff.eff_reads in
760
  (* check that every user effect actually happens *)
761 762 763 764 765 766 767 768 769
  if not (Spv.subset urds erds) then Loc.errorm ?loc:e.e_loc
    "variable@ %a@ does@ not@ occur@ in@ this@ expression"
    Pretty.print_vs (Spv.choose (Spv.diff urds erds)).pv_vs;
  if bad_write ueff eeff then List.iter (fun (weff,t) ->
    if bad_write weff eeff then Loc.errorm ?loc:t.t_loc
      "this@ write@ effect@ does@ not@ happen@ in@ the@ expression") uwrl;
  if bad_raise ueff eeff then Loc.errorm ?loc:e.e_loc
    "this@ expression@ does@ not@ raise@ exception@ %a"
    print_xs (Sexn.choose (Sexn.diff ueff.eff_raises eeff.eff_raises));
770
  if ueff.eff_oneway && not eeff.eff_oneway then Loc.errorm ?loc:e.e_loc
771
    "this@ expression@ does@ not@ diverge";
772
  (* check that every computed effect is listed *)
773 774 775 776 777
  if check_rwd && not (Spv.subset erds urds) then Spv.iter (fun v ->
    Loc.errorm ?loc:e.e_loc
      "this@ expression@ depends@ on@ variable@ %a@ left@ out@ in@ \
      the@ specification" Pretty.print_vs v.pv_vs) (Spv.diff erds urds);
  if check_rwd && bad_write eeff ueff then
778
    Loc.errorm ?loc:(e_locate_effect (fun eff -> bad_write eff ueff) e)
779 780
      "this@ expression@ produces@ an@ unlisted@ write@ effect";
  if ecty.cty_args <> [] && bad_raise eeff ueff then Sexn.iter (fun xs ->
781
    Loc.errorm ?loc:(e_locate_effect (fun eff -> Sexn.mem xs eff.eff_raises) e)
782
      "this@ expression@ raises@ unlisted@ exception@ %a"
783
      print_xs xs) (Sexn.diff eeff.eff_raises ueff.eff_raises);
784 785
  if check_rwd && eeff.eff_oneway && not ueff.eff_oneway then
    Loc.errorm ?loc:(e_locate_effect (fun eff -> eff.eff_oneway) e)
786 787
      "this@ expression@ may@ diverge,@ but@ this@ is@ not@ \
        stated@ in@ the@ specification"
788

Andrei Paskevich's avatar
Andrei Paskevich committed
789
let check_aliases recu c =
790 791 792
  let rds_regs = c.cty_freeze.isb_reg in
  let report r _ _ =
    if Mreg.mem r rds_regs then let spv = Spv.filter
793
        (fun v -> ity_r_occurs r v.pv_ity) (cty_reads c) in
794
      Loc.errorm "The type of this function contains an alias with \
795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811
        external variable %a" print_pv (Spv.choose spv)
    else Loc.errorm "The type of this function contains an alias" in
  (* we allow the value in a non-recursive function to contain
     regions coming the function's arguments, but not from the
     context. It is sometimes useful to write a function around
     a constructor or a projection. For recursive functions, we
     impose the full non-alias discipline, to ensure the safety
     of region polymorphism (see add_rec_mono). We do not track
     aliases inside the type of an argument or a result, which
     may break the type inference, but we have a safety net
     type checking in Expr. *)
  let add_ity regs ity =
    let frz = ity_freeze isb_empty ity in
    Mreg.union report regs frz.isb_reg in
  let add_arg regs v = add_ity regs v.pv_ity in
  let regs = List.fold_left add_arg rds_regs c.cty_args in
  ignore (add_ity (if recu then regs else rds_regs) c.cty_result)
812

813
let check_fun rsym dsp e =
Andrei Paskevich's avatar
Andrei Paskevich committed
814
  let c,e = match e with
815
    | { c_node = Cfun e; c_cty = c } -> c,e
Andrei Paskevich's avatar
Andrei Paskevich committed
816 817 818 819 820 821 822
    | _ -> invalid_arg "Dexpr.check_fun" in
  let c = match rsym with
    | Some s -> s.rs_cty
    | None -> c in
  check_spec dsp c e;
  check_aliases (rsym <> None) c

823 824
(** Environment *)

Andrei Paskevich's avatar
Andrei Paskevich committed
825
type env = {
826
  rsm : rsymbol Mstr.t;
827
  pvm : pvsymbol Mstr.t;
828
  old : (pvsymbol Mstr.t * (let_defn * pvsymbol) Hpv.t) Mstr.t;
829 830
}

831
let env_empty = {
832
  rsm = Mstr.empty;
833
  pvm = Mstr.empty;
834
  old = Mstr.empty;
835 836
}

837 838 839
exception UnboundLabel of string

let find_old pvm (ovm,old) v =
840
  if v.pv_ity.ity_imm then v else
841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865
  let n = v.pv_vs.vs_name.id_string in
  (* if v is top-level, both ov and pv are None.
     If v is local, ov and pv must be equal to v.
     If they are not equal, then v is defined under the label,
     so we return v and do not register an "oldie" for it. *)
  let ov = Mstr.find_opt n ovm in
  let pv = Mstr.find_opt n pvm in
  if not (Opt.equal pv_equal ov pv) then v
  else match Hpv.find_opt old v with
    | Some (_,o) -> o
    | None ->
        let e = e_pure (t_var v.pv_vs) in
        let id = id_clone v.pv_vs.vs_name in
        let ld = let_var id ~ghost:true e in
        Hpv.add old v ld; snd ld

let register_old env v l =
  find_old env.pvm (Mstr.find_exn (UnboundLabel l) l env.old) v

let get_later env later = later env.pvm (register_old env)

let add_label ({pvm = pvm; old = old} as env) l =
  let ht = Hpv.create 3 in
  { env with old = Mstr.add l (pvm, ht) old }, ht

Andrei Paskevich's avatar
Andrei Paskevich committed
866
let rebase_old {pvm = pvm} preold old fvs =
867 868 869 870
  let rebase v (_,{pv_vs = o}) sbs =
    if not (Mvs.mem o fvs) then sbs else match preold with
      | Some preold ->
          Mvs.add o (t_var (find_old pvm preold v).pv_vs) sbs
871
      | None -> raise (UnboundLabel "0") in
872 873
  Hpv.fold rebase old Mvs.empty

Andrei Paskevich's avatar
Andrei Paskevich committed
874
let rebase_pre env preold old pl =
875 876
  let pl = List.map to_fmla pl in
  let fvs = List.fold_left t_freevars Mvs.empty pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
877
  let sbs = rebase_old env preold old fvs in
878 879
  List.map (t_subst sbs) pl

Andrei Paskevich's avatar
Andrei Paskevich committed
880
let rebase_variant env preold old varl =
881 882
  let add s (t,_) = t_freevars s t in
  let fvs = List.fold_left add Mvs.empty varl in
Andrei Paskevich's avatar
Andrei Paskevich committed
883
  let sbs = rebase_old env preold old fvs in
884 885 886
  let conv (t,rel) = t_subst sbs t, rel in
  List.map conv varl

887 888 889 890
let get_oldies old =
  Hpv.fold (fun v (_,o) sbs -> Mpv.add o v sbs) old Mpv.empty

let add_rsymbol ({rsm = rsm; pvm = pvm} as env) rs =
891
  let n = rs.rs_name.id_string in
892 893 894 895
  let pvm = match rs.rs_logic with
    | RLpv pv -> Mstr.add n pv pvm
    | _ -> pvm in
  { env with rsm = Mstr.add n rs rsm; pvm = pvm }
896

897
let add_pvsymbol ({pvm = pvm} as env) pv =
898
  let n = pv.pv_vs.vs_name.id_string in
899
  { env with pvm = Mstr.add n pv pvm }
900

901 902
let add_pv_map ({pvm = pvm} as env) vm =
  { env with pvm = Mstr.set_union vm pvm }
903 904 905 906 907

let add_binders env pvl = List.fold_left add_pvsymbol env pvl

(** Abstract values *)

Andrei Paskevich's avatar
Andrei Paskevich committed
908 909 910 911
let cty_of_spec env bl dsp dity =
  let ity = ity_of_dity dity in
  let bl = binders bl in
  let env = add_binders env bl in
912 913
  let preold = Mstr.find_opt "0" env.old in
  let env, old = add_label env "0" in
914
  let dsp = get_later env dsp ity in
915
  let _, eff = effect_of_dspec dsp in
916
  let eff = eff_reset_overwritten eff in
917
  let eff = eff_reset eff (ity_freeregs Sreg.empty ity) in
Andrei Paskevich's avatar
Andrei Paskevich committed
918
  let p = rebase_pre env preold old dsp.ds_pre in
919
  let q = create_post ity dsp.ds_post in
Andrei Paskevich's avatar
Andrei Paskevich committed
920
  let xq = create_xpost dsp.ds_xpost in
921
  create_cty bl p q xq (get_oldies old) eff ity
922 923 924

(** Expressions *)

Andrei Paskevich's avatar
Andrei Paskevich committed
925 926 927 928
let warn_unused s loc =
  if s = "" || s.[0] <> '_' then
  Warning.emit ?loc "unused variable %s" s

929
let check_used_pv e pv = if not (Spv.mem pv e.e_effect.eff_reads) then
Andrei Paskevich's avatar
Andrei Paskevich committed
930
  warn_unused pv.pv_vs.vs_name.id_string pv.pv_vs.vs_name.id_loc
931

932 933 934 935
let e_let_check ld e = match ld with
  | LDvar (v,_) -> check_used_pv e v; e_let ld e
  | _           -> e_let ld e

936 937
let rec strip uloc labs de = match de.de_node with
  | DEcast (de,_) -> strip uloc labs de
938
  | DEuloc (de,loc) -> strip (Some (Some loc)) labs de
939 940 941
  | DElabel (de,s) -> strip uloc (Slab.union labs s) de
  | _ -> uloc, labs, de

942 943 944 945 946 947 948 949 950
let get_pv env n = Mstr.find_exn (Dterm.UnboundVar n) n env.pvm
let get_rs env n = Mstr.find_exn (Dterm.UnboundVar n) n env.rsm

let rec expr uloc env ({de_loc = loc} as de) =
  let uloc, labs, de = strip uloc Slab.empty de in
  let e = Loc.try3 ?loc try_expr uloc env de in
  let loc = Opt.get_def loc uloc in
  if loc = None && Slab.is_empty labs
  then e else e_label ?loc labs e
Andrei Paskevich's avatar
Andrei Paskevich committed
951

952
and cexp uloc env ghost ({de_loc = loc} as de) =
953
  let uloc, labs, de = strip uloc Slab.empty de in
954 955 956 957 958
  if not (Slab.is_empty labs) then Warning.emit ?loc
    "Ignoring labels over a higher-order expression";
  Loc.try4 ?loc try_cexp uloc env ghost de

and try_cexp uloc env ghost de0 = match de0.de_node with
959 960 961 962
  | DEvar <