val elift1_p
      (#a #b: Type)
      (#p: (a -> Type))
      ($f: (x: a{p x} -> GTot b))
      (r: erased a {p (reveal r)})
    : Tot (z: erased b {reveal z == f (reveal r)})
let elift1_p
      (#a #b: Type)
      (#p: (a -> Type))
      ($f: (x: a{p x} -> GTot b))
      (r: erased a {p (reveal r)})
    : Tot (z: erased b {reveal z == f (reveal r)}) =
  let x:(x: a{p x}) = reveal r in
  return (f x)
val elift1_p
      (#a #b: Type)
      (#p: (a -> Type))
      ($f: (x: a{p x} -> GTot b))
      (r: erased a {p (reveal r)})
    : Tot (z: erased b {reveal z == f (reveal r)})
let elift1_p
      (#a #b: Type)
      (#p: (a -> Type))
      ($f: (x: a{p x} -> GTot b))
      (r: erased a {p (reveal r)})
    : Tot (z: erased b {reveal z == f (reveal r)}) =
let x:(x: a{p x}) = reveal r in
return (f x)
FStar.Ghost.fsti.checked
prims.fst.checked FStar.Pervasives.fsti.checked
FStar.Ghost.fsti
FStar.Ghost.erased FStar.Ghost.reveal FStar.Ghost.return Prims.eq2
(*
   Copyright 2008-2014 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module FStar.Ghost

/// This module provides an erased type to abstract computationally
/// irrelevant values.
///
/// It relies on the GHOST effect defined in Prims.
///
/// [erased a] is decorated with the erasable attribute. As such,
///
///    1. The type is considered non-informative.
///
///       So, [Ghost (erased a)] can be subsumed to [Pure (erased a)]
///
///    2. The compiler extracts [erased a] to [unit]
///
///       The type is [erased a] is in a bijection with [a], as
///       witnessed by the [hide] and [reveal] function.
///
/// Importantly, computationally relevant code cannot use [reveal]
/// (it's marked [GTot])
///
/// Just like Coq's prop, it is okay to use erased types
/// freely as long as we produce an erased type.
///
/// [reveal] and [hide] are coercions: the typechecker will
/// automatically insert them when required. That is, if the type of
/// an expression is [erased X], and the expected type is NOT an
/// [erased Y], it will insert [reveal], and vice versa for [hide].

(** [erased t] is the computationally irrelevant counterpart of [t] *)
[@@ erasable]
new
val erased ([@@@strictly_positive] a: Type u#a) : Type u#a

(** [erased t] is in a bijection with [t], as witnessed by [reveal]
    and [hide] *)
val reveal: #a: Type u#a -> erased a -> GTot a

val hide: #a: Type u#a -> a -> Tot (erased a)

val hide_reveal (#a: Type) (x: erased a)
    : Lemma (ensures (hide (reveal x) == x)) [SMTPat (reveal x)]

val reveal_hide (#a: Type) (x: a) : Lemma (ensures (reveal (hide x) == x)) [SMTPat (hide x)]


/// The rest of this module includes several well-defined defined
/// notions. They are not trusted.

(** [Tot] is a sub-effect of [GTot] F* will usually subsume [Tot]
    computations to [GTot] computations, though, occasionally, it may
    be useful to apply this coercion explicitly. *)
let tot_to_gtot (f: ('a -> Tot 'b)) (x: 'a) : GTot 'b = f x

(** [erased]: Injecting a value into [erased]; just an alias of [hide] *)
let return (#a: Type) (x: a) : erased a = hide x

(** Sequential composition of erased *)
let bind (#a #b: Type) (x: erased a) (f: (a -> Tot (erased b))) : Tot (erased b) =
  let y = reveal x in
  f y

unfold
let (let@) (x:erased 'a) (f:('a -> Tot (erased 'b))) : Tot (erased 'b) = bind x f

(** Unary map *)
irreducible
let elift1 (#a #b: Type) (f: (a -> GTot b)) (x: erased a)
    : Tot (y: erased b {reveal y == f (reveal x)}) =
  let@ xx = x in return (f xx)

(** Binary map *)
irreducible
let elift2 (#a #b #c: Type) (f: (a -> b -> GTot c)) (x: erased a) (y: erased b)
    : Tot (z: erased c {reveal z == f (reveal x) (reveal y)}) =
  let@ xx = x in
  let@ yy = y in
  return (f xx yy)

(** Ternary map *)
irreducible
let elift3
      (#a #b #c #d: Type)
      (f: (a -> b -> c -> GTot d))
      (ga: erased a)
      (gb: erased b)
      (gc: erased c)
    : Tot (gd: erased d {reveal gd == f (reveal ga) (reveal gb) (reveal gc)}) =
  let@ a = ga in
  let@ b = gb in
  let@ c = gc in
  return (f a b c)

(** Pushing a refinement type under the [erased] constructor *)
let push_refinement #a (#p: (a -> Type0)) (r: erased a {p (reveal r)})
    : erased (x: a{p x /\ x == reveal r}) =
  let x:(x: a{p x}) = reveal r in
  return x

(** Mapping a function with a refined domain over a refined erased value *)
irreducible
let elift1_p
      (#a #b: Type)
      (#p: (a -> Type))
      ($f: (x: a{p x} -> GTot b))
val elift1_p
      (#a #b: Type)
      (#p: (a -> Type))
      ($f: (x: a{p x} -> GTot b))
      (r: erased a {p (reveal r)})
    : Tot (z: erased b {reveal z == f (reveal r)})
$f: (x: a{p x} -> Prims.GTot b) -> r: FStar.Ghost.erased a {p (FStar.Ghost.reveal r)}
  -> z: FStar.Ghost.erased b {FStar.Ghost.reveal z == f (FStar.Ghost.reveal r)}