Require Import Ascii String List.
Require Import List.
Import ListNotations.
Require Import untyped_syntax micheline_syntax error location.
Require Import syntax_type.
Require Import Lia.
Require Import trie.
Require micheline_lexer.
Require Coq.Program.Wf.
Import error.Notations.
Import untyped_syntax.notations.
Open Scope string.

Inductive string_literal :=
| S_ABS
| S_ADD
| S_ADDRESS
| S_AMOUNT
| S_AND
| S_APPLY
| S_ASSERT
| S_ASSERT_LEFT
| S_ASSERT_NONE
| S_ASSERT_RIGHT
| S_ASSERT_SOME
| S_BALANCE
| S_BLAKE2B
| S_CAR
| S_CAST
| S_CDR
| S_CHAIN_ID
| S_CHECK_SIGNATURE
| S_COMPARE
| S_CONCAT
| S_CONS
| S_CONTRACT
| S_CREATE_CONTRACT
| S_DIG
| S_DIP
| S_DROP
| S_DUG
| S_DUP
| S_EDIV
| S_EMPTY_BIG_MAP
| S_EMPTY_MAP
| S_EMPTY_SET
| S_EQ
| S_EXEC
| S_Elt
| S_FAIL
| S_FAILWITH
| S_False
| S_GE
| S_GET
| S_GT
| S_HASH_KEY
| S_IF
| S_IF_CONS
| S_IF_LEFT
| S_IF_NIL
| S_IF_NONE
| S_IF_RIGHT
| S_IF_SOME
| S_IMPLICIT_ACCOUNT
| S_INT
| S_ISNAT
| S_ITER
| S_LAMBDA
| S_LE
| S_LEFT
| S_LOOP
| S_LOOP_LEFT
| S_LSL
| S_LSR
| S_LT
| S_Left
| S_MAP
| S_MEM
| S_MUL
| S_NEG
| S_NEQ
| S_NIL
| S_NONE
| S_NOT
| S_NOW
| S_None
| S_OR
| S_PACK
| S_PAIR
| S_PUSH
| S_Pair
| S_RENAME
| S_RIGHT
| S_Right
| S_SELF
| S_SENDER
| S_SET_DELEGATE
| S_SHA256
| S_SHA512
| S_SIZE
| S_SLICE
| S_SOME
| S_SOURCE
| S_SUB
| S_SWAP
| S_Some
| S_TRANSFER_TOKENS
| S_True
| S_UNIT
| S_UNPACK
| S_UPDATE
| S_Unit
| S_XOR
| S_address
| S_big_map
| S_bool
| S_bytes
| S_chain_id
| S_code
| S_contract
| S_int
| S_key
| S_key_hash
| S_lambda
| S_list
| S_map
| S_mutez
| S_nat
| S_operation
| S_option
| S_or
| S_pair
| S_parameter
| S_set
| S_signature
| S_storage
| S_string
| S_timestamp
| S_unit
| S_ : String.string -> string_literal.

Definition string_literals :=
  [
    ("ABS", S_ABS);
  ("ADD", S_ADD);
  ("ADDRESS", S_ADDRESS);
  ("AMOUNT", S_AMOUNT);
  ("AND", S_AND);
  ("APPLY", S_APPLY);
  ("ASSERT", S_ASSERT);
  ("ASSERT_LEFT", S_ASSERT_LEFT);
  ("ASSERT_NONE", S_ASSERT_NONE);
  ("ASSERT_RIGHT", S_ASSERT_RIGHT);
  ("ASSERT_SOME", S_ASSERT_SOME);
  ("BALANCE", S_BALANCE);
  ("BLAKE2B", S_BLAKE2B);
  ("CAR", S_CAR);
  ("CAST", S_CAST);
  ("CDR", S_CDR);
  ("CHAIN_ID", S_CHAIN_ID);
  ("CHECK_SIGNATURE", S_CHECK_SIGNATURE);
  ("COMPARE", S_COMPARE);
  ("CONCAT", S_CONCAT);
  ("CONS", S_CONS);
  ("CONTRACT", S_CONTRACT);
  ("CREATE_CONTRACT", S_CREATE_CONTRACT);
  ("DIG", S_DIG);
  ("DIP", S_DIP);
  ("DROP", S_DROP);
  ("DUG", S_DUG);
  ("DUP", S_DUP);
  ("EDIV", S_EDIV);
  ("EMPTY_BIG_MAP", S_EMPTY_BIG_MAP);
  ("EMPTY_MAP", S_EMPTY_MAP);
  ("EMPTY_SET", S_EMPTY_SET);
  ("EQ", S_EQ);
  ("EXEC", S_EXEC);
  ("Elt", S_Elt);
  ("FAIL", S_FAIL);
  ("FAILWITH", S_FAILWITH);
  ("False", S_False);
  ("GE", S_GE);
  ("GET", S_GET);
  ("GT", S_GT);
  ("HASH_KEY", S_HASH_KEY);
  ("IF", S_IF);
  ("IF_CONS", S_IF_CONS);
  ("IF_LEFT", S_IF_LEFT);
  ("IF_NIL", S_IF_NIL);
  ("IF_NONE", S_IF_NONE);
  ("IF_RIGHT", S_IF_RIGHT);
  ("IF_SOME", S_IF_SOME);
  ("IMPLICIT_ACCOUNT", S_IMPLICIT_ACCOUNT);
  ("INT", S_INT);
  ("ISNAT", S_ISNAT);
  ("ITER", S_ITER);
  ("LAMBDA", S_LAMBDA);
  ("LE", S_LE);
  ("LEFT", S_LEFT);
  ("LOOP", S_LOOP);
  ("LOOP_LEFT", S_LOOP_LEFT);
  ("LSL", S_LSL);
  ("LSR", S_LSR);
  ("LT", S_LT);
  ("Left", S_Left);
  ("MAP", S_MAP);
  ("MEM", S_MEM);
  ("MUL", S_MUL);
  ("NEG", S_NEG);
  ("NEQ", S_NEQ);
  ("NIL", S_NIL);
  ("NONE", S_NONE);
  ("NOT", S_NOT);
  ("NOW", S_NOW);
  ("None", S_None);
  ("OR", S_OR);
  ("PACK", S_PACK);
  ("PAIR", S_PAIR);
  ("PUSH", S_PUSH);
  ("Pair", S_Pair);
  ("RENAME", S_RENAME);
  ("RIGHT", S_RIGHT);
  ("Right", S_Right);
  ("SELF", S_SELF);
  ("SENDER", S_SENDER);
  ("SET_DELEGATE", S_SET_DELEGATE);
  ("SHA256", S_SHA256);
  ("SHA512", S_SHA512);
  ("SIZE", S_SIZE);
  ("SLICE", S_SLICE);
  ("SOME", S_SOME);
  ("SOURCE", S_SOURCE);
  ("SUB", S_SUB);
  ("SWAP", S_SWAP);
  ("Some", S_Some);
  ("TRANSFER_TOKENS", S_TRANSFER_TOKENS);
  ("True", S_True);
  ("UNIT", S_UNIT);
  ("UNPACK", S_UNPACK);
  ("UPDATE", S_UPDATE);
  ("Unit", S_Unit);
  ("XOR", S_XOR);
  ("address", S_address);
  ("big_map", S_big_map);
  ("bool", S_bool);
  ("bytes", S_bytes);
  ("chain_id", S_chain_id);
  ("code", S_code);
  ("contract", S_contract);
  ("int", S_int);
  ("key", S_key);
  ("key_hash", S_key_hash);
  ("lambda", S_lambda);
  ("list", S_list);
  ("map", S_map);
  ("mutez", S_mutez);
  ("nat", S_nat);
  ("operation", S_operation);
  ("option", S_option);
  ("or", S_or);
  ("pair", S_pair);
  ("parameter", S_parameter);
  ("set", S_set);
  ("signature", S_signature);
  ("storage", S_storage);
  ("string", S_string);
  ("timestamp", S_timestamp);
  ("unit", S_unit)
  ].

