From: acondolu <andrea.condoluci@unibo.it>
Date: Wed, 28 Jun 2017 14:29:21 +0000 (+0200)
Subject: Minor fixes
X-Git-Tag: weak-reduction-separation~71
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=83894fd0e03553e80e42a741827e1e6233417750;p=fireball-separation.git

Minor fixes
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index c627151..acfec51 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -12,42 +12,12 @@ type problem =
  ; ps: i_n_var list (* the n-th inert must become n *)
  ; sigma: (int * nf) list (* the computed substitution *)
  ; deltas: (int * nf) list ref list (* collection of all branches *)
- }
-
-
-(* let heads = Util.sort_uniq (List.map hd_of_i_var p.ps) in
-for all head
-  List.map (fun (_, bs) -> List.map (fun (x,_) -> List.nth p.ps x) !bs) p.deltas *)
-
-(* let ($) f x = f x;; *)
-
-(* let subterms tms freshno =
- let apply_var =
-  let no = ref freshno in
-  function t -> incr no; mk_app t (`Var !no) in
- let applicative hd args = snd (
-    List.fold_left (fun (hd, acc) t -> let hd = mk_app hd t in hd, hd::acc) (hd, []) args) in
- let rec aux t = match t with
- | `Var _ -> []
- | `I(v,ts) ->
-    (* applicative (`Var v) (Listx.to_list ts) @  *)
-     Util.concat_map aux (Listx.to_list ts) @ List.map apply_var (Listx.to_list ts)
- | `Lam(_,_,t) -> aux (lift ~-1 t)
- | `Match(u,_,bs_lift,bs,args) ->
-    aux (u :> nf) @
-     (* applicative (`Match(u,bs_lift,bs,[])) args @ *)
-      Util.concat_map aux args @ List.map apply_var args
-      (* @ Util.concat_map (aux ++ (lift bs_lift) ++ snd) !bs *)
- | `N _ -> []
- in let tms' = (* Util.sort_uniq ~compare:eta_compare*) (Util.concat_map aux tms) in
- tms @ tms'
- (* List.map (fun (t, v) -> match t with `N _ -> t | _ -> mk_app t v) (List.combine tms (List.mapi (fun i _ -> `Var(freshno+i)) tms)) *)
-;; *)
+};;
 
 let all_terms p =
-(match p.div with None -> [] | Some t -> [(t :> i_n_var)])
-@ p.conv
-@ p.ps
+ (match p.div with None -> [] | Some t -> [(t :> i_n_var)])
+ @ p.conv
+ @ p.ps
 ;;
 
 let problem_measure p = 0 ;;
@@ -84,17 +54,16 @@ let make_fresh_var p arity =
 
 let make_fresh_vars p arities =
  List.fold_right
-  (* fold_left vs. fold_right hides/shows the bug in problem q7 *)
   (fun arity (p, vars) -> let p, var = make_fresh_var p arity in p, var::vars)
   arities
   (p, [])
 ;;
 
 let simple_expand_match ps =
-  let rec aux level = function
+ let rec aux level = function
   | #i_num_var as t -> aux_i_num_var level t
   | `Lam(b,t) -> `Lam(b,aux (level+1) t)
-  and aux_i_num_var level = function
+ and aux_i_num_var level = function
   | `Match(u,v,bs_lift,bs,args) as torig ->
     let u = aux_i_num_var level u in
     bs := List.map (fun (n, x) -> n, aux 0 x) !bs;
@@ -111,7 +80,8 @@ let simple_expand_match ps =
        `Match(cast_to_i_num_var u,v,bs_lift,bs,List.map (aux level) args))
   | `I(v,args) -> `I(v,Listx.map (aux level) args)
   | `N _ | `Var _ as t -> t
-in aux_i_num_var 0;;
+ in aux_i_num_var 0
+;;
 
 let fixpoint f =
  let rec aux x = let x' = f x in if x <> x' then aux x' else x in aux
@@ -494,7 +464,7 @@ let auto_instantiate (n,p) =
   | x::_, _ ->
       prerr_endline ("INSTANTIATING " ^ string_of_var x);
       x in
-(* Strategy that decreases the special_k to 0 first (round robin)
+(* Strategy that  decreases the special_k to 0 first (round robin)
 1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *)
 let x =
  try