Module ErgoSpec.Backend.Qcert.QcertType

Require Import List.
Require Import ZArith.
Require Import EquivDec.
Require Import RelationClasses.
Require Import Equivalence.
Require Import String.

Require Import Qcert.Utils.Utils.
Require Import Qcert.Data.DataSystem.

Require Import QcertData.
Require Import QcertToSpark.

Import ListNotations.
Local Open Scope list_scope.
Local Open Scope string_scope.
Local Open Scope nstring_scope.


Inductive enhanced_type : Set :=
  | enhancedTop : enhanced_type
  | enhancedBottom : enhanced_type
  | enhancedString : enhanced_type
  | enhancedDateTimeFormat : enhanced_type
  | enhancedDateTime : enhanced_type
  | enhancedDateTimeDuration : enhanced_type
  | enhancedDateTimePeriod : enhanced_type
.

Definition enhanced_type_to_string (et:enhanced_type) : string :=
  match et with
  | enhancedTop => "ETop"
  | enhancedBottom => "EBottom"
  | enhancedString => "EString"
  | enhancedDateTimeFormat => "EDateTimeFormat"
  | enhancedDateTime => "EDateTime"
  | enhancedDateTimeDuration => "EDateTimeDuration"
  | enhancedDateTimePeriod => "EDateTimePeriod"
  end.

Definition string_to_enhanced_type (s:string) : option enhanced_type :=
  match s with
  | "ETop"%string => Some enhancedTop
  | "EBottom"%string => Some enhancedBottom
  | "EString"%string => Some enhancedString
  | "EDateTimeFormat"%string => Some enhancedDateTimeFormat
  | "EDateTime"%string => Some enhancedDateTime
  | "EDateTimeDuration"%string => Some enhancedDateTimeDuration
  | "EDateTimePeriod"%string => Some enhancedDateTimePeriod
  | _ => None
  end.

Definition enhanced_type_join (t1 t2:enhanced_type)
  := match t1, t2 with
     | enhancedBottom, _ => t2
     | _, enhancedBottom => t1
     | enhancedString, enhancedString => enhancedString
     | enhancedDateTimeFormat, enhancedDateTimeFormat => enhancedDateTimeFormat
     | enhancedDateTime, enhancedDateTime => enhancedDateTime
     | enhancedDateTimeDuration, enhancedDateTimeDuration => enhancedDateTimeDuration
     | enhancedDateTimePeriod, enhancedDateTimePeriod => enhancedDateTimePeriod
     | _, _ => enhancedTop
     end.

Definition enhanced_type_meet (t1 t2:enhanced_type)
  := match t1, t2 with
     | enhancedTop, _ => t2
     | _, enhancedTop => t1
     | enhancedString, enhancedString => enhancedString
     | enhancedDateTimeFormat, enhancedDateTimeFormat => enhancedDateTimeFormat
     | enhancedDateTime, enhancedDateTime => enhancedDateTime
     | enhancedDateTimeDuration, enhancedDateTimeDuration => enhancedDateTimeDuration
     | enhancedDateTimePeriod, enhancedDateTimePeriod => enhancedDateTimePeriod
     | _, _ => enhancedBottom
     end.

Inductive enhanced_subtype : enhanced_type -> enhanced_type -> Prop :=
| enhanced_subtype_top t : enhanced_subtype t enhancedTop
| enhanced_subtype_bottom t : enhanced_subtype enhancedBottom t
| enhanced_subtype_refl t : enhanced_subtype t t.

Instance enhanced_subtype_pre : PreOrder enhanced_subtype.

Instance enhanced_subtype_post : PartialOrder eq enhanced_subtype.

Instance enhanced_type_lattice : Lattice enhanced_type eq
  := {
      join := enhanced_type_join
      ; meet := enhanced_type_meet
    }.

Instance enhanced_type_olattice : OLattice eq enhanced_subtype.

Program Instance enhanced_foreign_type : foreign_type
  := mk_foreign_type enhanced_type _ _ _ _ _ _ _.