ocaml/pure.ml

   1 open Util.Vars
   2
   3 module Pure =
   4 struct
   5
   6 type t =
   7   | V of int
   8   | A of t * t
   9   | L of t
  10   | B
  11
  12 let rec print ?(l=[]) =
  13  function
  14     V n -> print_name l n
  15   | A(t1,t2) -> "(" ^ print ~l t1 ^ " " ^ print ~l t2 ^ ")"
  16   | L t ->
  17      let name = string_of_var (List.length l) in
  18      "λ" ^ name ^ "." ^ print ~l:(name::l) t
  19   | B -> "B"
  20
  21 let lift m =
  22  let rec aux l =
  23   function
  24    | V n -> V (if n < l then n else n+m)
  25    | A (t1,t2) -> A (aux l t1, aux l t2)
  26    | L t -> L (aux (l+1) t)
  27    | B -> B
  28  in
  29   aux 0
  30
  31 (* Reference implementation.
  32    Reduction machine used below
  33 let subst delift_by_one what with_what =
  34  let rec aux l =
  35   function
  36    | A(t1,t2) -> A(aux l t1, aux l t2)
  37    | V n ->
  38        if n = what + l then
  39         lift l with_what
  40        else
  41         V (if delift_by_one && n >= l then n-1 else n)
  42    | L t -> L (aux (l+1) t)
  43  in
  44   aux 0
  45
  46 let rec whd =
  47  function
  48   | A(t1, t2) ->
  49      let t2 = whd t2 in
  50      let t1 = whd t1 in
  51       (match t1 with
  52         | L f -> whd (subst true 0 t2 f)
  53         | V _
  54         | A _ -> A(t1,t2))
  55   | V _
  56   | L _ as t -> t
  57 *)
  58
  59 let unwind ?(tbl = Hashtbl.create 317) m =
  60  let rec unwind (e,t,s) =
  61   let cache_unwind m =
  62    try
  63     Hashtbl.find tbl m
  64    with
  65     Not_found ->
  66      let t = unwind m in
  67       Hashtbl.add tbl m t ;
  68       t in
  69   let s = List.map cache_unwind s in
  70   let rec aux l =
  71    function
  72     | A(t1,t2) -> A(aux l t1, aux l t2)
  73     | V n as x when n < l -> x
  74     | V n ->
  75        (try
  76          lift l (cache_unwind (List.nth e (n - l)))
  77         with Failure _ -> V (n - l))
  78     | L t -> L (aux (l+1) t)
  79     | B -> B in
  80   let t = aux 0 t in
  81   List.fold_left (fun f a -> A(f,a)) t s
  82 in
  83  unwind m
  84
  85 let mwhd m =
  86  let rec aux =
  87   function
  88    | (e,A(t1,t2),s) ->
  89        let t2' = aux (e,t2,[]) in
  90        let (_,t,_) = t2' in
  91        if t = B
  92         then t2'
  93         else aux (e,t1,t2'::s)
  94    | (e,L t,x::s) -> aux (x::e,t,s)
  95    | (e,V n,s) as m ->
  96       (try
  97         let e,t,s' = List.nth e n in
  98         aux (e,t,s'@s)
  99        with Failure _ -> m)
 100    | (e, B, _) -> (e, B, [])
 101    | (_,L _,[]) as m -> m
 102  in
 103   unwind (aux m)
 104
 105 end
 106
 107 module Scott =
 108 struct
 109
 110 open Pure
 111
 112 let rec mk_n n =
 113  if n = 0 then L (L (A (V 1, L (V 0)))) else L (L (A (V 0, mk_n (n-1))))
 114
 115 let dummy = V (max_int / 2)
 116
 117 let mk_match t bs =
 118  let bs = List.sort (fun (n1,_) (n2,_) -> compare n1 n2) bs in
 119  let rec aux m t =
 120   function
 121      [] -> dummy
 122    | (n,p)::tl as l ->
 123       if n = m then
 124        A (A (t, L (lift (m+1) p)), L (aux (m+1) (V 0) tl))
 125       else
 126        A (A (t, dummy), L (aux (m+1) (V 0) l))
 127  in
 128   aux 0 t bs
 129
 130 end