fstar 2025.02.17 · OCaml Package

val is_in : Prims.unit -> FStar_Monotonic_HyperHeap.hmap -> Prims.bool

val is_heap_color : Prims.int -> Prims.bool

type sid = Prims.unit

type 'm map_invariant_predicate = Prims.unit

type 'h downward_closed_predicate = Prims.unit

type ('tip, 'h) tip_top_predicate = Prims.unit

type ('h, 'n) rid_ctr_pred_predicate = Prims.unit

type 'm map_invariant = Prims.unit

type 'h downward_closed = Prims.unit

type ('tip, 'h) tip_top = Prims.unit

type ('h, 'n) rid_ctr_pred = Prims.unit

type ('tip, 'h) is_tip = Prims.unit

type ('h, 'ctr, 'tip) is_wf_with_ctr_and_tip = Prims.unit

type mem' =

| HS of Prims.int * FStar_Monotonic_HyperHeap.hmap * Prims.unit

val uu___is_HS : mem' -> Prims.bool

val __proj__HS__item__rid_ctr : mem' -> Prims.int

val __proj__HS__item__h : mem' -> FStar_Monotonic_HyperHeap.hmap

val mk_mem : Prims.int -> FStar_Monotonic_HyperHeap.hmap -> Prims.unit -> mem'

val get_hmap : mem' -> FStar_Monotonic_HyperHeap.hmap

val get_rid_ctr : mem' -> Prims.int

type mem = mem'

val empty_mem : mem

type 'm poppable = Prims.unit

val remove_elt : 'a FStar_Set.set -> 'a -> 'a FStar_Set.set

type ('m0, 'm1) popped = Prims.unit

val pop : mem -> mem

type (!'a, !'rel) mreference' =

| MkRef of Prims.unit * ('a, 'rel) FStar_Monotonic_Heap.mref

val uu___is_MkRef : ('a, 'rel) mreference' -> Prims.bool

val __proj__MkRef__item__ref : 
  ('a, 'rel) mreference' ->
  ('a, 'rel) FStar_Monotonic_Heap.mref

type (!'a, !'rel) mreference = ('a, 'rel) mreference'

val mk_mreference : 
  Prims.unit ->
  'a FStar_Monotonic_Heap.ref ->
  ('a, 'rel) mreference

val as_ref : 
  ('uuuuu, 'uuuuu1) mreference ->
  ('uuuuu, 'uuuuu1) FStar_Monotonic_Heap.mref

type (!'a, !'rel) mstackref = ('a, 'rel) mreference

type (!'a, !'rel) mref = ('a, 'rel) mreference

type (!'a, !'rel) mmmstackref = ('a, 'rel) mreference

type (!'a, !'rel) mmmref = ('a, 'rel) mreference

type ('i, !'a, !'rel) s_mref = ('a, 'rel) mreference

val live_region : mem -> Prims.unit -> Prims.bool

type ('a, 'rel, 'm, 's) contains = Prims.unit

type ('a, 'rel, 'r, 'm) unused_in = Prims.unit

type ('a, 'rel, 'm, 'r) contains_ref_in_its_region =
  ('a, 'rel, Prims.unit, Prims.unit) FStar_Monotonic_Heap.contains

type ('a, 'rel, 'r, 'm0, 'm1) fresh_ref = Prims.unit

type ('i, 'm0, 'm1) fresh_region = Prims.unit

val alloc : 
  Prims.unit ->
  'a ->
  Prims.bool ->
  mem ->
  ('a, 'rel) mreference * mem

val free : ('a, 'rel) mreference -> mem -> mem

val upd_tot : mem -> ('a, 'rel) mreference -> 'a -> mem

val sel_tot : mem -> ('a, 'rel) mreference -> 'a

type ('m0, 'm1) fresh_frame = Prims.unit

val hs_push_frame : mem -> mem

val new_eternal_region : 
  mem ->
  Prims.unit ->
  Prims.int FStar_Pervasives_Native.option ->
  Prims.unit * mem

val new_freeable_heap_region : mem -> Prims.unit -> Prims.unit * mem

val free_heap_region : mem -> Prims.unit -> mem

type ('s, 'm0, 'm1) modifies = Prims.unit

type ('s, 'm0, 'm1) modifies_transitively = Prims.unit

type 'm0 heap_only = Prims.unit

val top_frame : mem -> FStar_Monotonic_Heap.heap

type ('id, 'h0, 'h1) modifies_one = Prims.unit

type ('id, 's, 'h0, 'h1) modifies_ref = Prims.unit

type some_ref =

| Ref of Prims.unit * Prims.unit * (Obj.t, Obj.t) mreference

val uu___is_Ref : some_ref -> Prims.bool

val __proj__Ref__item___2 : some_ref -> (Prims.unit, Prims.unit) mreference

type some_refs = some_ref Prims.list

val regions_of_some_refs : some_refs -> Prims.unit FStar_Set.set

type ('i, 'rs, 'h0, 'h1) modifies_some_refs = Obj.t

val norm_steps : FStar_NormSteps.norm_step Prims.list

type ('rs, 'h0, 'h1) mods = Prims.unit

type aref =

| ARef of Prims.unit * FStar_Monotonic_Heap.aref

val uu___is_ARef : aref -> Prims.bool

val __proj__ARef__item__aref_aref : aref -> FStar_Monotonic_Heap.aref

val dummy_aref : aref

val aref_of : ('uuuuu, 'uuuuu1) mreference -> aref

type ('a, 'h) aref_unused_in = Prims.unit

type ('h, 'a, 'v, 'rel) aref_live_at = Prims.unit

val reference_of : 
  mem ->
  aref ->
  Prims.unit ->
  Prims.unit ->
  (Obj.t, Obj.t) mreference

package fstar