Unverified Commit 243b6bfd authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Remove commented code

parent 19aed443
......@@ -40,20 +40,6 @@ Module Proofs (C : syntax.ContractContext).
michelson_type_of_type ty = Return _ mty ->
exists td, type_data d mty = Michocoq.error.Return td.
Proof.
(* induction v using val_ind; intros d ty' mty Hd Hty Hmty; simpl in *. *)
(* - (* numval *) *)
(* admit. *)
(* (* AJ: this blocks coq. *)
(* * destruct v; invert Hd; invert Hty; invert Hmty; simpl; *)
(* * unfold type_data, mtyper.type_data; eexists; eauto. *)
(* *) *)
(* - (* bool *) *)
(* invert Hty; invert Hmty. *)
(* destruct b; simpl in *; invert Hd; eexists; reflexivity. *)
(* - (* record *) *)
(* admit. *)
(* - (* variant *) *)
(* admit. *)
Admitted.
Fixpoint michelson_stack_type_of_rty (lt : list (label * ty)) : M syntax.stack_type :=
......@@ -64,18 +50,6 @@ Module Proofs (C : syntax.ContractContext).
Return _ (mty::sty)
end.
(* Lemma michelson_stack_type_of_rty_map_ret : forall lt, *)
(* michelson_stack_type_of_rty lt (map (fun '(l, _) => l) lt) = *)
(* Return _ (map (fun '(_, t) => (michelson_type_of_type t)) lt). *)
(* Proof. *)
(* induction lt; simpl. *)
(* - reflexivity. *)
(* - destruct a as [hd t]. *)
(* destruct string_dec; try contradiction. *)
(* simpl. rewrite IHlt; simpl. *)
(* reflexivity. *)
(* Qed. *)
Lemma compute_dig_typing: forall var ty' lt lt' ll ll' ins mty sty sty',
type_and_remove var lt = Return _ (ty', lt') ->
compute_dig var ll = Return _ (ins, ll') ->
......@@ -108,14 +82,6 @@ Module Proofs (C : syntax.ContractContext).
unpair_rec_to_stack lt = (ins, ll) ->
exists ins' ll', pair_stack_to_rec lt ll = Return _ (ins', ll').
Proof.
(* induction lt using list_hdhd_ins; intros ins ll Hunpair. *)
(* - simpl in *. invert Hunpair. eexists; eauto. *)
(* - simpl in *. destruct a as [l t]. *)
(* invert Hunpair. *)
(* repeat eexists. *)
(* unfold compute_dig. simpl. rewrite string_dec_same; simpl. *)
(* auto. *)
(* - admit. *)
Admitted.
Ltac unfold_check :=
......@@ -135,29 +101,6 @@ Module Proofs (C : syntax.ContractContext).
michelson_stack_type_of_rty lt = Return _ sty -> michelson_stack_type_of_rty lt' = Return _ sty' ->
exists res, type_check_instruction type_instruction ins sty (mty::sty') = Michocoq.error.Return res.
Proof.
(* induction arg; intros ins ty' lt lt' ll ll' mty sty sty' Hty Hcomp Hmty Hsty Hsty'; simpl in *. *)
(* - (* var *) *)
(* apply bind_eq_return in Hty as [[ty'' lt''] [Hty Heq]]; invert Heq. *)
(* unfold_check. *)
(* apply bind_eq_return in Hcomp as [[insDig ll''] [Hcomp Hcomp']]; invert Hcomp'. *)
(* specialize (compute_dig_typing var _ _ _ _ _ _ _ _ _ Hty Hcomp Hmty Hsty Hsty') as [tins Hdig]. *)
(* rewrite Hdig; simpl. unfold_cast. *)
(* admit. *)
(* (* AJ: does not work anymore *)
(* * eexists reflexivity. *)
(* *) *)
(* - (* val *) *)
(* apply bind_eq_return in Hty as [ty'' [Hty Hty2]]; invert Hty2. *)
(* apply bind_eq_return in Hcomp as [d [Hd1 Hd2]]. *)
(* apply bind_eq_return in Hd2 as [ty'' [Hd2 Hd3]]. *)
(* apply bind_eq_return in Hd3 as [td' [Hd3 Hd4]]; invert Hd4. *)
(* rewrite Hsty in Hsty'; invert Hsty'. rewrite Hty in Hd2; invert Hd2. *)
(* rewrite Hmty in Hd3; invert Hd3. *)
(* specialize (data_type_correct _ d ty'' td' Hd1 Hty Hmty) as [td Htd]. *)
(* unfold_check; unfold type_data in Htd. *)
(* (* rewrite Htd; simpl. unfold_cast. eexists; auto. *) *)
(* admit. *)
(* - (* record *) admit. *)
Admitted.
Lemma compile_funct_type_correct : forall funct defs ins ty ty' mty mty' sty,
......@@ -166,24 +109,6 @@ Module Proofs (C : syntax.ContractContext).
michelson_type_of_type ty = Return _ mty -> michelson_type_of_type ty' = Return _ mty' ->
exists res, type_check_instruction type_instruction ins (mty::sty) (mty'::sty) = Michocoq.error.Return res.
Proof.
(* intros funct defs ins ty ty' mty mty' sty Hty Hcomp Hmty Hmty'. *)
(* induction funct; invert Hty; invert Hcomp; simpl in *. *)
(* - (* dup *) *)
(* apply bind_eq_return in Hmty' as [mty'' [Hmty'' Hmty']]. *)
(* apply bind_eq_return in Hmty' as [mty''' [Hmty''' Hmty']]. *)
(* rewrite Hmty in Hmty''; rewrite Hmty in Hmty'''; invert Hmty''; invert Hmty'''. *)
(* invert Hmty'. *)
(* unfold_check. unfold_cast. *)
(* eexists. *)
(* admit. *)
(* (* AJ: no longer works *)
(* * reflexivity. *)
(* *) *)
(* - (* constr *) *)
(* destruct vty5. *)
(* apply bind_eq_return in H0 as [[ty'' lt''] [Hret1 Hret2]]. *)
(* destruct (type_eq ty ty'') eqn:Heq; invert Hret2. *)
(* admit. *)
Admitted.
(** Rhs adds a single element to the stack *)
......@@ -194,30 +119,6 @@ Module Proofs (C : syntax.ContractContext).
michelson_stack_type_of_rty lt = Return _ sty -> michelson_stack_type_of_rty lt' = Return _ sty' ->
exists res, type_check_instruction type_instruction ins sty (mty::sty') = Michocoq.error.Return res.
Proof.
(* induction rhs; intros defs ins ty' lt lt' ll ll' mty sty sty' Hty Hcomp Hmty Hsty Hsty'; simpl in *. *)
(* - (* arg *) *)
(* specialize (compile_arg_type_correct arg5 ins _ _ _ _ _ _ _ _ Hty Hcomp Hmty Hsty Hsty') as Harg. *)
(* assumption. *)
(* - (* app *) *)
(* apply bind_eq_return in Hcomp as [[ins1 ll''] [Hcarg Hcomp]]. *)
(* apply bind_eq_return in Hcomp as [ins2 [Hcfunct Hret]]. invert Hret. *)
(* apply bind_eq_return in Hty as [[ty'' rt''] [Htarg Hty]]. *)
(* apply bind_eq_return in Hty as [ty''' [Htfunct Hret]]. invert Hret. *)
(* (* specialize (compile_arg_type_correct arg5 ins1 _ _ _ _ _ _ _ Htarg Hcarg Hsty Hsty') as [resa Harg]. *) *)
(* (* specialize (compile_funct_type_correct f5 ins2 _ _ sty' Htfunct Hcfunct) as [resf Hfunct]. *) *)
(* (* unfold_check. *) admit. *)
(* - (* projection *) admit. *)
(* - (* update *) admit. *)
(* - (* add *) *)
(* apply bind_eq_return in Hty as [[ty1 lt1] [Hty1 Hty]]; *)
(* apply bind_eq_return in Hty as [[ty2 lt2] [Hty2 Hty]]. *)
(* apply bind_eq_return in Hcomp as [[ins1 ll1] [Hcomp1 Hcomp]]; *)
(* apply bind_eq_return in Hcomp as [[ins2 ll2] [Hcomp2 Hcomp]]. invert Hcomp. *)
(* destruct ty1; destruct ty2; invert Hty; simpl; admit. *)
(* - (* sub *) admit. *)
(* - (* mul *) admit. *)
(* - (* div *) admit. *)
(* - (* match *) admit. *)
Admitted.
Lemma compile_instr_type_correct : forall ins defs lt lt' unins ll ll' sty sty',
......@@ -227,24 +128,6 @@ Module Proofs (C : syntax.ContractContext).
michelson_stack_type_of_rty lt' = Return _ sty' ->
exists res, type_check_instruction type_instruction unins sty sty' = Michocoq.error.Return res.
Proof.
(* induction ins; intros defs lt lt' unins ll ll' sty sty' Hty Hcomp Hsty Hsty'; *)
(* invert Hty; invert Hcomp; simpl in *. *)
(* - (* noop *) *)
(* rewrite Hsty in Hsty'. invert Hsty'. *)
(* unfold_check. unfold_cast. *)
(* eexists. reflexivity. *)
(* - (* seq *) *)
(* admit. *)
(* - (* assign *) *)
(* admit. *)
(* - (* drop *) *)
(* admit. *)
(* - (* match *) *)
(* admit. *)
(* - (* loop_left *) *)
(* admit. *)
(* - (* loop *) *)
(* admit. *)
Admitted.
End Proofs.
......@@ -330,50 +330,3 @@ Proof.
try exact I; try reflexivity; try discriminate H12; try inversion H12;
try (apply IHs1; auto).
Qed.
(* Module Type TType. *)
(* Parameter T : Type. *)
(* End TType. *)
(* Module LexicoOrder (T: TType) <: TotalLeBool. *)
(* Definition t := (string * T.T)%type. *)
(* Definition leb := @lexico_leb_pair T.T. *)
(* Theorem leb_total : forall s1 s2, leb s1 s2 = true \/ leb s2 s1 = true. *)
(* Proof. *)
(* intros p1 p2. destruct p1 as [s1 t1]; destruct p2 as [s2 t2]. *)
(* unfold leb. repeat rewrite lexico_leb_le. *)
(* apply lexico_total. *)
(* Qed. *)
(* End LexicoOrder. *)
(* Inductive NotSorted : list string -> Prop := *)
(* | NotSortedCons1 a l : NotSorted l -> NotSorted (a::l) *)
(* | NotSortedCons2 a l : Exists (fun s => ~(lexico_le a s)) l -> NotSorted (a::l). *)
(* Theorem StronglySorted_NotSorted_dec : forall l, *)
(* { StronglySorted lexico_le l } + { NotSorted l }. *)
(* Proof. *)
(* induction l. *)
(* - left. constructor. *)
(* - destruct IHl. *)
(* + specialize (Forall_Exists_dec (lexico_le a) (lexico_le_dec a) l). *)
(* intros [Hforall|Hexists]. *)
(* * left. constructor; auto. *)
(* * right. apply NotSortedCons2; auto. *)
(* + right. constructor; auto. *)
(* Qed. *)
(* Corollary StronglySorted_NotSorted_iff: forall l, *)
(* NotSorted l <-> ~(StronglySorted lexico_le l). *)
(* Proof. *)
(* induction l. *)
(* - split; intros. inversion H. exfalso. apply H; constructor. *)
(* - split; intros. *)
(* + intro contra. inversion H; subst. rewrite IHl in H1. *)
(* apply H1. inversion contra; auto. *)
(* inversion contra; subst. *)
(* specialize (Exists_Forall_neg (lexico_le a) l (lexico_le_or a)) as Hneg. *)
(* rewrite Hneg in H1; apply H1; auto. *)
(* + specialize (StronglySorted_NotSorted_dec (a::l)) as [HStrong|HNot]; auto. *)
(* exfalso. auto. *)
(* Qed. *)
......@@ -51,71 +51,6 @@ Module LexicoOrderRhs <: TotalLeBool.
End LexicoOrderRhs.
Module LexicoRhsSort:= Sort LexicoOrderRhs.
(* Module LexicoPattern <: TotalLeBool. *)
(* Definition t := pattern %type. *)
(* Definition leb (p1 p2:pattern) := *)
(* match p1,p2 with *)
(* | pattern_variant const1 var1, *)
(* pattern_variant const2 var2 => *)
(* lexico_leb const1 const2 *)
(* | pattern_variant const1 var1, _ => true *)
(* | pattern_nil , pattern_variant _ _ => false *)
(* | pattern_nil , _ => true *)
(* | pattern_cons var1 var2 , pattern_variant _ _ => false *)
(* | pattern_cons var1 var2 , pattern_nil => false *)
(* | pattern_cons var1 var2 , _ => true *)
(* | pattern_any, pattern_any => true *)
(* | pattern_any, _ => false *)
(* end. *)
(* Theorem leb_total : forall s1 s2, leb s1 s2 = true \/ leb s2 s1 = true. *)
(* Proof. *)
(* intros p1 p2. *)
(* destruct p1 ; destruct p2 ; unfold leb; auto. *)
(* repeat rewrite lexico_leb_le. *)
(* apply lexico_total. *)
(* Qed. *)
(* End LexicoPattern. *)
(* Module LexicoPatternSort:= Sort LexicoPattern. *)
(* Module LexicoPattern_( T:Typ ) <: TotalLeBool. *)
(* Definition t := (pattern*T.t) %type. *)
(* Definition leb (p1 p2:(pattern*T.t)) := *)
(* let '(p1,_) := p1 in *)
(* let '(p2,_) := p2 in *)
(* LexicoPattern.leb p1 p2. *)
(* Theorem leb_total : forall s1 s2, leb s1 s2 = true \/ leb s2 s1 = true. *)
(* Proof. *)
(* intros p1 p2. *)
(* destruct p1 ; destruct p2 ; unfold leb; auto. *)
(* apply LexicoPattern.leb_total. *)
(* Qed. *)
(* End LexicoPattern_. *)
Module Ins <: Equalities.Typ .
Definition t := instruction.
End Ins.
Module Rhs <: Equalities.Typ .
Definition t := rhs.
End Rhs.
(* Module LexicoPatternIns_Sort. *)
(* Module LexPat := (LexicoPattern_ Ins). *)
(* Include Sort LexPat. *)
(* End LexicoPatternIns_Sort. *)
(* Module LexicoPatternRHS_Sort. *)
(* Module LexPat := (LexicoPattern_ Rhs). *)
(* Include Sort LexPat. *)
(* End LexicoPatternRHS_Sort. *)
Module LexicoOrderIns <: TotalLeBool.
Definition t := (string * label * instruction)%type.
Definition leb := @lexico_leb_triple label instruction.
......
This diff is collapsed.
......@@ -23,191 +23,17 @@ Module Context.
Michocoq.error.Failed syntax_type.type (Michocoq.error.Typing _ "contract typing not supported" ).
End Context.
(* Module comp := Michocomp ST Context. Import comp. *)
Open Scope string.
(* Albert value -> Michelson data *)
(* Definition michelson_of_record := Eval compute in (michelson_data_of_val (val_rval (rval_record (("b", (val_num (numval_int 1%Z)))::("a", val_num (numval_int 2%Z))::nil)))). *)
(* Goal michelson_of_record = Return concrete_data (Pair (Int_constant 2) (Int_constant 1)). *)
(* reflexivity. *)
(* Qed. *)
(* Definition michelson_of_variant := Eval compute in (michelson_data_of_val (val_constr "B" (val_num (numval_int 42%Z)) (vty_variant (("A", ty_int)::("B", ty_int)::("C", ty_nat)::nil)))). *)
(* Goal michelson_of_variant = Return concrete_data (Right (Left (Int_constant 42))). *)
(* reflexivity. *)
(* Qed. *)
(* Albert -> Michelson type *)
Definition michelson_of_nil_rty := Eval compute in (michelson_type_of_type (ty_rty (rty_record nil))).
Goal michelson_of_nil_rty = Return type unit.
reflexivity.
Qed.
(* Definition michelson_of_rty := Eval compute in (michelson_type_of_type (ty_rty (rty_record (("c", ty_nat)::("b", ty_mutez)::("a", ty_int)::nil)))). *)
(* Goal michelson_of_rty = Return type (pair (Comparable_type nat) (pair (Comparable_type mutez) (Comparable_type int))). *)
(* reflexivity. *)
(* Qed. *)
(* Definition michelson_of_vty_option := Eval compute in (michelson_type_of_type (ty_vty (vty_variant (("None", ty_unit)::("Some", ty_nat)::nil)))). *)
(* Goal michelson_of_vty_option = Return type (option (Comparable_type nat)). *)
(* reflexivity. *)
(* Qed. *)
(* Definition michelson_of_vty := Eval compute in (michelson_type_of_type (ty_vty (vty_variant (("A", ty_unit)::("B", ty_nat)::nil)))). *)
(* Goal michelson_of_vty = Return type (or unit (Comparable_type nat)). *)
(* reflexivity. *)
(* Qed. *)
(* Compiler tests *)
Definition startStack := ("b"::"m"::"or"::"v"::"x"::"y"::"z"::nil).
(* Definition startType := rty_record (("b", ty_bool) *)
(* ::("m", ty_mutez) *)
(* ::("or", ty_or ty_int ty_nat) *)
(* ::("v", ty_vty (vty_variant (("A", ty_int)::("B", ty_int)::("C", ty_int)::nil))) *)
(* ::("x", ty_int) *)
(* ::("y", ty_nat) *)
(* ::("z", ty_rty (rty_record (("a", ty_int)::("b", ty_mutez)::("c", ty_int)::nil)))::nil). *)
Import untyped_syntax.
Notation "UNPAIR%" := (SEQ DUP (SEQ CAR (DIP CDR))).
Definition type_and_compile ins rt ll := type_and_compile ins rt ll (* nil *).
(* Definition assign_add := Eval compute in (type_and_compile (instr_assign (lhs_var "r") (rhs_add "x" "y")) startType startStack). *)
(* Goal assign_add = Return (instruction * Datatypes.list string) (SEQ (SEQ (SEQ (DIG 5) (DIG 5)) ADD) (DUG 3), "b" :: "m" :: "or" :: "r" :: "v" :: "z" :: nil). *)
(* reflexivity. *)
(* Qed. *)
(* Definition assign_projection := Eval compute in (type_and_compile (instr_assign (lhs_var "p") (rhs_projection "z" "b")) startType startStack). *)
(* Goal assign_projection = Return (instruction * Datatypes.list string) (SEQ (SEQ (DIG 6) (SEQ CDR CAR)) (DUG 3), "b" :: "m" :: "or" :: "p" :: "v" :: "x" :: "y" :: nil). *)
(* reflexivity. *)
(* Qed. *)
(* Definition assign_update := Eval compute in (type_and_compile (instr_assign (lhs_var "p") (rhs_update "z" (("b", "m")::("c","x")::nil))) startType startStack). *)
(* Goal assign_update = *)
(* Return (instruction * Datatypes.list string) *)
(* (SEQ *)
(* (SEQ (DIG 6) *)
(* (SEQ (SEQ DUP (SEQ CAR (DIP 1 CDR))) *)
(* (SEQ (DIP 1 (SEQ (SEQ DUP (SEQ CAR (DIP 1 CDR))) (SEQ (DROP 1) (SEQ (DIG 2) (SEQ (DIP 1 (SEQ (DROP 1) (DIG 3))) PAIR))))) PAIR))) *)
(* (DUG 2), "b" :: "or" :: "p" :: "v" :: "y" :: nil). *)
(* reflexivity. *)
(* Qed. *)
(* Definition assign_lhs_record := Eval compute in (type_and_compile (instr_assign (lhs_record (("b","d")::("a", "c")::nil)) (rhs_arg (arg_var "z"))) startType startStack). *)
(* Goal assign_lhs_record = *)
(* Return (instruction * Datatypes.list string) *)
(* (SEQ (DIG 6) (SEQ (SEQ DUP (SEQ CAR (DIP 1 CDR))) (SEQ (DUG 2) (DUG 1))), "b" :: "c" :: "d" :: "m" :: "or" :: "v" :: "x" :: "y" :: nil). *)
(* reflexivity. *)
(* Qed. *)
(* Definition assign_rhs_record:= Eval compute in (type_and_compile (instr_assign (lhs_var "r") (rhs_arg (arg_record (("a1", "x")::("a2","z")::nil)))) startType startStack). *)
(* Goal assign_rhs_record = *)
(* Return (instruction * Datatypes.list string) (SEQ (SEQ (SEQ (DIG 6) (DIG 5)) PAIR) (DUG 3), "b" :: "m" :: "or" :: "r" :: "v" :: "y" :: nil). *)
(* reflexivity. *)
(* Qed. *)
(* Definition drop := Eval compute in (type_and_compile (instr_drop "y") startType startStack). *)
(* Goal drop = *)
(* Return (instruction * Datatypes.list string) (SEQ (DIG 5) (DROP 1), "b" :: "m" :: "or" :: "v" :: "x" :: "z" :: nil). *)
(* reflexivity. *)
(* Qed. *)
(* Definition assign_dup:= Eval compute in (type_and_compile (instr_assign (lhs_var "v2") (rhs_app fun_dup (arg_var "y"))) startType startStack). *)
(* Goal assign_dup = *)
(* Return (instruction * Datatypes.list string) (SEQ (SEQ (DIG 5) (SEQ DUP PAIR)) (DUG 4), "b" :: "m" :: "or" :: "v" :: "v2" :: "x" :: "z" :: nil). *)
(* reflexivity. *)
(* Qed. *)
(* Definition assign_fun_app := Eval compute in (type_and_compile (instr_assign (lhs_var "v2") (rhs_app (fun_constr "B" (vty_variant (("A", ty_int)::("B", ty_int)::("C", ty_int)::nil))) (arg_var "x"))) startType startStack). *)
(* Goal assign_fun_app = *)
(* Return (instruction * Datatypes.list string) *)
(* (SEQ (SEQ (DIG 4) (SEQ (LEFT (Comparable_type int)) (RIGHT (Comparable_type int)))) (DUG 4), "b" :: "m" :: "or" :: "v" :: "v2" :: "y" :: "z" :: nil). *)
(* reflexivity. *)
(* Qed. *)
(* Definition assign_option := Eval compute in (type_and_compile (instr_assign (lhs_var "opt") (rhs_app (fun_constr "Some" (vty_variant (("None", ty_unit)::("Some", ty_int)::nil))) (arg_var "x"))) startType startStack). *)
(* Goal assign_option = *)
(* Return (instruction * Datatypes.list string) (SEQ (SEQ (DIG 4) SOME) (DUG 2), "b" :: "m" :: "opt" :: "or" :: "v" :: "y" :: "z" :: nil). *)
(* reflexivity. *)
(* Qed. *)
(* Definition assign_match_variant := Eval compute in (type_and_compile *)
(* (instr_assign (lhs_var "res") *)
(* (rhs_match "v" (branchesrhs_branches *)
(* ((pattern_variant "A" "i", (rhs_arg (arg_var "i"))) *)
(* ::(pattern_variant "B" "i", (rhs_arg (arg_var "i"))) *)
(* ::(pattern_variant "C" "i", (rhs_arg (arg_var "i")))::nil)))) *)
(* startType startStack). *)
(* Goal assign_match_variant = *)
(* Return (instruction * Datatypes.list string) *)
(* (SEQ (SEQ (DIG 3) (IF_LEFT (DIG 0) (SEQ (DIG 3) (IF_LEFT (DIG 0) (DIG 0))))) (DUG 3), "b" :: "m" :: "or" :: "res" :: "x" :: "y" :: "z" :: nil). *)
(* reflexivity. *)
(* Qed. *)
(* Definition match_variant := Eval compute in *)
(* (type_and_compile *)
(* (instr_match "v" ( branchesins_branches ( *)
(* (pattern_variant "A" "i", (instr_seq (instr_drop "x") (instr_assign (lhs_var "r") (rhs_arg (arg_var "i"))))) *)
(* ::(pattern_variant "B" "i", (instr_seq (instr_drop "i") (instr_assign (lhs_var "r") (rhs_arg (arg_var "x"))))) *)
(* ::(pattern_variant "C" "i", (instr_seq (instr_drop "x")(instr_assign (lhs_var "r") (rhs_arg (arg_var "i")))))::nil))) *)
(* startType startStack). *)
(* Goal match_variant = *)
(* Return (instruction * Datatypes.list string) *)
(* (SEQ (DIG 3) *)
(* (IF_LEFT (SEQ (DUG 1) (SEQ (SEQ (DIG 4) (DROP 1)) (SEQ (DIG 1) (DUG 3)))) *)
(* (SEQ (DIG 3) *)
(* (IF_LEFT (SEQ (DUG 1) (SEQ (SEQ (DIG 1) (DROP 1)) (SEQ (DIG 3) (DUG 3)))) (SEQ (DUG 1) (SEQ (SEQ (DIG 4) (DROP 1)) (SEQ (DIG 1) (DUG 3))))))), *)
(* "b" :: "m" :: "or" :: "r" :: "y" :: "z" :: nil). *)
(* reflexivity. *)
(* Qed. *)
(* Definition loop_left := Eval compute in *)
(* (type_and_compile *)
(* (instr_loop_left "or" "o" (instr_assign (lhs_var "or") *)
(* (rhs_app (fun_constr "Left" (vty_variant (("Left", ty_int)::("Right", ty_nat)::nil))) *)
(* (arg_var "o")))) *)
(* startType startStack). *)
(* Goal loop_left = *)
(* Return (instruction * Datatypes.list string) *)
(* (SEQ (SEQ (DIG 2) (LOOP_LEFT (SEQ (DUG 2) (SEQ (SEQ (SEQ (DIG 2) (LEFT (Comparable_type nat))) (DUG 2)) (DIG 2))))) (DROP 1), *)
(* "b" :: "m" :: "v" :: "x" :: "y" :: "z" :: nil). *)
(* reflexivity. *)
(* Qed. *)
(* Definition loop_bool := Eval compute in *)
(* (type_and_compile *)
(* (instr_loop "b" (instr_assign (lhs_var "b") *)
(* (rhs_app (fun_constr "True" (vty_variant (("False", ty_unit)::("True", ty_unit)::nil))) *)
(* (arg_value (val_rval (rval_record nil)))))) *)
(* startType startStack). *)
(* Goal loop_bool = *)
(* Return (instruction * Datatypes.list string) *)
(* (SEQ (DIG 0) (LOOP (SEQ (SEQ (SEQ (PUSH unit Unit) (SEQ (DROP 1) (PUSH (Comparable_type bool) True_))) (DUG 0)) (DIG 0))), *)
(* "m" :: "or" :: "v" :: "x" :: "y" :: "z" :: nil). *)
(* reflexivity. *)
(* Qed. *)
(* Definition type_and_fun_def := Eval compute in *)
(* (type_and_compile_prog ( *)
(* (prog_defs (def_tdef "int" ty_int) *)
(* (prog_defs (def_tdef "int+nat" (ty_vty (vty_variant (("A", (ty_var "int"))::("B", ty_nat)::nil)))) *)
(* (prog_defs (def_fdef "f0" (ty_rty (rty_record (("i", ty_int)::nil))) *)
(* (ty_rty (rty_record (("v", (ty_var "int+nat"))::nil))) *)
(* (instr_assign (lhs_var "v") (rhs_app (fun_constr "A" (vty_variant (("A", ty_int)::("B", ty_nat)::nil))) (arg_var "i")))) *)
(* (prog_def (def_fdef "f1" (ty_rty (rty_record (("a", ty_int)::("ri", (ty_rty (rty_record (("i", ty_int)::nil))))::nil))) *)
(* (ty_rty (rty_record (("a", ty_int)::("rv", (ty_rty (rty_record (("v", (ty_var "int+nat"))::nil))))::nil))) *)
(* (instr_assign (lhs_var "rv") (rhs_app (fun_var "f0") (arg_var "ri")))) *)
(* )))))). *)
(* Goal type_and_fun_def = *)
(* Return (Datatypes.list (string * type * instruction * type)) *)
(* (("f0", Comparable_type int, LEFT (Comparable_type nat), or (Comparable_type int) (Comparable_type nat)) *)
(* :: ("f1", pair (Comparable_type int) (Comparable_type int), *)
(* SEQ (SEQ DUP (SEQ CAR (DIP 1 CDR))) (SEQ (SEQ (DIG 1) (LEFT (Comparable_type nat))) (SEQ (DIG 1) PAIR)), *)
(* pair (Comparable_type int) (or (Comparable_type int) (Comparable_type nat))) :: nil). *)
(* reflexivity. *)
(* Qed. *)
End Tests.
(* Require Import String. *)
(* (** Arithmetics *) *)
(* Inductive arith_op : Set := *)
(* | Add | Sub | Mul | Div | Rem | And | Or | Xor | Lsl | Lsr. *)
(* Definition not_num (nv:num_val) : num_val := nv. (* TODO *) *)
(* Definition bin_arith (op:arith_op) (nv1:num_val) (nv2:num_val) : num_val := nv1. (* TODO *) *)
(* Definition abs (nv:num_val) : num_val := nv. (* TODO *) *)
(* (** Comparisons *) *)
(* Inductive cmp_op : Set := *)
(* | Eq | Neq | Inf | Sup | InfEq | SupEq. *)
(* Axiom compare_num : cmp_op -> num_val -> num_val -> Prop. *)
(* Axiom compare_str : cmp_op -> string_val -> string_val -> Prop. *)
(* Axiom compare_bytes : cmp_op -> bytes_val -> bytes_val -> Prop. *)
(* (* String operations *) *)
(* Definition slice (nv1:num_val) (nv2:num_val) (s:string) := s. (* TODO *) *)
(* (* Bytes operations *) *)
(* Definition pack (_:value) : string_val := EmptyString. (* TODO *) *)
(* Definition unpack (s:string_val) : value := (val_rval (rval_record nil)). (* TODO *) *)
(* (* Domain specific operations *) *)
(* Definition get_contract (a:add_val) : add_val := a. (* TODO *) *)
(* Definition get_address (a:add_val) : add_val := a. (* TODO *) *)
(* Definition get_implicit_account (a:add_val) : add_val := a. (* TODO *) *)
......@@ -11,33 +11,8 @@ Fixpoint string_of_type (t:ty) : string :=
++(String.concat ";" (List.map (fun '(l, t) => (l++":"++(string_of_type t))) rt))
++" }"
| ty_var v => v
(* | ty_nat => "nat" | ty_int => "int" | ty_mutez => "mutez" | ty_timestamp => "timestamp" *)
(* | ty_unit => "unit" *)
(* | ty_prod ty1 ty2 => "("++(string_of_type ty1)++"*"++(string_of_type ty2)++")" *)
(* | ty_vty (vty_variant vt) => "[ " *)
(* ++(String.concat ";" (List.map (fun '(l, t) => (l++":"++(string_of_type t))) vt)) *)
(* ++" ]" *)
(* | ty_option ty => "(option "++(string_of_type ty)++")" *)
(* | ty_or ty1 ty2 => "("++(string_of_type ty1)++"+"++(string_of_type ty2)++")" *)
(* | ty_bool => "bool" *)
(* | ty_string => "string" | ty_bytes => "bytes" *)
(* | ty_list ty => "(list "++(string_of_type ty)++")" *)
(* | ty_map ty ty' => "(map "++(string_of_type ty)++" "++(string_of_type ty')++")" *)
(* | ty_big_map ty ty' => "(bigmap "++(string_of_type ty)++" "++(string_of_type ty')++")" *)
(* | ty_operation => "operation" | ty_key_hash => "key_hash" | ty_address => "address" *)
(* | ty_contract ty => "(contract "++(string_of_type ty)++")" *)
(* | ty_key => "key" *)
(* | ty_signature => "signature" *)
end.
(* Fixpoint string_of_pattern (pat:pattern) : string := *)
(* match pat with *)
(* | pattern_any => "_" *)
(* | pattern_variant constructor5 var => constructor5++