Module ErgoSpec.Backend.Qcert.QcertDataTyping

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.JSON.JSONSystem.
Require Import Qcert.Data.DataSystem.

Require Import Qcert.Compiler.Component.UriComponent.
Require Import LogComponent.
Require Import MathComponent.
Require Import DateTimeComponent.

Require Import QcertData.
Require Import QcertType.

Inductive enhanced_has_type : enhanced_data -> enhanced_type -> Prop :=
| enhanced_has_type_top fd : enhanced_has_type fd enhancedTop
| enhanced_has_type_dateTimeFormat (tp:DATE_TIME_FORMAT) : enhanced_has_type (enhanceddateTimeformat tp) enhancedDateTimeFormat
| enhanced_has_type_dateTime (tp:DATE_TIME) : enhanced_has_type (enhanceddateTime tp) enhancedDateTime
| enhanced_has_type_dateTimeduration (tp:DATE_TIME_DURATION) : enhanced_has_type (enhanceddateTimeduration tp) enhancedDateTimeDuration
| enhanced_has_type_dateTimeperiod (tp:DATE_TIME_PERIOD) : enhanced_has_type (enhanceddateTimeperiod tp) enhancedDateTimePeriod
.

Definition enhanced_infer_type (d:enhanced_data) : option enhanced_type
  := match d with
     | enhanceddateTimeformat _ => Some enhancedDateTimeFormat
     | enhanceddateTime _ => Some enhancedDateTime
     | enhanceddateTimeduration _ => Some enhancedDateTimeDuration
     | enhanceddateTimeperiod _ => Some enhancedDateTimePeriod
     end.

Program Instance enhanced_foreign_data_typing :
  @foreign_data_typing enhanced_foreign_data enhanced_foreign_type
  := mk_foreign_data_typing
       enhanced_foreign_data
       enhanced_foreign_type
       enhanced_has_type _ _ _
       enhanced_infer_type _ _ _
.