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.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
status, [] (*CSC: TO BE FIXED *)
| GrafiteAst.Set (loc, name, value) -> status, []
(* GrafiteTypes.set_option status name value,[] *)
+ | GrafiteAst.NObj (loc,obj) ->
+ let ty, name =
+ match obj with
+ | CicNotationPt.Theorem (_,name,ty,_) -> ty, name
+ | _ -> 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
+ nlexicon_status [] [] [] (text,prefix_len,ty)
+ in
+ let nmenv, nsubst, nlexicon_status, nbo =
+ GrafiteDisambiguate.disambiguate_nterm (Some nty)
+ 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 =
+ GrafiteTypes.ProofMode { NTactics.gstatus = ninitial_stack;
+ istatus = {
+ NTactics.pstatus =
+ NUri.uri_of_string suri, 0, nmenv, nsubst,
+ (NCic.Constant ([],"",Some nbo,nty,(`Provided,`Definition,`Regular)));
+ lstatus = nlexicon_status} }
+ },
+ []
| GrafiteAst.Obj (loc,obj) ->
let ext,name =
match obj with
let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
{ status with GrafiteTypes.proof_status =
GrafiteTypes.Incomplete_proof
- { GrafiteTypes.proof = initial_proof; stack = initial_stack } },
+ { GrafiteTypes.proof = initial_proof; stack = initial_stack } ;
+ },
[]
| _ ->
if metasenv <> [] then
| GrafiteAst.Tactic (_, None, punct) ->
eval_tactical status
(punctuation_tactical_of_ast (text,prefix_len,punct)),[]
+ | GrafiteAst.NTactic (_(*loc*), tac, punct) ->
+ (match status.GrafiteTypes.ng_status with
+ | 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
+ NTactics.pp_tac_status nstatus;
+ { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, [])
| GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
let status =
eval_tactical status