package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.6.0.tbz
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8
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 144
(** 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/lets 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,d)) = match d with | None -> _Prod a (Bindlib.bind_var x t) | Some d -> _LLet a d (Bindlib.bind_var x t) 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 Bindlib variables in [env]. Note that the order is reversed: [vars [(xn,an);..;(x1,a1)] = [|x1;..;xn|]]. *) let vars : env -> tvar array = fun env -> Array.of_list (List.rev_map (fun (_,(x,_,_)) -> x) 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 variables in [env] and injects them in [tbox]. 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 -> Array.of_list (List.rev_map (fun (_,(x,_,_)) -> _Vari x) 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 -> term option -> tbinder -> 'a) -> 'a = fun c t f -> match unfold t with | Prod(a,b) -> f a None b | LLet(a,d,b) -> f a (Some d) b | _ -> match Eval.whnf c t with | Prod(a,b) -> f a None 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 d 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) (Option.map lift d) 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 d b -> let x, b = Bindlib.unbind b in build_env (i+1) (add x (lift a) (Option.map lift d) 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 d b -> let env = add xs.(i) (lift a) (Option.map lift d) 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)"
>