Skip to content

Instantly share code, notes, and snippets.

@jozefg

jozefg/nbe.ml

Last active March 20, 2021 00:13
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save jozefg/47027557fcd924874097c4ef360dd4ac to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save jozefg/47027557fcd924874097c4ef360dd4ac to your computer and use it in GitHub Desktop.
Download ZIP
Raw
nbe.ml
module Syn =
struct
type uni_level = int
type t =
| Var of int (* DeBruijn indices for variables *)
| Nat | Zero | Succ of t | Rec of t * uni_level * t * t * t
| Pi of t * t | Lam of t | Ap of t * t
| Uni of uni_level
| Subst of t * subst
and subst =
| Shift
| Id
| Compose of subst * subst
| First of subst * t
type env = t list
end
module D =
struct
type env = t list
and t =
| Lam of Syn.t * env
| Neutral of t * ne
| Nat
| Zero
| Succ of t
| Pi of t * t
| Uni of Syn.uni_level
and ne =
| Var of int
| Ap of ne * nf
| Rec of nf * Syn.uni_level * nf * nf * ne
and nf =
| Normal of t * t
end
let rec apply_subst (sub : Syn.subst) (env : D.env) : D.env =
match sub with
| Shift -> List.tl env
| Id -> env
| Compose (sub1, sub2) -> apply_subst sub2 env |> apply_subst sub1
| First (sub, t) -> eval t env :: apply_subst sub env
and do_rec lev uni tp zero suc n : D.t =
match n with
| D.Zero -> zero
| D.Succ n -> do_ap (do_ap suc n) (do_rec lev uni tp zero suc n)
| D.Neutral (_, e) ->
(* Issue, Normal demands a type *)
let tp' = D.Normal (D.Uni uni, tp) in
let zero' = D.Normal (do_ap tp D.Zero, zero) in
let suc_tp =
D.Pi
( D.Nat
, D.Pi
( do_ap tp (D.Neutral (D.Nat, D.Var lev))
, do_ap tp (D.Succ (D.Neutral (D.Nat, D.Var lev))))) in
let suc' = D.Normal (suc_tp, suc) in
let final_tp = do_ap tp n in
D.Neutral (final_tp, D.Rec (tp', uni, zero', suc', e))
| _ -> failwith "Not a number"
and do_ap f a : D.t =
match f with
| D.Lam (body, env) -> eval body (a :: env)
| D.Neutral (tp, e) ->
begin
match tp with
| D.Pi (src, dst) ->
let dst = do_ap dst a in
D.Neutral (dst, D.Ap (e, D.Normal (src, a)))
| _ -> failwith "Not a Pi in do_ap"
end
| _ -> failwith "Not a function in do_ap"
and eval (t : Syn.t) (env : D.env) =
match t with
| Syn.Var i -> List.nth env i
| Syn.Nat -> D.Nat
| Syn.Zero -> D.Zero
| Syn.Succ t -> D.Succ (eval t env)
| Syn.Rec (tp, uni, zero, suc, n) ->
do_rec (List.length env) uni (eval tp env) (eval zero env) (eval suc env) (eval n env)
| Syn.Pi (src, dest) -> D.Pi (eval src env, eval dest env)
| Syn.Uni i -> D.Uni i
| Syn.Lam t -> D.Lam (t, env)
| Ap (t1, t2) -> do_ap (eval t1 env) (eval t2 env)
| Subst (t, subst) -> eval t (apply_subst subst env)
let rec read_back_nf (size : int) (nf : D.nf) : Syn.t =
match nf with
| D.Normal (D.Pi (src, dest), f) ->
let arg = D.Neutral (src, D.Var size) in
let nf = D.Normal (do_ap dest arg, do_ap f arg) in
Syn.Lam (read_back_nf (size + 1) nf)
| D.Normal (D.Nat, D.Zero) -> Syn.Zero
| D.Normal (D.Nat, D.Succ nf) -> Syn.Succ (read_back_nf size (D.Normal (D.Nat, nf)))
| D.Normal (D.Nat, D.Neutral (_, ne)) -> read_back_ne size ne
| D.Normal (D.Uni i, D.Nat) -> Syn.Nat
| D.Normal (D.Uni i, D.Pi (src, dest)) ->
Syn.Pi
(read_back_nf size (D.Normal (D.Uni i, src)),
read_back_nf size (D.Normal (D.Uni i, dest)))
| D.Normal (D.Uni i, D.Neutral (_, ne)) -> read_back_ne size ne
| _ -> failwith "Ill-typed read_back_nf"
and read_back_ne (size : int) (ne : D.ne) : Syn.t =
match ne with
| D.Var x -> Syn.Var (size - (x + 1))
| D.Ap (ne, arg) ->
Syn.Ap (read_back_ne size ne, read_back_nf size arg)
| D.Rec (tp, uni, zero, suc, n) ->
Syn.Rec
(read_back_nf size tp,
uni,
read_back_nf size zero,
read_back_nf size suc,
read_back_ne size n)
let rec initial_env env =
match env with
| [] -> []
| t :: env ->
let env' = initial_env env in
let d = D.Neutral (eval t env', D.Var (List.length env)) in
d :: env'
let normalize ~env ~term ~tp =
let env' = initial_env env in
let tp' = eval tp env' in
let term' = eval term env' in
read_back_nf (List.length env') (D.Normal (tp', term'))
let test =
let open Syn in
Rec (Lam Nat, 0, Zero, Lam (Lam (Succ (Succ (Var 0)))), Succ (Succ Zero))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment