From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 6 Apr 2009 15:43:14 +0000 (+0000)
Subject: unification:
X-Git-Tag: make_still_working~4115
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d174e54c365ab9df38367de9336c213a03be3c27;p=helm.git

unification:
 - the case

    (? args) v.s. ?(tag:OUT_SCOPE)

   is considered as a pattern-driven delifting.
 - the case ? args v.s. t is reduced to ?[args] v.s. t
 - eta-contraction reimplemented
 - beta-expand no longer used

delift:
 - handle out/in scope tag

ntactics:
 - elim sets the out_scope tag for 1 entry
---

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 5062353cd..1a2b5471b 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -21,17 +21,19 @@ let newmeta =
 
 exception NotInTheList;;
 
-let position n (shift, lc) =
+let position to_skip n (shift, lc) =
   match lc with
+  | NCic.Irl _ when to_skip > 0 -> assert false  (* unclear to me *)
   | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList
   | NCic.Irl _ -> n - shift
   | NCic.Ctx tl ->
-      let rec aux k = function 
+      let rec aux to_skip k = function 
          | [] -> raise NotInTheList
+         | _ :: tl when to_skip > 0 -> aux (to_skip - 1) (k+1) tl
          | (NCic.Rel m)::_ when m + shift = n -> k
-         | _::tl -> aux (k+1) tl 
+         | _::tl -> aux to_skip (k+1) tl 
       in
-       aux 1 tl
+       aux to_skip 1 tl
 ;;
 
 let pack_lc orig = 
@@ -193,25 +195,53 @@ and restrict metasenv subst i restrictions =
     | NCicUtils.Meta_not_found _ -> assert false
 ;;
 
+let rec flexible_arg subst = function 
+  | NCic.Meta (i,_) | NCic.Appl (NCic.Meta (i,_) :: _)-> 
+      (try 
+        let _,_,t,_ = List.assoc i subst in
+        flexible_arg subst t
+      with Not_found -> true)
+  | _ -> false
+;;
+
+let flexible subst l = List.exists (flexible_arg subst) l;;
+
+let in_scope_tag  = "tag:in_scope" ;;
+let out_scope_tag_prefix = "tag:out_scope:" 
+let out_scope_tag n = out_scope_tag_prefix ^ string_of_int n ;;
+let is_out_scope_tag tag =
+   String.length tag > String.length out_scope_tag_prefix &&
+   String.sub tag 0 (String.length out_scope_tag_prefix) = out_scope_tag_prefix 
+;;
+let int_of_out_scope_tag tag = 
+  int_of_string
+   (String.sub tag (String.length out_scope_tag_prefix)
+     (String.length tag - (String.length out_scope_tag_prefix)))
+;;
+
+
 (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), 
    otherwise the occur check does not make sense in case of unification
    of ?n with ?n *)
 let delift ~unify metasenv subst context n l t =
-  let unify_list = 
+  let unify_list in_scope = 
     match l with
     | _, NCic.Irl _ -> fun _ _ _ _ _ -> None
     | shift, NCic.Ctx l -> fun metasenv subst context k t ->
-       HExtlib.list_findopt
-        (fun li i ->
-          let li = NCicSubstitution.lift (k+shift) li in
-          match unify metasenv subst context li t with
-          | Some (metasenv,subst) -> 
-              Some ((metasenv, subst), NCic.Rel (i+1+k))
-          | None -> None)
-        l
+       if flexible_arg subst t then None else
+         let lb = List.map (fun t -> t, flexible_arg subst t) l in
+         HExtlib.list_findopt
+          (fun (li,flexible) i ->
+            if flexible || i < in_scope then None else
+             let li = NCicSubstitution.lift (k+shift) li in
+             match unify metasenv subst context li t with
+             | Some (metasenv,subst) -> 
+                 Some ((metasenv, subst), NCic.Rel (i+1+k))
+             | None -> None)
+          lb
   in
-  let rec aux k (metasenv, subst as ms) t = 
-   match unify_list metasenv subst context k t with
+  let rec aux (context,k,in_scope) (metasenv, subst as ms) t = 
+   match unify_list in_scope metasenv subst context k t with
    | Some x -> x
    | None -> 
     match t with 
