X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=7fa2b48d8bc081f1a6fb3a5566253cd9bc89d7c7;hb=d7f32114f3806b51c2ee483dcb5a86e08d086a72;hp=4f6a726dfaf809535fe1c3633d42a9442c017e05;hpb=bf6f5b964bd4e6c16401a4bfab3c29d6824be22a;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 4f6a726df..7fa2b48d8 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -16,30 +16,8 @@ open Printf
 let debug = true
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
-exception Error of string lazy_t
-let fail msg = raise (Error msg)
-
-type lowtac_status = {
-        pstatus : NCic.obj;
-        lstatus : LexiconEngine.status
-}
-
-type lowtactic = lowtac_status * int -> lowtac_status * int list * int list
-
-type tac_status = {
-        gstatus : Continuationals.Stack.t; 
-        istatus : lowtac_status;
-} 
-
-type tactic = tac_status -> tac_status
-
-type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
-
-let pp_tac_status status = 
-  prerr_endline (NCicPp.ppobj status.istatus.pstatus)
-;;
-
 open Continuationals.Stack
+open NTacStatus
 
 let dot_tac status =
   let new_gstatus = 
@@ -170,12 +148,16 @@ let skip_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)
+
+let compare_statuses ~past ~present =
+ let _,_,past,_,_ = past.pstatus in 
+ let _,_,present,_,_ = present.pstatus in 
+ 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 =>
@@ -188,15 +170,10 @@ let compare_menv ~past ~present =
    (e.g. the tactic could perform a global analysis of the set of goals)
 *)
 
-let exec tac (low_status,g) =
+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
+   status.istatus
 ;;
 
 let distribute_tac tac status =
@@ -216,8 +193,9 @@ let distribute_tac tac status =
                 match switch_of_loc loc with
                 | Closed _ -> fail (lazy "cannot apply to a Closed goal")
                 | Open n -> 
-                   let s, go', gc' = tac (s,n) in
-                   s, (go @- gc') @+ go', gc @+ gc'
+                   let sn = tac s n in
+                   let go', gc' = compare_statuses ~past:s ~present:sn in
+                   sn, (go @- gc') @+ go', gc @+ gc'
             in
             aux s go gc loc_tl
       in
@@ -233,191 +211,121 @@ let distribute_tac tac status =
        { gstatus = stack; istatus = sn }
 ;;
 
-type cic_term = NCic.conjecture
-type ast_term = string * int * CicNotationPt.term
-type position = Ctx of NCic.context | Term of cic_term
 
-
-let relocate (name,ctx,t as term) context =
-  let is_prefix l1 l2 =
-    let rec aux = function
-      | [],[] -> true
-      | x::xs, y::ys -> x=y && aux (xs,ys)
-      | _ -> false
-    in
-      aux (List.rev l1, List.rev l2)
-  in
-  if ctx = context then term else 
-  if is_prefix ctx context then 
-    (name, context, 
-      NCicSubstitution.lift (List.length context - List.length ctx) t)
-  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 
+let select ~where status goal = 
+ let goalty = get_goalty status goal in
+ let (wanted,_,where) = GrafiteDisambiguate.disambiguate_npattern where in
+ let path = 
+   match where with None -> NCic.Implicit `Term | Some where -> where 
  in
- let metasenv, subst, lexicon_status, t = 
-   GrafiteDisambiguate.disambiguate_nterm expty
-    status.lstatus context metasenv subst t 
+ let status, newgoalty = select_term status goalty (wanted,path) in
+ let status, instance = 
+   mk_meta status (ctx_of newgoalty) (`Decl newgoalty) 
  in
- let new_pstatus = uri,height,metasenv,subst,obj in
- { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t) 
+ instantiate status goal instance
 ;;
 
-let select_term low_status (name,context,term) (path, matched) =
-  let eq context (status as old_status) t1 t2 =
-    let _,_,t2 = relocate t2 context in
-    if t2 = t1 then true, status else false, old_status 
-  in
-  let match_term m =
-    let rec aux ctx status t =
-      let b, status = eq ctx status t m in
-      if b then 
-        let n,h,metasenv,subst,o = status.pstatus in
-        let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
-        let metasenv, instance, ty = 
-          NCicMetaSubst.mk_meta ~name:"expanded" metasenv ctx (`WithType ty)
-        in
-        let metasenv, subst = 
-          NCicUnification.unify (NCicUnifHint.db ()) metasenv subst ctx 
-            t instance
-        in
-        let status = { status with pstatus = n,h,metasenv,subst,o } in
-        status, instance
-      else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t
-     in 
-       aux
-  in 
-  let rec select status ctx pat cic = 
-    match pat, cic with
-    | NCic.Prod (_,s1,t1), NCic.Prod (n,s2,t2) ->
-        let status, s = select status ctx s1 s2 in
-        let ctx = (n, NCic.Decl s2) :: ctx in
-        let status, t = select status ctx t1 t2 in
-        status, NCic.Prod (n,s,t)
-    | NCic.Appl l1, NCic.Appl l2 ->
-        let status, l = 
-           List.fold_left2
-             (fun (status,l) x y -> 
-              let status, x = select status ctx x y in
-              status, l @ [x])
-             (status,[]) l1 l2
-        in
-        status, NCic.Appl l
-    | NCic.Implicit `Hole, t -> status, t
-    | NCic.Implicit `Term, t -> 
-        let status, matched = disambiguate status matched None (Ctx ctx) in
-        match_term matched ctx status t
-    | _,t -> status, t
-  in
-  let status, term = select low_status context path term in
-  let _,_,_,subst,_ = status.pstatus in
-  let selections = 
-    HExtlib.filter_map 
-      (function (i,(Some "expanded",c,_,_)) -> Some i | _ -> None) 
-      subst
-  in
-  status, (name, context, term), selections
-;;
+let select_tac ~where = distribute_tac (select ~where) ;;
 
-let get_goal (status : lowtac_status) (g : int) =
- let _,_,metasenv,_,_ = status.pstatus in
- List.assoc g metasenv
+let exact t status goal =
+ let goalty = get_goalty status goal in
+ let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
+ instantiate status goal t
 ;;
 
-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 instantiate status i t =
- let name,height,metasenv,subst,obj = status.pstatus in
- let _, context, ty = List.assoc i metasenv in
- let _,_,t = relocate t context in
- let m = NCic.Meta (i,(0,NCic.Irl (List.length context))) in
- let db = NCicUnifHint.db () in (* XXX fixme *)
- let metasenv, subst = NCicUnification.unify db metasenv subst context m t in
- { status with pstatus = (name,height,metasenv,subst,obj) }
-;;
+let exact_tac t = distribute_tac (exact t) ;;
 
-let mkmeta name status (_,ctx,ty) =
-  let n,h,metasenv,s,o = status.pstatus in
-  let metasenv, instance, _ = 
-    NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty)
-  in
-  let status = { status with pstatus = n,h,metasenv,s,o } in
-  status, (name,ctx,instance)
-;;
-
-let apply t (status as orig, goal) =
- let goalty = get_goal status goal in
- let status, t = disambiguate status t (Some goalty) (Term goalty) in
- let status = instantiate status goal t in
- return ~orig status
+let reopen status =
+ let n,h,metasenv,subst,o = status.pstatus in
+ let subst, newm = 
+   List.partition 
+    (function (_,(Some tag,_,_,_)) -> 
+            tag <> in_scope_tag && tag <> out_scope_tag
+    | _ -> true)
+    subst 
+ in
+ let in_m, out_m = 
+   List.partition
+     (function (_,(Some tag,_,_,_)) -> tag = in_scope_tag | _ -> assert false)
+     newm
+ in
+ let metasenv = List.map (fun (i,(_,c,_,t)) -> i,(None,c,t)) in_m @ metasenv in
+ let in_m = List.map fst in_m in
+ let out_m = match out_m with [i] -> i | _ -> assert false in
+ { status with pstatus = n,h,metasenv,subst,o }, in_m, out_m 
 ;;
 
-let change what (*where*) with_what (status as orig, goal) =
- let (name,_,_ as goalty) = get_goal status goal in
- let status, newgoalty, selections = 
-   select_term status goalty 
-     (NCic.Prod ("_",NCic.Implicit `Hole,NCic.Implicit `Term), what)
+let change ~where ~with_what status goal =
+ let goalty = get_goalty status goal in
+ let (wanted,_,where) = GrafiteDisambiguate.disambiguate_npattern where in
+ let path = 
+   match where with None -> NCic.Implicit `Term | Some where -> where 
  in
+ let status, newgoalty = select_term status goalty (wanted,path) in
+ let status, in_scope, out_scope = reopen status in
+ let status =  List.fold_left (exact with_what) status in_scope in
+
+ let j,(n,cctx,bo,_) = out_scope in
+ let _ = typeof status (ctx_of goalty) (Obj.magic (n,cctx,bo))  in
 
  let n,h,metasenv,subst,o = status.pstatus in
- let subst, newm = 
-   List.partition (fun i,_ -> not (List.mem i selections)) subst 
- in
- let metasenv = List.map (fun (i,(n,c,_,t)) -> i,(n,c,t)) newm @ metasenv in
+ let subst = out_scope :: subst in
  let status = { status with pstatus = n,h,metasenv,subst,o } in
 
- let status =  (* queste sono apply, usa un tatticale! *)
-   List.fold_left 
-     (fun status i -> 
-       let x = get_goal status i in
-       let status, with_what = 
-         disambiguate status with_what (Some x) (Term x) 
-       in
-       instantiate status i with_what) 
-     status selections
+ let status, instance = 
+   mk_meta status (ctx_of newgoalty) (`Decl newgoalty) 
  in
- let status, m = mkmeta name status newgoalty in
- let status = instantiate status goal m in
- return ~orig status
+ instantiate status goal instance
 ;;
 
-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 
- 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
+let apply t status goal = exact t status goal;;
 
-   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";
+let apply_tac t = distribute_tac (apply t) ;;
+let change_tac ~where ~with_what = distribute_tac (change ~where ~with_what) ;;
+
+let elim_tac ~what ~where status =
+ block_tac
+   [ select_tac ~where;
+     distribute_tac (fun status goal ->
+       let goalty = get_goalty status goal in
+       let status, what = 
+         disambiguate status what None (ctx_of goalty) in
+       let _ty_what = typeof status (ctx_of what) what in 
+       (* check inductive... find eliminator *)
+       let w = (*astify what *) CicNotationPt.Ident ("m",None) in
+       let holes = [ 
+         CicNotationPt.Implicit;CicNotationPt.Implicit;CicNotationPt.Implicit]
+       in
+       let eliminator = 
+         CicNotationPt.Appl(CicNotationPt.Ident("nat_ind",None)::holes @ [ w ])
+       in
+       exec (apply_tac ("",0,eliminator)) status goal) ] 
+   status
+;;
 
-  { lstatus = lexicon_status; pstatus = new_pstatus }, open_goals, closed_goals
+let intro_tac name =
+ exact_tac
+  ("",0,(CicNotationPt.Binder (`Lambda,
+   (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)))
 ;;
 
-let apply_tac t = distribute_tac (apply t) ;;
-let change_tac w ww = distribute_tac (change w ww) ;;
+let case ~what status goal =
+ let gty = get_goalty status goal in
+ let status, what = disambiguate status what None (ctx_of gty) in
+ let ty = typeof status (ctx_of what) what in
+ let ref, consno, left, right = analyse_indty status ty in
+ let t =
+  NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1,
+    HExtlib.mk_list (NCic.Implicit `Term) consno)
+ in
+ let ctx = ctx_of gty in
+ let status,t,ty = refine status ctx (mk_cic_term ctx t) None in
+ instantiate status goal t
+;;
 
+let case_tac ~what = distribute_tac (case ~what);;
+
+let case1_tac name =
+ block_tac [ intro_tac name; 
+             case_tac ~what:("",0,CicNotationPt.Ident (name,None)) ]
+;;