ocaml/num.ml

   1 open Util
   2 open Util.Vars
   3 open Pure
   4
   5 (* debug options *)
   6 let debug_display_arities = false;;
   7
   8 (************ Syntax ************************************)
   9
  10 (* Normal forms*)
  11
  12 (* Var n = n-th De Bruijn index, 0-based *)
  13
  14 (*type nf =
  15   | Lam of nf
  16   | Var of int
  17   | i
  18 and i =
  19   | I of int * nf listx
  20 ;;*)
  21 type var = int * (* arity of variable*) int;;
  22 type 'nf i_var_ = [ `I of var * 'nf Listx.listx | `Var of var ]
  23 type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ]
  24 type 'nf i_num_var_ = [
  25   | 'nf i_n_var_
  26   | `Match of 'nf i_num_var_ * (* originating var *) var * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf list
  27 ]
  28 type 'nf nf_ = [ `Lam of (* was_unpacked *) bool * 'nf nf_ * ('nf nf_) list | 'nf i_num_var_ ]
  29 type nf = nf nf_
  30 type i_var = nf i_var_;;
  31 type i_n_var = nf i_n_var_;;
  32 type i_num_var = nf i_num_var_;;
  33
  34 let hd_of_i_var =
  35  function
  36    `I ((v,_),_)
  37  | `Var (v,_) -> v
  38
  39 let hd_of =
  40  function
  41    `I ((v,_),_)
  42  | `Var(v,_) -> Some v
  43  | `N _ -> None
  44  | `Match _ -> assert false
  45
  46 let arity_of_hd =
  47 function
  48   `I ((_,a),_)
  49 | `Var(_,a) -> a
  50 | _ -> 0 (* FIXME? *)
  51
  52 let lift m (t : nf) =
  53  let aux_var l (n, ar) = (if n < l then n else n+m), ar in
  54  let rec aux_i_num_var l =
  55   function
  56     `I(v,args) -> `I(aux_var l v, Listx.map (aux l) args)
  57    | `Var v -> `Var(aux_var l v)
  58    | `N _ as x -> x
  59    | `Match(t,v,lift,bs,args) ->
  60       `Match(aux_i_num_var l t, v, lift + m, bs, List.map (aux l) args)
  61  and aux l =
  62   function
  63      #i_num_var as x -> (aux_i_num_var l x :> nf)
  64    | `Lam(b,nf,g) -> `Lam (b, aux (l+1) nf, List.map (aux (l+1)) g)
  65  in
  66   (aux 0 t : nf)
  67 ;;
  68
  69 (* put t under n lambdas, lifting t accordingtly *)
  70 let rec make_lams t =
  71  function
  72    0 -> t
  73  | n when n > 0 -> `Lam (false, lift 1 (make_lams t (n-1)), [])
  74  | _ -> assert false
  75
  76 let free_vars' =
  77  let rec aux n = function
  78     `N _ -> []
  79   | `Var(x,ar) -> if x < n then [] else [(x-n,ar)]
  80   | `I((x,ar),args) ->
  81       (if x < n then [] else [(x-n,ar)]) @
  82       List.concat (List.map (aux n) (Listx.to_list args))
  83   | `Lam(_,t,g) -> List.concat (List.map (aux (n+1)) (t::g))
  84   | `Match(t,_,liftno,bs,args) ->
  85       aux n (t :> nf) @
  86       List.concat (List.map (fun (_,t) -> aux (n-liftno) t) !bs) @
  87       List.concat (List.map (aux n) args)
  88   in aux 0
  89 ;;
  90 let free_vars = (List.map fst) ++ free_vars';;
  91
  92 module ToScott =
  93 struct
  94
  95 let delta = let open Pure in L(A(V 0, V 0))
  96
  97 let bomb = ref(`Var(-1, -666));;
  98
  99 let rec t_of_i_num_var =
 100  function
 101   | `N n -> Scott.mk_n n
 102   | `Var(v,_) as x -> assert (x <> !bomb); Pure.V v
 103   | `Match(t,_,liftno,bs,args) ->
 104       let bs = List.map (
 105         function (n,t) -> n,
 106          (if t = !bomb then delta
 107           else Pure.L (t_of_nf (lift (liftno+1) t)))
 108         ) !bs in
 109       let t = t_of_i_num_var t in
 110       let m = Scott.mk_match t bs in
 111       let m = Pure.A(m,delta) in
 112       List.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) m args
 113   | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) (Pure.V v) args
 114 and t_of_nf =
 115  function
 116   | #i_num_var as x -> t_of_i_num_var x
 117   | `Lam(b,f,g) ->
 118     let t = t_of_nf (lift (List.length g) f) in
 119     let t = List.fold_left (fun t g -> Pure.A(Pure.L t, t_of_nf g)) t g in
 120     Pure.L t
 121
 122 end
 123
 124
 125 (************ Pretty-printing ************************************)
 126
 127 (* let rec string_of_term l  = fun _ -> "";; *)
 128
 129 let string_of_term =
 130  let boundvar x = "v" ^ string_of_int x in
 131  let varname lev l n =
 132   if n < lev then boundvar (lev-n-1)
 133    else if n - lev < List.length l then List.nth l (n-lev)
 134     else "`" ^ string_of_int (n-lev) in
 135  let rec string_of_term_w_pars lev l  = function
 136   | `Var(n,ar) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "")
 137   | `N n -> string_of_int n
 138   | `I _ as t -> "(" ^ string_of_term_no_pars_app lev l t ^ ")"
 139   | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam lev l t ^ ")"
 140   | `Match(t,(v,ar),bs_lift,bs,args) ->
 141       (* assert (bs_lift = lev); *)
 142      "(["^ varname 0 l v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^",match " ^ string_of_term_no_pars lev l (t :> nf) ^
 143      " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (t :> nf)) !bs) ^ "] " ^
 144      String.concat " " (List.map (string_of_term l) (args :> nf list)) ^ ")"
 145  and string_of_term_no_pars_app lev l  = function
 146   | `I((n,ar), args) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "") ^ " " ^ String.concat " " (List.map (string_of_term_w_pars lev l) (Listx.to_list args :> nf list))
 147   | #nf as t -> string_of_term_w_pars lev l t
 148  and string_of_term_no_pars_lam lev l  = function
 149   | `Lam(_,t,g) -> "λ" ^ boundvar lev ^ ". " ^ (string_of_term_no_pars_lam (lev+1) l t)
 150      ^ (if g = [] then "" else String.concat ", " ("" :: List.map (string_of_term_no_pars (lev+1) l) g))
 151   | _ as t -> string_of_term_no_pars lev l t
 152  and string_of_term_no_pars lev l = function
 153   | `Lam _ as t -> string_of_term_no_pars_lam lev l t
 154   | #nf as t -> string_of_term_no_pars_app lev l t
 155  and string_of_term t = string_of_term_no_pars 0 t in
 156  string_of_term
 157 ;;
 158
 159 let print ?(l=[]) = string_of_term l;;
 160 let string_of_nf t = string_of_term [] (t:>nf);;
 161
 162 (************ Hereditary substitutions ************************************)
 163
 164 let cast_to_i_var =
 165  function
 166     #i_var as y -> (y : i_var)
 167   | t ->
 168     prerr_endline (print (t :> nf));
 169     assert false (* algorithm failed *)
 170
 171 let cast_to_i_n_var =
 172  function
 173     #i_n_var as y -> (y : i_n_var)
 174   | t ->
 175     prerr_endline (print (t :> nf));
 176     assert false (* algorithm failed *)
 177
 178 let cast_to_i_num_var =
 179  function
 180     #i_num_var as y -> (y : i_num_var)
 181   | t ->
 182     prerr_endline (print (t :> nf));
 183     assert false (* algorithm failed *)
 184
 185 let rec set_arity arity = function
 186 (* FIXME because onlt variables should be in branches of matches, one day *)
 187 | `Var(n,_) -> `Var(n,arity)
 188 | `N _ as t -> t
 189 | `Lam(false, t, []) -> `Lam(false, set_arity arity t, [])
 190 | `Match(t,(n,_),bs_lift,bs,args) -> `Match(t,(n,arity),bs_lift,bs,args)
 191 | `I _ | `Lam _ -> assert false
 192
 193 let minus1 n = if n = min_int then n else n - 1;;
 194
 195 let rec mk_app (h : nf) (arg : nf) =
 196 (*let res =*)
 197  match h with
 198     `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args)
 199   | `Var v -> `I(v, Listx.Nil arg)
 200   | `Lam(truelam,nf,g) -> assert (g = []); subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
 201   | `Match(t,v,lift,bs,args) -> `Match(t,v,lift,bs,List.append args [arg])
 202   | `N _ -> assert false (* Numbers cannot be applied *)
 203 (*in let l = ["v0";"v1";"v2"] in
 204 prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*)
 205
 206 and mk_appl h args =
 207  (*prerr_endline ("MK_APPL: " ^ print h ^ " " ^ String.concat " " (List.map print args));*)
 208  List.fold_left mk_app h args
 209
 210 and mk_appx h args = Listx.fold_left mk_app h args
 211
 212 and mk_match t (n,ar) bs_lift bs args =
 213  (*prerr_endline ("MK_MATCH: ([" ^ print t ^ "] " ^ String.concat " " (Listx.to_list (Listx.map (fun (n,t) -> string_of_int n ^ " => " ^ print t) bs)) ^ ") " ^ String.concat " " (List.map print args));*)
 214  match t with
 215     `N m ->
 216       (try
 217         let h = List.assoc m !bs in
 218         let h = set_arity (minus1 ar) h in
 219         let h = lift bs_lift h in
 220         mk_appl h args
 221        with Not_found ->
 222         `Match (t,(n,ar),bs_lift,bs,args))
 223   | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args)
 224
 225 and subst truelam delift_by_one what (with_what : nf) (where : nf) =
 226  let rec aux_propagate_arity ar = function
 227  | `Lam(false,t,g) when not delift_by_one -> assert (g = []); `Lam(false,aux_propagate_arity ar t,[])
 228  | `Match(`I(v,args),(x,_),liftno,bs,args') when not delift_by_one ->
 229     `Match(`I(v,args),(x,ar),liftno,bs,args')
 230  | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int); ar) else oldar)
 231  | _ as t -> t in
 232  let rec aux_i_num_var l =
 233   function
 234      `I((n,ar),args) ->
 235        if n = what + l then
 236         mk_appx (lift l (aux_propagate_arity ar with_what)) (Listx.map (aux l) args)
 237        else
 238         `I (((if delift_by_one && n >= l then n-1 else n), ar), Listx.map (aux l) args)
 239    | `Var(n,ar) ->
 240        if n = what + l then
 241         lift l (aux_propagate_arity ar with_what)
 242        else
 243         `Var((if delift_by_one && n >= l then n-1 else n), ar)
 244    | `N _ as x -> x
 245    | `Match(t,v,bs_lift,bs,args) ->
 246        let bs_lift = bs_lift + if delift_by_one then -1 else 0 in
 247        (* Warning! It now applies again the substitution in branches of matches.
 248           But careful, it does it many times, for every occurrence of
 249           the match. This is okay because what does not occur in with_what. *)
 250        let l' = l - bs_lift  in
 251        let with_what' = lift l' (with_what :> nf) in
 252        (* The following line should be the identity when delift_by_one = true because we
 253           are assuming the ts to not contain lambda-bound variables. *)
 254        bs := List.map (fun (n,t) -> n,subst truelam false what with_what' t) !bs ;
 255        let body = cast_to_i_num_var (aux_i_num_var l t) in
 256        mk_match body v bs_lift bs (List.map (aux l) (args :> nf list))
 257  and aux l(*lift*) =
 258 (*function iii -> let res = match iii with*)
 259   function
 260    | #i_num_var as x -> aux_i_num_var l x
 261    | `Lam(b, nf, g) -> `Lam(b, aux (l+1) nf, List.map (aux (l+1)) g)
 262 (*in let ll = ["v0";"v1";"v2"] in
 263 prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool delift_by_one ^ " what:" ^ (List.nth ll what) ^ " with_what:" ^ print ~l:ll with_what ^ " where:" ^ print ~l:ll iii ^ " res:" ^ print ~l:ll res); res*)
 264  in
 265   aux 0 where
 266 ;;
 267
 268 (************** Algorithm(s) ************************)
 269
 270 let eta_compare x y =
 271  (* let clex a b = let diff = ? a b in if diff = 0 then cont () else 0 in *)
 272  let clex aux1 aux2 (a1,a2) (b1,b2) =
 273   let diff = aux1 a1 b1 in if diff = 0 then aux2 a2 b2 else diff in
 274  let rec lex aux l1 l2 =
 275   match l1,l2 with
 276  | [], [] -> 0
 277  | [], _ -> -1
 278  | _, [] -> 1
 279  | x::xs, y::ys -> clex aux (lex aux) (x,xs) (y,ys) in
 280  let rec aux t1 t2 = match t1, t2 with
 281   | `Var(n,_) , `Var(m,_) -> compare n m
 282   | `I((n1,_), l1), `I((n2,_), l2) ->
 283     clex compare (lex aux) (n1, Listx.to_list l1) (n2, Listx.to_list l2)
 284   | `Lam _, `N _ -> -1
 285   | `N _, `Lam _ -> 1
 286   | `Lam(_,t1,_), `Lam(_,t2,_) -> aux t1 t2
 287   | `Lam(_,t1,_), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
 288   | t2, `Lam(_,t1,_) ->   aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
 289   | `N n1, `N n2 -> compare n1 n2
 290   | `Match(u,_,bs_lift,bs,args), `Match(u',_,bs_lift',bs',args') ->
 291     let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in
 292     let bs' = List.sort (fun (n,_) (m,_) -> compare n m) !bs' in
 293     clex aux (clex (lex (clex compare aux)) (lex aux)) ((u :> nf), (bs, args)) ((u' :> nf), (bs', args'))
 294   | `Match _, _ -> -1
 295   | _, `Match _ -> 1
 296   | `N _, _ -> -1
 297   | _, `N _ -> 1
 298   | `I _, _ -> -1
 299   | _, `I _ -> 1
 300   in aux x y
 301 ;;
 302
 303 let eta_eq (#nf as x) (#nf as y) = 0 = eta_compare x y ;;
 304
 305 let rec eta_subterm sub t =
 306  if eta_eq sub t then true else
 307   match t with
 308   | `Lam(_,t,g) -> List.exists (eta_subterm (lift 1 sub)) (t::g)
 309   | `Match(u,ar,liftno,bs,args) ->
 310      eta_subterm sub (u :> nf)
 311      || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
 312      || List.exists (eta_subterm sub) (args :> nf list)
 313   | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
 314    | `Var(v',_) -> v = v'
 315    | `I((v',_), args') -> v = v'
 316     && Listx.length args' < Listx.length args
 317     && List.for_all (fun (x,y) -> eta_eq x y) (List.combine (Util.take (Listx.length args') (Listx.to_list args)) (Listx.to_list args'))
 318    | _ -> false
 319    )
 320   | `N _ | `Var _ -> false
 321 ;;
 322
 323 let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;;
 324
 325
 326 let max_arity_tms n =
 327  let max a b = match a, b with
 328   | None, None -> None
 329   | None, Some x
 330   | Some x, None -> Some x
 331   | Some x, Some y -> Some (Pervasives.max x y) in
 332  let aux_var l (m,a) = if n + l = m then Some a else None in
 333  let rec aux l = function
 334   | `Var v -> aux_var l v
 335   | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms))
 336   | `Lam(_,t, g) -> List.fold_left (fun n t -> max n (aux (l+1) t)) None (t::g)
 337   | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs))
 338   | `N _ -> None
 339  and aux_tms l =
 340   List.fold_left (fun acc t -> max acc (aux l t)) None in
 341  fun tms -> aux_tms 0 (tms :> nf list)
 342 ;;
 343
 344 let get_first_args var =
 345 let rec aux l = function
 346 | `Lam(_,t,_) -> aux (l+1) t
 347 | `Match(u,orig,liftno,bs,args) -> Util.concat_map (aux l) args
 348 | `I((n,_), args) -> if n = var + l then [Listx.last args] else []
 349 | `N _
 350 | `Var _ -> []
 351 in aux 0
 352 ;;
 353
 354 let compute_arities m =
 355  let rec aux n tms =
 356   if n = 0
 357    then []
 358    else
 359     let tms = Util.filter_map (function `Lam(_,t,_) -> Some t | _ -> None ) tms in
 360     let arity = match max_arity_tms (m-n) tms with None -> -666 | Some x -> x in
 361      arity :: (aux (n-1) tms)
 362  in fun tms -> List.rev (aux m tms)
 363 ;;
 364
 365 let compute_arities var special_k all_tms =
 366  let tms = List.fold_left (fun acc t -> acc @ (get_first_args var t)) [] all_tms in
 367  compute_arities special_k tms
 368 ;;