let pure_wp_monotonic = pure_wp_monotonic0
let pure_wp_monotonic =
pure_wp_monotonic0
prims.fst.checked
prims.fst
Prims.pure_wp_monotonic0
(*
   Copyright 2008-2020 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 Prims

/// This module is implicitly opened in the scope of all other modules.
///
/// It provides the very basic primitives on which F* is
/// built, including the definition of total functions, the basic
/// logical connectives, the PURE and GHOST effects and the like.
///
/// While some of the primitives have logical significance, others are
/// define various conveniences in the language, e.g., type of
/// attributes.


(***** Begin trusted primitives *****)

(** Primitives up to the definition of the GTot effect are trusted
    Beyond that all definitions are fully verified *)


(** Type of attributes *)
assume new
type attribute : Type0 

(** An attribute indicating that some definition must be processed by the
    Dijkstra monads for free construction *)
assume
val cps:attribute

(** A predicate to express when a type supports decidable equality
    The type-checker emits axioms for [hasEq] for each inductive type *)
assume
type hasEq : Type -> GTot Type0 

(** A convenient abbreviation, [eqtype] is the type of types in
    universe 0 which support decidable equality *)
type eqtype = a: Type0{hasEq a}

(** [bool] is a two element type with elements [true] and [false]. We
    assume it is primitive, for convenient interop with other
    languages, although it could easily be defined as an inductive type
    with two cases, [BTrue | BFalse] *)
assume new
type bool : eqtype 

(** [empty] is the empty inductive type. The type with no
    inhabitants represents logical falsehood. Note, [empty] is
    seldom used directly in F*. We instead use its "squashed" variant,
    [False], see below. *)
type empty = 

(** [trivial] is the singleton inductive type---it is trivially
    inhabited. Like [empty], [trivial] is seldom used. We instead use
    its "squashed" variants, [True] *)
type trivial = | T

(** [unit]: another singleton type, with its only inhabitant written [()]
    we assume it is primitive, for convenient interop with other languages *)
assume new
type unit : eqtype

(** [squash p] is a central type in F*---[squash p] is the proof
    irrelevant analog of [p] and is represented as a unit
    refinement. Squashed proofs are typically discharged using an SMT
    solver, without any proof terms explicitly reconstructed. As
    such, one way to think of [squash p] is as the type of properties
    proven using classical axioms without building proof terms.

    Note, [squash p] is just a unit refinement, it resides in universe
    0, lowering the universe of [p]. From this perspective, one may
    also see [squash] as a coercion down to universe 0.

    The type is marked [tac_opaque] to indicate to Meta-F* that
    instances of [squash] should not be unfolded when evaluating
    tactics (since many optimizations in F*'s SMT encoding rely
    specifically on occurrences of [squash].

    See FStar.Squash for various ways of manipulating squashed
    types. *)
[@@ "tac_opaque"]
type squash (p: Type) : Type0 = x: unit{p}

(** [auto_squash] is equivalent to [squash]. However, F* will
    automatically insert `auto_squash` when simplifying terms,
    converting terms of the form `p /\ True` to `auto_squash p`.

    We distinguish these automatically inserted squashes from explicit,
    user-written squashes.

    A user should not have to manipulate [auto_squash] at all, except
    in rare circumstances when writing tactics to process proofs that
    have already been partially simplified by F*'s simplifier.
*)
let auto_squash (p: Type) = squash p

(** The [logical] type is transitionary. It is just an abbreviation
    for [Type0], but is used to classify uses of the basic squashed
    logical connectives that follow. Some day, we plan to remove the
    [logical] type, replacing it with [prop] (also defined below).

    The type is marked [private] to intentionally prevent user code
    from referencing this type, hopefully easing the removal of
    [logical] in the future. *)
private
type logical = Type0

(** An attribute indicating that a symbol is an smt theory symbol and
    hence may not be used in smt patterns.  The typechecker warns if
    such symbols are used in patterns *)
assume
val smt_theory_symbol:attribute

(** [l_True] has a special bit of syntactic sugar. It is written just
    as "True" and rendered in the ide as [True]. It is a squashed version
    of constructive truth, [trivial]. *)
[@@ "tac_opaque"; smt_theory_symbol]
let l_True:logical = squash trivial

(** [l_False] has a special bit of syntactic sugar. It is written just
    as "False" and rendered in the ide as [Falsee]. It is a squashed version
    of constructive falsehood, the empty type. *)
[@@ "tac_opaque"; smt_theory_symbol]
let l_False:logical = squash empty

(** The type of provable equalities, defined as the usual inductive
    type with a single constructor for reflexivity.  As with the other
    connectives, we often work instead with the squashed version of
    equality, below. *)
type equals (#a: Type) (x: a) : a -> Type = | Refl : equals x x

(** [eq2] is the squashed version of [equals]. It's a proof
   irrelevant, homogeneous equality in Type#0 and is written with
   an infix binary [==].

   TODO: instead of hard-wiring the == syntax,
         we should just rename eq2 to op_Equals_Equals
*)
[@@ "tac_opaque"; smt_theory_symbol]
type eq2 (#a: Type) (x: a) (y: a) : logical = squash (equals x y)

(** bool-to-type coercion: This is often automatically inserted type,
    when using a boolean in context expecting a type. But,
    occasionally, one may have to write [b2t] explicitly *)
type b2t (b: bool) : logical = (b == true)

(** constructive conjunction *)
type pair (p: Type) (q: Type) = | Pair : _1:p -> _2:q -> pair p q

(** squashed conjunction, specialized to [Type0], written with an
    infix binary [/\] *)
[@@ "tac_opaque"; smt_theory_symbol]
type l_and (p: logical) (q: logical) : logical = squash (pair p q)

(** constructive disjunction *)
type sum (p: Type) (q: Type) =
  | Left : v:p -> sum p q
  | Right : v:q -> sum p q

(** squashed disjunction, specialized to [Type0], written with an
    infix binary [\/] *)
[@@ "tac_opaque"; smt_theory_symbol]
type l_or (p: logical) (q: logical) : logical = squash (sum p q)

(** squashed (non-dependent) implication, specialized to [Type0],
    written with an infix binary [==>]. Note, [==>] binds weaker than
    [/\] and [\/] *)
[@@ "tac_opaque"; smt_theory_symbol]
type l_imp (p: logical) (q: logical) : logical = squash (p -> GTot q)
(* ^^^ NB: The GTot effect is primitive;            *)
(*         elaborated using GHOST a few lines below *)

(** squashed double implication, infix binary [<==>] *)
[@@ smt_theory_symbol]
type l_iff (p: logical) (q: logical) : logical = (p ==> q) /\ (q ==> p)

(** squashed negation, prefix unary [~] *)
[@@ smt_theory_symbol]
type l_not (p: logical) : logical = l_imp p False

(** l_ITE is a weak form of if-then-else at the level of
    logical formulae. It's not much used.

    TODO: Can we remove it *)
unfold
type l_ITE (p: logical) (q: logical) (r: logical) : logical = (p ==> q) /\ (~p ==> r)


(** One of the main axioms provided by prims is [precedes], a
    built-in well-founded partial order over all terms. It's typically
    written with an infix binary [<<].

    The [<<] order includes:
        * The [<] ordering on natural numbers
        * The subterm ordering on inductive types
        * [f x << D f] for data constructors D of an inductive t whose
          arguments include a ghost or total function returning a t *)

assume
type precedes : #a: Type -> #b: Type -> a -> b -> Type0

(** The type of primitive strings of characters; See FStar.String *)
assume new
type string : eqtype 

(** This attribute can be added to the declaration or definition of
    any top-level symbol. It causes F* to report a warning on any
    use of that symbol, printing the [msg] argument.
    
    This is used, for instance to:
    
    - tag every escape hatch, e.g., [assume], [admit], etc

    Reports for uses of symbols tagged with this attribute
    are controlled using the `--report_assumes` option
    and warning number 334. 
    
    See tests/micro-benchmarks/WarnOnUse.fst
 *)
assume
val warn_on_use (msg: string) : Tot unit

(** The [deprecated "s"] attribute: "s" is an alternative function
    that should be printed in the warning it can be omitted if the use
    case has no such function *)
assume
val deprecated (s: string) : Tot unit


(** Within the SMT encoding, we have a relation [(HasType e t)]
    asserting that (the encoding of) [e] has a type corresponding to
    (the encoding of) [t].

    It is sometimes convenient, e.g., when writing triggers for
    quantifiers, to have access to this relation at the source
    level. The [has_type] predicate below reflects the SMT encodings
    [HasType] relation. We also use it to define the type [prop] or
    proof irrelevant propositions, below.

    Note, unless you have a really good reason, you probably don't
    want to use this [has_type] predicate. F*'s type theory certainly
    does not internalize its own typing judgment *)
[@@deprecated "'has_type' is intended for internal use and debugging purposes only; \
                do not rely on it for your proofs"]
assume
type has_type : #a: Type -> a -> Type -> Type0 

(** Squashed universal quantification, or dependent products, written
    [forall (x:a). p x], specialized to Type0 *)
[@@ "tac_opaque"; smt_theory_symbol]
type l_Forall (#a: Type) (p: (a -> GTot Type0)) : logical = squash (x: a -> GTot (p x))

#push-options "--warn_error -288" 
(** [p1 `subtype_of` p2] when every element of [p1] is also an element
    of [p2]. *)
let subtype_of (p1 p2: Type) = forall (x: p1). has_type x p2
#pop-options

(** The type of squashed types.

    Note, the [prop] type is a work in progress in F*. In particular,
    we would like in the future to more systematically use [prop] for
    proof-irrelevant propositions throughout the libraries. However,
    we still use [Type0] in many places. 

    See https://github.com/FStarLang/FStar/issues/1048 for more
    details and the current status of the work.
    *)
type prop = a: Type0{a `subtype_of` unit}

(**** The PURE effect *)

(** The type of pure preconditions *)
let pure_pre = Type0

(** Pure postconditions, predicates on [a], on which the precondition
    [pre] is also valid. This provides a way for postcondition formula
    to be typed in a context where they can assume the validity of the
    precondition. This is discussed extensively in Issue #57 *)
let pure_post' (a pre: Type) = _: a{pre} -> GTot Type0
let pure_post (a: Type) = pure_post' a True

(** A pure weakest precondition transforms postconditions on [a]-typed
    results to pure preconditions

    We require the weakest preconditions to satisfy the monotonicity
    property over the postconditions
    To enforce it, we first define a vanilla wp type,
    and then refine it with the monotonicity condition *)
let pure_wp' (a: Type) = pure_post a -> GTot pure_pre

(** The monotonicity predicate is marked opaque_to_smt,
    meaning that its definition is hidden from the SMT solver,
    and if required, will need to be explicitly revealed
    This has the advantage that clients that do not need to work with it
    directly, don't have the (quantified) definition in their solver context *)

let pure_wp_monotonic0 (a:Type) (wp:pure_wp' a) =
  forall (p q:pure_post a). (forall (x:a). p x ==> q x) ==> (wp p ==> wp q)
val pure_wp_monotonic : a: Type -> wp: Prims.pure_wp' a -> Prims.logical
a: Type -> wp: Prims.pure_wp' a -> Prims.logical