From 54e3c9f41b51d6e2a395252b45875532c40a0595 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 19 Dec 2008 10:05:31 +0000
Subject: [PATCH] added 'unification hint command to add a term to the new
 unification hint database'

---
 .../METAS/meta.helm-grafite_engine.src        |  2 +-
 .../software/components/grafite/grafiteAst.ml |  3 +-
 .../components/grafite/grafiteAstPp.ml        |  2 ++
 .../grafite_engine/grafiteEngine.ml           | 29 ++++++++++++++++---
 4 files changed, 30 insertions(+), 6 deletions(-)

diff --git a/helm/software/components/METAS/meta.helm-grafite_engine.src b/helm/software/components/METAS/meta.helm-grafite_engine.src
index c7203724c..bcd72841e 100644
--- a/helm/software/components/METAS/meta.helm-grafite_engine.src
+++ b/helm/software/components/METAS/meta.helm-grafite_engine.src
@@ -1,4 +1,4 @@
-requires="helm-library helm-grafite helm-tactics"
+requires="helm-library helm-grafite helm-tactics helm-ng_refiner"
 version="0.0.1"
 archive(byte)="grafite_engine.cma"
 archive(native)="grafite_engine.cmxa"
diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index c700c836b..c861a1a45 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -150,12 +150,13 @@ type ('term,'lazy_term) macro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 13
+let magic = 14
 
 type ('term,'obj) command =
   | Index of loc * 'term option (* key *) * UriManager.uri (* value *)
   | Coercion of loc * 'term * bool (* add_obj *) *
      int (* arity *) * int (* saturations *)
+  | UnificationHint of (loc * 'term)
   | Default of loc * string * UriManager.uri list
   | Drop of loc
   | Include of loc * string
diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 9d8d41537..0399e4ca3 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -313,6 +313,8 @@ let pp_command ~term_pp ~obj_pp = function
   | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
   | Coercion (_, t, do_composites, i, j) ->
      pp_coercion ~term_pp t do_composites i j
+  | UnificationHint (_,t) -> 
+      "unification hint " ^ term_pp t
   | Default (_,what,uris) -> pp_default what uris
   | Drop _ -> "drop"
   | Include (_,path) -> "include \"" ^ path ^ "\""
diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index f58f4303c..7cf3897fa 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:
@@ -482,7 +492,13 @@ let refinement_toolkit = {
   RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv; 
   RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
  }
-  
+ 
+let eval_unification_hint status t = 
+  (* XXX no undo *)        
+  NCicUnifHint.add_user_provided_hint t;
+  status,[]
+;;
+
 let eval_coercion status ~add_composites uri arity saturations =
  let uri = 
    try CicUtil.uri_of_term uri 
@@ -554,8 +570,6 @@ 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 =
@@ -656,6 +670,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       status,[] 
   | 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.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,[]
@@ -853,7 +869,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
-- 
2.39.2