X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=d4738a5515d73cb9cabc3b9a948869d1ef6dd4a8;hb=9e7df95a820cb91d075f1a20d703175da874596c;hp=6b341f77c314a581e130e7e9e7f55ad712821334;hpb=7233348f05485c2ee317df9c3407cf1ce7e56927;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 6b341f77c..d4738a551 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -336,14 +336,14 @@ let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) =
  let after = ProofEngineTypes.goals_of_proof proof in
  let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
  let proof, opened_goals = 
-  let uri, metasenv_after_tactic, _subst, t, ty, attrs = proof in
+  let uri, metasenv_after_tactic, subst, t, ty, attrs = proof in
   let reordered_metasenv, opened_goals = 
     reorder_metasenv
      starting_metasenv
      metasenv_after_refinement metasenv_after_tactic
      opened goal always_opens_a_goal
   in
-  let proof' = uri, reordered_metasenv, _subst, t, ty, attrs in
+  let proof' = uri, reordered_metasenv, [], t, ty, attrs in
   proof', opened_goals
  in
  let incomplete_proof =
@@ -583,6 +583,13 @@ 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) 
@@ -609,8 +616,6 @@ let eval_ng_tac (text, prefix_len, tac) =
       NTactics.elim_tac 
         ~what:(text,prefix_len,what)
         ~where:(text,prefix_len,where)
-  | GrafiteAst.NEval (_loc, where, reduction) ->
-      NTactics.eval_tac ~reduction ~where:(text,prefix_len,where)
   | GrafiteAst.NGeneralize (_loc, where) -> 
       NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
@@ -618,10 +623,23 @@ 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.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)
 ;;
+      
+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
 (text,prefix_len,cmd) ->
@@ -689,7 +707,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,
@@ -742,8 +760,7 @@ 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 ->
@@ -751,25 +768,40 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
        | GrafiteTypes.ProofMode
           { NTacStatus.istatus =
              {NTacStatus.pstatus = pstatus; lstatus=lexicon_status} } ->
-            let uri,height,menv,subst,obj = pstatus in
+            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,[],[],NTacStatus.apply_subst_obj subst obj
-              in
+              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;
                NCicLibrary.add_obj uri obj;
-               {status with 
+               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 },`Old []
+                  GrafiteTypes.CommandMode lexicon_status },`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;
      status, `Old [] (*CSC: TO BE FIXED *)
   | GrafiteAst.Set (loc, name, value) -> status, `Old []
 (*       GrafiteTypes.set_option status name value,[] *)
+  | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) ->
+      NCicEnvironment.add_constraint strict [false,u1] [false,u2];
+      status, `New [u1;u2]
   | GrafiteAst.NObj (loc,obj) ->
      let lexicon_status =
        match status.GrafiteTypes.ng_status with
@@ -779,25 +811,21 @@ prerr_endline "CSC: here we should fix the height!!!";
       GrafiteDisambiguate.disambiguate_nobj lexicon_status
        ~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
+     let status =
+      { status with
+         GrafiteTypes.ng_status = 
+          GrafiteTypes.ProofMode
+           (subst_metasenv_and_fix_names
+            { NTacStatus.gstatus = ninitial_stack; 
+             istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}})
+             }
+     in
      (match nmenv with
-        [] ->
-          (* CSC: cut&paste code from NQed *)
-          let obj =
-prerr_endline "CSC: here we should fix the height!!!";
-           uri,height,[],[],NTacStatus.apply_subst_obj nsubst nobj
-          in
-           NCicLibrary.add_obj uri obj;
-           {status with 
-             GrafiteTypes.ng_status=GrafiteTypes.CommandMode lexicon_status },
-           `Old []
-      | _ ->
-        let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
-        { status with
-           GrafiteTypes.ng_status = 
-            GrafiteTypes.ProofMode
-             { NTacStatus.gstatus = ninitial_stack; 
-               istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}
-             },`Old [])
+         [] ->
+          eval_command.ec_go ~disambiguate_command opts status
+           ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+       | _ -> status,`New [])
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with
@@ -888,13 +916,15 @@ prerr_endline "CSC: here we should fix the height!!!";
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
   | GrafiteAst.NTactic (_(*loc*), tac, punct) ->
-      (match  status.GrafiteTypes.ng_status with
+      (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 = subst_metasenv_and_fix_names 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 }, `Old [])
+         { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
+         `New [])
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status = 
       eval_tactical status
@@ -902,6 +932,15 @@ 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) ->