Bug fixed: singleton application.

[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 1fd62d2b1eedb56e66bb153903cae5f15a0fde8e..f1aea02da0a71efd0bece6fa26c0df667a5cc685 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -510,7 +510,7 @@ let pos_in_list x l =
         HExtlib.list_findopt (fun y i -> if y = x then Some i else None) l
       with
       | Some i -> i
-      | None _ -> assert false
+      | None -> assert false
 ;;
 
 let pos_of x t = 
@@ -531,7 +531,7 @@ let term_at i t =
         HExtlib.list_findopt (fun y j -> if i+1=j then Some y else None) l
       with
       | Some i -> i
-      | None _ -> assert false)
+      | None -> assert false)
   | _ -> assert false
 ;;
 
@@ -956,7 +956,10 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         in
         let obj = uri,height,[],[],obj_kind in
          let status = NCicLibrary.add_obj status obj in
-         let objs = NCicElim.mk_elims obj in
+       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 ->
@@ -964,7 +967,50 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                status,uri::uris_rev
             ) (status,[]) objs in
          let uris = uri::List.rev uris_rev in
-          status#set_ng_mode `CommandMode,`New uris
+*)
+         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
+  | 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")