Merge branch 'improve_diverges_effect'

bench/typing/bad/partial_function.mlw

+val partial function f (x:int) : unit

bench/typing/bad/partial_ghost_fun.ml

+val partial random () : int
+let ghost f () = random ()

bench/typing/bad/partial_ghost_fun.mlw

+val partial random () : int
+let ghost f () = random ()
\ No newline at end of file

bench/typing/bad/partial_ghostvar.mlw

+val partial f (x:int) : unit
+
+let main () =
+  let ghost s = 3 in
+  f s;
+  42
\ No newline at end of file

bench/typing/bad/partial_lemma.mlw

+let partial lemma f (x:int)
+  ensures { true }
+= ()

bench/typing/bad/partial_refine.mlw

+module S
+  val constant c : int
+  val f () : int
+end
+
+module I2
+  val partial random () : int
+  clone export S with val f = random
+end
\ No newline at end of file

bench/typing/bad/partial_terminates.mlw

+let partial f () = 2
\ No newline at end of file

bench/typing/bad/partial_witness.mlw

+val partial random () : int
+
+type t = { x: int } invariant { x = 0 } by { x = random () }
\ No newline at end of file

bench/typing/good/partial.mlw

+val partial random () : int
+val f (x:int) : unit
+
+use int.Int
+
+let main () =
+  let r = random () in
+  let s = random () in
+  let ghost x = random () in
+  f x;
+  f r;
+  f x;
+  r * s
\ No newline at end of file

examples/use_api/clone.ml

@@ -120,6 +120,7 @@ let d2 : Ptree.decl =
     sp_variant = [];
     sp_checkrw = false;
     sp_diverge = false;
+    sp_partial = false;
   }
   in
   let body: expr = mk_expr Etrue in
@@ -150,6 +151,7 @@ let d3 : Ptree.decl =
     sp_variant = [];
     sp_checkrw = false;
     sp_diverge = false;
+    sp_partial = false;
   }
   in
   let body: expr = mk_evar id_b in
@@ -184,6 +186,7 @@ let d1 : Ptree.decl =
     sp_variant = [];
     sp_checkrw = false;
     sp_diverge = false;
+    sp_partial = false;
   }
   in
   let body: expr = mk_expr (Ecast (mk_econst "42", PTtyapp (Qident a, []))) in

examples/use_api/mlw_tree.ml

@@ -117,6 +117,7 @@ let d1 : decl =
     sp_variant = [];
     sp_checkrw = false;
     sp_diverge = false;
+    sp_partial = false;
   }
   in
   let body = mk_eapp mul_int [mk_evar id_x; mk_econst "7"] in
@@ -163,6 +164,7 @@ let d2 =
     sp_variant = [];
     sp_checkrw = false;
     sp_diverge = false;
+    sp_partial = false;
   }
   in
   let body =
@@ -221,6 +223,7 @@ let d3 =
     sp_variant = [];
     sp_checkrw = false;
     sp_diverge = false;
+    sp_partial = false;
   }
   in
   let body =

plugins/python/py_main.ml

@@ -79,6 +79,7 @@ let empty_spec = {
   sp_variant = [];
   sp_checkrw = false;
   sp_diverge = false;
+  sp_partial = false;
 }
 
 type env = {

plugins/python/py_parser.mly

@@ -38,7 +38,7 @@
     sp_pre     = [];    sp_post    = [];  sp_xpost  = [];
     sp_reads   = [];    sp_writes  = [];  sp_alias  = [];
     sp_variant = [];
-    sp_checkrw = false; sp_diverge = false;
+    sp_checkrw = false; sp_diverge = false; sp_partial = false;
   }
 
   let spec_union s1 s2 = {
@@ -51,6 +51,7 @@
     sp_variant = variant_union s1.sp_variant s2.sp_variant;
     sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
     sp_diverge = s1.sp_diverge || s2.sp_diverge;
+    sp_partial = s1.sp_partial || s2.sp_partial;
   }
 
 %}

share/emacs/why3.el