Definition string_literal_dict_aux : String.string -> Datatypes.option string_literal :=
  Eval cbv in
    extract (dict string_literals 1000) I.

Definition make_string_literal (s : String.string) : string_literal :=
  match string_literal_dict_aux s with
  | Some l => l
  | None => S_ s
  end.

Definition loc_pmicheline := loc_gmicheline string_literal.

Definition to_pmicheline := map_gmicheline make_string_literal.

Definition micheline2michelson_sctype (bem : loc_pmicheline) : M simple_comparable_type :=
  let 'Mk_loc_micheline ((b, e), m) := bem in
  match m with
  | PRIM (_, S_string) _ nil => Return string
  | PRIM (_, S_nat) _ nil => Return nat
  | PRIM (_, S_int) _ nil => Return int
  | PRIM (_, S_bytes) _ nil => Return bytes
  | PRIM (_, S_bool) _ nil => Return bool
  | PRIM (_, S_mutez) _ nil => Return mutez
  | PRIM (_, S_key_hash) _ nil => Return key_hash
  | PRIM (_, S_timestamp) _ nil => Return timestamp
  | PRIM (_, S_address) _ nil => Return address
  | _ => Failed _ (Expansion b e)
  end.

Fixpoint micheline2michelson_ctype (bem : loc_pmicheline) : M comparable_type :=
  let 'Mk_loc_micheline ((b, e), m) := bem in
  match m with
  | PRIM (_, S_pair) _ (a :: b :: nil) =>
    let! a := micheline2michelson_sctype a in
    let! b := micheline2michelson_ctype b in
    Return (Cpair a b)
  | _ =>
    let! a := micheline2michelson_sctype bem in
    Return (Comparable_type_simple a)
  end.

Definition extract_one_field_annot_from_list annots : M annot_o :=
  match annots with
  | nil => Return None
  | Mk_annot (_, _, annot) :: nil => Return (Some annot)
  | _ :: Mk_annot (b, e, _) :: _ => Failed _ (Expansion b e)
  end.

Definition is_field_annot annot :=
  match annot with
  | Mk_annot (_, _, EmptyString) => false
  | Mk_annot (_, _, String c _) => micheline_lexer.eqb_ascii c "%"%char
  end.

Definition extract_one_field_annot (bem : loc_pmicheline) : M annot_o :=
  let 'Mk_loc_micheline ((b, e), m) := bem in
  match m with
  | PRIM p annots args =>
    let filtered_annots := List.filter is_field_annot annots in
    extract_one_field_annot_from_list filtered_annots
  | _ => Return None
  end.

Fixpoint micheline2michelson_type (bem : loc_pmicheline) : M type :=
  try (let! ty := micheline2michelson_sctype bem in Return (Comparable_type ty))
      (let 'Mk_loc_micheline ((b, e), m) := bem in
       match m with
       | PRIM (_, S_key) _ nil => Return key
       | PRIM (_, S_unit) _ nil => Return unit
       | PRIM (_, S_signature) _ nil => Return signature
       | PRIM (_, S_operation) _ nil => Return operation
       | PRIM (_, S_chain_id) _ nil => Return chain_id
       | PRIM (_, S_option) _ (a :: nil) =>
        let! a := micheline2michelson_type a in
        Return (option a)
       | PRIM (_, S_list) _ (a :: nil) =>
        let! a := micheline2michelson_type a in
        Return (list a)
       | PRIM (_, S_contract) _ (a :: nil) =>
        let! a := micheline2michelson_type a in
        Return (contract a)
       | PRIM (_, S_set) _ (a :: nil) =>
        let! a := micheline2michelson_ctype a in
        Return (set a)
       | PRIM (_, S_pair) _ (a :: b :: nil) =>
        let! a := micheline2michelson_type a in
        let! b := micheline2michelson_type b in
        Return (pair a b)
       | PRIM (_, S_or) _ (a :: b :: nil) =>
        let! an := extract_one_field_annot a in
        let! bn := extract_one_field_annot b in
        let! a := micheline2michelson_type a in
        let! b := micheline2michelson_type b in
        Return (or a an b bn)
       | PRIM (_, S_lambda) _ (a :: b :: nil) =>
        let! a := micheline2michelson_type a in
        let! b := micheline2michelson_type b in
        Return (lambda a b)
       | PRIM (_, S_map) _ (a :: b :: nil) =>
        let! a := micheline2michelson_ctype a in
        let! b := micheline2michelson_type b in
        Return (map a b)
       | PRIM (_, S_big_map) _ (a :: b :: nil) =>
        let! a := micheline2michelson_ctype a in
        let! b := micheline2michelson_type b in
        Return (big_map a b)
       | _ => Failed _ (Expansion b e)
       end).

