]> matita.cs.unibo.it Git - helm.git/commitdiff
improved check in delift for flexible lc entries.
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 15 Sep 2009 13:53:04 +0000 (13:53 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 15 Sep 2009 13:53:04 +0000 (13:53 +0000)
added a function to easily delift a term w.r.t.
other terms, thanks to delift, used to propagate the expected type
of a letin.

helm/software/components/ng_refiner/nCicMetaSubst.ml
helm/software/components/ng_refiner/nCicRefiner.ml
helm/software/components/ng_refiner/nCicUnification.ml
helm/software/components/ng_refiner/nCicUnification.mli
helm/software/matita/nlibrary/depends
helm/software/matita/nlibrary/depends.dot
helm/software/matita/nlibrary/depends.png
helm/software/matita/nlibrary/sets/partitions.ma

index 927c288a0543766830a730ee0df60ac39d33b773..60abe85c37c08879ea80d01ededa27c158d0192f 100644 (file)
@@ -206,12 +206,29 @@ and restrict metasenv subst i restrictions =
     | NCicUtils.Meta_not_found _ -> assert false
 ;;
 
-let rec flexible_arg subst = function 
+let rec flexible_arg context subst = function 
   | NCic.Meta (i,_) | NCic.Appl (NCic.Meta (i,_) :: _)-> 
       (try 
         let _,_,t,_ = List.assoc i subst in
-        flexible_arg subst t
+        flexible_arg context subst t
       with Not_found -> true)
+   (* this is a cheap whd, it only performs zeta-reduction.
+    * 
+    * it works when the **omissis** disambiguation algorithm
+    * is run on `let x := K a b in t`, K is substituted for a 
+    * ? and thus in t metavariables have a flexible Rel
+    *)
+  | NCic.Rel i ->
+      (try
+         match List.nth context (i-1)
+         with 
+         | _,NCic.Def (bo,_) ->
+               flexible_arg context subst
+                 (NCicSubstitution.lift i bo)
+         | _ -> false
+      with 
+      | Failure _ -> assert false
+      | Invalid_argument _ -> assert false)
   | _ -> false
 ;;
 
@@ -258,8 +275,8 @@ let delift ~unify metasenv subst context n l t =
     match l with
     | _, NCic.Irl _ -> fun _ _ _ _ _ -> None
     | shift, NCic.Ctx l -> fun metasenv subst context k t ->
-       if flexible_arg subst t || contains_in_scope subst t then None else
-         let lb = List.map (fun t -> t, flexible_arg subst t) l in
+       if flexible_arg context subst t || contains_in_scope subst t then None else
+         let lb = List.map (fun t -> t, flexible_arg context subst t) l in
          HExtlib.list_findopt
           (fun (li,flexible) i ->
             if flexible || i < in_scope then None else
index 7c199f8c07bf0c64ec295392f99083ad81b20db8..56ec069d2c77bb7d30eff3773073908bdc01b6ff 100644 (file)
@@ -114,10 +114,14 @@ let rec typeof rdb
           (NCicPp.ppterm ~metasenv ~subst:[] ~context expty)));
            try 
              let metasenv, subst =
+    (*D*)inside 'U'; try let rc = 
                NCicUnification.unify rdb metasenv subst context infty expty 
+    (*D*)in outside(); rc with exc -> outside (); raise exc
              in
              metasenv, subst, t, expty
-           with exc -> 
+           with 
+           | NCicUnification.Uncertain _ 
+           | NCicUnification.UnificationFailure _ as exc -> 
              try_coercions rdb ~localise 
                metasenv subst context t orig infty expty true exc)
     | None -> metasenv, subst, t, infty
@@ -229,8 +233,18 @@ let rec typeof rdb
        let metasenv, subst, t, _ = 
          typeof_aux metasenv subst context (Some ty) t in
        let context1 = (n, C.Def (t,ty)) :: context in
+       let metasenv, subst, expty1 = 
+         match expty with 
+         | None -> metasenv, subst, None 
+         | Some x -> 
+             let m, s, x = 
+               NCicUnification.delift_term_wrt_terms 
+                 rdb metasenv subst context x [t]
+             in
+               m, s, Some x
+       in
        let metasenv, subst, bo, bo_ty = 
-         typeof_aux metasenv subst context1 None bo 
+         typeof_aux metasenv subst context1 expty1 bo 
        in
        let bo_ty = NCicSubstitution.subst ~avoid_beta_redexes:true t bo_ty in
        metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty
