From: Enrico Tassi Date: Thu, 27 Nov 2008 17:44:31 +0000 (+0000) Subject: New modules stack: X-Git-Tag: make_still_working~4490 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3323758b99384afb5c7a70aa31bc006a78af64dd;p=helm.git New modules stack: grafiteDisambiguator | cicDisambiguator | | multiPassDisambiagutor |disambiguate nCicDisambiguator| --- 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/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml new file mode 100644 index 000000000..af4a9e49e --- /dev/null +++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml @@ -0,0 +1,187 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id$ *) + +open Printf + +let debug = false;; +let debug_print s = + if debug then prerr_endline (Lazy.force s);; + +exception Ambiguous_input +(* the integer is an offset to be added to each location *) +exception DisambiguationError of + int * + ((Stdpp.location list * string * string) list * + (DisambiguateTypes.domain_item * string) list * + (Stdpp.location * string) Lazy.t * bool) list list + (** parameters are: option name, error message *) + +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 + "matita.auto_disambiguation" + then + function l -> l + else + raise Ambiguous_input + +let mono_interp_callback _ _ _ = raise Ambiguous_input + +let _choose_uris_callback = ref mono_uris_callback +let _choose_interp_callback = ref mono_interp_callback +let set_choose_uris_callback f = _choose_uris_callback := f +let set_choose_interp_callback f = _choose_interp_callback := f + +module Callbacks = + struct + let interactive_user_uri_choice = !_choose_uris_callback + + let interactive_interpretation_choice interp = + !_choose_interp_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" + * query is a syntax error *) + end + +module Disambiguator = Disambiguate.Make (Callbacks) + +(* implement module's API *) + +let only_one_pass = ref false;; + +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 + 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, e) -> minimize d, a, b, c, e) choices), + user_asked + +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_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 + = + 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 ~passes ~aliases ~universe ~f thing diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.mli b/helm/software/components/disambiguation/multiPassDisambiguator.mli new file mode 100644 index 000000000..7a4ae53aa --- /dev/null +++ b/helm/software/components/disambiguation/multiPassDisambiguator.mli @@ -0,0 +1,102 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(** raised when ambiguous input is found but not expected (e.g. in the batch + * compiler) *) +exception Ambiguous_input +(* the integer is an offset to be added to each location *) +exception DisambiguationError of + int * + ((Stdpp.location list * string * string) list * + (DisambiguateTypes.domain_item * string) list * + (Stdpp.location * string) Lazy.t * bool) list list + (** parameters are: option name, error message *) + +(** 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 + +val set_choose_interp_callback: + DisambiguateTypes.interactive_interpretation_choice_type -> unit + +(** @raise Ambiguous_input if called, default value for internal + * choose_uris_callback if not set otherwise with set_choose_uris_callback + * above *) +val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type + +(** @raise Ambiguous_input if called, default value for internal + * choose_interp_callback if not set otherwise with set_choose_interp_callback + * above *) +val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type + +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/grafite_parser/multiPassDisambiguator.ml b/helm/software/components/grafite_parser/multiPassDisambiguator.ml deleted file mode 100644 index a81709f23..000000000 --- a/helm/software/components/grafite_parser/multiPassDisambiguator.ml +++ /dev/null @@ -1,215 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -open Printf - -let debug = false;; -let debug_print s = - if debug then prerr_endline (Lazy.force s);; - -exception Ambiguous_input -(* the integer is an offset to be added to each location *) -exception DisambiguationError of - int * - ((Stdpp.location list * string * string) list * - (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 = - if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true - "matita.auto_disambiguation" - then - function l -> l - else - raise Ambiguous_input - -let mono_interp_callback _ _ _ = raise Ambiguous_input - -let _choose_uris_callback = ref mono_uris_callback -let _choose_interp_callback = ref mono_interp_callback -let set_choose_uris_callback f = _choose_uris_callback := f -let set_choose_interp_callback f = _choose_interp_callback := f - -module Callbacks = - struct - let interactive_user_uri_choice = !_choose_uris_callback - - let interactive_interpretation_choice interp = - !_choose_interp_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" - * query is a syntax error *) - end - -module Disambiguator = CicDisambiguate.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 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, e) -> minimize d, a, b, c, e) choices), - user_asked - -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 - = - assert (fresh_instances = None); - let f = - Disambiguator.disambiguate_term ~lookup_in_library ~context ~metasenv ~subst ?goal ?initial_ugraph - 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 diff --git a/helm/software/components/grafite_parser/multiPassDisambiguator.mli b/helm/software/components/grafite_parser/multiPassDisambiguator.mli deleted file mode 100644 index 337c92e2f..000000000 --- a/helm/software/components/grafite_parser/multiPassDisambiguator.mli +++ /dev/null @@ -1,58 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(** raised when ambiguous input is found but not expected (e.g. in the batch - * compiler) *) -exception Ambiguous_input -(* the integer is an offset to be added to each location *) -exception DisambiguationError of - int * - ((Stdpp.location list * string * string) list * - (DisambiguateTypes.domain_item * string) list * - (Stdpp.location * string) Lazy.t * bool) list list - (** parameters are: option name, error message *) - -(** initially false; for debugging only (???) *) -val only_one_pass: bool ref - -val set_choose_uris_callback: - DisambiguateTypes.interactive_user_uri_choice_type -> unit - -val set_choose_interp_callback: - DisambiguateTypes.interactive_interpretation_choice_type -> unit - -(** @raise Ambiguous_input if called, default value for internal - * choose_uris_callback if not set otherwise with set_choose_uris_callback - * above *) -val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type - -(** @raise Ambiguous_input if called, default value for internal - * choose_interp_callback if not set otherwise with set_choose_interp_callback - * above *) -val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type - -(** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *) - -include CicDisambiguate.CicDisambiguator 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/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml new file mode 100644 index 000000000..8c0874056 --- /dev/null +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -0,0 +1,429 @@ +(* + ||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 $ *) + +open Printf + +open DisambiguateTypes +open UriManager + +module Ast = CicNotationPt +module NRef = NReference + +let debug_print _ = ();; + +let cic_name_of_name = function + | Ast.Ident (n, None) -> n + | _ -> assert false +;; + +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))); + try + let localise t = + try NCicUntrusted.NCicHash.find localization_tbl t + with Not_found -> assert false + in + let metasenv, subst, term, _ = + NCicRefiner.typeof metasenv subst context term None ~localise + in + Disambiguate.Ok (term, metasenv, subst, ()) + with + | NCicRefiner.Uncertain loc_msg -> + debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^ + NCicPp.ppterm ~metasenv ~subst ~context term)) ; + Disambiguate.Uncertain loc_msg + | NCicRefiner.RefineFailure loc_msg -> + debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s" + (NCicPp.ppterm ~metasenv ~subst ~context term) (snd(Lazy.force loc_msg)))); + Disambiguate.Ko loc_msg +;; + + (* TODO move it to Cic *) +let find_in_context name context = + let rec aux acc = function + | [] -> raise Not_found + | hd :: _ when hd = name -> acc + | _ :: tl -> aux (acc + 1) tl + in + aux 1 context + +let interpretate_term + ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl += + (* create_dummy_ids shouldbe used only for interpretating patterns *) + assert (uri = None); + + let rec aux ~localize loc context = function + | CicNotationPt.AttributedTerm (`Loc loc, term) -> + let res = aux ~localize loc context term in + if localize then NCicUntrusted.NCicHash.add localization_tbl res loc; + res + | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term + | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> + let cic_args = List.map (aux ~localize loc context) args in + Disambiguate.resolve env (Symbol (symb, i)) ~args:cic_args () + | CicNotationPt.Appl terms -> + NCic.Appl (List.map (aux ~localize loc context) terms) + | CicNotationPt.Binder (binder_kind, (var, typ), body) -> + let cic_type = aux_option ~localize loc context `Type typ in + let cic_name = cic_name_of_name var in + let cic_body = aux ~localize loc (cic_name :: context) body in + (match binder_kind with + | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body) + | `Pi + | `Forall -> NCic.Prod (cic_name, cic_type, cic_body) + | `Exists -> + Disambiguate.resolve env (Symbol ("exists", 0)) + ~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ()) + | CicNotationPt.Case (term, indty_ident, outtype, branches) -> + let cic_term = aux ~localize loc context term in + let cic_outtype = aux_option ~localize loc context `Term outtype in + let do_branch ((_, _, args), term) = + let rec do_branch' context = function + | [] -> aux ~localize loc context term + | (name, typ) :: tl -> + let cic_name = cic_name_of_name name in + let cic_body = do_branch' (cic_name :: context) tl in + let typ = + match typ with + | None -> NCic.Implicit `Type + | Some typ -> aux ~localize loc context typ + in + NCic.Lambda (cic_name, typ, cic_body) + in + do_branch' context args + in + if create_dummy_ids then + let branches = + List.map + (function + Ast.Wildcard,term -> ("wildcard",None,[]), term + | Ast.Pattern _,_ -> + raise (DisambiguateTypes.Invalid_choice + (lazy (loc, "Syntax error: the left hand side of a "^ + "branch pattern must be \"_\""))) + ) branches + in + (* + NCic.MutCase (ref, cic_outtype, cic_term, + (List.map do_branch branches)) + *) ignore branches; assert false (* patterns not implemented yet *) + else + let indtype_ref = + match indty_ident with + | Some (indty_ident, _) -> + (match Disambiguate.resolve env (Id indty_ident) () with + | NCic.Const r -> r + | NCic.Implicit _ -> + raise (Disambiguate.Try_again + (lazy "The type of the term to be matched is still unknown")) + | _ -> + raise (DisambiguateTypes.Invalid_choice + (lazy (loc,"The type of the term to be matched "^ + "is not (co)inductive!")))) + | None -> + let rec fst_constructor = + function + (Ast.Pattern (head, _, _), _) :: _ -> head + | (Ast.Wildcard, _) :: tl -> fst_constructor tl + | [] -> raise (Invalid_choice (lazy (loc,"The type "^ + "of the term to be matched cannot be determined "^ + "because it is an inductive type without constructors "^ + "or because all patterns use wildcards"))) + in + (match Disambiguate.resolve env (Id (fst_constructor branches)) () with + | NCic.Const r -> r + | NCic.Implicit _ -> + raise (Disambiguate.Try_again + (lazy "The type of the term to be matched is still unknown")) + | _ -> + raise (DisambiguateTypes.Invalid_choice + (lazy (loc, + "The type of the term to be matched is not (co)inductive!")))) + in + let _,leftsno,itl,_,indtyp_no = + NCicEnvironment.get_checked_indtys indtype_ref in + let _,_,_,cl = + try + List.nth itl indtyp_no + with _ -> assert false in + let rec count_prod t = + match NCicReduction.whd [] t with + NCic.Prod (_, _, t) -> 1 + (count_prod t) + | _ -> 0 + in + let rec sort branches cl = + match cl with + [] -> + let rec analyze unused unrecognized useless = + function + [] -> + if unrecognized != [] then + raise (DisambiguateTypes.Invalid_choice + (lazy + (loc,"Unrecognized constructors: " ^ + String.concat " " unrecognized))) + else if useless > 0 then + raise (DisambiguateTypes.Invalid_choice + (lazy + (loc,"The last " ^ string_of_int useless ^ + "case" ^ if useless > 1 then "s are" else " is" ^ + " unused"))) + else + [] + | (Ast.Wildcard,_)::tl when not unused -> + analyze true unrecognized useless tl + | (Ast.Pattern (head,_,_),_)::tl when not unused -> + analyze unused (head::unrecognized) useless tl + | _::tl -> analyze unused unrecognized (useless + 1) tl + in + analyze false [] 0 branches + | (_,name,ty)::cltl -> + let rec find_and_remove = + function + [] -> + raise + (DisambiguateTypes.Invalid_choice + (lazy (loc, "Missing case: " ^ name))) + | ((Ast.Wildcard, _) as branch :: _) as branches -> + branch, branches + | (Ast.Pattern (name',_,_),_) as branch :: tl + when name = name' -> + branch,tl + | branch::tl -> + let found,rest = find_and_remove tl in + found, branch::rest + in + let branch,tl = find_and_remove branches in + match branch with + Ast.Pattern (name,y,args),term -> + if List.length args = count_prod ty - leftsno then + ((name,y,args),term)::sort tl cltl + else + raise + (DisambiguateTypes.Invalid_choice + (lazy (loc,"Wrong number of arguments for " ^ name))) + | Ast.Wildcard,term -> + let rec mk_lambdas = + function + 0 -> term + | n -> + CicNotationPt.Binder + (`Lambda, (CicNotationPt.Ident ("_", None), None), + mk_lambdas (n - 1)) + in + (("wildcard",None,[]), + mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl + in + let branches = sort branches cl in + NCic.Match (indtype_ref, cic_outtype, cic_term, + (List.map do_branch branches)) + | CicNotationPt.Cast (t1, t2) -> + let cic_t1 = aux ~localize loc context t1 in + let cic_t2 = aux ~localize loc context t2 in + NCic.LetIn ("_",cic_t2,cic_t1, NCic.Rel 1) + | CicNotationPt.LetIn ((name, typ), def, body) -> + let cic_def = aux ~localize loc context def in + let cic_name = cic_name_of_name name in + let cic_typ = + match typ with + | None -> NCic.Implicit `Type + | Some t -> aux ~localize loc context t + in + let cic_body = aux ~localize loc (cic_name :: context) body in + NCic.LetIn (cic_name, cic_def, cic_typ, cic_body) + | CicNotationPt.LetRec (_kind, _defs, _body) -> + assert false (* + let context' = + List.fold_left + (fun acc (_, (name, _), _, _) -> + cic_name_of_name name :: acc) + context defs + in + let cic_body = + let unlocalized_body = aux ~localize:false loc context' body in + match unlocalized_body with + NCic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n + | NCic.Appl (NCic.Rel n::l) when n <= List.length defs -> + (try + let l' = + List.map + (function t -> + let t',subst,metasenv = + CicMetaSubst.delift_rels [] [] (List.length defs) t + in + assert (subst=[]); + assert (metasenv=[]); + t') l + in + (* We can avoid the LetIn. But maybe we need to recompute l' + so that it is localized *) + if localize then + match body with + CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) -> + (* since we avoid the letin, the context has no + * recfuns in it *) + let l' = List.map (aux ~localize loc context) l in + `AvoidLetIn (n,l') + | _ -> assert false + else + `AvoidLetIn (n,l') + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + if localize then + `AddLetIn (aux ~localize loc context' body) + else + `AddLetIn unlocalized_body) + | _ -> + if localize then + `AddLetIn (aux ~localize loc context' body) + else + `AddLetIn unlocalized_body + in + let inductiveFuns = + List.map + (fun (params, (name, typ), body, decr_idx) -> + let add_binders kind t = + List.fold_right + (fun var t -> CicNotationPt.Binder (kind, var, t)) params t + in + let cic_body = + aux ~localize loc context' (add_binders `Lambda body) in + let cic_type = + aux_option ~localize loc context (Some `Type) + (HExtlib.map_option (add_binders `Pi) typ) in + let name = + match cic_name_of_name name with + | NCic.Anonymous -> + CicNotationPt.fail loc + "Recursive functions cannot be anonymous" + | NCic.Name name -> name + in + (name, decr_idx, cic_type, cic_body)) + defs + in + let fix_or_cofix n = + match kind with + `Inductive -> NCic.Fix (n,inductiveFuns) + | `CoInductive -> + let coinductiveFuns = + List.map + (fun (name, _, typ, body) -> name, typ, body) + inductiveFuns + in + NCic.CoFix (n,coinductiveFuns) + in + let counter = ref ~-1 in + let build_term _ (var,_,ty,_) t = + incr counter; + NCic.LetIn (NCic.Name var, fix_or_cofix !counter, ty, t) + in + (match cic_body with + `AvoidLetInNoAppl n -> + let n' = List.length inductiveFuns - n in + fix_or_cofix n' + | `AvoidLetIn (n,l) -> + let n' = List.length inductiveFuns - n in + NCic.Appl (fix_or_cofix n'::l) + | `AddLetIn cic_body -> + List.fold_right (build_term inductiveFuns) inductiveFuns + cic_body) +*) + | CicNotationPt.Ident _ + | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed + | CicNotationPt.Ident (name, subst) -> + assert (subst = None); + (try + NCic.Rel (find_in_context name context) + with Not_found -> Disambiguate.resolve env (Id name) ()) + | CicNotationPt.Uri (name, subst) -> + assert (subst = None); + (try + NCic.Const (NRef.reference_of_string name) + with NRef.IllFormedReference _ -> + CicNotationPt.fail loc "Ill formed reference") + | CicNotationPt.Implicit -> NCic.Implicit `Term + | CicNotationPt.UserInput -> assert false (*NCic.Implicit (Some `Hole) +patterns not implemented *) + | CicNotationPt.Num (num, i) -> Disambiguate.resolve env (Num i) ~num () + | CicNotationPt.Meta (index, subst) -> + let cic_subst = + List.map + (function None -> assert false| Some t -> aux ~localize loc context t) + subst + in + NCic.Meta (index, (0, NCic.Ctx cic_subst)) + | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop + | CicNotationPt.Sort `Set -> assert false + | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type + [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"]) + | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type + [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"]) + | CicNotationPt.Symbol (symbol, instance) -> + Disambiguate.resolve env (Symbol (symbol, instance)) () + | _ -> assert false (* god bless Bologna *) + and aux_option ~localize loc context annotation = function + | None -> NCic.Implicit annotation + | Some term -> aux ~localize loc context term + in + aux ~localize:true HExtlib.dummy_floc context ast + +let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast + ~localization_tbl += + let context = List.map fst context in + interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast +~localization_tbl +;; + +let domain_of_term ~context = + Disambiguate.domain_of_ast_term ~context +;; + +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 + List.map (function (a,b,c,d,_) -> a,b,c,d) res, b +;; diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli new file mode 100644 index 000000000..ffcd8f99b --- /dev/null +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli @@ -0,0 +1,32 @@ +(* + ||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 $ *) + +val disambiguate_term : + context:NCic.context -> + metasenv:NCic.metasenv -> + subst:NCic.substitution -> + ?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 * + NCic.substitution * + NCic.term) list * + bool diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.ml b/helm/software/components/ng_disambiguation/nDisambiguate.ml deleted file mode 100644 index 0429cc988..000000000 --- a/helm/software/components/ng_disambiguation/nDisambiguate.ml +++ /dev/null @@ -1,435 +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 $ *) - -open Printf - -open DisambiguateTypes -open UriManager - -module Ast = CicNotationPt -module NRef = NReference - -let debug_print _ = ();; - -let cic_name_of_name = function - | Ast.Ident (n, None) -> n - | _ -> assert false -;; - -let refine_term metasenv subst context uri term _ ~localization_tbl = - assert (uri=None); - debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" - (NCicPp.ppterm ~metasenv ~subst ~context term))); - try - let localise t = - try NCicUntrusted.NCicHash.find localization_tbl t - with Not_found -> assert false - in - let metasenv, subst, term, _ = - NCicRefiner.typeof metasenv subst context term None ~localise - in - Disambiguate.Ok (term, metasenv, subst, ()) - with - | NCicRefiner.Uncertain loc_msg -> - debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^ - NCicPp.ppterm ~metasenv ~subst ~context term)) ; - Disambiguate.Uncertain loc_msg - | NCicRefiner.RefineFailure loc_msg -> - debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s" - (NCicPp.ppterm ~metasenv ~subst ~context term) (snd(Lazy.force loc_msg)))); - Disambiguate.Ko loc_msg -;; - - (* TODO move it to Cic *) -let find_in_context name context = - let rec aux acc = function - | [] -> raise Not_found - | hd :: _ when hd = name -> acc - | _ :: tl -> aux (acc + 1) tl - in - aux 1 context - -let interpretate_term - ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl -= - (* create_dummy_ids shouldbe used only for interpretating patterns *) - assert (uri = None); - - let rec aux ~localize loc context = function - | CicNotationPt.AttributedTerm (`Loc loc, term) -> - let res = aux ~localize loc context term in - if localize then NCicUntrusted.NCicHash.add localization_tbl res loc; - res - | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term - | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> - let cic_args = List.map (aux ~localize loc context) args in - Disambiguate.resolve env (Symbol (symb, i)) ~args:cic_args () - | CicNotationPt.Appl terms -> - NCic.Appl (List.map (aux ~localize loc context) terms) - | CicNotationPt.Binder (binder_kind, (var, typ), body) -> - let cic_type = aux_option ~localize loc context `Type typ in - let cic_name = cic_name_of_name var in - let cic_body = aux ~localize loc (cic_name :: context) body in - (match binder_kind with - | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body) - | `Pi - | `Forall -> NCic.Prod (cic_name, cic_type, cic_body) - | `Exists -> - Disambiguate.resolve env (Symbol ("exists", 0)) - ~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ()) - | CicNotationPt.Case (term, indty_ident, outtype, branches) -> - let cic_term = aux ~localize loc context term in - let cic_outtype = aux_option ~localize loc context `Term outtype in - let do_branch ((_, _, args), term) = - let rec do_branch' context = function - | [] -> aux ~localize loc context term - | (name, typ) :: tl -> - let cic_name = cic_name_of_name name in - let cic_body = do_branch' (cic_name :: context) tl in - let typ = - match typ with - | None -> NCic.Implicit `Type - | Some typ -> aux ~localize loc context typ - in - NCic.Lambda (cic_name, typ, cic_body) - in - do_branch' context args - in - if create_dummy_ids then - let branches = - List.map - (function - Ast.Wildcard,term -> ("wildcard",None,[]), term - | Ast.Pattern _,_ -> - raise (DisambiguateTypes.Invalid_choice - (lazy (loc, "Syntax error: the left hand side of a "^ - "branch pattern must be \"_\""))) - ) branches - in - (* - NCic.MutCase (ref, cic_outtype, cic_term, - (List.map do_branch branches)) - *) ignore branches; assert false (* patterns not implemented yet *) - else - let indtype_ref = - match indty_ident with - | Some (indty_ident, _) -> - (match Disambiguate.resolve env (Id indty_ident) () with - | NCic.Const r -> r - | NCic.Implicit _ -> - raise (Disambiguate.Try_again - (lazy "The type of the term to be matched is still unknown")) - | _ -> - raise (DisambiguateTypes.Invalid_choice - (lazy (loc,"The type of the term to be matched "^ - "is not (co)inductive!")))) - | None -> - let rec fst_constructor = - function - (Ast.Pattern (head, _, _), _) :: _ -> head - | (Ast.Wildcard, _) :: tl -> fst_constructor tl - | [] -> raise (Invalid_choice (lazy (loc,"The type "^ - "of the term to be matched cannot be determined "^ - "because it is an inductive type without constructors "^ - "or because all patterns use wildcards"))) - in - (match Disambiguate.resolve env (Id (fst_constructor branches)) () with - | NCic.Const r -> r - | NCic.Implicit _ -> - raise (Disambiguate.Try_again - (lazy "The type of the term to be matched is still unknown")) - | _ -> - raise (DisambiguateTypes.Invalid_choice - (lazy (loc, - "The type of the term to be matched is not (co)inductive!")))) - in - let _,leftsno,itl,_,indtyp_no = - NCicEnvironment.get_checked_indtys indtype_ref in - let _,_,_,cl = - try - List.nth itl indtyp_no - with _ -> assert false in - let rec count_prod t = - match NCicReduction.whd [] t with - NCic.Prod (_, _, t) -> 1 + (count_prod t) - | _ -> 0 - in - let rec sort branches cl = - match cl with - [] -> - let rec analyze unused unrecognized useless = - function - [] -> - if unrecognized != [] then - raise (DisambiguateTypes.Invalid_choice - (lazy - (loc,"Unrecognized constructors: " ^ - String.concat " " unrecognized))) - else if useless > 0 then - raise (DisambiguateTypes.Invalid_choice - (lazy - (loc,"The last " ^ string_of_int useless ^ - "case" ^ if useless > 1 then "s are" else " is" ^ - " unused"))) - else - [] - | (Ast.Wildcard,_)::tl when not unused -> - analyze true unrecognized useless tl - | (Ast.Pattern (head,_,_),_)::tl when not unused -> - analyze unused (head::unrecognized) useless tl - | _::tl -> analyze unused unrecognized (useless + 1) tl - in - analyze false [] 0 branches - | (_,name,ty)::cltl -> - let rec find_and_remove = - function - [] -> - raise - (DisambiguateTypes.Invalid_choice - (lazy (loc, "Missing case: " ^ name))) - | ((Ast.Wildcard, _) as branch :: _) as branches -> - branch, branches - | (Ast.Pattern (name',_,_),_) as branch :: tl - when name = name' -> - branch,tl - | branch::tl -> - let found,rest = find_and_remove tl in - found, branch::rest - in - let branch,tl = find_and_remove branches in - match branch with - Ast.Pattern (name,y,args),term -> - if List.length args = count_prod ty - leftsno then - ((name,y,args),term)::sort tl cltl - else - raise - (DisambiguateTypes.Invalid_choice - (lazy (loc,"Wrong number of arguments for " ^ name))) - | Ast.Wildcard,term -> - let rec mk_lambdas = - function - 0 -> term - | n -> - CicNotationPt.Binder - (`Lambda, (CicNotationPt.Ident ("_", None), None), - mk_lambdas (n - 1)) - in - (("wildcard",None,[]), - mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl - in - let branches = sort branches cl in - NCic.Match (indtype_ref, cic_outtype, cic_term, - (List.map do_branch branches)) - | CicNotationPt.Cast (t1, t2) -> - let cic_t1 = aux ~localize loc context t1 in - let cic_t2 = aux ~localize loc context t2 in - NCic.LetIn ("_",cic_t2,cic_t1, NCic.Rel 1) - | CicNotationPt.LetIn ((name, typ), def, body) -> - let cic_def = aux ~localize loc context def in - let cic_name = cic_name_of_name name in - let cic_typ = - match typ with - | None -> NCic.Implicit `Type - | Some t -> aux ~localize loc context t - in - let cic_body = aux ~localize loc (cic_name :: context) body in - NCic.LetIn (cic_name, cic_def, cic_typ, cic_body) - | CicNotationPt.LetRec (_kind, _defs, _body) -> - assert false (* - let context' = - List.fold_left - (fun acc (_, (name, _), _, _) -> - cic_name_of_name name :: acc) - context defs - in - let cic_body = - let unlocalized_body = aux ~localize:false loc context' body in - match unlocalized_body with - NCic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n - | NCic.Appl (NCic.Rel n::l) when n <= List.length defs -> - (try - let l' = - List.map - (function t -> - let t',subst,metasenv = - CicMetaSubst.delift_rels [] [] (List.length defs) t - in - assert (subst=[]); - assert (metasenv=[]); - t') l - in - (* We can avoid the LetIn. But maybe we need to recompute l' - so that it is localized *) - if localize then - match body with - CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) -> - (* since we avoid the letin, the context has no - * recfuns in it *) - let l' = List.map (aux ~localize loc context) l in - `AvoidLetIn (n,l') - | _ -> assert false - else - `AvoidLetIn (n,l') - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - if localize then - `AddLetIn (aux ~localize loc context' body) - else - `AddLetIn unlocalized_body) - | _ -> - if localize then - `AddLetIn (aux ~localize loc context' body) - else - `AddLetIn unlocalized_body - in - let inductiveFuns = - List.map - (fun (params, (name, typ), body, decr_idx) -> - let add_binders kind t = - List.fold_right - (fun var t -> CicNotationPt.Binder (kind, var, t)) params t - in - let cic_body = - aux ~localize loc context' (add_binders `Lambda body) in - let cic_type = - aux_option ~localize loc context (Some `Type) - (HExtlib.map_option (add_binders `Pi) typ) in - let name = - match cic_name_of_name name with - | NCic.Anonymous -> - CicNotationPt.fail loc - "Recursive functions cannot be anonymous" - | NCic.Name name -> name - in - (name, decr_idx, cic_type, cic_body)) - defs - in - let fix_or_cofix n = - match kind with - `Inductive -> NCic.Fix (n,inductiveFuns) - | `CoInductive -> - let coinductiveFuns = - List.map - (fun (name, _, typ, body) -> name, typ, body) - inductiveFuns - in - NCic.CoFix (n,coinductiveFuns) - in - let counter = ref ~-1 in - let build_term _ (var,_,ty,_) t = - incr counter; - NCic.LetIn (NCic.Name var, fix_or_cofix !counter, ty, t) - in - (match cic_body with - `AvoidLetInNoAppl n -> - let n' = List.length inductiveFuns - n in - fix_or_cofix n' - | `AvoidLetIn (n,l) -> - let n' = List.length inductiveFuns - n in - NCic.Appl (fix_or_cofix n'::l) - | `AddLetIn cic_body -> - List.fold_right (build_term inductiveFuns) inductiveFuns - cic_body) -*) - | CicNotationPt.Ident _ - | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed - | CicNotationPt.Ident (name, subst) -> - assert (subst = None); - (try - NCic.Rel (find_in_context name context) - with Not_found -> Disambiguate.resolve env (Id name) ()) - | CicNotationPt.Uri (name, subst) -> - assert (subst = None); - (try - NCic.Const (NRef.reference_of_string name) - with NRef.IllFormedReference _ -> - CicNotationPt.fail loc "Ill formed reference") - | CicNotationPt.Implicit -> NCic.Implicit `Term - | CicNotationPt.UserInput -> assert false (*NCic.Implicit (Some `Hole) -patterns not implemented *) - | CicNotationPt.Num (num, i) -> Disambiguate.resolve env (Num i) ~num () - | CicNotationPt.Meta (index, subst) -> - let cic_subst = - List.map - (function None -> assert false| Some t -> aux ~localize loc context t) - subst - in - NCic.Meta (index, (0, NCic.Ctx cic_subst)) - | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop - | CicNotationPt.Sort `Set -> assert false - | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type - [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"]) - | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type - [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"]) - | CicNotationPt.Symbol (symbol, instance) -> - Disambiguate.resolve env (Symbol (symbol, instance)) () - | _ -> assert false (* god bless Bologna *) - and aux_option ~localize loc context annotation = function - | None -> NCic.Implicit annotation - | Some term -> aux ~localize loc context term - in - aux ~localize:true HExtlib.dummy_floc context ast - -let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast - ~localization_tbl -= - let context = List.map fst context in - interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast -~localization_tbl -;; - -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) - 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 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 - *) diff --git a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli deleted file mode 100644 index 153af12bc..000000000 --- a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli +++ /dev/null @@ -1,33 +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 - -val disambiguate_term : - context:NCic.context -> - metasenv:NCic.metasenv -> - subst:NCic.substitution -> - ?goal:int -> - aliases:NCic.term DisambiguateTypes.environment -> - universe:NCic.term DisambiguateTypes.multiple_environment option -> - 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