Fixpoint micheline2michelson_data (bem : loc_pmicheline) : M concrete_data :=
  let 'Mk_loc_micheline ((b, e), m) := bem in
  match m with
  | SEQ l =>
    let! l :=
      (fix micheline2michelson_data_list (l : Datatypes.list loc_pmicheline) : M (Datatypes.list concrete_data) :=
        match l with
        | nil => Return nil
        | m :: l =>
          let! d := micheline2michelson_data m in
          let! l := micheline2michelson_data_list l in
          Return (d :: l)
        end
      ) l in
    Return (Concrete_seq l)
  | STR s => Return (String_constant s)
  | NUMBER z => Return (Int_constant z)
  | BYTES s => Return (Bytes_constant s)
  | PRIM (_, S_Unit) _ nil => Return Unit
  | PRIM (_, S_True) _ nil => Return True_
  | PRIM (_, S_False) _ nil => Return False_
  | PRIM (_, S_Pair) _ (a :: b :: nil) =>
    let! a := micheline2michelson_data a in
    let! b := micheline2michelson_data b in
    Return (Pair a b)
  | PRIM (_, S_Elt) _ (a :: b :: nil) =>
    let! a := micheline2michelson_data a in
    let! b := micheline2michelson_data b in
    Return (Elt a b)
  | PRIM (_, S_Left) _ (a :: nil) =>
    let! a := micheline2michelson_data a in
    Return (Left a)
  | PRIM (_, S_Right) _ (a :: nil) =>
    let! a := micheline2michelson_data a in
    Return (Right a)
  | PRIM (_, S_Some) _ (a :: nil) =>
    let! a := micheline2michelson_data a in
    Return (Some_ a)
  | PRIM (_, S_None) _ nil => Return None_
  | PRIM _ _ _ => Failed _ (Expansion b e)
  end.

Definition op_of_string (s : string_literal) b e :=
  match s with
  | S_EQ => Return EQ
  | S_NEQ => Return NEQ
  | S_LE => Return LE
  | S_GE => Return GE
  | S_LT => Return LT
  | S_GT => Return GT
  | _ => Failed _ (Expansion b e)
  end.

Definition FAIL := Instruction_seq {UNIT; FAILWITH}.
Definition ASSERT := Instruction_seq {IF_ IF_bool {} {FAIL}}.

Definition IF_op_of_string (s : String.string) b e bt bf :=
  match s with
  | String "I" (String "F" s) =>
    let s := make_string_literal s in
    let! op := op_of_string s b e in
    Return (op ;; IF_ IF_bool bt bf ;; NOOP)
  | _ => Failed _ (Expansion b e)
  end.

Definition ASSERT_op_of_string (s : String.string) b e :=
  match s with
  | String "A" (String "S" (String "S" (String "E" (String "R" (String "T" (String "_" s)))))) =>
    let s := make_string_literal s in
    let! op := op_of_string s b e in
    Return (op ;; ASSERT ;; NOOP)
  | _ => Failed _ (Expansion b e)
  end.

Definition ASSERT_NONE := Instruction_seq {IF_NONE {} {FAIL}}.
Definition ASSERT_SOME := Instruction_seq {IF_NONE {FAIL} {}}.
Definition ASSERT_LEFT := Instruction_seq {IF_LEFT {} {FAIL}}.
Definition ASSERT_RIGHT := Instruction_seq {IF_LEFT {FAIL} {}}.

Fixpoint DUP_Sn n : instruction_seq :=
  match n with
  | 0 => {DUP}
  | S n => {DIP 1 (DUP_Sn n); SWAP}
  end.

Definition IF_SOME bt bf := Instruction_seq {IF_NONE bf bt}.
Definition IF_RIGHT bt bf := Instruction_seq {IF_LEFT bf bt}.
Definition IF_NIL bt bf := Instruction_seq {IF_CONS bf bt}.

Inductive cadr : Set :=
| Cadr_CAR : cadr -> cadr
| Cadr_CDR : cadr -> cadr
| Cadr_nil : cadr.

Fixpoint micheline2michelson_cadr (x : cadr) : instruction_seq :=
  match x with
  | Cadr_CAR x => CAR ;; micheline2michelson_cadr x
  | Cadr_CDR x => CDR ;; micheline2michelson_cadr x
  | Cadr_nil => {}
  end.

Fixpoint micheline2michelson_set_cadr (x : cadr) : instruction_seq :=
  match x with
  | Cadr_CAR Cadr_nil =>
    {CDR; SWAP; PAIR}
  | Cadr_CDR Cadr_nil =>
    {CAR; PAIR}
  | Cadr_CAR x =>
    {DUP; DIP 1 (CAR;; micheline2michelson_set_cadr x); CDR; SWAP; PAIR}
  | Cadr_CDR x =>
    {DUP; DIP 1 (CDR;; micheline2michelson_set_cadr x); CAR; PAIR}
  | Cadr_nil => {} (* Should not happen *)
  end.

Fixpoint micheline2michelson_map_cadr (x : cadr) (code : instruction_seq) : instruction_seq :=
  match x with
  | Cadr_CAR Cadr_nil =>
    {DUP; CDR; DIP 1 (CAR;; code); SWAP; PAIR}
  | Cadr_CDR Cadr_nil =>
    {DUP; CDR} ;;; code ;;; {SWAP; CAR; PAIR}
  | Cadr_CAR x =>
    {DUP; DIP 1 (CAR;; micheline2michelson_map_cadr x code); CDR; SWAP; PAIR}
  | Cadr_CDR x =>
    {DUP; DIP 1 (CDR;; micheline2michelson_map_cadr x code); CAR; PAIR}
  | Cadr_nil => code (* Should not happen *)
  end.

(* PAPAIR stuff *)

Inductive direction := Left | Right.

Inductive papair_token := token_P | token_A | token_I.

Fixpoint lex_papair (s : String.string) (fail : exception) :
  M (Datatypes.list papair_token) :=
  match s with
  | String "P" s =>
    let! l := lex_papair s fail in
    Return (cons token_P l)
  | String "A" s =>
    let! l := lex_papair s fail in
    Return (cons token_A l)
  | String "I" s =>
    let! l := lex_papair s fail in
    Return (cons token_I l)
  | "R"%string => Return nil
  | _ => Failed _ fail
  end.

Inductive papair_d : direction -> Set :=
| Papair_d_P d : papair_d Left -> papair_d Right -> papair_d d
| Papair_d_A : papair_d Left
| Papair_d_I : papair_d Right.

Fixpoint parse_papair (d : direction) (s : Datatypes.list papair_token) (fail : exception)
         (fuel : Datatypes.nat) (Hs : List.length s < fuel) {struct fuel} :
  M (papair_d d * sig (fun r : Datatypes.list papair_token => List.length r < List.length s)).
Proof.
  destruct fuel.
  - destruct (PeanoNat.Nat.nlt_0_r _ Hs).
  - destruct s as [|c s].
    + exact (Failed _ fail).
    + refine (match c, d
              return M (papair_d d *
                        (sig (fun r : Datatypes.list papair_token => List.length r < S (List.length s))))
              with
              | token_P, d1 =>
                let! (l, exist _ s1 Hl) := parse_papair Left s fail fuel _ in
                let! (r, exist _ s2 Hr) := parse_papair Right s1 fail fuel _ in
                Return (Papair_d_P d l r, exist _ s2 _)
              | token_A, Left => Return (Papair_d_A, exist _ s _)
              | token_I, Right => Return (Papair_d_I, exist _ s _)
              | _, _ => Failed _ fail
              end); simpl in *; lia.
Defined.

Inductive papair_left : Set :=
| Papair_l_P : papair_left -> papair_right -> papair_left
| Papair_l_A : papair_left
with papair_right : Set :=
| Papair_r_P : papair_left -> papair_right -> papair_right
| Papair_r_I : papair_right.

Fixpoint papair_l_of_papair_d (x : papair_d Left) : papair_left :=
  match x in papair_d Left return papair_left with
  | Papair_d_A => Papair_l_A
  | Papair_d_P Left l r =>
    Papair_l_P (papair_l_of_papair_d l) (papair_r_of_papair_d r)
  end
with
papair_r_of_papair_d (x : papair_d Right) : papair_right :=
  match x in papair_d Right return papair_right with
  | Papair_d_I => Papair_r_I
  | Papair_d_P Right l r =>
    Papair_r_P (papair_l_of_papair_d l) (papair_r_of_papair_d r)
  end.

Fixpoint size_l (x : papair_left) :=
  match x with
  | Papair_l_A => 0
  | Papair_l_P l r => 1 + size_l l + size_r r
  end
with
size_r (y : papair_right) :=
  match y with
  | Papair_r_I => 0
  | Papair_r_P l r => 1 + size_l l + size_r r
  end.

Inductive papair : Set :=
| Papair_PAIR : papair
| Papair_A : papair -> papair
| Papair_I : papair -> papair
| Papair_P : papair -> papair -> papair.

Program Fixpoint papair_of_l_r (x : papair_left) (y : papair_right) {measure (size_l x + size_r y)}: papair :=
  match x, y with
  | Papair_l_A, Papair_r_I => Papair_PAIR
  | Papair_l_A, Papair_r_P l r =>
    Papair_A (papair_of_l_r l r)
  | Papair_l_P l r, Papair_r_I =>
    Papair_I (papair_of_l_r l r)
  | Papair_l_P xl xr, Papair_r_P yl yr =>
    Papair_P (papair_of_l_r xl xr) (papair_of_l_r yl yr)
  end.
Next Obligation.
  simpl.
  lia.
Defined.
Next Obligation.
  simpl.
  lia.
Defined.
Next Obligation.
  simpl.
  lia.
Defined.

Fixpoint micheline2michelson_papair (x : papair) : instruction_seq :=
  match x with
  | Papair_PAIR => {PAIR}
  | Papair_A y => {DIP 1 (micheline2michelson_papair y); PAIR}
  | Papair_I x => micheline2michelson_papair x ;;; {PAIR}
  | Papair_P x y => micheline2michelson_papair x ;;;
                    {DIP 1 (micheline2michelson_papair y); PAIR}
  end.

Fixpoint micheline2michelson_unpapair (x : papair) : instruction :=
  match x with
  | Papair_PAIR => UNPAIR
  | Papair_A y => Instruction_seq {UNPAIR; DIP 1 { micheline2michelson_unpapair y }}
  | Papair_I x => Instruction_seq {UNPAIR; micheline2michelson_unpapair x}
  | Papair_P x y => Instruction_seq {UNPAIR;
                    DIP 1 {micheline2michelson_unpapair y};
                    micheline2michelson_unpapair x}
  end.

Definition parse_papair_full (s : String.string) (fail : exception) :
  M instruction_seq :=
  let! toks : Datatypes.list papair_token := lex_papair s fail in
  let! (l, exist _ toks2 Htoks2) := parse_papair Left toks fail (S (List.length toks)) ltac:(simpl; lia) in
  let! (r, exist _ toks3 Htoks3) := parse_papair Right toks2 fail (S (List.length toks2)) ltac:(simpl; lia) in
  match toks3 with
  | nil => Return
                  (micheline2michelson_papair
                      (papair_of_l_r
                        (papair_l_of_papair_d l)
                        (papair_r_of_papair_d r)))
  | _ => Failed _ fail
  end.

Definition parse_unpapair_full (s : String.string) (fail : exception)
  : M instruction :=
  let! toks : Datatypes.list papair_token := lex_papair s fail in
  let! (l, exist _ toks2 Htoks2) := parse_papair Left toks fail (S (List.length toks)) ltac:(simpl; lia) in
  let! (r, exist _ toks3 Htoks3) := parse_papair Right toks2 fail (S (List.length toks2)) ltac:(simpl; lia) in
  match toks3 with
  | nil => Return
                  (micheline2michelson_unpapair
                      (papair_of_l_r
                        (papair_l_of_papair_d l)
                        (papair_r_of_papair_d r)))
  | _ => Failed _ fail
  end.


Definition return_instruction (i : instruction) : M instruction_seq :=
  Return {i}%michelson_untyped.

Definition return_opcode (op : opcode) : M instruction_seq :=
  return_instruction (instruction_opcode op).

Definition return_macro (i : instruction_seq) : M instruction_seq :=
  return_instruction (Instruction_seq i).

