Added "nocomposites" to coercions.

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index ff26c00d680315440942891ec47411c8d053f316..6b5344f580b4873aa62b3d5be45916e04d136dbd 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -84,7 +84,7 @@ type nmacro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 35
+let magic = 36
 
 (* composed magic: term + command magics. No need to change this value *)
 let magic = magic + 10000 * NotationPt.magic
@@ -104,9 +104,7 @@ type command =
   | NInverter of loc * string * nterm * bool list option * nterm option
   | NUnivConstraint of loc * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
-  | NCoercion of loc * string *
-      nterm * nterm *
-      (string * nterm) * nterm
+  | NCoercion of loc * string * bool * nterm * nterm * (string * nterm) * nterm
   | NQed of loc
   (* ex lexicon commands *)
   | Alias of loc * alias_spec

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 2f37a4e92f5c1fcc0ba6a84c2ebfed95a0725a92..f286cf6b8160fac4bc34dba41eeaf018742b5b11 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -485,9 +485,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       GrafiteTypes.Serializer.require
        ~alias_only ~baseuri ~fname:fullpath status
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
-  | GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
+  | GrafiteAst.NCoercion (loc, name, compose, t, ty, source, target) ->
      let status, composites =
-      NCicCoercDeclaration.eval_ncoercion status name t ty source target in
+      NCicCoercDeclaration.eval_ncoercion status name compose t ty source
+       target in
      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
      let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
       eval_alias status (mode,aliases)
@@ -622,7 +623,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                  let status, nuris = 
                    NCicCoercDeclaration.
                      basic_eval_and_record_ncoercion_from_t_cpos_arity 
-                      status (name,t,cpos,arity) in
+                      status (name,true,t,cpos,arity) in
                  let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in
                   eval_alias status (mode,aliases)
                with MultiPassDisambiguator.DisambiguationError _-> 

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml
index f1b051d46f229915a02bdfe15daaf9f238a0a3d0..929d1123560a92103b8b8ddc34a9f88ae5830a2f 100644 (file)
--- a/matita/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml
@@ -259,11 +259,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 +271,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,11 +283,11 @@ 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
@@ -305,17 +306,17 @@ 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 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=[]);
@@ -327,7 +328,7 @@ let eval_ncoercion (status: #GrafiteTypes.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, 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
 ;;

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.mli b/matita/components/grafite_engine/nCicCoercDeclaration.mli
index 9bca1143d3fdb4315be5bd1d5d7f763193cb9ee3..66e3a561b33ca5c65dc1f69b0ef6f26f5b7b80aa 100644 (file)
--- a/matita/components/grafite_engine/nCicCoercDeclaration.mli
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.mli
@@ -10,10 +10,11 @@
       V_______________________________________________________________ *)
 
 
-(* evals a coercion declaration statement: name t ty (id,src) tgt *)
+(* evals a coercion declaration statement: name compose t ty (id,src) tgt *)
 val eval_ncoercion: 
    #GrafiteTypes.status as 'status ->
      string ->
+     bool ->
      NotationPt.term ->
      NotationPt.term ->
      string * NotationPt.term ->
@@ -24,5 +25,5 @@ val eval_ncoercion:
  * the arity in the `:arity>` syntax *)
 val basic_eval_and_record_ncoercion_from_t_cpos_arity: 
    #GrafiteTypes.status as 'status ->
-     string * NCic.term * int * int -> 'status * NUri.uri list
+     string * bool * NCic.term * int * int -> 'status * NUri.uri list
 

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index aeb0080c4fa163023069d8d2e681fffccf46933c..762da10f5131c05e482b3cafcdab069eb8a48ff8 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -579,8 +579,9 @@ EXTEND
     | IDENT "coercion"; name = IDENT; SYMBOL ":"; ty = term; 
         SYMBOL <:unicode<def>>; t = term; "on"; 
         id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
-        "to"; target = term ->
-          G.NCoercion(loc,name,t,ty,(id,source),target)     
+        "to"; target = term; compose = OPT [ IDENT "nocomposites" -> () ]  ->
+          let compose = compose = None in
+          G.NCoercion(loc,name,compose,t,ty,(id,source),target)     
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         G.NObj (loc, N.Record (params,name,ty,fields))
     | IDENT "copy" ; s = IDENT; IDENT "from"; u = URI; "with"; 

diff --git a/matita/components/ng_paramodulation/nCicProof.ml b/matita/components/ng_paramodulation/nCicProof.ml
index cabca8259aefc524e89ed5b0e8e74f27049df70e..3f30a85c30ca84422d9b7554f3050581a0d4ac92 100644 (file)
--- a/matita/components/ng_paramodulation/nCicProof.ml
+++ b/matita/components/ng_paramodulation/nCicProof.ml
@@ -181,7 +181,7 @@ let debug c _ = c;;
               List.fold_left
                (fun (i,acc) t ->
                  i+1,
-                      let f = extract status amount vl f in
+                  let f = extract status amount vl f in
                   if i = n then
                    let imp = NCic.Implicit `Term in
                     NCic.Appl (dag::imp::imp::imp(* f *)::imp::imp::

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index 1e37ff79793ba03894f306c0be69acb50bbe7115..c8f67f1769e523fd53df6f7c067d99c68bcfa915 100644 (file)
--- a/matita/components/ng_refiner/nCicUnification.ml
+++ b/matita/components/ng_refiner/nCicUnification.ml
@@ -99,6 +99,8 @@ let outside exc_opt =
     match !times with time1::tl -> times := tl; time1 | [] -> assert false in
    prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1));
    (match exc_opt with
+   | Some (UnificationFailure msg) ->  prerr_endline ("exception raised: NCicUnification.UnificationFailure:" ^ Lazy.force msg)
+   | Some (Uncertain msg) ->  prerr_endline ("exception raised: NCicUnification.Uncertain:" ^ Lazy.force msg)
    | Some e ->  prerr_endline ("exception raised: " ^ Printexc.to_string e)
    | None -> ());
    try

diff --git a/matita/components/syntax_extensions/.depend b/matita/components/syntax_extensions/.depend
index 25e67131fca0487c4390d310d8307722b5058067..119f13093a98003e4d06ea0244ce7aae7f76e6e3 100644 (file)
--- a/matita/components/syntax_extensions/.depend
+++ b/matita/components/syntax_extensions/.depend
@@ -1,5 +1,5 @@
-utf8Macro.cmi: 
-utf8MacroTable.cmo: 
-utf8MacroTable.cmx: 
-utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi 
-utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi 
+utf8Macro.cmi:
+utf8MacroTable.cmo:
+utf8MacroTable.cmx:
+utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
+utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi