Commit b75572c5 authored by Pietro Abate's avatar Pietro Abate
Browse files

Add new function abstr to compute substitution for a lambda abstraction

parent 78fa0667
......@@ -3244,7 +3244,7 @@ let apply_raw s t =
(* cell i of ai contains /\k<=i s_k, cell j of aj contains /\k<=j t_k *)
let ai = ref [| |]
and aj = ref [| |] in
let result = ref any in
(* let result = ref any in *)
let tallying i j =
try
let s = get ai i in
......@@ -3296,3 +3296,12 @@ let apply_full s t =
res
let apply s t = let s,_,_,_ = apply_raw s t in s
let abstr s t =
let ss = Positive.substitutefree s in
let delta = all_vars t in
let sl = Tallying.tallying [(ss,t)] in
List.fold_left (fun acc e ->
let e1 = Tallying.CS.E.filter (fun v _ -> Var.Set.mem v delta) e in
e1 :: acc
) [] sl
......@@ -427,9 +427,11 @@ end
val apply : t -> t -> Tallying.CS.sl
val apply_full : t -> t -> t
val apply_raw : t -> t -> Tallying.CS.sl * t * t * t
(* apply_raw s t returns the 4-tuple (subst,ss, tt, res) where
(** apply_raw s t returns the 4-tuple (subst,ss, tt, res) where
subst is the set of substitution that make the application succeed,
ss and tt are the expansions of s and t corresponding to that substitution
and res is the type of the result of the application
*)
val apply_raw : t -> t -> Tallying.CS.sl * t * t * t
(** tallying sigma s < t *)
val abstr : t -> t -> Tallying.CS.sl
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment