+let basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern) status =
+ let status =
+ if not alias_only then
+ Interpretations.add_interpretation status dsc (symbol, args) cic_appl_pattern
+ else
+ status
+ in
+ let mode = GrafiteAst.WithPreferences (*assert false*) in (* MATITA 1.0 VEDI SOTTO *)
+ let diff =
+ [DisambiguateTypes.Symbol (symbol, 0), GrafiteAst.Symbol_alias (symbol,0,dsc)]
+ in
+ GrafiteDisambiguate.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 ~refresh_uri_in_reference
+ ~alias_only
+ =
+ 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 ~alias_only (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 ~alias_only:false data status in
+ NCicLibrary.dump_obj status (inject_interpretation data)
+;;
+
+let basic_eval_alias (mode,diff) status =
+ GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
+;;
+
+let inject_alias =
+ let basic_eval_alias (mode,diff) ~refresh_uri_in_universe ~refresh_uri_in_term
+ ~refresh_uri_in_reference ~alias_only =
+ basic_eval_alias (mode,diff)
+ in
+ GrafiteTypes.Serializer.register#run "alias" basic_eval_alias
+;;
+
+let eval_alias status data=
+ let status = basic_eval_alias data status in
+ NCicLibrary.dump_obj status (inject_alias data)
+;;
+
+let basic_eval_input_notation (l1,l2) status =
+ GrafiteParser.extend status l1
+ (fun env loc ->
+ NotationPt.AttributedTerm
+ (`Loc loc,TermContentPres.instantiate_level2 status env l2))
+;;
+
+let inject_input_notation =
+ let basic_eval_input_notation (l1,l2)
+ ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~alias_only status
+ =
+ if not alias_only then
+ let l1 =
+ CicNotationParser.refresh_uri_in_checked_l1_pattern
+ ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
+ ~refresh_uri_in_reference l1 in
+ let l2 = NotationUtil.refresh_uri_in_term
+ ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
+ ~refresh_uri_in_reference l2
+ in
+ basic_eval_input_notation (l1,l2) status
+ else
+ status
+ in
+ GrafiteTypes.Serializer.register#run "input_notation"
+ basic_eval_input_notation
+;;
+
+let eval_input_notation status data=
+ let status = basic_eval_input_notation data status in
+ NCicLibrary.dump_obj status (inject_input_notation data)
+;;
+
+let basic_eval_output_notation (l1,l2) status =
+ TermContentPres.add_pretty_printer status l2 l1
+;;
+
+let inject_output_notation =
+ let basic_eval_output_notation (l1,l2)
+ ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+ ~alias_only status
+ =
+ if not alias_only then
+ let l1 =
+ CicNotationParser.refresh_uri_in_checked_l1_pattern
+ ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
+ ~refresh_uri_in_reference l1 in
+ let l2 = NotationUtil.refresh_uri_in_term
+ ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
+ ~refresh_uri_in_reference l2
+ in
+ basic_eval_output_notation (l1,l2) status
+ else
+ status
+ in
+ GrafiteTypes.Serializer.register#run "output_notation"
+ basic_eval_output_notation
+;;
+
+let eval_output_notation status data=
+ let status = basic_eval_output_notation data status in
+ NCicLibrary.dump_obj status (inject_output_notation data)
+;;
+