=
let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
in
- NCicLibrary.Serializer.register
- "unification_hints" basic_eval_unification_hint
+ NCicLibrary.Serializer.register#run "unification_hints"
+ object(_ : 'a NCicLibrary.register_type)
+ method run = basic_eval_unification_hint
+ end
;;
let eval_unification_hint status t n =
status,`New []
;;
+let basic_index_obj l status =
+ status#set_auto_cache
+ (List.fold_left
+ (fun t (k,v) ->
+ NDiscriminationTree.DiscriminationTree.index t k v)
+ status#auto_cache l)
+;;
+
+let record_index_obj =
+ let aux l
+ ~refresh_uri_in_universe
+ ~refresh_uri_in_term
+ =
+ basic_index_obj
+ (List.map
+ (fun k,v -> refresh_uri_in_term k, refresh_uri_in_term v)
+ l)
+ in
+ NCicLibrary.Serializer.register#run "index_obj"
+ object(_ : 'a NCicLibrary.register_type)
+ method run = aux
+ end
+;;
+
+let index_obj_for_auto status (uri, height, _, _, kind) =
+ let data =
+ match kind with
+ | NCic.Fixpoint _ -> []
+ | NCic.Inductive _ -> []
+ | NCic.Constant (_,_,_, ty, _) ->
+ [ ty, NCic.Const(NReference.reference_of_spec
+ uri (NReference.Def height)) ]
+ in
+ let status = basic_index_obj data status in
+ let dump = record_index_obj data :: status#dump in
+ status#set_dump dump
+;;
+
+
let basic_eval_add_constraint (u1,u2) status =
NCicLibrary.add_constraint status u1 u2
;;
let u2 = refresh_uri_in_universe u2 in
basic_eval_add_constraint (u1,u2)
in
- NCicLibrary.Serializer.register "constraints" basic_eval_add_constraint
+ NCicLibrary.Serializer.register#run "constraints"
+ object(_:'a NCicLibrary.register_type)
+ method run = basic_eval_add_constraint
+ end
;;
let eval_add_constraint status u1 u2 =
status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
;;
+
let rec eval_ncommand opts status (text,prefix_len,cmd) =
match cmd with
| GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
let obj = uri,height,[],[],obj_kind in
let old_status = status in
let status = NCicLibrary.add_obj status obj in
+ let status = index_obj_for_auto status obj in
(* prerr_endline (NCicPp.ppobj obj); *)
HLog.message ("New object: " ^ NUri.string_of_uri uri);
(try