X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=5d1b81d7442605411098412ab3f332ab332e3966;hb=a4de429b26c16152e710bfaa07c8814cc3cb018f;hp=ceaa759622a741ab37768c6482fd415a0b62494e;hpb=b964a69273d19ed84a7a3d089fceaf475f8ae1ea;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index ceaa75962..5d1b81d74 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -637,12 +637,14 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status =
          in
          let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
          let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in
+(*
          prerr_endline (
            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 (bo,src,tgt,arity,pos)
        with 
        | NCicTypeChecker.TypeCheckerFailure _
@@ -960,31 +962,63 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           | _ -> obj_kind
         in
         let obj = uri,height,[],[],obj_kind in
-         let status = NCicLibrary.add_obj status obj in
-       prerr_endline (NCicPp.ppobj obj);
-         let boxml = NCicElim.mk_elims obj in
+        let old_status = status in
+        let status = NCicLibrary.add_obj status obj in
+        HLog.message ("New object: " ^ NUri.string_of_uri uri);
+         (try
+       (*prerr_endline (NCicPp.ppobj obj);*)
+           let boxml = NCicElim.mk_elims obj in
+           let boxml = boxml @ NCicElim.mk_projections obj in
 (*
-         let objs = [] in
-         let timestamp,uris_rev =
-           List.fold_left
-            (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
-              let status = NCicLibrary.add_obj status obj in
-               status,uri::uris_rev
-            ) (status,[]) objs in
-         let uris = uri::List.rev uris_rev in
+           let objs = [] in
+           let timestamp,uris_rev =
+             List.fold_left
+              (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
+                let status = NCicLibrary.add_obj status obj in
+                 status,uri::uris_rev
+              ) (status,[]) objs in
+           let uris = uri::List.rev uris_rev in
 *)
-         let status = status#set_ng_mode `CommandMode in
-let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
-         List.fold_left
-          (fun (status,uris) boxml ->
-            let status,nuris =
-             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,`New [] (* uris *)) boxml
+           let status = status#set_ng_mode `CommandMode in
+           let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
+           let status,uris =
+            List.fold_left
+             (fun (status,uris) boxml ->
+               try
+                let status,nuris =
+                 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
+               with
+                NCicTypeChecker.TypeCheckerFailure msg
+                 when Lazy.force msg =
+                 "Sort elimination not allowed" ->
+                  status,uris
+             ) (status,`New [] (* uris *)) boxml in
+           let coercions =
+            match obj with
+              _,_,_,_,NCic.Inductive
+               (true,leftno,[_,_,_,[_,_,_]],(_,`Record fields))
+               ->
+                HExtlib.filter_map
+                 (fun (name,is_coercion,arity) ->
+                   if is_coercion then Some(name,leftno,arity) else None) fields
+            | _ -> [] in
+           let status =
+            List.fold_left
+             (fun status (name,cpos,arity) ->
+                (*CSC: COME DICHIARO LA COERCION??? *)
+                status
+             ) status coercions
+           in
+            status,uris
+          with
+           exn ->
+            NCicLibrary.time_travel old_status;
+            raise exn)
   | GrafiteAst.NCopy (log,tgt,src_uri, map) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")
@@ -1011,7 +1045,7 @@ let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
        in
        let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
        let status = status#set_obj (tgt_uri,0,[],[],ok) in
-       prerr_endline (NCicPp.ppobj (tgt_uri,0,[],[],ok));
+       (*prerr_endline (NCicPp.ppobj (tgt_uri,0,[],[],ok));*)
        let status = status#set_stack ninitial_stack in
        let status = subst_metasenv_and_fix_names status in
        let status = status#set_ng_mode `ProofMode in