X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaScript.ml;h=26a0f2487503af6530841f54bc9b3c8cc0c35274;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=0d59d6f47fcfc9ba8b8e4031658bf382fcfe76dd;hpb=6b8da04f526b3484dc92f61a23a8e61e63422c13;p=helm.git diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 0d59d6f47..26a0f2487 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -24,9 +24,11 @@ *) open Printf - open MatitaTypes +let debug = true +let debug_print = if debug then prerr_endline else ignore + (** raised when one of the script margins (top or bottom) is reached *) exception Margin @@ -85,6 +87,24 @@ let eval_with_engine status user_goal parsed_text st = DisambiguateTypes.Environment.empty | _ -> MatitaSync.alias_diff ~from:status new_status in + (* we remove the defined object since we consider them "automathic aliases" *) + let new_aliases = + let module DTE = DisambiguateTypes.Environment in + let module UM = UriManager in + DTE.fold ( + fun k ((v,_) as value) acc -> + let b = + try + let v = UM.strip_xpointer (UM.uri_of_string v) in + List.exists (fun (s,_) -> s = v) new_status.objects + with UM.IllFormedUri _ -> false + in + if b then + acc + else + DTE.add k value acc + ) new_aliases DTE.empty + in let new_text = if DisambiguateTypes.Environment.is_empty new_aliases then parsed_text @@ -100,7 +120,7 @@ let eval_with_engine status user_goal parsed_text st = else new_text in - [ new_status, new_text ], parsed_text_length, None + [ new_status, new_text ], parsed_text_length let disambiguate term status = let module MD = MatitaDisambiguator in @@ -114,7 +134,8 @@ let disambiguate term status = | _ -> assert false let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text -script mac = + script mac += let module TA = TacticAst in let module TAPp = TacticAstPp in let module MQ = MetadataQuery in @@ -132,18 +153,18 @@ script mac = let l = MQ.match_term ~dbd term in let entry = `Whelp (TAPp.pp_macro_cic (TA.WMatch (loc, term)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length | TA.WInstance (loc, term) -> let term = disambiguate term status in let l = MQ.instance ~dbd term in let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length | TA.WLocate (loc, s) -> let l = MQ.locate ~dbd s in let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length | TA.WElim (loc, term) -> let term = disambiguate term status in let uri = @@ -154,21 +175,21 @@ script mac = let l = MQ.elim ~dbd uri in let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length | TA.WHint (loc, term) -> let term = disambiguate term status in let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in let l = List.map fst (MQ.experimental_hint ~dbd s) in let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length (* REAL macro *) | TA.Hint loc -> let s = MatitaMisc.get_proof_status status in let l = List.map fst (MQ.experimental_hint ~dbd s) in let selected = urichooser l in (match selected with - | [] -> [], parsed_text_length, None + | [] -> [], parsed_text_length | [uri] -> let ast = (TA.Executable (loc, @@ -181,8 +202,14 @@ script mac = comment parsed_text ^ "\n" ^ TAPp.pp_statement ast in - [ new_status , extra_text ], parsed_text_length, None - | _ -> assert false) + [ new_status , extra_text ], parsed_text_length + | _ -> + MatitaLog.error + "The result of the urichooser should be only 1 uri, not:\n"; + List.iter ( + fun u -> MatitaLog.error (u ^ "\n") + ) selected; + assert false) | TA.Check (_,term) -> let metasenv = MatitaMisc.get_proof_metasenv status in let context = MatitaMisc.get_proof_context status in @@ -199,8 +226,8 @@ script mac = let ty,_ = CTC.type_of_aux' metasenv context term ugraph in let t_and_ty = Cic.Cast (term,ty) in mathviewer#show_entry (`Cic (t_and_ty,metasenv)); - [], parsed_text_length, None - | TA.Abort _ -> + [], parsed_text_length +(* | TA.Abort _ -> let rec go_back () = let status = script#status.proof_status in match status with @@ -215,7 +242,7 @@ script mac = | TA.Undo (_, Some i) -> [], parsed_text_length, Some (fun () -> for j = 1 to i do script#retract () done) | TA.Undo (_, None) -> [], parsed_text_length, - Some (fun () -> script#retract ()) + Some (fun () -> script#retract ()) *) (* TODO *) | TA.Quit _ -> failwith "not implemented" | TA.Print (_,kind) -> failwith "not implemented" @@ -249,13 +276,13 @@ user_goal script s = let parsed_text, parsed_text_length = text_of_loc loc in let remain_len = String.length s - parsed_text_length in let s = String.sub s parsed_text_length remain_len in - let s,len, act = + let s,len = eval_statement status mathviewer urichooser user_goal script s in (match s with | (status, text) :: tl -> - ((status, parsed_text ^ text)::tl), (parsed_text_length + len), act - | [] -> [], 0, None) + ((status, parsed_text ^ text)::tl), (parsed_text_length + len) + | [] -> [], 0) | TacticAst.Executable (loc, ex) -> let parsed_text, parsed_text_length = text_of_loc loc in eval_executable @@ -290,7 +317,7 @@ object (self) method private _advance ?statement () = let s = match statement with Some s -> s | None -> self#getFuture in MatitaLog.debug ("evaluating: " ^ first_line s ^ " ..."); - let (entries, parsed_len, post_advance_action) = + let (entries, parsed_len) = eval_statement self#status mathviewer urichooser userGoal self s in let (new_statuses, new_statements) = List.split entries in (* @@ -306,10 +333,7 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; end; let new_text = String.concat "" new_statements in buffer#insert ~iter:start new_text; - self#moveMark (String.length new_text); - match post_advance_action with - | Some f -> f () - | _ -> () + self#moveMark (String.length new_text) method private _retract () = match statements, history with