(feature) StartOf/EndOf support for DateTime

Signed-off-by: Jerome Simeon <[email protected]>

backends/javascript/ergo-runtime.js

@@ -224,6 +224,9 @@ function toStringQ(v, quote) {
         }
         return result + "]";
     }
+    if (v.hasOwnProperty('_isAMomentObject')) {
+        return v.format();
+    }
     if(v.hasOwnProperty('nat')){
         return "" + v.nat;
     }
@@ -547,7 +550,7 @@ function dateTimeComponent(part, date) {
     date = mustBeDate(date);
     switch(part) {
     case DAY:
-        return date.dayOfMonth();
+        return date.date();
     case MONTH:
         return date.month();
     case YEAR:
@@ -672,3 +675,15 @@ function mustBeUnit(unit) {
 	      return;
     throw new Error("Expected a duration unit but got " + JSON.stringify(unit));
 }
+
+function dateTimeStartOf(part, date) {
+    date = mustBeDate(date);
+    mustBeUnit(part);
+    return date.startOf(part);
+}
+
+function dateTimeEndOf(part, date) {
+    date = mustBeDate(date);
+    mustBeUnit(part);
+    return date.endOf(part);
+}

extraction/src/DateTime.ml

@@ -113,3 +113,13 @@ let dseconds (x1:dateTime) (x2:dateTime) : float =
 let plus (x1:dateTime) (d1:duration) : dateTime = Calendar.add x1 d1
 let minus (x1:dateTime) (d1:duration) : dateTime = Calendar.rem x1 d1
 
+let start_of_day (x1:dateTime) = raise Not_found
+let start_of_month (x1:dateTime) = raise Not_found
+let start_of_quarter (x1:dateTime) = raise Not_found
+let start_of_year (x1:dateTime) = raise Not_found
+
+let end_of_day (x1:dateTime) = raise Not_found
+let end_of_month (x1:dateTime) = raise Not_found
+let end_of_quarter (x1:dateTime) = raise Not_found
+let end_of_year (x1:dateTime) = raise Not_found
+

extraction/stdlib/stdlib.ergo

@@ -10,10 +10,22 @@ define concept Duration {
 define function now() : DateTime
 define function dateTime(x:String) : DateTime
 
-define function dateTimeDayOfMonth(x:DateTime) : Double
-define function dateTimeMonth(x:DateTime) : Double
-define function dateTimeQuarter(x:DateTime) : Double
-define function dateTimeYear(x:DateTime) : Double
+define function dateTimeDayOfMonth(x:DateTime) : Integer
+define function dateTimeMonth(x:DateTime) : Integer
+define function dateTimeQuarter(x:DateTime) : Integer
+define function dateTimeYear(x:DateTime) : Integer
+
+define enum DateTimeComponent {
+	DAY, MONTH, QUARTER, YEAR
+}
+
+define function dateTimeComponent(x:DateTime, y:DateTimeComponent) : Integer {
+	match y
+	with "DAY" then return dateTimeDayOfMonth(x)
+	with "MONTH" then return dateTimeMonth(x)
+	with "QUARTER" then return dateTimeQuarter(x)
+	else return dateTimeYear(x)
+}
 
 define function dateTimeIsAfter(x:DateTime, y:DateTime) : Boolean
 define function dateTimeIsBefore(x:DateTime, y:DateTime) : Boolean
@@ -26,8 +38,31 @@ define function dateTimeDiff(x:DateTime, y:DateTime) : Duration
 define function dateTimeDiffDays(x:DateTime, y:DateTime) : Double
 define function dateTimeDiffSeconds(x:DateTime, y:DateTime) : Double
 
-define function min(x:Double[]) : Double
-define function count(x:Double[]) : Integer
+define function dateTimeStartOfDayOfMonth(x:DateTime) : DateTime
+define function dateTimeStartOfMonth(x:DateTime) : DateTime
+define function dateTimeStartOfQuarter(x:DateTime) : DateTime
+define function dateTimeStartOfYear(x:DateTime) : DateTime
+
+define function dateTimeStartOf(x:DateTime, y:DateTimeComponent) : DateTime {
+	match y
+	with "DAY" then return dateTimeStartOfDayOfMonth(x)
+	with "MONTH" then return dateTimeStartOfMonth(x)
+	with "QUARTER" then return dateTimeStartOfQuarter(x)
+	else return dateTimeStartOfYear(x)
+}
+
+define function dateTimeEndOfDayOfMonth(x:DateTime) : DateTime
+define function dateTimeEndOfMonth(x:DateTime) : DateTime
+define function dateTimeEndOfQuarter(x:DateTime) : DateTime
+define function dateTimeEndOfYear(x:DateTime) : DateTime
+
+define function dateTimeEndOf(x:DateTime, y:DateTimeComponent) : DateTime {
+	match y
+	with "DAY" then return dateTimeEndOfDayOfMonth(x)
+	with "MONTH" then return dateTimeEndOfMonth(x)
+	with "QUARTER" then return dateTimeEndOfQuarter(x)
+	else return dateTimeEndOfYear(x)
+}
 
 // Integer operations
 define function integerAbs(x:Integer) : Integer

mechanization/Backend/Model/DateTimeModelPart.v

@@ -149,6 +149,30 @@ Extract Inlined Constant DATE_TIME_quarter => "(fun x -> DateTime.quarter x)".
 Axiom DATE_TIME_year : DATE_TIME -> Z.
 Extract Inlined Constant DATE_TIME_year => "(fun x -> DateTime.year x)".
 
+Axiom DATE_TIME_start_of_day : DATE_TIME -> DATE_TIME.
+Extract Inlined Constant DATE_TIME_start_of_day => "(fun x -> DateTime.start_of_day x)".
+
+Axiom DATE_TIME_start_of_month : DATE_TIME -> DATE_TIME.
+Extract Inlined Constant DATE_TIME_start_of_month => "(fun x -> DateTime.start_of_month x)".
+
+Axiom DATE_TIME_start_of_quarter : DATE_TIME -> DATE_TIME.
+Extract Inlined Constant DATE_TIME_start_of_quarter => "(fun x -> DateTime.start_of_quarter x)".
+
+Axiom DATE_TIME_start_of_year : DATE_TIME -> DATE_TIME.
+Extract Inlined Constant DATE_TIME_start_of_year => "(fun x -> DateTime.start_of_year x)".
+
+Axiom DATE_TIME_end_of_day : DATE_TIME -> DATE_TIME.
+Extract Inlined Constant DATE_TIME_end_of_day => "(fun x -> DateTime.end_of_day x)".
+
+Axiom DATE_TIME_end_of_month : DATE_TIME -> DATE_TIME.
+Extract Inlined Constant DATE_TIME_end_of_month => "(fun x -> DateTime.end_of_month x)".
+
+Axiom DATE_TIME_end_of_quarter : DATE_TIME -> DATE_TIME.
+Extract Inlined Constant DATE_TIME_end_of_quarter => "(fun x -> DateTime.end_of_quarter x)".
+
+Axiom DATE_TIME_end_of_year : DATE_TIME -> DATE_TIME.
+Extract Inlined Constant DATE_TIME_end_of_year => "(fun x -> DateTime.end_of_year x)".
+
 Definition DATE_TIME_component (part:date_time_component) (dt:DATE_TIME) : Z :=
   match part with
   | date_time_DAY => DATE_TIME_day dt
@@ -157,9 +181,27 @@ Definition DATE_TIME_component (part:date_time_component) (dt:DATE_TIME) : Z :=
   | date_time_YEAR => DATE_TIME_year dt
   end.
 
+Definition DATE_TIME_start_of (part:date_time_component) (dt:DATE_TIME) : DATE_TIME :=
+  match part with
+  | date_time_DAY => DATE_TIME_start_of_day dt
+  | date_time_MONTH => DATE_TIME_start_of_month dt
+  | date_time_QUARTER => DATE_TIME_start_of_quarter dt
+  | date_time_YEAR => DATE_TIME_start_of_year dt
+  end.
+
+Definition DATE_TIME_end_of (part:date_time_component) (dt:DATE_TIME) : DATE_TIME :=
+  match part with
+  | date_time_DAY => DATE_TIME_end_of_day dt
+  | date_time_MONTH => DATE_TIME_end_of_month dt
+  | date_time_QUARTER => DATE_TIME_end_of_quarter dt
+  | date_time_YEAR => DATE_TIME_end_of_year dt
+  end.
+
 Inductive date_time_unary_op
   :=
   | uop_date_time_component : date_time_component -> date_time_unary_op
+  | uop_date_time_start_of : date_time_component -> date_time_unary_op
+  | uop_date_time_end_of : date_time_component -> date_time_unary_op
   | uop_date_time_from_string
   | uop_date_time_duration_from_string
 .
@@ -170,6 +212,10 @@ Definition date_time_unary_op_tostring (f:date_time_unary_op) : String.string
   := match f with
      | uop_date_time_component part =>
        "(dateTimeComponent" ++ (date_time_component_tostring part) ++ ")"
+     | uop_date_time_start_of part =>
+       "(dateTimeStartOf" ++ (date_time_component_tostring part) ++ ")"
+     | uop_date_time_end_of part =>
+       "(dateTimeEndOf" ++ (date_time_component_tostring part) ++ ")"
      | uop_date_time_from_string => "DateTimeFromString"
      | uop_date_time_duration_from_string => "DateTimeDurationFromString"
      end.
@@ -185,14 +231,17 @@ Definition date_time_component_to_java_string (part:date_time_component): string
      | date_time_YEAR => "UnaryOperators.year"
      end.
 
-
 Definition date_time_to_java_unary_op
              (indent:nat) (eol:String.string)
              (quotel:String.string) (fu:date_time_unary_op)
              (d:java_json) : java_json
   := match fu with
      | uop_date_time_component part =>
        mk_java_unary_op1 "date_time_component" (date_time_component_to_java_string part) d
+     | uop_date_time_start_of part =>
+       mk_java_unary_op1 "date_time_start_of" (date_time_component_to_java_string part) d
+     | uop_date_time_end_of part =>
+       mk_java_unary_op1 "date_time_end_of" (date_time_component_to_java_string part) d
      | uop_date_time_from_string => mk_java_unary_op0 "date_time_from_string" d
      | uop_date_time_duration_from_string => mk_java_unary_op0 "date_time_duration_from_string" d
      end.
@@ -203,6 +252,8 @@ Definition date_time_to_javascript_unary_op
              (d:String.string) : String.string
   := match fu with
      | uop_date_time_component part => "dateTimeComponent(" ++ quotel ++ (toString part) ++ quotel ++ ", " ++ d ++ ")"
+     | uop_date_time_start_of part => "dateTimeStartOf(" ++ quotel ++ (toString part) ++ quotel ++ ", " ++ d ++ ")"
+     | uop_date_time_end_of part => "dateTimeEndOf(" ++ quotel ++ (toString part) ++ quotel ++ ", " ++ d ++ ")"
      | uop_date_time_from_string => "dateTimeFromString(" ++ d ++ ")"
      | uop_date_time_duration_from_string => "dateTimeDurationFromString(" ++ d ++ ")"
      end.
@@ -213,6 +264,10 @@ Definition date_time_to_ajavascript_unary_op
   := match fu with
      | uop_date_time_component part =>
        call_runtime "dateTimeComponent" [ expr_literal (literal_string (toString part)); e ]
+     | uop_date_time_start_of part =>
+       call_runtime "dateTimeStartOf" [ expr_literal (literal_string (toString part)); e ]
+     | uop_date_time_end_of part =>
+       call_runtime "dateTimeEndOf" [ expr_literal (literal_string (toString part)); e ]
      | uop_date_time_from_string => call_runtime "dateTimeFromString" [ e ]
      | uop_date_time_duration_from_string => call_runtime "dateTimeDurationFromString" [ e ]
      end.

mechanization/Backend/Model/ErgoEnhancedModel.v

@@ -210,6 +210,10 @@ Definition date_time_unary_op_interp (op:date_time_unary_op) (d:data) : option d
   := match op with
      | uop_date_time_component part =>
        lift dnat (onddateTime (DATE_TIME_component part) d)
+     | uop_date_time_start_of part =>
+       lift denhanceddateTime (onddateTime (DATE_TIME_start_of part) d)
+     | uop_date_time_end_of part =>
+       lift denhanceddateTime (onddateTime (DATE_TIME_end_of part) d)
      | uop_date_time_from_string =>
        lift denhanceddateTime (ondstring DATE_TIME_from_string d)
      | uop_date_time_duration_from_string =>
@@ -237,6 +241,8 @@ Next Obligation.
   - decide equality.
   - decide equality.
     decide equality.
+    decide equality.
+    decide equality.
 Defined.
 Next Obligation.
   constructor; intros op.
@@ -252,6 +258,8 @@ Next Obligation.
       unfold onddateTime, denhanceddateTime, denhanceddateTimeinterval, lift in H; simpl in H;
         destruct d; simpl in H; try discriminate.
     + destruct f; invcs H; repeat constructor.
+    + destruct f; invcs H; repeat constructor.
+    + destruct f; invcs H; repeat constructor.
     + invcs H; repeat constructor.
     + invcs H; repeat constructor.
 Qed.
@@ -1485,6 +1493,8 @@ Inductive date_time_unary_op_has_type {model:brand_model} :
   date_time_unary_op -> rtype -> rtype -> Prop
   :=
   | tuop_date_time_component part : date_time_unary_op_has_type (uop_date_time_component part) DateTime Nat
+  | tuop_date_time_start_of part : date_time_unary_op_has_type (uop_date_time_start_of part) DateTime DateTime
+  | tuop_date_time_end_of part : date_time_unary_op_has_type (uop_date_time_end_of part) DateTime DateTime
   | tuop_date_time_from_string : date_time_unary_op_has_type uop_date_time_from_string RType.String DateTime
   | tuop_date_time_duration_from_string : date_time_unary_op_has_type uop_date_time_duration_from_string RType.String DateTimeInterval
 .
@@ -1496,6 +1506,10 @@ Definition date_time_unary_op_type_infer {model : brand_model} (op:date_time_una
   match op with
   | uop_date_time_component part =>
     if isDateTime τ₁ then Some Nat else None
+  | uop_date_time_start_of part =>
+    if isDateTime τ₁ then Some DateTime else None
+  | uop_date_time_end_of part =>
+    if isDateTime τ₁ then Some DateTime else None
   | uop_date_time_from_string =>
     if isString τ₁ then Some DateTime else None
   | uop_date_time_duration_from_string =>
@@ -1509,6 +1523,10 @@ Definition date_time_unary_op_type_infer_sub {model : brand_model} (op:date_time
   match op with
   | uop_date_time_component part =>
     enforce_unary_op_schema (τ₁,DateTime) Nat
+  | uop_date_time_start_of part =>
+    enforce_unary_op_schema (τ₁,DateTime) DateTime
+  | uop_date_time_end_of part =>
+    enforce_unary_op_schema (τ₁,DateTime) DateTime
   | uop_date_time_from_string =>
     enforce_unary_op_schema (τ₁,RType.String) DateTime
   | uop_date_time_duration_from_string =>
@@ -1579,6 +1597,16 @@ Proof.
           inversion H; subst; clear H; constructor;
             rewrite Float_canon; constructor.
   - destruct d; simpl in *.
+    + destruct τ₁; simpl in *; try congruence;
+        destruct x; simpl in *; try congruence;
+          destruct ft; simpl in *; try congruence;
+            inversion H; subst; clear H; constructor;
+              rewrite Foreign_canon; constructor.
+    + destruct τ₁; simpl in *; try congruence;
+        destruct x; simpl in *; try congruence;
+          destruct ft; simpl in *; try congruence;
+            inversion H; subst; clear H; constructor;
+              rewrite Foreign_canon; constructor.
     + destruct τ₁; simpl in *; try congruence;
         destruct x; simpl in *; try congruence;
           destruct ft; simpl in *; try congruence;
@@ -1621,6 +1649,18 @@ Proof.
           inversion H0; subst; clear H0;
             inversion H1; subst; clear H1;
               reflexivity.
+    + destruct ft; simpl in *; try congruence;
+        inversion H; subst; clear H;
+          rewrite Foreign_canon in H0;
+          inversion H0; subst; clear H0;
+            inversion H1; subst; clear H1;
+              reflexivity.
+    + destruct ft; simpl in *; try congruence;
+        inversion H; subst; clear H;
+          rewrite Foreign_canon in H0;
+          inversion H0; subst; clear H0;
+            inversion H1; subst; clear H1;
+              reflexivity.
     + inversion H; subst; clear H;
         rewrite String_canon in H0;
         inversion H0; subst; clear H0;
@@ -1655,6 +1695,8 @@ Proof.
             inversion H0; subst; clear H0;
               inversion H2; subst; clear H2.
     + simpl in H; congruence.
+    + simpl in H; congruence.
+    + simpl in H; congruence.
 Qed.
 
 Definition enhanced_unary_op_typing_infer_sub {model:brand_model} (fu:enhanced_unary_op) (τ:rtype) : option (rtype*rtype) :=
@@ -2065,15 +2107,21 @@ Module CompEnhanced.
 
     Module Ops.
       Module Unary.
-        Definition date_time_component (component:date_time_component)
+        Definition date_time_get_component (component:date_time_component)
           := OpForeignUnary (enhanced_unary_date_time_op (uop_date_time_component component)).
+        Definition date_time_start_of (component:date_time_component)
+          := OpForeignUnary (enhanced_unary_date_time_op (uop_date_time_start_of component)).
+        Definition date_time_end_of (component:date_time_component)
+          := OpForeignUnary (enhanced_unary_date_time_op (uop_date_time_end_of component)).
         Definition date_time_from_string
           := OpForeignUnary (enhanced_unary_date_time_op uop_date_time_from_string).
         Definition date_time_duration_from_string
           := OpForeignUnary (enhanced_unary_date_time_op uop_date_time_duration_from_string).
 
         (* for coq style syntax *)
-        Definition OpDateTimeComponent := date_time_component.
+        Definition OpDateTimeGetComponent := date_time_get_component.
+        Definition OpDateTimeStartOf := date_time_start_of.
+        Definition OpDateTimeEndOf := date_time_end_of.
         Definition OpDateTimeFromString := date_time_from_string.
         Definition OpDateTimeIntervalFromString := date_time_duration_from_string.
 

mechanization/ErgoC/Lang/ErgoCStdlib.v

@@ -98,6 +98,24 @@ Section ErgoCStdlib.
           mk_unary prov (OpForeignUnary (enhanced_unary_date_time_op (uop_date_time_component date_time_QUARTER))))
       :: ("org.accordproject.ergo.stdlib.dateTimeYear",
           mk_unary prov (OpForeignUnary (enhanced_unary_date_time_op (uop_date_time_component date_time_YEAR))))
+
+      :: ("org.accordproject.ergo.stdlib.dateTimeStartOfDayOfMonth",
+          mk_unary prov (OpForeignUnary (enhanced_unary_date_time_op (uop_date_time_start_of date_time_DAY))))
+      :: ("org.accordproject.ergo.stdlib.dateTimeStartOfMonth",
+          mk_unary prov (OpForeignUnary (enhanced_unary_date_time_op (uop_date_time_start_of date_time_MONTH))))
+      :: ("org.accordproject.ergo.stdlib.dateTimeStartOfQuarter",
+          mk_unary prov (OpForeignUnary (enhanced_unary_date_time_op (uop_date_time_start_of date_time_QUARTER))))
+      :: ("org.accordproject.ergo.stdlib.dateTimeStartOfYear",
+          mk_unary prov (OpForeignUnary (enhanced_unary_date_time_op (uop_date_time_start_of date_time_YEAR))))
+
+      :: ("org.accordproject.ergo.stdlib.dateTimeEndOfDayOfMonth",
+          mk_unary prov (OpForeignUnary (enhanced_unary_date_time_op (uop_date_time_end_of date_time_DAY))))
+      :: ("org.accordproject.ergo.stdlib.dateTimeEndOfMonth",
+          mk_unary prov (OpForeignUnary (enhanced_unary_date_time_op (uop_date_time_end_of date_time_MONTH))))
+      :: ("org.accordproject.ergo.stdlib.dateTimeEndOfQuarter",
+          mk_unary prov (OpForeignUnary (enhanced_unary_date_time_op (uop_date_time_end_of date_time_QUARTER))))
+      :: ("org.accordproject.ergo.stdlib.dateTimeEndOfYear",
+          mk_unary prov (OpForeignUnary (enhanced_unary_date_time_op (uop_date_time_end_of date_time_YEAR))))
       :: nil.
 
   Definition foreign_binary_operator_table prov : ergo_stdlib_table :=