From 8f9d476c32c48d14348a61889dc191c7696bd404 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 9 May 2006 13:40:24 +0000 Subject: [PATCH] types2006 patch --- .../binaries/saturate/saturate_main.ml | 2 +- helm/software/components/cic_acic/cic2acic.ml | 4 +- .../cic_disambiguation/disambiguate.ml | 94 +++++++------ .../cic_disambiguation/disambiguate.mli | 6 +- .../cic_disambiguation/disambiguateTypes.ml | 5 +- .../cic_disambiguation/disambiguateTypes.mli | 5 +- helm/software/components/extlib/hExtlib.ml | 2 +- .../grafite_engine/grafiteEngine.ml | 74 ++++++----- .../grafite_engine/grafiteEngine.mli | 12 +- .../grafite_parser/dependenciesParser.ml | 6 - .../grafite_parser/grafiteDisambiguate.ml | 71 ++++++---- .../grafite_parser/grafiteDisambiguate.mli | 18 ++- .../grafite_parser/grafiteDisambiguator.ml | 12 +- .../grafite_parser/grafiteDisambiguator.mli | 4 +- .../matita/library/algebra/finite_groups.ma | 28 ++-- .../matita/library/algebra/semigroups.ma | 8 +- helm/software/matita/matita.glade | 17 ++- helm/software/matita/matitaEngine.ml | 20 +-- helm/software/matita/matitaEngine.mli | 19 +-- helm/software/matita/matitaGtkMisc.ml | 8 +- helm/software/matita/matitaGui.ml | 124 +++++++++++++++++- helm/software/matita/matitaScript.ml | 4 +- 22 files changed, 372 insertions(+), 171 deletions(-) diff --git a/helm/software/components/binaries/saturate/saturate_main.ml b/helm/software/components/binaries/saturate/saturate_main.ml index efcfca4ed..afe8fbb83 100644 --- a/helm/software/components/binaries/saturate/saturate_main.ml +++ b/helm/software/components/binaries/saturate/saturate_main.ml @@ -64,7 +64,7 @@ struct CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term) in try - fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast + fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ("",0,ast) ?initial_ugraph ~aliases ~universe:None) with Exit -> raise (Ambiguous_term (lazy term)) end diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml index 8540e0e64..a7d3cbc70 100644 --- a/helm/software/components/cic_acic/cic2acic.ml +++ b/helm/software/components/cic_acic/cic2acic.ml @@ -166,9 +166,9 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes { D.synthesized = (***CSC: patch per provare i tempi CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *) - if global_computeinnertypes then + (*if global_computeinnertypes then Cic.Sort (Cic.Type (CicUniv.fresh())) - else + else*) CicReduction.whd context (xxx_type_of_aux' metasenv context tt); D.expected = None} in diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 667c50770..d3af05256 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -39,6 +39,7 @@ exception PathNotWellFormed exception Try_again of string Lazy.t type aliases = bool * DisambiguateTypes.environment +type 'a disambiguator_input = string * int * 'a let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () @@ -521,19 +522,25 @@ let rev_uniq = let compare = Pervasives.compare end in - let module Set = Set.Make (SortedItem) in + let module Map = Map.Make (SortedItem) in fun l -> let rev_l = List.rev l in - let (_, uniq_rev_l) = + let (members, uniq_rev_l) = List.fold_left - (fun (members, rev_l) elt -> - if Set.mem elt members then - (members, rev_l) - else - Set.add elt members, elt :: rev_l) - (Set.empty, []) rev_l + (fun (members, rev_l) (loc,elt) -> + try + let locs = Map.find elt members in + if List.mem loc locs then + members, rev_l + else + Map.add elt (loc::locs) members, rev_l + with + | Not_found -> Map.add elt [loc] members, elt :: rev_l) + (Map.empty, []) rev_l in - List.rev uniq_rev_l + List.rev_map + (fun e -> try Map.find e members,e with Not_found -> assert false) + uniq_rev_l (* "aux" keeps domain in reverse order and doesn't care about duplicates. * Domain item more in deep in the list will be processed first. @@ -549,7 +556,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function | CicNotationPt.Binder (kind, (var, typ), body) -> let kind_dom = match kind with - | `Exists -> [ Symbol ("exists", 0) ] + | `Exists -> [ loc, Symbol ("exists", 0) ] | _ -> [] in let type_dom = domain_rev_of_term_option loc context typ in @@ -563,7 +570,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function let outtype_dom = domain_rev_of_term_option loc context outtype in let get_first_constructor = function | [] -> [] - | ((head, _, _), _) :: _ -> [ Id head ] + | ((head, _, _), _) :: _ -> [ loc, Id head ] in let do_branch ((head, _, args), term) = let (term_context, args_domain) = @@ -583,7 +590,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function branches_dom @ outtype_dom @ term_dom @ (match indty_ident with | None -> get_first_constructor branches - | Some (ident, _) -> [ Id ident ]) + | Some (ident, _) -> [ loc, Id ident ]) | CicNotationPt.Cast (term, ty) -> let term_dom = domain_rev_of_term ~loc context term in let ty_dom = domain_rev_of_term ~loc context ty in @@ -622,22 +629,22 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function [] with Not_found -> (match subst with - | None -> [Id name] + | None -> [loc, Id name] | Some subst -> List.fold_left (fun dom (_, term) -> let dom' = domain_rev_of_term ~loc context term in dom' @ dom) - [Id name] subst)) + [loc, Id name] subst)) | CicNotationPt.Uri _ -> [] | CicNotationPt.Implicit -> [] - | CicNotationPt.Num (num, i) -> [ Num i ] + | CicNotationPt.Num (num, i) -> [loc, Num i ] | CicNotationPt.Meta (index, local_context) -> List.fold_left (fun dom term -> domain_rev_of_term_option loc context term @ dom) [] local_context | CicNotationPt.Sort _ -> [] - | CicNotationPt.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ] + | CicNotationPt.Symbol (symbol, instance) -> [loc, Symbol (symbol, instance) ] | CicNotationPt.UserInput | CicNotationPt.Literal _ | CicNotationPt.Layout _ @@ -658,7 +665,7 @@ let domain_of_obj ~context ast = (match bo with None -> [] | Some bo -> domain_rev_of_term [] bo) @ - domain_of_term [] ty + domain_rev_of_term [] ty | CicNotationPt.Inductive (params,tyl) -> let dom = List.flatten ( @@ -675,7 +682,7 @@ let domain_of_obj ~context ast = ) dom params in List.filter - (fun name -> + (fun (_,name) -> not ( List.exists (fun (name',_) -> name = Id name') params || List.exists (fun (name',_,_,_) -> name = Id name') tyl) ) dom @@ -690,7 +697,7 @@ let domain_of_obj ~context ast = ) (dom @ domain_rev_of_term [] ty) params in List.filter - (fun name-> + (fun (_,name) -> not ( List.exists (fun (name',_) -> name = Id name') params || List.exists (fun (name',_,_) -> name = Id name') fields) ) dom @@ -704,7 +711,7 @@ let domain_diff dom1 dom2 = List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt')) (fun _ -> false) dom2 in - List.filter (fun elt -> not (is_in_dom2 elt)) dom1 + List.filter (fun (_,elt) -> not (is_in_dom2 elt)) dom1 module type Disambiguator = sig @@ -716,7 +723,7 @@ sig ?initial_ugraph:CicUniv.universe_graph -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> - CicNotationPt.term -> + CicNotationPt.term disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.term* @@ -729,7 +736,7 @@ sig aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) - CicNotationPt.obj -> + CicNotationPt.obj disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.obj * @@ -744,8 +751,12 @@ module Make (C: Callbacks) = let uris = match uris with | [] -> - [(C.input_or_locate_uri - ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())] + (match + (C.input_or_locate_uri + ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ()) + with + | None -> [] + | Some uri -> [uri]) | [uri] -> [uri] | _ -> C.interactive_user_uri_choice ~selection_mode:`MULTIPLE @@ -773,7 +784,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let disambiguate_thing ~dbd ~context ~metasenv ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe - ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing + ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing + (thing_txt,thing_txt_prefix_len,thing) = debug_print (lazy "DISAMBIGUATE INPUT"); let disambiguate_context = (* cic context -> disambiguate context *) @@ -784,7 +796,7 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); let thing_dom = domain_of_thing ~context:disambiguate_context thing in debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s" - (string_of_domain thing_dom))); + (string_of_domain (List.map snd thing_dom)))); (* debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s" (DisambiguatePp.pp_environment aliases))); @@ -852,7 +864,7 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let test_env aliases todo_dom ugraph = let filled_env = List.fold_left - (fun env item -> + (fun env (_,item) -> Environment.add item ("Implicit", (match item with @@ -886,7 +898,7 @@ in refine_profiler.HExtlib.profile foo () | Ok (thing, metasenv),new_univ -> [ aliases, diff, metasenv, thing, new_univ ], [] | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg]) - | item :: remaining_dom -> + | (locs,item) :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item))); let choices = @@ -895,7 +907,8 @@ in refine_profiler.HExtlib.profile foo () | Some choices -> choices in match choices with [] -> - [], [None,lazy ("No choices for " ^ string_of_domain_item item)] + [], [Some (List.hd locs), + lazy ("No choices for " ^ string_of_domain_item item)] | [codomain_item] -> (* just one choice. We perform a one-step look-up and if the next set of choices is also a singleton we @@ -906,7 +919,7 @@ in refine_profiler.HExtlib.profile foo () let lookup_in_todo_dom,next_choice_is_single = match remaining_dom with [] -> None,false - | he::_ -> + | (_,he)::_ -> let choices = lookup_choices he in Some choices,List.length choices = 1 in @@ -962,20 +975,24 @@ in refine_profiler.HExtlib.profile foo () debug_print (lazy "SINGLE INTERPRETATION"); [diff,metasenv,t,ugraph], false | l,_ -> - debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); + debug_print + (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); let choices = List.map (fun (env, _, _, _, _) -> List.map - (fun domain_item -> + (fun (locs,domain_item) -> let description = fst (Environment.find domain_item env) in - (descr_of_domain_item domain_item, description)) + locs,descr_of_domain_item domain_item, description) thing_dom) l in - let choosed = C.interactive_interpretation_choice choices in + let choosed = + C.interactive_interpretation_choice + thing_txt thing_txt_prefix_len choices + in (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed), true in @@ -985,7 +1002,8 @@ in refine_profiler.HExtlib.profile foo () failwith "Disambiguate: circular dependency" let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe term + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe + (text,prefix_len,term) = let term = if fresh_instances then CicNotationUtil.freshen_term term else term @@ -993,10 +1011,10 @@ in refine_profiler.HExtlib.profile foo () disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term - ~refine_thing:refine_term term + ~refine_thing:refine_term (text,prefix_len,term) let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri - obj + (text,prefix_len,obj) = let obj = if fresh_instances then CicNotationUtil.freshen_obj obj else obj @@ -1004,6 +1022,6 @@ in refine_profiler.HExtlib.profile foo () disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj - obj + (text,prefix_len,obj) end diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli index a2cc0d0e7..e7c6b777f 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.mli +++ b/helm/software/components/cic_disambiguation/disambiguate.mli @@ -34,6 +34,8 @@ val interpretate_path : context:Cic.name list -> CicNotationPt.term -> Cic.term +type 'a disambiguator_input = string * int * 'a + module type Disambiguator = sig (** @param fresh_instances when set to true fresh instances will be generated @@ -47,7 +49,7 @@ sig ?initial_ugraph:CicUniv.universe_graph -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> - CicNotationPt.term -> + CicNotationPt.term disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.term * @@ -61,7 +63,7 @@ sig aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) - CicNotationPt.obj -> + CicNotationPt.obj disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.obj * diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.ml b/helm/software/components/cic_disambiguation/disambiguateTypes.ml index 4a2e43a20..79388f819 100644 --- a/helm/software/components/cic_disambiguation/disambiguateTypes.ml +++ b/helm/software/components/cic_disambiguation/disambiguateTypes.ml @@ -105,9 +105,10 @@ module type Callbacks = title:string -> msg:string -> id:string -> UriManager.uri list -> UriManager.uri list val interactive_interpretation_choice: - (string * string) list list -> int list + string -> int -> + (Token.flocation list * string * string) list list -> int list val input_or_locate_uri: - title:string -> ?id:string -> unit -> UriManager.uri + title:string -> ?id:string -> unit -> UriManager.uri option end let string_of_domain_item = function diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.mli b/helm/software/components/cic_disambiguation/disambiguateTypes.mli index 4f4b3c3ec..b584f0bec 100644 --- a/helm/software/components/cic_disambiguation/disambiguateTypes.mli +++ b/helm/software/components/cic_disambiguation/disambiguateTypes.mli @@ -71,12 +71,13 @@ module type Callbacks = UriManager.uri list val interactive_interpretation_choice : - (string * string) list list -> int list + string -> int -> + (Token.flocation list * string * string) list list -> int list (** @param title gtk window title for user prompting * @param id unbound identifier which originated this callback invocation *) val input_or_locate_uri: - title:string -> ?id:string -> unit -> UriManager.uri + title:string -> ?id:string -> unit -> UriManager.uri option end val string_of_domain_item: domain_item -> string diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index bf725122c..57511db0e 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -27,7 +27,7 @@ (** PROFILING *) -let profiling_enabled = ComponentsConf.profiling +let profiling_enabled = false ;; (* ComponentsConf.profiling *) let something_profiled = ref false diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index c6139e0e5..8b83bcff0 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -34,6 +34,8 @@ exception Macro of (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) exception ReadOnlyUri of string +type 'a disambiguator_input = string * int * 'a + type options = { do_heavy_checks: bool ; clean_baseuri: bool @@ -275,13 +277,13 @@ let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= |+ FINE DEBUG CODE +| *) before @ produced_metas @ after, goals -let apply_tactic ~disambiguate_tactic tactic (status, goal) = +let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) = (* prerr_endline "apply_tactic"; *) (* prerr_endline (Continuationals.Stack.pp (GrafiteTypes.get_stack status)); *) let starting_metasenv = GrafiteTypes.get_proof_metasenv status in let before = List.map (fun g, _, _ -> g) starting_metasenv in (* prerr_endline "disambiguate"; *) - let status, tactic = disambiguate_tactic status goal tactic in + let status, tactic = disambiguate_tactic status goal (text,prefix_len,tactic) in let metasenv_after_refinement = GrafiteTypes.get_proof_metasenv status in let proof = GrafiteTypes.get_current_proof status in let proof_status = proof, goal in @@ -330,34 +332,36 @@ type eval_ast = disambiguate_tactic: (GrafiteTypes.status -> ProofEngineTypes.goal -> - ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic -> + (('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic) + disambiguator_input -> GrafiteTypes.status * (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> disambiguate_command: (GrafiteTypes.status -> - 'obj GrafiteAst.command -> + ('obj GrafiteAst.command) disambiguator_input -> GrafiteTypes.status * Cic.obj GrafiteAst.command) -> disambiguate_macro: (GrafiteTypes.status -> - 'term GrafiteAst.macro -> + ('term GrafiteAst.macro) disambiguator_input -> Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> ?do_heavy_checks:bool -> ?clean_baseuri:bool -> GrafiteTypes.status -> - ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> + (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) + disambiguator_input -> GrafiteTypes.status * UriManager.uri list } type 'a eval_command = {ec_go: 'term 'obj. disambiguate_command: - (GrafiteTypes.status -> - 'obj GrafiteAst.command -> - GrafiteTypes.status * Cic.obj GrafiteAst.command) -> - options -> GrafiteTypes.status -> 'obj GrafiteAst.command -> + (GrafiteTypes.status -> ('obj GrafiteAst.command) disambiguator_input -> + GrafiteTypes.status * Cic.obj GrafiteAst.command) -> + options -> GrafiteTypes.status -> + ('obj GrafiteAst.command) disambiguator_input -> GrafiteTypes.status * UriManager.uri list } @@ -366,23 +370,24 @@ type 'a eval_executable = disambiguate_tactic: (GrafiteTypes.status -> ProofEngineTypes.goal -> - ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic -> + (('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic) + disambiguator_input -> GrafiteTypes.status * (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> disambiguate_command: (GrafiteTypes.status -> - 'obj GrafiteAst.command -> + ('obj GrafiteAst.command) disambiguator_input -> GrafiteTypes.status * Cic.obj GrafiteAst.command) -> disambiguate_macro: (GrafiteTypes.status -> - 'term GrafiteAst.macro -> + ('term GrafiteAst.macro) disambiguator_input -> Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> options -> GrafiteTypes.status -> - ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code -> + (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code) disambiguator_input -> GrafiteTypes.status * UriManager.uri list } @@ -434,7 +439,7 @@ let eval_tactical ~disambiguate_tactic status tac = type tactic = input_status -> output_status - let id_tactic = apply_tactic (GrafiteAst.IdTac HExtlib.dummy_floc) + let id_tactic = apply_tactic ("",0,(GrafiteAst.IdTac HExtlib.dummy_floc)) let mk_tactic tac = tac let apply_tactic tac = tac let goals (_, opened, closed) = opened, closed @@ -449,7 +454,9 @@ let eval_tactical ~disambiguate_tactic status tac = end in let module MatitaTacticals = Tacticals.Make (MatitaStatus) in - let rec tactical_of_ast l tac = + let rec tactical_of_ast l (text,prefix_len,tac) = + let apply_tactic t = apply_tactic (text, prefix_len, t) in + let tactical_of_ast l t = tactical_of_ast l (text,prefix_len,t) in match tac with | GrafiteAst.Tactic (loc, tactic) -> MatitaTacticals.tactic (MatitaStatus.mk_tactic (apply_tactic tactic)) @@ -556,8 +563,9 @@ let add_obj uri obj status = let status,lemmas = GrafiteSync.add_obj refinement_toolkit uri obj status in status, lemmas -let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> - let status,cmd = disambiguate_command status cmd in +let rec eval_command = {ec_go = fun ~disambiguate_command opts status +(text,prefix_len,cmd) -> + let status,cmd = disambiguate_command status (text,prefix_len,cmd) in let status,uris = match cmd with | GrafiteAst.Default (loc, what, uris) as cmd -> @@ -697,23 +705,25 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},uris | _ -> status,uris -} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command ~disambiguate_macro opts status ex -> +} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command +~disambiguate_macro opts status (text,prefix_len,ex) -> match ex with | GrafiteAst.Tactical (_, tac, None) -> - eval_tactical ~disambiguate_tactic status tac,[] + eval_tactical ~disambiguate_tactic status (text,prefix_len,tac),[] | GrafiteAst.Tactical (_, tac, Some punct) -> - let status = eval_tactical ~disambiguate_tactic status tac in - eval_tactical ~disambiguate_tactic status punct,[] + let status = + eval_tactical ~disambiguate_tactic status (text,prefix_len,tac) in + eval_tactical ~disambiguate_tactic status (text,prefix_len,punct),[] | GrafiteAst.Command (_, cmd) -> - eval_command.ec_go ~disambiguate_command opts status cmd + eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd) | GrafiteAst.Macro (loc, macro) -> - raise (Macro (loc,disambiguate_macro status macro)) + raise (Macro (loc,disambiguate_macro status (text,prefix_len,macro))) } and eval_from_moo = {efm_go = fun status fname -> let ast_of_cmd cmd = - GrafiteAst.Executable (HExtlib.dummy_floc, + ("",0,GrafiteAst.Executable (HExtlib.dummy_floc, GrafiteAst.Command (HExtlib.dummy_floc, - cmd)) + cmd))) in let moo = GrafiteMarshal.load_moo fname in List.fold_left @@ -721,15 +731,17 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> let ast = ast_of_cmd ast in let status,lemmas = eval_ast.ea_go - ~disambiguate_tactic:(fun status _ tactic -> status,tactic) - ~disambiguate_command:(fun status cmd -> status,cmd) + ~disambiguate_tactic:(fun status _ (_,_,tactic) -> status,tactic) + ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd) ~disambiguate_macro:(fun _ _ -> assert false) status ast in assert (lemmas=[]); status) status moo -} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command ~disambiguate_macro ?(do_heavy_checks=false) ?(clean_baseuri=true) status st +} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command +~disambiguate_macro ?(do_heavy_checks=false) ?(clean_baseuri=true) status +(text,prefix_len,st) -> let opts = { do_heavy_checks = do_heavy_checks ; @@ -738,8 +750,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> match st with | GrafiteAst.Executable (_,ex) -> eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command - ~disambiguate_macro opts status ex - | GrafiteAst.Comment (_,c) -> eval_comment status c,[] + ~disambiguate_macro opts status (text,prefix_len,ex) + | GrafiteAst.Comment (_,c) -> eval_comment status (text,prefix_len,c),[] } let eval_ast = eval_ast.ea_go diff --git a/helm/software/components/grafite_engine/grafiteEngine.mli b/helm/software/components/grafite_engine/grafiteEngine.mli index ee5f3a157..b1df57281 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.mli +++ b/helm/software/components/grafite_engine/grafiteEngine.mli @@ -29,27 +29,31 @@ exception Macro of GrafiteAst.loc * (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) +type 'a disambiguator_input = string * int * 'a + val eval_ast : disambiguate_tactic: (GrafiteTypes.status -> ProofEngineTypes.goal -> - ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic -> + (('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic) + disambiguator_input -> GrafiteTypes.status * (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> disambiguate_command: (GrafiteTypes.status -> - 'obj GrafiteAst.command -> + ('obj GrafiteAst.command) disambiguator_input -> GrafiteTypes.status * Cic.obj GrafiteAst.command) -> disambiguate_macro: (GrafiteTypes.status -> - 'term GrafiteAst.macro -> + ('term GrafiteAst.macro) disambiguator_input -> Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> ?do_heavy_checks:bool -> ?clean_baseuri:bool -> GrafiteTypes.status -> - ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> + (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) + disambiguator_input -> (* the new status and generated objects, if any *) GrafiteTypes.status * UriManager.uri list diff --git a/helm/software/components/grafite_parser/dependenciesParser.ml b/helm/software/components/grafite_parser/dependenciesParser.ml index dee951118..69a28c962 100644 --- a/helm/software/components/grafite_parser/dependenciesParser.ml +++ b/helm/software/components/grafite_parser/dependenciesParser.ml @@ -83,10 +83,4 @@ let baseuri_of_script ~include_paths file = let uri = Http_getter_misc.strip_trailing_slash buri in if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then HLog.error (file ^ " sets an incorrect baseuri: " ^ buri); - (try - ignore(Http_getter.resolve ~writable:false uri) - with - | Http_getter_types.Unresolvable_URI _ -> - HLog.error (file ^ " sets an unresolvable baseuri: " ^ buri) - | Http_getter_types.Key_not_found _ -> ()); uri diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 26c74e657..3d1899835 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -27,30 +27,41 @@ exception BaseUriNotSetYet +type tactic = + (CicNotationPt.term, CicNotationPt.term, + CicNotationPt.term GrafiteAst.reduction, string) + GrafiteAst.tactic + +type lazy_tactic = + (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) + GrafiteAst.tactic + let singleton = function | [x], _ -> x | _ -> assert false +;; (** @param term not meaningful when context is given *) -let disambiguate_term lexicon_status_ref context metasenv term = +let disambiguate_term text prefix_len lexicon_status_ref context metasenv term = let lexicon_status = !lexicon_status_ref in let (diff, metasenv, cic, _) = singleton (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ()) ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) - ~context ~metasenv term) + ~context ~metasenv (text,prefix_len,term)) in let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in lexicon_status_ref := lexicon_status; metasenv,cic - +;; + (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term * rationale: lazy_term will be invoked in different context to obtain a term, * each invocation will disambiguate the term and can add aliases. Once all * disambiguations have been performed, the first returned function can be * used to obtain the resulting aliases *) -let disambiguate_lazy_term lexicon_status_ref term = +let disambiguate_lazy_term text prefix_len lexicon_status_ref term = (fun context metasenv ugraph -> let lexicon_status = !lexicon_status_ref in let (diff, metasenv, cic, ugraph) = @@ -59,12 +70,15 @@ let disambiguate_lazy_term lexicon_status_ref term = ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~context ~metasenv - term) in + (text,prefix_len,term)) in let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in lexicon_status_ref := lexicon_status; cic, metasenv, ugraph) +;; -let disambiguate_pattern lexicon_status_ref (wanted, hyp_paths, goal_path) = +let disambiguate_pattern + text prefix_len lexicon_status_ref (wanted, hyp_paths, goal_path) += let interp path = Disambiguate.interpretate_path [] path in let goal_path = HExtlib.map_option interp goal_path in let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in @@ -72,14 +86,17 @@ let disambiguate_pattern lexicon_status_ref (wanted, hyp_paths, goal_path) = match wanted with None -> None | Some wanted -> - let wanted = disambiguate_lazy_term lexicon_status_ref wanted in + let wanted = + disambiguate_lazy_term text prefix_len lexicon_status_ref wanted + in Some wanted in (wanted, hyp_paths, goal_path) +;; -let disambiguate_reduction_kind lexicon_status_ref = function +let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function | `Unfold (Some t) -> - let t = disambiguate_lazy_term lexicon_status_ref t in + let t = disambiguate_lazy_term text prefix_len lexicon_status_ref t in `Unfold (Some t) | `Demodulate | `Normalize @@ -87,12 +104,19 @@ let disambiguate_reduction_kind lexicon_status_ref = function | `Simpl | `Unfold None | `Whd as kind -> kind - -let disambiguate_tactic lexicon_status_ref context metasenv tactic = - let disambiguate_term = disambiguate_term lexicon_status_ref in - let disambiguate_pattern = disambiguate_pattern lexicon_status_ref in - let disambiguate_reduction_kind = disambiguate_reduction_kind lexicon_status_ref in - let disambiguate_lazy_term = disambiguate_lazy_term lexicon_status_ref in +;; + +let disambiguate_tactic + lexicon_status_ref context metasenv (text,prefix_len,tactic) += + let disambiguate_term = + disambiguate_term text prefix_len lexicon_status_ref in + let disambiguate_pattern = + disambiguate_pattern text prefix_len lexicon_status_ref in + let disambiguate_reduction_kind = + disambiguate_reduction_kind text prefix_len lexicon_status_ref in + let disambiguate_lazy_term = + disambiguate_lazy_term text prefix_len lexicon_status_ref in match tactic with | GrafiteAst.Absurd (loc, term) -> let metasenv,cic = disambiguate_term context metasenv term in @@ -224,7 +248,7 @@ let disambiguate_tactic lexicon_status_ref context metasenv tactic = let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Transitivity (loc, cic) -let disambiguate_obj lexicon_status ~baseuri metasenv obj = +let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) = let uri = match obj with | CicNotationPt.Inductive (_,(name,_,_,_)::_) @@ -239,12 +263,13 @@ let disambiguate_obj lexicon_status ~baseuri metasenv obj = singleton (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ()) ~aliases:lexicon_status.LexiconEngine.aliases - ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri obj) in + ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri + (text,prefix_len,obj)) in let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in lexicon_status, metasenv, cic -let disambiguate_command lexicon_status ~baseuri metasenv = - function +let disambiguate_command lexicon_status ~baseuri metasenv (text,prefix_len,cmd)= + match cmd with | GrafiteAst.Coercion _ | GrafiteAst.Default _ | GrafiteAst.Drop _ @@ -254,11 +279,13 @@ let disambiguate_command lexicon_status ~baseuri metasenv = lexicon_status,metasenv,cmd | GrafiteAst.Obj (loc,obj) -> let lexicon_status,metasenv,obj = - disambiguate_obj lexicon_status ~baseuri metasenv obj in + disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj)in lexicon_status, metasenv, GrafiteAst.Obj (loc,obj) -let disambiguate_macro lexicon_status_ref metasenv context macro = - let disambiguate_term = disambiguate_term lexicon_status_ref in +let disambiguate_macro + lexicon_status_ref metasenv context (text,prefix_len, macro) += + let disambiguate_term = disambiguate_term text prefix_len lexicon_status_ref in match macro with | GrafiteAst.WMatch (loc,term) -> let metasenv,term = disambiguate_term context metasenv term in diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli index b04aa3cde..582ab11ec 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli @@ -25,24 +25,32 @@ exception BaseUriNotSetYet +type tactic = + (CicNotationPt.term, CicNotationPt.term, + CicNotationPt.term GrafiteAst.reduction, string) + GrafiteAst.tactic + +type lazy_tactic = + (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) + GrafiteAst.tactic + val disambiguate_tactic: LexiconEngine.status ref -> Cic.context -> Cic.metasenv -> - (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string) GrafiteAst.tactic -> - Cic.metasenv * - (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic + tactic Disambiguate.disambiguator_input -> + Cic.metasenv * lazy_tactic val disambiguate_command: LexiconEngine.status -> baseuri:string option -> Cic.metasenv -> - CicNotationPt.obj GrafiteAst.command -> + (CicNotationPt.obj GrafiteAst.command) Disambiguate.disambiguator_input -> LexiconEngine.status * Cic.metasenv * Cic.obj GrafiteAst.command val disambiguate_macro: LexiconEngine.status ref -> Cic.metasenv -> Cic.context -> - CicNotationPt.term GrafiteAst.macro -> + (CicNotationPt.term GrafiteAst.macro) Disambiguate.disambiguator_input -> Cic.metasenv * Cic.term GrafiteAst.macro diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml index 2803c88f6..d9de808b0 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml @@ -37,7 +37,9 @@ exception Unbound_identifier of string type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list -type choose_interp_callback = (string * string) list list -> int list +type choose_interp_callback = + string -> int -> + (Token.flocation list * string * string) list list -> int list let mono_uris_callback ~id = if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true @@ -47,7 +49,7 @@ let mono_uris_callback ~id = else raise Ambiguous_input -let mono_interp_callback _ = 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 @@ -63,12 +65,10 @@ module Callbacks = let interactive_interpretation_choice interp = !_choose_interp_callback interp - let input_or_locate_uri ~(title:string) ?id = + 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 *) - let msg = match id with Some id -> id | _ -> "_" in - raise (Unbound_identifier msg) end module Disambiguator = Disambiguate.Make (Callbacks) @@ -95,6 +95,8 @@ let disambiguate_thing ~aliases ~universe (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 diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.mli b/helm/software/components/grafite_parser/grafiteDisambiguator.mli index b7c85f6af..b70eb737f 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguator.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguator.mli @@ -31,7 +31,9 @@ exception DisambiguationError of int * (Token.flocation option * string Lazy.t) list list type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list -type choose_interp_callback = (string * string) list list -> int list +type choose_interp_callback = + string -> int -> (Token.flocation list * string * string) list list -> + int list val set_choose_uris_callback: choose_uris_callback -> unit val set_choose_interp_callback: choose_interp_callback -> unit diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma index 44238d69e..64c65b266 100644 --- a/helm/software/matita/library/algebra/finite_groups.ma +++ b/helm/software/matita/library/algebra/finite_groups.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/algebra/finite_groups/". include "algebra/groups.ma". -record finite_enumerable (T:Type) : Type ≝ +record finite_enumerable (T:Type) : Type≝ { order: nat; repr: nat → T; index_of: T → nat; @@ -39,7 +39,7 @@ for @{ 'card $C }. interpretation "Finite_enumerable order" 'card C = (cic:/matita/algebra/finite_groups/order.con C _). -record finite_enumerable_SemiGroup : Type ≝ +record finite_enumerable_SemiGroup : Type≝ { semigroup:> SemiGroup; is_finite_enumerable:> finite_enumerable semigroup }. @@ -60,7 +60,7 @@ interpretation "Index_of_finite_enumerable representation" (* several definitions/theorems to be moved somewhere else *) -definition ltb ≝ λn,m. leb n m ∧ notb (eqb n m). +definition ltb ≝λn,m. leb n m ∧ notb (eqb n m). theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n (repr_index_of ? (is_finite_enumerable G)) in HH; apply (ex_intro ? ? (G \sub a)); - letin GOGO ≝ (refl_eq ? (repr ? (is_finite_enumerable G) O)); + letin GOGO ≝(refl_eq ? (repr ? (is_finite_enumerable G) O)); clearbody GOGO; rewrite < HH in GOGO; rewrite < HH in GOGO:(? ? % ?); rewrite > (op_associative ? G) in GOGO; - letin GaGa ≝ (H ? ? ? GOGO); + letin GaGa ≝(H ? ? ? GOGO); clearbody GaGa; clear GOGO; constructor 1; [ simplify; apply (semigroup_properties G) | unfold is_left_unit; intro; - letin GaxGax ≝ (refl_eq ? (G \sub a ·x)); - clearbody GaxGax; + letin GaxGax ≝(refl_eq ? (G \sub a ·x)); + clearbody GaxGax; (* demo *) rewrite < GaGa in GaxGax:(? ? % ?); rewrite > (op_associative ? (semigroup_properties G)) in GaxGax; apply (H ? ? ? GaxGax) | unfold is_right_unit; intro; - letin GaxGax ≝ (refl_eq ? (x·G \sub a)); + letin GaxGax ≝(refl_eq ? (x·G \sub a)); clearbody GaxGax; rewrite < GaGa in GaxGax:(? ? % ?); rewrite < (op_associative ? (semigroup_properties G)) in GaxGax; diff --git a/helm/software/matita/library/algebra/semigroups.ma b/helm/software/matita/library/algebra/semigroups.ma index 12ff95311..539228c8c 100644 --- a/helm/software/matita/library/algebra/semigroups.ma +++ b/helm/software/matita/library/algebra/semigroups.ma @@ -18,7 +18,7 @@ include "higher_order_defs/functions.ma". (* Magmas *) -record Magma : Type ≝ +record Magma : Type≝ { carrier:> Type; op: carrier → carrier → carrier }. @@ -32,10 +32,10 @@ interpretation "magma operation" 'magma_op a b = (* Semigroups *) -record isSemiGroup (M:Magma) : Prop ≝ +record isSemiGroup (M:Magma) : Prop≝ { op_associative: associative ? (op M) }. -record SemiGroup : Type ≝ +record SemiGroup : Type≝ { magma:> Magma; semigroup_properties:> isSemiGroup magma }. @@ -51,6 +51,6 @@ theorem is_left_unit_to_is_right_unit_to_eq: is_left_unit ? e → is_right_unit ? e' → e=e'. intros; rewrite < (H e'); - rewrite < (H1 e) in \vdash (? ? % ?); + rewrite < (H1 e) in \vdash (? ? % ?). reflexivity. qed. diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 96a016b95..a756e4042 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -682,8 +682,8 @@ - 350 - 250 + 450 + 400 title GTK_WINDOW_TOPLEVEL GTK_WIN_POS_NONE @@ -3043,6 +3043,19 @@ + + + + True + True + True + gtk-go-forward + True + GTK_RELIEF_NORMAL + True + 0 + + 0 diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index 18022691c..404809959 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -30,7 +30,7 @@ open Printf let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; -let disambiguate_tactic lexicon_status_ref grafite_status goal tac = +let disambiguate_tactic text prefix_len lexicon_status_ref grafite_status goal tac = let metasenv,tac = GrafiteDisambiguate.disambiguate_tactic lexicon_status_ref @@ -63,15 +63,15 @@ let disambiguate_macro lexicon_status_ref grafite_status macro context = GrafiteTypes.set_metasenv metasenv grafite_status,macro let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status - grafite_status ast + grafite_status (text,prefix_len,ast) = let lexicon_status_ref = ref lexicon_status in let new_grafite_status,new_objs = GrafiteEngine.eval_ast - ~disambiguate_tactic:(disambiguate_tactic lexicon_status_ref) + ~disambiguate_tactic:(disambiguate_tactic text prefix_len lexicon_status_ref) ~disambiguate_command:(disambiguate_command lexicon_status_ref) ~disambiguate_macro:(disambiguate_macro lexicon_status_ref) - ?do_heavy_checks ?clean_baseuri grafite_status ast in + ?do_heavy_checks ?clean_baseuri grafite_status (text,prefix_len,ast) in let new_lexicon_status = LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs in let new_aliases = @@ -99,7 +99,8 @@ let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status ((new_grafite_status,new_lexicon_status),None)::intermediate_states let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false) - ?do_heavy_checks ?clean_baseuri lexicon_status grafite_status str cb + ?do_heavy_checks ?clean_baseuri lexicon_status grafite_status + str cb = let rec loop lexicon_status grafite_status statuses = let loop = @@ -121,7 +122,7 @@ let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false) cb grafite_status ast; let new_statuses = eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status - grafite_status ast in + grafite_status ("",0,ast) in let grafite_status,lexicon_status = match new_statuses with [] -> assert false @@ -133,10 +134,3 @@ let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false) in loop lexicon_status grafite_status [] ;; - -let eval_string ~first_statement_only ~include_paths ?do_heavy_checks - ?clean_baseuri lexicon_status status str -= - eval_from_stream ~first_statement_only ~include_paths ?do_heavy_checks - ?clean_baseuri lexicon_status status (Ulexing.from_utf8_string str) - (fun _ _ -> ()) diff --git a/helm/software/matita/matitaEngine.mli b/helm/software/matita/matitaEngine.mli index a3c54dea6..3fb5c7637 100644 --- a/helm/software/matita/matitaEngine.mli +++ b/helm/software/matita/matitaEngine.mli @@ -28,9 +28,10 @@ val eval_ast : ?clean_baseuri:bool -> LexiconEngine.status -> GrafiteTypes.status -> - (CicNotationPt.term, CicNotationPt.term, + string * int * + ((CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) - GrafiteAst.statement -> + GrafiteAst.statement) -> ((GrafiteTypes.status * LexiconEngine.status) * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option ) list @@ -38,18 +39,9 @@ val eval_ast : (* heavy checks slow down the compilation process but give you some interesting * infos like if the theorem is a duplicate *) -val eval_string : - first_statement_only:bool -> - include_paths:string list -> - ?do_heavy_checks:bool -> - ?clean_baseuri:bool -> - LexiconEngine.status -> - GrafiteTypes.status -> - string -> - ((GrafiteTypes.status * LexiconEngine.status) * - (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option - ) list +(* should be used only by the compiler since it looses the + * disambiguation_context (text,prefix_len,_) *) val eval_from_stream : first_statement_only:bool -> include_paths:string list -> @@ -66,3 +58,4 @@ val eval_from_stream : ((GrafiteTypes.status * LexiconEngine.status) * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option ) list + diff --git a/helm/software/matita/matitaGtkMisc.ml b/helm/software/matita/matitaGtkMisc.ml index c397215a7..6407ae35d 100644 --- a/helm/software/matita/matitaGtkMisc.ml +++ b/helm/software/matita/matitaGtkMisc.ml @@ -443,8 +443,14 @@ let utf8_parsed_text s floc = let start, stop = HExtlib.loc_of_floc floc in let start_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:start in let stop_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:stop in + assert(stop_bytes >= start_bytes); let bytes = stop_bytes - start_bytes in - String.sub s start_bytes bytes, bytes + try + String.sub s start_bytes bytes, bytes + with Invalid_argument _ -> + Printf.eprintf "%s/%d/%d\n" s start_bytes bytes; + assert false + let utf8_string_length s = if BuildTimeConf.debug then diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index e9a84c9b4..04b86d0b7 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -1256,7 +1256,8 @@ class interpModel = tree_store#get ~row:iter ~column:interp_no_col end -let interactive_interp_choice () choices = +let interactive_interp_choice () = + fun text prefix_len choices -> let gui = instance () in assert (choices <> []); let dialog = gui#newRecordDialog () in @@ -1285,6 +1286,127 @@ let interactive_interp_choice () choices = GtkThread.main (); (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel) +let interactive_string_choice + text prefix_len ?(title = "") ?(msg = "") () ~id locs uris += + let gui = instance () in + let dialog = gui#newUriDialog () in + dialog#uriEntryHBox#misc#hide (); + dialog#uriChoiceSelectedButton#misc#hide (); + dialog#uriChoiceAutoButton#misc#hide (); + dialog#uriChoiceConstantsButton#misc#hide (); + dialog#uriChoiceTreeView#selection#set_mode + (`SINGLE :> Gtk.Tags.selection_mode); + let model = new stringListModel dialog#uriChoiceTreeView in + let choices = ref None in + dialog#uriChoiceDialog#set_title title; + let hack_len = MatitaGtkMisc.utf8_string_length text in + let rec colorize acc_len = function + | [] -> + let floc = HExtlib.floc_of_loc (acc_len,hack_len) in + fst(MatitaGtkMisc.utf8_parsed_text text floc) + | he::tl -> + let start, stop = HExtlib.loc_of_floc he in + let floc1 = HExtlib.floc_of_loc (acc_len,start) in + let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in + let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in + str1 ^ "" ^ str2 ^ "" ^ colorize stop tl + in +(* List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in + Printf.eprintf "(%d,%d)" start stop) locs; *) + let locs = + List.sort + (fun loc1 loc2 -> + fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2)) + locs + in +(* prerr_endline "XXXXXXXXXXXXXXXXXXXX"; + List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in + Printf.eprintf "(%d,%d)" start stop) locs; + prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *) + dialog#uriChoiceLabel#set_use_markup true; + let txt = colorize 0 locs in + let txt,_ = MatitaGtkMisc.utf8_parsed_text txt + (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt)) + in + dialog#uriChoiceLabel#set_label txt; + List.iter model#easy_append uris; + let return v = + choices := v; + dialog#uriChoiceDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); + connect_button dialog#uriChoiceForwardButton (fun _ -> + match model#easy_selection () with + | [] -> () + | uris -> return (Some uris)); + connect_button dialog#uriChoiceAbortButton (fun _ -> return None); + dialog#uriChoiceDialog#show (); + GtkThread.main (); + (match !choices with + | None -> raise MatitaTypes.Cancel + | Some uris -> uris) + +let interactive_interp_choice () text prefix_len choices = +(* List.iter (fun (l,_,_) -> + List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in + Printf.eprintf "(%d,%d)" start stop) l; prerr_endline "") + ((List.hd choices)); *) + let filter_choices filter = + let rec is_compatible filter = + function + [] -> true + | (_,id,dsc)::tl -> + try + if List.assoc id filter = dsc then + is_compatible filter tl + else + false + with + Not_found -> true + in + List.filter (fun (_,interp) -> is_compatible filter interp) + in + let rec get_choices id = + function + [] -> [] + | (_,he)::tl -> + let _,_,dsc = List.find (fun (_,id',_) -> id = id') he in + dsc :: (List.filter (fun dsc' -> dsc <> dsc') (get_choices id tl)) + in + let example_interp = + match choices with + [] -> assert false + | he::_ -> he in + let ask_user id locs choices = + interactive_string_choice + text prefix_len + ~title:"Ambiguous input" + ~msg:("Choose an interpretation for " ^ id) () ~id locs choices + in + let rec classify ids filter partial_interpretations = + match ids with + [] -> List.map fst partial_interpretations + | (locs,id,_)::tl -> + let choices = get_choices id partial_interpretations in + let chosen_dsc = + match choices with + [dsc] -> dsc + | _ -> + match ask_user id locs choices with + [x] -> x + | _ -> assert false + in + let filter = (id,chosen_dsc)::filter in + let compatible_interps = filter_choices filter partial_interpretations in + classify tl filter compatible_interps in + let enumerated_choices = + let idx = ref ~-1 in + List.map (fun interp -> incr idx; !idx,interp) choices + in + classify example_interp [] enumerated_choices + let _ = (* disambiguator callbacks *) GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ()); diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index b853ddd4e..07a7cbd2e 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -85,9 +85,11 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal let parsed_text_length = String.length skipped_txt + String.length nonskipped_txt in + let text = skipped_txt ^ nonskipped_txt in + let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in let enriched_history_fragment = MatitaEngine.eval_ast ~do_heavy_checks:true - lexicon_status grafite_status st + lexicon_status grafite_status (text,prefix_len,st) in let enriched_history_fragment = List.rev enriched_history_fragment in (* really fragile *) -- 2.39.2