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
{ 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
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 ()
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.
| 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
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) =
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
[]
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 _
(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 (
) 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
) (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
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
?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*
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 *
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
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 *)
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)));
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
| 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 =
| 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
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
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
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
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
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
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
?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 *
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 *
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
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
(** PROFILING *)
-let profiling_enabled = ComponentsConf.profiling
+let profiling_enabled = false ;; (* ComponentsConf.profiling *)
let something_profiled = ref false
(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
|+ 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
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
}
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
}
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
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))
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 ->
{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
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 ;
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
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
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
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) =
~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
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
| `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
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,_,_,_)::_)
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 _
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
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
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
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
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)
(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
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
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;
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
}.
(* 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<m.
intros;
| clear n;
letin f' ≝
(λx.
- let fSn1 ≝ f (S n1) in
- let fx ≝ f x in
+ let fSn1 ≝f (S n1) in
+ let fx ≝f x in
match ltb fSn1 fx with
[ true ⇒ pred fx
| false ⇒ fx
]
].
qed.
-
+(* demo *)
theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid:
∀G:finite_enumerable_SemiGroup.
left_cancellable ? (op G) →
right_cancellable ? (op G) →
∃e:G. isMonoid (mk_PreMonoid G e).
intros;
-letin f ≝ (λn.ι(G \sub O · G \sub n));
+letin f ≝(λn.ι(G \sub O · G \sub n));
cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
-[ letin EX ≝ (Hcut O ?);
+[ letin EX ≝(Hcut O ?);
[ apply le_O_n
| clearbody EX;
clear Hcut;
unfold f in EX;
elim EX;
clear EX;
- letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
+ letin HH ≝(eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
clearbody HH;
rewrite > (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;
(* Magmas *)
-record Magma : Type ≝
+record Magma : Type≝
{ carrier:> Type;
op: carrier → carrier → carrier
}.
(* 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
}.
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.
</widget>
<widget class="GtkDialog" id="RecordChoiceDialog">
- <property name="width_request">350</property>
- <property name="height_request">250</property>
+ <property name="width_request">450</property>
+ <property name="height_request">400</property>
<property name="title" translatable="yes">title</property>
<property name="type">GTK_WINDOW_TOPLEVEL</property>
<property name="window_position">GTK_WIN_POS_NONE</property>
</child>
</widget>
</child>
+
+ <child>
+ <widget class="GtkButton" id="uriChoiceForwardButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-go-forward</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">0</property>
+ </widget>
+ </child>
</widget>
<packing>
<property name="padding">0</property>
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
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 =
((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 =
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
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 _ _ -> ())
?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
(* 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 ->
((GrafiteTypes.status * LexiconEngine.status) *
(DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option
) list
+
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
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
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 ^ "<b>" ^ str2 ^ "</b>" ^ 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 ());
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 *)
projects / helm.git / commitdiff