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