mentre si compila Z/times.ma. Il bug sembra essere transiente.
- in MatitaEngine unificare/rimuovere eval_string, eval_from_stream e
eval_from_stream_greedy
- - disambiguazione: attualmente io (CSC) ho committato la versione di
- disambiguate.ml che NON ricorda gli alias in caso di disambiguazione
- univoca (senza scelte per l'utente). [ cercare commento "Experimental" ]
- Il problema di questa soluzione e' che rallenta in maniera significativa
- l'esecuzione degli script. DOMANDA: quanto costano le fasi di
- fetch/decode/execute delle linee dello script?
- Una possibile alternativa e' avere alias "soft": se la disambiguazione
- fallisce gli alias soft vengono ripuliti e si riprova.
- Altra soluzione (Gares): avere alias multipli e provare tutti gli alias
- multipli. Da combinare con il "ritenta con istanze multiple in caso di
- fallimento".
- SOLUZIONE PENSATA CON ANDREA: 1. la interpretate aggiunge un alias
- implicito; 2. gli alias vengono ricordati come nella soluzione originale
- (e veloce); 3. se la disambiguazione fallisce, allora gli alias vengono
- dimenticati (quali? tutti? tutti tranne quelli chiesti all'utente?)
- e si ritenta; se fallisce ancora si generano
- istanze differenti e si ritenta; 4. ritentare anche senza e poi con
- coercions? oppure ordinare preferendo la soluzione che non ha introdotto
- coercions?; 5. che fare se alla fine restano piu' scelte? se si mettono
- gli alias nello script viene un paciugo, credo! in particolare quando
- vengono usate n istanze
- matitamake foo/a.ma non funziona; bisogna chiamarlo con
matitamake /x/y/z/foo/a.ma
- notazione -> Luca e Zack
DEMONI E ALTRO
DONE
+- disambiguazione: attualmente io (CSC) ho committato la versione di
+ disambiguate.ml che NON ricorda gli alias in caso di disambiguazione
+ univoca (senza scelte per l'utente). [ cercare commento "Experimental" ]
+ Il problema di questa soluzione e' che rallenta in maniera significativa
+ l'esecuzione degli script. DOMANDA: quanto costano le fasi di
+ fetch/decode/execute delle linee dello script?
+ Una possibile alternativa e' avere alias "soft": se la disambiguazione
+ fallisce gli alias soft vengono ripuliti e si riprova.
+ Altra soluzione (Gares): avere alias multipli e provare tutti gli alias
+ multipli. Da combinare con il "ritenta con istanze multiple in caso di
+ fallimento".
+ SOLUZIONE PENSATA CON ANDREA: 1. la interpretate aggiunge un alias
+ implicito; 2. gli alias vengono ricordati come nella soluzione originale
+ (e veloce); 3. se la disambiguazione fallisce, allora gli alias vengono
+ dimenticati (quali? tutti? tutti tranne quelli chiesti all'utente?)
+ e si ritenta; se fallisce ancora si generano
+ istanze differenti e si ritenta; 4. ritentare anche senza e poi con
+ coercions? oppure ordinare preferendo la soluzione che non ha introdotto
+ coercions?; 5. che fare se alla fine restano piu' scelte? se si mettono
+ gli alias nello script viene un paciugo, credo! in particolare quando
+ vengono usate n istanze -> Zack, CSC
- theorem t: True. elim O. ==> BOOM! unificazione di una testa flessibile con
True -> Gares
- parsing contestuale (tattiche replace, change e forse altre)
capire dove fare la select per avere i contesti in cui disambiguare gli
- altri argomenti. -> Zack, Enrico, CSC
+ altri argomenti. -> Zack
- tattica unfold su rel a let-in bound variables: c'e' ancora un bug
aperto: "unfold x in H:..." la x passata alla unfold vive nel contesto
del goal e non in quello del pattern. Pertanto invece di cercare di
con pattern, visto che in tal caso e' l'intero parsing a dover essere
fatto in un contesto differente. Risolvendo quel bug si risolve
automaticamente anche questo.
- -> Zack, Enrico, CSC
+ -> Zack
- Usare il cicbrowser per fare "Whelp instance": lui riscrive la barra
con la notazione alla Coq V7.0 che non riesce piu' a riparsare! -> Zack
- implementare inclusione file di configurazione (perche' ora tutti
exception Ambiguous_input
-type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
+type choose_uris_callback =
+ id:string -> UriManager.uri list -> UriManager.uri list
+
type choose_interp_callback = (string * string) list list -> int list
let mono_uris_callback ~id =
function l -> l
else
raise Ambiguous_input
+
let mono_interp_callback _ = raise Ambiguous_input
let _choose_uris_callback = ref mono_uris_callback
(* implement module's API *)
-let disambiguate_term = Disambiguator.disambiguate_term
+let disambiguate_thing ~aliases
+ ~(f:?fresh_instances:bool -> aliases:Disambiguate.aliases -> 'a -> 'b)
+ ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b)
+ (thing: 'a)
+=
+ let library = false, DisambiguateTypes.empty_environment in
+ let multi_aliases = true, aliases in
+ let mono_aliases = false, aliases in
+ let passes = (* <fresh_instances?, aliases, coercions?> *)
+ [ (false, mono_aliases, false);
+ (false, multi_aliases, false);
+ (true, library, false);
+ (true, mono_aliases, true);
+ (true, multi_aliases, true);
+ (true, library, true);
+ ]
+ in
+ let try_pass (fresh_instances, aliases, use_coercions) =
+ CoercDb.use_coercions := use_coercions;
+ f ~fresh_instances ~aliases thing
+ in
+ let rec aux =
+ function
+ | [ pass ] -> try_pass pass
+ | hd :: tl ->
+ (try
+ try_pass hd
+ with Disambiguate.NoWellTypedInterpretation ->
+ let (_, user_asked) as res = aux tl in
+ if user_asked then res else set_aliases aliases res)
+ | [] -> assert false
+ in
+ let saved_use_coercions = !CoercDb.use_coercions in
+ try
+ let res = aux passes in
+ CoercDb.use_coercions := saved_use_coercions;
+ res
+ with exn ->
+ CoercDb.use_coercions := saved_use_coercions;
+ raise exn
+
+let set_aliases aliases (choices, user_asked) =
+ (List.map (fun (_, a, b, c) -> aliases, a, b, c) choices),
+ user_asked
+
+let disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph ~aliases term =
+ let f =
+ Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
+ in
+ disambiguate_thing ~aliases ~f ~set_aliases term
+
+let disambiguate_obj ~dbd ~aliases ~uri obj =
+ let f = Disambiguator.disambiguate_obj ~dbd ~uri in
+ disambiguate_thing ~aliases ~f ~set_aliases obj
-let disambiguate_obj = Disambiguator.disambiguate_obj
(** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *)
-include Disambiguate.Disambiguator
- (*
- * val disambiguate_term: ...
- *)
+val disambiguate_term :
+ dbd:Mysql.dbd ->
+ context:Cic.context ->
+ metasenv:Cic.metasenv ->
+ ?initial_ugraph:CicUniv.universe_graph ->
+ aliases:DisambiguateTypes.environment -> (* previous interpretation status *)
+ DisambiguateTypes.term ->
+ (DisambiguateTypes.environment * (* new interpretation status *)
+ Cic.metasenv * (* new metasenv *)
+ Cic.term *
+ CicUniv.universe_graph) list * (* disambiguated term *)
+ bool (* has interactive_interpretation_choice been invoked? *)
+
+(** @param fresh_instances as per disambiguate_term *)
+val disambiguate_obj :
+ dbd:Mysql.dbd ->
+ aliases:DisambiguateTypes.environment -> (* previous interpretation status *)
+ uri:UriManager.uri option -> (* required only for inductive types *)
+ GrafiteAst.obj ->
+ (DisambiguateTypes.environment * (* new interpretation status *)
+ Cic.metasenv * (* new metasenv *)
+ Cic.obj *
+ CicUniv.universe_graph) list * (* disambiguated obj *)
+ bool (* has interactive_interpretation_choice been invoked? *)
| GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
let singleton = function
- | [x] -> x
+ | [x], _ -> x
| _ -> assert false
let disambiguate_term status_ref term =
cic, metasenv, ugraph)
let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
- let interp path =
- Disambiguate.interpretate_path [] !status_ref.aliases path
- in
+ let interp path = Disambiguate.interpretate_path [] path in
let goal_path = interp goal_path in
let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
let wanted =
| GrafiteAst.Inductive _ -> assert false
| GrafiteAst.Theorem _ -> None in
let (aliases, metasenv, cic, _) =
- match
- MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
- ~aliases:(status.aliases) ~uri obj
- with
- | [x] -> x
- | _ -> assert false
+ singleton
+ (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
+ ~aliases:(status.aliases) ~uri obj)
in
let proof_status =
match status.proof_status with
set_option status name value
| GrafiteAst.Drop loc -> raise Drop
| GrafiteAst.Qed loc ->
- let uri, metasenv, bo, ty =
+ let uri, metasenv, bo, ty =
match status.proof_status with
| Proof (Some uri, metasenv, body, ty) ->
uri, metasenv, body, ty
code in DisambiguatePp *)
match spec with
| GrafiteAst.Ident_alias (id,uri) ->
- DisambiguateTypes.Environment.add
+ DisambiguateTypes.Environment.cons
(DisambiguateTypes.Id id)
(uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
status.aliases
| GrafiteAst.Symbol_alias (symb, instance, desc) ->
- DisambiguateTypes.Environment.add
+ DisambiguateTypes.Environment.cons
(DisambiguateTypes.Symbol (symb,instance))
(DisambiguateChoices.lookup_symbol_by_dsc symb desc)
status.aliases
| GrafiteAst.Number_alias (instance,desc) ->
- DisambiguateTypes.Environment.add
+ DisambiguateTypes.Environment.cons
(DisambiguateTypes.Num instance)
(DisambiguateChoices.lookup_num_by_dsc desc) status.aliases
in
MatitaSync.set_proof_aliases status aliases
| GrafiteAst.Render _ -> assert false (* ZACK: to be removed *)
| GrafiteAst.Dump _ -> assert false (* ZACK: to be removed *)
- | GrafiteAst.Interpretation _
+ | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
+ let status' =
+ { status with
+ moo_content_rev =
+ (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev }
+ in
+ let aliases' =
+ DisambiguateTypes.Environment.cons
+ (DisambiguateTypes.Symbol (symbol, 0))
+ (DisambiguateChoices.lookup_symbol_by_dsc symbol dsc)
+ status.aliases
+ in
+ MatitaSync.set_proof_aliases status' aliases'
| GrafiteAst.Notation _ as stm ->
{ status with moo_content_rev =
(GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev }
let new_aliases =
match ex with
| TA.Command (_, TA.Alias _)
- | TA.Command (_, TA.Include _) -> DisambiguateTypes.Environment.empty
+ | TA.Command (_, TA.Include _)
+ | TA.Command (_, TA.Interpretation _) ->
+ DisambiguateTypes.Environment.empty
| _ -> MatitaSync.alias_diff ~from:status new_status
in
(* we remove the defined object since we consider them "automatic aliases" *)
let initial_space,status,new_status_and_text_list_rev =
let module DTE = DisambiguateTypes.Environment in
let module UM = UriManager in
- DTE.fold (
+ DTE.fold_flatten (
fun k ((v,_) as value) (initial_space,status,acc) ->
let b =
try
let initial_space =
if initial_space = "" then "\n" else initial_space in
initial_space ^
- DisambiguatePp.pp_environment(DTE.add k value DTE.empty) in
+ DisambiguatePp.pp_environment(DTE.cons k value DTE.empty) in
let new_status =
- {status with aliases = DTE.add k value status.aliases}
+ {status with aliases = DTE.cons k value status.aliases}
in
"\n",new_status,((new_status, new_text)::acc)
) new_aliases (initial_space,status,[]) in
let aliases = MatitaMisc.get_proof_aliases status in
let interps = MD.disambiguate_term dbd context metasenv aliases term in
match interps with
- | [_,_,x,_] -> x
+ | [_,_,x,_], _ -> x
| _ -> assert false
let eval_macro guistuff status unparsed_text parsed_text script mac =
in
let _, metasenv , term, ugraph =
match interps with
- | [x] -> x
+ | [x], _ -> x
| _ -> assert false
in
let ty,_ = CTC.type_of_aux' metasenv context term ugraph in
let alias_diff ~from status =
let module Map = DisambiguateTypes.Environment in
- Map.fold
+ Map.fold_flatten
(fun domain_item codomain_item acc ->
if not (Map.mem domain_item from.aliases) then
- Map.add domain_item codomain_item acc
+ Map.cons domain_item codomain_item acc
else
begin
try
- let description1 = fst(Map.find domain_item from.aliases) in
- let description2 = fst(Map.find domain_item status.aliases) in
- if description1 <> description2 then
- Map.add domain_item codomain_item acc
- else
- acc
+ let codomain1 = Map.find domain_item from.aliases in
+ let codomain2 = Map.find domain_item status.aliases in
+ List.fold_right
+ (fun item env ->
+ let dsc = fst item in
+ if not (List.exists (fun (dsc', _) -> dsc'=dsc) codomain1) then
+ Map.cons domain_item codomain_item env
+ else
+ env)
+ codomain2 acc
with Not_found -> acc
end)
status.aliases Map.empty
let set_proof_aliases status aliases =
- let new_status = {status with aliases = aliases } in
+ let new_status = { status with aliases = aliases } in
let diff = alias_diff ~from:status new_status in
let textual_diff =
if DisambiguateTypes.Environment.is_empty diff then
projects / helm.git / commitdiff