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