@@ -509,11 +523,13 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
           let metasenv,subst, flex_prod, _ =
            typeof rdb ~localise metasenv subst
             context flex_prod None in
+(*
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context
             ^ "\nOF: " ^
             NCicPp.ppterm ~metasenv ~subst ~context t ^  " === " ^
             NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
+*)
           let metasenv, subst =
              try NCicUnification.unify rdb metasenv subst context t flex_prod 
              with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
index c224708533e5c6789606d943ac37fa4d23a609fb..2f6332d51d748ad0c90ecf71c81c5219ccd79cec 100644 (file)
@@ -95,8 +95,8 @@ let outside () =
 let pp s = 
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;
-let pp _ = ();;
 
+let pp _ = ();;
 
 let ppcontext = NCicPp.ppcontext;;
 let ppmetasenv = NCicPp.ppmetasenv;;
@@ -152,20 +152,11 @@ let rec lambda_intros rdb metasenv subst context t args =
        in
        metasenv, subst, bo
    | (arg,ty)::tail ->
+       let metasenv, subst, telescopic_ty = 
+         delift_term_wrt_terms rdb metasenv subst context_of_args ty 
+           (List.rev processed_args)
+       in
        let name = "HBeta"^string_of_int n in
-       let metasenv,_,instance,_ =
-        NCicMetaSubst.mk_meta metasenv context_of_args `Term in
-       let meta_applied =
-        NCicUntrusted.mk_appl instance (List.rev processed_args) in
-let metasenv,subst,_,_ =
- !refiner_typeof ((rdb :> NRstatus.status)#set_coerc_db NCicCoercion.empty_db) metasenv subst context_of_args meta_applied None
-in
-       let metasenv,subst =
-        unify rdb true metasenv subst context_of_args meta_applied ty in
-       let telescopic_ty = NCicSubstitution.lift n instance in
-       let telescopic_ty =
-        NCicUntrusted.mk_appl
-         telescopic_ty (mk_irl (List.length processed_args)) in
        let metasenv, subst, bo =
         mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1)
          (arg::processed_args) tail
@@ -669,8 +660,23 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
           | UnificationFailure _ -> raise (UnificationFailure msg)
           | Uncertain _ -> raise exn
  (*D*)  in outside(); rc with exn -> outside (); raise exn 
+
+and delift_term_wrt_terms rdb metasenv subst context t args =
+  let metasenv, _, instance, _ =
+    NCicMetaSubst.mk_meta metasenv context `Term in
+  let meta_applied = NCicUntrusted.mk_appl instance args in
+  let metasenv,subst,meta_applied,_ =
+    !refiner_typeof ((rdb:> NRstatus.status)#set_coerc_db NCicCoercion.empty_db)
+      metasenv subst context meta_applied None
+  in
+  let metasenv, subst =
+   unify rdb true metasenv subst context meta_applied t in
+  let t = NCicSubstitution.lift (List.length args) instance in
+  let t = NCicUntrusted.mk_appl t (mk_irl (List.length args)) in
+   metasenv, subst, t
 ;;
 
+
 let unify rdb ?(test_eq_only=false) = 
   indent := "";      
   unify rdb test_eq_only;;
index 891c0738ecb9d9ee7b8e412c88526977918c562b..944b4c18707feed829f9f1ae2b5edf8cd4c28bff 100644 (file)
@@ -32,38 +32,9 @@ val unify :
 (* this should be moved elsewhere *)
 val fix_sorts: NCic.term -> NCic.term
 
-(* 
-exception UnificationFailure of string Lazy.t;;
-exception Uncertain of string Lazy.t;;
-exception AssertFailure of string Lazy.t;;
-
-(* fo_unif metasenv context t1 t2                *)
-(* unifies [t1] and [t2] in a context [context]. *)
-(* Only the metavariables declared in [metasenv] *)
-(* can be used in [t1] and [t2].                 *)
-(* The returned substitution can be directly     *)
-(* withouth first unwinding it.                  *)
-val fo_unif :
-  Cic.metasenv -> Cic.context -> 
-    Cic.term -> Cic.term -> CicUniv.universe_graph -> 
-      Cic.substitution * Cic.metasenv * CicUniv.universe_graph
-
-(* fo_unif_subst metasenv subst context t1 t2    *)
-(* unifies [t1] and [t2] in a context [context]  *)
-(* and with [subst] as the current substitution  *)
-(* (i.e. unifies ([subst] [t1]) and              *)
-(* ([subst] [t2]) in a context                   *)
-(* ([subst] [context]) using the metasenv        *)
-(* ([subst] [metasenv])                          *)
-(* Only the metavariables declared in [metasenv] *)
-(* can be used in [t1] and [t2].                 *)
-(* [subst] and the substitution returned are not *)
-(* unwinded.                                     *)
-(*CSC: fare un tipo unione Unwinded o ToUnwind e fare gestire la
- cosa all'apply_subst!!!*)
-val fo_unif_subst :
-  Cic.substitution -> Cic.context -> Cic.metasenv -> 
-    Cic.term -> Cic.term -> CicUniv.universe_graph ->
-      Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+val delift_term_wrt_terms:
+  #NRstatus.status -> 
+  NCic.metasenv -> NCic.substitution -> NCic.context -> 
+  NCic.term -> NCic.term list ->
+   NCic.metasenv * NCic.substitution * NCic.term
 
-      *)
index 105946ce0a245b8c8c96483eafafcb32f1bb88dd..c5d90654b8341b896871c91bf5b349447660dd0c 100644 (file)
@@ -1,11 +1,10 @@
 logic/cprop.ma hints_declaration.ma sets/setoids1.ma
-sets/sets.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma
-topology/igft.ma logic/connectives.ma
+sets/sets.ma hints_declaration.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma
+topology/igft.ma sets/sets.ma
 datatypes/bool.ma logic/pts.ma
 sets/setoids1.ma properties/relations1.ma sets/setoids.ma
 logic/equality.ma logic/connectives.ma properties/relations.ma
 sets/setoids.ma logic/connectives.ma properties/relations.ma
-.unnamed.ma logic/pts.ma
 logic/connectives.ma logic/pts.ma
 datatypes/pairs.ma logic/pts.ma
 algebra/abelian_magmas.ma algebra/magmas.ma
@@ -14,7 +13,7 @@ nat/minus.ma nat/order.ma
 algebra/magmas.ma sets/sets.ma
 properties/relations1.ma logic/pts.ma
 nat/big_ops.ma algebra/magmas.ma nat/order.ma
-nat/nat.ma logic/equality.ma sets/setoids.ma
+nat/nat.ma hints_declaration.ma logic/equality.ma sets/setoids.ma
 properties/relations.ma logic/pts.ma
 nat/compare.ma datatypes/bool.ma nat/order.ma
 hints_declaration.ma logic/pts.ma
index 521bb637d9e586ca5e9bc9f13e2e7889e2fab4ac..b987610afd2155ea6a6699cedda2f4fd5d82cae8 100644 (file)
@@ -3,12 +3,13 @@ digraph g {
   "logic/cprop.ma" -> "hints_declaration.ma" [];
   "logic/cprop.ma" -> "sets/setoids1.ma" [];
   "sets/sets.ma" [];
+  "sets/sets.ma" -> "hints_declaration.ma" [];
   "sets/sets.ma" -> "logic/connectives.ma" [];
   "sets/sets.ma" -> "logic/cprop.ma" [];
   "sets/sets.ma" -> "properties/relations1.ma" [];
   "sets/sets.ma" -> "sets/setoids1.ma" [];
   "topology/igft.ma" [];
-  "topology/igft.ma" -> "logic/connectives.ma" [];
+  "topology/igft.ma" -> "sets/sets.ma" [];
   "datatypes/bool.ma" [];
   "datatypes/bool.ma" -> "logic/pts.ma" [];
   "sets/setoids1.ma" [];
@@ -20,8 +21,6 @@ digraph g {
   "sets/setoids.ma" [];
   "sets/setoids.ma" -> "logic/connectives.ma" [];
   "sets/setoids.ma" -> "properties/relations.ma" [];
-  ".unnamed.ma" [];
-  ".unnamed.ma" -> "logic/pts.ma" [];
   "logic/connectives.ma" [];
   "logic/connectives.ma" -> "logic/pts.ma" [];
   "datatypes/pairs.ma" [];
@@ -42,6 +41,7 @@ digraph g {
   "nat/big_ops.ma" -> "algebra/magmas.ma" [];
   "nat/big_ops.ma" -> "nat/order.ma" [];
   "nat/nat.ma" [];
+  "nat/nat.ma" -> "hints_declaration.ma" [];
   "nat/nat.ma" -> "logic/equality.ma" [];
   "nat/nat.ma" -> "sets/setoids.ma" [];
   "properties/relations.ma" [];
index 04d00a692f0a80de3c1270fea3ce02b9623becfb..e3fb6c2526f0a057baccbc502a14ac563a6a77c3 100644 (file)
Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ
index e33ddfa1d00af461221edc4c86c4d8d4a6831de0..40ecd43b43ec88377f22796f37a77555cfb54c53 100644 (file)
 (**************************************************************************)
 
 include "sets/sets.ma".
-include "nat/plus.ma". (* tempi biblici neggli include che fa plus.ma *)
+include "nat/plus.ma". 
 include "nat/compare.ma".
 include "nat/minus.ma".
 include "datatypes/pairs.ma".
 
-
+alias symbol "eq" (instance 2) = "leibnitz's equality".
+alias symbol "eq" (instance 1) = "setoid eq".
+alias symbol "eq" = "setoid eq".
+alias symbol "eq" = "setoid1 eq".
 alias symbol "eq" = "setoid eq".
 alias symbol "eq" = "setoid1 eq".
 alias symbol "eq" = "setoid eq".
+alias symbol "eq" = "setoid1 eq".
 nrecord partition (A: setoid) : Type[1] ≝ 
  { support: setoid;
    indexes: qpowerclass support;
@@ -129,9 +133,10 @@ nlemma partition_splits_card:
  ∀A. ∀P:partition A. ∀n,s.
   ∀f:isomorphism ?? (Nat_ n) (indexes ? P).
    (∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i))) →
-    (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) A).
- #A; #P; #Sn; ncases Sn
-  [ #s; #f; #fi; nlapply (covers ? P); *; #_; #H;
+    (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) (Full_set A)).
+#A; #P; #Sn; ncases Sn
+  [ #s; #f; #fi;
+    ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #H;
     (*
     nlapply
      (big_union_preserves_iso ??? (indexes A P) (Nat_ O) (λx.class ? P x) f);
@@ -139,7 +144,7 @@ nlemma partition_splits_card:
     nelim daemon (* impossibile *)
   | #n; #s; #f; #fi; @
   [ @
-     [ napply (λm.let p ≝ iso_nat_nat_union s m n in iso_f ???? (fi (fst … p)) (snd … p))
+     [ napply (λm.let p ≝ (iso_nat_nat_union s m n) in iso_f ???? (fi (fst … p)) (snd … p))
      | #a; #a'; #H; nrewrite < H; napply refl ]
 ##| #x; #Hx; nwhd; napply I
 ##| #y; #_;
@@ -147,12 +152,12 @@ nlemma partition_splits_card:
     ngeneralize in match (Hc y I) in ⊢ ?; *; #index; *; #Hi1; #Hi2;
     ngeneralize in match (f_sur ???? f ? Hi1) in ⊢ ?; *; #nindex; *; #Hni1; #Hni2;
     ngeneralize in match (f_sur ???? (fi nindex) y ?) in ⊢ ?
-     [##2: napply (. #‡(†?));##[##3: napply Hni2 |##2: ##skip | nassumption]##]
+     [##2: napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
     *; #nindex2; *; #Hni21; #Hni22;
     nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2);
     napply (ex_intro … xxx); napply conj
      [ napply iso_nat_nat_union_pre [ napply le_S_S_to_le; nassumption | nassumption ]
-   ##| nwhd in ⊢ (???%%); napply (.= ?) [ nassumption|##skip]
+   ##| nwhd in ⊢ (???%%); napply (.= ?) [##3: nassumption|##skip]
        ngeneralize in match (iso_nat_nat_union_char n s xxx ?) in ⊢ ?
         [##2: napply iso_nat_nat_union_pre [ napply le_S_S_to_le; nassumption | nassumption]##]
        *; *; #K1; #K2; #K3;
@@ -168,7 +173,7 @@ nlemma partition_splits_card:
       ngeneralize in match (disjoint ? P (iso_f ???? f i1) (iso_f ???? f i1') ???) in ⊢ ?
        [##2,3: napply f_closed; nassumption
        |##4: napply ex_intro [ napply (iso_f ???? (fi i1) i2) ] napply conj
-         [ napply f_closed; nassumption ##| napply (. ?‡#) [##2: nassumption | ##3: ##skip]
+         [ napply f_closed; nassumption ##| napply (. ?‡#) [ nassumption | ##2: ##skip]
          nwhd; napply f_closed; nassumption]##]
       #E'; ngeneralize in match (? : i1=i1') in ⊢ ?
        [##2: napply (f_inj … E'); nassumption
@@ -204,4 +209,4 @@ ndefinition partition_of_compatible_equivalence_relation:
     napply sym; nassumption
   | nnormalize; napply conj
      [ #a; #_; napply I | #a; #_; napply (ex_intro … a); napply conj [ napply I | napply refl]##]
-nqed.
\ No newline at end of file
+nqed.