("Unable to create projection " ^ name ^ " because it requires " ^ depend);
status
) status projections
+
+(* to avoid a long list of recursive functions *)
+let eval_from_stream_greedy_ref = ref (fun _ _ _ -> assert false);;
-let eval_command output status cmd =
+let eval_command status cmd =
match cmd with
+ | TacticAst.Include (loc, path) ->
+ let path = MatitaMisc.obj_file_of_script path in
+ let stream = Stream.of_channel (open_in path) in
+ let status = ref status in
+ (try
+ !eval_from_stream_greedy_ref status stream (fun _ _ -> ())
+ with
+ CicTextualParser2.Parse_error (floc,err) as exc ->
+ (* check for EOI *)
+ if Stream.peek stream = None then ()
+ else raise exc
+ );
+ !status
| TacticAst.Set (loc, name, value) ->
let value =
if name = "baseuri" then
| TacticAst.Coercion (loc, coercion) ->
eval_coercion status coercion
| TacticAst.Alias (loc, spec) ->
- let status =
+ let aliases =
match spec with
| TacticAst.Ident_alias (id,uri) ->
- {status with aliases =
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Id id)
- ("boh?",(fun _ _ _ -> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
- status.aliases }
+ DisambiguateTypes.Environment.add
+ (DisambiguateTypes.Id id)
+ (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
+ status.aliases
| TacticAst.Symbol_alias (symb, instance, desc) ->
- {status with aliases =
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Symbol (symb,instance))
- (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
- status.aliases }
+ DisambiguateTypes.Environment.add
+ (DisambiguateTypes.Symbol (symb,instance))
+ (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
+ status.aliases
| TacticAst.Number_alias (instance,desc) ->
- {status with aliases =
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Num instance)
- (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
+ DisambiguateTypes.Environment.add
+ (DisambiguateTypes.Num instance)
+ (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases
in
- output (TacticAstPp.pp_alias spec ^ ".\n");
- status
+ MatitaSync.set_proof_aliases status aliases
| TacticAst.Obj (loc,obj) ->
let ext,name =
match obj with
| Cic.CurrentProof _
| Cic.Variable _ -> assert false
-let eval_executable output status ex =
+let eval_executable status ex =
match ex with
| TacticAst.Tactical (_, tac) -> eval_tactical status tac
- | TacticAst.Command (_, cmd) -> eval_command output status cmd
+ | TacticAst.Command (_, cmd) -> eval_command status cmd
| TacticAst.Macro (_, mac) ->
command_error (sprintf "The macro %s can't be in a script"
(TacticAstPp.pp_macro_cic mac))
let eval_comment status c = status
-let eval output status st =
+let eval status st =
match st with
- | TacticAst.Executable (_,ex) -> eval_executable output status ex
+ | TacticAst.Executable (_,ex) -> eval_executable status ex
| TacticAst.Comment (_,c) -> eval_comment status c
let disambiguate_term status term =
| Intermediate _ -> Intermediate metasenv
| Proof _ -> assert false
in
- let status =
- { status with
- aliases = aliases;
- proof_status = proof_status }
- in
+ let status = { status with proof_status = proof_status } in
+ let status = MatitaSync.set_proof_aliases status aliases in
status, cic
let disambiguate_obj status obj =
| Intermediate _
| Proof _ -> assert false
in
- let status =
- { status with
- aliases = aliases;
- proof_status = proof_status }
- in
+ let status = { status with proof_status = proof_status } in
+ let status = MatitaSync.set_proof_aliases status aliases in
status, cic
let disambiguate_pattern status (wanted, hyp_paths, goal_path) =
status, tacticals
let disambiguate_command status = function
+ | TacticAst.Include (loc,path) as cmd -> status,cmd
| TacticAst.Coercion (loc, term) ->
let status, term = disambiguate_term status term in
status, TacticAst.Coercion (loc,term)
let status, ex = disambiguate_executable status ex in
status, TacticAst.Executable (loc,ex)
-let eval_ast output status ast =
+let eval_ast status ast =
let status,st = disambiguate_statement status ast in
(* this disambiguation step should be deferred to support tacticals *)
- eval output status st
+ eval status st
-let eval_from_stream output status str cb =
+let eval_from_stream status str cb =
let stl = CicTextualParser2.parse_statements str in
List.iter
- (fun ast -> cb !status ast;status := eval_ast output !status ast) stl
+ (fun ast -> cb !status ast;status := eval_ast !status ast) stl
-let eval_from_stream_greedy output status str cb =
+let eval_from_stream_greedy status str cb =
while true do
print_string "matita> ";
flush stdout;
let ast = CicTextualParser2.parse_statement str in
cb !status ast;
- status := eval_ast output !status ast
+ status := eval_ast !status ast
done
+;;
+
+(* to avoid a long list of recursive functions *)
+eval_from_stream_greedy_ref := eval_from_stream_greedy;;
-let eval_string output status str =
- eval_from_stream output status (Stream.of_string str) (fun _ _ -> ())
+let eval_string status str =
+ eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
let default_options () =
(*
let initial_status =
lazy {
aliases = DisambiguateTypes.empty_environment;
+ moo_content_rev = [];
proof_status = No_proof;
options = default_options ();
objects = [];
projects / helm.git / blobdiff