X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=2099bf06a8ed10987547cc8b7afa4ddddcc49cd3;hb=b2a9b21233b1b7c645175e26fc3f3ab03a308c08;hp=f58f4303c2ada346206ac1fb31c77312581be168;hpb=987627a48b2a3c2345d1af2c2a6b1ab78aa90b58;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index f58f4303c..2099bf06a 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -427,6 +427,16 @@ type 'a eval_command =
    GrafiteTypes.status * UriManager.uri list
  }
 
+type 'a eval_comment =
+ {ecm_go: 'term 'lazy_term 'reduction_kind 'obj 'ident.
+  disambiguate_command:
+   (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input ->
+    GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> 
+  options -> GrafiteTypes.status -> 
+    (('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input ->
+   GrafiteTypes.status * UriManager.uri list
+ }
+
 type 'a eval_executable =
  {ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
   disambiguate_tactic:
@@ -460,45 +470,51 @@ let coercion_moo_statement_of (uri,arity, saturations,_) =
   GrafiteAst.Coercion
    (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
 
-let refinement_toolkit = {
-  RefinementTool.type_of_aux' = 
-    (fun ?localization_tbl e c t u ->
-      let saved = !CicRefine.insert_coercions in 
-      CicRefine.insert_coercions:= false;
-      let rc = 
-        try 
-          let t, ty, metasenv, ugraph = 
-            CicRefine.type_of_aux' ?localization_tbl e c t u in
-          RefinementTool.Success (t, ty, metasenv, ugraph)
-        with
-        | CicRefine.RefineFailure s
-        | CicRefine.Uncertain s 
-        | CicRefine.AssertFailure s -> RefinementTool.Exception s
-      in
-      CicRefine.insert_coercions := saved;
-      rc);
-  RefinementTool.ppsubst = CicMetaSubst.ppsubst;
-  RefinementTool.apply_subst = CicMetaSubst.apply_subst; 
-  RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv; 
-  RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
- }
-  
+let eval_unification_hint status t n = 
+  (* XXX no undo *)        
+  NCicUnifHint.add_user_provided_hint t n;
+  status,[]
+;;
+
+let add_coercions_of_lemmas lemmas status =
+  let moo_content = 
+    HExtlib.filter_map 
+      (fun uri ->
+        match CoercDb.is_a_coercion (Cic.Const (uri,[])) with
+        | None -> None
+        | Some (_,tgt,_,sat,_) ->
+            let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+            Some (coercion_moo_statement_of (uri,arity,sat,0)))
+      lemmas
+  in
+  let status = GrafiteTypes.add_moo_content moo_content status in 
+  {status with GrafiteTypes.coercions = CoercDb.dump () }, 
+  lemmas
+
 let eval_coercion status ~add_composites uri arity saturations =
  let uri = 
    try CicUtil.uri_of_term uri 
    with Invalid_argument _ -> 
      raise (Invalid_argument "coercion can only be constants/constructors")
  in
- let status,compounds =
-  GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity
-   saturations (GrafiteTypes.get_baseuri status)
- in
- let moo_content = 
-   List.map coercion_moo_statement_of ((uri,arity,saturations,0)::compounds)
+ let status, lemmas =
+  GrafiteSync.add_coercion ~add_composites 
+    ~pack_coercion_obj:CicRefine.pack_coercion_obj
+   status uri arity saturations (GrafiteTypes.get_baseuri status) in
+ let moo_content = coercion_moo_statement_of (uri,arity,saturations,0) in
+ let status = GrafiteTypes.add_moo_content [moo_content] status in 
+  add_coercions_of_lemmas lemmas status
+
+let eval_prefer_coercion status c =
+ let uri = 
+   try CicUtil.uri_of_term c 
+   with Invalid_argument _ -> 
+     raise (Invalid_argument "coercion can only be constants/constructors")
  in
- let status = GrafiteTypes.add_moo_content moo_content status in
-  {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
-   List.map (fun u,_,_,_ -> u) compounds
+ let status = GrafiteSync.prefer_coercion status uri in
+ let moo_content = GrafiteAst.PreferCoercion (HExtlib.dummy_floc,c) in
+ let status = GrafiteTypes.add_moo_content [moo_content] status in 
+ status, []  
 
 module MatitaStatus =
  struct
@@ -554,85 +570,45 @@ let eval_tactical status tac =
   in
   status
 
-let eval_comment status c = status
-
-(* since the record syntax allows to declare coercions, we have to put this
- * information inside the moo *)
-let add_coercions_of_record_to_moo obj lemmas status =
-  let attributes = CicUtil.attributes_of_obj obj in
-  let is_record x _ = match x with `Class (`Record att) -> Some att | _-> None in
-  match HExtlib.list_findopt is_record attributes with
-  | None -> status,[]
-  | Some fields -> 
-      let is_a_coercion uri =
-        try
-          let obj,_ = 
-            CicEnvironment.get_cooked_obj  CicUniv.oblivion_ugraph uri in
-          let attrs = CicUtil.attributes_of_obj obj in
-          try 
-            match List.find 
-             (function `Class (`Coercion _) -> true | _-> false) attrs
-            with `Class (`Coercion n) -> true,n | _ -> assert false
-          with Not_found -> false,0            
-        with Not_found -> assert false
-      in
-      let buri = GrafiteTypes.get_baseuri status in
-      (* looking at the fields we can know the 'wanted' coercions, but not the 
-       * actually generated ones. So, only the intersection between the wanted
-       * and the actual should be in the moo as coercion, while everithing in
-       * lemmas should go as aliases *)
-      let wanted_coercions = 
-        HExtlib.filter_map 
-          (function 
-            | (name,true,arity) -> 
-               Some 
-                 (arity, UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con" ))
-            | _ -> None) 
-          fields
-      in
-      (*prerr_endline "wanted coercions:";
-      List.iter 
-        (fun u -> prerr_endline (UriManager.string_of_uri u)) 
-        wanted_coercions; *)
-      let coercions, moo_content = 
-        List.split
-          (HExtlib.filter_map 
-            (fun uri ->
-              let is_a_wanted_coercion,arity_wanted = 
-                try
-                  let arity,_ = 
-                    List.find (fun (n,u) -> UriManager.eq u uri) 
-                      wanted_coercions
-                  in
-                  true, arity
-                with Not_found -> false, 0
-              in
-              let is_a_coercion, arity_coercion = is_a_coercion uri in
-              if is_a_coercion then
-                Some (uri, coercion_moo_statement_of (uri,arity_coercion,0,0))
-              else if is_a_wanted_coercion then
-                Some (uri, coercion_moo_statement_of (uri,arity_wanted,0,0))
-              else
-                None)
-            lemmas)
-      in
-      (*prerr_endline "actual coercions:";
-      List.iter 
-        (fun u -> prerr_endline (UriManager.string_of_uri u)) 
-        coercions; 
-      prerr_endline "lemmas was:";
-      List.iter 
-        (fun u -> prerr_endline (UriManager.string_of_uri u)) 
-        lemmas; *)
-      let status = GrafiteTypes.add_moo_content moo_content status in 
-      {status with 
-        GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions}, 
-      lemmas
+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.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)
+  | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+  | GrafiteAst.NRewrite (_loc,dir,what,where) ->
+     NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
+      ~where:(text,prefix_len,where)
+;;
 
-let add_obj uri obj status =
- let status,lemmas = GrafiteSync.add_obj refinement_toolkit uri obj status in
- status, lemmas 
-      
 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
@@ -654,8 +630,12 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 *)
       let status = GrafiteTypes.add_moo_content [cmd] status 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.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,[]
@@ -722,6 +702,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
@@ -773,7 +785,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
@@ -782,7 +795,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
             CicMetaSubst.ppmetasenv [] metasenv));
          let status, lemmas = add_obj uri obj status in 
          let status,new_lemmas =
-          add_coercions_of_record_to_moo obj lemmas status
+          add_coercions_of_lemmas lemmas status
          in
           {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
            uri::new_lemmas@lemmas
@@ -812,6 +825,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
@@ -853,7 +874,12 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
   | GrafiteAst.Executable (_,ex) ->
      eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command
       ~disambiguate_macro opts status (text,prefix_len,ex)
-  | GrafiteAst.Comment (_,c) -> eval_comment status (text,prefix_len,c),[]
+  | GrafiteAst.Comment (_,c) -> 
+      eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c) 
+} and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) -> 
+    status, []
 }
+;;
+
 
 let eval_ast = eval_ast.ea_go