X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=40a490d6bb5941bf736edbd61532e769f49acf7e;hb=dee331ab42d5d625f32fecc3e70df013c2dd093d;hp=492e5505514bd9ee6561e402e061a7b101a681fa;hpb=b225178112c2c5ef1a717ac7e647d854d94b2e52;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 492e55055..40a490d6b 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -24,7 +24,7 @@ type lowtac_status = {
         lstatus : LexiconEngine.status
 }
 
-type lowtactic = lowtac_status * int -> lowtac_status * int list * int list
+type lowtactic = lowtac_status -> int -> lowtac_status 
 
 type tac_status = {
         gstatus : Continuationals.Stack.t; 
@@ -34,11 +34,17 @@ type tac_status = {
 type tactic = tac_status -> tac_status
 
 type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
+type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
 
 let pp_tac_status status = 
   prerr_endline (NCicPp.ppobj status.istatus.pstatus)
 ;;
 
+let pp_lowtac_status status = 
+  prerr_endline "--------------------------------------------";
+  prerr_endline (NCicPp.ppobj status.pstatus)
+;;
+
 open Continuationals.Stack
 
 let dot_tac status =
@@ -167,7 +173,38 @@ 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_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 =>
+         distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
+    3) tac G = distribute_tac (exec tac) G if  
+       tac = distribute_tac lowtac
+
+   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 status = tac { gstatus = stack ; istatus = low_status } in
+   status.istatus
+;;
+
+let distribute_tac tac status =
   match status.gstatus with
   | [] -> assert false
   | (g, t, k, tag) :: s ->
@@ -184,8 +221,9 @@ let fold_tactic 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
@@ -201,19 +239,286 @@ let fold_tactic 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 context (name,ctx,t as term) =
+  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 apply t (status,goal) =
- let _,_,metasenv, subst,_ = status.pstatus in
- let _,context,gty = List.assoc goal metasenv in
+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 context ty in Some x 
+ in
  let metasenv, subst, lexicon_status, t = 
-   GrafiteDisambiguate.disambiguate_nterm (Some gty) status.lstatus context metasenv subst t 
+   GrafiteDisambiguate.disambiguate_nterm expty
+    status.lstatus context metasenv subst t 
  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], []
+ let new_pstatus = uri,height,metasenv,subst,obj in
+ { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t) 
+;;
+
+let in_scope_tag = "tag:in_scope" ;;
+let out_scope_tag = "tag:out_scope" ;;
+
+let typeof status where t =
+  let _,_,metasenv,subst,_ = status.pstatus in
+  let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
+  let _,_,t = relocate ctx t in
+  let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
+  None, ctx, ty
+;;
+  
+let unify status where a b =
+  let n,h,metasenv,subst,o = status.pstatus in
+  let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
+  let _,_,a = relocate ctx a in
+  let _,_,b = relocate ctx b in
+  let metasenv, subst = 
+    NCicUnification.unify (NCicUnifHint.db ()) metasenv subst ctx a b
+  in
+  { status with pstatus = n,h,metasenv,subst,o }
+;;
+
+let refine status where term expty =
+  let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
+  let nt,_,term = relocate ctx term in
+  let ne, ty = 
+    match expty with None -> None, None 
+    | Some e -> let n,_, e = relocate ctx e in Some n, Some e
+  in
+  let name,height,metasenv,subst,obj = status.pstatus in
+  let db = NCicUnifHint.db () in (* XXX fixme *)
+  let coercion_db = NCicCoercion.db () in
+  let look_for_coercion = NCicCoercion.look_for_coercion coercion_db in
+  let metasenv, subst, t, ty = 
+   NCicRefiner.typeof db ~look_for_coercion metasenv subst ctx term ty
+  in
+  { status with pstatus = (name,height,metasenv,subst,obj) }, 
+  (nt,ctx,t), (ne,ctx,ty)
+;;
+
+let get_goal (status : lowtac_status) (g : int) =
+ let _,_,metasenv,_,_ = status.pstatus in
+ List.assoc g metasenv
+;;
+
+let instantiate status i t =
+ let (goalname, context, _ as ety) = get_goal status i in
+ let status, (_,_,t), (_,_,ty) = refine status (`Term ety) t (Some ety) in
+
+ let name,height,metasenv,subst,obj = status.pstatus in
+ let metasenv = List.filter (fun j,_ -> j <> i) metasenv in
+ let subst = (i, (goalname, context, t, ty)) :: subst in
+ { status with pstatus = (name,height,metasenv,subst,obj) }
 ;;
 
-let apply_tac t = fold_tactic (apply t) ;;
+let mk_meta status ?name where bo_or_ty =
+  let n,h,metasenv,subst,o = status.pstatus in
+  let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
+  match bo_or_ty with
+  | `Decl ty ->
+      let _,_,ty = relocate ctx ty in
+      let metasenv, _, instance, _ = 
+        NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty)
+      in
+      let status = { status with pstatus = n,h,metasenv,subst,o } in
+      status, (None,ctx,instance)
+  | `Def bo ->
+      let _,_,ty = typeof status (`Ctx ctx) bo in
+      let metasenv, metano, instance, _ = 
+        NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty)
+      in
+      let status = { status with pstatus = n,h,metasenv,subst,o } in
+      let status = instantiate status metano bo in
+      status, (None,ctx,instance)
+;;
+
+let select_term low_status (name,context,term) (wanted,path) =
+  let found status ctx t wanted =
+    (* we could lift wanted step-by-step *)
+    try true, unify status (`Ctx ctx) (None,ctx,t) wanted
+    with 
+    | NCicUnification.UnificationFailure _ 
+    | NCicUnification.Uncertain _ -> false, status
+  in
+  let match_term status ctx (wanted : cic_term) t =
+    let rec aux ctx status t =
+      let b, status = found status ctx t wanted in
+      if b then 
+        let status, (_,_,t) = 
+          mk_meta status ~name:in_scope_tag (`Ctx ctx) (`Def (None,ctx,t))
+        in    
+        status, t
+      else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t
+     in 
+       aux ctx status t
+  in 
+  let rec select status ctx pat cic = 
+    match pat, cic with
+    | NCic.LetIn (_,t1,s1,b1), NCic.LetIn (n,t2,s2,b2) ->
+        let status, t = select status ctx t1 t2 in
+        let status, s = select status ctx s1 s2 in
+        let ctx = (n, NCic.Def (s2,t2)) :: ctx in
+        let status, b = select status ctx b1 b2 in
+        status, NCic.LetIn (n,t,s,b)
+    | NCic.Lambda (_,s1,t1), NCic.Lambda (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.Lambda (n,s,t)
+    | 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, x::l)
+             (status,[]) l1 l2
+        in
+        status, NCic.Appl (List.rev l)
+    | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2) ->
+        let status, t = select status ctx t1 t2 in
+        let status, ot = select status ctx ot1 ot2 in
+        let status, pl = 
+           List.fold_left2
+             (fun (status,l) x y -> 
+              let status, x = select status ctx x y in
+              status, x::l)
+             (status,[]) pl1 pl2
+        in
+        status, NCic.Match (u,ot,t,List.rev pl)
+    | NCic.Implicit `Hole, t -> 
+        (match wanted with
+        | Some wanted -> 
+             let status, wanted = disambiguate status wanted None (`Ctx ctx) in
+             match_term status ctx wanted t
+        | None -> match_term status ctx (None,ctx,t) t)
+    | NCic.Implicit _, t -> status, t
+    | _,t -> 
+        fail (lazy ("malformed pattern: " ^ NCicPp.ppterm ~metasenv:[]
+          ~context:[] ~subst:[] pat))
+  in
+  let status, term = select low_status context path term in
+  let term = (name, context, term) in
+  mk_meta status ~name:out_scope_tag (`Ctx context) (`Def term)
+;;
+
+let select ~where status goal = 
+ let name, _, _ as goalty = get_goal 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, instance = 
+   mk_meta status ?name (`Term newgoalty) (`Decl newgoalty) 
+ in
+ instantiate status goal instance
+;;
+
+let select_tac ~where = distribute_tac (select ~where) ;;
+
+let exact t status goal =
+ let goalty = get_goal status goal in
+ let status, t = disambiguate status t (Some goalty) (`Term goalty) in
+ instantiate status goal t
+;;
+
+let exact_tac t = distribute_tac (exact t) ;;
+
+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 ~where ~with_what status goal =
+ let (name,_,_ as goalty) = get_goal 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 (`Term goalty) (n,cctx,bo)  in
+
+ let n,h,metasenv,subst,o = status.pstatus in
+ let subst = out_scope :: subst in
+ let status = { status with pstatus = n,h,metasenv,subst,o } in
+
+ let status, instance = 
+   mk_meta status ?name (`Term newgoalty) (`Decl newgoalty) 
+ in
+ instantiate status goal instance
+;;
+
+let apply t status goal = exact t status goal;;
+
+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_goal status goal in
+       let status, (_,_,w as what) = 
+         disambiguate status what None (`Term goalty) in
+       let _ty_what = typeof status (`Term 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
+;;
 
+let intro_tac name =
+ exact_tac
+  ("",0,(CicNotationPt.Binder (`Lambda,
+   (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)))
+;;