;;
let eval_unification_hint status t n =
- let newast,metasenv,subst,status,t =
+ let metasenv,subst,status,t =
GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in
assert (metasenv=[]);
let t = NCicUntrusted.apply_subst status subst [] t in
else
status
in
- let mode = GrafiteAst.WithPreferences (*assert false*) in (* MATITA 1.0 VEDI SOTTO *)
let diff =
(* FIXME! the uri should be filled with something meaningful! *)
- [DisambiguateTypes.Symbol (symbol, Some (None,dsc)),
+ [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 =
prerr_endline "basic_eval_alias";
- GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
+ 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 =
List.fold_left
(fun status (name,cpos,arity) ->
try
- let newast,metasenv,subst,status,t =
+ let metasenv,subst,status,t =
GrafiteDisambiguate.disambiguate_nterm status None [] [] []
("",0,NotationPt.Ident (name,`Ambiguous)) in
assert (metasenv = [] && subst = []);
let metasenv,subst,status,sort = match sort with
| None -> [],[],status,NCic.Sort NCic.Prop
| Some s ->
- let newast,metasenv,subst,status,sort =
+ let metasenv,subst,status,sort =
GrafiteDisambiguate.disambiguate_nterm status None [] [] []
(text,prefix_len,s)
in metasenv,subst,status,sort
"ninverter: found target %s, which is not a sort"
(status#ppterm ~metasenv ~subst ~context:[] sort))) in
let status = status#set_ng_mode `ProofMode in
- let newast,metasenv,subst,status,indty =
+ let metasenv,subst,status,indty =
GrafiteDisambiguate.disambiguate_nterm status None [] [] subst
(text,prefix_len,indty) in
let indtyno,(_,leftno,tys,_,_) =
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
code in DisambiguatePp *)
match spec with
| GrafiteAst.Ident_alias (id,uri) ->
- [DisambiguateTypes.Id (id,Some uri),spec]
+ [DisambiguateTypes.Id id,spec]
| GrafiteAst.Symbol_alias (symb, uri, desc) ->
- [DisambiguateTypes.Symbol (symb, Some (uri,desc)),spec]
+ [DisambiguateTypes.Symbol symb,spec]
| GrafiteAst.Number_alias (uri,desc) ->
- [DisambiguateTypes.Num (Some (uri,desc)),spec]
+ [DisambiguateTypes.Num,spec]
in
let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*)
eval_alias status (mode,diff)