(* Copyright (c) 2017, the Dart project authors.  Please see the AUTHORS file
 * for details. All rights reserved. Use of this source code is governed by a
 * BSD-style license that can be found in the LICENSE file. *)

Require Export List.
Require Export Coq.FSets.FMapWeakList.
Require Export Coq.Structures.DecidableTypeEx.
Require Export Coq.Structures.Equalities.
Require Export Coq.Strings.String.
Require Import CpdtTactics.

(** * Auxiliary definitions. *)

(** Strings are used as keys in maps of getters, setters, and methods of
  interface types.  For maps we use the list-based unordered representation,
  because it only requires decidability on the domain of keys.  [String_as_MDT]
  and [String_as_UDT] below are auxiliary modules to define [StringMap]. *)

Module String_as_MDT.
  Definition t := string.
  Definition eq_dec := string_dec.
End String_as_MDT.

Module String_as_UDT := Equalities.Make_UDT(String_as_MDT).

(** [NatMap] is used to map type variables to type locations and to map type
  locations to type values. *)
Module NatMap := FMapWeakList.Make(Nat_as_DT).

(** [StringMap] is used to map identifiers to getters, setters, and methods. *)
Module StringMap := FMapWeakList.Make(String_as_UDT).

(* A "comp A" denotes a partial function that may not terminate on some inputs
   or terminate without an answer on others. *)
Module ComputationMonad.

  Definition comp (A : Type) := nat -> option A.

  Definition comp_return {A : Type} (a : A) : comp A := fun _ => Some a.
  Definition abort {A : Type} : comp A := fun _ => None.

  Definition comp_bind {A : Type} {B : Type} (x : comp A) (y : A -> comp B) : comp B :=
    fun n => match x n with None => None | Some a => y a n end.
  Definition comp_unsome {A : Type} (v : option A) : comp A := fun _ => v.

  Notation "[ x ]" := (comp_return x) (at level 0, x at level 200).
  Notation "[[ x ]]" := (comp_unsome x) (at level 0, x at level 99).
  Notation "x <- m1 ; m2" := (comp_bind m1 (fun x => m2)) (at level 70, right associativity).

  Fixpoint comp_fix' (A : Type) (B : Type) (f : (A -> comp B) -> (A -> comp B)) (a : A) (n : nat) {struct n} : option B :=
    match n with
    | O => None
    | (S n) => let rec := fun (a : A) => comp_unsome (comp_fix' _ _ f a n) in f rec a n
    end.

  Definition Fix {A : Type} {B : Type} (f : (A -> comp B) -> (A -> comp B)) : A -> comp B :=
    fun a => fun n => comp_fix' _ _ f a n.

  Module Continuity.

    Definition continuous {A: Type} (f: comp A) : Prop :=
      forall n k v, n <= k -> f n = Some v -> f k = Some v.

    Lemma return_cont {A: Type} : forall a : A, continuous (comp_return a).
      intros.
      unfold comp_return.
      unfold continuous.
      auto.
    Qed.

    Lemma abort_cont {A : Type} : continuous (@abort A).
      unfold abort.
      unfold continuous.
      auto.
    Qed.

  End Continuity.

End ComputationMonad.

Module OptionMonad.

  Notation "[ x ]" := (Some x) (at level 0, x at level 200).

  Definition opt_bind {A B} (x : option A) (f : A -> option B) : option B :=
    match x with
    | None => None
    | Some v => f v
    end.

  Notation "x <- m1 ; m2" := (opt_bind m1 (fun x => m2)) (at level 70, right associativity).

End OptionMonad.

Module ListExtensions.
  Import ComputationMonad.

  Fixpoint mmap {A B} (f : A -> comp B) (l : list A) : comp (list B) :=
    match l with
    | nil => [nil]
    | (x::xs) => (x' <- f x; xs' <- mmap f xs; [x' :: xs'])
    end.

End ListExtensions.