Skip to main content

Browse the archive

Revision ee26cc55310c92dae5f6afeb38d2b2ea9413569e authored by Alley Stoughton on 15 May 2023, 19:51:42 UTC, committed by Pierre-Yves Strub on 16 May 2023, 07:04:10 UTC 
Commit b2106aa suppressed additional parentheses around match ... end in all circumstances, even though on the left and right of applications the parser requires parentheses, the theory being this makes it easier for humans to scan. So this commit inserts parentheses around matches in applications, but not elsewhere (e.g., not in infix operators). See below for examples. [The pretty printer needs a major redesign, so this is another stopgap measure.]
 
require import AllCore List. type t = [ A of int | B of bool].

(* the following formulas now parse and pretty-print the same *)

lemma foo1 (f : int -> bool) :
f (match A 3 with | A a => a | B b => if b then 1 else 2 end).
proof. abort.

lemma foo2 :
(match A 3 with | A a => fun _ => a | B b => fun _ => 2 end) 3 = 4.
proof. abort.

lemma foo3 (f : (int -> int) -> (int -> int)) :
f (match A 3 with | A a => fun _ => a | B b => fun _ => 2 end) 3 = 4.
proof. abort.

lemma foo4 (f : int -> bool) :
f (1 + match A 3 with | A a => a | B b => if b then 1 else 2 end).
proof. abort.

lemma foo5 (f : int -> bool) :
f (match A 3 with | A a => a | B b => if b then 1 else 2 end + 1).
proof. abort.

lemma foo6 (f : int -> bool) :
f (3 + match A 3 with | A a => a | B b => if b then 1 else 2 end + 1).
proof. abort.
1 parent 94538c5
Raw File
default.nix 
{ withProvers ? false, devDeps ? [] }:

with import <nixpkgs> {};

let why3_local =
  why3.overrideAttrs (o : rec {
    version = "1.6.0";
    src = fetchurl {
      url = "https://why3.gitlabpages.inria.fr/releases/${o.pname}-${version}.tar.gz";
      sha256 = "sha256-hFvM6kHScaCtcHCc6Vezl9CR7BFbiKPoTEh7kj0ZJxw=";
    };
  });
in
let why3 = why3_local; in

let provers =
  if withProvers then [
    alt-ergo
    z3
  ] else []; in

stdenv.mkDerivation {
  pname = "easycrypt";
  version = "git";
  src = ./.;

  buildInputs = [ git ] ++ (with ocamlPackages; [
    ocaml
    findlib
    batteries
    camlp-streams
    dune_3
    dune-build-info
    dune-site
    inifiles
    menhir
    menhirLib
    yojson
    why3
    zarith
  ]);

  propagatedBuildInputs = [ why3 ]
    ++ devDeps
    ++ provers;

  installPhase = ''
    runHook preInstall
    dune install --prefix $out -p $pname
    runHook postInstall
  '';
}
back to top