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