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/value/match.ml.html

Source file match.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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
open Domain
open Lib
module Mixfix = Domain.Mixfix
open Lang
open Il
open Error
open Util.Source

(* Whether a value belongs to a type (including subtyping) *)

let rec sub_ (find_typdef_opt : TId.t -> Type.Typdef.t option)
    (find_func : FId.t -> tparam list * typ list * typ) (typ : typ)
    (value : value) : bool =
  match typ.it with
  | BoolT -> ( match value.it with BoolV _ -> true | _ -> false)
  | NumT `NatT -> (
      match value.it with
      | NumV (`Nat _) -> true
      | NumV (`Int i) -> Bigint.(i >= zero)
      | _ -> false)
  | NumT `IntT -> ( match value.it with NumV _ -> true | _ -> false)
  | TextT -> ( match value.it with TextV _ -> true | _ -> false)
  | VarT (tid, targs) -> (
      let td = find_typdef_opt tid |> Option.get in
      match td with
      | Param | Defining _ -> error typ.at "unexpected type variable"
      | Extern -> ( match value.it with ExternV _ -> true | _ -> false)
      | Defined (tparams, deftyp) -> (
          match (deftyp.it, value.it) with
          | PlainT typ, _ ->
              let theta = TIdMap.of_lists tparams targs in
              let typ = Type.Subst.subst_typ theta typ in
              sub_ find_typdef_opt find_func typ value
          | StructT typfields, StructV valuefields
            when List.length typfields = List.length valuefields ->
              let theta = TIdMap.of_lists tparams targs in
              List.for_all2
                (fun (atom_t, typ) (atom_v, value) ->
                  Atom.eq atom_t.it atom_v.it
                  &&
                  let typ = Type.Subst.subst_typ theta typ in
                  sub_ find_typdef_opt find_func typ value)
                typfields valuefields
          | VariantT typcases, CaseV valuecase ->
              let theta = TIdMap.of_lists tparams targs in
              let values = Mixfix.args valuecase in
              List.exists
                (fun (nottyp, _, _) ->
                  Mixfix.eq_mixop nottyp.it valuecase
                  &&
                  let nottyp = Type.Subst.subst_nottyp theta nottyp in
                  let typs = Mixfix.args nottyp.it in
                  subs_ find_typdef_opt find_func typs values)
                typcases
          | _ -> false))
  | TupleT typs -> (
      match value.it with
      | TupleV values ->
          List.length typs = List.length values
          && List.for_all2 (sub_ find_typdef_opt find_func) typs values
      | _ -> false)
  | IterT (typ_inner, Opt) -> (
      match value.it with
      | OptV value_opt -> (
          match value_opt with
          | Some value_inner ->
              sub_ find_typdef_opt find_func typ_inner value_inner
          | None -> true)
      | _ -> true)
  | IterT (typ_inner, List) -> (
      match value.it with
      | ListV values ->
          List.for_all (sub_ find_typdef_opt find_func typ_inner) values
      | _ -> false)
  | FuncT (tparams_t, typs_params_t, typ_ret_t) -> (
      match value.it with
      | FuncV fid ->
          let tparams_v, typs_params_v, typ_ret_v = find_func fid in
          Type.Equiv.equiv_functyp find_typdef_opt typ.at tparams_t
            typs_params_t typ_ret_t tparams_v typs_params_v typ_ret_v
      | _ -> false)

and subs_ (find_typdef_opt : TId.t -> Type.Typdef.t option)
    (find_func : FId.t -> tparam list * typ list * typ) (typs : typ list)
    (values : value list) : bool =
  List.length typs = List.length values
  && List.for_all2 (sub_ find_typdef_opt find_func) typs values

(* Caches *)

(* Caching subtyping of type variables to values,
   using the pair of type variable and value id as key *)

type cache_sub_var = (string * int, bool) Hashtbl.t

(* Caching type definition finder *)

let cache_find_typdef_opt find_typdef_opt =
  let cache : (string, Type.Typdef.t option) Hashtbl.t = Hashtbl.create 8 in
  fun (tid : TId.t) ->
    match Hashtbl.find_opt cache tid.it with
    | Some td_opt -> td_opt
    | None ->
        let td_opt = find_typdef_opt tid in
        Hashtbl.add cache tid.it td_opt;
        td_opt

(* Entry point *)

let sub cache_sub_var find_typdef_opt find_func typ value =
  match typ.it with
  | VarT (tid, []) -> (
      let key = (tid.it, value.note.vid) in
      match Hashtbl.find_opt cache_sub_var key with
      | Some res -> res
      | None ->
          let res =
            sub_ (cache_find_typdef_opt find_typdef_opt) find_func typ value
          in
          Hashtbl.add cache_sub_var key res;
          res)
  | _ -> sub_ (cache_find_typdef_opt find_typdef_opt) find_func typ value

let subs find_typdef_opt find_func typs values =
  subs_ (cache_find_typdef_opt find_typdef_opt) find_func typs values