- ProofEngineHelpers: namer_of exported from GrafiteEngine
+module PEH = ProofEngineHelpers
+
exception Drop
(* mo file name, ma file name *)
exception IncludedFileNotCompiled of string * string
exception Drop
(* mo file name, ma file name *)
exception IncludedFileNotCompiled of string * string
-(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
- * names as long as they are available, then it fallbacks to name generation
- * using FreshNamesGenerator module *)
-let namer_of names =
- let len = List.length names in
- let count = ref 0 in
- fun metasenv context name ~typ ->
- if !count < len then begin
- let name = match List.nth names !count with
- | Some s -> Cic.Name s
- | None -> Cic.Anonymous
- in
- incr count;
- name
- end else
- FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
-
let rec tactic_of_ast status ast =
let module PET = ProofEngineTypes in
match ast with
let rec tactic_of_ast status ast =
let module PET = ProofEngineTypes in
match ast with
Tactics.auto ~params ~dbd:(LibraryDb.instance ())
~universe:status.GrafiteTypes.universe
| GrafiteAst.Cases (_, what, (howmany, names)) ->
Tactics.auto ~params ~dbd:(LibraryDb.instance ())
~universe:status.GrafiteTypes.universe
| GrafiteAst.Cases (_, what, (howmany, names)) ->
- Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
+ Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(PEH.namer_of names)
what
| GrafiteAst.Change (_, pattern, with_what) ->
Tactics.change ~pattern with_what
what
| GrafiteAst.Change (_, pattern, with_what) ->
Tactics.change ~pattern with_what
| GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
| GrafiteAst.Compose (_,t1,t2,times,(howmany, names)) ->
Tactics.compose times t1 t2 ?howmany
| GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
| GrafiteAst.Compose (_,t1,t2,times,(howmany, names)) ->
Tactics.compose times t1 t2 ?howmany
- ~mk_fresh_name_callback:(namer_of names)
+ ~mk_fresh_name_callback:(PEH.namer_of names)
| GrafiteAst.Contradiction _ -> Tactics.contradiction
| GrafiteAst.Constructor (_, n) -> Tactics.constructor n
| GrafiteAst.Cut (_, ident, term) ->
let names = match ident with None -> [] | Some id -> [Some id] in
| GrafiteAst.Contradiction _ -> Tactics.contradiction
| GrafiteAst.Constructor (_, n) -> Tactics.constructor n
| GrafiteAst.Cut (_, ident, term) ->
let names = match ident with None -> [] | Some id -> [Some id] in
- Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
+ Tactics.cut ~mk_fresh_name_callback:(PEH.namer_of names) term
| GrafiteAst.Decompose (_, names) ->
| GrafiteAst.Decompose (_, names) ->
- let mk_fresh_name_callback = namer_of names in
+ let mk_fresh_name_callback = PEH.namer_of names in
Tactics.decompose ~mk_fresh_name_callback ()
| GrafiteAst.Demodulate _ ->
Tactics.demodulate
~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
| GrafiteAst.Destruct (_,term) -> Tactics.destruct term
| GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
Tactics.decompose ~mk_fresh_name_callback ()
| GrafiteAst.Demodulate _ ->
Tactics.demodulate
~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
| GrafiteAst.Destruct (_,term) -> Tactics.destruct term
| GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
- Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
+ Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names)
~pattern what
| GrafiteAst.ElimType (_, what, using, (depth, names)) ->
~pattern what
| GrafiteAst.ElimType (_, what, using, (depth, names)) ->
- Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
+ Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names)
what
| GrafiteAst.Exact (_, term) -> Tactics.exact term
| GrafiteAst.Exists _ -> Tactics.exists
what
| GrafiteAst.Exact (_, term) -> Tactics.exact term
| GrafiteAst.Exists _ -> Tactics.exists
Tactics.fold ~reduction ~term ~pattern
| GrafiteAst.Fourier _ -> Tactics.fourier
| GrafiteAst.FwdSimpl (_, hyp, names) ->
Tactics.fold ~reduction ~term ~pattern
| GrafiteAst.Fourier _ -> Tactics.fourier
| GrafiteAst.FwdSimpl (_, hyp, names) ->
- Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names)
+ Tactics.fwd_simpl ~mk_fresh_name_callback:(PEH.namer_of names)
~dbd:(LibraryDb.instance ()) hyp
| GrafiteAst.Generalize (_,pattern,ident) ->
let names = match ident with None -> [] | Some id -> [Some id] in
~dbd:(LibraryDb.instance ()) hyp
| GrafiteAst.Generalize (_,pattern,ident) ->
let names = match ident with None -> [] | Some id -> [Some id] in
- Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern
+ Tactics.generalize ~mk_fresh_name_callback:(PEH.namer_of names) pattern
| GrafiteAst.IdTac _ -> Tactics.id
| GrafiteAst.Intros (_, (howmany, names)) ->
PrimitiveTactics.intros_tac ?howmany
| GrafiteAst.IdTac _ -> Tactics.id
| GrafiteAst.Intros (_, (howmany, names)) ->
PrimitiveTactics.intros_tac ?howmany
- ~mk_fresh_name_callback:(namer_of names) ()
+ ~mk_fresh_name_callback:(PEH.namer_of names) ()
| GrafiteAst.Inversion (_, term) ->
Tactics.inversion term
| GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) ->
let names = match ident with None -> [] | Some id -> [Some id] in
| GrafiteAst.Inversion (_, term) ->
Tactics.inversion term
| GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) ->
let names = match ident with None -> [] | Some id -> [Some id] in
- Tactics.lapply ~mk_fresh_name_callback:(namer_of names)
+ Tactics.lapply ~mk_fresh_name_callback:(PEH.namer_of names)
~linear ?how_many ~to_what what
| GrafiteAst.Left _ -> Tactics.left
| GrafiteAst.LetIn (loc,term,name) ->
~linear ?how_many ~to_what what
| GrafiteAst.Left _ -> Tactics.left
| GrafiteAst.LetIn (loc,term,name) ->
- Tactics.letin term ~mk_fresh_name_callback:(namer_of [Some name])
+ Tactics.letin term ~mk_fresh_name_callback:(PEH.namer_of [Some name])
| GrafiteAst.Reduce (_, reduction_kind, pattern) ->
(match reduction_kind with
| `Normalize -> Tactics.normalize ~pattern
| GrafiteAst.Reduce (_, reduction_kind, pattern) ->
(match reduction_kind with
| `Normalize -> Tactics.normalize ~pattern
Tactics.replace ~pattern ~with_what
| GrafiteAst.Rewrite (_, direction, t, pattern, names) ->
EqualityTactics.rewrite_tac ~direction ~pattern t
Tactics.replace ~pattern ~with_what
| GrafiteAst.Rewrite (_, direction, t, pattern, names) ->
EqualityTactics.rewrite_tac ~direction ~pattern t
-(* to be replaced with ~mk_fresh_name_callback:(namer_of names) *)
+(* to be replaced with ~mk_fresh_name_callback:(PEH.namer_of names) *)
(List.map (function Some s -> s | None -> assert false) names)
| GrafiteAst.Right _ -> Tactics.right
| GrafiteAst.Ring _ -> Tactics.ring
(List.map (function Some s -> s | None -> assert false) names)
| GrafiteAst.Right _ -> Tactics.right
| GrafiteAst.Ring _ -> Tactics.ring
(MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
;;
(MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
;;
+(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
+ * names as long as they are available, then it fallbacks to name generation
+ * using FreshNamesGenerator module *)
+let namer_of names =
+ let len = List.length names in
+ let count = ref 0 in
+ fun metasenv context name ~typ ->
+ if !count < len then begin
+ let name = match List.nth names !count with
+ | Some s -> Cic.Name s
+ | None -> Cic.Anonymous
+ in
+ incr count;
+ name
+ end else
+ FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
(Cic.context * Cic.term) list * int
val split_with_normalize: Cic.context * Cic.term ->
(Cic.context * Cic.term) list * int
(Cic.context * Cic.term) list * int
val split_with_normalize: Cic.context * Cic.term ->
(Cic.context * Cic.term) list * int
+
+(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
+ * names as long as they are available, then it fallbacks to name generation
+ * using FreshNamesGenerator module *)
+val namer_of: string option list -> ProofEngineTypes.mk_fresh_name_type
+let ifs ~start ~continuations ~fail =
+ let ifs status =
+ let xoutput =
+ try
+ let result = PET.apply_tactic start status in
+ info (lazy ("Tacticals.ifs: succedeed!!!"));
+ Some result
+ with PET.Fail _ -> None
+ in
+ let tactic = match xoutput with
+ | Some res -> thens ~start:(const_tac res) ~continuations
+ | None -> fail
+ in
+ PET.apply_tactic tactic status
+ in
+ PET.mk_tactic ifs
+
let first ~tactics =
let rec first ~(tactics: tactic list) status =
info (lazy "in Tacticals.first");
let first ~tactics =
let rec first ~(tactics: tactic list) status =
info (lazy "in Tacticals.first");
val first: tactics: tactic list -> tactic
val thens: start: tactic -> continuations: tactic list -> tactic
val then_: start: tactic -> continuation: tactic -> tactic
val first: tactics: tactic list -> tactic
val thens: start: tactic -> continuations: tactic list -> tactic
val then_: start: tactic -> continuation: tactic -> tactic
+val ifs: start: tactic -> continuations: tactic list -> fail: tactic -> tactic
val if_: start: tactic -> continuation: tactic -> fail: tactic -> tactic
val seq: tactics: tactic list -> tactic (** "folding" of then_ *)
val repeat_tactic: tactic: tactic -> tactic
val if_: start: tactic -> continuation: tactic -> fail: tactic -> tactic
val seq: tactics: tactic list -> tactic (** "folding" of then_ *)
val repeat_tactic: tactic: tactic -> tactic