X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FnCicCoercDeclaration.ml;h=a2ed8044a187a9236f365f18794a9f73ee65c02b;hb=0af3592e3a85a4bb82c5c6df259cf9ab117ba0b1;hp=4522a0a1a917855a8aed045d35b1eaa52d753e94;hpb=d4f2d4c1a4784f84aa27e1bb96b8b377a6553c65;p=helm.git

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml
index 4522a0a1a..a2ed8044a 100644
--- a/matita/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml
@@ -54,7 +54,7 @@ let rec cleanup_funclass_skel = function
     | _ -> skel_dummy
 ;;
 
-let src_tgt_of_ty_cpos_arity ty cpos arity =
+let src_tgt_of_ty_cpos_arity status ty cpos arity =
   let pis = count_prod ty in
   let tpos = pis - arity in
   let rec pi_nth i j = function
@@ -72,7 +72,7 @@ let src_tgt_of_ty_cpos_arity ty cpos arity =
       | NCic.Meta _ 
       | NCic.Implicit _ as x -> x
       | NCic.Rel _ -> skel_dummy
-      | t -> NCicUtils.map (fun _ () -> ()) () aux t
+      | t -> NCicUtils.map status (fun _ () -> ()) () aux t
     in
      aux () t
   in 
@@ -80,17 +80,17 @@ let src_tgt_of_ty_cpos_arity ty cpos arity =
   mask (pi_tail 0 tpos ty)
 ;;
 
-let rec cleanup_skel () = function
+let rec cleanup_skel status () = function
   | NCic.Meta _ -> skel_dummy
-  | t -> NCicUtils.map (fun _ () -> ()) () cleanup_skel t
+  | t -> NCicUtils.map status (fun _ () -> ()) () (cleanup_skel status) t
 ;;
 
-let close_in_context t metasenv = 
+let close_in_context status t metasenv = 
   let rec aux m_subst subst ctx = function
    | (i,(tag,[],ty)) :: tl ->
         let name = "x" ^ string_of_int (List.length ctx) in
         let subst = (i,(tag,[],NCic.Rel (List.length tl+1),ty))::subst in
-        let ty = NCicUntrusted.apply_subst (m_subst (List.length ctx)) ctx ty in
+        let ty = NCicUntrusted.apply_subst status (m_subst (List.length ctx)) ctx ty in
         let m_subst m = 
           (i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m)
         in
@@ -100,20 +100,20 @@ let close_in_context t metasenv =
                 since metas occurring in t have an empty context,
                 the substitution i build makes sense (i.e, the Rel
                 I pun in the subst will not be lifted by subst_meta *)
-           NCicUntrusted.apply_subst subst ctx
-             (NCicSubstitution.lift (List.length ctx) t)
+           NCicUntrusted.apply_subst status subst ctx
+             (NCicSubstitution.lift status (List.length ctx) t)
    | _ -> assert false
   in
   aux (fun _ -> []) [] [] metasenv
 ;;
 
-let toposort metasenv = 
+let toposort status metasenv = 
   let module T = HTopoSort.Make(
     struct type t = int * NCic.conjecture let compare (i,_) (j,_) = i-j end) 
   in
   let deps (_,(_,_,t)) =
     List.filter (fun (j,_) -> 
-      List.mem j (NCicUntrusted.metas_of_term [] [] t)) metasenv
+      List.mem j (NCicUntrusted.metas_of_term status [] [] t)) metasenv
   in
   T.topological_sort metasenv deps
 ;;
@@ -133,26 +133,29 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
            (try 
             let metasenv,subst,status,src =
               GrafiteDisambiguate.disambiguate_nterm 
-                status None ctx [] [] ("",0,src) in
-            let src = NCicUntrusted.apply_subst subst [] src in
+                status `XTSort ctx [] [] ("",0,src) in
+            let src = NCicUntrusted.apply_subst status 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
+            let src = cleanup_skel status () src in
             status, src, cpos
            with 
-           | NCicUnification.UnificationFailure _
-           | NCicUnification.Uncertain _
-           | MultiPassDisambiguator.DisambiguationError _ ->
-               raise (GrafiteTypes.Command_error "bad source pattern"))
+           | NCicUnification.UnificationFailure msg
+           | NCicUnification.Uncertain msg ->
+               raise (GrafiteTypes.Command_error ("bad source pattern: " ^ 
+Lazy.force msg))
+            | MultiPassDisambiguator.DisambiguationError _ ->
+               raise (GrafiteTypes.Command_error ("bad source pattern: 
+disambiguation error")))
       | _ -> assert false
     in
       aux 0 [] ty
   in
   let status, tgt, arity = 
-    let metasenv,subst,status,tgt =
+    let _metasenv,subst,status,tgt =
       GrafiteDisambiguate.disambiguate_nterm 
-        status None [] [] [] ("",0,tgt) in
-    let tgt = NCicUntrusted.apply_subst subst [] tgt in
+        status `XTSort [] [] [] ("",0,tgt) in
+    let tgt = NCicUntrusted.apply_subst status subst [] tgt in
     (* CHECK che sia unificabile mancante *)
     let rec count_prod = function
       | NCic.Prod (_,_,x) -> 1 + count_prod x
@@ -161,7 +164,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
     let arity = count_prod tgt in
     let tgt=
       if arity > 0 then cleanup_funclass_skel tgt 
-      else cleanup_skel () tgt 
+      else cleanup_skel status () tgt 
     in
      status, tgt, arity
   in
@@ -179,7 +182,7 @@ let fresh_uri status prefix suffix =
 
 exception Stop;;
 
-let close_graph name t s d to_s from_d p a status =
+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) 
@@ -217,32 +220,32 @@ let close_graph name t s d to_s from_d p a status =
                 NCicUnification.unify status metasenv subst [] a b)
             (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 bo = NCicUntrusted.apply_subst status subst [] bo in
+         let p = NCicUntrusted.apply_subst status subst [] p in
+         let metasenv = NCicUntrusted.apply_subst_metasenv status subst metasenv in
+         let metasenv = toposort status metasenv in
+         let bo = close_in_context status bo metasenv in
          let pos = 
            match p with 
            | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv) 
