package p4spectec

  1. Overview
  2. Docs
P4-SpecTec: A mechanization toolchain for the P4 Programming Language

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (2)

Authors

  1. K
    KAIST PLRG

Maintainers

  1. 9
    99jaehyunlee@kaist.ac.kr

Sources

v0.1.2.tar.gz
md5=1a3bc0a385fe1ecf403c019f49aa6de6
sha512=5d20b5821f33e2a3a5419b208606f27c01511994c2b3b1e1cdf4c077056dfd0aa81682af0720e1060ee2bfb0341918fcc4c53159820205a2bc32b725e5c1a714

doc/src/p4spectec.pass/pass.ml.html

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