diff options
| author | Son Ho | 2022-11-14 09:06:15 +0100 |
|---|---|---|
| committer | Son HO | 2022-11-14 14:21:04 +0100 |
| commit | 3eba613a9ff9d5c265fbe2676f6bd324728d9ca4 (patch) | |
| tree | eeac1d917f398906ab4aeaa3627561d980f0492a /Makefile | |
| parent | 2a0ecfbef81231a394df71817a4cd9e81582b7de (diff) | |
Implement a pass to decompose nested patterns in let-bindings
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -146,7 +146,7 @@ tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) # This generates very ugly code, but is good to test the translation. .PHONY: test-transp-betree_main test-transp-betree_main: transp-betree_main -test-transp-betree_main: OPTIONS += -backend fstar -unfold-monads -test-trans-units +test-transp-betree_main: OPTIONS += -backend fstar -test-trans-units test-transp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) test-transp-betree_main: BACKEND_SUBDIR := "fstar" test-transp-betree_main: SUBDIR:=betree_back_stateful @@ -186,14 +186,14 @@ transp-%: gen-llbcp-% tfstarp-% echo "# Test $* done" .PHONY: tfstar-% -tfstar-%: OPTIONS += -backend fstar -unfold-monads -test-trans-units +tfstar-%: OPTIONS += -backend fstar -test-trans-units tfstar-%: BACKEND_SUBDIR := fstar tfstar-%: $(AENEAS_CMD) # "p" stands for "Polonius" .PHONY: tfstarp-% -tfstarp-%: OPTIONS += -backend fstar -unfold-monads -test-trans-units +tfstarp-%: OPTIONS += -backend fstar -test-trans-units tfstarp-%: BACKEND_SUBDIR := fstar tfstarp-%: $(AENEAS_CMD) @@ -201,7 +201,7 @@ tfstarp-%: # TODO: -test-trans-units # It doesn't work on vec_push_fwd, I don't understand why. .PHONY: tcoq-% -tcoq-%: OPTIONS += -backend coq -decompose-monads +tcoq-%: OPTIONS += -backend coq tcoq-%: BACKEND_SUBDIR := coq tcoq-%: $(AENEAS_CMD) |