(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
match ast with
| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
+ | GrafiteAst.ApplyS (_, term) ->
+ Tactics.applyS ~term ~dbd:(LibraryDb.instance ())
| GrafiteAst.Assumption _ -> Tactics.assumption
- | GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
- AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
- ~dbd:(LibraryDb.instance ()) ()
+ | GrafiteAst.Auto (_,params) ->
+ AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ())
| GrafiteAst.Change (_, pattern, with_what) ->
Tactics.change ~pattern with_what
| GrafiteAst.Clear (_,id) -> Tactics.clear id
| GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
| GrafiteAst.Contradiction _ -> Tactics.contradiction
- | GrafiteAst.Compare (_, term) -> Tactics.compare term
| GrafiteAst.Constructor (_, n) -> Tactics.constructor n
| GrafiteAst.Cut (_, ident, term) ->
let names = match ident with None -> [] | Some id -> [id] in
Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
- | GrafiteAst.DecideEquality _ -> Tactics.decide_equality
| GrafiteAst.Decompose (_, types, what, names) ->
let to_type = function
| GrafiteAst.Type (uri, typeno) -> uri, typeno
|+ 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
}
let coercion_moo_statement_of uri =
GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false)
+let refinement_toolkit = {
+ RefinementTool.type_of_aux' =
+ (fun ?localization_tbl e c t u ->
+ let saved = !CicRefine.insert_coercions in
+ CicRefine.insert_coercions:= false;
+ let rc =
+ try
+ let t, ty, metasenv, ugraph =
+ CicRefine.type_of_aux' ?localization_tbl e c t u in
+ RefinementTool.Success (t, ty, metasenv, ugraph)
+ with
+ | CicRefine.RefineFailure s
+ | CicRefine.Uncertain s
+ | CicRefine.AssertFailure s -> RefinementTool.Exception s
+ in
+ CicRefine.insert_coercions := saved;
+ rc);
+ RefinementTool.ppsubst = CicMetaSubst.ppsubst;
+ RefinementTool.apply_subst = CicMetaSubst.apply_subst;
+ RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv;
+ RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
+ }
+
let eval_coercion status ~add_composites uri =
- let basedir = Helm_registry.get "matita.basedir" in
let status,compounds =
- prerr_endline "evaluating a coercion command";
- GrafiteSync.add_coercion ~basedir ~add_composites status uri in
+ GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri in
let moo_content = coercion_moo_statement_of uri in
let status = GrafiteTypes.add_moo_content [moo_content] status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
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))
MatitaTacticals.solve_tactics
~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
- | GrafiteAst.Skip loc -> MatitaTacticals.skip
- | GrafiteAst.Dot loc -> MatitaTacticals.dot
- | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon
- | GrafiteAst.Branch loc -> MatitaTacticals.branch
- | GrafiteAst.Shift loc -> MatitaTacticals.shift
- | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i
- | GrafiteAst.Merge loc -> MatitaTacticals.merge
- | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals
- | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus
+ | GrafiteAst.Skip _loc -> MatitaTacticals.skip
+ | GrafiteAst.Dot _loc -> MatitaTacticals.dot
+ | GrafiteAst.Semicolon _loc -> MatitaTacticals.semicolon
+ | GrafiteAst.Branch _loc -> MatitaTacticals.branch
+ | GrafiteAst.Shift _loc -> MatitaTacticals.shift
+ | GrafiteAst.Pos (_loc, i) -> MatitaTacticals.pos i
+ | GrafiteAst.Merge _loc -> MatitaTacticals.merge
+ | GrafiteAst.Focus (_loc, goals) -> MatitaTacticals.focus goals
+ | GrafiteAst.Unfocus _loc -> MatitaTacticals.unfocus
+ | GrafiteAst.Wildcard _loc -> MatitaTacticals.wildcard
in
let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in
let status = (* is proof completed? *)
| _ -> None)
fields
in
+ (*
prerr_endline "wanted coercions:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
- wanted_coercions;
+ wanted_coercions; *)
let coercions, moo_content =
List.split
(HExtlib.filter_map
None)
lemmas)
in
- prerr_endline "actual coercions:";
+ (* prerr_endline "actual coercions:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
- coercions;
+ coercions; *)
let status = GrafiteTypes.add_moo_content moo_content status in
{status with
GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions},
lemmas
let add_obj uri obj status =
- let basedir = Helm_registry.get "matita.basedir" in
- let status,lemmas = GrafiteSync.add_obj ~basedir uri obj status in
+ 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 basedir = Helm_registry.get "matita.basedir" 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 ->
LibraryObjects.set_default what uris;
GrafiteTypes.add_moo_content [cmd] status,[]
| GrafiteAst.Include (loc, baseuri) ->
- let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
- if not (Sys.file_exists moopath) then
- raise (IncludedFileNotCompiled moopath);
+ let moopath_rw, moopath_r =
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true,
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:false
+ in
+ let moopath =
+ if Sys.file_exists moopath_r then moopath_r else
+ if Sys.file_exists moopath_rw then moopath_rw else
+ raise (IncludedFileNotCompiled moopath_rw)
+ in
let status = eval_from_moo.efm_go status moopath in
status,[]
| GrafiteAst.Set (loc, name, value) ->
HLog.error (sprintf "uri %s belongs to a read-only repository" value);
raise (ReadOnlyUri value)
end;
- if not (GrafiteMisc.is_empty value) && opts.clean_baseuri then begin
+ if not (Http_getter_storage.is_empty value) &&
+ opts.clean_baseuri
+ then begin
HLog.message ("baseuri " ^ value ^ " is not empty");
HLog.message ("cleaning baseuri " ^ value);
- LibraryClean.clean_baseuris ~basedir [value];
+ LibraryClean.clean_baseuris [value];
+ assert (Http_getter_storage.is_empty value);
end;
+ HExtlib.mkdir
+ (Filename.dirname (Http_getter.filename ~writable:true (value ^
+ "/foo.con")));
end;
GrafiteTypes.set_option status name value,[]
| GrafiteAst.Drop loc -> raise Drop
(match types with (name,_,_,_)::_ -> name | _ -> assert false)
| _ -> assert false in
let uri =
- UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext)
- in
+ UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext) in
+ let obj = CicRefine.pack_coercion_obj obj in
let metasenv = GrafiteTypes.get_proof_metasenv status in
match obj with
| Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
("Theorem already proved: " ^ UriManager.string_of_uri x ^
"\nPlease use a variant."));
end;
- assert (metasenv = metasenv');
- let initial_proof = (Some uri, metasenv, bo, ty) in
- let initial_stack = Continuationals.Stack.of_metasenv metasenv in
+ let initial_proof = (Some uri, metasenv', bo, ty) in
+ let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
{ status with GrafiteTypes.proof_status =
GrafiteTypes.Incomplete_proof
{ GrafiteTypes.proof = initial_proof; stack = initial_stack } },
{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
projects / helm.git / blobdiff