Merge pull request #43 from MetaBorgCube/release/1.0.0

Release/1.0.0

change_version.sh

@@ -1,4 +1,4 @@
-FROMVERSION=0.8.1
-TOVERSION=0.8.2
+FROMVERSION=0.8.2
+TOVERSION=0.8.3
 
 grep -rEl --exclude=*/target/* --exclude=*/src-gen/* --include=*.{yaml,xml,MF} "${FROMVERSION}(.qualifier|-SNAPSHOT)" * | xargs sed -i "" "s/${FROMVERSION}/${TOVERSION}/g"

change_version_to_stable.sh

@@ -1,5 +1,5 @@
-FROMVERSION=0.8.2
-TOVERSION=0.8.2
+FROMVERSION=0.8.3
+TOVERSION=1.0.0
 
 grep -rEl --exclude=*/target/* --exclude=*/src-gen/* --include=*.{yaml,xml,MF} "${FROMVERSION}.qualifier" * | xargs sed -i "" "s/${FROMVERSION}.qualifier/${TOVERSION}/g"
 grep -rEl --exclude=*/target/* --exclude=*/src-gen/* --include=*.{yaml,xml,MF} "${FROMVERSION}-SNAPSHOT" * | xargs sed -i "" "s/${FROMVERSION}-SNAPSHOT/${TOVERSION}/g"

icedust.eclipse.feature/feature.xml

@@ -2,8 +2,8 @@
 <feature
   id="icedust.eclipse.feature"
   label="icedust language Eclipse plugin"
-  version="0.8.2"
+  version="1.0.0"
 >
-  <plugin id="icedust.eclipse" version="0.8.2" unpack="true" />
+  <plugin id="icedust.eclipse" version="1.0.0" unpack="true" />
   <includes id="org.metaborg.spoofax.eclipse.feature" version="0" />
 </feature>

icedust.eclipse.feature/pom.xml

@@ -6,7 +6,7 @@
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.metaborg.lang</groupId>
   <artifactId>icedust.eclipse.feature</artifactId>
-  <version>0.8.2</version>
+  <version>1.0.0</version>
   <packaging>eclipse-feature</packaging>
 
   <parent>

icedust.eclipse.site/pom.xml

@@ -6,7 +6,7 @@
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.metaborg.lang</groupId>
   <artifactId>icedust.eclipse.site</artifactId>
-  <version>0.8.2</version>
+  <version>1.0.0</version>
   <packaging>eclipse-update-site</packaging>
 
   <parent>

icedust.eclipse.site/site.xml

@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <site>
-   <feature url="features/icedust.eclipse.feature_0.8.2.jar" id="icedust.eclipse.feature" version="0.8.2">
+   <feature url="features/icedust.eclipse.feature_1.0.0.jar" id="icedust.eclipse.feature" version="1.0.0">
       <category name="icedust"/>
    </feature>
    <category-def name="icedust" label="icedust language Eclipse plugin">

icedust.eclipse/META-INF/MANIFEST.MF

@@ -2,7 +2,7 @@ Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: icedust language Eclipse plugin
 Bundle-SymbolicName: icedust.eclipse;singleton:=true
-Bundle-Version: 0.8.2
+Bundle-Version: 1.0.0
 Bundle-Vendor: org.metaborg.lang
 Bundle-ActivationPolicy: lazy
 Require-Bundle: org.metaborg.spoofax.eclipse

icedust.eclipse/pom.xml

@@ -6,7 +6,7 @@
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.metaborg.lang</groupId>
   <artifactId>icedust.eclipse</artifactId>
-  <version>0.8.2</version>
+  <version>1.0.0</version>
   <packaging>eclipse-plugin</packaging>
 
   <parent>

icedust.example/metaborg.yaml

@@ -1,4 +1,4 @@
 ---
 dependencies:
   compile:
-  - org.metaborg.lang:icedust:0.8.2
+  - org.metaborg.lang:icedust:1.0.0

icedust.example/pom.xml

@@ -7,7 +7,7 @@
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.metaborg.lang</groupId>
   <artifactId>icedust.example</artifactId>
-  <version>0.8.2</version>
+  <version>1.0.0</version>
   <packaging>spoofax-project</packaging>
 
   <parent>
@@ -20,7 +20,7 @@
     <dependency>
       <groupId>org.metaborg.lang</groupId>
       <artifactId>icedust</artifactId>
-      <version>0.8.2</version>
+      <version>1.0.0</version>
       <type>spoofax-language</type>
     </dependency>
   </dependencies>

icedust.proofs/multiplicities.v

@@ -135,30 +135,28 @@ Function avgo(l : list nat) : option nat :=
 Function conj(l : list bool) : bool := fold_left andb l true.
 Function disj(l : list bool) : bool := fold_left orb  l false.
 
-Fixpoint indexOf_nat (l : list nat) (x : nat) : option nat :=
+Fixpoint list_incr_all (l : list nat) : list nat :=
   match l with
-  | []     => None
+  | []     => []
+  | h :: t => (h + 1) :: (list_incr_all t)
+  end.
+
+Fixpoint indexOf_nat (l : list nat) (x : nat) : list nat :=
+  match l with
+  | []     => []
   | h :: t =>
       match eqb x h with
-      | true  => Some 0
-      | false =>
-          match indexOf_nat t x with
-          | None   => None
-          | Some i => Some (i+1)
-          end
+      | true  => 0 :: (list_incr_all (indexOf_nat t x))
+      | false => list_incr_all (indexOf_nat t x)
       end
   end.
-Fixpoint indexOf_bool (l : list bool) (x : bool) : option nat :=
+Fixpoint indexOf_bool (l : list bool) (x : bool) : list nat :=
   match l with
-  | []     => None
+  | []     => []
   | h :: t =>
       match beq x h with
-      | true  => Some 0
-      | false =>
-          match indexOf_bool t x with
-          | None   => None
-          | Some i => Some (i+1)
-          end
+      | true  => 0 :: (list_incr_all (indexOf_bool t x))
+      | false => list_incr_all (indexOf_bool t x)
       end
   end.
 
@@ -420,13 +418,13 @@ Inductive evalR : expr -> val -> Prop :=
       e1 \\ intv v1s ->
       e2 \\ intv v2s ->
       vtuples = list_pair_with2 v1s v2s ->
-      EIndexOf e1 e2 \\ intv (fmap (funtuple indexOf_nat) vtuples)
+      EIndexOf e1 e2 \\ intv (flat_map (funtuple indexOf_nat) vtuples)
 
   | E_IndexOf_Bool : forall (e1 e2 : expr) v1s v2s vtuples,
       e1 \\ boolv v1s ->
       e2 \\ boolv v2s ->
       vtuples = list_pair_with2 v1s v2s ->
-      EIndexOf e1 e2 \\ intv (fmap (funtuple indexOf_bool) vtuples)
+      EIndexOf e1 e2 \\ intv (flat_map (funtuple indexOf_bool) vtuples)
 
 where "e '\\' v" := (evalR e v) : type_scope.
 
@@ -734,11 +732,11 @@ Fixpoint evalF (e : expr) : option val :=
       match v1, v2 with
       | Some (intv v1s), Some (intv v2s) =>
           let vtuples := list_pair_with2 v1s v2s in
-          let vs := fmap (funtuple indexOf_nat) vtuples in
+          let vs := flat_map (funtuple indexOf_nat) vtuples in
           Some (intv vs)
       | Some (boolv v1s), Some (boolv v2s) =>
           let vtuples := list_pair_with2 v1s v2s in
-          let vs := fmap (funtuple indexOf_bool) vtuples in
+          let vs := flat_map (funtuple indexOf_bool) vtuples in
           Some (intv vs)
       | _,_ => None
       end
@@ -989,6 +987,8 @@ Inductive typeR : expr -> type -> Prop :=
 
 where "e ':' t" := (typeR e t) : type_scope.
 
+(* Note: not needed for proofs
+
 Fixpoint typeF (e : expr) : option type :=
   match e with
   | EInt n =>
@@ -1301,6 +1301,8 @@ Example typeR_1 :
   (EPlus (EInt 1) (EInt 2)) : intty.
 Proof. apply typeR_eq_typeF. simpl. reflexivity. Qed.
 
+*)
+
 (***** multiplicity checker *****
 
 Specification in same place as type checker. *)
@@ -1491,10 +1493,12 @@ Inductive multR : expr -> mult -> Prop :=
   | M_IndexOf : forall (e1 e2 : expr) m1 m2,
       e1 ~ m1 ->
       e2 ~ m2 ->
-      EIndexOf e1 e2 ~ mult_lower_zero m2
+      EIndexOf e1 e2 ~ mult_lower_zero (mult_crossproduct m1 m2)
 
 where "e '~' m" := (multR e m) : type_scope.
 
+(* Note: not needed for proofs
+
 Fixpoint multF (e : expr) : mult :=
   match e with
   | EInt n =>
@@ -1637,7 +1641,7 @@ Fixpoint multF (e : expr) : mult :=
   | EIndexOf e1 e2 =>
       let m1 := multF e1 in
       let m2 := multF e2 in
-      mult_lower_zero m2
+      mult_lower_zero (mult_crossproduct m1 m2)
 
   end.
 
@@ -1669,6 +1673,8 @@ Example multR_2 :
   (EConcat (EInt 1) (EInt 2)) ~ oneOrMore.
 Proof. apply multR_eq_multF. simpl. reflexivity. Qed.
 
+*)
+
 
 (***** aux functions for proving type- and multiplicity soundness *****)
 Definition valty (v : val) : type :=
@@ -1777,33 +1783,26 @@ Proof.
   induction H.
   (* literals *)
   all: try(apply exists_some).
-  (* unops *)
-  all: simpl.
+  (* rest *)
   all: try rename IHtypeR into IHtypeR1.
-  all: destruct IHtypeR1 as [v1 Hv1].
-  all: rewrite Hv1.
-  all: apply evalR_eq_evalF in Hv1.
-  all: apply type_preservation with (v:=v1) in H ; try assumption.
-  all: unfold valty in H.
-  all: case_match; try congruence.
-  all: try apply exists_some.
-  (* binops *)
-  all: destruct IHtypeR2 as [v2 Hv2].
-  all: rewrite Hv2.
-  all: apply evalR_eq_evalF in Hv2.
-  all: apply type_preservation with (v:=v2) in H0 ; try assumption.
-  all: unfold valty in H0.
-  all: case_match; try congruence.
+  all:     destruct IHtypeR1 as [v1 Hv1].
+  all: try(destruct IHtypeR2 as [v2 Hv2]).
+  all: try(destruct IHtypeR3 as [v3 Hv3]).
+  all:     apply evalR_eq_evalF in Hv1 as Hv1R.
+  all: try(apply evalR_eq_evalF in Hv2 as Hv2R).
+  all: try(apply evalR_eq_evalF in Hv3 as Hv3R).
+  all:     apply type_preservation with (v:=v1) in H ; try assumption.
+  all: try(apply type_preservation with (v:=v2) in H0 ; try assumption).
+  all: try(apply type_preservation with (v:=v3) in H1 ; try assumption).
+  all:     unfold valty in H.
+  all: try(unfold valty in H0).
+  all: try(unfold valty in H1).
+  all: repeat(case_match; try congruence). (* splits up polymorphic cases *)
+  all: simpl.
+  all:     rewrite Hv1.
+  all: try(rewrite Hv2).
+  all: try(rewrite Hv3).
   all: try apply exists_some.
-  (* if *)
-  all: destruct IHtypeR3 as [v3 Hv3].
-  all: rewrite Hv3.
-  all: apply evalR_eq_evalF in Hv3.
-  all: apply type_preservation with (v:=v3) in H1 ; try assumption.
-  all: subst.
-  all: unfold valty in H1.
-  all: case_match; try congruence.
-  all: apply exists_some.
 Qed.
 
 Theorem typed_evalR_totality : forall (e : expr) t,
@@ -1865,7 +1864,7 @@ Proof.
   generalize dependent m.
   induction Hval.
   all: intros.
-  (* proof literals of mult one *)
+  (* proof literals and total aggregations *)
   all: try(simpl; constructor).
   (* get multiplicities of sub expressions *)
   all: inversion Hmult.

icedust.test/dynamic-semantics/java/features/expressions/datetime/datetime.spt

@@ -19,6 +19,7 @@ fixture [[
     2017-03-05 10:00:00 <= 2017-03-05 08:00:00
     2017-03-05 10:00:00 <= 2017-03-05 10:00:00 
     2017-09-05 18:00:00 == 2017-09-05 18:00:00
+    min(2018-03-16 16:00:00 ++ 2018-03-15 16:00:00 ) == 2018-03-15 16:00:00
 //
     [[...]] 
 ]]
@@ -33,4 +34,5 @@ false
 false
 true
 true
+true
 "

icedust.test/metaborg.yaml

@@ -1,8 +1,8 @@
-id: org.metaborg:icedust.test:0.8.2
+id: org.metaborg:icedust.test:1.0.0
 name: IceDust
 dependencies:
   compile:
-  - org.metaborg.lang:icedust:0.8.2
+  - org.metaborg.lang:icedust:1.0.0
   - org.metaborg:org.metaborg.meta.lang.spt:${metaborgVersion}
 runtime:
   nabl2:

icedust.test/pom.xml

@@ -7,7 +7,7 @@
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.metaborg.lang</groupId>
   <artifactId>icedust.test</artifactId>
-  <version>0.8.2</version>
+  <version>1.0.0</version>
   <packaging>spoofax-test</packaging>
 
   <parent>
@@ -20,7 +20,7 @@
     <dependency>
       <groupId>org.metaborg.lang</groupId>
       <artifactId>icedust</artifactId>
-      <version>0.8.2</version>
+      <version>1.0.0</version>
       <type>spoofax-language</type>
     </dependency>
     <dependency>
@@ -39,7 +39,7 @@
         <artifactId>spoofax-maven-plugin</artifactId>
         <version>${metaborg-version}</version>
         <configuration>
-          <languageUnderTest>org.metaborg.lang:icedust:0.8.2</languageUnderTest>
+          <languageUnderTest>org.metaborg.lang:icedust:1.0.0</languageUnderTest>
         </configuration>
       </plugin>
     </plugins>

icedust.test/static-semantics/types/aggregation.spt

@@ -25,11 +25,12 @@ test type of aggr max   [[max(4 ++ 3 ++ 8)]]    run get-type2 to Int()
 test type of aggr avg   [[avg(1 ++ 3)]]         run get-type2 to Int()
 test type of aggr sum   [[sum(1 ++ 3)]]         run get-type2 to Int()
 test type of aggr concat[[concat("a" ++ "b")]]  run get-type2 to String()
-//test type of aggr count [[count("a" ++ "b")]]   run get-type2 to Int()
+test type of aggr count [[count("a" ++ "b")]]   run get-type2 to Int()
 test type of aggr disj  [[disj(true ++ false)]] run get-type2 to Boolean()
 test type of aggr conj  [[conj(true ++ false)]] run get-type2 to Boolean()
 
 test type of aggr min  Float  [[min(4.4 ++ 3.4)]] run get-type2 to Float()
+test type of aggr min  Float  [[min(2018-03-16 16:00:00 ++ 2018-03-15 16:00:00 )]] run get-type2 to Datetime()
 
 test error on aggr min String  [[ min("b" ++ "c")]] 1 error
 test error on aggr concat Int  [[ concat(2 ++ 3) ]] 1 error

icedust/editor/Syntax.esv

@@ -26,6 +26,7 @@ menus
   menu: "Debug"
 
     action: "debug-get-ast-value" = debug-get-ast-value
+    action: "Count entities, attributes, relations, and functions" = debug-count-constructs (openeditor)
 
 views