module Prims

(* logical connectives *)
type l_and :: E => E => P
type l_or  :: E => E => P
type l_not :: E => P
type l_iff :: E => E => P
type l_implies :: E => E => P
type Forall :: 'a::* => ('a => E) => E
type Exists :: 'a::* => ('a => E) => E
type ForallA :: 'a::A => ('a => E) => E
type ExistsA :: 'a::A => ('a => E) => E
type Relational :: E => E
type DoubleSided :: E => E
type True :: P
type False :: P
type EqTyp :: E => E => E
type Eq :: 'a::* => 'a => 'a => P
type Eq2 :: 'a::* => 'b::* => 'a => 'b => P
type EqA :: 'a::A => 'a => 'a => E

type NTuple =
  | Tuple_UU : 'a -> 'b -> ('a * 'b)
  | Tuple_UA : 'a::* -> 'b::A -> 'a -> 'b -> ('a * 'b) 
  | Tuple_AU : 'a::A -> 'b::* -> 'a -> 'b -> ('a * 'b)
  | Tuple_AA : 'a::A -> 'b::A -> 'a -> 'b -> ('a * 'b)

type pf  :: E => P  =
  | T                : pf True

type object
type bool
type unit
type int
type string
type bytes
logic val L : 'a -> 'a
logic val R : 'a -> 'a
val op_Equality : x:'a -> y:'a -> z:bool { z=true <=> x=y}

(* string operations *)
val concat : string -> string -> string

(* Integer arithmetic *)
logic val Add : int -> int -> int
logic val Sub : int -> int -> int
logic val Mul : int -> int -> int
logic val Div : int -> int -> int
logic val Minus : int -> int
logic val Modulo : int -> int -> int

type LT :: int => int => E
type GT :: int => int => E
type LTE :: int => int => E
type GTE :: int => int => E

val id : 'a::* -> 'a -> 'a
let id x = x

val idprop : 'a::P -> 'a -> 'a
let idprop x = x

val idint: int -> int
let idint x = id x

type option 'a = 
  | None : option 'a
  | Some : 'a -> option 'a

val bind_opt: ('a -> 'b) -> option 'a -> option 'b
let bind_opt f x = match x with
  | None -> None
  | Some x -> Some (f x)
  
type list 'a = 
  | Nil : list 'a
  | Cons : 'a -> list 'a -> list 'a

type In :: 'a::* => 'a => list 'a => P
type ListUnion :: 'a::* => list 'a => list 'a => list 'a => P
assume In_hd: forall (hd:'a) (tl:list 'a). (In hd (Cons hd tl))
assume In_tl: forall (hd:'a) (x:'a) (tl:list 'a). (In x tl) => (In x (Cons hd tl))
assume notinNil: forall (x:'a). not (In x Nil)
assume notinCons: forall (x:'a) (y:'a) (tl:list 'a). ((not (In x tl)) && (not (x=y))) => not (In x (Cons y tl))

(* Work around inexistence of || *)
val logor : bool -> bool -> bool
let logor a b = match a with
  | true -> true
  | false -> b

val elem : 'a -> list 'a -> bool
let rec elem a xs = match xs with
  | Nil -> false
  | Cons hd tl -> logor (a = hd) (elem a tl)

val fold_left: ('a -> 'b -> 'a) -> 'a -> list 'b -> 'a
let rec fold_left f x y = match y with
  | Nil -> x
  | Cons hd tl -> fold_left f (f x hd) tl

val fold_right: ('a -> 'b -> 'b) -> list 'a -> 'b -> 'b
let rec fold_right f l x = match l with
  | Nil -> x
  | Cons hd tl -> fold_right f tl (f hd x)

val iterate: ('a -> unit) -> list 'a -> unit
let rec iterate f x = match x with
  | Nil -> ()
  | Cons a tl -> let _ = f a in iterate f tl
                                  
val append: x:list 'a -> y:list 'a -> z:list 'a { forall (a:'a). In a z <=> (In a x || In a y)}
let rec append x y = match x with
  | Nil -> y
  | Cons a tl -> Cons a (append tl y)

val concatMap: ('a -> list 'b) -> list 'a -> list 'b
let rec concatMap f = function
  | [] -> []
  | a::tl -> append (f a) (concatMap f tl)

extern reference FStar { language = "JavaScript";
       		       	 dll="";
			 namespace="window";
			 classname="" }

type jspair :: * => * => *
extern FStar val mkPair : 'a -> 'b -> jspair 'a 'b
extern FStar val app : (jspair 'a 'b -> 'c) -> jspair 'a 'b -> 'c
extern FStar val fstPair : jspair 'a 'b -> 'a
extern FStar val sndPair : jspair 'a 'b -> 'b

extern FStar val failwith : string -> 'a
extern FStar val deleteFromWindow : string -> unit
extern FStar val exportToWindow : string -> 'a -> unit
extern FStar val around : string -> 'a -> unit
extern FStar val around2 : string -> 'a -> unit

extern FStar val random_string : unit -> string

type ref :: * => *
extern FStar val initRef : 'a -> ref 'a
extern FStar val getRef : ref 'a -> 'a
extern FStar val setRef : ref 'a -> 'a -> unit



extern reference Window {language = "JavaScript";
                         dll="";
                         namespace="window"; 
                         classname=""}


extern reference Dom { language = "JavaScript";
                       dll="";
                       namespace="window";
                       classname="document"}


extern Dom type DOMElement
extern Dom val body : DOMElement

extern Window val raw_getInnerHTML : string -> string
extern Window val raw_setInnerHTML : string -> string -> unit

extern Window val alert : 'a -> unit
extern Window val jsopen : string -> unit

extern Window val setInterval : jspair (unit -> unit) int -> unit
extern Window val setTimeout : jspair (unit -> unit) int -> unit

extern Window val postMessage : jspair string string -> unit


extern Window val createElement : string -> DOMElement
extern Window val getElementNodeName : DOMElement -> string

(* localStorage API *)

extern reference LocalStorage { language = "JavaScript";
                       dll="";
                       namespace="window";
                       classname="localStorage"}


extern LocalStorage val setItem : jspair string string -> unit
extern LocalStorage val getItem : string -> string
extern LocalStorage val removeItem : string -> unit
extern LocalStorage val clear : unit -> unit
extern LocalStorage val key : int -> string
extern LocalStorage val length : unit -> int



val map: ('a -> 'b) -> list 'a -> list 'b
let rec map f x = match x with
  | Nil -> Nil
  | Cons a tl -> 
      let b = f a in 
        alert(a); 
        alert("mapped to"); 
        alert(b);
        Cons b (map f tl)

val _dummy_op_Dereference : ref 'a -> 'a

(* Primitive functions with trusted specs for concrete refinements *)
val _dummy_op_AmpAmp             : bool -> bool -> bool
val _dummy_op_BarBar             : bool -> bool -> bool
val _dummy_op_Negation           : bool -> bool

val _dummy_op_Multiply           : int -> int -> int
val _dummy_op_Division           : int -> int -> int
val _dummy_op_Subtraction        : int -> int -> int
val _dummy_op_Addition           : int -> int -> int
val _dummy_op_Minus              : int -> int
val _dummy_op_Modulus            : int -> int -> int

val _dummy_op_GreaterThanOrEqual : int -> int -> bool
val _dummy_op_LessThanOrEqual : int -> int -> bool
val _dummy_op_GreaterThan : int -> int -> bool
val _dummy_op_LessThan : int -> int -> bool