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/inverse.ml.html
Source file inverse.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 145 146 147
(** Compute the inverse image of a term wrt an injective function. *) open Term open Timed open Common open Print open Lplib (** Logging function for unification. *) let log = Logger.make 'v' "invr" "inverse" let log = log.pp (** [cache f s] is equivalent to [f s] but [f s] is computed only once unless the rules of [s] are changed. *) let cache : (sym -> 'a) -> (sym -> 'a) = fun f -> let cache = ref [] in fun s -> let srs = !(s.sym_rules) in try let rs, x = List.assq s !cache in if rs == srs then x else raise Not_found with Not_found -> let x = f s in cache := (s, (srs, x))::!cache; x (** [const_graph s] returns the list of pairs [(s0,s1)] such that [s] has a rule of the form [s (s0 ...) ↪ s1 ...]. *) let const_graph : sym -> (sym * sym) list = fun s -> if Logger.log_enabled () then log "check rules of %a" sym s; let add s0 s1 l = if Logger.log_enabled () then log (Color.yel "%a %a ↪ %a") sym s sym s0 sym s1; (s0,s1)::l in let f l rule = match rule.lhs with | [l1] -> begin match get_args l1 with | Symb s0, _ -> let n = Bindlib.mbinder_arity rule.rhs in let r = Bindlib.msubst rule.rhs (Array.make n TE_None) in begin match get_args r with | Symb s1, _ -> add s0 s1 l | _ -> l end | _ -> l end | _ -> l in List.fold_left f [] !(s.sym_rules) (** cached version of [const_rules]. *) let const_graph : sym -> (sym * sym) list = cache const_graph (** [inverse_const s s'] returns [s0] if [s] has a rule of the form [s (s0 ...) ↪ s' ...]. @raise [Not_found] otherwise. *) let inverse_const : sym -> sym -> sym = fun s s' -> fst (List.find (fun (_,s1) -> s1 == s') (const_graph s)) (** [prod_graph s] returns the list of tuples [(s0,s1,s2,b)] such that [s] has a rule of the form [s (s0 _ _) ↪ Π x:s1 _, s2 r] with [b=true] iff [x] occurs in [r]. *) let prod_graph : sym -> (sym * sym * sym * bool) list = fun s -> if Logger.log_enabled () then log "check rules of %a" sym s; let add (s0,s1,s2,b) l = if Logger.log_enabled () then if b then log (Color.yel "%a (%a _ _) ↪ Π x:%a _, %a _[x]") sym s sym s0 sym s1 sym s2 else log (Color.yel "%a (%a _ _) ↪ %a _ → %a _") sym s sym s0 sym s1 sym s2; (s0,s1,s2,b)::l in let f l rule = match rule.lhs with | [l1] -> begin match get_args l1 with | Symb s0, [_;_] -> let n = Bindlib.mbinder_arity rule.rhs in let r = Bindlib.msubst rule.rhs (Array.make n TE_None) in begin match r with | Prod(a,b) -> begin match get_args a with | Symb s1, [_] -> begin match get_args (Bindlib.subst b mk_Kind) with | Symb(s2), [_] -> add (s0,s1,s2,Bindlib.binder_occur b) l | _ -> l end | _ -> l end | _ -> l end | _ -> l end | _ -> l in List.fold_left f [] !(s.sym_rules) (** cached version of [prod_graph]. *) let prod_graph : sym -> (sym * sym * sym * bool) list = cache prod_graph (** [inverse_prod s s'] returns [(s0,s1,s2,b)] if [s] has a rule of the form [s (s0 _ _) ↪ Π x:s1 _, s2 r] with [b=true] iff [x] occurs in [r], and either [s1] has a rule of the form [s1 (s3 ...) ↪ s' ...] or [s1 == s']. @raise [Not_found] otherwise. *) let inverse_prod : sym -> sym -> sym * sym * sym * bool = fun s s' -> match prod_graph s with | [] -> raise Not_found | [x] -> x | graph -> let f (_,s1,_,_) = try let _ = inverse_const s1 s' in true with Not_found -> false in try List.find f graph with Not_found -> List.find (fun (_,s1,_,_) -> s1 == s') graph (** [inverse s v] tries to compute a term [u] such that [s(u)] reduces to [v]. @raise [Not_found] otherwise. *) let rec inverse : sym -> term -> term = fun s v -> if Logger.log_enabled () then log "compute %a⁻¹(%a)" sym s term v; match get_args v with | Symb s', [t] when s' == s -> t | Symb s', ts -> add_args (mk_Symb (inverse_const s s')) ts | Prod(a,b), _ -> let s0,s1,s2,occ = match get_args a with | Symb s', _ -> inverse_prod s s' | _ -> raise Not_found in let t1 = inverse s1 a in let t2 = let x, b = Bindlib.unbind b in let b = inverse s2 b in if occ then Bindlib.unbox (_Abst (lift a) (Bindlib.bind_var x (lift b))) else b in add_args (mk_Symb s0) [t1;t2] | _ -> raise Not_found let inverse : sym -> term -> term = fun s v -> let t = inverse s v in let v' = mk_Appl(mk_Symb s,t) in if Eval.eq_modulo [] v' v then t else (if Logger.log_enabled() then log "%a ≢ %a@" term v' term v; raise Not_found)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>