Fixpoint micheline2michelson_instruction (bem : loc_pmicheline) : M instruction_seq :=
  let 'Mk_loc_micheline ((b, e), m) := bem in
  match m with
  | SEQ l =>
    (fix micheline2michelson_instr_seq (l : Datatypes.list loc_pmicheline) : M instruction_seq :=
       match l with
       | nil => Return NOOP
       | i1 :: i2 =>
        let! i1 := micheline2michelson_instruction i1 in
        let! i2 := micheline2michelson_instr_seq i2 in
        Return (i1 ;;; i2)
       end) l
  | PRIM (_, S_FAILWITH) _ nil => return_instruction FAILWITH
  | PRIM (_, S_EXEC) _ nil => return_instruction EXEC
  | PRIM (_, S_APPLY) _ nil => return_opcode APPLY
  | PRIM (_, S_DROP) _ nil => return_opcode (DROP 1)
  | PRIM (_, S_DROP) _ (Mk_loc_micheline (_, NUMBER n) :: nil) =>
    return_opcode (DROP (BinInt.Z.to_nat n))
  | PRIM (_, S_DUP) _ nil => return_opcode DUP
  | PRIM (_, S_SWAP) _ nil => return_opcode SWAP
  | PRIM (_, S_UNIT) _ nil => return_opcode UNIT
  | PRIM (_, S_EQ) _ nil => return_opcode EQ
  | PRIM (_, S_NEQ) _ nil => return_opcode NEQ
  | PRIM (_, S_LT) _ nil => return_opcode LT
  | PRIM (_, S_GT) _ nil => return_opcode GT
  | PRIM (_, S_LE) _ nil => return_opcode LE
  | PRIM (_, S_GE) _ nil => return_opcode GE
  | PRIM (_, S_OR) _ nil => return_opcode OR
  | PRIM (_, S_AND) _ nil => return_opcode AND
  | PRIM (_, S_XOR) _ nil => return_opcode XOR
  | PRIM (_, S_NOT) _ nil => return_opcode NOT
  | PRIM (_, S_NEG) _ nil => return_opcode NEG
  | PRIM (_, S_ABS) _ nil => return_opcode ABS
  | PRIM (_, S_ISNAT) _ nil => return_opcode ISNAT
  | PRIM (_, S_INT) _ nil => return_opcode INT
  | PRIM (_, S_ADD) _ nil => return_opcode ADD
  | PRIM (_, S_SUB) _ nil => return_opcode SUB
  | PRIM (_, S_MUL) _ nil => return_opcode MUL
  | PRIM (_, S_EDIV) _ nil => return_opcode EDIV
  | PRIM (_, S_LSL) _ nil => return_opcode LSL
  | PRIM (_, S_LSR) _ nil => return_opcode LSR
  | PRIM (_, S_COMPARE) _ nil => return_opcode COMPARE
  | PRIM (_, S_CONCAT) _ nil => return_opcode CONCAT
  | PRIM (_, S_SIZE) _ nil => return_opcode SIZE
  | PRIM (_, S_SLICE) _ nil => return_opcode SLICE
  | PRIM (_, S_PAIR) _ nil => return_opcode PAIR
  | PRIM (_, S_CAR) _ nil => return_opcode CAR
  | PRIM (_, S_CDR) _ nil => return_opcode CDR
  | PRIM (_, S_GET) _ nil => return_opcode GET
  | PRIM (_, S_SOME) _ nil => return_opcode SOME
  | PRIM (_, S_NONE) _ (ty :: nil) =>
    let! ty := micheline2michelson_type ty in
    return_opcode (NONE ty)
  | PRIM (_, S_LEFT) _ (ty :: nil) =>
    let! ty := micheline2michelson_type ty in
    return_opcode (LEFT ty)
  | PRIM (_, S_RIGHT) _ (ty :: nil) =>
    let! ty := micheline2michelson_type ty in
    return_opcode (RIGHT ty)
  | PRIM (_, S_CONS) _ nil => return_opcode CONS
  | PRIM (_, S_NIL) _ (ty :: nil) =>
    let! ty := micheline2michelson_type ty in
    return_opcode (NIL ty)
  | PRIM (_, S_TRANSFER_TOKENS) _ nil =>
    return_opcode TRANSFER_TOKENS
  | PRIM (_, S_SET_DELEGATE) _ nil => return_opcode SET_DELEGATE
  | PRIM (_, S_BALANCE) _ nil => return_opcode BALANCE
  | PRIM (_, S_ADDRESS) _ nil => return_opcode ADDRESS
  | PRIM (_, S_CONTRACT) _ (ty :: nil) =>
    let! an := extract_one_field_annot bem in
    let! ty := micheline2michelson_type ty in
    return_opcode (CONTRACT an ty)
  | PRIM (_, S_SOURCE) _ nil => return_opcode SOURCE
  | PRIM (_, S_SENDER) _ nil => return_opcode SENDER
  | PRIM (_, S_SELF) _ nil =>
    let! an := extract_one_field_annot bem in
    return_instruction (SELF an)
  | PRIM (_, S_AMOUNT) _ nil => return_opcode AMOUNT
  | PRIM (_, S_IMPLICIT_ACCOUNT) _ nil => return_opcode IMPLICIT_ACCOUNT
  | PRIM (_, S_NOW) _ nil => return_opcode NOW
  | PRIM (_, S_PACK) _ nil => return_opcode PACK
  | PRIM (_, S_UNPACK) _ (ty :: nil) =>
    let! ty := micheline2michelson_type ty in
    return_opcode (UNPACK ty)
  | PRIM (_, S_HASH_KEY) _ nil => return_opcode HASH_KEY
  | PRIM (_, S_BLAKE2B) _ nil => return_opcode BLAKE2B
  | PRIM (_, S_SHA256) _ nil => return_opcode SHA256
  | PRIM (_, S_SHA512) _ nil => return_opcode SHA512
  | PRIM (_, S_CHECK_SIGNATURE) _ nil =>
    return_opcode CHECK_SIGNATURE
  | PRIM (_, S_MEM) _ nil => return_opcode MEM
  | PRIM (_, S_UPDATE) _ nil => return_opcode UPDATE
  | PRIM (_, S_CHAIN_ID) _ nil => return_opcode CHAIN_ID
  | PRIM (_, S_LOOP) _ (i :: nil) =>
    let! i := micheline2michelson_instruction i in
    return_instruction (LOOP i)
  | PRIM (_, S_LOOP_LEFT) _ (i :: nil) =>
    let! i := micheline2michelson_instruction i in
    return_instruction (LOOP_LEFT i)
  | PRIM (_, S_DIP) _ (i :: nil) =>
    let! i := micheline2michelson_instruction i in
    return_instruction (DIP 1 i)
  | PRIM (_, S_DIP) _ (Mk_loc_micheline (_, NUMBER n) :: i :: nil) =>
    let! i := micheline2michelson_instruction i in
    return_instruction (DIP (BinInt.Z.to_nat n) i)
  | PRIM (_, S_DIG) _ (Mk_loc_micheline (_, NUMBER n) :: nil) =>
    return_opcode (DIG (BinInt.Z.to_nat n))
  | PRIM (_, S_DUG) _ (Mk_loc_micheline (_, NUMBER n) :: nil) =>
    return_opcode (DUG (BinInt.Z.to_nat n))
  | PRIM (_, S_ITER) _ (i :: nil) =>
    let! i := micheline2michelson_instruction i in
    return_instruction (ITER i)
  | PRIM (_, S_MAP) _ (i :: nil) =>
    let! i := micheline2michelson_instruction i in
    return_instruction (MAP i)
  | PRIM (_, S_CREATE_CONTRACT) _
               (Mk_loc_micheline
                  (_, SEQ
                        ((Mk_loc_micheline (_, PRIM (_, S_storage) _ (storage_ty :: nil))) ::
                        (Mk_loc_micheline (_, PRIM (_, S_parameter) _ (params_ty :: nil)) as param) ::
                        (Mk_loc_micheline (_, PRIM (_, S_code) _ (i :: nil))) :: nil)) ::
                  nil) =>
    let! an := extract_one_field_annot param in
    let! i := micheline2michelson_instruction i in
    let! sty := micheline2michelson_type storage_ty in
    let! pty := micheline2michelson_type params_ty in
    return_instruction (CREATE_CONTRACT sty pty an i)
  | PRIM (_, S_CREATE_CONTRACT) _
               (Mk_loc_micheline
                  (_, SEQ
                        ((Mk_loc_micheline (_, PRIM (_, S_parameter) _ (params_ty :: nil)) as param) ::
                        (Mk_loc_micheline (_, PRIM (_, S_storage) _ (storage_ty :: nil))) ::
                        (Mk_loc_micheline (_, PRIM (_, S_code) _ (i :: nil))) :: nil)) ::
                  nil) =>
    let! an := extract_one_field_annot param in
    let! i := micheline2michelson_instruction i in
    let! sty := micheline2michelson_type storage_ty in
    let! pty := micheline2michelson_type params_ty in
    return_instruction (CREATE_CONTRACT sty pty an i)
  | PRIM (_, S_EMPTY_SET) _ (cty :: nil) =>
    let! cty := micheline2michelson_ctype cty in
    return_opcode (EMPTY_SET cty)
  | PRIM (_, S_EMPTY_MAP) _ (kty :: vty :: nil) =>
    let! kty := micheline2michelson_ctype kty in
    let! vty := micheline2michelson_type vty in
    return_opcode (EMPTY_MAP kty vty)
  | PRIM (_, S_EMPTY_BIG_MAP) _ (kty :: vty :: nil) =>
    let! kty := micheline2michelson_ctype kty in
    let! vty := micheline2michelson_type vty in
    return_opcode (EMPTY_BIG_MAP kty vty)
  | PRIM (_, S_IF) _ (i1 :: i2 :: nil) =>
    let! i1 := micheline2michelson_instruction i1 in
    let! i2 := micheline2michelson_instruction i2 in
    return_instruction (IF_ IF_bool i1 i2)
  | PRIM (_, S_IF_NONE) _ (i1 :: i2 :: nil) =>
    let! i1 := micheline2michelson_instruction i1 in
    let! i2 := micheline2michelson_instruction i2 in
    return_instruction (IF_NONE i1 i2)
  | PRIM (_, S_IF_LEFT) _ (i1 :: i2 :: nil) =>
    let! i1 := micheline2michelson_instruction i1 in
    let! i2 := micheline2michelson_instruction i2 in
    return_instruction (IF_LEFT i1 i2)
  | PRIM (_, S_IF_CONS) _ (i1 :: i2 :: nil) =>
    let! i1 := micheline2michelson_instruction i1 in
    let! i2 := micheline2michelson_instruction i2 in
    return_instruction (IF_CONS i1 i2)
  | PRIM (_, S_LAMBDA) _ (a :: b :: i :: nil) =>
    let! a := micheline2michelson_type a in
    let! b := micheline2michelson_type b in
    let! i := micheline2michelson_instruction i in
    return_instruction (LAMBDA a b i)
  | PRIM (_, S_PUSH) _ (a :: v :: nil) =>
    let! a := micheline2michelson_type a in
    let! v :=
      match a with
      | lambda _ _ =>
        let! i := micheline2michelson_instruction v in
        Return (Instruction i)
      | _ => micheline2michelson_data v
      end in
    return_instruction (PUSH a v)

  | PRIM (_, S_RENAME) _ _ => Return NOOP
  | PRIM (_, S_CAST) _ _ => Return NOOP


  (* Macros *)
  | PRIM (_, S_FAIL) _ nil => return_instruction FAIL
  | PRIM (_, S_ASSERT) _ nil => return_instruction ASSERT
  | PRIM (_, S_ASSERT_NONE) _ nil => return_instruction ASSERT_NONE
  | PRIM (_, S_ASSERT_SOME) _ nil => return_instruction ASSERT_SOME
  | PRIM (_, S_ASSERT_LEFT) _ nil => return_instruction ASSERT_LEFT
  | PRIM (_, S_ASSERT_RIGHT) _ nil => return_instruction ASSERT_RIGHT

  | PRIM (_, S_IF_SOME) _ (i1 :: i2 :: nil) =>
    let! i1 := micheline2michelson_instruction i1 in
    let! i2 := micheline2michelson_instruction i2 in
    return_instruction (IF_SOME i1 i2)
  | PRIM (_, S_IF_RIGHT) _ (i1 :: i2 :: nil) =>
    let! i1 := micheline2michelson_instruction i1 in
    let! i2 := micheline2michelson_instruction i2 in
    return_instruction (IF_RIGHT i1 i2)
  | PRIM (_, S_IF_NIL) _ (i1 :: i2 :: nil) =>
    let! i1 := micheline2michelson_instruction i1 in
    let! i2 := micheline2michelson_instruction i2 in
    return_instruction (IF_NIL i1 i2)

  | PRIM (_, S_ (String "C" (String "M" (String "P" s)))) _ nil =>
    let s := make_string_literal s in
    let! op := op_of_string s b e in
    return_macro {COMPARE; op}
  | PRIM (_,
       S_ (String "I" (String "F" (String "C" (String "M" (String "P" s)))))) _ (i1 :: i2 :: nil) =>
    let! i1 := micheline2michelson_instruction i1 in
    let! i2 := micheline2michelson_instruction i2 in
    let s := make_string_literal s in
    let! op := op_of_string s b e in
    return_macro {COMPARE; op; IF_ IF_bool i1 i2}
  | PRIM (_,
       S_ (String "I" (String "F" s))) _ (i1 :: i2 :: nil) =>
    let! i1 := micheline2michelson_instruction i1 in
    let! i2 := micheline2michelson_instruction i2 in
    let s := make_string_literal s in
    let! op := op_of_string s b e in
    return_macro {op; IF_ IF_bool i1 i2}
  | PRIM (_,
          S_ (String "A" (String "S" (String "S" (String "E" (String "R" (String "T"
              (String "_" (String "C" (String "M" (String "P" s))))))))))) _ nil =>
    let s := make_string_literal s in
    let! op := op_of_string s b e in
    return_macro {COMPARE; op; IF_ IF_bool {} {FAIL}}

  | PRIM (_, S_ (String "A" (String "S" (String "S" (String "E" (String "R" (String "T"
                                                                                    (String "_" s)))))))) _ nil =>
    let s := make_string_literal s in
    let! op := op_of_string s b e in
    return_macro {op; IF_ IF_bool {} {FAIL}}

  | PRIM (_, S_ "CR") _ nil =>
    Failed _ (Expansion_prim b e "CR")
  | PRIM (_, S_ "SET_CR") _ nil =>
    Failed _ (Expansion_prim b e "SET_CR")
  | PRIM (_, S_ "MAP_CR") _ nil =>
    Failed _ (Expansion_prim b e "MAP_CR")

  (* CADAAR *)
  | PRIM (_, S_ (String "C" s)) _ nil =>
    let prim := String "C" s in
    let get_cadr := fix get_cadr s :=
                      match s with
                      | "R" => Return Cadr_nil
                      | String "A" s =>
                        let! x := get_cadr s in
                        Return (Cadr_CAR x)
                      | String "D" s =>
                        let! x := get_cadr s in
                        Return (Cadr_CDR x)
                      | _ => Failed _ (Expansion_prim b e prim)
                      end in
    let! x := get_cadr s in
    return_macro (micheline2michelson_cadr x)

  | PRIM (_, S_ (String "S" (String "E"(String "T"(String "_"(String "C" s))))))
         _ nil =>
    let prim := String "S" (String "E"(String "T"(String "_"(String "C" s)))) in
    let get_cadr := fix get_cadr s :=
                      match s with
                      | "R" => Return Cadr_nil
                      | String "A" s =>
                        let! x := get_cadr s in
                        Return (Cadr_CAR x)
                      | String "D" s =>
                        let! x := get_cadr s in
                        Return (Cadr_CDR x)
                      | _ => Failed _ (Expansion_prim b e prim)
                      end in
    let! x := get_cadr s in
    return_macro (micheline2michelson_set_cadr x)

  | PRIM (_, S_ (String "M" (String "A"(String "P"(String "_"(String "C" s))))))
         _ (a :: nil) =>
    let prim := String "M" (String "A"(String "P"(String "_"(String "C" s)))) in
    let get_cadr := fix get_cadr s :=
                      match s with
                      | "R" => Return Cadr_nil
                      | String "A" s =>
                        let! x := get_cadr s in
                        Return (Cadr_CAR x)
                      | String "D" s =>
                        let! x := get_cadr s in
                        Return (Cadr_CDR x)
                      | _ => Failed _ (Expansion_prim b e prim)
                      end in
    let! x := get_cadr s in
    let! code := micheline2michelson_instruction a in
    return_macro (micheline2michelson_map_cadr x code)

  | PRIM (_, S_ (String "D" (String "I" s))) _ (a :: nil) =>
    let is_diip := fix is_diip s :=
                     match s with
                     | "P" => true
                     | String "I" s => is_diip s
                     | _ => false
                     end in
    if is_diip s then
      let! a := micheline2michelson_instruction a in
      return_instruction (DIP (String.length s) a)
    else Failed _ (Expansion_prim b e (String "D" (String "I" s)))
  | PRIM (_, S_DUP) _ (Mk_loc_micheline (_, NUMBER n) :: nil) =>
    match BinInt.Z.to_nat n with
    | S n => return_macro (DUP_Sn n)
    | O => Failed _ (Expansion b e)
    end
  | PRIM (_, S_ (String "D" (String "U" (String "U" s)))) _ nil =>
    let is_duup := fix is_duup s :=
                     match s with
                     | "P" => true
                     | String "U" s => is_duup s
                     | _ => false
                     end in
    if is_duup s then return_macro (DUP_Sn (String.length s))
    else Failed _ (Expansion_prim b e (String "D" (String "U" (String "U" s))))

  (* PAPAIR *)
  | PRIM (_, S_ (String "P" s)) _ nil =>
    let prim := String "P" s in
    let fail := Expansion_prim b e prim in
    let! full := parse_papair_full s fail in
    return_macro full

  (* UNPAPAIR *)
  | PRIM (_, S_ (String "U" (String "N" (String "P" s)))) _ nil =>
    let prim := String "U" (String "N" (String "P" s)) in
    let fail := Expansion_prim b e prim in
    let! full := parse_unpapair_full s fail in
    return_instruction full

  (* Unknown case *)
  | PRIM (_, S_ s) _ _ => Failed _ (Expansion_prim b e s)
  | _ => Failed _ (Expansion b e)
  end.

