Skip to content

Instantly share code, notes, and snippets.

@EduardoRFS

EduardoRFS/lazy-optimal.ml

Last active September 22, 2025 21:08
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save EduardoRFS/6c34bf5d004b0b11b9fe6fd82ead78ec to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save EduardoRFS/6c34bf5d004b0b11b9fe6fd82ead78ec to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. EduardoRFS revised this gist Sep 22, 2025. No changes.
  2. EduardoRFS revised this gist Sep 22, 2025. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion lazy-optimal.ml
    View file
    Original file line number Diff line number Diff line change
    @@ -28,7 +28,7 @@ let rec subst ~to_ ~depth term =
    match term with
    | T_var var -> (
    let to_ = Lazy.force to_ in
    match var = depth with true -> to_ | false -> T_var var)
    match var = depth with true -> shift ~by:depth to_ | false -> T_var var)
    | T_lambda body ->
    let body =
    let depth = 1 + depth in
  3. EduardoRFS revised this gist Sep 22, 2025. 1 changed file with 37 additions and 17 deletions.
    54 changes: 37 additions & 17 deletions lazy-optimal.ml
    View file
    Original file line number Diff line number Diff line change
    @@ -1,42 +1,62 @@
    type var = int
    type index = int

    type term =
    | T_var of var
    | T_lambda of var * term lazy_t
    | T_var of index
    | T_lambda of term lazy_t
    | T_apply of term lazy_t * term lazy_t

    let rec subst from ~to_ term =
    let rec shift ~by ~depth term =
    match term with
    | T_var var -> (
    match var <= depth with true -> T_var (by + var) | false -> T_var var)
    | T_lambda body ->
    let body =
    let depth = 1 + depth in
    shift_lazy ~by ~depth body
    in
    T_lambda body
    | T_apply (funct, arg) ->
    let funct = shift_lazy ~by ~depth funct in
    let arg = shift_lazy ~by ~depth arg in
    T_apply (funct, arg)

    and shift_lazy ~by ~depth term = lazy (shift ~by ~depth (Lazy.force term))

    let shift ~by term = shift ~by ~depth:0 term

    let rec subst ~to_ ~depth term =
    match term with
    | T_var var -> (
    let to_ = Lazy.force to_ in
    match var = from with true -> to_ | false -> T_var var)
    | T_lambda (var, body) ->
    match var = depth with true -> to_ | false -> T_var var)
    | T_lambda body ->
    let body =
    match var = from with
    | true -> body
    | false -> subst_lazy from ~to_ body
    let depth = 1 + depth in
    subst_lazy ~to_ ~depth body
    in
    T_lambda (var, body)
    T_lambda body
    | T_apply (funct, arg) ->
    let funct = subst_lazy from ~to_ funct in
    let arg = subst_lazy from ~to_ arg in
    let funct = subst_lazy ~to_ ~depth funct in
    let arg = subst_lazy ~to_ ~depth arg in
    T_apply (funct, arg)

    and subst_lazy from ~to_ term = lazy (subst from ~to_ (Lazy.force term))
    and subst_lazy ~to_ ~depth term = lazy (subst ~to_ ~depth (Lazy.force term))

    let subst ~to_ term = subst ~to_ ~depth:0 term

    let rec eval term =
    match term with
    | T_var var -> T_var var
    | T_lambda (var, body) ->
    | T_lambda body ->
    let body = eval_lazy body in
    T_lambda (var, body)
    T_lambda body
    | T_apply (funct, arg) -> (
    let funct = eval_lazy funct in
    let arg = eval_lazy arg in
    match Lazy.force funct with
    | T_lambda (var, body) ->
    | T_lambda body ->
    let body = Lazy.force body in
    eval @@ subst var ~to_:arg body
    eval @@ subst ~to_:arg body
    | T_var _ | T_apply (_, _) -> T_apply (funct, arg))

    and eval_lazy term = lazy (eval (Lazy.force term))
  4. EduardoRFS revised this gist Sep 22, 2025. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion lazy-optimal.ml
    View file
    Original file line number Diff line number Diff line change
    @@ -16,7 +16,7 @@ let rec subst from ~to_ term =
    | true -> body
    | false -> subst_lazy from ~to_ body
    in
    T_lambda (from, body)
    T_lambda (var, body)
    | T_apply (funct, arg) ->
    let funct = subst_lazy from ~to_ funct in
    let arg = subst_lazy from ~to_ arg in
  5. EduardoRFS created this gist Sep 22, 2025.
    42 changes: 42 additions & 0 deletions lazy-optimal.ml
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,42 @@
    type var = int

    type term =
    | T_var of var
    | T_lambda of var * term lazy_t
    | T_apply of term lazy_t * term lazy_t

    let rec subst from ~to_ term =
    match term with
    | T_var var -> (
    let to_ = Lazy.force to_ in
    match var = from with true -> to_ | false -> T_var var)
    | T_lambda (var, body) ->
    let body =
    match var = from with
    | true -> body
    | false -> subst_lazy from ~to_ body
    in
    T_lambda (from, body)
    | T_apply (funct, arg) ->
    let funct = subst_lazy from ~to_ funct in
    let arg = subst_lazy from ~to_ arg in
    T_apply (funct, arg)

    and subst_lazy from ~to_ term = lazy (subst from ~to_ (Lazy.force term))

    let rec eval term =
    match term with
    | T_var var -> T_var var
    | T_lambda (var, body) ->
    let body = eval_lazy body in
    T_lambda (var, body)
    | T_apply (funct, arg) -> (
    let funct = eval_lazy funct in
    let arg = eval_lazy arg in
    match Lazy.force funct with
    | T_lambda (var, body) ->
    let body = Lazy.force body in
    eval @@ subst var ~to_:arg body
    | T_var _ | T_apply (_, _) -> T_apply (funct, arg))

    and eval_lazy term = lazy (eval (Lazy.force term))