env.ml (1884B)
1 module UniqMap = Uniq.UniqMap 2 3 module UniqTsil = struct 4 module IndexMap = Map.Make(Int) 5 6 module VarMap = Uniq.RangeMap.Make(struct 7 type v = int 8 type v' = int * int 9 let offset i j = (i, j) 10 end) 11 12 type t = { 13 length: int; 14 index_to_var: Uniq.range IndexMap.t; 15 var_to_index: VarMap.t; 16 } 17 18 let lin: t = { 19 length = 0; 20 index_to_var = IndexMap.empty; 21 var_to_index = VarMap.empty; 22 } 23 24 let snoc 25 : t -> Uniq.range -> t 26 = fun {length; index_to_var; var_to_index} vars -> { 27 length = length + 1; 28 index_to_var = IndexMap.add length vars index_to_var; 29 var_to_index = VarMap.add vars length var_to_index; 30 } 31 32 let var_of 33 : t -> Index.t -> Uniq.uniq 34 = fun {length; index_to_var; _} (Index.Of (i, j)) -> 35 let l = length - i - 1 in (* Convert index i to level l. *) 36 Uniq.get (IndexMap.find l index_to_var) j 37 38 let index_of 39 : t -> Uniq.uniq -> Index.t option 40 = fun {length; var_to_index; _} var -> 41 match VarMap.find_opt var var_to_index with 42 | Some (l, j) -> 43 let i = length - l - 1 in (* Convert level l to index i. *) 44 Some (Index.Of (i, j)) 45 | None -> None 46 end 47 48 type 'a environment = { 49 bindings: UniqTsil.t; 50 definitions: 'a UniqMap.t; 51 } 52 53 let empty: 'a. 'a environment = { 54 bindings = UniqTsil.lin; 55 definitions = UniqMap.empty; 56 } 57 58 let bind 59 : 'a. 'a environment -> Uniq.range -> 'a environment 60 = fun env vars -> 61 {env with bindings = UniqTsil.snoc env.bindings vars} 62 63 let define 64 : 'a. 'a environment -> Uniq.uniq -> 'a -> 'a environment 65 = fun env var value -> 66 {env with definitions = UniqMap.add var value env.definitions} 67 68 let index 69 : 'a. 'a environment -> Index.t -> Uniq.uniq 70 = fun env ij -> UniqTsil.var_of env.bindings ij 71 72 let quote 73 : 'a. 'a environment -> Uniq.uniq -> Index.t option 74 = fun env var -> UniqTsil.index_of env.bindings var 75 76 let eval 77 : 'a. 'a environment -> Uniq.uniq -> 'a option 78 = fun env var -> UniqMap.find_opt var env.definitions