clean_baseuri: bool
}
+(** 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
Tactics.auto ~params ~dbd:(LibraryDb.instance ())
~universe:status.GrafiteTypes.universe
| GrafiteAst.Cases (_, what, (howmany, names)) ->
- Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(PEH.namer_of names)
+ Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
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
- ~mk_fresh_name_callback:(PEH.namer_of names)
+ ~mk_fresh_name_callback:(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
- Tactics.cut ~mk_fresh_name_callback:(PEH.namer_of names) term
+ Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
| GrafiteAst.Decompose (_, names) ->
- let mk_fresh_name_callback = PEH.namer_of names in
+ let mk_fresh_name_callback = 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.Destruct (_,xterms) -> Tactics.destruct xterms
| GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
- Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names)
+ Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
~pattern what
| GrafiteAst.ElimType (_, what, using, (depth, names)) ->
- Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names)
+ Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
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.fwd_simpl ~mk_fresh_name_callback:(PEH.namer_of names)
+ Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names)
~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:(PEH.namer_of names) pattern
+ Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern
| GrafiteAst.IdTac _ -> Tactics.id
| GrafiteAst.Intros (_, (howmany, names)) ->
PrimitiveTactics.intros_tac ?howmany
- ~mk_fresh_name_callback:(PEH.namer_of names) ()
+ ~mk_fresh_name_callback:(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
- Tactics.lapply ~mk_fresh_name_callback:(PEH.namer_of names)
+ 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:(PEH.namer_of [Some name])
+ Tactics.letin term ~mk_fresh_name_callback:(namer_of [Some name])
| 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
-(* to be replaced with ~mk_fresh_name_callback:(PEH.namer_of names) *)
+(* to be replaced with ~mk_fresh_name_callback:(namer_of names) *)
(List.map (function Some s -> s | None -> assert false) names)
| GrafiteAst.Right _ -> Tactics.right
| GrafiteAst.Ring _ -> Tactics.ring
| GrafiteAst.Split _ -> Tactics.split
- | GrafiteAst.Subst _ -> Tactics.subst
| GrafiteAst.Symmetry _ -> Tactics.symmetry
| GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
(* Implementazioni Aggiunte *)
| _ -> false
let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal=
- let module PEH = ProofEngineHelpers in
(* let print_m name metasenv =
prerr_endline (">>>>> " ^ name);
prerr_endline (CicMetaSubst.ppmetasenv [] metasenv)