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/type/subst.ml.html

Source file subst.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
module Fresh_ = Fresh
open Domain.Lib
module Mixfix = Domain.Mixfix
open Lang
open Il
open Error
open Util.Source

(* Substitution of type variables *)

type theta = Typ.t TIdMap.t

let freshen_tparams (tparams : tparam list) : theta * tparam list =
  List.fold_left
    (fun (theta, tids_fresh) tparam ->
      let tid_fresh = "__FRESH" ^ string_of_int (Fresh_.fresh ()) $ no_region in
      let typ_fresh = VarT (tid_fresh, []) $ no_region in
      let theta = TIdMap.add tparam typ_fresh theta in
      (theta, tids_fresh @ [ tid_fresh ]))
    (TIdMap.empty, []) tparams

(* Types *)

let rec subst_typ_inner (theta : theta) (typ : typ) : typ =
  match typ.it with
  | BoolT | NumT _ | TextT -> typ
  | VarT (tid, targs) -> (
      match TIdMap.find_opt tid theta with
      | Some _ when targs <> [] ->
          error typ.at "higher-order substitution is disallowed"
      | Some typ -> typ
      | None ->
          let targs = subst_typs_inner theta targs in
          VarT (tid, targs) $ typ.at)
  | TupleT typs ->
      let typs = subst_typs_inner theta typs in
      TupleT typs $ typ.at
  | IterT (typ, iter) ->
      let typ = subst_typ_inner theta typ in
      IterT (typ, iter) $ typ.at
  | FuncT (tparams, typs_params, typ_ret) ->
      let theta_fresh, tparams = freshen_tparams tparams in
      let typs_params =
        typs_params |> subst_typs_inner theta_fresh |> subst_typs_inner theta
      in
      let typ_ret =
        typ_ret |> subst_typ_inner theta_fresh |> subst_typ_inner theta
      in
      FuncT (tparams, typs_params, typ_ret) $ typ.at

and subst_typs_inner (theta : theta) (typs : typ list) : typ list =
  List.map (subst_typ_inner theta) typs

let subst_typ (theta : theta) (typ : typ) : typ =
  if TIdMap.is_empty theta then typ else subst_typ_inner theta typ

let subst_typs (theta : theta) (typs : typ list) : typ list =
  if TIdMap.is_empty theta then typs else subst_typs_inner theta typs

(* Variant types *)

let subst_nottyp (theta : theta) (nottyp : nottyp) : nottyp =
  if TIdMap.is_empty theta then nottyp
  else Mixfix.map (subst_typ theta) nottyp.it $ nottyp.at

let subst_typcase (theta : theta) (typcase : typcase) : typcase =
  let nottyp, typorigin, hints = typcase in
  let nottyp = subst_nottyp theta nottyp in
  let typorigin =
    let id, targs = typorigin.it in
    let targs = subst_typs theta targs in
    (id, targs) $ typorigin.at
  in
  (nottyp, typorigin, hints)

(* Parameters *)

let rec subst_param (theta : theta) (param : param) : param =
  match param.it with
  | ExpP typ ->
      let typ = subst_typ theta typ in
      ExpP typ $ param.at
  | DefP (id, tparams, params, typ) ->
      let theta_fresh, tparams = freshen_tparams tparams in
      let params = params |> subst_params theta_fresh |> subst_params theta in
      let typ = typ |> subst_typ theta_fresh |> subst_typ theta in
      DefP (id, tparams, params, typ) $ param.at

and subst_params (theta : theta) (params : param list) : param list =
  List.map (subst_param theta) params