@@ -25,7 +25,7 @@
 (defconst why3-font-lock-keywords-1
   (list
    `(,(why3-regexp-opt '("invariant" "variant" "diverges" "requires" "ensures" "pure" "returns" "raises" "reads" "writes" "alias" "assert" "assume" "check")) . font-lock-type-face)
-   `(,(why3-regexp-opt '("use" "clone" "scope" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "raise" "return" "break" "continue" "try" "with" "theory" "uses" "module" "converter" "fun" "at" "old" "true" "false" "forall" "exists" "label" "by" "so" "meta")) . font-lock-keyword-face)
+   `(,(why3-regexp-opt '("use" "clone" "scope" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "partial" "raise" "return" "break" "continue" "try" "with" "theory" "uses" "module" "converter" "fun" "at" "old" "true" "false" "forall" "exists" "label" "by" "so" "meta")) . font-lock-keyword-face)
    )
   "Minimal highlighting for Why3 mode")
 

share/vim/syntax/why3.vim

@@ -93,7 +93,7 @@ syn keyword  whyKeyword  then type with
 
 syn keyword  whyKeyword  abstract any break continue
 syn keyword  whyKeyword  exception fun ghost label
-syn keyword  whyKeyword  model mutable private
+syn keyword  whyKeyword  model mutable partial private
 syn keyword  whyKeyword  raise rec return val while
 
 syn keyword  whyBoolean  true false

src/mlw/dexpr.ml

@@ -384,6 +384,7 @@ type dspec_final = {
   ds_reads   : pvsymbol list;
   ds_writes  : term list;
   ds_diverge : bool;
+  ds_partial : bool;
   ds_checkrw : bool;
 }
 
@@ -892,6 +893,7 @@ let effect_of_dspec dsp =
         Loc.errorm ?loc:t.t_loc "mutable expression expected" in
   let wl, eff = List.fold_left add_write ([], eff_read pvs) dsp.ds_writes in
   let eff = Mxs.fold (fun xs _ eff -> eff_raise eff xs) dsp.ds_xpost eff in
+  let eff = if dsp.ds_partial then eff_partial eff else eff in
   let eff = if dsp.ds_diverge then eff_diverge eff else eff in
   wl, eff
 
@@ -924,8 +926,10 @@ let check_spec inr dsp ecty ({e_loc = loc} as e) =
   if check_ue && bad_raise ueff eeff then Loc.errorm ?loc
     "this@ expression@ does@ not@ raise@ exception@ %a"
     print_xs (Sxs.choose (Sxs.diff ueff.eff_raises eeff.eff_raises));
-  if check_ue && ueff.eff_oneway && not eeff.eff_oneway then Loc.errorm ?loc
-      "this@ expression@ does@ not@ diverge";
+  if check_ue && diverges ueff.eff_oneway && not (diverges eeff.eff_oneway)
+    then Loc.errorm ?loc "this@ expression@ does@ not@ diverge";
+  if check_ue && partial ueff.eff_oneway && total eeff.eff_oneway
+    then Loc.errorm ?loc "this@ expression@ does@ not@ diverge@ or@ fail";
   (* check that every computed effect is listed *)
   if check_rw && bad_read eeff ueff then Loc.errorm ?loc
     "this@ expression@ depends@ on@ variable@ %a,@ \

src/mlw/dexpr.mli

@@ -76,6 +76,7 @@ type dspec_final = {
   ds_reads   : pvsymbol list;
   ds_writes  : term list;
   ds_diverge : bool;
+  ds_partial : bool;
   ds_checkrw : bool;
 }
 

src/mlw/expr.ml

@@ -74,8 +74,10 @@ let rs_kind s = match s.rs_logic with
 let rs_ghost s = s.rs_cty.cty_effect.eff_ghost
 
 let check_effects ?loc c =
-  if c.cty_effect.eff_oneway then Loc.errorm ?loc
+  if diverges c.cty_effect.eff_oneway then Loc.errorm ?loc
     "This function may not terminate, it cannot be used as pure";
+  if partial c.cty_effect.eff_oneway then Loc.errorm ?loc
+    "This function may fail, it cannot be used as pure";
   if not (cty_pure c) then Loc.errorm ?loc
     "This function has side effects, it cannot be used as pure"
 
@@ -451,7 +453,7 @@ let localize_reset_stale v r el =
 
 (* localize a divergence *)
 let localize_divergence el =
-  let diverges eff = eff.eff_oneway in
+  let diverges eff = diverges eff.eff_oneway in
   List.iter (fun e -> if diverges e.e_effect then
     let loc = e_locate_effect diverges e in
     Loc.error ?loc GhostDivergence) el;
@@ -1149,7 +1151,7 @@ let ls_decr_of_rec_defn = function
   | { rec_rsym = {rs_cty = {cty_pre = {t_node = Tapp (ls,_)}::_}} } -> Some ls
   | _ -> None
 
-(* pretty-pringting *)
+(* pretty-printing *)
 
 open Format
 open Pretty
@@ -1172,8 +1174,9 @@ let forget_let_defn = function
 let print_rs fmt s =
   Ident.print_decoded fmt (id_unique sprinter (id_of_rs s))
 
-let print_rs_head fmt s = fprintf fmt "%s%s%a%a"
+let print_rs_head fmt s = fprintf fmt "%s%s%s%a%a"
   (if s.rs_cty.cty_effect.eff_ghost then "ghost " else "")
+  (if partial s.rs_cty.cty_effect.eff_oneway then "partial " else "")
   (match s.rs_logic with
     | RLnone -> ""
     | RLpv _ -> "function "

src/mlw/ity.ml

@@ -868,6 +868,21 @@ exception IllegalAssign of region * region * region
 exception ImpureVariable of tvsymbol * ity
 exception GhostDivergence
 
+(* termination status *)
+type oneway =
+  | Total
+  | Partial
+  | Diverges
+
+let total status = (status = Total)
+let partial status = (status = Partial)
+let diverges status = (status = Diverges)
+
+let oneway_union t1 t2 = match t1, t2 with
+  | Total, Total -> Total
+  | _, Diverges | Diverges, _ -> Diverges
+  | _ -> Partial
+
 type effect = {
   eff_reads  : Spv.t;         (* known variables *)
   eff_writes : Spv.t Mreg.t;  (* writes to fields *)
@@ -876,7 +891,7 @@ type effect = {
   eff_resets : Sreg.t;        (* locked by covers *)
   eff_raises : Sxs.t;         (* raised exceptions *)
   eff_spoils : Stv.t;         (* immutable tyvars *)
-  eff_oneway : bool;          (* non-termination *)
+  eff_oneway : oneway;        (* non-termination *)
   eff_ghost  : bool;          (* ghost status *)
 }
 
@@ -888,7 +903,7 @@ let eff_empty = {
   eff_resets = Sreg.empty;
   eff_raises = Sxs.empty;
   eff_spoils = Stv.empty;
-  eff_oneway = false;
+  eff_oneway = Total;
   eff_ghost  = false;
 }
 
@@ -906,7 +921,7 @@ let eff_equal e1 e2 =
 let eff_pure e =
   Mreg.is_empty e.eff_writes &&
   Sxs.is_empty e.eff_raises &&
-  not e.eff_oneway
+  total e.eff_oneway
 
 let check_writes {eff_writes = wrt} pvs =
   if not (Mreg.is_empty wrt) then Spv.iter (fun v ->
@@ -940,12 +955,12 @@ let reset_taints e =
 
 let eff_ghostify gh e =
   if not gh || e.eff_ghost then e else
-  if e.eff_oneway then raise GhostDivergence else
+  if not (total e.eff_oneway) then raise GhostDivergence else
   reset_taints { e with eff_ghost = true }
 
 let eff_ghostify_weak gh e =
   if not gh || e.eff_ghost then e else
-  if e.eff_oneway || not (Sxs.is_empty e.eff_raises) then e else
+  if not (total e.eff_oneway && Sxs.is_empty e.eff_raises) then e else
   if not (Sreg.equal e.eff_taints (visible_writes e)) then e else
   (* it is not enough to catch BadGhostWrite from eff_ghostify below,
      because e may not have in eff_reads the needed visible variables
@@ -953,9 +968,15 @@ let eff_ghostify_weak gh e =
      Therefore, we check that all visible writes are already taints. *)
   eff_ghostify gh e
 
-let eff_diverge e = if e.eff_oneway then e else
+let eff_partial e =
+  if diverges e.eff_oneway || partial e.eff_oneway then e else
+  if e.eff_ghost then raise GhostDivergence else
+  { e with eff_oneway = Partial }
+
+let eff_diverge e =
+  if diverges e.eff_oneway then e else
   if e.eff_ghost then raise GhostDivergence else
-  { e with eff_oneway = true }
+  { e with eff_oneway = Diverges }
 
 let eff_read_pre rd e =
   if Spv.subset rd e.eff_reads then e else
@@ -1077,7 +1098,7 @@ let eff_assign asl =
     eff_resets = resets;
     eff_raises = Sxs.empty;
     eff_spoils = Stv.empty;
-    eff_oneway = false;
+    eff_oneway = Total;
     eff_ghost  = ghost } in
   (* verify that we can rebuild every value *)
   check_writes effect reads;
@@ -1120,7 +1141,7 @@ let eff_union e1 e2 = {
   eff_resets = Sreg.union e1.eff_resets e2.eff_resets;
   eff_raises = Sxs.union e1.eff_raises e2.eff_raises;
   eff_spoils = Stv.union e1.eff_spoils e2.eff_spoils;
-  eff_oneway = e1.eff_oneway || e2.eff_oneway;
+  eff_oneway = oneway_union e1.eff_oneway e2.eff_oneway;
   eff_ghost  = e1.eff_ghost && e2.eff_ghost }
 
 let eff_union e1 e2 =
@@ -1481,8 +1502,10 @@ let cty_exec ({cty_effect = eff} as c) =
      in the resulting pvsymbol. Thus, we have to forbid all effects,
      including allocation. TODO/FIXME: we should probably forbid
      the rest of the signature to contain regions at all. *)
-  if eff.eff_oneway then Loc.errorm
+  if diverges eff.eff_oneway then Loc.errorm
     "This function may not terminate, it cannot be used as pure";
+  if partial eff.eff_oneway then Loc.errorm
+    "This function may fail, it cannot be used as pure";
   if not (eff_pure eff && Sreg.is_empty eff.eff_resets) then Loc.errorm
     "This function has side effects, it cannot be used as pure";
   if not (Mreg.is_empty c.cty_freeze.isb_reg) then Loc.errorm
@@ -1679,7 +1702,7 @@ let print_spec args pre post xpost oldies eff fmt ity =
   fprintf fmt "@[<hov 4>@[%a@]%a@]"
     (Pp.print_list_pre Pp.space print_pvty) args
     (Pp.print_option print_result) ity;
-  if eff.eff_oneway then pp_print_string fmt " diverges";
+  if diverges eff.eff_oneway then pp_print_string fmt " diverges";
   let reads = List.fold_right Spv.remove args eff.eff_reads in
   if not (Spv.is_empty reads) then fprintf fmt "@\nreads  { @[%a@] }"
     (Pp.print_list Pp.comma print_pv) (Spv.elements reads);

src/mlw/ity.mli

@@ -339,6 +339,16 @@ exception IllegalAssign of region * region * region
 exception ImpureVariable of tvsymbol * ity
 exception GhostDivergence
 
+(* termination status *)
+type oneway =
+  | Total
+  | Partial
+  | Diverges
+
+val total : oneway -> bool
+val partial : oneway -> bool
+val diverges : oneway -> bool
+
 type effect = private {
   eff_reads  : Spv.t;         (* known variables *)
   eff_writes : Spv.t Mreg.t;  (* writes to fields *)
@@ -347,7 +357,7 @@ type effect = private {
   eff_resets : Sreg.t;        (* locked by covers *)
   eff_raises : Sxs.t;         (* raised exceptions *)
   eff_spoils : Stv.t;         (* immutable tyvars *)
-  eff_oneway : bool;          (* non-termination *)
+  eff_oneway : oneway;        (* non-termination *)
   eff_ghost  : bool;          (* ghost status *)
 }
 
@@ -377,9 +387,10 @@ val eff_catch : effect -> xsymbol -> effect
 
 val eff_spoil : effect -> ity -> effect
 
-val eff_diverge : effect -> effect                (* forbidden if ghost *)
-val eff_ghostify : bool -> effect -> effect       (* forbidden if diverges *)
-val eff_ghostify_weak : bool -> effect -> effect  (* only if has no effect *)
+val eff_partial : effect -> effect                      (* forbidden if ghost *)
+val eff_diverge : effect -> effect                      (* forbidden if ghost *)
+val eff_ghostify : bool -> effect -> effect (* forbidden if fails or diverges *)
+val eff_ghostify_weak : bool -> effect -> effect     (* only if has no effect *)
 
 val eff_union_seq : effect -> effect -> effect  (* checks for stale variables *)
 val eff_union_par : effect -> effect -> effect  (* no stale-variable check *)

src/mlw/pdecl.ml

@@ -88,8 +88,10 @@ let create_plain_record_decl ~priv ~mut id args fdl invl witn =
     [create_constructor ~constr:1 cid s fdl] in
   if witn <> [] then begin
     List.iter2 (fun fd ({e_loc = loc} as e) ->
-      if e.e_effect.eff_oneway then Loc.errorm ?loc
+      if diverges e.e_effect.eff_oneway then Loc.errorm ?loc
         "This expression may not terminate, it cannot be a witness";
+      if partial e.e_effect.eff_oneway then Loc.errorm ?loc
+        "This expression may fail, it cannot be a witness";
       if not (eff_pure e.e_effect) then Loc.errorm ?loc
         "This expression has side effects, it cannot be a witness";
       let ety = ty_of_ity e.e_ity and fty = fd.pv_vs.vs_ty in
@@ -539,7 +541,7 @@ let create_let_decl ld =
     Loc.error ?loc:ls.ls_name.id_loc (Decl.NoTerminationProof ls) in
   let is_trusted_rec = match ld with
     | LDrec ({rec_sym = {rs_logic = RLls ls; rs_cty = c}; rec_varl = []}::_)
-      when not c.cty_effect.eff_oneway -> abst = [] || fail_trusted_rec ls
+      when total c.cty_effect.eff_oneway -> abst = [] || fail_trusted_rec ls
     | _ -> false in
   let defn = if defn = [] then [] else
     let dl = List.map (fun (s,vl,t) -> make_ls_defn s vl t) defn in

src/mlw/pmodule.ml

@@ -451,6 +451,8 @@ let empty_clones m = {
   xs_table = Mxs.empty;
 }
 
+exception CloneDivergence of ident * ident
+
 (* populate the clone structure *)
 
 let rec sm_trans_ty tym tsm ty = match ty.ty_node with
@@ -730,7 +732,8 @@ let clone_cty cl sm ?(drop_decr=false) cty =
   let eff = eff_reset (eff_write reads writes) resets in
   let add_raise xs eff = eff_raise eff (sm_find_xs sm xs) in
   let eff = Sxs.fold add_raise cty.cty_effect.eff_raises eff in
-  let eff = if cty.cty_effect.eff_oneway then eff_diverge eff else eff in
+  let eff = if partial cty.cty_effect.eff_oneway then eff_partial eff else eff in
+  let eff = if diverges cty.cty_effect.eff_oneway then eff_diverge eff else eff in
   let cty = create_cty ~mask:cty.cty_mask args pre post xpost olds eff res in
   cty_ghostify (cty_ghost cty) cty
 
@@ -1052,6 +1055,11 @@ let clone_pdecl inst cl uc d = match d.pd_node with
       | RLls ls, RLls ls' -> cl.ls_table <- Mls.add ls ls' cl.ls_table
       | _ -> raise (BadInstance rs.rs_name)
       end;
+      begin
+        match cty.cty_effect.eff_oneway, rs'.rs_cty.cty_effect.eff_oneway with
+        | _, Total | Diverges, _ | Partial, Partial -> ()
+        | _ -> raise (CloneDivergence (rs.rs_name, rs'.rs_name))
+      end;
       cl.rs_table <- Mrs.add rs rs' cl.rs_table;
       let e = e_exec (c_app rs' cty.cty_args [] cty.cty_result) in
       let cexp = c_fun ~mask:cty.cty_mask cty.cty_args cty.cty_pre
@@ -1228,9 +1236,15 @@ let print_module fmt m = Format.fprintf fmt
   "@[<hov 2>module %s@\n%a@]@\nend" m.mod_theory.th_name.id_string
   (Pp.print_list Pp.newline2 print_unit) m.mod_units
 
+let print_id fmt id = Ident.print_decoded fmt id.id_string
+
 let () = Exn_printer.register (fun fmt e -> match e with
   | IncompatibleNotation nm -> Format.fprintf fmt
       "Incombatible type signatures for notation '%a'" Ident.print_decoded nm
   | ModuleNotFound (sl,s) -> Format.fprintf fmt
       "Module %s not found in library %a" s print_path sl
+  | CloneDivergence (iv, il) -> Format.fprintf fmt
+      "Cannot instantiate symbol %a with symbol %a \
+       that has worse termination status"
+      print_id iv print_id il
   | _ -> raise e)

src/mlw/vc.ml

@@ -538,7 +538,7 @@ let rec k_expr env lps e res xmap =
            Kseq (k_expr env lps e v xmap, 0, k v) in
   let var_or_proxy = var_or_proxy_case xmap in
   let check_divergence k =
-    if eff.eff_oneway && not env.divergent then begin
+    if diverges eff.eff_oneway && not env.divergent then begin
       if Debug.test_noflag debug_ignore_diverges then
       Warning.emit ?loc "termination@ of@ this@ expression@ \
         cannot@ be@ proved,@ but@ there@ is@ no@ `diverges'@ \

src/parser/lexer.mll

@@ -43,6 +43,7 @@
         "match", MATCH;
         "meta", META;
         "not", NOT;
+        "partial", PARTIAL;
         "predicate", PREDICATE;
         "range", RANGE;
         "scope", SCOPE;

src/parser/parser.mly

@@ -79,6 +79,7 @@
     sp_variant = [];
     sp_checkrw = false;
     sp_diverge = false;
+    sp_partial = false;
   }
 
   let spec_union s1 s2 = {
@@ -91,6 +92,7 @@
     sp_variant = variant_union s1.sp_variant s2.sp_variant;
     sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
     sp_diverge = s1.sp_diverge || s2.sp_diverge;
+    sp_partial = s1.sp_partial || s2.sp_partial;
   }
 
   let break_id    = "'Break"
@@ -106,6 +108,29 @@
     | Pwild -> sp
     | _ -> { sp with sp_post = List.map apply sp.sp_post }
 
+  type partial =
+    | Regular
+    | Partial
+    | Ghost
+
+  let ghost part = (part = Ghost)
+
+  let apply_partial_sp part sp =
+    if part <> Partial then sp else
+    { sp with sp_partial = true }
+
+  let apply_partial part e =
+    if part <> Partial then e else
+    let ed = match e.expr_desc with
+      | Efun (_::_ as bl, op, m, s, ex) ->
+          Efun (bl, op, m, apply_partial_sp part s, ex)
+      | Eany (_::_ as pl, rsk, op, m, s) ->
+          Eany (pl, rsk, op, m, apply_partial_sp part s)
+      | _ ->
+          Loc.errorm ~loc:e.expr_loc
+            "this expression cannot be declared partial" in
+    { e with expr_desc = ed }
+
   let we_attr = Ident.create_attribute "expl:witness existence"
 
   let pre_of_any any_loc ty ql =
@@ -177,7 +202,7 @@
 
 %token ABSTRACT ABSURD ALIAS ANY ASSERT ASSUME AT BEGIN BREAK CHECK
 %token CONTINUE DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
-%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD
+%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD PARTIAL
 %token PRIVATE PURE RAISE RAISES READS REC REQUIRES
 %token RETURN RETURNS TO TRY VAL VARIANT WHILE WRITES
 
@@ -727,16 +752,26 @@ numeral:
 (* Program declarations *)
 
 prog_decl:
-| VAL ghost kind attrs(lident_rich) mk_expr(val_defn) { Dlet (add_model_trace_attr $4, $2, $3, $5) }
-| LET ghost kind attrs(lident_rich) mk_expr(fun_defn) { Dlet ($4, $2, $3, $5) }
-| LET ghost kind attrs(lident_rich) const_defn        { Dlet ($4, $2, $3, $5) }
-| LET REC with_list1(rec_defn)                        { Drec $3 }
-| EXCEPTION attrs(uident_nq)        { Dexn ($2, PTtuple [], Ity.MaskVisible) }
-| EXCEPTION attrs(uident_nq) return { Dexn ($2, fst $3, snd $3) }
+| VAL ghost kind attrs(lident_rich) mk_expr(val_defn)
+    { Dlet (add_model_trace_attr $4, ghost $2, $3, apply_partial $2 $5) }
+| LET ghost kind attrs(lident_rich) mk_expr(fun_defn)
+    { Dlet ($4, ghost $2, $3, apply_partial $2 $5) }
+| LET ghost kind attrs(lident_rich) const_defn
+    { Dlet ($4, ghost $2, $3, apply_partial $2 $5) }
+| LET REC with_list1(rec_defn)
+    { Drec $3 }
+| EXCEPTION attrs(uident_nq)
+    { Dexn ($2, PTtuple [], Ity.MaskVisible) }
+| EXCEPTION attrs(uident_nq) return
+    { Dexn ($2, fst $3, snd $3) }
 
 ghost:
-| (* epsilon *) { false }
-| GHOST         { true }
+| (* epsilon *) { Regular }
+| PARTIAL       { Partial }
+| GHOST         { Ghost }
+| GHOST PARTIAL
+| PARTIAL GHOST { Loc.errorm ~loc:(floc $startpos $endpos)
+                    "Ghost functions cannot be partial" }
 
 kind:
 | (* epsilon *) { Expr.RKnone }
@@ -753,7 +788,7 @@ rec_defn:
       let spec = apply_return pat (spec_union $6 $8) in
       let id = mk_id return_id $startpos($7) $endpos($7) in
       let e = { $9 with expr_desc = Eoptexn (id, mask, $9) } in
-      $3, $1, $2, $4, ty, mask, spec, e }
+      $3, ghost $1, $2, $4, ty, mask, apply_partial_sp $1 spec, e }
 
 fun_defn:
 | binders return_opt spec EQUAL spec seq_expr
@@ -866,7 +901,7 @@ single_expr_:
         | Pas (p,v,g) -> Pas (push p, v, g)
         | Por (p,q) -> Por (push p, q)
         | _ -> Pghost pat) in
