diff --git a/flake.nix b/flake.nix index 76593bca24..d8e3c51bf8 100644 --- a/flake.nix +++ b/flake.nix @@ -58,7 +58,6 @@ (_: prev: with prev; { ocamlPackages = ocaml-ng.ocamlPackages_4_14; - coqPackages = coqPackages_8_13; ocamlformat = ocaml-ng.ocamlPackages_4_14.ocamlformat_0_21_0; }) rust-overlay.overlays.default diff --git a/nix/ligo.nix b/nix/ligo.nix index 6f0a329599..10592521d7 100644 --- a/nix/ligo.nix +++ b/nix/ligo.nix @@ -29,7 +29,6 @@ in nativeBuildInputs = [ menhir ocaml-recovery-parser - coq_8_13 crunch odoc python3Packages.jsonschema @@ -100,7 +99,6 @@ in linol linol-lwt dune-configurator # ??? - coq_8_13 # ??? alcotest # with-test ppx_expect # with-test ppx_inline_test # with-test diff --git a/nix/overlay.nix b/nix/overlay.nix index 64f96d4ccc..83cd418ae4 100644 --- a/nix/overlay.nix +++ b/nix/overlay.nix @@ -353,10 +353,6 @@ with prev; { }; }); }); - coq_8_13 = coq_8_13.override { - customOCamlPackages = final.ocaml-ng.ocamlPackages_4_14; - buildIde = false; - }; tree-sitter = tree-sitter.override ( # override for getting tree-sitter version 0.25.3 let diff --git a/src/bin/expect_tests/top_level_binding_pattern_cameligo.ml b/src/bin/expect_tests/top_level_binding_pattern_cameligo.ml index ffcb0d8569..5545deb6e5 100644 --- a/src/bin/expect_tests/top_level_binding_pattern_cameligo.ml +++ b/src/bin/expect_tests/top_level_binding_pattern_cameligo.ml @@ -1052,7 +1052,7 @@ let%expect_test _ = Called from Cli_helpers.return_result_lwt.get_formatted_result in file "src/main/helpers/cli_helpers.ml", line 185, characters 19-84 Re-raised at Cli.run in file "src/bin/cli.ml", line 3757, characters 21-30 Called from Cli_expect_tests__Cli_expect.run_ligo_bad in file "src/bin/expect_tests/cli_expect.ml", line 46, characters 18-31 - Called from Cli_expect_tests__Top_level_binding_pattern_cameligo.(fun) in file "src/bin/expect_tests/top_level_binding_pattern_cameligo.ml", line 970, characters 2-156 + Called from Cli_expect_tests__Top_level_binding_pattern_cameligo.(fun) in file "src/bin/expect_tests/top_level_binding_pattern_cameligo.ml", line 961, characters 2-156 Called from Expect_test_collector.Make.Instance_io.exec in file "collector/expect_test_collector.ml", line 234, characters 12-19 |}] let%expect_test _ = diff --git a/src/bin/expect_tests/top_level_binding_pattern_jsligo.ml b/src/bin/expect_tests/top_level_binding_pattern_jsligo.ml index 48b0cda891..6cd810cb1e 100644 --- a/src/bin/expect_tests/top_level_binding_pattern_jsligo.ml +++ b/src/bin/expect_tests/top_level_binding_pattern_jsligo.ml @@ -366,5 +366,5 @@ let%expect_test _ = Called from Cli_helpers.return_result_lwt.get_formatted_result in file "src/main/helpers/cli_helpers.ml", line 185, characters 19-84 Re-raised at Cli.run in file "src/bin/cli.ml", line 3757, characters 21-30 Called from Cli_expect_tests__Cli_expect.run_ligo_bad in file "src/bin/expect_tests/cli_expect.ml", line 46, characters 18-31 - Called from Cli_expect_tests__Top_level_binding_pattern_jsligo.(fun) in file "src/bin/expect_tests/top_level_binding_pattern_jsligo.ml", line 284, characters 2-155 + Called from Cli_expect_tests__Top_level_binding_pattern_jsligo.(fun) in file "src/bin/expect_tests/top_level_binding_pattern_jsligo.ml", line 275, characters 2-155 Called from Expect_test_collector.Make.Instance_io.exec in file "collector/expect_test_collector.ml", line 234, characters 12-19 |}] diff --git a/src/bin/expect_tests/warnings.ml b/src/bin/expect_tests/warnings.ml index 8ef5210862..a8bea1f6b5 100644 --- a/src/bin/expect_tests/warnings.ml +++ b/src/bin/expect_tests/warnings.ml @@ -158,7 +158,7 @@ let%expect_test _ = Called from Cli_helpers.return_result_lwt.get_formatted_result in file "src/main/helpers/cli_helpers.ml", line 185, characters 19-84 Re-raised at Cli.run in file "src/bin/cli.ml", line 3757, characters 21-30 Called from Cli_expect_tests__Cli_expect.run_ligo_bad in file "src/bin/expect_tests/cli_expect.ml", line 46, characters 18-31 - Called from Cli_expect_tests__Warnings.(fun) in file "src/bin/expect_tests/warnings.ml", line 62, characters 2-144 + Called from Cli_expect_tests__Warnings.(fun) in file "src/bin/expect_tests/warnings.ml", line 107, characters 2-144 Called from Expect_test_collector.Make.Instance_io.exec in file "collector/expect_test_collector.ml", line 234, characters 12-19 |}] let%expect_test _ = @@ -232,7 +232,7 @@ let%expect_test _ = Called from Cli_helpers.return_result_lwt.get_formatted_result in file "src/main/helpers/cli_helpers.ml", line 185, characters 19-84 Re-raised at Cli.run in file "src/bin/cli.ml", line 3757, characters 21-30 Called from Cli_expect_tests__Cli_expect.run_ligo_bad in file "src/bin/expect_tests/cli_expect.ml", line 46, characters 18-31 - Called from Cli_expect_tests__Warnings.(fun) in file "src/bin/expect_tests/warnings.ml", line 84, characters 2-88 + Called from Cli_expect_tests__Warnings.(fun) in file "src/bin/expect_tests/warnings.ml", line 165, characters 2-88 Called from Expect_test_collector.Make.Instance_io.exec in file "collector/expect_test_collector.ml", line 234, characters 12-19 |}] (* some check about the warnings of the E_constructor cases *) diff --git a/src/coq/.gitignore b/src/coq/.gitignore deleted file mode 100644 index 7676ce638e..0000000000 --- a/src/coq/.gitignore +++ /dev/null @@ -1,10 +0,0 @@ -Makefile.coq -Makefile.coq.conf -.Makefile.coq.d -.lia.cache -*.aux -*.glob -*.vo -*.vok -*.vos -.Makefile.coq.d diff --git a/src/coq/Makefile b/src/coq/Makefile deleted file mode 100644 index e5b91579ff..0000000000 --- a/src/coq/Makefile +++ /dev/null @@ -1,10 +0,0 @@ -include Makefile.coq - -HIDE := $(if $(VERBOSE),,@) - -Makefile.coq: - coq_makefile -f _CoqProject -o Makefile.coq - -clean:: - $(HIDE)rm .lia.cache Makefile.coq Makefile.coq.conf -f - $(HIDE)find . -name .\*.aux -type f -delete diff --git a/src/coq/README.md b/src/coq/README.md deleted file mode 100644 index 9c9724b338..0000000000 --- a/src/coq/README.md +++ /dev/null @@ -1,57 +0,0 @@ -## Ligo_coq - -This directory contains Coq code implementing part of the "backend" -compiler. - -Extraction is performed in -[extraction.v](../coq_ocaml/extraction.v). This results in a module -`Ligo_coq_ocaml` which contains the various modules extracted from -Coq, as listed in the [dune file](../coq_ocaml/dune). - -## Development - -To develop Coq here, you could simply edit .v files and `dune build` -(or `nix build ...`.) But this is not very nice. - -You can use Proof General like so: - -```sh -# prepare to use PG: -cd src/coq -make -# ...use PG... -# prepare to use dune again: -make clean -dune build -``` - -(Dune will complain if you don't `make clean` the PG files out.) - -## Overview - -At the moment, only pass 14-stacking is implemented in -Coq. `Ligo_coq_ocaml.Compiler` is integrated into the rest of the LIGO -compiler in -[15-stacking/compiler_program.ml](../passes/15-stacking/compiler_program.ml). Certain -hypotheses in the Coq compiler are instantiated there, too. - -An intermediate language is defined in [ligo.v](./ligo.v). This is -emitted by the previous pass in -[14-scoping/scoping.ml](../passes/14-scoping/scoping.ml). - -In [micheline.v](./micheline.v) a Coq version Micheline is defined -which extracts directly to Tezos_micheline. - -This Micheline is used for source (IR) types in [ligo.v](./ligo.v) and -target (Michelson) types and programs in -[michelson.v](./michelson.v). This allows us to use the identity as -the type translation function for the compiler. - -The main compiler function is `compile_expr` in -[compiler.v](./compiler.v), which translates the IR expressions to -Michelson. (We need to optimise the resulting Micheline still, but -that is not in Coq, yet.) - -The only current proof is a type preservation proof, stated at -`expr_type_preservation` and proved at `type_preservation`, in -[compiler.v](./compiler.v). diff --git a/src/coq/_CoqProject b/src/coq/_CoqProject deleted file mode 100644 index eaa7ae07d2..0000000000 --- a/src/coq/_CoqProject +++ /dev/null @@ -1,3 +0,0 @@ --R . ligo_coq -./ope.v -./compiler.v diff --git a/src/coq/co_de_bruijn.v b/src/coq/co_de_bruijn.v deleted file mode 100644 index f03c1994a1..0000000000 --- a/src/coq/co_de_bruijn.v +++ /dev/null @@ -1,446 +0,0 @@ -Local Set Warnings "-implicit-core-hint-db". -Set Implicit Arguments. -From Coq Require Import List Program.Equality. -Import ListNotations. - - -Inductive usage : Set := Drop | Keep. - -(* Valid triplets ([Drop,Keep,Drop,…], [1,…], [0,1,2,…]) where the xs list contains only the elements - of the ys list which are marked as Keep in the us list. *) -Inductive used {A : Type} : list usage -> list A -> list A -> Prop := -| Used_nil : used [] [] [] -| Used_drop {us y xs ys} : used us xs ys -> used (Drop :: us) xs (y :: ys) -| Used_keep {us y xs ys} : used us xs ys -> used (Keep :: us) (y :: xs) (y :: ys) -. - -#[export] Hint Constructors used. - -(* Example: *) -Goal used [Drop; Keep; Drop; Keep; Keep] - [ 1 ; 3 ; 4 ] - [0 ; 1 ; 2 ; 3 ; 4 ]. -repeat constructor. -Qed. - -Lemma used_app {A : Type} {us1 us2 : list usage} {xs1 xs2 ys1 ys2 : list A} : - used us1 xs1 ys1 -> - used us2 xs2 ys2 -> - used (us1 ++ us2) (xs1 ++ xs2) (ys1 ++ ys2). -Proof. - intros H1; induction H1; intros H2; auto; - constructor; eapply IHused; auto. -Qed. - -Lemma used_drops {A : Type} (xs : list A) : - used (repeat Drop (length xs)) [] xs. -Proof. - induction xs; simpl; auto. -Qed. - -Lemma used_keeps {A : Type} (xs : list A) : - used (repeat Keep (length xs)) xs xs. -Proof. - induction xs; simpl; auto. -Qed. - -#[export] Hint Resolve used_app. -#[export] Hint Resolve used_drops. -#[export] Hint Resolve used_keeps. - -Definition filter_keeps (us : list usage) : list usage := - filter (fun u => match u with | Keep => true | Drop => false end) us. - -(* Selects the elements of xs which are marked as Keep in us, discards the ones marked as Drop. - If xs is longer, Keep is assumed for the remaining elements; if us is longer, it is effectively - truncated to xs's length. These edge cases are likely placeholders for cases that should not happen, - preconditions like length us = length xs are used in lemmas like used_filter_keeps_right_usages. *) -Fixpoint select {A : Type} (us : list usage) (xs : list A) : list A := - match (us, xs) with - | ([], _) => xs - | (_, []) => [] - | (Drop :: us, _ :: xs) => select us xs - | (Keep :: us, x :: xs) => x :: select us xs - end. - -Lemma select_app : - forall {A : Type} (us1 us2 : list usage) (xs1 xs2 : list A), - length us1 = length xs1 -> - length us2 = length xs2 -> - select (us1 ++ us2) (xs1 ++ xs2) = select us1 xs1 ++ select us2 xs2. -Proof. - intros A us1; induction us1; intros us2 xs1 xs2 Hlen1 Hlen2; simpl in *; - destruct xs1; inversion Hlen1 as [Hlen1']; auto; - destruct a; simpl; try (apply f_equal); auto. -Qed. - -Inductive side : Set := Left | Right | Both. - -Definition splitting := list side. - -Inductive splits {A : Type} : list side -> list A -> list A -> list A -> Prop := -| Splits_nil : splits [] [] [] [] -| Splits_left {ss zs x xs ys} : splits ss zs xs ys -> splits (Left :: ss) (x :: zs) (x :: xs) ys -| Splits_right {ss zs xs y ys} : splits ss zs xs ys -> splits (Right :: ss) (y :: zs) xs (y :: ys) -| Splits_both {ss z zs xs ys} : splits ss zs xs ys -> splits (Both :: ss) (z :: zs) (z :: xs) (z :: ys) -. - -(* Example: *) -Goal splits [Left; Right; Left; Right; Both; Right] - [0 ; 1 ; 2 ; 3 ; 4 ; 5 ] - [0 ; 2 ; 4 ] (* Items marked Left or Both *) - [ 1 ; 3 ; 4 ; 5 ] (* Items marked Right or Both *). -repeat constructor. -Qed. - -#[export] Hint Constructors splits. - -(* If there are no elements in the left list, then the right list is equal to the original *) -Lemma splits_right {A : Type} : - forall (outer : splitting) (d1 d2 : list A), - splits outer d1 [] d2 -> - d1 = d2. -Proof. - intros; dependent induction H; subst; auto; - erewrite IHsplits by auto; auto. -Qed. - -(* If there are no elements in the left list, the sides are all Right *) -Lemma splits_right_rights {A : Type} : - forall (outer : splitting) (d1 d2 : list A), - splits outer d1 [] d2 -> - outer = repeat Right (length d1). -Proof. - intros; dependent induction H; auto; - simpl; erewrite <- IHsplits by auto; auto. -Qed. - -(* It is possible to prefix the left list and the original list with a number of elements, and put the - same number of Left as a prefix to the sides. *) -Lemma splits_lefts {A : Type} : - forall (outer : splitting) (g g' d1 d2 : list A), - splits outer d1 g d2 -> - splits (repeat Left (length g') ++ outer) (g' ++ d1) (g' ++ g) d2. -Proof. - intros outer g g'. - generalize dependent g. - generalize dependent outer. - induction g'; intros; auto; - apply IHg' in H; simpl; auto. -Qed. - -#[export] Hint Resolve splits_lefts. - -(* The original list can be copied to the left list by using the same number of Left sides. *) -Lemma splits_lefts' {A : Type} : - forall (g : list A), - splits (repeat Left (length g)) g g []. -Proof. - intros; - enough (splits (repeat Left (length g) ++ []) (g ++ []) (g ++ []) []) - by (repeat rewrite app_nil_r in H; auto); - eapply splits_lefts; auto. -Qed. - -#[export] Hint Resolve splits_lefts'. - -(* The left list contains only Keep elements, but the right list contains all elements (regardless of Keep or Drop) *) -Definition keep_right (u : usage) : side := - match u with - | Drop => Right - | Keep => Both - end. - -Definition keep_rights (us : list usage) : list side := - List.map keep_right us. - -(* The right list contains only Keep elements, but the left list contains all elements (regardless of Keep or Drop) *) -Definition keep_left (u : usage) : side := - match u with - | Drop => Left - | Keep => Both - end. - -Definition keep_lefts (us : list usage) : list side := - List.map keep_left us. - -(* Elements that appear in the left list (or both) are kept, those which only appear in the right list are dropped *) -Definition left_usage (s : side) : usage := - match s with - | Left => Keep - | Right => Drop - | Both => Keep - end. - -(* Elements that appear in the right list (or both) are kept, those which only appear in the left list are dropped *) -Definition right_usage (s : side) : usage := - match s with - | Left => Drop - | Right => Keep - | Both => Keep - end. - -Definition left_usages (ss : splitting) : list usage := List.map left_usage ss. - -Definition right_usages (ss : splitting) : list usage := List.map right_usage ss. - -(* Takes a splitting list (Left|Right|Both) and returns - a Keep|Drop usage list for the left list, and a Keep|Drop usage list for the right list. *) -Definition usages (ss : splitting) : list usage * list usage := - (left_usages ss, right_usages ss). - -(* Example: *) -Goal usages [Left; Right; Left; Right; Both; Right] = - ([Keep; Drop; Keep; Drop; Keep; Drop ], - [Drop; Keep; Drop; Keep; Keep; Keep]). -auto. -Qed. - -Definition split {A : Type} (ss : splitting) (xs : list A) : list A * list A := - (select (left_usages ss) xs, select (right_usages ss) xs). - -(* ++ and left_usages are commutative *) -Lemma left_usages_app (ss ss' : splitting) : - left_usages (ss ++ ss') = left_usages ss ++ left_usages ss'. -Proof. unfold left_usages; apply map_app. Qed. - -(* ++ and right_usages are commutative *) -Lemma right_usages_app (ss ss' : splitting) : - right_usages (ss ++ ss') = right_usages ss ++ right_usages ss'. -Proof. unfold right_usages; apply map_app. Qed. - -(* left_usages preserves length *) -Lemma left_usages_length (ss : splitting) : - length (left_usages ss) = length ss. -Proof. unfold left_usages; apply map_length. Qed. - -(* right_usages preserves length *) -Lemma right_usages_length (ss : splitting) : - length (right_usages ss) = length ss. -Proof. unfold right_usages; apply map_length. Qed. - -(* right_usages gives a result which is correct for the "used" prop *) -Lemma used_splits_right {A : Type} {ss : splitting} {xs ys zs : list A} : - splits ss zs xs ys -> - used (right_usages ss) ys zs. -Proof. intros; induction H; simpl; auto. Qed. - -#[export] Hint Resolve used_splits_right. - -(* Transforms all the "Right" elements into "Both" elements *) -Lemma splits_keep_rights_left_usages {A : Type} {ss : list side} {g g1 g2 : list A} : - splits ss g g1 g2 -> - splits (keep_rights (left_usages ss)) g g1 g. -Proof. - intros; induction H; simpl; eauto. -Qed. - -Definition example_splits_keep_rights_left_usages := - splits_keep_rights_left_usages - (ltac:(repeat constructor) - : splits [Left; Right; Left; Right; Both; Right] - [0 ; 1 ; 2 ; 3 ; 4 ; 5 ] - [0 ; 2 ; 4 ] - [ 1 ; 3 ; 4 ; 5 ]) - : splits [Both; Right; Both; Right; Both; Right] - [0 ; 1 ; 2 ; 3 ; 4 ; 5 ] - [0 ; 2 ; 4 ] - [0 ; 1 ; 2 ; 3 ; 4 ; 5 ]. - -(* converts splits ss g g1 g2 to used _ g2 g2 *) -Lemma used_filter_keeps_right_usages {A : Type} {ss : list side} {g g1 g2 : list A} : - splits ss g g1 g2 -> - used (filter_keeps (right_usages ss)) g2 g2. -Proof. - intros; induction H; simpl; auto. -Qed. - -(* Proof of equivalence between the "select" representation and the "used" representation, - with the precondition that the two arguments to "select" have the same length. *) -Lemma select_iff_used : - forall {A : Type} (us : list usage) (xs ys : list A), - (length us = length xs /\ select us xs = ys) <-> used us ys xs. -Proof. - intros A us; induction us; intros xs ys; - split; intros H; try (destruct H as [Hlen H]; subst). - - destruct xs; inversion Hlen; simpl; auto. - - inversion H; subst; auto. - - destruct xs; inversion Hlen; simpl; - destruct a; constructor; apply IHus; auto. - - inversion H; subst; simpl; - eenough (length us = length ys0 /\ select us ys0 = _) - by (destruct H0 as [Hlen H0]; rewrite Hlen; rewrite H0; auto); - apply IHus; assumption. -Qed. - -Hint Rewrite @select_iff_used. - -(* (select us xs) returns a list that is valid for (used us _ xs) *) -Lemma used_select : - forall {A : Type} (us : list usage) (xs : list A), - length us = length xs -> - used us (select us xs) xs. -Proof. intros; rewrite <- select_iff_used; auto. Qed. - -#[export] Hint Resolve used_select. - -Lemma select_iff_splits : - forall {A : Type} (ss : splitting) (zs xs ys : list A), - (List.length ss = List.length zs /\ - select (left_usages ss) zs = xs /\ - select (right_usages ss) zs = ys) <-> splits ss zs xs ys. -Proof. - intros A ss; induction ss; intros zs xs ys; split; intros H; try (destruct H as [Hlen [Hl Hr]]). - - subst; simpl; destruct zs; inversion Hlen; auto. - - inversion H; subst; auto. - - destruct zs; inversion Hlen; destruct a; subst; constructor; apply IHss; auto. - - inversion H; subst; - eenough (length ss = length zs0 /\ - select (left_usages ss) zs0 = _ /\ - select (right_usages ss) zs0 = _) - by (simpl; destruct H0 as [Hlen [Hl Hr]]; rewrite Hlen, Hl, Hr; auto); - apply IHss; auto. -Qed. - -Hint Rewrite @select_iff_splits. - -(* Proof that (split ss zs L R) allows "L = the left selection" and "R = right selection" *) -Lemma splits_select : - forall {A : Type} (ss : splitting) (zs : list A), - length ss = length zs -> - splits ss zs (select (left_usages ss) zs) (select (right_usages ss) zs). -Proof. intros. rewrite <- select_iff_splits. auto. Qed. - -#[export] Hint Resolve splits_select. - -(* The next few definitions and lemma show the associativity of splits: - (splits outer Δ₁ Γ Δ₂) /\ (splits inner Γ Γ₁ Γ₂) - implies - ∃ Δ', (splits assoc1 Δ₁ Γ₁ Δ') /\ (splits assoc2 Δ' Γ₂ Δ₂) - - The associativity happens at the result leaves (the final splitted lists): - ((Γ₁ Γ₂) Δ₂) - (Γ₁ (Γ₂ Δ₂)) - - The names come from the main use case: we are compiling an expression, say f x. - Γ is the environment of the expression, which is split into two parts Γ₁ (stuff - used in f) and Γ₂ (stuff used in x.) then Δ₁ is the input Michelson stack, and - Δ₂ is the output Michelson stack. the outer splitting is part of the setup of - the compiler -- everything in the input Michelson stack is either used in the - current expression or is left over in Δ₂ (or both.) - *) - -Fixpoint assoc_splitting1 (outer inner : splitting) : splitting := - match (outer, inner) with - | (Left :: outer, Left :: inner) => Left :: assoc_splitting1 outer inner - | (Left :: outer, Right :: inner) => Right :: assoc_splitting1 outer inner - | (Left :: outer, Both :: inner) => Both :: assoc_splitting1 outer inner - | (Right :: outer, inner) => Right :: assoc_splitting1 outer inner - | (Both :: outer, Left :: inner) => Both :: assoc_splitting1 outer inner - | (Both :: outer, Right :: inner) => Right :: assoc_splitting1 outer inner - | (Both :: outer, Both :: inner) => Both :: assoc_splitting1 outer inner - | ([], inner) => [] - | (_, []) => [] - end. - -Fixpoint assoc_splitting2 (outer inner : splitting) : splitting := - match (outer, inner) with - | (Left :: outer, Left :: inner) => assoc_splitting2 outer inner - | (Left :: outer, Right :: inner) => Left :: assoc_splitting2 outer inner - | (Left :: outer, Both :: inner) => Left :: assoc_splitting2 outer inner - | (Right :: outer, inner) => Right :: assoc_splitting2 outer inner - | (Both :: outer, Left :: inner) => Right :: assoc_splitting2 outer inner - | (Both :: outer, Right :: inner) => Both :: assoc_splitting2 outer inner - | (Both :: outer, Both :: inner) => Both :: assoc_splitting2 outer inner - | ([], inner) => [] - | (_, []) => [] - end. - -Definition assoc_splitting (outer inner : splitting) : splitting * splitting := - (assoc_splitting1 outer inner, assoc_splitting2 outer inner). - -Lemma assoc_splits : - forall {outer inner : splitting}, - forall {A : Type} {d1 g d2 g1 g2 : list A}, - splits outer d1 g d2 -> - splits inner g g1 g2 -> - exists d', - splits (fst (assoc_splitting outer inner)) d1 g1 d' /\ - splits (snd (assoc_splitting outer inner)) d' g2 d2. -Proof. - intros outer; induction outer; intros inner A g g1 g2 d1 d2 Houter Hinner; - inversion Houter; subst; inversion Hinner; subst; - eauto; - try (specialize (IHouter _ _ _ _ _ _ _ H4 H5)); - try (specialize (IHouter _ _ _ _ _ _ _ H4 Hinner)); - destruct IHouter as [x' [Houter' Hinner']]; simpl; eauto. -Qed. - -Definition flip_side (s : side) : side := - match s with - | Left => Right - | Right => Left - | Both => Both - end. - -(* flip the side of all elements of a splitting *) -Definition flip_splitting (ss : splitting) : splitting := - List.map flip_side ss. - -(* in (splits ss values left_elements right_elements), we can flip ss and swap left_elements with right_elements *) -Lemma flip_splits : - forall {A : Type} {ss : splitting}, - forall {g g1 g2 : list A}, - splits ss g g1 g2 -> - splits (flip_splitting ss) g g2 g1. -Proof. intros; induction H; simpl; auto. Qed. - -(* the result of (split (flip_splitting ss) zs …) can be obtained by doing selections on the original - ss, without involving flip_splitting. *) -Lemma splits_flip_select : - forall {A : Type} (ss : splitting) (zs : list A), - length ss = length zs -> - splits (flip_splitting ss) zs (select (right_usages ss) zs) (select (left_usages ss) zs). -Proof. - intros; apply flip_splits, splits_select; assumption. -Qed. - -#[export] Hint Resolve splits_flip_select. - -(* currently only used by uncertified OCaml code at - src/passes/13-scoping/scoping.ml *) -Fixpoint union (ls rs : list usage) : splitting * list usage := - match (ls, rs) with - | ([], []) => - ([], []) - | (l :: ls, r :: rs) => - let (ss, us) := union ls rs in - match (l, r) with - | (Drop, Drop) => (ss, Drop :: us) - | (Drop, Keep) => (Right :: ss, Keep :: us) - | (Keep, Drop) => (Left :: ss, Keep :: us) - | (Keep, Keep) => (Both :: ss, Keep :: us) - end - (* ill-typed cases: *) - (* | ([], r :: rs) => *) - (* let (ss, us) := coproduct [] rs in *) - (* match r with *) - (* | Drop => (Left :: ss, Keep :: us) *) - (* | Keep => (Both :: ss, Keep :: us) *) - (* end *) - (* | (l :: ls, []) => *) - (* let (ss, us) := coproduct ls [] in *) - (* match l with *) - (* | Drop => (Right :: ss, Keep :: us) *) - (* | Keep => (Both :: ss, Keep :: us) *) - (* end *) - | _ => ([], []) - end. - -(* Example: *) -Goal union [Keep; Drop; Drop; Keep; Keep; Drop ] - [Drop; Keep; Drop; Keep; Keep; Keep ] = - ([Left; Right; Both; Both; Right], - [Keep; Keep; Drop; Keep; Keep; Keep]). -auto. -Qed. diff --git a/src/coq/compiler.v b/src/coq/compiler.v deleted file mode 100644 index 2b2837441d..0000000000 --- a/src/coq/compiler.v +++ /dev/null @@ -1,1863 +0,0 @@ -Local Set Warnings "-implicit-core-hint-db". -Set Implicit Arguments. -From Coq Require Import String List Arith ZArith Program.Tactics micromega.Lia micromega.Zify. -From Coq Require Extraction. -Import ListNotations. -Open Scope string_scope. -Unset Lia Cache. - -From ligo_coq Require Import ope. - -(* http://poleiro.info/posts/2018-10-15-checking-for-constructors.html *) -Ltac head t := - (* slightly modified, we will evaluate to get a head *) - let t := eval hnf in t in - match t with - | ?t' _ => head t' - | _ => t - end. - -Ltac head_constructor t := - let t' := head t in is_constructor t'. - -Ltac invert H := inversion H; subst; clear H. - -Ltac invert_pred p := - match goal with - | [H : p |- _] => invert H - | [H : p _ |- _] => invert H - | [H : p _ _ |- _] => invert H - | [H : p _ _ _ |- _] => invert H - | [H : p _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ _ _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ |- _] => invert H - | [H : p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ |- _] => invert H - end. - -Definition done (T : Type) : Type := T. - -Ltac mark_done H := - let A := type of H in - change (done A) in H. - -Ltac clear_done := - repeat - match goal with - | [H : done ?A |- _] => - change A in H - end. - -Axiom bytes : Set. -Extract Inlined Constant bytes => "bytes". - -(* I am sorry this is one big section. It seemed like the easiest, - stupidest way to deal with the Context assumptions below. If you - find a way to break this up into multiple files, please do it. - - Maybe most of the Context should instead be Axioms with custom - Extraction? *) -Section compiler. - -Local Open Scope list. - -Context {meta : Set}. (* metadata for expressions (source location, etc) *) -Context {null : meta}. (* null metadata *) -Context {base_type : Set}. (* arbitrary base types (probably Micheline) *) - -(* Types: essentially Michelson's types, shared by source and target - stages here *) -Inductive ty : Set := -| T_base : meta -> base_type -> ty - -| T_unit : meta -> ty -| T_pair : meta -> option string -> option string -> ty -> ty -> ty - -| T_or : meta -> option string -> option string -> ty -> ty -> ty - -| T_func : meta -> ty -> ty -> ty -| T_lambda : meta -> ty -> ty -> ty - -| T_option : meta -> ty -> ty -| T_list : meta -> ty -> ty -| T_set : meta -> ty -> ty -| T_map : meta -> ty -> ty -> ty -| T_big_map : meta -> ty -> ty -> ty -| T_ticket : meta -> ty -> ty -| T_contract : meta -> ty -> ty -(* TODO delete the types we don't need *) -| T_bool : meta -> ty -| T_int : meta -> ty -| T_nat : meta -> ty -| T_mutez : meta -> ty -| T_string : meta -> ty -| T_bytes : meta -> ty -(* these only exist for CREATE_CONTRACT *) -| T_address : meta -> ty -| T_key_hash : meta -> ty -| T_operation : meta -> ty -. - -Context {with_var_names : list bool -> list ty -> meta -> meta}. -Context {lit micheline : Set}. -Context {lit_code : meta -> lit -> list micheline}. -Context {global_constant : meta -> string -> list micheline}. - - -(* Source language: de Bruijn LIGO expressions. For comments about - specific constructors, see the typing derivations [expr_typed] - below. - - The expressions are currently given as three mutual inductive - types: [expr] for expressions, [binds] for binding forms in - expressions (lambda bodies, match cases, etc,) and [args] for - tuples of expressions. - - [args] is isomorphic to [list expr], but is defined mutually in - order to avoid nested induction. Compare this to the different - choice adopted for Michelson below, where [prog] _is_ just [list - instr], and so nested induction is required to define - [strengthen_instr]. *) -Inductive expr : Set := -| E_var : meta -> nat -> expr -| E_let_in : meta -> expr -> binds -> expr - -| E_tuple : meta -> args -> expr -| E_let_tuple : meta -> expr -> binds -> expr -| E_proj : meta -> expr -> nat -> nat -> expr -| E_update : meta -> args -> nat -> nat -> expr - -| E_app : meta -> args -> expr -| E_lam : meta -> binds -> ty -> expr -| E_rec : meta -> binds -> ty -> expr - -| E_literal : meta -> lit -> expr - -| E_pair : meta -> args -> expr -| E_car : meta -> expr -> expr -| E_cdr : meta -> expr -> expr - -| E_unit : meta -> expr - -| E_left : meta -> ty -> expr -> expr -| E_right : meta -> ty -> expr -> expr - -| E_if_left : meta -> expr -> binds -> binds -> expr -| E_if_bool : meta -> expr -> expr -> expr -> expr -| E_if_none : meta -> expr -> expr -> binds -> expr -| E_if_cons : meta -> expr -> binds -> expr -> expr - -| E_iter : meta -> binds -> expr -> expr -| E_map : meta -> binds -> expr -> expr -| E_loop_left : meta -> binds -> ty -> expr -> expr -| E_fold : meta -> expr -> expr -> binds -> expr -| E_fold_right : meta -> ty -> expr -> expr -> binds -> expr - -(* TODO add typing rules for these ...maybe ;) *) -| E_deref : meta -> nat -> expr -| E_let_mut_in : meta -> expr -> binds -> expr -| E_assign : meta -> nat -> expr -> expr -| E_for : meta -> args -> binds -> expr -| E_for_each : meta -> expr -> binds -> expr -| E_while : meta -> expr -> expr -> expr - -| E_failwith : meta -> expr -> expr - -| E_raw_michelson : meta -> ty -> ty -> list micheline -> expr -| E_inline_michelson : meta -> list micheline -> args -> expr -| E_global_constant : meta -> ty -> string -> args -> expr -| E_create_contract : meta -> ty -> ty -> binds -> args -> expr - -with binds : Set := -| Binds : meta -> list ty -> expr -> binds - -with args : Set := -| Args_nil : meta -> args -| Args_cons : meta -> expr -> args -> args -. - -Scheme expr_ind' := Induction for expr Sort Prop -with binds_ind' := Induction for binds Sort Prop -with args_ind' := Induction for args Sort Prop. -Combined Scheme expr_mutind from expr_ind', binds_ind', args_ind'. - -Fixpoint args_length (e : args) : nat := - match e with - | Args_nil _ => O - | Args_cons _ _ e => S (args_length e) - end. - -Definition binds_length (e : binds) : nat := - match e with - | Binds _ ts _ => length ts - end. - -Local Generalizable Variable l n. - -Inductive tuple : list ty -> ty -> Prop := -| Tuple_nil : - `{tuple [] (T_unit l)} -| Tuple_one {a} : - tuple [a] a -| Tuple_cons {a1 a2 az a2z'} : - `{tuple (a2 :: az) a2z' -> - tuple (a1 :: a2 :: az) (T_pair l n1 n2 a1 a2z')} -. - -Inductive iter_class : ty -> ty -> Prop := -| Iter_list {a} : - `{iter_class a (T_list l a)} -| Iter_set {a} : - `{iter_class a (T_set l a)} -| Iter_map {k v} : - `{iter_class (T_pair l1 n1 n2 k v) (T_map l2 k v)} -. - -Inductive map_class : ty -> ty -> ty -> ty -> Prop := -| Map_list {a b} : - `{map_class a b (T_list l1 a) (T_list l2 b)} -| Map_map {k v r} : - `{map_class (T_pair l1 n1 n2 k v) r (T_map l2 k v) (T_map l3 k r)} -. - -Hint Constructors iter_class : michelson. -Hint Constructors map_class : michelson. - -Generalizable Variable g. (* TODO *) - -Inductive expr_typed : list ty -> expr -> ty -> Prop := -| E_var_typed {a} : - `{List.nth_error g n = Some a -> - expr_typed g (E_var l n) a} -| E_let_in_typed {e1 e2 a b} : - `{expr_typed g e1 a -> - binds_typed g e2 [a] b -> - expr_typed g (E_let_in l e1 e2) b} -| E_tuple_typed {args az t} : - `{tuple az t -> - args_typed g args az -> - expr_typed g (E_tuple l1 args) t} -| E_let_tuple_typed {az azt c e1 e2} : - `{tuple az azt -> - expr_typed g e1 azt -> - binds_typed g e2 az c -> - expr_typed g (E_let_tuple l3 e1 e2) c} -| E_proj_typed {az azt a e i n} : - `{tuple az azt -> - List.nth_error az i = Some a -> - List.length az = n -> - expr_typed g e azt -> - expr_typed g (E_proj l1 e i n) a} -| E_update_typed {a az azt args i n} : - `{tuple az azt -> - List.nth_error az i = Some a -> - List.length az = n -> - args_typed g args [azt; a] -> - expr_typed g (E_update l1 args i n) azt} -| E_app_typed {args a b} : - `{args_typed g args [T_func l1 a b; a] -> - expr_typed g (E_app l2 args) b} -| E_lam_typed {a b e} : - `{binds_typed g e [a] b -> - expr_typed g (E_lam l1 e b) (T_func l2 a b)} -| E_literal_typed {lit a} : - `{(* TODO postulate some typing *) - expr_typed g (E_literal l lit) a} -| E_pair_typed {args a b} : - `{args_typed g args [a; b] -> - expr_typed g (E_pair l1 args) (T_pair l2 n1 n2 a b)} -| E_car_typed {e a b} : - `{expr_typed g e (T_pair l1 n1 n2 a b) -> - expr_typed g (E_car l2 e) a} -| E_cdr_typed {e a b} : - `{expr_typed g e (T_pair l1 n1 n2 a b) -> - expr_typed g (E_cdr l2 e) b} -| E_unit_typed : - `{expr_typed g (E_unit l1) (T_unit l2)} -| E_left_typed {e a b} : - `{expr_typed g e a -> - expr_typed g (E_left l1 b e) (T_or l2 n1 n2 a b)} -| E_right_typed {e a b} : - `{expr_typed g e b -> - expr_typed g (E_right l1 a e) (T_or l2 n1 n2 a b)} -| E_if_left_typed {e1 e2 e3 a b c} : - `{expr_typed g e1 (T_or l1 n1 n2 a b) -> - binds_typed g e2 [a] c -> - binds_typed g e3 [b] c -> - expr_typed g (E_if_left l2 e1 e2 e3) c} -| E_if_bool_typed {e1 e2 e3 c} : - `{expr_typed g e1 (T_bool l1) -> - expr_typed g e2 c -> - expr_typed g e3 c -> - expr_typed g (E_if_bool l2 e1 e2 e3) c} -| E_if_none_typed {e1 e2 e3 a c} : - `{expr_typed g e1 (T_option l1 a) -> - expr_typed g e2 c -> - binds_typed g e3 [a] c -> - expr_typed g (E_if_none l2 e1 e2 e3) c} -| E_if_cons_typed {e1 b2 e3 a c} : - `{expr_typed g e1 (T_list l1 a) -> - binds_typed g b2 [a; T_list l2 a] c -> - expr_typed g e3 c -> - expr_typed g (E_if_cons l3 e1 b2 e3) c} -| E_iter_typed {elem coll e1 e2} : - `{iter_class elem coll -> - binds_typed g e1 [elem] (T_unit l1) -> - expr_typed g e2 coll -> - expr_typed g (E_iter l2 e1 e2) (T_unit l3)} -| E_map_typed {elem elem' coll coll' e1 e2} : - `{map_class elem elem' coll coll' -> - binds_typed g e1 [elem] elem' -> - expr_typed g e2 coll -> - expr_typed g (E_map l e1 e2) coll'} -| E_loop_left_typed {a b e1 e2} : - `{binds_typed g e1 [a] (T_or l1 n1 n2 a b) -> - expr_typed g e2 a -> - expr_typed g (E_loop_left l2 e1 b e2) b} -| E_fold_typed {elem coll ret e1 e2 e3} : - `{iter_class elem coll -> - expr_typed g e1 ret -> - expr_typed g e2 coll -> - binds_typed g e3 [T_pair l1 n1 n2 ret elem] ret -> - expr_typed g (E_fold l2 e1 e2 e3) ret} -| E_fold_right_typed {elem coll ret e1 e2 e3} : - `{iter_class elem coll -> - expr_typed g e1 ret -> - expr_typed g e2 coll -> - binds_typed g e3 [T_pair l1 n1 n2 elem ret] ret -> - expr_typed g (E_fold_right l2 elem e1 e2 e3) ret} -| E_failwith_typed {a b e} : - `{expr_typed g e a -> - expr_typed g (E_failwith l1 e) b} -(* E_raw_michelson emits a Michelson lambda directly. It is used for - [%Michelson ({| ... |} : a -> b)] in LIGO. Probably we should - delete it and migrate to E_inline_michelson. *) -| E_raw_michelson_typed {code a b} : - `{(* TODO should postulate some typing *) - expr_typed g (E_raw_michelson l1 a b code) (T_lambda l2 a b)} -(* E_inline_michelson inlines Michelson code directly, applied to some - given arguments. It is currently only used for the "predefined - constants" in predefined.ml, but could be exposed to users - someday. TODO we should probably have a [ty] in the syntax for the - return type [b], since it cannot be inferred? *) -| E_inline_michelson_typed {code args az b} : - `{args_typed g args az -> - (* TODO should postulate some typing *) - expr_typed g (E_inline_michelson l1 code args) b} -(* E_global_constant is for Tezos "global constants". It is very - similar to E_inline_michelson, but accepts the string hash of a - Tezos "global constant" in place of the Michelson code. *) -| E_global_constant_typed {az b hash args} : - `{args_typed g args az -> - (* TODO should postulate some typing *) - expr_typed g (E_global_constant l1 b hash args) b} -(* E_create_contract only exists here because it seemed easiest to put - it here. - - It is not easy to handle in an earlier pass using - E_inline_michelson, because that earlier pass would need access to - the later passes of the compiler, in order to compile, optimize, - and render the given contract into Micheline. - - A previous version of this Coq compiler had a more complicated - interaction with the predefineds which made it possible to handle - CREATE_CONTRACT using a predefined, but that was very confusing, - and didn't work well with the current choices here. *) -| E_create_contract_typed {p s script args} : - `{binds_typed [] script [T_pair l1 n1 n2 p s] (T_pair l2 n3 n4 (T_operation l3) s) -> - args_typed g args [T_option l4 (T_key_hash l5); T_mutez l6; s] -> - expr_typed g (E_create_contract l7 p s script args) (T_pair l8 n5 n6 (T_operation l9) (T_address l10))} -with binds_typed : list ty -> binds -> list ty -> ty -> Prop := -| Binds_typed {a e ts} : - `{expr_typed (ts ++ g) e a -> - binds_typed g (Binds l ts e) ts a} -with args_typed : list ty -> args -> list ty -> Prop := -| Args_nil_typed : - `{args_typed g (Args_nil l) []} -| Args_cons_typed {e args d a} : - `{expr_typed g e a -> - args_typed g args d -> - args_typed g (Args_cons l e args) (d ++ [a])} -. - -Hint Constructors expr_typed : ligo. -Hint Constructors binds_typed : ligo. -Hint Constructors args_typed : ligo. - - - -(************* - * Michelson * - *************) - -Reserved Notation "'prog'". - -Inductive instr : Set := -| I_RAW : meta -> nat -> list micheline -> instr - -| I_SEQ : meta -> prog -> instr -| I_DIP : meta -> prog -> instr -| I_DIG : meta -> nat -> instr -| I_DUG : meta -> nat -> instr -| I_DUP : meta -> nat -> instr -| I_DROP : meta -> nat -> instr -| I_SWAP : meta -> instr - -| I_UNIT : meta -> instr -| I_TRUE : meta -> instr (* fictional version of PUSH bool True, for impl of E_while... *) - -| I_LEFT : meta -> ty -> instr -| I_RIGHT : meta -> ty -> instr -| I_IF_LEFT : meta -> prog -> prog -> instr - -| I_PAIR : meta -> nat -> instr -| I_UNPAIR : meta -> nat -> instr -| I_GET : meta -> nat -> instr -| I_UPDATE : meta -> nat -> instr -| I_CAR : meta -> instr -| I_CDR : meta -> instr - -| I_IF : meta -> prog -> prog -> instr - -| I_IF_NONE : meta -> prog -> prog -> instr - -| I_NIL : meta -> ty -> instr -| I_CONS : meta -> instr -| I_IF_CONS : meta -> prog -> prog -> instr - -| I_FUNC : meta -> list ty -> ty -> ty -> list bool -> list bool -> prog -> instr (* VERY FICTION *) -| I_REC_FUNC : meta -> list ty -> ty -> ty -> list bool -> list bool -> prog -> instr (* VERY FICTION *) -| I_LAMBDA : meta -> ty -> ty -> prog -> instr -| I_EXEC : meta -> instr (* func or lambda *) -| I_APPLY_LAMBDA : meta -> ty -> instr (* FICTION (APPLY but with a type arg) *) - -| I_LOOP : meta -> prog -> instr -| I_LOOP_LEFT : meta -> prog -> instr - -| I_FAILWITH : meta -> instr - -| I_ITER : meta -> prog -> instr -| I_MAP : meta -> prog -> instr - -(* convenient fictional instruction for implementing E_for (arithmetic - progression loops) without exposing arithmetic here right now... *) -| I_FOR : meta -> prog -> instr - -| I_CREATE_CONTRACT : meta -> ty -> ty -> prog -> instr -where -"'prog'" := (list instr). - -Inductive packable : ty -> Prop := -| Packable_unit : `{packable (T_unit l)} -| Packable_pair {a b} : - `{packable a -> packable b -> - packable (T_pair l n1 n2 a b)} -| Packable_or {a b} : - `{packable a -> packable b -> - packable (T_or l n1 n2 a b)} -(* T_func is not packable, T_lambda is: *) -| Packable_lambda {a b} : - `{packable (T_lambda l a b)} -| Packable_int : - `{packable (T_int l)} -| Packable_nat : - `{packable (T_nat l)} -| Packable_mutez : - `{packable (T_mutez l)} -| Packable_bool : - `{packable (T_bool l)} -| Packable_bytes : - `{packable (T_bytes l)} -(* TODO *) -. - -Hint Constructors packable : michelson. - -Inductive comparable : ty -> Prop := -| Comparable_int : `{comparable (T_int l)} -| Comparable_nat : `{comparable (T_nat l)} -| Comparable_mutez : `{comparable (T_mutez l)} -(* TODO *) -. - -Hint Constructors comparable : michelson. - -(* Characterization of Michelson "comb types", which must have at - least 2 "fields" *) -Inductive comb_ty : ty -> list ty -> Prop := -| Comb_two {a b} : - `{comb_ty (T_pair l n1 n2 a b) [a; b]} -| Comb_cons {c ts t} : - `{comb_ty c ts -> - comb_ty (T_pair l n1 n2 t c) (t :: ts)} -. - -Hint Constructors comb_ty : michelson. - -(* Characterization of comb [GET k] typing *) -Inductive comb_get_ty : ty -> nat -> ty -> Prop := -| Comb_get_zero' {a} : - comb_get_ty a O a -| Comb_get_one' {x y} : - `{comb_get_ty (T_pair l1 n1 n2 x y) 1 x} -| Comb_get_plustwo {n x y z} : - `{comb_get_ty y n z -> - comb_get_ty (T_pair l1 n1 n2 x y) (S (S n)) z} -. - -(* Characterization of comb [UPDATE k] typing *) -Inductive comb_update_ty : ty -> ty -> nat -> ty -> Prop := -| Comb_update_zero {t x}: - comb_update_ty t x O x -| Comb_update_one {a1 a2 b} : - `{comb_update_ty (T_pair l1 n1 n2 a1 b) a2 1 (T_pair l2 n3 n4 a2 b)} -| Comb_update_plustwo {n a b1 b2 c} : - `{comb_update_ty b1 c n b2 -> - comb_update_ty (T_pair l1 n1 n2 a b1) c (S (S n)) (T_pair l2 n3 n4 a b2)} -. - -Definition mutez_bound : Z.t := Z.pow 2 63. - -Inductive instr_typed : instr -> list ty -> list ty -> Prop := -(* I_RAW allows embedding raw Michelson. It's like an instruction [RAW n { code }] which means to apply the code *) -| Raw_typed {p s1 s2 b} : - `{(* raw_typed p s1 b -> *) - length s1 = n -> - instr_typed (I_RAW l n p) (s1 ++ s2) (b :: s2)} -(* Structural stuff *) -| Seq_typed {p s1 s2} : - `{prog_typed p s1 s2 -> - instr_typed (I_SEQ l p) s1 s2} -| Dip_typed {p a s1 s2} : - `{prog_typed p s1 s2 -> - instr_typed (I_DIP l p) (a :: s1) (a :: s2)} -| Dig_typed {n a s1 s2} : - `{length s1 = n -> - instr_typed (I_DIG l n) (s1 ++ a :: s2) (a :: s1 ++ s2)} -| Dug_typed {n a s1 s2} : - `{length s1 = n -> - instr_typed (I_DUG l n) (a :: s1 ++ s2) (s1 ++ a :: s2)} -| Dup_typed {n s t} : - `{List.nth_error s n = Some t -> - instr_typed (I_DUP l (S n)) s (t :: s)} -| Drop_typed {s1 s2} : - `{length s1 = n -> - instr_typed (I_DROP l n) (s1 ++ s2) s2} -| Swap_typed {a b s} : - `{instr_typed (I_SWAP l) (a :: b :: s) (b :: a :: s)} - -(* Unit *) -| Unit_typed {s} : - `{instr_typed (I_UNIT l1) s (T_unit l2 :: s)} -| True_typed {s} : - `{instr_typed (I_TRUE l1) s (T_bool l2 :: s)} - -(* Or *) -| Left_typed {a b s} : - `{instr_typed (I_LEFT l1 b) (a :: s) (T_or l2 n1 n2 a b :: s)} -| Right_typed {a b s} : - `{instr_typed (I_RIGHT l1 a) (b :: s) (T_or l2 n1 n2 a b :: s)} -| If_left_typed {bt bf a b s1 s2} : - `{prog_typed bt (a :: s1) s2 -> - prog_typed bf (b :: s1) s2 -> - instr_typed (I_IF_LEFT l1 bt bf) (T_or l2 n1 n2 a b :: s1) s2} - -(* Pairs *) -| Pair_typed {n t ts s} : - `{comb_ty t ts -> - length ts = n -> - instr_typed (I_PAIR l1 n) (ts ++ s) (t :: s)} -| Unpair_typed {n t ts s} : - `{comb_ty t ts -> - length ts = n -> - instr_typed (I_UNPAIR l1 n) (t :: s) (ts ++ s)} - -| Get_typed {t n x s} : - `{comb_get_ty t n x -> - instr_typed (I_GET l1 n) (t :: s) (x :: s)} -| Update_typed {t x n t' s} : - `{comb_update_ty t x n t' -> - instr_typed (I_UPDATE l1 n) (x :: t :: s) (t' :: s)} - -| Car_typed {a b s} : - `{instr_typed (I_CAR l1) (T_pair l2 n1 n2 a b :: s) (a :: s)} -| Cdr_typed {a b s} : - `{instr_typed (I_CDR l1) (T_pair l2 n1 n2 a b :: s) (b :: s)} - -(* Bools *) -| If_typed {bt bf s1 s2} : - `{prog_typed bt s1 s2 -> - prog_typed bf s1 s2 -> - instr_typed (I_IF l1 bt bf) (T_bool l2 :: s1) s2} - -(* Option *) -| If_none_typed {bt bf a s1 s2} : - `{prog_typed bt s1 s2 -> - prog_typed bf (a :: s1) s2 -> - instr_typed (I_IF_NONE l1 bt bf) (T_option l2 a :: s1) s2} - -(* List *) -| Nil_instr_typed {a s1} : - `{instr_typed (I_NIL l1 a) s1 (T_list l2 a :: s1)} -| Cons_instr_typed {a s} : - `{instr_typed (I_CONS l1) (a :: T_list l1 a :: s) (T_list l2 a :: s)} -| If_cons_typed {bt bf a s1 s2} : - `{prog_typed bt (a :: T_list l1 a :: s1) s2 -> - prog_typed bf s1 s2 -> - instr_typed (I_IF_CONS l2 bt bf) (T_list l3 a :: s1) s2} - -(* Functions *) -| Func_typed {a b r1 r2 code s d1 d2} : - `{prog_typed code (a :: d1) (b :: d2) -> - ope_valid r1 (length s) -> - select r1 s = d1 -> - ope_valid r2 (length d1) -> - select r2 d1 = d2 -> - instr_typed (I_FUNC l1 d1 a b r1 r2 code) s (T_func l2 a b :: s)} -| Recfunc_typed {a b r1 r2 code s d1 d2} : - `{prog_typed code (a :: (T_lambda l1 a b) :: d1) (b :: d2) -> - ope_valid r1 (length s) -> - select r1 s = d1 -> - ope_valid r2 (length d1) -> - select r2 d1 = d2 -> - instr_typed (I_REC_FUNC l1 d1 a b r1 r2 code) s (T_func l2 a b :: s)} -| Exec_func_typed {a b s} : - `{instr_typed (I_EXEC l1) (a :: T_func l2 a b :: s) (b :: s)} - -(* Lambdas *) -| Lambda_typed {a b code s} : - `{prog_typed code [a] [b] -> - instr_typed (I_LAMBDA l1 a b code) s (T_lambda l2 a b :: s)} -| Exec_lambda_typed {a b s} : - `{instr_typed (I_EXEC l1) (a :: T_lambda l2 a b :: s) (b :: s)} -| Apply_lambda_typed {a b c s} : - `{packable a -> - instr_typed (I_APPLY_LAMBDA l1 a) (a :: T_lambda l2 (T_pair l3 n1 n2 a b) c :: s) (T_lambda l4 b c :: s)} - -(* Loops *) -| Loop_typed {body s} : - `{prog_typed body s (T_bool l1 :: s) -> - instr_typed (I_LOOP l2 body) (T_bool l3 :: s) s} -| Loop_left_typed {a b body s} : - `{prog_typed body (a :: s) (T_or l1 n1 n2 a b :: s) -> - instr_typed (I_LOOP_LEFT l2 body) (T_or l3 n1 n2 a b :: s) (b :: s)} -| Iter_typed_list {body a s} : - `{prog_typed body (a :: s) s -> - instr_typed (I_ITER l1 body) (T_list l2 a :: s) s} -| Map_typed_list {body a b s} : - `{prog_typed body (a :: s) (b :: s) -> - instr_typed (I_MAP l1 body) (T_list l2 a :: s) (T_list l3 b :: s)} -(* FICTION *) -| For_typed {body s} : - `{prog_typed body (T_int l1 :: s) s -> - instr_typed (I_FOR l2 body) (T_int l3 :: T_int l4 :: T_int l5 :: s) s} - -(* Failure *) -| Failwith_typed {a s1 s2} : - `{instr_typed (I_FAILWITH l) (a :: s1) s2} - -(* CREATE_CONTRACT *) -| Create_contract_typed_list {p' s' code s1} : - `{prog_typed code [T_pair l1 n1 n2 p' s'] [T_pair l2 n3 n4 (T_list l3 (T_operation l4)) s'] -> - instr_typed (I_CREATE_CONTRACT l5 p' s' code) (T_option l6 (T_key_hash l7) :: T_mutez l8 :: s' :: s1) (T_operation l9 :: T_address l10 :: s1)} - -with prog_typed : prog -> list ty -> list ty -> Prop := -| Nil_typed {s} : - prog_typed [] (* P_nil *) s s -| Cons_typed {i p s1 s2 s3} : - instr_typed i s1 s2 -> - prog_typed p s2 s3 -> - prog_typed (i :: p) (* (P_cons i p) *) s1 s3 -. - -Hint Constructors instr_typed : michelson. -Hint Constructors prog_typed : michelson. - -Scheme instr_typed_ind' := Induction for instr_typed Sort Prop -with prog_typed_ind' := Induction for prog_typed Sort Prop. - -Combined Scheme instr_typed_mutind from - instr_typed_ind', prog_typed_ind'. - -Lemma dig_0_typed {l x s1} : instr_typed (I_DIG l 0) (x :: s1) (x :: s1). -Proof. - change (instr_typed (I_DIG l 0) ([] ++ x :: s1) (x :: [] ++ s1)); - eauto with michelson. -Defined. - -Lemma drop_1_typed {l x s1} : instr_typed (I_DROP l 1) (x :: s1) s1. -Proof. - change (instr_typed (I_DROP l 1) ([x] ++ s1) s1); - eauto with michelson. -Defined. - -Lemma pair_2_typed {x y s1} : `{instr_typed (I_PAIR l1 2) (x :: y :: s1) (T_pair l2 n1 n2 x y :: s1)}. -Proof. - intros; - change (instr_typed (I_PAIR l1 2) ([x; y] ++ s1) (T_pair l2 n1 n2 x y :: s1)); - eauto with michelson. -Defined. - -Hint Resolve dig_0_typed : michelson. -Hint Resolve drop_1_typed : michelson. -Hint Resolve pair_2_typed : michelson. - -Lemma prog_typed_app {p1 p2 s1 s2 s3} : - prog_typed p1 s1 s2 -> - prog_typed p2 s2 s3 -> - prog_typed (p1 ++ p2) s1 s3. -Proof. - intros H; - revert p2 s3; - induction H; - intros; - simpl; eauto with michelson. -Qed. - -Hint Resolve prog_typed_app : michelson. - -Notation stack_ty := (list ty). - -(************ - * Compiler * - ************) - -Fixpoint compile_ope_aux (n : nat) (us : ope) : prog := - match us with - | [] => [] - | false :: us => [I_DIG null n; - I_SEQ null (compile_ope_aux (S n) us); - I_DROP null 1] - | true :: us => compile_ope_aux (S n) us - end. - -Definition compile_ope (us : ope) : prog := - compile_ope_aux O us. - -Lemma compile_ope_aux_typed : - forall us n s1 s2, - length s1 = n -> - length us = length s2 -> - prog_typed (compile_ope_aux n us) (s1 ++ s2) (s1 ++ select us s2). -Proof. - intros us; induction us as [|u us]; intros n s1 s2 H1 H2; eauto; - destruct s2; try (simpl in H2; exfalso; lia); - simpl; eauto with michelson; - destruct u; simpl; eauto. - - enough (H : prog_typed (compile_ope_aux (S n) us) ((s1 ++ [t]) ++ s2) ((s1 ++ [t]) ++ select us s2)) - by (repeat rewrite <- app_assoc in H; exact H); - eapply IHus. - + rewrite app_length; simpl; lia. - + simpl in H2; lia. - - repeat econstructor; eauto. - + enough (H : prog_typed (compile_ope_aux (S n) us) (t :: s1 ++ s2) ([t] ++ s1 ++ select us s2)) by exact H; - change (prog_typed (compile_ope_aux (S n) us) ((t :: s1) ++ s2) ((t :: s1) ++ select us s2)); - eapply IHus; simpl; eauto. - + eauto. -Qed. - -Lemma compile_ope_typed : - forall {us g g'}, - length us = length g -> - select us g = g' -> - prog_typed (compile_ope us) g g'. -Proof. - intros; subst; apply compile_ope_aux_typed with (s1 := []); auto. -Qed. - -Lemma compile_ope_aux_weak_lemma1 : - forall us m n, compile_ope_aux n (us ++ repeat true m) = compile_ope_aux n us. -Proof. - intros us; induction us as [|u us]; intros m n; simpl. - - revert n; induction m; intros n. - + reflexivity. - + eapply IHm. - - destruct u; rewrite IHus; reflexivity. -Qed. - -Lemma compile_ope_weak_lemma1 : - forall us m, compile_ope (us ++ repeat true m) = compile_ope us. -Proof. - unfold compile_ope; intros; eapply compile_ope_aux_weak_lemma1. -Qed. - -Lemma compile_ope_weak_typed : - forall {us g g' d}, - length us = length g -> - select us g = g' -> - prog_typed (compile_ope us) (g ++ d) (g' ++ d). -Proof. - intros us g g' d H1 H2; - assert (H3 : prog_typed (compile_ope (us ++ repeat true (length d))) (g ++ d) (g' ++ d)) - by (eapply compile_ope_typed; - [ repeat rewrite app_length; rewrite repeat_length; eauto - | rewrite select_app; eauto; rewrite select_repeat_true; rewrite H2; reflexivity ]); - rewrite compile_ope_weak_lemma1 in H3; - exact H3. -Qed. - -Fixpoint comb (az : list ty) : ty := - match az with - | [] => T_unit null - | [a] => a - | a :: az => T_pair null None None a (comb az) - end. - -Definition PAIR (n : nat) : prog := - match n with - | 0 => [I_UNIT null] - | 1 => [] - | _ => [I_PAIR null n] - end. - -Definition UNPAIR (n : nat) : prog := - match n with - | 0 => [I_DROP null 1] - | 1 => [] - | _ => [I_UNPAIR null n] - end. - -(* hmm, reusing the names GET and UPDATE is confusing because these are different *) -Definition GET (i n : nat) : prog := - let i := if beq_nat (S i) n - then 2 * i - else 2 * i + 1 in - [I_GET null i]. - -Definition UPDATE (i n : nat) : prog := - let i := if beq_nat (S i) n - then 2 * i - else 2 * i + 1 in - [I_UPDATE null i]. - -Fixpoint compile_expr (r : ope) (env : list ty) (e : expr) {struct e} : prog := - match e with - | E_var l n => - [I_SEQ l [I_DUP null (S (embed r n))]] - | E_let_in l e1 e2 => - let e1' := compile_expr r env e1 in - let e2' := compile_binds r env e2 in - [I_SEQ l [I_SEQ null e1'; - I_SEQ null e2']] - | E_deref l n => [I_SEQ l [I_DUP null (S (embed r n))]] - | E_let_mut_in l e1 e2 => - let e1' := compile_expr r env e1 in - let e2' := compile_binds r env e2 in - [I_SEQ l [I_SEQ null e1'; - I_SEQ null e2']] - | E_assign l n e1 => - let e1' := compile_expr r env e1 in - [I_SEQ l [I_SEQ null e1'; - I_DUG null (embed r n); - I_DIG null (S (embed r n)); - I_DROP null 1; - I_UNIT null]] - | E_for l args body => - let args' := compile_args r env args in - let body' := compile_binds r env body in - [I_SEQ l [I_SEQ null args'; - I_FOR null [I_SEQ null body'; I_DROP null 1]; - I_UNIT null]] - | E_for_each l coll body => - let coll' := compile_expr r env coll in - let body' := compile_binds r env body in - (* TODO? this is a hack to make map iteration work -- Michelson - gives you the key and value in a pair, but LIGO things here - are set up to expect two stack elements, so insert an UNPAIR - in the map case: *) - if beq_nat 2 (binds_length body) - then - [I_SEQ l [I_SEQ null coll'; - I_ITER null [I_UNPAIR null 2; I_SEQ null body'; I_DROP null 1]; - I_UNIT null]] - else - [I_SEQ l [I_SEQ null coll'; - I_ITER null [I_SEQ null body'; I_DROP null 1]; - I_UNIT null]] - | E_while l cond body => - let cond' := compile_expr r env cond in - let body' := compile_expr (false :: r) env body in - [I_TRUE null; - I_LOOP l [I_SEQ null cond'; - I_DUP null 1; - I_IF null [I_SEQ null body'; I_DROP null 1] []]; - I_UNIT null] - | E_tuple l args => - [I_SEQ l [I_SEQ null (compile_args r env args); - I_SEQ null (PAIR (args_length args))]] - | E_let_tuple l e1 e2 => - [I_SEQ l [I_SEQ null (compile_expr r env e1); - I_SEQ null (UNPAIR (binds_length e2)); - I_SEQ null (compile_binds r env e2)]] - | E_proj l e i n => - [I_SEQ l [I_SEQ null (compile_expr r env e); - I_SEQ null (GET i n)]] - | E_update l args i n => - [I_SEQ l [I_SEQ null (compile_args r env args); - I_SEQ null (UPDATE i n)]] - | E_app l e => - [I_SEQ l [I_SEQ null (compile_args r env e); - I_SWAP null; - I_EXEC null]] - | E_lam l e b => - let a := match e with - | Binds _ [a] _ => a - | _ => T_unit null - end in - [I_SEQ l [I_FUNC null env a b (trim r (length env)) (repeat true (length env)) - (compile_binds (repeat true (length env)) env e)]] - | E_rec l e b => - let a := match e with - | Binds _ [a;_] _ => a - | _ => T_unit null - end in - [I_SEQ l [I_REC_FUNC null env a b (trim r (length env)) (repeat true (length env)) - (compile_binds (repeat true (length env)) env e)]] - | E_literal l lit => - [I_SEQ l [I_RAW null O (lit_code null lit)]] - | E_pair l e => - [I_SEQ l [I_SEQ null (compile_args r env e); - I_PAIR null 2]] - | E_car l e => - [I_SEQ l [I_SEQ null (compile_expr r env e); - I_CAR null]] - | E_cdr l e => - [I_SEQ l [I_SEQ null (compile_expr r env e); - I_CDR null]] - | E_unit l => - [I_SEQ l [I_UNIT null]] - | E_left l b e => - [I_SEQ l [I_SEQ null (compile_expr r env e); - I_LEFT null b]] - | E_right l a e => - [I_SEQ l [I_SEQ null (compile_expr r env e); - I_RIGHT null a]] - | E_if_bool l e1 e2 e3 => - [I_SEQ l [I_SEQ null (compile_expr r env e1); - I_IF null (compile_expr r env e2) (compile_expr r env e3)]] - | E_if_none l e1 e2 b3 => - [I_SEQ l [I_SEQ null (compile_expr r env e1); - I_IF_NONE null (compile_expr r env e2) (compile_binds r env b3)]] - | E_if_cons l e1 b2 e3 => - [I_SEQ l [I_SEQ null (compile_expr r env e1); - I_IF_CONS null (compile_binds r env b2) (compile_expr r env e3)]] - | E_if_left l e1 b2 b3 => - [I_SEQ l [I_SEQ null (compile_expr r env e1); - I_IF_LEFT null (compile_binds r env b2) (compile_binds r env b3)]] - | E_iter l e1 e2 => - [I_SEQ l [I_SEQ null (compile_expr r env e2); - I_ITER null (compile_binds r env e1 ++ [I_DROP l 1]); - I_UNIT null]] - | E_map l e1 e2 => - [I_SEQ l [I_SEQ null (compile_expr r env e2); - I_MAP null (compile_binds r env e1)]] - | E_loop_left l e1 b e2 => - [I_SEQ l [I_SEQ null (compile_expr r env e2); - I_LEFT null b; - I_LOOP_LEFT null (compile_binds r env e1)]] - | E_fold l e1 e2 e3 => - [I_SEQ l [I_SEQ null (compile_expr r env e1); - I_SEQ null (compile_expr (false :: r) env e2); - I_ITER null [I_SWAP null; I_PAIR null 2; - I_SEQ null (compile_binds r env e3)]]] - | E_fold_right l elem e1 e2 e3 => - [I_SEQ l [I_SEQ null (compile_expr r env e1); - I_SEQ null (compile_expr (false :: r) env e2); - I_NIL null elem; I_SWAP null; I_ITER null [I_CONS null]; - I_ITER null [I_PAIR null 2; - I_SEQ null (compile_binds r env e3)]]] - | E_failwith l e => - [I_SEQ l [I_SEQ null (compile_expr r env e); - I_FAILWITH null]] - | E_raw_michelson l a b code => - [I_SEQ l [I_LAMBDA null a b [I_RAW null 1 code]]] - | E_inline_michelson l code args => - [I_SEQ l (compile_args r env args ++ [I_RAW null (args_length args) code])] - | E_global_constant l b hash args => - [I_SEQ l [I_SEQ null (compile_args r env args); - I_RAW null (args_length args) (global_constant null hash)]] - | E_create_contract l p s script args => - [I_SEQ l [I_SEQ null (compile_args r env args); - (* following CREATE_CONTRACT is also given location l - because "view_restrictions" error messages depended - on it, hmm *) - I_CREATE_CONTRACT l p s (compile_binds [true] [T_pair null None None p s] script); - I_PAIR null 2]] - end -with -compile_args - (r : ope) (env : list ty) (e : args) {struct e} : prog := - match e with - | Args_nil l => [] - | Args_cons l e args => - [I_SEQ null (compile_expr r env e); - I_SEQ null (compile_args (false :: r) env args)] - end -with -compile_binds - (r : ope) (env : list ty) (e : binds) {struct e} : prog := - match e with - | Binds l az e => - let env' := az ++ env in - let r' := repeat true (length az) ++ r in - app [I_SEQ (with_var_names r' env' null) []] - (app (compile_expr r' env' e) - [I_DIP null [I_DROP null (length az)]]) - end. - -Definition compile_expr_typed (e : expr) : Prop := - forall g a, - expr_typed g e a -> - forall r d, - select r d = g -> - prog_typed (compile_expr r g e) d (a :: d). - -Definition compile_args_typed (e : args) : Prop := - forall g az, - args_typed g e az -> - forall r d, - select r d = g -> - prog_typed (compile_args r g e) d (az ++ d). - -Definition compile_binds_typed (e : binds) : Prop := - forall g az b, - binds_typed g e az b -> - forall r d, - select r d = g -> - prog_typed (compile_binds r g e) (az ++ d) (b :: d). - -Ltac Zify.zify_pre_hook ::= - repeat match goal with - | [H : @eq (list _) _ _ |- _] => - eapply (f_equal (@length _)) in H; - repeat rewrite app_length, plus_comm in H; - simpl in H - end. - -Lemma type_preservation : - (forall e, compile_expr_typed e) /\ - (forall e, compile_binds_typed e) /\ - (forall e, compile_args_typed e). -Proof. - eapply expr_mutind; - unfold compile_expr_typed, compile_binds_typed, compile_args_typed; - intros; - first[ invert_pred expr_typed - | invert_pred args_typed - | invert_pred binds_typed - ]; - repeat match goal with - | [H1 : forall g b, expr_typed g ?e b -> forall r d, select r d = g -> prog_typed (compile_expr r g ?e) d (b :: d), - H2: expr_typed ?g ?e ?b |- _] => - first [epose proof (H1 _ _ H2 [] _ eq_refl) - |epose proof (H1 _ _ H2 _ _ eq_refl)]; - mark_done H2 - | [H1 : forall g az b, binds_typed g ?e az b -> forall r d, select r d = g -> prog_typed (compile_binds r g ?e) (az ++ d) (b :: d), - H2: binds_typed ?g ?e ?az ?b |- _] => - first [epose proof (H1 _ _ _ H2 [] _ eq_refl) - |epose proof (H1 _ _ _ H2 _ _ eq_refl)]; - mark_done H2 - | [H1 : forall g az, args_typed g ?e az -> forall r d, select r d = g -> prog_typed (compile_args r g ?e) d (az ++ d), - H2: args_typed ?g ?e ?az |- _] => - first [epose proof (H1 _ _ H2 [] _ eq_refl) - |epose proof (H1 _ _ H2 _ _ eq_refl)]; - mark_done H2 - end; - clear_done; - simpl. - (* E_var *) - - repeat econstructor; - rewrite nth_error_embed; - auto; congruence. - (* E_let_in *) - - eauto with michelson. - admit. - (* E_tuple *) - - admit. - (* E_let_tuple *) - - admit. - (* E_proj *) - - admit. - (* E_update *) - - admit. - (* E_app *) - - admit. - (* E_lam *) - - admit. - (* E_literal *) - - admit. - (* E_pair *) - - admit. - (* E_car *) - - admit. - (* E_cdr *) - - admit. - (* E_unit *) - - admit. - (* E_left *) - - admit. - (* E_right *) - - admit. - (* E_if_left *) - - admit. - (* E_if_bool *) - - admit. - (* E_if_none *) - - admit. - (* E_if_cons *) - - admit. - (* E_iter *) - - admit. - (* E_map *) - - admit. - (* E_loop_left *) - - admit. - (* E_fold *) - - invert_pred iter_class. - + eauto 20 with michelson. - + admit. - + admit. - (* E_fold_right *) - - invert_pred iter_class. - + eauto 20 with michelson. - + admit. - + admit. - (* E_failwith *) - - eauto with michelson. - admit. - (* E_raw_michelson *) - - admit. - (* E_inline_michelson *) - - admit. - (* E_global_constant *) - - admit. - (* E_create_contract *) - - admit. - (* Binds *) - - specialize (H _ _ H8 (repeat true (length az) ++ r) (az ++ d)); - rewrite select_app in H by (rewrite repeat_length; auto); - rewrite select_repeat_true in H; - specialize (H eq_refl); - econstructor; [repeat econstructor|]; - eapply prog_typed_app; - eauto with michelson. - (* Args_nil *) - - eauto with michelson. - (* Args_cons *) - - eauto with michelson. -Admitted. - -(* This is used to postulate termination for strengthening loops. Should - probably replace it with specific Axioms? *) -Definition TRUST_ME_IT_TERMINATES {A : Set} : A. -Proof. admit. Admitted. - -Reserved Notation "'strengthen_progg'". - -Context {strengthen_meta : ope -> meta -> meta}. - -Fixpoint - strengthen_instr (i : instr) (r : list bool) {struct i} : list bool * prog := - match i with - | I_RAW l n code => - if ope_hd r - then (repeat true n ++ tl r, - [I_RAW l n code]) - (* if we knew that the code is pure, we could do this: *) - (* else (repeat false n ++ tl r, []) *) - (* but instead we have to settle for: *) - else (repeat true n ++ tl r, - [I_RAW l n code; I_DROP null 1]) - | I_SEQ l p => - let rp' := strengthen_progg p r in - let r' := fst rp' in - let p' := snd rp' in - let l' := strengthen_meta r' l in - (r', - [I_SEQ l' p']) - | I_DIP l p => - let rp' := strengthen_progg p (tl r) in - let r' := fst rp' in - let p' := snd rp' in - (ope_hd r :: r', - if ope_hd r - then [I_DIP l p'] - else p') - | I_DIG l n => - if ope_hd r - then - let r := tl r in - (split_left n r ++ true :: split_right n r, - [I_DIG l (weight (split_left n r))]) - else - let r := tl r in - (split_left n r ++ false :: split_right n r, - []) - | I_DUG l n => - let r1 := split_left n r in - let r2 := split_right n r in - if ope_hd r2 - then - let r2 := tl r2 in - (true :: r1 ++ r2, - [I_DUG l (weight r1)]) - else - let r2 := tl r2 in - (false :: r1 ++ r2, - []) - | I_DUP l n => - let r1 := split_left n r in - let r2 := split_right n r in - if ope_hd r1 - then - (tl r1 ++ true :: tl r2, - if ope_hd r2 - then [I_DUP l (S (weight (tl r1)))] - else [I_DIG l (weight (tl r1))]) - else - (tl r1 ++ r2, []) - | I_DROP l n => - (repeat false n ++ r, []) (* :D *) - | I_SWAP l => - (ope_hd (tl r) :: ope_hd r :: tl (tl r), - if andb (ope_hd r) (ope_hd (tl r)) - then [I_SWAP l] - else []) - | I_UNIT l => - (tl r, - if ope_hd r - then [I_UNIT l] - else []) - | I_TRUE l => - (tl r, - if ope_hd r - then [I_TRUE l] - else []) - | I_PAIR l n => - if ope_hd r - then (repeat true n ++ tl r, [I_PAIR l n]) - else (repeat false n ++ tl r, []) - | I_UNPAIR l n => - let r1 := split_left n r in - let r2 := split_right n r in - if leb 1 (weight r1) - then - if leb (weight r1) 1 - then - (* only one thing selected, use GET *) - let idx := (fix todo (n : nat) (r1 : ope) {struct r1} : nat := - match r1 with - | [] => 0 - | b :: r1 => if b then n else todo (S n) r1 - end) 0 r1 in - (* comb elements are indexed with GET 2i+1, except the last - element which is GET 2i. *) - let zero_or_one := if (beq_nat idx (n-1)) then 0 else 1 in - (true :: r2, [I_GET l (zero_or_one + 2 * idx)]) - else - (* more than one thing selected, use UNPAIR *) - (true :: r2, I_UNPAIR l n :: compile_ope r1) - else - (* nothing selected *) - (false :: r2, []) - | I_GET l n => - (r, - if ope_hd r - then [I_GET l n] - else []) - | I_UPDATE l n => - (ope_hd r :: r, - if ope_hd r - then [I_UPDATE l n] - else []) - | I_CAR l => - (r, - if ope_hd r - then [I_CAR l] - else []) - | I_CDR l => - (r, - if ope_hd r - then [I_CDR l] - else []) - | I_LEFT l b => - (r, - if ope_hd r - then [I_LEFT l b] - else []) - | I_RIGHT l a => - (r, - if ope_hd r - then [I_RIGHT l a] - else []) - | I_IF_LEFT l bt bf => - let (rt, bt') := strengthen_progg bt r in - let (rf, bf') := strengthen_progg bf r in - let r' := true :: union (tl rt) (tl rf) in - (r', - [I_IF_LEFT l - (compile_ope (ope_hd rt :: inj1 (tl rt) (tl rf)) ++ bt') - (compile_ope (ope_hd rf :: inj2 (tl rt) (tl rf)) ++ bf')]) - - | I_IF l bt bf => - let (rt, bt') := strengthen_progg bt r in - let (rf, bf') := strengthen_progg bf r in - let r' := true :: union rt rf in - (r', - [I_IF l - (compile_ope (inj1 rt rf) ++ bt') - (compile_ope (inj2 rt rf) ++ bf')]) - - | I_IF_NONE l bt bf => - let (rt, bt') := strengthen_progg bt r in - let (rf, bf') := strengthen_progg bf r in - let r' := true :: union rt (tl rf) in - (r', - [I_IF_NONE l - (compile_ope (inj1 rt (tl rf)) ++ bt') - (compile_ope (ope_hd rf :: inj2 rt (tl rf)) ++ bf')]) - - | I_NIL l a => - (tl r, - if ope_hd r - then [I_NIL l a] - else []) - | I_CONS l => - (ope_hd r :: ope_hd r :: tl r, - if ope_hd r - then [I_CONS l] - else []) - | I_IF_CONS l bt bf => - let (rt, bt') := strengthen_progg bt r in - let (rf, bf') := strengthen_progg bf r in - let r' := true :: union (tl (tl rt)) rf in - (r', - [I_IF_CONS l - (compile_ope (ope_hd rt :: ope_hd (tl rt) :: inj1 (tl (tl rt)) rf) ++ bt') - (compile_ope (inj2 (tl (tl rt)) rf) ++ bf')]) - - | I_FUNC l cs a b r1 r2 body => - if ope_hd r - then - let (rb, body') := strengthen_progg body (true :: repeat false (weight r2)) in - (union (comp (tl rb) r1) (tl r), - I_FUNC l - (select (tl rb) cs) - a b - (inj1 (comp (tl rb) r1) (tl r)) - (repeat false (weight (tl rb))) - (compile_ope [ope_hd rb] ++ body') - :: compile_ope (true :: inj2 (comp (tl rb) r1) (tl r))) - else (tl r, []) - | I_REC_FUNC l cs a b r1 r2 body => - if ope_hd r - then - let (rb, body') := strengthen_progg body (true :: repeat false (weight r2)) in - (union (comp (tl (tl rb)) r1) (tl r), - I_REC_FUNC l - (select (tl (tl rb)) cs) - a b - (inj1 (comp (tl (tl rb)) r1) (tl r)) - (repeat false (weight (tl (tl rb)))) - (compile_ope [ope_hd rb; ope_hd (tl rb)] ++ body') - :: compile_ope (true :: inj2 (comp (tl (tl rb)) r1) (tl r))) - else (tl r, []) - | I_LAMBDA l a b body => - (tl r, - if ope_hd r - then - let (rb, body') := strengthen_progg body [true] in - [I_LAMBDA l a b (compile_ope [ope_hd rb] ++ body')] - else []) - | I_EXEC l => - (true :: true :: tl r, - I_EXEC l :: compile_ope [ope_hd r]) - | I_APPLY_LAMBDA l c => - (ope_hd r :: ope_hd r :: tl r, - if ope_hd r - then [I_APPLY_LAMBDA l c] - else []) - - | I_FAILWITH l => - ([true], - [I_FAILWITH l]) - - | I_LOOP l body => - let rfix := proj1_sig (fix_ope (fun x => union (fst (strengthen_progg body (true :: x))) r) [] TRUST_ME_IT_TERMINATES) in - let (rb, body') := strengthen_progg body (true :: rfix) in - (true :: rfix, - I_LOOP l (compile_ope (inj1 rb r) ++ body') :: compile_ope (inj2 rb r)) - | I_LOOP_LEFT l body => - let rfix := proj1_sig (fix_ope (fun x => union (tl (fst (strengthen_progg body (true :: x)))) (tl r)) [] TRUST_ME_IT_TERMINATES) in - let (rb, body') := strengthen_progg body (true :: rfix) in - (true :: rfix, - I_LOOP_LEFT l (compile_ope (ope_hd rb :: inj1 (tl rb) (tl r)) ++ body') :: compile_ope (ope_hd r :: inj2 (tl rb) (tl r))) - | I_ITER l body => - let rfix := proj1_sig (fix_ope (fun x => union (tl (fst (strengthen_progg body x))) r) [] TRUST_ME_IT_TERMINATES) in - let (rb, body') := strengthen_progg body rfix in - (true :: rfix, - I_ITER l (compile_ope (ope_hd rb :: inj1 (tl rb) r) ++ body') :: compile_ope (inj2 (tl rb) r)) - | I_MAP l body => - let rfix := proj1_sig (fix_ope (fun x => union (tl (fst (strengthen_progg body (true :: x)))) (tl r)) [] TRUST_ME_IT_TERMINATES) in - let (rb, body') := strengthen_progg body (true :: rfix) in - (true :: rfix, - I_MAP l (compile_ope (true :: inj1 (tl rb) (tl r)) ++ body') :: compile_ope (ope_hd r :: inj2 (tl rb) (tl r))) - | I_FOR l body => - let rfix := proj1_sig (fix_ope (fun x => union (tl (fst (strengthen_progg body x))) r) [] TRUST_ME_IT_TERMINATES) in - let (rb, body') := strengthen_progg body rfix in - (true :: true :: true :: rfix, - I_FOR l (compile_ope (ope_hd rb :: inj1 (tl rb) r) ++ body') :: compile_ope (inj2 (tl rb) r)) - | I_CREATE_CONTRACT l p s script => - let (rs, script') := strengthen_progg script [true] in - (true :: true :: true :: tl (tl r), - [I_CREATE_CONTRACT l p s (compile_ope [ope_hd rs] ++ script')]) - - end -(* this notation deals with the nested induction problem here, with - instrs containing lists of instrs *) -where "'strengthen_progg'" := - (fix strengthen_prog (p : prog) (r : ope) {struct p} : list bool * prog := - match p with - | [] => (r, []) - | i :: p => - let r1p' := strengthen_prog p r in - let r1 := fst r1p' in - let p' := snd r1p' in - let r2i' := strengthen_instr i r1 in - let r2 := fst r2i' in - let i' := snd r2i' in - (r2, i' ++ p') - end). - -(* Exposing the 'strengthen_progg' notation for extraction: *) -Definition strengthen_prog (p : prog) (r : ope) : list bool * prog := - strengthen_progg p r. - -Definition strengthen_instr_preservation : - forall i s1 s2, instr_typed i s1 s2 -> Prop := - fun i s1 s2 _ => - forall r, - (* TODO use ope_valid here? *) - length r <= length s2 -> - length (fst (strengthen_instr i r)) <= length s1 /\ - prog_typed (snd (strengthen_instr i r)) - (select (fst (strengthen_instr i r)) s1) - (select r s2). - -Definition strengthen_prog_preservation : - forall p s1 s2, prog_typed p s1 s2 -> Prop := - fun p s1 s2 _ => - forall r, - length r <= length s2 -> - length (fst (strengthen_progg p r)) <= length s1 /\ - prog_typed (snd (strengthen_progg p r)) - (select (fst (strengthen_progg p r)) s1) - (select r s2). - -Lemma tl_length {A : Set} (xs : list A) : - length (tl xs) = length xs - 1. -Proof. destruct xs; simpl; try rewrite Nat.sub_0_r; reflexivity. Qed. - -Ltac strengthen_rewrite := - subst; simpl; simpl in *; - repeat first [rewrite app_length in * - |rewrite repeat_length in * - |rewrite tl_length in * - |rewrite inj1_length in * - |rewrite inj2_length in * - |rewrite union_length in * - |rewrite select_inj1 in * - |rewrite select_inj2 in * - |rewrite select_app in * - |rewrite select_filter_id in * - |rewrite select_repeat_false in * - |rewrite select_repeat_true' in * - |rewrite split_left_length in * - |rewrite split_right_length in * - |rewrite split_left_nil in * - |rewrite split_right_nil in * - |rewrite select_split in * - |rewrite select_weight in * - |simpl in *]. - -Opaque compile_ope. - -Lemma strengthen_instr_typed : - (forall i s1 s2 (H : instr_typed i s1 s2), strengthen_instr_preservation H) /\ - (forall p s1 s2 (H : prog_typed p s1 s2), strengthen_prog_preservation H). -Proof with try split; try lia; eauto 15 with michelson. - eapply (@instr_typed_mutind - strengthen_instr_preservation - strengthen_prog_preservation); - unfold strengthen_prog_preservation; - unfold strengthen_instr_preservation; - simpl; intros; - match goal with - | [|- True] => trivial - | _ => idtac - end. - (* I_RAW *) - - destruct r as [|[|] r]; - strengthen_rewrite... - (* I_SEQ *) - - specialize (H r H0); destruct_conjs; eauto with michelson. - (* I_DIP *) - - specialize (H (tl r)); - rewrite tl_length in H; - specialize (H ltac:(lia)); - destruct_conjs; - remember (strengthen_progg p (tl r)) as p'; - destruct r as [|[|] r]; - split; - try lia; - try eassumption; - simpl; - eauto with michelson. - (* I_DIG *) - - destruct r as [|[|] r]; - strengthen_rewrite; - try split; try lia; eauto with michelson; - econstructor; econstructor; - strengthen_rewrite; - auto. - (* I_DUG *) - - remember (split_right (length s1) r) as rr; - destruct rr as [|[|] rr]; - try destruct u; - subst; rewrite <- Heqrr in *; - strengthen_rewrite; - try rewrite <- Heqrr in *; - try split; try lia; eauto with michelson; - pose proof (f_equal (@length _) Heqrr) as Hlen; - simpl in Hlen; - rewrite split_right_length in Hlen; - try lia; - econstructor; econstructor; - strengthen_rewrite; auto. - (* I_DUP *) - - pose proof (nth_error_split _ _ e); - destruct_conjs; - destruct r as [|[|] r]; - strengthen_rewrite; - try split; try lia; eauto with michelson; - remember (split_right (length H0) r) as rr; - destruct rr as [|[|] rr]; - strengthen_rewrite; - econstructor; econstructor; - strengthen_rewrite; - auto; - rewrite nth_error_app2 by (rewrite select_weight; auto; rewrite split_left_length; auto); - rewrite select_weight by (rewrite split_left_length; auto); - rewrite Nat.sub_diag; - reflexivity. - (* I_DROP *) - - strengthen_rewrite... - (* I_SWAP *) - - destruct r as [|[|] [|[|] r]]; strengthen_rewrite... - (* I_UNIT *) - - destruct r as [|[|] r]; strengthen_rewrite... - (* I_TRUE *) - - destruct r as [|[|] r]; strengthen_rewrite... - (* I_LEFT *) - - destruct r as [|[|] r]; strengthen_rewrite... - (* I_RIGHT *) - - destruct r as [|[|] r]; strengthen_rewrite... - (* I_IF_LEFT *) - - specialize (H r); - specialize (H0 r); - remember (strengthen_progg bt r) as bt'; - destruct bt' as [[|[|] rt] bt']; - remember (strengthen_progg bf r) as bf'; - destruct bf' as [[|[|] rf] bf']; - simpl; - specialize (H H1); - specialize (H0 H1); - destruct_conjs; - strengthen_rewrite; - try split; - repeat rewrite union_nil_r; - try lia; - try solve [rewrite union_length; lia]; - try solve [econstructor; econstructor; - eapply prog_typed_app; - try eassumption; - eapply compile_ope_typed; - simpl; - first[ rewrite inj1_length; - rewrite select_weight by (rewrite union_length; lia); - reflexivity - | rewrite select_inj1; reflexivity - | rewrite inj2_length; - rewrite select_weight by (rewrite union_length; lia); - reflexivity - | rewrite select_inj2; reflexivity ]]. - + econstructor; econstructor; - eapply prog_typed_app; - try eassumption; - eapply compile_ope_typed; - auto. - + assert (hmm : match rf with - | [] => [] - | _ :: _ => repeat false (Datatypes.length (filter id rf)) - end = repeat false (Datatypes.length (filter id rf))) - by (destruct rf; reflexivity); - rewrite hmm; clear hmm; - econstructor; econstructor; - eapply prog_typed_app; - try eassumption; - eapply compile_ope_typed; - simpl; - try rewrite repeat_length; - try rewrite select_weight; - try rewrite select_repeat_false; - try rewrite select_filter_id; - auto; lia. - + assert (hmm : match rf with - | [] => [] - | _ :: _ => repeat false (Datatypes.length (filter id rf)) - end = repeat false (Datatypes.length (filter id rf))) - by (destruct rf; reflexivity); - rewrite hmm; clear hmm; - econstructor; econstructor; - eapply prog_typed_app; - try eassumption; - eapply compile_ope_typed; - simpl; - try rewrite repeat_length; - try rewrite select_weight; - try rewrite select_repeat_false; - try rewrite select_filter_id; - auto; lia. - + econstructor; econstructor; - eapply prog_typed_app; - try eassumption; - eapply compile_ope_typed; - simpl; - try rewrite repeat_length; - try rewrite select_weight; - try rewrite select_repeat_false; - try rewrite select_filter_id; - auto; try lia; - repeat rewrite inj1_length; - repeat rewrite inj2_length; - repeat rewrite union_nil_r; - repeat rewrite union_nil_l; - auto; - match goal with - | [|- context G [select (inj1 ?r []) (select ?r ?s)]] => - let H := fresh "H" in - let g := context G [select (inj1 r []) (select (union r []) s)] in - enough (H : g) by (rewrite union_nil_r in H; exact H); - rewrite select_inj1 - | [|- context G [select (inj2 ?r []) (select ?r ?s)]] => - let H := fresh "H" in - let g := context G [select (inj2 r []) (select (union r []) s)] in - enough (H : g) by (rewrite union_nil_r in H; exact H); - rewrite select_inj2 - end; - reflexivity. - + econstructor; econstructor; - eapply prog_typed_app; - try eassumption; - eapply compile_ope_typed; - simpl. - * rewrite inj1_length; rewrite union_nil_r; - rewrite select_weight by lia; auto. - * rewrite <- (union_nil_r rt) at 2; - rewrite select_inj1; auto. - * rewrite inj2_length, union_nil_r; - rewrite select_weight by lia; auto. - * rewrite <- (union_nil_r rt) at 2; - rewrite select_inj2; auto. - (* I_PAIR *) - - destruct r as [|[|] r]; - strengthen_rewrite... - (* I_UNPAIR *) - - admit. - (* I_GET *) - - destruct r as [|[|] r]; strengthen_rewrite... - (* I_UPDATE *) - - destruct r as [|[|] r]; strengthen_rewrite... - (* I_CAR *) - - destruct r as [|[|] r]; strengthen_rewrite... - (* I_CDR *) - - destruct r as [|[|] r]; strengthen_rewrite... - (* I_IF *) - - specialize (H r); - specialize (H0 r); - remember (strengthen_progg bt r) as bt'; - destruct bt' as [[|[|] rt] bt']; - remember (strengthen_progg bf r) as bf'; - destruct bf' as [[|[|] rf] bf']; - simpl; - specialize (H H1); - specialize (H0 H1); - destruct_conjs; - strengthen_rewrite; - try split; - repeat rewrite union_nil_r; - try lia; - try solve [rewrite union_length; lia]; - econstructor; econstructor; - eapply prog_typed_app; - try eassumption; - eapply compile_ope_typed; - try reflexivity; - destruct s1; strengthen_rewrite... - (* I_IF_NONE *) - - specialize (H r); - specialize (H0 r); - remember (strengthen_progg bt r) as bt'; - destruct bt' as [rt bt']; - remember (strengthen_progg bf r) as bf'; - destruct bf' as [[|[|] rf] bf']; - simpl; - specialize (H H1); - specialize (H0 H1); - destruct_conjs; - strengthen_rewrite; - try split; - try lia; - try eassumption; - econstructor; try econstructor; - try eapply prog_typed_app; - try eapply compile_ope_typed; - strengthen_rewrite... - (* I_NIL *) - - split; destruct r as [|[|] r]; strengthen_rewrite... - (* I_CONS *) - - admit. - (* I_IF_CONS *) - - specialize (H r); - specialize (H0 r); - remember (strengthen_progg bt r) as bt'; - destruct bt' as [[|[|] [|[|] rt]] bt']; - remember (strengthen_progg bf r) as bf'; - destruct bf' as [rf bf']; - specialize (H H1); - specialize (H0 H1); - destruct_conjs; - strengthen_rewrite; - try split; - try lia; - try eassumption; - econstructor; econstructor; - eapply prog_typed_app; - try eassumption; - try eapply compile_ope_typed; - try destruct rf; - try destruct b; - try destruct s1; - strengthen_rewrite... - (* I_FUNC *) - - admit. - (* I_REC_FUNC *) - - admit. - (* I_EXEC *) - - destruct r; - split; - simpl in *; - try lia; - repeat econstructor. - + eapply compile_ope_typed; auto. - + destruct b0. - * apply (@compile_ope_weak_typed [true] [b] [b]); auto. - * apply (@compile_ope_weak_typed [false] [b] []); auto. - (* I_LAMBDA *) - - specialize (H [true] ltac:(simpl; lia)); - remember (strengthen_progg code [true]) as code'; - destruct code' as [rcode code']; - destruct r as [|[|] r]; - strengthen_rewrite... - destruct_conjs; - econstructor; econstructor; - eapply prog_typed_app; - try eapply compile_ope_typed; - try eassumption; - try reflexivity; - destruct rcode as [|[|] rcode]; - try reflexivity; - simpl; rewrite select_nothing; - reflexivity. - (* I_EXEC *) - - destruct r as [|[|] r]; split; simpl in *; try lia; - try (repeat econstructor; eapply compile_ope_typed; reflexivity); - repeat econstructor; eapply (@compile_ope_weak_typed [false] [b] []); reflexivity. - (* I_APPLY_LAMBDA *) - - destruct r as [|[|] r]; strengthen_rewrite... - (* I_LOOP *) - - match goal with [|- context[fix_ope ?f ?x ?d]] => remember (fix_ope f x d) as rfix end; - destruct rfix as [rfix rfixed]; - simpl; - pose proof (union_length (fst (strengthen_progg body (true :: rfix))) r) as Hlen1; - assert (Hlen2 : length rfix <= length s). - { eapply (f_equal (@proj1_sig _ _)) in Heqrfix; - simpl in Heqrfix; - rewrite Heqrfix; - eapply fix_ope_preserves. - - intros x Hx; - rewrite union_length; - pose proof (proj1 (H (true :: x) (le_n_S _ _ Hx))); - lia. - - simpl; lia. } - pose proof (H (true :: rfix) (le_n_S _ _ Hlen2)) as [H1 H2]; - repeat match goal with - | [|- context[let (x, y) := ?z in _]] => - rewrite (surjective_pairing z) - end; - remember (strengthen_progg body (true :: rfix)) as rbody'; - simpl; - split; [lia|]; - repeat econstructor; - try eapply prog_typed_app; - try eapply compile_ope_typed; - try rewrite inj1_length; - try rewrite inj2_length. - + admit. - + assert (HH : select (inj1 (fst rbody') r) (select rfix s) = - select (inj1 (fst rbody') r) (select (union (fst rbody') r) s)) by admit. - rewrite HH, select_inj1; reflexivity. - + exact H2. - + admit. - + assert (HH : select (inj2 (fst rbody') r) (select rfix s) = - select (inj2 (fst rbody') r) (select (union (fst rbody') r) s)) by admit. - rewrite HH, select_inj2; reflexivity. - (* I_LOOP_LEFT *) - - admit. - (* I_ITER *) - - admit. - (* I_MAP *) - - admit. - (* I_FOR *) - - admit. - (* I_FAILWITH *) - - idtac... - (* I_CREATE_CONTRACT *) - - admit. - (* nil prog *) - - split... - (* cons prog *) - - specialize (H0 r H1); - destruct_conjs; - specialize (H (fst (strengthen_progg p r)) H0); - destruct_conjs; - split; try lia; - remember (strengthen_progg p r) as p'; - destruct p' as [r' p']; - try lia; - eapply prog_typed_app... -Admitted. - -End compiler. diff --git a/src/coq/dune b/src/coq/dune deleted file mode 100644 index 532a613772..0000000000 --- a/src/coq/dune +++ /dev/null @@ -1,8 +0,0 @@ -(coq.theory - (name ligo_coq) - (modules :standard) - (mode vo) - ; TODO hmm, nix barfs in opaline because this will install in - ; lib_root section for coq user-contrib - ; (package ligo) - ) diff --git a/src/coq/lemmas.v b/src/coq/lemmas.v deleted file mode 100644 index b32a8b1b2a..0000000000 --- a/src/coq/lemmas.v +++ /dev/null @@ -1,33 +0,0 @@ -Set Implicit Arguments. -From Coq Require Import List. -Import ListNotations. - -(* Induction on lists built by appending elements one by one (xs ++ [x]), also called snoc xs x, the opposite of cons x xs. - Given a prop that accepts a list of A (P : list A -> Prop), - If the prop is satisfied for the empty list (P []) - And appending any single A to any list of A preserves the prop (forall x xs, P xs -> P (xs ++ [x])), - Then the prop holds for any list of A. *) -Lemma snoc_list_ind : - forall {A : Set} (P : list A -> Prop), - P [] -> (forall x xs, P xs -> P (xs ++ [x])) -> - forall xs, P xs. -Proof. - intros A' P Pnil Psnoc xs. - enough (P (rev (rev xs))). rewrite rev_involutive in H. assumption. - apply rev_list_ind. - - assumption. - - enough (forall a l, P (rev (rev l)) -> P (rev (a :: rev l))). - { intros a l Prl. specialize (H a (rev l)). - rewrite rev_involutive in H. specialize (H Prl). - rewrite rev_involutive in H. assumption. } - intros a l Pl. rewrite rev_involutive in Pl. - simpl. rewrite rev_involutive. - apply Psnoc; assumption. -Qed. - - -(* The length of (xs ++ [x]) a.k.a. (snoc xs x), the opposite of (cons x xs), - is equal to 1 + (length xs) *) -Lemma length_snoc {A : Type} {xs : list A} {x : A} : - length (xs ++ [x]) = S (length xs). -Proof. induction xs; simpl; auto. Qed. diff --git a/src/coq/ope.v b/src/coq/ope.v deleted file mode 100644 index bc5600fa5f..0000000000 --- a/src/coq/ope.v +++ /dev/null @@ -1,896 +0,0 @@ -From Coq Require Import List Lia. -From Coq Require Arith.Peano_dec. -Import ListNotations. -Unset Lia Cache. - -(* Definitions and lemmas related to order-preserving embeddings - (OPEs). - - The central concept below is slice categories of categories of - OPEs. - - See for example "Everybody's Got To Be Somewhere", Conor McBride: - https://arxiv.org/abs/1807.04085 - - An order-preserving embedding from a list [xs] into a list [ys] is - a witness that [xs] is a (not necessarily continiguous) subsequence - of [ys]. There can be more than one witness, for example [x] embeds - into [x; x] in two different ways. - - Here we will work with an extrinsically-typed version of these - concepts. In particular, we represent objects in the slice category - of OPEs as lists of booleans: *) - -Notation ope := (list bool). - -(* Each element of the list says whether to keep (true) or drop - (false) the corresponding element of the codomain list [ys]. We can - thus compute the selected list [xs]: *) - -Fixpoint select {A : Set} (r : ope) (ys : list A) : list A := - match r with - | [] => [] - | u :: r => - match ys with - | [] => [] - | y :: ys => - if u - then y :: select r ys - else select r ys - end - end. - -(* This representation is somewhat improper; a given [list bool] may - contain more or fewer elements than the list [ys]. Assuming an - additional length restriction, we could define an isomorphism: - - {r : list bool | length r = length ys} ~= slice category over ys - - Instead, I will treat a too-short list as if it were padded with - [false] on the right. I will usually simply ignore the possibility - that the OPE is too long. In some specific cases we will need to - rule this out, which motivates proving the "length" lemmas below - (comp_length etc.) *) - - -(* Now, we define various operations and lemmas on the slice - category. *) - -(* Selecting from nothing gives nothing. *) -Lemma select_nothing {A : Set} (r : ope) : @select A r [] = []. -Proof. induction r; auto. Qed. - -(* Select distributes over list concatenation *) -Lemma select_app {A : Set} (r1 r2 : ope) (xs ys : list A) : - length r1 = length xs -> - select (r1 ++ r2) (xs ++ ys) = (select r1 xs ++ select r2 ys)%list. -Proof. - revert r2 xs ys; - induction r1; - intros; - destruct xs; - try discriminate H; - try destruct a; - simpl; - try rewrite IHr1; - auto. -Qed. - -(* (repeat true) selects everything *) -Lemma select_repeat_true {A : Set} (xs : list A) : - select (repeat true (length xs)) xs = xs. -Proof. induction xs; simpl; try rewrite IHxs; auto. Qed. - -Lemma select_repeat_true' {A : Set} (xs : list A) {n} : - n >= length xs -> - select (repeat true n) xs = xs. -Proof. - revert n; induction xs; intros n H1; simpl. - - rewrite select_nothing; reflexivity. - - simpl in H1; destruct n; try solve [inversion H1]; simpl; apply f_equal, IHxs; lia. -Qed. - -(* (repeat false) selects nothing *) -Lemma select_repeat_false {A : Set} (xs : list A) {n} : - select (repeat false n) xs = []. -Proof. - revert n; induction xs; intros n; simpl. - - rewrite select_nothing; reflexivity. - - destruct n; try reflexivity; eapply IHxs. -Qed. - -(* Composition, in some sense. See lemma [select_comp] below. *) -Fixpoint comp (us vs : ope) : ope := - match vs with - | [] => [] - | v :: vs => - if v - then - match us with - | [] => [] - | u :: us => u :: comp us vs - end - else false :: comp us vs - end. - -Lemma comp_length (us vs : ope) : - length (comp us vs) <= length vs. -Proof. - revert us; induction vs as [|v vs]; - intros us; - simpl in *; - try lia; - destruct v; - destruct us; - simpl in *; - try lia; - try (eapply le_n_S, IHvs; lia). -Qed. - -(* Selection of composition is composition of selections: *) -Lemma select_comp {A : Set} (us vs : ope) (xs : list A) : - select (comp us vs) xs = select us (select vs xs). -Proof. - revert us xs; - induction vs as [|v vs]; - intros [|u us] [|x xs]; - try destruct u; - try destruct v; - try reflexivity; - solve [simpl; rewrite IHvs; auto]. -Qed. - -(* The coproduct in the slice category, as described by - McBride. [union us vs] selects everything selected by _either_ [us] - or [vs]. See the lemmas [select_inj1] and [select_inj2] below. *) -Fixpoint union (us vs : ope) : ope := - match (us, vs) with - | ([], vs) => vs - | (us, []) => us - | (u :: us, v :: vs) => orb u v :: union us vs - end. - -Lemma union_nil_r (us : ope) : union us [] = us. -Proof. induction us; auto; simpl; rewrite IHus; auto. Qed. - -Lemma union_nil_l (us : ope) : union [] us = us. -Proof. reflexivity. Qed. - -Lemma union_length (us vs : ope) : length (union us vs) = max (length us) (length vs). -Proof. - revert vs; induction us as [|u us]; intros [|v vs]; simpl; - try reflexivity; - eapply f_equal, IHus. -Qed. - -(* The "injections" into the coproduct. [inj1 us vs] selects the - 'left' part of the union. See also the lemmas [select_inj1] and - [select_inj2] below. *) -Fixpoint inj1 (us vs : ope) : ope := - match (us, vs) with - | (us, []) => filter id us - | ([], vs) => repeat false (length (filter id vs)) - | (u :: us, v :: vs) => - if orb u v - then u :: inj1 us vs - else inj1 us vs - end. - -(* [inj2] selects the 'right' part of the union. *) -Fixpoint inj2 (us vs : ope) : ope := - match (us, vs) with - | ([], vs) => filter id vs - | (us, []) => repeat false (length (filter id us)) - | (u :: us, v :: vs) => - if orb u v - then v :: inj2 us vs - else inj2 us vs - end. - -(* Side lemma *) -Lemma select_filter_id {A : Set} (us : ope) (xs : list A) : - select (filter id us) (select us xs) = select us xs. -Proof. - revert xs; - induction us as [|u us]; - intros [|x xs]; - try destruct u; - simpl; - repeat rewrite select_nothing; - auto; - rewrite IHus; auto. -Qed. - -Lemma select_inj1 {A : Set} (us vs : ope) (xs : list A) : - select (inj1 us vs) (select (union us vs) xs) = select us xs. -Proof. - revert vs xs; - induction us as [|u us]; - intros [|v vs] [|x xs]; - try destruct u; - try destruct v; - repeat rewrite select_nothing; simpl; - repeat rewrite select_filter_id; simpl; - repeat rewrite select_repeat_false; simpl; - try rewrite IHus; - auto; - destruct (select vs xs); - try reflexivity; - rewrite select_repeat_false; - reflexivity. -Qed. - -Lemma select_inj2 {A : Set} (us vs : ope) (xs : list A) : - select (inj2 us vs) (select (union us vs) xs) = select vs xs. -Proof. - revert vs xs; - induction us as [|u us]; - intros [|v vs] [|x xs]; - try destruct u; - try destruct v; - repeat rewrite select_nothing; simpl; - repeat rewrite select_filter_id; simpl; - repeat rewrite select_repeat_false; simpl; - try rewrite IHus; - auto; - destruct (select us xs); - try reflexivity; - rewrite select_repeat_false; - reflexivity. -Qed. - -Lemma inj1_length (us vs : ope) : - length (inj1 us vs) = length (filter id (union us vs)). -Proof. - revert vs; induction us as [|[|] us]; - intros [|[|] vs]; - simpl; - try reflexivity; - try specialize (IHus vs); - try lia; - try rewrite repeat_length; - reflexivity. -Qed. - -Lemma inj2_length (us vs : ope) : - length (inj2 us vs) = length (filter id (union us vs)). -Proof. - revert vs; induction us as [|[|] us]; - intros [|[|] vs]; - simpl; - try reflexivity; - try specialize (IHus vs); - try lia; - try rewrite repeat_length; - reflexivity. -Qed. - -(* [only] selects one element by index *) -Fixpoint only (n : nat) : ope := - match n with - | O => [true] - | S n => false :: only n - end. - -Lemma select_only {A : Set} (n : nat) (xs : list A) : - select (only n) xs = match List.nth_error xs n with None => [] | Some x => [x] end. -Proof. revert xs; induction n; destruct xs; simpl; auto. Qed. - -(* right inverse to [only]: first selected index, or 0. *) -Fixpoint one (us : ope) : nat := - match us with - | [] => O - | u :: us => - if u - then O - else S (one us) - end. - -Lemma one_only (n : nat) : one (only n) = n. -Proof. induction n; simpl; auto. Qed. - -Lemma nth_error_one {A : Set} (us : ope) (x : A) (xs : list A) : - select us xs = [x] -> - nth_error xs (one us) = Some x. -Proof. - revert x xs; - induction us as [|u us]; - intros; - destruct xs as [|x' xs]; simpl in *; - try discriminate H; - destruct u; simpl in *; - try (inversion H; subst; reflexivity); - apply IHus; auto. -Qed. - -(* Action of OPEs on de Bruijn indices *) -Fixpoint embed (r : ope) (n : nat) : nat := - match r with - | [] => O - | false :: r => S (embed r n) - | true :: r => - match n with - | O => O - | S n => S (embed r n) - end - end. - -Lemma nth_error_embed {A : Set} (r : ope) (ys : list A) (n : nat) : - nth_error (select r ys) n <> None -> - nth_error ys (embed r n) = nth_error (select r ys) n. -Proof. - revert ys n; - induction r; intros; simpl. - - destruct ys; - exfalso; contradiction H; destruct n; auto. - - destruct a; destruct ys; - try solve [exfalso; contradiction H; destruct n; auto]. - + destruct n; try reflexivity; eapply IHr; auto. - + eapply IHr; auto. -Qed. - - -(* like firstn, but pads with false so that the result has at least n elements *) -Fixpoint split_left (n : nat) (r : ope) : ope := - match n with - | O => [] - | S n => - match r with - | [] => repeat false (S n) - | u :: r => - u :: split_left n r - end - end. - -Definition split_right := @skipn bool. - -Lemma split_left_length {n r} : - length (split_left n r) = n. -Proof. - revert r; - induction n; - intros r; - simpl; try reflexivity. - - destruct r; simpl. - + rewrite repeat_length; reflexivity. - + rewrite IHn; reflexivity. -Qed. - -Lemma split_right_length {n r} : - length (split_right n r) = length r - n. -Proof. - unfold split_right; apply skipn_length. -Qed. - -Lemma split_left_nil {n} : - split_left n [] = repeat false n. -Proof. destruct n; eauto. Qed. - -Lemma split_right_nil {n} : - split_right n [] = []. -Proof. destruct n; eauto. Qed. - -(* "Weight" of an OPE: number of elements selected. *) -Definition weight (r : ope) : nat := length (filter id r). - -Lemma select_weight {A : Set} {r : ope} {xs : list A} : - length r <= length xs -> - length (select r xs) = weight r. -Proof. - revert xs; induction r as [|u r]; intros xs H1; - unfold weight; simpl; try reflexivity; - destruct xs as [|x xs]; - destruct u; simpl; simpl in H1. - - exfalso; lia. - - exfalso; lia. - - apply f_equal, IHr; lia. - - apply IHr; lia. -Qed. - -Lemma select_length_le_weight {A : Set} {r : ope} {xs : list A} : - length (select r xs) <= weight r. -Proof. - revert xs; induction r as [|[] r]; intros [|x xs]; - unfold weight; simpl; try reflexivity; try lia; - try apply le_n_S; - apply IHr. -Qed. - -Lemma select_length_le_length {A : Set} {r : ope} {xs : list A} : - length (select r xs) <= length xs. -Proof. - revert xs; induction r as [|[] r]; intros [|x xs]; - unfold weight; simpl; try reflexivity; try lia; - first [apply le_n_S | apply le_S]; - apply IHr. -Qed. - -Lemma select_split {A : Set} {r : ope} {xs ys : list A} : - select r (xs ++ ys) = - select (split_left (length xs) r) xs ++ select (split_right (length xs) r) ys. -Proof. - revert xs ys; - induction r as [|u r]; - intros xs ys. - - rewrite split_left_nil, select_repeat_false, split_right_nil; reflexivity. - - destruct u; destruct xs as [|x xs]; - try reflexivity; - try (simpl; try apply f_equal; apply IHr). -Qed. - -Lemma select_split' {A : Set} {r : ope} {xs : list A} {n : nat} : - select (split_left n r ++ split_right n r) xs = select r xs. -Proof. - revert r n; induction xs; intros r n. - - repeat rewrite select_nothing; auto. - - destruct n; try reflexivity; - destruct r as [|[|] r]; - simpl. - + rewrite app_nil_r, select_repeat_false; auto. - + apply f_equal, IHxs. - + apply IHxs. -Qed. - -Definition ope_hd (r : ope) : bool := - match r with - | [] => false - | u :: r => u - end. - - - -(* Definitions and lemmas about equivalence of OPEs *) - -Inductive null_ope : ope -> Prop := -| Null_ope_nil : - null_ope [] -| Null_ope_drop {r} : - null_ope r -> - null_ope (false :: r) -. - -Lemma null_ope_iff_select {r} : - null_ope r <-> - (forall {A : Set} {xs : list A}, select r xs = []). -Proof. - split. - - intros H; induction H; intros; - try reflexivity; - destruct xs as [|x xs]; - try reflexivity; - eapply IHnull_ope. - - intros H; induction r as [|[|] r]. - + constructor. - + discriminate (H unit [tt]). - + constructor; - eapply IHr; - intros; - destruct xs as [|x xs]. - * apply select_nothing. - * exact (H _ (x :: x :: xs)). -Qed. - -Inductive equiv_ope : ope -> ope -> Prop := -| Equiv_ope_nil : - equiv_ope [] [] -| Equiv_ope_drop_nil {r1} : - equiv_ope r1 [] -> - equiv_ope (false :: r1) [] -| Equiv_ope_nil_drop {r2} : - equiv_ope [] r2 -> - equiv_ope [] (false :: r2) -| Equiv_ope_drop {r1 r2} : - equiv_ope r1 r2 -> - equiv_ope (false :: r1) (false :: r2) -| Equiv_ope_keep {r1 r2} : - equiv_ope r1 r2 -> - equiv_ope (true :: r1) (true :: r2) -. - -Definition ext_equiv_ope (r1 r2 : ope) : Prop := - forall (A : Set) (xs : list A), select r1 xs = select r2 xs. - -Lemma equiv_ope_iff_select {r1 r2} : - equiv_ope r1 r2 <-> ext_equiv_ope r1 r2. -Proof. - unfold ext_equiv_ope; - split. - - intros H; induction H; intros; - try destruct xs; - try reflexivity; - simpl; - try eapply IHequiv_ope; - rewrite IHequiv_ope; - reflexivity. - - revert r2; - induction r1 as [|u1 r1]; - intros r2; - induction r2 as [|u2 r2]; - intros H1. - + constructor. - + destruct u2. - * discriminate (H1 unit [tt]). - * constructor; eapply IHr2; intros; - destruct xs as [|x xs]; - try (simpl; rewrite select_nothing; reflexivity); - exact (H1 _ (x :: x :: xs)). - + destruct u1. - * discriminate (H1 unit [tt]). - * constructor; eapply IHr1; intros; - destruct xs as [|x xs]; - try (simpl; rewrite select_nothing; reflexivity); - exact (H1 _ (x :: x :: xs)). - + destruct u1, u2. - * { constructor; eapply IHr1; intros; - destruct xs as [|x xs]. - - repeat rewrite select_nothing; reflexivity. - - specialize (H1 _ (x :: x :: xs)); - exact (f_equal (@tl _) H1). } - * specialize (H1 unit [tt]); - simpl in H1; - repeat rewrite select_nothing in H1; - discriminate H1. - * specialize (H1 unit [tt]); - simpl in H1; - repeat rewrite select_nothing in H1; - discriminate H1. - * { constructor; eapply IHr1; intros; - destruct xs as [|x xs]. - - repeat rewrite select_nothing; reflexivity. - - exact (H1 _ (x :: x :: xs)). } -Qed. - -Definition equiv_ope_refl {r} : - equiv_ope r r. -Proof. induction r as [|[|] r]; constructor; auto. Defined. - -Definition equiv_ope_sym {r1 r2} : - equiv_ope r1 r2 -> - equiv_ope r2 r1. -Proof. intros H; induction H; constructor; auto. Defined. -Lemma null_ope_iff_equiv_ope_nil_r {r} : null_ope r <-> equiv_ope r []. -Proof. - split; rewrite null_ope_iff_select, equiv_ope_iff_select; auto. -Qed. - -Lemma null_ope_iff_equiv_ope_nil_l {r} : null_ope r <-> equiv_ope [] r. -Proof. - split; rewrite null_ope_iff_select, equiv_ope_iff_select; unfold ext_equiv_ope; simpl; auto. -Qed. - -Fixpoint bnull_ope (r : list bool) : bool := - match r with - | [] => true - | u :: r => if u then false else (bnull_ope r) - end. - -Lemma reflect_bnull_ope {r} : Bool.reflect (null_ope r) (bnull_ope r). -Proof. - induction r as [|[|] r]. - - repeat constructor. - - constructor; intros H; inversion H. - - simpl; destruct IHr. - + repeat constructor; auto. - + repeat constructor; intros H; inversion H; auto. -Qed. - -Fixpoint bequiv_ope (r1 r2 : list bool) {struct r1} : bool := - match (r1, r2) with - | ([], r2) => bnull_ope r2 - | (r1, []) => bnull_ope r1 - | (u1 :: r1, u2 :: r2) => - andb (Bool.eqb u1 u2) (bequiv_ope r1 r2) - end. - -Lemma bequiv_ope_nil_r (r : ope) : bequiv_ope r [] = bnull_ope r. -Proof. induction r as [|[|] r]; eauto. Qed. - -Lemma bnull_ope_sound {r} : - Bool.Is_true (bnull_ope r) -> null_ope r. -Proof. - induction r as [|[] r]; - simpl; - intros H; - try contradiction; - constructor; - auto. -Defined. - -Lemma bnull_ope_complete {r} : - null_ope r -> Bool.Is_true (bnull_ope r). -Proof. intros H; induction H; simpl; auto. Defined. - -Lemma null_ope_implies_equiv_ope_r' {r1 r2} : - null_ope r2 -> r1 = [] -> equiv_ope r1 r2. -Proof. - intros H1; revert r1; induction H1; intros r1 H2; - rewrite H2; constructor; - auto. -Defined. - -Lemma equiv_ope_r_implies_null_ope' {r1 r2} : - equiv_ope r1 r2 -> r1 = [] -> null_ope r2. -Proof. - intros H1; induction H1; intros H2; - try constructor; - try discriminate H2; - auto. -Defined. - -Lemma equiv_ope_l_implies_null_ope' {r1 r2} : - equiv_ope r1 r2 -> r2 = [] -> null_ope r1. -Proof. - intros H1; induction H1; intros H2; - try constructor; - try discriminate H2; - auto. -Defined. - -Lemma null_ope_implies_equiv_ope_l' {r1 r2} : - null_ope r1 -> r2 = [] -> equiv_ope r1 r2. -Proof. - intros H1; revert r2; - induction H1; intros r2 H2; - rewrite H2; constructor; - auto. -Defined. - -Lemma null_ope_implies_equiv_ope_r {r} : - null_ope r -> equiv_ope [] r. -Proof. intros H; eapply null_ope_implies_equiv_ope_r'; auto. Defined. - -Lemma equiv_ope_r_implies_null_ope {r} : - equiv_ope [] r -> null_ope r. -Proof. intros H; eapply equiv_ope_r_implies_null_ope'; eauto. Defined. - -Lemma null_ope_implies_equiv_ope_l {r} : - null_ope r -> equiv_ope r []. -Proof. intros H; eapply null_ope_implies_equiv_ope_l'; auto. Defined. - -Lemma equiv_ope_l_implies_null_ope {r} : - equiv_ope r [] -> null_ope r. -Proof. intros H; eapply equiv_ope_l_implies_null_ope'; eauto. Defined. - -Lemma bequiv_ope_sound {r1 r2} : - Bool.Is_true (bequiv_ope r1 r2) -> equiv_ope r1 r2. -Proof. - revert r2; - induction r1 as [|[] r1]; - intros r2; - simpl; intros H; - try contradiction. - - apply null_ope_implies_equiv_ope_r, bnull_ope_sound; - assumption. - - destruct r2 as [|[] r2]; - simpl in H; - try contradiction; - constructor; - auto. - - destruct r2 as [|[] r2]; - simpl in H; - try contradiction; - constructor; - auto; - eapply null_ope_implies_equiv_ope_l, bnull_ope_sound; - auto. -Defined. - -Lemma bequiv_ope_complete {r1 r2} : - equiv_ope r1 r2 -> Bool.Is_true (bequiv_ope r1 r2). -Proof. - intros H; induction H; simpl in *; - try trivial; - eapply bnull_ope_complete, equiv_ope_l_implies_null_ope; auto. -Defined. - -Lemma is_true_iff {b : bool} : Bool.Is_true b <-> b = true. -Proof. - split. - - destruct b; intros H; try contradiction H; reflexivity. - - intros; subst; constructor. -Defined. - -Lemma reflect_bequiv_ope {r1 r2} : Bool.reflect (equiv_ope r1 r2) (bequiv_ope r1 r2). -Proof. - eapply Bool.iff_reflect; split; intros H. - - eapply bequiv_ope_complete in H; - eapply is_true_iff; - auto. - - eapply is_true_iff in H; - eapply bequiv_ope_sound; - auto. -Defined. - -Fixpoint trim (r : ope) (n : nat) : ope := - match n with - | O => [] - | S n => - match r with - | [] => [] - | u :: r => - u :: trim r (if u then n else S n) - end - end. - -Lemma trim_zero {r : ope} : trim r O = []. -Proof. destruct r; reflexivity. Qed. - -Lemma trim_ok {A : Set} {r : ope} {n : nat} {xs : list A} : - n >= length (select r xs) -> - select (trim r n) xs = select r xs. -Proof. - revert n xs; induction r as [|[] r]; intros [|n] [|x xs] H1; - try reflexivity; - simpl in *; - try (exfalso; lia). - - apply f_equal, IHr; lia. - - destruct (select r xs); try reflexivity; inversion H1. - (* whaat *) - - destruct r as [|[] r]; try reflexivity; - destruct xs as [|x2 xs]; - simpl in *; - try reflexivity. - + eapply f_equal; specialize (IHr (S n) (x2 :: xs) H1); simpl in IHr; inversion IHr; reflexivity. - + specialize (IHr (S n) (x2 :: xs)); simpl in IHr; eapply IHr; eauto. -Qed. - -Lemma trim_weight {r : ope} {n : nat} : - weight (trim r n) <= n. -Proof. - revert n; induction r as [|[] r]; intros [|n]; - try reflexivity; - unfold weight; - simpl; - try lia; - try apply le_n_S; - try apply IHr. -Qed. - -Fixpoint normalize (r : ope) : ope := - match r with - | [] => [] - | false :: r => - match normalize r with - | [] => [] - | r' => false :: r' - end - | true :: r => - true :: normalize r - end. - -Lemma normalize_ok (r : ope) : ext_equiv_ope r (normalize r). -Proof. - unfold ext_equiv_ope; - induction r as [|[] r]; - intros A xs; - destruct xs as [|x xs]; - simpl; - try reflexivity; - try apply f_equal; - try apply IHr; - try (rewrite select_nothing; reflexivity); - destruct (normalize r); - rewrite IHr; reflexivity. -Qed. - -Definition ope_valid (r : ope) (n : nat) := length (normalize r) <= n. - -Lemma length_normalize_trim {A : Set} (r : ope) (xs : list A) : - length (normalize (trim r (length (select r xs)))) <= length xs. -Proof. - revert xs; induction r as [|[] r]; intros [|x xs]; - simpl; try lia. - - eapply le_n_S; auto. - - specialize (IHr xs); - destruct (select r xs) eqn:H; - simpl in *; try lia; - destruct (normalize (trim r (S (length l)))); - simpl in *; lia. -Qed. - -Lemma trim_valid {A : Set} (r : ope) (xs : list A) : - ope_valid (trim r (Datatypes.length (select r xs))) (Datatypes.length xs). -Proof. - unfold ope_valid; (* rewrite width_ok; *) eapply length_normalize_trim. -Qed. - -Lemma repeat_valid (n : nat) : - ope_valid (repeat true n) n. -Proof. - induction n; unfold ope_valid; (* rewrite width_ok; *) simpl; - auto; eapply le_n_S; auto. -Qed. - -(* Finding a fixed point of a function on OPEs by iterating the - function, using the Braga method (see Dominique Larchey-Wendling - and Jean François-Monin, 2020.) - - This is used to "strengthen" Michelson loops in [strengthen_instr] - in compiler.v, doing a kind of data-flow fixed-point analysis. - - [fix_ope] will take a function [f] and starting point [x], and will - iterate [f], taking [x, f x, f (f x)...] until a fixed point is - found: some x' with [equiv_ope (f x') x']. - - First, the domain predicate [fix_ope_dom] picks out [f] and [x] - where this process will terminate: *) -Inductive fix_ope_dom (f : ope -> ope) (x : ope) : Prop := -| Fix_ope_done : - equiv_ope (f x) x -> - fix_ope_dom f x -| Fix_ope_step : - fix_ope_dom f (f x) -> - fix_ope_dom f x -. - -Scheme fix_ope_dom_ind' := Induction for fix_ope_dom Sort Prop. - -(* Helper for when we found a fixed point: *) -Lemma fix_ope_done {f x} : bequiv_ope (f x) x = true -> {y : ope | equiv_ope (f y) y}. -Proof. - intros H1; - exists x; - rewrite <- (Bool.reflect_iff _ _ (@reflect_bequiv_ope (f x) x)) in H1; - exact H1. -Defined. - -(* Inversion lemma as per Braga method: *) -Lemma fix_ope_step_inv {f x} : - bequiv_ope (f x) x = false -> - fix_ope_dom f x -> - fix_ope_dom f (f x). -Proof. - intros H1 H2; inversion H2. - - pose proof (@reflect_bequiv_ope (f x) x) as H3; - rewrite H1 in H3; - inversion H3; - contradiction. - - assumption. -Defined. - -(* Now the Braga magic: Coq believes [fix_ope] is structurally - recursive on the domain predicate *) -Fixpoint fix_ope (f : ope -> ope) (x : ope) (D : fix_ope_dom f x) {struct D} : - {y : ope | equiv_ope (f y) y} := - (if bequiv_ope (f x) x as b return (bequiv_ope (f x) x = b -> {y : ope | equiv_ope (f y) y}) - then fix_ope_done - else fun Hbeq => fix_ope f (f x) (fix_ope_step_inv Hbeq D)) - eq_refl. - -(* Copy of fix_ope generalized over [bequiv_ope (f x) x] with an - equation, to help below. *) -Definition fix_ope' (f : ope -> ope) (x : ope) (D : fix_ope_dom f x) (b : bool) (H : bequiv_ope (f x) x = b) : - {y : ope | equiv_ope (f y) y} := - (if b return (bequiv_ope (f x) x = b -> {y : ope | equiv_ope (f y) y}) - then fix_ope_done - else fun Hbeq => fix_ope f (f x) (fix_ope_step_inv Hbeq D)) - H. - -(* If the function [f] preserves some property of OPEs, then so does - [fix_ope f]. This can be used to prove correctness for code emitted - using a [fix_ope]: prove correctness using [x] and prove that - correctness is preserved by [f], then conclude correctness using - [fix_ope f x]. *) -Lemma fix_ope_preserves (P : ope -> Prop) - {f : ope -> ope} {x : ope} {D : fix_ope_dom f x} : - (forall x, P x -> P (f x)) -> P x -> - P (proj1_sig (fix_ope f x D)). -Proof. - induction D using fix_ope_dom_ind'; - intros H1 H2. - - enough (G : forall b H, P (proj1_sig (fix_ope' f x (Fix_ope_done f x e) b H))) - by (exact (G _ eq_refl)); - intros b H3; - destruct b. - + assumption. - + exfalso; - rewrite (Bool.reflect_iff _ _ (@reflect_bequiv_ope (f x) x)) in e; - rewrite H3 in e; - discriminate e. - - enough (G : forall b H, P (proj1_sig (fix_ope' f x (Fix_ope_step f x D) b H))) - by (exact (G _ eq_refl)); - intros b H3; - destruct b. - + assumption. - + eapply IHD; eauto. -Qed. diff --git a/src/coq/types.v b/src/coq/types.v deleted file mode 100644 index faad21920f..0000000000 --- a/src/coq/types.v +++ /dev/null @@ -1,44 +0,0 @@ -Local Set Warnings "-implicit-core-hint-db". -Set Implicit Arguments. -From Coq Require Import String List. -Import ListNotations. - -(* Inductive D : Prop -> Prop := *) -(* | DD : D (exists P, D P) *) -(* . *) -(* Error: Non strictly positive occurrence of "D" in "D (exists P : Prop, D P)". *) - -(* From ligo_coq Require Import micheline. *) - -Section types. - -Context {A : Set}. - -(* -Local Open Scope string_scope. - -(* This typeclass-like prop accepts types which are suitable arguments for the "iter" Michelson instruction. - class iter_class item iterable - instance a (list a) - instance a (set a) - instance (pair k v) (map k v) *) -Inductive iter_class : node A string -> node A string -> Prop := -| Iter_list {l a n} : iter_class a (Prim l "list" [a] n) -| Iter_set {l a n} : iter_class a (Prim l "set" [a] n) -| Iter_map {l1 l2 k v n1 n2} : iter_class (Prim l1 "pair" [k; v] n1) (Prim l2 "map" [k; v] n2) -. - -(* This typeclass-like prop accepts types which are suitable arguments for the "map" Michelson instruction. - class iter_class item result_item collection result_collection - instance a b (list a) (list b) -- Mapping an (a -> b) function on a (list a) gives a (list b) - instance (pair k v) r (map k v) (map k r) -- Mapping a (k*v -> r) function on a (map k v) gives a (map k r) *) -Inductive map_class : node A string -> node A string -> node A string -> node A string -> Prop := -| Map_list {l1 l2 a b n1 n2} : map_class a b (Prim l1 "list" [a] n1) (Prim l2 "list" [b] n2) -| Map_map {l1 l2 l3 k v r n1 n2 n3} : map_class (Prim l1 "pair" [k; v] n1) r (Prim l2 "map" [k; v] n2) (Prim l3 "map" [k; r] n3) -. - -Hint Constructors iter_class. -Hint Constructors map_class. -*) - -End types. diff --git a/src/coq_ocaml/README.md b/src/coq_ocaml/README.md deleted file mode 100644 index a8663b0eaf..0000000000 --- a/src/coq_ocaml/README.md +++ /dev/null @@ -1,7 +0,0 @@ -This is where Coq code from [src/coq](../coq) is extracted to OCaml. - -(This is in a separate directory only to suppress a warning emitted -when it is placed inside [src/coq](../coq).) - -To get more stuff extracted, mention it in the `Separate Extraction` -command at the bottom of [extraction.v](./extraction.v). diff --git a/src/coq_ocaml/dune b/src/coq_ocaml/dune deleted file mode 100644 index 901c4e1a19..0000000000 --- a/src/coq_ocaml/dune +++ /dev/null @@ -1,23 +0,0 @@ -(library - (name ligo_coq_ocaml) - (public_name ligo.coq_ocaml) - (flags -w "-33-39") - (libraries core zarith octez-libs.micheline sexplib) - (preprocess - (pps ppx_jane))) - -(coq.extraction - (prelude extraction) - (extracted_modules - ;; Coq stuff (hmm) - Datatypes - Bool - Nat - PeanoNat - List - Specif - ;; LIGO /src/coq stuff - ope - compiler) - (theories ligo_coq) - (plugins zarith)) diff --git a/src/coq_ocaml/extraction.v b/src/coq_ocaml/extraction.v deleted file mode 100644 index c158f65857..0000000000 --- a/src/coq_ocaml/extraction.v +++ /dev/null @@ -1,43 +0,0 @@ -(* ZArith stuff below was stolen from Mi-cho-coq: - https://gitlab.com/nomadic-labs/mi-cho-coq/-/blob/eb5a0b469c45472afa87335abee5c1644eb10349/src/michocoq/extraction/extraction.v - *) - -(* Open Source License *) -(* Copyright (c) 2019 Nomadic Labs. *) - -(* Permission is hereby granted, free of charge, to any person obtaining a *) -(* copy of this software and associated documentation files (the "Software"), *) -(* to deal in the Software without restriction, including without limitation *) -(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *) -(* and/or sell copies of the Software, and to permit persons to whom the *) -(* Software is furnished to do so, subject to the following conditions: *) - -(* The above copyright notice and this permission notice shall be included *) -(* in all copies or substantial portions of the Software. *) - -From ligo_coq Require Import compiler ope. -From Coq Require Extraction. -Require ExtrOcamlBasic. -Require ExtrOcamlNativeString. -(* -Require Import ZArith NArith. - -(* Mapping Z to the OCaml library Zarith. *) -Extract Inductive positive => -"Zarith.t" - [ "(fun x -> Zarith.add Zarith.one (Zarith.mul (Zarith.add Zarith.one Zarith.one) x))" "(fun x -> Zarith.mul (Zarith.add Zarith.one Zarith.one) x)" "Zarith.one" ] - "(fun b1 b2 b3 x -> Zarith.(if equal x one then b3 () else let (q, r) = ediv_rem x (of_int 2) in if equal r zero then b2 q else b1 q))". - -Extract Inductive Z => -"Zarith.t" - [ "Zarith.zero" "" "Zarith.neg" ] - "(fun b1 b2 b3 x -> Zarith.(if x > zero then b2 x else if x < zero then b3 x else b1 ()))". - -Extract Inductive N => "Zarith.t" - [ "Zarith.zero" "" ] "(fun b1 b2 x -> Zarith.(if x > zero then b2 x else b1 ()))". -*) - -(* TODO *) -Local Set Warnings "-extraction-logical-axiom". - -Separate Extraction compile_ope compile_expr compile_binds strengthen_prog. diff --git a/src/main/api/common/resolve_config.ml b/src/main/api/common/resolve_config.ml index f146e329ff..67501e0efc 100644 --- a/src/main/api/common/resolve_config.ml +++ b/src/main/api/common/resolve_config.ml @@ -32,7 +32,7 @@ type contract_env = } [@@deriving yojson_of] -type evaluated_michelson = (Mini_c.meta, string) Scoping.Micheline.node +type evaluated_michelson = (Mini_c.meta, string) Tezos_micheline.Micheline.node let yojson_of_evaluated_michelson (em : evaluated_michelson) : Display.json = let open Tezos_utils.Michelson in diff --git a/src/main/compile/dune b/src/main/compile/dune index 41d11007ce..69f79d1e8a 100644 --- a/src/main/compile/dune +++ b/src/main/compile/dune @@ -25,7 +25,6 @@ spilling mini_c self_mini_c - scoping stacking self_michelson aggregation diff --git a/src/main/interpreter/common/interpreter.ml b/src/main/interpreter/common/interpreter.ml index 457f2ab456..e5ce49cac2 100644 --- a/src/main/interpreter/common/interpreter.ml +++ b/src/main/interpreter/common/interpreter.ml @@ -1849,12 +1849,11 @@ and eval_ligo ~(raise : _ Trace.raise) ~steps ~options let* v = eval_ligo e calltrace env in return ( v - , Stacking.To_micheline.translate_type - (Scoping.translate_type - (Trace.trace ~raise Main_errors.spilling_tracer - @@ Spilling.compile_type - @@ Trace.trace ~raise Main_errors.expansion_tracer - @@ Expansion.compile_type_expression e.type_expression)) )) + , Ligo_compile.Of_mini_c.compile_type + (Trace.trace ~raise Main_errors.spilling_tracer + @@ Spilling.compile_type + @@ Trace.trace ~raise Main_errors.expansion_tracer + @@ Expansion.compile_type_expression e.type_expression) )) args in (match code.expression_content with diff --git a/src/main/main_errors/dune b/src/main/main_errors/dune index 89d1afd3d6..598a9d4620 100644 --- a/src/main/main_errors/dune +++ b/src/main/main_errors/dune @@ -19,7 +19,6 @@ spilling self_ast_aggregated self_mini_c - scoping stacking self_michelson) (preprocess diff --git a/src/main/main_errors/formatter.ml b/src/main/main_errors/formatter.ml index 7e36509a3c..96c2f41bfb 100644 --- a/src/main/main_errors/formatter.ml +++ b/src/main/main_errors/formatter.ml @@ -379,7 +379,6 @@ let rec error_ppformat | `Self_mini_c_tracer e -> Self_mini_c.Errors.error_ppformat ~display_format ~no_colour f e | `Spilling_tracer e -> Spilling.Errors.error_ppformat ~display_format ~no_colour f e - | `Scoping_tracer e -> Scoping.Errors.error_ppformat ~display_format f e | `Stacking_tracer e -> Stacking.Errors.error_ppformat ~display_format f e | `Main_interpret_not_enough_initial_accounts (loc, max) -> Format.fprintf @@ -777,7 +776,6 @@ let rec error_json : Types.all -> Ligo_Error.t list = | `Expansion_tracer e -> [ Expansion.Errors.error_json e ] | `Spilling_tracer e -> [ Spilling.Errors.error_json e ] | `Self_mini_c_tracer e -> [ Self_mini_c.Errors.error_json e ] - | `Scoping_tracer e -> [ Scoping.Errors.error_json e ] | `Stacking_tracer e -> [ Stacking.Errors.error_json e ] | `Main_interpret_test_entry_not_found _ | `Main_interpret_target_lang_error _ diff --git a/src/main/main_errors/types.ml b/src/main/main_errors/types.ml index 49a5e81705..c454f5fb8d 100644 --- a/src/main/main_errors/types.ml +++ b/src/main/main_errors/types.ml @@ -42,7 +42,6 @@ type all = | `Expansion_tracer of Expansion.Errors.expansion_error | `Spilling_tracer of Spilling.Errors.spilling_error | `Self_mini_c_tracer of Self_mini_c.Errors.self_mini_c_error - | `Scoping_tracer of Scoping.Errors.scoping_error | `Stacking_tracer of Stacking.Errors.stacking_error | `Ligo_init_unrecognized_template of string list | `Ligo_init_registry_template_error of string diff --git a/src/passes/16-scoping/dune b/src/passes/16-scoping/dune deleted file mode 100644 index 2d15fa2734..0000000000 --- a/src/passes/16-scoping/dune +++ /dev/null @@ -1,8 +0,0 @@ -(library - (name scoping) - (public_name ligo.scoping) - (instrumentation - (backend bisect_ppx)) - (libraries simple-utils ligo_prim mini_c predefined ligo_coq_ocaml) - (preprocess - (pps ppx_poly_constructor))) diff --git a/src/passes/16-scoping/errors.ml b/src/passes/16-scoping/errors.ml deleted file mode 100644 index 5026b0da12..0000000000 --- a/src/passes/16-scoping/errors.ml +++ /dev/null @@ -1,123 +0,0 @@ -module Michelson = Tezos_utils.Michelson -open Ligo_prim -module Display = Simple_utils.Display -module Ligo_Error = Simple_utils.Error - -type scoping_error = - [ `Scoping_corner_case of string * string - | `Scoping_contract_entrypoint of string - | `Scoping_bad_iterator of Constant.constant' - | `Scoping_not_comparable_pair_struct - | `Scoping_could_not_tokenize_michelson of string - | `Scoping_could_not_parse_michelson of string - | `Scoping_untranspilable of int Michelson.t * int Michelson.t - | `Scoping_unsupported_primitive of Constant.constant' - ] -[@@deriving poly_constructor { prefix = "scoping_" }] - -let stage = "scoping" - -let corner_case_msg () = - "Sorry, we don't have a proper error message for this error. Please report this use \ - case so we can improve on this." - - -let error_ppformat - : display_format:string Display.display_format -> Format.formatter -> scoping_error - -> unit - = - fun ~display_format f a -> - match display_format with - | Human_readable | Dev -> - (match a with - | `Scoping_unsupported_primitive c -> - Format.fprintf f "@[unsupported primitive %a@]" Constant.pp_constant' c - | `Scoping_corner_case (loc, msg) -> - let s = - Format.asprintf "Scoping corner case at %s : %s.\n%s" loc msg (corner_case_msg ()) - in - Format.pp_print_string f s - | `Scoping_contract_entrypoint loc -> - let s = - Format.asprintf "contract entrypoint must be given as a literal string: %s" loc - in - Format.pp_print_string f s - | `Scoping_bad_iterator cst -> - let s = Format.asprintf "bad iterator: iter %a" Mini_c.PP.constant cst in - Format.pp_print_string f s - | `Scoping_not_comparable_pair_struct -> - let s = - "Invalid comparable value. When using a tuple with more than 2 components, \ - structure the tuple like this: \"(a, (b, c))\". " - in - Format.pp_print_string f s - | `Scoping_could_not_tokenize_michelson code -> - Format.fprintf f "Could not tokenize raw Michelson: %s" code - | `Scoping_could_not_parse_michelson code -> - Format.fprintf f "Could not parse raw Michelson: %s" code - | `Scoping_untranspilable (ty, value) -> - Format.fprintf - f - "Could not untranspile Michelson value: %a %a" - Michelson.pp - ty - Michelson.pp - value) - - -let error_json : scoping_error -> Ligo_Error.t = - fun e -> - let open Ligo_Error in - match e with - | `Scoping_unsupported_primitive c -> - let message = - Format.asprintf "@[unsupported primitive %a@]" Constant.pp_constant' c - in - let content = make_content ~message () in - make ~stage ~content - | `Scoping_corner_case (location, msg) -> - let message = - Format.asprintf - "Scoping corner case at %s : %s.\n%s" - location - msg - (corner_case_msg ()) - in - let content = make_content ~message () in - make ~stage ~content - | `Scoping_contract_entrypoint loc -> - let message = - Format.asprintf "contract entrypoint must be given as a literal string: %s" loc - in - let content = make_content ~message () in - make ~stage ~content - | `Scoping_bad_iterator cst -> - let message = Format.asprintf "bad iterator: iter %a" Mini_c.PP.constant cst in - let content = make_content ~message () in - make ~stage ~content - | `Scoping_not_comparable_pair_struct -> - let message = - "Invalid comparable value. When using a tuple with more than 2 components, \ - structure the tuple like this: \"(a, (b, c))\". " - in - let content = make_content ~message () in - make ~stage ~content - | `Scoping_could_not_tokenize_michelson code -> - let message = Format.asprintf "Could not tokenize raw Michelson: %s" code in - let content = make_content ~message () in - make ~stage ~content - | `Scoping_could_not_parse_michelson code -> - let message = Format.asprintf "Could not parse raw Michelson: %s" code in - let content = make_content ~message () in - make ~stage ~content - | `Scoping_untranspilable (ty, value) -> - let message = - Format.asprintf - "Could not untranspile Michelson value: %a %a" - Michelson.pp - ty - Michelson.pp - value - in - let content = make_content ~message () in - make ~stage ~content diff --git a/src/passes/16-scoping/scoping.ml b/src/passes/16-scoping/scoping.ml deleted file mode 100644 index 0c2195a217..0000000000 --- a/src/passes/16-scoping/scoping.ml +++ /dev/null @@ -1,605 +0,0 @@ -module I = Mini_c -module O = Ligo_coq_ocaml.Compiler -module Micheline = Tezos_micheline.Micheline -module Trace = Simple_utils.Trace -module Location = Simple_utils.Location -module Ligo_string = Simple_utils.Ligo_string -module Ligo_option = Simple_utils.Ligo_option -module Var = Ligo_prim.Value_var -module Errors = Errors - -type meta = Mini_c.meta -type binder_meta = Mini_c.binder_meta - -(* We should use this less: *) -let nil : meta = - { location = Location.generated - ; env = [] - ; binder = None - ; source_type = None - ; application = None - } - - -type base_type = (meta, string) Micheline.node -type oty = (meta, base_type) O.ty - -let binder_meta (var : Var.t option) (source_type : I.type_expression) - : binder_meta option - = - Option.map var ~f:(fun var : binder_meta -> - { location = Var.get_location var - ; name = (if Var.is_generated var then None else Some (Var.to_name_exn var)) - ; source_type = source_type.source_type - }) - - -(* Next stage uses Micheline for its types: *) -let rec translate_type ?var : I.type_expression -> oty = - fun a -> - let nil : meta = - { location = Location.generated - ; env = [] - ; binder = binder_meta var a - ; source_type = None - ; application = None - } - in - match a.type_content with - | I.T_tuple ts -> tuple_comb nil ts - | I.T_or ((ann1, a1), (ann2, a2)) -> - O.T_or (nil, ann1, ann2, translate_type a1, translate_type a2) - | I.T_function (a1, a2) -> O.T_func (nil, translate_type a1, translate_type a2) - | I.T_base I.TB_unit -> T_base (nil, Prim (nil, "unit", [], [])) - | I.T_base I.TB_bool -> T_base (nil, Prim (nil, "bool", [], [])) - | I.T_base I.TB_string -> T_base (nil, Prim (nil, "string", [], [])) - | I.T_base I.TB_bytes -> T_base (nil, Prim (nil, "bytes", [], [])) - | I.T_base I.TB_nat -> T_base (nil, Prim (nil, "nat", [], [])) - | I.T_base I.TB_int -> T_base (nil, Prim (nil, "int", [], [])) - | I.T_base I.TB_mutez -> T_base (nil, Prim (nil, "mutez", [], [])) - | I.T_base I.TB_operation -> T_base (nil, Prim (nil, "operation", [], [])) - | I.T_base I.TB_address -> T_base (nil, Prim (nil, "address", [], [])) - | I.T_base I.TB_key -> T_base (nil, Prim (nil, "key", [], [])) - | I.T_base I.TB_key_hash -> T_base (nil, Prim (nil, "key_hash", [], [])) - | I.T_base I.TB_chain_id -> T_base (nil, Prim (nil, "chain_id", [], [])) - | I.T_base I.TB_signature -> T_base (nil, Prim (nil, "signature", [], [])) - | I.T_base I.TB_timestamp -> T_base (nil, Prim (nil, "timestamp", [], [])) - | I.T_base I.TB_baker_hash -> T_base (nil, Prim (nil, "baker_hash", [], [])) - | I.T_base I.TB_pvss_key -> T_base (nil, Prim (nil, "pvss_key", [], [])) - | I.T_base I.TB_baker_operation -> T_base (nil, Prim (nil, "baker_operation", [], [])) - | I.T_base I.TB_bls12_381_g1 -> T_base (nil, Prim (nil, "bls12_381_g1", [], [])) - | I.T_base I.TB_bls12_381_g2 -> T_base (nil, Prim (nil, "bls12_381_g2", [], [])) - | I.T_base I.TB_bls12_381_fr -> T_base (nil, Prim (nil, "bls12_381_fr", [], [])) - | I.T_base I.TB_never -> T_base (nil, Prim (nil, "never", [], [])) - | I.T_base I.TB_tx_rollup_l2_address -> - T_base (nil, Prim (nil, "tx_rollup_l2_address", [], [])) - | I.T_base (I.TB_type_int memo_size) -> T_base (nil, Int (nil, memo_size)) - | I.T_base I.TB_chest -> T_base (nil, Prim (nil, "chest", [], [])) - | I.T_base I.TB_chest_key -> T_base (nil, Prim (nil, "chest_key", [], [])) - | I.T_ticket x -> T_ticket (nil, translate_type x) - | I.T_sapling_transaction memo_size -> - T_base (nil, Prim (nil, "sapling_transaction", [ Int (nil, memo_size) ], [])) - | I.T_sapling_state memo_size -> - T_base (nil, Prim (nil, "sapling_state", [ Int (nil, memo_size) ], [])) - | I.T_map (a1, a2) -> T_map (nil, translate_type a1, translate_type a2) - | I.T_big_map (a1, a2) -> T_big_map (nil, translate_type a1, translate_type a2) - | I.T_list a -> T_list (nil, translate_type a) - | I.T_set a -> T_set (nil, translate_type a) - | I.T_contract a -> T_contract (nil, translate_type a) - | I.T_option a -> T_option (nil, translate_type a) - - -(* could consider delaying this to the next pass, in Coq, but - currently the Coq pass type translation is the identity *) -and tuple_comb_ann nil ts = - match ts with - | [] -> None, O.T_unit nil - | [ (ann, t) ] -> ann, translate_type t - | (ann1, t1) :: ts -> - let t1 = translate_type t1 in - let ann, ts = tuple_comb_ann nil ts in - None, O.T_pair (nil, ann1, ann, t1, ts) - - -and tuple_comb nil ts = snd (tuple_comb_ann nil ts) - -let rec int_to_nat (x : int) : Ligo_coq_ocaml.Datatypes.nat = - if x <= 0 then O else S (int_to_nat (x - 1)) - - -let translate_var (x : I.var_name) (env : I.environment) = - let _, idx = - match I.Environment.Environment.get_i_opt x env with - | Some v -> v - | None -> - failwith - @@ Format.asprintf "Corner case: %a not found in env" Ligo_prim.Value_var.pp x - in - int_to_nat idx - - -(* probably should use result monad for conformity? but all errors - here are supposed to be impossible, under the assumption that the - input program is well-typed *) -let internal_error loc msg = - failwith - (Format.asprintf - "@[Internal error, please report this as a bug@ %s@ %s@ @]" - loc - msg) - - -let extract_applications (expr : I.expression) (env : I.environment) - : I.application_meta option - = - match expr.type_expression.source_type, expr.content with - (* If an expression is a function and it's an application - then we're interested in it *) - | Some { type_content = T_arrow _; _ }, E_application (f, args) -> - let applied_function = - match f.content with - | E_variable var_name | E_deref var_name -> Some var_name - | _ -> None - in - let args = - (* After uncurrying in self_mini_c some applications - are changed from `f a b c` to `f (a, b, c)`. - We can differ them by location - (location for uncurried tuple would be generated) *) - if Location.is_dummy_or_generated args.location - then ( - match args.content with - | E_tuple args -> args - | _ -> [ args ]) - else [ args ] - in - let to_applied_argument (expr : I.expression) : I.applied_argument = - match expr.content with - | E_variable var | E_deref var -> - let orig_var = - (* We want to have a location of binded variable *) - Option.value ~default:var (I.Environment.Environment.get_var_opt var env) - in - Var orig_var - | _ -> Expression_location expr.location - in - let arguments = - List.map args ~f:(fun expr -> - expr.type_expression.source_type, to_applied_argument expr) - in - Some { I.applied_function; I.arguments } - | _ -> None - - -(* The translation. Given an expression in an environment, returns a - "co-de Bruijn" expression with an embedding (`list usage`) showing - which things in the environment were used. *) - -(* Let |-I and |-O be the input and output typing judgments. If - env |-I expr : a, and translate_expression expr env = (expr', us), then - select us env |-O expr' : a. *) -let rec translate_expression ~raise (expr : I.expression) (env : I.environment) - : (meta, base_type, Ligo_prim.Literal_value.t, (meta, string) Micheline.node) O.expr - = - let meta : meta = - { location = expr.location - ; env = [] - ; binder = None - ; source_type = expr.type_expression.source_type - ; application = extract_applications expr env - } - in - let ty = expr.type_expression in - let translate_expression = translate_expression ~raise in - let translate_args = translate_args ~raise in - let translate_binder = translate_binder ~raise in - let translate_binder2 = translate_binder2 ~raise in - let translate_binderN = translate_binderN ~raise in - match expr.content with - | E_literal lit -> O.E_literal (meta, lit) - | E_variable x -> E_var (meta, translate_var x env) - | E_closure { binder; body } -> - let binder_type, return_type = - (* TODO move binder type to the binder, like all other binders? *) - (* at the moment, this is the only error here! so I am not - bothering with error machinery... *) - match Mini_c.get_t_function expr.type_expression with - | None -> internal_error __LOC__ "type of lambda is not a function type" - | Some t -> t - in - let binder = binder, binder_type in - let binder = translate_binder (binder, body) env in - O.E_lam (meta, binder, translate_type return_type) - | E_rec { rec_binder; func = { binder; body } } -> - let binder_type, return_type = - (* TODO move binder type to the binder, like all other binders? *) - (* at the moment, this is the only error here! so I am not - bothering with error machinery... *) - match Mini_c.get_t_function expr.type_expression with - | None -> internal_error __LOC__ "type of lambda is not a function type" - | Some t -> t - in - let binder = binder, binder_type in - let rec_binder = rec_binder, expr.type_expression in - let binder = translate_binder2 ((binder, rec_binder), body) env in - O.E_rec (meta, binder, translate_type return_type) - | E_constant constant -> - let mich, args = translate_constant ~raise meta constant expr.type_expression env in - O.E_inline_michelson (meta, mich, args) - | E_application (f, x) -> - let args = translate_args [ f; x ] env in - E_app (meta, args) - | E_iterator (name, body, expr) -> - let body = translate_binder body env in - let expr = translate_expression expr env in - (match name with - | C_ITER -> O.E_iter (meta, body, expr) - | C_MAP -> O.E_map (meta, body, expr) - | C_LOOP_LEFT -> - let b = translate_type ty in - O.E_loop_left (meta, body, b, expr) - | _ -> internal_error __LOC__ "invalid iterator constant") - | E_fold (body, coll, init) -> - let body = translate_binder body env in - let coll = translate_expression coll env in - let init = translate_expression init env in - O.E_fold (meta, init, coll, body) - | E_fold_right (body, (coll, elem_type), init) -> - let elem_type = translate_type elem_type in - let body = translate_binder body env in - let coll = translate_expression coll env in - let init = translate_expression init env in - E_fold_right (meta, elem_type, init, coll, body) - | E_if_bool (e1, e2, e3) -> - let e1 = translate_expression e1 env in - let e2 = translate_expression e2 env in - let e3 = translate_expression e3 env in - E_if_bool (meta, e1, e2, e3) - | E_if_none (e1, e2, e3) -> - let e1 = translate_expression e1 env in - let e2 = translate_expression e2 env in - let e3 = translate_binder e3 env in - E_if_none (meta, e1, e2, e3) - (* NB: flipping around because it is backwards in Mini_c *) - | E_if_cons (e1, e3, e2) -> - let e1 = translate_expression e1 env in - let e2 = translate_binder2 e2 env in - let e3 = translate_expression e3 env in - E_if_cons (meta, e1, e2, e3) - | E_if_left (e1, e2, e3) -> - let e1 = translate_expression e1 env in - let e2 = translate_binder e2 env in - let e3 = translate_binder e3 env in - E_if_left (meta, e1, e2, e3) - | E_let_in (e1, _inline, e2) -> - let e1 = translate_expression e1 env in - let e2 = translate_binder e2 env in - E_let_in (meta, e1, e2) - | E_tuple exprs -> - let exprs = translate_args exprs env in - E_tuple (meta, exprs) - | E_let_tuple (e1, e2) -> - let e1 = translate_expression e1 env in - let e2 = translate_binderN e2 env in - E_let_tuple (meta, e1, e2) - | E_proj (e, i, n) -> - let e = translate_expression e env in - E_proj (meta, e, int_to_nat i, int_to_nat n) - | E_update (e1, i, e2, n) -> - let args = translate_args [ e2; e1 ] env in - E_update (meta, args, int_to_nat i, int_to_nat n) - | E_raw_michelson code -> - (* maybe should move type into syntax? *) - let a, b = - match Mini_c.get_t_function ty with - | None -> - internal_error - __LOC__ - (Format.asprintf - "type of Michelson insertion ([%%Michelson ...]) is not a function type = %a" - Mini_c.PP.type_expression - ty) - | Some (a, b) -> a, b - in - let wipe_locations l e = - Tezos_micheline.Micheline.(inject_locations (fun _ -> l) (strip_locations e)) - in - let code = List.map ~f:(wipe_locations nil) code in - E_raw_michelson (meta, translate_type a, translate_type b, code) - | E_inline_michelson (code, args') -> - let args = - List.map - ~f:(fun e -> - ( translate_expression e env - , Stacking.To_micheline.translate_type (translate_type e.type_expression) )) - args' - in - let wipe_locations l e = - Tezos_micheline.Micheline.(inject_locations (fun _ -> l) (strip_locations e)) - in - let code = List.map ~f:(wipe_locations nil) code in - let used = ref [] in - let replace m = - let open Tezos_micheline.Micheline in - match m with - | Prim (_, s, [], [ id ]) - when String.equal "typeopt" s && String.is_prefix ~prefix:"$" id -> - let id = String.chop_prefix_exn ~prefix:"$" id in - let id = Int.of_string id in - used := id :: !used; - (match List.nth args id with - | Some (_, Prim (_, "option", [ t ], _)) -> t - | _ -> internal_error __LOC__ (Format.sprintf "could not resolve (typeopt %d)" id)) - | Prim (_, s, [], [ id ]) - when String.equal "type" s && String.is_prefix ~prefix:"$" id -> - let id = String.chop_prefix_exn ~prefix:"$" id in - let id = Int.of_string id in - used := id :: !used; - (match List.nth args id with - | None -> internal_error __LOC__ (Format.sprintf "could not resolve (type %d)" id) - | Some (_, t) -> t) - | Prim (_, s, [], [ id ]) - when String.equal "litstr" s && String.is_prefix ~prefix:"$" id -> - let id = String.chop_prefix_exn ~prefix:"$" id in - let id = Int.of_string id in - used := id :: !used; - (match List.nth args id with - | Some (E_literal (m, Literal_string s), _) -> String (m, Ligo_string.extract s) - | _ -> internal_error __LOC__ (Format.sprintf "could not resolve (litstr %d)" id)) - | Prim (_, s, [], [ id ]) - when String.equal "codestr" s && String.is_prefix ~prefix:"$" id -> - let id = String.chop_prefix_exn ~prefix:"$" id in - let id = Int.of_string id in - used := id :: !used; - (match List.nth args id with - | Some (E_literal (m, Literal_string s), _) -> - let open Tezos_micheline in - let code = Ligo_string.extract s in - let code, errs = Micheline_parser.tokenize code in - (match errs with - | _ :: _ -> - internal_error __LOC__ (Format.sprintf "could not parse raw michelson") - | [] -> - let code, errs = Micheline_parser.parse_expression ~check:false code in - (match errs with - | _ :: _ -> - internal_error __LOC__ (Format.sprintf "could not parse raw michelson") - | [] -> - let code = Micheline.strip_locations code in - (* hmm *) - let code = Micheline.inject_locations (fun _ -> Location.generated) code in - map_node (fun _ -> m) (fun x -> x) code)) - | _ -> internal_error __LOC__ (Format.sprintf "could not resolve (litstr %d)" id)) - | Prim (a, b, c, d) -> - let open Tezos_micheline.Micheline in - let f arg (c, d) = - match arg with - | Prim (_, s, [], [ id ]) - when String.equal "annot" s && String.is_prefix ~prefix:"$" id -> - let id = String.chop_prefix_exn ~prefix:"$" id in - let id = Int.of_string id in - used := id :: !used; - let annot = - match List.nth args id with - | Some (E_literal (_, Literal_string s), _) -> Ligo_string.extract s - | _ -> - internal_error __LOC__ (Format.sprintf "could not resolve (annot %d)" id) - in - c, annot :: d - | m -> m :: c, d - in - let c, d = List.fold_right ~f ~init:([], d) c in - Prim (a, b, c, d) - | m -> m - in - let code = List.map ~f:(Tezos_utils.Michelson.map replace) code in - let args' = - List.filter_mapi - ~f:(fun i v -> - if not (List.mem !used i ~equal:Stdlib.( = )) then Some v else None) - args' - in - let args' = translate_args args' env in - E_inline_michelson (meta, code, args') - | E_global_constant (hash, args) -> - let args = translate_args args env in - let output_ty = translate_type ty in - E_global_constant (meta, output_ty, hash, args) - | E_create_contract (p, s, code, args) -> - let p = translate_type p in - let s = translate_type s in - let code = translate_binder code [] in - let args = translate_args args env in - E_create_contract (meta, p, s, code, args) - | E_let_mut_in (e1, e2) -> - let e1 = translate_expression e1 env in - let e2 = translate_binder e2 env in - E_let_mut_in (meta, e1, e2) - | E_deref x -> E_deref (meta, translate_var x env) - | E_assign (x, e) -> - let x = translate_var x env in - let e = translate_expression e env in - E_assign (meta, x, e) - | E_for (start, final, incr, body) -> - let args = translate_args [ start; final; incr ] env in - let body = translate_binder body env in - E_for (meta, args, body) - | E_for_each (coll, _coll_type, body) -> - let coll = translate_expression coll env in - let body = translate_binderN body env in - E_for_each (meta, coll, body) - | E_while (cond, body) -> - let cond = translate_expression cond env in - let body = translate_expression body env in - E_while (meta, cond, body) - - -and translate_binder ~raise (binder, body) env = - let env' = I.Environment.add binder env in - let body = translate_expression ~raise body env' in - let binder, binder_type = binder in - O.Binds (nil, [ translate_type ~var:binder binder_type ], body) - - -and translate_binder2 ~raise ((binder1, binder2), body) env = - let env' = I.Environment.add binder1 (I.Environment.add binder2 env) in - let body = translate_expression ~raise body env' in - let binder1, binder1_type = binder1 in - let binder2, binder2_type = binder2 in - O.Binds - ( nil - , [ translate_type ~var:binder1 binder1_type - ; translate_type ~var:binder2 binder2_type - ] - , body ) - - -and translate_binderN ~raise (vars, body) env = - let env' = List.fold_right ~f:I.Environment.add vars ~init:env in - let body = translate_expression ~raise body env' in - O.Binds (nil, List.map ~f:(fun (var, ty) -> translate_type ~var ty) vars, body) - - -and translate_args ~raise (arguments : I.expression list) env : _ O.args = - let arguments = List.rev arguments in - let arguments = - List.map ~f:(fun argument -> translate_expression ~raise argument env) arguments - in - List.fold_right - ~f:(fun arg args -> O.Args_cons (nil, arg, args)) - arguments - ~init:(O.Args_nil nil) - - -and translate_constant - ~(raise : _ Trace.raise) - (meta : meta) - (expr : I.constant) - (ty : I.type_expression) - env - : _ Micheline.node list * _ O.args - = - let module Let_syntax = struct - let bind : 'a option -> f:('a -> 'b option) -> 'b option = - fun x ~f -> - match x with - | Some x -> f x - | None -> None - end - in - let ( let* ) x f = Let_syntax.bind ~f x in - (* Here we will handle some special predefined operators which take - some "static args". These are mostly types from the typing - judgment, but also annotations (for SELF, CONTRACT) or scripts - (for CREATE_CONTRACT.) - - First we translate any static args and return the rest of the - non-static arguments, if any: *) - let translate_type t = Stacking.To_micheline.translate_type (translate_type t) in - let translate_args = translate_args ~raise in - (* This is for compatibility with the existing stuff in - Predefined.Michelson and below. I believe this stuff should be - simplified away but don't want to do it right now. *) - let module O = struct - type static_args = Type_args of string option * (meta, string) Micheline.node list - - let apply_static_args : string -> static_args -> _ Micheline.node = - fun prim args -> - match args with - | Type_args (annot, types) -> Prim (nil, prim, types, Option.to_list annot) - - - let wipe_locations l e = - Tezos_micheline.Micheline.(inject_locations (fun _ -> l) (strip_locations e)) - end - in - let open O in - let special : (static_args * I.expression list) option = - let return (x : static_args * I.expression list) : _ = Some x in - match expr.cons_name with - | C_GLOBAL_CONSTANT -> - (match expr.arguments with - | { content = E_literal (Literal_string hash); type_expression = _; _ } :: arguments - -> - let hash = Ligo_string.extract hash in - return - ( Type_args - ( None - , [ translate_type ty; Prim (nil, "constant", [ String (nil, hash) ], []) ] - ) - , arguments ) - | _ -> None) - | C_NONE -> - let* a = Mini_c.get_t_option ty in - return (Type_args (None, [ translate_type a ]), expr.arguments) - | C_NIL | C_LIST_EMPTY -> - let* a = Mini_c.get_t_list ty in - return (Type_args (None, [ translate_type a ]), expr.arguments) - | C_LOOP_CONTINUE | C_LEFT -> - let b = - match ty.type_content with - | T_or (_, (_, b)) -> b - | _ -> failwith (Format.asprintf "WRONG TYPE %a\n%!" Mini_c.PP.type_expression ty) - in - (* let* (_, b) = Mini_c.get_t_or ty in *) - return (Type_args (None, [ translate_type b ]), expr.arguments) - | C_LOOP_STOP | C_RIGHT -> - let* a, _ = Mini_c.get_t_or ty in - return (Type_args (None, [ translate_type a ]), expr.arguments) - | C_SET_EMPTY -> - let* a = Mini_c.get_t_set ty in - return (Type_args (None, [ translate_type a ]), expr.arguments) - | C_MAP_EMPTY | C_BIG_MAP_EMPTY -> - let* a, b = Ligo_option.(map_pair_or (Mini_c.get_t_map, Mini_c.get_t_big_map) ty) in - return (Type_args (None, [ translate_type a; translate_type b ]), expr.arguments) - | C_MAP_REMOVE -> - let* _, b = Ligo_option.(map_pair_or (Mini_c.get_t_map, Mini_c.get_t_big_map) ty) in - return (Type_args (None, [ translate_type b ]), expr.arguments) - (* TODO handle CREATE_CONTRACT sooner *) - (* | C_CREATE_CONTRACT -> *) - (* (match expr.arguments with *) - (* | { content= E_closure body ; type_expression = closure_ty ; location =_ } :: arguments -> *) - (* let* (input_ty, _) = Mini_c.get_t_function closure_ty in *) - (* let* (p, s) = Mini_c.get_t_pair input_ty in *) - (* let body = translate_closed_function ~raise ~proto body input_ty in *) - (* return (Script_arg (O.Script (translate_type p, translate_type s, body)), arguments) *) - (* | _ -> None) *) - | _ -> None - in - (* Either we got static args, or none: *) - let static_args = - match special with - | Some (static_args, _) -> static_args - | None -> O.Type_args (None, []) - in - (* Remaining/all non-static args: *) - let arguments = - match special with - | Some (_, arguments) -> arguments - | None -> expr.arguments - in - let arguments = translate_args arguments env in - match Predefined.Michelson.get_operators expr.cons_name with - | Some x -> - ( [ (* Handle predefined (and possibly special) operators, applying - any type/annot/script args using apply_static_args. *) - Predefined.Michelson.unpredicate - meta - (fun prim -> wipe_locations () (apply_static_args prim static_args)) - x - ] - , arguments ) - | None -> raise.error (Errors.unsupported_primitive expr.cons_name) - - -and translate_closed_function - ~raise - ?(env = []) - ({ binder; body } : I.anon_function) - input_ty - : _ O.binds - = - let body = - translate_expression ~raise body (Mini_c.Environment.add (binder, input_ty) env) - in - Binds (nil, [ translate_type input_ty ], body) diff --git a/src/passes/17-stacking/compiler_program.ml b/src/passes/17-stacking/compiler_program.ml index dc4af7c05b..f6eb97efd0 100644 --- a/src/passes/17-stacking/compiler_program.ml +++ b/src/passes/17-stacking/compiler_program.ml @@ -7,102 +7,3 @@ type compiled_expression = { expr_ty : (meta, string) node ; expr : (meta, string) node } - -let null = Mini_c.dummy_meta -let rec repeat x n = if n <= 0 then [] else x :: repeat x (n - 1) - -type base_type = (meta, string) Tezos_micheline.Micheline.node -type oty = (meta, base_type) Ligo_coq_ocaml.Compiler.ty - -let get_ty_meta : oty -> meta = - fun x -> - match x with - | T_base (meta, _) -> meta - | T_unit meta -> meta - | T_pair (meta, _, _, _, _) -> meta - | T_or (meta, _, _, _, _) -> meta - | T_func (meta, _, _) -> meta - | T_lambda (meta, _, _) -> meta - | T_option (meta, _) -> meta - | T_list (meta, _) -> meta - | T_set (meta, _) -> meta - | T_map (meta, _, _) -> meta - | T_big_map (meta, _, _) -> meta - | T_ticket (meta, _) -> meta - | T_contract (meta, _) -> meta - | T_bool meta -> meta - | T_int meta -> meta - | T_nat meta -> meta - | T_mutez meta -> meta - | T_string meta -> meta - | T_bytes meta -> meta - | T_address meta -> meta - | T_key_hash meta -> meta - | T_operation meta -> meta - - -(* returns a list `ret` such that `select r ret = env` by inserting - None entries, probably should do this in Coq instead but - whatever *) -let rec unselect (r : bool list) (env : 'a option list) : 'a option list = - match r with - | [] -> [] - | false :: r -> None :: unselect r env - | true :: r -> - (match env with - | [] -> None :: unselect r [] - | x :: env -> x :: unselect r env) - - -let with_var_names (r : bool list) (env : oty list) (m : meta) : meta = - { m with env = unselect r (List.map ~f:(fun ty -> (get_ty_meta ty).binder) env) } - - -let compile_binds env expr = - Ligo_coq_ocaml.Compiler.compile_binds - null - with_var_names - To_micheline.literal_code - To_micheline.global_constant - (repeat true (List.length env)) - env - expr - - -let compile_expr env expr = - Ligo_coq_ocaml.Compiler.compile_expr - null - with_var_names - To_micheline.literal_code - To_micheline.global_constant - (repeat true (List.length env)) - env - expr - - -let compile_expr env e = - let open Lwt.Let_syntax in - let p = compile_expr env e in - let rs, p = To_micheline.strengthen_prog p [ true ] in - (* TODO *) - let () = - if List.length (List.filter ~f:Fn.id rs) > 0 - then failwith "TODO expr used something" - else () - in - (* hmm, why did this end up here *) - let drops = Ligo_coq_ocaml.Compiler.compile_ope null rs in - let%bind drops = To_micheline.translate_prog drops in - let%map p = To_micheline.translate_prog p in - Seq (null, drops @ p) - - -let compile_function_body e = - let open Lwt.Let_syntax in - let p = compile_binds [] e in - let rs, p = To_micheline.strengthen_prog p [ true ] in - let%map p = To_micheline.translate_prog p in - (* hmm, why did this end up here *) - if Option.value ~default:false (List.hd rs) - then Seq (null, p) - else Seq (null, Prim (null, "DROP", [], []) :: p) diff --git a/src/passes/17-stacking/compiler_program.mli b/src/passes/17-stacking/compiler_program.mli index 50ab73bb8b..6057256e5e 100644 --- a/src/passes/17-stacking/compiler_program.mli +++ b/src/passes/17-stacking/compiler_program.mli @@ -1,4 +1,3 @@ -open Ligo_prim open Tezos_micheline.Micheline type meta = Mini_c.meta @@ -7,17 +6,3 @@ type compiled_expression = { expr_ty : (meta, string) node ; expr : (meta, string) node } - -open Ligo_coq_ocaml.Compiler - -(* TODO ugh *) -(* type ('meta, 'base_type, 'op, 'lit, 'static_args, 'micheline) expr *) - -val compile_expr - : (meta, (meta, string) Tezos_micheline.Micheline.node) ty list - -> (meta, (meta, string) node, Literal_value.t, (meta, string) node) expr - -> (meta, string) node Lwt.t - -val compile_function_body - : (meta, (meta, string) node, Literal_value.t, (meta, string) node) binds - -> (meta, string) node Lwt.t diff --git a/src/passes/17-stacking/dune b/src/passes/17-stacking/dune index 520f595189..e4181f7e04 100644 --- a/src/passes/17-stacking/dune +++ b/src/passes/17-stacking/dune @@ -6,7 +6,6 @@ (libraries simple-utils ligo.proto-alpha-utils - ligo_coq_ocaml self_michelson mini_c octez-libs.hacl) diff --git a/src/passes/17-stacking/stacking.ml b/src/passes/17-stacking/stacking.ml index c8a4391dc7..1fe7627887 100644 --- a/src/passes/17-stacking/stacking.ml +++ b/src/passes/17-stacking/stacking.ml @@ -1,5 +1,4 @@ module Decompiler = Decompiler -module To_micheline = To_micheline module Program = Compiler_program module Errors = Errors include Program diff --git a/src/passes/17-stacking/to_micheline.ml b/src/passes/17-stacking/to_micheline.ml deleted file mode 100644 index 354f8db599..0000000000 --- a/src/passes/17-stacking/to_micheline.ml +++ /dev/null @@ -1,449 +0,0 @@ -open Core -open Tezos_micheline.Micheline -open Ligo_prim -module Location = Simple_utils.Location -module Ligo_string = Simple_utils.Ligo_string -module Compiler = Ligo_coq_ocaml.Compiler -module Datatypes = Ligo_coq_ocaml.Datatypes - -type meta = Mini_c.meta - -let null = Mini_c.dummy_meta -let int_to_mich (x : int) : (meta, string) node = Int (null, Z.of_int x) - -let nat_to_mich : Datatypes.nat -> (meta, string) node = - let rec aux (x : Z.t) (n : Datatypes.nat) : (meta, string) node = - match n with - | O -> Int (null, x) - | S n -> aux (Z.add Z.one x) n - in - aux Z.zero - - -let smaller m1 m2 = - let open Self_michelson in - let open Lwt.Let_syntax in - let measure mich = - Lwt.map Bytes.length (Proto_alpha_utils.Memory_proto_alpha.to_bytes mich) - in - let optimize = - optimize - ~experimental_disable_optimizations_for_debugging:false - ~has_comment:(fun _ -> false) - in - let%bind loc1 = measure (optimize (Seq (null, m1))) in - let%bind loc2 = measure (optimize (Seq (null, m2))) in - Lwt.return (if loc1 <= loc2 then m1 else m2) - - -(* Should port these to Coq and prove them... and/or just eliminate - FUNC in the Coq compiler *) -let compile_dups1 (s : bool list) : _ node list = - let rec aux n s = - match s with - | [] -> [] - | false :: s -> aux (n - 1) s - | true :: s -> - [ Prim (null, "DIG", [ int_to_mich (n - 1) ], []) - ; Prim (null, "DUP", [], []) - ; Prim (null, "DUG", [ int_to_mich n ], []) - ] - @ aux n s - in - aux (List.length s) (List.rev s) - - -let compile_dups2 (s : bool list) : _ node list = - let rec aux i n s = - match s with - | [] -> [] - | false :: s -> - [ Prim (null, "DIG", [ int_to_mich i ], []) - ; Prim (null, "DUG", [ int_to_mich (n - 1) ], []) - ] - @ aux (i - 1) (n - 1) s - | true :: s -> - [ Prim (null, "DIG", [ int_to_mich i ], []) - ; Prim (null, "DUP", [], []) - ; Prim (null, "DUG", [ int_to_mich n ], []) - ; Prim (null, "DUG", [ int_to_mich i ], []) - ] - @ aux (i - 1) n s - in - aux (List.length s - 1) (List.length s) (List.rev s) - - -let compile_dups (s : bool list) : _ node list Lwt.t = - smaller (compile_dups1 s) (compile_dups2 s) - - -let literal_type_prim (l : Literal_value.t) : string = - match l with - | Literal_unit -> "unit" - | Literal_int _ -> "int" - | Literal_nat _ -> "nat" - | Literal_timestamp _ -> "timestamp" - | Literal_mutez _ -> "mutez" - | Literal_string _ -> "string" - | Literal_bytes _ -> "bytes" - | Literal_address _ -> "address" - | Literal_signature _ -> "signature" - | Literal_key _ -> "key" - | Literal_key_hash _ -> "key_hash" - | Literal_chain_id _ -> "chain_id" - | Literal_operation _ -> "operation" - | Literal_bls12_381_g1 _ -> "bls12_381_g1" - | Literal_bls12_381_g2 _ -> "bls12_381_g2" - | Literal_bls12_381_fr _ -> "bls12_381_fr" - | Literal_chest _ -> "chest" - | Literal_chest_key _ -> "chest_key" - - -let literal_type (l : Literal_value.t) : (meta, string) node = - Prim (null, literal_type_prim l, [], []) - - -let literal_value (l : Literal_value.t) : (meta, string) node = - match l with - | Literal_unit -> Prim (null, "Unit", [], []) - | Literal_int x -> Int (null, x) - | Literal_nat x -> Int (null, x) - | Literal_timestamp x -> Int (null, x) - | Literal_mutez x -> Int (null, x) - | Literal_string x -> String (null, Ligo_string.extract x) - | Literal_bytes x -> Bytes (null, x) - | Literal_address x -> String (null, x) - | Literal_signature x -> String (null, x) - | Literal_key x -> String (null, x) - | Literal_key_hash x -> String (null, x) - | Literal_chain_id x -> String (null, x) - | Literal_operation x -> Bytes (null, x) - | Literal_bls12_381_g1 x -> Bytes (null, x) - | Literal_bls12_381_g2 x -> Bytes (null, x) - | Literal_bls12_381_fr x -> Bytes (null, x) - | Literal_chest x -> Bytes (null, x) - | Literal_chest_key x -> Bytes (null, x) - - -let literal_code (meta : meta) (l : Literal_value.t) : (meta, string) node list = - [ Prim (meta, "PUSH", [ literal_type l; literal_value l ], []) ] - - -let global_constant (meta : meta) (hash : string) : (meta, string) node list = - [ Prim (meta, "constant", [ String (null, hash) ], []) ] - - -let annotate (ann : string option) (x : ('meta, string) node) : ('meta, string) node = - match ann with - | None -> x - | Some ann -> - (match x with - | Prim (l, p, args, anns) -> Prim (l, p, args, ("%" ^ ann) :: anns) - | x -> x) - - -let rec translate_type (t : ('l, ('l, 'p) node) Compiler.ty) : ('l, 'p) node = - match t with - | T_base (_l, b) -> b - (* func is a fictional version of lambda *) - | T_func (l, a1, a2) | T_lambda (l, a1, a2) -> - Prim (l, "lambda", [ translate_type a1; translate_type a2 ], []) - | T_unit l -> Prim (l, "unit", [], []) - | T_pair (l, n1, n2, a1, a2) -> - Prim - (l, "pair", [ annotate n1 (translate_type a1); annotate n2 (translate_type a2) ], []) - | T_or (l, n1, n2, a1, a2) -> - Prim - (l, "or", [ annotate n1 (translate_type a1); annotate n2 (translate_type a2) ], []) - | T_option (l, a) -> Prim (l, "option", [ translate_type a ], []) - | T_list (l, a) -> Prim (l, "list", [ translate_type a ], []) - | T_set (l, a) -> Prim (l, "set", [ translate_type a ], []) - | T_map (l, a1, a2) -> Prim (l, "map", [ translate_type a1; translate_type a2 ], []) - | T_big_map (l, a1, a2) -> - Prim (l, "big_map", [ translate_type a1; translate_type a2 ], []) - | T_ticket (l, a1) -> Prim (l, "ticket", [ translate_type a1 ], []) - | T_contract (l, a1) -> Prim (l, "contract", [ translate_type a1 ], []) - | T_bool l -> Prim (l, "bool", [], []) - | T_int l -> Prim (l, "int", [], []) - | T_nat l -> Prim (l, "nat", [], []) - | T_mutez l -> Prim (l, "mutez", [], []) - | T_string l -> Prim (l, "string", [], []) - | T_bytes l -> Prim (l, "bytes", [], []) - | T_operation l -> Prim (l, "operation", [], []) - | T_address l -> Prim (l, "address", [], []) - | T_key_hash l -> Prim (l, "key_hash", [], []) - - -let has_field_annot = function - | Prim (_, _, _, anns) -> - List.exists anns ~f:(fun ann -> - String.length ann > 1 && String.equal "%" (String.sub ann ~pos:0 ~len:1)) - | _ -> false - - -(* Replace [pair (a %x) (pair (b %y) (c %z))] with [pair (a %x) (b %y) (c %z)]. *) -let rec tuplify_pair_types t = - match t with - | Prim (l, "pair", args, ann) -> - (match List.rev (List.map ~f:tuplify_pair_types args) with - | [] -> t (* impossible *) - | last_arg :: rev_args -> - (match last_arg with - | Prim (_, "pair", last_arg_args, _) when not (has_field_annot last_arg) -> - let args = List.rev rev_args @ last_arg_args in - Prim (l, "pair", args, ann) - | _ -> - let args = List.rev (last_arg :: rev_args) in - Prim (l, "pair", args, ann))) - | Prim (l, p, args, ann) -> Prim (l, p, List.map ~f:tuplify_pair_types args, ann) - | Seq (l, args) -> Seq (l, List.map ~f:tuplify_pair_types args) - | t -> t - - -let translate_type t = tuplify_pair_types (translate_type t) - -let translate_tuple = function - | [] -> Prim (null, "unit", [], []) - | [ a ] -> translate_type a - | az -> Prim (null, "pair", List.map ~f:translate_type az, []) - - -let unpair_tuple = function - | [] -> [ Prim (null, "DROP", [], []) ] - | [ _a ] -> [] - | az -> [ Prim (null, "UNPAIR", [ int_to_mich (List.length az) ], []) ] - - -let pair_tuple = function - | [] -> [ Prim (null, "UNIT", [], []) ] - | [ _a ] -> [] - | az -> [ Prim (null, "PAIR", [ int_to_mich (List.length az) ], []) ] - - -let rec translate_instr - (instr : (meta, (meta, string) node, (meta, string) node) Compiler.instr) - : (meta, string) node list Lwt.t - = - let open Lwt.Let_syntax in - match instr with - (* TODO... *) - | I_FUNC (l, cs, a, b, proj1, proj2, body) -> - let weight p = List.length (List.filter ~f:Fn.id p) in - let n = List.length cs in - if n = 0 - then ( - let%map prog = translate_prog body in - [ Prim (l, "LAMBDA", [ translate_type a; translate_type b; Seq (null, prog) ], []) ]) - else ( - let capture = translate_tuple cs in - let%bind prog = translate_prog body in - let%map dups = compile_dups (false :: proj1) in - [ Prim - ( l - , "LAMBDA" - , [ Prim (null, "pair", [ capture; translate_type a ], []) - ; translate_type b - ; Seq - ( null - , [ Prim (null, "UNPAIR", [], []) ] - @ unpair_tuple cs - @ [ Prim (null, "DIG", [ int_to_mich n ], []) ] - @ prog - @ - if weight proj2 = 0 - then [] - else - [ Prim - ( null - , "DIP" - , [ Seq - ( null - , [ Prim (null, "DROP", [ int_to_mich (weight proj2) ], []) - ] ) - ] - , [] ) - ] ) - ] - , [] ) - ] - @ dups - @ pair_tuple cs - @ [ Prim (null, "APPLY", [], []) ]) - | I_REC_FUNC (l, cs, a, b, proj1, proj2, body) -> - let weight p = List.length (List.filter ~f:Fn.id p) in - let n = List.length cs in - if n = 0 - then ( - let%map prog = translate_prog body in - [ Prim - (l, "LAMBDA_REC", [ translate_type a; translate_type b; Seq (null, prog) ], []) - ]) - else ( - let capture = translate_tuple cs in - let%bind prog = translate_prog body in - let%map dups = compile_dups (false :: proj1) in - [ Prim - ( l - , "LAMBDA_REC" - , [ Prim (null, "pair", [ capture; translate_type a ], []) - ; translate_type b - ; Seq - ( null - , [ Prim (null, "UNPAIR", [], []) ] - @ [ Prim (null, "DUP", [], []) ] - @ unpair_tuple cs - @ [ Prim (null, "DIG", [ int_to_mich (n + 2) ], []) ] - @ [ Prim (null, "DIG", [ int_to_mich (n + 1) ], []) ] - @ [ Prim (null, "APPLY", [], []) ] - @ [ Prim (null, "DIG", [ int_to_mich (n + 1) ], []) ] - @ prog - @ - if weight proj2 = 0 - then [] - else - [ Prim - ( null - , "DIP" - , [ Seq - ( null - , [ Prim (null, "DROP", [ int_to_mich (weight proj2) ], []) - ] ) - ] - , [] ) - ] ) - ] - , [] ) - ] - @ dups - @ pair_tuple cs - @ [ Prim (null, "APPLY", [], []) ]) - (* FICTION *) - | I_FOR (_, body) -> - (* hmmm *) - let%map prog = translate_prog body in - [ Prim (null, "DUP", [ Int (null, Z.of_int 2) ], []) - ; Prim (null, "DUP", [ Int (null, Z.of_int 2) ], []) - ; Prim (null, "COMPARE", [], []) - ; Prim (null, "LE", [], []) - ; Prim - ( null - , "LOOP" - , [ Seq - ( null - , [ Prim (null, "DUP", [], []) - ; Prim (null, "DUG", [ Int (null, Z.of_int 3) ], []) - ; Prim (null, "DIP", [ Int (null, Z.of_int 3); Seq (null, prog) ], []) - ; Prim (null, "DUP", [ Int (null, Z.of_int 3) ], []) - ; Prim (null, "ADD", [], []) - ; Prim (null, "DUP", [ Int (null, Z.of_int 2) ], []) - ; Prim (null, "DUP", [ Int (null, Z.of_int 2) ], []) - ; Prim (null, "COMPARE", [], []) - ; Prim (null, "LE", [], []) - ] ) - ] - , [] ) - ; Prim (null, "DROP", [ Int (null, Z.of_int 3) ], []) - ] - | I_LAMBDA (l, a, b, body) -> - let%map prog = translate_prog body in - [ Prim (l, "LAMBDA", [ translate_type a; translate_type b; Seq (null, prog) ], []) ] - | I_APPLY_LAMBDA (l, _ty) -> Lwt.return [ Prim (l, "APPLY", [], []) ] - | I_RAW (_l, _n, raw) -> Lwt.return raw - | I_SEQ (l, p) -> - let%map prog = translate_prog p in - [ Seq (l, prog) ] - | I_DIP (l, p) -> - let%map prog = translate_prog p in - [ Prim (l, "DIP", [ Seq (null, prog) ], []) ] - | I_DIG (l, n) -> Lwt.return [ Prim (l, "DIG", [ nat_to_mich n ], []) ] - | I_DUG (l, n) -> Lwt.return [ Prim (l, "DUG", [ nat_to_mich n ], []) ] - | I_DUP (l, n) -> Lwt.return [ Prim (l, "DUP", [ nat_to_mich n ], []) ] - | I_DROP (l, n) -> Lwt.return [ Prim (l, "DROP", [ nat_to_mich n ], []) ] - | I_SWAP l -> Lwt.return [ Prim (l, "SWAP", [], []) ] - | I_UNIT l -> Lwt.return [ Prim (l, "UNIT", [], []) ] - | I_TRUE l -> - Lwt.return - [ Prim (l, "PUSH", [ Prim (null, "bool", [], []); Prim (null, "True", [], []) ], []) - ] - | I_LEFT (l, a) -> Lwt.return [ Prim (l, "LEFT", [ translate_type a ], []) ] - | I_RIGHT (l, b) -> Lwt.return [ Prim (l, "RIGHT", [ translate_type b ], []) ] - | I_IF_LEFT (l, bt, bf) -> - let%bind bt = translate_prog bt in - let%map bf = translate_prog bf in - [ Prim (l, "IF_LEFT", [ Seq (null, bt); Seq (null, bf) ], []) ] - | I_PAIR (l, n) -> Lwt.return [ Prim (l, "PAIR", [ nat_to_mich n ], []) ] - | I_UNPAIR (l, n) -> Lwt.return [ Prim (l, "UNPAIR", [ nat_to_mich n ], []) ] - | I_GET (l, n) -> Lwt.return [ Prim (l, "GET", [ nat_to_mich n ], []) ] - | I_UPDATE (l, n) -> Lwt.return [ Prim (l, "UPDATE", [ nat_to_mich n ], []) ] - | I_CAR l -> Lwt.return [ Prim (l, "CAR", [], []) ] - | I_CDR l -> Lwt.return [ Prim (l, "CDR", [], []) ] - | I_IF (l, bt, bf) -> - let%bind bt = translate_prog bt in - let%map bf = translate_prog bf in - [ Prim (l, "IF", [ Seq (null, bt); Seq (null, bf) ], []) ] - | I_IF_NONE (l, bt, bf) -> - let%bind bt = translate_prog bt in - let%map bf = translate_prog bf in - [ Prim (l, "IF_NONE", [ Seq (null, bt); Seq (null, bf) ], []) ] - | I_NIL (l, a) -> Lwt.return [ Prim (l, "NIL", [ translate_type a ], []) ] - | I_CONS l -> Lwt.return [ Prim (l, "CONS", [], []) ] - | I_IF_CONS (l, bt, bf) -> - let%bind bt = translate_prog bt in - let%map bf = translate_prog bf in - [ Prim (l, "IF_CONS", [ Seq (null, bt); Seq (null, bf) ], []) ] - | I_EXEC l -> Lwt.return [ Prim (l, "EXEC", [], []) ] - | I_LOOP (l, body) -> - let%map prog = translate_prog body in - [ Prim (l, "LOOP", [ Seq (null, prog) ], []) ] - | I_LOOP_LEFT (l, body) -> - let%map prog = translate_prog body in - [ Prim (l, "LOOP_LEFT", [ Seq (null, prog) ], []) ] - (* | I_PUSH (l, a, x) -> failwith "TODO" *) - | I_FAILWITH l -> Lwt.return [ Prim (l, "FAILWITH", [], []) ] - | I_ITER (l, body) -> - let%map prog = translate_prog body in - [ Prim (l, "ITER", [ Seq (null, prog) ], []) ] - | I_MAP (l, body) -> - let%map prog = translate_prog body in - [ Prim (l, "MAP", [ Seq (null, prog) ], []) ] - | I_CREATE_CONTRACT (l, p, s, script) -> - let%map prog = translate_prog script in - [ Prim - ( l - , "CREATE_CONTRACT" - , [ Seq - ( null - , [ Prim (null, "parameter", [ translate_type p ], []) - ; Prim (null, "storage", [ translate_type s ], []) - ; Prim (null, "code", [ Seq (null, prog) ], []) - ] ) - ] - , [] ) - ] - - -and translate_prog prog = - Lwt.map List.concat @@ Lwt.all @@ List.map ~f:translate_instr prog - - -(* strengthening of metadata (select the part of the env info which is - still relevant after strengthening) *) -let strengthen_meta (r : bool list) (m : meta) = - { m with env = Ligo_coq_ocaml.Ope.select r m.env } - - -let strengthen_prog prog embedding = - let prog1 = prog in - let us, prog2 = - Compiler.strengthen_prog - null - (* hmm, I believe these are not used by strengthen_prog. they can - probably be removed somehow from the extraction? *) - (fun _ _ -> failwith "TODO") - (fun _ _ -> failwith "TODO") - (fun _ _ -> failwith "TODO") - strengthen_meta - prog1 - embedding - in - us, prog2 diff --git a/src/passes/predefined/dune b/src/passes/predefined/dune index b443a285eb..1160ce27c7 100644 --- a/src/passes/predefined/dune +++ b/src/passes/predefined/dune @@ -3,4 +3,4 @@ (public_name ligo.predefined) (instrumentation (backend bisect_ppx)) - (libraries simple-utils ast_core ast_typed mini_c stacking ligo_coq_ocaml)) + (libraries simple-utils ast_core ast_typed mini_c stacking))