From 3323758b99384afb5c7a70aa31bc006a78af64dd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 27 Nov 2008 17:44:31 +0000 Subject: [PATCH] New modules stack: grafiteDisambiguator | cicDisambiguator | | multiPassDisambiagutor |disambiguate nCicDisambiguator| --- .../METAS/meta.helm-disambiguation.src | 4 + .../METAS/meta.helm-ng_disambiguation.src | 2 +- .../cic_disambiguation/cicDisambiguate.ml | 236 ++++++++---------- .../cic_disambiguation/cicDisambiguate.mli | 83 +++--- .../components/disambiguation/.depend | 10 + .../components/disambiguation/.depend.opt | 10 + .../components/disambiguation/Makefile | 6 +- .../components/disambiguation/disambiguate.ml | 62 +++-- .../disambiguation/disambiguate.mli | 17 +- .../multiPassDisambiguator.ml | 166 +++++------- .../multiPassDisambiguator.mli | 50 +++- .../grafite_parser/grafiteDisambiguate.ml | 6 +- .../components/ng_disambiguation/.depend | 6 +- .../components/ng_disambiguation/Makefile | 3 +- .../{nDisambiguate.ml => nCicDisambiguate.ml} | 76 +++--- ...Disambiguator.mli => nCicDisambiguate.mli} | 17 +- .../ng_disambiguation/nDisambiguate.mli | 39 --- .../nGrafiteDisambiguator.ml | 182 -------------- 18 files changed, 368 insertions(+), 607 deletions(-) create mode 100644 helm/software/components/METAS/meta.helm-disambiguation.src create mode 100644 helm/software/components/disambiguation/.depend create mode 100644 helm/software/components/disambiguation/.depend.opt rename helm/software/components/{grafite_parser => disambiguation}/multiPassDisambiguator.ml (62%) rename helm/software/components/{grafite_parser => disambiguation}/multiPassDisambiguator.mli (53%) rename helm/software/components/ng_disambiguation/{nDisambiguate.ml => nCicDisambiguate.ml} (91%) rename helm/software/components/ng_disambiguation/{nGrafiteDisambiguator.mli => nCicDisambiguate.mli} (76%) delete mode 100644 helm/software/components/ng_disambiguation/nDisambiguate.mli delete mode 100644 helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml diff --git a/helm/software/components/METAS/meta.helm-disambiguation.src b/helm/software/components/METAS/meta.helm-disambiguation.src new file mode 100644 index 000000000..706f6dd12 --- /dev/null +++ b/helm/software/components/METAS/meta.helm-disambiguation.src @@ -0,0 +1,4 @@ +requires="helm-acic_content" +version="0.0.1" +archive(byte)="disambiguation.cma" +archive(native)="disambiguation.cmxa" diff --git a/helm/software/components/METAS/meta.helm-ng_disambiguation.src b/helm/software/components/METAS/meta.helm-ng_disambiguation.src index 2fbadf445..59c5f5ec5 100644 --- a/helm/software/components/METAS/meta.helm-ng_disambiguation.src +++ b/helm/software/components/METAS/meta.helm-ng_disambiguation.src @@ -1,4 +1,4 @@ -requires="helm-whelp helm-acic_content helm-ng_refiner helm-cic_disambiguation" +requires="helm-whelp helm-acic_content helm-ng_refiner helm-disambiguation" version="0.0.1" archive(byte)="ng_disambiguation.cma" archive(native)="ng_disambiguation.cmxa" diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index a7e65bcfc..97f24c190 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -29,42 +29,60 @@ module Ast = CicNotationPt let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () -let refine_term metasenv subst context uri term ugraph ~localization_tbl = +let rec string_context_of_context = + List.map + (function + | Cic.Name n -> Some n + | Cic.Anonymous -> Some "_") +;; + +let refine_term metasenv subst context uri ~use_coercions + term ugraph ~localization_tbl = (* if benchmark then incr actual_refinements; *) assert (uri=None); - debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); - try - let term', _, metasenv',ugraph1 = - CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in - (Disambiguate.Ok (term', metasenv',[],ugraph1)) - with - exn -> - let rec process_exn loc = - function - HExtlib.Localized (loc,exn) -> process_exn loc exn - | CicRefine.Uncertain msg -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; - Disambiguate.Uncertain (lazy (loc,Lazy.force msg)) - | CicRefine.RefineFailure msg -> - debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) (Lazy.force msg))); - Disambiguate.Ko (lazy (loc,Lazy.force msg)) - | exn -> raise exn - in - process_exn Stdpp.dummy_loc exn + debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); + let saved_use_coercions = !CicRefine.insert_coercions in + try + CicRefine.insert_coercions := use_coercions; + let term', _, metasenv',ugraph1 = + CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl + in + CicRefine.insert_coercions := saved_use_coercions; + (Disambiguate.Ok (term', metasenv',[],ugraph1)) + with + exn -> + CicRefine.insert_coercions := saved_use_coercions; + let rec process_exn loc = + function + HExtlib.Localized (loc,exn) -> process_exn loc exn + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; + Disambiguate.Uncertain (lazy (loc,Lazy.force msg)) + | CicRefine.RefineFailure msg -> + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppterm term) (Lazy.force msg))); + Disambiguate.Ko (lazy (loc,Lazy.force msg)) + | exn -> raise exn + in + process_exn Stdpp.dummy_loc exn -let refine_obj metasenv subst context uri obj ugraph ~localization_tbl = +let refine_obj metasenv subst context uri ~use_coercions obj ugraph + ~localization_tbl = assert (context = []); assert (metasenv = []); assert (subst = []); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ; + let saved_use_coercions = !CicRefine.insert_coercions in try + CicRefine.insert_coercions := use_coercions; let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj ~localization_tbl in - (Disambiguate.Ok (obj', metasenv,[],ugraph)) + CicRefine.insert_coercions := saved_use_coercions; + (Disambiguate.Ok (obj', metasenv,[],ugraph)) with exn -> + CicRefine.insert_coercions := saved_use_coercions; let rec process_exn loc = function HExtlib.Localized (loc,exn) -> process_exn loc exn @@ -367,7 +385,9 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in (try if is_uri ast then raise Not_found;(* don't search the env for URIs *) - let index = Disambiguate.find_in_context name context in + let index = + Disambiguate.find_in_context name (string_context_of_context context) + in if subst <> None then CicNotationPt.fail loc "Explicit substitutions not allowed here"; Cic.Rel index @@ -584,118 +604,62 @@ interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast ~localization_tbl ;; +let mk_implicit = + function true -> Cic.Implicit (Some `Closed) + | _ -> Cic.Implicit None +;; +let string_context_of_context = + List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some + (Cic.Anonymous,_) -> Some "_");; +let disambiguate_term ~context ~metasenv ~subst ?goal + ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe + ~lookup_in_library + (text,prefix_len,term) += + let hint = match goal with + | None -> (fun _ x -> x), fun k -> k + | Some i -> + (fun metasenv t -> + let _,c,ty = CicUtil.lookup_meta i metasenv in + assert(c=context); + Cic.Cast(t,ty)), + function + | Disambiguate.Ok (t,m,s,ug) -> + (match t with + | Cic.Cast(t,_) -> Disambiguate.Ok (t,m,s,ug) + | _ -> assert false) + | k -> k + in + let localization_tbl = Cic.CicHash.create 503 in + MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst + ~initial_ugraph ~aliases ~mk_implicit ~string_context_of_context + ~universe ~lookup_in_library + ~uri:None ~pp_thing:CicNotationPp.pp_term + ~domain_of_thing:Disambiguate.domain_of_term + ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) + ~refine_thing:refine_term (text,prefix_len,term) + ~localization_tbl + ~hint + ~freshen_thing:CicNotationUtil.freshen_term + ~passes:(MultiPassDisambiguator.passes ()) -module type CicDisambiguator = -sig - val disambiguate_term : - ?fresh_instances:bool -> - context:Cic.context -> - metasenv:Cic.metasenv -> - subst:Cic.substitution -> - ?goal:int -> - ?initial_ugraph:CicUniv.universe_graph -> - aliases:Cic.term DisambiguateTypes.environment -> - universe:Cic.term DisambiguateTypes.multiple_environment option -> - lookup_in_library:( - DisambiguateTypes.interactive_user_uri_choice_type -> - DisambiguateTypes.input_or_locate_uri_type -> - DisambiguateTypes.Environment.key -> - Cic.term DisambiguateTypes.codomain_item list) -> - CicNotationPt.term Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * - Cic.term DisambiguateTypes.codomain_item) list * - Cic.metasenv * - Cic.substitution * - Cic.term* - CicUniv.universe_graph) list * - bool - - val disambiguate_obj : - ?fresh_instances:bool -> - aliases:Cic.term DisambiguateTypes.environment -> - universe:Cic.term DisambiguateTypes.multiple_environment option -> - uri:UriManager.uri option -> (* required only for inductive types *) - lookup_in_library:( - DisambiguateTypes.interactive_user_uri_choice_type -> - DisambiguateTypes.input_or_locate_uri_type -> - DisambiguateTypes.Environment.key -> - Cic.term DisambiguateTypes.codomain_item list) -> - CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * - Cic.term DisambiguateTypes.codomain_item) list * - Cic.metasenv * - Cic.substitution * - Cic.obj * - CicUniv.universe_graph) list * - bool -end - -module Make (C: DisambiguateTypes.Callbacks) = - struct - module Disambiguator = Disambiguate.Make(C) - - let mk_implicit = - function true -> Cic.Implicit (Some `Closed) - | _ -> Cic.Implicit None - ;; - - let disambiguate_term ?(fresh_instances=false) ~context ~metasenv - ~subst ?goal - ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe - ~lookup_in_library - (text,prefix_len,term) - = - let term = - if fresh_instances then CicNotationUtil.freshen_term term else term - in - let hint = match goal with - | None -> (fun _ x -> x), fun k -> k - | Some i -> - (fun metasenv t -> - let _,c,ty = CicUtil.lookup_meta i metasenv in - assert(c=context); - Cic.Cast(t,ty)), - function - | Disambiguate.Ok (t,m,s,ug) -> - (match t with - | Cic.Cast(t,_) -> Disambiguate.Ok (t,m,s,ug) - | _ -> assert false) - | k -> k - in - let localization_tbl = Cic.CicHash.create 503 in - Disambiguator.disambiguate_thing ~context ~metasenv ~subst - ~initial_ugraph ~aliases ~mk_implicit - ~universe ~lookup_in_library - ~uri:None ~pp_thing:CicNotationPp.pp_term - ~domain_of_thing:Disambiguate.domain_of_term - ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) - ~refine_thing:refine_term (text,prefix_len,term) - ~localization_tbl - ~hint - - let disambiguate_obj - ?(fresh_instances=false) ~aliases ~universe ~uri ~lookup_in_library - (text,prefix_len,obj) - = - let obj = - if fresh_instances then CicNotationUtil.freshen_obj obj else obj - in - let hint = - (fun _ x -> x), - fun k -> k - in - let localization_tbl = Cic.CicHash.create 503 in - Disambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] - ~aliases ~universe ~uri ~mk_implicit - ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) - ~domain_of_thing:Disambiguate.domain_of_obj - ~lookup_in_library - ~initial_ugraph:CicUniv.empty_ugraph - ~interpretate_thing:interpretate_obj - ~refine_thing:refine_obj - ~localization_tbl - ~hint - (text,prefix_len,obj) -end +let disambiguate_obj ~aliases ~universe ~uri ~lookup_in_library + (text,prefix_len,obj) += + let hint = (fun _ x -> x), fun k -> k in + let localization_tbl = Cic.CicHash.create 503 in + MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] + ~aliases ~universe ~uri ~mk_implicit ~string_context_of_context + ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) + ~domain_of_thing:Disambiguate.domain_of_obj + ~lookup_in_library + ~initial_ugraph:CicUniv.empty_ugraph + ~interpretate_thing:interpretate_obj + ~refine_thing:refine_obj + ~localization_tbl + ~hint + ~passes:(MultiPassDisambiguator.passes ()) + ~freshen_thing:CicNotationUtil.freshen_obj + (text,prefix_len,obj) diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.mli b/helm/software/components/cic_disambiguation/cicDisambiguate.mli index 375723a76..0e228de10 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.mli +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.mli @@ -27,49 +27,42 @@ For details, see the HELM web site: http://helm.cs.unibo.it/ val interpretate_path : context:Cic.name list -> CicNotationPt.term -> Cic.term -module type CicDisambiguator = -sig - val disambiguate_term : - ?fresh_instances:bool -> - context:Cic.context -> - metasenv:Cic.metasenv -> - subst:Cic.substitution -> - ?goal:int -> - ?initial_ugraph:CicUniv.universe_graph -> - aliases:Cic.term DisambiguateTypes.environment -> - universe:Cic.term DisambiguateTypes.multiple_environment option -> - lookup_in_library:( - DisambiguateTypes.interactive_user_uri_choice_type -> - DisambiguateTypes.input_or_locate_uri_type -> - DisambiguateTypes.Environment.key -> - Cic.term DisambiguateTypes.codomain_item list) -> - CicNotationPt.term Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * - Cic.term DisambiguateTypes.codomain_item) list * - Cic.metasenv * - Cic.substitution * - Cic.term* - CicUniv.universe_graph) list * - bool +val disambiguate_term : + context:Cic.context -> + metasenv:Cic.metasenv -> + subst:Cic.substitution -> + ?goal:int -> + ?initial_ugraph:CicUniv.universe_graph -> + aliases:Cic.term DisambiguateTypes.environment -> + universe:Cic.term DisambiguateTypes.multiple_environment option -> + lookup_in_library:( + DisambiguateTypes.interactive_user_uri_choice_type -> + DisambiguateTypes.input_or_locate_uri_type -> + DisambiguateTypes.Environment.key -> + Cic.term DisambiguateTypes.codomain_item list) -> + CicNotationPt.term Disambiguate.disambiguator_input -> + ((DisambiguateTypes.domain_item * + Cic.term DisambiguateTypes.codomain_item) list * + Cic.metasenv * + Cic.substitution * + Cic.term* + CicUniv.universe_graph) list * + bool - val disambiguate_obj : - ?fresh_instances:bool -> - aliases:Cic.term DisambiguateTypes.environment -> - universe:Cic.term DisambiguateTypes.multiple_environment option -> - uri:UriManager.uri option -> (* required only for inductive types *) - lookup_in_library:( - DisambiguateTypes.interactive_user_uri_choice_type -> - DisambiguateTypes.input_or_locate_uri_type -> - DisambiguateTypes.Environment.key -> - Cic.term DisambiguateTypes.codomain_item list) -> - CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * - Cic.term DisambiguateTypes.codomain_item) list * - Cic.metasenv * - Cic.substitution * - Cic.obj * - CicUniv.universe_graph) list * - bool -end - -module Make (C : DisambiguateTypes.Callbacks) : CicDisambiguator +val disambiguate_obj : + aliases:Cic.term DisambiguateTypes.environment -> + universe:Cic.term DisambiguateTypes.multiple_environment option -> + uri:UriManager.uri option -> (* required only for inductive types *) + lookup_in_library:( + DisambiguateTypes.interactive_user_uri_choice_type -> + DisambiguateTypes.input_or_locate_uri_type -> + DisambiguateTypes.Environment.key -> + Cic.term DisambiguateTypes.codomain_item list) -> + CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input -> + ((DisambiguateTypes.domain_item * + Cic.term DisambiguateTypes.codomain_item) list * + Cic.metasenv * + Cic.substitution * + Cic.obj * + CicUniv.universe_graph) list * + bool diff --git a/helm/software/components/disambiguation/.depend b/helm/software/components/disambiguation/.depend new file mode 100644 index 000000000..aba9ffea7 --- /dev/null +++ b/helm/software/components/disambiguation/.depend @@ -0,0 +1,10 @@ +disambiguate.cmi: disambiguateTypes.cmi +multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi +disambiguateTypes.cmo: disambiguateTypes.cmi +disambiguateTypes.cmx: disambiguateTypes.cmi +disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi +disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi +multiPassDisambiguator.cmo: disambiguateTypes.cmi disambiguate.cmi \ + multiPassDisambiguator.cmi +multiPassDisambiguator.cmx: disambiguateTypes.cmx disambiguate.cmx \ + multiPassDisambiguator.cmi diff --git a/helm/software/components/disambiguation/.depend.opt b/helm/software/components/disambiguation/.depend.opt new file mode 100644 index 000000000..aba9ffea7 --- /dev/null +++ b/helm/software/components/disambiguation/.depend.opt @@ -0,0 +1,10 @@ +disambiguate.cmi: disambiguateTypes.cmi +multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi +disambiguateTypes.cmo: disambiguateTypes.cmi +disambiguateTypes.cmx: disambiguateTypes.cmi +disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi +disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi +multiPassDisambiguator.cmo: disambiguateTypes.cmi disambiguate.cmi \ + multiPassDisambiguator.cmi +multiPassDisambiguator.cmx: disambiguateTypes.cmx disambiguate.cmx \ + multiPassDisambiguator.cmi diff --git a/helm/software/components/disambiguation/Makefile b/helm/software/components/disambiguation/Makefile index b961efbff..d01dd73df 100644 --- a/helm/software/components/disambiguation/Makefile +++ b/helm/software/components/disambiguation/Makefile @@ -1,10 +1,10 @@ PACKAGE = disambiguation INTERFACE_FILES = \ disambiguateTypes.mli \ - disambiguate.mli + disambiguate.mli \ + multiPassDisambiguator.mli IMPLEMENTATION_FILES = \ - $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ - $(patsubst %,%_notation.ml,$(NOTATIONS)) + $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) all: diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml index 4ef0d1058..12b7b01a9 100644 --- a/helm/software/components/disambiguation/disambiguate.ml +++ b/helm/software/components/disambiguation/disambiguate.ml @@ -119,11 +119,17 @@ let resolve (env: 'term codomain_item Environment.t) (item: domain_item) ?(num = let find_in_context name context = let rec aux acc = function | [] -> raise Not_found - | Cic.Name hd :: tl when hd = name -> acc + | Some hd :: tl when hd = name -> acc | _ :: tl -> aux (acc + 1) tl in aux 1 context +let string_of_name = + function + | Ast.Ident (n, None) -> Some n + | _ -> assert false +;; + let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function | Ast.AttributedTerm (`Loc loc, term) -> domain_of_term ~loc ~context term @@ -182,7 +188,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function let type_dom = domain_of_term_option ~loc ~context typ in let body_dom = domain_of_term ~loc - ~context:(CicNotationUtil.cic_name_of_name var :: context) body in + ~context:(string_of_name var :: context) body in (match kind with | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ] | _ -> type_dom @ body_dom) @@ -199,7 +205,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function let (term_context, args_domain) = List.fold_left (fun (cont, dom) (name, typ) -> - (CicNotationUtil.cic_name_of_name name :: cont, + (string_of_name name :: cont, (match typ with | None -> dom | Some typ -> dom @ domain_of_term ~loc ~context:cont typ))) @@ -223,14 +229,12 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function let body_dom = domain_of_term ~loc ~context body in let type_dom = domain_of_term_option ~loc ~context typ in let where_dom = - domain_of_term ~loc - ~context:(CicNotationUtil.cic_name_of_name var :: context) where in + domain_of_term ~loc ~context:(string_of_name var :: context) where in body_dom @ type_dom @ where_dom | Ast.LetRec (kind, defs, where) -> let add_defs context = List.fold_left - (fun acc (_, (var, _), _, _) -> - CicNotationUtil.cic_name_of_name var :: acc + (fun acc (_, (var, _), _, _) -> string_of_name var :: acc ) context defs in let where_dom = domain_of_term ~loc ~context:(add_defs context) where in let defs_dom = @@ -239,14 +243,14 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function let context' = add_defs (List.fold_left - (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc) + (fun acc (var,_) -> string_of_name var :: acc) context params) in List.rev (snd (List.fold_left (fun (context,res) (var,ty) -> - CicNotationUtil.cic_name_of_name var :: context, + string_of_name var :: context, domain_of_term_option ~loc ~context ty @ res) (add_defs context,[]) params)) @ dom @@ -296,7 +300,6 @@ let domain_of_term ~context term = uniq_domain (domain_of_term ~context term) let domain_of_obj ~context ast = - let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in assert (context = []); match ast with | Ast.Theorem (_,_,ty,bo) -> @@ -308,15 +311,13 @@ let domain_of_obj ~context ast = let context, dom = List.fold_left (fun (context, dom) (var, ty) -> - let context' = CicNotationUtil.cic_name_of_name var :: context in + let context' = string_of_name var :: context in match ty with None -> context', dom | Some ty -> context', dom @ domain_of_term context ty ) ([], []) params in let context_w_types = - List.rev_map - (fun (var, _, _, _) -> Cic.Name var) tyl - @ context in + List.rev_map (fun (var, _, _, _) -> Some var) tyl @ context in dom @ List.flatten ( List.map @@ -330,18 +331,18 @@ let domain_of_obj ~context ast = let context, dom = List.fold_left (fun (context, dom) (var, ty) -> - let context' = CicNotationUtil.cic_name_of_name var :: context in + let context' = string_of_name var :: context in match ty with None -> context', dom | Some ty -> context', dom @ domain_of_term context ty ) ([], []) params in - let context_w_types = Cic.Name var :: context in + let context_w_types = Some var :: context in dom @ domain_of_term context ty @ snd (List.fold_left (fun (context,res) (name,ty,_,_) -> - Cic.Name name::context, res @ domain_of_term context ty + Some name::context, res @ domain_of_term context ty ) (context_w_types,[]) fields) let domain_of_obj ~context obj = @@ -349,11 +350,6 @@ let domain_of_obj ~context obj = let domain_of_ast_term = domain_of_term;; -let domain_of_term ~context term = - let context = - List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context - in - domain_of_term ~context term (* dom1 \ dom2 *) let domain_diff dom1 dom2 = (* let domain_diff = Domain.diff *) @@ -385,7 +381,9 @@ sig context:'context -> metasenv:'metasenv -> subst:'subst -> + use_coercions:bool -> mk_implicit:(bool -> 'refined_term) -> + string_context_of_context:('context -> string option list) -> initial_ugraph:'ugraph -> hint: ('metasenv -> 'raw_thing -> 'raw_thing) * @@ -402,7 +400,7 @@ sig 'refined_term DisambiguateTypes.codomain_item list) -> uri:'uri -> pp_thing:('ast_thing -> string) -> - domain_of_thing:(context:'context -> 'ast_thing -> domain) -> + domain_of_thing:(context: string option list -> 'ast_thing -> domain) -> interpretate_thing:( context:'context -> env:'refined_term DisambiguateTypes.codomain_item @@ -413,7 +411,7 @@ sig localization_tbl:'cichash -> 'raw_thing) -> refine_thing:( - 'metasenv -> 'subst -> 'context -> 'uri -> + 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool -> 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> localization_tbl:'cichash -> @@ -429,7 +427,8 @@ module Make (C: Callbacks) = let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let disambiguate_thing - ~context ~metasenv ~subst ~mk_implicit + ~context ~metasenv ~subst ~use_coercions + ~mk_implicit ~string_context_of_context ~initial_ugraph:base_univ ~hint ~aliases ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing @@ -438,7 +437,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" = debug_print (lazy "DISAMBIGUATE INPUT"); debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); - let thing_dom = domain_of_thing ~context thing in + 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))); (* @@ -525,8 +525,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let cic_thing = (fst hint) metasenv cic_thing in let foo () = let k = - refine_thing metasenv subst - context uri cic_thing ugraph ~localization_tbl + refine_thing metasenv subst context uri + ~use_coercions cic_thing ugraph ~localization_tbl in let k = (snd hint) k in k @@ -666,7 +666,6 @@ in refine_profiler.HExtlib.profile foo () | Uncertain _ -> aux aliases diff lookup_in_todo_dom todo_dom [] | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] in - try let res = match aux' aliases [] None todo_dom with | [],uncertain,errors -> @@ -722,10 +721,5 @@ in refine_profiler.HExtlib.profile foo () true in res - with - CicEnvironment.CircularDependency s -> - failwith "Disambiguate: circular dependency" end - - diff --git a/helm/software/components/disambiguation/disambiguate.mli b/helm/software/components/disambiguation/disambiguate.mli index 92e11870f..310b74b8b 100644 --- a/helm/software/components/disambiguation/disambiguate.mli +++ b/helm/software/components/disambiguation/disambiguate.mli @@ -59,14 +59,13 @@ val resolve : DisambiguateTypes.Environment.key -> ?num:string -> ?args:'term list -> unit -> 'term -val find_in_context: string -> Cic.name list -> int - -val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain +val find_in_context: string -> string option list -> int +val domain_of_ast_term: context: + string option list -> CicNotationPt.term -> domain val domain_of_term: context: - (Cic.name * 'a) option list -> CicNotationPt.term -> domain + string option list -> CicNotationPt.term -> domain val domain_of_obj: - context:(Cic.name * 'a) option list -> - CicNotationPt.term CicNotationPt.obj -> domain + context:string option list -> CicNotationPt.term CicNotationPt.obj -> domain module type Disambiguator = sig @@ -74,7 +73,9 @@ sig context:'context -> metasenv:'metasenv -> subst:'subst -> + use_coercions:bool -> mk_implicit:(bool -> 'refined_term) -> + string_context_of_context:('context -> string option list) -> initial_ugraph:'ugraph -> hint: ('metasenv -> 'raw_thing -> 'raw_thing) * @@ -91,7 +92,7 @@ sig 'refined_term DisambiguateTypes.codomain_item list) -> uri:'uri -> pp_thing:('ast_thing -> string) -> - domain_of_thing:(context:'context -> 'ast_thing -> domain) -> + domain_of_thing:(context: string option list -> 'ast_thing -> domain) -> interpretate_thing:( context:'context -> env:'refined_term DisambiguateTypes.codomain_item @@ -102,7 +103,7 @@ sig localization_tbl:'cichash -> 'raw_thing) -> refine_thing:( - 'metasenv -> 'subst -> 'context -> 'uri -> + 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool -> 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> localization_tbl:'cichash -> diff --git a/helm/software/components/grafite_parser/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml similarity index 62% rename from helm/software/components/grafite_parser/multiPassDisambiguator.ml rename to helm/software/components/disambiguation/multiPassDisambiguator.ml index a81709f23..af4a9e49e 100644 --- a/helm/software/components/grafite_parser/multiPassDisambiguator.ml +++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml @@ -39,7 +39,6 @@ exception DisambiguationError of (DisambiguateTypes.domain_item * string) list * (Stdpp.location * string) Lazy.t * bool) list list (** parameters are: option name, error message *) -exception Unbound_identifier of string let mono_uris_callback ~selection_mode ?ok ?(enable_button_for_non_vars = true) ~title ~msg ~id = @@ -70,95 +69,25 @@ module Callbacks = * query is a syntax error *) end -module Disambiguator = CicDisambiguate.Make (Callbacks) +module Disambiguator = Disambiguate.Make (Callbacks) (* implement module's API *) let only_one_pass = ref false;; -let disambiguate_thing ~aliases ~universe - ~(f:?fresh_instances:bool -> - aliases:'term DisambiguateTypes.environment -> - universe:'term DisambiguateTypes.multiple_environment option -> - 'a -> 'b) - ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b) - ~(drop_aliases_and_clear_diff: 'b -> 'b) - (thing: 'a) -= - assert (universe <> None); - let library = false, DisambiguateTypes.Environment.empty, None in - let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in - let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in - let passes = (* *) - if !only_one_pass then - [ (true, mono_aliases, false) ] - else - [ (true, mono_aliases, false); - (true, multi_aliases, false); - (true, mono_aliases, true); - (true, multi_aliases, true); - (true, library, false); - (* for demo to reduce the number of interpretations *) - (true, library, true); - ] - in - let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) = - CicRefine.insert_coercions := insert_coercions; - f ~fresh_instances ~aliases ~universe thing - in - let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) = - if use_mono_aliases then - drop_aliases ~minimize_instances:true res (* one shot aliases *) - else if user_asked then - drop_aliases ~minimize_instances:true res (* one shot aliases *) - else - drop_aliases_and_clear_diff res - in - let rec aux i errors passes = - debug_print (lazy ("Pass: " ^ string_of_int i)); - match passes with - [ pass ] -> - (try - set_aliases pass (try_pass pass) - with Disambiguate.NoWellTypedInterpretation (offset,newerrors) -> - raise (DisambiguationError (offset, errors @ [newerrors]))) - | hd :: tl -> - (try - set_aliases hd (try_pass hd) - with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) -> - aux (i+1) (errors @ [newerrors]) tl) - | [] -> assert false - in - let saved_insert_coercions = !CicRefine.insert_coercions in - try - let res = aux 1 [] passes in - CicRefine.insert_coercions := saved_insert_coercions; - res - with exn -> - CicRefine.insert_coercions := saved_insert_coercions; - raise exn - -type disambiguator_thing = - { do_it : - 'a 'b 'term. - aliases:'term DisambiguateTypes.environment -> - universe:'term DisambiguateTypes.multiple_environment option -> - f:(?fresh_instances:bool -> - aliases:'term DisambiguateTypes.environment -> - universe:'term DisambiguateTypes.multiple_environment option -> - 'a -> 'b * bool) -> - drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) -> - drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool - } - -let disambiguate_thing = - let profiler = HExtlib.profile "disambiguate_thing" in - { do_it = - fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing - -> profiler.HExtlib.profile - (disambiguate_thing ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff) thing - } +let passes () = (* *) + if !only_one_pass then + [ (true, `Mono, false) ] + else + [ (true, `Mono, false); + (true, `Multi, false); + (true, `Mono, true); + (true, `Multi, true); + (true, `Library, false); + (* for demo to reduce the number of interpretations *) + (true, `Library, true); + ] +;; let drop_aliases ?(minimize_instances=false) (choices, user_asked) = let module D = DisambiguateTypes in @@ -199,17 +128,60 @@ let drop_aliases_and_clear_diff (choices, user_asked) = (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices), user_asked -let disambiguate_term ?fresh_instances ~context ~metasenv ~subst ?goal ?initial_ugraph ~aliases ~universe ~lookup_in_library term +let disambiguate_thing ~passes ~aliases ~universe ~f thing = + assert (universe <> None); + let library = false, DisambiguateTypes.Environment.empty, None in + let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in + let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in + let passes = + List.map + (function (fresh_instances,env,use_coercions) -> + fresh_instances, + (match env with `Mono -> mono_aliases | `Multi -> multi_aliases | + `Library -> library), + use_coercions) passes in + let try_pass (fresh_instances, (_, aliases, universe), use_coercions) = + f ~fresh_instances ~aliases ~universe ~use_coercions thing + in + let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) = + if use_mono_aliases then + drop_aliases ~minimize_instances:true res (* one shot aliases *) + else if user_asked then + drop_aliases ~minimize_instances:true res (* one shot aliases *) + else + drop_aliases_and_clear_diff res + in + let rec aux i errors passes = + debug_print (lazy ("Pass: " ^ string_of_int i)); + match passes with + [ pass ] -> + (try + set_aliases pass (try_pass pass) + with Disambiguate.NoWellTypedInterpretation (offset,newerrors) -> + raise (DisambiguationError (offset, errors @ [newerrors]))) + | hd :: tl -> + (try + set_aliases hd (try_pass hd) + with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) -> + aux (i+1) (errors @ [newerrors]) tl) + | [] -> assert false + in + aux 1 [] passes + +let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst + ~mk_implicit ~string_context_of_context ~initial_ugraph ~hint ~aliases + ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing + ~interpretate_thing ~refine_thing ~localization_tbl thing = - assert (fresh_instances = None); - let f = - Disambiguator.disambiguate_term ~lookup_in_library ~context ~metasenv ~subst ?goal ?initial_ugraph + let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) = + let thing = if fresh_instances then freshen_thing thing else thing + in + Disambiguator.disambiguate_thing + ~context ~metasenv ~subst ~use_coercions + ~mk_implicit ~string_context_of_context + ~initial_ugraph ~hint + ~aliases ~universe ~lookup_in_library + ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing + ~localization_tbl (txt,len,thing) in - disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff term - -let disambiguate_obj ?fresh_instances ~aliases ~universe ~uri ~lookup_in_library obj = - assert (fresh_instances = None); - let f = Disambiguator.disambiguate_obj ~lookup_in_library ~uri in - disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff obj + disambiguate_thing ~passes ~aliases ~universe ~f thing diff --git a/helm/software/components/grafite_parser/multiPassDisambiguator.mli b/helm/software/components/disambiguation/multiPassDisambiguator.mli similarity index 53% rename from helm/software/components/grafite_parser/multiPassDisambiguator.mli rename to helm/software/components/disambiguation/multiPassDisambiguator.mli index 337c92e2f..7a4ae53aa 100644 --- a/helm/software/components/grafite_parser/multiPassDisambiguator.mli +++ b/helm/software/components/disambiguation/multiPassDisambiguator.mli @@ -37,6 +37,8 @@ exception DisambiguationError of (** initially false; for debugging only (???) *) val only_one_pass: bool ref +val passes : unit -> (bool * [> `Library | `Mono | `Multi ] * bool) list + val set_choose_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type -> unit @@ -53,6 +55,48 @@ val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type * above *) val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type -(** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *) - -include CicDisambiguate.CicDisambiguator +val disambiguate_thing: + passes:(bool * [ `Library | `Mono | `Multi ] * bool) list -> + freshen_thing: ('ast_thing -> 'ast_thing) -> + context:'context -> + metasenv:'metasenv -> + subst:'subst -> + mk_implicit:(bool -> 'refined_term) -> + string_context_of_context:('context -> string option list) -> + initial_ugraph:'ugraph -> + hint: + ('metasenv -> 'raw_thing -> 'raw_thing) * + (('refined_thing,'metasenv,'subst,'ugraph) Disambiguate.test_result -> + ('refined_thing,'metasenv,'subst,'ugraph) Disambiguate.test_result) -> + aliases:'refined_term DisambiguateTypes.codomain_item + DisambiguateTypes.Environment.t -> + universe:'refined_term DisambiguateTypes.codomain_item list + DisambiguateTypes.Environment.t option -> + lookup_in_library:( + DisambiguateTypes.interactive_user_uri_choice_type -> + DisambiguateTypes.input_or_locate_uri_type -> + DisambiguateTypes.Environment.key -> + 'refined_term DisambiguateTypes.codomain_item list) -> + uri:'uri -> + pp_thing:('ast_thing -> string) -> + domain_of_thing: + (context: string option list -> 'ast_thing -> Disambiguate.domain) -> + interpretate_thing:( + context:'context -> + env:'refined_term DisambiguateTypes.codomain_item + DisambiguateTypes.Environment.t -> + uri:'uri -> + is_path:bool -> + 'ast_thing -> + localization_tbl:'cichash -> + 'raw_thing) -> + refine_thing:( + 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool -> + 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> + ('refined_thing, 'metasenv,'subst,'ugraph) Disambiguate.test_result) -> + localization_tbl:'cichash -> + string * int * 'ast_thing -> + ((DisambiguateTypes.Environment.key * + 'refined_term DisambiguateTypes.codomain_item) list * + 'metasenv * 'subst * 'refined_thing * 'ugraph) + list * bool diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index ef9da1f20..33d7273e8 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -101,7 +101,7 @@ term = let lexicon_status = !lexicon_status_ref in let (diff, metasenv, subst, cic, _) = singleton "first" - (MultiPassDisambiguator.disambiguate_term + (CicDisambiguate.disambiguate_term ~aliases:lexicon_status.LexiconEngine.aliases ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~lookup_in_library @@ -122,7 +122,7 @@ let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term = let lexicon_status = !lexicon_status_ref in let (diff, metasenv, _, cic, ugraph) = singleton "second" - (MultiPassDisambiguator.disambiguate_term ~lookup_in_library + (CicDisambiguate.disambiguate_term ~lookup_in_library ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~context ~metasenv ~subst:[] ?goal @@ -528,7 +528,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = ); *) let (diff, metasenv, _, cic, _) = singleton "third" - (MultiPassDisambiguator.disambiguate_obj ~lookup_in_library + (CicDisambiguate.disambiguate_obj ~lookup_in_library ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri (text,prefix_len,obj)) in diff --git a/helm/software/components/ng_disambiguation/.depend b/helm/software/components/ng_disambiguation/.depend index 833273319..6b4ef95c1 100644 --- a/helm/software/components/ng_disambiguation/.depend +++ b/helm/software/components/ng_disambiguation/.depend @@ -1,4 +1,2 @@ -nDisambiguate.cmo: nDisambiguate.cmi -nDisambiguate.cmx: nDisambiguate.cmi -nGrafiteDisambiguator.cmo: nDisambiguate.cmi nGrafiteDisambiguator.cmi -nGrafiteDisambiguator.cmx: nDisambiguate.cmx nGrafiteDisambiguator.cmi +nCicDisambiguate.cmo: nCicDisambiguate.cmi +nCicDisambiguate.cmx: nCicDisambiguate.cmi diff --git a/helm/software/components/ng_disambiguation/Makefile b/helm/software/components/ng_disambiguation/Makefile index 411b10feb..91e3c09c7 100644 --- a/helm/software/components/ng_disambiguation/Makefile +++ b/helm/software/components/ng_disambiguation/Makefile @@ -1,8 +1,7 @@ PACKAGE = ng_disambiguation PREDICATES = -INTERFACE_FILES = \ - nDisambiguate.mli nGrafiteDisambiguator.mli\ +INTERFACE_FILES = nCicDisambiguate.mli IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml similarity index 91% rename from helm/software/components/ng_disambiguation/nDisambiguate.ml rename to helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 0429cc988..8c0874056 100644 --- a/helm/software/components/ng_disambiguation/nDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -26,7 +26,7 @@ let cic_name_of_name = function | _ -> assert false ;; -let refine_term metasenv subst context uri term _ ~localization_tbl = +let refine_term metasenv subst context uri ~use_coercions:_ term _ ~localization_tbl = assert (uri=None); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (NCicPp.ppterm ~metasenv ~subst ~context term))); @@ -389,47 +389,41 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ;; let domain_of_term ~context = - let context = List.map (fun name,_ -> Cic.Name name) context in Disambiguate.domain_of_ast_term ~context ;; -module Make (C : DisambiguateTypes.Callbacks) = struct - module Disambiguator = Disambiguate.Make(C) - - let disambiguate_term ?(fresh_instances=false) ~context ~metasenv ~subst - ~aliases ~universe ~lookup_in_library ?goal - (text,prefix_len,term) - = - let term = - if fresh_instances then CicNotationUtil.freshen_term term else term - in - let localization_tbl = NCicUntrusted.NCicHash.create 503 in - let hint = - match goal with - None -> (fun _ y -> y),(fun x -> x) - | Some n -> - (fun metasenv y -> - let _,_,ty = NCicUtils.lookup_meta n metasenv in - NCic.LetIn ("_",ty,y,NCic.Rel 1)), - (function - | Disambiguate.Ok (t,m,s,ug) -> - (match t with - | NCic.LetIn ("_",_,y,NCic.Rel 1) -> Disambiguate.Ok (y,m,s,ug) - | _ -> assert false) - | k -> k) +let disambiguate_term ~context ~metasenv ~subst ?goal + ~aliases ~universe ~lookup_in_library + (text,prefix_len,term) + = + let localization_tbl = NCicUntrusted.NCicHash.create 503 in + let hint = + match goal with + None -> (fun _ y -> y),(fun x -> x) + | Some n -> + (fun metasenv y -> + let _,_,ty = NCicUtils.lookup_meta n metasenv in + NCic.LetIn ("_",ty,y,NCic.Rel 1)), + (function + | Disambiguate.Ok (t,m,s,ug) -> + (match t with + | NCic.LetIn ("_",_,y,NCic.Rel 1) -> Disambiguate.Ok (y,m,s,ug) + | _ -> assert false) + | k -> k) + in + let res,b = + MultiPassDisambiguator.disambiguate_thing + ~freshen_thing:CicNotationUtil.freshen_term + ~context ~metasenv ~initial_ugraph:() ~aliases + ~string_context_of_context:(List.map (fun (x,_) -> Some x)) + ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term + ~mk_implicit:(function false -> NCic.Implicit `Term + | true -> NCic.Implicit `Closed) + ~passes:(MultiPassDisambiguator.passes ()) + ~lookup_in_library ~domain_of_thing:domain_of_term + ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) + ~refine_thing:refine_term (text,prefix_len,term) + ~localization_tbl ~hint ~subst in - let res,b = - Disambiguator.disambiguate_thing - ~context ~metasenv ~initial_ugraph:() ~aliases - ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term - ~mk_implicit:(function false -> NCic.Implicit `Term - | true -> NCic.Implicit `Closed) - ~lookup_in_library ~domain_of_thing:domain_of_term - ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) - ~refine_thing:refine_term (text,prefix_len,term) - ~localization_tbl ~hint ~subst - in - List.map (function (a,b,c,d,_) -> a,b,c,d) res, b - ;; - -end + List.map (function (a,b,c,d,_) -> a,b,c,d) res, b +;; diff --git a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli similarity index 76% rename from helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli rename to helm/software/components/ng_disambiguation/nCicDisambiguate.mli index 153af12bc..ffcd8f99b 100644 --- a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli @@ -9,13 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -(* $Id$ *) - -exception DisambiguationError of - int * - ((Stdpp.location list * string * string) list * - (DisambiguateTypes.domain_item * string) list * - (Stdpp.location * string) Lazy.t * bool) list list +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) val disambiguate_term : context:NCic.context -> @@ -24,10 +18,15 @@ val disambiguate_term : ?goal:int -> aliases:NCic.term DisambiguateTypes.environment -> universe:NCic.term DisambiguateTypes.multiple_environment option -> + lookup_in_library:( + DisambiguateTypes.interactive_user_uri_choice_type -> + DisambiguateTypes.input_or_locate_uri_type -> + DisambiguateTypes.Environment.key -> + NCic.term DisambiguateTypes.codomain_item list) -> CicNotationPt.term Disambiguate.disambiguator_input -> ((DisambiguateTypes.domain_item * NCic.term DisambiguateTypes.codomain_item) list * - NCic.metasenv * (* new metasenv *) + NCic.metasenv * NCic.substitution * - NCic.term) list * (* disambiguated term *) + NCic.term) list * bool diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.mli b/helm/software/components/ng_disambiguation/nDisambiguate.mli deleted file mode 100644 index ae1b16f59..000000000 --- a/helm/software/components/ng_disambiguation/nDisambiguate.mli +++ /dev/null @@ -1,39 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) - -module Make (C : DisambiguateTypes.Callbacks) : sig -val disambiguate_term : - ?fresh_instances:bool -> - context:NCic.context -> - metasenv:NCic.metasenv -> - subst:NCic.substitution -> - aliases:NCic.term DisambiguateTypes.environment ->(* previous interpretation status *) - universe:NCic.term DisambiguateTypes.multiple_environment option -> - lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> - msg:string -> - id:string -> - UriManager.uri list -> UriManager.uri list) -> - (title:string -> ?id:string -> unit -> UriManager.uri option) -> - DisambiguateTypes.Environment.key -> - NCic.term DisambiguateTypes.codomain_item list) -> - ?goal: int -> - CicNotationPt.term Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * NCic.term DisambiguateTypes.codomain_item) list * - NCic.metasenv * (* new metasenv *) - NCic.substitution * - NCic.term) list * (* disambiguated term *) - bool -end diff --git a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml deleted file mode 100644 index 9aa41c52b..000000000 --- a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml +++ /dev/null @@ -1,182 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id$ *) - -exception DisambiguationError of - int * - ((Stdpp.location list * string * string) list * - (DisambiguateTypes.domain_item * string) list * - (Stdpp.location * string) Lazy.t * bool) list list - -open Printf - -let debug = false;; -let debug_print s = - if debug then prerr_endline (Lazy.force s);; - -module Callbacks = - struct - let interactive_user_uri_choice ~selection_mode ?ok - ?(enable_button_for_non_vars = true) ~title ~msg ~id uris = - assert false - - let interactive_interpretation_choice interp = - assert false - - let input_or_locate_uri ~(title:string) ?id () = - assert false - end - -module Disambiguator = NDisambiguate.Make (Callbacks) - -let only_one_pass = ref false;; - -let disambiguate_thing ~aliases ~universe - ~(f:?fresh_instances:bool -> - aliases:NCic.term DisambiguateTypes.environment -> - universe:NCic.term DisambiguateTypes.multiple_environment option -> - 'a -> 'b) - ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b) - ~(drop_aliases_and_clear_diff: 'b -> 'b) - (thing: 'a) -= - assert (universe <> None); - let library = false, DisambiguateTypes.Environment.empty, None in - let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in - let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in - let passes = (* *) - if !only_one_pass then - [ (true, mono_aliases, false) ] - else - [ (true, mono_aliases, false); - (true, multi_aliases, false); - (true, mono_aliases, true); - (true, multi_aliases, true); - (true, library, false); - (* for demo to reduce the number of interpretations *) - (true, library, true); - ] - in - let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) = - CicRefine.insert_coercions := insert_coercions; - f ~fresh_instances ~aliases ~universe thing - in - let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) = - if use_mono_aliases then - drop_aliases ~minimize_instances:true res (* one shot aliases *) - else if user_asked then - drop_aliases ~minimize_instances:true res (* one shot aliases *) - else - drop_aliases_and_clear_diff res - in - let rec aux i errors passes = - debug_print (lazy ("Pass: " ^ string_of_int i)); - match passes with - [ pass ] -> - (try - set_aliases pass (try_pass pass) - with Disambiguate.NoWellTypedInterpretation (offset,newerrors) -> - raise (DisambiguationError (offset, errors @ [newerrors]))) - | hd :: tl -> - (try - set_aliases hd (try_pass hd) - with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) -> - aux (i+1) (errors @ [newerrors]) tl) - | [] -> assert false - in - let saved_insert_coercions = !CicRefine.insert_coercions in - try - let res = aux 1 [] passes in - CicRefine.insert_coercions := saved_insert_coercions; - res - with exn -> - CicRefine.insert_coercions := saved_insert_coercions; - raise exn - -type disambiguator_thing = - { do_it : - 'a 'b. - aliases:NCic.term DisambiguateTypes.environment -> - universe:NCic.term DisambiguateTypes.multiple_environment option -> - f:(?fresh_instances:bool -> - aliases:NCic.term DisambiguateTypes.environment -> - universe:NCic.term DisambiguateTypes.multiple_environment option -> - 'a -> 'b * bool) -> - drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) -> - drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool - } - -let disambiguate_thing = - let profiler = HExtlib.profile "disambiguate_thing" in - { do_it = - fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing - -> profiler.HExtlib.profile - (disambiguate_thing ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff) thing - } - -let drop_aliases ?(minimize_instances=false) (choices, user_asked) = - let module D = DisambiguateTypes in - let minimize d = - if not minimize_instances then - d - else - let rec aux = - function - [] -> [] - | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 -> - if - List.for_all - (function - (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2 - | _ -> true - ) d - then - (D.Symbol (s,0),ci)::(aux tl) - else - he::(aux tl) - | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 -> - if - List.for_all - (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d - then - (D.Num 0,ci)::(aux tl) - else - he::(aux tl) - | he::tl -> he::(aux tl) - in - aux d - in - (List.map (fun (d, a, b, c) -> minimize d, a, b, c) choices), - user_asked - -let drop_aliases_and_clear_diff (choices, user_asked) = - (List.map (fun (_, a, b, c) -> [], a, b, c) choices), - user_asked - -let disambiguate_term ~context ~metasenv ~subst ?goal - ~aliases ~universe term - = - let f = - Disambiguator.disambiguate_term ~context ~metasenv ~subst ?goal - ~lookup_in_library:(fun _ _ -> assert false) - in - disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff term - -let disambiguate_obj ~aliases ~universe ~uri obj = - assert false (* - assert (fresh_instances = None); - let f = Disambiguator.disambiguate_obj ~uri ~lookup_in_library:(fun _ _ -> assert false) in - disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff obj - *) -- 2.39.2