GrafiteTypes.set_metasenv metasenv status,tac
let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
- status ast
+ grafite_status ast
=
let lexicon_status_ref = ref lexicon_status in
- let status,new_objs =
+ let new_grafite_status,new_objs =
GrafiteEngine.eval_ast
~disambiguate_tactic:(disambiguate_tactic lexicon_status_ref)
~disambiguate_command:(disambiguate_command lexicon_status_ref)
- ?do_heavy_checks ?clean_baseuri status ast
+ ?do_heavy_checks ?clean_baseuri grafite_status ast in
+ let new_lexicon_status =
+ LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs in
+ let new_aliases =
+ LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in
+ let _,intermediate_states =
+ let baseuri = GrafiteTypes.get_string_option new_grafite_status "baseuri" in
+ List.fold_left
+ (fun (lexicon_status,acc) (k,((v,_) as value)) ->
+ let b =
+ try
+ UriManager.buri_of_uri (UriManager.uri_of_string v) = baseuri
+ with
+ UriManager.IllFormedUri _ -> false (* v is a description, not a URI *)
+ in
+ if b then
+ lexicon_status,acc
+ else
+ let new_lexicon_status =
+ LexiconEngine.set_proof_aliases lexicon_status [k,value]
+ in
+ new_lexicon_status,
+ ((new_grafite_status,new_lexicon_status),Some (k,value))::acc
+ ) (lexicon_status,[]) new_aliases
in
- let lexicon_status =
- LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs
- in
- lexicon_status,status
+ ((new_grafite_status,new_lexicon_status),None)::intermediate_states
let eval_from_stream ~include_paths ?(prompt=false) ?do_heavy_checks
- ?clean_baseuri lexicon_status status str cb
+ ?clean_baseuri lexicon_status grafite_status str cb
=
- let rec loop lexicon_status status =
- if prompt then (print_string "matita> "; flush stdout);
- try
- let lexicon_status,ast = GrafiteParser.parse_statement ~include_paths str lexicon_status in
- (match ast with
- GrafiteParser.LNone _ -> loop lexicon_status status
- | GrafiteParser.LSome ast ->
- cb status ast;
- let lexicon_status,status =
- eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status status ast
- in
- loop lexicon_status status)
- with
- End_of_file -> lexicon_status,status
-in
- loop lexicon_status status
+ let rec loop lexicon_status grafite_status statuses =
+ if prompt then (print_string "matita> "; flush stdout);
+ try
+ let lexicon_status,ast =
+ GrafiteParser.parse_statement ~include_paths str lexicon_status
+ in
+ (match ast with
+ GrafiteParser.LNone _ ->
+ loop lexicon_status grafite_status
+ (((grafite_status,lexicon_status),None)::statuses)
+ | GrafiteParser.LSome ast ->
+ cb grafite_status ast;
+ let new_statuses =
+ eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
+ grafite_status ast in
+ let grafite_status,lexicon_status =
+ match new_statuses with
+ [] -> assert false
+ | (s,_)::_ -> s
+ in
+ loop lexicon_status grafite_status (new_statuses @ statuses))
+ with
+ End_of_file -> statuses
+ in
+ loop lexicon_status grafite_status []
;;
let eval_string ~include_paths ?do_heavy_checks ?clean_baseuri lexicon_status
GrafiteTypes.status ->
(CicNotationPt.term, CicNotationPt.term,
CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
- GrafiteAst.statement -> LexiconEngine.status * GrafiteTypes.status
+ 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 *)
?clean_baseuri:bool ->
LexiconEngine.status ->
GrafiteTypes.status ->
- string -> LexiconEngine.status * GrafiteTypes.status
+ string ->
+ ((GrafiteTypes.status * LexiconEngine.status) *
+ (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option
+ ) list
val eval_from_stream :
include_paths:string list ->
(CicNotationPt.term, CicNotationPt.term,
CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
GrafiteAst.statement -> unit) ->
- LexiconEngine.status * GrafiteTypes.status
+ ((GrafiteTypes.status * LexiconEngine.status) *
+ (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option
+ ) list
[ grafite_status,
initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ]
| _ -> initial_space,grafite_status,[] in *)
- let new_lexicon_status,new_grafite_status =
+ let enriched_history_fragment =
MatitaEngine.eval_ast ~do_heavy_checks:true
new_lexicon_status new_grafite_status st
in
- let new_aliases =
- LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in
- (* we remove the defined object since we consider them "automatic aliases" *)
- let dummy_st =
- TA.Comment (HExtlib.dummy_floc, TA.Note (HExtlib.dummy_floc, ""))
- in
- let initial_space,lexicon_status,new_status_and_text_list_rev =
+ let _,new_text_list_rev =
let module DTE = DisambiguateTypes.Environment in
let module UM = UriManager in
- let baseuri = GrafiteTypes.get_string_option new_grafite_status "baseuri" in
- List.fold_left (
- fun (initial_space,lexicon_status,acc) (k,((v,_) as value)) ->
- let b =
- try
- UM.buri_of_uri (UM.uri_of_string v) = baseuri
- with
- UriManager.IllFormedUri _ -> false (* v is a description, not a URI *)
- in
- if b then
- initial_space,lexicon_status,acc
- else
- let new_text =
- let initial_space =
- if initial_space = "" then "\n" else initial_space in
- initial_space ^
- DisambiguatePp.pp_environment
- (DisambiguateTypes.Environment.add k value
- DisambiguateTypes.Environment.empty) in
- let new_lexicon_status =
- LexiconEngine.set_proof_aliases lexicon_status [k,value]
- in
- "\n",new_lexicon_status,(((new_grafite_status,new_lexicon_status), (new_text, Some dummy_st))::acc)
- ) (initial_space,lexicon_status,[]) new_aliases in
- let parsed_text = initial_space ^ parsed_text in
- let res =
- List.rev new_status_and_text_list_rev @ new_status_and_text_list' @
- [(new_grafite_status,new_lexicon_status),(parsed_text, Some st)]
+ List.fold_right (
+ fun (_,alias) (initial_space,acc) ->
+ match alias with
+ None -> initial_space,initial_space::acc
+ | Some (k,((v,_) as value)) ->
+ let new_text =
+ let initial_space =
+ if initial_space = "" then "\n" else initial_space
+ in
+ initial_space ^
+ DisambiguatePp.pp_environment
+ (DisambiguateTypes.Environment.add k value
+ DisambiguateTypes.Environment.empty)
+ in
+ "\n",new_text::acc
+ ) enriched_history_fragment (initial_space,[]) in
+ let new_text_list_rev =
+ match enriched_history_fragment,new_text_list_rev with
+ (_,None)::_, initial_space::tl -> (initial_space ^ parsed_text)::tl
+ | _,_ -> assert false
in
- res,parsed_text_length
+ let res =
+ try
+ List.combine (fst (List.split enriched_history_fragment)) new_text_list_rev
+ with
+ Invalid_argument _ -> assert false
+ in
+ res,parsed_text_length
let eval_with_engine
guistuff lexicon_status grafite_status user_goal parsed_text st
TA.Apply (loc, CicNotationPt.Uri (suri, None))),
Some (TA.Dot loc))))
in
+(*
let new_lexicon_status,new_grafite_status =
MatitaEngine.eval_ast lexicon_status grafite_status ast in
let extra_text =
comment parsed_text ^ "\n" ^ pp_eager_statement_ast ast in
[ (new_grafite_status,new_lexicon_status), (extra_text, Some ast) ],
parsed_text_length
+*) assert false (* implementarla con una ricorsione *)
| _ ->
HLog.error
"The result of the urichooser should be only 1 uri, not:\n";
match st with
| GrafiteParser.LNone loc ->
let parsed_text, parsed_text_length = text_of_loc loc in
- [(grafite_status,lexicon_status),(parsed_text,None)],
+ [(grafite_status,lexicon_status),parsed_text],
parsed_text_length
| GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) ->
let parsed_text, parsed_text_length = text_of_loc loc in
(offset+parsed_text_length, errorll))
in
(match s with
- | (statuses,(text, ast)) :: tl ->
- (statuses,(parsed_text ^ text, ast))::tl,
- parsed_text_length + len
+ | (statuses,text)::tl ->
+ (statuses,parsed_text ^ text)::tl,parsed_text_length + len
| [] -> [], 0)
| GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
let parsed_text, parsed_text_length = text_of_loc loc in
eval_statement buffer guistuff self#lexicon_status self#grafite_status
userGoal self st
in
- let (new_statuses, new_statements, new_asts) =
- let statuses, statements = List.split entries in
- let texts, asts = List.split statements in
- statuses, texts, asts
+ let new_statuses, new_statements =
+ let statuses, texts = List.split entries in
+ statuses, texts
in
- history <- List.rev new_statuses @ history;
- statements <- List.rev new_statements @ statements;
+ history <- new_statuses @ history;
+ statements <- new_statements @ statements;
let start = buffer#get_iter_at_mark (`MARK locked_mark) in
- let new_text = String.concat "" new_statements in
+ let new_text = String.concat "" (List.rev new_statements) in
if statement <> None then
buffer#insert ~iter:start new_text
else begin
projects / helm.git / commitdiff