From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 22 Jul 2009 09:24:55 +0000 (+0000)
Subject: Almost ready to implement coercion declaration for record fields. But how?
X-Git-Tag: make_still_working~3638
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b0325c1fa8f59f8aaff2b6df59f3852338e82523;p=helm.git

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

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 99414f63c..5d1b81d74 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -981,22 +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 ->
-              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
+           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;