Project

General

Profile

« Previous | Next » 

Revision 1d3f2f66

Added by Pierre-Loïc Garoche almost 4 years ago

every in kind2 syntax

View differences:

src/printers.ml
128 128 
and pp_app fmt id e r =
129 129 
  match r with
130 130 
  | None -> pp_call fmt id e
131 
  | Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c
131 
  | Some c ->
132 
     if !Options.kind2_print &&
133 
          not (List.mem id Basic_library.internal_funs) then
134 
       (* We only translate calls to nodes in kind2. The other may be
135 
          rejected by Kind2 *)
136 
       fprintf fmt "(restart %s every (%a)) (%a)"
137 
         id
138 
         pp_expr c
139 
         pp_expr e
140 
     else
141 
       fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c
132 142 

  		




  133
  143
  
    
and pp_call fmt id e =


  		




  134
  144
  
    
  match id, e.expr_desc with


  		












Also available in:  Unified diff