Matitaweb: large commit porting to the new Matita 0.95 syntax.

[helm.git] / matitaB / components / grafite_engine / nCicCoercDeclaration.ml

diff --git a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
index 2693d608b37307140d80fa6b2b063f3447cbbd4e..03e3f87e18d452c0f2ee5305800969acf7827650 100644 (file)
--- a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml
@@ -134,7 +134,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
          if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
          else
            (try 
-            let newast,metasenv,subst,status,src =
+            let metasenv,subst,status,src =
               GrafiteDisambiguate.disambiguate_nterm 
                 status None ctx [] [] ("",0,src) in
             let src = NCicUntrusted.apply_subst status subst [] src in
@@ -145,14 +145,14 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
            with 
            | NCicUnification.UnificationFailure _
            | NCicUnification.Uncertain _
-           | MultiPassDisambiguator.DisambiguationError _ ->
+           | GrafiteDisambiguate.Error _ -> 
                raise (GrafiteTypes.Command_error "bad source pattern"))
       | _ -> assert false
     in
       aux 0 [] ty
   in
   let status, tgt, arity = 
-    let newast, metasenv,subst,status,tgt =
+    let metasenv,subst,status,tgt =
       GrafiteDisambiguate.disambiguate_nterm 
         status None [] [] [] ("",0,tgt) in
     let tgt = NCicUntrusted.apply_subst status subst [] tgt in
@@ -174,7 +174,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
 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
+    if NCicLibrary.aliases_of status u = [] then u
     else diverge (mk ("__" ^ string_of_int i)) (i+1)
   in
    diverge (mk "") 0
@@ -262,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
@@ -274,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)
@@ -285,17 +286,17 @@ 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 ~alias_only status
  =
   if not alias_only then
-   List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status
+   List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status))) l status
   else
    status
  in
@@ -308,29 +309,29 @@ let basic_eval_and_record_ncoercion infos status =
 ;;
 
 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 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 newast_ty,metasenv,subst,status,ty =
+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
  assert (metasenv=[]);
  let ty = NCicUntrusted.apply_subst status subst [] ty in
- let newast_t,metasenv,subst,status,t =
+ let metasenv,subst,status,t =
   GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
  assert (metasenv=[]);
  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
 ;;