X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=7e395e1c19bb096a7bc57845002624ba54c48b66;hb=9aa2722ff4aa7868ffd14e5a820cd6dc79e2c8a6;hp=5ce1386aeb0b16a9aca5a0f4abbde42270d3afe9;hpb=2914bfbeac3c2e0f53ba8c612cd11b3b2afbabce;p=helm.git diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml index 5ce1386ae..7e395e1c1 100644 --- a/matitaB/components/disambiguation/disambiguate.ml +++ b/matitaB/components/disambiguation/disambiguate.ml @@ -31,14 +31,8 @@ open DisambiguateTypes module Ast = NotationPt -(* the integer is an offset to be added to each location *) -exception Ambiguous_input -(* the integer is an offset to be added to each location *) -exception NoWellTypedInterpretation of - int * - ((Stdpp.location list * string * string) list * - (DisambiguateTypes.domain_item * string) list * - (Stdpp.location * string) Lazy.t * bool) list +exception NoWellTypedInterpretation of (Stdpp.location * string) + exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) @@ -51,6 +45,7 @@ type 'a disambiguator_input = string * int * 'a type domain = domain_tree list and domain_tree = Node of Stdpp.location list * domain_item * domain +(* let mono_uris_callback ~selection_mode ?ok ?(enable_button_for_non_vars = true) ~title ~msg ~id = if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true @@ -60,8 +55,8 @@ let mono_uris_callback ~selection_mode ?ok else raise Ambiguous_input -let mono_interp_callback _ _ _ = raise Ambiguous_input -let mono_disamb_callback _ = raise Ambiguous_input +let mono_interp_callback _ _ _ = assert false +let mono_disamb_callback _ = assert false let _choose_uris_callback = ref mono_uris_callback let _choose_interp_callback = ref mono_interp_callback @@ -73,6 +68,8 @@ let set_choose_disamb_callback f = _choose_disamb_callback := f let interactive_user_uri_choice = !_choose_uris_callback let interactive_interpretation_choice interp = !_choose_interp_callback interp let interactive_ast_choice interp = !_choose_disamb_callback interp +*) + let input_or_locate_uri ~(title:string) ?id () = None (* Zack: I try to avoid using this callback. I therefore assume that * the presence of an identifier that can't be resolved via "locate" @@ -133,6 +130,15 @@ type ('term,'metasenv,'subst,'graph) test_result = | Ko of (Stdpp.location * string) Lazy.t | Uncertain of (Stdpp.location * string) Lazy.t +type ('alias,'ast_thing,'metasenv,'subst,'thing,'ugraph) disamb_result = + | Disamb_success of ('ast_thing * 'metasenv * 'subst * 'thing * 'ugraph) list + (* each element of this list is a list of partially instantiated asts, + * sharing the last instantiated node, together with the location of that + * node; each ast is associated with the actual instantiation of the node, + * the refinement error, and the location at which refinement fails *) + | Disamb_failure of + (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list + let resolve ~env ~universe ~mk_choice item interpr arg = (* let _ = (mk_choice : (GrafiteAst.alias_spec -> 'b DisambiguateTypes.codomain_item)) in *) @@ -299,11 +305,11 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function ) [] defs in defs_dom @ where_dom - | Ast.Ident (name, x) -> - let x = match x with + | Ast.Ident (name, _x) -> + (* let x = match x with | `Uri u -> Some u - | _ -> None - in + | _ -> None + in *) (try (* the next line can raise Not_found *) ignore(find_in_context name context); [] @@ -480,50 +486,59 @@ let pattern_split ctx = function ;; (* this function is used to get the children of a given node, together with - * their context + * their context and their location * contexts are expressed in the form of functions Ast -> Ast *) -(* split : ('term -> 'a) -> 'term -> (('term -> 'a) * 'term) list *) -let rec split ctx = function +(* split : location -> ('term -> 'a) -> 'term -> (('term -> 'a) * 'term * loc) list *) +let rec split loc ctx t = + let loc_of_attr oldloc = function + | `Loc l -> l + | _ -> oldloc + in + match t with | Ast.AttributedTerm (attr,t) -> - [(fun x -> ctx (Ast.AttributedTerm(attr,x))),t] - | Ast.Appl tl -> list_split (*split*) (fun ctx0 t0 -> [ctx0,t0]) (fun x -> ctx (Ast.Appl x)) [] tl + [(fun x -> ctx (Ast.AttributedTerm(attr,x))),t, loc_of_attr loc attr] + | Ast.Appl tl -> list_split (*split*) (fun ctx0 t0 -> [ctx0,t0,loc]) (fun x -> ctx (Ast.Appl x)) [] tl | Ast.Binder (k,((n,None) as n'),body) -> - [ (fun v -> ctx (Ast.Binder (k,n',v))),body] + [ (fun v -> ctx (Ast.Binder (k,n',v))),body, loc] | Ast.Binder (k,((n,Some ty) as n'),body) -> - [(fun v -> ctx (Ast.Binder (k,(n,Some v),body))), ty - ;(fun v -> ctx (Ast.Binder (k,n',v))),body] + [(fun v -> ctx (Ast.Binder (k,(n,Some v),body))), ty, loc + ;(fun v -> ctx (Ast.Binder (k,n',v))),body, loc] | Ast.Case (t,ity,outty,pl) -> let outty_split = match outty with | None -> [] | Some u -> [(fun x -> ctx (Ast.Case (t,ity,Some x,pl))),u] in - ((fun x -> ctx (Ast.Case (x,ity,outty,pl))),t):: + List.map (fun (a,b) -> a,b,loc) + (((fun x -> ctx (Ast.Case (x,ity,outty,pl))),t):: outty_split@list_split (fun ctx0 (p,x) -> ((fun y -> ctx0 (p,y)),x)::pattern_split (fun y -> ctx0 (y,x)) p) (fun x -> ctx (Ast.Case(t,ity,outty,x))) - [] pl - | Ast.Cast (u,v) -> [ (fun x -> ctx (Ast.Cast (x,v))),u - ; (fun x -> ctx (Ast.Cast (u,x))),v ] + [] pl) + | Ast.Cast (u,v) -> [ (fun x -> ctx (Ast.Cast (x,v))),u,loc + ; (fun x -> ctx (Ast.Cast (u,x))),v,loc ] | Ast.LetIn ((n,None) as n',u,v) -> - [ (fun x -> ctx (Ast.LetIn (n',x,v))), u - ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ] + [ (fun x -> ctx (Ast.LetIn (n',x,v))), u,loc + ; (fun x -> ctx (Ast.LetIn (n',u,x))), v,loc ] | Ast.LetIn ((n,Some t) as n',u,v) -> - [ (fun x -> ctx (Ast.LetIn ((n,Some x),u,v))), t - ; (fun x -> ctx (Ast.LetIn (n',x,v))), u - ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ] + [ (fun x -> ctx (Ast.LetIn ((n,Some x),u,v))), t,loc + ; (fun x -> ctx (Ast.LetIn (n',x,v))), u, loc + ; (fun x -> ctx (Ast.LetIn (n',u,x))), v, loc ] | Ast.LetRec (k,funs,where) -> (* we do not use where any more?? *) - list_split letrecaux_split (fun x -> ctx (Ast.LetRec(k,x,where))) [] funs + List.map (fun (a,b) -> a,b,loc) + (list_split letrecaux_split (fun x -> ctx (Ast.LetRec(k,x,where))) [] funs) | _ -> [] (* leaves *) ;; +type 'ast marked_ast = + (NotationPt.term -> 'ast) * NotationPt.term * Stdpp.location -(* top_split : 'a -> ((term -> 'a) * term) list - * returns all the possible top-level (ctx,t) for its input *) +(* top_split : 'a -> ((term -> 'a) * term * loc) list + * such that it returns all the possible top-level (ctx,t,dummy_loc) for its input *) let bfvisit ~pp_term top_split test t = let rec aux = function | [] -> None - | (ctx0,t0 as hd)::tl -> + | (ctx0,t0,loc as hd)::tl -> (* prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *) debug_print (lazy ("visiting t0 = " ^ pp_term t0)); if test t0 then (debug_print (lazy "t0 is ambiguous"); Some hd) @@ -534,7 +549,7 @@ let bfvisit ~pp_term top_split test t = List.iter (fun (ctx',t') -> prerr_endline ("-- subnode " ^ (pp_term t'))) t0'; aux (tl@t0')) *) - let t0' = split ctx0 t0 in + let t0' = split loc ctx0 t0 in aux (tl@t0') (* in aux [(fun x -> x),t] *) in aux (top_split t) @@ -542,22 +557,24 @@ let bfvisit ~pp_term top_split test t = let obj_split (o:Ast.term Ast.obj) = match o with | Ast.Inductive (ls,itl) -> - list_split var_split (fun x -> Ast.Inductive (x,itl)) [] ls@ - list_split ity_split (fun x -> Ast.Inductive (ls,x)) [] itl + List.map (fun (a,b) -> a,b,Stdpp.dummy_loc) + (list_split var_split (fun x -> Ast.Inductive (x,itl)) [] ls@ + list_split ity_split (fun x -> Ast.Inductive (ls,x)) [] itl) | Ast.Theorem (flav,n,ty,None,p) -> - [(fun x -> Ast.Theorem (flav,n,x,None,p)), ty] + [(fun x -> Ast.Theorem (flav,n,x,None,p)), ty, Stdpp.dummy_loc] | Ast.Theorem (flav,n,ty,(Some bo as bo'),p) -> - [(fun x -> Ast.Theorem (flav,n,x,bo',p)), ty - ;(fun x -> Ast.Theorem (flav,n,ty,Some x,p)), bo] + [(fun x -> Ast.Theorem (flav,n,x,bo',p)), ty, Stdpp.dummy_loc + ;(fun x -> Ast.Theorem (flav,n,ty,Some x,p)), bo, Stdpp.dummy_loc] | Ast.Record (ls,n,ty,fl) -> - list_split var_split (fun x -> Ast.Record (x,n,ty,fl)) [] ls@ - [(fun x -> Ast.Record (ls,n,x,fl)),ty]@ - list_split field_split (fun x -> Ast.Record (ls,n,ty,x)) [] fl + List.map (fun (a,b) -> a,b,Stdpp.dummy_loc) + (list_split var_split (fun x -> Ast.Record (x,n,ty,fl)) [] ls@ + [(fun x -> Ast.Record (ls,n,x,fl)),ty]@ + list_split field_split (fun x -> Ast.Record (ls,n,ty,x)) [] fl) ;; let bfvisit_obj = bfvisit obj_split;; -let bfvisit = bfvisit (fun t -> [(fun x -> x),t]) ;; +let bfvisit = bfvisit (fun t -> [(fun x -> x),t,Stdpp.dummy_loc]) ;; let domain_item_of_ast = function | Ast.Ident (id,_) -> DisambiguateTypes.Id id @@ -576,6 +593,10 @@ let ast_of_alias_spec t alias = match (t,alias) with | _ -> assert false ;; +(* returns an optional (loc*string): + * - None means success (the ast is refinable) + * - Some (loc,err) means refinement has failed with error err at location loc + *) let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl t = try @@ -589,20 +610,27 @@ let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~universe ~use_coercions cic_thing expty ugraph ~localization_tbl in match (refine_profiler.HExtlib.profile foo ()) with | Ko x -> - let _,err = Lazy.force x in + let loc,err = Lazy.force x in debug_print (lazy ("test_interpr error: " ^ err)); - false - | _ -> true + Some (loc,err) + | _ -> None with (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) | Invalid_choice loc_msg -> Ko loc_msg*) - | Invalid_choice _ -> false - | _ -> true + | Invalid_choice x -> + let loc,err = Lazy.force x in + debug_print (lazy ("test_interpr invalid choice: " ^ err)); + Some (loc,err) + | e -> debug_print (lazy ("uncaught error: "^ Printexc.to_string e));None ;; +exception Not_ambiguous;; + let rec disambiguate_list ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri ~interpretate_thing - ~refine_thing ~ugraph ~visit ~universe ~mk_localization_tbl ~pp_thing ~pp_term ts = + ~refine_thing ~ugraph ~visit ~universe ~mk_localization_tbl ~pp_thing ~pp_term + ts errors = + let disambiguate_list = disambiguate_list ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri ~interpretate_thing ~refine_thing ~ugraph ~visit ~universe @@ -633,15 +661,15 @@ let rec disambiguate_list let get_instances ctx t = try let choices = find_choices (domain_item_of_ast t) in - List.map (fun t0 -> ctx (ast_of_alias_spec t t0)) choices + List.map (fun t0 -> ctx (ast_of_alias_spec t t0), t0) choices with | Not_found -> [] in match ts with - | [] -> None - | t0 :: tl -> - debug_print (lazy ("disambiguate_list: t0 = " ^ pp_thing t0)); + | [] -> [], errors + | _ -> + (* debug_print (lazy ("disambiguate_list: t0 = " ^ pp_thing t0)); *) let is_ambiguous = function | Ast.Ident (_,`Ambiguous) | Ast.Num (_,None) @@ -655,34 +683,55 @@ let rec disambiguate_list | Ast.Symbol (sym,_) -> "SYM " ^ sym | _ -> "ERROR!" in - (* get first ambiguous subterm (or return disambiguated term) *) - match visit ~pp_term is_ambiguous t0 with - | None -> - debug_print (lazy ("visit -- not ambiguous node:\n" ^ pp_thing t0)); - Some (t0,tl) - | Some (ctx, t) -> - debug_print (lazy ("visit -- found ambiguous node: " ^ astpp t ^ - "\nin " ^ pp_thing (ctx t))); - (* get possible instantiations of t *) - let instances = get_instances ctx t in - debug_print (lazy "-- possible instances:"); - List.iter - (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0)))) instances; - (* perforate ambiguous subterms and test refinement *) - debug_print (lazy "-- survivors:"); - let survivors = List.filter test_interpr instances in - List.iter - (fun u0 -> debug_print (lazy ("-- survivor: " ^ (pp_thing u0)))) survivors; - disambiguate_list (survivors@tl) + let process_ast t0 = + (* get first ambiguous subterm (or return disambiguated term) *) + match visit ~pp_term is_ambiguous t0 with + | None -> +(* debug_print (lazy ("visit -- not ambiguous node:\n" ^ pp_thing + * t0));*) + (* Some (t0,tl), errors *) + raise Not_ambiguous + | Some (ctx, t, loc_t) -> + debug_print (lazy ("visit -- found ambiguous node: " ^ astpp t ^ + "\nin " ^ pp_thing (ctx t))); + (* get possible instantiations of t *) + let instances = get_instances ctx t in + if instances = [] then + raise (NoWellTypedInterpretation (loc_t, "No choices for " ^ astpp t)); + debug_print (lazy "-- possible instances:"); +(* List.iter + (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0)))) +instances; *) + (* perforate ambiguous subterms and test refinement *) + let instances = List.map (fun (x,a) -> (x,Some a),test_interpr x) instances in + debug_print (lazy "-- survivors:"); + let survivors, defuncts = + List.partition (fun (_,o) -> o = None) instances in + survivors, (defuncts, loc_t) + + in + try + let ts', new_errors = List.split (List.map process_ast ts) in + let ts' = List.map (fun ((t,_),_) -> t) (List.flatten ts') in + let errors' = match new_errors with + | (_,l)::_ -> + let ne' = + List.map (fun (a,b) -> a, HExtlib.unopt b) + (List.flatten (List.map fst new_errors)) in + let ne' = List.map (fun ((x,a),(l,e)) -> x,a,l,e) ne' in + (ne',l)::errors + | _ -> errors + in disambiguate_list ts' errors' + with Not_ambiguous -> ts,errors ;; let disambiguate_thing ~context ~metasenv ~subst ~use_coercions - ~string_context_of_context - ~initial_ugraph:base_univ ~expty - ~mk_implicit ~description_of_alias ~fix_instance - ~aliases ~universe ~lookup_in_library - ~uri ~pp_thing ~pp_term ~domain_of_thing ~interpretate_thing ~refine_thing + ~string_context_of_context ~initial_ugraph:base_univ + ~expty ~mk_implicit ~description_of_alias + ~fix_instance ~aliases ~universe + ~lookup_in_library ~uri ~pp_thing ~pp_term + ~domain_of_thing ~interpretate_thing ~refine_thing ~visit ~mk_localization_tbl (thing_txt,thing_txt_prefix_len,thing) = @@ -692,15 +741,12 @@ let disambiguate_thing ~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl in (* real function *) - let rec aux tl = - match disambiguate_list ~mk_localization_tbl ~context ~metasenv ~subst + let aux tl = + disambiguate_list ~mk_localization_tbl ~context ~metasenv ~subst ~interpretate_thing ~refine_thing ~ugraph:base_univ ~visit ~use_coercions ~expty ~uri ~env ~universe ~pp_thing - ~pp_term tl with - | None -> [] - | Some (t,tl') -> t::aux tl' + ~pp_term tl [] in - let refine t = let localization_tbl = mk_localization_tbl 503 in debug_print (lazy "before interpretate_thing"); @@ -711,31 +757,37 @@ let disambiguate_thing match refine_thing metasenv subst context uri ~use_coercions t' expty base_univ ~localization_tbl with | Ok (t',m',s',u') -> t,m',s',t',u' - | Uncertain x -> - let _,err = Lazy.force x in + | Uncertain x | Ko x -> + let loc,err = Lazy.force x in debug_print (lazy ("refinement uncertain after disambiguation: " ^ err)); - assert false - | _ -> assert false + raise (NoWellTypedInterpretation (loc,err)) in - if not (test_interpr thing) then - (debug_print (lazy ("preliminary test fail: " ^ pp_thing thing)); - raise (NoWellTypedInterpretation (0,[]))) - else - let res = aux [thing] in - let res = - HExtlib.filter_map (fun t -> - try Some (refine t) - with _ -> - debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));None) res + match (test_interpr thing) with + | Some (loc,err) -> + debug_print (lazy ("preliminary test fail: " ^ pp_thing thing)); + Disamb_failure ([[thing,None,loc,err],loc]) + | None -> + let res,errors = aux [thing] in + let res,inner_errors = + List.split + (List.map (fun t -> + try (Some (refine t), None) + (* this error is actually a singleton *) + with NoWellTypedInterpretation loc_err -> + debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t))); + None, Some loc_err) res) in + let res = HExtlib.filter_map (fun x -> x) res in + let inner_errors = + HExtlib.filter_map + (function Some (loc,err) -> Some (thing,None,loc,err) | None -> None) + inner_errors + in + let errors = + if inner_errors <> [] then (inner_errors,Stdpp.dummy_loc)::errors + else errors in - match res with - | [] -> raise (NoWellTypedInterpretation (0,[])) - | [t] -> res,false - | _ -> - let choices = List.map (fun (t,_,_,_,_) -> pp_thing t) res in - let user_choice = interactive_ast_choice choices in - [ List.nth res user_choice ], true - (* let pp_thing (t,_,_,_,_,_) = prerr_endline ("interpretation: " ^ (pp_thing t)) in - List.iter pp_thing res; res,true *) + (match res with + | [] -> prerr_endline ((string_of_int (List.length errors)) ^ " error frames");Disamb_failure errors + | _ -> Disamb_success res) ;;