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