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+m else n)
  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 (if what < 0 then n = what else 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    | B -> B
  44  in
  45   aux 0
  46
  47 (* let rec whd =
  48  function
  49   | A(t1, t2) ->
  50      let t2 = whd t2 in
  51      let t1 = whd t1 in
  52       (match t1 with
  53         | L f -> whd (subst true 0 t2 f)
  54         | V _
  55         | A _ -> A(t1,t2))
  56   | V _
  57   | L _ as t -> t
  58 *)
  59
  60 let unwind ?(tbl = Hashtbl.create 317) m =
  61  let rec unwind (e,t,s) =
  62   let cache_unwind m =
  63    try
  64     Hashtbl.find tbl m
  65    with
  66     Not_found ->
  67      let t = unwind m in
  68       Hashtbl.add tbl m t ;
  69       t in
  70   let s = List.map cache_unwind s in
  71   let rec aux l =
  72    function
  73     | A(t1,t2) -> A(aux l t1, aux l t2)
  74     | V n as x when n < l -> x
  75     | V n ->
  76        (try
  77          lift l (cache_unwind (List.nth e (n - l)))
  78         with Failure _ -> V n)
  79     | L t -> L (aux (l+1) t)
  80     | B -> B in
  81   let t = aux 0 t in
  82   List.fold_left (fun f a -> A(f,a)) t s
  83 in
  84  unwind m
  85
  86
  87 (* let rec print_machine (e,t,s) =
  88  "[" ^ String.concat "," (List.map print_machine e) ^
  89      "|" ^ print t ^ "|" ^
  90      String.concat "," (List.map print_machine s) ^ "]"
  91 ;; *)
  92
  93   let omega = let delta = L(A(V 0, V 0)) in A(delta,delta)
  94
  95   let rec is_divergent =
  96    function
  97       t when t = omega -> true
  98     | A(t,_) -> is_divergent t
  99     | L(t) -> is_divergent t
 100     | _ -> false
 101
 102   let mwhd m =
 103    let rec aux g =
 104     function
 105     (* mmm -> print_endline (print_machine mmm); match mmm with *)
 106         m when is_divergent (unwind m) -> [], B, []
 107      | (e,A(t1,t2),s) ->
 108          let t2' = aux g (e,t2,[]) in
 109          let (_,t,_) = t2' in
 110          if t = B
 111           then t2'
 112           else aux g (e,t1,t2'::s)
 113      | (e,L t,x::s) -> aux g (x::e,t,s)
 114      | (e,V n,s) as m ->
 115         (try
 116           let e,t,s' = List.nth e n in
 117           aux g (e,t,s'@s)
 118          with Invalid_argument _ | Failure _ -> m
 119          )
 120      | (e, B, _) -> (e, B, [])
 121      | (e, L t, []) ->
 122       let t = subst true 0 (V g) t in
 123       (* print_endline ("." ^ string_of_int g ^ " " ^ print_machine ((e,t,[]))); *)
 124       let m' = aux (g-1) (e, t, []) in
 125       let t' = unwind m' in
 126       (* print_endline ("=" ^ print t');
 127       print_endline ("==" ^ print (lift 1 t')); *)
 128       let t' = subst false g (V 0) (lift 1 t') in
 129       (* print_endline ("===" ^ print t'); *)
 130       [], (if t' = B then t' else L t'), []
 131
 132    in
 133     unwind (aux ~-2 m)
 134 ;;
 135
 136 let omega should_explode =
 137  if should_explode
 138   then let f t = A(t,t) in f (L (f (V 0)))
 139   else B
 140 ;;
 141
 142 let diverged = (=) B;;
 143
 144 (* Note: maps only variables <= freshno *)
 145 let env_of_sigma freshno sigma =
 146  let rec aux n =
 147   if n > freshno then
 148    []
 149   else
 150    let e = aux (n+1) in
 151    (try
 152     e, lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
 153    with
 154     Not_found -> ([], V n, []) ) :: e
 155  in aux 0
 156
 157 end
 158
 159 module Scott =
 160 struct
 161
 162 open Pure
 163
 164 let rec mk_n n =
 165  if n = 0 then L (L (A (V 1, L (V 0)))) else L (L (A (V 0, mk_n (n-1))))
 166
 167 let dummy = V (max_int / 2)
 168
 169 let mk_match t bs =
 170  let bs = List.sort (fun (n1,_) (n2,_) -> compare n1 n2) bs in
 171  let rec aux m t =
 172   function
 173      [] -> dummy
 174    | (n,p)::tl as l ->
 175       if n = m then
 176        A (A (t, L (lift (m+1) p)), L (aux (m+1) (V 0) tl))
 177       else
 178        A (A (t, dummy), L (aux (m+1) (V 0) l))
 179  in
 180   aux 0 t bs
 181
 182 end