From:  <andrea.condoluci@unibo.it>
Date: Mon, 26 Jun 2017 11:47:30 +0000 (+0200)
Subject: Problems pass, but still missing computation of arities of fresh applicative vars
X-Git-Tag: weak-reduction-separation~73
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a083188139e0ae7c4db8e6f0d7b7c913006fa148;p=fireball-separation.git

Problems pass, but still missing computation of arities of fresh applicative vars
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index f71f360..8a5cc37 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -448,8 +448,8 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))
 let instantiate p x n =
  (if hd_of_i_var (cast_to_i_var !bomb) = x
    then failwithProblem p ("BOMB (" ^ string_of_nf !bomb ^ ") cannot be instantiated!"));
- (* ACL FIXME compute arity of x correctly below! *)
- let arity_of_x = -666 in
+ let arity_of_x = max_arity_tms x (all_terms p) in
+ (if arity_of_x < 0 then failwithProblem p "step on a var of negative arity");
  (* AC: FIXME compute arities correctly below! *)
  let arities = Array.to_list (Array.make (n+1) 0) in
  let p,vars = make_fresh_vars p arities in
@@ -481,7 +481,10 @@ let auto_instantiate (n,p) =
     | [], y::_ ->
       prerr_endline ("INSTANTIATING CRITICAL TO EAT " ^ string_of_var y); y
     | [], [] ->
-     let heads = List.sort compare (filter_map (fun t -> match t with `Var _ -> None | x -> hd_of x) ((match p.div with Some t -> [(t :> i_n_var)] | _ -> []) @ p.ps)) in
+     let heads =
+      List.sort compare (filter_map (
+       fun t -> match t with `Var _ -> None | x -> if arity_of_hd x < 0 then None else hd_of x
+      ) ((match p.div with Some t -> [(t :> i_n_var)] | _ -> []) @ p.ps)) in
      (match heads with
          [] -> assert false
        | x::_ ->
@@ -494,7 +497,7 @@ let auto_instantiate (n,p) =
 1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *)
 let x =
  try
-  match hd_of (List.find (fun t -> compute_special_k (Listx.Nil (t :> nf)) > 0) (all_terms p)) with
+  match hd_of (List.find (fun t -> compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t >= 0) (all_terms p)) with
       None -> assert false
     | Some x ->
        prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
@@ -757,7 +760,7 @@ let magic_conv ~div ~conv ~nums cmds =
   let special_k = compute_special_k (Listx.from_list all_tms) in (* compute initial special K *)
   (* casts *)
   let div = option_map cast_to_i_var div in
-  let conv = List.map cast_to_i_n_var conv in
+  let conv = Util.filter_map (function #i_n_var as t -> Some (cast_to_i_n_var t) | _ -> None) conv in
   let tms = List.map cast_to_i_n_var tms in
 
   let ps = List.map append_zero tms in (* crea lista applicando zeri o dummies *)
diff --git a/ocaml/num.ml b/ocaml/num.ml
index 9d80313..614dde8 100644
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -40,6 +40,12 @@ let hd_of =
  | `N _ -> None
  | `Match _ -> assert false
 
+let arity_of_hd =
+function
+  `I ((_,a),_)
+| `Var(_,a) -> a
+| _ -> 0 (* FIXME? *)
+
 let lift m (t : nf) =
  let aux_var l (n, ar) = (if n < l then n else n+m), ar in
  let rec aux_i_num_var l =
@@ -102,23 +108,9 @@ end
 
 (************ Pretty-printing ************************************)
 
-let rec print ?(l=[]) =
- function
-    `Var(n,_) -> print_name l n
-  | `N n -> string_of_int n
-  | `Match(t,_,bs_lift,bs,args) ->
-     "([" ^ print ~l (t :> nf) ^
-     " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (lift bs_lift t)) !bs) ^ "] " ^
-     String.concat " " (List.map (print ~l) args) ^ ")"
-  | `I((n,_),args) -> "(" ^ print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")"
-  | `Lam(_,nf) ->
-     let name = string_of_var (List.length l) in
-     "λ" ^ name ^ "." ^ print ~l:(name::l) (nf : nf)
-;;
-
 let rec string_of_term l =
  let rec string_of_term_w_pars l = function
-  | `Var(n,_) -> print_name l n
+  | `Var(n,ar) -> print_name l n ^ ":" ^ string_of_int ar
   | `N n -> string_of_int n
   | `I _ as t -> "(" ^ string_of_term_no_pars_app l (t :> nf) ^ ")"
   | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam l t ^ ")"
@@ -127,7 +119,7 @@ let rec string_of_term l =
      " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (lift bs_lift t)) !bs) ^ "] " ^
      String.concat " " (List.map (string_of_term l) args) ^ ")"
  and string_of_term_no_pars_app l = function
-  | `I((n,_), args) -> print_name l n ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args))
+  | `I((n,ar), args) -> print_name l n  ^ ":" ^ string_of_int ar ^ " " ^ String.concat " " (List.map (string_of_term_w_pars l) (Listx.to_list args))
   | #nf as t -> string_of_term_w_pars l t
  and string_of_term_no_pars_lam l  = function
   | `Lam(_,t) -> let name = string_of_var (List.length l) in
