From a765e0bc1bce1a39a58084593d30814eb05df3ea Mon Sep 17 00:00:00 2001 From: Daco Harkes Date: Mon, 13 Nov 2017 21:23:56 +0100 Subject: [PATCH 01/13] Revert "ctree -> jar" This reverts commit 2e9823186f5666af3094d82e413bd352d7eabb69. --- icedust/editor/Main.esv | 2 +- icedust/metaborg.yaml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/icedust/editor/Main.esv b/icedust/editor/Main.esv index 4d62cc1f..8cf8d65f 100644 --- a/icedust/editor/Main.esv +++ b/icedust/editor/Main.esv @@ -11,6 +11,6 @@ language extensions : ice - provider : target/metaborg/stratego.jar + provider : target/metaborg/stratego.ctree provider : target/metaborg/stratego-javastrat.jar provider : lib-js/nashorn.jar \ No newline at end of file diff --git a/icedust/metaborg.yaml b/icedust/metaborg.yaml index c5ed0bc3..848d550e 100644 --- a/icedust/metaborg.yaml +++ b/icedust/metaborg.yaml @@ -29,7 +29,7 @@ language: sdf: sdf2table: java stratego: - format: jar + format: ctree args: - -la - stratego-lib From 40cf491c4383ca89e3fddcc2dbd0dca1d4103aab Mon Sep 17 00:00:00 2001 From: Daco Harkes Date: Mon, 13 Nov 2017 21:24:08 +0100 Subject: [PATCH 02/13] Revert "change version from 0.7.2-SNAPSHOT to 0.8.0" This reverts commit e8b30b7876d7f3e65603160ac76b2add577e15d7. --- change_version_to_stable.sh | 4 ++-- icedust.eclipse.feature/feature.xml | 4 ++-- icedust.eclipse.feature/pom.xml | 2 +- icedust.eclipse.site/pom.xml | 2 +- icedust.eclipse.site/site.xml | 2 +- icedust.eclipse/META-INF/MANIFEST.MF | 2 +- icedust.eclipse/pom.xml | 2 +- icedust.example/metaborg.yaml | 2 +- icedust.example/pom.xml | 4 ++-- icedust.test/metaborg.yaml | 4 ++-- icedust.test/pom.xml | 6 +++--- icedust/metaborg.yaml | 2 +- icedust/pom.xml | 2 +- pom.xml | 2 +- 14 files changed, 20 insertions(+), 20 deletions(-) diff --git a/change_version_to_stable.sh b/change_version_to_stable.sh index 884edcd3..372cca50 100755 --- a/change_version_to_stable.sh +++ b/change_version_to_stable.sh @@ -1,5 +1,5 @@ -FROMVERSION=0.7.2 -TOVERSION=0.8.0 +FROMVERSION=0.7.1 +TOVERSION=0.7.1 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" diff --git a/icedust.eclipse.feature/feature.xml b/icedust.eclipse.feature/feature.xml index 82912556..9d1d76f7 100644 --- a/icedust.eclipse.feature/feature.xml +++ b/icedust.eclipse.feature/feature.xml @@ -2,8 +2,8 @@ - + diff --git a/icedust.eclipse.feature/pom.xml b/icedust.eclipse.feature/pom.xml index 5b0e53d4..5a39cf23 100644 --- a/icedust.eclipse.feature/pom.xml +++ b/icedust.eclipse.feature/pom.xml @@ -6,7 +6,7 @@ 4.0.0 org.metaborg.lang icedust.eclipse.feature - 0.8.0 + 0.7.2-SNAPSHOT eclipse-feature diff --git a/icedust.eclipse.site/pom.xml b/icedust.eclipse.site/pom.xml index 37938e2d..db5845da 100644 --- a/icedust.eclipse.site/pom.xml +++ b/icedust.eclipse.site/pom.xml @@ -6,7 +6,7 @@ 4.0.0 org.metaborg.lang icedust.eclipse.site - 0.8.0 + 0.7.2-SNAPSHOT eclipse-update-site diff --git a/icedust.eclipse.site/site.xml b/icedust.eclipse.site/site.xml index 9f2b0bc9..648d95e6 100644 --- a/icedust.eclipse.site/site.xml +++ b/icedust.eclipse.site/site.xml @@ -1,6 +1,6 @@ - + diff --git a/icedust.eclipse/META-INF/MANIFEST.MF b/icedust.eclipse/META-INF/MANIFEST.MF index 2ac6d9fc..991d3982 100644 --- a/icedust.eclipse/META-INF/MANIFEST.MF +++ b/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.0 +Bundle-Version: 0.7.2.qualifier Bundle-Vendor: org.metaborg.lang Bundle-ActivationPolicy: lazy Require-Bundle: org.metaborg.spoofax.eclipse diff --git a/icedust.eclipse/pom.xml b/icedust.eclipse/pom.xml index 096293b3..2fabb7e9 100644 --- a/icedust.eclipse/pom.xml +++ b/icedust.eclipse/pom.xml @@ -6,7 +6,7 @@ 4.0.0 org.metaborg.lang icedust.eclipse - 0.8.0 + 0.7.2-SNAPSHOT eclipse-plugin diff --git a/icedust.example/metaborg.yaml b/icedust.example/metaborg.yaml index 9827aa32..ed53d5f0 100644 --- a/icedust.example/metaborg.yaml +++ b/icedust.example/metaborg.yaml @@ -1,4 +1,4 @@ --- dependencies: compile: - - org.metaborg.lang:icedust:0.8.0 + - org.metaborg.lang:icedust:0.7.2-SNAPSHOT diff --git a/icedust.example/pom.xml b/icedust.example/pom.xml index f50df087..f04d7d9a 100644 --- a/icedust.example/pom.xml +++ b/icedust.example/pom.xml @@ -7,7 +7,7 @@ 4.0.0 org.metaborg.lang icedust.example - 0.8.0 + 0.7.2-SNAPSHOT spoofax-project @@ -20,7 +20,7 @@ org.metaborg.lang icedust - 0.8.0 + 0.7.2-SNAPSHOT spoofax-language diff --git a/icedust.test/metaborg.yaml b/icedust.test/metaborg.yaml index 80af6358..2c71f1e9 100644 --- a/icedust.test/metaborg.yaml +++ b/icedust.test/metaborg.yaml @@ -1,8 +1,8 @@ -id: org.metaborg:icedust.test:0.8.0 +id: org.metaborg:icedust.test:0.7.2-SNAPSHOT name: IceDust dependencies: compile: - - org.metaborg.lang:icedust:0.8.0 + - org.metaborg.lang:icedust:0.7.2-SNAPSHOT - org.metaborg:org.metaborg.meta.lang.spt:${metaborgVersion} runtime: nabl2: diff --git a/icedust.test/pom.xml b/icedust.test/pom.xml index 57c54c25..5254697a 100644 --- a/icedust.test/pom.xml +++ b/icedust.test/pom.xml @@ -7,7 +7,7 @@ 4.0.0 org.metaborg.lang icedust.test - 0.8.0 + 0.7.2-SNAPSHOT spoofax-test @@ -20,7 +20,7 @@ org.metaborg.lang icedust - 0.8.0 + 0.7.2-SNAPSHOT spoofax-language @@ -39,7 +39,7 @@ spoofax-maven-plugin ${metaborg-version} - org.metaborg.lang:icedust:0.8.0 + org.metaborg.lang:icedust:0.7.2-SNAPSHOT diff --git a/icedust/metaborg.yaml b/icedust/metaborg.yaml index 848d550e..daaa0069 100644 --- a/icedust/metaborg.yaml +++ b/icedust/metaborg.yaml @@ -1,5 +1,5 @@ --- -id: org.metaborg.lang:icedust:0.8.0 +id: org.metaborg.lang:icedust:0.7.2-SNAPSHOT name: icedust dependencies: compile: diff --git a/icedust/pom.xml b/icedust/pom.xml index 1d731555..279a8035 100644 --- a/icedust/pom.xml +++ b/icedust/pom.xml @@ -7,7 +7,7 @@ 4.0.0 org.metaborg.lang icedust - 0.8.0 + 0.7.2-SNAPSHOT spoofax-language diff --git a/pom.xml b/pom.xml index 8d8911a7..af9a242c 100644 --- a/pom.xml +++ b/pom.xml @@ -5,7 +5,7 @@ 4.0.0 icedust.build - 0.8.0 + 0.7.2-SNAPSHOT pom From caef7e3254b95662cfd4f69ae3674bd9c391c135 Mon Sep 17 00:00:00 2001 From: Daco Harkes Date: Mon, 13 Nov 2017 21:26:09 +0100 Subject: [PATCH 03/13] change version from 0.7.2-SNAPSHOT to 0.8.1-SNAPSHOT script --- change_version.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/change_version.sh b/change_version.sh index e0fa9a9f..7988d2cb 100755 --- a/change_version.sh +++ b/change_version.sh @@ -1,4 +1,4 @@ -FROMVERSION=0.7.1 -TOVERSION=0.7.2 +FROMVERSION=0.7.2 +TOVERSION=0.8.1 grep -rEl --exclude=*/target/* --exclude=*/src-gen/* --include=*.{yaml,xml,MF} "${FROMVERSION}(.qualifier|-SNAPSHOT)" * | xargs sed -i "" "s/${FROMVERSION}/${TOVERSION}/g" From 29a7443489cb60ff36718d247d141ec9308200b3 Mon Sep 17 00:00:00 2001 From: Daco Harkes Date: Mon, 13 Nov 2017 21:26:24 +0100 Subject: [PATCH 04/13] change version from 0.7.2-SNAPSHOT to 0.8.1-SNAPSHOT --- icedust.eclipse.feature/feature.xml | 4 ++-- icedust.eclipse.feature/pom.xml | 2 +- icedust.eclipse.site/pom.xml | 2 +- icedust.eclipse.site/site.xml | 2 +- icedust.eclipse/META-INF/MANIFEST.MF | 2 +- icedust.eclipse/pom.xml | 2 +- icedust.example/metaborg.yaml | 2 +- icedust.example/pom.xml | 4 ++-- icedust.test/metaborg.yaml | 4 ++-- icedust.test/pom.xml | 6 +++--- icedust/metaborg.yaml | 2 +- icedust/pom.xml | 2 +- pom.xml | 2 +- 13 files changed, 18 insertions(+), 18 deletions(-) diff --git a/icedust.eclipse.feature/feature.xml b/icedust.eclipse.feature/feature.xml index 9d1d76f7..514e9792 100644 --- a/icedust.eclipse.feature/feature.xml +++ b/icedust.eclipse.feature/feature.xml @@ -2,8 +2,8 @@ - + diff --git a/icedust.eclipse.feature/pom.xml b/icedust.eclipse.feature/pom.xml index 5a39cf23..04dc4c47 100644 --- a/icedust.eclipse.feature/pom.xml +++ b/icedust.eclipse.feature/pom.xml @@ -6,7 +6,7 @@ 4.0.0 org.metaborg.lang icedust.eclipse.feature - 0.7.2-SNAPSHOT + 0.8.1-SNAPSHOT eclipse-feature diff --git a/icedust.eclipse.site/pom.xml b/icedust.eclipse.site/pom.xml index db5845da..a5b5e2ac 100644 --- a/icedust.eclipse.site/pom.xml +++ b/icedust.eclipse.site/pom.xml @@ -6,7 +6,7 @@ 4.0.0 org.metaborg.lang icedust.eclipse.site - 0.7.2-SNAPSHOT + 0.8.1-SNAPSHOT eclipse-update-site diff --git a/icedust.eclipse.site/site.xml b/icedust.eclipse.site/site.xml index 648d95e6..ccbc1213 100644 --- a/icedust.eclipse.site/site.xml +++ b/icedust.eclipse.site/site.xml @@ -1,6 +1,6 @@ - + diff --git a/icedust.eclipse/META-INF/MANIFEST.MF b/icedust.eclipse/META-INF/MANIFEST.MF index 991d3982..d92b29f2 100644 --- a/icedust.eclipse/META-INF/MANIFEST.MF +++ b/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.7.2.qualifier +Bundle-Version: 0.8.1.qualifier Bundle-Vendor: org.metaborg.lang Bundle-ActivationPolicy: lazy Require-Bundle: org.metaborg.spoofax.eclipse diff --git a/icedust.eclipse/pom.xml b/icedust.eclipse/pom.xml index 2fabb7e9..75497831 100644 --- a/icedust.eclipse/pom.xml +++ b/icedust.eclipse/pom.xml @@ -6,7 +6,7 @@ 4.0.0 org.metaborg.lang icedust.eclipse - 0.7.2-SNAPSHOT + 0.8.1-SNAPSHOT eclipse-plugin diff --git a/icedust.example/metaborg.yaml b/icedust.example/metaborg.yaml index ed53d5f0..d0a2b24d 100644 --- a/icedust.example/metaborg.yaml +++ b/icedust.example/metaborg.yaml @@ -1,4 +1,4 @@ --- dependencies: compile: - - org.metaborg.lang:icedust:0.7.2-SNAPSHOT + - org.metaborg.lang:icedust:0.8.1-SNAPSHOT diff --git a/icedust.example/pom.xml b/icedust.example/pom.xml index f04d7d9a..1cde304f 100644 --- a/icedust.example/pom.xml +++ b/icedust.example/pom.xml @@ -7,7 +7,7 @@ 4.0.0 org.metaborg.lang icedust.example - 0.7.2-SNAPSHOT + 0.8.1-SNAPSHOT spoofax-project @@ -20,7 +20,7 @@ org.metaborg.lang icedust - 0.7.2-SNAPSHOT + 0.8.1-SNAPSHOT spoofax-language diff --git a/icedust.test/metaborg.yaml b/icedust.test/metaborg.yaml index 2c71f1e9..716b9bdf 100644 --- a/icedust.test/metaborg.yaml +++ b/icedust.test/metaborg.yaml @@ -1,8 +1,8 @@ -id: org.metaborg:icedust.test:0.7.2-SNAPSHOT +id: org.metaborg:icedust.test:0.8.1-SNAPSHOT name: IceDust dependencies: compile: - - org.metaborg.lang:icedust:0.7.2-SNAPSHOT + - org.metaborg.lang:icedust:0.8.1-SNAPSHOT - org.metaborg:org.metaborg.meta.lang.spt:${metaborgVersion} runtime: nabl2: diff --git a/icedust.test/pom.xml b/icedust.test/pom.xml index 5254697a..0afb6ac6 100644 --- a/icedust.test/pom.xml +++ b/icedust.test/pom.xml @@ -7,7 +7,7 @@ 4.0.0 org.metaborg.lang icedust.test - 0.7.2-SNAPSHOT + 0.8.1-SNAPSHOT spoofax-test @@ -20,7 +20,7 @@ org.metaborg.lang icedust - 0.7.2-SNAPSHOT + 0.8.1-SNAPSHOT spoofax-language @@ -39,7 +39,7 @@ spoofax-maven-plugin ${metaborg-version} - org.metaborg.lang:icedust:0.7.2-SNAPSHOT + org.metaborg.lang:icedust:0.8.1-SNAPSHOT diff --git a/icedust/metaborg.yaml b/icedust/metaborg.yaml index daaa0069..1edcfa4c 100644 --- a/icedust/metaborg.yaml +++ b/icedust/metaborg.yaml @@ -1,5 +1,5 @@ --- -id: org.metaborg.lang:icedust:0.7.2-SNAPSHOT +id: org.metaborg.lang:icedust:0.8.1-SNAPSHOT name: icedust dependencies: compile: diff --git a/icedust/pom.xml b/icedust/pom.xml index 279a8035..22713889 100644 --- a/icedust/pom.xml +++ b/icedust/pom.xml @@ -7,7 +7,7 @@ 4.0.0 org.metaborg.lang icedust - 0.7.2-SNAPSHOT + 0.8.1-SNAPSHOT spoofax-language diff --git a/pom.xml b/pom.xml index af9a242c..f59df844 100644 --- a/pom.xml +++ b/pom.xml @@ -5,7 +5,7 @@ 4.0.0 icedust.build - 0.7.2-SNAPSHOT + 0.8.1-SNAPSHOT pom From c0c14aedf83309110537c43f64d64bfef5ea333d Mon Sep 17 00:00:00 2001 From: Daco Harkes Date: Mon, 13 Nov 2017 21:34:12 +0100 Subject: [PATCH 05/13] Revert "update build-badge url" This reverts commit 5c55154df69bf4fd5b07c4040573389acf0adc34. --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 7c8e5774..2203f0a5 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -[![Build status](http://buildfarm.metaborg.org/job/metaborgcube/job/IceDust/job/master/badge/icon)](http://buildfarm.metaborg.org/job/metaborgcube/job/IceDust/job/master/) +[![Build status](http://buildfarm.metaborg.org/job/metaborgcube/job/IceDust/job/develop/badge/icon)](http://buildfarm.metaborg.org/job/metaborgcube/job/IceDust/job/develop/) # IceDust ![](icedust/icons/icedust-32x32.png "IceDust logo") From 83543edd98645a99aa433b76d6d5e4f0af8e3758 Mon Sep 17 00:00:00 2001 From: Nick ten Veen Date: Wed, 15 Nov 2017 14:14:12 +0100 Subject: [PATCH 06/13] icedust pom still had version 2.2.1 --- icedust/pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/icedust/pom.xml b/icedust/pom.xml index 22713889..8cade971 100644 --- a/icedust/pom.xml +++ b/icedust/pom.xml @@ -13,7 +13,7 @@ org.metaborg parent.language - 2.2.1 + 2.3.0 From d62fe9f5c81d788abc7153c117c1d0b031000b5c Mon Sep 17 00:00:00 2001 From: Daco Harkes Date: Thu, 30 Nov 2017 17:29:49 +0100 Subject: [PATCH 07/13] started with multiplicity proof for interpreter with environment --- icedust.proofs/multiplicities2.v | 186 +++++++++++++++++++++++++++++++ 1 file changed, 186 insertions(+) create mode 100644 icedust.proofs/multiplicities2.v diff --git a/icedust.proofs/multiplicities2.v b/icedust.proofs/multiplicities2.v new file mode 100644 index 00000000..287c1640 --- /dev/null +++ b/icedust.proofs/multiplicities2.v @@ -0,0 +1,186 @@ +(* +This is an extension of multiplicities.v with expressions that use environments + +Under construction +*) + +Require Import List. +Import ListNotations. +Require Import Coq.Init.Nat. +Require Import Coq.Strings.String. +Require Export Coq.FSets.FMapWeakList. +Require Export Coq.Structures.DecidableType. +Module StringEQ <: DecidableType. + Definition t := string. + Definition eq := @eq t. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + Definition eq_dec := string_dec. +End StringEQ. +Module M := FMapWeakList.Make(StringEQ). + +(***** higher order helper functions *****) +Fixpoint list_pair_with {X Y : Type} (lx : list X) (y : Y) : list (X*Y) := + match lx with + | [] => [] + | x :: tx => (x, y) :: (list_pair_with tx y) + end. + +Fixpoint list_pair_with2 {X Y : Type} (x : X) (ly : list Y) : list (X*Y) := + match ly with + | [] => [] + | y :: ty => (x, y) :: (list_pair_with2 x ty) + end. + +Fixpoint list_crossproduct {X Y : Type} + (lx : list X) (ly : list Y) : list (X*Y) := + match lx with + | [] => [] + | x :: tx => (list_pair_with2 x ly) ++ (list_crossproduct tx ly) + end. + +Fixpoint fmap {A B:Type} (f:A -> option B) (l:list A) : list B := + match l with + | nil => nil + | cons x t => + match f x with + | None => (fmap f t) + | Some y => y :: (fmap f t) + end + end. + +Fixpoint foldo {A:Type} (f:A->A->A) (l:list A) : option A := + match l with + | [] => None + | h :: t => Some(fold_left f t h) + end. + +Function to_list {X:Type} (v : option X) : list X := + match v with + | None => [] + | Some x => [x] + end. + +Function funtuple {X Y Z : Type} (f: X -> Y -> Z) (t:X*Y) : Z := + match t with + | (v1, v2) => f v1 v2 + end. + +Function iftuple {X : Type} (t : (bool*(X*X))) : X := + match t with + | (true, (v2, _ )) => v2 + | (false, (_ , v3)) => v3 + end. + +(***** Signatures *****) +Inductive expr : Type := + | EInt : nat -> expr + | ETrue : expr + | EFalse : expr + | EAnd : expr -> expr -> expr + | EPlus : expr -> expr -> expr + | EVar : string -> expr + | EFilter : expr -> string -> expr -> expr. + +Inductive val : Type := + | intv : list nat -> val + | boolv : list bool -> val. + +Definition env: Type := M.t val. + +(***** helper functions *****) +Definition get (m : env) (k : string) := + M.find k m. + +Definition set (m : env) (k : string) (v : val) := + M.add k v m. + +Definition empty := + M.empty nat. + +(***** Interpreter *****) +Reserved Notation "env '|-' e '\\' v" + (at level 50, left associativity). + +Inductive evalR : env -> expr -> val -> Prop := + | E_Int : forall env (n:nat), + env |- EInt n \\ intv [n] + + | E_True : forall env, + env |- ETrue \\ boolv [true] + + | E_False : forall env, + env |- EFalse \\ boolv [false] + + | E_And : forall env (e1 e2 : expr) v1s v2s vtuples, + env |- e1 \\ boolv v1s -> + env |- e2 \\ boolv v2s -> + vtuples = list_crossproduct v1s v2s -> + env |- EAnd e1 e2 \\ boolv (map (funtuple andb) vtuples) + + | E_Plus : forall env (e1 e2 : expr) v1s v2s vtuples, + env |- e1 \\ intv v1s -> + env |- e2 \\ intv v2s -> + vtuples = list_crossproduct v1s v2s -> + env |- EPlus e1 e2 \\ intv (map (funtuple plus) vtuples) + + | E_Var_Bool : forall env n v1s, + Some (boolv v1s) = get env n -> + env |- EVar n \\ boolv v1s + + (* add filter *) + +where "env '|-' e '\\' v" := (evalR env e v) : type_scope. + +Fixpoint evalF (env : env) (e : expr) : option val := + match e with + | EInt n => + Some (intv [n]) + + | ETrue => + Some (boolv [true]) + + | EFalse => + Some (boolv [false]) + + | EAnd e1 e2 => + let v1 := evalF env e1 in + let v2 := evalF env e2 in + match v1, v2 with + | Some (boolv v1s), Some (boolv v2s) => + let vtuples := list_crossproduct v1s v2s in + let vs := map (funtuple andb) vtuples in + Some (boolv vs) + | _,_ => None + end + + | EPlus e1 e2 => + let v1 := evalF env e1 in + let v2 := evalF env e2 in + match v1, v2 with + | Some (intv v1s), Some (intv v2s) => + let vtuples := list_crossproduct v1s v2s in + let vs := map (funtuple plus) vtuples in + Some (intv vs) + | _,_ => None + end + + | EVar n => + let v1 := get env n in + v1 + + | EFilter e1 n e2 => (* implement filter instead of lambda *) + let v1 := evalF env e1 in + match v1 with + | Some (boolv v1s) => + let env' := set env n (boolv v1s) in (* use fold over elements *) + let v2 := evalF env' e2 in + v2 + | Some (intv v1s) => + let env' := set env n (intv v1s) in + let v2 := evalF env' e2 in + v2 + | None => None + end + end. From 2fc8c5aae27ebd4009efa3fdfa02af01cb714006 Mon Sep 17 00:00:00 2001 From: Daco Harkes Date: Fri, 8 Dec 2017 16:26:38 +0100 Subject: [PATCH 08/13] get through Java 1.7 type checker --- icedust/lib-java/src/lib/icedust/Expressions.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/icedust/lib-java/src/lib/icedust/Expressions.java b/icedust/lib-java/src/lib/icedust/Expressions.java index 491587c1..55e700e9 100644 --- a/icedust/lib-java/src/lib/icedust/Expressions.java +++ b/icedust/lib-java/src/lib/icedust/Expressions.java @@ -33,12 +33,12 @@ public static E choice_One_One(E e1, E e2) { @SuppressWarnings("unchecked") public static Collection choice_One_Many(T e1, Collection e2) { - return e1 != null ? toCollection(e1) : (Collection) e2; + return e1 != null ? (Collection) toCollection(e1) : (Collection) e2; } @SuppressWarnings("unchecked") public static Collection choice_Many_One(Collection e1, U e2) { - return e1.size() > 0 ? (Collection) e1 : e2 != null ? toCollection(e2) : (Collection) e1; + return e1.size() > 0 ? (Collection) e1 : e2 != null ? (Collection) toCollection(e2) : (Collection) e1; } @SuppressWarnings("unchecked") @@ -553,13 +553,13 @@ public static E conditional_One_One_One(Boolean b, E i, E j) { @SuppressWarnings("unchecked") public static Collection conditional_One_One_Many(Boolean b, T i, Collection j) { Collection c = emptyCollection(); - return b == null ? c : b ? toCollection(i) : (Collection) j; + return b == null ? c : b ? (Collection) toCollection(i) : (Collection) j; } @SuppressWarnings("unchecked") public static Collection conditional_One_Many_One(Boolean b, Collection i, U j) { Collection c = emptyCollection(); - return b == null ? c : b ? (Collection) i : toCollection(j); + return b == null ? c : b ? (Collection) i : (Collection) toCollection(j); } @SuppressWarnings("unchecked") From 0b1f5b18870371f7f0fcb1dbc8536cce57bae25e Mon Sep 17 00:00:00 2001 From: Daco Harkes Date: Fri, 8 Dec 2017 17:01:28 +0100 Subject: [PATCH 09/13] WebDSL backend: work around WebDSL/Java type system for generic built in functions. (regression of e6f4db749a43f777986c08ec907a355fd68dc52b) --- .../lib-java/src/lib/icedust/Expressions.java | 102 ++++++++++++++++++ .../lib-webdsl/lib/icedust/Expressions.app | 32 +++--- .../trans/generating/webdsl/expressions.str | 19 ++-- 3 files changed, 131 insertions(+), 22 deletions(-) diff --git a/icedust/lib-java/src/lib/icedust/Expressions.java b/icedust/lib-java/src/lib/icedust/Expressions.java index 55e700e9..49d99e84 100644 --- a/icedust/lib-java/src/lib/icedust/Expressions.java +++ b/icedust/lib-java/src/lib/icedust/Expressions.java @@ -109,6 +109,87 @@ public static Collection difference_Many_Many(Collection e1, c.removeAll(e2); return c; } + + // multiplicity expressions WebDSL types + + public static E choice_One_One_Object(E e1, E e2) { + return e1 != null ? e1 : e2; + } + + public static Collection choice_One_Many_Object(E e1, Collection e2) { + return e1 != null ? toCollection(e1) : e2; + } + + public static Collection choice_Many_One_Object(Collection e1, E e2) { + return e1.size() > 0 ? e1 : e2 != null ? toCollection(e2) : e1; + } + + public static Collection choice_Many_Many_Object(Collection e1, Collection e2) { + return e1.size() > 0 ? e1 : e2; + } + + public static Collection merge_One_One_Object(E e1, E e2) { + Collection c = emptyCollection(); + if (e1 != null) + c.add(e1); + if (e2 != null) + c.add(e2); + return c; + } + + public static Collection merge_One_Many_Object(E e1, Collection e2) { + Collection c = emptyCollection(); + if (e1 != null) + c.add(e1); + c.addAll(e2); + return c; + } + + public static Collection merge_Many_One_Object(Collection e1, E e2) { + Collection c = emptyCollection(); + c.addAll(e1); + if (e2 != null) + c.add(e2); + return c; + } + + public static Collection merge_Many_Many_Object(Collection e1, Collection e2) { + Collection c = emptyCollection(); + c.addAll(e1); + c.addAll(e2); + return c; + } + + public static E difference_One_One_Object(E e1, E e2) { + if (e1 == null) + return null; + if (e1.equals(e2)) + return null; + return e1; + } + + public static E difference_One_Many_Object(E e1, Collection e2) { + if (e1 == null) + return null; + if(e2.contains(e1)) + return null; + return e1; + } + + public static Collection difference_Many_One_Object(Collection e1, E e2) { + Collection c = emptyCollection(); + c.addAll(e1); + if (e2 != null) + c.removeAll(Collections.singleton(e2)); + return c; + } + + public static Collection difference_Many_Many_Object(Collection e1, Collection e2) { + Collection c = emptyCollection(); + c.addAll(e1); + c.removeAll(e2); + return c; + } // math expressions @@ -568,6 +649,27 @@ public static Collection conditional_One_Many_M return (Collection) (b == null ? c : b ? i : j); } + // logic expressions : conditional : WebDSL + + public static E conditional_One_One_One_Object(Boolean b, E i, E j) { + return b == null ? null : b ? i : j; + } + + public static Collection conditional_One_One_Many_Object(Boolean b, E i, Collection j) { + Collection c = emptyCollection(); + return b == null ? c : b ? toCollection(i) : j; + } + + public static Collection conditional_One_Many_One_Object(Boolean b, Collection i, E j) { + Collection c = emptyCollection(); + return b == null ? c : b ? i : toCollection(j); + } + + public static Collection conditional_One_Many_Many_Object(Boolean b, Collection i, Collection j) { + Collection c = emptyCollection(); + return b == null ? c : b ? i : j; + } + // cast expressions public static Float asFloat_One(Integer i) { diff --git a/icedust/lib-webdsl/lib/icedust/Expressions.app b/icedust/lib-webdsl/lib/icedust/Expressions.app index f16ccaf2..9a7abaea 100644 --- a/icedust/lib-webdsl/lib/icedust/Expressions.app +++ b/icedust/lib-webdsl/lib/icedust/Expressions.app @@ -3,18 +3,18 @@ module lib/icedust/Expressions section java implementations native class lib.icedust.Expressions as Expressions{ - static choice_One_One(Object, Object) : Object - static choice_One_Many(Object, List) : List - static choice_Many_One(List, Object) : List - static choice_Many_Many(List, List) : List - static merge_One_One(Object, Object) : List - static merge_One_Many(Object, List) : List - static merge_Many_One(List, Object) : List - static merge_Many_Many(List, List) : List - static difference_One_One(Object, Object) : Object - static difference_One_Many(Object, List) : Object - static difference_Many_One(List, Object) : List - static difference_Many_Many(List, List) : List + static choice_One_One_Object(Object, Object) : Object + static choice_One_Many_Object(Object, List) : List + static choice_Many_One_Object(List, Object) : List + static choice_Many_Many_Object(List, List) : List + static merge_One_One_Object(Object, Object) : List + static merge_One_Many_Object(Object, List) : List + static merge_Many_One_Object(List, Object) : List + static merge_Many_Many_Object(List, List) : List + static difference_One_One_Object(Object, Object) : Object + static difference_One_Many_Object(Object, List) : Object + static difference_Many_One_Object(List, Object) : List + static difference_Many_Many_Object(List, List) : List static first(List) : Object static first(List, Int) : List static indexOf(List, Object) : Int @@ -69,10 +69,10 @@ section java implementations static neq_One_Many(Object, List) : Bool static neq_Many_One(List, Object) : Bool static neq_Many_Many(List, List) : Bool - static conditional_One_One_One(Bool, Object, Object) : Object - static conditional_One_One_Many(Bool, Object, List) : Object - static conditional_One_Many_One(Bool, List, Object) : Object - static conditional_One_Many_Many(Bool, List, List) : Object + static conditional_One_One_One_Object(Bool, Object, Object) : Object + static conditional_One_One_Many_Object(Bool, Object, List) : Object + static conditional_One_Many_One_Object(Bool, List, Object) : Object + static conditional_One_Many_Many_Object(Bool, List, List) : Object static asFloat_One(Int) : Float static asFloat_Many(List ) : List static asInteger_One(Float) : Int diff --git a/icedust/trans/generating/webdsl/expressions.str b/icedust/trans/generating/webdsl/expressions.str index 543a9fd0..dda8f3d2 100644 --- a/icedust/trans/generating/webdsl/expressions.str +++ b/icedust/trans/generating/webdsl/expressions.str @@ -23,11 +23,13 @@ imports // functions rules // WebDSL specific: no generics, explicit casts - webdsl-lib-call-cast = ?If(_,_,_) + webdsl-lib-call-cast-object = ?If(_,_,_) - webdsl-lib-call-cast = ?Merge(_, _) - webdsl-lib-call-cast = ?Difference(_, _) - webdsl-lib-call-cast = ?ChoiceLeft(_, _) + webdsl-lib-call-cast-object = ?Merge(_, _) + webdsl-lib-call-cast-object = ?Difference(_, _) + webdsl-lib-call-cast-object = ?ChoiceLeft(_, _) + + webdsl-lib-call-cast = webdsl-lib-call-cast-object webdsl-lib-call-cast = ?Function("first", _) webdsl-lib-call-cast = ?Function("elemAt",_) @@ -41,14 +43,19 @@ rules // lib expression calls arg* := e; e1* := arg*; x_methodpostfix := e; + if e then + x_methodpostfix2 := $[[x_methodpostfix]_Object] + else + x_methodpostfix2 := x_methodpostfix + end; if e then srt1 := e; result := exp |[ - Expressions.x_methodpostfix(e1*) as srt1 + Expressions.x_methodpostfix2(e1*) as srt1 ]| else result := exp |[ - Expressions.x_methodpostfix(e1*) + Expressions.x_methodpostfix2(e1*) ]| end From c36d0adae12df032c77c8082fd43cabda68bb6d0 Mon Sep 17 00:00:00 2001 From: Daco Harkes Date: Mon, 13 Nov 2017 19:25:05 +0100 Subject: [PATCH 10/13] ctree -> jar --- icedust/editor/Main.esv | 2 +- icedust/metaborg.yaml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/icedust/editor/Main.esv b/icedust/editor/Main.esv index 8cf8d65f..4d62cc1f 100644 --- a/icedust/editor/Main.esv +++ b/icedust/editor/Main.esv @@ -11,6 +11,6 @@ language extensions : ice - provider : target/metaborg/stratego.ctree + provider : target/metaborg/stratego.jar provider : target/metaborg/stratego-javastrat.jar provider : lib-js/nashorn.jar \ No newline at end of file diff --git a/icedust/metaborg.yaml b/icedust/metaborg.yaml index 1edcfa4c..80cbf9b0 100644 --- a/icedust/metaborg.yaml +++ b/icedust/metaborg.yaml @@ -29,7 +29,7 @@ language: sdf: sdf2table: java stratego: - format: ctree + format: jar args: - -la - stratego-lib From 1479c1feb46f9eaf5e1cc039a281b5ddecfcc82e Mon Sep 17 00:00:00 2001 From: Daco Harkes Date: Fri, 8 Dec 2017 17:08:26 +0100 Subject: [PATCH 11/13] change version from 0.8.1-SNAPSHOT to 0.8.1 script --- change_version_to_stable.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/change_version_to_stable.sh b/change_version_to_stable.sh index 372cca50..770a21b5 100755 --- a/change_version_to_stable.sh +++ b/change_version_to_stable.sh @@ -1,5 +1,5 @@ -FROMVERSION=0.7.1 -TOVERSION=0.7.1 +FROMVERSION=0.8.1 +TOVERSION=0.8.1 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" From 73ca9eb4d05060cbbbe7e40570562df68d18d625 Mon Sep 17 00:00:00 2001 From: Daco Harkes Date: Fri, 8 Dec 2017 17:09:15 +0100 Subject: [PATCH 12/13] change version from 0.8.1-SNAPSHOT to 0.8.1 --- icedust.eclipse.feature/feature.xml | 4 ++-- icedust.eclipse.feature/pom.xml | 2 +- icedust.eclipse.site/pom.xml | 2 +- icedust.eclipse.site/site.xml | 2 +- icedust.eclipse/META-INF/MANIFEST.MF | 2 +- icedust.eclipse/pom.xml | 2 +- icedust.example/metaborg.yaml | 2 +- icedust.example/pom.xml | 4 ++-- icedust.test/metaborg.yaml | 4 ++-- icedust.test/pom.xml | 6 +++--- icedust/metaborg.yaml | 2 +- icedust/pom.xml | 2 +- pom.xml | 2 +- 13 files changed, 18 insertions(+), 18 deletions(-) diff --git a/icedust.eclipse.feature/feature.xml b/icedust.eclipse.feature/feature.xml index 514e9792..14ef5217 100644 --- a/icedust.eclipse.feature/feature.xml +++ b/icedust.eclipse.feature/feature.xml @@ -2,8 +2,8 @@ - + diff --git a/icedust.eclipse.feature/pom.xml b/icedust.eclipse.feature/pom.xml index 04dc4c47..d851bdf2 100644 --- a/icedust.eclipse.feature/pom.xml +++ b/icedust.eclipse.feature/pom.xml @@ -6,7 +6,7 @@ 4.0.0 org.metaborg.lang icedust.eclipse.feature - 0.8.1-SNAPSHOT + 0.8.1 eclipse-feature diff --git a/icedust.eclipse.site/pom.xml b/icedust.eclipse.site/pom.xml index a5b5e2ac..f2b083b5 100644 --- a/icedust.eclipse.site/pom.xml +++ b/icedust.eclipse.site/pom.xml @@ -6,7 +6,7 @@ 4.0.0 org.metaborg.lang icedust.eclipse.site - 0.8.1-SNAPSHOT + 0.8.1 eclipse-update-site diff --git a/icedust.eclipse.site/site.xml b/icedust.eclipse.site/site.xml index ccbc1213..817b2e0c 100644 --- a/icedust.eclipse.site/site.xml +++ b/icedust.eclipse.site/site.xml @@ -1,6 +1,6 @@ - + diff --git a/icedust.eclipse/META-INF/MANIFEST.MF b/icedust.eclipse/META-INF/MANIFEST.MF index d92b29f2..77bbeee0 100644 --- a/icedust.eclipse/META-INF/MANIFEST.MF +++ b/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.1.qualifier +Bundle-Version: 0.8.1 Bundle-Vendor: org.metaborg.lang Bundle-ActivationPolicy: lazy Require-Bundle: org.metaborg.spoofax.eclipse diff --git a/icedust.eclipse/pom.xml b/icedust.eclipse/pom.xml index 75497831..d9dd07a6 100644 --- a/icedust.eclipse/pom.xml +++ b/icedust.eclipse/pom.xml @@ -6,7 +6,7 @@ 4.0.0 org.metaborg.lang icedust.eclipse - 0.8.1-SNAPSHOT + 0.8.1 eclipse-plugin diff --git a/icedust.example/metaborg.yaml b/icedust.example/metaborg.yaml index d0a2b24d..a8c8c1a9 100644 --- a/icedust.example/metaborg.yaml +++ b/icedust.example/metaborg.yaml @@ -1,4 +1,4 @@ --- dependencies: compile: - - org.metaborg.lang:icedust:0.8.1-SNAPSHOT + - org.metaborg.lang:icedust:0.8.1 diff --git a/icedust.example/pom.xml b/icedust.example/pom.xml index 1cde304f..56954967 100644 --- a/icedust.example/pom.xml +++ b/icedust.example/pom.xml @@ -7,7 +7,7 @@ 4.0.0 org.metaborg.lang icedust.example - 0.8.1-SNAPSHOT + 0.8.1 spoofax-project @@ -20,7 +20,7 @@ org.metaborg.lang icedust - 0.8.1-SNAPSHOT + 0.8.1 spoofax-language diff --git a/icedust.test/metaborg.yaml b/icedust.test/metaborg.yaml index 716b9bdf..75edfbfa 100644 --- a/icedust.test/metaborg.yaml +++ b/icedust.test/metaborg.yaml @@ -1,8 +1,8 @@ -id: org.metaborg:icedust.test:0.8.1-SNAPSHOT +id: org.metaborg:icedust.test:0.8.1 name: IceDust dependencies: compile: - - org.metaborg.lang:icedust:0.8.1-SNAPSHOT + - org.metaborg.lang:icedust:0.8.1 - org.metaborg:org.metaborg.meta.lang.spt:${metaborgVersion} runtime: nabl2: diff --git a/icedust.test/pom.xml b/icedust.test/pom.xml index 0afb6ac6..05d410a2 100644 --- a/icedust.test/pom.xml +++ b/icedust.test/pom.xml @@ -7,7 +7,7 @@ 4.0.0 org.metaborg.lang icedust.test - 0.8.1-SNAPSHOT + 0.8.1 spoofax-test @@ -20,7 +20,7 @@ org.metaborg.lang icedust - 0.8.1-SNAPSHOT + 0.8.1 spoofax-language @@ -39,7 +39,7 @@ spoofax-maven-plugin ${metaborg-version} - org.metaborg.lang:icedust:0.8.1-SNAPSHOT + org.metaborg.lang:icedust:0.8.1 diff --git a/icedust/metaborg.yaml b/icedust/metaborg.yaml index 80cbf9b0..c8900cc3 100644 --- a/icedust/metaborg.yaml +++ b/icedust/metaborg.yaml @@ -1,5 +1,5 @@ --- -id: org.metaborg.lang:icedust:0.8.1-SNAPSHOT +id: org.metaborg.lang:icedust:0.8.1 name: icedust dependencies: compile: diff --git a/icedust/pom.xml b/icedust/pom.xml index 8cade971..29a1cdb5 100644 --- a/icedust/pom.xml +++ b/icedust/pom.xml @@ -7,7 +7,7 @@ 4.0.0 org.metaborg.lang icedust - 0.8.1-SNAPSHOT + 0.8.1 spoofax-language diff --git a/pom.xml b/pom.xml index f59df844..82b81ff3 100644 --- a/pom.xml +++ b/pom.xml @@ -5,7 +5,7 @@ 4.0.0 icedust.build - 0.8.1-SNAPSHOT + 0.8.1 pom From c5c2b51ebb3c5a3e522225d3fcb498469459f952 Mon Sep 17 00:00:00 2001 From: Daco Harkes Date: Mon, 13 Nov 2017 21:05:48 +0100 Subject: [PATCH 13/13] update build-badge url --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 2203f0a5..7c8e5774 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -[![Build status](http://buildfarm.metaborg.org/job/metaborgcube/job/IceDust/job/develop/badge/icon)](http://buildfarm.metaborg.org/job/metaborgcube/job/IceDust/job/develop/) +[![Build status](http://buildfarm.metaborg.org/job/metaborgcube/job/IceDust/job/master/badge/icon)](http://buildfarm.metaborg.org/job/metaborgcube/job/IceDust/job/master/) # IceDust ![](icedust/icons/icedust-32x32.png "IceDust logo")