ng_tactics \
grafite_engine \
tptp_grafite \
+ ng_kernel \
+ ng_refiner \
$(NULL)
METAS = $(MODULES:%=METAS/META.helm-%)
-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
(* literal, substitutions.
* Some [] -> user has given an empty explicit substitution list
* None -> user has given no explicit substitution list *)
- | Implicit of [`Vector | `JustOne]
+ | Implicit of [`Vector | `JustOne | `Tagged of string]
| Meta of int * meta_subst list
| Num of string * int (* literal, instance *)
| Sort of sort_kind
-proceduralHelpers.cmi:
-proceduralClassify.cmi:
-proceduralOptimizer.cmi:
-proceduralTypes.cmi:
-proceduralMode.cmi:
-proceduralConversion.cmi:
procedural1.cmi: proceduralTypes.cmi
procedural2.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:
dist:
mkdir -p $(DIST)/Sources
+ cp ReadMe $(DIST)
cp *.ml *.mli *.mll *.mly Makefile _tags $(DIST)/Sources
cd $(DIST); ln -s Sources/matitaprover.native matitaprover
tar -cvzf $(DIST).tgz $(DIST)
-table_creator.cmo:
-table_creator.cmx:
gallina8Parser.cmi: types.cmo
grafiteParser.cmi: types.cmo
grafite.cmi: types.cmo
-engine.cmi:
-types.cmo:
-types.cmx:
-options.cmo:
-options.cmx:
gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmo gallina8Parser.cmi
gallina8Parser.cmi: types.cmx
grafiteParser.cmi: types.cmx
grafite.cmi: types.cmx
-engine.cmi:
-types.cmo:
-types.cmx:
-options.cmo:
-options.cmx:
gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmx gallina8Parser.cmi
-cicUniv.cmi:
unshare.cmi: cic.cmo
deannotate.cmi: cic.cmo
cicParser.cmi: cic.cmo
cicUtil.cmi: cic.cmo
helmLibraryObjects.cmi: cic.cmo
-libraryObjects.cmi:
cic_indexable.cmi: cic.cmo
path_indexing.cmi: cic.cmo
cicInspect.cmi: cic.cmo
-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
CicEnvironment.CircularDependency _ ->
raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
| CicNotationPt.Implicit `Vector -> assert false
- | CicNotationPt.Implicit `JustOne -> Cic.Implicit None
+ | CicNotationPt.Implicit (`JustOne | `Tagged _) -> Cic.Implicit None
| CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
| CicNotationPt.Num (num, i) ->
Disambiguate.resolve ~mk_choice ~env
-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
-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
make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args
in
[B.H([],
- (if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::
+ (*(if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::*)
+ (B.b_kw "by")::
B.b_space::
B.Text([],"(")::pres_args@[B.Text([],")")])], None
else
-disambiguateTypes.cmi:
disambiguate.cmi: disambiguateTypes.cmi
multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi
disambiguateTypes.cmo: disambiguateTypes.cmi
-componentsConf.cmi:
-hExtlib.cmi:
-hMarshal.cmi:
-patternMatcher.cmi:
-hLog.cmi:
-trie.cmi:
-discrimination_tree.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
true
with
Http_user_agent.Http_error _ -> false
- | Not_found -> prerr_endline "An object has metadata but no XML. This is an internal bug of ocaml-http: Zack, please fix it!"; assert false
+ | Not_found -> prerr_endline (Printf.sprintf "An object %s has metadata but no XML. This is an internal bug of ocaml-http: Zack, please fix it!"
+ url); assert false
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
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 28
+let magic = 30
type ('term,'obj) command =
| Index of loc * 'term option (* key *) * UriManager.uri (* value *)
type ncommand =
| UnificationHint of loc * CicNotationPt.term * int (* term, precedence *)
| NObj of loc * CicNotationPt.term CicNotationPt.obj
+ | NInverter of loc * string * CicNotationPt.term
| NUnivConstraint of loc * NUri.uri * NUri.uri
| NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
| NCoercion of loc * string *
let pp_ncommand = function
| UnificationHint (_,t, n) ->
"unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+ | NInverter (_,_,_)
| NObj (_,_)
| NUnivConstraint (_) -> "not supported"
| NCoercion (_) -> "not supported"
-grafiteTypes.cmi:
grafiteSync.cmi: grafiteTypes.cmi
nCicCoercDeclaration.cmi: grafiteTypes.cmi
grafiteEngine.cmi: grafiteTypes.cmi
[] ->
eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
| _ -> status,`New [])
+ | GrafiteAst.NInverter (loc, name, indty) ->
+ if status#ng_mode <> `CommandMode then
+ raise (GrafiteTypes.Command_error "Not in command mode")
+ else
+ let status = status#set_ng_mode `ProofMode in
+ let metasenv,subst,status,indty =
+ GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in
+ let _,leftno,tys,_,_ = match indty with
+ NCic.Const r -> NCicEnvironment.get_checked_indtys r
+ | _ -> assert false in
+ let it = match tys with
+ hd::tl -> hd
+ | _ -> assert false
+ in
+ let status,obj =
+ NInversion.mk_inverter name it leftno status status#baseuri in
+ let _,_,menv,_,_ = obj in
+ (match menv with
+ [] ->
+ eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ | _ -> assert false)
| GrafiteAst.NUnivConstraint (loc,u1,u2) ->
eval_add_constraint status [`Type,u1] [`Type,u2]
;;
exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
type 'a disambiguator_input = string * int * 'a
-
+
val eval_ast :
disambiguate_tactic:
(GrafiteTypes.status ->
disambiguator_input ->
(* the new status and generated objects, if any *)
GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
-
-dependenciesParser.cmi:
-grafiteParser.cmi:
-cicNotation2.cmi:
-nEstatus.cmi:
grafiteDisambiguate.cmi: nEstatus.cmi
-print_grammar.cmi:
dependenciesParser.cmo: dependenciesParser.cmi
dependenciesParser.cmx: dependenciesParser.cmi
grafiteParser.cmo: grafiteParser.cmi
G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body))
| IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
+ | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = term ->
+ G.NInverter (loc,name,indty)
| NLETCOREC ; defs = let_defs ->
nmk_rec_corec `CoInductive defs loc
| NLETREC ; defs = let_defs ->
-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
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
-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
-sqlStatements.cmi:
-metadataTypes.cmi:
metadataExtractor.cmi: metadataTypes.cmi
metadataPp.cmi: metadataTypes.cmi
metadataConstraints.cmi: metadataTypes.cmi
-ncic2astMatcher.cmi:
-nTermCicContent.cmi:
ncic2astMatcher.cmo: ncic2astMatcher.cmi
ncic2astMatcher.cmx: ncic2astMatcher.cmi
nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi
-nCicDisambiguate.cmi:
nCicDisambiguate.cmo: nCicDisambiguate.cmi
nCicDisambiguate.cmx: nCicDisambiguate.cmi
| CicNotationPt.NRef nref -> NCic.Const nref
| CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
| CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
+ | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
| CicNotationPt.UserInput -> NCic.Implicit `Hole
| CicNotationPt.Num (num, i) ->
Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
-nUri.cmi:
nReference.cmi: nUri.cmi
nCicUtils.cmi: nCic.cmo
nCicSubstitution.cmi: nCic.cmo
type sort = Prop | Type of universe
type implicit_annotation =
- [ `Closed | `Type | `Hole | `Term | `Typeof of int | `Vector ]
+ [ `Closed | `Type | `Hole | `Tagged of string | `Term | `Typeof of int | `Vector ]
+
type lc_kind = Irl of int | Ctx of term list
| `Closed -> "â–ª"
| `Type -> ""
| `Hole -> "â–¡"
+ | `Tagged s -> "[\"" ^ s ^ "\"]"
| `Term -> "Term"
| `Typeof x -> "Ty("^string_of_int x^")"
| `Vector -> "…"
-terms.cmi:
pp.cmi: terms.cmi
foSubst.cmi: terms.cmi
orderings.cmi: terms.cmi
nCicBlob.cmi: terms.cmi
cicBlob.cmi: terms.cmi
nCicProof.cmi: terms.cmi
-nCicParamod.cmi:
terms.cmo: terms.cmi
terms.cmx: terms.cmi
pp.cmo: terms.cmi pp.cmi
-nDiscriminationTree.cmi:
-nCicMetaSubst.cmi:
-nCicUnifHint.cmi:
nCicCoercion.cmi: nCicUnifHint.cmi
-nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi
+nRstatus.cmi: nCicCoercion.cmi
nCicUnification.cmi: nRstatus.cmi
nCicRefiner.cmi: nRstatus.cmi
nDiscriminationTree.cmo: nDiscriminationTree.cmi
nCicCoercion.cmi
nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
nCicCoercion.cmi
-nRstatus.cmo: nCicUnifHint.cmi nCicCoercion.cmi nRstatus.cmi
-nRstatus.cmx: nCicUnifHint.cmx nCicCoercion.cmx nRstatus.cmi
-nCicUnification.cmo: nRstatus.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \
- nCicCoercion.cmi nCicUnification.cmi
-nCicUnification.cmx: nRstatus.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
- nCicCoercion.cmx nCicUnification.cmi
+nRstatus.cmo: nCicCoercion.cmi nRstatus.cmi
+nRstatus.cmx: nCicCoercion.cmx nRstatus.cmi
+nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi
+nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi
nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicCoercion.cmi \
nCicRefiner.cmi
nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicCoercion.cmx \
| `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
| `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
| `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
+ | `Tagged s -> NCicMetaSubst.mk_meta ~name:s metasenv context (foo `Term)
| `Vector ->
raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^
"can only be used in argument position")))
-nCicTacReduction.cmi:
-nTacStatus.cmi:
-nCicElim.cmi:
nTactics.cmi: nTacStatus.cmi
+nInversion.cmi: nTacStatus.cmi
nCicTacReduction.cmo: nCicTacReduction.cmi
nCicTacReduction.cmx: nCicTacReduction.cmi
nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi
nCicElim.cmx: nCicElim.cmi
nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi
nTactics.cmx: nTacStatus.cmx nCicElim.cmx nTactics.cmi
+nInversion.cmo: nTactics.cmi nInversion.cmi
+nInversion.cmx: nTactics.cmx nInversion.cmi
nCicTacReduction.mli \
nTacStatus.mli \
nCicElim.mli \
- nTactics.mli
+ nTactics.mli \
+ nInversion.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
--- /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 $ *)
+
+let fresh_name =
+ let i = ref 0 in
+ function () ->
+ incr i;
+ "z" ^ string_of_int !i
+;;
+
+let mk_id id =
+ let id = if id = "_" then fresh_name () else id in
+ CicNotationPt.Ident (id,None)
+;;
+
+let rec split_arity ~subst context te =
+ match NCicReduction.whd ~subst context te with
+ | NCic.Prod (name,so,ta) ->
+ split_arity ~subst ((name, (NCic.Decl so))::context) ta
+ | t -> context, t
+;;
+
+let mk_appl =
+ function
+ [] -> assert false
+ | [x] -> x
+ | l -> CicNotationPt.Appl l
+;;
+
+let rec mk_prods l t =
+ match l with
+ [] -> t
+ | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
+;;
+
+let rec mk_lambdas l t =
+ match l with
+ [] -> t
+ | hd::tl -> CicNotationPt.Binder (`Lambda, (mk_id hd, None), mk_lambdas tl t)
+;;
+
+let rec mk_arrows l t =
+ match l with
+ [] -> t
+ | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id "_", Some hd), mk_arrows tl t)
+;;
+
+let subst_metasenv_and_fix_names status =
+ let u,h,metasenv, subst,o = status#obj in
+ let o =
+ NCicUntrusted.map_obj_kind ~skip_body:true
+ (NCicUntrusted.apply_subst subst []) o
+ in
+ status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
+;;
+
+let mk_inverter name it leftno status baseuri =
+ prerr_endline ("leftno = " ^ string_of_int leftno);
+ let _,ind_name,ty,cl = it in
+ prerr_endline ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty);
+ let ncons = List.length cl in
+ (*let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
+ let params = List.rev_map (function name,_ -> mk_id name) params in
+ prerr_endline ("lunghezza params = " ^ string_of_int (List.length params));*)
+ let args,sort = split_arity ~subst:[] [] ty in
+ prerr_endline ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort);
+ (*let args = List.rev_map (function name,_ -> mk_id name) args in
+ prerr_endline ("lunghezza args = " ^ string_of_int (List.length args));*)
+ let nparams = List.length args in
+ prerr_endline ("nparams = " ^ string_of_int nparams);
+
+ let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (nparams+1)) in
+ prerr_endline ("lunghezza xs = " ^ string_of_int (List.length xs));
+ let ls, rs = HExtlib.split_nth leftno xs in
+ prerr_endline ("lunghezza ls = " ^ string_of_int (List.length ls));
+ prerr_endline ("lunghezza rs = " ^ string_of_int (List.length rs));
+ let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (nparams+1)) in
+
+ let id_xs = List.map mk_id xs in
+ let id_ls = List.map mk_id ls in
+ let id_rs = List.map mk_id rs in
+ let id_ys = List.map mk_id ys in
+
+ (* pseudocode let t = Lambda y1 ... yr. xs_ = ys_ -> pred *)
+
+ (* check: assuming we have more than one right parameter *)
+ (* pred := P yr- *)
+ let pred = mk_appl ((mk_id "P")::id_ys) in
+
+ let selection = HExtlib.mk_list true (List.length ys) in
+ let prods =
+ let rec prodaux = function
+ [],[],[] -> pred
+ | false :: l,x::xs,y::ys -> prodaux (l,xs,ys)
+ | true :: l,x::xs,y::ys ->
+ CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])),
+ prodaux (l,xs,ys))
+ | _ -> assert false
+ in prodaux (selection,id_rs,id_ys)
+ in
+
+ let lambdas = mk_lambdas (ys@["p"]) prods in
+
+ let hyplist =
+ let rec hypaux k = function
+ 0 -> []
+ | n -> ("H" ^ string_of_int k) :: hypaux (k+1) (n-1)
+ in (hypaux 1 ncons)
+ in
+ prerr_endline ("lunghezza ys = " ^ string_of_int (List.length ys));
+ let theorem = mk_prods xs
+ (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort `Prop))),
+ mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", (*Some (mk_appl (List.map mk_id (ind_name::xs)))) *)
+ Some (CicNotationPt.Implicit `JustOne)),
+ mk_appl (mk_id "P"::id_rs)))))
+ in
+ let t = mk_appl ( [mk_id (ind_name ^ "_ind"); lambdas] @
+ List.map mk_id hyplist @
+ CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in
+
+ prerr_endline ("NINVERTER 0");
+ let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri
+ (baseuri ^ name ^ ".def",
+ 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some (CicNotationPt.Implicit (`Tagged "inv")))) in
+ prerr_endline ("NINVERTER 1");
+ let uri,height,nmenv,nsubst,nobj = theorem in
+ let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
+ let status = status#set_obj theorem in
+ let status = status#set_stack ninitial_stack in
+ let status = subst_metasenv_and_fix_names status in
+
+ let cut_theorem =
+ mk_arrows (List.map
+ (fun x -> let x = mk_id x in mk_appl [mk_id "eq";
+ CicNotationPt.Implicit `JustOne;
+ x;x]) rs) (mk_appl (mk_id "P"::List.map mk_id rs)) in
+ let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
+ CicNotationPt.Implicit (`Tagged "end"));
+ CicNotationPt.Implicit (`Tagged "cut")] in
+
+ let intros = List.map (fun x -> NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in
+ (*let branches =
+ let rec branch_aux k = function
+ 0 -> [NTactics.apply_tac ("",0,mk_id "H")]
+ | n -> NTactics.apply_tac ("",0,mk_id ("H"^(string_of_int k)))::(branch_aux (k+1) (n-1))
+ in branch_aux 1 ncons
+ in*)
+
+ let status = NTactics.block_tac
+ (NTactics.branch_tac::
+ NTactics.case_tac "inv"::
+ (intros @
+ [NTactics.apply_tac ("",0,cut);
+ NTactics.branch_tac;
+ NTactics.case_tac "end";
+ (*NTactics.intro_tac "Hcut";*)
+ NTactics.apply_tac ("",0,mk_id "Hcut");
+ NTactics.apply_tac ("",0,mk_id "refl_eq");
+ NTactics.shift_tac;
+ NTactics.case_tac "cut";
+ NTactics.apply_tac ("",0,t);
+ (* NTactics.branch_tac]
+ @ branches @
+ [NTactics.merge_tac; *)
+ NTactics.merge_tac;
+ NTactics.merge_tac;
+ NTactics.skip_tac])) status in
+ status,status#obj
+;;
+
+
+let ast_of_sort s =
+ match s with
+ NCic.Prop -> `Prop,"ind"
+ | NCic.Type u ->
+ let u = NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] (NCic.Sort s) in
+ (try
+ if String.sub u 0 4 = "Type" then
+ `NType (String.sub u 4 (String.length u - 4)), "rect_" ^ u
+ else if String.sub u 0 5 = "CProp" then
+ `NCProp (String.sub u 5 (String.length u - 5)), "rect_" ^ u
+ else
+ (prerr_endline u;
+ assert false)
+ with Failure _ -> assert false)
+;;
--- /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 $ *)
+
+val mk_inverter: string -> NCic.inductiveType -> int -> (#NTacStatus.tac_status as 's) -> string -> 's * NCic.obj
+
status#set_stack gstatus
;;
+let case_tac lab status =
+ let gstatus =
+ match status#stack with
+ | [] -> assert false
+ | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
+ when is_fresh loc ->
+ let l_js = List.filter
+ (fun curloc ->
+ let _,_,metasenv,_,_ = status#obj in
+ match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with
+ Some s,_,_ when s = lab -> true
+ | _ -> false) ([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#set_stack gstatus
+;;
+
let wildcard_tac status =
let gstatus =
match status#stack with
val branch_tac: 's NTacStatus.tactic
val shift_tac: 's NTacStatus.tactic
val pos_tac: int list -> 's NTacStatus.tactic
+val case_tac: string -> 's NTacStatus.tactic
val wildcard_tac: 's NTacStatus.tactic
val merge_tac: 's NTacStatus.tactic
val focus_tac: int list -> 's NTacStatus.tactic
-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
-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: proofEngineTypes.cmi automationCache.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: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi
declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi
-(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Apr 28 17:14:45 CEST 2009 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Mon May 18 11:04:27 CEST 2009 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyP : term:Cic.term -> ProofEngineTypes.tactic
-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
-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
-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
projects / helm.git / commitdiff