Merge branch 'dev' of gitlab.com:ligolang/ligo into rinderknecht@pprint

.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

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)
 

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",
+            "@docusaurus/types": "^2.0.0-alpha.50",
-            "is-number": "^3.0.0",
+            "sitemap": "^3.2.2"
-            "repeat-string": "^1.6.1",
-            "to-regex-range": "^2.1.0"
           }
         },
         "find-up": {

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",

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;
+}

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;
+}

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; }

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 ];
+}

nix/mac-overlay.nix

@@ -0,0 +1,9 @@
+oself: osuper:
+let
+  fixHardeningWarning = pkg: pkg.overrideAttrs (_: {
+    hardeningDisable = [ "strictoverflow" ];
+  });
+in
+{
+  hacl = fixHardeningWarning osuper.hacl;
+}

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;
+}

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";
+        });
+      })
+    ]);
+}

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/
+  '';
+}

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;
+})

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/<owner>/<repo>/archive/<rev>.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/<owner>/<repo>/archive/<rev>.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/<owner>/<repo>/archive/<rev>.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<version>/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/<owner>/<repo>/archive/<rev>.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/<owner>/<repo>/archive/<rev>.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/<owner>/<repo>/archive/<rev>.tar.gz"
+    }
+}

nix/sources.nix

@@ -0,0 +1,134 @@
+# This file has been generated by Niv.
+
+let
+
+  #
+  # The fetchers. fetch_<type> fetches specs of type <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 <package> -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 <package> -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 = <nixpkgs> == ./.;
+    in
+      if builtins.hasAttr "nixpkgs" sources
+      then sourcesNixpkgs
+      else if hasNixpkgsPath && ! hasThisAsNixpkgsPath then
+        import <nixpkgs> {}
+      else
+        abort
+          ''
+            Please specify either <nixpkgs> (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); }

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 ];
+    });
+  });
+}

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")
+ )

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"

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"

src/bin/cli.ml

@@ -2,12 +2,7 @@ open Cmdliner
 open Trace
 open Cli_helpers
 
-let version =
+let version = Version.version
-  Format.asprintf
-    "Rolling release\nHash: %s\nDate: %s\nCI job id: %s"
-    Version.hash
-    Version.commit_date
-    Version.job_id
 
 let main =
   let man =

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)

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

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

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})]

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))
+)

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

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)
+let compile_expression ?(env = Ast_typed.Environment.full_empty) ~(state : Ast_typed.typer_state) (e : Ast_core.expression)
-    : (Ast_typed.expression * Typer.Solver.state) result =
+    : (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

src/passes/1-parser/cameligo/.gitignore

@@ -11,3 +11,6 @@ _build/*
 /Lexer.ml
 /LexToken.ml
 /Tests
+error.messages
+error.messages.new
+ParErr.ml

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}

src/passes/1-parser/pascaligo/.gitignore

@@ -11,3 +11,6 @@ _build/*
 /Lexer.ml
 /LexToken.ml
 /Tests
+error.messages
+error.messages.new
+ParErr.ml

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}

src/passes/1-parser/reasonligo/.gitignore

@@ -11,3 +11,6 @@ _build/*
 /Lexer.ml
 /LexToken.ml
 /Tests
+error.messages
+error.messages.new
+ParErr.ml

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}

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

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 TB_int)
-  | T_constant (TC_int) -> ok (T_base TC_int)
+  | T_constant (TC_nat)       -> ok (T_base TB_nat)
-  | T_constant (TC_nat) -> ok (T_base TC_nat)
+  | T_constant (TC_mutez)     -> ok (T_base TB_mutez)
-  | T_constant (TC_mutez) -> ok (T_base TC_mutez)
+  | T_constant (TC_string)    -> ok (T_base TB_string)
-  | T_constant (TC_string) -> ok (T_base TC_string)
+  | T_constant (TC_bytes)     -> ok (T_base TB_bytes)
-  | T_constant (TC_bytes) -> ok (T_base TC_bytes)
+  | T_constant (TC_address)   -> ok (T_base TB_address)
-  | T_constant (TC_address) -> ok (T_base TC_address)
+  | T_constant (TC_timestamp) -> ok (T_base TB_timestamp)
-  | T_constant (TC_timestamp) -> ok (T_base TC_timestamp)
+  | T_constant (TC_unit)      -> ok (T_base TB_unit)
-  | T_constant (TC_unit) -> ok (T_base TC_unit)
+  | T_constant (TC_operation) -> ok (T_base TB_operation)
-  | T_constant (TC_operation) -> ok (T_base TC_operation)
+  | T_constant (TC_signature) -> ok (T_base TB_signature)
-  | T_constant (TC_signature) -> ok (T_base TC_signature)
+  | T_constant (TC_key)       -> ok (T_base TB_key)
-  | T_constant (TC_key) -> ok (T_base TC_key)
+  | T_constant (TC_key_hash)  -> ok (T_base TB_key_hash)
-  | T_constant (TC_key_hash) -> ok (T_base TC_key_hash)
+  | T_constant (TC_chain_id)  -> ok (T_base TB_chain_id)
-  | T_constant (TC_chain_id) -> ok (T_base TC_chain_id)
+  | T_constant (TC_void)      -> ok (T_base TB_void)
-  | T_constant (TC_void)     -> ok (T_base TC_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") @@

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) @@

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 =

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")
+    | TB_unit -> fail (not_comparable "unit")
-    | TC_void -> fail (not_comparable "void")
+    | TB_void -> fail (not_comparable "void")
-    | TC_bool -> return bool_k
+    | TB_bool -> return bool_k
-    | TC_nat -> return nat_k
+    | TB_nat -> return nat_k
-    | TC_mutez -> return tez_k
+    | TB_mutez -> return tez_k
-    | TC_int -> return int_k
+    | TB_int -> return int_k
-    | TC_string -> return string_k
+    | TB_string -> return string_k
-    | TC_address -> return address_k
+    | TB_address -> return address_k
-    | TC_timestamp -> return timestamp_k
+    | TB_timestamp -> return timestamp_k
-    | TC_bytes -> return bytes_k
+    | TB_bytes -> return bytes_k
-    | TC_operation -> fail (not_comparable "operation")
+    | TB_operation -> fail (not_comparable "operation")
-    | TC_signature -> fail (not_comparable "signature")
+    | TB_signature -> fail (not_comparable "signature")
-    | TC_key -> fail (not_comparable "key")
+    | TB_key -> fail (not_comparable "key")
-    | TC_key_hash -> return key_hash_k
+    | TB_key_hash -> return key_hash_k
-    | TC_chain_id -> fail (not_comparable "chain_id")
+    | 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
+    | TB_unit -> return unit
-    | TC_void -> fail (not_compilable_type "void")
+    | TB_void -> fail (not_compilable_type "void")
-    | TC_bool -> return bool
+    | TB_bool -> return bool
-    | TC_int -> return int
+    | TB_int -> return int
-    | TC_nat -> return nat
+    | TB_nat -> return nat
-    | TC_mutez -> return tez
+    | TB_mutez -> return tez
-    | TC_string -> return string
+    | TB_string -> return string
-    | TC_address -> return address
+    | TB_address -> return address
-    | TC_timestamp -> return timestamp
+    | TB_timestamp -> return timestamp
-    | TC_bytes -> return bytes
+    | TB_bytes -> return bytes
-    | TC_operation -> return operation
+    | TB_operation -> return operation
-    | TC_signature -> return signature
+    | TB_signature -> return signature
-    | TC_key -> return key
+    | TB_key -> return key
-    | TC_key_hash -> return key_hash
+    | TB_key_hash -> return key_hash
-    | TC_chain_id -> return chain_id
+    | 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
+  | TB_unit -> ok @@ O.prim T_unit
-  | TC_void -> fail (Ty.not_compilable_type "void")
+  | TB_void -> fail (Ty.not_compilable_type "void")
-  | TC_bool -> ok @@ O.prim T_bool
+  | TB_bool -> ok @@ O.prim T_bool
-  | TC_int -> ok @@ O.prim T_int
+  | TB_int -> ok @@ O.prim T_int
-  | TC_nat -> ok @@ O.prim T_nat
+  | TB_nat -> ok @@ O.prim T_nat
-  | TC_mutez -> ok @@ O.prim T_mutez
+  | TB_mutez -> ok @@ O.prim T_mutez
-  | TC_string -> ok @@ O.prim T_string
+  | TB_string -> ok @@ O.prim T_string
-  | TC_address -> ok @@ O.prim T_address
+  | TB_address -> ok @@ O.prim T_address
-  | TC_timestamp -> ok @@ O.prim T_timestamp
+  | TB_timestamp -> ok @@ O.prim T_timestamp
-  | TC_bytes -> ok @@ O.prim T_bytes
+  | TB_bytes -> ok @@ O.prim T_bytes
-  | TC_operation -> ok @@ O.prim T_operation
+  | TB_operation -> ok @@ O.prim T_operation
-  | TC_signature -> ok @@ O.prim T_signature
+  | TB_signature -> ok @@ O.prim T_signature
-  | TC_key -> ok @@ O.prim T_key
+  | TB_key -> ok @@ O.prim T_key
-  | TC_key_hash -> ok @@ O.prim T_key_hash
+  | TB_key_hash -> ok @@ O.prim T_key_hash
-  | TC_chain_id -> ok @@ O.prim T_chain_id
+  | TB_chain_id -> ok @@ O.prim T_chain_id
 
 let rec type_ : type_value -> O.michelson result =
   function

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 () =

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

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

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

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

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

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

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"
+      | C_arrow        -> "arrow"
-      | Solver.Core.C_option       -> "option"
+      | C_option       -> "option"
-      | Solver.Core.C_record       -> failwith "record"
+      | C_record       -> failwith "record"
-      | Solver.Core.C_variant      -> failwith "variant"
+      | C_variant      -> failwith "variant"
-      | Solver.Core.C_map          -> "map"
+      | C_map          -> "map"
-      | Solver.Core.C_big_map      -> "big_map"
+      | C_big_map      -> "big_map"
-      | Solver.Core.C_list         -> "list"
+      | C_list         -> "list"
-      | Solver.Core.C_set          -> "set"
+      | C_set          -> "set"
-      | Solver.Core.C_unit         -> "unit"
+      | C_unit         -> "unit"
-      | Solver.Core.C_bool         -> "bool"
+      | C_string       -> "string"
-      | Solver.Core.C_string       -> "string"
+      | C_nat          -> "nat"
-      | Solver.Core.C_nat          -> "nat"
+      | C_mutez        -> "mutez"
-      | Solver.Core.C_mutez        -> "mutez"
+      | C_timestamp    -> "timestamp"
-      | Solver.Core.C_timestamp    -> "timestamp"
+      | C_int          -> "int"
-      | Solver.Core.C_int          -> "int"
+      | C_address      -> "address"
-      | Solver.Core.C_address      -> "address"
+      | C_bytes        -> "bytes"
-      | Solver.Core.C_bytes        -> "bytes"
+      | C_key_hash     -> "key_hash"
-      | Solver.Core.C_key_hash     -> "key_hash"
+      | C_key          -> "key"
-      | Solver.Core.C_key          -> "key"
+      | C_signature    -> "signature"
-      | Solver.Core.C_signature    -> "signature"
+      | C_operation    -> "operation"
-      | Solver.Core.C_operation    -> "operation"
+      | C_contract     -> "contract"
-      | Solver.Core.C_contract     -> "contract"
+      | C_chain_id     -> "chain_id"
-      | Solver.Core.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

src/passes/8-typer-new/dune

@@ -8,6 +8,7 @@
     ast_typed
     operators
     UnionFind
+    environment
   )
   (preprocess
     (pps ppx_let)

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
+open Ast_typed.Types
-
-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(α, …) *)
 
 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 , 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 , 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 {aval=(P_constant _ as a); bval=(P_forall _ as b)}   -> insert_fresh a b
-  | C_equation ((P_forall forall), (P_variable b))        -> gather_forall b forall
+  | C_equation {aval=(P_forall forall); bval=(P_variable b)}        -> gather_forall b forall
-  | C_equation (P_variable a, P_forall forall)            -> gather_forall a forall
+  | C_equation {aval=P_variable a; bval=P_forall forall}            -> gather_forall a forall
-  | C_equation (P_variable a, P_variable b)               -> gather_alias a b
+  | C_equation {aval=P_variable a; bval=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 {aval=P_variable a; bval=P_constant { p_ctor_tag; p_ctor_args }} -> split_constant a p_ctor_tag p_ctor_args
-  | C_equation (P_constant (c_tag , args), P_variable b)  -> split_constant b c_tag 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 {aval=(_ as a); bval=(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=(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_typeclass { tc_args; typeclass }                              -> split_typeclass tc_args typeclass
-  | C_access_label (tv, label, result)                    -> let _todo = ignore (tv, label, result) in failwith "TODO"
+  | 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_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 -> (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"
+      | T.C_arrow     -> "arrow"
-      | Core.C_option    -> "option"
+      | T.C_option    -> "option"
-      | Core.C_record    -> failwith "record"
+      | T.C_record    -> failwith "record"
-      | Core.C_variant   -> failwith "variant"
+      | T.C_variant   -> failwith "variant"
-      | Core.C_map       -> "map"
+      | T.C_map       -> "map"
-      | Core.C_big_map   -> "big_map"
+      | T.C_big_map   -> "big_map"
-      | Core.C_list      -> "list"
+      | T.C_list      -> "list"
-      | Core.C_set       -> "set"
+      | T.C_set       -> "set"
-      | Core.C_unit      -> "unit"
+      | T.C_unit      -> "unit"
-      | Core.C_bool      -> "bool"
+      | T.C_string    -> "string"
-      | Core.C_string    -> "string"
+      | T.C_nat       -> "nat"
-      | Core.C_nat       -> "nat"
+      | T.C_mutez     -> "mutez"
-      | Core.C_mutez     -> "mutez"
+      | T.C_timestamp -> "timestamp"
-      | Core.C_timestamp -> "timestamp"
+      | T.C_int       -> "int"
-      | Core.C_int       -> "int"
+      | T.C_address   -> "address"
-      | Core.C_address   -> "address"
+      | T.C_bytes     -> "bytes"
-      | Core.C_bytes     -> "bytes"
+      | T.C_key_hash  -> "key_hash"
-      | Core.C_key_hash  -> "key_hash"
+      | T.C_key       -> "key"
-      | Core.C_key       -> "key"
+      | T.C_signature -> "signature"
-      | Core.C_signature -> "signature"
+      | T.C_operation -> "operation"
-      | Core.C_operation -> "operation"
+      | T.C_contract  -> "contract"
-      | Core.C_contract  -> "contract"
+      | T.C_chain_id  -> "chain_id"
-      | Core.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 (<?) ca cb =
@@ -550,7 +502,7 @@ let rec compare_list f = function
   | [] -> (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 <? fun () -> compare_list compare_type_expression a2 b2
+      | P_constant { p_ctor_tag=b1; p_ctor_args=b2 } -> compare_simple_c_constant a1 b1 <? fun () -> 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 <? fun () -> compare_type_expression a2 b2)
+      | P_apply { tf=b1; targ=b2 } -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2)
 and compare_type_constraint = function
-  | C_equation (a1, a2) -> (function
+  | C_equation { aval=a1; bval=a2 } -> (function
-      | C_equation (b1, b2) -> compare_type_expression a1 b1 <? fun () -> compare_type_expression a2 b2
+      | C_equation { aval=b1; bval=b2 } -> compare_type_expression a1 b1 <? fun () -> 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 <? fun () -> compare_typeclass a2 b2
+      | C_typeclass { tc_args=b1; typeclass=b2 } -> compare_list compare_type_expression a1 b1 <? fun () -> 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 <? fun () -> compare_label a2 b2  <? fun () -> 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 <? fun () -> compare_label a2 b2  <? fun () -> 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 <? fun () -> 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
+  let select_and_propagate : ('old_input, 'selector_output) selector -> _ propagator -> _ -> 'a -> structured_dbs -> _ * new_constraints * new_assignments =
-  module AlreadySelected = Set.Make(BlaBla)
+    let mem elt set = match RedBlackTrees.PolySet.find_opt elt set with None -> false | Some _ -> true in
-
-  let select_and_propagate : ('old_input, 'selector_output) selector -> BlaBla.t propagator -> _ -> 'a -> structured_dbs -> _ * new_constraints * new_assignments =
     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)
+let select_and_propagate_break_ctor = select_and_propagate selector_break_ctor propagator_break_ctor
-module M_specialize1 = M(OutputSpecialize1)
+let select_and_propagate_specialize1 = select_and_propagate selector_specialize1 propagator_specialize1
-
-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 ;
-}
 
 (* 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 = {
+let initial_state : typer_state = (* {
-  structured_dbs   : structured_dbs   ;
-  already_selected : already_selected ;
-}
-
-let initial_state : 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 *)
+    aliases = UF.empty (fun s -> Format.asprintf "%a" Var.pp s) Var.compare ; (* unionfind *)
-    assignments = TypeVariableMap.empty; (* c_constructor_simpl TypeVariableMap.t *)
+    assignments = Map.create ~cmp:Var.compare; (* c_constructor_simpl TypeVariableMap.t *)
-    grouped_by_variable = TypeVariableMap.empty; (* constraints 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 ;
+    break_ctor = Set.create ~cmp:compare_output_break_ctor;
-    specialize1 = M_specialize1.AlreadySelected.empty ;
+    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

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

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 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 : Solver.state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
+  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 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, program) = type_xyz_returns_state env_state_node in
+  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
+          (Map.find_opt root assignments) in
-      let Solver.{ tv ; c_tag ; tv_list } = assignment 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 type_program (p : I.program) : (O.program * O.typer_state) result =
-  let empty_env = Ast_typed.Environment.full_empty in
+  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
+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 -> Solver.state -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> (O.matching_expr * Solver.state) result = type_match
+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_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 * 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_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 * Solver.state) result = type_program p
+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 * Solver.state * I.expression) -> (environment * Solver.state * O.expression) Trace.result = type_expression_returns_state
+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 : 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_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

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_program : I.program -> (O.program * O.typer_state) result
-val type_declaration : environment -> Solver.state -> I.declaration -> (environment * Solver.state * O.declaration option) 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 : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result
-val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.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

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),[])

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 (P_variable whole_expr) sum ;
-    C_equation (t_arg , c_arg)
+    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 list = collection T.C_list
-let set  = collection O.C_set
+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 k_type = T.P_variable (Core.fresh_type_variable ()) in
-  let v_type = O.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 k_type = T.P_variable (Core.fresh_type_variable ()) in
-  let v_type = O.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 ds' (p_constant C_map [ind' ; P_variable v]) ;
-      C_equation (P_variable whole_expr , P_constant (C_option , [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 a' (p_constant C_unit []) ;
-      C_equation (b' , P_variable whole_expr)
+      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 expr'                   (P_variable (Stage_common.Constant.t_bool)) ;
-      C_equation (body'                 , P_constant (C_unit , [])) ;
+      c_equation body'                   (p_constant C_unit []) ;
-      C_equation (P_variable whole_expr , 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 v'  e' ;
-      C_equation (P_variable whole_expr , P_constant (C_unit , []))
+      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' annot' ;
-      C_equation (e' , P_variable whole_expr)
+      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)]
+    | Some body -> [c_equation (P_variable unification_body) (type_expression_to_type_value body)]
-  in O.[
+  in [
-      C_equation (type_expression_to_type_value fresh , P_variable unification_arg) ;
+      c_equation (type_expression_to_type_value fresh) (P_variable unification_arg) ;
-      C_equation (P_variable whole_expr ,
+      c_equation (P_variable whole_expr)
-                  P_constant (C_arrow , [P_variable unification_arg ;
+                 (p_constant C_arrow ([P_variable unification_arg ;
-                                         P_variable unification_body]))
+                                       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
+  let args_tuple = p_constant C_record args' in
-  O.[
+  [
-      C_equation (f , P_constant (C_arrow , [args_tuple ; P_variable whole_expr]))
+      c_equation f (p_constant C_arrow ([args_tuple ; P_variable whole_expr]))
   ] , whole_expr

src/passes/8-typer-old/dune

@@ -8,6 +8,7 @@
     ast_typed
     typer_new
     operators
+    environment
   )
   (preprocess
     (pps ppx_let)

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),[])

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_program : I.program -> (O.program * O.typer_state) result
-val type_declaration : environment -> Solver.state -> I.declaration -> (environment * Solver.state * O.declaration option) 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

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_program : I.program -> (O.program * O.typer_state) result
-val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * Solver.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

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

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

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

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

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 _ ->

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,())

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

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
 

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 _ ->

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

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

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}
 

src/stages/3-ast_core/PP.ml

@@ -76,8 +76,6 @@ and matching : type a . (formatter -> a -> unit) -> formatter -> (a,unit) matchi
         fprintf ppf "@[<hv>| (%a) ->@;<1 2>%a@]" (list_sep_d expression_variable) lst f b
     | Match_variant (lst, _) ->
         fprintf ppf "@[<hv>%a@]" (list_sep (matching_variant_case f) (tag "@ ")) lst
-    | Match_bool {match_true ; match_false} ->
-        fprintf ppf "@[<hv>| 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 "@[<hv>| 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 _ ->

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

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

src/stages/4-ast_typed/.gitignore

@@ -0,0 +1,2 @@
+/generated_fold.ml
+

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=_}} ->

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 "{@,@[<hv 2> %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 [@,@[<hv 2> %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 [@,@[<hv 2> %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 "[@,@[<hv 2> %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 "[@,@[<hv 2> %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 "[@,@[<hv 2> (*%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 [@,@[<hv 2> %a @]@,]" aux2 lst);
+    poly_set                  = (fun _visitor continue () set   ->
+      let lst = (RedBlackTrees.PolySet.elements set) in
+      fprintf ppf "Set [@,@[<hv 2> %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 [@,@[<hv 2> %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
+include Fold.Folds(struct
-let type_expression = print fold__type_expression
+  type state = unit ;;
+  type 'a t = formatter -> 'a -> unit ;;
+  let f = print ;;
+end)

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

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"
 
 

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

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)

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", []

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_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 _ )
         -> 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
@@ -532,3 +528,11 @@ let equal_variables a b : bool =
   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 }

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

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

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 ;
+}

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)

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 =
+and type_constant ppf (tb:type_base) : unit =
-  let s = match tc with 
+  let s = match tb with 
-    | TC_unit      -> "unit"
+    | TB_unit      -> "unit"
-    | TC_string    -> "string"
+    | TB_string    -> "string"
-    | TC_bytes     -> "bytes"
+    | TB_bytes     -> "bytes"
-    | TC_nat       -> "nat"
+    | TB_nat       -> "nat"
-    | TC_int       -> "int"
+    | TB_int       -> "int"
-    | TC_mutez     -> "mutez"
+    | TB_mutez     -> "mutez"
-    | TC_bool      -> "bool"
+    | TB_bool      -> "bool"
-    | TC_operation -> "operation"
+    | TB_operation -> "operation"
-    | TC_address   -> "address"
+    | TB_address   -> "address"
-    | TC_key       -> "key"
+    | TB_key       -> "key"
-    | TC_key_hash  -> "key_hash"
+    | TB_key_hash  -> "key_hash"
-    | TC_signature -> "signature"
+    | TB_signature -> "signature"
-    | TC_timestamp -> "timestamp"
+    | TB_timestamp -> "timestamp"
-    | TC_chain_id  -> "chain_id"
+    | TB_chain_id  -> "chain_id"
-    | TC_void      -> "void"
+    | 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{|

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_int  : type_value = T_base TB_int
-let t_unit : type_value = T_base TC_unit
+let t_unit : type_value = T_base TB_unit
-let t_nat : type_value = T_base TC_nat
+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 )

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

src/stages/adt_generator/adt_generator.ml

@@ -1 +1,2 @@
 module Generic = Generic
+module Common = Common

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;;

src/stages/adt_generator/dune

@@ -2,5 +2,6 @@
   (name adt_generator)
   (public_name ligo.adt_generator)
   (libraries
+    simple-utils
   )
 )

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 "open Adt_generator.Common;;";
-say "let (>>?) v f = Simple_utils.Trace.bind f v;;";
-say "let return v = Simple_utils.Trace.ok v;;";
 say "open $moduleName;;";
 
 say "";
 say "(* must be provided by one of the open or include statements: *)";
 for $adts.grep({$_<kind> ne $record && $_<kind> ne $variant}).map({$_<kind>}).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<name> = \{";
+    say "type ('state, 'err) _continue_fold_map__$t<name> = \{";
-        say "    node__$t<name> : 'state -> $t<name> -> ('state * $t<newName>) monad ;";
+        say "    node__$t<name> : 'state -> $t<name> -> ('state * $t<newName> , 'err) monad ;";
     for $t<ctorsOrFields>.list -> $c
-    { say "    $t<name>__$c<name> : 'state -> {$c<type> || 'unit'} -> ('state * {$c<newType> || 'unit'}) monad ;" }
+    { say "    $t<name>__$c<name> : 'state -> {$c<type> || 'unit'} -> ('state * {$c<newType> || 'unit'} , 'err) monad ;" }
     say '  };;';
 }
 
-say "type 'state continue_fold_map = \{";
+say "type ('state , 'err) _continue_fold_map__$moduleName = \{";
 for $adts.list -> $t {
-    say "    $t<name> : 'state continue_fold_map__$t<name> ;";
+    say "    $t<name> : ('state , 'err) _continue_fold_map__$t<name> ;";
 }
 say '  };;';
 
 say "";
 for $adts.list -> $t
-{ say "type 'state fold_map_config__$t<name> = \{";
+{ say "type ('state, 'err) fold_map_config__$t<name> = \{";
-  say "    node__$t<name> : 'state -> $t<name> -> 'state continue_fold_map -> ('state * $t<newName>) monad ;"; # (*Adt_info.node_instance_info ->*)
+  say "    node__$t<name> : 'state -> $t<name> -> ('state, 'err) _continue_fold_map__$moduleName -> ('state * $t<newName> , 'err) monad ;"; # (*Adt_info.node_instance_info ->*)
-  say "    node__$t<name>__pre_state : 'state -> $t<name> -> 'state monad ;"; # (*Adt_info.node_instance_info ->*)
+  say "    node__$t<name>__pre_state : 'state -> $t<name> -> ('state, 'err) monad ;"; # (*Adt_info.node_instance_info ->*)
-  say "    node__$t<name>__post_state : 'state -> $t<name> -> $t<newName> -> 'state monad ;"; # (*Adt_info.node_instance_info ->*)
+  say "    node__$t<name>__post_state : 'state -> $t<name> -> $t<newName> -> ('state, 'err) monad ;"; # (*Adt_info.node_instance_info ->*)
   for $t<ctorsOrFields>.list -> $c
-  { say "    $t<name>__$c<name> : 'state -> {$c<type> || 'unit'} -> 'state continue_fold_map -> ('state * {$c<newType> || 'unit'}) monad ;"; # (*Adt_info.ctor_or_field_instance_info ->*)
+  { say "    $t<name>__$c<name> : 'state -> {$c<type> || 'unit'} -> ('state, 'err) _continue_fold_map__$moduleName -> ('state * {$c<newType> || '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<name> : 'state fold_map_config__$t<name>;" }
+{ say "    $t<name> : ('state, 'err) fold_map_config__$t<name>;" }
 say '  };;';
 
-say "";
+say "include Adt_generator.Generic.BlahBluh";
-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 "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 "type ('state, 'err) mk_continue_fold_map = \{";
-say "  fn : 'state mk_continue_fold_map -> 'state fold_map_config -> 'state 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<name> : type qstate . qstate mk_continue_fold_map -> qstate fold_map_config -> qstate -> $t<name> -> (qstate * $t<newName>) monad = fun mk_continue_fold_map visitor state x ->";
+{ say "let _fold_map__$t<name> : type qstate err . (qstate,err) mk_continue_fold_map -> (qstate,err) fold_map_config__$moduleName -> qstate -> $t<name> -> (qstate * $t<newName>, err) 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 continue_fold_map : (qstate,err) _continue_fold_map__$moduleName = mk_continue_fold_map.fn mk_continue_fold_map visitor in";
   say "  visitor.$t<name>.node__$t<name>__pre_state state x >>? fun state ->"; # (*(fun () -> whole_adt_info, info__$t<name>)*)
   say "  visitor.$t<name>.node__$t<name> state x continue_fold_map >>? fun (state, new_x) ->"; # (*(fun () -> whole_adt_info, info__$t<name>)*)
   say "  visitor.$t<name>.node__$t<name>__post_state state x new_x >>? fun state ->"; # (*(fun () -> whole_adt_info, info__$t<name>)*)
   say "  return (state, new_x);;";
   say "";
   for $t<ctorsOrFields>.list -> $c
-  { say "let _fold_map__$t<name>__$c<name> : type qstate . qstate mk_continue_fold_map -> qstate fold_map_config -> qstate -> { $c<type> || 'unit' } -> (qstate * { $c<newType> || 'unit' }) monad = fun mk_continue_fold_map visitor state x ->";
+  { say "let _fold_map__$t<name>__$c<name> : type qstate err . (qstate,err) mk_continue_fold_map -> (qstate,err) fold_map_config__$moduleName -> qstate -> { $c<type> || 'unit' } -> (qstate * { $c<newType> || 'unit' }, err) 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 continue_fold_map : (qstate,err) _continue_fold_map__$moduleName = mk_continue_fold_map.fn mk_continue_fold_map visitor in";
     say "  visitor.$t<name>.$t<name>__$c<name> state x continue_fold_map;;"; # (*(fun () -> whole_adt_info, info__$t<name>, info__$t<name>__$c<name>)*)
     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<name> = \{";
@@ -410,16 +403,16 @@ say "";
 # fold_map functions : tying the knot
 say "";
 for $adts.list -> $t
-{ say "let fold_map__$t<name> : type qstate . qstate fold_map_config -> qstate -> $t<name> -> (qstate * $t<newName>) monad =";
+{ say "let fold_map__$t<name> : type qstate err . (qstate,err) fold_map_config__$moduleName -> qstate -> $t<name> -> (qstate * $t<newName>,err) monad =";
   say "  fun visitor state x -> _fold_map__$t<name> mk_continue_fold_map visitor state x;;";
   for $t<ctorsOrFields>.list -> $c
-  { say "let fold_map__$t<name>__$c<name> : type qstate . qstate fold_map_config -> qstate -> { $c<type> || 'unit' } -> (qstate * { $c<newType> || 'unit' }) monad =";
+  { say "let fold_map__$t<name>__$c<name> : type qstate err . (qstate,err) fold_map_config__$moduleName -> qstate -> { $c<type> || 'unit' } -> (qstate * { $c<newType> || 'unit' },err) monad =";
     say "  fun visitor state x -> _fold_map__$t<name>__$c<name> mk_continue_fold_map visitor state x;;"; } }
 
 
 for $adts.list -> $t
 {
-   say "let no_op_node__$t<name> : type state . state -> $t<name> -> state continue_fold_map -> (state * $t<newName>) monad =";
+   say "let no_op_node__$t<name> : type state . state -> $t<name> -> (state,_) _continue_fold_map__$moduleName -> (state * $t<newName>,_) monad =";
   say "  fun state v continue ->"; # (*_info*)
   say "    match v with";
   if ($t<kind> eq $variant) {
@@ -446,7 +439,7 @@ for $adts.list -> $t
 }
 
 for $adts.list -> $t
-{ say "let no_op__$t<name> : type state . state fold_map_config__$t<name> = \{";
+{ say "let no_op__$t<name> : type state . (state,_) fold_map_config__$t<name> = \{";
   say "  node__$t<name> = no_op_node__$t<name>;";
   say "  node__$t<name>__pre_state = (fun state v -> ignore v; return state) ;"; # (*_info*)
   say "  node__$t<name>__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<name> = no_op__$t<name>;" }
 say '};;';
 
 say "";
 for $adts.list -> $t
-{ say "let with__$t<name> : _ -> _ fold_map_config -> _ fold_map_config = (fun node__$t<name> op -> \{ op with $t<name> = \{ op.$t<name> with node__$t<name> \} \});;";
+{ say "let with__$t<name> : _ -> _ fold_map_config__$moduleName -> _ fold_map_config__$moduleName = (fun node__$t<name> op -> \{ op with $t<name> = \{ op.$t<name> with node__$t<name> \} \});;";
-  say "let with__$t<name>__pre_state : _ -> _ fold_map_config -> _ fold_map_config = (fun node__$t<name>__pre_state op -> \{ op with $t<name> = \{ op.$t<name> with node__$t<name>__pre_state \} \});;";
+  say "let with__$t<name>__pre_state : _ -> _ fold_map_config__$moduleName -> _ fold_map_config__$moduleName = (fun node__$t<name>__pre_state op -> \{ op with $t<name> = \{ op.$t<name> with node__$t<name>__pre_state \} \});;";
-  say "let with__$t<name>__post_state : _ -> _ fold_map_config -> _ fold_map_config = (fun node__$t<name>__post_state op -> \{ op with $t<name> = \{ op.$t<name> with node__$t<name>__post_state \} \});;";
+  say "let with__$t<name>__post_state : _ -> _ fold_map_config__$moduleName -> _ fold_map_config__$moduleName = (fun node__$t<name>__post_state op -> \{ op with $t<name> = \{ op.$t<name> with node__$t<name>__post_state \} \});;";
   for $t<ctorsOrFields>.list -> $c
-  { say "let with__$t<name>__$c<name> : _ -> _ fold_map_config -> _ fold_map_config = (fun $t<name>__$c<name> op -> \{ op with $t<name> = \{ op.$t<name> with $t<name>__$c<name> \} \});;"; } }
+  { say "let with__$t<name>__$c<name> : _ -> _ fold_map_config__$moduleName -> _ fold_map_config__$moduleName = (fun $t<name>__$c<name> op -> \{ op with $t<name> = \{ op.$t<name> with $t<name>__$c<name> \} \});;"; } }
+
+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<name> = M.f fold__$t<name>;;"; }
+say "end";

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

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

src/stages/common/constant.ml

@@ -0,0 +1,2 @@
+open Types
+let t_bool : type_variable = Var.of_name "bool"

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;

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"

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 _ ->
+        | T.T_arrow { type1; type2 } ->
-          let _TODO = substs in
+           let%bind type1 = s_type_expression ~substs type1 in
-          failwith "TODO: T_function"
+           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 -> (
+      | P_apply { tf; targ } -> (
-          let ab' = pair_map self ab in
+          P_apply { tf = self tf ; targ = self targ }
-          P_apply ab'
         )
       | 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 -> (
+      | C_equation { aval; bval } -> (
-          let ab' = pair_map (fun tv -> type_value ~tv ~substs) ab in
+        let aux tv = type_value ~tv ~substs in
-          C_equation ab'
+          C_equation { aval = aux aval ; bval = aux bval }
         )
-      | C_typeclass (tvs , tc) -> (
+      | C_typeclass { tc_args; typeclass=tc } -> (
-          let tvs' = List.map (fun tv -> type_value ~tv ~substs) tvs in
+          let tc_args = List.map (fun tv -> type_value ~tv ~substs) tc_args in
-          let tc' = typeclass ~tc ~substs in
+          let tc = typeclass ~tc ~substs in
-          C_typeclass (tvs' , tc')
+          C_typeclass {tc_args ; typeclass=tc}
         )
-      | C_access_label (tv , l , v') -> (
+      | C_access_label { c_access_label_tval; accessor; c_access_label_tvar } -> (
-          let tv' = type_value ~tv ~substs in
+          let c_access_label_tval = type_value ~tv:c_access_label_tval ~substs in
-          C_access_label (tv' , l , v')
+          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) ->
+        P_apply {tf = P_forall { binder; constraints; body }; targ} ->
-        let constraints = List.map (fun c -> constraint_ ~c ~substs:(mk_substs ~v:binder ~expr:arg)) constraints in
+        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:arg) , constraints)
+        (type_value ~tv:body ~substs:(mk_substs ~v:binder ~expr:targ) , constraints)
       | _ -> (tv , [])
   end
 

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 =
+let tc type_vars allowed_list : type_constraint =
-  Core.C_typeclass (type_vars , allowed_list)
+  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 (-->) arg ret = p_constant C_arrow     [arg; ret]
-let option t  = P_constant (C_option  , [t])
+let option t      = p_constant C_option    [t]
-let pair a b  = P_constant (C_record , [a; b])
+let pair a b      = p_constant C_record    [a; b]
-let sum  a b  = P_constant (C_variant, [a; b])
+let sum  a b      = p_constant C_variant   [a; b]
-let map  k v  = P_constant (C_map   , [k; v])
+let map  k v      = p_constant C_map       [k; v]
-let unit      = P_constant (C_unit    , [])
+let unit          = p_constant C_unit      []
-let list   t  = P_constant (C_list    , [t])
+let list   t      = p_constant C_list      [t]
-let set    t  = P_constant (C_set     , [t])
+let set    t      = p_constant C_set       [t]
-let bool      = P_constant (C_bool    , [])
+let bool          = P_variable Stage_common.Constant.t_bool
-let string    = P_constant (C_string  , [])
+let string        = p_constant C_string    []
-let nat       = P_constant (C_nat     , [])
+let nat           = p_constant C_nat       []
-let mutez     = P_constant (C_mutez  , [])
+let mutez         = p_constant C_mutez     []
-let timestamp = P_constant (C_timestamp , [])
+let timestamp     = p_constant C_timestamp []
-let int       = P_constant (C_int     , [])
+let int           = p_constant C_int       []
-let address   = P_constant (C_address , [])
+let address       = p_constant C_address   []
-let chain_id  = P_constant (C_chain_id , [])
+let chain_id      = p_constant C_chain_id  []
-let bytes     = P_constant (C_bytes   , [])
+let bytes         = p_constant C_bytes     []
-let key       = P_constant (C_key     , [])
+let key           = p_constant C_key       []
-let key_hash  = P_constant (C_key_hash  , [])
+let key_hash      = p_constant C_key_hash  []
-let signature = P_constant (C_signature , [])
+let signature     = p_constant C_signature []
-let operation = P_constant (C_operation , [])
+let operation     = p_constant C_operation []
-let contract t = P_constant (C_contract , [t])
+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 tuple0        = p_constant C_record    []
-let tuple1 a     = P_constant (C_record , [a])
+let tuple1 a      = p_constant C_record    [a]
-let tuple2 a b   = P_constant (C_record , [a; b])
+let tuple2 a b    = p_constant C_record    [a; b]
-let tuple3 a b c = P_constant (C_record , [a; b; c])
+let tuple3 a b c  = p_constant C_record    [a; b; c]

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)