new apply almost there

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 492e5505514bd9ee6561e402e061a7b101a681fa..4ce980b28e60ca2b14b77397ef9415713b62e7ff 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -201,18 +201,30 @@ let fold_tactic tac status =
        { gstatus = stack; istatus = sn }
 ;;
 
+let compare_menv ~past ~present =
+  List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i past)) present),
+  List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
+;;
 
 let apply t (status,goal) =
- let _,_,metasenv, subst,_ = status.pstatus in
- let _,context,gty = List.assoc goal metasenv in
+ let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in
+ let name,context,gty = List.assoc goal metasenv in
  let metasenv, subst, lexicon_status, t = 
    GrafiteDisambiguate.disambiguate_nterm (Some gty) status.lstatus context metasenv subst t 
  in
+ let subst, metasenv = 
+   (goal, (name, context, t, gty)):: subst,
+   List.filter(fun (x,_) -> x <> goal) metasenv
+ in
+ let open_goals, closed_goals = compare_menv ~past:old_metasenv ~present:metasenv in
+ let new_pstatus = uri,height,metasenv,subst,obj in
+
    prerr_endline ("termine disambiguato: " ^ NCicPp.ppterm ~context ~metasenv ~subst t);
    prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv);
    prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv);
    prerr_endline "fine napply";
-   { status with lstatus = lexicon_status }, [goal], []
+
+  { lstatus = lexicon_status; pstatus = new_pstatus }, open_goals, closed_goals
 ;;
 
 let apply_tac t = fold_tactic (apply t) ;;