Merge remote-tracking branch 'origin/georges-bash-security-and-error-detection' into feature/#3-add-odoc-to-website

.gitlab-ci.yml

@@ -72,18 +72,13 @@ stages:
     # Install dependencies
     # rsync is needed by opam to sync a package installed from a local directory with the copy in ~/.opam
     - apt-get update -qq
-    - apt-get -y -qq install rsync libhidapi-dev libcap-dev libev-dev bubblewrap
+    - scripts/install_native_dependencies.sh
-    - wget https://github.com/ocaml/opam/releases/download/2.0.1/opam-2.0.1-x86_64-linux -O opam-2.0.1-x86_64-linux
+    - scripts/install_opam.sh
-    - cp opam-2.0.1-x86_64-linux /usr/local/bin/opam
-    - chmod +x /usr/local/bin/opam
     - export PATH="/usr/local/bin${PATH:+:}${PATH:-}"
 
-    # Initialise opam
+    # Initialise opam, create switch, load opam environment variables
     - printf '' | opam init --bare
-    - eval $(opam config env)
+    - printf '' | opam switch create ligo-switch ocaml-base-compiler.4.06.1
-
-    # Create switch
-    - printf '' | opam switch create toto ocaml-base-compiler.4.06.1
     - eval $(opam config env)
 
     # Show versions and current switch
@@ -96,8 +91,7 @@ local-dune-job:
   <<: *before_script
   stage: test
   script:
-    - vendors/opam-repository-tools/rewrite-local-opam-repository.sh
+    - scripts/setup_ligo_opam_repository.sh
-    - opam repository add localrepo "file://$PWD/vendors/ligo-opam-repository-local-generated/"
     - opam install -y --build-test --deps-only ./src/
     - dune build -p ligo
     # TODO: also try instead from time to time:

Makefile

@@ -0,0 +1,3 @@
+build-deps:
+	scripts/install_native_dependencies.sh
+	scripts/install_opam.sh

docker/Dockerfile

@@ -16,12 +16,12 @@ ADD . /ligo
 # the upcoming scripts
 WORKDIR /ligo
 
-# Setup a custom opam repository where ligo is published
-RUN sh scripts/setup_ligo_opam_repository.sh
-
 # Install required native dependencies
 RUN sh scripts/install_native_dependencies.sh
 
+# Setup a custom opam repository where ligo is published
+RUN sh scripts/setup_ligo_opam_repository.sh
+
 RUN opam update
 
 # Install ligo

gitlab-pages/docs/language-basics-entrypoints.md

@@ -8,7 +8,7 @@ title: Entrypoints
 <!--DOCUSAURUS_CODE_TABS-->
 <!--Pascaligo-->
 ```Pascal
-function main (const p : int ; const s : int) : (list(operation) * unit) is
+function main (const p : int ; const s : int) : (list(operation) * int) is
   block {skip} with ((nil : list(operation)), s + 1)
 ```
 <!--END_DOCUSAURUS_CODE_TABS-->

scripts/build_docker_image.sh

@@ -1 +1,4 @@
+#!/bin/sh
+set -e
+
 docker build -t ligolang/ligo -f docker/Dockerfile .

scripts/install_ligo_with_dependencies.sh

@@ -1 +1,5 @@
-cd src && opam install . --yes
+#!/bin/sh
+set -e
+
+cd src
+opam install . --yes

scripts/install_native_dependencies.sh

@@ -1,8 +1,14 @@
+#!/bin/sh
+set -e
+
 apt-get update -qq
-apt-get -y install \
+apt-get -y -qq install \
     libev-dev \
     perl \
     pkg-config \
     libgmp-dev \
     libhidapi-dev \
-    m4
+    m4 \
+    libcap-dev \
+    bubblewrap \
+    rsync

scripts/install_opam.sh

@@ -0,0 +1,10 @@
+#!/bin/sh
+set -e
+
+# TODO: this has many different modes of failure (file temp.opam-2.0.1-x86_64-linux.download-in-progress already exists, /usr/local/bin/opam already exists and is a directory or hard link, …)
+# Try to improve these aspects.
+
+wget https://github.com/ocaml/opam/releases/download/2.0.1/opam-2.0.1-x86_64-linux -O temp.opam-2.0.1-x86_64-linux.download-in-progress
+cp -i temp.opam-2.0.1-x86_64-linux.download-in-progress /usr/local/bin/opam
+chmod +x /usr/local/bin/opam
+rm temp.opam-2.0.1-x86_64-linux.download-in-progress

scripts/installer.sh

@@ -1,31 +1,96 @@
-#!/bin/bash
+#!/bin/sh
+set -e
+
 # You can run this installer like this:
 # curl https://gitlab.com/ligolang/ligo/blob/master/scripts/installer.sh | bash
 # Make sure the marigold/ligo image is published at docker hub first
-set -euET -o pipefail
+
+if test $# -ne 1; then
+  printf 'Usage: installer.sh VERSION'\\n
+  printf \\n
+  printf '  where VERSION can be "next" or a version number like 1.0.0'\\n
+  exit 1
+else
   version=$1
-printf "\nInstalling LIGO ($version)\n\n"
+  printf \\n'Installing LIGO (%s)'\\n\\n "$version"
 
   if [ $version = "next" ]
   then
     # Install the ligo.sh from master
-        wget https://gitlab.com/ligolang/ligo/raw/dev/scripts/ligo.sh
+    url=https://gitlab.com/ligolang/ligo/raw/dev/scripts/ligo.sh
   else
     # Install the ligo.sh from master
-        wget https://gitlab.com/ligolang/ligo/raw/master/scripts/ligo.sh
+    url=https://gitlab.com/ligolang/ligo/raw/master/scripts/ligo.sh
   fi
 
-
-# Overwrite LIGO version in the executable
-sed -i '' "s/latest/$version/g" ligo.sh
-
-# Copy the exucutable to the appropriate directory
-sudo cp ligo.sh /usr/local/bin/ligo
-sudo chmod +x /usr/local/bin/ligo
-rm ligo.sh
-
   # Pull the docker image used by ligo.sh
   docker pull "ligolang/ligo:$version"
 
+  # Install ligo.sh
+  # Rationale behind this part of the script:
+  # * mv is one of the few commands which is atomic
+  #   * therefore we will create a file with the desired contents, and if that works, atomically mv it.
+  #     If something goes wrong it will attempt to remove the temporary file
+  #     (if removing the temporary file fails it's not a big deal due to the fairly explicit file name,
+  #      the fact that it is hidden, and its small size)
+  # * most utilities (e.g. touch) don't explicitly state that they support umask in their man page
+  #   * therefore we try to set the mode for the temporary file with an umask + do a chmod just to be sure
+  #   * this leaves open a race condition where:
+  #     0) umask isn't applied by touch (e.g. the file already exists)
+  #     1) for some reason touch creates an executable file (e.g. the file already exists)
+  #     2) a user grabs the file while it is executable, and triggers its execution (the process is created but execution of the script doesn't start yet)
+  #     3) chmod makes it non-executable
+  #     4) the file is partially written
+  #     5) the execution actually starts, and executes a prefix of the desired command, and that prefix is usable for adverse effects
+  #     To mitigate this, we wrap the command in the script with
+  #         if true; then the_command; fi
+  #     That way, the shell will raise an error due to a missing "fi" if the script executed while it is partially written
+  #   * This still leaves open the same race condition where a propper prefix of #!/bin/sh\nif can be used to adverse effect, but there's not much we can do about this.
+  # * after the file is completely written, we make it executable
+  # * we then check for the cases where `mv` misbehaves
+  # * we then atomically move it to (hopefully) its destination
+  # * the main risks here are if /usr/local/bin/ is writable by hostile users on the same machine (then there are bigger problems than what is our concern)
+  #   or if root itself tries to create a race condition (then there are bigger problems than what is our concern)
+
+  # It's hard to place comments inside a sequence of commands, so here are the comments for the following code:
+  # wget     download to stdout
+  # | sudo   become root (sudo) for the rest of the commands
+  #   (      subshell (to clean up temporary file if anything goes wrong)
+  #          remove temporary file in case it already exists
+  #   &&     create temporary file with (hopefully) the right permissions
+  #   &&     fix permisisons in case the creation didn't take umask into account
+  #   &&     redirect the output of the wget download to the temporary file
+  #   ) ||   clean up temporary file if any command in the previous block failed
+
+  wget "$url" -O - \
+  | sed -e "s/next/$version/g" \
+  | sudo sh -c ' \
+    ( \
+      rm -f /usr/local/bin/.temp.ligo.before-atomic-move \
+      && (umask 0600 > /dev/null 2>&1; UMASK=0600 touch /usr/local/bin/.temp.ligo.before-atomic-move) \
+      && chmod 0600 /usr/local/bin/.temp.ligo.before-atomic-move \
+      && cat > /usr/local/bin/.temp.ligo.before-atomic-move \
+    ) || (rm /usr/local/bin/.temp.ligo.before-atomic-move; exit 1)'
+
+  # sudo     become root (sudo) for the rest of the commands
+  #   (      subshell (to clean up temporary file if anything goes wrong)
+  #   &&     check that the download seems complete (one can't rely on sigpipe & failures to correctly stop the sudo session in case the download fails)
+  #   &&     overwite LIGO version in the executable
+  #   &&     now that the temporary file is complete, make it executable
+  #   && if  check for some corner cases: destination exists and is a directory
+  #   elif   check for some corner cases: destination exists and is symbolic link
+  #   else   atomically (hopefully) move temporary file to its destination
+  #   ) ||   clean up temporary file if any command in the previous block failed
+
+  sudo sh -c ' \
+    ( \
+         grep "END OF DOWNLOADED FILE" /usr/local/bin/.temp.ligo.before-atomic-move \
+      && chmod 0755 /usr/local/bin/.temp.ligo.before-atomic-move \
+      && if test -d /usr/local/bin/ligo; then printf "/usr/local/bin/ligo already exists and is a directory, cancelling installation"'\\\\'n; rm /usr/local/bin/.temp.ligo.before-atomic-move; \
+         elif test -L /usr/local/bin/ligo; then printf "/usr/local/bin/ligo already exists and is a symbolic link, cancelling installation"'\\\\'n; rm /usr/local/bin/.temp.ligo.before-atomic-move; \
+         else mv -i /usr/local/bin/.temp.ligo.before-atomic-move /usr/local/bin/ligo; fi \
+    ) || (rm /usr/local/bin/.temp.ligo.before-atomic-move; exit 1)'
+
   # Installation finished, try running 'ligo' from your CLI
-printf "\nInstallation successful, try to run 'ligo --help' now.\n"
+  printf \\n'Installation successful, try to run '\''ligo --help'\'' now.'\\n
+fi

scripts/ligo.sh

@@ -1,2 +1,10 @@
-#!/bin/bash
+#!/bin/sh
-docker run -it -v "$PWD":"$PWD" -w "$PWD" ligolang/ligo:latest "$@"
+set -e
+if [ test "x$PWD" = "x" ]; then
+  echo "Cannot detect the current directory, the environment variable PWD is empty."
+  exit 1
+else
+  docker run -it -v "$PWD":"$PWD" -w "$PWD" ligolang/ligo:next "$@"
+fi
+# Do not remove the next line. It is used as an approximate witness that the download of this file was complete. This string should not appear anywhere else in the file.
+# END OF DOWNLOADED FILE

scripts/setup_ligo_opam_repository.sh

@@ -1,3 +1,6 @@
+#!/bin/sh
+set -e
+
 vendors/opam-repository-tools/rewrite-local-opam-repository.sh
 opam repo add ligo-opam-repository ./vendors/ligo-opam-repository-local-generated
 opam update ligo-opam-repository

src/ast_simplified/combinators.ml

@@ -49,7 +49,7 @@ let e_record ?loc map : expression = Location.wrap ?loc @@ E_record map
 let e_tuple ?loc lst : expression = Location.wrap ?loc @@ E_tuple lst
 let e_some ?loc s : expression = Location.wrap ?loc @@ E_constant ("SOME", [s])
 let e_none ?loc () : expression = Location.wrap ?loc @@ E_constant ("NONE", [])