-           | t -> raise Stop
+           | _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 ty = NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] [] bo in
+         let src,tgt = src_tgt_of_ty_cpos_arity status ty pos arity in
          let src = only_head src in
          let tgt = only_head tgt in
          debug (lazy(
            "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 ^
+           status#ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
+           status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
+           status#ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
+           status#ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^
            " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity));
          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 height = NCicTypeChecker.height_of_obj_kind status uri [] obj_kind in
          let obj = uri,height,[],[],obj_kind in
          let c = 
            NCic.Const 
@@ -259,11 +262,11 @@ let close_graph name t s d to_s from_d p a status =
 ;;
 
 (* idempotent *)
-let basic_index_ncoercion (name,t,s,d,position,arity) status =
+let basic_index_ncoercion (name,_compose,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 basic_eval_ncoercion (name,compose,t,s,d,p,a) status =
   let to_s = 
     NCicCoercion.look_for_coercion status [] [] [] skel_dummy s
   in
@@ -271,10 +274,11 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status =
     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
+  let composites =
+   if compose then close_graph name t s d to_s from_d p a status else [] in
   List.fold_left 
     (fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) -> 
-      let info = name,t,s,d,p,a in
+      let info = name,compose,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)
@@ -282,50 +286,52 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status =
 ;;
 
 let record_ncoercion =
- let aux (name,t,s,d,p,a) ~refresh_uri_in_term =
+ let aux (name,compose,t,s,d,p,a) ~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_index_ncoercion (name,t,s,d,p,a)
+   basic_index_ncoercion (name,compose,t,s,d,p,a)
  in
- let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
-  ~refresh_uri_in_reference
+ let aux_l l ~refresh_uri_in_universe:_ ~refresh_uri_in_term
+  ~refresh_uri_in_reference:_ ~alias_only status
  =
-   List.fold_right (aux ~refresh_uri_in_term) l
+  if not alias_only then
+   List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status
+  else
+   status
  in
-  GrafiteTypes.Serializer.register#run "ncoercion" aux_l 
+  GrafiteTypes.Serializer.register#run "ncoercion" aux_l
 ;;
 
 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
+  NCicLibrary.dump_obj status (record_ncoercion (infos::cinfos)), uris
 ;;
 
 let basic_eval_and_record_ncoercion_from_t_cpos_arity 
-      status (name,t,cpos,arity) 
+      status (name,compose,t,cpos,arity) 
 =
-  let ty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] t in
-  let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in
+  let ty = NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] [] t in
+  let src,tgt = src_tgt_of_ty_cpos_arity status ty cpos arity in
   let status, uris =
-   basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
+   basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status
   in
    status,uris
 ;;
 
-let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt = 
+let eval_ncoercion (status: #GrafiteTypes.status) name compose t ty (id,src) tgt = 
  let metasenv,subst,status,ty =
-  GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
+  GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] ("",0,ty) in
  assert (metasenv=[]);
- let ty = NCicUntrusted.apply_subst subst [] ty in
+ let ty = NCicUntrusted.apply_subst status subst [] ty in
  let metasenv,subst,status,t =
-  GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
+  GrafiteDisambiguate.disambiguate_nterm status (`XTSome ty) [] [] [] ("",0,t) in
  assert (metasenv=[]);
- let t = NCicUntrusted.apply_subst subst [] t in
+ let t = NCicUntrusted.apply_subst status subst [] t in
  let status, src, tgt, cpos, arity = 
    src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
  let status, uris =
-  basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
+  basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status
  in
   status,uris
 ;;