Source file value.ml

open Logic.Lambda
open UtilsLib

module AcgSig = AcgData.Signature.Data_Signature

type vterm =
  | StringTerm of string * Error.pos
  | RealTerm of AcgSig.t * Lambda.term * Lambda.stype * (Containers.SharedForest.SharedForest.weight option)

type value = vterm LazyList.t

let get_term_value_in_sig s vt =
  match vt with
  | StringTerm (str, (pos, _)) ->
    let lexbuf = Sedlexing.Utf8.from_string str in
    let () = Error.set_position lexbuf pos in
    let () = Sedlexing.set_filename lexbuf pos.Lexing.pos_fname in
    (match Grammars.Parsers.parse_term lexbuf s with
    | None -> failwith "Term parsing error"
    | Some (t, ty) -> (t, ty))
  | RealTerm (st, t, ty, _w) ->
    if st = s then (t, ty) else
      Errors.(ScriptErrors.emit (Script_l.WrongSignature (fst (AcgSig.name st), fst (AcgSig.name s))))

let value_from_string s (s_pos, e_pos) =
  let s_pos = { s_pos with Lexing.pos_cnum = s_pos.Lexing.pos_cnum + 1 } in
  LazyList.one (StringTerm (s, (s_pos, e_pos)))

let print_aux c v =
  match v with
  | RealTerm (s, t, ty, w) ->
    let pp_w fmt = function
      | None -> ()
      | Some w -> Format.fprintf fmt " (%a)" Containers.SharedForest.SharedForest.pp_weight  w in
    (* Kept for debugging: depth/size pretty printer for terms *)
    (*let pp_s fmt (d, s) = Format.fprintf fmt " (depth: %d, size: %d)" d s in
      Logs.app (fun m -> m "@[<hv 2>Term%a%a:@ %a@ :@ %a@]" *)
    let () = Logs.app (fun m -> m "@[<hov>Term%a:@ @[%a@ @[:@ %a@]@]@]"
                 pp_w
                 w
                 (* pp_s
                    (Lambda.size ~id_to_term:(fun i -> AcgSig.unfold_term_definition i s) t) *)
                 (AcgSig.pp_term s) t
                 (AcgSig.pp_type s) ty) in
    let () = flush stdout in
    c + 1
  | StringTerm _ -> Errors.(ScriptErrors.emit Script_l.NoSignatureTerm)

let print print_count vl =
  try
    let nb_terms = LazyList.fold_left print_aux 0 vl in
    if print_count then Logs.app (fun m -> m "%i term%s computed." nb_terms (if nb_terms = 1 then "" else "s"))
  with
    Sys.Break ->
      let () = Logs.app (fun m -> m "@.") in
      let () = flush stdout in ()