PACKAGE = disambiguation
INTERFACE_FILES = \
disambiguateTypes.mli \
- disambiguate.mli \
- multiPassDisambiguator.mli
+ disambiguate.mli
IMPLEMENTATION_FILES = \
$(patsubst %.mli, %.ml, $(INTERFACE_FILES))
module Ast = NotationPt
+(* hard errors, spurious errors *)
exception NoWellTypedInterpretation of
- int *
- ((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * string) list *
- (Stdpp.location * string) Lazy.t * bool) list
+ ((Stdpp.location * string) list *
+ (Stdpp.location * string) list)
+
exception PathNotWellFormed
(** raised when an environment is not enough informative to decide *)
| 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
+ (* hard errors, spurious errors *)
+ (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list *
+ (('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 *)
) [] 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); []
;;
(* 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)
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)
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
| _ -> 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
~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 Some (loc,err)
+ | _ -> 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
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)
| 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
+ 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)
=
~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");
assert false
| _ -> assert false
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)
+ 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 =
+ HExtlib.filter_map (fun t ->
+ try Some (refine t)
with _ ->
- debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));None) res
+(* debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));*)
+ None) res
in
- match res with
- | [] -> raise (NoWellTypedInterpretation (0,[]))
- (* XXX : the boolean seems not to play a role any longer *)
- | [t] -> res,false
- | _ -> res, true
- (* 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
+ | [] -> Disamb_failure (errors,[])
+ | _ -> Disamb_success res)
;;
(** {2 Disambiguation interface} *)
-(* the integer is an offset to be added to each location *)
-(* list of located error messages, each list is a tuple:
- * - environment in string form
- * - environment patch
- * - location
- * - error message
- * - significancy of the error message, if false the error is likely to be
- * useless for the final user ... *)
+type ('alias,'ast_thing,'metasenv,'subst,'thing,'ugraph) disamb_result =
+ | Disamb_success of ('ast_thing * 'metasenv * 'subst * 'thing * 'ugraph) list
+ | Disamb_failure of
+ (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list *
+ (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list
+
exception NoWellTypedInterpretation of
- int *
- ((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * string) list *
- (Stdpp.location * string) Lazy.t *
- bool) list
+ ((Stdpp.location * string) list *
+ (Stdpp.location * string) list)
+
exception PathNotWellFormed
type 'a disambiguator_input = string * int * 'a
('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
visit:(pp_term:(NotationPt.term -> string) ->
(NotationPt.term -> bool) -> 'ast_thing ->
- ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) ->
+ ((NotationPt.term -> 'ast_thing) * NotationPt.term * Stdpp.location) option) ->
mk_localization_tbl:(int -> 'cichash) ->
'ast_thing disambiguator_input ->
- ('ast_thing * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool
+ (GrafiteAst.alias_spec,'ast_thing,'metasenv,'subst,'refined_thing,'ugraph) disamb_result
+
+type 'ast marked_ast =
+ (NotationPt.term -> 'ast) * NotationPt.term * Stdpp.location
val bfvisit :
pp_term:(NotationPt.term -> string) ->
(NotationPt.term -> bool) ->
- NotationPt.term -> ((NotationPt.term -> NotationPt.term) * NotationPt.term) option
+ NotationPt.term -> (NotationPt.term marked_ast) option
val bfvisit_obj :
pp_term:(NotationPt.term -> string) ->
(NotationPt.term -> bool) ->
- NotationPt.term NotationPt.obj -> ((NotationPt.term -> NotationPt.term NotationPt.obj) * NotationPt.term) option
+ NotationPt.term NotationPt.obj ->
+ ((NotationPt.term NotationPt.obj) marked_ast) option
disambiguate_thing ~description_of_alias ~passes ~aliases
~universe ~visit ~f thing
*)
- try
+ match
Disambiguate.disambiguate_thing
~context ~metasenv ~subst ~use_coercions:true ~string_context_of_context
~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~fix_instance
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~visit
~mk_localization_tbl ~pp_term thing
with
- | Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
- raise (DisambiguationError (offset, [newerrors]))
+ | Disambiguate.Disamb_success res -> res
+ | Disambiguate.Disamb_failure (herrors, serrors) ->
+ (* temporary *)
+ let offset = 0 in
+ raise (DisambiguationError (offset, newerrors))
else
nstatus
with
- | MultiPassDisambiguator.DisambiguationError _
+ | GrafiteDisambiguate.Error _
| NCicTypeChecker.TypeCheckerFailure _ ->
(*HLog.warn "error in generating projection/eliminator";*)
status
status (name,t,cpos,arity) in
let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in
eval_alias status (mode,aliases)
- with MultiPassDisambiguator.DisambiguationError _->
+ with GrafiteDisambiguate.Error _ ->
HLog.warn ("error in generating coercion: "^name);
status)
status coercions
List.fold_left
(fun status tac ->
let status = eval_ng_tac (text,prefix_len,tac) status in
+ prerr_endline "prima di subst_metasenv_and_fix_names";
subst_metasenv_and_fix_names status)
status tacl
in
with
| NCicUnification.UnificationFailure _
| NCicUnification.Uncertain _
- | MultiPassDisambiguator.DisambiguationError _ ->
+ | GrafiteDisambiguate.Error _ ->
raise (GrafiteTypes.Command_error "bad source pattern"))
| _ -> assert false
in
(* 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.InterprEnv.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
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 choices, _ = NCicDisambiguate.disambiguate_term
+ let _,_,thing' = thing in
+ match NCicDisambiguate.disambiguate_term
status
~aliases:status#disambiguate_db.interpr
~expty
~mk_implicit ~fix_instance
~description_of_alias:GrafiteAst.description_of_alias
~context ~metasenv ~subst thing
- in
- let _,_,thing' = thing in
- match choices with
- | [newast, metasenv, subst, cic] ->
+ 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
- | [] -> assert false
- | _ ->
+ | Disambiguate.Disamb_success (_::_ as choices) ->
let diffs =
- List.map (fun (ast,_,_,_) ->
+ List.map (fun (ast,_,_,_,_) ->
diff_term Stdpp.dummy_loc thing' ast) choices
- in
- raise (Ambiguous_input (find_diffs diffs))
+ 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 =
NUri.uri_of_string (baseuri ^ "/" ^ name)
in
- let choices, _ = NCicDisambiguate.disambiguate_obj
+ match NCicDisambiguate.disambiguate_obj
status
~lookup_in_library:(nlookup_in_library status)
~description_of_alias:GrafiteAst.description_of_alias
~aliases:status#disambiguate_db.interpr
~universe:(status#disambiguate_db.multi_aliases)
obj'
- in
- match choices with
- | [ast, _, _, cic] ->
- let diff = diff_obj Stdpp.dummy_loc obj ast in
- let status = add_to_interpr status diff
- in
- status, cic
- | [] -> assert false
- | _ ->
+ 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,_,_,_) ->
+ List.map (fun (ast,_,_,_,_) ->
diff_obj Stdpp.dummy_loc obj ast) choices
in
- raise (Ambiguous_input (find_diffs diffs))
+ 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 =
method set_disambiguate_status: #g_status -> 'self
end
-(* val eval_with_new_aliases:
+(* 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
+
+ (* val eval_with_new_aliases:
#status as 'status -> ('status -> 'a) ->
((Stdpp.location * DisambiguateTypes.domain_item) * GrafiteAst.alias_spec) list * 'a
*)
let _ = (aliases : GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t) in
let local_names = List.map (fun (n,_) -> n) context in
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
- let res,b =
- MultiPassDisambiguator.disambiguate_thing
- ~freshen_thing:NotationUtil.freshen_term
- ~context ~metasenv ~initial_ugraph:() ~aliases
- ~mk_implicit ~description_of_alias ~fix_instance
+ Disambiguate.disambiguate_thing
+ ~context ~metasenv ~subst ~use_coercions:true
~string_context_of_context:(List.map (fun (x,_) -> Some x))
- ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status)
- ~passes:(MultiPassDisambiguator.passes ())
- ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
+ ~initial_ugraph:() ~expty
+ ~mk_implicit ~description_of_alias ~fix_instance ~aliases
+ ~universe ~lookup_in_library
+ ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status)
+ ~domain_of_thing:Disambiguate.domain_of_term
~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
~refine_thing:(refine_term status)
(text,prefix_len,
(initialize_ast ~universe ~lookup_in_library ~local_names term))
~visit:Disambiguate.bfvisit
- ~mk_localization_tbl ~expty ~subst
- in
- List.map (function (t,a,b,c,_) -> t,a,b,c) res, b
+ ~mk_localization_tbl
;;
-
let disambiguate_obj (status: #NCicCoercion.status)
~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
=
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
- let res,b =
- let obj' = initialize_obj ~universe ~lookup_in_library obj in
- MultiPassDisambiguator.disambiguate_thing
- ~freshen_thing:NotationUtil.freshen_obj
- ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
- ~mk_implicit ~description_of_alias ~fix_instance
+ let obj' = initialize_obj ~universe ~lookup_in_library obj in
+ Disambiguate.disambiguate_thing
+ ~context:[] ~metasenv:[] ~subst:[] ~use_coercions:true
~string_context_of_context:(List.map (fun (x,_) -> Some x))
- ~universe
- ~uri:(Some uri)
- ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status)) ~pp_term:(NotationPp.pp_term status)
- ~passes:(MultiPassDisambiguator.passes ())
- ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
+ ~initial_ugraph:() ~expty:None
+ ~mk_implicit ~description_of_alias ~fix_instance ~aliases
+ ~universe ~lookup_in_library
+ ~uri:(Some uri) ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status))
+ ~pp_term:(NotationPp.pp_term status)
+ ~domain_of_thing:Disambiguate.domain_of_obj
~interpretate_thing:(interpretate_obj status ~mk_choice)
~refine_thing:(refine_obj status)
(text,prefix_len,obj')
~visit:Disambiguate.bfvisit_obj
- ~mk_localization_tbl ~expty:None
- in
- List.map (function (o,a,b,c,_) -> o,a,b,c) res, b
+ ~mk_localization_tbl
;;
(*
let _ =
DisambiguateTypes.Environment.key ->
GrafiteAst.alias_spec list) ->
NotationPt.term Disambiguate.disambiguator_input ->
- (NotationPt.term *
- NCic.metasenv *
- NCic.substitution *
- NCic.term) list *
- bool
+ (GrafiteAst.alias_spec,NotationPt.term,NCic.metasenv,NCic.substitution,NCic.term,unit) Disambiguate.disamb_result
val disambiguate_obj :
#NCicCoercion.status ->
GrafiteAst.alias_spec list) ->
uri:NUri.uri ->
string * int * NotationPt.term NotationPt.obj ->
- (NotationPt.term NotationPt.obj *
- NCic.metasenv *
- NCic.substitution * NCic.obj)
- list * bool
+ (GrafiteAst.alias_spec,NotationPt.term NotationPt.obj,NCic.metasenv,NCic.substitution,NCic.obj,unit) Disambiguate.disamb_result
val disambiguate_path: #NCicEnvironment.status -> NotationPt.term -> NCic.term
let wrap fname f x =
try f x
with
- | MultiPassDisambiguator.DisambiguationError _
+ | GrafiteDisambiguate.Error _
| NCicRefiner.RefineFailure _
| NCicUnification.UnificationFailure _
| NCicTypeChecker.TypeCheckerFailure _
predefined_virtuals.mli \
matitaMathView.mli \
matitaScript.mli \
- matitaGui.mli \
$(NULL)
CMLI = \
matitaTypes.mli \
cicMathView.ml \
matitadaemon.ml \
matitaGtkMisc.ml \
- matita.ml \
virtuals.ml \
lablGraphviz.ml \
matitaEngine.ml \
ALL_SYNTAX_MLI = matitaScriptLexer.mli
PROGRAMS_BYTE = \
- matita matitac matitadaemon matitaclean
+ matitac matitadaemon matitaclean
PROGRAMS = $(PROGRAMS_BYTE)
PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE))
NOINST_PROGRAMS =
$(H)ln -sf matitac.opt matitac
linkonly:
- $(H)echo " OCAMLC matita.ml"
- $(H)$(OCAMLC) $(PKGS) -linkpkg -o matita $(CMOS) $(OCAML_DEBUG_FLAGS) matita.ml
$(H)echo " OCAMLC matitac.ml"
$(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitac.ml
$(H)echo " OCAMLC matitadaemon.ml"
None, "NTactic error: " ^ Lazy.force msg
| NTacStatus.Error (msg,Some exn) ->
None, "NTactic error: " ^ Lazy.force msg ^ "\n" ^ snd(to_string exn)
- | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
+(* | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
let loc =
match errorll with
| ((_,_,loc_msg,_)::_)::_ ->
in
loc,
"********** DISAMBIGUATION ERRORS: **********\n" ^
- explain (aux errorll)
+ explain (aux errorll) *)
| exn -> None, "Uncaught exception: " ^ Printexc.to_string exn
("Do not catch top-level exception "
^ "(useful for backtrace inspection)");
"-onepass",
- Arg.Unit (fun () -> MultiPassDisambiguator.only_one_pass := true),
+ Arg.Unit (fun () -> () (* MultiPassDisambiguator.only_one_pass := true *)),
"Enable only one disambiguation pass";
]
else []
HExtlib.Localized (floc, exn) ->
HExtlib.raise_localized_exception
~offset:(MatitaGtkMisc.utf8_string_length parsed_text) floc exn
- | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
+ (* | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
raise
(MultiPassDisambiguator.DisambiguationError
- (offset+parsed_text_length, errorll))
+ (offset+parsed_text_length, errorll)) *)
in
assert (text=""); (* no macros inside comments, please! *)
let st,text = s in
open Http_types;;
exception Emphasized_error of string
-exception Ambiguous of string
+exception Disamb_error of string
module Stack = Continuationals.Stack
cgi#out_channel#commit_work()
;;
+let xml_of_disamb_error l =
+ let mk_alias = function
+ | GrafiteAst.Ident_alias (_,uri) -> "href=\"" ^ uri ^ "\""
+ | GrafiteAst.Symbol_alias (_,uri,desc)
+ | GrafiteAst.Number_alias (uri,desc) ->
+ let uri = try HExtlib.unopt uri with _ -> "cic:/fakeuri.def(1)" in
+ "href=\"" ^ uri ^ "\" title=\"" ^
+ (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
+ ^ "\""
+ in
+
+ let mk_interpr (loc,a) =
+ let x,y = HExtlib.loc_of_floc loc in
+ Printf.sprintf "<interpretation start=\"%d\" stop=\"%d\" %s />"
+ x y (mk_alias a)
+ in
+
+ let mk_failure (il,loc,msg) =
+ let x,y = HExtlib.loc_of_floc loc in
+ Printf.sprintf "<failure start=\"%d\" stop=\"%d\" title=\"%s\">%s</failure>"
+ x y (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () msg)
+ (String.concat "" (List.map mk_interpr il))
+ in
+
+ let mk_choice (a,fl) =
+ let fl' = String.concat "" (List.map mk_failure fl) in
+ match a with
+ | None -> "<choice>" ^ fl' ^ "</choice>"
+ | Some a -> Printf.sprintf "<choice %s>%s</choice>" (mk_alias a) fl'
+ in
+
+ let mk_located (loc,cl) =
+ let x,y = HExtlib.loc_of_floc loc in
+ Printf.sprintf "<choicepoint start=\"%d\" stop=\"%d\">%s</choicepoint>"
+ x y (String.concat "" (List.map mk_choice cl))
+ in
+ "<disamberror>" ^ (String.concat "" (List.map mk_located l)) ^ "</disamberror>"
+;;
+
let advance0 sid text =
let status = MatitaAuthentication.get_status sid in
let history = MatitaAuthentication.get_history sid in
*)
let strchoices = Printf.sprintf
"<ambiguity start=\"%d\" stop=\"%d\">%s</ambiguity>" x y strchoices
- in raise (Ambiguous strchoices)
+ in raise (Disamb_error strchoices)
+ | GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l))
(* | End_of_file -> ... *)
in
MatitaAuthentication.set_status sid st;
~content_type:"text/xml; charset=\"utf-8\""
();
cgi#out_channel#output_string body
- | Ambiguous text ->
+ | Disamb_error text ->
let body = "<response>" ^ text ^ "</response>" in
cgi # set_header
~cache:`No_cache
let error_msg = function
| Emphasized_error text -> "<localized>" ^ text ^ "</localized>"
- | Ambiguous text -> (* <ambiguity> *) text
+ | Disamb_error text -> text
| End_of_file _ -> (* not an error *) ""
| e -> (* unmanaged error *)
"<error>" ^
if (is_defined(xml)) {
var parsed = xml.getElementsByTagName("parsed")[0];
var ambiguity = xml.getElementsByTagName("ambiguity")[0];
+ var disamberr = xml.getElementsByTagName("disamberror")[0];
if (is_defined(parsed)) {
// debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
var len = parseInt(parsed.getAttribute("length"));
matita.disambMode = true;
updateSide();
}
+ else if (is_defined(disamberr)) {
+ set_cps(disamberr.childNodes);
+ matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
+ matita.disambMode = true;
+ disable_toparea();
+ next_cp(0);
+ }
else {
var error = xml.getElementsByTagName("error")[0];
unlocked.innerHTML = error.childNodes[0].wholeText;
}
+// get or set <choicepoint>'s (in case of disamb error)
+function get_cps() {
+ return matita.choicepoints
+}
+
+function set_cps(cps) {
+ matita.choicepoints = cps;
+}
+
+// get radio buttons for <choice>'s in a given cp
+function get_choice_opts(i) {
+ var res = [];
+ var choices = get_cps()[i].childNodes;
+ for (var j = 0;j < choices.length;j++) {
+ var href = choices[j].getAttribute("href");
+ var title = choices[j].getAttribute("title");
+ var desc;
+ if (is_defined(title)) {
+ desc = title;
+ } else {
+ desc = href;
+ }
+
+ res[j] = document.createElement("input");
+ res[j].setAttribute("type","radio");
+ res[j].setAttribute("name","choice");
+ res[j].setAttribute("choicepointno",i);
+ res[j].setAttribute("choiceno",j);
+ res[j].setAttribute("href",href);
+ res[j].setAttribute("title",title);
+ res[j].setAttribute("desc",desc);
+
+ if (j == 0) res[j].setAttribute("checked","");
+ }
+ return res;
+}
+
+// get radio buttons for <failure>'s in a given choice
+function get_failure_opts(i,j) {
+ var res = [];
+ var failures = get_cps()[i].childNodes[j].childNodes;
+ for (var k = 0;k < failures.length;k++) {
+ var start = failures[k].getAttribute("start");
+ var stop = failures[k].getAttribute("stop");
+ var title = failures[k].getAttribute("title");
+
+ res[k] = document.createElement("input");
+ res[k].setAttribute("type","radio");
+ res[k].setAttribute("name","failure");
+ res[k].setAttribute("choicepointno",i);
+ res[k].setAttribute("choiceno",j);
+ res[k].setAttribute("failureno",k);
+ res[k].setAttribute("start",start);
+ res[k].setAttribute("stop",stop);
+ res[k].setAttribute("title",title);
+
+ if (k == 0) res[k].setAttribute("checked","");
+ }
+ return res;
+}
+
+function next_cp(curcp) {
+ var cp = get_cps()[curcp];
+ var start = parseInt(cp.getAttribute("start"));
+ var stop = parseInt(cp.getAttribute("stop"));
+
+ matita.errorStart = start;
+ matita.errorStop = stop;
+ // matita.unlockedbackup = unlocked.innerHTML.html_to_matita();
+
+ var unlockedtxt = matita.unlockedbackup;
+ var pre = unlockedtxt.substring(0,start).matita_to_html();
+ var mid = unlockedtxt.substring(start,stop).matita_to_html();
+ var post = unlockedtxt.substring(stop).matita_to_html();
+ unlocked.innerHTML = pre +
+ "<span class=\"error\" title=\"disambiguation failed\">" +
+ mid + "</span>" + post;
+
+ var title = "<H3>Disambiguation failed</H3>";
+ disambcell.innerHTML = title;
+ var choices = get_choice_opts(curcp);
+ for (var i = 0;i < choices.length;i++) {
+ disambcell.appendChild(choices[i]);
+ disambcell.appendChild(document.createTextNode(choices[i].getAttribute("desc")));
+ disambcell.appendChild(document.createElement("br"));
+ }
+
+ // update index of the next choicepoint
+ new_curcp = (curcp + 1) % get_cps().length;
+
+ var okbutton = document.createElement("input");
+ okbutton.setAttribute("type","button");
+ okbutton.setAttribute("value","OK");
+ okbutton.setAttribute("onclick","show_failures()");
+ var cancelbutton = document.createElement("input");
+ cancelbutton.setAttribute("type","button");
+ cancelbutton.setAttribute("value","Close");
+ cancelbutton.setAttribute("onclick","cancel_disambiguate()");
+ var tryagainbutton = document.createElement("input");
+ tryagainbutton.setAttribute("type","button");
+ if (new_curcp > 0) {
+ tryagainbutton.setAttribute("value","Try something else");
+ } else {
+ tryagainbutton.setAttribute("value","Restart");
+ }
+ tryagainbutton.setAttribute("onclick","next_cp(" + new_curcp + ")");
+
+ disambcell.appendChild(okbutton);
+ disambcell.appendChild(tryagainbutton);
+ disambcell.appendChild(cancelbutton);
+
+ //disable_toparea();
+
+ //matita.disambMode = true;
+ updateSide();
+
+}
+
+function show_failures() {
+
+ var choice = document.getElementsByName("choice")[get_checked_index("choice")];
+ var cpno = parseInt(choice.getAttribute("choicepointno"));
+ var choiceno = parseInt(choice.getAttribute("choiceno"));
+ var choicedesc = choice.getAttribute("desc");
+
+ var title = "<H3>Disambiguation failed</H3>";
+ var subtitle = "<p>Errors at node " + choiceno + " = " + choicedesc + "</p>";
+
+ disambcell.innerHTML = title + subtitle;
+ var failures = get_failure_opts(cpno,choiceno);
+ for (var i = 0;i < failures.length;i++) {
+ disambcell.appendChild(failures[i]);
+ disambcell.appendChild(document.createTextNode(failures[i].getAttribute("title")));
+ disambcell.appendChild(document.createElement("br"));
+ }
+
+ var okbutton = document.createElement("input");
+ okbutton.setAttribute("type","button");
+ okbutton.setAttribute("value","Show error loc");
+ okbutton.setAttribute("onclick","show_err()");
+ var cancelbutton = document.createElement("input");
+ cancelbutton.setAttribute("type","button");
+ cancelbutton.setAttribute("value","Close");
+ cancelbutton.setAttribute("onclick","cancel_disambiguate()");
+ var backbutton = document.createElement("input");
+ backbutton.setAttribute("type","button");
+ backbutton.setAttribute("value","<< Back");
+ backbutton.setAttribute("onclick","next_cp(" + cpno + ")");
+
+ disambcell.appendChild(backbutton);
+ disambcell.appendChild(okbutton);
+ disambcell.appendChild(cancelbutton);
+
+}
+
+function show_err() {
+ var radios = document.getElementsByName("failure");
+ for (i = 0; i < radios.length; i++) {
+ if (radios[i].checked) {
+ var start = radios[i].getAttribute("start");
+ var stop = radios[i].getAttribute("stop");
+ var title = radios[i].getAttribute("title");
+ var unlockedtxt = matita.unlockedbackup;
+ var pre = unlockedtxt.substring(0,start).matita_to_html();
+ var mid = unlockedtxt.substring(start,stop).matita_to_html();
+ var post = unlockedtxt.substring(stop).matita_to_html();
+ unlocked.innerHTML = pre +
+ "<span class=\"error\" title=\"Disambiguation failure\">" +
+ mid + "</span>" + post;
+ break;
+ }
+ }
+}
+
function gotoBottom()
{
processor = function(xml) {
}
}
+function do_showerror() {
+ var i = get_checked_index("choice");
+ if (i != null) {
+ var pre = matita.unlockedbackup
+ .substring(0,matita.ambiguityStart).matita_to_html();
+ var mid = matita.unlockedbackup
+ .substring(matita.ambiguityStart,matita.ambiguityStop)
+ .matita_to_html();
+ var post = matita.unlockedbackup
+ .substring(matita.ambiguityStop).matita_to_html();
+
+ var href = matita.interpretations[i].href;
+ var title = matita.interpretations[i].title;
+
+ if (is_defined(title)) {
+ mid = "<A href=\"" + href + "\" title=\"" + title + "\">" + mid + "</A>";
+ } else {
+ mid = "<A href=\"" + href + "\">" + mid + "</A>";
+ }
+
+ unlocked.innerHTML = pre + mid + post;
+
+ }
+}
+
function readCookie(name) {
var nameEQ = name + "=";
var ca = document.cookie.split(';');
projects / helm.git / commitdiff