-      let pat = if $2 then push $4 else $4 in
+      let pat = if ghost $2 then push $4 else $4 in
       let rec unfold gh d p = match p.pat_desc with
         | Pparen p | Pscope (_,p) -> unfold gh d p
         | Pghost p -> unfold true d p
@@ -877,13 +912,13 @@ single_expr_:
         | _ when $3 = Expr.RKnone -> Ematch (d, [pat, $8], [])
         | _ -> Loc.errorm ~loc:(floc $startpos($3) $endpos($3))
             "illegal kind qualifier" in
-      unfold false $6 pat }
+      unfold false (apply_partial $2 $6) pat }
 | LET ghost kind attrs(lident_op_nq) EQUAL seq_expr IN seq_expr
-    { Elet ($4, $2, $3, $6, $8) }
+    { Elet ($4, ghost $2, $3, apply_partial $2 $6, $8) }
 | LET ghost kind attrs(lident_nq) mk_expr(fun_defn) IN seq_expr
-    { Elet ($4, $2, $3, $5, $7) }
+    { Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) }
 | LET ghost kind attrs(lident_op_nq) mk_expr(fun_defn) IN seq_expr
-    { Elet ($4, $2, $3, $5, $7) }
+    { Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) }
 | LET REC with_list1(rec_defn) IN seq_expr
     { Erec ($3, $5) }
 | FUN binders spec ARROW spec seq_expr
