status
let add_obj = GrafiteSync.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj
-
+
+let eval_ng_punct (_text, _prefix_len, punct) =
+ match punct with
+ | GrafiteAst.Dot _ -> NTactics.dot_tac
+ | GrafiteAst.Semicolon _ -> fun x -> x
+ | GrafiteAst.Branch _ -> NTactics.branch_tac
+ | GrafiteAst.Shift _ -> NTactics.shift_tac
+ | GrafiteAst.Pos (_,l) -> NTactics.pos_tac l
+ | GrafiteAst.Wildcard _ -> NTactics.wildcard_tac
+ | GrafiteAst.Merge _ -> NTactics.merge_tac
+;;
+
+let eval_ng_tac (text, prefix_len, tac) =
+ match tac with
+ | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t)
+ | GrafiteAst.NCases (_loc, what, where) ->
+ NTactics.cases_tac
+ ~what:(text,prefix_len,what)
+ ~where:(text,prefix_len,where)
+ | GrafiteAst.NCase1 (_loc,n) -> NTactics.case1_tac n
+ | GrafiteAst.NChange (_loc, pat, ww) ->
+ NTactics.change_tac
+ ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww)
+ | GrafiteAst.NElim (_loc, what, where) ->
+ NTactics.elim_tac
+ ~what:(text,prefix_len,what)
+ ~where:(text,prefix_len,where)
+ | GrafiteAst.NId _ -> (fun x -> x)
+ | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+;;
+
let rec eval_command = {ec_go = fun ~disambiguate_command opts status
(text,prefix_len,cmd) ->
let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
| _ -> assert false
in
let suri = "cic:/ng_matita/" ^ name ^ ".def" in
+ let nlexicon_status =
+ match status.GrafiteTypes.ng_status with
+ | GrafiteTypes.ProofMode _ -> assert false
+ | GrafiteTypes.CommandMode ls -> ls
+ in
let nmenv, nsubst, nlexicon_status, nty =
GrafiteDisambiguate.disambiguate_nterm None
- LexiconEngine.initial_status [] [] [] (text,prefix_len,ty)
+ nlexicon_status [] [] [] (text,prefix_len,ty)
in
let nmenv, nsubst, nlexicon_status, nbo =
GrafiteDisambiguate.disambiguate_nterm (Some nty)
- LexiconEngine.initial_status [] nmenv nsubst ("",0,CicNotationPt.Implicit)
+ nlexicon_status [] nmenv nsubst ("",0,CicNotationPt.Implicit)
in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
prerr_endline ("nuovo lemma: " ^ NCicPp.ppmetasenv ~subst:nsubst nmenv);
{ status with
- GrafiteTypes.ng_status = Some { NTactics.gstatus = ninitial_stack;
+ GrafiteTypes.ng_status =
+ GrafiteTypes.ProofMode { NTacStatus.gstatus = ninitial_stack;
istatus = {
- NTactics.pstatus =
+ NTacStatus.pstatus =
NUri.uri_of_string suri, 0, nmenv, nsubst,
(NCic.Constant ([],"",Some nbo,nty,(`Provided,`Definition,`Regular)));
lstatus = nlexicon_status} }
| GrafiteAst.Tactic (_, None, punct) ->
eval_tactical status
(punctuation_tactical_of_ast (text,prefix_len,punct)),[]
- | GrafiteAst.NTactic (_(*loc*), Some (GrafiteAst.NApply (_loc, t)), punct) ->
+ | GrafiteAst.NTactic (_(*loc*), tac, punct) ->
(match status.GrafiteTypes.ng_status with
- | None -> assert false
- | Some status ->
- let nts = NTactics.apply_tac (text,prefix_len,t) status in
- prerr_endline "esco da apply";
- NTactics.pp_tac_status nts;
- (*
- let tac = apply_tactic ~disambiguate_tactic (text,prefix_len,tac) in
- let status = eval_tactical status (tactic_of_ast' tac) in
- eval_tactical status
- (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
- *) assert false)
- | GrafiteAst.NTactic (_, None, _punct) -> assert false (*
- eval_tactical status
- (punctuation_tactical_of_ast (text,prefix_len,punct)),[] *)
+ | GrafiteTypes.CommandMode _ -> assert false
+ | GrafiteTypes.ProofMode nstatus ->
+ let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
+ let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
+ NTacStatus.pp_tac_status nstatus;
+ { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, [])
| GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
let status =
eval_tactical status