X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=9b454f29429647d6a4bb6202ae6e4a6b7357d382;hb=5c8de084e314e41f3dc2f605f6242283e930b803;hp=037a36f38ca164790ba9b5af23f75c88c752d841;hpb=df753672ee6c511b6ce721c2124e3294d0a28dbd;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 037a36f38..9b454f294 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -471,8 +471,16 @@ let coercion_moo_statement_of (uri,arity, saturations,_) =
    (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
 
 let eval_unification_hint status t n = 
-  (* XXX no undo *)        
-  NCicUnifHint.add_user_provided_hint t n;
+ let aux status =
+  let hstatus =
+   NCicUnifHint.add_user_provided_hint (status.NRstatus.uhint_db) t n
+  in
+   { status with NRstatus.uhint_db = hstatus } in
+ let rstatus = aux (GrafiteTypes.get_rstatus status) in
+ let status = GrafiteTypes.set_rstatus rstatus status in
+ let dump = GrafiteTypes.get_dump status in
+ let dump = fun status -> aux (dump status) in
+ let status = GrafiteTypes.set_dump dump status in
   status,`Old []
 ;;
 
@@ -583,13 +591,6 @@ let eval_ng_punct (_text, _prefix_len, punct) =
   | GrafiteAst.Merge _ -> NTactics.merge_tac 
 ;;
 
-let eval_ng_non_punct (_text, _prefix_len, punct) =
-  match punct with
-  | GrafiteAst.Focus (_,l) -> NTactics.focus_tac l
-  | GrafiteAst.Unfocus _ -> NTactics.unfocus_tac
-  | GrafiteAst.Skip _ -> NTactics.skip_tac
-;;
-
 let eval_ng_tac (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
@@ -604,6 +605,10 @@ let eval_ng_tac (text, prefix_len, tac) =
            ) hyps,
           (text,prefix_len,concl))
        ) seqs)
+  | GrafiteAst.NAuto (_loc, (l,a)) ->
+      NTactics.auto_tac
+	~params:(List.map (fun x -> "",0,x) l,a)
+  | GrafiteAst.NBranch _ -> NTactics.branch_tac 
   | GrafiteAst.NCases (_loc, what, where) ->
       NTactics.cases_tac 
         ~what:(text,prefix_len,what)
@@ -612,10 +617,12 @@ let eval_ng_tac (text, prefix_len, tac) =
   | GrafiteAst.NChange (_loc, pat, ww) -> 
       NTactics.change_tac 
        ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) 
+  | GrafiteAst.NDot _ -> NTactics.dot_tac 
   | GrafiteAst.NElim (_loc, what, where) ->
       NTactics.elim_tac 
         ~what:(text,prefix_len,what)
         ~where:(text,prefix_len,where)
+  | GrafiteAst.NFocus (_,l) -> NTactics.focus_tac l
   | GrafiteAst.NGeneralize (_loc, where) -> 
       NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
@@ -623,11 +630,29 @@ let eval_ng_tac (text, prefix_len, tac) =
   | GrafiteAst.NLetIn (_loc,where,what,name) ->
       NTactics.letin_tac ~where:(text,prefix_len,where) 
         ~what:(text,prefix_len,what) name
+  | GrafiteAst.NMerge _ -> NTactics.merge_tac 
+  | GrafiteAst.NPos (_,l) -> NTactics.pos_tac l
   | GrafiteAst.NReduce (_loc, reduction, where) ->
       NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where)
   | GrafiteAst.NRewrite (_loc,dir,what,where) ->
      NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
       ~where:(text,prefix_len,where)
+  | GrafiteAst.NSemicolon _ -> fun x -> x
+  | GrafiteAst.NShift _ -> NTactics.shift_tac 
+  | GrafiteAst.NSkip _ -> NTactics.skip_tac
+  | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
+  | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac 
+;;
+      
+let subst_metasenv_and_fix_names s =
+  let u,h,metasenv, subst,o = s.NTacStatus.istatus.NTacStatus.pstatus in
+  let o = 
+    NCicUntrusted.map_obj_kind ~skip_body:true 
+     (NCicUntrusted.apply_subst subst []) o
+  in
+  { s with NTacStatus.istatus =
+     { s.NTacStatus.istatus with NTacStatus.pstatus =
+        u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o}}
 ;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status
@@ -696,7 +721,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,`Old []
   | GrafiteAst.Drop loc -> raise Drop
-  | GrafiteAst.Include (loc, baseuri) ->
+  | GrafiteAst.Include (loc, _, baseuri) ->
      let moopath_rw, moopath_r = 
        LibraryMisc.obj_file_of_baseuri 
          ~must_exist:false ~baseuri ~writable:true,
@@ -709,6 +734,10 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
            raise (IncludedFileNotCompiled (moopath_rw,baseuri))
      in
      let status = eval_from_moo.efm_go status moopath in
+     let rstatus = GrafiteTypes.get_rstatus status in
+     let rstatus =
+      NCicLibrary.require ~baseuri:(NUri.uri_of_string baseuri) rstatus in
+     let status = GrafiteTypes.set_rstatus rstatus status in
 (* debug
      let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in
      let nat_uri = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in
@@ -749,40 +778,39 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       let name = UriManager.name_of_uri uri in
       let obj = Cic.Constant (name,Some (Lazy.force bo),ty,[],attrs) in
       let status, lemmas = add_obj uri obj status in
-       {status with 
-	  GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+       {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
         (*CSC: I throw away the arities *)
         `Old (uri::lemmas)
   | GrafiteAst.NQed loc ->
       (match status.GrafiteTypes.ng_status with
        | GrafiteTypes.ProofMode
           { NTacStatus.istatus =
-             {NTacStatus.pstatus = pstatus; lstatus=lexicon_status} } ->
-            let uri,height,menv,subst,obj = pstatus in
+             { NTacStatus.pstatus = pstatus; estatus = estatus } } ->
+            let uri,height,menv,subst,obj_kind = pstatus in
              if menv <> [] then
               raise
                (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
              else
-              let obj =
-prerr_endline "CSC: here we should fix the height!!!";
-               (uri,height,[],[],
-                NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst)
-                 obj) in
-              NCicTypeChecker.typecheck_obj obj;
-              NCicLibrary.add_obj uri obj;
-              let objs = NCicElim.mk_elims obj in
-              let uris =
-               uri::
-                List.map
-                 (fun (uri,_,_,_,_) as obj ->
-                   NCicTypeChecker.typecheck_obj obj;
-                   NCicLibrary.add_obj uri obj;
-                   uri
-                 ) objs
-              in
-               {status with 
-                 GrafiteTypes.ng_status = 
-                  GrafiteTypes.CommandMode lexicon_status },`New uris
+              let obj_kind =
+               NCicUntrusted.map_obj_kind 
+                (NCicUntrusted.apply_subst subst []) obj_kind in
+              let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
+              let obj = uri,height,[],[],obj_kind in
+               NCicTypeChecker.typecheck_obj obj;
+               let timestamp = NCicLibrary.add_obj uri obj in
+               let objs = NCicElim.mk_elims obj in
+               let timestamp,uris_rev =
+                 List.fold_left
+                  (fun (timestamp,uris_rev) (uri,_,_,_,_) as obj ->
+                    NCicTypeChecker.typecheck_obj obj;
+                    let timestamp = NCicLibrary.add_obj uri obj in
+                     timestamp,uri::uris_rev
+                  ) (timestamp,[]) objs in
+               let uris = uri::List.rev uris_rev in
+                GrafiteTypes.set_library_db timestamp
+                 {status with 
+                  GrafiteTypes.ng_status = 
+                   GrafiteTypes.CommandMode estatus },`New uris
        | _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
   | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> 
      Setoids.add_relation id a aeq refl sym trans;
@@ -793,12 +821,13 @@ prerr_endline "CSC: here we should fix the height!!!";
       NCicEnvironment.add_constraint strict [false,u1] [false,u2];
       status, `New [u1;u2]
   | GrafiteAst.NObj (loc,obj) ->
-     let lexicon_status =
+     let estatus =
        match status.GrafiteTypes.ng_status with
        | GrafiteTypes.ProofMode _ -> assert false
-       | GrafiteTypes.CommandMode ls -> ls in
-     let lexicon_status,obj =
-      GrafiteDisambiguate.disambiguate_nobj lexicon_status
+       | GrafiteTypes.CommandMode es -> es 
+     in
+     let estatus,obj =
+      GrafiteDisambiguate.disambiguate_nobj estatus
        ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in
      let uri,height,nmenv,nsubst,nobj = obj in
      let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
@@ -806,9 +835,10 @@ prerr_endline "CSC: here we should fix the height!!!";
       { status with
          GrafiteTypes.ng_status = 
           GrafiteTypes.ProofMode
-           { NTacStatus.gstatus = ninitial_stack; 
-             istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}
-           }
+           (subst_metasenv_and_fix_names
+            { NTacStatus.gstatus = ninitial_stack; 
+             istatus = { NTacStatus.pstatus = obj; estatus = estatus}})
+             }
      in
      (match nmenv with
          [] ->
@@ -904,12 +934,17 @@ prerr_endline "CSC: here we should fix the height!!!";
   | GrafiteAst.Tactic (_, None, punct) ->
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
-  | GrafiteAst.NTactic (_(*loc*), tac, punct) ->
+  | GrafiteAst.NTactic (_(*loc*), tacl) ->
       (match status.GrafiteTypes.ng_status with
       | GrafiteTypes.CommandMode _ -> assert false
       | GrafiteTypes.ProofMode nstatus ->
-         let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
-         let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
+         let nstatus =
+          List.fold_left 
+            (fun nstatus tac ->
+              let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
+              subst_metasenv_and_fix_names nstatus)
+            nstatus tacl
+         in
          NTacStatus.pp_tac_status nstatus;
          { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
          `New [])
@@ -920,15 +955,6 @@ prerr_endline "CSC: here we should fix the height!!!";
      in
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
-  | GrafiteAst.NNonPunctuationTactical (_, non_punct, punct) ->
-     (match status.GrafiteTypes.ng_status with
-     | GrafiteTypes.CommandMode _ -> assert false
-     | GrafiteTypes.ProofMode nstatus ->
-        let nstatus = eval_ng_non_punct (text,prefix_len,non_punct) nstatus in
-        let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
-        NTacStatus.pp_tac_status nstatus;
-        { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
-        `New [])
   | GrafiteAst.Command (_, cmd) ->
       eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd)
   | GrafiteAst.Macro (loc, macro) ->