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 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) -> `Lam (b, aux (l+1) nf)
  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) -> aux (n+1) t
  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) -> Pure.L (t_of_nf f)
 118
 119 end
 120
 121
 122 (************ Pretty-printing ************************************)
 123
 124 (* let rec string_of_term l  = fun _ -> "";; *)
 125
 126 let string_of_term =
 127  let boundvar x = "v" ^ string_of_int x in
 128  let varname lev l n =
 129   if n < lev then boundvar (lev-n-1)
 130    else if n - lev < List.length l then List.nth l (n-lev)
 131     else "`" ^ string_of_int (n-lev) in
 132  let rec string_of_term_w_pars lev l  = function
 133   | `Var(n,ar) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "")
 134   | `N n -> string_of_int n
 135   | `I _ as t -> "(" ^ string_of_term_no_pars_app lev l t ^ ")"
 136   | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam lev l t ^ ")"
 137   | `Match(t,(v,ar),bs_lift,bs,args) ->
 138       (* assert (bs_lift = lev); *)
 139      "(["^ varname 0 l v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^",match " ^ string_of_term_no_pars lev l (t :> nf) ^
 140      " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (t :> nf)) !bs) ^ "] " ^
 141      String.concat " " (List.map (string_of_term l) (args :> nf list)) ^ ")"
 142  and string_of_term_no_pars_app lev l  = function
 143   | `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))
 144   | #nf as t -> string_of_term_w_pars lev l t
 145  and string_of_term_no_pars_lam lev l  = function
 146   | `Lam(_,t) -> "λ" ^ boundvar lev ^ ". " ^ (string_of_term_no_pars_lam (lev+1) l t)
 147   | _ as t -> string_of_term_no_pars lev l t
 148  and string_of_term_no_pars lev l = function
 149   | `Lam _ as t -> string_of_term_no_pars_lam lev l t
 150   | #nf as t -> string_of_term_no_pars_app lev l t
 151  and string_of_term t = string_of_term_no_pars 0 t in
 152  string_of_term
 153 ;;
 154
 155 let print ?(l=[]) = string_of_term l;;
 156 let string_of_nf t = string_of_term [] (t:>nf);;
 157
 158 (************ Hereditary substitutions ************************************)
 159
 160 let cast_to_i_var =
 161  function
 162     #i_var as y -> (y : i_var)
 163   | t ->
 164     prerr_endline (print (t :> nf));
 165     assert false (* algorithm failed *)
 166
 167 let cast_to_i_n_var =
 168  function
 169     #i_n_var as y -> (y : i_n_var)
 170   | t ->
 171     prerr_endline (print (t :> nf));
 172     assert false (* algorithm failed *)
 173
 174 let cast_to_i_num_var =
 175  function
 176     #i_num_var as y -> (y : i_num_var)
 177   | t ->
 178     prerr_endline (print (t :> nf));
 179     assert false (* algorithm failed *)
 180
 181 let rec set_arity arity = function
 182 (* FIXME because onlt variables should be in branches of matches, one day *)
 183 | `Var(n,_) -> `Var(n,arity)
 184 | `N _ as t -> t
 185 | `Lam(false, t) -> `Lam(false, set_arity arity t)
 186 | `Match(t,(n,_),bs_lift,bs,args) -> `Match(t,(n,arity),bs_lift,bs,args)
 187 | `I _ | `Lam _ -> assert false
 188
 189 let minus1 n = if n = min_int then n else n - 1;;
 190
 191 let rec mk_app (h : nf) (arg : nf) =
 192 (*let res =*)
 193  match h with
 194     `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args)
 195   | `Var v -> `I(v, Listx.Nil arg)
 196   | `Lam(truelam,nf) -> subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
 197   | `Match(t,v,lift,bs,args) -> `Match(t,v,lift,bs,List.append args [arg])
 198   | `N _ -> assert false (* Numbers cannot be applied *)
 199 (*in let l = ["v0";"v1";"v2"] in
 200 prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*)
 201
 202 and mk_appl h args =
 203  (*prerr_endline ("MK_APPL: " ^ print h ^ " " ^ String.concat " " (List.map print args));*)
 204  List.fold_left mk_app h args
 205
 206 and mk_appx h args = Listx.fold_left mk_app h args
 207
 208 and mk_match t (n,ar) bs_lift bs args =
 209  (*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));*)
 210  match t with
 211     `N m ->
 212       (try
 213         let h = List.assoc m !bs in
 214         let h = set_arity (minus1 ar) h in
 215         let h = lift bs_lift h in
 216         mk_appl h args
 217        with Not_found ->
 218         `Match (t,(n,ar),bs_lift,bs,args))
 219   | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args)
 220
 221 and subst truelam delift_by_one what (with_what : nf) (where : nf) =
 222  let rec aux_propagate_arity ar = function
 223  | `Lam(false, t) when not delift_by_one -> `Lam(false, aux_propagate_arity ar t)
 224  | `Match(`I(v,args),(x,_),liftno,bs,args') when not delift_by_one ->
 225     `Match(`I(v,args),(x,ar),liftno,bs,args')
 226  | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int); ar) else oldar)
 227  | _ as t -> t in
 228  let rec aux_i_num_var l =
 229   function
 230      `I((n,ar),args) ->
 231        if n = what + l then
 232         mk_appx (lift l (aux_propagate_arity ar with_what)) (Listx.map (aux l) args)
 233        else
 234         `I (((if delift_by_one && n >= l then n-1 else n), ar), Listx.map (aux l) args)
 235    | `Var(n,ar) ->
 236        if n = what + l then
 237         lift l (aux_propagate_arity ar with_what)
 238        else
 239         `Var((if delift_by_one && n >= l then n-1 else n), ar)
 240    | `N _ as x -> x
 241    | `Match(t,v,bs_lift,bs,args) ->
 242        let bs_lift = bs_lift + if delift_by_one then -1 else 0 in
 243        (* Warning! It now applies again the substitution in branches of matches.
 244           But careful, it does it many times, for every occurrence of
 245           the match. This is okay because what does not occur in with_what. *)
 246        let l' = l - bs_lift  in
 247        let with_what' = lift l' (with_what :> nf) in
 248        (* The following line should be the identity when delift_by_one = true because we
 249           are assuming the ts to not contain lambda-bound variables. *)
 250        bs := List.map (fun (n,t) -> n,subst truelam false what with_what' t) !bs ;
 251        let body = cast_to_i_num_var (aux_i_num_var l t) in
 252        mk_match body v bs_lift bs (List.map (aux l) (args :> nf list))
 253  and aux l(*lift*) =
 254 (*function iii -> let res = match iii with*)
 255   function
 256    | #i_num_var as x -> aux_i_num_var l x
 257    | `Lam(b, nf) -> `Lam(b, aux (l+1) nf)
 258 (*in let ll = ["v0";"v1";"v2"] in
 259 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*)
 260  in
 261   aux 0 where
 262 ;;
 263
 264 (************** Algorithm(s) ************************)
 265
 266 let eta_compare x y =
 267  (* let clex a b = let diff = ? a b in if diff = 0 then cont () else 0 in *)
 268  let clex aux1 aux2 (a1,a2) (b1,b2) =
 269   let diff = aux1 a1 b1 in if diff = 0 then aux2 a2 b2 else diff in
 270  let rec lex aux l1 l2 =
 271   match l1,l2 with
 272  | [], [] -> 0
 273  | [], _ -> -1
 274  | _, [] -> 1
 275  | x::xs, y::ys -> clex aux (lex aux) (x,xs) (y,ys) in
 276  let rec aux t1 t2 = match t1, t2 with
 277   | `Var(n,_) , `Var(m,_) -> compare n m
 278   | `I((n1,_), l1), `I((n2,_), l2) ->
 279     clex compare (lex aux) (n1, Listx.to_list l1) (n2, Listx.to_list l2)
 280   | `Lam _, `N _ -> -1
 281   | `N _, `Lam _ -> 1
 282   | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2
 283   | `Lam(_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
 284   | t2, `Lam(_,t1) ->   aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
 285   | `N n1, `N n2 -> compare n1 n2
 286   | `Match(u,_,bs_lift,bs,args), `Match(u',_,bs_lift',bs',args') ->
 287     let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in
 288     let bs' = List.sort (fun (n,_) (m,_) -> compare n m) !bs' in
 289     clex aux (clex (lex (clex compare aux)) (lex aux)) ((u :> nf), (bs, args)) ((u' :> nf), (bs', args'))
 290   | `Match _, _ -> -1
 291   | _, `Match _ -> 1
 292   | `N _, _ -> -1
 293   | _, `N _ -> 1
 294   | `I _, _ -> -1
 295   | _, `I _ -> 1
 296   in aux x y
 297 ;;
 298
 299 let eta_eq (#nf as x) (#nf as y) = 0 = eta_compare x y ;;
 300
 301 let rec eta_subterm sub t =
 302  if eta_eq sub t then true else
 303   match t with
 304   | `Lam(_,t') -> eta_subterm (lift 1 sub) t'
 305   | `Match(u,ar,liftno,bs,args) ->
 306      eta_subterm sub (u :> nf)
 307      || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
 308      || List.exists (eta_subterm sub) (args :> nf list)
 309   | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
 310    | `Var(v',_) -> v = v'
 311    | `I((v',_), args') -> v = v'
 312     && Listx.length args' < Listx.length args
 313     && 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'))
 314    | _ -> false
 315    )
 316   | `N _ | `Var _ -> false
 317 ;;
 318
 319 let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;;
 320
 321
 322 let max_arity_tms n =
 323  let max a b = match a, b with
 324   | None, None -> None
 325   | None, Some x
 326   | Some x, None -> Some x
 327   | Some x, Some y -> Some (Pervasives.max x y) in
 328  let aux_var l (m,a) = if n + l = m then Some a else None in
 329  let rec aux l = function
 330   | `Var v -> aux_var l v
 331   | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms))
 332   | `Lam(_,t) -> aux (l+1) t
 333   | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs))
 334   | `N _ -> None
 335  and aux_tms l =
 336   List.fold_left (fun acc t -> max acc (aux l t)) None in
 337  fun tms -> aux_tms 0 (tms :> nf list)
 338 ;;
 339
 340 let get_first_args var =
 341 let rec aux l = function
 342 | `Lam(_,t) -> aux (l+1) t
 343 | `Match(u,orig,liftno,bs,args) -> Util.concat_map (aux l) args
 344 | `I((n,_), args) -> if n = var + l then [Listx.last args] else []
 345 | `N _
 346 | `Var _ -> []
 347 in aux 0
 348 ;;
 349
 350 let compute_arities m =
 351  let rec aux n tms =
 352   if n = 0
 353    then []
 354    else
 355     let tms = Util.filter_map (function `Lam(_,t) -> Some t | _ -> None ) tms in
 356     let arity = match max_arity_tms (m-n) tms with None -> -666 | Some x -> x in
 357      arity :: (aux (n-1) tms)
 358  in fun tms -> List.rev (aux m tms)
 359 ;;
 360
 361 let compute_arities var special_k all_tms =
 362  let tms = List.fold_left (fun acc t -> acc @ (get_first_args var t)) [] all_tms in
 363  compute_arities special_k tms
 364 ;;