Skip to main content

🍬 Script_ir_annot.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Non_empty_string.

Inductive var_annot : Set :=
| Var_annot : var_annot.

Inductive type_annot : Set :=
| Type_annot : type_annot.

Inductive field_annot : Set :=
| Field_annot : Non_empty_string.t field_annot.

Definition error_unexpected_annot {A : Set}
  (loc_value : Alpha_context.Script.location) (annot : list A) : M? unit :=
  match annot with
  | []Result.return_unit
  | cons _ _
    Error_monad.error_value
      (Build_extensible "Unexpected_annotation" Alpha_context.Script.location
        loc_value)
  end.

#[bypass_check(guard)]
Definition string_iter {A : Set}
  (p_value : ascii Pervasives.result unit A) (s_value : string)
  (i_value : int) : Pervasives.result unit A :=
  let len := String.length s_value in
  let fix aux (i_value : int) {struct i_value} : Pervasives.result unit A :=
    if i_value i len then
      Result.return_unit
    else
      let? '_ := p_value (String.get s_value i_value) in
      aux (i_value +i 1) in
  aux i_value.

Definition is_allowed_char (function_parameter : ascii) : bool :=
  match function_parameter with
  |
    ("a" % char | "b" % char | "c" % char | "d" % char | "e" % char | "f" % char
    | "g" % char | "h" % char | "i" % char | "j" % char | "k" % char |
    "l" % char | "m" % char | "n" % char | "o" % char | "p" % char | "q" % char
    | "r" % char | "s" % char | "t" % char | "u" % char | "v" % char |
    "w" % char | "x" % char | "y" % char | "z" % char | "A" % char | "B" % char
    | "C" % char | "D" % char | "E" % char | "F" % char | "G" % char |
    "H" % char | "I" % char | "J" % char | "K" % char | "L" % char | "M" % char
    | "N" % char | "O" % char | "P" % char | "Q" % char | "R" % char |
    "S" % char | "T" % char | "U" % char | "V" % char | "W" % char | "X" % char
    | "Y" % char | "Z" % char | "_" % char | "." % char | "%" % char |
    "@" % char | "0" % char | "1" % char | "2" % char | "3" % char | "4" % char
    | "5" % char | "6" % char | "7" % char | "8" % char | "9" % char) ⇒ true
  | _false
  end.

Definition check_char
  (loc_value : Alpha_context.Script.location) (c_value : ascii) : M? unit :=
  if is_allowed_char c_value then
    Result.return_unit
  else
    Error_monad.error_value
      (Build_extensible "Unexpected_annotation" Alpha_context.Script.location
        loc_value).

Definition max_annot_length : int := 255.

Inductive annot_opt : Set :=
| Field_annot_opt : option Non_empty_string.t annot_opt
| Type_annot_opt : option type_annot annot_opt
| Var_annot_opt : option var_annot annot_opt.

Definition _at : Non_empty_string.t := Non_empty_string.of_string_exn "@".

Definition parse_annot
  (loc_value : Alpha_context.Script.location) (s_value : string)
  : M? annot_opt :=
  let sub_or_wildcard {A : Set}
    (wrap : option Non_empty_string.t A) (s_value : string) : M? A :=
    match Non_empty_string.of_string s_value with
    | Nonereturn? (wrap None)
    | Some s_value
      match String.get s_value 0 with
      |
        ("a" % char | "b" % char | "c" % char | "d" % char | "e" % char |
        "f" % char | "g" % char | "h" % char | "i" % char | "j" % char |
        "k" % char | "l" % char | "m" % char | "n" % char | "o" % char |
        "p" % char | "q" % char | "r" % char | "s" % char | "t" % char |
        "u" % char | "v" % char | "w" % char | "x" % char | "y" % char |
        "z" % char | "A" % char | "B" % char | "C" % char | "D" % char |
        "E" % char | "F" % char | "G" % char | "H" % char | "I" % char |
        "J" % char | "K" % char | "L" % char | "M" % char | "N" % char |
        "O" % char | "P" % char | "Q" % char | "R" % char | "S" % char |
        "T" % char | "U" % char | "V" % char | "W" % char | "X" % char |
        "Y" % char | "Z" % char | "_" % char | "0" % char | "1" % char |
        "2" % char | "3" % char | "4" % char | "5" % char | "6" % char |
        "7" % char | "8" % char | "9" % char) ⇒
        let? '_ := string_iter (check_char loc_value) s_value 1 in
        return? (wrap (Some s_value))
      | _
        Error_monad.error_value
          (Build_extensible "Unexpected_annotation"
            Alpha_context.Script.location loc_value)
      end
    end in
  let len := String.length s_value in
  if (len =i 0) || (len >i max_annot_length) then
    Error_monad.error_value
      (Build_extensible "Unexpected_annotation" Alpha_context.Script.location
        loc_value)
  else
    let rest := String.sub s_value 1 (len -i 1) in
    match String.get s_value 0 with
    | ":" % char
      sub_or_wildcard
        (fun (a_value : option Non_empty_string.t) ⇒
          Type_annot_opt
            (Option.map
              (fun (function_parameter : Non_empty_string.t) ⇒
                let '_ := function_parameter in
                Type_annot) a_value)) rest
    | "@" % char
      sub_or_wildcard
        (fun (a_value : option Non_empty_string.t) ⇒
          Var_annot_opt
            (Option.map
              (fun (function_parameter : Non_empty_string.t) ⇒
                let '_ := function_parameter in
                Var_annot) a_value)) rest
    | "%" % char
      sub_or_wildcard
        (fun (a_value : option Non_empty_string.t) ⇒ Field_annot_opt a_value)
        rest
    | _
      Error_monad.error_value
        (Build_extensible "Unexpected_annotation" Alpha_context.Script.location
          loc_value)
    end.

