X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.ml;h=4b1bdfcc872f32cb9bcf22f4fd6b8899d6148f5c;hb=5f1afbcf716a9275f70baa02a5a464bd2abc0726;hp=cbe14f9d5b8aaf0bcb370a70dc22d8fd86a0e494;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml index cbe14f9d5..4b1bdfcc8 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml @@ -25,16 +25,24 @@ (* $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 = @@ -43,39 +51,45 @@ class type g_status = method disambiguate_db: db end -class virtual status = +class virtual status uid = object (self) - inherit Interpretations.status + inherit Interpretations.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) 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 -;; +;;*) 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 + 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 set_proof_aliases status ~implicit_aliases mode new_aliases = - prerr_endline "set_proof_aliases"; - if mode = GrafiteAst.WithoutPreferences then - status - else - (prerr_endline "set_proof_aliases 2"; - let aliases = - List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) - status#disambiguate_db.aliases new_aliases in +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 @@ -83,13 +97,10 @@ 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) + status#set_disambiguate_db new_status + exception BaseUriNotSetYet @@ -105,13 +116,18 @@ let singleton msg = function let __Implicit = "__Implicit__" let __Closed_Implicit = "__Closed_Implicit__" -let ncic_mk_choice status = function +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 @@ -119,12 +135,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 + 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 @@ -144,7 +162,7 @@ let nlookup_in_library interactive_user_uri_choice input_or_locate_uri item = match item with - | DisambiguateTypes.Id (id,_) -> + | DisambiguateTypes.Id id -> (try let references = NCicLibrary.resolve id in List.map @@ -175,14 +193,114 @@ let nlookup_in_library ;;*) 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 +;; let disambiguate_nterm status expty context metasenv subst thing = - let newast, diff, metasenv, subst, cic = + let newast, metasenv, subst, cic = singleton "first" (NCicDisambiguate.disambiguate_term status - ~aliases:status#disambiguate_db.aliases + ~aliases:status#disambiguate_db.interpr ~expty ~universe:(status#disambiguate_db.multi_aliases) ~lookup_in_library:nlookup_in_library @@ -191,11 +309,11 @@ let disambiguate_nterm status expty context metasenv subst thing ~description_of_alias:GrafiteAst.description_of_alias ~context ~metasenv ~subst thing) in - let status = - set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences - diff + let _,_,thing' = thing in + let diff = diff_term Stdpp.dummy_loc thing' newast in + let status = add_to_interpr status diff in - newast, metasenv, subst, status, cic + metasenv, subst, status, cic ;; @@ -260,7 +378,7 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = in NUri.uri_of_string (baseuri ^ "/" ^ name) in - let diff, _, _, cic = + let ast, _, _, cic = singleton "third" (NCicDisambiguate.disambiguate_obj status @@ -268,12 +386,11 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = ~description_of_alias:GrafiteAst.description_of_alias ~mk_choice:(ncic_mk_choice status) ~mk_implicit ~fix_instance ~uri - ~aliases:status#disambiguate_db.aliases + ~aliases:status#disambiguate_db.interpr ~universe:(status#disambiguate_db.multi_aliases) (text,prefix_len,obj)) in - let status = - set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences - diff + let diff = diff_obj Stdpp.dummy_loc obj ast in + let status = add_to_interpr status diff in status, cic ;; @@ -288,14 +405,16 @@ let disambiguate_cic_appl_pattern status args = (List.exists (function (NotationPt.IdentArg (_,id')) -> id'=id) args) -> - let item = DisambiguateTypes.Id (id,None) in + let item = DisambiguateTypes.Id id in begin 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 -> @@ -320,6 +439,8 @@ let aliases_for_objs status refs = List.map (fun u -> let name = NCicPp.r2s status true u in - DisambiguateTypes.Id (name, Some (NReference.string_of_reference u)), + (* 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)