-let e_map_update ?loc k v old : expression = Location.wrap ?loc @@ E_constant ("MAP_UPDATE" , [k ; v ; old])
+let e_map_add ?loc k v old : expression = Location.wrap ?loc @@ E_constant ("MAP_ADD" , [k ; v ; old])
 let e_map ?loc lst : expression = Location.wrap ?loc @@ E_map lst
 let e_list ?loc lst : expression = Location.wrap ?loc @@ E_list lst
 let e_pair ?loc a b : expression = Location.wrap ?loc @@ E_tuple [a; b]

src/ast_simplified/misc.ml

@@ -1,33 +1,63 @@
 open Trace
 open Types
 
+module Errors = struct
+  let different_literals_because_different_types name a b () =
+    let title () = "literals have different types: " ^ name in
+    let message () = "" in
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" PP.literal a) ;
+      ("b" , fun () -> Format.asprintf "%a" PP.literal b )
+    ] in
+    error ~data title message ()
+
+  let different_literals name a b () =
+    let title () = name ^ " are different" in
+    let message () = "" in
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" PP.literal a) ;
+      ("b" , fun () -> Format.asprintf "%a" PP.literal b )
+    ] in
+    error ~data title message ()
+
+  let error_uncomparable_literals name a b () =
+    let title () = name ^ " are not comparable" in
+    let message () = "" in
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" PP.literal a) ;
+      ("b" , fun () -> Format.asprintf "%a" PP.literal b )
+    ] in
+    error ~data title message ()
+end
+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 _ -> simple_fail "different bools"
+  | Literal_bool _, Literal_bool _ -> fail @@ different_literals "different bools" a b
-  | Literal_bool _, _ -> simple_fail "bool vs non-bool"
+  | 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 _ -> simple_fail "different ints"
+  | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
-  | Literal_int _, _ -> simple_fail "int vs non-int"
+  | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b
   | Literal_nat a, Literal_nat b when a = b -> ok ()
-  | Literal_nat _, Literal_nat _ -> simple_fail "different nats"
+  | Literal_nat _, Literal_nat _ -> fail @@ different_literals "different nats" a b
-  | Literal_nat _, _ -> simple_fail "nat vs non-nat"
+  | Literal_nat _, _ -> fail @@ different_literals_because_different_types "nat vs non-nat" a b
   | Literal_tez a, Literal_tez b when a = b -> ok ()
-  | Literal_tez _, Literal_tez _ -> simple_fail "different tezs"
+  | Literal_tez _, Literal_tez _ -> fail @@ different_literals "different tezs" a b
-  | Literal_tez _, _ -> simple_fail "tez vs non-tez"
+  | Literal_tez _, _ -> fail @@ different_literals_because_different_types "tez vs non-tez" a b
   | Literal_string a, Literal_string b when a = b -> ok ()
-  | Literal_string _, Literal_string _ -> simple_fail "different strings"
+  | Literal_string _, Literal_string _ -> fail @@ different_literals "different strings" a b
-  | Literal_string _, _ -> simple_fail "string vs non-string"
+  | Literal_string _, _ -> fail @@ different_literals_because_different_types "string vs non-string" a b
   | Literal_bytes a, Literal_bytes b when a = b -> ok ()
-  | Literal_bytes _, Literal_bytes _ -> simple_fail "different bytess"
+  | Literal_bytes _, Literal_bytes _ -> fail @@ different_literals "different bytess" a b
-  | Literal_bytes _, _ -> simple_fail "bytes vs non-bytes"
+  | Literal_bytes _, _ -> fail @@ different_literals_because_different_types "bytes vs non-bytes" a b
   | Literal_unit, Literal_unit -> ok ()
-  | Literal_unit, _ -> simple_fail "unit vs non-unit"
+  | Literal_unit, _ -> fail @@ different_literals_because_different_types "unit vs non-unit" a b
   | Literal_address a, Literal_address b when a = b -> ok ()
-  | Literal_address _, Literal_address _ -> simple_fail "different addresss"
+  | Literal_address _, Literal_address _ -> fail @@ different_literals "different addresss" a b
-  | Literal_address _, _ -> simple_fail "address vs non-address"
+  | Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b
-  | Literal_operation _, Literal_operation _ -> simple_fail "can't compare operations"
+  | Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b
-  | Literal_operation _, _ -> simple_fail "operation vs non-operation"
+  | Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b
 
 
 let rec assert_value_eq (a, b: (expression * expression )) : unit result =

src/ast_typed/combinators.ml

@@ -20,6 +20,7 @@ let t_address ?s () : type_value = make_t (T_constant ("address", [])) s
 let t_operation ?s () : type_value = make_t (T_constant ("operation", [])) s
 let t_nat ?s () : type_value = make_t (T_constant ("nat", [])) s
 let t_tez ?s () : type_value = make_t (T_constant ("tez", [])) s
+let t_timestamp ?s () : type_value = make_t (T_constant ("timestamp", [])) s
 let t_unit ?s () : type_value = make_t (T_constant ("unit", [])) s
 let t_option o ?s () : type_value = make_t (T_constant ("option", [o])) s
 let t_tuple lst ?s () : type_value = make_t (T_tuple lst) s
@@ -76,6 +77,10 @@ let get_t_bytes (t:type_value) : unit result = match t.type_value' with
   | T_constant ("bytes", []) -> ok ()
   | _ -> simple_fail "not a bytes"
 
+let get_t_string (t:type_value) : unit result = match t.type_value' with
+  | T_constant ("string", []) -> ok ()
+  | _ -> simple_fail "not a string"
+
 let get_t_contract (t:type_value) : type_value result = match t.type_value' with
   | T_constant ("contract", [x]) -> ok x
   | _ -> simple_fail "not a contract"
@@ -139,6 +144,7 @@ let assert_t_list t =
 
 let is_t_list = Function.compose to_bool get_t_list
 let is_t_nat = Function.compose to_bool get_t_nat
+let is_t_string = Function.compose to_bool get_t_string
 let is_t_int = Function.compose to_bool get_t_int
 
 let assert_t_bytes = fun t ->

src/ast_typed/misc.ml

@@ -4,18 +4,39 @@ open Types
 module Errors = struct
   let different_kinds a b () =
     let title = (thunk "different kinds") in
-    let full () = Format.asprintf "(%a) VS (%a)" PP.type_value a PP.type_value b in
+    let message () = "" in
-    error title full ()
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" PP.type_value a) ;
+      ("b" , fun () -> Format.asprintf "%a" PP.type_value b )
+    ] in
+    error ~data title message ()
 
   let different_constants a b () =
     let title = (thunk "different constants") in
-    let full () = Format.asprintf "%s VS %s" a b in
+    let message () = "" in
-    error title full ()
+    let data = [
+      ("a" , fun () -> Format.asprintf "%s" a) ;
+      ("b" , fun () -> Format.asprintf "%s" b )
+    ] in
+    error ~data title message ()
 
   let different_size_type name a b () =
     let title () = name ^ " have different sizes" in
-    let full () = Format.asprintf "%a VS %a" PP.type_value a PP.type_value b in
+    let message () = "" in
-    error title full ()
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" PP.type_value a) ;
+      ("b" , fun () -> Format.asprintf "%a" PP.type_value b )
+    ] in
+    error ~data title message ()
+
+  let different_props_in_record ka kb () =
+    let title () = "different keys in record" in
+    let message () = "" in
+    let data = [
+      ("key_a" , fun () -> Format.asprintf "%s" ka) ;
+      ("key_b" , fun () -> Format.asprintf "%s" kb )
+    ] in
+    error ~data title message ()
 
   let different_size_constants = different_size_type "constants"
 
@@ -25,6 +46,85 @@ module Errors = struct
 
   let different_size_records = different_size_type "records"
 
+  let different_types name a b () =
+    let title () = name ^ " are different" in
+    let message () = "" in
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" PP.type_value a) ;
+      ("b" , fun () -> Format.asprintf "%a" PP.type_value b )
+    ] in
+    error ~data title message ()
+
+  let different_literals name a b () =
+    let title () = name ^ " are different" in
+    let message () = "" in
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" PP.literal a) ;
+      ("b" , fun () -> Format.asprintf "%a" PP.literal b )
+    ] in
+    error ~data title message ()
+
+  let different_values name a b () =
+    let title () = name ^ " are different" in
+    let message () = "" in
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" PP.value a) ;
+      ("b" , fun () -> Format.asprintf "%a" PP.value b )
+    ] in
+    error ~data title message ()
+
+  let different_literals_because_different_types name a b () =
+    let title () = "literals have different types: " ^ name in
+    let message () = "" in
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" PP.literal a) ;
+      ("b" , fun () -> Format.asprintf "%a" PP.literal b )
+    ] in
+    error ~data title message ()
+
+  let different_values_because_different_types name a b () =
+    let title () = "values have different types: " ^ name in
+    let message () = "" in
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" PP.value a) ;
+      ("b" , fun () -> Format.asprintf "%a" PP.value b )
+    ] in
+    error ~data title message ()
+
+  let error_uncomparable_literals name a b () =
+    let title () = name ^ " are not comparable" in
+    let message () = "" in
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" PP.literal a) ;
+      ("b" , fun () -> Format.asprintf "%a" PP.literal b )
+    ] in
+    error ~data title message ()
+
+  let error_uncomparable_values name a b () =
+    let title () = name ^ " are not comparable" in
+    let message () = "" in
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" PP.value a) ;
+      ("b" , fun () -> Format.asprintf "%a" PP.value b )
+    ] in
+    error ~data title message ()
+
+  let different_size_values name a b () =
+    let title () = name in
+    let message () = "" in
+    let data = [
+      ("a" , fun () -> Format.asprintf "%a" PP.value a) ;
+      ("b" , fun () -> Format.asprintf "%a" PP.value b )
+    ] in
+    error ~data title message ()
+
+  let missing_key_in_record_value k () =
+    let title () = "missing keys in one of the records" in
+    let message () = "" in
+    let data = [
+      ("missing_key" , fun () -> Format.asprintf "%s" k)
+    ] in
+    error ~data title message ()
 end
 
 module Free_variables = struct
@@ -186,7 +286,7 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
       let%bind _ =
         trace_strong (different_constants ca cb)
         @@ Assert.assert_true (ca = cb) in
-      trace (simple_error "constant sub-expression")
+      trace (different_types "constant sub-expression" a b)
       @@ bind_list_iter assert_type_value_eq (List.combine lsta lstb)
     )
   | T_constant _, _ -> fail @@ different_kinds a b
@@ -202,7 +302,7 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
       let%bind _ =
         trace_strong (different_size_sums a b)
         @@ Assert.assert_list_same_size sa' sb' in
-      trace (simple_error "sum type") @@
+      trace (different_types "sum type" a b) @@
       bind_list_iter aux (List.combine sa' sb')
     )
   | T_sum _, _ -> fail @@ different_kinds a b
@@ -211,18 +311,15 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
       let rb' = SMap.to_kv_list rb in
       let aux ((ka, va), (kb, vb)) =
         let%bind _ =
-          let error =
+          trace (different_types "records" a b) @@
-            let title () = "different props in record" in
+          trace_strong (different_props_in_record ka kb) @@
-            let content () = Format.asprintf "%s vs %s" ka kb in
-            error title content in
-          trace_strong error @@
           Assert.assert_true (ka = kb) in
         assert_type_value_eq (va, vb)
       in
       let%bind _ =
         trace_strong (different_size_records a b)
         @@ Assert.assert_list_same_size ra' rb' in
-      trace (simple_error "record type")
+      trace (different_types "record type" a b)
       @@ bind_list_iter aux (List.combine ra' rb')
 
     )
@@ -239,30 +336,30 @@ let type_value_eq ab = Trace.to_bool @@ assert_type_value_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 _ -> simple_fail "different bools"
+  | Literal_bool _, Literal_bool _ -> fail @@ different_literals "booleans" a b
-  | Literal_bool _, _ -> simple_fail "bool vs non-bool"
+  | 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 _ -> simple_fail "different ints"
+  | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
-  | Literal_int _, _ -> simple_fail "int vs non-int"
+  | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b
   | Literal_nat a, Literal_nat b when a = b -> ok ()
-  | Literal_nat _, Literal_nat _ -> simple_fail "different nats"
+  | Literal_nat _, Literal_nat _ -> fail @@ different_literals "different nats" a b
-  | Literal_nat _, _ -> simple_fail "nat vs non-nat"
+  | Literal_nat _, _ -> fail @@ different_literals_because_different_types "nat vs non-nat" a b
   | Literal_tez a, Literal_tez b when a = b -> ok ()
