X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=ccd02981f2f4f5a5516eb861dbca2e1cae29ca99;hb=a9c8d96d47a5895c99bca2fe93decf464bca62c3;hp=6b341f77c314a581e130e7e9e7f55ad712821334;hpb=7233348f05485c2ee317df9c3407cf1ce7e56927;p=helm.git diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 6b341f77c..ccd02981f 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -336,14 +336,14 @@ let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) = let after = ProofEngineTypes.goals_of_proof proof in let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in let proof, opened_goals = - let uri, metasenv_after_tactic, _subst, t, ty, attrs = proof in + let uri, metasenv_after_tactic, subst, t, ty, attrs = proof in let reordered_metasenv, opened_goals = reorder_metasenv starting_metasenv metasenv_after_refinement metasenv_after_tactic opened goal always_opens_a_goal in - let proof' = uri, reordered_metasenv, _subst, t, ty, attrs in + let proof' = uri, reordered_metasenv, [], t, ty, attrs in proof', opened_goals in let incomplete_proof = @@ -583,6 +583,13 @@ let eval_ng_punct (_text, _prefix_len, punct) = | GrafiteAst.Merge _ -> NTactics.merge_tac ;; +let eval_ng_non_punct (_text, _prefix_len, punct) = + match punct with + | GrafiteAst.Focus (_,l) -> NTactics.focus_tac l + | GrafiteAst.Unfocus _ -> NTactics.unfocus_tac + | GrafiteAst.Skip _ -> NTactics.skip_tac +;; + let eval_ng_tac (text, prefix_len, tac) = match tac with | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) @@ -609,8 +616,6 @@ let eval_ng_tac (text, prefix_len, tac) = NTactics.elim_tac ~what:(text,prefix_len,what) ~where:(text,prefix_len,where) - | GrafiteAst.NEval (_loc, where, reduction) -> - NTactics.eval_tac ~reduction ~where:(text,prefix_len,where) | GrafiteAst.NGeneralize (_loc, where) -> NTactics.generalize_tac ~where:(text,prefix_len,where) | GrafiteAst.NId _ -> (fun x -> x) @@ -618,6 +623,8 @@ let eval_ng_tac (text, prefix_len, tac) = | GrafiteAst.NLetIn (_loc,where,what,name) -> NTactics.letin_tac ~where:(text,prefix_len,where) ~what:(text,prefix_len,what) name + | GrafiteAst.NReduce (_loc, reduction, where) -> + NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where) | GrafiteAst.NRewrite (_loc,dir,what,where) -> NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what) ~where:(text,prefix_len,where) @@ -758,12 +765,24 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status else let obj = prerr_endline "CSC: here we should fix the height!!!"; - uri,height,[],[],NTacStatus.apply_subst_obj subst obj + (uri,height,[],[], + NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst) + obj) in + NCicTypeChecker.typecheck_obj obj; + NCicLibrary.add_obj uri obj; + let objs = NCicElim.mk_elims obj in + let uris = + uri:: + List.map + (fun (uri,_,_,_,_) as obj -> + NCicTypeChecker.typecheck_obj obj; + NCicLibrary.add_obj uri obj; + uri + ) objs in - NCicLibrary.add_obj uri obj; {status with GrafiteTypes.ng_status = - GrafiteTypes.CommandMode lexicon_status },`Old [] + GrafiteTypes.CommandMode lexicon_status },`New uris | _ -> raise (GrafiteTypes.Command_error "Not in proof mode")) | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> Setoids.add_relation id a aeq refl sym trans; @@ -779,25 +798,20 @@ prerr_endline "CSC: here we should fix the height!!!"; GrafiteDisambiguate.disambiguate_nobj lexicon_status ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in let uri,height,nmenv,nsubst,nobj = obj in + let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in + let status = + { status with + GrafiteTypes.ng_status = + GrafiteTypes.ProofMode + { NTacStatus.gstatus = ninitial_stack; + istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}} + } + in (match nmenv with - [] -> - (* CSC: cut&paste code from NQed *) - let obj = -prerr_endline "CSC: here we should fix the height!!!"; - uri,height,[],[],NTacStatus.apply_subst_obj nsubst nobj - in - NCicLibrary.add_obj uri obj; - {status with - GrafiteTypes.ng_status=GrafiteTypes.CommandMode lexicon_status }, - `Old [] - | _ -> - let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in - { status with - GrafiteTypes.ng_status = - GrafiteTypes.ProofMode - { NTacStatus.gstatus = ninitial_stack; - istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}} - },`Old []) + [] -> + eval_command.ec_go ~disambiguate_command opts status + ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + | _ -> status,`New []) | GrafiteAst.Obj (loc,obj) -> let ext,name = match obj with @@ -888,13 +902,14 @@ prerr_endline "CSC: here we should fix the height!!!"; eval_tactical status (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old [] | GrafiteAst.NTactic (_(*loc*), tac, punct) -> - (match status.GrafiteTypes.ng_status with + (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 NTacStatus.pp_tac_status nstatus; - { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, `Old []) + { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus }, + `New []) | GrafiteAst.NonPunctuationTactical (_, tac, punct) -> let status = eval_tactical status @@ -902,6 +917,15 @@ prerr_endline "CSC: here we should fix the height!!!"; in eval_tactical status (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old [] + | GrafiteAst.NNonPunctuationTactical (_, non_punct, punct) -> + (match status.GrafiteTypes.ng_status with + | GrafiteTypes.CommandMode _ -> assert false + | GrafiteTypes.ProofMode nstatus -> + let nstatus = eval_ng_non_punct (text,prefix_len,non_punct) 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 }, + `New []) | GrafiteAst.Command (_, cmd) -> eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd) | GrafiteAst.Macro (loc, macro) ->