X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FnCicCoercDeclaration.ml;h=7fcd6a473f4595f70047f2bda5fce0b6867b68bf;hb=d3a143f3edce2a255c449526e0ecf85435a6bad4;hp=141ae369e226ed0f5c2d60de59b5ab23a6babfd5;hpb=889815067d64e081eb90ea1a792890c2ad4e511c;p=helm.git

diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
index 141ae369e..7fcd6a473 100644
--- a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
@@ -9,7 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-let debug s = prerr_endline (Lazy.force s) ;;
+(* let debug s = prerr_endline (Lazy.force s) ;;*)
 let debug _ = ();;
 
 let skel_dummy = NCic.Implicit `Type;;
@@ -32,12 +32,6 @@ let pos_in_list x l =
       | None -> assert false
 ;;
 
-let pos_of x t = 
-  match t with
-  | NCic.Appl l -> pos_in_list x l
-  | _ -> assert false
-;;
-
 let rec count_prod = function
   | NCic.Prod (_,_,x) -> 1 + count_prod x
   | _ -> 0
@@ -130,14 +124,62 @@ 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
+;;
+
+exception Stop;;
+
+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) 
@@ -154,13 +196,13 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status =
     let c_o_from_d = 
       product 
         (fun (n,mc,c,_,j) (n1,m1,t1,ty,i) -> 
-          compose_names n1 n,m1@mc,t1,[i,c],j,count_prod ty) 
+          compose_names n n1,m1@mc,t1,[i,c],j,count_prod ty) 
         [c] from_d
     in
     let to_s_o_c_o_from_d =
       product 
         (fun (n1,m1,t1,_,j) (n,m,t,upl,i,a)-> 
-          compose_names n n1,m@m1,t,(i,t1)::upl,j,a)
+          compose_names n1 n,m@m1,t,(i,t1)::upl,j,a)
         to_s c_o_from_d
     in
     to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
@@ -176,104 +218,100 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status =
             (metasenv,[]) upl
          in
          let bo = NCicUntrusted.apply_subst subst [] bo in
+         let p = NCicUntrusted.apply_subst subst [] p in
+         let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
          let metasenv = toposort metasenv in
          let bo = close_in_context bo metasenv in
          let pos = 
            match p with 
            | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv) 
-           | _ -> assert false
+           | t -> raise Stop
          in
          let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
          let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in
          let src = only_head src in
          let tgt = only_head tgt in
          debug (lazy(
-           "composite: "^
+           "composite " ^ name ^ ": "^
            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
            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
+       | NCicUnification.Uncertain _ | Stop -> 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
+  NCicLibrary.Serializer.register#run "ncoercion"
+   object(self : 'a NCicLibrary.register_type)
+    method run = aux_l 
+   end
 ;;
 
-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
 ;;