-type options = {
- do_heavy_checks: bool ;
- include_paths: string list ;
- clean_baseuri: bool
-}
-
-type statement =
- (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement
-
-(** 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
- | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
- | GrafiteAst.Apply (_, term) -> Tactics.apply term
- | GrafiteAst.Assumption _ -> Tactics.assumption
- | GrafiteAst.Auto (_,depth,width) ->
- AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) ()
- | GrafiteAst.Change (_, pattern, with_what) ->
- Tactics.change ~pattern with_what
- | GrafiteAst.Clear (_,id) -> Tactics.clear id
- | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
- | GrafiteAst.Contradiction _ -> Tactics.contradiction
- | GrafiteAst.Compare (_, term) -> Tactics.compare term
- | GrafiteAst.Constructor (_, n) -> Tactics.constructor n
- | GrafiteAst.Cut (_, ident, term) ->
- let names = match ident with None -> [] | Some id -> [id] in
- Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
- | GrafiteAst.DecideEquality _ -> Tactics.decide_equality
- | GrafiteAst.Decompose (_, types, what, names) ->
- let to_type = function
- | GrafiteAst.Type (uri, typeno) -> uri, typeno
- | GrafiteAst.Ident _ -> assert false
- in
- let user_types = List.rev_map to_type types in
- let dbd = MatitaDb.instance () in
- let mk_fresh_name_callback = namer_of names in
- Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
- | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
- | GrafiteAst.Elim (_, what, using, depth, names) ->
- Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
- | GrafiteAst.ElimType (_, what, using, depth, names) ->
- Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
- | GrafiteAst.Exact (_, term) -> Tactics.exact term
- | GrafiteAst.Exists _ -> Tactics.exists
- | GrafiteAst.Fail _ -> Tactics.fail
- | GrafiteAst.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
- | GrafiteAst.Fourier _ -> Tactics.fourier
- | GrafiteAst.FwdSimpl (_, hyp, names) ->
- Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(MatitaDb.instance ()) hyp
- | GrafiteAst.Generalize (_,pattern,ident) ->
- let names = match ident with None -> [] | Some id -> [id] in
- Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern
- | GrafiteAst.Goal (_, n) -> Tactics.set_goal n
- | GrafiteAst.IdTac _ -> Tactics.id
- | GrafiteAst.Injection (_,term) -> Tactics.injection term
- | GrafiteAst.Intros (_, None, names) ->
- PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
- | GrafiteAst.Intros (_, Some num, names) ->
- PrimitiveTactics.intros_tac ~howmany:num
- ~mk_fresh_name_callback:(namer_of names) ()
- | GrafiteAst.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
- | GrafiteAst.Left _ -> Tactics.left
- | GrafiteAst.LetIn (loc,term,name) ->
- Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
- | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
- (match reduction_kind with
- | `Normalize -> Tactics.normalize ~pattern
- | `Reduce -> Tactics.reduce ~pattern
- | `Simpl -> Tactics.simpl ~pattern
- | `Whd -> Tactics.whd ~pattern)
- | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
- | GrafiteAst.Replace (_, pattern, with_what) ->
- Tactics.replace ~pattern ~with_what
- | GrafiteAst.Rewrite (_, direction, t, pattern) ->
- EqualityTactics.rewrite_tac ~direction ~pattern t
- | GrafiteAst.Right _ -> Tactics.right
- | GrafiteAst.Ring _ -> Tactics.ring
- | GrafiteAst.Split _ -> Tactics.split
- | GrafiteAst.Symmetry _ -> Tactics.symmetry
- | GrafiteAst.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
- | GrafiteAst.Apply (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, GrafiteAst.Apply (loc, cic)
- | GrafiteAst.Absurd (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, GrafiteAst.Absurd (loc, cic)
- | GrafiteAst.Assumption loc -> status, GrafiteAst.Assumption loc
- | GrafiteAst.Auto (loc,depth,width) -> status, GrafiteAst.Auto (loc,depth,width)
- | GrafiteAst.Change (loc, pattern, with_what) ->
- let status, with_what = disambiguate_term status with_what in
- let status, pattern = disambiguate_pattern status pattern in
- status, GrafiteAst.Change (loc, pattern, with_what)
- | GrafiteAst.Clear (loc,id) -> status,GrafiteAst.Clear (loc,id)
- | GrafiteAst.ClearBody (loc,id) -> status,GrafiteAst.ClearBody (loc,id)
- | GrafiteAst.Compare (loc,term) ->
- let status, term = disambiguate_term status term in
- status, GrafiteAst.Compare (loc,term)
- | GrafiteAst.Constructor (loc,n) ->
- status, GrafiteAst.Constructor (loc,n)
- | GrafiteAst.Contradiction loc ->
- status, GrafiteAst.Contradiction loc
- | GrafiteAst.Cut (loc, ident, term) ->
- let status, cic = disambiguate_term status term in
- status, GrafiteAst.Cut (loc, ident, cic)
- | GrafiteAst.DecideEquality loc ->
- status, GrafiteAst.DecideEquality loc
- | GrafiteAst.Decompose (loc, types, what, names) ->
- let disambiguate (status, types) = function
- | GrafiteAst.Type _ -> assert false
- | GrafiteAst.Ident id ->
- match disambiguate_term status (CicNotationPt.Ident (id, None)) with
- | status, Cic.MutInd (uri, tyno, _) ->
- status, (GrafiteAst.Type (uri, tyno) :: types)
- | _ ->
- raise Disambiguate.NoWellTypedInterpretation
- in
- let status, types = List.fold_left disambiguate (status, []) types in
- status, GrafiteAst.Decompose(loc, types, what, names)
- | GrafiteAst.Discriminate (loc,term) ->
- let status,term = disambiguate_term status term in
- status, GrafiteAst.Discriminate(loc,term)
- | GrafiteAst.Exact (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, GrafiteAst.Exact (loc, cic)
- | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
- let status, what = disambiguate_term status what in
- let status, using = disambiguate_term status using in
- status, GrafiteAst.Elim (loc, what, Some using, depth, idents)
- | GrafiteAst.Elim (loc, what, None, depth, idents) ->
- let status, what = disambiguate_term status what in
- status, GrafiteAst.Elim (loc, what, None, depth, idents)
- | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
- let status, what = disambiguate_term status what in
- let status, using = disambiguate_term status using in
- status, GrafiteAst.ElimType (loc, what, Some using, depth, idents)
- | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
- let status, what = disambiguate_term status what in
- status, GrafiteAst.ElimType (loc, what, None, depth, idents)
- | GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc
- | GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc
- | GrafiteAst.Fold (loc,reduction_kind, term, pattern) ->
- let status, pattern = disambiguate_pattern status pattern in
- let status, term = disambiguate_term status term in
- status, GrafiteAst.Fold (loc,reduction_kind, term, pattern)
- | GrafiteAst.FwdSimpl (loc, hyp, names) ->
- status, GrafiteAst.FwdSimpl (loc, hyp, names)
- | GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc
- | GrafiteAst.Generalize (loc,pattern,ident) ->
- let status, pattern = disambiguate_pattern status pattern in
- status, GrafiteAst.Generalize(loc,pattern,ident)
- | GrafiteAst.Goal (loc, g) -> status, GrafiteAst.Goal (loc, g)
- | GrafiteAst.IdTac loc -> status,GrafiteAst.IdTac loc
- | GrafiteAst.Injection (loc,term) ->
- let status, term = disambiguate_term status term in
- status, GrafiteAst.Injection (loc,term)
- | GrafiteAst.Intros (loc, num, names) ->
- status, GrafiteAst.Intros (loc, num, names)
- | GrafiteAst.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
- in
- let status, to_what = List.fold_right f to_what (status, []) in
- let status, what = disambiguate_term status what in
- status, GrafiteAst.LApply (loc, depth, to_what, what, ident)
- | GrafiteAst.Left loc -> status, GrafiteAst.Left loc
- | GrafiteAst.LetIn (loc, term, name) ->
- let status, term = disambiguate_term status term in
- status, GrafiteAst.LetIn (loc,term,name)
- | GrafiteAst.Reduce (loc, reduction_kind, pattern) ->
- let status, pattern = disambiguate_pattern status pattern in
- status, GrafiteAst.Reduce(loc, reduction_kind, pattern)
- | GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc
- | GrafiteAst.Replace (loc, pattern, with_what) ->
- let status, pattern = disambiguate_pattern status pattern in
- let status, with_what = disambiguate_term status with_what in
- status, GrafiteAst.Replace (loc, pattern, with_what)
- | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
- let status, term = disambiguate_term status t in
- let status, pattern = disambiguate_pattern status pattern in
- status, GrafiteAst.Rewrite (loc, dir, term, pattern)
- | GrafiteAst.Right loc -> status, GrafiteAst.Right loc
- | GrafiteAst.Ring loc -> status, GrafiteAst.Ring loc
- | GrafiteAst.Split loc -> status, GrafiteAst.Split loc
- | GrafiteAst.Symmetry loc -> status, GrafiteAst.Symmetry loc
- | GrafiteAst.Transitivity (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, GrafiteAst.Transitivity (loc, cic)
-
-let apply_tactic tactic status =
- let status,tactic = disambiguate_tactic status tactic in
- let tactic = tactic_of_ast tactic in
- let (proof, goals) =
- ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status) in
- let dummy = -1 in
- { status with
- proof_status = MatitaTypes.Incomplete_proof (proof,dummy) }, goals
-
-module MatitaStatus =
- struct
- type input_status = MatitaTypes.status
- type output_status = MatitaTypes.status * ProofEngineTypes.goal list
- type tactic = input_status -> output_status
-
- let focus (status,_) goal =
- let proof,_ = MatitaMisc.get_proof_status status in
- {status with proof_status = MatitaTypes.Incomplete_proof (proof,goal)}
-
- let goals (_,goals) = goals
-
- let set_goals (status,_) goals = status,goals
-
- let id_tac status =
- apply_tactic (GrafiteAst.IdTac Disambiguate.dummy_floc) status
-
- let mk_tactic tac = tac
-
- let apply_tactic tac = tac
-
- end
-
-module MatitaTacticals = Tacticals.Make(MatitaStatus)
-
-let eval_tactical status tac =
- let rec tactical_of_ast tac =
- match tac with
- | GrafiteAst.Tactic (loc, tactic) -> apply_tactic tactic
- | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
- MatitaTacticals.seq ~tactics:(List.map tactical_of_ast tacticals)
- | GrafiteAst.Do (loc, num, tactical) ->
- MatitaTacticals.do_tactic ~n:num ~tactic:(tactical_of_ast tactical)
- | GrafiteAst.Repeat (loc, tactical) ->
- MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast tactical)
- | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
- MatitaTacticals.thens ~start:(tactical_of_ast tactical)
- ~continuations:(List.map tactical_of_ast tacticals)
- | GrafiteAst.First (loc, tacticals) ->
- MatitaTacticals.first
- ~tactics:(List.map (fun t -> "", tactical_of_ast t) tacticals)
- | GrafiteAst.Try (loc, tactical) ->
- MatitaTacticals.try_tactic ~tactic:(tactical_of_ast tactical)
- | GrafiteAst.Solve (loc, tacticals) ->
- MatitaTacticals.solve_tactics
- ~tactics:(List.map (fun t -> "",tactical_of_ast t) tacticals)