librarian.ml: now the read_only .moo's are managed "correctly" (i.e. better than...

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index fa3ba4988477dd0aa777a462b5e350a65eee9f5c..147bb555fe349a063c9f6fc77cb52e7993d6bd56 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -39,60 +39,65 @@ let flexible l =
 
 exception WrongShape;;
 
-let eta_reduce after_beta_expansion after_beta_expansion_body
-     before_beta_expansion
- =
- try
-  match before_beta_expansion,after_beta_expansion_body with
-  | NCic.Appl l1, NCic.Appl l2 ->
-      let rec all_but_last check_last = function
-        | [] -> assert false
-        | [NCic.Rel 1] -> []
-        | [_] -> if check_last then raise WrongShape else []
-        | he::tl -> he::(all_but_last check_last tl)
-      in
-      let all_but_last check_last l =
-        match all_but_last check_last l with
-        | [] -> assert false
-        | [he] -> he
-        | l -> NCic.Appl l
-      in
-      let t = 
-        NCicSubstitution.subst (NCic.Sort NCic.Prop) (all_but_last true l2) in
-      let all_but_last = all_but_last false l in
-      if t = all_but_last then all_but_last else after_beta_expansion
-  | _ -> after_beta_expansion
- with WrongShape -> after_beta_expansion
+let eta_reduce = 
+  let delift_if_not_occur body orig =
+    try 
+        NCicSubstitution.psubst ~avoid_beta_redexes:true
+          (fun () -> raise WrongShape) [()] body
+    with WrongShape -> orig
+  in
+  function
+  | NCic.Lambda(name, src, NCic.Appl [hd; NCic.Rel 1]) as orig ->
+      delift_if_not_occur hd orig
+  | NCic.Lambda(name, src, NCic.Appl (hd :: l)) as orig
+    when HExtlib.list_last l = NCic.Rel 1 ->
+       let body = 
+         let args, _ = Hextlib.split_nth (List.length l - 1) l in
+         NCic.Appl (hd::args)
+       in
+       delift_if_not_occur body orig
+  | t -> t
 ;;
-
-let rec beta_expand num test_equality_only metasenv subst context t arg =
-  let rec aux (n,context as k) (metasenv, subst as acc) t' =
+  
+let rec beta_expand num test_eq_only swap metasenv subst context t arg =
+  let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
    try
     let metasenv, subst =
-     unify (* test_equality_only *) metasenv subst context
+     unify test_eq_only metasenv subst context
       (NCicSubstitution.lift n arg) t'
     in
      (metasenv, subst), C.Rel (1 + n)
    with Uncertain _ | UnificationFailure _ ->
        match t' with
-       | NCic.Rel m  -> 
-           (metasenv, subst), if m <= n then NCic.Rel m else NCic.Rel (m+1)
+       | NCic.Rel m orig -> 
+           (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
        (* andrea: in general, beta_expand can create badly typed
         terms. This happens quite seldom in practice, UNLESS we
         iterate on the local context. For this reason, we renounce
         to iterate and just lift *)
        | NCic.Meta (i,(shift,lc)) ->
            (metasenv,subst), NCic.Meta (i,(shift+1,lc))
+       | NCic.Prod (name, src, tgt) as orig ->
+           let (metasenv, subst), src1 = aux (n,context,true) acc src in 
+           let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
+           let (metasenv,subst), tgt1 = aux k (metasenv, subst) tgt in 
+           if src == src1 && tgt == tgt1 then orig else
+           NCic.Prod (name, src1, tgt1)
        | t -> 
            NCicUntrusted.map_term_fold_a 
-             (fun e (n,ctx) -> n+i,e::ctx) k aux acc t
+             (fun e (n,ctx) -> n+1,e::ctx) k aux acc t
 
   in
   let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
   let fresh_name = "Hbeta" ^ string_of_int num in
-  let (metasenv,subst), t = aux (0, context) (metasenv, subst) t in
-  let t = eta_reduce (C.Lambda (fresh_name,argty,t)) t t in
-  metasenv, subst, t
+  let (metasenv,subst,_), t1 = 
+    aux (0, context, test_eq_only) (metasenv, subst) t in
+  let t2 = eta_reduce (C.Lambda (fresh_name,argty,t1)) in
+  try 
+    ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
+    metasenv, subst, t2
+  with NCicTypeChecker.TypeCheckerFailure _ -> 
+    NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
 
 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
   let _, subst, metasenv, hd =
@@ -231,7 +236,7 @@ and unify metasenv subst context t1 t2 =
            (* we verify that none of the args is a Meta, 
               since beta expanding w.r.t a metavariable makes no sense  *)
               let subst, metasenv, beta_expanded =
-                beta_expand_many 
+                beta_expand_many (* passare swap *)
                   test_equality_only metasenv subst context t2 args ugraph 
               in
                 aux test_eq_only metasenv subst context