@@ -900,13 +935,13 @@ single_expr_:
         "this expression should not raise exceptions";
       if spec.sp_alias <> [] then Loc.errorm ~loc
         "this expression cannot have alias restrictions";
-      if spec.sp_diverge then Loc.errorm ~loc
+      if spec.sp_diverge || spec.sp_partial then Loc.errorm ~loc
         "this expression must terminate";
       let pre = pre_of_any loc ty spec.sp_post in
       let spec = { spec with sp_pre = spec.sp_pre @ pre } in
       Eany ([], Expr.RKnone, Some ty, mask, spec) }
 | VAL ghost kind attrs(lident_rich) mk_expr(val_defn) IN seq_expr
-    { Elet ($4, $2, $3, $5, $7) }
+    { Elet ($4, ghost $2, $3, apply_partial $2 $5, $7) }
 | MATCH seq_expr WITH ext_match_cases END
     { let bl, xl = $4 in Ematch ($2, bl, xl) }
 | EXCEPTION attrs(uident) IN seq_expr
@@ -1179,7 +1214,7 @@ pat_uni_:
 | pat_arg_                              { $1 }
 | uqualid pat_arg+                      { Papp ($1,$2) }
 | GHOST mk_pat(pat_uni_)                { Pghost $2 }
-| mk_pat(pat_uni_) AS ghost attrs(lident_nq)
+| mk_pat(pat_uni_) AS boption(GHOST) attrs(lident_nq)
                                         { Pas ($1,add_model_trace_attr $4,$3) }
 | mk_pat(pat_uni_) cast                 { Pcast ($1,$2) }
 
