fixed coercion mechanism w.r.t. undo/require

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index f7df56315e235a5e42d179579e546c824f7020ce..ec9f3866fdab4bbffab2ce894ab17e937b809cef 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -41,6 +41,11 @@ type options = {
   do_heavy_checks: bool ; 
 }
 
+let concat_nuris uris nuris =
+   match uris,nuris with
+   | `New uris, `New nuris -> `New (nuris@uris)
+   | _ -> assert false
+;;
 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   * names as long as they are available, then it fallbacks to name generation
   * using FreshNamesGenerator module *)
@@ -767,9 +772,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                  eval_ncommand opts status
                   ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
                 in
-                 match uris,nuris with
-                    `New uris, `New nuris -> status,`New (nuris@uris)
-                  | _ -> assert false
+                status, concat_nuris uris nuris
                with
                 NCicTypeChecker.TypeCheckerFailure msg
                  when Lazy.force msg =
@@ -785,16 +788,21 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                  (fun (name,is_coercion,arity) ->
                    if is_coercion then Some(name,leftno,arity) else None) fields
             | _ -> [] in
-           let status =
+           let status,uris =
             List.fold_left
-             (fun status (name,cpos,arity) ->
+             (fun (status,uris) (name,cpos,arity) ->
                let metasenv,subst,status,t =
                 GrafiteDisambiguate.disambiguate_nterm None status [] [] []
                  ("",0,CicNotationPt.Ident (name,None)) in
                assert (metasenv = [] && subst = []);
-               NCicCoercDeclaration.basic_eval_and_inject_ncoercion_from_t_cpos_arity 
-                 status (name,t,cpos,arity)
-             ) status coercions
+               let status, nuris = 
+                 NCicCoercDeclaration.
+                   basic_eval_and_record_ncoercion_from_t_cpos_arity 
+                    status (name,t,cpos,arity)
+               in
+               let uris = concat_nuris nuris uris in
+               status, uris) 
+             (status,uris) coercions
            in
             status,uris
           with

diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
index 141ae369e226ed0f5c2d60de59b5ab23a6babfd5..550cb93c4a10394ffcdd7ecc74146d416de77cfb 100644 (file)
--- a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
@@ -130,14 +130,61 @@ let only_head = function
   | t -> t
 ;;
 
-let basic_eval_ncoercion (name,t,s,d,p,a) status =
-  let to_s = 
-    NCicCoercion.look_for_coercion status [] [] [] skel_dummy s
+let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
+  let status, src, cpos = 
+    let rec aux cpos ctx = function
+      | NCic.Prod (name,ty,bo) ->
+         if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
+         else
+           (try 
+            let metasenv,subst,status,src =
+              GrafiteDisambiguate.disambiguate_nterm 
+                None status ctx [] [] ("",0,src) in
+            let src = NCicUntrusted.apply_subst subst [] src in
+            (* CHECK that the declared pattern matches the abstraction *)
+            let _ = NCicUnification.unify status metasenv subst ctx ty src in
+            let src = cleanup_skel () src in
+            status, src, cpos
+           with 
+           | NCicUnification.UnificationFailure _
+           | NCicUnification.Uncertain _
+           | MultiPassDisambiguator.DisambiguationError _ ->
+               raise (GrafiteTypes.Command_error "bad source pattern"))
+      | _ -> assert false
+    in
+      aux 0 [] ty
   in
-  let from_d = 
-    NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
+  let status, tgt, arity = 
+    let metasenv,subst,status,tgt =
+      GrafiteDisambiguate.disambiguate_nterm 
+        None status [] [] [] ("",0,tgt) in
+    let tgt = NCicUntrusted.apply_subst subst [] tgt in
+    (* CHECK che sia unificabile mancante *)
+    let rec count_prod = function
+      | NCic.Prod (_,_,x) -> 1 + count_prod x
+      | _ -> 0
+    in
+    let arity = count_prod tgt in
+    let tgt=
+      if arity > 0 then cleanup_funclass_skel tgt 
+      else cleanup_skel () tgt 
+    in
+     status, tgt, arity
   in
