tactic cases works! delift clears tags

[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 c6bebbc397e00cf5dfad8a7645e5fbb3078ff670..af8b086bfb58a256999d28a49fbe34cc72990f44 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -470,9 +470,9 @@ let coercion_moo_statement_of (uri,arity, saturations,_) =
   GrafiteAst.Coercion
    (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
 
-let eval_unification_hint status t = 
+let eval_unification_hint status t n = 
   (* XXX no undo *)        
-  NCicUnifHint.add_user_provided_hint t;
+  NCicUnifHint.add_user_provided_hint t n;
   status,[]
 ;;
 
@@ -571,7 +571,37 @@ let eval_tactical status tac =
   status
 
 let add_obj = GrafiteSync.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj
-      
+
+let eval_ng_punct (_text, _prefix_len, punct) =
+  match punct with
+  | GrafiteAst.Dot _ -> NTactics.dot_tac 
+  | GrafiteAst.Semicolon _ -> fun x -> x
+  | GrafiteAst.Branch _ -> NTactics.branch_tac 
+  | GrafiteAst.Shift _ -> NTactics.shift_tac 
+  | GrafiteAst.Pos (_,l) -> NTactics.pos_tac l
+  | GrafiteAst.Wildcard _ -> NTactics.wildcard_tac 
+  | GrafiteAst.Merge _ -> NTactics.merge_tac 
+;;
+
+let eval_ng_tac (text, prefix_len, tac) =
+  match tac with
+  | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
+  | GrafiteAst.NCases (_loc, what, where) ->
+      NTactics.cases_tac 
+        ~what:(text,prefix_len,what)
+        ~where:(text,prefix_len,where)
+  | GrafiteAst.NCase1 (_loc,n) -> NTactics.case1_tac n
+  | GrafiteAst.NChange (_loc, pat, ww) -> 
+      NTactics.change_tac 
+       ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) 
+  | GrafiteAst.NElim (_loc, what, where) ->
+      NTactics.elim_tac 
+        ~what:(text,prefix_len,what)
+        ~where:(text,prefix_len,where)
+  | GrafiteAst.NId _ -> (fun x -> x)
+  | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+;;
+
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 (text,prefix_len,cmd) ->
  let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
@@ -597,8 +627,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      eval_prefer_coercion status coercion
   | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
      eval_coercion status ~add_composites uri arity saturations 
-  | GrafiteAst.UnificationHint (loc, t) ->
-     eval_unification_hint status t
+  | GrafiteAst.UnificationHint (loc, t, n) ->
+     eval_unification_hint status t n
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,[]
@@ -665,6 +695,38 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      status, [] (*CSC: TO BE FIXED *)
   | GrafiteAst.Set (loc, name, value) -> status, []
 (*       GrafiteTypes.set_option status name value,[] *)
+  | GrafiteAst.NObj (loc,obj) ->
+     let ty, name = 
+       match obj with
+       | CicNotationPt.Theorem (_,name,ty,_) -> ty, name
+       | _ -> assert false
+     in
+     let suri = "cic:/ng_matita/" ^ name ^ ".def" in
+     let nlexicon_status =
+       match status.GrafiteTypes.ng_status with
+       | GrafiteTypes.ProofMode _ -> assert false
+       | GrafiteTypes.CommandMode ls -> ls
+     in
+     let nmenv, nsubst, nlexicon_status, nty = 
+       GrafiteDisambiguate.disambiguate_nterm None
+       nlexicon_status [] [] [] (text,prefix_len,ty)
+     in
+     let nmenv, nsubst, nlexicon_status, nbo = 
+       GrafiteDisambiguate.disambiguate_nterm (Some nty)
+       nlexicon_status [] nmenv nsubst ("",0,CicNotationPt.Implicit)
+     in
+     let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
+     prerr_endline ("nuovo lemma: " ^ NCicPp.ppmetasenv ~subst:nsubst nmenv);
+     { status with
+        GrafiteTypes.ng_status = 
+           GrafiteTypes.ProofMode { NTacStatus.gstatus = ninitial_stack; 
+          istatus = { 
+            NTacStatus.pstatus = 
+             NUri.uri_of_string suri, 0, nmenv, nsubst, 
+              (NCic.Constant ([],"",Some nbo,nty,(`Provided,`Definition,`Regular)));
+            lstatus = nlexicon_status} }   
+     },
+      []
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with
@@ -716,7 +778,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
          let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
          { status with GrafiteTypes.proof_status =
             GrafiteTypes.Incomplete_proof
-             { GrafiteTypes.proof = initial_proof; stack = initial_stack } },
+            { GrafiteTypes.proof = initial_proof; stack = initial_stack } ;
+         },
           []
      | _ ->
          if metasenv <> [] then
@@ -755,6 +818,14 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
   | GrafiteAst.Tactic (_, None, punct) ->
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
+  | GrafiteAst.NTactic (_(*loc*), tac, punct) ->
+      (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
+         NTacStatus.pp_tac_status nstatus;
+         { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, [])
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status = 
       eval_tactical status