Almost ready to implement coercion declaration for record fields. But how?

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index b5f503497590bca86fd161922f417d9d9d586c3c..5d1b81d7442605411098412ab3f332ab332e3966 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -964,9 +964,11 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         let obj = uri,height,[],[],obj_kind 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 =
@@ -979,16 +981,40 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
 *)
            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,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;