-requires="helm-cic"
+requires="helm-cic helm-acic_content"
version="0.0.1"
archive(byte)="grafite.cma"
archive(native)="grafite.cmxa"
-requires="helm-library helm-grafite helm-tactics helm-ng_refiner"
+requires="helm-library helm-grafite helm-tactics helm-ng_tactics helm-ng_refiner"
version="0.0.1"
archive(byte)="grafite_engine.cma"
archive(native)="grafite_engine.cmxa"
--- /dev/null
+requires="helm-ng_disambiguation helm-lexicon helm-grafite_parser helm-tactics"
+version="0.0.1"
+archive(byte)="ng_tactics.cma"
+archive(native)="ng_tactics.cmxa"
ng_kernel \
ng_refiner \
ng_disambiguation \
- grafite_engine \
grafite_parser \
+ ng_tactics \
+ grafite_engine \
tptp_grafite \
$(NULL)
+content.cmi:
acic2content.cmi: content.cmi
content2cic.cmi: content.cmi
cicNotationUtil.cmi: cicNotationPt.cmo
cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi
acic2astMatcher.cmi: cicNotationPt.cmo
termAcicContent.cmi: cicNotationPt.cmo
+cicNotationPt.cmo:
+cicNotationPt.cmx:
content.cmo: content.cmi
content.cmx: content.cmi
acic2content.cmo: content.cmi acic2content.cmi
+content.cmi:
acic2content.cmi: content.cmi
content2cic.cmi: content.cmi
cicNotationUtil.cmi: cicNotationPt.cmx
cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi
acic2astMatcher.cmi: cicNotationPt.cmx
termAcicContent.cmi: cicNotationPt.cmx
+cicNotationPt.cmo:
+cicNotationPt.cmx:
content.cmo: content.cmi
content.cmx: content.cmi
acic2content.cmo: content.cmi acic2content.cmi
+proceduralHelpers.cmi:
+proceduralClassify.cmi:
+proceduralOptimizer.cmi:
+proceduralTypes.cmi:
+proceduralMode.cmi:
+proceduralConversion.cmi:
procedural1.cmi: proceduralTypes.cmi
proceduralTeX.cmi: proceduralTypes.cmi
+acic2Procedural.cmi:
proceduralHelpers.cmo: proceduralHelpers.cmi
proceduralHelpers.cmx: proceduralHelpers.cmi
proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi
+proceduralHelpers.cmi:
+proceduralClassify.cmi:
+proceduralOptimizer.cmi:
+proceduralTypes.cmi:
+proceduralMode.cmi:
+proceduralConversion.cmi:
procedural1.cmi: proceduralTypes.cmi
proceduralTeX.cmi: proceduralTypes.cmi
+acic2Procedural.cmi:
proceduralHelpers.cmo: proceduralHelpers.cmi
proceduralHelpers.cmx: proceduralHelpers.cmi
proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi
+extractor.cmo:
+extractor.cmx:
+extractor_manager.cmo:
+extractor_manager.cmx:
+extractor.cmo:
+extractor.cmx:
+extractor_manager.cmo:
+extractor_manager.cmx:
+table_creator.cmo:
+table_creator.cmx:
+table_creator.cmo:
+table_creator.cmx:
v8Parser.cmi: types.cmo
grafite.cmi: types.cmo
+engine.cmi:
+types.cmo:
+types.cmx:
+options.cmo:
+options.cmx:
v8Parser.cmo: types.cmo options.cmo v8Parser.cmi
v8Parser.cmx: types.cmx options.cmx v8Parser.cmi
v8Lexer.cmo: v8Parser.cmi options.cmo
v8Parser.cmi: types.cmx
grafite.cmi: types.cmx
+engine.cmi:
+types.cmo:
+types.cmx:
+options.cmo:
+options.cmx:
v8Parser.cmo: types.cmx options.cmx v8Parser.cmi
v8Parser.cmx: types.cmx options.cmx v8Parser.cmi
v8Lexer.cmo: v8Parser.cmi options.cmx
+cicUniv.cmi:
unshare.cmi: cic.cmo
deannotate.cmi: cic.cmo
cicParser.cmi: cic.cmo
+cicUniv.cmi:
unshare.cmi: cic.cmx
deannotate.cmi: cic.cmx
cicParser.cmi: cic.cmx
+eta_fixing.cmi:
+doubleTypeInference.cmi:
+cic2acic.cmi:
cic2Xml.cmi: cic2acic.cmi
eta_fixing.cmo: eta_fixing.cmi
eta_fixing.cmx: eta_fixing.cmi
+eta_fixing.cmi:
+doubleTypeInference.cmi:
+cic2acic.cmi:
cic2Xml.cmi: cic2acic.cmi
eta_fixing.cmo: eta_fixing.cmi
eta_fixing.cmx: eta_fixing.cmi
+cicDisambiguate.cmi:
+disambiguateChoices.cmi:
cicDisambiguate.cmo: cicDisambiguate.cmi
cicDisambiguate.cmx: cicDisambiguate.cmi
disambiguateChoices.cmo: disambiguateChoices.cmi
+cicDisambiguate.cmi:
+disambiguateChoices.cmi:
cicDisambiguate.cmo: cicDisambiguate.cmi
cicDisambiguate.cmx: cicDisambiguate.cmi
disambiguateChoices.cmo: disambiguateChoices.cmi
;;
let refine_term metasenv subst context uri ~use_coercions
- term ugraph ~localization_tbl =
+ term expty ugraph ~localization_tbl =
(* if benchmark then incr actual_refinements; *)
assert (uri=None);
debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
let saved_use_coercions = !CicRefine.insert_coercions in
try
CicRefine.insert_coercions := use_coercions;
+ let term =
+ match expty with
+ | None -> term
+ | Some ty -> Cic.Cast(term,ty)
+ in
let term', _, metasenv',ugraph1 =
CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl
+ in
+ let term' =
+ match expty, term' with
+ | None,_ -> term'
+ | Some _,Cic.Cast (term',_) -> term'
+ | _ -> assert false
in
CicRefine.insert_coercions := saved_use_coercions;
(Disambiguate.Ok (term', metasenv',[],ugraph1))
in
process_exn Stdpp.dummy_loc exn
-let refine_obj metasenv subst context uri ~use_coercions obj ugraph
+let refine_obj metasenv subst context uri ~use_coercions obj _ ugraph
~localization_tbl =
assert (context = []);
assert (metasenv = []);
List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some
(Cic.Anonymous,_) -> Some "_");;
-let disambiguate_term ~context ~metasenv ~subst ?goal
+let disambiguate_term ~context ~metasenv ~subst ~expty
?(initial_ugraph = CicUniv.oblivion_ugraph)
~mk_implicit ~description_of_alias ~mk_choice
~aliases ~universe ~lookup_in_library (text,prefix_len,term)
=
- let hint = match goal with
- | None -> (fun _ x -> x), fun k -> k
- | Some i ->
- (fun metasenv t ->
- let _,c,ty = CicUtil.lookup_meta i metasenv in
- assert(c=context);
- Cic.Cast(t,ty)),
- function
- | Disambiguate.Ok (t,m,s,ug) ->
- (match t with
- | Cic.Cast(t,_) -> Disambiguate.Ok (t,m,s,ug)
- | _ -> assert false)
- | k -> k
- in
let mk_localization_tbl x = Cic.CicHash.create x in
MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
~initial_ugraph ~aliases ~string_context_of_context
~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
~refine_thing:refine_term (text,prefix_len,term)
~mk_localization_tbl
- ~hint
+ ~expty
~freshen_thing:CicNotationUtil.freshen_term
~passes:(MultiPassDisambiguator.passes ())
let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
=
- let hint = (fun _ x -> x), fun k -> k in
let mk_localization_tbl x = Cic.CicHash.create x in
MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
~aliases ~universe ~uri ~string_context_of_context
~interpretate_thing:(interpretate_obj ~mk_choice)
~refine_thing:refine_obj
~mk_localization_tbl
- ~hint
+ ~expty:None
~passes:(MultiPassDisambiguator.passes ())
~freshen_thing:CicNotationUtil.freshen_obj
(text,prefix_len,obj)
context:Cic.context ->
metasenv:Cic.metasenv ->
subst:Cic.substitution ->
- ?goal:int ->
+ expty:Cic.term option ->
?initial_ugraph:CicUniv.universe_graph ->
mk_implicit:(bool -> 'alias) ->
description_of_alias:('alias -> string) ->
+cicExportation.cmi:
cicExportation.cmo: cicExportation.cmi
cicExportation.cmx: cicExportation.cmi
+cicExportation.cmi:
cicExportation.cmo: cicExportation.cmi
cicExportation.cmx: cicExportation.cmi
+cicLogger.cmi:
+cicEnvironment.cmi:
+cicPp.cmi:
+cicUnivUtils.cmi:
+cicSubstitution.cmi:
+cicMiniReduction.cmi:
+cicReduction.cmi:
+cicTypeChecker.cmi:
+freshNamesGenerator.cmi:
+cicDischarge.cmi:
cicLogger.cmo: cicLogger.cmi
cicLogger.cmx: cicLogger.cmi
cicEnvironment.cmo: cicEnvironment.cmi
+cicLogger.cmi:
+cicEnvironment.cmi:
+cicPp.cmi:
+cicUnivUtils.cmi:
+cicSubstitution.cmi:
+cicMiniReduction.cmi:
+cicReduction.cmi:
+cicTypeChecker.cmi:
+freshNamesGenerator.cmi:
+cicDischarge.cmi:
cicLogger.cmo: cicLogger.cmi
cicLogger.cmx: cicLogger.cmi
cicEnvironment.cmo: cicEnvironment.cmi
+cicMetaSubst.cmi:
+cicMkImplicit.cmi:
+termUtil.cmi:
+coercGraph.cmi:
+cicUnification.cmi:
+cicReplace.cmi:
+cicRefine.cmi:
cicMetaSubst.cmo: cicMetaSubst.cmi
cicMetaSubst.cmx: cicMetaSubst.cmi
cicMkImplicit.cmo: cicMkImplicit.cmi
+cicMetaSubst.cmi:
+cicMkImplicit.cmi:
+termUtil.cmi:
+coercGraph.cmi:
+cicUnification.cmi:
+cicReplace.cmi:
+cicRefine.cmi:
cicMetaSubst.cmo: cicMetaSubst.cmi
cicMetaSubst.cmx: cicMetaSubst.cmi
cicMkImplicit.cmo: cicMkImplicit.cmi
+renderingAttrs.cmi:
+cicNotationLexer.cmi:
+cicNotationParser.cmi:
+mpresentation.cmi:
+box.cmi:
+content2presMatcher.cmi:
termContentPres.cmi: cicNotationParser.cmi
boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi
cicNotationPres.cmi: mpresentation.cmi box.cmi
+renderingAttrs.cmi:
+cicNotationLexer.cmi:
+cicNotationParser.cmi:
+mpresentation.cmi:
+box.cmi:
+content2presMatcher.cmi:
termContentPres.cmi: cicNotationParser.cmi
boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi
cicNotationPres.cmi: mpresentation.cmi box.cmi
+disambiguateTypes.cmi:
disambiguate.cmi: disambiguateTypes.cmi
multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi
disambiguateTypes.cmo: disambiguateTypes.cmi
+disambiguateTypes.cmi:
disambiguate.cmi: disambiguateTypes.cmi
multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi
disambiguateTypes.cmo: disambiguateTypes.cmi
let disambiguate_thing
~context ~metasenv ~subst ~use_coercions
~string_context_of_context
- ~initial_ugraph:base_univ ~hint
+ ~initial_ugraph:base_univ ~expty
~mk_implicit ~description_of_alias
~aliases ~universe ~lookup_in_library
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
interpretate_thing ~context ~env:filled_env
~uri ~is_path:false thing ~localization_tbl
in
- let cic_thing = (fst hint) metasenv cic_thing in
let foo () =
- let k =
refine_thing metasenv subst context uri
- ~use_coercions cic_thing ugraph ~localization_tbl
- in
- let k = (snd hint) k in
- k
+ ~use_coercions cic_thing expty ugraph ~localization_tbl
in refine_profiler.HExtlib.profile foo ()
with
| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
use_coercions:bool ->
string_context_of_context:('context -> string option list) ->
initial_ugraph:'ugraph ->
- hint:
- ('metasenv -> 'raw_thing -> 'raw_thing) *
- (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
- ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
+ expty: 'refined_thing option ->
mk_implicit:(bool -> 'alias) ->
description_of_alias:('alias -> string) ->
aliases:'alias DisambiguateTypes.Environment.t ->
'raw_thing) ->
refine_thing:(
'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
- 'raw_thing -> 'ugraph -> localization_tbl:'cichash ->
+ 'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash ->
('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
mk_localization_tbl:(int -> 'cichash) ->
'ast_thing disambiguator_input ->
aux 1 [] passes
let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
- ~string_context_of_context ~initial_ugraph ~hint ~mk_implicit
+ ~string_context_of_context ~initial_ugraph ~expty ~mk_implicit
~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing
~domain_of_thing ~interpretate_thing ~refine_thing ~mk_localization_tbl thing
=
let thing = if fresh_instances then freshen_thing thing else thing in
Disambiguate.disambiguate_thing
~context ~metasenv ~subst ~use_coercions ~string_context_of_context
- ~initial_ugraph ~hint ~mk_implicit ~description_of_alias
+ ~initial_ugraph ~expty ~mk_implicit ~description_of_alias
~aliases ~universe ~lookup_in_library
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
~mk_localization_tbl (txt,len,thing)
subst:'subst ->
string_context_of_context:('context -> string option list) ->
initial_ugraph:'ugraph ->
- hint:
- ('metasenv -> 'raw_thing -> 'raw_thing) *
- (('refined_thing,'metasenv,'subst,'ugraph) Disambiguate.test_result ->
- ('refined_thing,'metasenv,'subst,'ugraph) Disambiguate.test_result) ->
+ expty: 'refined_thing option ->
mk_implicit:(bool -> 'alias) ->
description_of_alias:('alias -> string) ->
aliases:'alias DisambiguateTypes.Environment.t ->
'raw_thing) ->
refine_thing:(
'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
- 'raw_thing -> 'ugraph -> localization_tbl:'cichash ->
+ 'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash ->
('refined_thing, 'metasenv,'subst,'ugraph) Disambiguate.test_result) ->
mk_localization_tbl:(int -> 'cichash) ->
string * int * 'ast_thing ->
+componentsConf.cmi:
+hExtlib.cmi:
+hMarshal.cmi:
+patternMatcher.cmi:
+hLog.cmi:
+trie.cmi:
+hTopoSort.cmi:
+refCounter.cmi:
+graphvizPp.cmi:
componentsConf.cmo: componentsConf.cmi
componentsConf.cmx: componentsConf.cmi
hExtlib.cmo: hExtlib.cmi
+componentsConf.cmi:
+hExtlib.cmi:
+hMarshal.cmi:
+patternMatcher.cmi:
+hLog.cmi:
+trie.cmi:
+hTopoSort.cmi:
+refCounter.cmi:
+graphvizPp.cmi:
componentsConf.cmo: componentsConf.cmi
componentsConf.cmx: componentsConf.cmi
hExtlib.cmo: hExtlib.cmi
+http_getter_wget.cmi:
+http_getter_logger.cmi:
+http_getter_misc.cmi:
+http_getter_const.cmi:
http_getter_env.cmi: http_getter_types.cmo
+http_getter_storage.cmi:
http_getter_common.cmi: http_getter_types.cmo
http_getter.cmi: http_getter_types.cmo
+http_getter_types.cmo:
+http_getter_types.cmx:
http_getter_wget.cmo: http_getter_types.cmo http_getter_wget.cmi
http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi
http_getter_logger.cmo: http_getter_logger.cmi
+http_getter_wget.cmi:
+http_getter_logger.cmi:
+http_getter_misc.cmi:
+http_getter_const.cmi:
http_getter_env.cmi: http_getter_types.cmx
+http_getter_storage.cmi:
http_getter_common.cmi: http_getter_types.cmx
http_getter.cmi: http_getter_types.cmx
+http_getter_types.cmo:
+http_getter_types.cmx:
http_getter_wget.cmo: http_getter_types.cmx http_getter_wget.cmi
http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi
http_getter_logger.cmo: http_getter_logger.cmi
grafiteAstPp.cmi: grafiteAst.cmo
grafiteMarshal.cmi: grafiteAst.cmo
+grafiteAst.cmo:
+grafiteAst.cmx:
grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi
grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi
grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmo grafiteMarshal.cmi
grafiteAstPp.cmi: grafiteAst.cmx
grafiteMarshal.cmi: grafiteAst.cmx
+grafiteAst.cmo:
+grafiteAst.cmx:
grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi
grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi
grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmx grafiteMarshal.cmi
[ `Term of 'term
| `Auto of 'term auto_params ]
+type ntactic =
+ NApply of loc * CicNotationPt.term
+
type ('term, 'lazy_term, 'reduction, 'ident) tactic =
(* Higher order tactics (i.e. tacticals) *)
| Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactic
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 16
+let magic = 17
type ('term,'obj) command =
| Index of loc * 'term option (* key *) * UriManager.uri (* value *)
| Set of loc * string * string
| Print of loc * string
| Qed of loc
+ | NObj of loc * CicNotationPt.term CicNotationPt.obj
-type ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical =
+type punctuation_tactical =
| Dot of loc
| Semicolon of loc
| Branch of loc
| Wildcard of loc
| Merge of loc
-type ('term,'lazy_term,'reduction,'ident) non_punctuation_tactical =
+type non_punctuation_tactical =
| Focus of loc * int list
| Unfocus of loc
| Skip of loc
type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
| Command of loc * ('term, 'obj) command
| Macro of loc * ('term,'lazy_term) macro
+ | NTactic of loc * ntactic option * punctuation_tactical
| Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option
- * ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical
- | NonPunctuationTactical of loc
- * ('term, 'lazy_term, 'reduction, 'ident) non_punctuation_tactical
- * ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical
+ * punctuation_tactical
+ | NonPunctuationTactical of loc * non_punctuation_tactical
+ * punctuation_tactical
type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment =
| Note of loc * string
| `Auto params -> pp_auto_params ~term_pp params
;;
+let pp_ntactic ~map_unicode_to_tex = function
+ | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+;;
+
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
let pp_terms = pp_terms ~term_pp in
let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in
| None -> "")
| Print (_,s) -> "print " ^ s
| Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value
+ | NObj (_,o) -> "not supported"
-let pp_punctuation_tactical ~term_pp ~lazy_term_pp =
+let pp_punctuation_tactical =
function
| Dot _ -> "."
| Semicolon _ -> ";"
| Wildcard _ -> "*:"
| Merge _ -> "]"
-let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp =
+let pp_non_punctuation_tactical =
function
| Focus (_, goals) ->
Printf.sprintf "focus %s" (String.concat " " (List.map string_of_int goals))
function
| Macro (_, macro) -> pp_macro ~term_pp ~lazy_term_pp macro ^ "."
| Tactic (_, Some tac, punct) ->
- pp_tactic ~map_unicode_to_tex ~lazy_term_pp ~term_pp tac
- ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+ pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp tac
+ ^ pp_punctuation_tactical punct
| Tactic (_, None, punct) ->
- pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+ pp_punctuation_tactical punct
+ | NTactic (_,Some tac, punct) ->
+ pp_ntactic ~map_unicode_to_tex tac
+ ^ pp_punctuation_tactical punct
+ | NTactic (_,None, punct) ->
+ pp_punctuation_tactical punct
| NonPunctuationTactical (_, tac, punct) ->
- pp_non_punctuation_tactical ~lazy_term_pp ~term_pp tac
- ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+ pp_non_punctuation_tactical tac
+ ^ pp_punctuation_tactical punct
| Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
map_unicode_to_tex:bool ->
string
-val pp_punctuation_tactical:
- term_pp:('term -> string) ->
- lazy_term_pp:('lazy_term -> string) ->
- ('term, 'lazy_term, 'term GrafiteAst.reduction, string)
- GrafiteAst.punctuation_tactical ->
- string
+val pp_punctuation_tactical: GrafiteAst.punctuation_tactical -> string
+grafiteTypes.cmi:
grafiteSync.cmi: grafiteTypes.cmi
grafiteEngine.cmi: grafiteTypes.cmi
grafiteTypes.cmo: grafiteTypes.cmi
+grafiteTypes.cmi:
grafiteSync.cmi: grafiteTypes.cmi
grafiteEngine.cmi: grafiteTypes.cmi
grafiteTypes.cmo: grafiteTypes.cmi
status, [] (*CSC: TO BE FIXED *)
| GrafiteAst.Set (loc, name, value) -> status, []
(* GrafiteTypes.set_option status name value,[] *)
+ | GrafiteAst.NObj (loc,obj) ->
+ let ty, name =
+ match obj with
+ | CicNotationPt.Theorem (_,name,ty,_) -> ty, name
+ | _ -> assert false
+ in
+ let suri = "cic:/ng_matita/" ^ name ^ ".def" in
+ let nmenv, nsubst, nlexicon_status, nty =
+ GrafiteDisambiguate.disambiguate_nterm None
+ LexiconEngine.initial_status [] [] [] (text,prefix_len,ty)
+ in
+ let nmenv, nsubst, nlexicon_status, nbo =
+ GrafiteDisambiguate.disambiguate_nterm (Some nty)
+ LexiconEngine.initial_status [] nmenv nsubst ("",0,CicNotationPt.Implicit)
+ in
+ let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
+ prerr_endline ("nuovo lemma: " ^ NCicPp.ppmetasenv ~subst:nsubst nmenv);
+ { status with
+ GrafiteTypes.ng_status = Some { NTactics.gstatus = ninitial_stack;
+ istatus = {
+ NTactics.pstatus =
+ NUri.uri_of_string suri, 0, nmenv, nsubst,
+ (NCic.Constant ([],"",Some nbo,nty,(`Provided,`Definition,`Regular)));
+ lstatus = nlexicon_status} }
+ },
+ []
| GrafiteAst.Obj (loc,obj) ->
let ext,name =
match obj with
let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
{ status with GrafiteTypes.proof_status =
GrafiteTypes.Incomplete_proof
- { GrafiteTypes.proof = initial_proof; stack = initial_stack } },
+ { GrafiteTypes.proof = initial_proof; stack = initial_stack } ;
+ },
[]
| _ ->
if metasenv <> [] then
| GrafiteAst.Tactic (_, None, punct) ->
eval_tactical status
(punctuation_tactical_of_ast (text,prefix_len,punct)),[]
+ | GrafiteAst.NTactic (_(*loc*), Some (GrafiteAst.NApply (_loc, t)), punct) ->
+ (match status.GrafiteTypes.ng_status with
+ | None -> assert false
+ | Some status ->
+ let nts = NTactics.apply_tac (text,prefix_len,t) status in
+ prerr_endline "esco da apply";
+ NTactics.pp_tac_status nts;
+ (*
+ let tac = apply_tactic ~disambiguate_tactic (text,prefix_len,tac) in
+ let status = eval_tactical status (tactic_of_ast' tac) in
+ eval_tactical status
+ (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
+ *) assert false)
+ | GrafiteAst.NTactic (_, None, _punct) -> assert false (*
+ eval_tactical status
+ (punctuation_tactical_of_ast (text,prefix_len,punct)),[] *)
| GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
let status =
eval_tactical status
coercions = CoercDb.empty_coerc_db;
universe = Universe.empty;
baseuri = baseuri;
+ ng_status = None;
}
coercions: CoercDb.coerc_db;
universe:Universe.universe;
baseuri: string;
+ ng_status: NTactics.tac_status option;
}
let get_current_proof status =
coercions: CoercDb.coerc_db;
universe:Universe.universe; (** universe of terms used by auto *)
baseuri: string;
+ ng_status: NTactics.tac_status option;
}
val dump_status : status -> unit
+dependenciesParser.cmi:
+grafiteParser.cmi:
+cicNotation2.cmi:
+grafiteDisambiguate.cmi:
grafiteWalker.cmi: grafiteParser.cmi
+print_grammar.cmi:
dependenciesParser.cmo: dependenciesParser.cmi
dependenciesParser.cmx: dependenciesParser.cmi
grafiteParser.cmo: grafiteParser.cmi
+dependenciesParser.cmi:
+grafiteParser.cmi:
+cicNotation2.cmi:
+grafiteDisambiguate.cmi:
grafiteWalker.cmi: grafiteParser.cmi
+print_grammar.cmi:
dependenciesParser.cmo: dependenciesParser.cmi
dependenciesParser.cmx: dependenciesParser.cmi
grafiteParser.cmo: grafiteParser.cmi
;;
(** @param term not meaningful when context is given *)
-let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv
+let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv
term =
let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, subst, cic, _) =
singleton "first"
(CicDisambiguate.disambiguate_term
~aliases:lexicon_status.LexiconEngine.aliases
- ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~expty ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
~lookup_in_library
~mk_choice:cic_mk_choice
~mk_implicit
metasenv,(*subst,*) cic
;;
+let disambiguate_nterm expty lexicon_status context metasenv subst thing
+=
+ let diff, metasenv, subst, cic =
+ singleton "first"
+ (NCicDisambiguate.disambiguate_term
+ ~coercion_db:(NCicCoercion.db ())
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~expty
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~lookup_in_library
+ ~mk_choice:ncic_mk_choice
+ ~mk_implicit
+ ~description_of_alias:LexiconAst.description_of_alias
+ ~context ~metasenv ~subst thing)
+ in
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ metasenv, subst, lexicon_status, cic
+;;
+
+
(** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
* rationale: lazy_term will be invoked in different context to obtain a term,
* each invocation will disambiguate the term and can add aliases. Once all
* disambiguations have been performed, the first returned function can be
* used to obtain the resulting aliases *)
-let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term =
+let disambiguate_lazy_term expty text prefix_len lexicon_status_ref term =
(fun context metasenv ugraph ->
let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, _, cic, ugraph) =
~description_of_alias:LexiconAst.description_of_alias
~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
- ~context ~metasenv ~subst:[] ?goal
- (text,prefix_len,term)) in
+ ~context ~metasenv ~subst:[]
+ (text,prefix_len,term) ~expty) in
let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
lexicon_status_ref := lexicon_status;
cic, metasenv, ugraph)
lexicon_status_ref context metasenv goal (text,prefix_len,tactic)
=
let disambiguate_term_hint =
- disambiguate_term goal text prefix_len lexicon_status_ref in
+ let _,_,expty =
+ List.find (fun (x,_,_) -> Some x = goal) metasenv
+ in
+ disambiguate_term (Some expty) text prefix_len lexicon_status_ref in
let disambiguate_term =
disambiguate_term None text prefix_len lexicon_status_ref in
let disambiguate_pattern =
in
UriManager.uri_of_string (baseuri ^ "/" ^ name)
in
- let try_new cic =
+ let _try_new cic =
(NCicLibrary.clear_cache ();
NCicEnvironment.invalidate ();
OCic2NCic.clear ();
let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
match cmd with
+ | GrafiteAst.NObj(loc,obj) -> lexicon_status, metasenv, GrafiteAst.NObj(loc,obj)
| GrafiteAst.Index(loc,key,uri) ->
let lexicon_status_ref = ref lexicon_status in
let disambiguate_term =
Cic.context ->
((CicNotationPt.term,CicNotationPt.term) GrafiteAst.macro) Disambiguate.disambiguator_input ->
Cic.metasenv * (Cic.term,Cic.lazy_term) GrafiteAst.macro
+
+val disambiguate_nterm :
+ NCic.term option -> LexiconEngine.status ->
+ NCic.context -> NCic.metasenv -> NCic.substitution ->
+ CicNotationPt.term Disambiguate.disambiguator_input ->
+ NCic.metasenv * NCic.substitution * LexiconEngine.status * NCic.term
]
];
using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
+ ntactic: [
+ [ IDENT "napply"; t = tactic_term ->
+ GrafiteAst.NApply (loc, t)
+ ]
+ ];
tactic: [
[ IDENT "absurd"; t = tactic_term ->
GrafiteAst.Absurd (loc, t)
| IDENT "skip" -> GrafiteAst.Skip loc
]
];
+ ntheorem_flavour: [
+ [ [ IDENT "ntheorem" ] -> `Theorem
+ ]
+ ];
theorem_flavour: [
[ [ IDENT "definition" ] -> `Definition
| [ IDENT "fact" ] -> `Fact
GrafiteAst.Obj (loc,
Ast.Theorem
(`Variant,name,typ,Some (Ast.Ident (newname, None))))
+ | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
| flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
| tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
GrafiteAst.Tactic (loc, Some tac, punct)
| punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
+ | tac = ntactic; punct = punctuation_tactical ->
+ GrafiteAst.NTactic (loc, Some tac, punct)
| tac = non_punctuation_tactical; punct = punctuation_tactical ->
GrafiteAst.NonPunctuationTactical (loc, tac, punct)
| mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
+domMisc.cmi:
+xml2Gdome.cmi:
domMisc.cmo: domMisc.cmi
domMisc.cmx: domMisc.cmi
xml2Gdome.cmo: xml2Gdome.cmi
+domMisc.cmi:
+xml2Gdome.cmi:
domMisc.cmo: domMisc.cmi
domMisc.cmx: domMisc.cmi
xml2Gdome.cmo: xml2Gdome.cmi
+hSql.cmi:
+hSqlite3.cmo:
+hSqlite3.cmx:
+hMysql.cmo:
+hMysql.cmx:
hSql.cmo: hSqlite3.cmo hMysql.cmo hSql.cmi
hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi
+hSql.cmi:
+hSqlite3.cmo:
+hSqlite3.cmx:
+hMysql.cmo:
+hMysql.cmx:
hSql.cmo: hSqlite3.cmx hMysql.cmx hSql.cmi
hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi
cicNotation.cmi: lexiconAst.cmo
lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmo cicNotation.cmi
lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmo
+lexiconAst.cmo:
+lexiconAst.cmx:
lexiconAstPp.cmo: lexiconAst.cmo lexiconAstPp.cmi
lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi
lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmo lexiconMarshal.cmi
cicNotation.cmi: lexiconAst.cmx
lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi
lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmx
+lexiconAst.cmo:
+lexiconAst.cmx:
lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi
lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi
lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx lexiconMarshal.cmi
+librarian.cmi:
+libraryMisc.cmi:
+libraryDb.cmi:
+coercDb.cmi:
cicCoercion.cmi: coercDb.cmi
+librarySync.cmi:
+cicElim.cmi:
+cicRecord.cmi:
+cicFix.cmi:
+libraryClean.cmi:
librarian.cmo: librarian.cmi
librarian.cmx: librarian.cmi
libraryMisc.cmo: libraryMisc.cmi
+librarian.cmi:
+libraryMisc.cmi:
+libraryDb.cmi:
+coercDb.cmi:
cicCoercion.cmi: coercDb.cmi
+librarySync.cmi:
+cicElim.cmi:
+cicRecord.cmi:
+cicFix.cmi:
+libraryClean.cmi:
librarian.cmo: librarian.cmi
librarian.cmx: librarian.cmi
libraryMisc.cmo: libraryMisc.cmi
+helmLogger.cmi:
helmLogger.cmo: helmLogger.cmi
helmLogger.cmx: helmLogger.cmi
+helmLogger.cmi:
helmLogger.cmo: helmLogger.cmi
helmLogger.cmx: helmLogger.cmi
+sqlStatements.cmi:
+metadataTypes.cmi:
metadataExtractor.cmi: metadataTypes.cmi
metadataPp.cmi: metadataTypes.cmi
metadataConstraints.cmi: metadataTypes.cmi
+sqlStatements.cmi:
+metadataTypes.cmi:
metadataExtractor.cmi: metadataTypes.cmi
metadataPp.cmi: metadataTypes.cmi
metadataConstraints.cmi: metadataTypes.cmi
+nCicDisambiguate.cmi:
nCicDisambiguate.cmo: nCicDisambiguate.cmi
nCicDisambiguate.cmx: nCicDisambiguate.cmi
+nCicDisambiguate.cmi:
nCicDisambiguate.cmo: nCicDisambiguate.cmi
nCicDisambiguate.cmx: nCicDisambiguate.cmi
;;
let refine_term
- metasenv subst context uri ~coercion_db ~use_coercions term _ ~localization_tbl=
+ metasenv subst context uri ~coercion_db ~use_coercions term expty _ ~localization_tbl=
assert (uri=None);
debug_print (lazy (sprintf "TEST_INTERPRETATION: %s"
(NCicPp.ppterm ~metasenv ~subst ~context term)));
if use_coercions then
NCicCoercion.look_for_coercion coercion_db
else (fun _ _ _ _ _ -> []))
- metasenv subst context term None ~localise
+ metasenv subst context term expty ~localise
in
Disambiguate.Ok (term, metasenv, subst, ())
with
let refine_obj
~coercion_db metasenv subst context uri
- ~use_coercions obj ugraph ~localization_tbl
+ ~use_coercions obj _ ugraph ~localization_tbl
=
assert (metasenv=[]);
assert (subst=[]);
*)
;;
-let disambiguate_term ~context ~metasenv ~subst ?goal
+let disambiguate_term ~context ~metasenv ~subst ~expty
~mk_implicit ~description_of_alias ~mk_choice
~aliases ~universe ~coercion_db ~lookup_in_library
(text,prefix_len,term)
=
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
- let hint =
- match goal with
- None -> (fun _ y -> y),(fun x -> x)
- | Some n ->
- (fun metasenv y ->
- let _,_,ty = NCicUtils.lookup_meta n metasenv in
- NCic.LetIn ("_",ty,y,NCic.Rel 1)),
- (function
- | Disambiguate.Ok (t,m,s,ug) ->
- (match t with
- | NCic.LetIn ("_",_,y,NCic.Rel 1) -> Disambiguate.Ok (y,m,s,ug)
- | _ -> assert false)
- | k -> k)
- in
let res,b =
MultiPassDisambiguator.disambiguate_thing
~freshen_thing:CicNotationUtil.freshen_term
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
~interpretate_thing:(interpretate_term ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
~refine_thing:(refine_term ~coercion_db) (text,prefix_len,term)
- ~mk_localization_tbl ~hint ~subst
+ ~mk_localization_tbl ~expty ~subst
in
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;
(text,prefix_len,obj)
=
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
- let hint = (fun x y -> y), (fun x -> x) in
let res,b =
MultiPassDisambiguator.disambiguate_thing
~freshen_thing:CicNotationUtil.freshen_obj
~interpretate_thing:(interpretate_obj ~mk_choice)
~refine_thing:(refine_obj ~coercion_db)
(text,prefix_len,obj)
- ~mk_localization_tbl ~hint
+ ~mk_localization_tbl ~expty:None
in
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;
context:NCic.context ->
metasenv:NCic.metasenv ->
subst:NCic.substitution ->
- ?goal:int ->
+ expty:NCic.term option ->
mk_implicit: (bool -> 'alias) ->
description_of_alias:('alias -> string) ->
mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
+nUri.cmi:
nReference.cmi: nUri.cmi
nCicUtils.cmi: nCic.cmo
nCicSubstitution.cmi: nCic.cmo
+nUri.cmi:
nReference.cmi: nUri.cmi
nCicUtils.cmi: nCic.cmx
nCicSubstitution.cmi: nCic.cmx
ppterm ~context ~subst ~metasenv ?inside_fix t
;;
-
-let ppobj = function
- | (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) ->
- "{"^NUri.string_of_uri u^"}\n"^
- (if b then "let rec " else "let corec ") ^
- String.concat "\nand "
- (List.map (fun (_,name,n,ty,bo) ->
- name^ " on " ^ string_of_int n ^ " : " ^
- ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^
- ppterm ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl)
- | (u,_,metasenv,subst,NCic.Inductive (b, leftno,tyl, _)) ->
- "{"^NUri.string_of_uri u^"} with "^string_of_int leftno^" fixed params\n"^
- (if b then "inductive " else "coinductive ")^
- String.concat "\nand "
- (List.map (fun (_,name,ty,cl) ->
- name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^
- String.concat "\n"
- (List.map (fun (_,name,ty) ->
- " | "^name^": "^ppterm ~metasenv ~subst ~context:[] ty)
- cl)) tyl) ^ "."
- | (u,_,metasenv,subst,NCic.Constant (_,name,None,ty, _)) ->
- "{"^NUri.string_of_uri u^"}\n"^
- "axiom " ^ name ^ " : " ^
- ppterm ~metasenv ~subst ~context:[] ty ^ "\n"
- | (u,_,metasenv,subst,NCic.Constant (_,name,Some bo,ty, _)) ->
- "{"^NUri.string_of_uri u^"}\n"^
- "definition " ^ name ^ " : " ^
- ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^
- ppterm ~metasenv ~subst ~context:[] bo ^ "\n"
-;;
-
let rec ppcontext ?(sep="\n") ~subst ~metasenv = function
| [] -> ""
| (name, NCic.Decl t) :: tl ->
let ppsubst ~metasenv subst = ppsubst ~metasenv ~subst subst;;
+
+let ppobj (u,_,metasenv, subst, o) =
+ "metasenv:\n" ^ ppmetasenv ~subst metasenv ^ "\n" ^
+ match o with
+ | NCic.Fixpoint (b, fl, _) ->
+ "{"^NUri.string_of_uri u^"}\n"^
+ (if b then "let rec " else "let corec ") ^
+ String.concat "\nand "
+ (List.map (fun (_,name,n,ty,bo) ->
+ name^ " on " ^ string_of_int n ^ " : " ^
+ ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^
+ ppterm ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl)
+ | NCic.Inductive (b, leftno,tyl, _) ->
+ "{"^NUri.string_of_uri u^"} with "^string_of_int leftno^" fixed params\n"^
+ (if b then "inductive " else "coinductive ")^
+ String.concat "\nand "
+ (List.map (fun (_,name,ty,cl) ->
+ name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^
+ String.concat "\n"
+ (List.map (fun (_,name,ty) ->
+ " | "^name^": "^ppterm ~metasenv ~subst ~context:[] ty)
+ cl)) tyl) ^ "."
+ | NCic.Constant (_,name,None,ty, _) ->
+ "{"^NUri.string_of_uri u^"}\n"^
+ "axiom " ^ name ^ " : " ^
+ ppterm ~metasenv ~subst ~context:[] ty ^ "\n"
+ | NCic.Constant (_,name,Some bo,ty, _) ->
+ "{"^NUri.string_of_uri u^"}\n"^
+ "definition " ^ name ^ " : " ^
+ ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^
+ ppterm ~metasenv ~subst ~context:[] bo ^ "\n"
+;;
+
let _ = NCicSubstitution.set_ppterm (ppterm ~margin:80);;
+nDiscriminationTree.cmi:
+nCicMetaSubst.cmi:
+nCicCoercion.cmi:
+nCicUnifHint.cmi:
nCicUnification.cmi: nCicUnifHint.cmi
nCicRefiner.cmi: nCicUnifHint.cmi
nDiscriminationTree.cmo: nDiscriminationTree.cmi
+nDiscriminationTree.cmi:
+nCicMetaSubst.cmi:
+nCicCoercion.cmi:
+nCicUnifHint.cmi:
nCicUnification.cmi: nCicUnifHint.cmi
nCicRefiner.cmi: nCicUnifHint.cmi
nDiscriminationTree.cmo: nDiscriminationTree.cmi
let _,_,_,ty = NCicUtils.lookup_subst n subst in ty
with NCicUtils.Subst_not_found _ -> try
let _,_,ty = NCicUtils.lookup_meta n metasenv in
- match ty with C.Implicit _ -> assert false | _ -> ty
+ match ty with C.Implicit _ ->
+ prerr_endline (string_of_int n);
+ prerr_endline (NCicPp.ppmetasenv ~subst metasenv);
+ prerr_endline (NCicPp.ppsubst ~metasenv subst);
+ assert false | _ -> ty
with NCicUtils.Meta_not_found _ ->
raise (AssertFailure (lazy (Printf.sprintf
"%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t))))
--- /dev/null
+nTactics.cmi:
+nTactics.cmo: nTactics.cmi
+nTactics.cmx: nTactics.cmi
--- /dev/null
+nTactics.cmi:
+nTactics.cmo: nTactics.cmi
+nTactics.cmx: nTactics.cmi
--- /dev/null
+PACKAGE = ng_tactics
+
+INTERFACE_FILES = \
+ nTactics.mli
+
+IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
+
+
+all:
+
+
+include ../../Makefile.defs
+include ../Makefile.common
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+open Printf
+
+let debug = true
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
+exception Error of string lazy_t
+let fail msg = raise (Error msg)
+
+type lowtac_status = {
+ pstatus : NCic.obj;
+ lstatus : LexiconEngine.status
+}
+
+type lowtactic = lowtac_status * int -> lowtac_status * int list * int list
+
+type tac_status = {
+ gstatus : Continuationals.Stack.t;
+ istatus : lowtac_status;
+}
+
+type tactic = tac_status -> tac_status
+
+type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
+
+let pp_tac_status status =
+ prerr_endline (NCicPp.ppobj status.istatus.pstatus)
+;;
+
+open Continuationals.Stack
+
+let dot_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | ([], _, [], _) :: _ as stack ->
+ (* backward compatibility: do-nothing-dot *)
+ stack
+ | (g, t, k, tag) :: s ->
+ match filter_open g, k with
+ | loc :: loc_tl, _ ->
+ (([ loc ], t, loc_tl @+ k, tag) :: s)
+ | [], loc :: k ->
+ assert (is_open loc);
+ (([ loc ], t, k, tag) :: s)
+ | _ -> fail (lazy "can't use \".\" here")
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let branch_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | (g, t, k, tag) :: s ->
+ match init_pos g with (* TODO *)
+ | [] | [ _ ] -> fail (lazy "too few goals to branch");
+ | loc :: loc_tl ->
+ ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let shift_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
+ (match g' with
+ | [] -> fail (lazy "no more goals to shift")
+ | loc :: loc_tl ->
+ (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
+ :: (loc_tl, t', k', tag) :: s))
+ | _ -> fail (lazy "can't shift goals here")
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let pos_tac i_s status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
+ when is_fresh loc ->
+ let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
+ ((l_js, t , [],`BranchTag)
+ :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
+ | _ -> fail (lazy "can't use relative positioning here")
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let wildcard_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
+ when is_fresh loc ->
+ (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
+ | _ -> fail (lazy "can't use wildcard here")
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let merge_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
+ ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
+ | _ -> fail (lazy "can't merge goals here")
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let focus_tac gs status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | s -> assert(gs <> []);
+ let stack_locs =
+ let add_l acc _ _ l = if is_open l then l :: acc else acc in
+ fold ~env:add_l ~cont:add_l ~todo:add_l [] s
+ in
+ List.iter
+ (fun g ->
+ if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
+ fail (lazy (sprintf "goal %d not found (or closed)" g)))
+ gs;
+ (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let unfocus_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | ([], [], [], `FocusTag) :: s -> s
+ | _ -> fail (lazy "can't unfocus, some goals are still open")
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let skip_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | (gl, t, k, tag) :: s ->
+ let gl = List.map switch_of_loc gl in
+ if List.exists (function Open _ -> true | Closed _ -> false) gl then
+ fail (lazy "cannot skip an open goal")
+ else
+ ([],t,k,tag) :: s
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let fold_tactic tac status =
+ match status.gstatus with
+ | [] -> assert false
+ | (g, t, k, tag) :: s ->
+ debug_print (lazy ("context length " ^string_of_int (List.length g)));
+ let rec aux s go gc =
+ function
+ | [] -> s, go, gc
+ | loc :: loc_tl ->
+ debug_print (lazy "inner eval tactical");
+ let s, go, gc =
+ if List.exists ((=) (goal_of_loc loc)) gc then
+ s, go, gc
+ else
+ match switch_of_loc loc with
+ | Closed _ -> fail (lazy "cannot apply to a Closed goal")
+ | Open n ->
+ let s, go', gc' = tac (s,n) in
+ s, (go @- gc') @+ go', gc @+ gc'
+ in
+ aux s go gc loc_tl
+ in
+ let s0, go0, gc0 = status.istatus, [], [] in
+ let sn, gon, gcn = aux s0 go0 gc0 g in
+ debug_print (lazy ("opened: "
+ ^ String.concat " " (List.map string_of_int gon)));
+ debug_print (lazy ("closed: "
+ ^ String.concat " " (List.map string_of_int gcn)));
+ let stack =
+ (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
+ in
+ { gstatus = stack; istatus = sn }
+;;
+
+
+let apply t (status,goal) =
+ let _,_,metasenv, subst,_ = status.pstatus in
+ let _,context,gty = List.assoc goal metasenv in
+ let metasenv, subst, lexicon_status, t =
+ GrafiteDisambiguate.disambiguate_nterm (Some gty) status.lstatus context metasenv subst t
+ in
+ prerr_endline ("termine disambiguato: " ^ NCicPp.ppterm ~context ~metasenv ~subst t);
+ prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv);
+ prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv);
+ prerr_endline "fine napply";
+ { status with lstatus = lexicon_status }, [goal], []
+;;
+
+let apply_tac t = fold_tactic (apply t) ;;
+
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+
+type lowtac_status = {
+ pstatus : NCic.obj;
+ lstatus : LexiconEngine.status
+}
+
+type lowtactic = lowtac_status * int -> lowtac_status * int list * int list
+
+type tac_status = {
+ gstatus : Continuationals.Stack.t;
+ istatus : lowtac_status;
+}
+
+type tactic = tac_status -> tac_status
+
+type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
+
+val dot_tac: tactic
+val branch_tac: tactic
+val shift_tac: tactic
+val pos_tac: int list -> tactic
+val wildcard_tac: tactic
+val merge_tac: tactic
+val focus_tac: int list -> tactic
+val unfocus_tac: tactic
+val skip_tac: tactic
+
+val fold_tactic: lowtactic -> tactic
+
+val apply_tac: tactic_term -> tactic
+
+
+val pp_tac_status: tac_status -> unit
+helm_registry.cmi:
helm_registry.cmo: helm_registry.cmi
helm_registry.cmx: helm_registry.cmi
+helm_registry.cmi:
helm_registry.cmo: helm_registry.cmi
helm_registry.cmx: helm_registry.cmi
+utf8Macro.cmi:
+utf8MacroTable.cmo:
+utf8MacroTable.cmx:
utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
+utf8Macro.cmi:
+utf8MacroTable.cmo:
+utf8MacroTable.cmx:
utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
+proofEngineTypes.cmi:
proofEngineHelpers.cmi: proofEngineTypes.cmi
+proofEngineReduction.cmi:
continuationals.cmi: proofEngineTypes.cmi
tacticals.cmi: proofEngineTypes.cmi
reductionTactics.cmi: proofEngineTypes.cmi
proofEngineStructuralRules.cmi: proofEngineTypes.cmi
primitiveTactics.cmi: proofEngineTypes.cmi
+hashtbl_equiv.cmi:
metadataQuery.cmi: proofEngineTypes.cmi
+universe.cmi:
autoTypes.cmi: proofEngineTypes.cmi
+autoCache.cmi:
+paramodulation/utils.cmi:
+closeCoercionGraph.cmi:
+paramodulation/subst.cmi:
paramodulation/equality.cmi: paramodulation/utils.cmi \
paramodulation/subst.cmi
paramodulation/founif.cmi: paramodulation/subst.cmi
auto.cmi: universe.cmi proofEngineTypes.cmi
destructTactic.cmi: proofEngineTypes.cmi
inversion.cmi: proofEngineTypes.cmi
+inversion_principle.cmi:
ring.cmi: proofEngineTypes.cmi
setoids.cmi: proofEngineTypes.cmi
+fourier.cmi:
fourierR.cmi: proofEngineTypes.cmi
fwdSimplTactic.cmi: proofEngineTypes.cmi
+history.cmi:
statefulProofEngine.cmi: proofEngineTypes.cmi
tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi
declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi
+proofEngineTypes.cmi:
proofEngineHelpers.cmi: proofEngineTypes.cmi
+proofEngineReduction.cmi:
continuationals.cmi: proofEngineTypes.cmi
tacticals.cmi: proofEngineTypes.cmi
reductionTactics.cmi: proofEngineTypes.cmi
proofEngineStructuralRules.cmi: proofEngineTypes.cmi
primitiveTactics.cmi: proofEngineTypes.cmi
+hashtbl_equiv.cmi:
metadataQuery.cmi: proofEngineTypes.cmi
+universe.cmi:
autoTypes.cmi: proofEngineTypes.cmi
+autoCache.cmi:
+paramodulation/utils.cmi:
+closeCoercionGraph.cmi:
+paramodulation/subst.cmi:
paramodulation/equality.cmi: paramodulation/utils.cmi \
paramodulation/subst.cmi
paramodulation/founif.cmi: paramodulation/subst.cmi
auto.cmi: universe.cmi proofEngineTypes.cmi
destructTactic.cmi: proofEngineTypes.cmi
inversion.cmi: proofEngineTypes.cmi
+inversion_principle.cmi:
ring.cmi: proofEngineTypes.cmi
setoids.cmi: proofEngineTypes.cmi
+fourier.cmi:
fourierR.cmi: proofEngineTypes.cmi
fwdSimplTactic.cmi: proofEngineTypes.cmi
+history.cmi:
statefulProofEngine.cmi: proofEngineTypes.cmi
tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi
declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi
let of_metasenv metasenv =
let goals = List.map (fun (g, _, _) -> g) metasenv in
[ zero_pos goals, [], [], `NoTag ]
+
+ let of_nmetasenv metasenv =
+ let goals = List.map (fun (g, _) -> g) metasenv in
+ [ zero_pos goals, [], [], `NoTag ]
let head_switches =
function
val find_goal: t -> goal (** find "next" goal *)
val is_empty: t -> bool (** a singleton empty level *)
val of_metasenv: Cic.metasenv -> t
+ val of_nmetasenv: (goal * 'a) list -> t
val head_switches: t -> switch list (** top level switches *)
val head_goals: t -> goal list (** top level goals *)
val head_tag: t -> tag (** top level tag *)
val shift_goals: t -> goal list (** second level goals *)
val open_goals: t -> goal list (** all (Open) goals *)
val goal_of_switch: switch -> goal
+ val filter_open : (goal * switch) list -> (goal * switch) list
+ val is_open: goal * switch -> bool
+ val is_fresh: goal * switch -> bool
+ val init_pos: (goal * switch) list -> (goal * switch) list
+ val goal_of_loc: goal * switch -> goal
+ val switch_of_loc: goal * switch -> switch
+ val zero_pos : goal list -> (goal * switch) list
+ val deep_close: goal list -> t -> t
+
+
+ val ( @+ ) : 'a list -> 'a list -> 'a list
+ val ( @- ) : 'a list -> 'a list -> 'a list
+ val ( @~- ) : ('a * switch) list -> goal list -> ('a * switch) list
+
+
(** @param int depth, depth 0 is the top of the stack *)
val fold:
+threadSafe.cmi:
+extThread.cmi:
threadSafe.cmo: threadSafe.cmi
threadSafe.cmx: threadSafe.cmi
extThread.cmo: extThread.cmi
+threadSafe.cmi:
+extThread.cmi:
threadSafe.cmo: threadSafe.cmi
threadSafe.cmx: threadSafe.cmi
extThread.cmo: extThread.cmi
parser.cmi: ast.cmo
+tptp2grafite.cmi:
+ast.cmo:
+ast.cmx:
lexer.cmo: parser.cmi
lexer.cmx: parser.cmx
parser.cmo: ast.cmo parser.cmi
parser.cmi: ast.cmx
+tptp2grafite.cmi:
+ast.cmo:
+ast.cmx:
lexer.cmo: parser.cmi
lexer.cmx: parser.cmx
parser.cmo: ast.cmx parser.cmi
+uriManager.cmi:
uriManager.cmo: uriManager.cmi
uriManager.cmx: uriManager.cmi
+uriManager.cmi:
uriManager.cmo: uriManager.cmi
uriManager.cmx: uriManager.cmi
+whelp.cmi:
+fwdQueries.cmi:
whelp.cmo: whelp.cmi
whelp.cmx: whelp.cmi
fwdQueries.cmo: fwdQueries.cmi
+whelp.cmi:
+fwdQueries.cmi:
whelp.cmo: whelp.cmi
whelp.cmx: whelp.cmi
fwdQueries.cmo: fwdQueries.cmi
+xml.cmi:
+xmlPushParser.cmi:
xml.cmo: xml.cmi
xml.cmx: xml.cmi
xmlPushParser.cmo: xmlPushParser.cmi
+xml.cmi:
+xmlPushParser.cmi:
xml.cmo: xml.cmi
xml.cmx: xml.cmi
xmlPushParser.cmo: xmlPushParser.cmi
+xmlDiff.cmi:
xmlDiff.cmo: xmlDiff.cmi
xmlDiff.cmx: xmlDiff.cmi
+xmlDiff.cmi:
xmlDiff.cmo: xmlDiff.cmi
xmlDiff.cmx: xmlDiff.cmi
projects / helm.git / commitdiff