X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.ml;h=d6e4e0c354f305f107fd79e09e16cff9e4eefa4d;hb=bbb6dd07ecb430bf06bb52c2506626106449a5af;hp=dbdd2131304c1ec34b4da5a0e717fa24e7743ab9;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml index dbdd21313..d6e4e0c35 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml @@ -25,55 +25,105 @@ (* $Id$ *) +module Ast = NotationPt + type db = { - aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t; + (* maps (loc,domain_item) to alias *) + interpr: GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t; + (* the universe of possible interpretations for all symbols/ids/nums *) multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t; - new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list + (* new_aliases: ((Stdpp.location * DisambiguateTypes.domain_item) * GrafiteAst.alias_spec) list *) } +let get_interpr db = + db.interpr +;; + let initial_status = { - aliases = DisambiguateTypes.Environment.empty; + interpr = DisambiguateTypes.InterprEnv.empty; multi_aliases = DisambiguateTypes.Environment.empty; - new_aliases = [] + (* new_aliases = [] *) } class type g_status = object inherit Interpretations.g_status + inherit NCicLibrary.g_status method disambiguate_db: db end -class virtual status = +class virtual status uid = object (self) - inherit Interpretations.status + inherit Interpretations.status uid + inherit NCicLibrary.status uid val disambiguate_db = initial_status method disambiguate_db = disambiguate_db method set_disambiguate_db v = {< disambiguate_db = v >} + method reset_disambiguate_db () = + {< disambiguate_db = { self#disambiguate_db with interpr = + DisambiguateTypes.InterprEnv.empty } >} method set_disambiguate_status : 'status. #g_status as 'status -> 'self - = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db) + = fun o -> ((self#set_interp_status o)#set_disambiguate_db + o#disambiguate_db)#set_lib_status o end -let eval_with_new_aliases status f = +(* let eval_with_new_aliases status f = let status = status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in let res = f status in let new_aliases = status#disambiguate_db.new_aliases in new_aliases,res -;; +;;*) + +(* reports the first source of ambiguity and its possible interpretations *) +exception Ambiguous_input of (Stdpp.location * GrafiteAst.alias_spec list) + +(* reports disambiguation errors *) +exception Error of + (* location of a choice point *) + (Stdpp.location * + (* one possible choice (or no valid choice) *) + (GrafiteAst.alias_spec option * + (* list of asts together with the failing location and error msg *) + ((Stdpp.location * GrafiteAst.alias_spec) list * + Stdpp.location * string) list) + list) + list let dump_aliases out msg status = out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:"); - DisambiguateTypes.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x)) - status#disambiguate_db.aliases - -let set_proof_aliases status ~implicit_aliases mode new_aliases = - if mode = GrafiteAst.WithoutPreferences then - status - else - let aliases = - List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) - status#disambiguate_db.aliases new_aliases in + DisambiguateTypes.InterprEnv.iter (fun _ x -> out (GrafiteAstPp.pp_alias x)) + status#disambiguate_db.interpr + +let add_to_interpr status new_aliases = + let interpr = + List.fold_left (fun acc (k,c) -> + DisambiguateTypes.InterprEnv.add k c acc) + status#disambiguate_db.interpr new_aliases + in + let new_status = + {status#disambiguate_db with interpr = interpr } + in + status#set_disambiguate_db new_status + +(* +let print_interpr status = + DisambiguateTypes.InterprEnv.iter + (fun loc alias -> + let start,stop = HExtlib.loc_of_floc loc in + let strpos = Printf.sprintf "@(%d,%d):" start stop in + match alias with + | GrafiteAst.Ident_alias (id,uri) -> + Printf.printf "%s [%s;%s]\n" strpos id uri + | GrafiteAst.Symbol_alias (name,_ouri,desc) -> + Printf.printf "%s <%s:%s>\n" strpos name desc + | GrafiteAst.Number_alias (_ouri,desc) -> + Printf.printf "%s \n" strpos desc) + status#disambiguate_db.interpr +*) + +let add_to_disambiguation_univ status new_aliases = let multi_aliases = List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias @@ -81,35 +131,28 @@ let set_proof_aliases status ~implicit_aliases mode new_aliases = status#disambiguate_db.multi_aliases new_aliases in let new_status = - {multi_aliases = multi_aliases ; - aliases = aliases; - new_aliases = - (if implicit_aliases then new_aliases else []) @ - status#disambiguate_db.new_aliases} + {status#disambiguate_db with multi_aliases = multi_aliases } in status#set_disambiguate_db new_status -exception BaseUriNotSetYet -let singleton msg = function - | [x], _ -> x - | l, _ -> - let debug = - Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations" - msg (List.length l) - in - prerr_endline debug; assert false +exception BaseUriNotSetYet let __Implicit = "__Implicit__" let __Closed_Implicit = "__Closed_Implicit__" -let ncic_mk_choice status = function - | GrafiteAst.Symbol_alias (name, _, dsc) -> +let ncic_mk_choice status a = + prerr_endline "ncic_mk_choice"; + match a with + | GrafiteAst.Symbol_alias (name,_, dsc) -> + prerr_endline ("caso 1: " ^ name ^ "; " ^ dsc); if name = __Implicit then dsc, `Sym_interp (fun _ -> NCic.Implicit `Term) else if name = __Closed_Implicit then dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed) else + (prerr_endline (Printf.sprintf "mk_choice: symbol %s, interpr %s" + name dsc); DisambiguateChoices.lookup_symbol_by_dsc status ~mk_implicit:(function | true -> NCic.Implicit `Closed @@ -117,12 +160,14 @@ let ncic_mk_choice status = function ~mk_appl:(function (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l) ~term_of_nref:(fun nref -> NCic.Const nref) - name dsc - | GrafiteAst.Number_alias (_, dsc) -> + name dsc) + | GrafiteAst.Number_alias (_,dsc) -> + prerr_endline ("caso 2: " ^ dsc); let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in desc, `Num_interp (fun num -> match f with `Num_interp f -> f num | _ -> assert false) | GrafiteAst.Ident_alias (name, uri) -> + prerr_endline ("caso 3: " ^ name); uri, `Sym_interp (fun l->assert(l = []); let nref = NReference.reference_of_string uri in @@ -133,32 +178,34 @@ let ncic_mk_choice status = function let mk_implicit b = match b with | false -> - GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit") + GrafiteAst.Symbol_alias (__Implicit,None,"Fake Implicit") | true -> - GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit") + GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit") ;; -let nlookup_in_library +let nlookup_in_library status interactive_user_uri_choice input_or_locate_uri item = match item with | DisambiguateTypes.Id id -> (try - let references = NCicLibrary.resolve id in + let references = NCicLibrary.resolve status id in List.map - (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u) + (fun u -> + GrafiteAst.Ident_alias (id,NReference.string_of_reference u) ) references with NCicEnvironment.ObjectNotFound _ -> []) | _ -> [] ;; -let fix_instance item l = +(* XXX TO BE REMOVED: no need to fix instances any more *) +(*let fix_instance item l = match item with DisambiguateTypes.Symbol (_,n) -> List.map (function - GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d) + GrafiteAst.Symbol_alias (s,d) -> GrafiteAst.Symbol_alias (s,n,d) | _ -> assert false ) l | DisambiguateTypes.Num n -> @@ -168,32 +215,165 @@ let fix_instance item l = | _ -> assert false ) l | DisambiguateTypes.Id _ -> l +;;*) +let fix_instance _ l = l;; + +let rec diff_term loc t u = match (t,u) with + | Ast.AttributedTerm (`Loc l,t'), Ast.AttributedTerm (_,u') -> diff_term l t' u' + | Ast.AttributedTerm (_,t'), Ast.AttributedTerm (_,u') -> diff_term loc t' u' + | Ast.Appl tl, Ast.Appl ul -> + List.fold_left2 (fun acc t0 u0 -> diff_term loc t0 u0@acc) [] tl ul + | Ast.Binder (_,v1,b1), Ast.Binder (_,v2,b2) -> + diff_var loc v1 v2@ diff_term loc b1 b2 + | Ast.Case (t1,ity1,outty1,pl1),Ast.Case (t2,ity2,outty2,pl2) -> + let ity_interp = match ity1,ity2 with + | Some (i,None), Some (_,Some r) -> + let uri = NReference.string_of_reference r in + [loc,GrafiteAst.Ident_alias (i,uri)] + | _ -> [] + in + let oty_interp = match outty1,outty2 with + | Some o1, Some o2 -> diff_term loc o1 o2 + | _ -> [] + in + (* pl = (case_pattern * term) list *) + let auxpatt (c1,u1) (c2,u2) acc = + let diff_cp = match c1,c2 with + | Ast.Pattern (i,href1,vars1), Ast.Pattern (_,href2,vars2) -> + let diff_i = match href1,href2 with + | None, Some r -> + let uri = NReference.string_of_reference r in + [loc,GrafiteAst.Ident_alias (i,uri)] + | _ -> [] + in + let diff_vars = + List.fold_right2 (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 [] + in + diff_i @ diff_vars + | _ -> [] + in + diff_term loc u1 u2 @ diff_cp @ acc + in + let pl_interp = List.fold_right2 auxpatt pl1 pl2 [] in + diff_term loc t1 t2 @ ity_interp @ oty_interp @ pl_interp + | Ast.Cast (u1,v1),Ast.Cast (u2,v2) -> + diff_term loc u1 u2@diff_term loc v1 v2 + | Ast.LetIn (var1,u1,v1),Ast.LetIn (var2,u2,v2) -> + diff_var loc var1 var2 @ diff_term loc u1 u2 @ diff_term loc v1 v2 + | Ast.LetRec (_,fl1,w1),Ast.LetRec (_,fl2,w2) -> + let diff_funs = + List.fold_right2 + (fun (vars1,f1,b1,_) (vars2,f2,b2,_) acc -> + let diff_vars = + List.fold_right2 + (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 [] + in + diff_vars @ diff_var loc f1 f2 @ diff_term loc b1 b2 @ acc) + fl1 fl2 [] + in + diff_funs @ diff_term loc w1 w2 + | Ast.Ident (n,`Ambiguous),Ast.Ident (_,`Uri u) -> + [loc,GrafiteAst.Ident_alias (n,u)] + | Ast.Symbol (s, None),Ast.Symbol(_,Some (uri,desc)) -> + [loc,GrafiteAst.Symbol_alias (s,uri,desc)] + | Ast.Num (_, None),Ast.Num (_,Some (uri,desc)) -> + [loc,GrafiteAst.Number_alias (uri,desc)] + | _ -> [] (* leaves *) +and diff_var loc (_,v1) (_,v2) = match v1,v2 with + | Some v1', Some v2' -> diff_term loc v1' v2' + | _ -> [] ;; +let diff_obj loc o1 o2 = match o1,o2 with + | Ast.Inductive (ls1,itys1), Ast.Inductive (ls2,itys2) -> + let diff_ls = + List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 [] + in + let diff_itys = + List.fold_right2 + (fun (i1,_,ty1,cl1) (i2,_,ty2,cl2) acc0 -> + let diff_cl = + List.fold_right2 + (fun (_,u) (_,v) acc1 -> diff_term loc u v @ acc1) + cl1 cl2 [] + in + diff_term loc ty1 ty2 @ diff_cl @ acc0) + itys1 itys2 [] + in + diff_ls @ diff_itys + | Ast.Theorem (_,i1,b1,ty1,_), Ast.Theorem (_,i2,b2,ty2,_) -> + let diff_tys = match ty1,ty2 with + | Some ty1', Some ty2' -> diff_term loc ty1' ty2' + | _ -> [] + in + diff_term loc b1 b2 @ diff_tys + | Ast.Record (ls1,_,ty1,fl1),Ast.Record (ls2,_,ty2,fl2) -> + let diff_ls = + List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 [] + in + let diff_fl = + List.fold_right2 + (fun (_,f1,_,_) (_,f2,_,_) acc -> diff_term loc f1 f2 @ acc) fl1 fl2 [] + in + diff_ls @ diff_term loc ty1 ty2 @ diff_fl + | _ -> assert false +;; + +(* this function, called on a list of choices that must + * be different, never fails and returns the location of + * the first ambiguity (and its possible interpretations) *) +let rec find_diffs l = + let loc,_ = List.hd (List.hd l) in + let hds = List.map (fun x -> snd (List.hd x)) l in + let uniq_hds = HExtlib.list_uniq (List.sort Pervasives.compare hds) in + + if List.length uniq_hds > 1 + then loc, uniq_hds + else + let tls = List.map List.tl l in + find_diffs tls +;; + +(* clusterize a list of errors according to the last chosen interpretation *) +let clusterize diff (eframe,loc0) = + let rec aux = function + | [] -> [] + | (_,choice,_,_ as x)::l0 -> + let matches,others = List.partition (fun (_,c,_,_) -> c = choice) l0 in + (choice,List.map (fun (a,_,l,e) -> diff a,l,e) (x::matches)) :: + aux others + in loc0, aux eframe let disambiguate_nterm status expty context metasenv subst thing = - let diff, metasenv, subst, cic = - singleton "first" - (NCicDisambiguate.disambiguate_term + let _,_,thing' = thing in + match NCicDisambiguate.disambiguate_term status - ~aliases:status#disambiguate_db.aliases + ~aliases:status#disambiguate_db.interpr ~expty - ~universe:(Some status#disambiguate_db.multi_aliases) - ~lookup_in_library:nlookup_in_library + ~universe:(status#disambiguate_db.multi_aliases) + ~lookup_in_library:(nlookup_in_library status) ~mk_choice:(ncic_mk_choice status) ~mk_implicit ~fix_instance ~description_of_alias:GrafiteAst.description_of_alias - ~context ~metasenv ~subst thing) - in - let status = - set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences - diff - in - metasenv, subst, status, cic + ~context ~metasenv ~subst thing + with + | Disambiguate.Disamb_success [newast,metasenv,subst,cic,_] -> + let diff = diff_term Stdpp.dummy_loc thing' newast in + let status = add_to_interpr status diff + in + metasenv, subst, status, cic + | Disambiguate.Disamb_success (_::_ as choices) -> + let diffs = + List.map (fun (ast,_,_,_,_) -> + diff_term Stdpp.dummy_loc thing' ast) choices + in + raise (Ambiguous_input (find_diffs diffs)) + | Disambiguate.Disamb_failure l -> + raise (Error (List.map (clusterize (diff_term Stdpp.dummy_loc thing')) l)) + | _ -> assert false ;; - type pattern = NotationPt.term Disambiguate.disambiguator_input option * (string * NCic.term) list * NCic.term option @@ -241,7 +421,7 @@ let disambiguate_just disambiguate_term context metasenv = metasenv, `Auto params ;; -let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = +let disambiguate_nobj status ?baseuri (text,prefix_len,obj as obj') = let uri = let baseuri = match baseuri with Some x -> x | None -> raise BaseUriNotSetYet @@ -255,22 +435,30 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = in NUri.uri_of_string (baseuri ^ "/" ^ name) in - let diff, _, _, cic = - singleton "third" - (NCicDisambiguate.disambiguate_obj + + match NCicDisambiguate.disambiguate_obj status - ~lookup_in_library:nlookup_in_library + ~lookup_in_library:(nlookup_in_library status) ~description_of_alias:GrafiteAst.description_of_alias ~mk_choice:(ncic_mk_choice status) ~mk_implicit ~fix_instance ~uri - ~aliases:status#disambiguate_db.aliases - ~universe:(Some status#disambiguate_db.multi_aliases) - (text,prefix_len,obj)) in - let status = - set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences - diff - in - status, cic + ~aliases:status#disambiguate_db.interpr + ~universe:(status#disambiguate_db.multi_aliases) + obj' + with + | Disambiguate.Disamb_success [newast,_,_,cic,_] -> + let diff = diff_obj Stdpp.dummy_loc obj newast in + let status = add_to_interpr status diff + in status, cic + | Disambiguate.Disamb_success (_::_ as choices) -> + let diffs = + List.map (fun (ast,_,_,_,_) -> + diff_obj Stdpp.dummy_loc obj ast) choices + in + raise (Ambiguous_input (find_diffs diffs)) + | Disambiguate.Disamb_failure l -> + raise (Error (List.map (clusterize (diff_obj Stdpp.dummy_loc obj)) l)) + | _ -> assert false ;; let disambiguate_cic_appl_pattern status args = @@ -288,9 +476,11 @@ let disambiguate_cic_appl_pattern status args = try match DisambiguateTypes.Environment.find item - status#disambiguate_db.aliases + (* status#disambiguate_db.aliases *) + status#disambiguate_db.multi_aliases with - GrafiteAst.Ident_alias (_, uri) -> + (* XXX : we only try the first match *) + GrafiteAst.Ident_alias (_,uri)::_ -> NotationPt.NRefPattern (NReference.reference_of_string uri) | _ -> assert false with Not_found -> @@ -311,10 +501,12 @@ let aliases_for_objs status refs = List.concat (List.map (fun nref -> - let references = NCicLibrary.aliases_of nref in + let references = NCicLibrary.aliases_of status nref in List.map (fun u -> let name = NCicPp.r2s status true u in + (* FIXME : we are forgetting the interpretation of the Id + * but is this useful anymore?!?!? *) DisambiguateTypes.Id name, GrafiteAst.Ident_alias (name,NReference.string_of_reference u) ) references) refs)