- let rec subst v st = function
- | term when st = `Var v -> term
- | `Var x when x = v -> st
- | `Var _ as term -> term
- | `App(t1,t2) -> `App(subst v st t1, subst v st t2)
- | `Lam(x, _) as term when x = v -> term
- (* if x is free in the inserted term st, a capture is possible
- * we handle by ...
- *)
- | `Lam(x, body) ->
- (match free_in x st with
- (* x not free in st, can substitute st for v without any captures *)
- | None -> `Lam(x, subst v st body)
- (* x free in st, need to alpha-convert `Lam(x, body) *)
- | Some max_x ->
- let bump_tag (tag, name) (tag', _) =
- (max tag tag') + 1, name in
- let bump_tag' ((_, name) as v1) ((_, name') as v2) =
- if name = name' then bump_tag v1 v2 else v1 in
- (* bump x > max_x from st, then check whether
- * it also needs to be bumped > v
- *)
- let uniq_x = bump_tag' (bump_tag x max_x) v in
- let uniq_x' = (match free_in uniq_x body with
- | None -> uniq_x
- (* bump uniq_x > max_x' from body *)
- | Some max_x' -> bump_tag uniq_x max_x'
- ) in
- (* alpha-convert body *)
- let body' = subst x (`Var uniq_x') body in
- (* now substitute st for v *)
- `Lam(uniq_x', subst v st body')
- )
+ let rec subst v new_term term = match new_term with
+ | `Var v' when equal_var v v' -> term
+ | _ -> (match term with
+ | `Var v' when equal_var v v' -> new_term
+ | `Var _ -> term
+ | `App(left, right) -> `App(subst v new_term left, subst v new_term right)
+ | `Lam(v', _) when equal_var v v' -> term
+ (* if x is free in the inserted term new_term, a capture is possible *)
+ | `Lam(v', body) ->
+ (match free_in v' new_term with
+ (* v' not free in new_term, can substitute new_term for v without any captures *)
+ | None -> `Lam(v', subst v new_term body)
+ (* v' free in new_term, need to alpha-convert *)
+ | Some max_x ->
+ let bump_tag (tag, name) (tag', _) =
+ (max tag tag') + 1, name in
+ let bump_tag' ((_, name) as v1) ((_, name') as v2) =
+ if (String.compare name name' == 0) then bump_tag v1 v2 else v1 in
+ (* bump v' > max_x from new_term, then check whether
+ * it also needs to be bumped > v
+ *)
+ let uniq_x = bump_tag' (bump_tag v' max_x) v in
+ let uniq_x' = (match free_in uniq_x body with
+ | None -> uniq_x
+ (* bump uniq_x > max_x' from body *)
+ | Some max_x' -> bump_tag uniq_x max_x'
+ ) in
+ (* alpha-convert body *)
+ let body' = subst v' (`Var uniq_x') body in
+ (* now substitute new_term for v *)
+ `Lam(uniq_x', subst v new_term body')
+ )
+ )