X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=b5f503497590bca86fd161922f417d9d9d586c3c;hb=8ced93b24ec20302294b3f627a6d06fc36bcc41a;hp=6533e3f86397dbfc38b34a552a5b4880427ba0ef;hpb=f8830ea7f8b308241d73e558092089a24ab2f867;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 6533e3f86..b5f503497 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -565,7 +565,12 @@ let close_in_context t metasenv =
           (i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m)
         in
         NCic.Lambda (name, ty, aux m_subst subst ((name,NCic.Decl ty)::ctx) tl)
-   | [] -> NCicUntrusted.apply_subst subst ctx
+   | [] -> 
+           (* STRONG ASSUMPTION: 
+                since metas occurring in t have an empty context,
+                the substitution i build makes sense (i.e, the Rel
+                I pun in the subst will not be lifted by subst_meta *)
+           NCicUntrusted.apply_subst subst ctx
              (NCicSubstitution.lift (List.length ctx) t)
    | _ -> assert false
   in
@@ -632,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 _
@@ -955,16 +962,68 @@ 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
-         let objs = NCicElim.mk_elims obj in
-         let timestamp,uris_rev =
+        let old_status = status in
+        let status = NCicLibrary.add_obj status obj in
+         (try
+       (*prerr_endline (NCicPp.ppobj obj);*)
+           let boxml = NCicElim.mk_elims 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 status = status#set_ng_mode `CommandMode in
+           let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
            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
-          status#set_ng_mode `CommandMode,`New uris
+            (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
+          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")
+     else
+       let tgt_uri_ext, old_ok = 
+         match NCicEnvironment.get_checked_obj src_uri with
+         | _,_,[],[], (NCic.Inductive _ as ok) -> ".ind", ok
+         | _,_,[],[], (NCic.Fixpoint _ as ok) -> ".con", ok
+         | _,_,[],[], (NCic.Constant _ as ok) -> ".con", ok
+         | _ -> assert false
+       in
+       let tgt_uri = NUri.uri_of_string (status#baseuri^"/"^tgt^tgt_uri_ext) in
+       let map = (src_uri, tgt_uri) :: map in
+       let ok = 
+         let rec subst () = function
+           | NCic.Meta _ -> assert false
+           | NCic.Const (NReference.Ref (u,spec)) as t ->
+               (try NCic.Const 
+                 (NReference.reference_of_spec (List.assoc u map)spec)
+               with Not_found -> t)
+           | t -> NCicUtils.map (fun _ _ -> ()) () subst t
+         in
+         NCicUntrusted.map_obj_kind ~skip_body:false (subst ()) old_ok
+       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));*)
+       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
+       eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
   | GrafiteAst.NObj (loc,obj) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")