+let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern) status =
+ let status =
+ Interpretations.add_interpretation status dsc (symbol, args) cic_appl_pattern
+ in
+ let mode = GrafiteAst.WithPreferences (*assert false*) in (* VEDI SOTTO *)
+ let diff =
+ [DisambiguateTypes.Symbol (symbol, 0), GrafiteAst.Symbol_alias (symbol,0,dsc)]
+ in
+ LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff
+;;
+
+let inject_interpretation =
+ let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
+ ~refresh_uri_in_universe ~refresh_uri_in_term
+ =
+ let rec refresh =
+ function
+ NotationPt.NRefPattern (NReference.Ref (uri,spec)) ->
+ NotationPt.NRefPattern
+ (NReference.reference_of_spec (NCicLibrary.refresh_uri uri) spec)
+ | NotationPt.VarPattern _
+ | NotationPt.ImplicitPattern as x -> x
+ | NotationPt.ApplPattern l -> NotationPt.ApplPattern (List.map refresh l)
+ in
+ let cic_appl_pattern = refresh cic_appl_pattern in
+ basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
+ in
+ GrafiteTypes.Serializer.register#run "interpretation"
+ basic_eval_interpretation
+;;
+
+let eval_interpretation status data=
+ let status = basic_eval_interpretation data status in
+ let dump = inject_interpretation data::status#dump in
+ status#set_dump dump
+;;
+
+