Definition parse_annots
  (loc_value : Alpha_context.Script.location) (op_staroptstar : option bool)
  : option bool list string M? (list annot_opt) :=
  let allow_special_var :=
    match op_staroptstar with
    | Some op_starsthstarop_starsthstar
    | Nonefalse
    end in
  fun (op_staroptstar : option bool) ⇒
    let allow_special_field :=
      match op_staroptstar with
      | Some op_starsthstarop_starsthstar
      | Nonefalse
      end in
    fun (l_value : list string) ⇒
      List.map_e
        (fun (function_parameter : string) ⇒
          match
            (function_parameter,
              match function_parameter with
              | "@%" ⇒ allow_special_var
              | _false
              end,
              match function_parameter with
              | "@%%" ⇒ allow_special_var
              | _false
              end,
              match function_parameter with
              | "%@" ⇒ allow_special_field
              | _false
              end) with
          | ("@%", true, _, _)return? (Var_annot_opt (Some Var_annot))
          | ("@%%", _, true, _)return? (Var_annot_opt (Some Var_annot))
          | ("%@", _, _, true)return? (Field_annot_opt (Some _at))
          | (s_value, _, _, _)parse_annot loc_value s_value
          end) l_value.

Definition opt_field_of_field_opt
  (function_parameter : option Non_empty_string.t) : option field_annot :=
  match function_parameter with
  | NoneNone
  | Some a_valueSome (Field_annot a_value)
  end.

Definition classify_annot
  (loc_value : Alpha_context.Script.location) (l_value : list annot_opt)
  : M?
    (list (option var_annot) × list (option type_annot) ×
      list (option field_annot)) :=
  (* ❌ Use a trivial matching for the `with` clause, like: *)
  typ_with_with_non_trivial_matching.

Definition get_one_annot {A : Set}
  (loc_value : Alpha_context.Script.location)
  (function_parameter : list (option A)) : M? (option A) :=
  match function_parameter with
  | []Result.return_none
  | cons a_value []return? a_value
  | _
    Error_monad.error_value
      (Build_extensible "Unexpected_annotation" Alpha_context.Script.location
        loc_value)
  end.

Definition get_two_annot {A : Set}
  (loc_value : Alpha_context.Script.location)
  (function_parameter : list (option A)) : M? (option A × option A) :=
  match function_parameter with
  | []return? (None, None)
  | cons a_value []return? (a_value, None)
  | cons a_value (cons b_value []) ⇒ return? (a_value, b_value)
  | _
    Error_monad.error_value
      (Build_extensible "Unexpected_annotation" Alpha_context.Script.location
        loc_value)
  end.

