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)]
+ (* FIXME! the uri should be filled with something meaningful! *)
+ [DisambiguateTypes.Symbol symbol,
+ GrafiteAst.Symbol_alias (symbol,None,dsc)]
in
- GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
+ GrafiteDisambiguate.add_to_disambiguation_univ status diff
;;
let inject_interpretation =
;;
let basic_eval_alias (mode,diff) status =
- GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
+ prerr_endline "basic_eval_alias";
+ GrafiteDisambiguate.add_to_disambiguation_univ status diff
;;
let inject_alias =
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 rec get_disamb = function
+ | [] -> Stdpp.dummy_loc,None,None
+ | (_,(NotationEnv.NoType,NotationEnv.DisambiguationValue dv))::_ -> dv
+ | _::tl -> get_disamb tl
+ in
+ let l2' = TermContentPres.instantiate_level2 status env (get_disamb env) l2 in
+ prerr_endline ("new l2 ast : " ^ (NotationPp.pp_term status l2'));
+ NotationPt.AttributedTerm (`Loc loc,l2'))
;;
let inject_input_notation =
try
let metasenv,subst,status,t =
GrafiteDisambiguate.disambiguate_nterm status None [] [] []
- ("",0,NotationPt.Ident (name,None)) in
+ ("",0,NotationPt.Ident (name,`Ambiguous)) in
assert (metasenv = [] && subst = []);
let status, nuris =
NCicCoercDeclaration.
let metasenv,subst,status,sort = match sort with
| None -> [],[],status,NCic.Sort NCic.Prop
| Some s ->
- GrafiteDisambiguate.disambiguate_nterm status None [] [] []
- (text,prefix_len,s)
+ let metasenv,subst,status,sort =
+ GrafiteDisambiguate.disambiguate_nterm status None [] [] []
+ (text,prefix_len,s)
+ in metasenv,subst,status,sort
in
assert (metasenv = []);
let sort = NCicReduction.whd status ~subst [] sort in
in
eval_interpretation status (dsc,(symbol, args),cic_appl_pattern)
| GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) ->
+ prerr_endline ("new notation: " ^ (NotationPp.pp_term status l1));
let l1 =
CicNotationParser.check_l1_pattern
l1 (dir = Some `RightToLeft) precedence associativity
if dir <> Some `RightToLeft then eval_input_notation status (l1,l2)
else status
in
+ let status =
if dir <> Some `LeftToRight then eval_output_notation status (l1,l2)
else status
+ in prerr_endline ("new grammar:\n" ^ (Print_grammar.ebnf_of_term status));
+ status
| GrafiteAst.Alias (loc, spec) ->
let diff =
(*CSC: Warning: this code should be factorized with the corresponding
match spec with
| GrafiteAst.Ident_alias (id,uri) ->
[DisambiguateTypes.Id id,spec]
- | GrafiteAst.Symbol_alias (symb, instance, desc) ->
- [DisambiguateTypes.Symbol (symb,instance),spec]
- | GrafiteAst.Number_alias (instance,desc) ->
- [DisambiguateTypes.Num instance,spec]
+ | GrafiteAst.Symbol_alias (symb, uri, desc) ->
+ [DisambiguateTypes.Symbol symb,spec]
+ | GrafiteAst.Number_alias (uri,desc) ->
+ [DisambiguateTypes.Num,spec]
in
let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*)
eval_alias status (mode,diff)