You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
49 lines
1.3 KiB
49 lines
1.3 KiB
(*
|
|
* Copyright (c) Facebook, Inc. and its affiliates.
|
|
*
|
|
* This source code is licensed under the MIT license found in the
|
|
* LICENSE file in the root directory of this source tree.
|
|
*)
|
|
|
|
open! IStd
|
|
|
|
module EvaluationTracker : sig
|
|
type eval_result = Eval_undefined | Eval_true | Eval_false
|
|
|
|
type content =
|
|
{ ast_node: Ctl_parser_types.ast_node
|
|
; phi: CTLTypes.t
|
|
; lcxt: CLintersContext.context
|
|
; eval_result: eval_result
|
|
; witness: Ctl_parser_types.ast_node option }
|
|
|
|
type eval_node = {id: int; content: content}
|
|
|
|
type tree = Tree of eval_node * tree list
|
|
|
|
type ast_node_to_display =
|
|
(* the node can be used to describe further sub calls in the evaluation stack *)
|
|
| Carry_forward of Ctl_parser_types.ast_node
|
|
(* the node cannot be further used to describe sub calls in the evaluation stack *)
|
|
| Last_occurrence of Ctl_parser_types.ast_node
|
|
|
|
type t =
|
|
{ next_id: int
|
|
; eval_stack: (tree * ast_node_to_display) Stack.t
|
|
; forest: tree list
|
|
; breakpoint_line: int option
|
|
; debugger_active: bool }
|
|
|
|
val create : SourceFile.t -> t
|
|
|
|
val create_content : Ctl_parser_types.ast_node -> CTLTypes.t -> CLintersContext.context -> content
|
|
|
|
val eval_begin : t -> content -> t
|
|
|
|
val eval_end : t -> Ctl_parser_types.ast_node option -> t
|
|
|
|
module DottyPrinter : sig
|
|
val dotty_of_ctl_evaluation : t -> string
|
|
end
|
|
end
|