New files for spdiff-restructuring

The goal is to split the code into more (smaller) units instead of the
current mess.

Restructuring the code should in the end allow making a Spdiff module
that can be used elsewhere.

Author: jespera

env.ml

@@ -0,0 +1,55 @@
+open Gtree
+
+let mk_env (m, t) = [(m, t)]
+
+let empty_env = ([] : ((string * gtree) list))
+
+(* given env and value t, find the _first_ binding m->t in env and return m
+ * there may be other bindings in env such that m'->t
+ *)
+let rev_lookup env t =
+  let rec loop env = match env with 
+  | [] -> None
+  | (m,t') :: env when t = t' -> Some m
+  | _ :: env -> loop env
+  in
+  loop env 
+
+  
+(* replace subterms of t that are bound in env with the binding metavariable
+   so subterm becomes m if m->subterm is in env
+   assumes that if m1->st & m2->st then m1 = m2
+   i.e. each metavariable denote DIFFERENT subterms
+   so that one can uniquely perform the rev_lookup
+*)
+let rec rev_sub env t =
+  match rev_lookup env t with
+  | Some m -> mkA("meta", m)
+  | None -> (match view t with 
+    | C(ty, ts) -> mkC(ty, 
+                       List.rev (List.fold_left 
+                                (fun acc_ts t -> rev_sub env t :: acc_ts) 
+                                [] ts)
+                      )
+    | _ -> t)
+
+(* replace metavars in t with their corresponding binding in env (if any)
+ *)
+let rec sub env t =
+  if env = [] then t 
+  else
+    let rec loop t' = match view t' with
+      | C (ct, ts) ->
+          mkC(ct, List.rev (
+            List.fold_left (fun b a -> (loop a) :: b) [] ts
+          ))
+      | A ("meta", mvar) -> (try 
+			       List.assoc mvar env with Not_found ->
+				 mkA ("meta", mvar)
+			    )
+      | _ -> t'
+    in
+      loop t
+
+let rev_assoc a l = 
+  fst(List.find (function (m,b) -> b = a) l)

gtree_util.ml

@@ -0,0 +1,44 @@
+open Gtree
+open Env
+
+let metactx = ref 0
+let reset_meta () = metactx := 0
+let inc x = let v = !x in (x := v + 1; v)
+let ref_meta () = inc metactx
+let mkM () = mkA("meta", "X" ^ string_of_int(ref_meta()))
+let meta_name m = match view m with
+  | A("meta", n) -> n
+  | _ -> raise (failwith "trying to fetch metaname of non-meta value")
+
+let make_gmeta name = mkA ("meta", name)
+
+let new_meta env t =
+  let m = "X" ^ string_of_int (ref_meta ()) in
+    [make_gmeta m], [(m,t)]
+let is_meta v = match view v with | A("meta", _) -> true | _ -> false
+
+let merge_terms t1 t2 =
+  let rec loop env t1 t2 = 
+    if t1 == t2 
+    then (t1, env)
+    else match view t1, view t2 with
+      | C(ty1, ts1), C(ty2, ts2) 
+        when ty1 = ty2 && List.length ts1 = List.length ts2
+	      -> let ts1, env' = List.fold_left2 
+	            (fun (acc_ts, env') t1' t2' -> 
+	                let t'', env'' = loop env' t1' t2'
+	                in (t'' :: acc_ts, env'')
+	            ) 
+              ([],env) ts1 ts2
+	         in (mkC(ty1, List.rev ts1), env')
+      | _ -> 
+          (match rev_lookup env (t1, t2) with
+		        | None -> let meta = mkM () in
+                      let metaName = meta_name meta in
+		                  (meta, (metaName, (t1,t2)) :: env)
+		        | Some name -> (mkA ("meta", name), env)
+	        )					
+  in
+    loop [] t1 t2
+
+

spdiff.mli

@@ -0,0 +1,12 @@
+module type Spdiff =
+  sig
+    type term
+    type term_pattern
+    type term_patch
+
+    type changeset
+
+    val get_term_patterns : changeset -> term_pattern list
+    val get_term_patches : changeset -> term_patch list
+  end
+

spdiffimpl.ml

@@ -0,0 +1,52 @@
+open Spdiff
+open Gtree
+
+module SpdiffImpl : Spdiff =
+  struct
+    type term = gtree
+    type term_pattern = gtree
+    type term_patch = (term_pattern * term_pattern) list
+    
+    type changeset = (term * term) list
+    
+    module Term = 
+      struct
+        open Hashcons
+        type t = gtree
+        let compare t1 t2 = 
+          if t1 == t2 then 0
+          else if t1.hkey < t2.hkey then -1 else 1 
+      end
+
+    module TermSet = Set.Make(Term)
+
+    let get_subterms t =
+      let rec loop acc subt = match view subt with
+      | A _ -> TermSet.add subt acc
+      | C(_, ts) -> List.fold_left loop (TermSet.add subt acc) ts in
+      loop TermSet.empty t
+
+    (*
+     * Given a changeset, find the set of term-patterns that occur in all of the
+     * LHS terms.
+     *
+     * The näive approach:
+       * compute all subterms for all LHS terms;
+       * for each subterm, try to anti-unify with all subterms in other
+       * term-pairs
+     *) 
+    let get_term_patterns cset = 
+      let lhs_terms = List.rev_map fst cset in
+      let lhs_subterm_sets = List.rev_map get_subterms lhs_terms in
+      let g subterm acc_term_patterns =
+
+      in
+      let f acc_term_patterns term_set =
+        TermSet.fold g term_set acc_term_patterns 
+      in
+      TermSet.elements (
+        List.fold_left f TermSet.empty lhs_subterm_sets
+      )
+
+    let get_term_patches cset = []
+  end

util.ml

@@ -0,0 +1,41 @@
+let grow
+  stop_grow
+  add_res
+  ext_cur
+  acc cur tail 
+  =
+  let rec loop acc cur tail =
+    match tail with
+    | [] -> add_res cur acc
+    | ls :: tail -> List.fold_left
+        (fun acc y -> 
+          let ext = ext_cur y cur in
+          if stop_grow ext acc
+          then acc
+          else loop acc ext tail
+        )
+        acc ls
+  in
+  loop acc cur tail
+
+let all_seqs all_subterms =
+  if List.length all_subterms = 1
+  then List.map (fun x -> [x]) (List.hd all_subterms)
+  else 
+    let stop ext acc = List.mem ext acc in
+    let add_res cur acc = cur :: acc in
+    let ext_cur elt cur = elt :: cur in
+    let h, t = List.hd all_subterms, List.tl all_subterms in
+    List.fold_left (fun acc x ->
+      grow stop add_res ext_cur acc [x] t) [] h
+
+let all_patterns all_subterm_seqs =
+  if List.length all_subterm_seqs = 1
+  then List.map (fun x -> [x]) (List.hd all_subterm_seqs)
+  else
+    let stop ext acc = List.mem ext acc in
+    let add_res cur acc = cur :: acc in
+    let ext_cur elt cur = elt :: cur in
+    let h, t = List.hd all_subterm_seqs, List.tl all_subterm_seqs in
+    List.fold_left (fun acc x ->
+      grow stop add_res ext_cur acc [x] t) [] h