@@ -230,12 +222,15 @@ prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool
 (************ Parsing ************************************)
 
 let parse' strs =
+  let fix_arity = function
+  | `I((n,_),args) -> `I((n,Listx.length args),args)
+  | _ -> assert false in
   let rec aux = function
   | Parser.Lam t -> `Lam (true, aux t)
-  | Parser.App (t1, t2) -> mk_app (aux t1) (aux t2)
-  | Parser.Var v -> `Var(v,-666)
-  in let (tms, free) = Parser.parse_many strs
-  in (List.map aux tms, free)
+  | Parser.App (t1, t2) -> fix_arity (mk_app (aux t1) (aux t2))
+  | Parser.Var v -> `Var(v,0) in
+  let (tms, free) = Parser.parse_many strs in
+  List.map aux tms, free
 ;;
 
 (************** Algorithm(s) ************************)
@@ -294,3 +289,17 @@ let rec eta_subterm sub t =
 ;;
 
 let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;;
+
+
+let max_arity_tms n =
+ let aux_var l (m,a) = if n + l = m then a else -1 in
+ let rec aux l = function
+  | `Var v -> aux_var l v
+  | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms))
+  | `Lam(_,t) -> aux (l+1) t
+  | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs))
+  | `N _ -> -1
+ and aux_tms l =
+  List.fold_left (fun acc t -> Pervasives.max acc (aux l t)) ~-1 in
+ fun tms -> aux_tms 0 (tms :> nf list)
+;;
diff --git a/ocaml/num.mli b/ocaml/num.mli
index c1ad8f0..5631382 100644
--- a/ocaml/num.mli
+++ b/ocaml/num.mli
@@ -18,6 +18,7 @@ type i_n_var = nf i_n_var_
 type i_num_var = nf i_num_var_
 val hd_of_i_var : i_var -> int
 val hd_of : i_n_var -> int option
+val arity_of_hd : i_n_var -> int
 (* put t under n lambdas, lifting t accordingtly *)
 val make_lams : nf -> int -> nf
 val lift : int -> nf -> nf
@@ -41,3 +42,4 @@ val parse' : string list -> nf list * string list
 val eta_compare : nf -> nf -> int
 val eta_eq : [< nf ] -> [< nf ] -> bool
 val eta_subterm : [< nf ] -> [< nf ] -> bool
+val max_arity_tms : int -> [< nf] list -> int
diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index a0ff453..e91c580 100644
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -289,7 +289,8 @@ main ([
  (* p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ; p14 ; p15 ; p16 ; p17 ; p18 ; p19 ; p20 ; p21 ; p22 ; p23 ; p24 ; p25 ; p26 ; p27 ; p28 ; p29 ; p30 ; p31 ; p32 ; p33 ; p34 ; p35 ; p36 ; p37 ; *)
  p24 ; p25 ;
 ] @ List.map ((|>) ()) [
- q1 ; q2; q3; q4 ; q5 ; q6 ;
+ q1 ; q2; q3; q4 ; q5 ;
+ q6 ;
  (* q7 ; *)
  q8 ;
  q9 ;