Require dexter_definition.
Require dexter_addlqt_string.

(*! Parser helpers !*)

Require parser_helpers.
Require error.
Import error.Notations.

Import List.ListNotations.
Open Scope list.

(* instruction *)

Definition instr_from_typer_result' s self_type A B :
  error.M (sigT (fun b => typer.instruction self_type b A B)) :=
  parser_helpers.michelson_type_checked_M
               s 100 self_type A B.

Definition instr_from_sig_to_error' self_type A B
  (v : (sigT (fun b => typer.instruction self_type b A B))) :
  error.M (typer.instruction self_type false A B) :=
  match v  with
  | existT _ true code => error.Failed _ (error.Assertion_Failure _ tt)
  | existT _ false code => error.Return code
  end.

Definition m_instr_from_string' s self_type A B:
  error.M (typer.instruction self_type false A B) :=
  let! v := instr_from_typer_result' s self_type A B in
  let! v' := instr_from_sig_to_error' self_type A B v in
  error.Return v'.


(* instruction_seq *)

Definition instr_seq_from_typer_result' s self_type A B :
  error.M (sigT (fun b => typer.instruction_seq self_type b A B)) :=
  parser_helpers.michelson_type_checked_seq_M
    s 100 self_type A B.

Definition instr_seq_from_sig_to_error' self_type A B
           (v : (sigT (fun b => typer.instruction_seq self_type b A B))) :
  error.M (typer.instruction_seq self_type false A B) :=
  match v  with
  | existT _ true code => error.Failed _ (error.Assertion_Failure _ tt)
  | existT _ false code => error.Return code
  end.

Definition m_instr_seq_from_string' s self_type A B:
  error.M (typer.instruction_seq self_type false A B) :=
  let! v := instr_seq_from_typer_result' s self_type A B in
  let! v' := instr_seq_from_sig_to_error' self_type A B v in
  error.Return v'.


(*! entrypoint fragments definition !*)

Definition m_ep_addLiquidity1_header :=
  Eval cbv in (m_instr_seq_from_string'
                 dexter_addlqt_string.ep_addLiquidity1_header
                 dexter_definition.self_type
                 (dexter_definition.parameter_ep_addLiquidity_ty
                    :: dexter_definition.storage_ty
                    :: nil)
                 (syntax_type.Comparable_type syntax_type.bool
                    :: dexter_definition.parameter_ep_addLiquidity_ty
                    :: dexter_definition.storage_ty
                    :: nil)
              ).
Definition ep_addLiquidity1_header := Eval cbv in (error.extract m_ep_addLiquidity1_header I).


Definition m_ep_addLiquidity2_no_lqt :=
  Eval cbv in (m_instr_seq_from_string'
                 dexter_addlqt_string.ep_addLiquidity2_no_lqt
                 dexter_definition.self_type
                 (dexter_definition.parameter_ep_addLiquidity_ty
                    :: dexter_definition.storage_ty
                    :: nil)
                 (syntax_type.pair (syntax_type.list syntax_type.operation) dexter_definition.storage_ty :: nil)
              ).
Definition ep_addLiquidity2_no_lqt := Eval cbv in (error.extract m_ep_addLiquidity2_no_lqt I).


Definition m_ep_addLiquidity3_some_lqt :=
  Eval cbv in (m_instr_seq_from_string'
                 dexter_addlqt_string.ep_addLiquidity3_some_lqt
                 dexter_definition.self_type
                 (dexter_definition.parameter_ep_addLiquidity_ty
                    :: dexter_definition.storage_ty
                    :: nil)
                 (syntax_type.pair (syntax_type.list syntax_type.operation) dexter_definition.storage_ty :: nil)).
Definition ep_addLiquidity3_some_lqt := Eval cbv in (error.extract m_ep_addLiquidity3_some_lqt I).


Import syntax.

Open Scope michelson_scope.

Definition ep_addLiquidity_alt :
    typer.instruction dexter_definition.self_type false
                      (dexter_definition.parameter_ep_addLiquidity_ty
                         :: dexter_definition.storage_ty
                         :: nil)
                      (syntax_type.pair
                         (syntax_type.list syntax_type.operation)
                         dexter_definition.storage_ty :: nil) :=
  Instruction_seq
  ( instruction_app
    ep_addLiquidity1_header
    { IF_TRUE ep_addLiquidity2_no_lqt ep_addLiquidity3_some_lqt } ).

Lemma ep_addLiquidity_alt_ok :
  ep_addLiquidity_alt = dexter_definition.ep_addLiquidity.
Proof.
  reflexivity.
Qed.