X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=7e395e1c19bb096a7bc57845002624ba54c48b66;hb=59fd7b5ea24e71b47aee069440f140bcccf1292a;hp=62d708a7fdfcce6797bff7e0fa07926a3e128a1e;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml index 62d708a7f..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,15 +55,21 @@ let mono_uris_callback ~selection_mode ?ok else raise Ambiguous_input -let mono_interp_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 +let _choose_disamb_callback = ref mono_disamb_callback let set_choose_uris_callback f = _choose_uris_callback := f let set_choose_interp_callback f = _choose_interp_callback := f +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" @@ -129,16 +130,40 @@ type ('term,'metasenv,'subst,'graph) test_result = | Ko of (Stdpp.location * string) Lazy.t | Uncertain of (Stdpp.location * string) Lazy.t -let resolve ~env ~mk_choice (item: domain_item) arg = +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 *) try - match snd (mk_choice (Environment.find item env)), arg with + let interpr = + match interpr with + | None -> InterprEnv.find item env + | Some i -> i + in + (* one, and only one interpretation is returned (or Not_found) *) + (*if (List.length interpr <> 1) + then (let strinterpr = + String.concat ", " (List.map GrafiteAst.description_of_alias interpr) in + prerr_endline (Printf.sprintf "choices for %s: %s" + (DisambiguateTypes.string_of_domain_item item) strinterpr); + assert false) + else + let interpr = List.hd interpr in*) + match snd (mk_choice interpr), arg with `Num_interp f, `Num_arg n -> f n | `Sym_interp f, `Args l -> f l | `Sym_interp f, `Num_arg n -> (* Implicit number! *) f [] | _,_ -> assert false with Not_found -> - failwith ("Domain item not found: " ^ - (DisambiguateTypes.string_of_domain_item item)) + failwith (": InterprEnv.find failed") (* TODO move it to Cic *) let find_in_context name context = @@ -155,16 +180,19 @@ let string_of_name = | _ -> assert false ;; +(* XXX: assuming the domain is composed of uninterpreted items only *) let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function | Ast.AttributedTerm (`Loc loc, term) -> domain_of_term ~loc ~context term | Ast.AttributedTerm (_, term) -> domain_of_term ~loc ~context term | Ast.Symbol (name, attr) -> - [ Node ([loc], Symbol (name,attr), []) ] + (match attr with + | None -> [ Node ([loc], Symbol name, []) ] + | _ -> []) (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *) - | Ast.Appl (Ast.Symbol (name, attr) as hd :: args) - | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (name,attr)) as hd :: args) + | Ast.Appl (Ast.Symbol (name, None) as hd :: args) + | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (name,None)) as hd :: args) -> let args_dom = List.fold_right @@ -175,13 +203,9 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function Ast.AttributedTerm (`Loc loc,_) -> loc | _ -> loc in - [ Node ([loc], Symbol (name,attr), args_dom) ] - | Ast.Appl (Ast.Ident (id,uri) as hd :: args) - | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (id,uri)) as hd :: args) -> - let uri = match uri with - | `Uri u -> Some u - | _ -> None - in + [ Node ([loc], Symbol name, args_dom) ] + | Ast.Appl (Ast.Ident (id,`Ambiguous) as hd :: args) + | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (id,`Ambiguous)) as hd :: args) -> let args_dom = List.fold_right (fun term acc -> domain_of_term ~loc ~context term @ acc) @@ -196,7 +220,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function ignore(find_in_context id context); args_dom with Not_found -> - [ Node ([loc], Id (id,uri), args_dom) ] ) + [ Node ([loc], Id id, args_dom) ] ) | Ast.Appl terms -> List.fold_right (fun term acc -> domain_of_term ~loc ~context term @ acc) @@ -207,17 +231,17 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function domain_of_term ~loc ~context:(string_of_name var :: context) body in (match kind with - | `Exists -> [ Node ([loc], Symbol ("exists",None), (type_dom @ body_dom)) ] + | `Exists -> [ Node ([loc], Symbol "exists", (type_dom @ body_dom)) ] | _ -> type_dom @ body_dom) | Ast.Case (term, indty_ident, outtype, branches) -> let term_dom = domain_of_term ~loc ~context term in let outtype_dom = domain_of_term_option ~loc ~context outtype in let rec get_first_constructor = function | [] -> [] - | (Ast.Pattern (head, Some r, _), _) :: _ -> - [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ] + | (Ast.Pattern (head, Some r, _), _) :: _ -> [] + (* [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ] *) | (Ast.Pattern (head, None, _), _) :: _ -> - [ Node ([loc], Id (head,None), []) ] + [ Node ([loc], Id head, []) ] | _ :: tl -> get_first_constructor tl in let do_branch = function @@ -239,9 +263,9 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in (match indty_ident with | None -> get_first_constructor branches - | Some (ident, None) -> [ Node ([loc], Id (ident,None) , []) ] - | Some (ident, Some r) -> - [ Node ([loc], Id (ident,Some (NReference.string_of_reference r)), []) ]) + | Some (ident, None) -> [ Node ([loc], Id ident , []) ] + | Some (ident, Some r) -> []) + (* [ Node ([loc], Id (ident,Some (NReference.string_of_reference r)), []) ]) *) @ term_dom @ outtype_dom @ branches_dom | Ast.Cast (term, ty) -> let term_dom = domain_of_term ~loc ~context term in @@ -281,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); [] @@ -301,11 +325,11 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function dom @ dom') [] subst in [ Node ([loc], Id name, terms) ]))*) - [ Node ([loc], Id (name,x), []) ]) + [ Node ([loc], Id name, []) ]) | Ast.NRef _ -> [] | Ast.NCic _ -> [] | Ast.Implicit _ -> [] - | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ] + | Ast.Num (num, i) -> [ Node ([loc], Num, []) ] | Ast.Meta (index, local_context) -> List.fold_left (fun dom term -> dom @ domain_of_term_option ~loc ~context term) @@ -374,18 +398,19 @@ let domain_of_obj ~context obj = uniq_domain (domain_of_obj ~context obj) (* dom1 \ dom2 *) +(* XXX: possibly should take into account locs? *) let domain_diff dom1 dom2 = (* let domain_diff = Domain.diff *) let is_in_dom2 elt = List.exists (function - | Symbol (symb,None) -> + | Symbol symb -> (match elt with - Symbol (symb',_) when symb = symb' -> true + Symbol symb' when symb = symb' -> true | _ -> false) - | Num _ -> + | Num -> (match elt with - Num _ -> true + Num -> true | _ -> false) | item -> elt = item ) dom2 @@ -432,6 +457,11 @@ let letrecaux_split ctx (args,f,bo,n) = [(fun x -> ctx (args,f,x,n)),bo] ;; +let mk_ident s = function +| None -> Ast.Ident (s,`Ambiguous) +| Some u -> Ast.Ident (s,`Uri (NReference.string_of_reference u)) +;; + (* splits a pattern (for case analysis) *) let pattern_split ctx = function | Ast.Wildcard -> [] @@ -442,122 +472,115 @@ let pattern_split ctx = function ((fun v -> ctx (Ast.Pattern (s,href,pre@(x,Some v)::post'))),y) ::auxpatt (pre@[x']) post' | (x,None as x')::post' -> auxpatt (pre@[x']) post' - in auxpatt [] pl + in + ((fun x -> + let id0, href0 = + match x with + | Ast.Ident (id,`Ambiguous) -> id, None + | Ast.Ident (id,`Uri u) -> id, Some u + | _ -> assert false + in + let href0 = HExtlib.map_option NReference.reference_of_string href0 + in ctx (Ast.Pattern (id0,href0,pl))), + mk_ident s href)::auxpatt [] pl ;; (* 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 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)); *) - prerr_endline ("t0 = " ^ pp_term t0); - if test t0 then (prerr_endline "caso 1"; Some hd) + debug_print (lazy ("visiting t0 = " ^ pp_term t0)); + if test t0 then (debug_print (lazy "t0 is ambiguous"); Some hd) else - let t0' = split ctx0 t0 in - (prerr_endline ("caso 2: length t0' = " ^ string_of_int - (List.length t0')); aux (tl@t0' (*split ctx0 t0*))) + (* + (prerr_endline ("splitting not ambiguous t0:"); + let t0' = split ctx0 t0 in + List.iter (fun (ctx',t') -> prerr_endline ("-- subnode " ^ + (pp_term t'))) t0'; + aux (tl@t0')) *) + let t0' = split loc ctx0 t0 in + aux (tl@t0') (* in aux [(fun x -> x),t] *) in aux (top_split 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 rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library t = - let mk_alias = function - | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None) - | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None) - | Ast.Num _ -> DisambiguateTypes.Num None - | _ -> assert false - in - let lookup_choices = - fun item -> - (*match universe with - | None -> - lookup_in_library - interactive_user_uri_choice - input_or_locate_uri item - | Some e -> - (try Environment.find item e - with Not_found -> []) -*) - (try Environment.find item universe - with Not_found -> []) - in - match t with - | Ast.Ident (_,None) - | Ast.Num (_,None) - | Ast.Symbol (_,None) -> - let choices = lookup_choices (mk_alias t) in - if List.length choices <> 1 then t - else List.hd choices - (* but we lose info on closedness *) - | t -> Ast.map (initialize_ast ~universe ~lookup_in_library) 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,None) - | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None) - | Ast.Num (n,_) -> DisambiguateTypes.Num None - | Ast.Case(_,Some (ityname,_),_,_) -> DisambiguateTypes.Id (ityname,None) + | Ast.Ident (id,_) -> DisambiguateTypes.Id id + | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol sym + | Ast.Num (n,_) -> DisambiguateTypes.Num + | Ast.Case(_,Some (ityname,_),_,_) -> DisambiguateTypes.Id ityname | _ -> assert false ;; @@ -570,80 +593,88 @@ let ast_of_alias_spec t alias = match (t,alias) with | _ -> assert false ;; -let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri +(* 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 let localization_tbl = mk_localization_tbl 503 in let cic_thing = - interpretate_thing ~context ~env + interpretate_thing ~context ~env ~universe ~uri ~is_path:false t ~localization_tbl in let foo () = refine_thing metasenv subst context uri ~use_coercions cic_thing expty ugraph ~localization_tbl in match (refine_profiler.HExtlib.profile foo ()) with - | Ko _ -> false - | _ -> true + | Ko x -> + let loc,err = Lazy.force x in + debug_print (lazy ("test_interpr error: " ^ err)); + 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 ~mk_localization_tbl ~pp_thing ~pp_term in let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty - ~env ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl + ~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl in let find_choices item = let a2s = function - | GrafiteAst.Ident_alias (id,_) - | GrafiteAst.Symbol_alias (id,_,_) -> id - | GrafiteAst.Number_alias _ -> "NUM" + | GrafiteAst.Ident_alias (_id,uri) -> uri + | GrafiteAst.Symbol_alias (_id,_,desc) -> desc + | GrafiteAst.Number_alias (_,desc) -> desc in let d2s = function - | Id (id,_) - | Symbol (id,_) -> id - | Num _ -> "NUM" + | Id id + | Symbol id -> id + | Num -> "NUM" in let res = Environment.find item universe in - prerr_endline (Printf.sprintf "choices for %s :\n%s" - (d2s item) (String.concat ", " (List.map a2s res))); + debug_print (lazy (Printf.sprintf "choices for %s :\n%s" + (d2s item) (String.concat ", " (List.map a2s res)))); res in 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 -> - prerr_endline ("disambiguation of t0 = " ^ pp_thing t0); + | [] -> [], errors + | _ -> + (* debug_print (lazy ("disambiguate_list: t0 = " ^ pp_thing t0)); *) let is_ambiguous = function | Ast.Ident (_,`Ambiguous) | Ast.Num (_,None) | Ast.Symbol (_,None) -> true - | Ast.Case (_,Some (ity,None),_,_) -> - (prerr_endline ("ambiguous case" ^ ity);true) - | Ast.Case (_,None,_,_) -> prerr_endline "amb1";false - | Ast.Case (_,Some (ity,Some r),_,_) -> - (prerr_endline ("amb2 " ^ NReference.string_of_reference r);false) - | Ast.Ident (n,`Uri u) -> - (prerr_endline ("uri " ^ u ^ "inside IDENT " ^ n) ;false ) + | Ast.Case (_,Some (ity,None),_,_) -> true | _ -> false in let astpp = function @@ -652,409 +683,111 @@ 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 -> - prerr_endline ("not ambiguous:\n" ^ pp_thing t0); - Some (t0,tl) - | Some (ctx, t) -> - prerr_endline ("disambiguating node " ^ astpp t ^ - "\nin " ^ pp_thing (ctx t)); - (* get possible instantiations of t *) - let instances = get_instances ctx t in - (* perforate ambiguous subterms and test refinement *) - let survivors = List.filter test_interpr instances in - 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) -(* let rec aux l = - match l with - | [] -> None - | (ctx,u)::vl -> - if test u - then (ctx,u) - else aux (vl@split ctx u) - in aux [t] -;;*) - -(* let rec instantiate_ast = function - | Ident (n,Some _) - | Symbol (s,Some _) - | Num (n,Some _) as t -> [] - | Ident (n,None) -> (* output: all possible instantiations of n *) - | Symbol (s,None) -> - | Num (n,None) -> - - - | AttributedTerm (a,u) -> AttributedTerm (a,f u) - | Appl tl -> Appl (List.map f tl) - | Binder (k,n,body) -> Binder (k,n,f body) - | Case (t,ity,oty,pl) -> - let pl' = List.map (fun (p,u) -> p,f u) pl in - Case (f t,ity,map_option f oty,pl') - | Cast (u,v) -> Cast (f u,f v) - | LetIn (n,u,v) -> LetIn (n,f u,f v) - | LetRec -> ada (* TODO *) - | t -> 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) = -(* XXX: will be thrown away *) - let todo_dom = domain_of_thing ~context:(string_context_of_context context) thing - in - let rec aux_env env = function - | [] -> env - | Node (_, item, l) :: tl -> - let env = - Environment.add item - (mk_implicit - (match item with | Id _ | Num _ -> true | Symbol _ -> false)) - env in - aux_env (aux_env env l) tl in - let env = aux_env aliases todo_dom in + let env = aliases in let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty - ~env ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl + ~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 - match refine_thing metasenv subst context uri - ~use_coercions - (interpretate_thing ~context ~env ~uri ~is_path:false t ~localization_tbl) - expty base_univ ~localization_tbl with - | Ok (t',m',s',u') -> ([]:(Environment.key * 'f) list),m',s',t',u' - | Uncertain x -> - let _,err = Lazy.force x in - prerr_endline ("refinement uncertain after disambiguation: " ^ err); - assert false - | _ -> assert false + debug_print (lazy "before interpretate_thing"); + let t' = + interpretate_thing ~context ~env ~universe ~uri ~is_path:false t ~localization_tbl + in + debug_print (lazy "after interpretate_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 | Ko x -> + let loc,err = Lazy.force x in + debug_print (lazy ("refinement uncertain after disambiguation: " ^ err)); + raise (NoWellTypedInterpretation (loc,err)) in - if not (test_interpr thing) then raise (NoWellTypedInterpretation (0,[])) - else - let res = aux [thing] in - let res = - HExtlib.filter_map (fun t -> try Some (refine t) with _ -> 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 - match res with - | [] -> raise (NoWellTypedInterpretation (0,[])) - | [t] -> res,false - | _ -> res,true + let errors = + if inner_errors <> [] then (inner_errors,Stdpp.dummy_loc)::errors + else errors + in + (match res with + | [] -> prerr_endline ((string_of_int (List.length errors)) ^ " error frames");Disamb_failure errors + | _ -> Disamb_success res) ;; -(* -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 ~domain_of_thing ~interpretate_thing ~refine_thing - ~mk_localization_tbl - (thing_txt,thing_txt_prefix_len,thing) -= - debug_print (lazy "DISAMBIGUATE INPUT"); - debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); - let thing_dom = - domain_of_thing ~context:(string_context_of_context context) thing in - debug_print - (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom))); - let current_dom = - Environment.fold (fun item _ dom -> item :: dom) aliases [] in - let todo_dom = domain_diff thing_dom current_dom in - debug_print - (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom))); - (* (2) lookup function for any item (Id/Symbol/Num) *) - let lookup_choices = - fun item -> - match universe with - | None -> - lookup_in_library - interactive_user_uri_choice - input_or_locate_uri item - | Some e -> - (try - fix_instance item (Environment.find item e) - with Not_found -> []) - in - - (* items with 1 choice are interpreted ASAP *) - let aliases, todo_dom = - let rec aux (aliases,acc) = function - | [] -> aliases, acc - | (Node (_, item,extra) as node) :: tl -> - let choices = lookup_choices item in - if List.length choices <> 1 then aux (aliases, acc@[node]) tl - else - let tl = tl @ extra in - if Environment.mem item aliases then aux (aliases, acc) tl - else aux (Environment.add item (List.hd choices) aliases, acc) tl - in - aux (aliases,[]) todo_dom - in - -(* - (* *) - let _ = - if benchmark then begin - let per_item_choices = - List.map - (fun dom_item -> - try - let len = List.length (lookup_choices dom_item) in - debug_print (lazy (sprintf "BENCHMARK %s: %d" - (string_of_domain_item dom_item) len)); - len - with No_choices _ -> 0) - thing_dom - in - max_refinements := List.fold_left ( * ) 1 per_item_choices; - actual_refinements := 0; - domain_size := List.length thing_dom; - choices_avg := - (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size) - end - in - (* *) -*) - - (* (3) test an interpretation filling with meta uninterpreted identifiers - *) - let test_env aliases todo_dom ugraph = - try - let rec aux env = function - | [] -> env - | Node (_, item, l) :: tl -> - let env = - Environment.add item - (mk_implicit - (match item with | Id _ | Num _ -> true | Symbol _ -> false)) - env in - aux (aux env l) tl in - let filled_env = aux aliases todo_dom in - let localization_tbl = mk_localization_tbl 503 in - let cic_thing = - interpretate_thing ~context ~env:filled_env - ~uri ~is_path:false thing ~localization_tbl - in -let foo () = - refine_thing metasenv subst context uri - ~use_coercions cic_thing expty ugraph ~localization_tbl -in refine_profiler.HExtlib.profile foo () - with - | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) - | Invalid_choice loc_msg -> Ko loc_msg - in - (* (4) build all possible interpretations *) - let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in - (* aux returns triples Ok/Uncertain/Ko *) - (* rem_dom is the concatenation of all the remainin domains *) - let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom = - debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom)); - match todo_dom with - | [] -> - assert (lookup_in_todo_dom = None); - (match test_env aliases rem_dom base_univ with - | Ok (thing, metasenv,subst,new_univ) -> - [ aliases, diff, metasenv, subst, thing, new_univ ], [], [] - | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true] - | Uncertain loc_msg -> - [],[aliases,diff,loc_msg],[]) - | Node (locs,item,inner_dom) :: remaining_dom -> - debug_print (lazy (sprintf "CHOOSED ITEM: %s" - (string_of_domain_item item))); - let choices = - match lookup_in_todo_dom with - None -> lookup_choices item - | Some choices -> choices in - match choices with - [] -> - [], [], - [aliases, diff, - (lazy (List.hd locs, - "No choices for " ^ string_of_domain_item item)), - true] -(* - | [codomain_item] -> - (* just one choice. We perform a one-step look-up and - if the next set of choices is also a singleton we - skip this refinement step *) - debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); - let new_env = Environment.add item codomain_item aliases in - let new_diff = (item,codomain_item)::diff in - let lookup_in_todo_dom,next_choice_is_single = - match remaining_dom with - [] -> None,false - | (_,he)::_ -> - let choices = lookup_choices he in - Some choices,List.length choices = 1 - in - if next_choice_is_single then - aux new_env new_diff lookup_in_todo_dom remaining_dom - base_univ - else - (match test_env new_env remaining_dom base_univ with - | Ok (thing, metasenv),new_univ -> - (match remaining_dom with - | [] -> - [ new_env, new_diff, metasenv, thing, new_univ ], [] - | _ -> - aux new_env new_diff lookup_in_todo_dom - remaining_dom new_univ) - | Uncertain (loc,msg),new_univ -> - (match remaining_dom with - | [] -> [], [new_env,new_diff,loc,msg,true] - | _ -> - aux new_env new_diff lookup_in_todo_dom - remaining_dom new_univ) - | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true]) -*) - | _::_ -> - let mark_not_significant failures = - List.map - (fun (env, diff, loc_msg, _b) -> - env, diff, loc_msg, false) - failures in - let classify_errors ((ok_l,uncertain_l,error_l) as outcome) = - if ok_l <> [] || uncertain_l <> [] then - ok_l,uncertain_l,mark_not_significant error_l - else - outcome in - let rec filter = function - | [] -> [],[],[] - | codomain_item :: tl -> - (*debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));*) - let new_env = Environment.add item codomain_item aliases in - let new_diff = (item,codomain_item)::diff in - (match - test_env new_env - (inner_dom@remaining_dom@rem_dom) base_univ - with - | Ok (thing, metasenv,subst,new_univ) -> -(* prerr_endline "OK"; *) - let res = - (match inner_dom with - | [] -> - [new_env,new_diff,metasenv,subst,thing,new_univ], - [], [] - | _ -> - aux new_env new_diff None inner_dom - (remaining_dom@rem_dom) - ) - in - res @@ filter tl - | Uncertain loc_msg -> -(* prerr_endline ("UNCERTAIN"); *) - let res = - (match inner_dom with - | [] -> [],[new_env,new_diff,loc_msg],[] - | _ -> - aux new_env new_diff None inner_dom - (remaining_dom@rem_dom) - ) - in - res @@ filter tl - | Ko loc_msg -> -(* prerr_endline "KO"; *) - let res = [],[],[new_env,new_diff,loc_msg,true] in - res @@ filter tl) - in - let ok_l,uncertain_l,error_l = - classify_errors (filter choices) - in - let res_after_ok_l = - List.fold_right - (fun (env,diff,_,_,_,_) res -> - aux env diff None remaining_dom rem_dom @@ res - ) ok_l ([],[],error_l) - in - List.fold_right - (fun (env,diff,_) res -> - aux env diff None remaining_dom rem_dom @@ res - ) uncertain_l res_after_ok_l - in - let aux' aliases diff lookup_in_todo_dom todo_dom = - if todo_dom = [] then - aux aliases diff lookup_in_todo_dom todo_dom [] - else - match test_env aliases todo_dom base_univ with - | Ok _ - | Uncertain _ -> - aux aliases diff lookup_in_todo_dom todo_dom [] - | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] - in - let res = - match aux' aliases [] None todo_dom with - | [],uncertain,errors -> - let errors = - List.map - (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true) - ) uncertain @ errors - in - let errors = - List.map - (fun (env,diff,loc_msg,significant) -> - let env' = - filter_map_domain - (fun locs domain_item -> - try - let description = - description_of_alias (Environment.find domain_item env) - in - Some (locs,descr_of_domain_item domain_item,description) - with - Not_found -> None) - thing_dom - in - let diff= List.map (fun a,b -> a,description_of_alias b) diff in - env',diff,loc_msg,significant - ) errors - in - raise (NoWellTypedInterpretation (0,errors)) - | [_,diff,metasenv,subst,t,ugraph],_,_ -> - debug_print (lazy "SINGLE INTERPRETATION"); - [diff,metasenv,subst,t,ugraph], false - | l,_,_ -> - debug_print - (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); - let choices = - List.map - (fun (env, _, _, _, _, _) -> - map_domain - (fun locs domain_item -> - let description = - description_of_alias (Environment.find domain_item env) - in - locs,descr_of_domain_item domain_item, description) - thing_dom) - l - in - let choosed = - interactive_interpretation_choice - thing_txt thing_txt_prefix_len choices - in - (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u) - choosed), - true - in - res - *)