-let coercion_moo_statement_of (uri,arity, saturations) =
- GrafiteAst.Coercion (HExtlib.dummy_floc, 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 coercion_moo_statement_of (uri,arity, saturations,_) =
+ GrafiteAst.Coercion
+ (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
+
+let basic_eval_unification_hint (t,n) status =
+ NCicUnifHint.add_user_provided_hint status t n
+;;
+
+let inject_unification_hint =
+ let basic_eval_unification_hint (t,n)
+ ~refresh_uri_in_universe
+ ~refresh_uri_in_term
+ =
+ let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
+ in
+ NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint
+;;
+
+let eval_unification_hint status t n =
+ let metasenv,subst,status,t =
+ GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,t) in
+ assert (metasenv=[]);
+ let t = NCicUntrusted.apply_subst subst [] t in
+ let status = basic_eval_unification_hint (t,n) status in
+ let dump = inject_unification_hint (t,n)::status#dump in
+ let status = status#set_dump dump in
+ status,`New []
+;;
+
+let basic_eval_ncoercion (name,t,s,d,p,a) status =
+ NCicCoercion.index_coercion status t s d a p
+;;
+
+let inject_ncoercion =
+ let basic_eval_ncoercion x ~refresh_uri_in_universe ~refresh_uri_in_term =
+ basic_eval_ncoercion x
+ in
+ NRstatus.Serializer.register "ncoercion" basic_eval_ncoercion
+;;
+
+let eval_ncoercion status name t ty (id,src) tgt =
+
+ let metasenv,subst,status,ty =
+ GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
+ assert (metasenv=[]);
+ let ty = NCicUntrusted.apply_subst subst [] ty in
+ let metasenv,subst,status,t =
+ GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
+ assert (metasenv=[]);
+ let t = NCicUntrusted.apply_subst subst [] t in
+
+ let src, cpos =
+ let rec aux cpos ctx = function
+ | NCic.Prod (name,ty,bo) ->
+ if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
+ else
+ let metasenv,subst,status,src =
+ GrafiteDisambiguate.disambiguate_nterm
+ None status [] [] [] ("",0,src) in
+ let src = NCicUntrusted.apply_subst subst [] src in
+ let _ = NCicUnification.unify status metasenv subst ctx ty src in
+ src, cpos
+ | _ -> assert false
+ in
+ aux 0 [] ty
+ in
+ let tgt, arity =
+ let metasenv,subst,status,tgt =
+ GrafiteDisambiguate.disambiguate_nterm
+ None status [] [] [] ("",0,tgt) in
+ let tgt = NCicUntrusted.apply_subst subst [] tgt in
+ (* CHECK *)
+ let rec count_prod = function
+ | NCic.Prod (_,_,x) -> 1 + count_prod x
+ | _ -> 0
+ in
+ tgt, count_prod tgt
+ in
+
+ let status = basic_eval_ncoercion (name,t,src,tgt,cpos,arity) status in
+ let dump = inject_ncoercion (name,t,src,tgt,cpos,arity)::status#dump in
+ let status = status#set_dump dump in
+ status,`New []
+;;
+
+let basic_eval_add_constraint (s,u1,u2) status =
+ NCicLibrary.add_constraint status s u1 u2
+;;
+
+let inject_constraint =
+ let basic_eval_add_constraint (s,u1,u2)
+ ~refresh_uri_in_universe
+ ~refresh_uri_in_term
+ =
+ let u1 = refresh_uri_in_universe u1 in
+ let u2 = refresh_uri_in_universe u2 in
+ basic_eval_add_constraint (s,u1,u2)
+ in
+ NRstatus.Serializer.register "constraints" basic_eval_add_constraint
+;;
+
+let eval_add_constraint status s u1 u2 =
+ let status = basic_eval_add_constraint (s,u1,u2) status in
+ let dump = inject_constraint (s,u1,u2)::status#dump in
+ let status = status#set_dump dump in
+ status,`Old []
+;;
+
+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#set_coercions (CoercDb.dump ()),
+ lemmas
+