Record untyped_michelson_file :=
  Mk_untyped_michelson_file
    { root_annotation : annot_o;
      parameter : type;
      storage : type;
      code : instruction_seq }.

Record untyped_michelson_file_opt :=
  Mk_untyped_michelson_file_opt
    { root_annot : annot_o;
      parameter_opt : Datatypes.option type;
      storage_opt : Datatypes.option type;
      code_opt : Datatypes.option instruction_seq }.

Definition read_parameter (ty : type) (root_annot : annot_o)
           (f : untyped_michelson_file_opt) :=
  match f.(parameter_opt) with
  | None => Return {| root_annot := root_annot;
                      parameter_opt := Some ty;
                      storage_opt := f.(storage_opt);
                      code_opt := f.(code_opt) |}
  | Some _ => Failed _ Parsing
  end.

Definition read_storage (ty : type) (f : untyped_michelson_file_opt) :=
  match f.(storage_opt) with
  | None => Return {| root_annot := f.(root_annot);
                      parameter_opt := f.(parameter_opt);
                      storage_opt := Some ty;
                      code_opt := f.(code_opt) |}
  | Some _ => Failed _ Parsing
  end.

Definition read_code (c : instruction_seq) (f : untyped_michelson_file_opt) :=
  match f.(code_opt) with
  | None => Return {| root_annot := f.(root_annot);
                      parameter_opt := f.(parameter_opt);
                      storage_opt := f.(storage_opt);
                      code_opt := Some c |}
  | Some _ => Failed _ Parsing
  end.

