package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.4.1.tbz
sha256=221dff97ab245c49b7e6480fa2a3a331ab70eb86dd5d521e2c73151029bbb787
sha512=a39961bb7f04f739660a98a52981d4793709619cd21310ca6982ba78af81ef09e01c7517ee3b8b2687b09f7d2614d878c1d69494ca6ab8ef8205d240c216ce8a
doc/src/lambdapi.core/env.ml.html
Source file env.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 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
(** Scoping environment for variables. *) open Lplib open Term (** Type of an environment, used in scoping to associate names to corresponding Bindlib variables and types. Note that it cannot be implemented by a map as the order is important. The structure is similar to {!type:Term.ctxt}, a tuple [(x,a,t)] is a variable [x], its type [a] and possibly its definition [t]. The typing environment [x1:A1,..,xn:An] is represented by the list [xn:An;..;x1:A1] in reverse order (last added variable comes first). *) type env = (string * (tvar * tbox * tbox option)) list type t = env (** [empty] is the empty environment. *) let empty : env = [] (** [add v a t env] extends the environment [env] by mapping the string [Bindlib.name_of v] to [(v,a,t)]. *) let add : tvar -> tbox -> tbox option -> env -> env = fun v a t env -> (Bindlib.name_of v, (v, a, t)) :: env (** [find n env] returns the Bindlib variable associated to the variable name [n] in the environment [env]. If none is found, [Not_found] is raised. *) let find : string -> env -> tvar = fun n env -> let (x,_,_) = List.assoc n env in x (** [mem n env] returns [true] iff [n] is mapped to a variable in [env]. *) let mem : string -> env -> bool = List.mem_assoc (** [to_prod env t] builds a sequence of products / let-bindings whose domains are the variables of the environment [env] (from left to right), and whose body is the term [t]. By calling [to_prod [(xn,an,None);⋯;(x1,a1,None)] t] you obtain a term of the form [Πx1:a1,..,Πxn:an,t]. *) let to_prod_box : env -> tbox -> tbox = fun env t -> let add_prod t (_,(x,a,u)) = let b = Bindlib.bind_var x t in match u with | Some u -> _LLet a u b | None -> _Prod a b in List.fold_left add_prod t env (** [to_prod] is an “unboxed” version of [to_prod_box]. *) let to_prod : env -> tbox -> term = fun env t -> Bindlib.unbox (to_prod_box env t) (** [to_abst env t] builds a sequence of abstractions or let bindings, depending on the definition of the elements in the environment whose domains are the variables of the environment [env] (from left to right), and which body is the term [t]: [to_abst [(xn,an,None);..;(x1,a1,None)] t = λx1:a1,..,λxn:an,t]. *) let to_abst : env -> tbox -> term = fun env t -> let add_abst t (_,(x,a,u)) = let b = Bindlib.bind_var x t in match u with | Some u -> _LLet a u b | None -> _Abst a b in Bindlib.unbox (List.fold_left add_abst t env) (** [vars env] extracts the array of the {e not defined} Bindlib variables in [env]. Note that the order is reversed: [vars [(xn,an);..;(x1,a1)] = [|x1;..;xn|]]. *) let vars : env -> tvar array = fun env -> let f (_, (x, _, u)) = if u = None then Some(x) else None in Array.of_list (List.filter_rev_map f env) (** [appl t env] applies [t] to the variables of [env]. *) let appl : tbox -> env -> tbox = fun t env -> List.fold_right (fun (_,(x,_,_)) t -> _Appl t (_Vari x)) env t (** [to_tbox env] extracts the array of the {e not defined} variables in [env] and injects them in the [tbox] type. This is the same as [Array.map _Vari (vars env)]. Note that the order is reversed: [to_tbox [(xn,an);..;(x1,a1)] = [|x1;..;xn|]]. *) let to_tbox : env -> tbox array = fun env -> let f (_, (x, _, u)) = if u = None then Some(_Vari x) else None in Array.of_list (List.filter_rev_map f env) (** [to_ctxt e] converts an environment into a context. *) let to_ctxt : env -> ctxt = List.map (fun (_,(v,a,t)) -> (v, Bindlib.unbox a, Option.map Bindlib.unbox t)) (** [match_prod c t f] returns [f a b] if [t] matches [Prod(a,b)] possibly after reduction. @raise [Invalid_argument] if [t] is not a product. *) let match_prod : ctxt -> term -> (term -> tbinder -> 'a) -> 'a = fun c t f -> match unfold t with | Prod(a,b) -> f a b | _ -> match Eval.whnf c t with | Prod(a,b) -> f a b | _ -> invalid_arg __LOC__ (** [of_prod c s t] returns a tuple [(env,b)] where [b] is constructed from the term [t] by unbinding as much dependent products as possible in the head of [t]. The free variables created by this process, prefixed by [s], are given (with their types) in the environment [env] (in reverse order). For instance, if [t] is of the form [Πx1:a1, ⋯, Πxn:an, b], then the function returns [b] and the environment [(xn,an); ⋯;(x1,a1)]. *) let of_prod : ctxt -> string -> term -> env * term = fun c s t -> let i = Stdlib.ref (-1) in let rec build_env env t = try match_prod c t (fun a b -> let name = Stdlib.(incr i; s ^ string_of_int !i) in let x, b = LibTerm.unbind_name name b in build_env (add x (lift a) None env) b) with Invalid_argument _ -> env, t in build_env [] t (** [of_prod_nth c n t] returns a tuple [(env,b)] where [b] is constructed from the term [t] by unbinding [n] dependent products. The free variables created by this process are given (with their types) in the environment [env] (in reverse order). For instance, if [t] is of the form [Πx1:a1, ⋯, Πxn:an, b] then the function returns [b] and the environment [(xn,an); ⋯;(x1,a1)]. [n] must be non-negative. @raise [Invalid_argument] if [t] does not evaluate to a series of (at least) [n] products. *) let of_prod_nth : ctxt -> int -> term -> env * term = fun c n t -> let rec build_env i env t = if i >= n then env, t else match_prod c t (fun a b -> let x, b = Bindlib.unbind b in build_env (i+1) (add x (lift a) None env) b) in build_env 0 [] t (** [of_prod_using c xs t] is similar to [of_prod s c n t] where [n = Array.length xs] except that it replaces unbound variables by those of [xs]. @raise [Invalid_argument] if [t] does not evaluate to a series of (at least) [n] products. *) let of_prod_using : ctxt -> tvar array -> term -> env * term = fun c xs t -> let n = Array.length xs in let rec build_env i env t = if i >= n then env, t else match_prod c t (fun a b -> let env = add xs.(i) (lift a) None env in build_env (i+1) env (Bindlib.subst b (mk_Vari(xs.(i))))) in build_env 0 [] t
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>