@@ -1211,7 +1246,7 @@ let_pat_conj_:
 let_pat_uni_:
 | pat_arg_                              { $1 }
 | uqualid pat_arg+                      { Papp ($1,$2) }
-| mk_pat(let_pat_uni_) AS ghost attrs(lident_nq)
+| mk_pat(let_pat_uni_) AS boption(GHOST) attrs(lident_nq)
                                         { Pas ($1,add_model_trace_attr $4,$3) }
 | mk_pat(let_pat_uni_) cast             { Pcast ($1,$2) }
 

src/parser/ptree.ml

@@ -111,6 +111,7 @@ type spec = {
   sp_variant : variant;
   sp_checkrw : bool;
   sp_diverge : bool;
+  sp_partial : bool;
 }
 
 type expr = {

src/parser/typing.ml

@@ -645,7 +645,8 @@ let dspec muc sp lvm xsm old ity = {
   ds_reads   = dreads muc sp.sp_reads lvm;
   ds_writes  = dwrites muc sp.sp_writes lvm;
   ds_checkrw = sp.sp_checkrw;
-  ds_diverge = sp.sp_diverge; }
+  ds_diverge = sp.sp_diverge;
+  ds_partial = sp.sp_partial; }
 
 let dspec_no_variant muc sp = match sp.sp_variant with
   | ({term_loc = loc},_)::_ ->

tests/test_extraction.mlw

@@ -169,7 +169,7 @@ module TestExtraction
     test_filter_ghost_args x 0 + 1
 
   let constant test_partial : int =
-    let partial = test_filter_ghost_args 3 in
+    let partial_ex = test_filter_ghost_args 3 in
     42
 
   let constant test_partial2 : int =