-(** 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 = Cic.Name (List.nth names !count) in
- incr count;
- name
- end else
- FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
-
-let tactic_of_ast = function
- | TacticAst.Absurd (_, term) -> Tactics.absurd term
- | TacticAst.Apply (_, term) -> Tactics.apply term
- | TacticAst.Assumption _ -> Tactics.assumption
- | TacticAst.Auto (_,depth,width) ->
- AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) ()
- | TacticAst.Change (_, pattern, with_what) ->
- Tactics.change ~pattern with_what
- | TacticAst.Clear (_,id) -> Tactics.clear id
- | TacticAst.ClearBody (_,id) -> Tactics.clearbody id
- | TacticAst.Contradiction _ -> Tactics.contradiction
- | TacticAst.Compare (_, term) -> Tactics.compare term
- | TacticAst.Constructor (_, n) -> Tactics.constructor n
- | TacticAst.Cut (_, ident, term) ->
- let names = match ident with None -> [] | Some id -> [id] in
- Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
- | TacticAst.DecideEquality _ -> Tactics.decide_equality
- | TacticAst.Decompose (_,term) -> Tactics.decompose term
- | TacticAst.Discriminate (_,term) -> Tactics.discriminate term
- | TacticAst.Elim (_, what, using, depth, names) ->
- Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
- | TacticAst.ElimType (_, what, using, depth, names) ->
- Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
- | TacticAst.Exact (_, term) -> Tactics.exact term
- | TacticAst.Exists _ -> Tactics.exists
- | TacticAst.Fail _ -> Tactics.fail
- | TacticAst.Fold (_, reduction_kind, term, pattern) ->
- let reduction =
- match reduction_kind with
- | `Normalize -> CicReduction.normalize ~delta:false ~subst:[]
- | `Reduce -> ProofEngineReduction.reduce
- | `Simpl -> ProofEngineReduction.simpl
- | `Whd -> CicReduction.whd ~delta:false ~subst:[]
- in
- Tactics.fold ~reduction ~term ~pattern
- | TacticAst.Fourier _ -> Tactics.fourier
- | TacticAst.FwdSimpl (_, hyp, names) ->
- Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(MatitaDb.instance ()) hyp
- | TacticAst.Generalize (_,pattern,ident) ->
- let names = match ident with None -> [] | Some id -> [id] in
- Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern
- | TacticAst.Goal (_, n) -> Tactics.set_goal n
- | TacticAst.IdTac _ -> Tactics.id
- | TacticAst.Injection (_,term) -> Tactics.injection term
- | TacticAst.Intros (_, None, names) ->
- PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
- | TacticAst.Intros (_, Some num, names) ->
- PrimitiveTactics.intros_tac ~howmany:num
- ~mk_fresh_name_callback:(namer_of names) ()
- | TacticAst.LApply (_, how_many, to_what, what, ident) ->
- let names = match ident with None -> [] | Some id -> [id] in
- Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many ~to_what what
- | TacticAst.Left _ -> Tactics.left
- | TacticAst.LetIn (loc,term,name) ->
- Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
- | TacticAst.Reduce (_, reduction_kind, pattern) ->
- (match reduction_kind with
- | `Normalize -> Tactics.normalize ~pattern
- | `Reduce -> Tactics.reduce ~pattern
- | `Simpl -> Tactics.simpl ~pattern
- | `Whd -> Tactics.whd ~pattern)
- | TacticAst.Reflexivity _ -> Tactics.reflexivity
- | TacticAst.Replace (_, pattern, with_what) ->
- Tactics.replace ~pattern ~with_what
- | TacticAst.Rewrite (_, direction, t, pattern) ->
- EqualityTactics.rewrite_tac ~direction ~pattern t
- | TacticAst.Right _ -> Tactics.right
- | TacticAst.Ring _ -> Tactics.ring
- | TacticAst.Split _ -> Tactics.split
- | TacticAst.Symmetry _ -> Tactics.symmetry
- | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
-
-let disambiguate_term status term =
- let (aliases, metasenv, cic, _) =
- match
- MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
- ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
- ~metasenv:(MatitaMisc.get_proof_metasenv status) term
- with
- | [x] -> x
- | _ -> assert false
- in
- let proof_status =
- match status.proof_status with
- | No_proof -> Intermediate metasenv
- | Incomplete_proof ((uri, _, proof, ty), goal) ->
- Incomplete_proof ((uri, metasenv, proof, ty), goal)
- | Intermediate _ -> Intermediate metasenv
- | Proof _ -> assert false
- in
- let status = { status with proof_status = proof_status } in
- let status = MatitaSync.set_proof_aliases status aliases in
- status, cic
-
-let disambiguate_pattern status (wanted, hyp_paths, goal_path) =
- let interp path = Disambiguate.interpretate_path [] status.aliases path in
- let goal_path = interp goal_path in
- let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
- let status,wanted =
- match wanted with
- None -> status,None
- | Some wanted ->
- let status,wanted = disambiguate_term status wanted in
- status, Some wanted
- in
- status, (wanted, hyp_paths ,goal_path)
-
-let disambiguate_tactic status = function
- | TacticAst.Apply (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Apply (loc, cic)
- | TacticAst.Absurd (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Absurd (loc, cic)
- | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
- | TacticAst.Auto (loc,depth,width) -> status, TacticAst.Auto (loc,depth,width)
- | TacticAst.Change (loc, pattern, with_what) ->
- let status, with_what = disambiguate_term status with_what in
- let status, pattern = disambiguate_pattern status pattern in
- status, TacticAst.Change (loc, pattern, with_what)
- | TacticAst.Clear (loc,id) -> status,TacticAst.Clear (loc,id)
- | TacticAst.ClearBody (loc,id) -> status,TacticAst.ClearBody (loc,id)
- | TacticAst.Compare (loc,term) ->
- let status, term = disambiguate_term status term in
- status, TacticAst.Compare (loc,term)
- | TacticAst.Constructor (loc,n) ->
- status, TacticAst.Constructor (loc,n)
- | TacticAst.Contradiction loc ->
- status, TacticAst.Contradiction loc
- | TacticAst.Cut (loc, ident, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Cut (loc, ident, cic)
- | TacticAst.DecideEquality loc ->
- status, TacticAst.DecideEquality loc
- | TacticAst.Decompose (loc,term) ->
- let status,term = disambiguate_term status term in
- status, TacticAst.Decompose(loc,term)
- | TacticAst.Discriminate (loc,term) ->
- let status,term = disambiguate_term status term in
- status, TacticAst.Discriminate(loc,term)
- | TacticAst.Exact (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Exact (loc, cic)
- | TacticAst.Elim (loc, what, Some using, depth, idents) ->
- let status, what = disambiguate_term status what in
- let status, using = disambiguate_term status using in
- status, TacticAst.Elim (loc, what, Some using, depth, idents)
- | TacticAst.Elim (loc, what, None, depth, idents) ->
- let status, what = disambiguate_term status what in
- status, TacticAst.Elim (loc, what, None, depth, idents)
- | TacticAst.ElimType (loc, what, Some using, depth, idents) ->
- let status, what = disambiguate_term status what in
- let status, using = disambiguate_term status using in
- status, TacticAst.ElimType (loc, what, Some using, depth, idents)
- | TacticAst.ElimType (loc, what, None, depth, idents) ->
- let status, what = disambiguate_term status what in
- status, TacticAst.ElimType (loc, what, None, depth, idents)
- | TacticAst.Exists loc -> status, TacticAst.Exists loc
- | TacticAst.Fail loc -> status,TacticAst.Fail loc
- | TacticAst.Fold (loc,reduction_kind, term, pattern) ->
- let status, pattern = disambiguate_pattern status pattern in
- let status, term = disambiguate_term status term in
- status, TacticAst.Fold (loc,reduction_kind, term, pattern)
- | TacticAst.FwdSimpl (loc, hyp, names) ->
- status, TacticAst.FwdSimpl (loc, hyp, names)
- | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
- | TacticAst.Generalize (loc,pattern,ident) ->
- let status, pattern = disambiguate_pattern status pattern in
- status, TacticAst.Generalize(loc,pattern,ident)
- | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
- | TacticAst.IdTac loc -> status,TacticAst.IdTac loc
- | TacticAst.Injection (loc,term) ->
- let status, term = disambiguate_term status term in
- status, TacticAst.Injection (loc,term)
- | TacticAst.Intros (loc, num, names) ->
- status, TacticAst.Intros (loc, num, names)
- | TacticAst.LApply (loc, depth, to_what, what, ident) ->
- let f term (status, to_what) =
- let status, term = disambiguate_term status term in
- status, term :: to_what