- Grammar for all obj commands ported to NG (let recs and inductives still need

[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 1f32e8c9e2db06944bf86b6e4ca8938940093fca..ebba1988dab1a22ab3f9069d9321b807dcd0d526 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -649,10 +649,35 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 *)
       let status = GrafiteTypes.add_moo_content [cmd] status in
       status,[] 
+  | GrafiteAst.Select (_,uri) as cmd ->
+      if List.mem cmd status.GrafiteTypes.moo_content_rev then status, []
+      else 
+       let cache = 
+         AutomationCache.add_term_to_active status.GrafiteTypes.automation_cache
+           [] [] [] (CicUtil.term_of_uri uri) None
+       in
+       let status = { status with GrafiteTypes.automation_cache = cache } in
+       let status = GrafiteTypes.add_moo_content [cmd] status in
+       status, []
+  | GrafiteAst.Pump (_,steps) ->
+      let cache = 
+        AutomationCache.pump status.GrafiteTypes.automation_cache steps
+      in
+      let status = { status with GrafiteTypes.automation_cache = cache } in
+      status, []
   | GrafiteAst.PreferCoercion (loc, coercion) ->
      eval_prefer_coercion status coercion
   | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
      eval_coercion status ~add_composites uri arity saturations 
+  | GrafiteAst.Inverter (loc, name, indty, params) ->
+     let buri = GrafiteTypes.get_baseuri status in 
+     let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in
+     let indty_uri = 
+       try CicUtil.uri_of_term indty
+       with Invalid_argument _ ->
+         raise (Invalid_argument "not an inductive type to invert")
+     in
+     Inversion_principle.build_inverter ~add_obj status uri indty_uri params
   | GrafiteAst.UnificationHint (loc, t, n) ->
      eval_unification_hint status t n
   | GrafiteAst.Default (loc, what, uris) as cmd ->
@@ -716,43 +741,57 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
          GrafiteTypes.proof_status = GrafiteTypes.No_proof},
         (*CSC: I throw away the arities *)
         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
+             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
+               NCicLibrary.add_obj uri obj;
+               {status with 
+                 GrafiteTypes.ng_status = 
+                  GrafiteTypes.CommandMode lexicon_status },[]
+       | _ -> 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, [] (*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 =
+     let lexicon_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} }   
-     },
-      []
+       | GrafiteTypes.CommandMode ls -> ls in
+     let lexicon_status,obj =
+      GrafiteDisambiguate.disambiguate_nobj lexicon_status
+       ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in
+     let uri,height,nmenv,nsubst,nobj = obj 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 },[]
+      | _ ->
+        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}}
+             },[])
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with