(fix) Additional dateTime operators

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

examples/latedeliveryandpenalty/logic.ergo

@@ -34,7 +34,7 @@ contract LateDeliveryAndPenalty over TemplateModel {
     ;
 
     // Calculate the time difference between current date and agreed upon date
-    define variable diff = momentDiff(now,agreed);
+    define variable diff = momentDiffDays(now,agreed);
     // Penalty formula
     define variable penalty =
       (diff / contract.penaltyDuration.amount) * contract.penaltyPercentage/100.0 * request.goodsValue;

examples/latedeliveryandpenalty/logic2.ergo

@@ -48,7 +48,7 @@ contract LateDeliveryAndPenalty over TemplateModel throws Error {
        return LateDeliveryAndPenaltyResponse{ 0, true }
      } else { // If not, calculate the penalty and whether the contract can be terminated
        // difference between current date and agreed upon date
-       define variable diff = moment.diff(moment.now(),agreed,penaltyDuration.unit);
+       define variable diff = momentDiffDay(moment.now(),agreed,penaltyDuration.unit);
        // Calls the function to calculate penalty
        define variable penalty = calculatePenalty(diff,request.goodsValue);
        // Return the response with the penalty and termination determination

examples/latedeliveryandpenalty/logic3.ergo

@@ -53,7 +53,7 @@ contract LateDeliveryAndPenalty over TemplateModel {
     };
 
     // difference between current date and agreed upon date
-    define variable diff = momentDiff(agreed,now());
+    define variable diff = momentDiffDay(agreed,now());
     define variable penalty = calculatePenalty(diff,request.goodsValue);
     return new LateDeliveryAndPenaltyResponse{
 	penalty: capped,

examples/promissory-note/logic.ergo

@@ -27,7 +27,7 @@ contract PromissoryNote over TemplateModel {
     define variable outstanding = contract.dollarAmount - request.amountPaid;
     enforce outstanding >= 0.0;
 
-    define variable numberOfDays = momentDiff(moment("17 May 2018 13:53:33 EST"),contract.date);
+    define variable numberOfDays = momentDiffDays(moment("17 May 2018 13:53:33 EST"),contract.date);
     enforce numberOfDays >= 0.0;
     define variable compounded =  outstanding * compoundInterestMultiple(contract.interestRate, numberOfDays);
 

examples/promissory-note/logic2.ergo

@@ -28,7 +28,7 @@ contract PromissoryNote over TemplateModel {
 		define variable interestRate = contract.interestRate ?? 3.4;
     enforce outstanding >= 0.0;
 
-    define variable numberOfDays = momentDiff(moment("17 May 2018 13:53:33 EST"),contract.date);
+    define variable numberOfDays = momentDiffDays(moment("17 May 2018 13:53:33 EST"),contract.date);
     enforce numberOfDays >= 0.0;
     define variable compounded =  outstanding * compoundInterestMultiple(interestRate, numberOfDays);
 

mechanization/Backend/Lib/EOperators.v

@@ -144,8 +144,10 @@ Module EOperators(ergomodel:ErgoBackendModel).
         := ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimeGt.
       Definition opdatege : op
         := ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimeGe.
-      Definition opdateintervalbetween : op
-        := ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimeIntervalBetween.
+      Definition opdateintervaldays : op
+        := ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimeIntervalDays.
+      Definition opdateintervalseconds : op
+        := ErgoEnhancedModel.CompEnhanced.Enhanced.Ops.Binary.OpDateTimeIntervalSeconds.
     End DateTime.
 
     Definition opequal : op

mechanization/Backend/Model/DateTimeModelPart.v

@@ -225,8 +225,11 @@ Extract Inlined Constant DATE_TIME_gt => "(fun x y -> x > y)".
 Axiom DATE_TIME_ge : DATE_TIME -> DATE_TIME -> bool.
 Extract Inlined Constant DATE_TIME_ge => "(fun x y -> x >= y)".
 
-Axiom DATE_TIME_DURATION_between : DATE_TIME -> DATE_TIME -> DATE_TIME_DURATION.
-Extract Inlined Constant DATE_TIME_DURATION_between => "(fun x y -> """")".
+Axiom DATE_TIME_DURATION_days : DATE_TIME -> DATE_TIME -> DATE_TIME_DURATION.
+Extract Inlined Constant DATE_TIME_DURATION_days => "(fun x y -> """")".
+
+Axiom DATE_TIME_DURATION_seconds : DATE_TIME -> DATE_TIME -> DATE_TIME_DURATION.
+Extract Inlined Constant DATE_TIME_DURATION_seconds => "(fun x y -> """")".
 
 Inductive date_time_binary_op
   :=
@@ -237,7 +240,8 @@ Inductive date_time_binary_op
   | bop_date_time_le
   | bop_date_time_gt
   | bop_date_time_ge
-  | bop_date_time_duration_between
+  | bop_date_time_duration_days
+  | bop_date_time_duration_seconds
 .
 
 Definition date_time_binary_op_tostring (f:date_time_binary_op) : String.string
@@ -249,7 +253,8 @@ Definition date_time_binary_op_tostring (f:date_time_binary_op) : String.string
      | bop_date_time_le => "DateTimeLe"
      | bop_date_time_gt => "DateTimeGt"
      | bop_date_time_ge => "DateTimeGe"
-     | bop_date_time_duration_between => "DateTimeDurationBetween"
+     | bop_date_time_duration_days => "DateTimeDurationDays"
+     | bop_date_time_duration_seconds => "DateTimeDurationSeconds"
      end.
 
 (* Java equivalent: JavaScriptBackend.jsFunc *)
@@ -268,8 +273,8 @@ Definition date_time_to_java_binary_op
      | bop_date_time_le =>  mk_java_binary_op0 "date_time_le" d1 d2
      | bop_date_time_gt =>  mk_java_binary_op0 "date_time_gt" d1 d2
      | bop_date_time_ge => mk_java_binary_op0 "date_time_ge" d1 d2
-     | bop_date_time_duration_between => mk_java_binary_op0 "date_time_duration_between" d1 d2
-
+     | bop_date_time_duration_days => mk_java_binary_op0 "date_time_duration_days" d1 d2
+     | bop_date_time_duration_seconds => mk_java_binary_op0 "date_time_duration_seconds" d1 d2
      end.
 
 Definition date_time_to_javascript_binary_op
@@ -284,7 +289,8 @@ Definition date_time_to_javascript_binary_op
      | bop_date_time_le =>  jsFunc "dateTimePointLe" d1 d2
      | bop_date_time_gt =>  jsFunc "dateTimePointGt" d1 d2
      | bop_date_time_ge => jsFunc "dateTimePointGe" d1 d2
-     | bop_date_time_duration_between => jsFunc "dateTimeDurationBetween" d1 d2
+     | bop_date_time_duration_days => jsFunc "dateTimeDurationDays" d1 d2
+     | bop_date_time_duration_seconds => jsFunc "dateTimeDurationSeconds" d1 d2
      end.  
 
 Definition date_time_to_ajavascript_binary_op
@@ -298,6 +304,7 @@ Definition date_time_to_ajavascript_binary_op
      | bop_date_time_le =>  call_runtime "dateTimePointLe" [ e1; e2 ]
      | bop_date_time_gt =>  call_runtime "dateTimePointGt" [ e1; e2 ]
      | bop_date_time_ge => call_runtime "dateTimePointGe" [ e1; e2 ]
-     | bop_date_time_duration_between => call_runtime "dateTimeDurationBetween" [ e1; e2 ]
+     | bop_date_time_duration_days => call_runtime "dateTimeDurationDays" [ e1; e2 ]
+     | bop_date_time_duration_seconds => call_runtime "dateTimeDurationSeconds" [ e1; e2 ]
      end.  
 

mechanization/Backend/Model/ErgoBackendRuntime.v

@@ -96,9 +96,12 @@ Module ErgoBackendRuntime <: ErgoBackendModel.
           | "momentAdd"%string =>
             Some (OpForeignBinary (enhanced_binary_date_time_op
                                      bop_date_time_plus))
-          | "momentDiff"%string =>
+          | "momentDiffDays"%string =>
             Some (OpForeignBinary (enhanced_binary_date_time_op
-                                     bop_date_time_duration_between))
+                                     bop_date_time_duration_days))
+          | "momentDiffSeconds"%string =>
+            Some (OpForeignBinary (enhanced_binary_date_time_op
+                                     bop_date_time_duration_seconds))
           | _ => None
           end
       in

mechanization/Backend/Model/ErgoEnhancedModel.v

@@ -264,7 +264,8 @@ Definition date_time_binary_op_interp
      | bop_date_time_le => rondbooldateTime2 DATE_TIME_le d1 d2
      | bop_date_time_gt => rondbooldateTime2 DATE_TIME_gt d1 d2
      | bop_date_time_ge => rondbooldateTime2 DATE_TIME_ge d1 d2
-     | bop_date_time_duration_between => lift denhanceddateTimeinterval (onddateTime2 DATE_TIME_DURATION_between d1 d2)
+     | bop_date_time_duration_days => lift denhanceddateTimeinterval (onddateTime2 DATE_TIME_DURATION_days d1 d2)
+     | bop_date_time_duration_seconds => lift denhanceddateTimeinterval (onddateTime2 DATE_TIME_DURATION_seconds d1 d2)
      end.
 
 Definition enhanced_binary_op_interp
@@ -1473,8 +1474,10 @@ Inductive date_time_binary_op_has_type {model:brand_model} :
       date_time_binary_op_has_type bop_date_time_gt DateTime DateTime Bool 
   | tbop_date_time_ge :
       date_time_binary_op_has_type bop_date_time_ge DateTime DateTime Bool
-  | tbop_date_time_duration_between  :
-      date_time_binary_op_has_type bop_date_time_duration_between DateTime DateTime DateTimeInterval
+  | tbop_date_time_duration_days  :
+      date_time_binary_op_has_type bop_date_time_duration_days DateTime DateTime DateTimeInterval
+  | tbop_date_time_duration_seconds  :
+      date_time_binary_op_has_type bop_date_time_duration_seconds DateTime DateTime DateTimeInterval
 .
 
 Definition date_time_binary_op_type_infer {model : brand_model} (op:date_time_binary_op) (τ₁ τ₂:rtype) :=
@@ -1493,7 +1496,9 @@ Definition date_time_binary_op_type_infer {model : brand_model} (op:date_time_bi
     if isDateTime τ₁ && isDateTime τ₂ then Some Bool else None
   | bop_date_time_ge =>
     if isDateTime τ₁ && isDateTime τ₂ then Some Bool else None
-  | bop_date_time_duration_between  =>
+  | bop_date_time_duration_days  =>
+    if isDateTime τ₁ && isDateTime τ₂ then Some DateTimeInterval else None
+  | bop_date_time_duration_seconds  =>
     if isDateTime τ₁ && isDateTime τ₂ then Some DateTimeInterval else None
   end.
 
@@ -1530,7 +1535,9 @@ Definition date_time_binary_op_type_infer_sub {model : brand_model} (op:date_tim
   | bop_date_time_gt
   | bop_date_time_ge =>
     enforce_binary_op_schema (τ₁,DateTime) (τ₂,DateTime) Bool
-  | bop_date_time_duration_between  =>
+  | bop_date_time_duration_days  =>
+    enforce_binary_op_schema (τ₁,DateTime) (τ₂,DateTime) DateTimeInterval
+  | bop_date_time_duration_seconds  =>
     enforce_binary_op_schema (τ₁,DateTime) (τ₂,DateTime) DateTimeInterval
   end.
 
@@ -1777,8 +1784,10 @@ Module CompEnhanced.
         Definition date_time_ge 
           := OpForeignBinary (enhanced_binary_date_time_op bop_date_time_ge).
 
-        Definition date_time_duration_between 
-          := OpForeignBinary (enhanced_binary_date_time_op (bop_date_time_duration_between)).
+        Definition date_time_duration_days
+          := OpForeignBinary (enhanced_binary_date_time_op (bop_date_time_duration_days)).
+        Definition date_time_duration_seconds 
+          := OpForeignBinary (enhanced_binary_date_time_op (bop_date_time_duration_seconds)).
 
         (* for coq style syntax *)
         Definition OpDateTimePlus := date_time_plus.
@@ -1789,7 +1798,8 @@ Module CompEnhanced.
         Definition OpDateTimeGt := date_time_gt.
         Definition OpDateTimeGe := date_time_ge.
 
-        Definition OpDateTimeIntervalBetween := date_time_duration_between.
+        Definition OpDateTimeIntervalDays := date_time_duration_days.
+        Definition OpDateTimeIntervalSeconds := date_time_duration_seconds.
 
       End Binary.
     End Ops.

packages/ergo-compiler/lib/ergo-runtime.js

@@ -578,11 +578,16 @@ function dateTimePointGe(date1, date2) {
     return compareDates(date1, date2) >= 0;
 }
 
-function dateTimeDurationBetween(date1, date2) {
+function dateTimeDurationDays(date1, date2) {
     date1 = mustBeDate(date1);
     date2 = mustBeDate(date2);
     return date1.diff(date2,'days');
 }
+function dateTimeDurationSeconds(date1, date2) {
+    date1 = mustBeDate(date1);
+    date2 = mustBeDate(date2);
+    return date1.diff(date2,'seconds');
+}
 
 function compareDates(date1, date2) {
     date1 = mustBeDate(date1);