matita/components/grafite_engine/grafiteEngine.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id$ *)
  27
  28 exception Drop
  29 (* mo file name, ma file name *)
  30 exception IncludedFileNotCompiled of string * string
  31 exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
  32
  33 type 'a disambiguator_input = string * int * 'a
  34
  35 type options = {
  36   do_heavy_checks: bool ;
  37 }
  38
  39 let concat_nuris uris nuris =
  40    match uris,nuris with
  41    | `New uris, `New nuris -> `New (nuris@uris)
  42    | _ -> assert false
  43 ;;
  44
  45 type eval_ast =
  46  {ea_go:
  47   'term 'lazy_term 'reduction 'obj 'ident.
  48
  49   disambiguate_command:
  50    (GrafiteTypes.status ->
  51     (GrafiteAst.command) disambiguator_input ->
  52     GrafiteTypes.status * GrafiteAst.command) ->
  53
  54   ?do_heavy_checks:bool ->
  55   GrafiteTypes.status ->
  56   GrafiteAst.statement disambiguator_input ->
  57   GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
  58  }
  59
  60 type 'a eval_command =
  61  {ec_go: 'term 'obj.
  62   disambiguate_command:
  63    (GrafiteTypes.status -> GrafiteAst.command disambiguator_input ->
  64     GrafiteTypes.status * GrafiteAst.command) ->
  65   options -> GrafiteTypes.status ->
  66     GrafiteAst.command disambiguator_input ->
  67    GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
  68  }
  69
  70 type 'a eval_comment =
  71  {ecm_go: 'term 'lazy_term 'reduction_kind 'obj 'ident.
  72   disambiguate_command:
  73    (GrafiteTypes.status -> GrafiteAst.command disambiguator_input ->
  74     GrafiteTypes.status * GrafiteAst.command) ->
  75   options -> GrafiteTypes.status -> GrafiteAst.comment disambiguator_input ->
  76    GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
  77  }
  78
  79 type 'a eval_executable =
  80  {ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
  81
  82   disambiguate_command:
  83    (GrafiteTypes.status ->
  84     GrafiteAst.command disambiguator_input ->
  85     GrafiteTypes.status * GrafiteAst.command) ->
  86
  87   options ->
  88   GrafiteTypes.status -> GrafiteAst.code disambiguator_input ->
  89   GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
  90  }
  91
  92 type 'a eval_from_moo =
  93  { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
  94
  95 let basic_eval_unification_hint (t,n) status =
  96  NCicUnifHint.add_user_provided_hint status t n
  97 ;;
  98
  99 let inject_unification_hint =
 100  let basic_eval_unification_hint (t,n)
 101    ~refresh_uri_in_universe
 102    ~refresh_uri_in_term
 103  =
 104   let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
 105  in
 106   NCicLibrary.Serializer.register#run "unification_hints"
 107    object(_ : 'a NCicLibrary.register_type)
 108      method run = basic_eval_unification_hint
 109    end
 110 ;;
 111
 112 let eval_unification_hint status t n =
 113  let metasenv,subst,status,t =
 114   GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,t) in
 115  assert (metasenv=[]);
 116  let t = NCicUntrusted.apply_subst subst [] t in
 117  let status = basic_eval_unification_hint (t,n) status in
 118  let dump = inject_unification_hint (t,n)::status#dump in
 119  let status = status#set_dump dump in
 120   status,`New []
 121 ;;
 122
 123 let basic_index_obj l status =
 124   status#set_auto_cache
 125     (List.fold_left
 126       (fun t (ks,v) ->
 127          List.fold_left (fun t k ->
 128            NDiscriminationTree.DiscriminationTree.index t k v)
 129           t ks)
 130     status#auto_cache l)
 131 ;;
 132
 133 let record_index_obj =
 134  let aux l
 135    ~refresh_uri_in_universe
 136    ~refresh_uri_in_term
 137  =
 138     basic_index_obj
 139       (List.map
 140         (fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v)
 141       l)
 142  in
 143   NCicLibrary.Serializer.register#run "index_obj"
 144    object(_ : 'a NCicLibrary.register_type)
 145      method run = aux
 146    end
 147 ;;
 148
 149 let compute_keys status uri height kind =
 150  let mk_item ty spec =
 151    let orig_ty = NTacStatus.mk_cic_term [] ty in
 152    let status,keys = NnAuto.keys_of_type status orig_ty in
 153    let keys =
 154      List.map
 155        (fun t ->
 156           snd (NTacStatus.term_of_cic_term status t (NTacStatus.ctx_of t)))
 157        keys
 158    in
 159    keys,NCic.Const(NReference.reference_of_spec uri spec)
 160  in
 161  let data =
 162   match kind with
 163   | NCic.Fixpoint (ind,ifl,_) ->
 164      HExtlib.list_mapi
 165        (fun (_,_,rno,ty,_) i ->
 166           if ind then mk_item ty (NReference.Fix (i,rno,height))
 167           else mk_item ty (NReference.CoFix height)) ifl
 168   | NCic.Inductive (b,lno,itl,_) ->
 169      HExtlib.list_mapi
 170        (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl
 171      @
 172      List.map (fun ((_,_,ty),i,j) -> mk_item ty (NReference.Con (i,j+1,lno)))
 173        (List.flatten (HExtlib.list_mapi
 174          (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl)
 175          itl))
 176   | NCic.Constant (_,_,Some _, ty, _) ->
 177      [ mk_item ty (NReference.Def height) ]
 178   | NCic.Constant (_,_,None, ty, _) ->
 179      [ mk_item ty NReference.Decl ]
 180  in
 181   HExtlib.filter_map
 182    (fun (keys, t) ->
 183      let keys = List.filter
 184        (function
 185          | (NCic.Meta _)
 186          | (NCic.Appl (NCic.Meta _::_)) -> false
 187          | _ -> true)
 188        keys
 189      in
 190      if keys <> [] then
 191       begin
 192         HLog.debug ("Indexing:" ^
 193           NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
 194         HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t ->
 195           NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys));
 196         Some (keys,t)
 197       end
 198      else
 199       begin
 200         HLog.debug ("Not indexing:" ^
 201           NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
 202         None
 203       end)
 204     data
 205 ;;
 206
 207 let index_obj_for_auto status (uri, height, _, _, kind) =
 208  (*prerr_endline (string_of_int height);*)
 209   let data = compute_keys status uri height kind in
 210   let status = basic_index_obj data status in
 211   let dump = record_index_obj data :: status#dump in
 212   status#set_dump dump
 213 ;;
 214
 215 let index_eq uri status =
 216   let eq_status = status#eq_cache in
 217   let eq_status1 = NCicParamod.index_obj eq_status uri in
 218     status#set_eq_cache eq_status1
 219 ;;
 220
 221 let record_index_eq =
 222  let basic_index_eq uri
 223    ~refresh_uri_in_universe
 224    ~refresh_uri_in_term
 225    = index_eq (NCicLibrary.refresh_uri uri)
 226  in
 227   NCicLibrary.Serializer.register#run "index_eq"
 228    object(_ : 'a NCicLibrary.register_type)
 229      method run = basic_index_eq
 230    end
 231 ;;
 232
 233 let index_eq_for_auto status uri =
 234  if NnAuto.is_a_fact_obj status uri then
 235    let newstatus = index_eq uri status in
 236      if newstatus#eq_cache == status#eq_cache then status
 237      else
 238        ((*prerr_endline ("recording " ^ (NUri.string_of_uri uri));*)
 239         let dump = record_index_eq uri :: newstatus#dump
 240         in newstatus#set_dump dump)
 241  else
 242    ((*prerr_endline "Not a fact";*)
 243    status)
 244 ;;
 245
 246 let basic_eval_add_constraint (u1,u2) status =
 247  NCicLibrary.add_constraint status u1 u2
 248 ;;
 249
 250 let inject_constraint =
 251  let basic_eval_add_constraint (u1,u2)
 252        ~refresh_uri_in_universe
 253        ~refresh_uri_in_term
 254  =
 255   let u1 = refresh_uri_in_universe u1 in
 256   let u2 = refresh_uri_in_universe u2 in
 257   basic_eval_add_constraint (u1,u2)
 258  in
 259   NCicLibrary.Serializer.register#run "constraints"
 260    object(_:'a NCicLibrary.register_type)
 261      method run = basic_eval_add_constraint
 262    end
 263 ;;
 264
 265 let eval_add_constraint status u1 u2 =
 266  let status = basic_eval_add_constraint (u1,u2) status in
 267  let dump = inject_constraint (u1,u2)::status#dump in
 268  let status = status#set_dump dump in
 269   status,`New []
 270 ;;
 271
 272 let eval_ng_tac tac =
 273  let rec aux f (text, prefix_len, tac) =
 274   match tac with
 275   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t)
 276   | GrafiteAst.NSmartApply (_loc, t) ->
 277       NnAuto.smart_apply_tac (text,prefix_len,t)
 278   | GrafiteAst.NAssert (_loc, seqs) ->
 279      NTactics.assert_tac
 280       ((List.map
 281         (function (hyps,concl) ->
 282           List.map
 283            (function
 284               (id,`Decl t) -> id,`Decl (text,prefix_len,t)
 285              |(id,`Def (b,t))->id,`Def((text,prefix_len,b),(text,prefix_len,t))
 286            ) hyps,
 287           (text,prefix_len,concl))
 288        ) seqs)
 289   | GrafiteAst.NAuto (_loc, (None,a)) ->
 290       NnAuto.auto_tac ~params:(None,a) ?trace_ref:None
 291   | GrafiteAst.NAuto (_loc, (Some l,a)) ->
 292       NnAuto.auto_tac
 293         ~params:(Some List.map (fun x -> "",0,x) l,a) ?trace_ref:None
 294   | GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false
 295   | GrafiteAst.NCases (_loc, what, where) ->
 296       NTactics.cases_tac
 297         ~what:(text,prefix_len,what)
 298         ~where:(text,prefix_len,where)
 299   | GrafiteAst.NCase1 (_loc,n) -> NTactics.case1_tac n
 300   | GrafiteAst.NChange (_loc, pat, ww) ->
 301       NTactics.change_tac
 302        ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww)
 303   | GrafiteAst.NConstructor (_loc,num,args) ->
 304      NTactics.constructor_tac
 305        ?num ~args:(List.map (fun x -> text,prefix_len,x) args)
 306   | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t)
 307 (*| GrafiteAst.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
 308   | GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
 309   | GrafiteAst.NDestruct (_,dom,skip) -> NDestructTac.destruct_tac dom skip
 310   | GrafiteAst.NDot _ -> NTactics.dot_tac
 311   | GrafiteAst.NElim (_loc, what, where) ->
 312       NTactics.elim_tac
 313         ~what:(text,prefix_len,what)
 314         ~where:(text,prefix_len,where)
 315   | GrafiteAst.NFocus (_,l) -> NTactics.focus_tac l
 316   | GrafiteAst.NGeneralize (_loc, where) ->
 317       NTactics.generalize_tac ~where:(text,prefix_len,where)
 318   | GrafiteAst.NId _ -> (fun x -> x)
 319   | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
 320   | GrafiteAst.NIntros (_loc,ns) -> NTactics.intros_tac ns
 321   | GrafiteAst.NInversion (_loc, what, where) ->
 322       NTactics.inversion_tac
 323         ~what:(text,prefix_len,what)
 324         ~where:(text,prefix_len,where)
 325   | GrafiteAst.NLApply (_loc, t) -> NTactics.lapply_tac (text,prefix_len,t)
 326   | GrafiteAst.NLetIn (_loc,where,what,name) ->
 327       NTactics.letin_tac ~where:(text,prefix_len,where)
 328         ~what:(text,prefix_len,what) name
 329   | GrafiteAst.NMerge _ -> NTactics.merge_tac
 330   | GrafiteAst.NPos (_,l) -> NTactics.pos_tac l
 331   | GrafiteAst.NPosbyname (_,s) -> NTactics.case_tac s
 332   | GrafiteAst.NReduce (_loc, reduction, where) ->
 333       NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where)
 334   | GrafiteAst.NRewrite (_loc,dir,what,where) ->
 335      NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
 336       ~where:(text,prefix_len,where)
 337   | GrafiteAst.NSemicolon _ -> fun x -> x
 338   | GrafiteAst.NShift _ -> NTactics.shift_tac
 339   | GrafiteAst.NSkip _ -> NTactics.skip_tac
 340   | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
 341   | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac
 342   | GrafiteAst.NTry (_,tac) -> NTactics.try_tac
 343       (aux f (text, prefix_len, tac))
 344   | GrafiteAst.NAssumption _ -> NTactics.assumption_tac
 345   | GrafiteAst.NBlock (_,l) ->
 346       NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
 347   |GrafiteAst.NRepeat (_,tac) ->
 348       NTactics.repeat_tac (f f (text, prefix_len, tac))
 349  in
 350   aux aux tac (* trick for non uniform recursion call *)
 351 ;;
 352
 353 let subst_metasenv_and_fix_names status =
 354   let u,h,metasenv, subst,o = status#obj in
 355   let o =
 356     NCicUntrusted.map_obj_kind ~skip_body:true
 357      (NCicUntrusted.apply_subst subst []) o
 358   in
 359    status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
 360 ;;
 361
 362
 363 let rec eval_ncommand opts status (text,prefix_len,cmd) =
 364   match cmd with
 365   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
 366   | GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
 367       NCicCoercDeclaration.eval_ncoercion status name t ty source target
 368   | GrafiteAst.NQed loc ->
 369      if status#ng_mode <> `ProofMode then
 370       raise (GrafiteTypes.Command_error "Not in proof mode")
 371      else
 372       let uri,height,menv,subst,obj_kind = status#obj in
 373        if menv <> [] then
 374         raise
 375          (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
 376        else
 377         let obj_kind =
 378          NCicUntrusted.map_obj_kind
 379           (NCicUntrusted.apply_subst subst []) obj_kind in
 380         let height = NCicTypeChecker.height_of_obj_kind uri [] obj_kind in
 381         (* fix the height inside the object *)
 382         let rec fix () = function
 383           | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri ->
 384              NCic.Const (NReference.reference_of_spec u
 385               (match spec with
 386               | NReference.Def _ -> NReference.Def height
 387               | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
 388               | NReference.CoFix _ -> NReference.CoFix height
 389               | NReference.Ind _ | NReference.Con _
 390               | NReference.Decl as s -> s))
 391           | t -> NCicUtils.map (fun _ () -> ()) () fix t
 392         in
 393         let obj_kind =
 394           match obj_kind with
 395           | NCic.Fixpoint _ ->
 396               NCicUntrusted.map_obj_kind (fix ()) obj_kind
 397           | _ -> obj_kind
 398         in
 399         let obj = uri,height,[],[],obj_kind in
 400         prerr_endline ("pp new obj \n"^NCicPp.ppobj obj);
 401         let old_status = status in
 402         let status = NCicLibrary.add_obj status obj in
 403         let index_obj =
 404          match obj_kind with
 405             NCic.Constant (_,_,_,_,(_,`Example,_))
 406           | NCic.Fixpoint (_,_,(_,`Example,_)) -> false
 407           | _ -> true
 408         in
 409         let status =
 410          if index_obj then
 411           let status = index_obj_for_auto status obj in
 412            (try index_eq_for_auto status uri
 413            with _ -> status)
 414          else
 415           status in
 416 (*
 417           try
 418             index_eq uri status
 419           with _ -> prerr_endline "got an exception"; status
 420         in *)
 421 (*         prerr_endline (NCicPp.ppobj obj); *)
 422         HLog.message ("New object: " ^ NUri.string_of_uri uri);
 423          (try
 424        (*prerr_endline (NCicPp.ppobj obj);*)
 425            let boxml = NCicElim.mk_elims obj in
 426            let boxml = boxml @ NCicElim.mk_projections obj in
 427 (*
 428            let objs = [] in
 429            let timestamp,uris_rev =
 430              List.fold_left
 431               (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
 432                 let status = NCicLibrary.add_obj status obj in
 433                  status,uri::uris_rev
 434               ) (status,[]) objs in
 435            let uris = uri::List.rev uris_rev in
 436 *)
 437            let status = status#set_ng_mode `CommandMode in
 438            let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
 439            let status,uris =
 440             List.fold_left
 441              (fun (status,uris) boxml ->
 442                try
 443                 let nstatus,nuris =
 444                  eval_ncommand opts status
 445                   ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
 446                 in
 447                 if nstatus#ng_mode <> `CommandMode then
 448                   begin
 449                     (*HLog.warn "error in generating projection/eliminator";*)
 450                     status, uris
 451                   end
 452                 else
 453                   nstatus, concat_nuris uris nuris
 454                with
 455                | MultiPassDisambiguator.DisambiguationError _
 456                | NCicTypeChecker.TypeCheckerFailure _ ->
 457                   (*HLog.warn "error in generating projection/eliminator";*)
 458                   status,uris
 459              ) (status,`New [] (* uris *)) boxml in
 460            let _,_,_,_,nobj = obj in
 461            let status = match nobj with
 462                NCic.Inductive (is_ind,leftno,[it],_) ->
 463                  let _,ind_name,ty,cl = it in
 464                  List.fold_left
 465                    (fun status outsort ->
 466                       let status = status#set_ng_mode `ProofMode in
 467                       try
 468                        (let status,invobj =
 469                          NInversion.mk_inverter
 470                           (ind_name ^ "_inv_" ^
 471                             (snd (NCicElim.ast_of_sort outsort)))
 472                           is_ind it leftno outsort status status#baseuri in
 473                        let _,_,menv,_,_ = invobj in
 474                        fst (match menv with
 475                              [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
 476                            | _ -> status,`New []))
 477                        (* XXX *)
 478                       with _ -> (*HLog.warn "error in generating inversion principle"; *)
 479                                 let status = status#set_ng_mode `CommandMode in status)
 480                   status
 481                   (NCic.Prop::
 482                     List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
 483               | _ -> status
 484            in
 485            let coercions =
 486             match obj with
 487               _,_,_,_,NCic.Inductive
 488                (true,leftno,[_,_,_,[_,_,_]],(_,`Record fields))
 489                ->
 490                 HExtlib.filter_map
 491                  (fun (name,is_coercion,arity) ->
 492                    if is_coercion then Some(name,leftno,arity) else None) fields
 493             | _ -> [] in
 494            let status,uris =
 495             List.fold_left
 496              (fun (status,uris) (name,cpos,arity) ->
 497                try
 498                  let metasenv,subst,status,t =
 499                   GrafiteDisambiguate.disambiguate_nterm None status [] [] []
 500                    ("",0,NotationPt.Ident (name,None)) in
 501                  assert (metasenv = [] && subst = []);
 502                  let status, nuris =
 503                    NCicCoercDeclaration.
 504                      basic_eval_and_record_ncoercion_from_t_cpos_arity
 505                       status (name,t,cpos,arity)
 506                  in
 507                  let uris = concat_nuris nuris uris in
 508                  status, uris
 509                with MultiPassDisambiguator.DisambiguationError _->
 510                  HLog.warn ("error in generating coercion: "^name);
 511                  status, uris)
 512              (status,uris) coercions
 513            in
 514             status,uris
 515           with
 516            exn ->
 517             NCicLibrary.time_travel old_status;
 518             raise exn)
 519   | GrafiteAst.NCopy (log,tgt,src_uri, map) ->
 520      if status#ng_mode <> `CommandMode then
 521       raise (GrafiteTypes.Command_error "Not in command mode")
 522      else
 523        let tgt_uri_ext, old_ok =
 524          match NCicEnvironment.get_checked_obj src_uri with
 525          | _,_,[],[], (NCic.Inductive _ as ok) -> ".ind", ok
 526          | _,_,[],[], (NCic.Fixpoint _ as ok) -> ".con", ok
 527          | _,_,[],[], (NCic.Constant _ as ok) -> ".con", ok
 528          | _ -> assert false
 529        in
 530        let tgt_uri = NUri.uri_of_string (status#baseuri^"/"^tgt^tgt_uri_ext) in
 531        let map = (src_uri, tgt_uri) :: map in
 532        let ok =
 533          let rec subst () = function
 534            | NCic.Meta _ -> assert false
 535            | NCic.Const (NReference.Ref (u,spec)) as t ->
 536                (try NCic.Const
 537                  (NReference.reference_of_spec (List.assoc u map)spec)
 538                with Not_found -> t)
 539            | t -> NCicUtils.map (fun _ _ -> ()) () subst t
 540          in
 541          NCicUntrusted.map_obj_kind ~skip_body:false (subst ()) old_ok
 542        in
 543        let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
 544        let status = status#set_obj (tgt_uri,0,[],[],ok) in
 545        (*prerr_endline (NCicPp.ppobj (tgt_uri,0,[],[],ok));*)
 546        let status = status#set_stack ninitial_stack in
 547        let status = subst_metasenv_and_fix_names status in
 548        let status = status#set_ng_mode `ProofMode in
 549        eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
 550   | GrafiteAst.NObj (loc,obj) ->
 551      if status#ng_mode <> `CommandMode then
 552       raise (GrafiteTypes.Command_error "Not in command mode")
 553      else
 554       let status,obj =
 555        GrafiteDisambiguate.disambiguate_nobj status
 556         ~baseuri:status#baseuri (text,prefix_len,obj) in
 557       let uri,height,nmenv,nsubst,nobj = obj in
 558       let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
 559       let status = status#set_obj obj in
 560       let status = status#set_stack ninitial_stack in
 561       let status = subst_metasenv_and_fix_names status in
 562       let status = status#set_ng_mode `ProofMode in
 563       (match nmenv with
 564           [] ->
 565            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
 566         | _ -> status,`New [])
 567   | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) ->
 568       if status#ng_mode <> `CommandMode then
 569         raise (GrafiteTypes.Command_error "Not in command mode")
 570       else
 571         let status = status#set_ng_mode `ProofMode in
 572         let metasenv,subst,status,indty =
 573           GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in
 574         let indtyno, (_,_,tys,_,_) = match indty with
 575             NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) ->
 576               indtyno, NCicEnvironment.get_checked_indtys r
 577           | _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in
 578         let it = List.nth tys indtyno in
 579         let status,obj =  NDestructTac.mk_discriminator it status in
 580         let _,_,menv,_,_ = obj in
 581           (match menv with
 582                [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
 583              | _ -> prerr_endline ("Discriminator: non empty metasenv");
 584                     status, `New []) *)
 585   | GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
 586      if status#ng_mode <> `CommandMode then
 587       raise (GrafiteTypes.Command_error "Not in command mode")
 588      else
 589       let metasenv,subst,status,sort = match sort with
 590         | None -> [],[],status,NCic.Sort NCic.Prop
 591         | Some s -> GrafiteDisambiguate.disambiguate_nterm None status [] [] []
 592                       (text,prefix_len,s)
 593       in
 594       assert (metasenv = []);
 595       let sort = NCicReduction.whd ~subst [] sort in
 596       let sort = match sort with
 597           NCic.Sort s -> s
 598         | _ ->  raise (Invalid_argument (Printf.sprintf "ninverter: found target %s, which is not a sort"
 599                                            (NCicPp.ppterm ~metasenv ~subst ~context:[] sort)))
 600       in
 601       let status = status#set_ng_mode `ProofMode in
 602       let metasenv,subst,status,indty =
 603        GrafiteDisambiguate.disambiguate_nterm None status [] [] subst (text,prefix_len,indty) in
 604       let indtyno,(_,leftno,tys,_,_) = match indty with
 605           NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) ->
 606             indtyno, NCicEnvironment.get_checked_indtys r
 607         | _ -> prerr_endline ("engine: indty ="  ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] indty) ; assert false in
 608       let it = List.nth tys indtyno in
 609      let status,obj = NInversion.mk_inverter name true it leftno ?selection sort
 610                         status status#baseuri in
 611      let _,_,menv,_,_ = obj in
 612      (match menv with
 613         [] ->
 614           eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
 615       | _ -> assert false)
 616   | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
 617       eval_add_constraint status [`Type,u1] [`Type,u2]
 618 ;;
 619
 620 let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 621 (text,prefix_len,cmd) ->
 622  let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
 623  let status,uris =
 624   match cmd with
 625   | GrafiteAst.Include (loc, baseuri) ->
 626      let status =
 627       let moopath_rw, moopath_r =
 628        LibraryMisc.obj_file_of_baseuri
 629          ~must_exist:false ~baseuri ~writable:true,
 630        LibraryMisc.obj_file_of_baseuri
 631          ~must_exist:false ~baseuri ~writable:false in
 632       let moopath =
 633        if Sys.file_exists moopath_r then moopath_r else
 634          if Sys.file_exists moopath_rw then moopath_rw else
 635            raise (IncludedFileNotCompiled (moopath_rw,baseuri))
 636       in
 637        eval_from_moo.efm_go status moopath
 638      in
 639       let status =
 640        NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
 641         status in
 642       let status =
 643        GrafiteTypes.add_moo_content
 644         [GrafiteAst.Include (loc,baseuri)] status
 645       in
 646        status,`New []
 647   | GrafiteAst.Print (_,_) -> status,`New []
 648   | GrafiteAst.Set (loc, name, value) -> status, `New []
 649  in
 650   status,uris
 651
 652 } and eval_executable = {ee_go = fun ~disambiguate_command
 653  opts status (text,prefix_len,ex) ->
 654   match ex with
 655   | GrafiteAst.NTactic (_(*loc*), tacl) ->
 656       if status#ng_mode <> `ProofMode then
 657        raise (GrafiteTypes.Command_error "Not in proof mode")
 658       else
 659        let status =
 660         List.fold_left
 661           (fun status tac ->
 662             let status = eval_ng_tac (text,prefix_len,tac) status in
 663             subst_metasenv_and_fix_names status)
 664           status tacl
 665        in
 666         status,`New []
 667   | GrafiteAst.Command (_, cmd) ->
 668       eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd)
 669   | GrafiteAst.NCommand (_, cmd) ->
 670       eval_ncommand opts status (text,prefix_len,cmd)
 671   | GrafiteAst.NMacro (loc, macro) ->
 672      raise (NMacro (loc,macro))
 673
 674 } and eval_from_moo = {efm_go = fun status fname ->
 675   let ast_of_cmd cmd =
 676     ("",0,GrafiteAst.Executable (HExtlib.dummy_floc,
 677       GrafiteAst.Command (HExtlib.dummy_floc,
 678         cmd)))
 679   in
 680   let moo = GrafiteMarshal.load_moo fname in
 681   List.fold_left
 682     (fun status ast ->
 683       let ast = ast_of_cmd ast in
 684       let status,lemmas =
 685        eval_ast.ea_go
 686          ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd)
 687          status ast
 688       in
 689        assert (lemmas=`New []);
 690        status)
 691     status moo
 692 } and eval_ast = {ea_go = fun ~disambiguate_command
 693 ?(do_heavy_checks=false) status
 694 (text,prefix_len,st)
 695 ->
 696   let opts = { do_heavy_checks = do_heavy_checks ; } in
 697   match st with
 698   | GrafiteAst.Executable (_,ex) ->
 699      eval_executable.ee_go ~disambiguate_command
 700       opts status (text,prefix_len,ex)
 701   | GrafiteAst.Comment (_,c) ->
 702       eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c)
 703 } and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) ->
 704     status, `New []
 705 }
 706 ;;
 707
 708
 709 let eval_ast = eval_ast.ea_go