From 30c395151dc98885d26c980b045ab87baffef498 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 28 Nov 2021 01:08:56 -0800 Subject: [PATCH] Use a different representation of values and prove equivalence of UCC evalutor --- code/dawn/DawnEval.v | 139 +++++++++++++++++++++------------ code/dawn/DawnV2.v | 179 +++++++++++++++++++++++++++++++++++++++++++ code/dawn/Ucc.hs | 64 ++++++++++++++++ 3 files changed, 335 insertions(+), 47 deletions(-) create mode 100644 code/dawn/DawnV2.v create mode 100644 code/dawn/Ucc.hs diff --git a/code/dawn/DawnEval.v b/code/dawn/DawnEval.v index b9fa7ef..01417c3 100644 --- a/code/dawn/DawnEval.v +++ b/code/dawn/DawnEval.v @@ -1,22 +1,22 @@ Require Import Coq.Lists.List. -Require Import Dawn. +Require Import DawnV2. Require Import Coq.Program.Equality. From Ltac2 Require Import Ltac2. Inductive step_result := | err - | middle (e : expr) (s : list expr) - | final (s : list expr). + | middle (e : expr) (s : value_stack) + | final (s : value_stack). -Fixpoint eval_step (s : list expr) (e : expr) : step_result := +Fixpoint eval_step (s : value_stack) (e : expr) : step_result := match e, s with | e_int swap, v' :: v :: vs => final (v :: v' :: vs) | e_int clone, v :: vs => final (v :: v :: vs) | e_int drop, v :: vs => final vs - | e_int quote, v :: vs => final (e_quote v :: vs) - | e_int compose, (e_quote v2) :: (e_quote v1) :: vs => final (e_quote (e_comp v1 v2) :: vs) - | e_int apply, (e_quote v1) :: vs => middle v1 vs - | e_quote e', vs => final (e_quote e' :: vs) + | e_int quote, v :: vs => final (v_quote (value_to_expr v) :: vs) + | e_int compose, (v_quote v2) :: (v_quote v1) :: vs => final (v_quote (e_comp v1 v2) :: vs) + | e_int apply, (v_quote v1) :: vs => middle v1 vs + | e_quote e', vs => final (v_quote e' :: vs) | e_comp e1 e2, vs => match eval_step vs e1 with | final vs' => middle e2 vs' @@ -26,12 +26,10 @@ Fixpoint eval_step (s : list expr) (e : expr) : step_result := | _, _ => err end. -Definition strip_value_list (vs : value_stack) := @map value expr (@projT1 expr IsValue) vs. - Theorem eval_step_correct : forall (e : expr) (vs vs' : value_stack), Sem_expr vs e vs' -> - (eval_step (strip_value_list vs) e = final (strip_value_list vs')) \/ + (eval_step vs e = final vs') \/ (exists (ei : expr) (vsi : value_stack), - eval_step (strip_value_list vs) e = middle ei (strip_value_list vsi) /\ + eval_step vs e = middle ei vsi /\ Sem_expr vsi ei vs'). Proof. intros e vs vs' Hsem. @@ -39,9 +37,9 @@ Proof. induction Hsem. - inversion H; (* The expression is just an intrnsic. *) (* Dismiss all the straightforward "final" cases, - of which most intrinsics are *) + of which most intrinsics are. *) try (left; reflexivity). - (* We are in an intermediate / middle case. *) + (* Only apply remains; We are in an intermediate / middle case. *) right. (* The semantics guarantee that the expression in the quote evaluates to the final state. *) @@ -63,26 +61,26 @@ Proof. eapply Sem_e_comp. apply Hsem'. apply Hsem2. Qed. -Inductive eval_chain (s : list expr) (e : expr) (s' : list expr) : Prop := - | chain_final (P : eval_step s e = final s') - | chain_middle (ei : expr) (si : list expr) - (P : eval_step s e = middle ei si) (rest : eval_chain si ei s'). +Inductive eval_chain (vs : value_stack) (e : expr) (vs' : value_stack) : Prop := + | chain_final (P : eval_step vs e = final vs') + | chain_middle (ei : expr) (vsi : value_stack) + (P : eval_step vs e = middle ei vsi) (rest : eval_chain vsi ei vs'). -Lemma eval_chain_merge : forall (e1 e2 : expr) (s s' s'' : list expr), - eval_chain s e1 s' -> eval_chain s' e2 s'' -> eval_chain s (e_comp e1 e2) s''. +Lemma eval_chain_merge : forall (e1 e2 : expr) (vs vs' vs'' : value_stack), + eval_chain vs e1 vs' -> eval_chain vs' e2 vs'' -> eval_chain vs (e_comp e1 e2) vs''. Proof. - intros e1 e2 s s' s'' ch1 ch2. + intros e1 e2 vs vs' vs'' ch1 ch2. induction ch1; eapply chain_middle; simpl; try (rewrite P); auto. Qed. -Lemma eval_chain_split : forall (e1 e2 : expr) (s s'' : list expr), - eval_chain s (e_comp e1 e2) s'' -> exists s', (eval_chain s e1 s') /\ (eval_chain s' e2 s''). +Lemma eval_chain_split : forall (e1 e2 : expr) (vs vs'' : value_stack), + eval_chain vs (e_comp e1 e2) vs'' -> exists vs', (eval_chain vs e1 vs') /\ (eval_chain vs' e2 vs''). Proof. - intros e1 e2 s ss'' ch. + intros e1 e2 vs vss'' ch. ltac1:(dependent induction ch). - - simpl in P. destruct (eval_step s e1); inversion P. - - simpl in P. destruct (eval_step s e1) eqn:Hval; try (inversion P). + - simpl in P. destruct (eval_step vs e1); inversion P. + - simpl in P. destruct (eval_step vs e1) eqn:Hval; try (inversion P). + injection P as Hinj; subst. specialize (IHch e e2 H0) as [s'0 [ch1 ch2]]. eexists. split. * eapply chain_middle. apply Hval. apply ch1. @@ -93,9 +91,9 @@ Proof. Qed. Theorem val_step_sem : forall (e : expr) (vs vs' : value_stack), - Sem_expr vs e vs' -> eval_chain (strip_value_list vs) e (strip_value_list vs') + Sem_expr vs e vs' -> eval_chain vs e vs' with eval_step_int : forall (i : intrinsic) (vs vs' : value_stack), - Sem_int vs i vs' -> eval_chain (strip_value_list vs) (e_int i) (strip_value_list vs'). + Sem_int vs i vs' -> eval_chain vs (e_int i) vs'. Proof. - intros e vs vs' Hsem. induction Hsem. @@ -106,7 +104,7 @@ Proof. apply chain_final. auto. + (* In compoition, by induction, we know that the two sub-expressions produce proper evaluation chains. Chains can be composed (via eval_chain_merge). *) - eapply eval_chain_merge with (strip_value_list vs2); auto. + eapply eval_chain_merge with vs2; auto. - intros i vs vs' Hsem. (* The evaluation chain depends on the specific intrinsic in use. *) inversion Hsem; subst; @@ -114,15 +112,9 @@ Proof. try (apply chain_final; auto; fail). (* Only apply is non-final. The first step is popping the quote from the stack, and the rest of the steps are given by the evaluation of the code in the quote. *) - apply chain_middle with e (strip_value_list vs0); auto. + apply chain_middle with e vs0; auto. Qed. -Theorem eval_step_sem_back : forall (e : expr) (vs vs' : value_stack), - eval_chain (strip_value_list vs) e (strip_value_list vs') -> Sem_expr vs e vs'. -Proof. - (* Thoughts: the issue is with the apparent nondeterminism of evalution. *) -Admitted. - Ltac2 Type exn ::= [ | Not_intrinsic ]. Ltac2 rec destruct_n (n : int) (vs : constr) : unit := @@ -146,15 +138,6 @@ Ltac2 int_arity (int : constr) : int := Ltac2 destruct_int_stack (int : constr) (va: constr) := destruct_n (int_arity int) va. -Ltac2 ensure_valid_value_stack () := Control.enter (fun () => - match! goal with - | [h : eval_step (strip_value_list ?a) (e_int ?b) = ?c |- _] => - let h := Control.hyp h in - destruct_int_stack b a; - try (inversion $h; fail) - | [|- _ ] => () - end). - Ltac2 ensure_valid_stack () := Control.enter (fun () => match! goal with | [h : eval_step ?a (e_int ?b) = ?c |- _] => @@ -164,15 +147,77 @@ Ltac2 ensure_valid_stack () := Control.enter (fun () => | [|- _ ] => () end). -Theorem test : forall (s s': list expr), eval_step s (e_int swap) = final s' -> - exists v1 v2 s'', s = v1 :: v2 :: s'' /\ s' = v2 :: v1 :: s''. +Theorem test : forall (vs vs': value_stack), eval_step vs (e_int swap) = final vs' -> + exists v1 v2 vs'', vs = v1 :: v2 :: vs'' /\ vs' = v2 :: v1 :: vs''. Proof. intros s s' Heq. ensure_valid_stack (). simpl in Heq. injection Heq as Hinj. subst. eauto. Qed. +Theorem eval_step_final_sem : forall (e : expr) (vs vs' : value_stack), + eval_step vs e = final vs' -> Sem_expr vs e vs'. +Proof. + intros e vs vs' Hev. destruct e. + - destruct i; ensure_valid_stack (); + (* Get rid of trivial cases that match one-to-one. *) + simpl in Hev; try (injection Hev as Hinj; subst; solve_basic ()). + + (* compose with one quoted value *) + destruct v. inversion Hev. + + (* compose with two quoted values. *) + destruct v; destruct v0. + injection Hev as Hinj; subst; solve_basic (). + + (* Apply is not final. *) destruct v. inversion Hev. + - (* Quote is always final, trivially. *) + simpl in Hev. injection Hev as Hinj; subst. solve_basic (). + - (* Compose is never final. *) + simpl in Hev. destruct (eval_step vs e1); inversion Hev. +Qed. + +Theorem eval_step_middle_sem : forall (e ei: expr) (vs vsi vs' : value_stack), + eval_step vs e = middle ei vsi -> + Sem_expr vsi ei vs' -> + Sem_expr vs e vs'. +Proof. + intros e. induction e; intros ei vs vsi vs' Hev Hsem. + - destruct i; ensure_valid_stack (). + + (* compose with one quoted value. *) + destruct v. inversion Hev. + + (* compose with two quoted values. *) + destruct v; destruct v0. inversion Hev. + + (* Apply *) + destruct v. injection Hev as Hinj; subst. + solve_basic (). auto. + - inversion Hev. + - simpl in Hev. + destruct (eval_step vs e1) eqn:Hev1. + + inversion Hev. + + injection Hev as Hinj; subst. inversion Hsem; subst. + specialize (IHe1 e vs vsi vs2 Hev1 H2). + eapply Sem_e_comp. apply IHe1. apply H4. + + injection Hev as Hinj; subst. + specialize (eval_step_final_sem e1 vs vsi Hev1) as Hsem1. + eapply Sem_e_comp. apply Hsem1. apply Hsem. +Qed. + +Theorem eval_step_sem_back : forall (e : expr) (vs vs' : value_stack), + eval_chain vs e vs' -> Sem_expr vs e vs'. +Proof. + intros e vs vs' ch. + ltac1:(dependent induction ch). + - apply eval_step_final_sem. auto. + - specialize (eval_step_middle_sem e ei vs vsi vs' P IHch). auto. +Qed. + +Corollary eval_step_no_sem : forall (e : expr) (vs vs' : value_stack), + ~ (Sem_expr vs e vs') -> ~(eval_chain vs e vs'). +Proof. + intros e vs vs' Hnsem Hch. + specialize (eval_step_sem_back _ _ _ Hch). auto. +Qed. + Require Extraction. Require Import ExtrHaskellBasic. Extraction Language Haskell. +Set Extraction KeepSingleton. Extraction "UccGen.hs" expr eval_step true false or. diff --git a/code/dawn/DawnV2.v b/code/dawn/DawnV2.v new file mode 100644 index 0000000..d8bb448 --- /dev/null +++ b/code/dawn/DawnV2.v @@ -0,0 +1,179 @@ +Require Import Coq.Lists.List. +From Ltac2 Require Import Ltac2. + +Inductive intrinsic := + | swap + | clone + | drop + | quote + | compose + | apply. + +Inductive expr := + | e_int (i : intrinsic) + | e_quote (e : expr) + | e_comp (e1 e2 : expr). + +Definition e_compose (e : expr) (es : list expr) := fold_left e_comp es e. + +Inductive value := v_quote (e : expr). +Definition value_stack := list value. + +Definition value_to_expr (v : value) : expr := + match v with + | v_quote e => e_quote e + end. + +Inductive Sem_int : value_stack -> intrinsic -> value_stack -> Prop := + | Sem_swap : forall (v v' : value) (vs : value_stack), Sem_int (v' :: v :: vs) swap (v :: v' :: vs) + | Sem_clone : forall (v : value) (vs : value_stack), Sem_int (v :: vs) clone (v :: v :: vs) + | Sem_drop : forall (v : value) (vs : value_stack), Sem_int (v :: vs) drop vs + | Sem_quote : forall (v : value) (vs : value_stack), Sem_int (v :: vs) quote ((v_quote (value_to_expr v)) :: vs) + | Sem_compose : forall (e e' : expr) (vs : value_stack), Sem_int (v_quote e' :: v_quote e :: vs) compose (v_quote (e_comp e e') :: vs) + | Sem_apply : forall (e : expr) (vs vs': value_stack), Sem_expr vs e vs' -> Sem_int (v_quote e :: vs) apply vs' + +with Sem_expr : value_stack -> expr -> value_stack -> Prop := + | Sem_e_int : forall (i : intrinsic) (vs vs' : value_stack), Sem_int vs i vs' -> Sem_expr vs (e_int i) vs' + | Sem_e_quote : forall (e : expr) (vs : value_stack), Sem_expr vs (e_quote e) (v_quote e :: vs) + | Sem_e_comp : forall (e1 e2 : expr) (vs1 vs2 vs3 : value_stack), + Sem_expr vs1 e1 vs2 -> Sem_expr vs2 e2 vs3 -> Sem_expr vs1 (e_comp e1 e2) vs3. + +Definition false : expr := e_quote (e_int drop). +Definition false_v : value := v_quote (e_int drop). + +Definition true : expr := e_quote (e_comp (e_int swap) (e_int drop)). +Definition true_v : value := v_quote (e_comp (e_int swap) (e_int drop)). + +Theorem false_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp false (e_int apply)) (v :: vs). +Proof. + intros v v' vs. + eapply Sem_e_comp. + - apply Sem_e_quote. + - apply Sem_e_int. apply Sem_apply. apply Sem_e_int. apply Sem_drop. +Qed. + +Theorem true_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp true (e_int apply)) (v' :: vs). +Proof. + intros v v' vs. + eapply Sem_e_comp. + - apply Sem_e_quote. + - apply Sem_e_int. apply Sem_apply. eapply Sem_e_comp. + * apply Sem_e_int. apply Sem_swap. + * apply Sem_e_int. apply Sem_drop. +Qed. + +Definition or : expr := e_comp (e_int clone) (e_int apply). + +Theorem or_false_v : forall (v : value) (vs : value_stack), Sem_expr (false_v :: v :: vs) or (v :: vs). +Proof with apply Sem_e_int. + intros v vs. + eapply Sem_e_comp... + - apply Sem_clone. + - apply Sem_apply... apply Sem_drop. +Qed. + +Theorem or_true : forall (v : value) (vs : value_stack), Sem_expr (true_v :: v :: vs) or (true_v :: vs). +Proof with apply Sem_e_int. + intros v vs. + eapply Sem_e_comp... + - apply Sem_clone... + - apply Sem_apply. eapply Sem_e_comp... + * apply Sem_swap. + * apply Sem_drop. +Qed. + +Definition or_false_false := or_false_v false_v. +Definition or_false_true := or_false_v true_v. +Definition or_true_false := or_true false_v. +Definition or_true_true := or_true true_v. + +Fixpoint quote_n (n : nat) := + match n with + | O => e_int quote + | S n' => e_compose (quote_n n') (e_int swap :: e_int quote :: e_int swap :: e_int compose :: nil) + end. + +Theorem quote_2_correct : forall (v1 v2 : value) (vs : value_stack), + Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (value_to_expr v1) (value_to_expr v2)) :: vs). +Proof with apply Sem_e_int. + intros v1 v2 vs. simpl. + repeat (eapply Sem_e_comp)... + - apply Sem_quote. + - apply Sem_swap. + - apply Sem_quote. + - apply Sem_swap. + - apply Sem_compose. +Qed. + +Theorem quote_3_correct : forall (v1 v2 v3 : value) (vs : value_stack), + Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (value_to_expr v1) (e_comp (value_to_expr v2) (value_to_expr v3))) :: vs). +Proof with apply Sem_e_int. + intros v1 v2 v3 vs. simpl. + repeat (eapply Sem_e_comp)... + - apply Sem_quote. + - apply Sem_swap. + - apply Sem_quote. + - apply Sem_swap. + - apply Sem_compose. + - apply Sem_swap. + - apply Sem_quote. + - apply Sem_swap. + - apply Sem_compose. +Qed. + +Ltac2 rec solve_basic () := Control.enter (fun _ => + match! goal with + | [|- Sem_int ?vs1 swap ?vs2] => apply Sem_swap + | [|- Sem_int ?vs1 clone ?vs2] => apply Sem_clone + | [|- Sem_int ?vs1 drop ?vs2] => apply Sem_drop + | [|- Sem_int ?vs1 quote ?vs2] => apply Sem_quote + | [|- Sem_int ?vs1 compose ?vs2] => apply Sem_compose + | [|- Sem_int ?vs1 apply ?vs2] => apply Sem_apply + | [|- Sem_expr ?vs1 (e_comp ?e1 ?e2) ?vs2] => eapply Sem_e_comp; solve_basic () + | [|- Sem_expr ?vs1 (e_int ?e) ?vs2] => apply Sem_e_int; solve_basic () + | [|- Sem_expr ?vs1 (e_quote ?e) ?vs2] => apply Sem_e_quote + | [_ : _ |- _] => () + end). + +Theorem quote_2_correct' : forall (v1 v2 : value) (vs : value_stack), + Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (value_to_expr v1) (value_to_expr v2)) :: vs). +Proof. intros. simpl. solve_basic (). Qed. + +Theorem quote_3_correct' : forall (v1 v2 v3 : value) (vs : value_stack), + Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (value_to_expr v1) (e_comp (value_to_expr v2) (value_to_expr v3))) :: vs). +Proof. intros. simpl. solve_basic (). Qed. + +Definition rotate_n (n : nat) := e_compose (quote_n n) (e_int swap :: e_int quote :: e_int compose :: e_int apply :: nil). + +Lemma eval_value : forall (v : value) (vs : value_stack), + Sem_expr vs (value_to_expr v) (v :: vs). +Proof. + intros v vs. + destruct v. + simpl. apply Sem_e_quote. +Qed. + +Theorem rotate_3_correct : forall (v1 v2 v3 : value) (vs : value_stack), + Sem_expr (v3 :: v2 :: v1 :: vs) (rotate_n 1) (v1 :: v3 :: v2 :: vs). +Proof. + intros. unfold rotate_n. simpl. solve_basic (). + repeat (eapply Sem_e_comp); apply eval_value. +Qed. + +Theorem rotate_4_correct : forall (v1 v2 v3 v4 : value) (vs : value_stack), + Sem_expr (v4 :: v3 :: v2 :: v1 :: vs) (rotate_n 2) (v1 :: v4 :: v3 :: v2 :: vs). +Proof. + intros. unfold rotate_n. simpl. solve_basic (). + repeat (eapply Sem_e_comp); apply eval_value. +Qed. + +Theorem e_comp_assoc : forall (e1 e2 e3 : expr) (vs vs' : value_stack), + Sem_expr vs (e_comp e1 (e_comp e2 e3)) vs' <-> Sem_expr vs (e_comp (e_comp e1 e2) e3) vs'. +Proof. + intros e1 e2 e3 vs vs'. + split; intros Heval. + - inversion Heval; subst. inversion H4; subst. + eapply Sem_e_comp. eapply Sem_e_comp. apply H2. apply H3. apply H6. + - inversion Heval; subst. inversion H2; subst. + eapply Sem_e_comp. apply H3. eapply Sem_e_comp. apply H6. apply H4. +Qed. diff --git a/code/dawn/Ucc.hs b/code/dawn/Ucc.hs new file mode 100644 index 0000000..4fd94db --- /dev/null +++ b/code/dawn/Ucc.hs @@ -0,0 +1,64 @@ +module Ucc where +import UccGen +import Text.Parsec +import Data.Functor.Identity +import Control.Applicative hiding ((<|>)) +import System.IO + +instance Show Intrinsic where + show Swap = "swap" + show Clone = "clone" + show Drop = "drop" + show Quote = "quote" + show Compose = "compose" + show Apply = "apply" + +instance Show Expr where + show (E_int i) = show i + show (E_quote e) = "[" ++ show e ++ "]" + show (E_comp e1 e2) = show e1 ++ " " ++ show e2 + +instance Show Value where + show (V_quote e) = show (E_quote e) + +type Parser a = ParsecT String () Identity a + +intrinsic :: Parser Intrinsic +intrinsic = (<* spaces) $ foldl1 (<|>) $ map (\(s, i) -> try (string s >> return i)) + [ ("swap", Swap) + , ("clone", Clone) + , ("drop", Drop) + , ("quote", Quote) + , ("compose", Compose) + , ("apply", Apply) + ] + +expression :: Parser Expr +expression = foldl1 E_comp <$> many1 single + where + single + = (E_int <$> intrinsic) + <|> (fmap E_quote $ char '[' *> spaces *> expression <* char ']' <* spaces) + +parseExpression :: String -> Either ParseError Expr +parseExpression = runParser expression () "" + +eval :: [Value] -> Expr -> Maybe [Value] +eval s e = + case eval_step s e of + Err -> Nothing + Final s' -> Just s' + Middle e' s' -> eval s' e' + +main :: IO () +main = do + putStr "> " + hFlush stdout + str <- getLine + case parseExpression str of + Right e -> + case eval [] e of + Just st -> putStrLn $ show st + _ -> putStrLn "Evaluation error" + _ -> putStrLn "Parse error" + main