open Printf
exception Drop
-exception IncludedFileNotCompiled of string (* file name *)
+(* mo file name, ma file name *)
+exception IncludedFileNotCompiled of string * string
exception Macro of
GrafiteAst.loc *
(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
let user_types = List.rev_map to_type types in
let dbd = LibraryDb.instance () in
let mk_fresh_name_callback = namer_of names in
- Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
+ Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
+ | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ())
| GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
| GrafiteAst.Elim (_, what, using, depth, names) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
| GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
let reduction =
match reduction_kind with
- | `Demodulate ->
- GrafiteTypes.command_error "demodulation can't be folded"
| `Normalize ->
PET.const_lazy_reduction
(CicReduction.normalize ~delta:false ~subst:[])
~mk_fresh_name_callback:(namer_of names) ()
| GrafiteAst.Inversion (_, term) ->
Tactics.inversion term
- | GrafiteAst.LApply (_, how_many, to_what, what, ident) ->
+ | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) ->
let names = match ident with None -> [] | Some id -> [id] in
- Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many
- ~to_what what
+ Tactics.lapply ~mk_fresh_name_callback:(namer_of names)
+ ~linear ?how_many ~to_what what
| GrafiteAst.Left _ -> Tactics.left
| GrafiteAst.LetIn (loc,term,name) ->
Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
| GrafiteAst.Reduce (_, reduction_kind, pattern) ->
(match reduction_kind with
- | `Demodulate -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~pattern
| `Normalize -> Tactics.normalize ~pattern
| `Reduce -> Tactics.reduce ~pattern
| `Simpl -> Tactics.simpl ~pattern
|+ 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
}
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? *)
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 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 ->
GrafiteTypes.add_moo_content [cmd] status,[]
| GrafiteAst.Include (loc, baseuri) ->
let moopath_rw, moopath_r =
- LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:true,
- LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:false
+ 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)
+ raise (IncludedFileNotCompiled (moopath_rw,baseuri))
in
let status = eval_from_moo.efm_go status moopath in
status,[]
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
{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