val return (a: Type) (x: a) : repr a (fun p s0 -> p (Success x) s0)
val return (a: Type) (x: a) : repr a (fun p s0 -> p (Success x) s0)
let return (a:Type) (x:a)
: repr a (fun p s0 -> p (Success x) s0)
= fun s0 -> Success x, s0
(*
   Copyright 2008-2018 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 MSeqExn

module W = FStar.Monotonic.Witnessed

/// This module provides a monotonic state + exception layered effect,
/// where state is a monotonic sequence of events


module Seq = FStar.Seq


/// The event type, it can be in any fixed universe

assume type event : Type u#1


/// An invariant that the monotonic sequence must maintain

assume type invariant (s:Seq.seq event) : Type0


/// state is a sequence of events that holds the invariant

type state = s:Seq.seq event{invariant s}


/// The result type for the exceptions

type result (a:Type) =
  | Success : a -> result a
  | Error   : string -> result a


/// The state grows monotonically

let grows : Preorder.preorder state =
  fun s1 s2 ->
  Seq.length s1 <= Seq.length s2 /\
  (forall (i:nat).{:pattern (Seq.index s1 i) \/ (Seq.index s2 i)}
            i < Seq.length s1 ==> Seq.index s1 i == Seq.index s2 i)


/// Now into the effect mechanics

type pre_t = state -> Type0
type post_t (a:Type) = result a -> state -> Type0
type wp_t0 (a:Type) = post_t a -> pre_t

unfold
let wpt_monotonic (#a:Type) (wp:wp_t0 a) =
  forall (p q:post_t a).
    (forall (r:result a) (s:state). p r s ==> q r s) ==>
    (forall (s:state). wp p s ==> wp q s)

type wp_t (a:Type) = wp:wp_t0 a{wpt_monotonic wp}

open FStar.Monotonic.Pure

let repr (a:Type) (wp:wp_t a) =
  s0:state ->
  PURE (result a & state)
    (as_pure_wp (fun p -> wp (fun x s1 -> grows s0 s1 ==> p (x, s1)) s0))
/
prims.fst.checked FStar.Seq.fst.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Witnessed.fsti.checked FStar.Monotonic.Pure.fst.checked
MSeqExn.fst
a: Type -> x: a -> MSeqExn.repr a (fun p s0 -> p (MSeqExn.Success x) s0)
MSeqExn.state FStar.Pervasives.Native.Mktuple2 MSeqExn.result MSeqExn.Success FStar.Pervasives.Native.tuple2 MSeqExn.repr
let return (a: Type) (x: a) : repr a (fun p s0 -> p (Success x) s0) =
  
fun s0 -> Success x, s0