From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 27 Mar 2009 12:11:01 +0000 (+0000)
Subject: exec and distribute implemented
X-Git-Tag: make_still_working~4135
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=7718257d24d2f0478810711e5b5a9c6bdded1f8e;p=helm.git

exec and distribute implemented
---

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 4ce980b28..baa7f38a9 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -167,7 +167,37 @@ let skip_tac status =
    { status with gstatus = new_gstatus }
 ;;
 
-let fold_tactic tac status =
+let block_tac l status =
+  List.fold_left (fun status tac -> tac status) status l
+;;
+ 
+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)
+;;
+
+(* Exec and distribute_tac form a retraction pair:
+    1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
+    2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
+         distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
+
+   Note that executing an high tactic on a set of goals may be stronger
+   than executing the same tactic on those goals, but once at a time
+   (e.g. the tactic could perform a global analysis of the set of goals)
+*)
+
+let exec tac (low_status,g) =
+  let stack = [ [0,Open g], [], [], `NoTag ] in
+  let _,_,old_metasenv,_,_ = low_status.pstatus in
+  let status = tac { gstatus = stack ; istatus = low_status } in
+  let _,_,metasenv,_,_ = status.istatus.pstatus in
+  let open_goals, closed_goals = 
+    compare_menv ~past:old_metasenv ~present:metasenv 
+  in
+   status.istatus, open_goals, closed_goals
+;;
+
+let distribute_tac tac status =
   match status.gstatus with
   | [] -> assert false
   | (g, t, k, tag) :: s ->
@@ -201,25 +231,73 @@ 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)
+(* attempt....
+type cic_term = NCic.conjecture
+type ast_term = CicNotationPt.term
+type position = Ctx of NCic.context | Term of cic_term
+
+let relocate (name,ctx,t as term) context =
+  if ctx = context then term else assert false
 ;;
 
+let disambiguate (status : lowtac_status) (t : ast_term)  
+                 (ty : cic_term option) (where : position) =
+ let uri,height,metasenv,subst,obj = status.pstatus in
+ let context = match where with Ctx c -> c | Term (_,c,_) -> c in
+ let expty = 
+   match ty with 
+   | None -> None | Some ty -> let _,_,x = relocate ty context in Some x 
+ in
+ let metasenv, subst, lexicon_status, t = 
+   GrafiteDisambiguate.disambiguate_nterm expty
+    status.lstatus context metasenv subst t 
+ in
+ let new_pstatus = uri,height,metasenv,subst,obj in
+ { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t) 
+;;
+
+let get_goal (status : low_status) (g : int) =
+ let _,_,metasenv,_,_ = status.pstatus in
+ List.assoc goal metasenv
+;;
+
+let return ~orig status = 
+ let _,_,past,_,_ = orig.pstatus in
+ let _,_,present,_,_ = status.pstatus in
+ let open_goals, closed_goals = compare_menv ~past ~present in
+ status, open_goals, closed_goals
+;;
+
+let apply t (status as orig,goal) =
+ let goal = get_goal status goal in
+ let status, t = disambiguate status t goal (Term goal) in
+ let subst, metasenv = 
+   (goal, (name, context, t, gty)):: subst,
+   List.filter(fun (x,_) -> x <> goal) metasenv
+ in
+ return ~orig status
+;;
+
+*)
+
+
 let apply t (status,goal) =
  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 
+   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 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 ("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";
@@ -227,5 +305,5 @@ let apply t (status,goal) =
   { lstatus = lexicon_status; pstatus = new_pstatus }, open_goals, closed_goals
 ;;
 
-let apply_tac t = fold_tactic (apply t) ;;
+let apply_tac t = distribute_tac (apply t) ;;
 
diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 831704924..f9747e824 100644
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -38,7 +38,8 @@ val focus_tac: int list -> tactic
 val unfocus_tac: tactic
 val skip_tac: tactic
 
-val fold_tactic: lowtactic -> tactic
+val distribute_tac: lowtactic -> tactic
+val block_tac: tactic list -> tactic
 
 val apply_tac: tactic_term -> tactic