Commit 988ae464 authored by Guillaume Claret's avatar Guillaume Claret 🐻 Committed by Mehdi Bouaziz
Browse files

Protocol/coq-of-ocaml: add axiom annotations for the interpreter

parent 02909fd2
Pipeline #275203908 passed with stages
in 73 minutes and 39 seconds
......@@ -198,6 +198,7 @@ let rec interp_stack_prefix_preserving_operation :
>|=? fun (rest', result) -> ((v, rest'), result)
| (Rest, v) ->
f v
[@@coq_axiom_with_reason "gadt"]
type step_constants = {
source : Contract.t;
......@@ -1446,6 +1447,7 @@ let rec step_bounded :
else None
in
logged_return ((result, rest), ctxt)
[@@coq_axiom_with_reason "gadt"]
let step :
type b a.
......@@ -1471,6 +1473,7 @@ let interp :
Log.log_interp ctxt code stack ;
step logger ctxt step_constants code stack
>|=? fun ((ret, ()), ctxt) -> (ret, ctxt)
[@@coq_axiom_with_reason "gadt"]
(* ---- contract handling ---------------------------------------------------*)
let execute logger ctxt mode step_constants ~entrypoint ~internal
......
......@@ -2703,6 +2703,7 @@ let find_entrypoint_for_type (type full exp) ~legacy ~(full : full ty)
>>? fun (_, Ex_ty ty) ->
merge_types ~legacy ctxt loc ty expected
>>? fun (Eq, ty, ctxt) -> ok (ctxt, entrypoint, (ty : exp ty))
[@@coq_axiom_with_reason "cast on err"]
module Entrypoints = Set.Make (String)
......@@ -6630,6 +6631,7 @@ let list_entrypoints (type full) (full : full ty) ctxt ~root_name =
(Entrypoints_map.singleton name ([], unparsed_full), true)
in
fold_tree full [] reachable ([], init)
[@@coq_axiom_with_reason "unsupported syntax"]
(* ---- Unparsing (Typed IR -> Untyped expressions) --------------------------*)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment