dtlc

dependently-typed lambda calculus toy
git clone git://git.rr3.xyz/dtlc
Log | Files | Refs | README | LICENSE

ctx.ml (1923B)


      1 open Node
      2 
      3 type 'a assignment = {
      4 	mutable typ: 'a;
      5 	mutable value: 'a;
      6 	mutable active: bool;
      7 }
      8 
      9 (* The "assignments" part of a context can be (and is) mutable, because it does
     10  * not get stored on core terms or semantic values after elaboration, but the
     11  * "env" part must not be mutable, because it gets saved on values. *)
     12 type 'a context = {
     13 	assignments: 'a assignment Tsil.t Name.Var.Map.t; (* XXX: tsil! Yuck! *)
     14 	env: 'a Env.environment;
     15 }
     16 
     17 let empty: 'a. 'a context = {
     18 	assignments = Name.Var.Map.empty;
     19 	env = Env.empty;
     20 }
     21 
     22 let assign
     23 : 'a. 'a context -> Name.Var.t array -> 'a -> 'a -> 'a context * 'a assignment
     24 = fun ctx names typ value ->
     25 	let asn = {typ; value; active = true} in
     26 	let shadow ctx name =
     27 		let add_to_tsil = function
     28 		| None -> Some (Tsil.Snoc (Tsil.Lin, asn))
     29 		| Some t -> Some (Tsil.Snoc (t, asn)) in
     30 		let assignments = Name.Var.Map.update name add_to_tsil ctx.assignments in
     31 		{ctx with assignments} in
     32 	(Array.fold_left shadow ctx names, asn)
     33 
     34 let bind
     35 : 'a. 'a context -> Uniq.range -> 'a context
     36 = fun ctx vars -> {ctx with env = Env.bind ctx.env vars}
     37 
     38 let define
     39 : 'a. 'a context -> Uniq.uniq -> 'a -> 'a context
     40 = fun ctx var value -> {ctx with env = Env.define ctx.env var value}
     41 
     42 let lookup
     43 : 'a. 'a context -> Name.Var.t -> int -> 'a assignment option
     44 = fun ctx name i ->
     45 	match Name.Var.Map.find_opt name ctx.assignments with
     46 	| Some t ->
     47 		let rec go i t = match i, t with
     48 		| 0, Tsil.Snoc (_, ({active = true; _} as asn)) -> Some asn
     49 		| i, Tsil.Snoc (t, {active = true; _}) -> go (i - 1) t
     50 		| i, Tsil.Snoc (t, {active = false; _}) -> go i t
     51 		| _, Tsil.Lin -> None in
     52 		go i t
     53 	| None -> None
     54 
     55 let index
     56 : 'a. 'a context -> Index.t -> Uniq.uniq
     57 = fun ctx ij -> Env.index ctx.env ij
     58 
     59 let quote
     60 : 'a. 'a context -> Uniq.uniq -> Index.t option
     61 = fun ctx var -> Env.quote ctx.env var
     62 
     63 let eval
     64 : 'a. 'a context -> Uniq.uniq -> 'a option
     65 = fun ctx var -> Env.eval ctx.env var