Source file value.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
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) * (string 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, _comment) ->
    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, comment) ->
    let pp_w fmt = function
      | None -> ()
      | Some w -> Format.fprintf fmt " (%a)" Containers.SharedForest.SharedForest.pp_weight  w in
    let pp_comment fmt = function
      | None -> ()
      | Some c -> Format.fprintf fmt "[%s] " c 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>%aTerm%a:@ @[%a@ @[:@ %a@]@]@]"
                 pp_comment
                 comment
                 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 ()