diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 767e9aa73..34c499512 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -15,6 +15,8 @@ stages: - ide-build - ide-e2e-test - ide-deploy + - nix + - nix-push # TODO provide sensible CI for master dont-merge-to-master: @@ -42,6 +44,7 @@ dont-merge-to-master: - build-and-package-ubuntu-18-04 - build-and-package-ubuntu-19-10 before_script: + - export COMMIT_DATE="$(git show --no-patch --format=%ci)" - export TERM=dumb - scripts/install_native_dependencies.sh - scripts/install_opam.sh # TODO: or scripts/install_build_environment.sh ? @@ -85,6 +88,7 @@ dont-merge-to-master: before_script: # Install dependencies # rsync is needed by opam to sync a package installed from a local directory with the copy in ~/.opam + - export COMMIT_DATE="$(git show --no-patch --format=%ci)" - export TERM=dumb - scripts/install_native_dependencies.sh - scripts/install_opam.sh # TODO: or scripts/install_build_environment.sh ? @@ -117,6 +121,7 @@ build-current-docker-image: - build-and-package-debian-10 <<: *docker script: + - export COMMIT_DATE="$(git show --no-patch --format=%ci)" - sh scripts/build_docker_image.sh next - sh scripts/test_cli.sh only: @@ -281,3 +286,162 @@ deploy-handoff: rules: - if: '$CI_COMMIT_REF_NAME == "dev"' when: always + + +##### The following jobs will replace the ones above! ##### +# TODO: add jobs for deploying the website, build a docker image and deploy it + +.prepare_nix: &prepare_nix + image: nixos/nix:latest + before_script: + - nix-env -f channel:nixos-unstable -iA gnutar gitMinimal cachix + - export COMMIT_DATE="$(git show --no-patch --format=%ci)" + - echo "sandbox = true" > /etc/nix/nix.conf + # A temporary caching solution + - cachix use balsoft + # TODO Don't upload everything, use a post-build-hook to only upload what can't be substituted + - cachix push -w balsoft & + +# The binary produced is useless by itself +binary-nix: + stage: nix + <<: *prepare_nix + only: + - merge_requests + - dev + - /^.*-run-dev$/ + script: + - nix-build nix -A ligo-bin + +doc-nix: + stage: nix + <<: *prepare_nix + only: + - merge_requests + - dev + - /^.*-run-dev$/ + script: + - nix-build nix -A ligo-doc + - cp -Lr result/share/doc result-doc + artifacts: + paths: + - result-doc + +test-nix: + stage: nix + <<: *prepare_nix + only: + - merge_requests + - dev + - /^.*-run-dev$/ + script: + - nix-build nix -A ligo-coverage + - cp -Lr result/share/coverage result-coverage + artifacts: + paths: + - result-coverage + +# FIXME For some reason, e2e tests can't build on CI. +.webide-e2e-nix: + stage: nix + <<: *prepare_nix + rules: + - changes: + - tools/webide/** + when: always + - if: '$CI_COMMIT_REF_NAME =~ /^(dev|.*-run-dev)$/ && $CI_PROJECT_PATH == "ligolang/ligo"' + when: always + script: + - nix-build nix -A ligo-editor.e2e + +docker-nix: + stage: nix + only: + - merge_requests + - dev + - /^.*-run-dev$/ + <<: *prepare_nix + script: + - nix-build nix -A ligo-docker + - cp -L result ligo.tar.gz + artifacts: + paths: + - ligo.tar.gz + +docker-push-nix: + stage: nix-push + <<: *docker + dependencies: + - docker-nix + needs: + - docker-nix + rules: + # Only deploy docker when from the dev branch AND on the canonical ligolang/ligo repository + - if: '$CI_COMMIT_REF_NAME =~ /^(dev|.*-run-dev)$/ && $CI_PROJECT_PATH == "ligolang/ligo"' + when: always + script: + - echo ${LIGO_REGISTRY_PASSWORD} | docker login -u ${LIGO_REGISTRY_USER} --password-stdin + - docker load -i=./ligo.tar.gz + - export LIGO_REGISTRY_FULL_NAME=${LIGO_REGISTRY_IMAGE_BUILD:-ligolang/ligo}:$(if test "$CI_COMMIT_REF_NAME" = "dev"; then echo next-nix; else echo next-attempt-nix; fi) + - docker tag ligo "${LIGO_REGISTRY_FULL_NAME}" + - docker push "${LIGO_REGISTRY_FULL_NAME}" + +webide-docker-nix: + stage: nix + only: + - merge_requests + - dev + - /^.*-run-dev$/ + <<: *prepare_nix + script: + - nix-build nix -A ligo-editor-docker + - cp -L result webide.tar.gz + artifacts: + paths: + - webide.tar.gz + + +webide-push-nix: + stage: nix-push + <<: *docker + dependencies: + - webide-docker-nix + needs: + - webide-docker-nix + rules: + # Only deploy docker when from the dev branch AND on the canonical ligolang/ligo repository + - if: '$CI_COMMIT_REF_NAME =~ /^(dev|.*-run-dev)$/ && $CI_PROJECT_PATH == "ligolang/ligo"' + when: always + script: + - echo "${CI_BUILD_TOKEN}" | docker login -u gitlab-ci-token --password-stdin registry.gitlab.com + - docker load -i=./webide.tar.gz + - docker tag ligo-editor "${WEBIDE_IMAGE_NAME}:nix${CI_COMMIT_SHORT_SHA}" + - docker push "${WEBIDE_IMAGE_NAME}:nix${CI_COMMIT_SHORT_SHA}" + +static-binary-nix: + stage: nix + <<: *prepare_nix + only: + - dev + - /^.*-run-dev$/ + script: + - nix-build nix -A ligo-static + # Check that the binary is truly static and has 0 dependencies + - test $(nix-store -q --references ./result | wc -l) -eq 0 + - cp -Lr result/bin result-static + artifacts: + paths: + - result-static + +website-nix: + stage: nix + <<: *prepare_nix + only: + - dev + - /^.*-run-dev$/ + script: + - nix-build nix -A ligo-website + - cp -Lr result/ result-website + artifacts: + paths: + - result-website diff --git a/docker/distribution/generic/build.Dockerfile b/docker/distribution/generic/build.Dockerfile index ba01c043c..a9630c79d 100644 --- a/docker/distribution/generic/build.Dockerfile +++ b/docker/distribution/generic/build.Dockerfile @@ -2,7 +2,11 @@ ARG target FROM ocaml/opam2:${target} ARG ci_job_id +ARG ci_commit_sha +ARG commit_date ENV CI_JOB_ID=$ci_job_id +ENV CI_COMMIT_SHA=$ci_commit_sha +ENV COMMIT_DATE=$commit_date RUN opam switch 4.07 && eval $(opam env) diff --git a/gitlab-pages/website/package-lock.json b/gitlab-pages/website/package-lock.json index 43d25ce3e..b42d4b706 100644 --- a/gitlab-pages/website/package-lock.json +++ b/gitlab-pages/website/package-lock.json @@ -1,6 +1,8 @@ { - "requires": true, + "name": "ligo-website", + "version": "0.0.1", "lockfileVersion": 1, + "requires": true, "dependencies": { "@ligolang/docusaurus-theme-compact-ligo-ide": { "version": "file:../../tools/compact-webide/packages/docusaurus-theme-compact-ligo-ide", @@ -1660,7 +1662,12 @@ "debug": { "version": "2.6.9", "requires": { - "ms": "2.0.0" + "@nodelib/fs.stat": "^2.0.2", + "@nodelib/fs.walk": "^1.2.3", + "glob-parent": "^5.1.0", + "merge2": "^1.3.0", + "micromatch": "^4.0.2", + "picomatch": "^2.2.1" } }, "decamelize": { @@ -2017,10 +2024,8 @@ "fill-range": { "version": "4.0.0", "requires": { - "extend-shallow": "^2.0.1", - "is-number": "^3.0.0", - "repeat-string": "^1.6.1", - "to-regex-range": "^2.1.0" + "@docusaurus/types": "^2.0.0-alpha.50", + "sitemap": "^3.2.2" } }, "find-up": { diff --git a/gitlab-pages/website/package.json b/gitlab-pages/website/package.json index 8fa752c2e..75ac51078 100644 --- a/gitlab-pages/website/package.json +++ b/gitlab-pages/website/package.json @@ -1,4 +1,6 @@ { + "name": "ligo-website", + "version": "0.0.1", "scripts": { "start": "docusaurus start --host 0.0.0.0 --port 3000", "build": "docusaurus build", diff --git a/nix/default.nix b/nix/default.nix new file mode 100644 index 000000000..cf7a81e2f --- /dev/null +++ b/nix/default.nix @@ -0,0 +1,9 @@ +{ sources ? import ./sources.nix }@args: +let pkgs = import ./pkgs.nix args; +in { + inherit (pkgs) + ligo ligo-tests ligo-doc ligo-coverage + ligo-bin ligo-static ligo-docker ligo-deb + ligo-editor ligo-editor-docker + ligo-website; +} diff --git a/nix/docker.nix b/nix/docker.nix new file mode 100644 index 000000000..acda1c971 --- /dev/null +++ b/nix/docker.nix @@ -0,0 +1,10 @@ +{ dockerTools, writeShellScriptBin, runCommand, mcpp, bash, coreutils, ligo, name ? "ligo" }: +let + tmp = runCommand "tmp" {} "mkdir -p $out/tmp"; +in +dockerTools.buildLayeredImage { + inherit name; + tag = "latest"; + contents = [ ligo tmp bash ]; + config.Entrypoint = name; +} diff --git a/nix/ligo-editor.nix b/nix/ligo-editor.nix new file mode 100644 index 000000000..9a1a88920 --- /dev/null +++ b/nix/ligo-editor.nix @@ -0,0 +1,71 @@ +{ stdenv, lib, mkYarnPackage, nodejs, python2, ligo-bin, coreutils +, writeShellScriptBin, makeFontsConf, buildEnv, rsync, sources +, chromium ? null }: +let + yarnLock = ../tools/webide/yarn.lock; + + installPhase = "mkdir $out; cp -Lr node_modules $out/node_modules"; + + server = mkYarnPackage { + name = "webide-server"; + src = ../tools/webide/packages/server; + buildPhase = '' + cp ${../tools/webide/tsconfig.json} tsconfig.json + yarn --offline run build + rm node_modules/server/server + ''; + doCheck = true; + checkPhase = "DATA_DIR=/tmp LIGO_CMD=${ligo-bin}/bin/ligo yarn --offline jest"; + distPhase = "true"; + inherit yarnLock installPhase; + }; + client = mkYarnPackage rec { + name = "webide-client"; + src = ../tools/webide/packages/client; + buildPhase = '' + export EXAMPLES_DIR=${../src/test/examples} + yarn --offline run build + rm node_modules/client/client + find deps/client/build -type f -exec sed -r "s,/nix/store/[a-z0-9]{32}-[^/]*,$out,g" -i '{}' \; + ''; + distPhase = "true"; + installPhase = "mkdir $out; cp -Lr deps/client/build $out"; + inherit yarnLock; + # Downloads node-sass from the official github repo + # Uncomment the commented lines if you wish to build it from source + yarnPreBuild = "export SASS_BINARY_PATH=${sources.node-sass-bin}"; + /* '' + mkdir -p "$HOME/.node-gyp/${nodejs.version}" + echo 9 > "$HOME/.node-gyp/${nodejs.version}/installVersion" + ln -sfv "${nodejs}/include" "$HOME/.node-gyp/${nodejs.version}" + ''; + */ + }; + + e2e = mkYarnPackage rec { + name = "webide-e2e"; + src = ../tools/webide/packages/e2e; + # Provide puppeteer with chromium, since it can't download it inside the nix sandbox. + # Also, since we override nodejs in our overlays, import chromium from pure nixpkgs to avoid a rebuild + buildPhase = '' + export HOME="$(pwd)" + export PUPPETEER_SKIP_CHROMIUM_DOWNLOAD=1 + export PUPPETEER_EXECUTABLE_PATH=${(import (import ./sources.nix).nixpkgs {}).chromium.outPath}/bin/chromium + ${ligo-editor}/bin/ligo-editor & + export API_HOST=http://localhost:8080 + export FONTCONFIG_FILE=${makeFontsConf { fontDirectories = [ ]; }} + yarn --offline jest + ''; + distPhase = "true"; + installPhase = "touch $out"; + inherit yarnLock; + }; + + ligo-editor = writeShellScriptBin "ligo-editor" '' + set -e + LIGO_CMD=${ligo-bin}/bin/ligo \ + STATIC_ASSETS=${client} \ + DATA_DIR=/tmp \ + ${nodejs}/bin/node ${server}/node_modules/server/dist/src/index.js + ''; +in ligo-editor // { inherit e2e; } diff --git a/nix/ligo-website.nix b/nix/ligo-website.nix new file mode 100644 index 000000000..5e95e7b8c --- /dev/null +++ b/nix/ligo-website.nix @@ -0,0 +1,18 @@ +{ buildNpmPackage, writeShellScriptBin, yarn, linkFarm, nodejs-slim, python2 +, ligo-doc, ligo-deb, ligo-static }: +buildNpmPackage { + src = ../gitlab-pages/website; + npmBuild = "npm run build"; + preBuild = '' + cp -r ${../gitlab-pages/docs} $NIX_BUILD_TOP/docs + chmod 700 -R $NIX_BUILD_TOP/docs + ''; + installPhase = '' + cp -Lr build $out + cp -r ${ligo-deb}/* $out/deb + mkdir -p $out/bin/linux + cp -r ${ligo-static}/bin/ligo $out/bin/linux/ligo + cp -r ${ligo-doc}/share/doc $out/odoc + ''; + extraEnvVars.nativeBuildInputs = [ python2 ]; +} diff --git a/nix/mac-overlay.nix b/nix/mac-overlay.nix new file mode 100644 index 000000000..8cbedb0b9 --- /dev/null +++ b/nix/mac-overlay.nix @@ -0,0 +1,9 @@ +oself: osuper: +let + fixHardeningWarning = pkg: pkg.overrideAttrs (_: { + hardeningDisable = [ "strictoverflow" ]; + }); +in +{ + hacl = fixHardeningWarning osuper.hacl; +} diff --git a/nix/nodejs-overlay.nix b/nix/nodejs-overlay.nix new file mode 100644 index 000000000..7a5badf30 --- /dev/null +++ b/nix/nodejs-overlay.nix @@ -0,0 +1,5 @@ +self: super: { + nodejs = super.nodejs-12_x; + nodePackages = super.nodePackages_12_x; + nodejs-slim = super.nodejs-slim-12_x; +} diff --git a/nix/ocaml-overlay.nix b/nix/ocaml-overlay.nix new file mode 100644 index 000000000..d811becad --- /dev/null +++ b/nix/ocaml-overlay.nix @@ -0,0 +1,140 @@ +{ sources ? import ./sources.nix +, CI_COMMIT_SHA ? builtins.getEnv "CI_COMMIT_SHA" +, COMMIT_DATE ? builtins.getEnv "COMMIT_DATE" }: +self: super: +let + opam-nix = import sources.opam-nix (import sources.nixpkgs { }); + inherit (import sources."gitignore.nix" { inherit (self) lib; }) + gitignoreSource; + filterOut = xs: + self.lib.cleanSourceWith { + filter = p: type: !(builtins.elem (builtins.baseNameOf p) xs); + src = gitignoreSource ../.; + }; +in { + ocamlPackages = self.ocaml-ng.ocamlPackages_4_07.overrideScope' + (builtins.foldl' self.lib.composeExtensions (_: _: { }) [ + (opam-nix.traverseOPAMRepo' sources.opam-repository) + (opam-nix.traverseOPAMRepo sources.tezos-opam-repository) + (opam-nix.callOPAMPackage (filterOut [ + ".git" + ".gitlab-ci.yml" + ".gitignore" + "nix" + "docker" + "tools" + "gitlab-pages" + ])) + (oself: osuper: { + ocamlfind = oself.findlib; + lablgtk = null; + lwt = oself.lwt4; + + conf-gmp = self.gmp; + conf-libev = self.libev; + conf-hidapi = self.hidapi; + conf-pkg-config = self.pkg-config; + + bigstring = osuper.bigstring.overrideAttrs (_: { doCheck = false; }); + xmldiff = osuper.xmldiff.overrideAttrs (_: { src = sources.xmldiff; }); + getopt = osuper.getopt.overrideAttrs (_: { configurePhase = "true"; }); + + ipaddr = osuper.ipaddr.versions."4.0.0"; + conduit = osuper.conduit.versions."2.1.0"; + conduit-lwt-unix = osuper.conduit-lwt-unix.versions."2.0.2"; + cohttp-lwt-unix = osuper.cohttp-lwt-unix.versions."2.4.0"; + cohttp-lwt = osuper.cohttp-lwt.versions."2.4.0"; + macaddr = osuper.macaddr.versions."4.0.0"; + ocaml-migrate-parsetree = + osuper.ocaml-migrate-parsetree.versions."1.4.0"; + ppx_tools_versioned = osuper.ppx_tools_versioned.versions."5.2.3"; + bisect_ppx = osuper.bisect_ppx.versions."2.0.0".overrideAttrs (_: { + src = builtins.fetchTarball + "https://github.com/aantron/bisect_ppx/archive/02dfb10188033a26d07d23480c2bc44a3a670357.tar.gz"; + }); + + proto-alpha-utils = osuper.proto-alpha-utils.overrideAttrs (oa: rec { + buildInputs = oa.buildInputs + ++ [ oself.tezos-protocol-006-PsCARTHA-parameters ]; + propagatedBuildInputs = buildInputs; + }); + tezos-protocol-compiler = osuper.tezos-protocol-compiler.overrideAttrs + (oa: rec { + buildInputs = oa.buildInputs ++ [ oself.pprint ]; + propagatedBuildInputs = buildInputs; + }); + + ligo = self.buildEnv { + name = "ligo"; + paths = with oself; [ + ligo-out.out + ligo-tests + ligo-doc + ligo-coverage + ]; + }; + + ligo-out = osuper.ligo.overrideAttrs (oa: { + name = "ligo-out"; + inherit CI_COMMIT_SHA COMMIT_DATE; + buildInputs = oa.buildInputs + ++ [ oself.UnionFind oself.Preprocessor ]; + nativeBuildInputs = oa.nativeBuildInputs + ++ [ self.buildPackages.rakudo ]; + }); + ligo-tests = osuper.ligo.overrideAttrs (oa: { + name = "ligo-tests"; + src = filterOut [ + ".git" + ".gitlab-ci.yml" + ".gitignore" + "nix" + "docker" + "tools" + ]; + outputs = [ "out" ]; + buildPhase = "dune runtest"; + nativeBuildInputs = oa.nativeBuildInputs + ++ [ self.buildPackages.rakudo ]; + installPhase = "mkdir $out"; + }); + ligo-doc = osuper.ligo.overrideAttrs (oa: { + name = "ligo-doc"; + buildInputs = oa.buildInputs + ++ [ oself.odoc oself.tezos-protocol-updater ]; + outputs = [ "out" ]; + buildPhase = "dune build @doc"; + nativeBuildInputs = oa.nativeBuildInputs + ++ [ self.buildPackages.rakudo ]; + installPhase = + "mkdir $out; cp -r _build/default/_doc/_html/ $out/doc"; + }); + ligo-coverage = oself.ligo-tests.overrideAttrs (oa: { + name = "ligo-coverage"; + nativeBuildInputs = oa.nativeBuildInputs + ++ [ self.buildPackages.rakudo ]; + buildPhase = '' + # Needed for coverage and nothing else + mkdir -p $out/share/coverage + echo "Coverage:" + BISECT_ENABLE=yes dune runtest --force + bisect-ppx-report html -o $out/share/coverage/all --title="LIGO overall test coverage" + bisect-ppx-report summary --per-file + echo "Test coverage:" + BISECT_ENABLE=yes dune runtest src/test --force + bisect-ppx-report html -o $out/share/coverage/ligo --title="LIGO test coverage" + bisect-ppx-report summary --per-file + echo "Doc coverage:" + BISECT_ENABLE=yes dune build @doc-test --force + bisect-ppx-report html -o $out/share/coverage/docs --title="LIGO doc coverage" + bisect-ppx-report summary --per-file + echo "CLI test coverage:" + BISECT_ENABLE=yes dune runtest src/bin/expect_tests + bisect-ppx-report html -o $out/share/coverage/cli --title="CLI test coverage" + bisect-ppx-report summary --per-file + ''; + installPhase = "true"; + }); + }) + ]); +} diff --git a/nix/packageDeb.nix b/nix/packageDeb.nix new file mode 100644 index 000000000..bb5f0a57b --- /dev/null +++ b/nix/packageDeb.nix @@ -0,0 +1,46 @@ +{ stdenv, lib, writeTextFile, ligo-static, dpkg }: +let + project = "ligo"; + version = "0.0.0"; + revision = lib.commitIdFromGitRepo ../.git; + pkgArch = "amd64"; + bin = "${ligo-static}/bin/ligo"; + pkgName = "${project}_0ubuntu${version}-${revision}_${pkgArch}"; + depends = ""; + maintainer = "ligolang ligolang.org"; + description = "A friendly Smart Contract Language for Tezos"; + + writeControlFile = writeTextFile { + name = "control"; + text = '' + Package: ${project} + Version: ${version}-${revision} + Priority: optional + Architecture: ${pkgArch} + Depends: ${depends} + Maintainer: ${maintainer} + Description: ${project} + ${description} + ''; + }; + +in stdenv.mkDerivation rec { + name = "${pkgName}.deb"; + + nativeBuildInputs = [ dpkg ]; + + phases = "packagePhase"; + + packagePhase = '' + mkdir ${pkgName} + mkdir -p ${pkgName}/usr/local/bin + cp ${bin} ${pkgName}/usr/local/bin/${project} + + mkdir ${pkgName}/DEBIAN + cp ${writeControlFile} ${pkgName}/DEBIAN/control + + dpkg-deb --build ${pkgName} + mkdir -p $out + cp ${name} $out/ + ''; +} diff --git a/nix/pkgs.nix b/nix/pkgs.nix new file mode 100644 index 000000000..d832dde56 --- /dev/null +++ b/nix/pkgs.nix @@ -0,0 +1,33 @@ +{ sources ? import ./sources.nix }: +let + ocaml-overlay = import ./ocaml-overlay.nix { inherit sources; }; + static-overlay = import ./static-overlay.nix pkgs; + mac-overlay = import ./mac-overlay.nix; + nodejs-overlay = import ./nodejs-overlay.nix; + pkgs = import sources.nixpkgs { + overlays = [ ocaml-overlay nodejs-overlay ] + ++ (if builtins.currentSystem == "x86_64-darwin" + then [ mac-overlay ] + else [ ]); + }; + separateBinary = pkg: + pkgs.runCommandNoCC "${pkg.name}-bin" { } + "mkdir -p $out/bin; cp -Lr ${pkg}/ligo $out/bin"; + + nix-npm-buildpackage = pkgs.callPackage sources.nix-npm-buildpackage { }; +in pkgs.extend (self: super: { + inherit (self.ocamlPackages) ligo ligo-out ligo-tests ligo-doc ligo-coverage; + ligo-bin = separateBinary self.ligo-out.bin; + ligo-docker = self.callPackage ./docker.nix { ligo = self.ligo-bin; }; + ligo-deb = self.callPackage ./packageDeb.nix { }; + ligo-editor = self.callPackage ./ligo-editor.nix { inherit sources; }; + ligo-editor-docker = self.callPackage ./docker.nix { + ligo = self.ligo-editor; + name = "ligo-editor"; + }; + ligo-website = self.callPackage ./ligo-website.nix { + inherit (nix-npm-buildpackage) buildNpmPackage; + }; + ligo-static = self.pkgsMusl.ligo-bin; + pkgsMusl = super.pkgsMusl.extend static-overlay; +}) diff --git a/nix/sources.json b/nix/sources.json new file mode 100644 index 000000000..8af15c341 --- /dev/null +++ b/nix/sources.json @@ -0,0 +1,87 @@ +{ + "gitignore.nix": { + "branch": "master", + "description": "Nix function for filtering local git sources", + "homepage": "", + "owner": "hercules-ci", + "repo": "gitignore.nix", + "rev": "2ced4519f865341adcb143c5d668f955a2cb997f", + "sha256": "0fc5bgv9syfcblp23y05kkfnpgh3gssz6vn24frs8dzw39algk2z", + "type": "tarball", + "url": "https://github.com/hercules-ci/gitignore.nix/archive/2ced4519f865341adcb143c5d668f955a2cb997f.tar.gz", + "url_template": "https://github.com///archive/.tar.gz" + }, + "nix-npm-buildpackage": { + "branch": "balsoft/local-deps", + "description": "Build nix packages that use npm/yarn", + "homepage": "", + "owner": "serokell", + "repo": "nix-npm-buildpackage", + "rev": "14d03b37cd421b281835ae245b6cbf5b84c26e80", + "sha256": "13lz138rcy2vfd13sa4l2r4y5nx7v5pslxfy1vdq2phpmnn9j9yb", + "type": "tarball", + "url": "https://github.com/serokell/nix-npm-buildpackage/archive/14d03b37cd421b281835ae245b6cbf5b84c26e80.tar.gz", + "url_template": "https://github.com///archive/.tar.gz" + }, + "nixpkgs": { + "branch": "nixos-unstable", + "description": "Pinned Nixpkgs tree (master follows nixos-unstable-small, only tags have stable history)", + "homepage": "", + "owner": "nixos", + "repo": "nixpkgs-channels", + "rev": "3320a06049fc259e87a2bd98f4cd42f15f746b96", + "sha256": "1g5l186d5xh187vdcpfsz1ff8s749949c1pclvzfkylpar09ldkl", + "type": "tarball", + "url": "https://github.com/nixos/nixpkgs-channels/archive/3320a06049fc259e87a2bd98f4cd42f15f746b96.tar.gz", + "url_template": "https://github.com///archive/.tar.gz" + }, + "node-sass-bin": { + "sha256": "0dl91l414na44h090cgghd06q0j2whlj9h98im2qb9823glq7xff", + "type": "file", + "url": "https://github.com/sass/node-sass/releases/download/v4.12.0/linux-x64-64_binding.node", + "url_template": "https://github.com/sass/node-sass/releases/download/v/linux-x64-64_binding.node", + "version": "4.12.0" + }, + "opam-nix": { + "branch": "master", + "description": "A handy nix library to package OCaml software from OPAM repositories", + "homepage": null, + "owner": "balsoft", + "repo": "opam-nix", + "rev": "75ad75c18b8d80d82c13dc30c3b8d70960b1b441", + "sha256": "0mcr32f5i71diysvpblbvgdnx2pdymwjb9nxz5gbcsib3vdg2p83", + "type": "tarball", + "url": "https://github.com/balsoft/opam-nix/archive/75ad75c18b8d80d82c13dc30c3b8d70960b1b441.tar.gz", + "url_template": "https://github.com///archive/.tar.gz" + }, + "opam-repository": { + "branch": "master", + "description": "Main public package repository for OPAM, the source package manager of OCaml.", + "homepage": "https://opam.ocaml.org", + "owner": "ocaml", + "repo": "opam-repository", + "rev": "d67e70b40203a6a1c77ccb2edbe136c1509a73a3", + "sha256": "1yphw9xcss284p51qnml5jvfs4mhjcjgdka3wk25q0437zdzqj4n", + "type": "tarball", + "url": "https://github.com/ocaml/opam-repository/archive/d67e70b40203a6a1c77ccb2edbe136c1509a73a3.tar.gz", + "url_template": "https://github.com///archive/.tar.gz" + }, + "tezos-opam-repository": { + "ref": "master", + "repo": "https://gitlab.com/ligolang/tezos-opam-repository", + "rev": "dfc46bd895b070bd89028a7ad98741d05ec684df", + "type": "git" + }, + "xmldiff": { + "branch": "master", + "description": "Diffs on XML trees", + "homepage": "http://zoggy.github.io/xmldiff", + "owner": "zoggy", + "repo": "xmldiff", + "rev": "5873df80c1ba8c79287dc42e5008fac14cefffed", + "sha256": "0b92j9j2xdd2gyi9bgp39w0w1lkp0vc2rxq6wx6xdfvvklpprgb4", + "type": "tarball", + "url": "https://github.com/zoggy/xmldiff/archive/5873df80c1ba8c79287dc42e5008fac14cefffed.tar.gz", + "url_template": "https://github.com///archive/.tar.gz" + } +} diff --git a/nix/sources.nix b/nix/sources.nix new file mode 100644 index 000000000..8a725cb4e --- /dev/null +++ b/nix/sources.nix @@ -0,0 +1,134 @@ +# This file has been generated by Niv. + +let + + # + # The fetchers. fetch_ fetches specs of type . + # + + fetch_file = pkgs: spec: + if spec.builtin or true then + builtins_fetchurl { inherit (spec) url sha256; } + else + pkgs.fetchurl { inherit (spec) url sha256; }; + + fetch_tarball = pkgs: spec: + if spec.builtin or true then + builtins_fetchTarball { inherit (spec) url sha256; } + else + pkgs.fetchzip { inherit (spec) url sha256; }; + + fetch_git = spec: + builtins.fetchGit { url = spec.repo; inherit (spec) rev ref; }; + + fetch_builtin-tarball = spec: + builtins.trace + '' + WARNING: + The niv type "builtin-tarball" will soon be deprecated. You should + instead use `builtin = true`. + + $ niv modify -a type=tarball -a builtin=true + '' + builtins_fetchTarball { inherit (spec) url sha256; }; + + fetch_builtin-url = spec: + builtins.trace + '' + WARNING: + The niv type "builtin-url" will soon be deprecated. You should + instead use `builtin = true`. + + $ niv modify -a type=file -a builtin=true + '' + (builtins_fetchurl { inherit (spec) url sha256; }); + + # + # Various helpers + # + + # The set of packages used when specs are fetched using non-builtins. + mkPkgs = sources: + let + sourcesNixpkgs = + import (builtins_fetchTarball { inherit (sources.nixpkgs) url sha256; }) {}; + hasNixpkgsPath = builtins.any (x: x.prefix == "nixpkgs") builtins.nixPath; + hasThisAsNixpkgsPath = == ./.; + in + if builtins.hasAttr "nixpkgs" sources + then sourcesNixpkgs + else if hasNixpkgsPath && ! hasThisAsNixpkgsPath then + import {} + else + abort + '' + Please specify either (through -I or NIX_PATH=nixpkgs=...) or + add a package called "nixpkgs" to your sources.json. + ''; + + # The actual fetching function. + fetch = pkgs: name: spec: + + if ! builtins.hasAttr "type" spec then + abort "ERROR: niv spec ${name} does not have a 'type' attribute" + else if spec.type == "file" then fetch_file pkgs spec + else if spec.type == "tarball" then fetch_tarball pkgs spec + else if spec.type == "git" then fetch_git spec + else if spec.type == "builtin-tarball" then fetch_builtin-tarball spec + else if spec.type == "builtin-url" then fetch_builtin-url spec + else + abort "ERROR: niv spec ${name} has unknown type ${builtins.toJSON spec.type}"; + + # Ports of functions for older nix versions + + # a Nix version of mapAttrs if the built-in doesn't exist + mapAttrs = builtins.mapAttrs or ( + f: set: with builtins; + listToAttrs (map (attr: { name = attr; value = f attr set.${attr}; }) (attrNames set)) + ); + + # fetchTarball version that is compatible between all the versions of Nix + builtins_fetchTarball = { url, sha256 }@attrs: + let + inherit (builtins) lessThan nixVersion fetchTarball; + in + if lessThan nixVersion "1.12" then + fetchTarball { inherit url; } + else + fetchTarball attrs; + + # fetchurl version that is compatible between all the versions of Nix + builtins_fetchurl = { url, sha256 }@attrs: + let + inherit (builtins) lessThan nixVersion fetchurl; + in + if lessThan nixVersion "1.12" then + fetchurl { inherit url; } + else + fetchurl attrs; + + # Create the final "sources" from the config + mkSources = config: + mapAttrs ( + name: spec: + if builtins.hasAttr "outPath" spec + then abort + "The values in sources.json should not have an 'outPath' attribute" + else + spec // { outPath = fetch config.pkgs name spec; } + ) config.sources; + + # The "config" used by the fetchers + mkConfig = + { sourcesFile ? ./sources.json + , sources ? builtins.fromJSON (builtins.readFile sourcesFile) + , pkgs ? mkPkgs sources + }: rec { + # The sources, i.e. the attribute set of spec name to spec + inherit sources; + + # The "pkgs" (evaluated nixpkgs) to use for e.g. non-builtin fetchers + inherit pkgs; + }; +in +mkSources (mkConfig {}) // { __functor = _: settings: mkSources (mkConfig settings); } diff --git a/nix/static-overlay.nix b/nix/static-overlay.nix new file mode 100644 index 000000000..5add8718f --- /dev/null +++ b/nix/static-overlay.nix @@ -0,0 +1,24 @@ +native: self: super: +let dds = x: x.overrideAttrs (o: { dontDisableStatic = true; }); +in { + buildPackages = super.buildPackages // { inherit (native) rakudo; }; + ocaml = self.ocaml-ng.ocamlPackages_4_07.ocaml; + libev = dds super.libev; + libusb = self.libusb1; + systemd = self.eudev; + libusb1 = dds (super.libusb1.override { + enableSystemd = true; + }); + gdb = null; + hidapi = dds (super.hidapi.override { systemd = self.eudev; }); + glib = (super.glib.override { libselinux = null; }).overrideAttrs + (o: { mesonFlags = o.mesonFlags ++ [ "-Dselinux=disabled" ]; }); + eudev = dds (super.eudev.overrideAttrs + (o: { nativeBuildInputs = o.nativeBuildInputs ++ [ super.gperf ]; })); + gmp = dds (super.gmp); + ocamlPackages = super.ocamlPackages.overrideScope' (self: super: { + ligo-out = super.ligo-out.overrideAttrs (_: { + patches = [ ./static.patch ]; + }); + }); +} diff --git a/nix/static.patch b/nix/static.patch new file mode 100644 index 000000000..f4ce39a39 --- /dev/null +++ b/nix/static.patch @@ -0,0 +1,12 @@ +diff --git a/src/bin/dune b/src/bin/dune +index 162963b4b..29dfa5191 100644 +--- a/src/bin/dune ++++ b/src/bin/dune +@@ -34,5 +34,6 @@ + (preprocess + (pps ppx_let ppx_blob bisect_ppx --conditional) + ) +- (flags (:standard -open Simple_utils)) ++ (flags (:standard -open Simple_utils) ++ -ccopt -static -cclib "-lgmp") + ) diff --git a/scripts/distribution/generic/env_variables.sh b/scripts/distribution/generic/env_variables.sh index 7279e4cbe..536ba0ad9 100755 --- a/scripts/distribution/generic/env_variables.sh +++ b/scripts/distribution/generic/env_variables.sh @@ -9,4 +9,6 @@ export LIGO_REGISTRY_IMAGE_BASE_NAME="ligolang/ligo" # ligo_incrementing-id_commit-hash export CI_JOB_ID="0" export CI_COMMIT_SHORT_SHA="$(git rev-parse --short HEAD)" +export CI_COMMIT_SHA="$(git rev-parse HEAD)" +export COMMIT_DATE="$(git show --no-patch --format=%ci)" export LIGO_DIST_DIR="./dist" diff --git a/scripts/distribution/generic/parameters.sh b/scripts/distribution/generic/parameters.sh index 2241b9fb0..16ff1f16b 100644 --- a/scripts/distribution/generic/parameters.sh +++ b/scripts/distribution/generic/parameters.sh @@ -15,6 +15,8 @@ target_os_version="$3" dist="$LIGO_DIST_DIR" version="$(echo $CI_JOB_ID)-$(echo $CI_COMMIT_SHORT_SHA)" ci_job_id="$CI_JOB_ID" +ci_commit_sha="$CI_COMMIT_SHA" +commit_date="$COMMIT_DATE" # Image names for building & packaging target="$target_os-$target_os_version" diff --git a/src/bin/cli.ml b/src/bin/cli.ml index 540b07f12..e7a629c32 100644 --- a/src/bin/cli.ml +++ b/src/bin/cli.ml @@ -2,12 +2,7 @@ open Cmdliner open Trace open Cli_helpers -let version = - Format.asprintf - "Rolling release\nHash: %s\nDate: %s\nCI job id: %s" - Version.hash - Version.commit_date - Version.job_id +let version = Version.version let main = let man = diff --git a/src/bin/dune b/src/bin/dune index 162963b4b..5d52779fc 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -18,7 +18,7 @@ (action (with-stdout-to version.ml (run "sh" "-c" - "printf 'let hash = \"%s\"\nlet commit_date = \"%s\"\nlet job_id = \"%s\"\n' \"$(git rev-parse HEAD)\" \"$(git show --no-patch --format=%ci)\" \"${CI_JOB_ID}\"")))) + "printf 'let version = \"Rolling Release\nCommit SHA1: %s\nCommit Date: %s\"' \"${CI_COMMIT_SHA}\" \"${COMMIT_DATE}\"")))) (executable (name runligo) diff --git a/src/bin/expect_tests/contract_tests.ml b/src/bin/expect_tests/contract_tests.ml index 69f2c4a7d..3e9c0199a 100644 --- a/src/bin/expect_tests/contract_tests.ml +++ b/src/bin/expect_tests/contract_tests.ml @@ -1425,7 +1425,7 @@ let%expect_test _ = let%expect_test _ = run_ligo_bad [ "compile-contract" ; bad_contract "redundant_constructors.mligo" ; "main" ] ; [%expect {| - ligo: redundant constructor: {"constructor":"Add","environment":"- E[]\tT[union_a -> sum[Add -> int , Remove -> int]] ]"} + ligo: redundant constructor: {"constructor":"Add","environment":"- E[]\tT[union_a -> sum[Add -> int , Remove -> int]]\n- E[]\tT[bool -> sum[false -> unit , true -> unit]]]"} If you're not sure how to fix this error, you can @@ -1465,7 +1465,7 @@ ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, char run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_no_inline.mligo" ; "main" ] ; [%expect {| - ligo: in file "create_contract_no_inline.mligo", line 3, characters 40-46. unbound type variable: {"variable":"return","location":"in file \"create_contract_no_inline.mligo\", line 3, characters 40-46","in":"- E[foo -> int]\tT[] ]","did_you_mean":"no suggestion"} + ligo: in file "create_contract_no_inline.mligo", line 3, characters 40-46. unbound type variable: {"variable":"return","location":"in file \"create_contract_no_inline.mligo\", line 3, characters 40-46","in":"- E[foo -> int]\tT[] - E[]\tT[bool -> sum[false -> unit , true -> unit]]]","did_you_mean":"no suggestion"} If you're not sure how to fix this error, you can diff --git a/src/bin/expect_tests/typer_error_tests.ml b/src/bin/expect_tests/typer_error_tests.ml index 3bb9f2651..14162cd5a 100644 --- a/src/bin/expect_tests/typer_error_tests.ml +++ b/src/bin/expect_tests/typer_error_tests.ml @@ -93,7 +93,7 @@ let%expect_test _ = run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_3.mligo" ; "main" ] ; [%expect {| - ligo: in file "error_typer_3.mligo", line 3, characters 34-53. tuples have different sizes: Expected these two types to be the same, but they're different (both are tuples, but with a different number of arguments) {"a":"( int * string * bool )","b":"( int * string )"} + ligo: in file "error_typer_3.mligo", line 3, characters 34-53. tuples have different sizes: Expected these two types to be the same, but they're different (both are tuples, but with a different number of arguments) {"a":"( int * string * sum[false -> unit , true -> unit] )","b":"( int * string )"} If you're not sure how to fix this error, you can @@ -106,7 +106,7 @@ let%expect_test _ = run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_4.mligo" ; "main" ] ; [%expect {| - ligo: in file "error_typer_4.mligo", line 4, characters 17-56. different keys in records: {"key_a":"c","key_b":"b","a":"record[a -> int , c -> bool , d -> string]","b":"record[a -> int , b -> string , c -> bool]"} + ligo: in file "error_typer_4.mligo", line 4, characters 17-56. different keys in records: {"key_a":"c","key_b":"b","a":"record[a -> int , c -> sum[false -> unit , true -> unit] , d -> string]","b":"record[a -> int , b -> string , c -> sum[false -> unit , true -> unit]]"} If you're not sure how to fix this error, you can @@ -119,7 +119,7 @@ let%expect_test _ = run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_5.mligo" ; "main" ] ; [%expect {| - ligo: in file "error_typer_5.mligo", line 1, characters 10-17. unbound type variable: {"variable":"boolean","location":"in file \"error_typer_5.mligo\", line 1, characters 10-17","in":"- E[]\tT[] ]","did_you_mean":"bool"} + ligo: in file "error_typer_5.mligo", line 1, characters 10-17. unbound type variable: {"variable":"boolean","location":"in file \"error_typer_5.mligo\", line 1, characters 10-17","in":"- E[]\tT[] - E[]\tT[bool -> sum[false -> unit , true -> unit]]]","did_you_mean":"bool"} If you're not sure how to fix this error, you can @@ -132,7 +132,7 @@ let%expect_test _ = run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_6.mligo" ; "main" ] ; [%expect {| - ligo: in file "error_typer_6.mligo", line 1, characters 30-64. different type constructors: Expected these two constant type constructors to be the same, but they're different {"a":"string","b":"bool"} + ligo: in file "error_typer_6.mligo", line 1, characters 30-64. different kinds: {"a":"string","b":"sum[false -> unit , true -> unit]"} If you're not sure how to fix this error, you can @@ -145,7 +145,7 @@ let%expect_test _ = run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_7.mligo" ; "main" ] ; [%expect {| - ligo: in file "error_typer_7.mligo", line 4, characters 18-48. records have different sizes: Expected these two types to be the same, but they're different (both are records, but with a different number of arguments) {"a":"record[a -> int , b -> string]","b":"record[a -> int , b -> string , c -> bool]"} + ligo: in file "error_typer_7.mligo", line 4, characters 18-48. records have different sizes: Expected these two types to be the same, but they're different (both are records, but with a different number of arguments) {"a":"record[a -> int , b -> string]","b":"record[a -> int , b -> string , c -> sum[false -> unit , true -> unit]]"} If you're not sure how to fix this error, you can diff --git a/src/environment/bool.ml b/src/environment/bool.ml new file mode 100644 index 000000000..d89bd7013 --- /dev/null +++ b/src/environment/bool.ml @@ -0,0 +1,4 @@ +open Ast_typed +open Stage_common.Constant + +let environment = env_sum_type ~type_name:t_bool @@ [(Constructor "true",{ctor_type=t_unit ();michelson_annotation=None});(Constructor "false",{ctor_type=t_unit ();michelson_annotation=None})] diff --git a/src/environment/dune b/src/environment/dune new file mode 100644 index 000000000..8cbb1e004 --- /dev/null +++ b/src/environment/dune @@ -0,0 +1,14 @@ +(library + (name environment) + (public_name ligo.environment) + (libraries + simple-utils + tezos-utils + ast_typed + stage_common + ) + (preprocess + (pps ppx_let bisect_ppx --conditional) + ) + (flags (:standard -open Simple_utils)) +) diff --git a/src/environment/environment.ml b/src/environment/environment.ml new file mode 100644 index 000000000..523531836 --- /dev/null +++ b/src/environment/environment.ml @@ -0,0 +1,11 @@ +open Ast_typed + +let merge e1 e2 = + let e1 = List.Ne.to_list e1 in + let e2 = List.Ne.to_list e2 in + List.Ne.of_list @@ e1 @ e2 + + +let default = Environment.full_empty + +let default = merge default Bool.environment diff --git a/src/main/compile/of_core.ml b/src/main/compile/of_core.ml index e6f0dfbba..c7992399e 100644 --- a/src/main/compile/of_core.ml +++ b/src/main/compile/of_core.ml @@ -4,7 +4,7 @@ type form = | Contract of string | Env -let compile (cform: form) (program : Ast_core.program) : (Ast_typed.program * Typer.Solver.state) result = +let compile (cform: form) (program : Ast_core.program) : (Ast_typed.program * Ast_typed.typer_state) result = let%bind (prog_typed , state) = Typer.type_program program in let () = Typer.Solver.discard_state state in let%bind applied = Self_ast_typed.all_program prog_typed in @@ -13,8 +13,8 @@ let compile (cform: form) (program : Ast_core.program) : (Ast_typed.program * Ty | Env -> ok applied in ok @@ (applied', state) -let compile_expression ?(env = Ast_typed.Environment.full_empty) ~(state : Typer.Solver.state) (e : Ast_core.expression) - : (Ast_typed.expression * Typer.Solver.state) result = +let compile_expression ?(env = Ast_typed.Environment.full_empty) ~(state : Ast_typed.typer_state) (e : Ast_core.expression) + : (Ast_typed.expression * Ast_typed.typer_state) result = let%bind (ae_typed,state) = Typer.type_expression_subst env state e in let () = Typer.Solver.discard_state state in let%bind ae_typed' = Self_ast_typed.all_expression ae_typed in diff --git a/src/passes/1-parser/cameligo/.gitignore b/src/passes/1-parser/cameligo/.gitignore index cca52dc59..29e7b3c41 100644 --- a/src/passes/1-parser/cameligo/.gitignore +++ b/src/passes/1-parser/cameligo/.gitignore @@ -10,4 +10,7 @@ _build/* /Parser.ml /Lexer.ml /LexToken.ml -/Tests \ No newline at end of file +/Tests +error.messages +error.messages.new +ParErr.ml \ No newline at end of file diff --git a/src/passes/1-parser/cameligo/dune b/src/passes/1-parser/cameligo/dune index 85a06d174..02b8f3663 100644 --- a/src/passes/1-parser/cameligo/dune +++ b/src/passes/1-parser/cameligo/dune @@ -95,6 +95,7 @@ (rule (targets error.messages) + (mode (promote (until-clean) (only *))) (deps Parser.mly ParToken.mly error.messages.checked-in LexToken.mli) (action (with-stdout-to %{targets} @@ -114,6 +115,7 @@ (rule (target error.messages.new) + (mode (promote (until-clean) (only *))) (action (with-stdout-to %{target} (run @@ -154,6 +156,7 @@ (rule (targets ParErr.ml) + (mode (promote (until-clean) (only *))) (deps Parser.mly ParToken.mly error.messages.checked-in LexToken.mli) (action (with-stdout-to %{targets} diff --git a/src/passes/1-parser/pascaligo/.gitignore b/src/passes/1-parser/pascaligo/.gitignore index cca52dc59..29e7b3c41 100644 --- a/src/passes/1-parser/pascaligo/.gitignore +++ b/src/passes/1-parser/pascaligo/.gitignore @@ -10,4 +10,7 @@ _build/* /Parser.ml /Lexer.ml /LexToken.ml -/Tests \ No newline at end of file +/Tests +error.messages +error.messages.new +ParErr.ml \ No newline at end of file diff --git a/src/passes/1-parser/pascaligo/dune b/src/passes/1-parser/pascaligo/dune index a63252fe7..ca4865ae9 100644 --- a/src/passes/1-parser/pascaligo/dune +++ b/src/passes/1-parser/pascaligo/dune @@ -96,6 +96,7 @@ (rule (targets error.messages) + (mode (promote (until-clean) (only *))) (deps Parser.mly ParToken.mly error.messages.checked-in LexToken.mli) (action (with-stdout-to %{targets} @@ -115,6 +116,7 @@ (rule (target error.messages.new) + (mode (promote (until-clean) (only *))) (action (with-stdout-to %{target} (run @@ -155,6 +157,7 @@ (rule (targets ParErr.ml) + (mode (promote (until-clean) (only *))) (deps Parser.mly ParToken.mly error.messages.checked-in LexToken.mli) (action (with-stdout-to %{targets} diff --git a/src/passes/1-parser/reasonligo/.gitignore b/src/passes/1-parser/reasonligo/.gitignore index cca52dc59..29e7b3c41 100644 --- a/src/passes/1-parser/reasonligo/.gitignore +++ b/src/passes/1-parser/reasonligo/.gitignore @@ -10,4 +10,7 @@ _build/* /Parser.ml /Lexer.ml /LexToken.ml -/Tests \ No newline at end of file +/Tests +error.messages +error.messages.new +ParErr.ml \ No newline at end of file diff --git a/src/passes/1-parser/reasonligo/dune b/src/passes/1-parser/reasonligo/dune index f89578a4c..b8f57b665 100644 --- a/src/passes/1-parser/reasonligo/dune +++ b/src/passes/1-parser/reasonligo/dune @@ -96,6 +96,7 @@ (rule (targets error.messages) + (mode (promote (until-clean) (only *))) (deps Parser.mly ParToken.mly error.messages.checked-in LexToken.mli) (action (with-stdout-to %{targets} @@ -115,6 +116,7 @@ (rule (target error.messages.new) + (mode (promote (until-clean) (only *))) (action (with-stdout-to %{target} (run @@ -155,6 +157,7 @@ (rule (targets ParErr.ml) + (mode (promote (until-clean) (only *))) (deps Parser.mly ParToken.mly error.messages.checked-in LexToken.mli) (action (with-stdout-to %{targets} diff --git a/src/passes/10-interpreter/interpreter.ml b/src/passes/10-interpreter/interpreter.ml index 5b15b414c..85c15c6fb 100644 --- a/src/passes/10-interpreter/interpreter.ml +++ b/src/passes/10-interpreter/interpreter.ml @@ -255,7 +255,6 @@ C_STEPS_TO_QUOTA (*interpreter*) and eval_literal : Ast_typed.literal -> value result = function | Literal_unit -> ok @@ V_Ct (C_unit) - | Literal_bool b -> ok @@ V_Ct (C_bool b) | Literal_int i -> ok @@ V_Ct (C_int i) | Literal_nat n -> ok @@ V_Ct (C_nat n) | Literal_timestamp i -> ok @@ V_Ct (C_timestamp i) @@ -329,6 +328,8 @@ and eval : Ast_typed.expression -> env -> value result arguments in apply_operator cons_name operands' ) + | E_constructor { constructor = Constructor c ; element } when (String.equal c "true" || String.equal c "false") + && element.expression_content = Ast_typed.e_unit () -> ok @@ V_Ct (C_bool (bool_of_string c)) | E_constructor { constructor = Constructor c ; element } -> let%bind v' = eval element env in ok @@ V_Construct (c,v') @@ -341,6 +342,10 @@ and eval : Ast_typed.expression -> env -> value result let {hd;tl;body;tv=_} = cases.match_cons in let env' = Env.extend (Env.extend env (hd,head)) (tl, V_List tail) in eval body env' + | Match_variant {cases=[{constructor=Constructor t;body=match_true};{constructor=Constructor f; body=match_false}];_}, V_Ct (C_bool b) + when String.equal t "true" && String.equal f "false" -> + if b then eval match_true env + else eval match_false env | Match_variant {cases ; tv=_} , V_Construct (matched_c , proj) -> let {constructor=_ ; pattern ; body} = List.find @@ -349,10 +354,6 @@ and eval : Ast_typed.expression -> env -> value result cases in let env' = Env.extend env (pattern, proj) in eval body env' - | Match_bool cases , V_Ct (C_bool true) -> - eval cases.match_true env - | Match_bool cases , V_Ct (C_bool false) -> - eval cases.match_false env | Match_option cases, V_Construct ("Some" , proj) -> let {opt;body;tv=_} = cases.match_some in let env' = Env.extend env (opt,proj) in diff --git a/src/passes/10-transpiler/transpiler.ml b/src/passes/10-transpiler/transpiler.ml index 37c005ef6..a7ca1f555 100644 --- a/src/passes/10-transpiler/transpiler.ml +++ b/src/passes/10-transpiler/transpiler.ml @@ -76,7 +76,7 @@ them. please report this to the developers." in error ~data title content let wrong_mini_c_value expected_type actual = - let title () = "illed typed intermediary value" in + let title () = "transpiler: illed typed intermediary value" in let content () = "type of intermediary value doesn't match what was expected" in let data = [ ("expected_type" , fun () -> expected_type) ; @@ -231,22 +231,23 @@ let transpile_constant' : AST.constant' -> constant' = function let rec transpile_type (t:AST.type_expression) : type_value result = match t.type_content with + | T_variable (name) when Var.equal name Stage_common.Constant.t_bool -> ok (T_base TB_bool) + | t when (compare t (t_bool ()).type_content) = 0-> ok (T_base TB_bool) | T_variable (name) -> fail @@ no_type_variable @@ name - | T_constant (TC_bool) -> ok (T_base TC_bool) - | T_constant (TC_int) -> ok (T_base TC_int) - | T_constant (TC_nat) -> ok (T_base TC_nat) - | T_constant (TC_mutez) -> ok (T_base TC_mutez) - | T_constant (TC_string) -> ok (T_base TC_string) - | T_constant (TC_bytes) -> ok (T_base TC_bytes) - | T_constant (TC_address) -> ok (T_base TC_address) - | T_constant (TC_timestamp) -> ok (T_base TC_timestamp) - | T_constant (TC_unit) -> ok (T_base TC_unit) - | T_constant (TC_operation) -> ok (T_base TC_operation) - | T_constant (TC_signature) -> ok (T_base TC_signature) - | T_constant (TC_key) -> ok (T_base TC_key) - | T_constant (TC_key_hash) -> ok (T_base TC_key_hash) - | T_constant (TC_chain_id) -> ok (T_base TC_chain_id) - | T_constant (TC_void) -> ok (T_base TC_void) + | T_constant (TC_int) -> ok (T_base TB_int) + | T_constant (TC_nat) -> ok (T_base TB_nat) + | T_constant (TC_mutez) -> ok (T_base TB_mutez) + | T_constant (TC_string) -> ok (T_base TB_string) + | T_constant (TC_bytes) -> ok (T_base TB_bytes) + | T_constant (TC_address) -> ok (T_base TB_address) + | T_constant (TC_timestamp) -> ok (T_base TB_timestamp) + | T_constant (TC_unit) -> ok (T_base TB_unit) + | T_constant (TC_operation) -> ok (T_base TB_operation) + | T_constant (TC_signature) -> ok (T_base TB_signature) + | T_constant (TC_key) -> ok (T_base TB_key) + | T_constant (TC_key_hash) -> ok (T_base TB_key_hash) + | T_constant (TC_chain_id) -> ok (T_base TB_chain_id) + | T_constant (TC_void) -> ok (T_base TB_void) | T_operator (TC_contract x) -> let%bind x' = transpile_type x in ok (T_contract x') @@ -267,11 +268,6 @@ let rec transpile_type (t:AST.type_expression) : type_value result = | T_operator (TC_option o) -> let%bind o' = transpile_type o in ok (T_option o') - | T_operator (TC_arrow {type1=param ; type2=result}) -> ( - let%bind param' = transpile_type param in - let%bind result' = transpile_type result in - ok (T_function (param', result')) - ) | T_sum m when Ast_typed.Helpers.is_michelson_or m -> let node = Append_tree.of_list @@ kv_list_of_cmap m in let aux a b : type_value annotated result = @@ -362,7 +358,6 @@ let record_access_to_lr : type_value -> type_value AST.label_map -> AST.label -> ok lst let rec transpile_literal : AST.literal -> value = fun l -> match l with - | Literal_bool b -> D_bool b | Literal_int n -> D_int n | Literal_nat n -> D_nat n | Literal_timestamp n -> D_timestamp n @@ -411,6 +406,8 @@ and transpile_annotated_expression (ae:AST.expression) : expression result = let%bind a = transpile_annotated_expression lamb in let%bind b = transpile_annotated_expression args in return @@ E_application (a, b) + | E_constructor {constructor=Constructor name;element} when (String.equal name "true"|| String.equal name "false") && element.expression_content = AST.e_unit () -> + return @@ E_literal (D_bool (bool_of_string name)) | E_constructor {constructor;element} -> ( let%bind param' = transpile_annotated_expression element in let (param'_expr , param'_tv) = Combinators.Expression.(get_content param' , get_type param') in @@ -563,9 +560,6 @@ and transpile_annotated_expression (ae:AST.expression) : expression result = | E_matching {matchee=expr; cases=m} -> ( let%bind expr' = transpile_annotated_expression expr in match m with - | Match_bool {match_true ; match_false} -> - let%bind (t , f) = bind_map_pair (transpile_annotated_expression) (match_true, match_false) in - return @@ E_if_bool (expr', t, f) | Match_option { match_none; match_some = {opt; body; tv} } -> let%bind n = transpile_annotated_expression match_none in let%bind (tv' , s') = @@ -586,6 +580,10 @@ and transpile_annotated_expression (ae:AST.expression) : expression result = in return @@ E_if_cons (expr' , nil , cons) ) + | Match_variant {cases=[{constructor=Constructor t;body=match_true};{constructor=Constructor f;body=match_false}];_} + when String.equal t "true" && String.equal f "false" -> + let%bind (t , f) = bind_map_pair (transpile_annotated_expression) (match_true, match_false) in + return @@ E_if_bool (expr', t, f) | Match_variant {cases ; tv} -> ( let%bind tree = trace_strong (corner_case ~loc:__LOC__ "getting lr tree") @@ @@ -686,9 +684,6 @@ and transpile_recursive {fun_name; fun_type; lambda} = let return ret = ok @@ Expression.make ret @@ ty in let%bind expr = transpile_annotated_expression m.matchee in match m.cases with - Match_bool {match_true; match_false} -> - let%bind (t , f) = bind_map_pair (replace_callback fun_name loop_type shadowed) (match_true, match_false) in - return @@ E_if_bool (expr, t, f) | Match_option { match_none; match_some = {opt; body; tv} } -> let%bind n = replace_callback fun_name loop_type shadowed match_none in let%bind (tv' , s') = @@ -709,6 +704,10 @@ and transpile_recursive {fun_name; fun_type; lambda} = in return @@ E_if_cons (expr , nil , cons) ) + | Match_variant {cases=[{constructor=Constructor t;body=match_true};{constructor=Constructor f;body=match_false}];_} + when String.equal t "true" && String.equal f "false" -> + let%bind (t , f) = bind_map_pair (replace_callback fun_name loop_type shadowed) (match_true, match_false) in + return @@ E_if_bool (expr, t, f) | Match_variant {cases;tv} -> ( let%bind tree = trace_strong (corner_case ~loc:__LOC__ "getting lr tree") @@ diff --git a/src/passes/10-transpiler/untranspiler.ml b/src/passes/10-transpiler/untranspiler.ml index bf59c6a81..edec0b53f 100644 --- a/src/passes/10-transpiler/untranspiler.ml +++ b/src/passes/10-transpiler/untranspiler.ml @@ -19,7 +19,7 @@ them. please report this to the developers." in error ~data title content let wrong_mini_c_value expected_type actual = - let title () = "illed typed intermediary value" in + let title () = "untranspiler: illed typed intermediary value" in let content () = "type of intermediary value doesn't match what was expected" in let data = [ ("expected_type" , fun () -> expected_type) ; @@ -44,6 +44,18 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul let open! AST in let return e = ok (make_a_e_empty e t) in match t.type_content with + | T_variable (name) when Var.equal name Stage_common.Constant.t_bool -> ( + let%bind b = + trace_strong (wrong_mini_c_value "bool" v) @@ + get_bool v in + return (e_bool b Environment.full_empty) + ) + | t when (compare t (t_bool ()).type_content) = 0-> ( + let%bind b = + trace_strong (wrong_mini_c_value "bool" v) @@ + get_bool v in + return (e_bool b Environment.full_empty) + ) | T_constant type_constant -> ( match type_constant with | TC_unit -> ( @@ -52,12 +64,6 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul get_unit v in return (E_literal Literal_unit) ) - | TC_bool -> ( - let%bind b = - trace_strong (wrong_mini_c_value "bool" v) @@ - get_bool v in - return (E_literal (Literal_bool b)) - ) | TC_int -> ( let%bind n = trace_strong (wrong_mini_c_value "int" v) @@ @@ -197,12 +203,6 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul let%bind init = return @@ E_constant {cons_name=C_LIST_EMPTY;arguments=[]} in bind_fold_right_list aux init lst' ) - | TC_arrow _ -> ( - let%bind n = - trace_strong (wrong_mini_c_value "lambda as string" v) @@ - get_string v in - return (E_literal (Literal_string n)) - ) | TC_set ty -> ( let%bind lst = trace_strong (wrong_mini_c_value "set" v) @@ diff --git a/src/passes/11-self_mini_c/subst.ml b/src/passes/11-self_mini_c/subst.ml index def581f96..f03de4865 100644 --- a/src/passes/11-self_mini_c/subst.ml +++ b/src/passes/11-self_mini_c/subst.ml @@ -117,7 +117,7 @@ let rec subst_expression : body:expression -> x:var_name -> expr:expression -> e (* hack to avoid reimplementing subst_binder for 2-ary binder in E_if_cons: intuitively, we substitute in \hd tl. expr' as if it were \hd. \tl. expr *) let subst_binder2 y z expr' = - let dummy = T_base TC_unit in + let dummy = T_base TB_unit in let hack = { content = E_closure { binder = z ; body = expr' } ; type_value = dummy } in match subst_binder y hack with @@ -199,7 +199,7 @@ let rec subst_expression : body:expression -> x:var_name -> expr:expression -> e ) let%expect_test _ = - let dummy_type = T_base TC_unit in + let dummy_type = T_base TB_unit in let wrap e = { content = e ; type_value = dummy_type } in let show_subst ~body ~x ~expr = diff --git a/src/passes/12-compiler/compiler_type.ml b/src/passes/12-compiler/compiler_type.ml index c4874ef38..559fcab5b 100644 --- a/src/passes/12-compiler/compiler_type.ml +++ b/src/passes/12-compiler/compiler_type.ml @@ -59,24 +59,24 @@ module Ty = struct let not_comparable name () = error (thunk "not a comparable type") (fun () -> name) () let not_compilable_type name () = error (thunk "not a compilable type") (fun () -> name) () - let comparable_type_base : type_constant -> ex_comparable_ty result = fun tb -> + let comparable_type_base : type_base -> ex_comparable_ty result = fun tb -> let return x = ok @@ Ex_comparable_ty x in match tb with - | TC_unit -> fail (not_comparable "unit") - | TC_void -> fail (not_comparable "void") - | TC_bool -> return bool_k - | TC_nat -> return nat_k - | TC_mutez -> return tez_k - | TC_int -> return int_k - | TC_string -> return string_k - | TC_address -> return address_k - | TC_timestamp -> return timestamp_k - | TC_bytes -> return bytes_k - | TC_operation -> fail (not_comparable "operation") - | TC_signature -> fail (not_comparable "signature") - | TC_key -> fail (not_comparable "key") - | TC_key_hash -> return key_hash_k - | TC_chain_id -> fail (not_comparable "chain_id") + | TB_unit -> fail (not_comparable "unit") + | TB_void -> fail (not_comparable "void") + | TB_bool -> return bool_k + | TB_nat -> return nat_k + | TB_mutez -> return tez_k + | TB_int -> return int_k + | TB_string -> return string_k + | TB_address -> return address_k + | TB_timestamp -> return timestamp_k + | TB_bytes -> return bytes_k + | TB_operation -> fail (not_comparable "operation") + | TB_signature -> fail (not_comparable "signature") + | TB_key -> fail (not_comparable "key") + | TB_key_hash -> return key_hash_k + | TB_chain_id -> fail (not_comparable "chain_id") let comparable_leaf : type a. (a, _) comparable_struct -> (a , leaf) comparable_struct result = fun a -> @@ -109,24 +109,24 @@ module Ty = struct | T_option _ -> fail (not_comparable "option") | T_contract _ -> fail (not_comparable "contract") - let base_type : type_constant -> ex_ty result = fun b -> + let base_type : type_base -> ex_ty result = fun b -> let return x = ok @@ Ex_ty x in match b with - | TC_unit -> return unit - | TC_void -> fail (not_compilable_type "void") - | TC_bool -> return bool - | TC_int -> return int - | TC_nat -> return nat - | TC_mutez -> return tez - | TC_string -> return string - | TC_address -> return address - | TC_timestamp -> return timestamp - | TC_bytes -> return bytes - | TC_operation -> return operation - | TC_signature -> return signature - | TC_key -> return key - | TC_key_hash -> return key_hash - | TC_chain_id -> return chain_id + | TB_unit -> return unit + | TB_void -> fail (not_compilable_type "void") + | TB_bool -> return bool + | TB_int -> return int + | TB_nat -> return nat + | TB_mutez -> return tez + | TB_string -> return string + | TB_address -> return address + | TB_timestamp -> return timestamp + | TB_bytes -> return bytes + | TB_operation -> return operation + | TB_signature -> return signature + | TB_key -> return key + | TB_key_hash -> return key_hash + | TB_chain_id -> return chain_id let rec type_ : type_value -> ex_ty result = function @@ -195,23 +195,23 @@ module Ty = struct end -let base_type : type_constant -> O.michelson result = +let base_type : type_base -> O.michelson result = function - | TC_unit -> ok @@ O.prim T_unit - | TC_void -> fail (Ty.not_compilable_type "void") - | TC_bool -> ok @@ O.prim T_bool - | TC_int -> ok @@ O.prim T_int - | TC_nat -> ok @@ O.prim T_nat - | TC_mutez -> ok @@ O.prim T_mutez - | TC_string -> ok @@ O.prim T_string - | TC_address -> ok @@ O.prim T_address - | TC_timestamp -> ok @@ O.prim T_timestamp - | TC_bytes -> ok @@ O.prim T_bytes - | TC_operation -> ok @@ O.prim T_operation - | TC_signature -> ok @@ O.prim T_signature - | TC_key -> ok @@ O.prim T_key - | TC_key_hash -> ok @@ O.prim T_key_hash - | TC_chain_id -> ok @@ O.prim T_chain_id + | TB_unit -> ok @@ O.prim T_unit + | TB_void -> fail (Ty.not_compilable_type "void") + | TB_bool -> ok @@ O.prim T_bool + | TB_int -> ok @@ O.prim T_int + | TB_nat -> ok @@ O.prim T_nat + | TB_mutez -> ok @@ O.prim T_mutez + | TB_string -> ok @@ O.prim T_string + | TB_address -> ok @@ O.prim T_address + | TB_timestamp -> ok @@ O.prim T_timestamp + | TB_bytes -> ok @@ O.prim T_bytes + | TB_operation -> ok @@ O.prim T_operation + | TB_signature -> ok @@ O.prim T_signature + | TB_key -> ok @@ O.prim T_key + | TB_key_hash -> ok @@ O.prim T_key_hash + | TB_chain_id -> ok @@ O.prim T_chain_id let rec type_ : type_value -> O.michelson result = function diff --git a/src/passes/2-concrete_to_imperative/cameligo.ml b/src/passes/2-concrete_to_imperative/cameligo.ml index 2134526bc..33d8cca21 100644 --- a/src/passes/2-concrete_to_imperative/cameligo.ml +++ b/src/passes/2-concrete_to_imperative/cameligo.ml @@ -768,11 +768,11 @@ and compile_logic_expression ?te_annot (t:Raw.logic_expr) : expr result = match t with | BoolExpr (False reg) -> ( let loc = Location.lift reg in - return @@ e_literal ~loc (Literal_bool false) + return @@ e_bool ~loc false ) | BoolExpr (True reg) -> ( let loc = Location.lift reg in - return @@ e_literal ~loc (Literal_bool true) + return @@ e_bool ~loc true ) | BoolExpr (Or b) -> compile_binop "OR" b @@ -1026,7 +1026,7 @@ and compile_cases : type a . (Raw.pattern * a) list -> (a, unit) matching_conten match patterns with | [(PFalse _, f) ; (PTrue _, t)] | [(PTrue _, t) ; (PFalse _, f)] -> - ok @@ Match_bool {match_true = t ; match_false = f} + ok @@ Match_variant ([((Constructor "true", Var.of_name "_"), t); ((Constructor "false", Var.of_name "_"), f)], ()) | [(PList (PCons c), cons); (PList (PListComp sugar_nil), nil)] | [(PList (PListComp sugar_nil), nil); (PList (PCons c), cons)] -> let%bind () = diff --git a/src/passes/2-concrete_to_imperative/pascaligo.ml b/src/passes/2-concrete_to_imperative/pascaligo.ml index 759295bc7..4ebef1559 100644 --- a/src/passes/2-concrete_to_imperative/pascaligo.ml +++ b/src/passes/2-concrete_to_imperative/pascaligo.ml @@ -487,11 +487,11 @@ and compile_logic_expression (t:Raw.logic_expr) : expression result = match t with | BoolExpr (False reg) -> ( let loc = Location.lift reg in - return @@ e_literal ~loc (Literal_bool false) + return @@ e_bool ~loc false ) | BoolExpr (True reg) -> ( let loc = Location.lift reg in - return @@ e_literal ~loc (Literal_bool true) + return @@ e_bool ~loc true ) | BoolExpr (Or b) -> compile_binop "OR" b @@ -1056,7 +1056,7 @@ and compile_cases : (Raw.pattern * expression) list -> matching_expr result = fu match patterns with | [(PConstr PFalse _ , f) ; (PConstr PTrue _ , t)] | [(PConstr PTrue _ , t) ; (PConstr PFalse _ , f)] -> - ok @@ Match_bool {match_true = t ; match_false = f} + ok @@ Match_variant ([((Constructor "true", Var.of_name "_"), t); ((Constructor "false", Var.of_name "_"), f)], ()) | [(PConstr PSomeApp v , some) ; (PConstr PNone _ , none)] | [(PConstr PNone _ , none) ; (PConstr PSomeApp v , some)] -> ( let (_, v) = v.value in diff --git a/src/passes/3-self_ast_imperative/helpers.ml b/src/passes/3-self_ast_imperative/helpers.ml index 677789b6f..159aa7bfb 100644 --- a/src/passes/3-self_ast_imperative/helpers.ml +++ b/src/passes/3-self_ast_imperative/helpers.ml @@ -104,11 +104,6 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini and fold_cases : 'a folder -> 'a -> matching_expr -> 'a result = fun f init m -> match m with - | Match_bool { match_true ; match_false } -> ( - let%bind res = fold_expression f init match_true in - let%bind res = fold_expression f res match_false in - ok res - ) | Match_list { match_nil ; match_cons = (_ , _ , cons, _) } -> ( let%bind res = fold_expression f init match_nil in let%bind res = fold_expression f res cons in @@ -272,11 +267,6 @@ and map_type_expression : ty_exp_mapper -> type_expression -> type_expression re and map_cases : exp_mapper -> matching_expr -> matching_expr result = fun f m -> match m with - | Match_bool { match_true ; match_false } -> ( - let%bind match_true = map_expression f match_true in - let%bind match_false = map_expression f match_false in - ok @@ Match_bool { match_true ; match_false } - ) | Match_list { match_nil ; match_cons = (hd , tl , cons, _) } -> ( let%bind match_nil = map_expression f match_nil in let%bind cons = map_expression f cons in @@ -433,11 +423,6 @@ let rec fold_map_expression : 'a fold_mapper -> 'a -> expression -> ('a * expres and fold_map_cases : 'a fold_mapper -> 'a -> matching_expr -> ('a * matching_expr) result = fun f init m -> match m with - | Match_bool { match_true ; match_false } -> ( - let%bind (init, match_true) = fold_map_expression f init match_true in - let%bind (init, match_false) = fold_map_expression f init match_false in - ok @@ (init, Match_bool { match_true ; match_false }) - ) | Match_list { match_nil ; match_cons = (hd , tl , cons, _) } -> ( let%bind (init, match_nil) = fold_map_expression f init match_nil in let%bind (init, cons) = fold_map_expression f init cons in diff --git a/src/passes/4-imperative_to_sugar/imperative_to_sugar.ml b/src/passes/4-imperative_to_sugar/imperative_to_sugar.ml index 99433d272..bdaf7f495 100644 --- a/src/passes/4-imperative_to_sugar/imperative_to_sugar.ml +++ b/src/passes/4-imperative_to_sugar/imperative_to_sugar.ml @@ -200,9 +200,6 @@ and compile_type_operator : I.type_operator -> O.type_operator result = | TC_big_map (k,v) -> let%bind (k,v) = bind_map_pair compile_type_expression (k,v) in ok @@ O.TC_big_map (k,v) - | TC_arrow (i,o) -> - let%bind (i,o) = bind_map_pair compile_type_expression (i,o) in - ok @@ O.TC_arrow (i,o) | TC_michelson_or _ | TC_michelson_pair _ -> fail @@ Errors.corner_case __LOC__ let rec compile_expression : I.expression -> O.expression result = @@ -384,26 +381,6 @@ and compile_matching : I.matching -> (O.expression option -> O.expression) resul in let%bind matchee = compile_expression matchee in match cases with - | I.Match_bool {match_true;match_false} -> - let%bind match_true' = compile_expression match_true in - let%bind match_false' = compile_expression match_false in - let env = Var.fresh () in - let%bind ((_,free_vars_true), match_true) = repair_mutable_variable_in_matching match_true' [] env in - let%bind ((_,free_vars_false), match_false) = repair_mutable_variable_in_matching match_false' [] env in - let match_true = add_to_end match_true (O.e_variable env) in - let match_false = add_to_end match_false (O.e_variable env) in - - let free_vars = List.sort_uniq Var.compare @@ free_vars_true @ free_vars_false in - if (List.length free_vars != 0) then - let match_expr = O.e_matching matchee (O.Match_bool {match_true; match_false}) in - let return_expr = fun expr -> - O.e_let_in (env,None) false false (store_mutable_variable free_vars) @@ - O.e_let_in (env,None) false false match_expr @@ - expr - in - ok @@ restore_mutable_variable return_expr free_vars env - else - return @@ O.e_matching matchee @@ O.Match_bool {match_true=match_true';match_false=match_false'} | I.Match_option {match_none;match_some} -> let%bind match_none' = compile_expression match_none in let (n,expr,tv) = match_some in @@ -663,9 +640,6 @@ and uncompile_type_operator : O.type_operator -> I.type_operator result = | TC_big_map (k,v) -> let%bind (k,v) = bind_map_pair uncompile_type_expression (k,v) in ok @@ I.TC_big_map (k,v) - | TC_arrow (i,o) -> - let%bind (i,o) = bind_map_pair uncompile_type_expression (i,o) in - ok @@ I.TC_arrow (i,o) let rec uncompile_expression' : O.expression -> I.expression result = fun e -> @@ -771,10 +745,6 @@ and uncompile_lambda : O.lambda -> I.lambda result = and uncompile_matching : O.matching_expr -> I.matching_expr result = fun m -> match m with - | O.Match_bool {match_true;match_false} -> - let%bind match_true = uncompile_expression' match_true in - let%bind match_false = uncompile_expression' match_false in - ok @@ I.Match_bool {match_true;match_false} | O.Match_list {match_nil;match_cons} -> let%bind match_nil = uncompile_expression' match_nil in let (hd,tl,expr,tv) = match_cons in diff --git a/src/passes/5-self_ast_sugar/helpers.ml b/src/passes/5-self_ast_sugar/helpers.ml index 0d3b353b7..953a8910f 100644 --- a/src/passes/5-self_ast_sugar/helpers.ml +++ b/src/passes/5-self_ast_sugar/helpers.ml @@ -103,11 +103,6 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini and fold_cases : 'a folder -> 'a -> matching_expr -> 'a result = fun f init m -> match m with - | Match_bool { match_true ; match_false } -> ( - let%bind res = fold_expression f init match_true in - let%bind res = fold_expression f res match_false in - ok res - ) | Match_list { match_nil ; match_cons = (_ , _ , cons, _) } -> ( let%bind res = fold_expression f init match_nil in let%bind res = fold_expression f res cons in @@ -255,11 +250,6 @@ and map_type_expression : ty_exp_mapper -> type_expression -> type_expression re and map_cases : exp_mapper -> matching_expr -> matching_expr result = fun f m -> match m with - | Match_bool { match_true ; match_false } -> ( - let%bind match_true = map_expression f match_true in - let%bind match_false = map_expression f match_false in - ok @@ Match_bool { match_true ; match_false } - ) | Match_list { match_nil ; match_cons = (hd , tl , cons, _) } -> ( let%bind match_nil = map_expression f match_nil in let%bind cons = map_expression f cons in @@ -402,11 +392,6 @@ let rec fold_map_expression : 'a fold_mapper -> 'a -> expression -> ('a * expres and fold_map_cases : 'a fold_mapper -> 'a -> matching_expr -> ('a * matching_expr) result = fun f init m -> match m with - | Match_bool { match_true ; match_false } -> ( - let%bind (init, match_true) = fold_map_expression f init match_true in - let%bind (init, match_false) = fold_map_expression f init match_false in - ok @@ (init, Match_bool { match_true ; match_false }) - ) | Match_list { match_nil ; match_cons = (hd , tl , cons, _) } -> ( let%bind (init, match_nil) = fold_map_expression f init match_nil in let%bind (init, cons) = fold_map_expression f init cons in diff --git a/src/passes/6-sugar_to_core/sugar_to_core.ml b/src/passes/6-sugar_to_core/sugar_to_core.ml index ce1af8ae2..c10098f45 100644 --- a/src/passes/6-sugar_to_core/sugar_to_core.ml +++ b/src/passes/6-sugar_to_core/sugar_to_core.ml @@ -66,9 +66,6 @@ and idle_type_operator : I.type_operator -> O.type_operator result = | TC_big_map (k,v) -> let%bind (k,v) = bind_map_pair idle_type_expression (k,v) in ok @@ O.TC_big_map (k,v) - | TC_arrow (i,o) -> - let%bind (i,o) = bind_map_pair idle_type_expression (i,o) in - ok @@ O.TC_arrow (i,o) let rec compile_expression : I.expression -> O.expression result = fun e -> @@ -162,7 +159,7 @@ let rec compile_expression : I.expression -> O.expression result = let%bind matchee = compile_expression condition in let%bind match_true = compile_expression then_clause in let%bind match_false = compile_expression else_clause in - return @@ O.E_matching {matchee; cases=Match_bool{match_true;match_false}} + return @@ O.E_matching {matchee; cases=Match_variant ([((Constructor "true", Var.of_name "_"),match_true);((Constructor "false", Var.of_name "_"), match_false)],())} | I.E_sequence {expr1; expr2} -> let%bind expr1 = compile_expression expr1 in let%bind expr2 = compile_expression expr2 in @@ -194,10 +191,6 @@ and compile_lambda : I.lambda -> O.lambda result = and compile_matching : I.matching_expr -> O.matching_expr result = fun m -> match m with - | I.Match_bool {match_true;match_false} -> - let%bind match_true = compile_expression match_true in - let%bind match_false = compile_expression match_false in - ok @@ O.Match_bool {match_true;match_false} | I.Match_list {match_nil;match_cons} -> let%bind match_nil = compile_expression match_nil in let (hd,tl,expr,tv) = match_cons in @@ -295,9 +288,6 @@ and uncompile_type_operator : O.type_operator -> I.type_operator result = let%bind (k,v) = bind_map_pair uncompile_type_expression (k,v) in ok @@ I.TC_big_map (k,v) | TC_map_or_big_map _ -> failwith "TC_map_or_big_map shouldn't be uncompiled" - | TC_arrow (i,o) -> - let%bind (i,o) = bind_map_pair uncompile_type_expression (i,o) in - ok @@ I.TC_arrow (i,o) let rec uncompile_expression : O.expression -> I.expression result = fun e -> @@ -366,10 +356,6 @@ and uncompile_lambda : O.lambda -> I.lambda result = and uncompile_matching : O.matching_expr -> I.matching_expr result = fun m -> match m with - | O.Match_bool {match_true;match_false} -> - let%bind match_true = uncompile_expression match_true in - let%bind match_false = uncompile_expression match_false in - ok @@ I.Match_bool {match_true;match_false} | O.Match_list {match_nil;match_cons} -> let%bind match_nil = uncompile_expression match_nil in let (hd,tl,expr,tv) = match_cons in diff --git a/src/passes/7-self_ast_core/helpers.ml b/src/passes/7-self_ast_core/helpers.ml index e76e4f064..d4311211e 100644 --- a/src/passes/7-self_ast_core/helpers.ml +++ b/src/passes/7-self_ast_core/helpers.ml @@ -72,11 +72,6 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini and fold_cases : 'a folder -> 'a -> matching_expr -> 'a result = fun f init m -> match m with - | Match_bool { match_true ; match_false } -> ( - let%bind res = fold_expression f init match_true in - let%bind res = fold_expression f res match_false in - ok res - ) | Match_list { match_nil ; match_cons = (_ , _ , cons, _) } -> ( let%bind res = fold_expression f init match_nil in let%bind res = fold_expression f res cons in @@ -179,11 +174,6 @@ and map_type_expression : ty_exp_mapper -> type_expression -> type_expression re and map_cases : exp_mapper -> matching_expr -> matching_expr result = fun f m -> match m with - | Match_bool { match_true ; match_false } -> ( - let%bind match_true = map_expression f match_true in - let%bind match_false = map_expression f match_false in - ok @@ Match_bool { match_true ; match_false } - ) | Match_list { match_nil ; match_cons = (hd , tl , cons, _) } -> ( let%bind match_nil = map_expression f match_nil in let%bind cons = map_expression f cons in @@ -284,11 +274,6 @@ let rec fold_map_expression : 'a fold_mapper -> 'a -> expression -> ('a * expres and fold_map_cases : 'a fold_mapper -> 'a -> matching_expr -> ('a * matching_expr) result = fun f init m -> match m with - | Match_bool { match_true ; match_false } -> ( - let%bind (init, match_true) = fold_map_expression f init match_true in - let%bind (init, match_false) = fold_map_expression f init match_false in - ok @@ (init, Match_bool { match_true ; match_false }) - ) | Match_list { match_nil ; match_cons = (hd , tl , cons, _) } -> ( let%bind (init, match_nil) = fold_map_expression f init match_nil in let%bind (init, cons) = fold_map_expression f init cons in diff --git a/src/passes/8-typer-new/PP.ml b/src/passes/8-typer-new/PP.ml index abecd4ef7..db1512f19 100644 --- a/src/passes/8-typer-new/PP.ml +++ b/src/passes/8-typer-new/PP.ml @@ -1,36 +1,36 @@ -open Solver +open Ast_typed open Format +module UF = UnionFind.Poly2 let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf -> function |SC_Constructor { tv; c_tag; tv_list=_ } -> let ct = match c_tag with - | Solver.Core.C_arrow -> "arrow" - | Solver.Core.C_option -> "option" - | Solver.Core.C_record -> failwith "record" - | Solver.Core.C_variant -> failwith "variant" - | Solver.Core.C_map -> "map" - | Solver.Core.C_big_map -> "big_map" - | Solver.Core.C_list -> "list" - | Solver.Core.C_set -> "set" - | Solver.Core.C_unit -> "unit" - | Solver.Core.C_bool -> "bool" - | Solver.Core.C_string -> "string" - | Solver.Core.C_nat -> "nat" - | Solver.Core.C_mutez -> "mutez" - | Solver.Core.C_timestamp -> "timestamp" - | Solver.Core.C_int -> "int" - | Solver.Core.C_address -> "address" - | Solver.Core.C_bytes -> "bytes" - | Solver.Core.C_key_hash -> "key_hash" - | Solver.Core.C_key -> "key" - | Solver.Core.C_signature -> "signature" - | Solver.Core.C_operation -> "operation" - | Solver.Core.C_contract -> "contract" - | Solver.Core.C_chain_id -> "chain_id" + | C_arrow -> "arrow" + | C_option -> "option" + | C_record -> failwith "record" + | C_variant -> failwith "variant" + | C_map -> "map" + | C_big_map -> "big_map" + | C_list -> "list" + | C_set -> "set" + | C_unit -> "unit" + | C_string -> "string" + | C_nat -> "nat" + | C_mutez -> "mutez" + | C_timestamp -> "timestamp" + | C_int -> "int" + | C_address -> "address" + | C_bytes -> "bytes" + | C_key_hash -> "key_hash" + | C_key -> "key" + | C_signature -> "signature" + | C_operation -> "operation" + | C_contract -> "contract" + | C_chain_id -> "chain_id" in fprintf ppf "CTOR %a %s()" Var.pp tv ct - |SC_Alias (a, b) -> fprintf ppf "Alias %a %a" Var.pp a Var.pp b + |SC_Alias { a; b } -> fprintf ppf "Alias %a %a" Var.pp a Var.pp b |SC_Poly _ -> fprintf ppf "Poly" |SC_Typeclass _ -> fprintf ppf "TC" @@ -48,6 +48,6 @@ let already_selected : _ -> already_selected -> unit = fun ppf already_selected let _ = already_selected in fprintf ppf "ALREADY_SELECTED" -let state : _ -> state -> unit = fun ppf state -> +let state : _ -> typer_state -> unit = fun ppf state -> let { structured_dbs=a ; already_selected=b } = state in fprintf ppf "STATE %a %a" structured_dbs a already_selected b diff --git a/src/passes/8-typer-new/dune b/src/passes/8-typer-new/dune index b7bbee5f4..bda5cb43a 100644 --- a/src/passes/8-typer-new/dune +++ b/src/passes/8-typer-new/dune @@ -8,6 +8,7 @@ ast_typed operators UnionFind + environment ) (preprocess (pps ppx_let) diff --git a/src/passes/8-typer-new/solver.ml b/src/passes/8-typer-new/solver.ml index ce2ba87d8..67b8b16b8 100644 --- a/src/passes/8-typer-new/solver.ml +++ b/src/passes/8-typer-new/solver.ml @@ -1,10 +1,15 @@ open Trace module Core = Typesystem.Core +module Map = RedBlackTrees.PolyMap +module Set = RedBlackTrees.PolySet +module UF = UnionFind.Poly2 module Wrap = Wrap open Wrap +open Ast_typed.Misc +(* TODO: remove this, it's not used anymore *) module TypeVariable = struct type t = Core.type_variable @@ -13,14 +18,6 @@ struct end -module UF = UnionFind.Partition0.Make(TypeVariable) - -type unionfind = UF.t - -(* end unionfind *) - -(* representant for an equivalence class of type variables *) -module TypeVariableMap = Map.Make(TypeVariable) (* @@ -59,48 +56,7 @@ Workflow: *) -open Core - -type structured_dbs = { - all_constraints : type_constraint_simpl list ; - aliases : unionfind ; - (* assignments (passive data structure). - Now: just a map from unification vars to types (pb: what about partial types?) - maybe just local assignments (allow only vars as children of pair(α,β)) *) - (* TODO: the rhs of the map should not repeat the variable name. *) - assignments : c_constructor_simpl TypeVariableMap.t ; - grouped_by_variable : constraints TypeVariableMap.t ; (* map from (unionfind) variables to constraints containing them *) - cycle_detection_toposort : unit ; (* example of structured db that we'll add later *) -} - -and constraints = { - (* If implemented in a language with decent sets, these should be sets not lists. *) - constructor : c_constructor_simpl list ; (* List of ('a = constructor(args…)) constraints *) - poly : c_poly_simpl list ; (* List of ('a = forall 'b, some_type) constraints *) - tc : c_typeclass_simpl list ; (* List of (typeclass(args…)) constraints *) -} - -and c_constructor_simpl = { - tv : type_variable; - c_tag : constant_tag; - tv_list : type_variable list; -} -(* copy-pasted from core.ml *) -and c_const = (type_variable * type_expression) -and c_equation = (type_expression * type_expression) -and c_typeclass_simpl = { - tc : typeclass ; - args : type_variable list ; -} -and c_poly_simpl = { - tv : type_variable ; - forall : p_forall ; -} -and type_constraint_simpl = - SC_Constructor of c_constructor_simpl (* α = ctor(β, …) *) - | SC_Alias of (type_variable * type_variable) (* α = β *) - | SC_Poly of c_poly_simpl (* α = forall β, δ where δ can be a more complex type *) - | SC_Typeclass of c_typeclass_simpl (* TC(α, …) *) +open Ast_typed.Types module UnionFindWrapper = struct (* Light wrapper for API for grouped_by_variable in the structured @@ -109,7 +65,7 @@ module UnionFindWrapper = struct fun variable dbs -> let variable , aliases = UF.get_or_set variable dbs.aliases in let dbs = { dbs with aliases } in - match TypeVariableMap.find_opt variable dbs.grouped_by_variable with + match Map.find_opt variable dbs.grouped_by_variable with Some l -> l | None -> { constructor = [] ; @@ -122,9 +78,9 @@ module UnionFindWrapper = struct let dbs = { dbs with aliases } in *) let variable_repr , aliases = UF.get_or_set variable dbs.aliases in let dbs = { dbs with aliases } in - let grouped_by_variable = TypeVariableMap.update variable_repr (function + let grouped_by_variable = Map.update variable_repr (function None -> Some c - | Some x -> Some { + | Some (x : constraints) -> Some { constructor = c.constructor @ x.constructor ; poly = c.poly @ x.poly ; tc = c.tc @ x.tc ; @@ -150,7 +106,7 @@ module UnionFindWrapper = struct (* Replace the two entries in grouped_by_variable by a single one *) ( let get_constraints ab = - match TypeVariableMap.find_opt ab dbs.grouped_by_variable with + match Map.find_opt ab dbs.grouped_by_variable with | Some x -> x | None -> { constructor = [] ; poly = [] ; tc = [] } in let constraints_a = get_constraints variable_repr_a in @@ -161,10 +117,10 @@ module UnionFindWrapper = struct tc = constraints_a.tc @ constraints_b.tc ; } in let grouped_by_variable = - TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in + Map.add variable_repr_a all_constraints dbs.grouped_by_variable in let dbs = { dbs with grouped_by_variable} in let grouped_by_variable = - TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in + Map.remove variable_repr_b dbs.grouped_by_variable in let dbs = { dbs with grouped_by_variable} in dbs ) @@ -207,7 +163,7 @@ let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_si SC_Constructor ({tv ; c_tag = _ ; tv_list} as c) -> store_constraint (tv :: tv_list) {constructor = [c] ; poly = [] ; tc = []} | SC_Typeclass ({tc = _ ; args} as c) -> store_constraint args {constructor = [] ; poly = [] ; tc = [c]} | SC_Poly ({tv; forall = _} as c) -> store_constraint [tv] {constructor = [] ; poly = [c] ; tc = []} - | SC_Alias (a , b) -> UnionFindWrapper.merge_constraints a b dbs + | SC_Alias { a; b } -> UnionFindWrapper.merge_constraints a b dbs in (dbs , [new_constraint]) (** Stores the first assinment ('a = ctor('b, …)) that is encountered. @@ -219,7 +175,7 @@ let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) nor fun dbs new_constraint -> match new_constraint with | SC_Constructor ({tv ; c_tag = _ ; tv_list = _} as c) -> - let assignments = TypeVariableMap.update tv (function None -> Some c | e -> e) dbs.assignments in + let assignments = Map.update tv (function None -> Some c | e -> e) dbs.assignments in let dbs = {dbs with assignments} in (dbs , [new_constraint]) | _ -> @@ -254,47 +210,47 @@ let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer fun dbs new_constraint -> let insert_fresh a b = let fresh = Core.fresh_type_variable () in - let (dbs , cs1) = normalizer_simpl dbs (C_equation (P_variable fresh, a)) in - let (dbs , cs2) = normalizer_simpl dbs (C_equation (P_variable fresh, b)) in + let (dbs , cs1) = normalizer_simpl dbs (c_equation (P_variable fresh) a) in + let (dbs , cs2) = normalizer_simpl dbs (c_equation (P_variable fresh) b) in (dbs , cs1 @ cs2) in let split_constant a c_tag args = let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in - let fresh_eqns = List.map (fun (v,t) -> C_equation (P_variable v, t)) (List.combine fresh_vars args) in + let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t) (List.combine fresh_vars args) in let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in (dbs , [SC_Constructor {tv=a;c_tag;tv_list=fresh_vars}] @ List.flatten recur) in let gather_forall a forall = (dbs , [SC_Poly { tv=a; forall }]) in - let gather_alias a b = (dbs , [SC_Alias (a, b)]) in + let gather_alias a b = (dbs , [SC_Alias { a ; b }]) in let reduce_type_app a b = let (reduced, new_constraints) = check_applied @@ type_level_eval b in let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs new_constraints in - let (dbs , resimpl) = normalizer_simpl dbs (C_equation (a , reduced)) in (* Note: this calls recursively but cant't fall in the same case. *) + let (dbs , resimpl) = normalizer_simpl dbs (c_equation a reduced) in (* Note: this calls recursively but cant't fall in the same case. *) (dbs , resimpl @ List.flatten recur) in let split_typeclass args tc = let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in - let fresh_eqns = List.map (fun (v,t) -> C_equation (P_variable v, t)) (List.combine fresh_vars args) in + let fresh_eqns = List.map (fun (v,t) -> c_equation (P_variable v) t) (List.combine fresh_vars args) in let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in (dbs, [SC_Typeclass { tc ; args = fresh_vars }] @ List.flatten recur) in match new_constraint with (* break down (forall 'b, body = forall 'c, body') into ('a = forall 'b, body and 'a = forall 'c, body')) *) - | C_equation ((P_forall _ as a), (P_forall _ as b)) -> insert_fresh a b + | C_equation {aval=(P_forall _ as a); bval=(P_forall _ as b)} -> insert_fresh a b (* break down (forall 'b, body = c(args)) into ('a = forall 'b, body and 'a = c(args)) *) - | C_equation ((P_forall _ as a), (P_constant _ as b)) -> insert_fresh a b + | C_equation {aval=(P_forall _ as a); bval=(P_constant _ as b)} -> insert_fresh a b (* break down (c(args) = c'(args')) into ('a = c(args) and 'a = c'(args')) *) - | C_equation ((P_constant _ as a), (P_constant _ as b)) -> insert_fresh a b + | C_equation {aval=(P_constant _ as a); bval=(P_constant _ as b)} -> insert_fresh a b (* break down (c(args) = forall 'b, body) into ('a = c(args) and 'a = forall 'b, body) *) - | C_equation ((P_constant _ as a), (P_forall _ as b)) -> insert_fresh a b - | C_equation ((P_forall forall), (P_variable b)) -> gather_forall b forall - | C_equation (P_variable a, P_forall forall) -> gather_forall a forall - | C_equation (P_variable a, P_variable b) -> gather_alias a b - | C_equation (P_variable a, P_constant (c_tag , args)) -> split_constant a c_tag args - | C_equation (P_constant (c_tag , args), P_variable b) -> split_constant b c_tag args + | C_equation {aval=(P_constant _ as a); bval=(P_forall _ as b)} -> insert_fresh a b + | C_equation {aval=(P_forall forall); bval=(P_variable b)} -> gather_forall b forall + | C_equation {aval=P_variable a; bval=P_forall forall} -> gather_forall a forall + | C_equation {aval=P_variable a; bval=P_variable b} -> gather_alias a b + | C_equation {aval=P_variable a; bval=P_constant { p_ctor_tag; p_ctor_args }} -> split_constant a p_ctor_tag p_ctor_args + | C_equation {aval=P_constant {p_ctor_tag; p_ctor_args}; bval=P_variable b} -> split_constant b p_ctor_tag p_ctor_args (* Reduce the type-level application, and simplify the resulting constraint + the extra constraints (typeclasses) that appeared at the forall binding site *) - | C_equation ((_ as a), (P_apply _ as b)) -> reduce_type_app a b - | C_equation ((P_apply _ as a), (_ as b)) -> reduce_type_app b a + | C_equation {aval=(_ as a); bval=(P_apply _ as b)} -> reduce_type_app a b + | C_equation {aval=(P_apply _ as a); bval=(_ as b)} -> reduce_type_app b a (* break down (TC(args)) into (TC('a, …) and ('a = arg) …) *) - | C_typeclass (args, tc) -> split_typeclass args tc - | C_access_label (tv, label, result) -> let _todo = ignore (tv, label, result) in failwith "TODO" + | C_typeclass { tc_args; typeclass } -> split_typeclass tc_args typeclass + | C_access_label { c_access_label_tval; accessor; c_access_label_tvar } -> let _todo = ignore (c_access_label_tval, accessor, c_access_label_tvar) in failwith "TODO" (* tv, label, result *) (* Random notes from live discussion. Kept here to include bits as a rationale later on / remind me of the discussion in the short term. * Feel free to erase if it rots here for too long. @@ -366,7 +322,6 @@ type 'selector_output propagator = 'selector_output -> structured_dbs -> new_con (* selector / propagation rule for breaking down composite types * For now: break pair(a, b) = pair(c, d) into a = c, b = d *) -type output_break_ctor = { a_k_var : c_constructor_simpl ; a_k'_var' : c_constructor_simpl } let selector_break_ctor : (type_constraint_simpl, output_break_ctor) selector = (* find two rules with the shape a = k(var …) and a = k'(var' …) *) fun type_constraint_simpl dbs -> @@ -376,6 +331,9 @@ let selector_break_ctor : (type_constraint_simpl, output_break_ctor) selector = with the same sort of constraint (constructor vs. constructor) is symmetric *) let other_cs = (UnionFindWrapper.get_constraints_related_to c.tv dbs).constructor in + let other_cs = List.filter (fun (o : c_constructor_simpl) -> Var.equal c.tv o.tv) other_cs in + (* TODO double-check the conditions in the propagator, we had a + bug here because the selector was too permissive. *) let cs_pairs = List.map (fun x -> { a_k_var = c ; a_k'_var' = x }) other_cs in WasSelected cs_pairs | SC_Alias _ -> WasNotSelected (* TODO: ??? (beware: symmetry) *) @@ -387,93 +345,89 @@ let compare_simple_c_constant = function | C_arrow -> (function (* N/A -> 1 *) | C_arrow -> 0 - | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) + | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_option -> (function | C_arrow -> 1 | C_option -> 0 - | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) + | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_record -> (function | C_arrow | C_option -> 1 | C_record -> 0 - | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) + | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_variant -> (function | C_arrow | C_option | C_record -> 1 | C_variant -> 0 - | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) + | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_map -> (function | C_arrow | C_option | C_record | C_variant -> 1 | C_map -> 0 - | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) + | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_big_map -> (function | C_arrow | C_option | C_record | C_variant | C_map -> 1 | C_big_map -> 0 - | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) + | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_list -> (function | C_arrow | C_option | C_record | C_variant | C_map | C_big_map -> 1 | C_list -> 0 - | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) + | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_set -> (function | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list -> 1 | C_set -> 0 - | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) + | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_unit -> (function | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set -> 1 | C_unit -> 0 - | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) - | C_bool -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit -> 1 - | C_bool -> 0 - | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) + | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_string -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool -> 1 + | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit -> 1 | C_string -> 0 | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_nat -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string -> 1 + | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string -> 1 | C_nat -> 0 | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_mutez -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat -> 1 + | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat -> 1 | C_mutez -> 0 | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_timestamp -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez -> 1 + | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez -> 1 | C_timestamp -> 0 | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_int -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp -> 1 + | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp -> 1 | C_int -> 0 | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_address -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1 + | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int -> 1 | C_address -> 0 | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_bytes -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1 + | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address -> 1 | C_bytes -> 0 | C_key_hash | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_key_hash -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1 + | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes -> 1 | C_key_hash -> 0 | C_key | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_key -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1 + | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash -> 1 | C_key -> 0 | C_signature | C_operation | C_contract | C_chain_id -> -1) | C_signature -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1 + | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key -> 1 | C_signature -> 0 | C_operation | C_contract | C_chain_id -> -1) | C_operation -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1 + | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature -> 1 | C_operation -> 0 | C_contract | C_chain_id -> -1) | C_contract -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1 + | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation -> 1 | C_contract -> 0 | C_chain_id -> -1) | C_chain_id -> (function - | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_bool | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> 1 + | C_arrow | C_option | C_record | C_variant | C_map | C_big_map | C_list | C_set | C_unit | C_string | C_nat | C_mutez | C_timestamp | C_int | C_address | C_bytes | C_key_hash | C_key | C_signature | C_operation | C_contract -> 1 | C_chain_id -> 0 (* N/A -> -1 *) ) @@ -483,29 +437,28 @@ let compare_simple_c_constant = function has been copied here. *) let debug_pp_constant : _ -> constant_tag -> unit = fun ppf c_tag -> let ct = match c_tag with - | Core.C_arrow -> "arrow" - | Core.C_option -> "option" - | Core.C_record -> failwith "record" - | Core.C_variant -> failwith "variant" - | Core.C_map -> "map" - | Core.C_big_map -> "big_map" - | Core.C_list -> "list" - | Core.C_set -> "set" - | Core.C_unit -> "unit" - | Core.C_bool -> "bool" - | Core.C_string -> "string" - | Core.C_nat -> "nat" - | Core.C_mutez -> "mutez" - | Core.C_timestamp -> "timestamp" - | Core.C_int -> "int" - | Core.C_address -> "address" - | Core.C_bytes -> "bytes" - | Core.C_key_hash -> "key_hash" - | Core.C_key -> "key" - | Core.C_signature -> "signature" - | Core.C_operation -> "operation" - | Core.C_contract -> "contract" - | Core.C_chain_id -> "chain_id" + | T.C_arrow -> "arrow" + | T.C_option -> "option" + | T.C_record -> failwith "record" + | T.C_variant -> failwith "variant" + | T.C_map -> "map" + | T.C_big_map -> "big_map" + | T.C_list -> "list" + | T.C_set -> "set" + | T.C_unit -> "unit" + | T.C_string -> "string" + | T.C_nat -> "nat" + | T.C_mutez -> "mutez" + | T.C_timestamp -> "timestamp" + | T.C_int -> "int" + | T.C_address -> "address" + | T.C_bytes -> "bytes" + | T.C_key_hash -> "key_hash" + | T.C_key -> "key" + | T.C_signature -> "signature" + | T.C_operation -> "operation" + | T.C_contract -> "contract" + | T.C_chain_id -> "chain_id" in Format.fprintf ppf "%s" ct @@ -520,7 +473,7 @@ let propagator_break_ctor : output_break_ctor propagator = (* produce constraints: *) (* a.tv = b.tv *) - let eq1 = C_equation (P_variable a.tv, P_variable b.tv) in + let eq1 = c_equation (P_variable a.tv) (P_variable b.tv) in (* a.c_tag = b.c_tag *) if (compare_simple_c_constant a.c_tag b.c_tag) <> 0 then failwith (Format.asprintf "type error: incompatible types, not same ctor %a vs. %a (compare returns %d)" debug_pp_c_constructor_simpl a debug_pp_c_constructor_simpl b (compare_simple_c_constant a.c_tag b.c_tag)) @@ -529,14 +482,13 @@ let propagator_break_ctor : output_break_ctor propagator = if List.length a.tv_list <> List.length b.tv_list then failwith "type error: incompatible types, not same length" else - let eqs3 = List.map2 (fun aa bb -> C_equation (P_variable aa, P_variable bb)) a.tv_list b.tv_list in + let eqs3 = List.map2 (fun aa bb -> c_equation (P_variable aa) (P_variable bb)) a.tv_list b.tv_list in let eqs = eq1 :: eqs3 in (eqs , []) (* no new assignments *) (* TODO : with our selectors, the selection depends on the order in which the constraints are added :-( :-( :-( :-( We need to return a lazy stream of constraints. *) -type output_specialize1 = { poly : c_poly_simpl ; a_k_var : c_constructor_simpl } let ( (function [] -> 0 | _::_ -> -1) (* This follows the behaviour of Pervasives.compare for lists of different length *) let compare_type_variable a b = Var.compare a b -let compare_label (a:accessor) (b:accessor) = +let compare_label (a:label) (b:label) = let Label a = a in let Label b = b in String.compare a b @@ -569,29 +521,29 @@ and compare_type_expression = function | P_variable b -> compare_type_variable a b | P_constant _ -> -1 | P_apply _ -> -1) - | P_constant (a1, a2) -> (function + | P_constant { p_ctor_tag=a1; p_ctor_args=a2 } -> (function | P_forall _ -> 1 | P_variable _ -> 1 - | P_constant (b1, b2) -> compare_simple_c_constant a1 b1 compare_list compare_type_expression a2 b2 + | P_constant { p_ctor_tag=b1; p_ctor_args=b2 } -> compare_simple_c_constant a1 b1 compare_list compare_type_expression a2 b2 | P_apply _ -> -1) - | P_apply (a1, a2) -> (function + | P_apply { tf=a1; targ=a2 } -> (function | P_forall _ -> 1 | P_variable _ -> 1 | P_constant _ -> 1 - | P_apply (b1, b2) -> compare_type_expression a1 b1 compare_type_expression a2 b2) + | P_apply { tf=b1; targ=b2 } -> compare_type_expression a1 b1 compare_type_expression a2 b2) and compare_type_constraint = function - | C_equation (a1, a2) -> (function - | C_equation (b1, b2) -> compare_type_expression a1 b1 compare_type_expression a2 b2 + | C_equation { aval=a1; bval=a2 } -> (function + | C_equation { aval=b1; bval=b2 } -> compare_type_expression a1 b1 compare_type_expression a2 b2 | C_typeclass _ -> -1 | C_access_label _ -> -1) - | C_typeclass (a1, a2) -> (function + | C_typeclass { tc_args=a1; typeclass=a2 } -> (function | C_equation _ -> 1 - | C_typeclass (b1, b2) -> compare_list compare_type_expression a1 b1 compare_typeclass a2 b2 + | C_typeclass { tc_args=b1; typeclass=b2 } -> compare_list compare_type_expression a1 b1 compare_typeclass a2 b2 | C_access_label _ -> -1) - | C_access_label (a1, a2, a3) -> (function + | C_access_label { c_access_label_tval=a1; accessor=a2; c_access_label_tvar=a3 } -> (function | C_equation _ -> 1 | C_typeclass _ -> 1 - | C_access_label (b1, b2, b3) -> compare_type_expression a1 b1 compare_label a2 b2 compare_type_variable a3 b3) + | C_access_label { c_access_label_tval=b1; accessor=b2; c_access_label_tvar=b3 } -> compare_type_expression a1 b1 compare_label a2 b2 compare_type_variable a3 b3) let compare_type_constraint_list = compare_list compare_type_constraint let compare_p_forall { binder = a1; constraints = a2; body = a3 } @@ -612,17 +564,6 @@ let compare_output_specialize1 { poly = a1; a_k_var = a2 } { poly = b1; a_k_var let compare_output_break_ctor { a_k_var=a1; a_k'_var'=a2 } { a_k_var=b1; a_k'_var'=b2 } = compare_c_constructor_simpl a1 b1 compare_c_constructor_simpl a2 b2 -module OutputSpecialize1 : (Set.OrderedType with type t = output_specialize1) = struct - type t = output_specialize1 - let compare = compare_output_specialize1 -end - - -module BreakCtor : (Set.OrderedType with type t = output_break_ctor) = struct - type t = output_break_ctor - let compare = compare_output_break_ctor -end - let selector_specialize1 : (type_constraint_simpl, output_specialize1) selector = (* find two rules with the shape (a = forall b, d) and a = k'(var' …) or vice versa *) (* TODO: do the same for two rules with the shape (a = forall b, d) and tc(a…) *) @@ -656,23 +597,21 @@ let propagator_specialize1 : output_specialize1 propagator = let fresh_existential = Core.fresh_type_variable () in (* Produce the constraint (b.tv = a.body[a.binder |-> fresh_existential]) The substitution is obtained by immediately applying the forall. *) - let apply = (P_apply (P_forall a.forall , P_variable fresh_existential)) in + let apply = (P_apply {tf = (P_forall a.forall); targ = P_variable fresh_existential}) in let (reduced, new_constraints) = check_applied @@ type_level_eval apply in - let eq1 = C_equation (P_variable b.tv, reduced) in + let eq1 = c_equation (P_variable b.tv) reduced in let eqs = eq1 :: new_constraints in (eqs, []) (* no new assignments *) -module M (BlaBla : Set.OrderedType) = struct - module AlreadySelected = Set.Make(BlaBla) - - let select_and_propagate : ('old_input, 'selector_output) selector -> BlaBla.t propagator -> _ -> 'a -> structured_dbs -> _ * new_constraints * new_assignments = + let select_and_propagate : ('old_input, 'selector_output) selector -> _ propagator -> _ -> 'a -> structured_dbs -> _ * new_constraints * new_assignments = + let mem elt set = match RedBlackTrees.PolySet.find_opt elt set with None -> false | Some _ -> true in fun selector propagator -> fun already_selected old_type_constraint dbs -> (* TODO: thread some state to know which selector outputs were already seen *) match selector old_type_constraint dbs with WasSelected selected_outputs -> (* TODO: fold instead. *) - let (already_selected , selected_outputs) = List.fold_left (fun (already_selected, selected_outputs) elt -> if AlreadySelected.mem elt already_selected then (AlreadySelected.add elt already_selected , elt :: selected_outputs) + let (already_selected , selected_outputs) = List.fold_left (fun (already_selected, selected_outputs) elt -> if mem elt already_selected then (RedBlackTrees.PolySet.add elt already_selected , elt :: selected_outputs) else (already_selected , selected_outputs)) (already_selected , selected_outputs) selected_outputs in (* Call the propagation rule *) let new_contraints_and_assignments = List.map (fun s -> propagator s dbs) selected_outputs in @@ -681,25 +620,16 @@ module M (BlaBla : Set.OrderedType) = struct (already_selected , List.flatten new_constraints , List.flatten new_assignments) | WasNotSelected -> (already_selected, [] , []) -end -module M_break_ctor = M(BreakCtor) -module M_specialize1 = M(OutputSpecialize1) - -let select_and_propagate_break_ctor = M_break_ctor.select_and_propagate selector_break_ctor propagator_break_ctor -let select_and_propagate_specialize1 = M_specialize1.select_and_propagate selector_specialize1 propagator_specialize1 - -type already_selected = { - break_ctor : M_break_ctor.AlreadySelected.t ; - specialize1 : M_specialize1.AlreadySelected.t ; -} +let select_and_propagate_break_ctor = select_and_propagate selector_break_ctor propagator_break_ctor +let select_and_propagate_specialize1 = select_and_propagate selector_specialize1 propagator_specialize1 (* Takes a constraint, applies all selector+propagator pairs to it. Keeps track of which constraints have already been selected. *) let select_and_propagate_all' : _ -> type_constraint_simpl selector_input -> structured_dbs -> _ * new_constraints * structured_dbs = let aux sel_propag new_constraint (already_selected , new_constraints , dbs) = let (already_selected , new_constraints', new_assignments) = sel_propag already_selected new_constraint dbs in - let assignments = List.fold_left (fun acc ({tv;c_tag=_;tv_list=_} as ele) -> TypeVariableMap.update tv (function None -> Some ele | x -> x) acc) dbs.assignments new_assignments in + let assignments = List.fold_left (fun acc ({tv;c_tag=_;tv_list=_} as ele) -> Map.update tv (function None -> Some ele | x -> x) acc) dbs.assignments new_assignments in let dbs = { dbs with assignments } in (already_selected , new_constraints' @ new_constraints , dbs) in @@ -757,12 +687,7 @@ let rec select_and_propagate_all : _ -> type_constraint selector_input list -> s * constraints : constraints TypeVariableMap.t ; * } *) -type state = { - structured_dbs : structured_dbs ; - already_selected : already_selected ; -} - -let initial_state : state = (* { +let initial_state : typer_state = (* { * unification_vars = UF.empty ; * constraints = TypeVariableMap.empty ; * assignments = TypeVariableMap.empty ; @@ -771,14 +696,14 @@ let initial_state : state = (* { structured_dbs = { all_constraints = [] ; (* type_constraint_simpl list *) - aliases = UF.empty ; (* unionfind *) - assignments = TypeVariableMap.empty; (* c_constructor_simpl TypeVariableMap.t *) - grouped_by_variable = TypeVariableMap.empty; (* constraints TypeVariableMap.t *) + aliases = UF.empty (fun s -> Format.asprintf "%a" Var.pp s) Var.compare ; (* unionfind *) + assignments = Map.create ~cmp:Var.compare; (* c_constructor_simpl TypeVariableMap.t *) + grouped_by_variable = Map.create ~cmp:Var.compare; (* constraints TypeVariableMap.t *) cycle_detection_toposort = (); (* unit *) } ; already_selected = { - break_ctor = M_break_ctor.AlreadySelected.empty ; - specialize1 = M_specialize1.AlreadySelected.empty ; + break_ctor = Set.create ~cmp:compare_output_break_ctor; + specialize1 = Set.create ~cmp:compare_output_specialize1 ; } } @@ -789,7 +714,7 @@ let initial_state : state = (* { Also, we should check at these places that we indeed do not need the state any further. Suzanne *) -let discard_state (_ : state) = () +let discard_state (_ : typer_state) = () (* let replace_var_in_state = fun (v : type_variable) (state : state) -> *) (* let aux_tv : type_expression -> _ = function *) @@ -809,7 +734,7 @@ let discard_state (_ : state) = () (* in List.map aux state *) (* This is the solver *) -let aggregate_constraints : state -> type_constraint list -> state result = fun state newc -> +let aggregate_constraints : typer_state -> type_constraint list -> typer_state result = fun state newc -> (* TODO: Iterate over constraints *) let _todo = ignore (state, newc) in let (a, b) = select_and_propagate_all state.already_selected newc state.structured_dbs in diff --git a/src/passes/8-typer-new/todo_use_fold_generator.ml b/src/passes/8-typer-new/todo_use_fold_generator.ml index 8256f039e..ce3e2fe98 100644 --- a/src/passes/8-typer-new/todo_use_fold_generator.ml +++ b/src/passes/8-typer-new/todo_use_fold_generator.ml @@ -10,7 +10,6 @@ let convert_type_constant : I.type_constant -> O.type_constant = function | TC_nat -> TC_nat | TC_int -> TC_int | TC_mutez -> TC_mutez - | TC_bool -> TC_bool | TC_operation -> TC_operation | TC_address -> TC_address | TC_key -> TC_key diff --git a/src/passes/8-typer-new/typer.ml b/src/passes/8-typer-new/typer.ml index 71ec621c2..e6c7955a7 100644 --- a/src/passes/8-typer-new/typer.ml +++ b/src/passes/8-typer-new/typer.ml @@ -2,18 +2,20 @@ open Trace module I = Ast_core module O = Ast_typed open O.Combinators +module DEnv = Environment module Environment = O.Environment module Solver = Solver type environment = Environment.t module Errors = Errors open Errors +module Map = RedBlackTrees.PolyMap open Todo_use_fold_generator (* Extract pairs of (name,type) in the declaration and add it to the environment *) -let rec type_declaration env state : I.declaration -> (environment * Solver.state * O.declaration option) result = function +let rec type_declaration env state : I.declaration -> (environment * O.typer_state * O.declaration option) result = function | Declaration_type (type_name , type_expression) -> let%bind tv = evaluate_type env type_expression in let env' = Environment.add_type (type_name) tv env in @@ -30,15 +32,8 @@ let rec type_declaration env state : I.declaration -> (environment * Solver.stat ok (post_env, state' , Some (O.Declaration_constant { binder ; expr ; inline ; post_env} )) ) -and type_match : environment -> Solver.state -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> (O.matching_expr * Solver.state) result = +and type_match : environment -> O.typer_state -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> (O.matching_expr * O.typer_state) result = fun e state t i ae loc -> match i with - | Match_bool {match_true ; match_false} -> - let%bind _ = - trace_strong (match_error ~expected:i ~actual:t loc) - @@ get_t_bool t in - let%bind (match_true , state') = type_expression e state match_true in - let%bind (match_false , state'') = type_expression e state' match_false in - ok (O.Match_bool {match_true ; match_false} , state'') | Match_option {match_none ; match_some} -> let%bind tv = trace_strong (match_error ~expected:i ~actual:t loc) @@ -186,18 +181,14 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu | TC_contract c -> let%bind c = evaluate_type e c in ok @@ O.TC_contract c - | TC_arrow ( arg , ret ) -> - let%bind arg' = evaluate_type e arg in - let%bind ret' = evaluate_type e ret in - ok @@ O.TC_arrow { type1=arg' ; type2=ret' } in return (T_operator (opt)) -and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.state) result = fun e state ?tv_opt ae -> +and type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result = fun e state ?tv_opt ae -> let () = ignore tv_opt in (* For compatibility with the old typer's API, this argument can be removed once the new typer is used. *) let open Solver in let module L = Logger.Stateful() in - let return : _ -> Solver.state -> _ -> _ (* return of type_expression *) = fun expr state constraints type_name -> + let return : _ -> O.typer_state -> _ -> _ (* return of type_expression *) = fun expr state constraints type_name -> let%bind new_state = aggregate_constraints state constraints in let tv = t_variable type_name () in let location = ae.location in @@ -233,9 +224,6 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression - return expr' state constraints expr_type ) - | E_literal (Literal_bool b) -> ( - return_wrapped (e_bool b) state @@ Wrap.literal (t_bool ()) - ) | E_literal (Literal_string s) -> ( return_wrapped (e_string s) state @@ Wrap.literal (t_string ()) ) @@ -366,7 +354,6 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression - let tvs = let aux (cur : O.matching_expr) = match cur with - | Match_bool { match_true ; match_false } -> [ match_true ; match_false ] | Match_list { match_nil ; match_cons = { hd=_ ; tl=_ ; body ; tv=_} } -> [ match_nil ; body ] | Match_option { match_none ; match_some = {opt=_; body; tv=_} } -> [ match_none ; body ] | Match_tuple { vars=_ ; body ; tvs=_ } -> [ body ] @@ -440,8 +427,8 @@ and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type ok(name, tv) (* Apply type_declaration on every node of the AST_core from the root p *) -let type_program_returns_state ((env, state, p) : environment * Solver.state * I.program) : (environment * Solver.state * O.program) result = - let aux ((e : environment), (s : Solver.state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) = +let type_program_returns_state ((env, state, p) : environment * O.typer_state * I.program) : (environment * O.typer_state * O.program) result = + let aux ((e : environment), (s : O.typer_state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) = let%bind (e' , s' , d'_opt) = type_declaration e s (Location.unwrap d) in let ds' = match d'_opt with | None -> ds @@ -455,8 +442,8 @@ let type_program_returns_state ((env, state, p) : environment * Solver.state * I let declarations = List.rev declarations in (* Common hack to have O(1) append: prepend and then reverse *) ok (env', state', declarations) -let type_and_subst_xyz (env_state_node : environment * Solver.state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * Solver.state * 'a) -> (environment * Solver.state * 'b) Trace.result) : ('b * Solver.state) result = - let%bind (env, state, program) = type_xyz_returns_state env_state_node in +let type_and_subst_xyz (env_state_node : environment * O.typer_state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * O.typer_state * 'a) -> (environment * O.typer_state * 'b) Trace.result) : ('b * O.typer_state) result = + let%bind (env, state, node) = type_xyz_returns_state env_state_node in let subst_all = let aliases = state.structured_dbs.aliases in let assignments = state.structured_dbs.assignments in @@ -468,29 +455,29 @@ let type_and_subst_xyz (env_state_node : environment * Solver.state * 'a) (apply try Some (Solver.UF.repr variable aliases) with Not_found -> None in let%bind assignment = trace_option (simple_error (Format.asprintf "can't find assignment for root %a" Var.pp root)) @@ - (Solver.TypeVariableMap.find_opt root assignments) in - let Solver.{ tv ; c_tag ; tv_list } = assignment in + (Map.find_opt root assignments) in + let O.{ tv ; c_tag ; tv_list } = assignment in let () = ignore tv (* I think there is an issue where the tv is stored twice (as a key and in the element itself) *) in let%bind (expr : O.type_content) = Typesystem.Core.type_expression'_of_simple_c_constant (c_tag , (List.map (fun s -> O.t_variable s ()) tv_list)) in ok @@ expr in - let p = apply_substs ~substs program in + let p = apply_substs ~substs node in p in - let%bind program = subst_all in + let%bind node = subst_all in let () = ignore env in (* TODO: shouldn't we use the `env` somewhere? *) - ok (program, state) + ok (node, state) -let type_program (p : I.program) : (O.program * Solver.state) result = - let empty_env = Ast_typed.Environment.full_empty in +let type_program (p : I.program) : (O.program * O.typer_state) result = + let empty_env = DEnv.default in let empty_state = Solver.initial_state in type_and_subst_xyz (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state -let type_expression_returns_state : (environment * Solver.state * I.expression) -> (environment * Solver.state * O.expression) Trace.result = +let type_expression_returns_state : (environment * O.typer_state * I.expression) -> (environment * O.typer_state * O.expression) Trace.result = fun (env, state, e) -> let%bind (e , state) = type_expression env state e in ok (env, state, e) -let type_expression_subst (env : environment) (state : Solver.state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * Solver.state) result = +let type_expression_subst (env : environment) (state : O.typer_state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * O.typer_state) result = let () = ignore tv_opt in (* For compatibility with the old typer's API, this argument can be removed once the new typer is used. *) type_and_subst_xyz (env , state , e) Typesystem.Misc.Substitution.Pattern.s_expression type_expression_returns_state @@ -498,14 +485,14 @@ let untype_type_expression = Untyper.untype_type_expression let untype_expression = Untyper.untype_expression (* These aliases are just here for quick navigation during debug, and can safely be removed later *) -let [@warning "-32"] (*rec*) type_declaration _env _state : I.declaration -> (environment * Solver.state * O.declaration option) result = type_declaration _env _state -and [@warning "-32"] type_match : environment -> Solver.state -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> (O.matching_expr * Solver.state) result = type_match +let [@warning "-32"] (*rec*) type_declaration _env _state : I.declaration -> (environment * O.typer_state * O.declaration option) result = type_declaration _env _state +and [@warning "-32"] type_match : environment -> O.typer_state -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> (O.matching_expr * O.typer_state) result = type_match and [@warning "-32"] evaluate_type (e:environment) (t:I.type_expression) : O.type_expression result = evaluate_type e t -and [@warning "-32"] type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.state) result = type_expression +and [@warning "-32"] type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result = type_expression and [@warning "-32"] type_lambda e state lam = type_lambda e state lam and [@warning "-32"] type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result = type_constant name lst tv_opt -let [@warning "-32"] type_program_returns_state ((env, state, p) : environment * Solver.state * I.program) : (environment * Solver.state * O.program) result = type_program_returns_state (env, state, p) -let [@warning "-32"] type_and_subst_xyz (env_state_node : environment * Solver.state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * Solver.state * 'a) -> (environment * Solver.state * 'b) Trace.result) : ('b * Solver.state) result = type_and_subst_xyz env_state_node apply_substs type_xyz_returns_state -let [@warning "-32"] type_program (p : I.program) : (O.program * Solver.state) result = type_program p -let [@warning "-32"] type_expression_returns_state : (environment * Solver.state * I.expression) -> (environment * Solver.state * O.expression) Trace.result = type_expression_returns_state -let [@warning "-32"] type_expression_subst (env : environment) (state : Solver.state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * Solver.state) result = type_expression_subst env state ?tv_opt e +let [@warning "-32"] type_program_returns_state ((env, state, p) : environment * O.typer_state * I.program) : (environment * O.typer_state * O.program) result = type_program_returns_state (env, state, p) +let [@warning "-32"] type_and_subst_xyz (env_state_node : environment * O.typer_state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * O.typer_state * 'a) -> (environment * O.typer_state * 'b) Trace.result) : ('b * O.typer_state) result = type_and_subst_xyz env_state_node apply_substs type_xyz_returns_state +let [@warning "-32"] type_program (p : I.program) : (O.program * O.typer_state) result = type_program p +let [@warning "-32"] type_expression_returns_state : (environment * O.typer_state * I.expression) -> (environment * O.typer_state * O.expression) Trace.result = type_expression_returns_state +let [@warning "-32"] type_expression_subst (env : environment) (state : O.typer_state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * O.typer_state) result = type_expression_subst env state ?tv_opt e diff --git a/src/passes/8-typer-new/typer.mli b/src/passes/8-typer-new/typer.mli index e5b91de0a..9c2e267fc 100644 --- a/src/passes/8-typer-new/typer.mli +++ b/src/passes/8-typer-new/typer.mli @@ -38,11 +38,11 @@ module Errors : sig *) end -val type_program : I.program -> (O.program * Solver.state) result -val type_declaration : environment -> Solver.state -> I.declaration -> (environment * Solver.state * O.declaration option) result +val type_program : I.program -> (O.program * O.typer_state) result +val type_declaration : environment -> O.typer_state -> I.declaration -> (environment * O.typer_state * O.declaration option) result val evaluate_type : environment -> I.type_expression -> O.type_expression result -val type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.state) result -val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.state) result +val type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result +val type_expression_subst : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result val type_constant : I.constant' -> O.type_expression list -> O.type_expression option -> (O.constant' * O.type_expression) result val untype_type_expression : O.type_expression -> I.type_expression result diff --git a/src/passes/8-typer-new/untyper.ml b/src/passes/8-typer-new/untyper.ml index f082bd072..11b3ef3b9 100644 --- a/src/passes/8-typer-new/untyper.ml +++ b/src/passes/8-typer-new/untyper.ml @@ -13,7 +13,6 @@ let unconvert_type_constant : O.type_constant -> I.type_constant = function | TC_nat -> TC_nat | TC_int -> TC_int | TC_mutez -> TC_mutez - | TC_bool -> TC_bool | TC_operation -> TC_operation | TC_address -> TC_address | TC_key -> TC_key @@ -194,10 +193,6 @@ let rec untype_type_expression (t:O.type_expression) : (I.type_expression) resul let%bind k = untype_type_expression k in let%bind v = untype_type_expression v in ok @@ I.TC_map_or_big_map (k,v) - | O.TC_arrow { type1=arg ; type2=ret } -> - let%bind arg' = untype_type_expression arg in - let%bind ret' = untype_type_expression ret in - ok @@ I.TC_arrow ( arg' , ret' ) | O.TC_contract c-> let%bind c = untype_type_expression c in ok @@ I.TC_contract c @@ -219,7 +214,6 @@ let untype_literal (l:O.literal) : I.literal result = match l with | Literal_unit -> ok Literal_unit | Literal_void -> ok Literal_void - | Literal_bool b -> ok (Literal_bool b) | Literal_nat n -> ok (Literal_nat n) | Literal_timestamp n -> ok (Literal_timestamp n) | Literal_mutez n -> ok (Literal_mutez n) @@ -301,10 +295,6 @@ and untype_lambda ty {binder; result} : I.lambda result = and untype_matching : (O.expression -> I.expression result) -> O.matching_expr -> I.matching_expr result = fun f m -> let open I in match m with - | Match_bool {match_true ; match_false} -> - let%bind match_true = f match_true in - let%bind match_false = f match_false in - ok @@ Match_bool {match_true ; match_false} | Match_tuple { vars ; body ; tvs=_ } -> let%bind b = f body in ok @@ I.Match_tuple ((vars, b),[]) diff --git a/src/passes/8-typer-new/wrap.ml b/src/passes/8-typer-new/wrap.ml index f51a38140..d5125e362 100644 --- a/src/passes/8-typer-new/wrap.ml +++ b/src/passes/8-typer-new/wrap.ml @@ -1,4 +1,5 @@ open Trace +open Ast_typed.Misc module Core = Typesystem.Core module I = Ast_core @@ -35,19 +36,18 @@ let rec type_expression_to_type_value : T.type_expression -> O.type_value = fun | T_sum kvmap -> let () = failwith "fixme: don't use to_list, it drops the variant keys, rows have a differnt kind than argument lists for now!" in let tlist = List.map (fun ({ctor_type;_}:T.ctor_content) -> ctor_type) (T.CMap.to_list kvmap) in - P_constant (C_variant, List.map type_expression_to_type_value tlist) + p_constant C_variant (List.map type_expression_to_type_value tlist) | T_record kvmap -> let () = failwith "fixme: don't use to_list, it drops the record keys, rows have a differnt kind than argument lists for now!" in let tlist = List.map (fun ({field_type;_}:T.field_content) -> field_type) (T.LMap.to_list kvmap) in - P_constant (C_record, List.map type_expression_to_type_value tlist) + p_constant C_record (List.map type_expression_to_type_value tlist) | T_arrow {type1;type2} -> - P_constant (C_arrow, List.map type_expression_to_type_value [ type1 ; type2 ]) + p_constant C_arrow (List.map type_expression_to_type_value [ type1 ; type2 ]) | T_variable (type_name) -> P_variable type_name | T_constant (type_name) -> - let csttag = Core.(match type_name with + let csttag = T.(match type_name with | TC_unit -> C_unit - | TC_bool -> C_bool | TC_string -> C_string | TC_nat -> C_nat | TC_mutez -> C_mutez @@ -63,44 +63,42 @@ let rec type_expression_to_type_value : T.type_expression -> O.type_value = fun | TC_void -> C_unit (* TODO : replace with void *) ) in - P_constant (csttag, []) + p_constant csttag [] | T_operator (type_operator) -> - let (csttag, args) = Core.(match type_operator with + let (csttag, args) = T.(match type_operator with | TC_option o -> (C_option, [o]) | TC_set s -> (C_set, [s]) | TC_map { k ; v } -> (C_map, [k;v]) | TC_big_map { k ; v } -> (C_big_map, [k;v]) | TC_map_or_big_map { k ; v } -> (C_map, [k;v]) - | TC_arrow { type1 ; type2 } -> (C_arrow, [ type1 ; type2 ]) | TC_list l -> (C_list, [l]) | TC_contract c -> (C_contract, [c]) ) in - P_constant (csttag, List.map type_expression_to_type_value args) + p_constant csttag (List.map type_expression_to_type_value args) let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_value = fun te -> match te.type_content with | T_sum kvmap -> let () = failwith "fixme: don't use to_list, it drops the variant keys, rows have a differnt kind than argument lists for now!" in let tlist = List.map (fun ({ctor_type;_}:I.ctor_content) -> ctor_type) (I.CMap.to_list kvmap) in - P_constant (C_variant, List.map type_expression_to_type_value_copypasted tlist) + p_constant C_variant (List.map type_expression_to_type_value_copypasted tlist) | T_record kvmap -> let () = failwith "fixme: don't use to_list, it drops the record keys, rows have a differnt kind than argument lists for now!" in let tlist = List.map (fun ({field_type;_}:I.field_content) -> field_type) (I.LMap.to_list kvmap) in - P_constant (C_record, List.map type_expression_to_type_value_copypasted tlist) + p_constant C_record (List.map type_expression_to_type_value_copypasted tlist) | T_arrow {type1;type2} -> - P_constant (C_arrow, List.map type_expression_to_type_value_copypasted [ type1 ; type2 ]) + p_constant C_arrow (List.map type_expression_to_type_value_copypasted [ type1 ; type2 ]) | T_variable type_name -> P_variable (type_name) (* eird stuff*) | T_constant (type_name) -> - let csttag = Core.(match type_name with + let csttag = T.(match type_name with | TC_unit -> C_unit - | TC_bool -> C_bool | TC_string -> C_string | _ -> failwith "unknown type constructor") in - P_constant (csttag,[]) + p_constant csttag [] | T_operator (type_name) -> - let (csttag, args) = Core.(match type_name with + let (csttag, args) = T.(match type_name with | TC_option o -> (C_option , [o]) | TC_list l -> (C_list , [l]) | TC_set s -> (C_set , [s]) @@ -108,10 +106,9 @@ let rec type_expression_to_type_value_copypasted : I.type_expression -> O.type_v | TC_big_map ( k , v ) -> (C_big_map, [k;v]) | TC_map_or_big_map ( k , v) -> (C_map, [k;v]) | TC_contract c -> (C_contract, [c]) - | TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ]) ) in - P_constant (csttag, List.map type_expression_to_type_value_copypasted args) + p_constant csttag (List.map type_expression_to_type_value_copypasted args) let failwith_ : unit -> (constraints * O.type_variable) = fun () -> let type_name = Core.fresh_type_variable () in @@ -120,12 +117,12 @@ let failwith_ : unit -> (constraints * O.type_variable) = fun () -> let variable : I.expression_variable -> T.type_expression -> (constraints * T.type_variable) = fun _name expr -> let pattern = type_expression_to_type_value expr in let type_name = Core.fresh_type_variable () in - [C_equation (P_variable (type_name) , pattern)] , type_name + [C_equation { aval = P_variable type_name ; bval = pattern }] , type_name let literal : T.type_expression -> (constraints * T.type_variable) = fun t -> let pattern = type_expression_to_type_value t in let type_name = Core.fresh_type_variable () in - [C_equation (P_variable (type_name) , pattern)] , type_name + [C_equation { aval = P_variable type_name ; bval = pattern }] , type_name (* let literal_bool : unit -> (constraints * O.type_variable) = fun () -> @@ -141,9 +138,9 @@ let literal : T.type_expression -> (constraints * T.type_variable) = fun t -> let tuple : T.type_expression list -> (constraints * T.type_variable) = fun tys -> let patterns = List.map type_expression_to_type_value tys in - let pattern = O.(P_constant (C_record , patterns)) in + let pattern = p_constant C_record patterns in let type_name = Core.fresh_type_variable () in - [C_equation (P_variable (type_name) , pattern)] , type_name + [C_equation { aval = P_variable type_name ; bval = pattern}] , type_name (* let t_tuple = ('label:int, 'v) … -> record ('label : 'v) … *) (* let t_constructor = ('label:string, 'v) -> variant ('label : 'v) *) @@ -172,8 +169,9 @@ end let access_label ~(base : T.type_expression) ~(label : O.accessor) : (constraints * T.type_variable) = let base' = type_expression_to_type_value base in let expr_type = Core.fresh_type_variable () in - [O.C_access_label (base' , label , expr_type)] , expr_type + [T.C_access_label { c_access_label_tval = base' ; accessor = label ; c_access_label_tvar = expr_type }] , expr_type +open Ast_typed.Misc let constructor : T.type_expression -> T.type_expression -> T.type_expression -> (constraints * T.type_variable) = fun t_arg c_arg sum -> @@ -182,64 +180,64 @@ let constructor let sum = type_expression_to_type_value sum in let whole_expr = Core.fresh_type_variable () in [ - C_equation (P_variable (whole_expr) , sum) ; - C_equation (t_arg , c_arg) + c_equation (P_variable whole_expr) sum ; + c_equation t_arg c_arg ; ] , whole_expr let record : T.field_content T.label_map -> (constraints * T.type_variable) = fun fields -> let record_type = type_expression_to_type_value (T.t_record fields ()) in let whole_expr = Core.fresh_type_variable () in - [C_equation (P_variable whole_expr , record_type)] , whole_expr + [c_equation (P_variable whole_expr) record_type] , whole_expr let collection : O.constant_tag -> T.type_expression list -> (constraints * T.type_variable) = fun ctor element_tys -> - let elttype = O.P_variable (Core.fresh_type_variable ()) in + let elttype = T.P_variable (Core.fresh_type_variable ()) in let aux elt = let elt' = type_expression_to_type_value elt - in O.C_equation (elttype , elt') in + in c_equation elttype elt' in let equations = List.map aux element_tys in let whole_expr = Core.fresh_type_variable () in - O.[ - C_equation (P_variable whole_expr , O.P_constant (ctor , [elttype])) + [ + c_equation (P_variable whole_expr) (p_constant ctor [elttype]) ; ] @ equations , whole_expr -let list = collection O.C_list -let set = collection O.C_set +let list = collection T.C_list +let set = collection T.C_set let map : (T.type_expression * T.type_expression) list -> (constraints * T.type_variable) = fun kv_tys -> - let k_type = O.P_variable (Core.fresh_type_variable ()) in - let v_type = O.P_variable (Core.fresh_type_variable ()) in + let k_type = T.P_variable (Core.fresh_type_variable ()) in + let v_type = T.P_variable (Core.fresh_type_variable ()) in let aux_k (k , _v) = let k' = type_expression_to_type_value k in - O.C_equation (k_type , k') in + c_equation k_type k' in let aux_v (_k , v) = let v' = type_expression_to_type_value v in - O.C_equation (v_type , v') in + c_equation v_type v' in let equations_k = List.map aux_k kv_tys in let equations_v = List.map aux_v kv_tys in let whole_expr = Core.fresh_type_variable () in - O.[ - C_equation (P_variable whole_expr , O.P_constant (C_map , [k_type ; v_type])) + [ + c_equation (P_variable whole_expr) (p_constant C_map [k_type ; v_type]) ; ] @ equations_k @ equations_v , whole_expr let big_map : (T.type_expression * T.type_expression) list -> (constraints * T.type_variable) = fun kv_tys -> - let k_type = O.P_variable (Core.fresh_type_variable ()) in - let v_type = O.P_variable (Core.fresh_type_variable ()) in + let k_type = T.P_variable (Core.fresh_type_variable ()) in + let v_type = T.P_variable (Core.fresh_type_variable ()) in let aux_k (k , _v) = let k' = type_expression_to_type_value k in - O.C_equation (k_type , k') in + c_equation k_type k' in let aux_v (_k , v) = let v' = type_expression_to_type_value v in - O.C_equation (v_type , v') in + c_equation v_type v' in let equations_k = List.map aux_k kv_tys in let equations_v = List.map aux_v kv_tys in let whole_expr = Core.fresh_type_variable () in - O.[ + [ (* TODO: this doesn't tag big_maps uniquely (i.e. if two big_map have the same type, they can be swapped. *) - C_equation (P_variable whole_expr , O.P_constant (C_big_map , [k_type ; v_type])) + c_equation (P_variable whole_expr) (p_constant C_big_map [k_type ; v_type]) ; ] @ equations_k @ equations_v , whole_expr let application : T.type_expression -> T.type_expression -> (constraints * T.type_variable) = @@ -247,8 +245,8 @@ let application : T.type_expression -> T.type_expression -> (constraints * T.typ let whole_expr = Core.fresh_type_variable () in let f' = type_expression_to_type_value f in let arg' = type_expression_to_type_value arg in - O.[ - C_equation (f' , P_constant (C_arrow , [arg' ; P_variable whole_expr])) + [ + c_equation f' (p_constant C_arrow [arg' ; P_variable whole_expr]) ; ] , whole_expr let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_variable) = @@ -257,9 +255,9 @@ let look_up : T.type_expression -> T.type_expression -> (constraints * T.type_va let ind' = type_expression_to_type_value ind in let whole_expr = Core.fresh_type_variable () in let v = Core.fresh_type_variable () in - O.[ - C_equation (ds' , P_constant (C_map, [ind' ; P_variable v])) ; - C_equation (P_variable whole_expr , P_constant (C_option , [P_variable v])) + [ + c_equation ds' (p_constant C_map [ind' ; P_variable v]) ; + c_equation (P_variable whole_expr) (p_constant C_option [P_variable v]) ; ] , whole_expr let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_variable) = @@ -267,9 +265,9 @@ let sequence : T.type_expression -> T.type_expression -> (constraints * T.type_v let a' = type_expression_to_type_value a in let b' = type_expression_to_type_value b in let whole_expr = Core.fresh_type_variable () in - O.[ - C_equation (a' , P_constant (C_unit , [])) ; - C_equation (b' , P_variable whole_expr) + [ + c_equation a' (p_constant C_unit []) ; + c_equation b' (P_variable whole_expr) ; ] , whole_expr let loop : T.type_expression -> T.type_expression -> (constraints * T.type_variable) = @@ -277,10 +275,10 @@ let loop : T.type_expression -> T.type_expression -> (constraints * T.type_varia let expr' = type_expression_to_type_value expr in let body' = type_expression_to_type_value body in let whole_expr = Core.fresh_type_variable () in - O.[ - C_equation (expr' , P_constant (C_bool , [])) ; - C_equation (body' , P_constant (C_unit , [])) ; - C_equation (P_variable whole_expr , P_constant (C_unit , [])) + [ + c_equation expr' (P_variable (Stage_common.Constant.t_bool)) ; + c_equation body' (p_constant C_unit []) ; + c_equation (P_variable whole_expr) (p_constant C_unit []) ] , whole_expr let let_in : T.type_expression -> T.type_expression option -> T.type_expression -> (constraints * T.type_variable) = @@ -289,18 +287,18 @@ let let_in : T.type_expression -> T.type_expression option -> T.type_expression let result' = type_expression_to_type_value result in let rhs_tv_opt' = match rhs_tv_opt with None -> [] - | Some annot -> O.[C_equation (rhs' , type_expression_to_type_value annot)] in + | Some annot -> [c_equation rhs' (type_expression_to_type_value annot)] in let whole_expr = Core.fresh_type_variable () in - O.[ - C_equation (result' , P_variable whole_expr) + [ + c_equation result' (P_variable whole_expr) ; ] @ rhs_tv_opt', whole_expr let recursive : T.type_expression -> (constraints * T.type_variable) = fun fun_type -> let fun_type = type_expression_to_type_value fun_type in let whole_expr = Core.fresh_type_variable () in - O.[ - C_equation (fun_type, P_variable whole_expr) + [ + c_equation fun_type (P_variable whole_expr) ; ], whole_expr let assign : T.type_expression -> T.type_expression -> (constraints * T.type_variable) = @@ -308,9 +306,9 @@ let assign : T.type_expression -> T.type_expression -> (constraints * T.type_var let v' = type_expression_to_type_value v in let e' = type_expression_to_type_value e in let whole_expr = Core.fresh_type_variable () in - O.[ - C_equation (v' , e') ; - C_equation (P_variable whole_expr , P_constant (C_unit , [])) + [ + c_equation v' e' ; + c_equation (P_variable whole_expr) (p_constant C_unit []) ; ] , whole_expr let annotation : T.type_expression -> T.type_expression -> (constraints * T.type_variable) = @@ -318,16 +316,16 @@ let annotation : T.type_expression -> T.type_expression -> (constraints * T.type let e' = type_expression_to_type_value e in let annot' = type_expression_to_type_value annot in let whole_expr = Core.fresh_type_variable () in - O.[ - C_equation (e' , annot') ; - C_equation (e' , P_variable whole_expr) + [ + c_equation e' annot' ; + c_equation e' (P_variable whole_expr) ; ] , whole_expr let matching : T.type_expression list -> (constraints * T.type_variable) = fun es -> let whole_expr = Core.fresh_type_variable () in let type_expressions = (List.map type_expression_to_type_value es) in - let cs = List.map (fun e -> O.C_equation (P_variable whole_expr , e)) type_expressions + let cs = List.map (fun e -> c_equation (P_variable whole_expr) e) type_expressions in cs, whole_expr let fresh_binder () = @@ -344,15 +342,15 @@ let lambda let unification_body = Core.fresh_type_variable () in let arg' = match arg with None -> [] - | Some arg -> O.[C_equation (P_variable unification_arg , type_expression_to_type_value arg)] in + | Some arg -> [c_equation (P_variable unification_arg) (type_expression_to_type_value arg)] in let body' = match body with None -> [] - | Some body -> O.[C_equation (P_variable unification_body , type_expression_to_type_value body)] - in O.[ - C_equation (type_expression_to_type_value fresh , P_variable unification_arg) ; - C_equation (P_variable whole_expr , - P_constant (C_arrow , [P_variable unification_arg ; - P_variable unification_body])) + | Some body -> [c_equation (P_variable unification_body) (type_expression_to_type_value body)] + in [ + c_equation (type_expression_to_type_value fresh) (P_variable unification_arg) ; + c_equation (P_variable whole_expr) + (p_constant C_arrow ([P_variable unification_arg ; + P_variable unification_body])) ] @ arg' @ body' , whole_expr (* This is pretty much a wrapper for an n-ary function. *) @@ -360,7 +358,7 @@ let constant : O.type_value -> T.type_expression list -> (constraints * T.type_v fun f args -> let whole_expr = Core.fresh_type_variable () in let args' = List.map type_expression_to_type_value args in - let args_tuple = O.P_constant (C_record , args') in - O.[ - C_equation (f , P_constant (C_arrow , [args_tuple ; P_variable whole_expr])) + let args_tuple = p_constant C_record args' in + [ + c_equation f (p_constant C_arrow ([args_tuple ; P_variable whole_expr])) ] , whole_expr diff --git a/src/passes/8-typer-old/dune b/src/passes/8-typer-old/dune index faec4e901..224914e78 100644 --- a/src/passes/8-typer-old/dune +++ b/src/passes/8-typer-old/dune @@ -8,6 +8,7 @@ ast_typed typer_new operators + environment ) (preprocess (pps ppx_let) diff --git a/src/passes/8-typer-old/typer.ml b/src/passes/8-typer-old/typer.ml index 7d2a70d8e..67385c1d5 100644 --- a/src/passes/8-typer-old/typer.ml +++ b/src/passes/8-typer-old/typer.ml @@ -4,6 +4,7 @@ module I = Ast_core module O = Ast_typed open O.Combinators +module DEnv = Environment module Environment = O.Environment module Solver = Typer_new.Solver @@ -226,7 +227,6 @@ let convert_type_constant : I.type_constant -> O.type_constant = function | TC_nat -> TC_nat | TC_int -> TC_int | TC_mutez -> TC_mutez - | TC_bool -> TC_bool | TC_operation -> TC_operation | TC_address -> TC_address | TC_key -> TC_key @@ -466,7 +466,7 @@ let unconvert_constant' : O.constant' -> I.constant' = function | C_SET_DELEGATE -> C_SET_DELEGATE | C_CREATE_CONTRACT -> C_CREATE_CONTRACT -let rec type_program (p:I.program) : (O.program * Solver.state) result = +let rec type_program (p:I.program) : (O.program * O.typer_state) result = let aux (e, acc:(environment * O.declaration Location.wrap list)) (d:I.declaration Location.wrap) = let%bind ed' = (bind_map_location (type_declaration e (Solver.placeholder_for_state_of_new_typer ()))) d in let loc : 'a . 'a Location.wrap -> _ -> _ = fun x v -> Location.wrap ~loc:x.location v in @@ -477,10 +477,10 @@ let rec type_program (p:I.program) : (O.program * Solver.state) result = in let%bind (_, lst) = trace (fun () -> program_error p ()) @@ - bind_fold_list aux (Environment.full_empty, []) p in + bind_fold_list aux (DEnv.default, []) p in ok @@ (List.rev lst , (Solver.placeholder_for_state_of_new_typer ())) -and type_declaration env (_placeholder_for_state_of_new_typer : Solver.state) : I.declaration -> (environment * Solver.state * O.declaration option) result = function +and type_declaration env (_placeholder_for_state_of_new_typer : O.typer_state) : I.declaration -> (environment * O.typer_state * O.declaration option) result = function | Declaration_type (type_name , type_expression) -> let%bind tv = evaluate_type env type_expression in let env' = Environment.add_type (type_name) tv env in @@ -496,13 +496,6 @@ and type_declaration env (_placeholder_for_state_of_new_typer : Solver.state) : and type_match : (environment -> I.expression -> O.expression result) -> environment -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> O.matching_expr result = fun f e t i ae loc -> match i with - | Match_bool {match_true ; match_false} -> - let%bind _ = - trace_strong (match_error ~expected:i ~actual:t loc) - @@ get_t_bool t in - let%bind match_true = f e match_true in - let%bind match_false = f e match_false in - ok (O.Match_bool {match_true ; match_false}) | Match_option {match_none ; match_some} -> let%bind tv = trace_strong (match_error ~expected:i ~actual:t loc) @@ -649,17 +642,13 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu let%bind k = evaluate_type e k in let%bind v = evaluate_type e v in ok @@ O.TC_map_or_big_map {k;v} - | TC_arrow ( arg , ret ) -> - let%bind arg' = evaluate_type e arg in - let%bind ret' = evaluate_type e ret in - ok @@ O.TC_arrow { type1=arg' ; type2=ret' } | TC_contract c -> let%bind c = evaluate_type e c in ok @@ O.TC_contract c in return (T_operator (opt)) -and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.state) result +and type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result = fun e _placeholder_for_state_of_new_typer ?tv_opt ae -> let%bind res = type_expression' e ?tv_opt ae in ok (res, (Solver.placeholder_for_state_of_new_typer ())) @@ -689,8 +678,6 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression trace_option (unbound_variable e name ae.location) @@ Environment.get_opt name e in return (E_variable name) tv'.type_value - | E_literal (Literal_bool b) -> - return (E_literal (Literal_bool b)) (t_bool ()) | E_literal Literal_unit -> return (E_literal (Literal_unit)) (t_unit ()) | E_literal Literal_void -> return (E_literal (Literal_void)) (t_unit ()) (* TODO : IS this really a t_unit ?*) @@ -917,7 +904,6 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression let tvs = let aux (cur:O.matching_expr) = match cur with - | Match_bool { match_true ; match_false } -> [ match_true ; match_false ] | Match_list { match_nil ; match_cons = {hd=_ ; tl=_ ; body ; tv=_} } -> [ match_nil ; body ] | Match_option { match_none ; match_some = {opt=_ ; body ; tv=_ } } -> [ match_none ; body ] | Match_tuple {vars=_;body;tvs=_} -> [ body ] @@ -1015,7 +1001,6 @@ let untype_literal (l:O.literal) : I.literal result = match l with | Literal_unit -> ok Literal_unit | Literal_void -> ok Literal_void - | Literal_bool b -> ok (Literal_bool b) | Literal_nat n -> ok (Literal_nat n) | Literal_timestamp n -> ok (Literal_timestamp n) | Literal_mutez n -> ok (Literal_mutez n) @@ -1088,10 +1073,6 @@ let rec untype_expression (e:O.expression) : (I.expression) result = and untype_matching : (O.expression -> I.expression result) -> O.matching_expr -> I.matching_expr result = fun f m -> let open I in match m with - | Match_bool {match_true ; match_false} -> - let%bind match_true = f match_true in - let%bind match_false = f match_false in - ok @@ Match_bool {match_true ; match_false} | Match_tuple {vars; body;tvs=_} -> let%bind b = f body in ok @@ I.Match_tuple ((vars, b),[]) diff --git a/src/passes/8-typer-old/typer.mli b/src/passes/8-typer-old/typer.mli index d1bf21393..ff7009a8c 100644 --- a/src/passes/8-typer-old/typer.mli +++ b/src/passes/8-typer-old/typer.mli @@ -38,11 +38,11 @@ module Errors : sig *) end -val type_program : I.program -> (O.program * Solver.state) result -val type_declaration : environment -> Solver.state -> I.declaration -> (environment * Solver.state * O.declaration option) result +val type_program : I.program -> (O.program * O.typer_state) result +val type_declaration : environment -> O.typer_state -> I.declaration -> (environment * O.typer_state * O.declaration option) result (* val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result *) val evaluate_type : environment -> I.type_expression -> O.type_expression result -val type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.state) result +val type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result val type_constant : I.constant' -> O.type_expression list -> O.type_expression option -> (O.constant' * O.type_expression) result (* val untype_type_value : O.type_value -> (I.type_expression) result diff --git a/src/passes/8-typer/typer.mli b/src/passes/8-typer/typer.mli index bf4c11f4d..8069ab943 100644 --- a/src/passes/8-typer/typer.mli +++ b/src/passes/8-typer/typer.mli @@ -11,6 +11,6 @@ module Solver = Typer_new.Solver type environment = Environment.t -val type_program : I.program -> (O.program * Solver.state) result -val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.state) result +val type_program : I.program -> (O.program * O.typer_state) result +val type_expression_subst : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result val untype_expression : O.expression -> I.expression result diff --git a/src/passes/9-self_ast_typed/helpers.ml b/src/passes/9-self_ast_typed/helpers.ml index c487ece1b..f42d1ea37 100644 --- a/src/passes/9-self_ast_typed/helpers.ml +++ b/src/passes/9-self_ast_typed/helpers.ml @@ -53,11 +53,6 @@ let rec fold_expression : 'a . 'a folder -> 'a -> expression -> 'a result = fun and fold_cases : 'a . 'a folder -> 'a -> matching_expr -> 'a result = fun f init m -> match m with - | Match_bool { match_true ; match_false } -> ( - let%bind res = fold_expression f init match_true in - let%bind res = fold_expression f res match_false in - ok res - ) | Match_list { match_nil ; match_cons = {hd=_; tl=_ ; body; tv=_} } -> ( let%bind res = fold_expression f init match_nil in let%bind res = fold_expression f res body in @@ -135,11 +130,6 @@ let rec map_expression : mapper -> expression -> expression result = fun f e -> and map_cases : mapper -> matching_expr -> matching_expr result = fun f m -> match m with - | Match_bool { match_true ; match_false } -> ( - let%bind match_true = map_expression f match_true in - let%bind match_false = map_expression f match_false in - ok @@ Match_bool { match_true ; match_false } - ) | Match_list { match_nil ; match_cons = {hd ; tl ; body ; tv} } -> ( let%bind match_nil = map_expression f match_nil in let%bind body = map_expression f body in @@ -230,11 +220,6 @@ let rec fold_map_expression : 'a . 'a fold_mapper -> 'a -> expression -> ('a * e and fold_map_cases : 'a . 'a fold_mapper -> 'a -> matching_expr -> ('a * matching_expr) result = fun f init m -> match m with - | Match_bool { match_true ; match_false } -> ( - let%bind (init, match_true) = fold_map_expression f init match_true in - let%bind (init, match_false) = fold_map_expression f init match_false in - ok @@ (init, Match_bool { match_true ; match_false }) - ) | Match_list { match_nil ; match_cons = { hd ; tl ; body ; tv } } -> ( let%bind (init, match_nil) = fold_map_expression f init match_nil in let%bind (init, body) = fold_map_expression f init body in diff --git a/src/passes/9-self_ast_typed/no_nested_big_map.ml b/src/passes/9-self_ast_typed/no_nested_big_map.ml index 710f1b3e4..c92034d3d 100644 --- a/src/passes/9-self_ast_typed/no_nested_big_map.ml +++ b/src/passes/9-self_ast_typed/no_nested_big_map.ml @@ -35,10 +35,6 @@ let rec check_no_nested_bigmap is_in_bigmap e = let%bind _ = check_no_nested_bigmap is_in_bigmap k in let%bind _ = check_no_nested_bigmap is_in_bigmap v in ok () - | T_operator (TC_arrow { type1 ; type2 }) -> - let%bind _ = check_no_nested_bigmap false type1 in - let%bind _ = check_no_nested_bigmap false type2 in - ok () | T_sum s -> let es = List.map (fun {ctor_type;_} -> ctor_type) (CMap.to_list s) in let%bind _ = bind_map_list (fun l -> check_no_nested_bigmap is_in_bigmap l) es in diff --git a/src/passes/9-self_ast_typed/tail_recursion.ml b/src/passes/9-self_ast_typed/tail_recursion.ml index 1d478b9df..ef4098c36 100644 --- a/src/passes/9-self_ast_typed/tail_recursion.ml +++ b/src/passes/9-self_ast_typed/tail_recursion.ml @@ -59,10 +59,6 @@ let rec check_recursive_call : expression_variable -> bool -> expression -> unit and check_recursive_call_in_matching = fun n final_path c -> match c with - | Match_bool {match_true;match_false} -> - let%bind _ = check_recursive_call n final_path match_true in - let%bind _ = check_recursive_call n final_path match_false in - ok () | Match_list {match_nil;match_cons={hd=_;tl=_;body;tv=_}} -> let%bind _ = check_recursive_call n final_path match_nil in let%bind _ = check_recursive_call n final_path body in diff --git a/src/passes/operators/operators.ml b/src/passes/operators/operators.ml index 670f45c42..e2ff180ba 100644 --- a/src/passes/operators/operators.ml +++ b/src/passes/operators/operators.ml @@ -43,7 +43,6 @@ module Concrete_to_imperative = struct | "nat" -> Some TC_nat | "int" -> Some TC_int | "tez" -> Some TC_mutez - | "bool" -> Some TC_bool | "operation" -> Some TC_operation | "address" -> Some TC_address | "key" -> Some TC_key diff --git a/src/stages/1-ast_imperative/PP.ml b/src/stages/1-ast_imperative/PP.ml index 0b9827d4a..c17860f9f 100644 --- a/src/stages/1-ast_imperative/PP.ml +++ b/src/stages/1-ast_imperative/PP.ml @@ -55,7 +55,6 @@ and type_operator : | TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v | TC_michelson_or (l,_, r,_) -> Format.asprintf "Michelson_or (%a,%a)" f l f r | TC_michelson_pair (l,_, r,_) -> Format.asprintf "Michelson_pair (%a,%a)" f l f r - | TC_arrow (k, v) -> Format.asprintf "arrow (%a,%a)" f k f v | TC_contract te -> Format.asprintf "Contract (%a)" f te in fprintf ppf "(TO_%s)" s @@ -184,8 +183,6 @@ and matching : type a . (formatter -> a -> unit) -> formatter -> (a,unit) matchi fprintf ppf "let (%a) = %a" (list_sep_d expression_variable) lst f b | Match_variant (lst, _) -> fprintf ppf "%a" (list_sep (matching_variant_case f) (tag "@.")) lst - | Match_bool {match_true ; match_false} -> - fprintf ppf "| True -> %a @.| False -> %a" f match_true f match_false | Match_list {match_nil ; match_cons = (hd, tl, match_cons, _)} -> fprintf ppf "| Nil -> %a @.| %a :: %a -> %a" f match_nil expression_variable hd expression_variable tl f match_cons | Match_option {match_none ; match_some = (some, match_some, _)} -> @@ -197,8 +194,6 @@ and matching_type ppf m = match m with fprintf ppf "tuple" | Match_variant (lst, _) -> fprintf ppf "variant %a" (list_sep matching_variant_case_type (tag "@.")) lst - | Match_bool _ -> - fprintf ppf "boolean" | Match_list _ -> fprintf ppf "list" | Match_option _ -> diff --git a/src/stages/1-ast_imperative/combinators.ml b/src/stages/1-ast_imperative/combinators.ml index 61002aa34..be9583890 100644 --- a/src/stages/1-ast_imperative/combinators.ml +++ b/src/stages/1-ast_imperative/combinators.ml @@ -21,7 +21,7 @@ open Errors let make_t ?(loc = Location.generated) type_content = {type_content; location=loc} -let t_bool ?loc () : type_expression = make_t ?loc @@ T_constant (TC_bool) +let t_bool ?loc () : type_expression = make_t ?loc @@ T_variable (Stage_common.Constant.t_bool) let t_string ?loc () : type_expression = make_t ?loc @@ T_constant (TC_string) let t_bytes ?loc () : type_expression = make_t ?loc @@ T_constant (TC_bytes) let t_int ?loc () : type_expression = make_t ?loc @@ T_constant (TC_int) @@ -88,7 +88,6 @@ let e_nat_z ?loc n : expression = make_e ?loc @@ E_literal (Literal_nat n) let e_nat ?loc n : expression = e_nat_z ?loc @@ Z.of_int n let e_timestamp_z ?loc n : expression = make_e ?loc @@ E_literal (Literal_timestamp n) let e_timestamp ?loc n : expression = e_timestamp_z ?loc @@ Z.of_int n -let e_bool ?loc b : expression = make_e ?loc @@ E_literal (Literal_bool b) let e_string ?loc s : expression = make_e ?loc @@ E_literal (Literal_string s) let e_address ?loc s : expression = make_e ?loc @@ E_literal (Literal_address s) let e_mutez_z ?loc s : expression = make_e ?loc @@ E_literal (Literal_mutez s) @@ -148,6 +147,8 @@ let e_while ?loc condition body = make_e ?loc @@ E_while {condition; body} let e_for ?loc binder start final increment body = make_e ?loc @@ E_for {binder;start;final;increment;body} let e_for_each ?loc binder collection collection_type body = make_e ?loc @@ E_for_each {binder;collection;collection_type;body} +let e_bool ?loc b : expression = e_constructor ?loc (string_of_bool b) (e_unit ()) + let ez_match_variant (lst : ((string * string) * 'a) list) = let lst = List.map (fun ((c,n),a) -> ((Constructor c, Var.of_name n), a) ) lst in Match_variant (lst,()) diff --git a/src/stages/1-ast_imperative/misc.ml b/src/stages/1-ast_imperative/misc.ml index 884822fff..cf27a497d 100644 --- a/src/stages/1-ast_imperative/misc.ml +++ b/src/stages/1-ast_imperative/misc.ml @@ -34,9 +34,6 @@ open Errors let assert_literal_eq (a, b : literal * literal) : unit result = match (a, b) with - | Literal_bool a, Literal_bool b when a = b -> ok () - | Literal_bool _, Literal_bool _ -> fail @@ different_literals "different bools" a b - | Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b | Literal_int a, Literal_int b when a = b -> ok () | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b diff --git a/src/stages/1-ast_imperative/types.ml b/src/stages/1-ast_imperative/types.ml index 49909998e..adb4cbbf5 100644 --- a/src/stages/1-ast_imperative/types.ml +++ b/src/stages/1-ast_imperative/types.ml @@ -24,7 +24,6 @@ and type_operator = | TC_set of type_expression | TC_map of type_expression * type_expression | TC_big_map of type_expression * type_expression - | TC_arrow of type_expression * type_expression | TC_michelson_or of type_expression * michelson_prct_annotation * type_expression * michelson_prct_annotation | TC_michelson_pair of type_expression * michelson_prct_annotation * type_expression * michelson_prct_annotation diff --git a/src/stages/2-ast_sugar/PP.ml b/src/stages/2-ast_sugar/PP.ml index 22f726ff6..8d8dad34b 100644 --- a/src/stages/2-ast_sugar/PP.ml +++ b/src/stages/2-ast_sugar/PP.ml @@ -51,7 +51,6 @@ and type_operator : (formatter -> type_expression -> unit) -> formatter -> type_ | TC_set te -> Format.asprintf "set(%a)" f te | TC_map (k, v) -> Format.asprintf "Map (%a,%a)" f k f v | TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v - | TC_arrow (k, v) -> Format.asprintf "arrow (%a,%a)" f k f v | TC_contract te -> Format.asprintf "Contract (%a)" f te in fprintf ppf "(TO_%s)" s @@ -151,8 +150,6 @@ and matching : type a . (formatter -> a -> unit) -> formatter -> (a,unit) matchi fprintf ppf "let (%a) = %a" (list_sep_d expression_variable) lst f b | Match_variant (lst, _) -> fprintf ppf "%a" (list_sep (matching_variant_case f) (tag "@.")) lst - | Match_bool {match_true ; match_false} -> - fprintf ppf "| True -> %a @.| False -> %a" f match_true f match_false | Match_list {match_nil ; match_cons = (hd, tl, match_cons, _)} -> fprintf ppf "| Nil -> %a @.| %a :: %a -> %a" f match_nil expression_variable hd expression_variable tl f match_cons | Match_option {match_none ; match_some = (some, match_some, _)} -> @@ -164,8 +161,6 @@ and matching_type ppf m = match m with fprintf ppf "tuple" | Match_variant (lst, _) -> fprintf ppf "variant %a" (list_sep matching_variant_case_type (tag "@.")) lst - | Match_bool _ -> - fprintf ppf "boolean" | Match_list _ -> fprintf ppf "list" | Match_option _ -> diff --git a/src/stages/2-ast_sugar/combinators.ml b/src/stages/2-ast_sugar/combinators.ml index a02e0ba71..dc8268eb8 100644 --- a/src/stages/2-ast_sugar/combinators.ml +++ b/src/stages/2-ast_sugar/combinators.ml @@ -27,7 +27,7 @@ let tuple_to_record lst = let (_, lst ) = List.fold_left aux (0,[]) lst in lst -let t_bool ?loc () : type_expression = make_t ?loc @@ T_constant (TC_bool) +let t_bool ?loc () : type_expression = make_t ?loc @@ T_variable (Stage_common.Constant.t_bool) let t_string ?loc () : type_expression = make_t ?loc @@ T_constant (TC_string) let t_bytes ?loc () : type_expression = make_t ?loc @@ T_constant (TC_bytes) let t_int ?loc () : type_expression = make_t ?loc @@ T_constant (TC_int) @@ -90,7 +90,6 @@ let e_unit ?loc () : expression = make_e ?loc @@ E_literal (Literal_unit) let e_int ?loc n : expression = make_e ?loc @@ E_literal (Literal_int n) let e_nat ?loc n : expression = make_e ?loc @@ E_literal (Literal_nat n) let e_timestamp ?loc n : expression = make_e ?loc @@ E_literal (Literal_timestamp n) -let e_bool ?loc b : expression = make_e ?loc @@ E_literal (Literal_bool b) let e_string ?loc s : expression = make_e ?loc @@ E_literal (Literal_string s) let e_address ?loc s : expression = make_e ?loc @@ E_literal (Literal_address s) let e_mutez ?loc s : expression = make_e ?loc @@ E_literal (Literal_mutez s) @@ -142,6 +141,8 @@ let e_map ?loc lst : expression = make_e ?loc @@ E_map lst let e_big_map ?loc lst : expression = make_e ?loc @@ E_big_map lst let e_look_up ?loc a b : expression = make_e ?loc @@ E_look_up (a,b) +let e_bool ?loc b : expression = e_constructor ?loc (Constructor (string_of_bool b)) (e_unit ()) + let make_option_typed ?loc e t_opt = match t_opt with | None -> e diff --git a/src/stages/2-ast_sugar/misc.ml b/src/stages/2-ast_sugar/misc.ml index 508ae70d9..f65e95796 100644 --- a/src/stages/2-ast_sugar/misc.ml +++ b/src/stages/2-ast_sugar/misc.ml @@ -34,9 +34,6 @@ open Errors let assert_literal_eq (a, b : literal * literal) : unit result = match (a, b) with - | Literal_bool a, Literal_bool b when a = b -> ok () - | Literal_bool _, Literal_bool _ -> fail @@ different_literals "different bools" a b - | Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b | Literal_int a, Literal_int b when a = b -> ok () | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b diff --git a/src/stages/2-ast_sugar/types.ml b/src/stages/2-ast_sugar/types.ml index 18295b7a5..c2007d945 100644 --- a/src/stages/2-ast_sugar/types.ml +++ b/src/stages/2-ast_sugar/types.ml @@ -30,7 +30,6 @@ and type_operator = | TC_set of type_expression | TC_map of type_expression * type_expression | TC_big_map of type_expression * type_expression - | TC_arrow of type_expression * type_expression and type_expression = {type_content: type_content; location: Location.t} diff --git a/src/stages/3-ast_core/PP.ml b/src/stages/3-ast_core/PP.ml index ac760dbba..cd269dcd6 100644 --- a/src/stages/3-ast_core/PP.ml +++ b/src/stages/3-ast_core/PP.ml @@ -76,8 +76,6 @@ and matching : type a . (formatter -> a -> unit) -> formatter -> (a,unit) matchi fprintf ppf "@[| (%a) ->@;<1 2>%a@]" (list_sep_d expression_variable) lst f b | Match_variant (lst, _) -> fprintf ppf "@[%a@]" (list_sep (matching_variant_case f) (tag "@ ")) lst - | Match_bool {match_true ; match_false} -> - fprintf ppf "@[| True ->@;<1 2>%a@ | False ->@;<1 2>%a@]" f match_true f match_false | Match_list {match_nil ; match_cons = (hd, tl, match_cons, _)} -> fprintf ppf "@[| Nil ->@;<1 2>%a@ | %a :: %a ->@;<1 2>%a@]" f match_nil expression_variable hd expression_variable tl f match_cons | Match_option {match_none ; match_some = (some, match_some, _)} -> @@ -89,8 +87,6 @@ and matching_type ppf m = match m with fprintf ppf "tuple" | Match_variant (lst, _) -> fprintf ppf "variant %a" (list_sep matching_variant_case_type (tag "@.")) lst - | Match_bool _ -> - fprintf ppf "boolean" | Match_list _ -> fprintf ppf "list" | Match_option _ -> diff --git a/src/stages/3-ast_core/combinators.ml b/src/stages/3-ast_core/combinators.ml index aff739d8a..e99cac234 100644 --- a/src/stages/3-ast_core/combinators.ml +++ b/src/stages/3-ast_core/combinators.ml @@ -27,7 +27,7 @@ let tuple_to_record lst = let (_, lst ) = List.fold_left aux (0,[]) lst in lst -let t_bool ?loc () : type_expression = make_t ?loc @@ T_constant (TC_bool) +let t_bool ?loc () : type_expression = make_t ?loc @@ T_variable (Stage_common.Constant.t_bool) let t_string ?loc () : type_expression = make_t ?loc @@ T_constant (TC_string) let t_bytes ?loc () : type_expression = make_t ?loc @@ T_constant (TC_bytes) let t_int ?loc () : type_expression = make_t ?loc @@ T_constant (TC_int) @@ -87,7 +87,6 @@ let e_unit ?loc () : expression = make_e ?loc @@ E_literal (Literal_unit) let e_int ?loc n : expression = make_e ?loc @@ E_literal (Literal_int n) let e_nat ?loc n : expression = make_e ?loc @@ E_literal (Literal_nat n) let e_timestamp ?loc n : expression = make_e ?loc @@ E_literal (Literal_timestamp n) -let e_bool ?loc b : expression = make_e ?loc @@ E_literal (Literal_bool b) let e_string ?loc s : expression = make_e ?loc @@ E_literal (Literal_string s) let e_address ?loc s : expression = make_e ?loc @@ E_literal (Literal_address s) let e_mutez ?loc s : expression = make_e ?loc @@ E_literal (Literal_mutez s) @@ -126,6 +125,8 @@ let e_record_update ?loc record path update = make_e ?loc @@ E_record_update {re let e_annotation ?loc anno_expr ty = make_e ?loc @@ E_ascription {anno_expr; type_annotation = ty} +let e_bool ?loc b : expression = e_constructor ?loc (string_of_bool b) (e_unit ()) + let make_option_typed ?loc e t_opt = match t_opt with | None -> e diff --git a/src/stages/3-ast_core/misc.ml b/src/stages/3-ast_core/misc.ml index ad38b9fec..dec3a8db6 100644 --- a/src/stages/3-ast_core/misc.ml +++ b/src/stages/3-ast_core/misc.ml @@ -34,9 +34,6 @@ open Errors let assert_literal_eq (a, b : literal * literal) : unit result = match (a, b) with - | Literal_bool a, Literal_bool b when a = b -> ok () - | Literal_bool _, Literal_bool _ -> fail @@ different_literals "different bools" a b - | Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b | Literal_int a, Literal_int b when a = b -> ok () | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b diff --git a/src/stages/4-ast_typed/.gitignore b/src/stages/4-ast_typed/.gitignore new file mode 100644 index 000000000..39f5407d5 --- /dev/null +++ b/src/stages/4-ast_typed/.gitignore @@ -0,0 +1,2 @@ +/generated_fold.ml + diff --git a/src/stages/4-ast_typed/PP.ml b/src/stages/4-ast_typed/PP.ml index a615096e8..08fd13a21 100644 --- a/src/stages/4-ast_typed/PP.ml +++ b/src/stages/4-ast_typed/PP.ml @@ -180,7 +180,6 @@ let literal ppf (l : literal) = match l with | Literal_unit -> fprintf ppf "unit" | Literal_void -> fprintf ppf "void" - | Literal_bool b -> fprintf ppf "%b" b | Literal_int z -> fprintf ppf "%a" Z.pp_print z | Literal_nat z -> fprintf ppf "+%a" Z.pp_print z | Literal_timestamp z -> fprintf ppf "+%a" Z.pp_print z @@ -205,7 +204,6 @@ let s = | TC_nat -> "nat" | TC_int -> "int" | TC_mutez -> "mutez" - | TC_bool -> "bool" | TC_operation -> "operation" | TC_address -> "address" | TC_key -> "key" @@ -250,7 +248,6 @@ and type_operator : | TC_map {k; v} -> Format.asprintf "Map (%a,%a)" f k f v | TC_big_map {k; v} -> Format.asprintf "Big Map (%a,%a)" f k f v | TC_map_or_big_map {k; v} -> Format.asprintf "Map Or Big Map (%a,%a)" f k f v - | TC_arrow {type1; type2} -> Format.asprintf "arrow (%a,%a)" f type1 f type2 | TC_contract te -> Format.asprintf "Contract (%a)" f te in fprintf ppf "(type_operator: %s)" s @@ -318,8 +315,6 @@ and matching : (formatter -> expression -> unit) -> _ -> matching_expr -> unit = fprintf ppf "let (%a) = %a" (list_sep_d expression_variable) vars f body | Match_variant {cases ; tv=_} -> fprintf ppf "%a" (list_sep (matching_variant_case f) (tag "@.")) cases - | Match_bool {match_true ; match_false} -> - fprintf ppf "| True -> %a @.| False -> %a" f match_true f match_false | Match_list {match_nil ; match_cons = {hd; tl; body; tv=_}} -> fprintf ppf "| Nil -> %a @.| %a :: %a -> %a" f match_nil expression_variable hd expression_variable tl f body | Match_option {match_none ; match_some = {opt; body; tv=_}} -> diff --git a/src/stages/4-ast_typed/PP_generic.ml b/src/stages/4-ast_typed/PP_generic.ml index d698c70e7..8138d70c0 100644 --- a/src/stages/4-ast_typed/PP_generic.ml +++ b/src/stages/4-ast_typed/PP_generic.ml @@ -10,11 +10,12 @@ let needs_parens = { | PolyInstance { poly =_; arguments=_; poly_continue } -> (poly_continue state) ); - type_variable = (fun _ _ _ -> false) ; + type_variable = (fun _ _ _ -> true) ; bool = (fun _ _ _ -> false) ; z = (fun _ _ _ -> false) ; string = (fun _ _ _ -> false) ; bytes = (fun _ _ _ -> false) ; + unit = (fun _ _ _ -> false) ; packed_internal_operation = (fun _ _ _ -> false) ; expression_variable = (fun _ _ _ -> false) ; constructor' = (fun _ _ _ -> false) ; @@ -28,6 +29,9 @@ let needs_parens = { list_ne = (fun _ _ _ _ -> false) ; option = (fun _visitor _continue _state o -> match o with None -> false | Some _ -> true) ; + poly_unionfind = (fun _ _ _ _ -> false) ; + poly_set = (fun _ _ _ _ -> false) ; + typeVariableMap = (fun _ _ _ _ -> false) ; } let op ppf = { @@ -36,19 +40,21 @@ let op ppf = { | RecordInstance { fields } -> let aux ppf (fld : 'x Adt_info.ctor_or_field_instance) = fprintf ppf "%s = %a" fld.cf.name (fun _ppf -> fld.cf_continue) () in - fprintf ppf "{ %a }" (list_sep aux (fun ppf () -> fprintf ppf " ; ")) fields + fprintf ppf "{@,@[ %a @]@,}" (list_sep aux (fun ppf () -> fprintf ppf " ;@ ")) fields | VariantInstance { constructor ; _ } -> if constructor.cf_new_fold needs_parens false then fprintf ppf "%s (%a)" constructor.cf.name (fun _ppf -> constructor.cf_continue) () - else fprintf ppf "%s %a" constructor.cf.name (fun _ppf -> constructor.cf_continue) () + else let spc = if String.equal constructor.cf.type_ "" then "" else " " in + fprintf ppf "%s%s%a" constructor.cf.name spc (fun _ppf -> constructor.cf_continue) () | PolyInstance { poly=_; arguments=_; poly_continue } -> (poly_continue ()) ); - type_variable = (fun _visitor () type_variable -> fprintf ppf "%a" Var.pp type_variable) ; + type_variable = (fun _visitor () type_variable -> fprintf ppf "Var %a" Var.pp type_variable) ; bool = (fun _visitor () b -> fprintf ppf "%s" (if b then "true" else "false")) ; z = (fun _visitor () i -> fprintf ppf "%a" Z.pp_print i) ; string = (fun _visitor () str -> fprintf ppf "\"%s\"" str) ; bytes = (fun _visitor () _bytes -> fprintf ppf "bytes...") ; + unit = (fun _visitor () () -> fprintf ppf "()") ; packed_internal_operation = (fun _visitor () _op -> fprintf ppf "Operation(...bytes)") ; expression_variable = (fun _visitor () ev -> fprintf ppf "%a" Var.pp ev) ; constructor' = (fun _visitor () (Constructor c) -> fprintf ppf "Constructor %s" c) ; @@ -59,31 +65,49 @@ let op ppf = { let lst = List.sort (fun (Constructor a, _) (Constructor b, _) -> String.compare a b) (CMap.bindings cmap) in let aux ppf (Constructor k, v) = fprintf ppf "(Constructor %s, %a)" k (fun _ppf -> continue ()) v in - fprintf ppf "CMap [ %a ]" (list_sep aux (fun ppf () -> fprintf ppf " ; ")) lst); + fprintf ppf "CMap [@,@[ %a @]@,]" (list_sep aux (fun ppf () -> fprintf ppf " ; ")) lst); label_map = (fun _visitor continue () lmap -> let lst = List.sort (fun (Label a, _) (Label b, _) -> String.compare a b) (LMap.bindings lmap) in let aux ppf (Label k, v) = fprintf ppf "(Constructor %s, %a)" k (fun _ppf -> continue ()) v in - fprintf ppf "LMap [ %a ]" (list_sep aux (fun ppf () -> fprintf ppf " ; ")) lst); + fprintf ppf "LMap [@,@[ %a @]@,]" (list_sep aux (fun ppf () -> fprintf ppf " ; ")) lst); list = (fun _visitor continue () lst -> let aux ppf elt = fprintf ppf "%a" (fun _ppf -> continue ()) elt in - fprintf ppf "[ %a ]" (list_sep aux (fun ppf () -> fprintf ppf " ; ")) lst); + fprintf ppf "[@,@[ %a @]@,]" (list_sep aux (fun ppf () -> fprintf ppf " ;@ ")) lst); location_wrap = (fun _visitor continue () lwrap -> let ({ wrap_content; location } : _ Location.wrap) = lwrap in fprintf ppf "{ wrap_content = %a ; location = %a }" (fun _ppf -> continue ()) wrap_content Location.pp location); list_ne = (fun _visitor continue () (first, lst) -> let aux ppf elt = fprintf ppf "%a" (fun _ppf -> continue ()) elt in - fprintf ppf "[ %a ]" (list_sep aux (fun ppf () -> fprintf ppf " ; ")) (first::lst)); + fprintf ppf "[@,@[ %a @]@,]" (list_sep aux (fun ppf () -> fprintf ppf " ;@ ")) (first::lst)); option = (fun _visitor continue () o -> match o with | None -> fprintf ppf "None" | Some v -> fprintf ppf "%a" (fun _ppf -> continue ()) v) ; + poly_unionfind = (fun _visitor continue () p -> + let lst = (UnionFind.Poly2.partitions p) in + let aux1 l = fprintf ppf "[@,@[ (*%a*) %a @]@,]" + (fun _ppf -> continue ()) (UnionFind.Poly2.repr (List.hd l) p) + (list_sep (fun _ppf -> continue ()) (fun ppf () -> fprintf ppf " ;@ ")) l in + let aux2 = list_sep (fun _ppf -> aux1) (fun ppf () -> fprintf ppf " ;@ ") in + fprintf ppf "UnionFind [@,@[ %a @]@,]" aux2 lst); + poly_set = (fun _visitor continue () set -> + let lst = (RedBlackTrees.PolySet.elements set) in + fprintf ppf "Set [@,@[ %a @]@,]" (list_sep (fun _ppf -> continue ()) (fun ppf () -> fprintf ppf " ;@ ")) lst); + typeVariableMap = (fun _visitor continue () tvmap -> + let lst = List.sort (fun (a, _) (b, _) -> Var.compare a b) (RedBlackTrees.PolyMap.bindings tvmap) in + let aux ppf (k, v) = + fprintf ppf "(Var %a, %a)" Var.pp k (fun _ppf -> continue ()) v in + fprintf ppf "typeVariableMap [@,@[ %a @]@,]" (list_sep aux (fun ppf () -> fprintf ppf " ;@ ")) lst); } let print : (unit fold_config -> unit -> 'a -> unit) -> formatter -> 'a -> unit = fun fold ppf v -> fold (op ppf) () v -let program = print fold__program -let type_expression = print fold__type_expression +include Fold.Folds(struct + type state = unit ;; + type 'a t = formatter -> 'a -> unit ;; + let f = print ;; +end) diff --git a/src/stages/4-ast_typed/ast_typed.ml b/src/stages/4-ast_typed/ast_typed.ml index 1b80a9d04..e78dc9188 100644 --- a/src/stages/4-ast_typed/ast_typed.ml +++ b/src/stages/4-ast_typed/ast_typed.ml @@ -1,6 +1,7 @@ module Types = Types module Environment = Environment module PP = PP +module PP_generic = PP_generic module Combinators = struct include Combinators include Combinators_environment diff --git a/src/stages/4-ast_typed/combinators.ml b/src/stages/4-ast_typed/combinators.ml index 54a6e6b22..13532e414 100644 --- a/src/stages/4-ast_typed/combinators.ml +++ b/src/stages/4-ast_typed/combinators.ml @@ -34,7 +34,6 @@ let make_n_t type_name type_value = { type_name ; type_value } let t_signature ?loc ?s () : type_expression = make_t ?loc (T_constant TC_signature) s let t_chain_id ?loc ?s () : type_expression = make_t ?loc (T_constant TC_chain_id) s -let t_bool ?loc ?s () : type_expression = make_t ?loc (T_constant TC_bool) s let t_string ?loc ?s () : type_expression = make_t ?loc (T_constant TC_string) s let t_bytes ?loc ?s () : type_expression = make_t ?loc (T_constant TC_bytes) s let t_key ?loc ?s () : type_expression = make_t ?loc (T_constant TC_key) s @@ -67,10 +66,13 @@ let t_big_map ?loc k v ?s () = make_t ?loc (T_operator (TC_big_map { k ; v })) s let t_map_or_big_map ?loc k v ?s () = make_t ?loc (T_operator (TC_map_or_big_map { k ; v })) s let t_sum m ?loc ?s () : type_expression = make_t ?loc (T_sum m) s -let make_t_ez_sum ?loc (lst:(constructor' * ctor_content) list) : type_expression = +let make_t_ez_sum ?loc ?s (lst:(constructor' * ctor_content) list) : type_expression = let aux prev (k, v) = CMap.add k v prev in let map = List.fold_left aux CMap.empty lst in - make_t ?loc (T_sum map) None + make_t ?loc (T_sum map) s + +let t_bool ?loc ?s () : type_expression = make_t_ez_sum ?loc ?s + [(Constructor "true", {ctor_type=t_unit ();michelson_annotation=None});(Constructor "false", {ctor_type=t_unit ();michelson_annotation=None})] let t_function param result ?loc ?s () : type_expression = make_t ?loc (T_arrow {type1=param; type2=result}) s let t_shallow_closure param result ?loc ?s () : type_expression = make_t ?loc (T_arrow {type1=param; type2=result}) s @@ -90,7 +92,8 @@ let get_lambda_with_type e = | _ -> simple_fail "not a lambda with functional type" let get_t_bool (t:type_expression) : unit result = match t.type_content with - | T_constant (TC_bool) -> ok () + | T_variable v when Var.equal v Stage_common.Constant.t_bool -> ok () + | t when (compare t (t_bool ()).type_content) = 0-> ok () | _ -> fail @@ Errors.not_a_x_type "bool" t () let get_t_int (t:type_expression) : unit result = match t.type_content with @@ -286,7 +289,6 @@ let e_unit () : expression_content = E_literal (Literal_unit) let e_int n : expression_content = E_literal (Literal_int n) let e_nat n : expression_content = E_literal (Literal_nat n) let e_mutez n : expression_content = E_literal (Literal_mutez n) -let e_bool b : expression_content = E_literal (Literal_bool b) let e_string s : expression_content = E_literal (Literal_string s) let e_bytes s : expression_content = E_literal (Literal_bytes s) let e_timestamp s : expression_content = E_literal (Literal_timestamp s) @@ -302,11 +304,15 @@ let e_application lamb args : expression_content = E_application {lamb;args} let e_variable v : expression_content = E_variable v let e_let_in let_binder inline rhs let_result = E_let_in { let_binder ; rhs ; let_result; inline } +let e_constructor constructor element: expression_content = E_constructor {constructor;element} + +let e_bool b env : expression_content = e_constructor (Constructor (string_of_bool b)) (make_e (e_unit ())(t_unit()) env) + let e_a_unit = make_e (e_unit ()) (t_unit ()) let e_a_int n = make_e (e_int n) (t_int ()) let e_a_nat n = make_e (e_nat n) (t_nat ()) let e_a_mutez n = make_e (e_mutez n) (t_mutez ()) -let e_a_bool b = make_e (e_bool b) (t_bool ()) +let e_a_bool b = fun env -> make_e (e_bool b env) (t_bool ()) env let e_a_string s = make_e (e_string s) (t_string ()) let e_a_address s = make_e (e_address s) (t_address ()) let e_a_pair a b = make_e (e_pair a b) @@ -326,6 +332,7 @@ let ez_e_a_record r = make_e (ez_e_record r) (ez_t_record (List.map (fun (x, y) let e_a_let_in binder expr body attributes = make_e (e_let_in binder expr body attributes) (get_type_expression body) + let get_a_int (t:expression) = match t.expression_content with | E_literal (Literal_int n) -> ok n @@ -338,7 +345,7 @@ let get_a_unit (t:expression) = let get_a_bool (t:expression) = match t.expression_content with - | E_literal (Literal_bool b) -> ok b + | E_constructor {constructor=Constructor name;element} when (String.equal name "true" || String.equal name "false") && element.expression_content = e_unit () -> ok (bool_of_string name) | _ -> simple_fail "not a bool" diff --git a/src/stages/4-ast_typed/combinators.mli b/src/stages/4-ast_typed/combinators.mli index 6d842c16c..a80fad951 100644 --- a/src/stages/4-ast_typed/combinators.mli +++ b/src/stages/4-ast_typed/combinators.mli @@ -33,7 +33,7 @@ val t_map : ?loc:Location.t -> type_expression -> type_expression -> ?s:S.type_e val t_big_map : ?loc:Location.t -> type_expression -> type_expression -> ?s:S.type_expression -> unit -> type_expression val t_map_or_big_map : ?loc:Location.t -> type_expression -> type_expression -> ?s:S.type_expression -> unit -> type_expression val t_sum : Types.te_cmap -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression -val make_t_ez_sum : ?loc:Location.t -> ( constructor' * ctor_content ) list -> type_expression +val make_t_ez_sum : ?loc:Location.t -> ?s:S.type_expression -> ( constructor' * ctor_content ) list -> type_expression val t_function : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression val t_shallow_closure : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression val get_type_expression : expression -> type_expression @@ -114,7 +114,7 @@ val e_unit : unit -> expression_content val e_int : Z.t -> expression_content val e_nat : Z.t -> expression_content val e_mutez : Z.t -> expression_content -val e_bool : bool -> expression_content +val e_bool : bool -> full_environment -> expression_content val e_string : string -> expression_content val e_bytes : bytes -> expression_content val e_timestamp : Z.t -> expression_content diff --git a/src/stages/4-ast_typed/dune b/src/stages/4-ast_typed/dune index 7a16fdd2a..370845a60 100644 --- a/src/stages/4-ast_typed/dune +++ b/src/stages/4-ast_typed/dune @@ -14,6 +14,7 @@ ast_core ; Is that a good idea? stage_common adt_generator + UnionFind ) (preprocess (pps ppx_let bisect_ppx --conditional) diff --git a/src/stages/4-ast_typed/helpers.ml b/src/stages/4-ast_typed/helpers.ml index 81d634bb6..7bcc4a934 100644 --- a/src/stages/4-ast_typed/helpers.ml +++ b/src/stages/4-ast_typed/helpers.ml @@ -9,7 +9,6 @@ let map_type_operator f = function | TC_map {k ; v} -> TC_map { k = f k ; v = f v } | TC_big_map {k ; v}-> TC_big_map { k = f k ; v = f v } | TC_map_or_big_map { k ; v }-> TC_map_or_big_map { k = f k ; v = f v } - | TC_arrow {type1 ; type2} -> TC_arrow { type1 = f type1 ; type2 = f type2 } let bind_map_type_operator f = function TC_contract x -> let%bind x = f x in ok @@ TC_contract x @@ -19,7 +18,6 @@ let bind_map_type_operator f = function | TC_map {k ; v} -> let%bind k = f k in let%bind v = f v in ok @@ TC_map {k ; v} | TC_big_map {k ; v} -> let%bind k = f k in let%bind v = f v in ok @@ TC_big_map {k ; v} | TC_map_or_big_map {k ; v} -> let%bind k = f k in let%bind v = f v in ok @@ TC_map_or_big_map {k ; v} - | TC_arrow {type1 ; type2}-> let%bind type1 = f type1 in let%bind type2 = f type2 in ok @@ TC_arrow {type1 ; type2} let type_operator_name = function TC_contract _ -> "TC_contract" @@ -29,7 +27,6 @@ let type_operator_name = function | TC_map _ -> "TC_map" | TC_big_map _ -> "TC_big_map" | TC_map_or_big_map _ -> "TC_map_or_big_map" - | TC_arrow _ -> "TC_arrow" let type_expression'_of_string = function | "TC_contract" , [x] -> ok @@ T_operator(TC_contract x) @@ -47,7 +44,6 @@ let type_expression'_of_string = function | "TC_nat" , [] -> ok @@ T_constant(TC_nat) | "TC_int" , [] -> ok @@ T_constant(TC_int) | "TC_mutez" , [] -> ok @@ T_constant(TC_mutez) - | "TC_bool" , [] -> ok @@ T_constant(TC_bool) | "TC_operation" , [] -> ok @@ T_constant(TC_operation) | "TC_address" , [] -> ok @@ T_constant(TC_address) | "TC_key" , [] -> ok @@ T_constant(TC_key) @@ -68,7 +64,6 @@ let string_of_type_operator = function | TC_map { k ; v } -> "TC_map" , [k ; v] | TC_big_map { k ; v } -> "TC_big_map" , [k ; v] | TC_map_or_big_map { k ; v } -> "TC_map_or_big_map" , [k ; v] - | TC_arrow { type1 ; type2 } -> "TC_arrow" , [type1 ; type2] let string_of_type_constant = function | TC_unit -> "TC_unit", [] @@ -77,7 +72,6 @@ let string_of_type_constant = function | TC_nat -> "TC_nat", [] | TC_int -> "TC_int", [] | TC_mutez -> "TC_mutez", [] - | TC_bool -> "TC_bool", [] | TC_operation -> "TC_operation", [] | TC_address -> "TC_address", [] | TC_key -> "TC_key", [] diff --git a/src/stages/4-ast_typed/misc.ml b/src/stages/4-ast_typed/misc.ml index 95c1b9289..2075d2ac1 100644 --- a/src/stages/4-ast_typed/misc.ml +++ b/src/stages/4-ast_typed/misc.ml @@ -234,7 +234,6 @@ module Free_variables = struct and matching : (bindings -> expression -> bindings) -> bindings -> matching_expr -> bindings = fun f b m -> match m with - | Match_bool { match_true = t ; match_false = fa } -> union (f b t) (f b fa) | Match_list { match_nil = n ; match_cons = {hd; tl; body; tv=_} } -> union (f b n) (f (union (of_list [hd ; tl]) b) body) | Match_option { match_none = n ; match_some = {opt; body; tv=_} } -> union (f b n) (f (union (singleton opt) b) body) | Match_tuple { vars ; body ; tvs=_ } -> @@ -342,8 +341,8 @@ let rec assert_type_expression_eq (a, b: (type_expression * type_expression)) : | (TC_map {k=ka;v=va} | TC_map_or_big_map {k=ka;v=va}), (TC_map {k=kb;v=vb} | TC_map_or_big_map {k=kb;v=vb}) | (TC_big_map {k=ka;v=va} | TC_map_or_big_map {k=ka;v=va}), (TC_big_map {k=kb;v=vb} | TC_map_or_big_map {k=kb;v=vb}) -> ok @@ ([ka;va] ,[kb;vb]) - | (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ | TC_arrow _ ), - (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ | TC_arrow _ ) + | (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ ), + (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ ) -> fail @@ different_operators opa opb in if List.length lsta <> List.length lstb then @@ -407,9 +406,6 @@ let type_expression_eq ab = Trace.to_bool @@ assert_type_expression_eq ab let assert_literal_eq (a, b : literal * literal) : unit result = match (a, b) with - | Literal_bool a, Literal_bool b when a = b -> ok () - | Literal_bool _, Literal_bool _ -> fail @@ different_literals "booleans" a b - | Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b | Literal_int a, Literal_int b when a = b -> ok () | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b @@ -529,6 +525,14 @@ let program_environment (program : program) : full_environment = | Declaration_constant { binder=_ ; expr=_ ; inline=_ ; post_env } -> post_env let equal_variables a b : bool = - match a.expression_content, b.expression_content with + match a.expression_content, b.expression_content with | E_variable a, E_variable b -> Var.equal a b | _, _ -> false + +let p_constant (p_ctor_tag : constant_tag) (p_ctor_args : p_ctor_args) = + P_constant { + p_ctor_tag : constant_tag ; + p_ctor_args : p_ctor_args ; + } + +let c_equation aval bval = C_equation { aval ; bval } diff --git a/src/stages/4-ast_typed/misc.mli b/src/stages/4-ast_typed/misc.mli index 924702ce8..fae2a1a36 100644 --- a/src/stages/4-ast_typed/misc.mli +++ b/src/stages/4-ast_typed/misc.mli @@ -71,3 +71,6 @@ val assert_literal_eq : ( literal * literal ) -> unit result val get_entry : program -> string -> expression result val program_environment : program -> full_environment + +val p_constant : constant_tag -> p_ctor_args -> type_value +val c_equation : type_value -> type_value -> type_constraint diff --git a/src/stages/4-ast_typed/misc_smart.ml b/src/stages/4-ast_typed/misc_smart.ml index 6b643d742..679789804 100644 --- a/src/stages/4-ast_typed/misc_smart.ml +++ b/src/stages/4-ast_typed/misc_smart.ml @@ -91,10 +91,6 @@ module Captured_variables = struct and matching : (bindings -> expression -> bindings result) -> bindings -> matching_expr -> bindings result = fun f b m -> match m with - | Match_bool { match_true = t ; match_false = fa } -> - let%bind t' = f b t in - let%bind fa' = f b fa in - ok @@ union t' fa' | Match_list { match_nil = n ; match_cons = {hd; tl; body; tv=_} } -> let%bind n' = f b n in let%bind c' = f (union (of_list [hd ; tl]) b) body in diff --git a/src/stages/4-ast_typed/types.ml b/src/stages/4-ast_typed/types.ml index cbf9bbd1b..4b0882119 100644 --- a/src/stages/4-ast_typed/types.ml +++ b/src/stages/4-ast_typed/types.ml @@ -9,7 +9,6 @@ type type_constant = | TC_nat | TC_int | TC_mutez - | TC_bool | TC_operation | TC_address | TC_key @@ -66,8 +65,6 @@ and type_operator = | TC_map of type_map_args | TC_big_map of type_map_args | TC_map_or_big_map of type_map_args - | TC_arrow of arrow - and type_expression = { type_content: type_content; @@ -77,7 +74,6 @@ and type_expression = { type literal = | Literal_unit - | Literal_bool of bool | Literal_int of z | Literal_nat of z | Literal_timestamp of z @@ -92,10 +88,6 @@ type literal = | Literal_void | Literal_operation of packed_internal_operation -type matching_content_bool = { - match_true : expression ; - match_false : expression ; - } and matching_content_cons = { hd : expression_variable; @@ -143,7 +135,6 @@ and matching_content_variant = { } and matching_expr = - | Match_bool of matching_content_bool | Match_list of matching_content_list | Match_option of matching_content_option | Match_tuple of matching_content_tuple @@ -425,3 +416,190 @@ and named_type_content = { type_name : type_variable; type_value : type_expression; } + + + + + +(* Solver types *) + +(* typevariable: to_string = (fun s -> Format.asprintf "%a" Var.pp s) *) +type unionfind = type_variable poly_unionfind + +(* core *) + +(* add information on the type or the kind for operator *) +type constant_tag = + | C_arrow (* * -> * -> * isn't this wrong? *) + | C_option (* * -> * *) + | C_record (* ( label , * ) … -> * *) + | C_variant (* ( label , * ) … -> * *) + | C_map (* * -> * -> * *) + | C_big_map (* * -> * -> * *) + | C_list (* * -> * *) + | C_set (* * -> * *) + | C_unit (* * *) + | C_string (* * *) + | C_nat (* * *) + | C_mutez (* * *) + | C_timestamp (* * *) + | C_int (* * *) + | C_address (* * *) + | C_bytes (* * *) + | C_key_hash (* * *) + | C_key (* * *) + | C_signature (* * *) + | C_operation (* * *) + | C_contract (* * -> * *) + | C_chain_id (* * *) + +(* TODO: rename to type_expression or something similar (it includes variables, and unevaluated functions + applications *) +type type_value = + | P_forall of p_forall + | P_variable of type_variable + | P_constant of p_constant + | P_apply of p_apply + +and p_apply = { + tf : type_value ; + targ : type_value ; +} +and p_ctor_args = type_value list +and p_constant = { + p_ctor_tag : constant_tag ; + p_ctor_args : p_ctor_args ; + } +and p_constraints = type_constraint list +and p_forall = { + binder : type_variable ; + constraints : p_constraints ; + body : type_value ; +} + +(* Different type of constraint *) +and ctor_args = type_variable list (* non-empty list *) +and simple_c_constructor = { + ctor_tag : constant_tag ; + ctor_args : ctor_args ; + } +and simple_c_constant = { + constant_tag: constant_tag ; (* for type constructors that do not take arguments *) + } +and c_const = { + c_const_tvar : type_variable ; + c_const_tval : type_value ; + } +and c_equation = { + aval : type_value ; + bval : type_value ; +} +and tc_args = type_value list +and c_typeclass = { + tc_args : tc_args ; + typeclass : typeclass ; +} +and c_access_label = { + c_access_label_tval : type_value ; + accessor : label ; + c_access_label_tvar : type_variable ; + } + +(*What i was saying just before *) +and type_constraint = + (* | C_assignment of (type_variable * type_pattern) *) + | C_equation of c_equation (* TVA = TVB *) + | C_typeclass of c_typeclass (* TVL ∈ TVLs, for now in extension, later add intensional (rule-based system for inclusion in the typeclass) *) + | C_access_label of c_access_label (* poor man's type-level computation to ensure that TV.label is type_variable *) +(* | … *) + +(* is the first list in case on of the type of the type class as a kind *->*->* ? *) +and tc_allowed = type_value list +and typeclass = tc_allowed list + +(* end core *) + +type c_constructor_simpl_typeVariableMap = c_constructor_simpl typeVariableMap +and constraints_typeVariableMap = constraints typeVariableMap +and type_constraint_simpl_list = type_constraint_simpl list +and structured_dbs = { + all_constraints : type_constraint_simpl_list ; + aliases : unionfind ; + (* assignments (passive data structure). *) + (* Now : just a map from unification vars to types (pb: what about partial types?) *) + (* maybe just local assignments (allow only vars as children of pair(α,β)) *) + (* TODO : the rhs of the map should not repeat the variable name. *) + assignments : c_constructor_simpl_typeVariableMap ; + grouped_by_variable : constraints_typeVariableMap ; (* map from (unionfind) variables to constraints containing them *) + cycle_detection_toposort : unit ; (* example of structured db that we'll add later *) +} + +and c_constructor_simpl_list = c_constructor_simpl list +and c_poly_simpl_list = c_poly_simpl list +and c_typeclass_simpl_list = c_typeclass_simpl list +and constraints = { + (* If implemented in a language with decent sets, these should be sets not lists. *) + constructor : c_constructor_simpl_list ; (* List of ('a = constructor(args…)) constraints *) + poly : c_poly_simpl_list ; (* List of ('a = forall 'b, some_type) constraints *) + tc : c_typeclass_simpl_list ; (* List of (typeclass(args…)) constraints *) +} +and type_variable_list = type_variable list +and c_constructor_simpl = { + tv : type_variable; + c_tag : constant_tag; + tv_list : type_variable_list; +} +and c_const_e = { + c_const_e_tv : type_variable ; + c_const_e_te : type_expression ; + } +and c_equation_e = { + aex : type_expression ; + bex : type_expression ; + } +and c_typeclass_simpl = { + tc : typeclass ; + args : type_variable_list ; +} +and c_poly_simpl = { + tv : type_variable ; + forall : p_forall ; +} +and type_constraint_simpl = + | SC_Constructor of c_constructor_simpl (* α = ctor(β, …) *) + | SC_Alias of c_alias (* α = β *) + | SC_Poly of c_poly_simpl (* α = forall β, δ where δ can be a more complex type *) + | SC_Typeclass of c_typeclass_simpl (* TC(α, …) *) + +and c_alias = { + a : type_variable ; + b : type_variable ; + } + + +(* sub-sub component: lazy selector (don't re-try all selectors every time) *) +(* For now: just re-try everytime *) + +(* selector / propagation rule for breaking down composite types *) +(* For now: break pair(a, b) = pair(c, d) into a = c, b = d *) +type output_break_ctor = { + a_k_var : c_constructor_simpl ; + a_k'_var' : c_constructor_simpl ; + } + +type output_specialize1 = { + poly : c_poly_simpl ; + a_k_var : c_constructor_simpl ; + } + +type m_break_ctor__already_selected = output_break_ctor poly_set +type m_specialize1__already_selected = output_specialize1 poly_set + +type already_selected = { + break_ctor : m_break_ctor__already_selected ; + specialize1 : m_specialize1__already_selected ; +} + +type typer_state = { + structured_dbs : structured_dbs ; + already_selected : already_selected ; +} diff --git a/src/stages/4-ast_typed/types_utils.ml b/src/stages/4-ast_typed/types_utils.ml index 34e7c5668..b9367fa0c 100644 --- a/src/stages/4-ast_typed/types_utils.ml +++ b/src/stages/4-ast_typed/types_utils.ml @@ -77,3 +77,48 @@ let fold_map__option : type a state new_a . (state -> a -> (state * new_a) resul match o with | None -> ok (state, None) | Some v -> let%bind state, v = f state v in ok (state, Some v) + + + + + +(* Solver types *) + +type 'a poly_unionfind = 'a UnionFind.Poly2.t + +(* typevariable: to_string = (fun s -> Format.asprintf "%a" Var.pp s) *) +(* representant for an equivalence class of type variables *) +type 'v typeVariableMap = (type_variable, 'v) RedBlackTrees.PolyMap.t + +type 'a poly_set = 'a RedBlackTrees.PolySet.t + +let fold_map__poly_unionfind : type a state new_a . (state -> a -> (state * new_a) result) -> state -> a poly_unionfind -> (state * new_a poly_unionfind) Simple_utils.Trace.result = + fun f state l -> + ignore (f, state, l) ; failwith "TODO + let aux acc element = + let%bind state , l = acc in + let%bind (state , new_element) = f state element in ok (state , new_element :: l) in + let%bind (state , l) = List.fold_left aux (ok (state , [])) l in + ok (state , l)" + +let fold_map__PolyMap : type k v state new_v . (state -> v -> (state * new_v) result) -> state -> (k, v) PolyMap.t -> (state * (k, new_v) PolyMap.t) result = + fun f state m -> + let aux k v ~acc = + let%bind (state , m) = acc in + let%bind (state , new_v) = f state v in + ok (state , PolyMap.add k new_v m) in + let%bind (state , m) = PolyMap.fold_inc aux m ~init:(ok (state, PolyMap.empty m)) in + ok (state , m) + +let fold_map__typeVariableMap : type a state new_a . (state -> a -> (state * new_a) result) -> state -> a typeVariableMap -> (state * new_a typeVariableMap) result = + fold_map__PolyMap + +let fold_map__poly_set : type a state new_a . (state -> a -> (state * new_a) result) -> state -> a poly_set -> (state * new_a poly_set) result = + fun f state s -> + let new_compare : (new_a -> new_a -> int) = failwith "TODO: thread enough information about the target AST so that we may compare things here." in + let aux elt ~acc = + let%bind (state , s) = acc in + let%bind (state , new_elt) = f state elt in + ok (state , PolySet.add new_elt s) in + let%bind (state , m) = PolySet.fold_inc aux s ~init:(ok (state, PolySet.create ~cmp:new_compare)) in + ok (state , m) diff --git a/src/stages/5-mini_c/PP.ml b/src/stages/5-mini_c/PP.ml index 2543fd675..96b9499a4 100644 --- a/src/stages/5-mini_c/PP.ml +++ b/src/stages/5-mini_c/PP.ml @@ -29,23 +29,23 @@ and environment_element ppf ((n, tv) : environment_element) = and environment ppf (x:environment) = fprintf ppf "Env[%a]" (list_sep_d environment_element) x -and type_constant ppf (tc:type_constant) : unit = - let s = match tc with - | TC_unit -> "unit" - | TC_string -> "string" - | TC_bytes -> "bytes" - | TC_nat -> "nat" - | TC_int -> "int" - | TC_mutez -> "mutez" - | TC_bool -> "bool" - | TC_operation -> "operation" - | TC_address -> "address" - | TC_key -> "key" - | TC_key_hash -> "key_hash" - | TC_signature -> "signature" - | TC_timestamp -> "timestamp" - | TC_chain_id -> "chain_id" - | TC_void -> "void" +and type_constant ppf (tb:type_base) : unit = + let s = match tb with + | TB_unit -> "unit" + | TB_string -> "string" + | TB_bytes -> "bytes" + | TB_nat -> "nat" + | TB_int -> "int" + | TB_mutez -> "mutez" + | TB_bool -> "bool" + | TB_operation -> "operation" + | TB_address -> "address" + | TB_key -> "key" + | TB_key_hash -> "key_hash" + | TB_signature -> "signature" + | TB_timestamp -> "timestamp" + | TB_chain_id -> "chain_id" + | TB_void -> "void" in fprintf ppf "(TC %s)" s @@ -255,7 +255,7 @@ let%expect_test _ = let%expect_test _ = let pp = expression' Format.std_formatter in - let dummy_type = T_base TC_unit in + let dummy_type = T_base TB_unit in let wrap e = { content = e ; type_value = dummy_type } in pp @@ E_closure { binder = Var.of_name "y" ; body = wrap (E_variable (Var.of_name "y")) } ; [%expect{| diff --git a/src/stages/5-mini_c/combinators.ml b/src/stages/5-mini_c/combinators.ml index 019a111be..1c255a36c 100644 --- a/src/stages/5-mini_c/combinators.ml +++ b/src/stages/5-mini_c/combinators.ml @@ -152,7 +152,7 @@ let get_t_contract t = match t with | _ -> fail @@ wrong_type "contract" t let get_t_operation t = match t with - | T_base TC_operation -> ok t + | T_base TB_operation -> ok t | _ -> fail @@ wrong_type "operation" t let get_operation (v:value) = match v with @@ -160,9 +160,9 @@ let get_operation (v:value) = match v with | _ -> simple_fail "not an operation" -let t_int : type_value = T_base TC_int -let t_unit : type_value = T_base TC_unit -let t_nat : type_value = T_base TC_nat +let t_int : type_value = T_base TB_int +let t_unit : type_value = T_base TB_unit +let t_nat : type_value = T_base TB_nat let t_function x y : type_value = T_function ( x , y ) let t_pair x y : type_value = T_pair ( x , y ) diff --git a/src/stages/5-mini_c/types.ml b/src/stages/5-mini_c/types.ml index 646c34913..ac8bfe4ae 100644 --- a/src/stages/5-mini_c/types.ml +++ b/src/stages/5-mini_c/types.ml @@ -1,4 +1,3 @@ - include Stage_common.Types type 'a annotated = string option * 'a @@ -7,7 +6,7 @@ type type_value = | T_pair of (type_value annotated * type_value annotated) | T_or of (type_value annotated * type_value annotated) | T_function of (type_value * type_value) - | T_base of type_constant + | T_base of type_base | T_map of (type_value * type_value) | T_big_map of (type_value * type_value) | T_list of type_value @@ -15,6 +14,23 @@ type type_value = | T_contract of type_value | T_option of type_value +and type_base = + | TB_unit + | TB_bool + | TB_string + | TB_bytes + | TB_nat + | TB_int + | TB_mutez + | TB_operation + | TB_address + | TB_key + | TB_key_hash + | TB_chain_id + | TB_signature + | TB_timestamp + | TB_void + and environment_element = expression_variable * type_value and environment = environment_element list diff --git a/src/stages/adt_generator/adt_generator.ml b/src/stages/adt_generator/adt_generator.ml index f96857f7b..11f617517 100644 --- a/src/stages/adt_generator/adt_generator.ml +++ b/src/stages/adt_generator/adt_generator.ml @@ -1 +1,2 @@ module Generic = Generic +module Common = Common diff --git a/src/stages/adt_generator/common.ml b/src/stages/adt_generator/common.ml new file mode 100644 index 000000000..890711eb9 --- /dev/null +++ b/src/stages/adt_generator/common.ml @@ -0,0 +1,3 @@ +type ('a,'err) monad = ('a) Simple_utils.Trace.result;; +let (>>?) v f = Simple_utils.Trace.bind f v;; +let return v = Simple_utils.Trace.ok v;; diff --git a/src/stages/adt_generator/dune b/src/stages/adt_generator/dune index 0e1a15f71..5e98e3845 100644 --- a/src/stages/adt_generator/dune +++ b/src/stages/adt_generator/dune @@ -2,5 +2,6 @@ (name adt_generator) (public_name ligo.adt_generator) (libraries + simple-utils ) ) diff --git a/src/stages/adt_generator/generator.raku b/src/stages/adt_generator/generator.raku index 85146e887..8b323c157 100644 --- a/src/stages/adt_generator/generator.raku +++ b/src/stages/adt_generator/generator.raku @@ -3,6 +3,11 @@ use v6.c; use strict; use worries; +# TODO: find a way to do mutual recursion between the produced file and some #include-y-thingy +# TODO: make an .mli +# TODO: shorthand for `foo list` etc. in field and constructor types +# TODO: error when reserved names are used ("state", … please list them here) + my $moduleName = @*ARGS[0].subst(/\.ml$/, '').samecase("A_"); my $variant = "_ _variant"; my $record = "_ _ record"; @@ -143,15 +148,13 @@ say ""; for $statements -> $statement { say "$statement" } -say "type 'a monad = 'a Simple_utils.Trace.result;;"; -say "let (>>?) v f = Simple_utils.Trace.bind f v;;"; -say "let return v = Simple_utils.Trace.ok v;;"; +say "open Adt_generator.Common;;"; say "open $moduleName;;"; say ""; say "(* must be provided by one of the open or include statements: *)"; for $adts.grep({$_ ne $record && $_ ne $variant}).map({$_}).unique -> $poly -{ say "let fold_map__$poly : type a new_a state . (state -> a -> (state * new_a) Simple_utils.Trace.result) -> state -> a $poly -> (state * new_a $poly) Simple_utils.Trace.result = fold_map__$poly;;"; } +{ say "let fold_map__$poly : type a new_a state . (state -> a -> (state * new_a, _) monad) -> state -> a $poly -> (state * new_a $poly , _) monad = fold_map__$poly;;"; } say ""; for $adts.kv -> $index, $t { @@ -182,47 +185,37 @@ say ";;"; say ""; for $adts.list -> $t { - say "type 'state continue_fold_map__$t = \{"; - say " node__$t : 'state -> $t -> ('state * $t) monad ;"; + say "type ('state, 'err) _continue_fold_map__$t = \{"; + say " node__$t : 'state -> $t -> ('state * $t , 'err) monad ;"; for $t.list -> $c - { say " $t__$c : 'state -> {$c || 'unit'} -> ('state * {$c || 'unit'}) monad ;" } + { say " $t__$c : 'state -> {$c || 'unit'} -> ('state * {$c || 'unit'} , 'err) monad ;" } say ' };;'; } -say "type 'state continue_fold_map = \{"; +say "type ('state , 'err) _continue_fold_map__$moduleName = \{"; for $adts.list -> $t { - say " $t : 'state continue_fold_map__$t ;"; + say " $t : ('state , 'err) _continue_fold_map__$t ;"; } say ' };;'; say ""; for $adts.list -> $t -{ say "type 'state fold_map_config__$t = \{"; - say " node__$t : 'state -> $t -> 'state continue_fold_map -> ('state * $t) monad ;"; # (*Adt_info.node_instance_info ->*) - say " node__$t__pre_state : 'state -> $t -> 'state monad ;"; # (*Adt_info.node_instance_info ->*) - say " node__$t__post_state : 'state -> $t -> $t -> 'state monad ;"; # (*Adt_info.node_instance_info ->*) +{ say "type ('state, 'err) fold_map_config__$t = \{"; + say " node__$t : 'state -> $t -> ('state, 'err) _continue_fold_map__$moduleName -> ('state * $t , 'err) monad ;"; # (*Adt_info.node_instance_info ->*) + say " node__$t__pre_state : 'state -> $t -> ('state, 'err) monad ;"; # (*Adt_info.node_instance_info ->*) + say " node__$t__post_state : 'state -> $t -> $t -> ('state, 'err) monad ;"; # (*Adt_info.node_instance_info ->*) for $t.list -> $c - { say " $t__$c : 'state -> {$c || 'unit'} -> 'state continue_fold_map -> ('state * {$c || 'unit'}) monad ;"; # (*Adt_info.ctor_or_field_instance_info ->*) + { say " $t__$c : 'state -> {$c || 'unit'} -> ('state, 'err) _continue_fold_map__$moduleName -> ('state * {$c || 'unit'} , 'err) monad ;"; # (*Adt_info.ctor_or_field_instance_info ->*) } say '};;' } -say "type 'state fold_map_config ="; +say "type ('state, 'err) fold_map_config__$moduleName ="; say ' {'; for $adts.list -> $t -{ say " $t : 'state fold_map_config__$t;" } +{ say " $t : ('state, 'err) fold_map_config__$t;" } say ' };;'; -say ""; -say "module StringMap = Map.Make(String);;"; -say "(* generic folds for nodes *)"; -say "type 'state generic_continue_fold_node = \{"; -say " continue : 'state -> 'state ;"; -say " (* generic folds for each field *)"; -say " continue_ctors_or_fields : ('state -> 'state) StringMap.t ;"; -say '};;'; -say "(* map from node names to their generic folds *)"; -say "type 'state generic_continue_fold = ('state generic_continue_fold_node) StringMap.t;;"; -say ""; +say "include Adt_generator.Generic.BlahBluh"; say "type ('state , 'adt_info_node_instance_info) _fold_config ="; say ' {'; say " generic : 'state -> 'adt_info_node_instance_info -> 'state;"; @@ -371,31 +364,31 @@ for $adts.list -> $t say ""; -say "type 'state mk_continue_fold_map = \{"; -say " fn : 'state mk_continue_fold_map -> 'state fold_map_config -> 'state continue_fold_map"; +say "type ('state, 'err) mk_continue_fold_map = \{"; +say " fn : ('state, 'err) mk_continue_fold_map -> ('state, 'err) fold_map_config__$moduleName -> ('state, 'err) _continue_fold_map__$moduleName"; say '};;'; # fold_map functions say ""; for $adts.list -> $t -{ say "let _fold_map__$t : type qstate . qstate mk_continue_fold_map -> qstate fold_map_config -> qstate -> $t -> (qstate * $t) monad = fun mk_continue_fold_map visitor state x ->"; - say " let continue_fold_map : qstate continue_fold_map = mk_continue_fold_map.fn mk_continue_fold_map visitor in"; +{ say "let _fold_map__$t : type qstate err . (qstate,err) mk_continue_fold_map -> (qstate,err) fold_map_config__$moduleName -> qstate -> $t -> (qstate * $t, err) monad = fun mk_continue_fold_map visitor state x ->"; + say " let continue_fold_map : (qstate,err) _continue_fold_map__$moduleName = mk_continue_fold_map.fn mk_continue_fold_map visitor in"; say " visitor.$t.node__$t__pre_state state x >>? fun state ->"; # (*(fun () -> whole_adt_info, info__$t)*) say " visitor.$t.node__$t state x continue_fold_map >>? fun (state, new_x) ->"; # (*(fun () -> whole_adt_info, info__$t)*) say " visitor.$t.node__$t__post_state state x new_x >>? fun state ->"; # (*(fun () -> whole_adt_info, info__$t)*) say " return (state, new_x);;"; say ""; for $t.list -> $c - { say "let _fold_map__$t__$c : type qstate . qstate mk_continue_fold_map -> qstate fold_map_config -> qstate -> { $c || 'unit' } -> (qstate * { $c || 'unit' }) monad = fun mk_continue_fold_map visitor state x ->"; - say " let continue_fold_map : qstate continue_fold_map = mk_continue_fold_map.fn mk_continue_fold_map visitor in"; + { say "let _fold_map__$t__$c : type qstate err . (qstate,err) mk_continue_fold_map -> (qstate,err) fold_map_config__$moduleName -> qstate -> { $c || 'unit' } -> (qstate * { $c || 'unit' }, err) monad = fun mk_continue_fold_map visitor state x ->"; + say " let continue_fold_map : (qstate,err) _continue_fold_map__$moduleName = mk_continue_fold_map.fn mk_continue_fold_map visitor in"; say " visitor.$t.$t__$c state x continue_fold_map;;"; # (*(fun () -> whole_adt_info, info__$t, info__$t__$c)*) say ""; } } # make the "continue" object say ""; say '(* Curries the "visitor" argument to the folds (non-customizable traversal functions). *)'; -say "let mk_continue_fold_map : 'state . 'state mk_continue_fold_map = \{ fn = fun self visitor ->"; +say "let mk_continue_fold_map : 'state 'err . ('state,'err) mk_continue_fold_map = \{ fn = fun self visitor ->"; say ' {'; for $adts.list -> $t { say " $t = \{"; @@ -410,16 +403,16 @@ say ""; # fold_map functions : tying the knot say ""; for $adts.list -> $t -{ say "let fold_map__$t : type qstate . qstate fold_map_config -> qstate -> $t -> (qstate * $t) monad ="; +{ say "let fold_map__$t : type qstate err . (qstate,err) fold_map_config__$moduleName -> qstate -> $t -> (qstate * $t,err) monad ="; say " fun visitor state x -> _fold_map__$t mk_continue_fold_map visitor state x;;"; for $t.list -> $c - { say "let fold_map__$t__$c : type qstate . qstate fold_map_config -> qstate -> { $c || 'unit' } -> (qstate * { $c || 'unit' }) monad ="; + { say "let fold_map__$t__$c : type qstate err . (qstate,err) fold_map_config__$moduleName -> qstate -> { $c || 'unit' } -> (qstate * { $c || 'unit' },err) monad ="; say " fun visitor state x -> _fold_map__$t__$c mk_continue_fold_map visitor state x;;"; } } for $adts.list -> $t { - say "let no_op_node__$t : type state . state -> $t -> state continue_fold_map -> (state * $t) monad ="; + say "let no_op_node__$t : type state . state -> $t -> (state,_) _continue_fold_map__$moduleName -> (state * $t,_) monad ="; say " fun state v continue ->"; # (*_info*) say " match v with"; if ($t eq $variant) { @@ -446,7 +439,7 @@ for $adts.list -> $t } for $adts.list -> $t -{ say "let no_op__$t : type state . state fold_map_config__$t = \{"; +{ say "let no_op__$t : type state . (state,_) fold_map_config__$t = \{"; say " node__$t = no_op_node__$t;"; say " node__$t__pre_state = (fun state v -> ignore v; return state) ;"; # (*_info*) say " node__$t__post_state = (fun state v new_v -> ignore (v, new_v); return state) ;"; # (*_info*) @@ -460,15 +453,21 @@ for $adts.list -> $t say ") ;"; } say ' }' } -say "let no_op : type state . state fold_map_config = \{"; +say "let no_op : type state . (state,_) fold_map_config__$moduleName = \{"; for $adts.list -> $t { say " $t = no_op__$t;" } say '};;'; say ""; for $adts.list -> $t -{ say "let with__$t : _ -> _ fold_map_config -> _ fold_map_config = (fun node__$t op -> \{ op with $t = \{ op.$t with node__$t \} \});;"; - say "let with__$t__pre_state : _ -> _ fold_map_config -> _ fold_map_config = (fun node__$t__pre_state op -> \{ op with $t = \{ op.$t with node__$t__pre_state \} \});;"; - say "let with__$t__post_state : _ -> _ fold_map_config -> _ fold_map_config = (fun node__$t__post_state op -> \{ op with $t = \{ op.$t with node__$t__post_state \} \});;"; +{ say "let with__$t : _ -> _ fold_map_config__$moduleName -> _ fold_map_config__$moduleName = (fun node__$t op -> \{ op with $t = \{ op.$t with node__$t \} \});;"; + say "let with__$t__pre_state : _ -> _ fold_map_config__$moduleName -> _ fold_map_config__$moduleName = (fun node__$t__pre_state op -> \{ op with $t = \{ op.$t with node__$t__pre_state \} \});;"; + say "let with__$t__post_state : _ -> _ fold_map_config__$moduleName -> _ fold_map_config__$moduleName = (fun node__$t__post_state op -> \{ op with $t = \{ op.$t with node__$t__post_state \} \});;"; for $t.list -> $c - { say "let with__$t__$c : _ -> _ fold_map_config -> _ fold_map_config = (fun $t__$c op -> \{ op with $t = \{ op.$t with $t__$c \} \});;"; } } + { say "let with__$t__$c : _ -> _ fold_map_config__$moduleName -> _ fold_map_config__$moduleName = (fun $t__$c op -> \{ op with $t = \{ op.$t with $t__$c \} \});;"; } } + +say ""; +say "module Folds (M : sig type state type 'a t val f : (state fold_config -> state -> 'a -> state) -> 'a t end) = struct"; +for $adts.list -> $t +{ say "let $t = M.f fold__$t;;"; } +say "end"; diff --git a/src/stages/adt_generator/generic.ml b/src/stages/adt_generator/generic.ml index c4f28821a..c48ca1ac1 100644 --- a/src/stages/adt_generator/generic.ml +++ b/src/stages/adt_generator/generic.ml @@ -1,3 +1,15 @@ +module BlahBluh = struct +module StringMap = Map.Make(String);; +(* generic folds for nodes *) +type 'state generic_continue_fold_node = { + continue : 'state -> 'state ; + (* generic folds for each field *) + continue_ctors_or_fields : ('state -> 'state) StringMap.t ; +};; +(* map from node names to their generic folds *) +type 'state generic_continue_fold = ('state generic_continue_fold_node) StringMap.t;; +end + module Adt_info (M : sig type ('state , 'adt_info_node_instance_info) fold_config end) = struct type kind = | Record diff --git a/src/stages/common/PP.ml b/src/stages/common/PP.ml index 93e46b96d..914a8bad6 100644 --- a/src/stages/common/PP.ml +++ b/src/stages/common/PP.ml @@ -130,7 +130,6 @@ let literal ppf (l : literal) = match l with | Literal_unit -> fprintf ppf "unit" | Literal_void -> fprintf ppf "void" - | Literal_bool b -> fprintf ppf "%b" b | Literal_int z -> fprintf ppf "%a" Z.pp_print z | Literal_nat z -> fprintf ppf "+%a" Z.pp_print z | Literal_timestamp z -> fprintf ppf "+%a" Z.pp_print z @@ -155,7 +154,6 @@ let s = | TC_nat -> "nat" | TC_int -> "int" | TC_mutez -> "mutez" - | TC_bool -> "bool" | TC_operation -> "operation" | TC_address -> "address" | TC_key -> "key" @@ -251,7 +249,6 @@ module Ast_PP_type (PARAMETER : AST_PARAMETER_TYPE) = struct | TC_map (k, v) -> Format.asprintf "Map (%a,%a)" f k f v | TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v | TC_map_or_big_map (k, v) -> Format.asprintf "Map Or Big Map (%a,%a)" f k f v - | TC_arrow (k, v) -> Format.asprintf "arrow (%a,%a)" f k f v | TC_contract te -> Format.asprintf "Contract (%a)" f te in fprintf ppf "(type_operator: %s)" s diff --git a/src/stages/common/constant.ml b/src/stages/common/constant.ml new file mode 100644 index 000000000..84727fd31 --- /dev/null +++ b/src/stages/common/constant.ml @@ -0,0 +1,2 @@ +open Types +let t_bool : type_variable = Var.of_name "bool" diff --git a/src/stages/common/types.ml b/src/stages/common/types.ml index 8974eb905..31582d372 100644 --- a/src/stages/common/types.ml +++ b/src/stages/common/types.ml @@ -20,7 +20,6 @@ type 'a constructor_map = 'a CMap.t | TC_nat | TC_int | TC_mutez - | TC_bool | TC_operation | TC_address | TC_key @@ -60,7 +59,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct | TC_map of type_expression * type_expression | TC_big_map of type_expression * type_expression | TC_map_or_big_map of type_expression * type_expression - | TC_arrow of type_expression * type_expression and type_expression = {type_content: type_content; location: Location.t; type_meta: type_meta} @@ -74,7 +72,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct | TC_map (x , y) -> TC_map (f x , f y) | TC_big_map (x , y)-> TC_big_map (f x , f y) | TC_map_or_big_map (x , y)-> TC_map_or_big_map (f x , f y) - | TC_arrow (x, y) -> TC_arrow (f x, f y) let bind_map_type_operator f = function TC_contract x -> let%bind x = f x in ok @@ TC_contract x @@ -84,7 +81,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct | TC_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_map (x , y) | TC_big_map (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y) | TC_map_or_big_map (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_map_or_big_map (x , y) - | TC_arrow (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_arrow (x , y) let type_operator_name = function TC_contract _ -> "TC_contract" @@ -94,7 +90,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct | TC_map _ -> "TC_map" | TC_big_map _ -> "TC_big_map" | TC_map_or_big_map _ -> "TC_map_or_big_map" - | TC_arrow _ -> "TC_arrow" let type_expression'_of_string = function | "TC_contract" , [x] -> ok @@ T_operator(TC_contract x) @@ -112,7 +107,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct | "TC_nat" , [] -> ok @@ T_constant(TC_nat) | "TC_int" , [] -> ok @@ T_constant(TC_int) | "TC_mutez" , [] -> ok @@ T_constant(TC_mutez) - | "TC_bool" , [] -> ok @@ T_constant(TC_bool) | "TC_operation" , [] -> ok @@ T_constant(TC_operation) | "TC_address" , [] -> ok @@ T_constant(TC_address) | "TC_key" , [] -> ok @@ T_constant(TC_key) @@ -133,7 +127,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct | TC_map (x , y) -> "TC_map" , [x ; y] | TC_big_map (x , y) -> "TC_big_map" , [x ; y] | TC_map_or_big_map (x , y) -> "TC_map_or_big_map" , [x ; y] - | TC_arrow (x , y) -> "TC_arrow" , [x ; y] let string_of_type_constant = function | TC_unit -> "TC_unit", [] @@ -142,7 +135,6 @@ module Ast_generic_type (PARAMETER : AST_PARAMETER_TYPE) = struct | TC_nat -> "TC_nat", [] | TC_int -> "TC_int", [] | TC_mutez -> "TC_mutez", [] - | TC_bool -> "TC_bool", [] | TC_operation -> "TC_operation", [] | TC_address -> "TC_address", [] | TC_key -> "TC_key", [] @@ -162,7 +154,6 @@ end type literal = | Literal_unit - | Literal_bool of bool | Literal_int of Z.t | Literal_nat of Z.t | Literal_timestamp of Z.t @@ -178,10 +169,6 @@ type literal = | Literal_operation of Memory_proto_alpha.Protocol.Alpha_context.packed_internal_operation and ('a,'tv) matching_content = - | Match_bool of { - match_true : 'a ; - match_false : 'a ; - } | Match_list of { match_nil : 'a ; match_cons : expression_variable * expression_variable * 'a * 'tv; diff --git a/src/stages/typesystem/core.ml b/src/stages/typesystem/core.ml index cf7dd41b8..1fc668ace 100644 --- a/src/stages/typesystem/core.ml +++ b/src/stages/typesystem/core.ml @@ -1,3 +1,27 @@ +type unionfind = Ast_typed.unionfind +type constant_tag = Ast_typed.constant_tag +type accessor = Ast_typed.label +type type_value = Ast_typed.type_value +type p_constraints = Ast_typed.p_constraints +type p_forall = Ast_typed.p_forall +type simple_c_constructor = Ast_typed.simple_c_constructor +type simple_c_constant = Ast_typed.simple_c_constant +type c_const = Ast_typed.c_const +type c_equation = Ast_typed.c_equation +type c_typeclass = Ast_typed.c_typeclass +type c_access_label = Ast_typed.c_access_label +type type_constraint = Ast_typed.type_constraint +type typeclass = Ast_typed.typeclass +type 'a typeVariableMap = 'a Ast_typed.typeVariableMap +type structured_dbs = Ast_typed.structured_dbs +type constraints = Ast_typed.constraints +type c_constructor_simpl = Ast_typed.c_constructor_simpl +type c_const_e = Ast_typed.c_const_e +type c_equation_e = Ast_typed.c_equation_e +type c_typeclass_simpl = Ast_typed.c_typeclass_simpl +type c_poly_simpl = Ast_typed.c_poly_simpl +type type_constraint_simpl = Ast_typed.type_constraint_simpl +type state = Ast_typed.typer_state type type_variable = Ast_typed.type_variable type type_expression = Ast_typed.type_expression @@ -6,76 +30,16 @@ type type_expression = Ast_typed.type_expression let fresh_type_variable : ?name:string -> unit -> type_variable = Var.fresh - -(* add information on the type or the kind for operator*) -type constant_tag = - | C_arrow (* * -> * -> * *) (* isn't this wrong*) - | C_option (* * -> * *) - | C_record (* ( label , * ) … -> * *) - | C_variant (* ( label , * ) … -> * *) - | C_map (* * -> * -> * *) - | C_big_map (* * -> * -> * *) - | C_list (* * -> * *) - | C_set (* * -> * *) - | C_unit (* * *) - | C_bool (* * *) - | C_string (* * *) - | C_nat (* * *) - | C_mutez (* * *) - | C_timestamp (* * *) - | C_int (* * *) - | C_address (* * *) - | C_bytes (* * *) - | C_key_hash (* * *) - | C_key (* * *) - | C_signature (* * *) - | C_operation (* * *) - | C_contract (* * -> * *) - | C_chain_id (* * *) - -type accessor = Ast_typed.label - -(* Weird stuff; please explain *) -type type_value = - | P_forall of p_forall - | P_variable of type_variable (* how a value can be a variable? *) - | P_constant of (constant_tag * type_value list) - | P_apply of (type_value * type_value) - -and p_forall = { - binder : type_variable ; - constraints : type_constraint list ; - body : type_value -} - -(* Different type of constraint *) (* why isn't this a variant ? *) -and simple_c_constructor = (constant_tag * type_variable list) (* non-empty list *) -and simple_c_constant = (constant_tag) (* for type constructors that do not take arguments *) -and c_const = (type_variable * type_value) -and c_equation = (type_value * type_value) -and c_typeclass = (type_value list * typeclass) -and c_access_label = (type_value * accessor * type_variable) - -(*What i was saying just before *) -and type_constraint = - (* | C_assignment of (type_variable * type_pattern) *) - | C_equation of c_equation (* TVA = TVB *) - | C_typeclass of c_typeclass (* TVL ∈ TVLs, for now in extension, later add intensional (rule-based system for inclusion in the typeclass) *) - | C_access_label of c_access_label (* poor man's type-level computation to ensure that TV.label is type_variable *) -(* | … *) - -(* is the first list in case on of the type of the type class as a kind *->*->* ? *) -and typeclass = type_value list list - open Trace -let type_expression'_of_simple_c_constant = function +let type_expression'_of_simple_c_constant : constant_tag * type_expression list -> Ast_typed.type_content result = fun (c, l) -> + match c, l with | C_contract , [x] -> ok @@ Ast_typed.T_operator(TC_contract x) | C_option , [x] -> ok @@ Ast_typed.T_operator(TC_option x) | C_list , [x] -> ok @@ Ast_typed.T_operator(TC_list x) | C_set , [x] -> ok @@ Ast_typed.T_operator(TC_set x) | C_map , [k ; v] -> ok @@ Ast_typed.T_operator(TC_map {k ; v}) | C_big_map , [k ; v] -> ok @@ Ast_typed.T_operator(TC_big_map {k ; v}) - | C_arrow , [x ; y] -> ok @@ Ast_typed.T_operator(TC_arrow {type1=x ; type2=y}) + | C_arrow , [x ; y] -> ok @@ Ast_typed.T_arrow {type1=x ; type2=y} (* For now, the arrow type constructor is special *) | C_record , _lst -> ok @@ failwith "records are not supported yet: T_record lst" | C_variant , _lst -> ok @@ failwith "sums are not supported yet: T_sum lst" | (C_contract | C_option | C_list | C_set | C_map | C_big_map | C_arrow ), _ -> @@ -87,7 +51,6 @@ let type_expression'_of_simple_c_constant = function | C_nat , [] -> ok @@ Ast_typed.T_constant(TC_nat) | C_int , [] -> ok @@ Ast_typed.T_constant(TC_int) | C_mutez , [] -> ok @@ Ast_typed.T_constant(TC_mutez) - | C_bool , [] -> ok @@ Ast_typed.T_constant(TC_bool) | C_operation , [] -> ok @@ Ast_typed.T_constant(TC_operation) | C_address , [] -> ok @@ Ast_typed.T_constant(TC_address) | C_key , [] -> ok @@ Ast_typed.T_constant(TC_key) @@ -95,5 +58,5 @@ let type_expression'_of_simple_c_constant = function | C_chain_id , [] -> ok @@ Ast_typed.T_constant(TC_chain_id) | C_signature , [] -> ok @@ Ast_typed.T_constant(TC_signature) | C_timestamp , [] -> ok @@ Ast_typed.T_constant(TC_timestamp) - | (C_unit | C_string | C_bytes | C_nat | C_int | C_mutez | C_bool | C_operation | C_address | C_key | C_key_hash | C_chain_id | C_signature | C_timestamp), _::_ -> + | (C_unit | C_string | C_bytes | C_nat | C_int | C_mutez | C_operation | C_address | C_key | C_key_hash | C_chain_id | C_signature | C_timestamp), _::_ -> failwith "internal error: wrong number of arguments for type constant" diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml index 499732a0e..17c1d3eff 100644 --- a/src/stages/typesystem/misc.ml +++ b/src/stages/typesystem/misc.ml @@ -85,9 +85,10 @@ module Substitution = struct | T.T_operator type_name_and_args -> let%bind type_name_and_args = T.Helpers.bind_map_type_operator (s_type_expression ~substs) type_name_and_args in ok @@ T.T_operator type_name_and_args - | T.T_arrow _ -> - let _TODO = substs in - failwith "TODO: T_function" + | T.T_arrow { type1; type2 } -> + let%bind type1 = s_type_expression ~substs type1 in + let%bind type2 = s_type_expression ~substs type2 in + ok @@ T.T_arrow { type1; type2 } and s_abstr_type_content : Ast_core.type_content w = fun ~substs -> function | Ast_core.T_sum _ -> failwith "TODO: subst: unimplemented case s_type_expression sum" @@ -119,7 +120,6 @@ module Substitution = struct | T.Literal_void -> let () = ignore @@ substs in ok @@ T.Literal_void - | (T.Literal_bool _ as x) | (T.Literal_int _ as x) | (T.Literal_nat _ as x) | (T.Literal_timestamp _ as x) @@ -224,16 +224,15 @@ module Substitution = struct and type_value ~tv ~substs = let self tv = type_value ~tv ~substs in let (v, expr) = substs in - match tv with + match (tv : type_value) with | P_variable v' when Var.equal v' v -> expr | P_variable _ -> tv - | P_constant (x , lst) -> ( + | P_constant {p_ctor_tag=x ; p_ctor_args=lst} -> ( let lst' = List.map self lst in - P_constant (x , lst') + P_constant {p_ctor_tag=x ; p_ctor_args=lst'} ) - | P_apply ab -> ( - let ab' = pair_map self ab in - P_apply ab' + | P_apply { tf; targ } -> ( + P_apply { tf = self tf ; targ = self targ } ) | P_forall p -> ( let aux c = constraint_ ~c ~substs in @@ -248,18 +247,18 @@ module Substitution = struct and constraint_ ~c ~substs = match c with - | C_equation ab -> ( - let ab' = pair_map (fun tv -> type_value ~tv ~substs) ab in - C_equation ab' + | C_equation { aval; bval } -> ( + let aux tv = type_value ~tv ~substs in + C_equation { aval = aux aval ; bval = aux bval } ) - | C_typeclass (tvs , tc) -> ( - let tvs' = List.map (fun tv -> type_value ~tv ~substs) tvs in - let tc' = typeclass ~tc ~substs in - C_typeclass (tvs' , tc') + | C_typeclass { tc_args; typeclass=tc } -> ( + let tc_args = List.map (fun tv -> type_value ~tv ~substs) tc_args in + let tc = typeclass ~tc ~substs in + C_typeclass {tc_args ; typeclass=tc} ) - | C_access_label (tv , l , v') -> ( - let tv' = type_value ~tv ~substs in - C_access_label (tv' , l , v') + | C_access_label { c_access_label_tval; accessor; c_access_label_tvar } -> ( + let c_access_label_tval = type_value ~tv:c_access_label_tval ~substs in + C_access_label {c_access_label_tval ; accessor ; c_access_label_tvar} ) and typeclass ~tc ~substs = @@ -270,9 +269,9 @@ module Substitution = struct (* Performs beta-reduction at the root of the type *) let eval_beta_root ~(tv : type_value) = match tv with - P_apply (P_forall { binder; constraints; body }, arg) -> - let constraints = List.map (fun c -> constraint_ ~c ~substs:(mk_substs ~v:binder ~expr:arg)) constraints in - (type_value ~tv:body ~substs:(mk_substs ~v:binder ~expr:arg) , constraints) + P_apply {tf = P_forall { binder; constraints; body }; targ} -> + let constraints = List.map (fun c -> constraint_ ~c ~substs:(mk_substs ~v:binder ~expr:targ)) constraints in + (type_value ~tv:body ~substs:(mk_substs ~v:binder ~expr:targ) , constraints) | _ -> (tv , []) end diff --git a/src/stages/typesystem/shorthands.ml b/src/stages/typesystem/shorthands.ml index 844be70a3..c01775120 100644 --- a/src/stages/typesystem/shorthands.ml +++ b/src/stages/typesystem/shorthands.ml @@ -1,7 +1,9 @@ +open Ast_typed.Types open Core +open Ast_typed.Misc -let tc type_vars allowed_list = - Core.C_typeclass (type_vars , allowed_list) +let tc type_vars allowed_list : type_constraint = + C_typeclass {tc_args = type_vars ; typeclass = allowed_list} let forall binder f = let () = ignore binder in @@ -45,32 +47,32 @@ let forall2_tc a b f = f a' b' let (=>) tc ty = (tc , ty) -let (-->) arg ret = P_constant (C_arrow , [arg; ret]) -let option t = P_constant (C_option , [t]) -let pair a b = P_constant (C_record , [a; b]) -let sum a b = P_constant (C_variant, [a; b]) -let map k v = P_constant (C_map , [k; v]) -let unit = P_constant (C_unit , []) -let list t = P_constant (C_list , [t]) -let set t = P_constant (C_set , [t]) -let bool = P_constant (C_bool , []) -let string = P_constant (C_string , []) -let nat = P_constant (C_nat , []) -let mutez = P_constant (C_mutez , []) -let timestamp = P_constant (C_timestamp , []) -let int = P_constant (C_int , []) -let address = P_constant (C_address , []) -let chain_id = P_constant (C_chain_id , []) -let bytes = P_constant (C_bytes , []) -let key = P_constant (C_key , []) -let key_hash = P_constant (C_key_hash , []) -let signature = P_constant (C_signature , []) -let operation = P_constant (C_operation , []) -let contract t = P_constant (C_contract , [t]) +let (-->) arg ret = p_constant C_arrow [arg; ret] +let option t = p_constant C_option [t] +let pair a b = p_constant C_record [a; b] +let sum a b = p_constant C_variant [a; b] +let map k v = p_constant C_map [k; v] +let unit = p_constant C_unit [] +let list t = p_constant C_list [t] +let set t = p_constant C_set [t] +let bool = P_variable Stage_common.Constant.t_bool +let string = p_constant C_string [] +let nat = p_constant C_nat [] +let mutez = p_constant C_mutez [] +let timestamp = p_constant C_timestamp [] +let int = p_constant C_int [] +let address = p_constant C_address [] +let chain_id = p_constant C_chain_id [] +let bytes = p_constant C_bytes [] +let key = p_constant C_key [] +let key_hash = p_constant C_key_hash [] +let signature = p_constant C_signature [] +let operation = p_constant C_operation [] +let contract t = p_constant C_contract [t] let ( * ) a b = pair a b (* These are used temporarily to de-curry functions that correspond to Michelson operators *) -let tuple0 = P_constant (C_record , []) -let tuple1 a = P_constant (C_record , [a]) -let tuple2 a b = P_constant (C_record , [a; b]) -let tuple3 a b c = P_constant (C_record , [a; b; c]) +let tuple0 = p_constant C_record [] +let tuple1 a = p_constant C_record [a] +let tuple2 a b = p_constant C_record [a; b] +let tuple3 a b c = p_constant C_record [a; b; c] diff --git a/src/test/adt_generator/dune b/src/test/adt_generator/dune index 63fabe8ed..4236b1815 100644 --- a/src/test/adt_generator/dune +++ b/src/test/adt_generator/dune @@ -7,7 +7,6 @@ (executable (name test_adt_generator) - (public_name ligo.test_adt_generator) (libraries adt_generator simple-utils) (preprocess (pps ppx_let bisect_ppx --conditional) diff --git a/src/test/adt_generator/use_a_fold.ml b/src/test/adt_generator/use_a_fold.ml index 8cfd5aa3a..484940341 100644 --- a/src/test/adt_generator/use_a_fold.ml +++ b/src/test/adt_generator/use_a_fold.ml @@ -58,8 +58,8 @@ let () = (* Test that the same fold_map_config can be ascibed with different 'a type arguments *) -let _noi : int fold_map_config = no_op (* (fun _ -> ()) *) -let _nob : bool fold_map_config = no_op (* (fun _ -> ()) *) +let _noi : (int, [> error]) fold_map_config__Amodule = no_op (* (fun _ -> ()) *) +let _nob : (bool, [> error]) fold_map_config__Amodule = no_op (* (fun _ -> ()) *) let () = let some_root : root = A [ { a1 = X (A [ { a1 = X (B [ 1 ; 2 ; 3 ]) ; a2 = W () } ]) ; a2 = Z (W ()) } ] in diff --git a/src/test/typer_tests.ml b/src/test/typer_tests.ml index 0d33e2da4..f6c1f8296 100644 --- a/src/test/typer_tests.ml +++ b/src/test/typer_tests.ml @@ -20,7 +20,7 @@ let int () : unit result = ok () module TestExpressions = struct - let test_expression ?(env = Typer.Environment.full_empty) + let test_expression ?(env = Environment.default) ?(state = Typer.Solver.initial_state) (expr : expression) (test_expected_ty : Typed.type_expression) = diff --git a/tools/webide/packages/client/public/index.html b/tools/webide/packages/client/public/index.html index 7d5c78cf0..a1f3acb8d 100644 --- a/tools/webide/packages/client/public/index.html +++ b/tools/webide/packages/client/public/index.html @@ -34,7 +34,10 @@ gtag("config", "UA-153751765-1"); - + LIGO Playground diff --git a/tools/webide/packages/e2e/test/common-utils.js b/tools/webide/packages/e2e/test/common-utils.js index 68cddbadc..61cd3bef0 100644 --- a/tools/webide/packages/e2e/test/common-utils.js +++ b/tools/webide/packages/e2e/test/common-utils.js @@ -52,6 +52,8 @@ exports.API_ROOT = `${exports.API_HOST}/api`; exports.fetchExamples = async () => (await fetch(`${exports.API_HOST}/static/examples/list`)).json(); exports.runCommandAndGetOutputFor = async (command, endpoint) => { + page.on('console', msg => console.log('PAGE LOG:', msg.text())); + await page.click('#configure-tab'); await exports.sleep(1000); diff --git a/vendors/Preprocessor/Preprocessor.opam b/vendors/Preprocessor/Preprocessor.opam index e7d47fcdc..0a45620c3 100644 --- a/vendors/Preprocessor/Preprocessor.opam +++ b/vendors/Preprocessor/Preprocessor.opam @@ -8,7 +8,7 @@ authors : "Christian Rinderknecht" license : "MIT" homepage : "https://gitlab.com/ligolang/Preprocessor" bug-reports : "https://gitlab.com/ligolang/ligo-utils/issues" -depends : ["dune" "base" "ocaml" "simple-utils"] +depends : ["dune" "base" "ocaml" "simple-utils" "bisect_ppx" "menhir" "getopt"] build : [ [ "sh" "-c" "printf 'let version = \"%s\"' \"$(git describe --always --dirty --abbrev=0)\" > Version.ml" ] [ "dune" "build" "-p" name "-j" jobs ] diff --git a/vendors/Red-Black_Trees/PolyMap.ml b/vendors/Red-Black_Trees/PolyMap.ml index ee485ec40..0ed6e9d6d 100644 --- a/vendors/Red-Black_Trees/PolyMap.ml +++ b/vendors/Red-Black_Trees/PolyMap.ml @@ -11,7 +11,7 @@ type ('key, 'value) map = ('key, 'value) t let create ~cmp = {tree = RB.empty; cmp} -let empty = {tree = RB.empty; cmp=Pervasives.compare} +let empty map = {tree = RB.empty; cmp=map.cmp} let is_empty map = RB.is_empty map.tree @@ -19,16 +19,23 @@ let add key value map = let cmp (k1,_) (k2,_) = map.cmp k1 k2 in {map with tree = RB.add ~cmp RB.New (key, value) map.tree} -exception Not_found +let remove key map = + let cmp k1 (k2,_) = map.cmp k1 k2 in + {map with tree = RB.remove ~cmp key map.tree} let find key map = let cmp k1 (k2,_) = map.cmp k1 k2 in try snd (RB.find ~cmp key map.tree) with - RB.Not_found -> raise Not_found + Not_found -> raise Not_found let find_opt key map = try Some (find key map) with Not_found -> None +let update key updater map = + match updater (find_opt key map) with + | None -> remove key map + | Some v -> add key v map + let bindings map = RB.fold_dec (fun ~elt ~acc -> elt::acc) ~init:[] map.tree diff --git a/vendors/Red-Black_Trees/PolyMap.mli b/vendors/Red-Black_Trees/PolyMap.mli index 7aafb8ae0..bff0e87ce 100644 --- a/vendors/Red-Black_Trees/PolyMap.mli +++ b/vendors/Red-Black_Trees/PolyMap.mli @@ -20,7 +20,7 @@ type ('key, 'value) map = ('key, 'value) t val create : cmp:('key -> 'key -> int) -> ('key, 'value) t -val empty : ('key, 'value) t +val empty : ('key, 'value) t -> ('key, 'new_value) t (* Emptiness *) @@ -33,12 +33,15 @@ val is_empty : ('key, 'value) t -> bool val add : 'key -> 'value -> ('key, 'value) t -> ('key, 'value) t +(* The value of the call [add key value map] is a map containing all + the bindings of the map [map], except for the binding of [key]. *) + +val remove : 'key -> ('key, 'value) t -> ('key, 'value) t + (* The value of the call [find key map] is the value associated to the [key] in the map [map]. If [key] is not bound in [map], the exception [Not_found] is raised. *) -exception Not_found - val find : 'key -> ('key, 'value) t -> 'value (* The value of the call [find_opt key map] is [Some value] if the key @@ -47,6 +50,17 @@ val find : 'key -> ('key, 'value) t -> 'value val find_opt : 'key -> ('key, 'value) t -> 'value option +(* The value of the call [update key f map] is a map containing all + the bindings of the map [map], extended by the binding of [key] to + the value returned by [f], when [f maybe_value] returns + [Some value]. On the other hand, when [f maybe_value] returns + [None], the existing binding for [key] in [map] is removed from the + map, if there is one. The argument [maybe_value] passed to [f] is + [Some value] if the key [key] is bound to [value] in the map [map], + and [None] otherwise. *) + +val update : 'key -> ('value option -> 'value option) -> ('key, 'value) map -> ('key, 'value) map + (* The value of the call [bindings map] is the association list containing the bindings of the map [map], sorted by increasing keys (with respect to the total comparison function used to create the diff --git a/vendors/Red-Black_Trees/PolySet.ml b/vendors/Red-Black_Trees/PolySet.ml index 7e60fc3bd..ab26380f2 100644 --- a/vendors/Red-Black_Trees/PolySet.ml +++ b/vendors/Red-Black_Trees/PolySet.ml @@ -11,17 +11,15 @@ type 'elt set = 'elt t let create ~cmp = {tree = RB.empty; cmp} -let empty = {tree = RB.empty; cmp=Pervasives.compare} +let empty set = {tree = RB.empty; cmp=set.cmp} let is_empty set = RB.is_empty set.tree let add elt set = {set with tree = RB.add ~cmp:set.cmp RB.New elt set.tree} -exception Not_found - let find elt set = try RB.find ~cmp:set.cmp elt set.tree with - RB.Not_found -> raise Not_found + Not_found -> raise Not_found let find_opt elt set = RB.find_opt ~cmp:set.cmp elt set.tree diff --git a/vendors/Red-Black_Trees/PolySet.mli b/vendors/Red-Black_Trees/PolySet.mli index 42f85a529..c8eb4b6d4 100644 --- a/vendors/Red-Black_Trees/PolySet.mli +++ b/vendors/Red-Black_Trees/PolySet.mli @@ -19,7 +19,7 @@ type 'elt set = 'elt t val create : cmp:('elt -> 'elt -> int) -> 'elt t -val empty : 'elt t +val empty : 'elt t -> 'elt t (* Emptiness *) @@ -38,8 +38,6 @@ val add : 'elt -> 'elt t -> 'elt t function of [set] (see [create]). If [elt] is not in [set], then the exception [Not_found] is raised. *) -exception Not_found - val find : 'elt -> 'elt t -> 'elt (* The call [find_opt elt set] is similar to [find elt set], except diff --git a/vendors/Red-Black_Trees/RedBlack.ml b/vendors/Red-Black_Trees/RedBlack.ml index 50bb9659f..f77954d09 100644 --- a/vendors/Red-Black_Trees/RedBlack.ml +++ b/vendors/Red-Black_Trees/RedBlack.ml @@ -50,7 +50,32 @@ let add ~cmp choice elt tree = in try blacken (insert tree) with Physical_equality -> tree -exception Not_found +let remove : type a b . cmp:(a -> b -> int) -> a -> b t -> b t = fun ~cmp elt tree -> + (* TODO: this leaves the tree not properly balanced. *) + let rec bst_shift_up : b t -> b t = function + | Ext -> failwith "unknown error" + | Int (colour, left, root, right) -> + ( + ignore root; (* we delete the root *) + match left, right with + | Ext, Ext -> Ext + | Ext, Int (_rcolour, _rleft, rroot, _rright) -> + let new_right = bst_shift_up right in + Int (colour, Ext, rroot, new_right) + | Int (_lcolour, _lleft, lroot, _lright), _ -> + let new_left = bst_shift_up left in + Int (colour, new_left, lroot, right) + ) in + let rec bst_delete : a -> b t -> b t = fun elt -> function + | Ext -> raise Not_found + | Int (colour, left, root, right) as current -> + let c = cmp elt root in + if c = 0 then bst_shift_up current + else if c < 0 then Int (colour, bst_delete elt left, root, right) + else Int (colour, left, root, bst_delete elt right) + in + try bst_delete elt tree + with Not_found -> tree let rec find ~cmp elt = function Ext -> raise Not_found diff --git a/vendors/Red-Black_Trees/RedBlack.mli b/vendors/Red-Black_Trees/RedBlack.mli index 65a45230c..16d1f1a2e 100644 --- a/vendors/Red-Black_Trees/RedBlack.mli +++ b/vendors/Red-Black_Trees/RedBlack.mli @@ -26,12 +26,19 @@ type choice = Old | New val add: cmp:('a -> 'a -> int) -> choice -> 'a -> 'a t -> 'a t +(* The value of the call [remove ~cmp x t] is a red-black tree + containing the same elements as [t] with the exception of the + element identified by [x]. The type of [x] can be different from + that of the elements of the tree, for example if the tree is used to + implement a map, x would be a [key], whereas the elements of the tree + would be [key, value] pairs. *) + +val remove: cmp:('a -> 'b -> int) -> 'a -> 'b t -> 'b t + (* The value of the call [find ~cmp x t] is the element [y] belonging to a node of the tree [t], such that [cmp x y = true]. If none, the exception [Not_found] is raised. *) -exception Not_found - val find: cmp:('a -> 'b -> int) -> 'a -> 'b t -> 'b (* The value of call [find_opt ~cmp x t] is [Some y] if there is an diff --git a/vendors/UnionFind/Poly2.ml b/vendors/UnionFind/Poly2.ml index dd3660b14..f3ac7fd8c 100644 --- a/vendors/UnionFind/Poly2.ml +++ b/vendors/UnionFind/Poly2.ml @@ -1,8 +1,6 @@ (** Persistent implementation of the Union/Find algorithm with height-balanced forests and no path compression. *) -(* type item = Item.t *) - let equal compare i j = compare i j = 0 type height = int @@ -43,6 +41,7 @@ let map_empty (compare : 'item -> 'item -> int) : ('item, 'value) map = RedBlack let map_find : 'item 'value . 'item -> ('item, 'value) map -> 'value = RedBlackTrees.PolyMap.find let map_iter : 'item 'value . ('item -> 'value -> unit) -> ('item, 'value) map -> unit = RedBlackTrees.PolyMap.iter let map_add : 'item 'value . 'item -> 'value -> ('item, 'value) map -> ('item, 'value) map = RedBlackTrees.PolyMap.add +let map_sorted_keys : 'item 'value . ('item, 'value) map -> 'item list = fun m -> List.map fst @@ RedBlackTrees.PolyMap.bindings m (** The type [partition] implements a partition of classes of equivalent items by means of a map from items to nodes of type @@ -76,17 +75,20 @@ let is_equiv (i: 'item) (j: 'item) (p: 'item partition) : bool = try equal p.compare (repr i p) (repr j p) with Not_found -> false -let get_or_set (i: 'item) (p: 'item partition) = +let get_or_set_h (i: 'item) (p: 'item partition) = try seek i p, p with Not_found -> let n = i,0 in (n, root n p) +let get_or_set (i: 'item) (p: 'item partition) = + let (i, _h), p = get_or_set_h i p in (i, p) + let mem i p = try Some (repr i p) with Not_found -> None let repr i p = try repr i p with Not_found -> i let equiv (i: 'item) (j: 'item) (p: 'item partition) : 'item partition = - let (ri,hi as ni), p = get_or_set i p in - let (rj,hj as nj), p = get_or_set j p in + let (ri,hi as ni), p = get_or_set_h i p in + let (rj,hj as nj), p = get_or_set_h j p in if equal p.compare ri rj then p else if hi > hj @@ -104,8 +106,8 @@ let equiv (i: 'item) (j: 'item) (p: 'item partition) : 'item partition = applied (which, without the constraint above, would yield a height-balanced new tree). *) let alias (i: 'item) (j: 'item) (p: 'item partition) : 'item partition = - let (ri,hi as ni), p = get_or_set i p in - let (rj,hj as nj), p = get_or_set j p in + let (ri,hi as ni), p = get_or_set_h i p in + let (rj,hj as nj), p = get_or_set_h j p in if equal p.compare ri rj then p else if hi = hj || equal p.compare ri i @@ -113,10 +115,39 @@ let alias (i: 'item) (j: 'item) (p: 'item partition) : 'item partition = else if hi < hj then link ni rj p else link nj ri p +(** {1 iteration over the elements} *) + +let elements : 'item . 'item partition -> 'item list = + fun { to_string=_; compare=_; map } -> + map_sorted_keys map + +let partitions : 'item . 'item partition -> 'item list list = + let compare_lists_by_first cmp la lb = + match la,lb with + | [],[] -> 0 + | [],_ -> -1 + | _,[] -> 1 + | a::_, b::_ -> cmp a b in + fun ({ to_string=_; compare; map } as p) -> + let aux acc elt = + RedBlackTrees.PolyMap.update + (repr elt p) + (function None -> Some [elt] | Some l -> Some (elt::l)) + acc in + let grouped = List.fold_left + aux + (RedBlackTrees.PolyMap.create ~cmp:compare) + (map_sorted_keys map) in + let partitions = RedBlackTrees.PolyMap.bindings grouped in + (* Sort the elements within partitions and partitions by their smallest element *) + let partitions = List.map snd partitions in + let partitions = List.map (List.sort compare) partitions in + let partitions = List.sort (compare_lists_by_first compare) partitions in + partitions + (** {1 Printing} *) -let print (p: 'item partition) = - let buffer = Buffer.create 80 in +let print ppf (p: 'item partition) = let print i node = let hi, hj, j = match node with @@ -124,8 +155,8 @@ let print (p: 'item partition) = | Link (j,hi) -> match map_find j p.map with Root hj | Link (_,hj) -> hi,hj,j in - let link = - Printf.sprintf "%s,%d -> %s,%d\n" + let () = + Format.fprintf ppf "%s,%d -> %s,%d\n" (p.to_string i) hi (p.to_string j) hj - in Buffer.add_string buffer link - in map_iter print p.map; buffer + in () + in map_iter print p.map diff --git a/vendors/UnionFind/Poly2.mli b/vendors/UnionFind/Poly2.mli new file mode 100644 index 000000000..8cea54c0c --- /dev/null +++ b/vendors/UnionFind/Poly2.mli @@ -0,0 +1,70 @@ +(** This module offers the abstract data type of a partition of + classes of equivalent items (Union & Find). *) + +(** The items are of type 't, they have to obey a total order, + but also they must be printable to ease debugging. *) + +type 'item partition +type 'item t = 'item partition + +(** {1 Creation} *) + +(** The value [empty] is an empty partition. *) +val empty : ('a -> string) -> ('a -> 'a -> int) -> 'a partition + +(** The value of [equiv i j p] is the partition [p] extended with + the equivalence of items [i] and [j]. If both [i] and [j] are + already known to be equivalent, then [equiv i j p == p]. *) +val equiv : 'item -> 'item -> 'item t -> 'item partition + +(** The value of [alias i j p] is the partition [p] extended with + the fact that item [i] is an alias of item [j]. This is the + same as [equiv i j p], except that it is guaranteed that the + item [i] is not the representative of its equivalence class in + [alias i j p]. *) +val alias : 'item -> 'item -> 'item partition -> 'item partition + +(** {1 Projection} *) + +(** The value of the call [repr i p] is [j] if the item [i] is in + the partition [p] and its representative is [j]. If [i] is not + in [p], then the value is [i]. *) +val repr : 'item -> 'item partition -> 'item + +(** The value of the call [get_or_set i p] is [j, p] if the item [i] is + in the partition [p] and its representative is [j]. If [i] is not + in [p], then the value is [i, p'], where p' is the partition [p] + extended with the fact that item [i] is a singleton partition. *) + +val get_or_set : 'item -> 'item t -> 'item * 'item t + +(** The value of the call [mem i p] is [Some j] if the item [i] is + in the partition [p] and its representative is [j]. If [i] is + not in [p], then the value is [None]. *) +val mem : 'item -> 'item partition -> 'item option + +(** The value of the call [elements p] is a list of the elements of p, + ordered in ascending order *) +val elements : 'item partition -> 'item list + +(** The value of the call [partitions p] is a list of the partitions + of p. A partition is a list of elements. The elements and + partitions are returned with a deterministic order (regardless of + the way the aliases have been made, the same partition will always + have the same order). *) +val partitions : 'item partition -> 'item list list + +(** The call [print p] is a value of type [Buffer.t] containing + strings denoting the partition [p], based on + [Ord.to_string]. *) +val print : Format.formatter -> 'item partition -> unit + +(** {1 Predicates} *) + +(** The value of [is_equiv i j p] is [true] if, and only if, the + items [i] and [j] belong to the same equivalence class in the + partition [p], that is, [i] and [j] have the same + representative. In particular, if either [i] or [j] do not + belong to [p], the value of [is_equiv i j p] is [false]. See + [mem] above. *) +val is_equiv : 'item -> 'item -> 'item partition -> bool diff --git a/vendors/ligo-utils/simple-utils/messages.sh b/vendors/ligo-utils/simple-utils/messages.sh index 418d09546..af46c9179 100755 --- a/vendors/ligo-utils/simple-utils/messages.sh +++ b/vendors/ligo-utils/simple-utils/messages.sh @@ -7,7 +7,7 @@ # specifications are located, in accordance with the convention of the # LIGO compiler source code. -#set -x +# set -x # ==================================================================== # General Settings and wrappers