Require Import Bool.
Require Import List.
Require Import String.
Require Import Map.

Set Implicit Arguments.
Unset Strict Implicit.


Section TYPEDVALUE_DEF.

Record typedvalue : Type := {type : Type; content : type}.

Inductive utopia : Set :=
    fan : utopia.

Definition undefinedtypedvalue := Build_typedvalue fan.

Definition eq_typedvalue := eq (A:=typedvalue).

Section PREDICATE_TYPEDVALUE_DEF.

Variable type1 : Type.
Variable type2 : Type.

Variable predicate1 : type1 -> Prop.

Definition predicate_typedvalue (tv : typedvalue) : Prop :=
  type tv = type1 /\
  (forall vr : type1, tv = Build_typedvalue vr -> predicate1 vr).

Variable predicate2 : type1 -> type2 -> Prop.

Definition predicate_type1_typedvalue2 (v1 : type1)
  (tv2 : typedvalue) : Prop :=
  type tv2 = type2 /\
  (forall v2 : type2, tv2 = Build_typedvalue v2 -> predicate2 v1 v2).

Definition predicate_typedvalue1_type2 (tv1 : typedvalue)
  (v2 : type2) : Prop :=
  type tv1 = type1 /\
  (forall v1 : type1, tv1 = Build_typedvalue v1 -> predicate2 v1 v2).

Definition predicate_typedvalue1_typedvalue2 (tv1 tv2 : typedvalue) : Prop :=
  type tv1 = type1 /\
  type tv2 = type2 /\
  (forall (v1 : type1) (v2 : type2),
   tv1 = Build_typedvalue v1 /\ tv2 = Build_typedvalue v2 -> predicate2 v1 v2).

End PREDICATE_TYPEDVALUE_DEF.

End TYPEDVALUE_DEF.


Section PVALUATION_DEF.

Definition pvaluation := map string typedvalue.

Definition emptypvaluation := null string typedvalue.

Definition pvalue := evaluate eq_string undefinedtypedvalue.

Definition pupdate :=
  refresh (Domain:=string) eq_string (Codomain:=typedvalue).

Definition prestrict := filter eq_string.

Definition eq_pvaluation :=
  eq_map eq_string eq_typedvalue undefinedtypedvalue.

Definition defined (pv : pvaluation) (v : string) :=
  pvalue pv v <> undefinedtypedvalue.

Definition is_type (pv : pvaluation) (v : string) (t : Type) :=
  type (pvalue pv v) = t.
End PVALUATION_DEF.