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 (_,xterm) -> Tactics.destruct xterm
| 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
| _ -> 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)
module PEH = ProofEngineHelpers
module ET = EqualityTactics
module DTI = DoubleTypeInference
-module FNG = FreshNamesGenerator
let debug = false
let debug_print =
in
PET.mk_tactic clear_term
-let simpl_in_term context = function
- | Cic.Rel i ->
- let name = match List.nth context (pred i) with
- | Some (Cic.Name s, Cic.Def _) -> s
- | Some (Cic.Name s, Cic.Decl _) -> s
- | _ -> assert false
- in
- RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None)
- | _ -> T.id_tac
-
-let mk_fresh_name metasenv context name typ =
- let name = C.Name name in
- match FNG.mk_fresh_name ~subst:[] metasenv context name ~typ with
- | C.Name s -> s
- | C.Anonymous -> assert false
-
let exists context = function
| C.Rel i -> List.nth context (pred i) <> None
| _ -> true
-let rec recur_on_child_tac name =
+let rec recur_on_child_tac ~before =
let recur_on_child status =
let (proof, goal) = status in
let _, metasenv, _subst, _, _, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
- debug_print (lazy ("\nrecur_on_child su: " ^ name));
+ debug_print (lazy ("\nrecur_on_child"));
debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
- let rec search_name i = function
- | [] -> T.id_tac
- | Some (Cic.Name n, _) :: _ when n = name ->
- destruct ~first_time:false (Cic.Rel i)
- | _ :: tl -> search_name (succ i) tl
+ let mk_lterm term c m ug =
+ let distance = List.length c - List.length context in
+ S.lift distance term, m, ug
in
- PET.apply_tactic (search_name 1 context) status
+ let lterm = mk_lterm (Cic.Rel 1) in
+ let continuation = destruct ~first_time:false lterm in
+ let tactic = T.then_ ~start:before ~continuation in
+ PET.apply_tactic tactic status
in
PET.mk_tactic recur_on_child
PET.mk_tactic fill_cut
in
debug_print (lazy ("CUT: " ^ pp context cutted));
- let name = mk_fresh_name metasenv context "Hcut" cutted in
- let mk_fresh_name_callback = PEH.namer_of [Some name] in
- debug_print (lazy ("figlio: " ^ name));
let tactic =
- T.thens ~start: (P.cut_tac ~mk_fresh_name_callback cutted)
+ T.thens ~start: (P.cut_tac cutted)
~continuations:[
- T.seq ~tactics:[continuation; recur_on_child_tac name];
+ recur_on_child_tac continuation;
fill_cut_tac term
]
in
debug_print (lazy ("nella premessa: " ^ name));
let pattern = None, [name, PET.hole], None in
let start = ET.rewrite_tac ~direction ~pattern term [] in
- let ok_tactic =
- T.seq ~tactics:[continuation; recur_on_child_tac name]
- in
- debug_print (lazy ("figlio: " ^ name));
+ let ok_tactic = recur_on_child_tac continuation in
T.if_ ~start ~continuation:ok_tactic ~fail:continuation
in
PET.apply_tactic tactic status
in
PET.mk_tactic subst_tac
-and destruct ~first_time term =
+and destruct ~first_time lterm =
let are_convertible hd1 hd2 metasenv context =
fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
in
let (proof, goal) = status in
let _,metasenv,_subst, _,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- debug_print (lazy ("\ndestruct di: " ^ pp context term));
- debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
- let termty,_ =
- CTC.type_of_aux' metasenv context term CU.empty_ugraph
- in
- debug_print (lazy ("\ndestruct su: " ^ pp context termty));
- let mk_lterm term c m ug =
- let distance = List.length c - List.length context in
- S.lift distance term, m, ug
- in
- let lterm = mk_lterm term in
- let mk_subst_chain direction index with_what what =
- let k = match term with C.Rel i -> i | _ -> -1 in
- let rec traverse_context first_time j = function
- | [] ->
- let continuation =
- T.seq ~tactics:[
- clear_term first_time lterm;
- clear_term false (mk_lterm what);
- clear_term false (mk_lterm with_what)
- ]
- in
- subst_tac ~direction ~lterm ~where:None ~continuation
- | Some (C.Name name, _) :: tl when j < index && j <> k ->
- debug_print (lazy ("\nsubst programmata: cosa: " ^ string_of_int index ^ ", dove: " ^ string_of_int j));
- subst_tac ~direction ~lterm ~where:(Some name)
- ~continuation:(traverse_context false (succ j) tl)
- | _ :: tl -> traverse_context first_time (succ j) tl
+ let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+ let tactic = if not (first_time || exists context term) then T.id_tac else begin
+ debug_print (lazy ("\ndestruct di: " ^ pp context term));
+ debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
+ let termty,_ = CTC.type_of_aux' metasenv context term CU.empty_ugraph in
+ debug_print (lazy ("\ndestruct su: " ^ pp context termty));
+ let mk_lterm term c m ug =
+ let distance = List.length c - List.length context in
+ S.lift distance term, m, ug
in
- traverse_context first_time 1 context
- in
- let tac = match termty with
+ let lterm = mk_lterm term in
+ let mk_subst_chain direction index with_what what =
+ let k = match term with C.Rel i -> i | _ -> -1 in
+ let rec traverse_context first_time j = function
+ | [] ->
+ let continuation =
+ T.seq ~tactics:[
+ clear_term first_time lterm;
+ clear_term false (mk_lterm what);
+ clear_term false (mk_lterm with_what)
+ ]
+ in
+ subst_tac ~direction ~lterm ~where:None ~continuation
+ | Some (C.Name name, _) :: tl when j < index && j <> k ->
+ debug_print (lazy ("\nsubst programmata: cosa: " ^ string_of_int index ^ ", dove: " ^ string_of_int j));
+ subst_tac ~direction ~lterm ~where:(Some name)
+ ~continuation:(traverse_context false (succ j) tl)
+ | _ :: tl -> traverse_context first_time (succ j) tl
+ in
+ traverse_context first_time 1 context
+ in
+ match termty with
| C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
when LibraryObjects.is_eq_URI equri ->
begin match t1,t2 with
end
| _ when first_time -> raise exn_nothingtodo
| _ (* when not first time *) -> T.id_tac
- in
- PET.apply_tactic tac status
+ end in
+ PET.apply_tactic tactic status
in
PET.mk_tactic destruct
-let lazy_destruct_tac ~first_time ~lterm =
- let lazy_destruct status =
+(* destruct performs either injection or discriminate or subst *)
+let destruct_tac xterm =
+ let destruct status =
let (proof, goal) = status in
let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let term, _, _ = lterm context metasenv CU.empty_ugraph in
- let tactic =
- if exists context term then destruct ~first_time term else T.id_tac
+ let mk_lterm term c m ug =
+ let distance = List.length c - List.length context in
+ S.lift distance term, m, ug
in
- PET.apply_tactic tactic status
- in
- PET.mk_tactic lazy_destruct
-
-(* destruct performs either injection or discriminate *)
-(* equivalent to Coq's "analyze equality" *)
-let destruct_tac = function
- | Some term -> destruct ~first_time:true term
- | None ->
- let destruct_all status =
- let (proof, goal) = status in
- let _,metasenv,_subst,_,_, _ = proof in
- let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let mk_lterm term c m ug =
- let distance = List.length c - List.length context in
- S.lift distance term, m, ug
- in
- let rec mk_tactics first_time i tacs = function
- | [] -> List.rev tacs
- | Some _ :: tl ->
- let lterm = mk_lterm (C.Rel i) in
- let tacs = lazy_destruct_tac ~first_time ~lterm :: tacs in
- mk_tactics false (succ i) tacs tl
- | _ :: tl -> mk_tactics first_time (succ i) tacs tl
- in
- let tactics = mk_tactics false 1 [] context in
- PET.apply_tactic (T.seq ~tactics) status
+ let tactics = match xterm with
+ | Some term -> [destruct ~first_time:true (mk_lterm term)]
+ | None ->
+ let rec mk_tactics first_time i tacs = function
+ | [] -> List.rev tacs
+ | Some _ :: tl ->
+ let lterm = mk_lterm (C.Rel i) in
+ let tacs = destruct ~first_time lterm :: tacs in
+ mk_tactics false (succ i) tacs tl
+ | _ :: tl -> mk_tactics first_time (succ i) tacs tl
+ in
+ mk_tactics false 1 [] context
in
- PET.mk_tactic destruct_all
+ PET.apply_tactic (T.seq ~tactics) status
+ in
+ PET.mk_tactic destruct
projects / helm.git / commitdiff