package p4spectec

  1. Overview
  2. Docs

Source file pass.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
module Elaborate = Elaborate
module Algo = Algo
module Structure = Structure
module Annotate = Annotate

(* Shortcuts *)

let expand_spec filenames =
  List.concat_map
    (fun filename ->
      if Sys_unix.is_directory_exn filename then
        Util.Filesys.collect_files ~suffix:".watsup" filename
      else [ filename ])
    filenames

(* Parsing *)

let parse paths_spec =
  paths_spec |> expand_spec |> List.concat_map Frontend.Parse.parse_file

(* Elaboration. *)

let cache_elab = Hashtbl.create 8

let elab paths_spec =
  match Hashtbl.find_opt cache_elab paths_spec with
  | Some spec -> spec
  | None ->
      let spec = paths_spec |> parse |> Elaborate.Elab.elab_spec in
      Hashtbl.replace cache_elab paths_spec spec;
      spec

(* Algorithmic conversion *)

let cache_algo = Hashtbl.create 8

let algo paths_spec =
  match Hashtbl.find_opt cache_algo paths_spec with
  | Some spec -> spec
  | None ->
      let spec = paths_spec |> elab |> Algo.algo_spec in
      Hashtbl.replace cache_algo paths_spec spec;
      spec

(* Structuring *)

let structure_cache = Hashtbl.create 8

let structure ~(final : bool) paths_spec =
  match Hashtbl.find_opt structure_cache (final, paths_spec) with
  | Some spec -> spec
  | None ->
      let spec = paths_spec |> algo |> Structure.Struct.struct_spec ~final in
      Hashtbl.replace structure_cache (final, paths_spec) spec;
      spec

(* Annotation (prose) generation *)

let annotate paths_spec =
  paths_spec |> structure ~final:false |> Annotate.annotate_spec