@@ -220,13 +250,13 @@ let delift ~unify metasenv subst context n l t =
         (try
           match List.nth context (n-k-1) with
           | _,NCic.Def (bo,_) -> 
-                (try ms, NCic.Rel ((position (n-k) l) + k)
+                (try ms, NCic.Rel ((position in_scope (n-k) l) + k)
                  with NotInTheList ->
                 (* CSC: This bit of reduction hurts performances since it is
                  * possible to  have an exponential explosion of the size of the
                  * proof. required for nat/nth_prime.ma *)
-                  aux k ms (NCicSubstitution.lift n bo))
-          | _,NCic.Decl _ -> ms, NCic.Rel ((position (n-k) l) + k)
+                  aux (context,k,in_scope) ms (NCicSubstitution.lift n bo))
+          | _,NCic.Decl _ -> ms, NCic.Rel ((position in_scope (n-k) l) + k)
         with Failure _ -> assert false) (*Unbound variable found in delift*)
     | NCic.Meta (i,_) when i=n ->
          raise (MetaSubstFailure (lazy (Printf.sprintf (
@@ -237,8 +267,13 @@ let delift ~unify metasenv subst context n l t =
     | NCic.Meta (i,l1) as orig ->
         (try
            let tag,_,t,_ = NCicUtils.lookup_subst i subst in
-           (match tag with None -> () | Some tag -> prerr_endline tag);
-           aux k ms (NCicSubstitution.subst_meta l1 t)
+           let in_scope = 
+             match tag with 
+             | Some tag when tag = in_scope_tag -> 0
+             | Some tag when is_out_scope_tag tag -> int_of_out_scope_tag tag
+             | _ -> in_scope
+           in
+           aux (context,k,in_scope) ms (NCicSubstitution.subst_meta l1 t)
          with NCicUtils.Subst_not_found _ ->
            if snd l1 = NCic.Irl 0 || snd l1 = NCic.Ctx [] then ms, orig
            else
@@ -307,7 +342,7 @@ let delift ~unify metasenv subst context n l t =
                     | t::tl ->
                         let ms, tbr, tl = deliftl tbr (j+1) ms tl in
                         try 
-                          let ms, t = aux k ms t in 
+                          let ms, t = aux (context,k,in_scope) ms t in 
                           ms, tbr, t::tl
                         with
                         | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl
@@ -330,9 +365,11 @@ let delift ~unify metasenv subst context n l t =
                       restrict metasenv subst i to_be_r in
                     (metasenv, subst), NCic.Meta(newmeta,l1))
 
-    | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
+    | t -> 
+        NCicUntrusted.map_term_fold_a 
+          (fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t
   in
-   try aux 0 (metasenv,subst) t
+   try aux (context,0,0) (metasenv,subst) t
    with NotInTheList ->
       (* This is the case where we fail even first order unification. *)
       (* The reason is that our delift function is weaker than first  *)
diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index 293e3a01f..1ed2fcee3 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.mli
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli
@@ -67,3 +67,9 @@ val saturate:
     NCic.context -> NCic.term -> int ->
        NCic.term * NCic.metasenv * NCic.term list
 
+val flexible: NCic.substitution -> NCic.term list -> bool
+
+val in_scope_tag : string
+val out_scope_tag : int -> string
+val is_out_scope_tag : string -> bool
+val int_of_out_scope_tag : string -> int
diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index f23116b63..d64fb005f 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -36,36 +36,45 @@ let mk_appl ~upto hd tl =
     | _ -> NCic.Appl (hd :: tl))
 ;;
 
-let flexible l = 
-  List.exists 
-    (function 
-       | NCic.Meta _  
-       | NCic.Appl (NCic.Meta _::_) -> true
-       | _ -> false) l
-;;
-
 exception WrongShape;;
 
-let eta_reduce = 
-  let delift_if_not_occur body orig =
+let eta_reduce subst t = 
+  let delift_if_not_occur body =
     try 
-        NCicSubstitution.psubst ~avoid_beta_redexes:true
-          (fun () -> raise WrongShape) [()] body
-    with WrongShape -> orig
+        Some (NCicSubstitution.psubst ~avoid_beta_redexes:true
+          (fun () -> raise WrongShape) [()] body)
+    with WrongShape -> None
+  in 
+  let rec eat_lambdas ctx = function
+    | NCic.Lambda (name, src, tgt) -> 
+        eat_lambdas ((name, src) :: ctx) tgt
+    | NCic.Meta (i,lc) as t->
+        (try 
+          let _,_,t,_ = NCicUtils.lookup_subst i subst in
+          let t = NCicSubstitution.subst_meta lc t in
+          eat_lambdas ctx t
+        with Not_found -> ctx, t)
+    | t -> ctx, t
   in
-  function
-  | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig ->
-      delift_if_not_occur hd orig
-  | NCic.Lambda(_, _, 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 context_body = eat_lambdas [] t in
+  let rec aux = function
+    | [],body -> body
+    | (name, src)::ctx, (NCic.Appl (hd::[NCic.Rel 1]) as bo) -> 
+        (match delift_if_not_occur hd with
+        | None -> aux (ctx,NCic.Lambda(name,src, bo)) 
+        | Some bo -> aux (ctx,bo))
+    | (name, src)::ctx, (NCic.Appl args as bo) 
+      when HExtlib.list_last args = NCic.Rel 1 -> 
+        let args, _ = HExtlib.split_nth (List.length args - 1) args in
+        (match delift_if_not_occur (NCic.Appl args) with
+        | None -> aux (ctx,NCic.Lambda(name,src, bo)) 
+        | Some bo -> aux (ctx,bo))
+    | (name, src) :: ctx, t ->
+        aux (ctx,NCic.Lambda(name,src, t)) 
+  in
+    aux context_body
 ;;
- 
+
 module C = NCic;;
 module Ref = NReference;;
 
@@ -98,13 +107,24 @@ let fix_sorts swap metasenv subst context meta t =
     aux () t
 ;;
 
-let rec beta_expand_many metasenv subst context t args =
+let is_locked n subst =
+   try
+     match NCicUtils.lookup_subst n subst with
+     | Some tag, _,_,_ when NCicMetaSubst.is_out_scope_tag tag -> true
+     | _ -> false
+   with NCicUtils.Subst_not_found _ -> false
+;;
+
+
+let rec lambda_intros metasenv subst context t args =
  let tty = NCicTypeChecker.typeof ~metasenv ~subst context t in
  let argsty = List.map (NCicTypeChecker.typeof ~metasenv ~subst context) args in
  let rec mk_lambda context n = function
    | [] -> 
        let metasenv, _, bo, _ = 
-         NCicMetaSubst.mk_meta metasenv context (`WithType tty) in
+         NCicMetaSubst.mk_meta metasenv context 
+           (`WithType (NCicSubstitution.lift n tty))
+       in
        metasenv, bo
    | ty::tail -> 
        let name = "HBeta"^string_of_int n in
@@ -159,12 +179,18 @@ and instantiate hdb test_eq_only metasenv subst context n lc t swap =
               pp msg; assert false
        in
        let lty = NCicSubstitution.subst_meta lc ty in
-       pp (lazy ("On the types: " ^
-        NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
-        NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
-         ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
-       let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
-       metasenv, subst, t
+       match ty_t with
+       | NCic.Implicit _ -> 
+           raise (UnificationFailure 
+             (lazy "trying to unify a term with a type"))
+       | ty_t -> 
+          pp (lazy ("On the types: " ^
+           NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
+           NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
+            ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
+          let metasenv,subst = 
+            unify test_eq_only metasenv subst context lty ty_t in
+          metasenv, subst, t
   in
          pp (lazy(string_of_int n ^ " := 111 = "^
            NCicPp.ppterm ~metasenv ~subst ~context t));
@@ -275,6 +301,34 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
                 let term2 = NCicSubstitution.subst_meta lc2 term in
                   unify hdb test_eq_only metasenv subst context term1 term2
               with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
+       
+       | NCic.Appl (NCic.Meta (i,l)::args), NCic.Meta (n, _) when 
+         not (NCicMetaSubst.flexible subst args) &&
+         is_locked n subst &&
+         not (List.mem_assoc i subst) 
+         ->
+           (* we verify that none of the args is a Meta, 
+              since beta expanding w.r.t a metavariable makes no sense  *)
+              let metasenv, lambda_Mj =
+                lambda_intros metasenv subst context t1 args
+              in
+              let metasenv, subst = 
+                unify hdb test_eq_only metasenv subst context 
+                  (C.Meta (i,l)) lambda_Mj
+              in
+              let t1 = NCicReduction.whd ~subst context t1 in
+              let i, l = 
+                match t1 with NCic.Meta (i,l) -> i, l | _ -> assert false
+              in
+              let metasenv, subst = 
+                instantiate hdb test_eq_only metasenv subst context i l t2 true
+              in
+              (try
+                let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+                let term = eta_reduce subst term in
+                let subst = List.filter (fun (j,_) -> j <> i) subst in
+                metasenv, ((i, (name, ctx, term, ty)) :: subst)
+              with Not_found -> assert false)
 
        | C.Meta (n,lc), t -> 
            (try 
@@ -316,29 +370,45 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
             with Invalid_argument _ -> 
               raise (fail_exc metasenv subst context t1 t2))
 
-       | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
+       | NCic.Appl (NCic.Meta (i,l)::args), _ when 
+         not (NCicMetaSubst.flexible subst args) ->
            (* we verify that none of the args is a Meta, 
               since beta expanding w.r.t a metavariable makes no sense  *)
-              let metasenv, beta_expanded =
-                beta_expand_many metasenv subst context t2 args
+              let metasenv, lambda_Mj =
+                lambda_intros metasenv subst context t1 args
               in
               let metasenv, subst = 
                 unify hdb test_eq_only metasenv subst context 
-                  (C.Meta (i,l)) beta_expanded
+                  (C.Meta (i,l)) lambda_Mj
               in
-              
-              (* .... eta_reduce ?i ... *)
+              let metasenv, subst = 
                 unify hdb test_eq_only metasenv subst context t1 t2 
+              in
+              (try
+                let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+                let term = eta_reduce subst term in
+                let subst = List.filter (fun (j,_) -> j <> i) subst in
+                metasenv, ((i, (name, ctx, term, ty)) :: subst)
+              with Not_found -> assert false)
 
-       | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
-              let metasenv, beta_expanded =
-                beta_expand_many metasenv subst context t1 args
+       | _, NCic.Appl (NCic.Meta (i,l)::args) when 
+         not(NCicMetaSubst.flexible subst args) ->
+              let metasenv, lambda_Mj =
+                lambda_intros metasenv subst context t2 args
               in
               let metasenv, subst =
                 unify hdb test_eq_only metasenv subst context 
-                 beta_expanded (C.Meta (i,l))
+                 lambda_Mj (C.Meta (i,l))
               in
+              let metasenv, subst = 
                 unify hdb test_eq_only metasenv subst context t1 t2 
+              in
+              (try
+                let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+                let term = eta_reduce subst term in
+                let subst = List.filter (fun (j,_) -> j <> i) subst in
+                metasenv, ((i, (name, ctx, term, ty)) :: subst)
+              with Not_found -> assert false)
 
        (* processing this case here we avoid a useless small delta step *)
        | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) 
diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 3d81ca53c..f0d12aa8e 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -158,9 +158,6 @@ let mk_meta status ?name ctx bo_or_ty =
       status, (None,ctx,instance)
 ;;
 
-let in_scope_tag = "tag:in_scope" ;;
-let out_scope_tag = "tag:out_scope" ;;
-
 let select_term low_status (name,context,term) (wanted,path) =
   let found status ctx t wanted =
     (* we could lift wanted step-by-step *)
@@ -174,7 +171,8 @@ let select_term low_status (name,context,term) (wanted,path) =
       let b, status = found status ctx t wanted in
       if b then 
         let status, (_,_,t) = 
-          mk_meta status ~name:in_scope_tag ctx (`Def (None, ctx, t))
+          mk_meta status ~name:NCicMetaSubst.in_scope_tag 
+            ctx (`Def (None, ctx, t))
         in    
         status, t
       else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t
@@ -232,7 +230,7 @@ let select_term low_status (name,context,term) (wanted,path) =
   in
   let status, term = select low_status context path term in
   let term = (name, context, term) in
-  mk_meta status ~name:out_scope_tag context (`Def term)
+  mk_meta status ~name:(NCicMetaSubst.out_scope_tag 1) context (`Def term)
 ;;
 
 let analyse_indty status ty = 
diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 1feac415b..ce3fd33b0 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -59,8 +59,6 @@ val mk_meta:
      lowtac_status * cic_term
 val instantiate: lowtac_status -> int -> cic_term -> lowtac_status
 
-val in_scope_tag: string
-val out_scope_tag: string
 val select_term:
   lowtac_status -> cic_term -> ast_term option * NCic.term ->
     lowtac_status * cic_term
diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 7fa2b48d8..f45aa656b 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -240,13 +240,15 @@ let reopen status =
  let subst, newm = 
    List.partition 
     (function (_,(Some tag,_,_,_)) -> 
-            tag <> in_scope_tag && tag <> out_scope_tag
+            tag <> NCicMetaSubst.in_scope_tag && 
+            not (NCicMetaSubst.is_out_scope_tag tag)
     | _ -> true)
     subst 
  in
  let in_m, out_m = 
    List.partition
-     (function (_,(Some tag,_,_,_)) -> tag = in_scope_tag | _ -> assert false)
+     (function (_,(Some tag,_,_,_)) -> 
+         tag = NCicMetaSubst.in_scope_tag | _ -> assert false)
      newm
  in
  let metasenv = List.map (fun (i,(_,c,_,t)) -> i,(None,c,t)) in_m @ metasenv in
@@ -288,11 +290,11 @@ let elim_tac ~what ~where status =
    [ select_tac ~where;
      distribute_tac (fun status goal ->
        let goalty = get_goalty status goal in
+       let _,_,w = what in
        let status, what = 
          disambiguate status what None (ctx_of goalty) in
        let _ty_what = typeof status (ctx_of what) what in 
        (* check inductive... find eliminator *)
-       let w = (*astify what *) CicNotationPt.Ident ("m",None) in
        let holes = [ 
          CicNotationPt.Implicit;CicNotationPt.Implicit;CicNotationPt.Implicit]
        in
diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend
index f3c6a8bd1..25e67131f 100644
--- a/helm/software/components/syntax_extensions/.depend
+++ b/helm/software/components/syntax_extensions/.depend
@@ -1,2 +1,5 @@
+utf8Macro.cmi: 
+utf8MacroTable.cmo: 
+utf8MacroTable.cmx: 
 utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi 
 utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi