tentative subst-sexpand and change

[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 dd09178c2d70cc27073d183ad73abcd516c0a812..4f6a726dfaf809535fe1c3633d42a9442c017e05 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -233,14 +233,26 @@ 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 =
-  if ctx = context then term else assert false
+  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)  
@@ -259,6 +271,62 @@ let disambiguate (status : lowtac_status) (t : ast_term)
  { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t) 
 ;;
 
+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 get_goal (status : lowtac_status) (g : int) =
  let _,_,metasenv,_,_ = status.pstatus in
  List.assoc g metasenv
@@ -281,13 +349,50 @@ let instantiate status i t =
  { status with pstatus = (name,height,metasenv,subst,obj) }
 ;;
 
+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 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)
+ 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 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
+ in
+ let status, m = mkmeta name status newgoalty in
+ let status = instantiate status goal m in
+ return ~orig status
+;;
 
 let apply t (status,goal) =
  let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in
@@ -314,4 +419,5 @@ let apply t (status,goal) =
 ;;
 
 let apply_tac t = distribute_tac (apply t) ;;
+let change_tac w ww = distribute_tac (change w ww) ;;