Definition check_type_annot
  (loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
  let? '(vars, types, fields) :=
    Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
      (classify_annot loc_value) in
  let? '_ := error_unexpected_annot loc_value vars in
  let? '_ := error_unexpected_annot loc_value fields in
  let? _a := get_one_annot loc_value types in
  return? tt.

Definition check_composed_type_annot
  (loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
  let? '(vars, types, fields) :=
    Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
      (classify_annot loc_value) in
  let? '_ := error_unexpected_annot loc_value vars in
  let? _t := get_one_annot loc_value types in
  let? '(_f1, _f2) := get_two_annot loc_value fields in
  return? tt.

Definition parse_field_annot
  (loc_value : Alpha_context.Script.location) (annot : string)
  : M? (option Non_empty_string.t) :=
  if
    ((String.length annot) i 0) ||
    (Compare.Char.(Compare.S.op_ltgt) (String.get annot 0) "%" % char)
  then
    Result.return_none
  else
    let? function_parameter := parse_annot loc_value annot in
    match function_parameter with
    | Field_annot_opt annot_optreturn? annot_opt
    | _return? None
    end.

Definition is_field_annot
  (loc_value : Alpha_context.Script.location) (a_value : string) : M? bool :=
  Error_monad.op_gtpipequestion (parse_field_annot loc_value a_value)
    Option.is_some.

Definition extract_field_annot (function_parameter : Alpha_context.Script.node)
  : M? (Alpha_context.Script.node × option Non_empty_string.t) :=
  match function_parameter with
  | (Micheline.Prim loc_value prim args annot) as expr
    let fix extract_first
      (acc_value : list string) (function_parameter : list string)
      : M?
        (Micheline.node Alpha_context.Script.location Alpha_context.Script.prim
          × option Non_empty_string.t) :=
      match function_parameter with
      | []return? (expr, None)
      | cons s_value rest
        let? function_parameter := parse_field_annot loc_value s_value in
        match function_parameter with
        | Noneextract_first (cons s_value acc_value) rest
        | (Some _) as some_field_annot
          let annot := List.rev_append acc_value rest in
          return? ((Micheline.Prim loc_value prim args annot), some_field_annot)
        end
      end in
    extract_first nil annot
  | exprreturn? (expr, None)
  end.

Definition has_field_annot (node_value : Alpha_context.Script.node) : M? bool :=
  let? function_parameter := extract_field_annot node_value in
  match function_parameter with
  | (_node, Some _)return? true
  | (_node, None)return? false
  end.

Definition remove_field_annot (node_value : Alpha_context.Script.node)
  : M? Alpha_context.Script.node :=
  let? '(node_value, _a) := extract_field_annot node_value in
  return? node_value.

Definition extract_entrypoint_annot (node_value : Alpha_context.Script.node)
  : M? (Alpha_context.Script.node × option Alpha_context.Entrypoint.t) :=
  let? '(node_value, field_annot_opt) := extract_field_annot node_value in
  return?
    (node_value,
      (Option.bind field_annot_opt
        (fun (field_annot : Non_empty_string.t) ⇒
          Alpha_context.Entrypoint.of_annot_lax_opt field_annot))).

Definition check_var_annot
  (loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
  let? '(vars, types, fields) :=
    Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
      (classify_annot loc_value) in
  let? '_ := error_unexpected_annot loc_value types in
  let? '_ := error_unexpected_annot loc_value fields in
  let? _a := get_one_annot loc_value vars in
  return? tt.

Definition check_constr_annot
  (loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
  let? '(vars, types, fields) :=
    Error_monad.op_gtgtquestion (parse_annots loc_value None (Some true) annot)
      (classify_annot loc_value) in
  let? _v := get_one_annot loc_value vars in
  let? _t := get_one_annot loc_value types in
  let? '(_f1, _f2) := get_two_annot loc_value fields in
  return? tt.

Definition check_two_var_annot
  (loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
  let? '(vars, types, fields) :=
    Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
      (classify_annot loc_value) in
  let? '_ := error_unexpected_annot loc_value types in
  let? '_ := error_unexpected_annot loc_value fields in
  let? '(_a1, _a2) := get_two_annot loc_value vars in
  return? tt.

Definition check_destr_annot
  (loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
  let? '(vars, types, fields) :=
    Error_monad.op_gtgtquestion (parse_annots loc_value (Some true) None annot)
      (classify_annot loc_value) in
  let? '_ := error_unexpected_annot loc_value types in
  let? _v := get_one_annot loc_value vars in
  let? _f := get_one_annot loc_value fields in
  return? tt.

Definition check_unpair_annot
  (loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
  let? '(vars, types, fields) :=
    Error_monad.op_gtgtquestion (parse_annots loc_value (Some true) None annot)
      (classify_annot loc_value) in
  let? '_ := error_unexpected_annot loc_value types in
  let? '(_vcar, _vcdr) := get_two_annot loc_value vars in
  let? '(_f1, _f2) := get_two_annot loc_value fields in
  return? tt.

Definition parse_entrypoint_annot
  (loc_value : Alpha_context.Script.location) (annot : list string)
  : M? (option field_annot) :=
  let? '(vars, types, fields) :=
    Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
      (classify_annot loc_value) in
  let? '_ := error_unexpected_annot loc_value types in
  let? f_value := get_one_annot loc_value fields in
  let? _v := get_one_annot loc_value vars in
  return? f_value.

Definition parse_entrypoint_annot_strict
  (loc_value : Alpha_context.Script.location) (annot : list string)
  : M? Alpha_context.Entrypoint.t :=
  let? function_parameter := parse_entrypoint_annot loc_value annot in
  match function_parameter with
  | NonePervasives.Ok Alpha_context.Entrypoint.default
  | Some (Field_annot a_value) ⇒
    Alpha_context.Entrypoint.of_annot_strict loc_value a_value
  end.

Definition parse_entrypoint_annot_lax
  (loc_value : Alpha_context.Script.location) (annot : list string)
  : M? Alpha_context.Entrypoint.t :=
  let? function_parameter := parse_entrypoint_annot loc_value annot in
  match function_parameter with
  | NonePervasives.Ok Alpha_context.Entrypoint.default
  | Some (Field_annot annot) ⇒ Alpha_context.Entrypoint.of_annot_lax annot
  end.

Definition check_var_type_annot
  (loc_value : Alpha_context.Script.location) (annot : list string) : M? unit :=
  let? '(vars, types, fields) :=
    Error_monad.op_gtgtquestion (parse_annots loc_value None None annot)
      (classify_annot loc_value) in
  let? '_ := error_unexpected_annot loc_value fields in
  let? _v := get_one_annot loc_value vars in
  let? _t := get_one_annot loc_value types in
  return? tt.