snapshot for CSC

[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..0904cf33119b99ff7183b998af6d1edbd95f01cb 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -538,9 +538,18 @@ let term_at i t =
 let src_tgt_of_ty_cpos_arity ty cpos arity =
   let pis = count_prod ty in
   let tpos = pis - arity in
-  let rec aux i j = function
+  let rec pi_nth i j = function
     | NCic.Prod (_,s,_) when i = j -> s
-    | NCic.Prod (_,_,t) -> aux (i+1) j t
+    | NCic.Prod (_,_,t) -> pi_nth (i+1) j t
+    | t -> assert (i = j); t
+  in
+  let rec cleanup_prod = function
+    | NCic.Prod (_,_,t) -> NCic.Prod ("_",NCic.Implicit `Type, cleanup_prod t)
+    | _ -> NCic.Implicit `Type
+  in
+  let rec pi_tail i j = function
+    | NCic.Prod (_,_,_) as t when i = j -> cleanup_prod t
+    | NCic.Prod (_,_,t) -> pi_tail (i+1) j t
     | t -> assert (i = j); t
   in
   let mask t =
@@ -552,7 +561,8 @@ let src_tgt_of_ty_cpos_arity ty cpos arity =
     in
      aux () t
   in 
-  mask (aux 0 cpos ty), mask (aux 0 tpos ty)
+  mask (pi_nth 0 cpos ty), 
+  mask (pi_tail 0 tpos ty)
 ;;
 
 let close_in_context t metasenv = 
@@ -658,8 +668,13 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status =
 ;;
 
 let inject_ncoercion =
- let basic_eval_ncoercion x ~refresh_uri_in_universe ~refresh_uri_in_term =
-  basic_eval_ncoercion x
+ let basic_eval_ncoercion (name,t,s,d,p,a) ~refresh_uri_in_universe
+  ~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_eval_ncoercion (name,t,s,d,p,a)
  in
   NRstatus.Serializer.register "ncoercion" basic_eval_ncoercion
 ;;
@@ -702,6 +717,12 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
   status, src, tgt, cpos, arity
 ;;
 
+let basic_eval_and_inject_ncoercion infos status =
+ let status = basic_eval_ncoercion infos status in
+ let dump = inject_ncoercion infos::status#dump in
+  status#set_dump dump
+;;
+
 let eval_ncoercion status name t ty (id,src) tgt = 
 
  let metasenv,subst,status,ty =
@@ -714,12 +735,10 @@ let eval_ncoercion status name t ty (id,src) tgt =
  let t = NCicUntrusted.apply_subst subst [] t in
 
  let status, src, tgt, cpos, arity = 
-   src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt
+   src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
+ let status =
+  basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status
  in
-
- let status = basic_eval_ncoercion (name,t,src,tgt,cpos,arity) status in
- let dump = inject_ncoercion (name,t,src,tgt,cpos,arity)::status#dump in
- let status = status#set_dump dump in
   status,`New []
 ;;
 
@@ -964,9 +983,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 +1000,46 @@ 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) ->
+               let metasenv,subst,status,t =
+                GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+                 ("",0,CicNotationPt.Ident (name,None)) in
+               assert (metasenv = [] && subst = []);
+               let ty = NCicTypeChecker.typeof ~subst ~metasenv [] t in
+               let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in
+                basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity)
+                 status
+             ) status coercions
+           in
+            status,uris
           with
            exn ->
             NCicLibrary.time_travel old_status;