Definition micheline2michelson_file (m : Datatypes.list loc_micheline) : M untyped_michelson_file :=
  let l :=
      match m with
      | Mk_loc_micheline (_, SEQ l) :: nil => l
      | l => l
      end
  in
  let! a :=
    error.list_fold_left
      (fun (a : untyped_michelson_file_opt) (lm : loc_micheline) =>
        let lm := to_pmicheline lm in
        let 'Mk_loc_micheline (_, _, m) := lm in
        match m with
        | PRIM (_, _, S_parameter) _ (cons param nil) =>
          let! an := extract_one_field_annot lm in
          let! ty := micheline2michelson_type param in
          read_parameter ty an a
        | PRIM (_, _, S_storage) _ (cons storage nil) =>
          let! ty := micheline2michelson_type storage in
          read_storage ty a
        | PRIM (_, _, S_code) _ (cons code nil) =>
          let! c := micheline2michelson_instruction code in
          read_code c a
        | _ => Failed _ Parsing
        end)
      l
      {| root_annot := None;
         parameter_opt := None;
         storage_opt := None;
         code_opt := None |} in
    match a.(parameter_opt), a.(storage_opt), a.(code_opt) with
    | Some param, Some storage, Some code =>
      Return {| root_annotation := a.(root_annot);
                parameter := param;
                storage := storage;
                code := code |}
    | _, _, _ => Failed _ Parsing
    end.