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
Makefile 
# -*- Makefile -*-

# --------------------------------------------------------------------
DUNE      ?= dune
ECARGS    ?=
ECTOUT    ?= 10
ECJOBS    ?= 0
ECEXTRA   ?= --report=report.log
ECPROVERS ?= Alt-Ergo Z3 CVC4
CHECKPY   ?=
CHECK     := $(CHECKPY) scripts/testing/runtest
CHECK     += --bin-args="$(ECARGS)" --bin-args="$(ECPROVERS:%=-p %)"
CHECK     += --timeout="$(ECTOUT)" --jobs="$(ECJOBS)"
CHECK     += $(ECEXTRA) config/tests.config

# --------------------------------------------------------------------
UNAME_P = $(shell uname -p)
UNAME_S = $(shell uname -s)

# --------------------------------------------------------------------
.PHONY: default build byte native tests check examples
.PHONY: clean install uninstall

default: build
	@true

build:
	rm -f src/ec.exe ec.native
	dune build -p easycrypt
	ln -sf src/ec.exe ec.native
ifeq ($(UNAME_P)-$(UNAME_S),arm-Darwin)
	-codesign -f -s - src/ec.exe
endif

install: build
	$(DUNE) install

uninstall:
	$(DUNE) uninstall

check: stdlib examples

stdlib: build
	$(CHECK) prelude stdlib

examples: build
	$(CHECK) examples mee-cbc

check: stdlib examples
	@true

clean:
	rm -f ec.native && $(DUNE) clean
	find theories examples -name '*.eco' -exec rm '{}' ';'

clean_eco:
	find theories examples -name '*.eco' -exec rm '{}' ';'
back to top