-  | Literal_tez _, Literal_tez _ -> simple_fail "different tezs"
+  | Literal_tez _, Literal_tez _ -> fail @@ different_literals "different tezs" a b
-  | Literal_tez _, _ -> simple_fail "tez vs non-tez"
+  | Literal_tez _, _ -> fail @@ different_literals_because_different_types "tez vs non-tez" a b
   | Literal_string a, Literal_string b when a = b -> ok ()
-  | Literal_string _, Literal_string _ -> simple_fail "different strings"
+  | Literal_string _, Literal_string _ -> fail @@ different_literals "different strings" a b
-  | Literal_string _, _ -> simple_fail "string vs non-string"
+  | Literal_string _, _ -> fail @@ different_literals_because_different_types "string vs non-string" a b
   | Literal_bytes a, Literal_bytes b when a = b -> ok ()
-  | Literal_bytes _, Literal_bytes _ -> simple_fail "different bytess"
+  | Literal_bytes _, Literal_bytes _ -> fail @@ different_literals "different bytes" a b
-  | Literal_bytes _, _ -> simple_fail "bytes vs non-bytes"
+  | Literal_bytes _, _ -> fail @@ different_literals_because_different_types "bytes vs non-bytes" a b
   | Literal_unit, Literal_unit -> ok ()
-  | Literal_unit, _ -> simple_fail "unit vs non-unit"
+  | Literal_unit, _ -> fail @@ different_literals_because_different_types "unit vs non-unit" a b
   | Literal_address a, Literal_address b when a = b -> ok ()
-  | Literal_address _, Literal_address _ -> simple_fail "different addresss"
+  | Literal_address _, Literal_address _ -> fail @@ different_literals "different addresss" a b
-  | Literal_address _, _ -> simple_fail "address vs non-address"
+  | Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b
-  | Literal_operation _, Literal_operation _ -> simple_fail "can't compare operations"
+  | Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b
-  | Literal_operation _, _ -> simple_fail "operation vs non-operation"
+  | Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b
 
 
 let rec assert_value_eq (a, b: (value*value)) : unit result =
@@ -275,13 +372,13 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
       assert_literal_eq (a, b)
   | E_constant (ca, lsta), E_constant (cb, lstb) when ca = cb -> (
       let%bind lst =
-        generic_try (simple_error "constants with different number of elements")
+        generic_try (different_size_values "constants with different number of elements" a b)
           (fun () -> List.combine lsta lstb) in
       let%bind _all = bind_list @@ List.map assert_value_eq lst in
       ok ()
     )
   | E_constant _, E_constant _ ->
-      simple_fail "different constants"
+      fail @@ different_values "constants" a b
   | E_constant _, _ ->
       let error_content () =
         Format.asprintf "%a vs %a"
@@ -295,34 +392,34 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
       ok ()
     )
   | E_constructor _, E_constructor _ ->
-      simple_fail "different constructors"
+      fail @@ different_values "constructors" a b
   | E_constructor _, _ ->
-      simple_fail "comparing constructor with other stuff"
+      fail @@ different_values_because_different_types "constructor vs. non-constructor" a b
 
   | E_tuple lsta, E_tuple lstb -> (
       let%bind lst =
-        generic_try (simple_error "tuples with different number of elements")
+        generic_try (different_size_values "tuples with different number of elements" a b)
           (fun () -> List.combine lsta lstb) in
       let%bind _all = bind_list @@ List.map assert_value_eq lst in
       ok ()
     )
   | E_tuple _, _ ->
-      simple_fail "comparing tuple with other stuff"
+      fail @@ different_values_because_different_types "tuple vs. non-tuple" a b
 
   | E_record sma, E_record smb -> (
-      let aux _ a b =
+      let aux k a b =
         match a, b with
         | Some a, Some b -> Some (assert_value_eq (a, b))
-        | _ -> Some (simple_fail "different record keys")
+        | _              -> Some (fail @@ missing_key_in_record_value k)
       in
       let%bind _all = bind_smap @@ SMap.merge aux sma smb in
       ok ()
     )
   | E_record _, _ ->
-      simple_fail "comparing record with other stuff"
+      fail @@ (different_values_because_different_types "record vs. non-record" a b)
 
   | E_map lsta, E_map lstb -> (
-      let%bind lst = generic_try (simple_error "maps of different lengths")
+      let%bind lst = generic_try (different_size_values "maps of different lengths" a b)
           (fun () ->
              let lsta' = List.sort compare lsta in
              let lstb' = List.sort compare lstb in
@@ -335,27 +432,27 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
       ok ()
     )
   | E_map _, _ ->
-      simple_fail "comparing map with other stuff"
+      fail @@ different_values_because_different_types "map vs. non-map" a b
 
   | E_list lsta, E_list lstb -> (
       let%bind lst =
-        generic_try (simple_error "list of different lengths")
+        generic_try (different_size_values "lists of different lengths" a b)
           (fun () -> List.combine lsta lstb) in
       let%bind _all = bind_map_list assert_value_eq lst in
       ok ()
     )
   | E_list _, _ ->
-      simple_fail "comparing list with other stuff"
+      fail @@ different_values_because_different_types "list vs. non-list" a b
   | (E_literal _, _) | (E_variable _, _) | (E_application _, _)
   | (E_lambda _, _) | (E_let_in _, _) | (E_tuple_accessor _, _)
   | (E_record_accessor _, _)
   | (E_look_up _, _) | (E_matching _, _) | (E_failwith _, _)
   | (E_assign _ , _)
-  | (E_sequence _, _) | (E_loop _, _)-> simple_fail "comparing not a value"
+  | (E_sequence _, _) | (E_loop _, _)-> fail @@ error_uncomparable_values "can't compare sequences nor loops" a b
 
-let merge_annotation (a:type_value option) (b:type_value option) : type_value result =
+let merge_annotation (a:type_value option) (b:type_value option) err : type_value result =
   match a, b with
-  | None, None -> simple_fail "no annotation"
+  | None, None -> fail @@ err
   | Some a, None -> ok a
   | None, Some b -> ok b
   | Some a, Some b ->

src/bin/cli.ml

@@ -1,11 +1,41 @@
 open Cmdliner
 open Trace
 
+let error_pp out (e : error) =
+    let open JSON_string_utils in
+  let message =
+    let opt = e |> member "message" |> string in
+    let msg = Option.unopt ~default:"" opt in
+    if msg = ""
+    then ""
+    else ": " ^ msg in
+  let error_code =
+    let error_code = e |> member "error_code" in
+    match error_code with
+    | `Null -> ""
+    | _ -> " (" ^ (J.to_string error_code) ^ ")" in
+  let title =
+    let opt = e |> member "title" |> string in
+    Option.unopt ~default:"" opt in
+  let data =
+    let data = e |> member "data" in
+    match data with
+    | `Null -> ""
+    | _ -> " " ^ (J.to_string data) ^ "\n" in
+  let infos =
+    let infos = e |> member "infos" in
+    match infos with
+    | `Null -> ""
+    | _ -> " " ^ (J.to_string infos) ^ "\n" in
+  Format.fprintf out "%s%s%s.\n%s%s" title error_code message data infos
+
+
 let toplevel x =
   match x with
   | Trace.Ok ((), annotations) -> ignore annotations; ()
-  | Error ss ->
+  | Error ss -> (
       Format.printf "%a%!" error_pp (ss ())
+    )
 
 let main =
   let term = Term.(const print_endline $ const "Ligo needs a command. Do ligo --help") in
@@ -46,15 +76,16 @@ let compile_file =
   let f source entry_point syntax =
     toplevel @@
     let%bind contract =
-      trace (simple_error "compile michelson") @@
+      trace (simple_info "compiling contract to michelson") @@
       Ligo.Run.compile_contract_file source entry_point syntax in
-    Format.printf "Contract:\n%s\n" contract ;
+    Format.printf "%s\n" contract ;
     ok ()
   in
   let term =
     Term.(const f $ source $ entry_point $ syntax) in
-  let docs = "Compile contracts." in
+  let cmdname = "compile-contract" in
-  (term , Term.info ~docs "compile-contract")
+  let docs = "Subcommand: compile a contract. See `ligo " ^ cmdname ^ " --help' for a list of options specific to this subcommand." in
+  (term , Term.info ~docs cmdname)
 
 let compile_parameter =
   let f source entry_point expression syntax =
@@ -62,13 +93,14 @@ let compile_parameter =
     let%bind value =
       trace (simple_error "compile-input") @@
       Ligo.Run.compile_contract_parameter source entry_point expression syntax in
-    Format.printf "Input:\n%s\n" value;
+    Format.printf "%s\n" value;
     ok ()
   in
   let term =
     Term.(const f $ source $ entry_point $ expression $ syntax) in
-  let docs = "Compile contracts parameters." in
+  let cmdname = "compile-parameter" in
-  (term , Term.info ~docs "compile-parameter")
+  let docs = "Subcommand: compile parameters to a michelson expression. The resulting michelson expression can be passed as an argument in a transaction which calls a contract. See `ligo " ^ cmdname ^ " --help' for a list of options specific to this subcommand." in
+  (term , Term.info ~docs cmdname)
 
 let compile_storage =
   let f source entry_point expression syntax =
@@ -76,13 +108,14 @@ let compile_storage =
     let%bind value =
       trace (simple_error "compile-storage") @@
       Ligo.Run.compile_contract_storage source entry_point expression syntax in
-    Format.printf "Storage:\n%s\n" value;
+    Format.printf "%s\n" value;
     ok ()
   in
   let term =
     Term.(const f $ source $ entry_point $ expression $ syntax) in
-  let docs = "Compile contracts storage." in
+  let cmdname = "compile-storage" in
-  (term , Term.info ~docs "compile-storage")
+  let docs = "Subcommand: compile an initial storage in ligo syntax to a michelson expression. The resulting michelson expression can be passed as an argument in a transaction which originates a contract. See `ligo " ^ cmdname ^ " --help' for a list of options specific to this subcommand." in
+  (term , Term.info ~docs cmdname)
 
 
 let () = Term.exit @@ Term.eval_choice main [compile_file ; compile_parameter ; compile_storage]

src/compiler/compiler_program.ml

@@ -464,8 +464,24 @@ let translate_entry (p:anon_function) : compiled_program result =
   let%bind output = Compiler_type.Ty.type_ output in
   ok ({input;output;body}:compiled_program)
 
+module Errors = struct
+  let corner_case ~loc message =
+    let title () = "corner case" in
+    let content () = "we don't have a good error message for this case. we are
+striving find ways to better report them and find the use-cases that generate
+them. please report this to the developers." in
+    let data = [
+      ("location" , fun () -> loc) ;
+      ("message" , fun () -> message) ;
+    ] in
+    error ~data title content
+end
+open Errors
+
 let translate_contract : anon_function -> michelson result = fun f ->
-  let%bind compiled_program = translate_entry f in
+  let%bind compiled_program =
+    trace_strong (corner_case ~loc:__LOC__ "compiling") @@
+    translate_entry f in
   let%bind (param_ty , storage_ty) = Combinators.get_t_pair f.input in
   let%bind param_michelson = Compiler_type.type_ param_ty in
   let%bind storage_michelson = Compiler_type.type_ storage_ty in

src/compiler/compiler_type.ml

@@ -22,6 +22,7 @@ module Ty = struct
     | Base_int -> return int_k
     | Base_string -> return string_k
     | Base_address -> return address_k
+    | Base_timestamp -> return timestamp_k
     | Base_bytes -> return bytes_k
     | Base_operation -> fail (not_comparable "operation")
 
@@ -48,6 +49,7 @@ module Ty = struct
     | Base_tez -> return tez
     | Base_string -> return string
     | Base_address -> return address
+    | Base_timestamp -> return timestamp
     | Base_bytes -> return bytes
     | Base_operation -> return operation
 
@@ -117,6 +119,7 @@ let base_type : type_base -> O.michelson result =
   | Base_tez -> ok @@ O.prim T_mutez
   | Base_string -> ok @@ O.prim T_string
   | Base_address -> ok @@ O.prim T_address
+  | Base_timestamp -> ok @@ O.prim T_timestamp
   | Base_bytes -> ok @@ O.prim T_bytes
   | Base_operation -> ok @@ O.prim T_operation
 

src/contracts/failwith.mligo

@@ -0,0 +1,8 @@
+type storage = unit
+
+(* let%entry main (p:unit) storage = *)
+(*   (failwith "This contract always fails" : unit) *)
+
+let%entry main (p:unit) storage =
+  if true then failwith "This contract always fails" else ()
+

src/contracts/guess_string.mligo

@@ -0,0 +1,24 @@
+(** Type of storage for this contract *)
+type storage = {
+  challenge : string ;
+}
+
+(** Initial storage *)
+let%init storage = {
+  challenge = "" ;
+}
+
+type param = {
+  new_challenge : string ;
+  attempt : string ;
+}
+
+let%entry attempt (p:param) storage =
+  (* if p.attempt <> storage.challenge then failwith "Failed challenge" else *)
+  let contract : unit contract = Operation.get_contract sender in
+  let transfer : operation = Operation.transaction (unit , contract , 10.00tz) in
+  (* TODO: no syntax for functional updates yet *)
+  (* let storage : storage = { storage with challenge = p.new_challenge } in *)
+  (* for now, rebuild the record by hand. *)
+  let storage : storage = { challenge = p.new_challenge } in
+  ((list [] : operation list), storage)

src/contracts/lambda.ligo

@@ -0,0 +1,6 @@
+function f (const x : unit) : unit is
+  begin skip end with unit
+
+function main (const p : unit ; const s : unit) : unit is
+  var y : unit := f(unit) ;
+  begin skip end with y

src/contracts/lambda.mligo

@@ -0,0 +1,9 @@
+type storage = unit
+
+(* not supported yet
+let%entry main (p:unit) storage =
+  (fun x -> ()) ()
+*)
+
+let%entry main (p:unit) storage =
+  (fun (x : unit) -> ()) ()

src/contracts/lambda2.mligo

@@ -0,0 +1,10 @@
+type storage = unit
+
+(* not supported yet
+let%entry main (p:unit) storage =
+  (fun x -> ()) ()
+*)
+
+let%entry main (p:unit) storage =
+  (fun (f : unit -> unit) -> f ())
+    (fun (x : unit) -> unit)

src/contracts/letin.mligo

@@ -0,0 +1,7 @@
+type storage = int * int
+
+let%entry main (n: int) storage =
+  let x : int * int =
+    let x : int = 7
+    in x + n, storage.(0) + storage.(1)
+  in (([] : operation list), x)

src/contracts/list.mligo

@@ -0,0 +1,10 @@
+type storage = int * int list
+
+type param = int list
+
+let%entry main (p : param) storage =
+  let storage =
+    match p with
+      [] -> storage
+    | hd::tl -> storage.(0) + hd, tl
+  in (([] : operation list), storage)

src/contracts/match.mligo

@@ -0,0 +1,13 @@
+type storage = int
+
+type param =
+  Add of int
+| Sub of int
+
+let%entry main (p : param) storage =
+  let storage =
+    storage +
+      (match p with
+         Add n -> n
+       | Sub n -> 0-n)
+  in (([] : operation list), storage)

src/contracts/match_bis.mligo

@@ -0,0 +1,20 @@
+type storage = int
+
+(* variant defining pseudo multi-entrypoint actions *)
+
+type action =
+| Increment of int
+| Decrement of int
+
+let add (a: int) (b: int) : int = a + b
+
+let subtract (a: int) (b: int) : int = a - b
+
+(* real entrypoint that re-routes the flow based on the action provided *)
+
+let%entry main (p : action) storage =
+  let storage =
+    match p with
+    | Increment n -> add storage n
+    | Decrement n -> subtract storage n
+  in (([] : operation list), storage)

src/contracts/new-syntax.mligo

@@ -14,8 +14,12 @@ type param = {
 }
 
 let%entry attempt (p:param) storage =
-  if Crypto.hash (Bytes.pack p.attempt) <> Bytes.pack storage.challenge then failwith "Failed challenge" ;
+  if Crypto.hash (Bytes.pack p.attempt) <> Bytes.pack storage.challenge
-  let contract : unit contract = Operation.get_contract sender in
+  then failwith "Failed challenge"
-  let transfer : operation = Operation.transaction (unit , contract , 10.00tz) in
+  else
-  let storage : storage = storage.challenge <- p.new_challenge in
+    let contract : unit contract =
-  ((list [] : operation list), storage)
+      Operation.get_contract sender in
+    let transfer : operation =
+      Operation.transaction (unit , contract , 10tz) in
+    let storage : storage = {challenge = p.new_challenge}
+    in (([] : operation list), storage)

src/contracts/parser-bad-reported-term.ligo

@@ -0,0 +1,6 @@
+function f (const x : unit) : unit is
+  begin skip end with unit
+
+function main (const p : unit ; const s : unit) : unit is
+  behin skip end with f unit
+// the srcloc is correct but the reported term is "skip" instead of "behin".

src/contracts/record.mligo

@@ -0,0 +1,47 @@
+type foobar = {
+ foo : int ;
+ bar : int ;
+}
+
+let fb : foobar = {
+  foo = 0 ;
+  bar = 0 ;
+}
+
+type abc = {
+  a : int ;
+  b : int ;
+  c : int
+}
+
+let abc : abc = {
+  a = 42 ;
+  b = 142 ;
+  c = 242
+}
+
+let a : int = abc.a
+let b : int = abc.b
+let c : int = abc.c
+
+let projection (r : foobar) : int = r.foo + r.bar
+
+let modify (r : foobar) : foobar = {foo = 256; bar = r.bar}
+
+let modify_abc (r : abc) : abc = {a = r.a; b = 2048; c = r.c}
+
+type big_record = {
+     a : int ;
+     b : int ;
+     c : int ;
+     d : int ;
+     e : int ;
+}
+
+let br : big_record = {
+  a = 23 ;
+  b = 23 ;
+  c = 23 ;
+  d = 23 ;
+  e = 23 ;
+}

src/contracts/website1.ligo

@@ -0,0 +1,2 @@
+function main (const p : int ; const s : int) : (list(operation) * int) is
+  block {skip} with ((nil : list(operation)), s + 1)

src/contracts/website2.ligo

@@ -0,0 +1,18 @@
+// variant defining pseudo multi-entrypoint actions
+type action is
+| Increment of int
+| Decrement of int
+
+function add (const a : int ; const b : int) : int is
+    block { skip } with a + b
+
+function subtract (const a : int ; const b : int) : int is
+    block { skip } with a - b
+
+// real entrypoint that re-routes the flow based on the action provided
+function main (const p : action ; const s : int) : (list(operation) * int) is
+  block {skip} with ((nil : list(operation)),
+    case p of
+    | Increment n -> add(s, n)
+    | Decrement n -> subtract(s, n)
+    end)

src/mini_c/PP.ml

@@ -16,6 +16,7 @@ let type_base ppf : type_base -> _ = function
   | Base_tez -> fprintf ppf "tez"
   | Base_string -> fprintf ppf "string"
   | Base_address -> fprintf ppf "address"
+  | Base_timestamp -> fprintf ppf "timestamp"
   | Base_bytes -> fprintf ppf "bytes"
   | Base_operation -> fprintf ppf "operation"
 

src/mini_c/types.ml

@@ -4,6 +4,7 @@ type type_base =
   | Base_unit
   | Base_bool
   | Base_int | Base_nat | Base_tez
+  | Base_timestamp
   | Base_string | Base_bytes | Base_address
   | Base_operation
 

src/operators/helpers.ml

@@ -9,8 +9,17 @@ module Typer = struct
       let full () = Format.asprintf "constant name: %s\nexpected: %d\ngot: %d\n"
           name expected (List.length got) in
       error title full
-  end
 
+    let error_uncomparable_types a b () =
+      let title () = "these types are not comparable" in
+      let message () = "" in
+      let data = [
+        ("a" , fun () -> Format.asprintf "%a" PP.type_value a) ;
+        ("b" , fun () -> Format.asprintf "%a" PP.type_value b )
+      ] in
+      error ~data title message ()
+  end
+  open Errors
 
   type type_result = string * type_value
   type typer' = type_value list -> type_value option -> type_result result
@@ -22,7 +31,7 @@ module Typer = struct
       let%bind tv' = f tv_opt in
       ok (s , tv')
     )
-    | _ -> fail @@ Errors.wrong_param_number s 0 lst
+    | _ -> fail @@ wrong_param_number s 0 lst
   let typer_0 name f : typer = (name , typer'_0 name f)
 
   let typer'_1 : name -> (type_value -> type_value result) -> typer' = fun s f lst _ ->
@@ -31,7 +40,7 @@ module Typer = struct
         let%bind tv' = f a in
         ok (s , tv')
       )
-    | _ -> fail @@ Errors.wrong_param_number s 1 lst
+    | _ -> fail @@ wrong_param_number s 1 lst
   let typer_1 name f : typer = (name , typer'_1 name f)
 
   let typer'_1_opt : name -> (type_value -> type_value option -> type_value result) -> typer' = fun s f lst tv_opt ->
@@ -40,7 +49,7 @@ module Typer = struct
         let%bind tv' = f a tv_opt in
         ok (s , tv')
       )
-    | _ -> fail @@ Errors.wrong_param_number s 1 lst
+    | _ -> fail @@ wrong_param_number s 1 lst
   let typer_1_opt name f : typer = (name , typer'_1_opt name f)
 
   let typer'_2 : name -> (type_value -> type_value -> type_value result) -> typer' = fun s f lst _ ->
@@ -49,7 +58,7 @@ module Typer = struct
         let%bind tv' = f a b in
         ok (s , tv')
       )
-    | _ -> fail @@ Errors.wrong_param_number s 2 lst
+    | _ -> fail @@ wrong_param_number s 2 lst
   let typer_2 name f : typer = (name , typer'_2 name f)
 
   let typer'_3 : name -> (type_value -> type_value -> type_value -> type_value result) -> typer' = fun s f lst _ ->
@@ -58,7 +67,7 @@ module Typer = struct
         let%bind tv' = f a b c in
         ok (s , tv')
       )
-    | _ -> fail @@ Errors.wrong_param_number s 3 lst
+    | _ -> fail @@ wrong_param_number s 3 lst
   let typer_3 name f : typer = (name , typer'_3 name f)
 
   let constant name cst = typer_0 name (fun _ -> ok cst)
@@ -70,7 +79,7 @@ module Typer = struct
 
   let comparator : string -> typer = fun s -> typer_2 s @@ fun a b ->
     let%bind () =
-      trace_strong (simple_error "Types a and b aren't comparable") @@
+      trace_strong (error_uncomparable_types a b) @@
       Assert.assert_true @@
       List.exists (eq_2 (a , b)) [
         t_int () ;

src/operators/operators.ml

@@ -42,6 +42,7 @@ module Simplify = struct
     ("bool" , "bool") ;
     ("operation" , "operation") ;
     ("address" , "address") ;
+    ("timestamp" , "timestamp") ;
     ("contract" , "contract") ;
     ("list" , "list") ;
     ("option" , "option") ;
@@ -60,8 +61,11 @@ module Simplify = struct
       ("int" , "INT") ;
       ("abs" , "ABS") ;
       ("amount" , "AMOUNT") ;
+      ("now" , "NOW") ;
       ("unit" , "UNIT") ;
       ("source" , "SOURCE") ;
+      ("sender" , "SENDER") ;
+      ("failwith" , "FAILWITH") ;
     ]
 
     let type_constants = type_constants
@@ -82,7 +86,54 @@ module Simplify = struct
   end
 
   module Ligodity = struct
-    include Pascaligo
+    let constants = [
+      ("Current.balance", "BALANCE") ;
+      ("balance", "BALANCE") ;
+      ("Current.time", "NOW") ;
+      ("time", "NOW") ;
+      ("Current.amount" , "AMOUNT") ;
+      ("amount", "AMOUNT") ;
+      ("Current.gas", "STEPS_TO_QUOTA") ;
+      ("gas", "STEPS_TO_QUOTA") ;
+      ("Current.sender" , "SENDER") ;
+      ("sender", "SENDER") ;
+      ("Current.failwith", "FAILWITH") ;
+      ("failwith" , "FAILWITH") ;
+
+      ("Crypto.hash" , "HASH") ;
+      ("Crypto.black2b", "BLAKE2B") ;
+      ("Crypto.sha256", "SHA256") ;
+      ("Crypto.sha512", "SHA512") ;
+      ("Crypto.hash_key", "HASH_KEY") ;
+      ("Crypto.check", "CHECK_SIGNATURE") ;
+
+      ("Bytes.pack" , "PACK") ;
+      ("Bytes.unpack", "UNPACK") ;
+      ("Bytes.length", "SIZE") ;
+      ("Bytes.size" , "SIZE") ;
+      ("Bytes.concat", "CONCAT") ;
+      ("Bytes.slice", "SLICE") ;
+      ("Bytes.sub", "SLICE") ;
+
+      ("String.length", "SIZE") ;
+      ("String.size", "SIZE") ;
+      ("String.slice", "SLICE") ;
+      ("String.sub", "SLICE") ;
+      ("String.concat", "CONCAT") ;
+
+      ("List.length", "SIZE") ;
+      ("List.size", "SIZE") ;
+      ("List.iter", "ITER") ;
+
+      ("Operation.transaction" , "CALL") ;
+      ("Operation.get_contract" , "GET_CONTRACT") ;
+      ("int" , "INT") ;
+      ("abs" , "ABS") ;
+      ("unit" , "UNIT") ;
+      ("source" , "SOURCE") ;
+    ]
+
+    let type_constants = type_constants
   end
 
 end
@@ -121,14 +172,15 @@ module Typer = struct
     | Some t -> ok t
 
   let sub = typer_2 "SUB" @@ fun a b ->
-    let%bind () =
+    if (eq_2 (a , b) (t_int ()))
-      trace_strong (simple_error "Types a and b aren't numbers") @@
+    then ok @@ t_int () else
-      Assert.assert_true @@
+    if (eq_2 (a , b) (t_nat ()))
-      List.exists (eq_2 (a , b)) [
+    then ok @@ t_int () else
-        t_int () ;
+    if (eq_2 (a , b) (t_timestamp ()))
-        t_nat () ;
+    then ok @@ t_int () else
-      ] in
+    if (eq_2 (a , b) (t_tez ()))
-    ok @@ t_int ()
+    then ok @@ t_tez () else
+      fail (simple_error "Typing substraction, bad parameters.")
 
   let some = typer_1 "SOME" @@ fun a -> ok @@ t_option a ()
 
@@ -137,18 +189,69 @@ module Typer = struct
     let%bind () = assert_type_value_eq (src , k) in
     ok m
 
-  let map_update : typer = typer_3 "MAP_UPDATE" @@ fun k v m ->
+  let map_add : typer = typer_3 "MAP_ADD" @@ fun k v m ->
     let%bind (src, dst) = get_t_map m in
     let%bind () = assert_type_value_eq (src, k) in
     let%bind () = assert_type_value_eq (dst, v) in
     ok m
 
+  let map_update : typer = typer_3 "MAP_UPDATE_TODO" @@ fun k v m ->
+    let%bind (src, dst) = get_t_map m in
+    let%bind () = assert_type_value_eq (src, k) in
+    let%bind v' = get_t_option v in
+    let%bind () = assert_type_value_eq (dst, v') in
+    ok m
+
+  let map_mem : typer = typer_2 "MAP_MEM_TODO" @@ fun k m ->
+    let%bind (src, _dst) = get_t_map m in
+    let%bind () = assert_type_value_eq (src, k) in
+    ok @@ t_bool ()
+
+  let map_find : typer = typer_2 "MAP_FIND_TODO" @@ fun k m ->
+    let%bind (src, dst) = get_t_map m in
+    let%bind () = assert_type_value_eq (src, k) in
+    ok @@ t_option dst ()
+
+  let map_fold : typer = typer_3 "MAP_FOLD_TODO" @@ fun f m acc ->
+    let%bind (src, dst) = get_t_map m in
+    let expected_f_type = t_function (t_tuple [(t_tuple [src ; dst] ()) ; acc] ()) acc () in
+    let%bind () = assert_type_value_eq (f, expected_f_type) in
+    ok @@ acc
+
+  let map_map : typer = typer_2 "MAP_MAP_TODO" @@ fun f m ->
+    let%bind (k, v) = get_t_map m in
+    let%bind (input_type, result_type) = get_t_function f in
+    let%bind () = assert_type_value_eq (input_type, t_tuple [k ; v] ()) in
+    ok @@ t_map k result_type ()
+
+  let map_map_fold : typer = typer_3 "MAP_MAP_TODO" @@ fun f m acc ->
+    let%bind (k, v) = get_t_map m in
+    let%bind (input_type, result_type) = get_t_function f in
+    let%bind () = assert_type_value_eq (input_type, t_tuple [t_tuple [k ; v] () ; acc] ()) in
+    let%bind ttuple = get_t_tuple result_type in
+    match ttuple with
+    | [result_acc ; result_dst ] ->
+      ok @@ t_tuple [ t_map k result_dst () ; result_acc ] ()
+    (* TODO: error message *)
+    | _ -> fail @@ simple_error "function passed to map should take (k * v) * acc as an argument"
+
+  let map_iter : typer = typer_2 "MAP_MAP_TODO" @@ fun f m ->
+    let%bind (k, v) = get_t_map m in
+    let%bind () = assert_type_value_eq (f, t_function (t_tuple [k ; v] ()) (t_unit ()) ()) in
+    ok @@ t_unit ()
+
   let size = typer_1 "SIZE" @@ fun t ->
     let%bind () =
       Assert.assert_true @@
       (is_t_map t || is_t_list t) in
     ok @@ t_nat ()
 
+  let failwith_ = typer_1 "FAILWITH" @@ fun t ->
+    let%bind () =
+      Assert.assert_true @@
+      (is_t_string t) in
+    ok @@ t_unit ()
+
   let get_force = typer_2 "MAP_GET_FORCE" @@ fun i m ->
     let%bind (src, dst) = get_t_map m in
     let%bind _ = assert_type_value_eq (src, i) in
@@ -178,6 +281,8 @@ module Typer = struct
 
   let amount = constant "AMOUNT" @@ t_tez ()
 
+  let now = constant "NOW" @@ t_timestamp ()
+
   let transaction = typer_3 "CALL" @@ fun param amount contract ->
     let%bind () = assert_t_tez amount in
     let%bind contract_param = get_t_contract contract in
@@ -210,6 +315,8 @@ module Typer = struct
     then ok @@ t_nat () else
     if eq_2 (a , b) (t_int ())
     then ok @@ t_int () else
+    if eq_1 a (t_tez ()) && eq_1 b (t_nat ())
+    then ok @@ t_tez () else
       simple_fail "Dividing with wrong types"
 
   let mod_ = typer_2 "MOD" @@ fun a b ->
@@ -222,9 +329,11 @@ module Typer = struct
     then ok @@ t_nat () else
     if eq_2 (a , b) (t_int ())
     then ok @@ t_int () else
+    if eq_2 (a , b) (t_tez ())
+    then ok @@ t_tez () else
     if (eq_1 a (t_nat ()) && eq_1 b (t_int ())) || (eq_1 b (t_nat ()) && eq_1 a (t_int ()))
     then ok @@ t_int () else
-      simple_fail "Adding with wrong types"
+      simple_fail "Adding with wrong types. Expected nat, int or tez."
 
   let constant_typers = Map.String.of_list [
       add ;
@@ -243,9 +352,18 @@ module Typer = struct
       boolean_operator_2 "OR" ;
       boolean_operator_2 "AND" ;
       map_remove ;
+      map_add ;
       map_update ;
+      map_mem ;
+      map_find ;
+      map_map_fold ;
+      map_map ;
+      map_fold ;
+      map_iter ;
+      (* map_size ; (* use size *) *)
       int ;
       size ;
+      failwith_ ;
       get_force ;
       bytes_pack ;
       bytes_unpack ;
@@ -257,6 +375,7 @@ module Typer = struct
       transaction ;
       get_contract ;
       abs ;
+      now ;
     ]
 
 end
@@ -309,10 +428,12 @@ module Compiler = struct
     ("CONS" , simple_binary @@ prim I_CONS) ;
     ("UNIT" , simple_constant @@ prim I_UNIT) ;
     ("AMOUNT" , simple_constant @@ prim I_AMOUNT) ;
+    ("NOW" , simple_constant @@ prim I_NOW) ;
     ("CALL" , simple_ternary @@ prim I_TRANSFER_TOKENS) ;
     ("SOURCE" , simple_constant @@ prim I_SOURCE) ;
     ("SENDER" , simple_constant @@ prim I_SENDER) ;
-    ( "MAP_UPDATE" , simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE ]) ;
+    ( "MAP_ADD" , simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE ]) ;
+    ( "MAP_UPDATE" , simple_ternary @@ prim I_UPDATE) ;
   ]
 
 end

src/parser/ligodity/Parser.mly

@@ -5,9 +5,12 @@ open AST
 
 (* Rewrite "let pattern = e" as "let x = e;; let x1 = ...;; let x2 = ...;;" *)
 
+(*
 module VMap = Utils.String.Map
 
-(*let ghost_of value = Region.{region=ghost; value}*)
+let ghost_of value = Region.{region=ghost; value}
+*)
+
 let ghost = Region.ghost
 
 (* let fail_syn_unif type1 type2 : 'a =

src/parser/ligodity/Tests/match.mml

@@ -0,0 +1,13 @@
+type storage = int
+
+type param =
+  Add of int
+| Sub of int
+
+let%entry main (p : param) storage =
+  let storage =
+    storage +
+      (match p with
+         Add n -> n
+       | Sub n -> 0-n)
+  in (([] : operation list), storage)

src/simplify/ligodity.ml

@@ -479,6 +479,18 @@ and simpl_fun lamb' : expr result =
     in
     bind_map_list aux p_args
   in
+  match args' with
+  | [ single ] -> (
+      let (binder , input_type) =
+        ((fst single).value , snd single) in
+      let%bind (body , body_type) = expr_to_typed_expr lamb.body in
+      let%bind output_type =
+        bind_map_option simpl_type_expression body_type in
+      let%bind result = simpl_expression body in
+      return @@ e_lambda ~loc binder (Some input_type) output_type result
+
+    )
+  | _ -> (
       let arguments_name = "arguments" in
       let (binder , input_type) =
         let type_expression = T_tuple (List.map snd args') in
@@ -495,6 +507,7 @@ and simpl_fun lamb' : expr result =
         let wraps = List.mapi aux args' in
         List.fold_right' (fun x f -> f x) result wraps in
       return @@ e_lambda ~loc binder (Some input_type) output_type wrapped_result
+    )
 
 
 and simpl_logic_expression ?te_annot (t:Raw.logic_expr) : expr result =

src/simplify/pascaligo.ml

@@ -15,10 +15,21 @@ let pseq_to_list = function
 let get_value : 'a Raw.reg -> 'a = fun x -> x.value
 
 module Errors = struct
+  let unsupported_ass_None region =
+    let title () = "assignment of None" in
+    let message () =
+      Format.asprintf "assignments of None are not supported yet" in
+    let data = [
+      ("none_expr",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ region)
+    ] in
+    error ~data title message
+
   let unsupported_entry_decl decl =
     let title () = "entry point declarations" in
     let message () =
-      Format.asprintf "entry points within the contract are not supported yet" in
+      Format.asprintf "entry points within the contract \
+                       are not supported yet" in
     let data = [
       ("declaration",
        fun () -> Format.asprintf "%a" Location.pp_lift @@ decl.Region.region)
@@ -92,13 +103,176 @@ module Errors = struct
   let unsupported_set_expr expr =
     let title () = "set expressions" in
     let message () =
-      Format.asprintf "set type is not supported yet" in
+      Format.asprintf "the set type is not supported yet" in
      let expr_loc = Raw.expr_to_region expr in
     let data = [
       ("expr_loc",
        fun () -> Format.asprintf "%a" Location.pp_lift @@ expr_loc)
     ] in
     error ~data title message
+
+  let unsupported_proc_calls call =
+    let title () = "procedure calls" in
+    let message () =
+      Format.asprintf "procedure calls are not supported yet" in
+    let data = [
+      ("call_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ call.Region.region)
+    ] in
+    error ~data title message
+
+  let unsupported_for_loops region =
+    let title () = "bounded iterators" in
+    let message () =
+      Format.asprintf "for loops are not supported yet" in
+    let data = [
+      ("loop_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ region)
+    ] in
+    error ~data title message
+
+  let unsupported_deep_map_assign v =
+    let title () = "map assignments" in
+    let message () =
+      Format.asprintf "assignments to embedded maps are not \
+                       supported yet" in
+    let data = [
+      ("lhs_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ v.Region.region)
+    ] in
+    error ~data title message
+
+  let unsupported_empty_record_patch record_expr =
+    let title () = "empty record patch" in
+    let message () =
+      Format.asprintf "empty record patches are not supported yet" in
+    let data = [
+      ("record_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ record_expr.Region.region)
+    ] in
+    error ~data title message
+
+  let unsupported_map_patches patch =
+    let title () = "map patches" in
+    let message () =
+      Format.asprintf "map patches (a.k.a. functional updates) are \
+                       not supported yet" in
+    let data = [
+      ("patch_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ patch.Region.region)
+    ] in
+    error ~data title message
+
+  let unsupported_set_patches patch =
+    let title () = "set patches" in
+    let message () =
+      Format.asprintf "set patches (a.k.a. functional updates) are \
+                       not supported yet" in
+    let data = [
+      ("patch_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ patch.Region.region)
+    ] in
+    error ~data title message
+
+  let unsupported_deep_map_rm path =
+    let title () = "binding removals" in
+    let message () =
+      Format.asprintf "removal of bindings from embedded maps \
+                       are not supported yet" in
+    let data = [
+      ("path_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ path.Region.region)
+    ] in
+    error ~data title message
+
+  let unsupported_set_removal remove =
+    let title () = "set removals" in
+    let message () =
+      Format.asprintf "removal of elements in a set is not \
+                       supported yet" in
+    let data = [
+      ("removal_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ remove.Region.region)
+    ] in
+    error ~data title message
+
+  let unsupported_non_var_pattern p =
+    let title () = "pattern is not a variable" in
+    let message () =
+      Format.asprintf "non-variable patterns in constructors \
+                       are not supported yet" in
+    let pattern_loc = Raw.pattern_to_region p in
+    let data = [
+      ("pattern_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ pattern_loc)
+    ] in
+    error ~data title message
+
+  let only_constructors p =
+    let title () = "constructors in patterns" in
+    let message () =
+      Format.asprintf "currently, only constructors are supported in patterns" in
+    let pattern_loc = Raw.pattern_to_region p in
+    let data = [
+      ("pattern_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ pattern_loc)
+    ] in
+    error ~data title message
+
+  let unsupported_tuple_pattern p =
+    let title () = "tuple pattern" in
+    let message () =
+      Format.asprintf "tuple patterns are not supported yet" in
+    let pattern_loc = Raw.pattern_to_region p in
+    let data = [
+      ("pattern_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ pattern_loc)
+    ] in
+    error ~data title message
+
+  let unsupported_deep_Some_patterns pattern =
+    let title () = "option patterns" in
+    let message () =
+      Format.asprintf "currently, only variables in Some constructors \
+                       in patterns are supported" in
+    let pattern_loc = Raw.pattern_to_region pattern in
+    let data = [
+      ("pattern_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ pattern_loc)
+    ] in
+    error ~data title message
+
+  let unsupported_deep_list_patterns cons =
+    let title () = "lists in patterns" in
+    let message () =
+      Format.asprintf "currently, only empty lists and x::y \
+                       are supported in patterns" in
+    let data = [
+      ("pattern_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ cons.Region.region)
+    ] in
+    error ~data title message
+
+  let unsupported_sub_blocks b =
+    let title () = "block instructions" in
+    let message () =
+      Format.asprintf "Sub-blocks are not supported yet" in
+    let data = [
+      ("block_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ b.Region.region)
+    ] in
+    error ~data title message
+
+  (* Logging *)
+
+  let simplifying_instruction t =
+    let title () = "simplifiying instruction" in
+    let message () = "" in
+    let data = [
+      ("instruction",
+       fun () -> Format.asprintf "%a" PP_helpers.(printer Parser.Pascaligo.ParserLog.print_instruction) t)
+    ] in
+    error ~data title message
 end
 
 open Errors
@@ -172,7 +346,7 @@ let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
 
 and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result =
   match lst with
-  | [] -> assert false
+  | [] -> ok @@ t_unit
   | [hd] -> simpl_type_expression hd
   | lst ->
       let%bind lst = bind_list @@ List.map simpl_type_expression lst in
@@ -542,7 +716,8 @@ and simpl_statement : Raw.statement -> (_ -> expression result) result =
 and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) result =
   fun t ->
   match t with
-  | ProcCall _ -> simple_fail "no proc call"
+  | ProcCall call ->
+      fail @@ unsupported_proc_calls call
   | Fail e -> (
       let%bind expr = simpl_expression e.value.fail_expr in
       return @@ e_failwith expr
@@ -557,8 +732,8 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
       let%bind body = simpl_block l.block.value in
       let%bind body = body None in
       return @@ e_loop cond body
-  | Loop (For _) ->
+  | Loop (For (ForInt {region; _} | ForCollect {region; _})) ->
-      simple_fail "no for yet"
+      fail @@ unsupported_for_loops region
   | Cond c -> (
       let (c , loc) = r_split c in
       let%bind expr = simpl_expression c.test in
@@ -576,7 +751,7 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
       let (a , loc) = r_split a in
       let%bind value_expr = match a.rhs with
         | Expr e -> simpl_expression e
-        | NoneExpr _ -> simple_fail "no none assignments yet"
+        | NoneExpr reg -> fail @@ unsupported_ass_None reg
       in
       match a.lhs with
         | Path path -> (
@@ -587,10 +762,10 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
             let v' = v.value in
             let%bind name = match v'.path with
               | Name name -> ok name
-              | _ -> simple_fail "no complex map assignments yet" in
+              | _ -> fail @@ unsupported_deep_map_assign v in
             let%bind key_expr = simpl_expression v'.index.value.inside in
             let old_expr = e_variable name.value in
-            let expr' = e_map_update key_expr value_expr old_expr in
+            let expr' = e_map_add key_expr value_expr old_expr in
             return @@ e_assign ~loc name.value [] expr'
           )
     )
@@ -614,7 +789,8 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
       let%bind inj = bind_list
         @@ List.map (fun (x:Raw.field_assign Region.reg) ->
             let (x , loc) = r_split x in
-            let%bind e = simpl_expression x.field_expr in ok (x.field_name.value, e , loc)
+            let%bind e = simpl_expression x.field_expr
+            in ok (x.field_name.value, e , loc)
           )
         @@ pseq_to_list r.record_inj.value.elements in
       let%bind expr =
@@ -622,27 +798,30 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
           e_assign ~loc name (access_path @ [ Access_record access ]) v in
         let assigns = List.map aux inj in
         match assigns with
-        | [] -> simple_fail "empty record patch"
+               (* E_sequence (E_skip, E_skip) ? *)
+        | [] -> fail @@ unsupported_empty_record_patch r.record_inj
         | hd :: tl -> (
-            let aux acc cur = e_sequence (acc) (cur) in
+            let aux acc cur = e_sequence acc cur in
             ok @@ List.fold_left aux hd tl
           )
       in
       return @@ expr
     )
-  | MapPatch _ -> simple_fail "no map patch yet"
+  | MapPatch patch ->
-  | SetPatch _ -> simple_fail "no set patch yet"
+      fail @@ unsupported_map_patches patch
+  | SetPatch patch ->
+      fail @@ unsupported_set_patches patch
   | MapRemove r -> (
       let (v , loc) = r_split r in
       let key = v.key in
       let%bind map = match v.map with
         | Name v -> ok v.value
-        | _ -> simple_fail "no complex map remove yet" in
+        | Path path -> fail @@ unsupported_deep_map_rm path in
       let%bind key' = simpl_expression key in
       let expr = e_constant ~loc "MAP_REMOVE" [key' ; e_variable map] in
       return @@ e_assign ~loc map [] expr
     )
-  | SetRemove _ -> simple_fail "no set remove yet"
+  | SetRemove r -> fail @@ unsupported_set_removal r
 
 and simpl_path : Raw.path -> string * Ast_simplified.access_path = fun p ->
   match p with
@@ -663,15 +842,10 @@ and simpl_path : Raw.path -> string * Ast_simplified.access_path = fun p ->
 
 and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t ->
   let open Raw in
-  let get_var (t:Raw.pattern) = match t with
+  let get_var (t:Raw.pattern) =
+    match t with
     | PVar v -> ok v.value
-    | _ ->
+    | p -> fail @@ unsupported_non_var_pattern p
-        let error =
-          let title () = "not a var" in
-          let content () = Format.asprintf "%a" (PP_helpers.printer Parser.Pascaligo.ParserLog.print_pattern) t in
-          error title content
-        in
-        fail error
   in
   let get_tuple (t:Raw.pattern) = match t with
     | PCons v -> npseq_to_list v.value
@@ -681,32 +855,33 @@ and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t -
   let get_single (t:Raw.pattern) =
     let t' = get_tuple t in
     let%bind () =
-      trace_strong (simple_error "not single") @@
+      trace_strong (unsupported_tuple_pattern t) @@
       Assert.assert_list_size t' 1 in
     ok (List.hd t') in
   let get_constr (t:Raw.pattern) = match t with
     | PConstr v ->
         let%bind var = get_single (snd v.value).value >>? get_var in
         ok ((fst v.value).value , var)
-    | _ -> simple_fail "not a constr"
+    | _ -> fail @@ only_constructors t
   in
   let%bind patterns =
     let aux (x , y) =
       let xs = get_tuple x in
-      trace_strong (simple_error "no tuple in patterns yet") @@
+      trace_strong (unsupported_tuple_pattern x) @@
       Assert.assert_list_size xs 1 >>? fun () ->
       ok (List.hd xs , y)
     in
     bind_map_list aux t in
   match patterns with
   | [(PFalse _ , f) ; (PTrue _ , t)]
-  | [(PTrue _ , t) ; (PFalse _ , f)] -> ok @@ Match_bool {match_true = t ; match_false = f}
+  | [(PTrue _ , t) ; (PFalse _ , f)] ->
+      ok @@ Match_bool {match_true = t ; match_false = f}
   | [(PSome v , some) ; (PNone _ , none)]
   | [(PNone _ , none) ; (PSome v , some)] -> (
       let (_, v) = v.value in
       let%bind v = match v.value.inside with
         | PVar v -> ok v.value
-        | _ -> simple_fail "complex none patterns not supported yet" in
+        | p -> fail @@ unsupported_deep_Some_patterns p in
       ok @@ Match_option {match_none = none ; match_some = (v, some) }
     )
   | [(PCons c , cons) ; (PList (PNil _) , nil)]
@@ -717,11 +892,12 @@ and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t -
             let%bind a = get_var a in
             let%bind b = get_var b in
             ok (a, b)
-        | _ -> simple_fail "complex list patterns not supported yet"
+        | _ -> fail @@ unsupported_deep_list_patterns c
       in
       ok @@ Match_list {match_cons = (a, b, cons) ; match_nil = nil}
   | lst ->
-      trace (simple_error "weird patterns not supported yet") @@
+      trace (simple_info "currently, only booleans, options, lists and \
+                         user-defined constructors are supported in patterns") @@
       let%bind constrs =
         let aux (x , y) =
           let error =
@@ -736,25 +912,25 @@ and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t -
         bind_map_list aux lst in
       ok @@ Match_variant constrs
 
-and simpl_instruction_block : Raw.instruction -> (_ -> expression result) result = fun t ->
+and simpl_instruction_block : Raw.instruction -> (_ -> expression result) result =
+  fun t ->
   match t with
   | Single s -> simpl_single_instruction s
   | Block b -> simpl_block b.value
 
-and simpl_instruction : Raw.instruction -> (_ -> expression result) result = fun t ->
+and simpl_instruction : Raw.instruction -> (_ -> expression result) result =
-  let main_error =
+  fun t ->
-    let title () = "simplifiying instruction" in
+  trace (simplifying_instruction t) @@
-    let content () = Format.asprintf "%a" PP_helpers.(printer Parser.Pascaligo.ParserLog.print_instruction) t in
-    error title content in
-  trace main_error @@
   match t with
   | Single s -> simpl_single_instruction s
-  | Block _ -> simple_fail "no block instruction yet"
+  | Block b -> fail @@ unsupported_sub_blocks b
 
-and simpl_statements : Raw.statements -> (_ -> expression result) result = fun ss ->
+and simpl_statements : Raw.statements -> (_ -> expression result) result =
+  fun ss ->
   let lst = npseq_to_list ss in
   let%bind fs = bind_map_list simpl_statement lst in
-  let aux : _ -> (expression option -> expression result) -> _ = fun prec cur ->
+  let aux : _ -> (expression option -> expression result) -> _ =
+    fun prec cur ->
       let%bind res = cur prec in
       ok @@ Some res in
   ok @@ fun (expr' : _ option) ->

src/test/.gitignore

@@ -0,0 +1 @@
+/dune-project

src/test/integration_tests.ml

@@ -439,16 +439,11 @@ let dispatch_counter_contract () : unit result =
     e_pair (e_typed_list [] t_operation) (e_int (op 42 n)) in
   expect_eq_n program "main" make_input make_expected
 
-let basic_mligo () : unit result =
+let failwith_mligo () : unit result =
-  let%bind typed = mtype_file ~debug_simplify:true "./contracts/basic.mligo" in
+  let%bind program = mtype_file "./contracts/failwith.mligo" in
-  let%bind result = evaluate_typed "foo" typed in
+  let make_input = e_pair (e_unit ()) (e_unit ()) in
-  Ligo.AST_Typed.assert_value_eq (Ligo.AST_Typed.Combinators.e_a_empty_int (42 + 127), result)
+  let make_expected = e_pair (e_typed_list [] t_operation) (e_unit ()) in
-
+  expect_eq program "main" make_input make_expected
-let counter_mligo () : unit result =
-  let%bind program = mtype_file "./contracts/counter.mligo" in
-  let make_input = fun n-> e_pair (e_int n) (e_int 42) in
-  let make_expected = fun n -> e_pair (e_typed_list [] t_operation) (e_int (42 + n)) in
-  expect_eq_n program "main" make_input make_expected
 
 let guess_the_hash_mligo () : unit result =
   let%bind program = mtype_file "./contracts/new-syntax.mligo" in
@@ -456,6 +451,91 @@ let guess_the_hash_mligo () : unit result =
   let make_expected = fun n -> e_pair (e_typed_list [] t_operation) (e_int (42 + n)) in
   expect_eq_n program "main" make_input make_expected
 
+let guess_string_mligo () : unit result =
+  let%bind program = mtype_file "./contracts/guess_string.mligo" in
+  let make_input = fun n -> e_pair (e_int n) (e_int 42) in
+  let make_expected = fun n -> e_pair (e_typed_list [] t_operation) (e_int (42 + n))
+  in expect_eq_n program "main" make_input make_expected
+
+let basic_mligo () : unit result =
+  let%bind typed = mtype_file ~debug_simplify:true "./contracts/basic.mligo" in
+  let%bind result = evaluate_typed "foo" typed in
+  Ligo.AST_Typed.assert_value_eq
+    (Ligo.AST_Typed.Combinators.e_a_empty_int (42 + 127), result)
+
+let counter_mligo () : unit result =
+  let%bind program = mtype_file "./contracts/counter.mligo" in
+  let make_input n = e_pair (e_int n) (e_int 42) in
+  let make_expected n = e_pair (e_typed_list [] t_operation) (e_int (42 + n)) in
+  expect_eq_n program "main" make_input make_expected
+
+let let_in_mligo () : unit result =
+  let%bind program = mtype_file "./contracts/letin.mligo" in
+  let make_input n = e_pair (e_int n) (e_pair (e_int 3) (e_int 5)) in
+  let make_expected n =
+    e_pair (e_typed_list [] t_operation) (e_pair (e_int (7+n)) (e_int (3+5)))
+  in expect_eq_n program "main" make_input make_expected
+
+let match_variant () : unit result =
+  let%bind program = mtype_file "./contracts/match.mligo" in
+  let make_input n =
+    e_pair (e_constructor "Sub" (e_int n)) (e_int 3) in
+  let make_expected n =
+    e_pair (e_typed_list [] t_operation) (e_int (3-n))
+  in expect_eq_n program "main" make_input make_expected
+
+let match_matej () : unit result =
+  let%bind program = mtype_file "./contracts/match_bis.mligo" in
+  let make_input n =
+    e_pair (e_constructor "Decrement" (e_int n)) (e_int 3) in
+  let make_expected n =
+    e_pair (e_typed_list [] t_operation) (e_int (3-n))
+  in expect_eq_n program "main" make_input make_expected
+
+let mligo_list () : unit result =
+  let%bind program = mtype_file "./contracts/list.mligo" in
+  let make_input n =
+    e_pair (e_list [e_int n; e_int (2*n)])
+           (e_pair (e_int 3) (e_list [e_int 8])) in
+  let make_expected n =
+    e_pair (e_typed_list [] t_operation)
+      (e_pair (e_int (n+3)) (e_list [e_int (2*n)]))
+  in expect_eq_n program "main" make_input make_expected
+
+let lambda_mligo () : unit result =
+  let%bind program = mtype_file "./contracts/lambda.mligo" in
+  let make_input = e_pair (e_unit ()) (e_unit ()) in
+  let make_expected = (e_unit ()) in
+  expect_eq program "main" make_input make_expected
+
+let lambda_ligo () : unit result =
+  let%bind program = type_file "./contracts/lambda.ligo" in
+  let make_input = e_pair (e_unit ()) (e_unit ()) in
+  let make_expected = (e_unit ()) in
+  expect_eq program "main" make_input make_expected
+
+let lambda2_mligo () : unit result =
+  let%bind program = mtype_file "./contracts/lambda2.mligo" in
+  let make_input = e_pair (e_unit ()) (e_unit ()) in
+  let make_expected = (e_unit ()) in
+  expect_eq program "main" make_input make_expected
+
+let website1_ligo () : unit result =
+  let%bind program = type_file "./contracts/website1.ligo" in
+  let make_input = fun n-> e_pair (e_int n) (e_int 42) in
+  let make_expected = fun _n -> e_pair (e_typed_list [] t_operation) (e_int (42 + 1)) in
+  expect_eq_n program "main" make_input make_expected
+
+let website2_ligo () : unit result =
+  let%bind program = type_file "./contracts/website2.ligo" in
+  let make_input = fun n ->
+    let action = if n mod 2 = 0 then "Increment" else "Decrement" in
+    e_pair (e_constructor action (e_int n)) (e_int 42) in
+  let make_expected = fun n ->
+    let op = if n mod 2 = 0 then (+) else (-) in
+    e_pair (e_typed_list [] t_operation) (e_int (op 42 n)) in
+  expect_eq_n program "main" make_input make_expected
+
 let main = test_suite "Integration (End to End)" [
     test "type alias" type_alias ;
     test "function" function_ ;
@@ -490,7 +570,18 @@ let main = test_suite "Integration (End to End)" [
     test "closure" closure ;
     test "shared function" shared_function ;
     test "higher order" higher_order ;
-    test "basic mligo" basic_mligo ;
+    test "basic (mligo)" basic_mligo ;
-    test "counter contract mligo" counter_mligo ;
+    test "counter contract (mligo)" counter_mligo ;
-    (* test "guess the hash mligo" guess_the_hash_mligo ; *)
+    test "let-in (mligo)" let_in_mligo ;
+    test "match variant (mligo)" match_variant ;
+    test "match variant 2 (mligo)" match_matej ;
+    (* test "list matching (mligo)" mligo_list ; *)
+    (* test "guess the hash mligo" guess_the_hash_mligo ; WIP? *)
+    (* test "failwith mligo" failwith_mligo ; *)
+    (* test "guess string mligo" guess_string_mligo ; WIP? *)
+    test "lambda mligo" lambda_mligo ;
+    test "lambda ligo" lambda_ligo ;
+    (* test "lambda2 mligo" lambda2_mligo ; *)
+    test "website1 ligo" website1_ligo ;
+    test "website2 ligo" website2_ligo ;
   ]

src/test/test_helpers.ml

@@ -5,6 +5,35 @@ type test =
   | Test_suite of (string * test list)
   | Test of test_case
 
+let error_pp out (e : error) =
+    let open JSON_string_utils in
+  let message =
+    let opt = e |> member "message" |> string in
+    let msg = Option.unopt ~default:"" opt in
+    if msg = ""
+    then ""
+    else ": " ^ msg in
+  let error_code =
+    let error_code = e |> member "error_code" in
+    match error_code with
+    | `Null -> ""
+    | _ -> " (" ^ (J.to_string error_code) ^ ")" in
+  let title =
+    let opt = e |> member "title" |> string in
+    Option.unopt ~default:"" opt in
+  let data =
+    let data = e |> member "data" in
+    match data with
+    | `Null -> ""
+    | _ -> " " ^ (J.to_string data) ^ "\n" in
+  let infos =
+    let infos = e |> member "infos" in
+    match infos with
+    | `Null -> ""
+    | _ -> " " ^ (J.to_string infos) ^ "\n" in
+  Format.fprintf out "%s%s%s.\n%s%s" title error_code message data infos
+
+
 let test name f =
   Test (
     Alcotest.test_case name `Quick @@ fun () ->
@@ -80,12 +109,12 @@ let expect_eq_n_aux ?options lst program entry_point make_input make_expected =
   let%bind _ = bind_map_list aux lst in
   ok ()
 
-let expect_eq_n ?options = expect_eq_n_aux ?options [0 ; 2 ; 42 ; 163 ; -1]
+let expect_eq_n ?options = expect_eq_n_aux ?options [0 ; 1 ; 2 ; 42 ; 163 ; -1]
-let expect_eq_n_pos ?options = expect_eq_n_aux ?options [0 ; 2 ; 42 ; 163]
+let expect_eq_n_pos ?options = expect_eq_n_aux ?options [0 ; 1 ; 2 ; 42 ; 163]
 let expect_eq_n_strict_pos ?options = expect_eq_n_aux ?options [2 ; 42 ; 163]
-let expect_eq_n_pos_small ?options = expect_eq_n_aux ?options [0 ; 2 ; 10]
+let expect_eq_n_pos_small ?options = expect_eq_n_aux ?options [0 ; 1 ; 2 ; 10]
-let expect_eq_n_strict_pos_small ?options = expect_eq_n_aux ?options [2 ; 10]
+let expect_eq_n_strict_pos_small ?options = expect_eq_n_aux ?options [1 ; 2 ; 10]
-let expect_eq_n_pos_mid = expect_eq_n_aux [0 ; 2 ; 10 ; 33]
+let expect_eq_n_pos_mid = expect_eq_n_aux [0 ; 1 ; 2 ; 10 ; 33]
 
 let expect_n_pos_small ?options = expect_n_aux ?options [0 ; 2 ; 10]
 let expect_n_strict_pos_small ?options = expect_n_aux ?options [2 ; 10]

src/transpiler/transpiler.ml

@@ -93,6 +93,7 @@ let rec translate_type (t:AST.type_value) : type_value result =
   | T_constant ("tez", []) -> ok (T_base Base_tez)
   | T_constant ("string", []) -> ok (T_base Base_string)
   | T_constant ("address", []) -> ok (T_base Base_address)
+  | T_constant ("timestamp", []) -> ok (T_base Base_timestamp)
   | T_constant ("unit", []) -> ok (T_base Base_unit)
   | T_constant ("operation", []) -> ok (T_base Base_operation)
   | T_constant ("contract", [x]) ->
@@ -603,7 +604,7 @@ let extract_constructor (v : value) (tree : _ Append_tree.t') : (string * value
     | Leaf (k, t), v -> ok (k, v, t)
     | Node {a}, D_left v -> aux (a, v)
     | Node {b}, D_right v -> aux (b, v)
-    | _ -> simple_fail "bad constructor path"
+    | _ -> fail @@ internal_assertion_failure "bad constructor path"
   in
   let%bind (s, v, t) = aux (tree, v) in
   ok (s, v, t)
@@ -617,7 +618,7 @@ let extract_tuple (v : value) (tree : AST.type_value Append_tree.t') : ((value *
         let%bind a' = aux (a, va) in
         let%bind b' = aux (b, vb) in
         ok (a' @ b')
-    | _ -> simple_fail "bad tuple path"
+    | _ -> fail @@ internal_assertion_failure "bad tuple path"
   in
   aux (tree, v)
 
@@ -630,7 +631,7 @@ let extract_record (v : value) (tree : _ Append_tree.t') : (_ list) result =
         let%bind a' = aux (a, va) in
         let%bind b' = aux (b, vb) in
         ok (a' @ b')
-    | _ -> simple_fail "bad record path"
+    | _ -> fail @@ internal_assertion_failure "bad record path"
   in
   aux (tree, v)
 

src/typer/typer.ml

@@ -145,24 +145,24 @@ module Errors = struct
     ] in
     error ~data title message ()
 
-  let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_value) ~(expression : O.value) (loc:Location.t) () =
+  let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_value) ~(expression : I.expression) (loc:Location.t) () =
     let title = (thunk "type error") in
     let message () = msg in
     let data = [
       ("expected"   , fun () -> Format.asprintf "%s" expected);
       ("actual"     , fun () -> Format.asprintf "%a" O.PP.type_value actual);
-      ("expression" , fun () -> Format.asprintf "%a" O.PP.value expression) ;
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
       ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
     ] in
     error ~data title message ()
 
-  let type_error ?(msg="") ~(expected: O.type_value) ~(actual: O.type_value) ~(expression : O.value) (loc:Location.t) () =
+  let type_error ?(msg="") ~(expected: O.type_value) ~(actual: O.type_value) ~(expression : I.expression) (loc:Location.t) () =
     let title = (thunk "type error") in
     let message () = msg in
     let data = [
       ("expected"   , fun () -> Format.asprintf "%a" O.PP.type_value expected);
       ("actual"     , fun () -> Format.asprintf "%a" O.PP.type_value actual);
-      ("expression" , fun () -> Format.asprintf "%a" O.PP.value expression) ;
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ;
       ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
     ] in
     error ~data title message ()
@@ -206,6 +206,13 @@ module Errors = struct
     ] in
     error ~data title message ()
 
+  let constant_error loc =
+    let title () = "typing constant" in
+    let message () = "" in
+    let data = [
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc ) ;
+    ] in
+    error ~data title message
 end
 open Errors
 
@@ -237,8 +244,8 @@ and type_declaration env : I.declaration -> (environment * O.declaration option)
       ok (env', Some (O.Declaration_constant ((make_n_e name ae') , (env , env'))))
     )
 
-and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> Location.t -> o O.matching result =
+and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> I.expression -> Location.t -> o O.matching result =
-  fun f e t i loc -> match i with
+  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)
@@ -286,6 +293,13 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
           let%bind acc = match acc with
             | None -> ok (Some variant)
             | Some variant' -> (
+                trace (type_error
+                         ~msg:"in match variant"
+                         ~expected:variant
+                         ~actual:variant'
+                         ~expression:ae
+                         loc
+                      ) @@
                 Ast_typed.assert_type_value_eq (variant , variant') >>? fun () ->
                 ok (Some variant)
               ) in
@@ -370,14 +384,13 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
     ok @@ make_a_e ~location expr tv e in
   let main_error =
     let title () = "typing expression" in
-    let content () =
+    let content () = "" in
-      match L.get () with
+    let data = [
-      | "" ->
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
-        Format.asprintf "Expression: %a\n" I.PP.expression ae
+      ("location" , fun () -> Format.asprintf "%a" Location.pp @@ Location.get_location ae) ;
-      | l ->
+      ("misc" , fun () -> L.get ()) ;
-        Format.asprintf "Expression: %a\nLog: %s\n" I.PP.expression ae l
+    ] in
-    in
+    error ~data title content in
-    error title content in
   trace main_error @@
   match Location.unwrap ae with
   (* Basic *)
@@ -504,7 +517,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
             @@ List.map fst lst' in
           let%bind annot = bind_map_option get_t_map_key tv_opt in
           trace (simple_info "empty map expression without a type annotation") @@
-          O.merge_annotation annot sub
+          O.merge_annotation annot sub (needs_annotation ae "this map literal")
         in
         let%bind value_type =
           let%bind sub =
@@ -513,7 +526,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
             @@ List.map snd lst' in
           let%bind annot = bind_map_option get_t_map_value tv_opt in
           trace (simple_info "empty map expression without a type annotation") @@
-          O.merge_annotation annot sub
+          O.merge_annotation annot sub (needs_annotation ae "this map literal")
         in
         ok (t_map key_type value_type ())
       in
@@ -556,12 +569,13 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
   | E_constant (name, lst) ->
       let%bind lst' = bind_list @@ List.map (type_expression e) lst in
       let tv_lst = List.map get_type_annotation lst' in
-      let%bind (name', tv) = type_constant name tv_lst tv_opt ae.location in
+      let%bind (name', tv) =
+        type_constant name tv_lst tv_opt ae.location in
       return (E_constant (name' , lst')) tv
   | E_application (f, arg) ->
-      let%bind f = type_expression e f in
+      let%bind f' = type_expression e f in
       let%bind arg = type_expression e arg in
-      let%bind tv = match f.type_annotation.type_value' with
+      let%bind tv = match f'.type_annotation.type_value' with
         | T_function (param, result) ->
             let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in
             ok result
@@ -569,10 +583,10 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
           fail @@ type_error_approximate
             ~expected:"should be a function type"
             ~expression:f
-            ~actual:f.type_annotation
+            ~actual:f'.type_annotation
-            f.location
+            f'.location
       in
-      return (E_application (f , arg)) tv
+      return (E_application (f' , arg)) tv
   | E_look_up dsi ->
       let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in
       let%bind (src, dst) = get_t_map ds.type_annotation in
@@ -607,7 +621,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
           return (O.E_matching (ex' , m')) (t_unit ())
         )
       | _ -> (
-          let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m ae.location in
+          let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m ae ae.location in
           let tvs =
             let aux (cur:O.value O.matching) =
               match cur with
@@ -639,7 +653,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
                       ~msg:"first part of the sequence should be of unit type"
                       ~expected:(O.t_unit ())
                       ~actual:a'_type_annot
-                      ~expression:a'
+                      ~expression:a
                       a'.location) @@
       Ast_typed.assert_type_value_eq (t_unit () , a'_type_annot) in
     return (O.E_sequence (a' , b')) (get_type_annotation b')
@@ -652,7 +666,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
                       ~msg:"while condition isn't of type bool"
                       ~expected:(O.t_bool ())
                       ~actual:t_expr'
-                      ~expression:expr'
+                      ~expression:expr
                       expr'.location) @@
       Ast_typed.assert_type_value_eq (t_bool () , t_expr') in
     let t_body' = get_type_annotation body' in
@@ -661,7 +675,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
                      ~msg:"while body isn't of unit type"
                      ~expected:(O.t_unit ())
                      ~actual:t_body'
-                     ~expression:body'
+                     ~expression:body
                      body'.location) @@
       Ast_typed.assert_type_value_eq (t_unit () , t_body') in
     return (O.E_loop (expr' , body')) (t_unit ())
@@ -697,7 +711,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
                      ~msg:"type of the expression to assign doesn't match left-hand-side"
                      ~expected:assign_tv
                      ~actual:t_expr'
-                     ~expression:expr'
+                     ~expression:expr
                      expr'.location) @@
       Ast_typed.assert_type_value_eq (assign_tv , t_expr') in
     return (O.E_assign (typed_name , path' , expr')) (t_unit ())
@@ -710,7 +724,11 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
   | E_annotation (expr , te) ->
     let%bind tv = evaluate_type e te in
     let%bind expr' = type_expression ~tv_opt:tv e expr in
-    let%bind type_annotation = O.merge_annotation (Some tv) (Some expr'.type_annotation) in
+    let%bind type_annotation =
+      O.merge_annotation
+        (Some tv)
+        (Some expr'.type_annotation)
+        (internal_assertion_failure "merge_annotations (Some ...) (Some ...) failed") in
     ok {expr' with type_annotation}
 
 
@@ -720,12 +738,13 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt
   let%bind typer =
     trace_option (unrecognized_constant name loc) @@
     Map.String.find_opt name ct in
+  trace (constant_error loc) @@
   typer lst tv_opt
 
 let untype_type_value (t:O.type_value) : (I.type_expression) result =
   match t.simplified with
   | Some s -> ok s
-  | _ -> simple_fail "trying to untype generated type"
+  | _ -> fail @@ internal_assertion_failure "trying to untype generated type"
 
 let untype_literal (l:O.literal) : I.literal result =
   let open I in

vendors/ligo-utils/simple-utils/trace.ml

@@ -200,6 +200,7 @@ let prepend_info = fun info err ->
 let simple_error str () = mk_error ~title:(thunk str) ()
 let simple_info str () = mk_info ~title:(thunk str) ()
 let simple_fail str = fail @@ simple_error str
+let internal_assertion_failure str = simple_error ("assertion failed: " ^ str)
 
 (**
    To be used when you only want to signal an error. It can be useful when

vendors/opam-repository-tools/rewrite-local-opam-repository.sh

@@ -1,13 +1,55 @@
-#!/bin/bash
+#!/bin/sh
-set -euET -o pipefail
+
-main(){
+# Stop on error.
-  root_dir="$(pwd | sed -e 's/\\/\\\\/' | sed -e 's/&/\\\&/' | sed -e 's/~/\\~/')"
+set -e
+
+# Defensive checks. We're going to remove an entire folder so this script is somewhat dangerous. Better check in advance what can go wrong in the entire execution of the script.
+if test -e index.tar.gz && test -e packages && test -e repo && test -e urls.txt; then
+  if test -d vendors/; then
+   if test -d "$PWD"; then
+      if command -v sed   >/dev/null 2>&1 \
+      && command -v rm    >/dev/null 2>&1 \
+      && command -v mkdir >/dev/null 2>&1 \
+      && command -v cp    >/dev/null 2>&1 \
+      && command -v find  >/dev/null 2>&1 \
+      && command -v xargs >/dev/null 2>&1 \
+      && command -v opam  >/dev/null 2>&1; then
+
+      # Escape the current directory, to be used as the replacement part of the sed regular expression
+      escaped_project_root="$(printf %s "$PWD" | sed -e 's/\\/\\\\/' | sed -e 's/&/\\\&/' | sed -e 's/~/\\~/')"
+
+      # Recreate vendors/ligo-opam-repository-local-generated which contains a copy of the files related to the opam repository
       rm -fr vendors/ligo-opam-repository-local-generated
       mkdir vendors/ligo-opam-repository-local-generated
-  cp -a index.tar.gz packages repo urls.txt vendors/ligo-opam-repository-local-generated
+      cp -pR index.tar.gz packages repo urls.txt vendors/ligo-opam-repository-local-generated
+
+      # Rewrite the URLs in the opam repository to point to the project root
+      (
         cd vendors/ligo-opam-repository-local-generated
-  grep -r --null -l src: | grep -z 'opam$' | xargs -0 \
+        find . -type f -name opam -print0 | xargs -0 sed -i -e 's~src:  *"https://gitlab.com/ligolang/ligo/-/archive/master/ligo\.tar\.gz"~src: "file://'"$escaped_project_root"'"~'
-    sed -i -e 's~src:  *"https://gitlab.com/ligolang/ligo/-/archive/master/ligo\.tar\.gz"~src: "file://'"$root_dir"'"~'
+      )
-  # TODO: run the update.sh script adequately to regenerate the index.tar.gz etc. in the local repo
+
-}
+      # Regenerate the index.tar.gz etc. in the local repo
-if main; then exit 0; else exit $?; fi
+      (
+        cd vendors/ligo-opam-repository-local-generated
+        opam admin index
+        opam admin cache
+      )
+      else
+        echo "One of the following commands is unavailable: sed rm mkdir cp find xargs opam."
+        exit 1
+      fi
+    else
+      echo "Unable to access the current directory as indicated by PWD. Was the CWD of the current shell removed?"
+      exit 1
+    fi
+
+  else
+    echo "Cannot find the directory vendors/ in the current directory"
+    exit 1
+  fi
+else
+  echo "Cannot find some of the following files in the current directory"
+  echo "index.tar.gz packages repo urls.txt"
+  exit 1
+fi