From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 28 Sep 2009 16:14:46 +0000 (+0000)
Subject: - fixed bug in coercion application, input/output swapped in unification
X-Git-Tag: make_still_working~3426
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f1c4852a4359cf278ed00d73d608856ff46bafbb;p=helm.git

- fixed bug in coercion application, input/output swapped in unification
- experimental automatic reduction of projections in apply-subst-metasenv
---

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index 633ecea57..fd3fd5f79 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -168,7 +168,37 @@ let clean_or_fix_dependent_abstrations ctx t =
     aux (List.map fst ctx) t
 ;;
 
-let apply_subst subst context t = 
+let rec fire_projection_redex () = function
+  | C.Meta _ as t -> t
+  | C.Appl(C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r)::args as ol)as ot->
+      let l = List.map (fire_projection_redex ()) ol in
+      let t = if l == ol then ot else C.Appl l in
+      let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes r in
+      let conclude () =
+        let l' = HExtlib.sharing_map (fire_projection_redex ()) l in
+        if l == l' then t else C.Appl l'
+      in
+      if (*pragma <> `Projection ||*) List.length args < rno then conclude ()
+      else
+        (match List.nth args rno with
+        | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->
+            let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *)
+            let t = C.Appl (fbody::args) in
+            (match NCicReduction.head_beta_reduce ~delta:max_int t with
+            | C.Match (_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat])->
+                  let _,kargs = HExtlib.split_nth leftno kargs in
+                  NCicReduction.head_beta_reduce 
+                    ~delta:max_int (C.Appl (pat :: kargs))
+            | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat]) :: args) ->
+                  let _,kargs = HExtlib.split_nth leftno kargs in
+                  NCicReduction.head_beta_reduce 
+                    ~delta:max_int (C.Appl (pat :: kargs @ args)) 
+            | _ -> conclude ()) 
+        | _ -> conclude ())
+  | t -> NCicUtils.map (fun _ _ -> ()) () fire_projection_redex t
+;;
+
+let apply_subst ?(fix_projections=false) subst context t = 
  let rec apply_subst subst () =
  function
     NCic.Meta (i,lc) ->
@@ -187,10 +217,12 @@ let apply_subst subst context t =
                    apply_subst subst () (NCicSubstitution.lift n t)) l))))
   | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t
  in
-  clean_or_fix_dependent_abstrations context (apply_subst subst () t)
+ (if fix_projections then fire_projection_redex () else fun x -> x)
+    (clean_or_fix_dependent_abstrations context (apply_subst subst () t))
 ;;
 
-let apply_subst_context subst context =
+let apply_subst_context ~fix_projections subst context =
+  let apply_subst = apply_subst ~fix_projections in
   let rec aux c = function 
     | [] -> []
     | (name,NCic.Decl t as e) :: tl -> 
@@ -206,6 +238,11 @@ let rec apply_subst_metasenv subst = function
   | [] -> []
   | (i,_) :: _ when List.mem_assoc i subst -> assert false
   | (i,(name,ctx,ty)) :: tl ->
-      (i,(name,apply_subst_context subst ctx,apply_subst subst ctx ty)) ::
+      (i,(name,apply_subst_context ~fix_projections:true subst ctx,
+               apply_subst ~fix_projections:true subst ctx ty)) ::
          apply_subst_metasenv subst tl
 ;;
+
+(* hide optional arg *)
+let apply_subst s c t = apply_subst s c t;;
+
diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index a1ce81470..a74946f1e 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -380,15 +380,16 @@ and try_coercions rdb
         (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
   | (_,metasenv, newterm, newtype, meta)::tl ->
       try 
+          pp (lazy("K=" ^ NCicPp.ppterm ~metasenv ~subst ~context newterm));
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context
             ^ "\nMENV: " ^
             NCicPp.ppmetasenv metasenv ~subst
             ^ "\nOF: " ^
-            NCicPp.ppterm ~metasenv ~subst ~context meta ^  " === " ^
-            NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n"));
+            NCicPp.ppterm ~metasenv ~subst ~context t ^  " === " ^
+            NCicPp.ppterm ~metasenv ~subst ~context meta ^ "\n"));
         let metasenv, subst = 
-          NCicUnification.unify rdb metasenv subst context meta t
+          NCicUnification.unify rdb metasenv subst context t meta
         in
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context