-  let status = NCicCoercion.index_coercion status name t s d a p in
+  status, src, tgt, cpos, arity
+;;
+
+let fresh_uri status prefix suffix = 
+  let mk x = NUri.uri_of_string (status#baseuri ^ "/" ^ prefix ^ x ^ suffix) in
+  let rec diverge u i =
+    if NCicLibrary.aliases_of u = [] then u
+    else diverge (mk ("__" ^ string_of_int i)) (i+1)
+  in
+   diverge (mk "") 0
+;;
+
+
+let close_graph name t s d to_s from_d p a status =
   let c =
     List.find 
      (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false) 
@@ -194,86 +241,77 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status =
            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^
            " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity));
-         Some (name,bo,src,tgt,arity,pos)
+         let uri = fresh_uri status name ".con" in
+         let obj_kind = NCic.Constant 
+           ([],name,Some bo,ty,(`Generated,`Definition,`Coercion arity)) 
+         in
+         let height = NCicTypeChecker.height_of_obj_kind uri [] obj_kind in
+         let obj = uri,height,[],[],obj_kind in
+         let c = 
+           NCic.Const 
+             (NReference.reference_of_spec uri (NReference.Def height))
+         in
+         Some (obj,name,c,src,tgt,pos,arity)
        with 
        | NCicTypeChecker.TypeCheckerFailure _
        | NCicUnification.UnificationFailure _ 
        | NCicUnification.Uncertain _ -> None
      ) composites
   in
+    composites
+;;
+
+(* idempotent *)
+let basic_index_ncoercion (name,t,s,d,position,arity) status =
+  NCicCoercion.index_coercion status name t s d arity position
+;;
+
+let basic_eval_ncoercion (name,t,s,d,p,a) status =
+  let to_s = 
+    NCicCoercion.look_for_coercion status [] [] [] skel_dummy s
+  in
+  let from_d = 
+    NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
+  in
+  let status = NCicCoercion.index_coercion status name t s d a p in
+  let composites = close_graph name t s d to_s from_d p a status in
   List.fold_left 
-    (fun st (name,t,s,d,a,p) -> NCicCoercion.index_coercion st name t s d a p) 
-    status composites
+    (fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) -> 
+      let info = name,t,s,d,p,a in
+      let st = NCicLibrary.add_obj st obj in
+      let st = basic_index_ncoercion info st in
+      uri::uris, info::infos, st)
+    ([],[],status) composites
 ;;
 
-let inject_ncoercion =
- let basic_eval_ncoercion (name,t,s,d,p,a) ~refresh_uri_in_universe
-  ~refresh_uri_in_term
- =
+let record_ncoercion =
+ let aux (name,t,s,d,p,a) ~refresh_uri_in_universe ~refresh_uri_in_term =
   let t = refresh_uri_in_term t in
   let s = refresh_uri_in_term s in
   let d = refresh_uri_in_term d in
-   basic_eval_ncoercion (name,t,s,d,p,a)
+   basic_index_ncoercion (name,t,s,d,p,a)
  in
-  NRstatus.Serializer.register "ncoercion" basic_eval_ncoercion
-;;
-
-let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
-  let status, src, cpos = 
-    let rec aux cpos ctx = function
-      | NCic.Prod (name,ty,bo) ->
-         if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
-         else
-           (try 
-            let metasenv,subst,status,src =
-              GrafiteDisambiguate.disambiguate_nterm 
-                None status ctx [] [] ("",0,src) in
-            let src = NCicUntrusted.apply_subst subst [] src in
-            (* CHECK that the declared pattern matches the abstraction *)
-            let _ = NCicUnification.unify status metasenv subst ctx ty src in
-            let src = cleanup_skel () src in
-            status, src, cpos
-           with 
-           | NCicUnification.UnificationFailure _
-           | NCicUnification.Uncertain _
-           | MultiPassDisambiguator.DisambiguationError _ ->
-               raise (GrafiteTypes.Command_error "bad source pattern"))
-      | _ -> assert false
-    in
-      aux 0 [] ty
-  in
-  let status, tgt, arity = 
-    let metasenv,subst,status,tgt =
-      GrafiteDisambiguate.disambiguate_nterm 
-        None status [] [] [] ("",0,tgt) in
-    let tgt = NCicUntrusted.apply_subst subst [] tgt in
-    (* CHECK che sia unificabile mancante *)
-    let rec count_prod = function
-      | NCic.Prod (_,_,x) -> 1 + count_prod x
-      | _ -> 0
-    in
-    let arity = count_prod tgt in
-    let tgt=
-      if arity > 0 then cleanup_funclass_skel tgt 
-      else cleanup_skel () tgt 
-    in
-     status, tgt, arity
-  in
-  status, src, tgt, cpos, arity
+ let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term =
+   List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l
+ in
+  NRstatus.Serializer.register "ncoercion" aux_l
 ;;
 
-let basic_eval_and_inject_ncoercion infos status =
- let status = basic_eval_ncoercion infos status in
- let dump = inject_ncoercion infos::status#dump in
-  status#set_dump dump
+let basic_eval_and_record_ncoercion infos status =
+ let uris, cinfos, status = basic_eval_ncoercion infos status in
+ let dump = record_ncoercion (infos::cinfos) :: status#dump in
+  status#set_dump dump, uris
 ;;
 
-let basic_eval_and_inject_ncoercion_from_t_cpos_arity 
+let basic_eval_and_record_ncoercion_from_t_cpos_arity 
       status (name,t,cpos,arity) 
 =
   let ty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] t in
   let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in
-  basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status
+  let status, uris =
+   basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
+  in
+   status,`New uris
 ;;
 
 let eval_ncoercion status name t ty (id,src) tgt = 
@@ -289,9 +327,9 @@ let eval_ncoercion status name t ty (id,src) tgt =
 
  let status, src, tgt, cpos, arity = 
    src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
- let status =
-  basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status
+ let status, uris =
+  basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
  in
-  status,`New []
+  status,`New uris
 ;;
 

diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.mli b/helm/software/components/grafite_engine/nCicCoercDeclaration.mli
index 66698156857b6a51c1f8d91a445c8453cb906c5c..aee0e9fc390a4463e9681eb46a7d90e76043154a 100644 (file)
--- a/helm/software/components/grafite_engine/nCicCoercDeclaration.mli
+++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.mli
@@ -12,17 +12,17 @@
 
 (* evals a coercion declaration statement: name t ty (id,src) tgt *)
 val eval_ncoercion: 
-     GrafiteTypes.status as 'status ->
+   #GrafiteTypes.status as 'status ->
      string ->
      CicNotationPt.term ->
      CicNotationPt.term ->
      string * CicNotationPt.term ->
-     CicNotationPt.term -> 'status * [> `New of 'c list ]
+     CicNotationPt.term -> 'status * [> `New of NUri.uri list ]
 
 (* for records, the term is the projection, already refined, while the
  * first integer is the number of left params and the second integer is 
  * the arity in the `:arity>` syntax *)
-val basic_eval_and_inject_ncoercion_from_t_cpos_arity: 
-     (GrafiteTypes.status as 'status) ->
-       string * NCic.term * int * int -> 'status
+val basic_eval_and_record_ncoercion_from_t_cpos_arity: 
+   #GrafiteTypes.status as 'status ->
+     string * NCic.term * int * int -> 'status * [> `New of NUri.uri list ]
 

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index fb733cdfcb877366658881b96c2365f06b37352a..9a2842e0ea899a20155e0b8b7a3b4d9331e49f40 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -270,12 +270,9 @@ let resolve name =
 ;;
 
 let aliases_of uri =
- try
   HExtlib.filter_map
    (fun (uri',_,nref) ->
      if NUri.eq uri' uri then Some nref else None) !local_aliases
- with
-  Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri)))
 ;;
 
 let add_obj status ((u,_,_,_,_) as obj) =

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index f3bd3b8898e35dd52f4f3d175ff79caf9690ca25..f140ef7700b7ca3b426debca3612628d8ac7f876 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -39,7 +39,6 @@ ndefinition big_union ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∃i. i ∈ T ∧
 ndefinition big_intersection ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∀i. i ∈ T → x ∈ f i }.
 
 ndefinition full_set: ∀A. Ω^A ≝ λA.{ x | True }.
-ncoercion full_set : ∀A:Type[0]. Ω^A ≝ full_set on A: Type[0] to (Ω^?).
 
 nlemma subseteq_refl: ∀A.∀S: Ω^A. S ⊆ S.
  #A; #S; #x; #H; nassumption.
@@ -62,6 +61,9 @@ nqed.
 
 include "sets/setoids1.ma".
 
+(* this has to be declared here, so that it is combined with carr *)
+ncoercion full_set : ∀A:Type[0]. Ω^A ≝ full_set on A: Type[0] to (Ω^?).
+
 ndefinition powerclass_setoid: Type[0] → setoid1.
  #A; @[ napply (Ω^A)| napply seteq ]
 nqed.