Working version, but positivity check is not on

Author: GuillaumeGen

Makefile

@@ -4,7 +4,7 @@ VERSION = devel
 # Compile with "make Q=" to display the commands that are run.
 Q = @
 
-PKG = -package dedukti -package xml-light
+PKG = -package dedukti -package xml-light -package str
 
 .PHONY: all
 all: sct

src/callgraph.ml

@@ -17,7 +17,7 @@ let pp_index fmt x =
   Format.pp_print_int fmt (int_of_index x)
 
 (** The local result express the result of the termination checker for this symbol *)
-type local_result = SelfLooping of (index list)
+type local_result = SelfLooping of string list
 
 (** The pretty printer for the type [local_result] *)
 let pp_local_result : local_result printer =
@@ -46,57 +46,100 @@ module IMap =
       end)
   end
 
-
-(** A call [{callee; caller; matrix; is_rec}] represents a call to the function symbol with key [callee] by the function symbole with the key [caller].
-    The [matrix] gives the relation between the parameters of the caller and the callee.
-    The coefficient [matrix.(a).(b)] give the relation between the [a]-th parameter of the caller and the [b]-th argument of the callee.
-    [rules] is the list of indexes of rules which lead to this call-matrix in the graph. *)
-type call =
-  { callee      : index      ; (** Key of the function symbol being called. *)
-    caller      : index      ; (** Key of the calling function symbol. *)
-    matrix      : matrix     ; (** Size change matrix of the call. *)
-  }
+module EdgeLabel = struct
+  type t = (string list * Cmp_matrix.t) list
+
+  let pp : t printer =
+    fun fmt l ->
+      Format.fprintf fmt "[%a]"
+        (pp_list ",@." (fun fmt (a,b) -> Cmp_matrix.pp fmt b)) l
+
+  let add_neutral : t = []
+
+  let plus : t -> t -> t =
+    let compare_cmp_matrix (m1 : Cmp_matrix.t) (m2 : Cmp_matrix.t) =
+      assert (m1.h = m2.h);
+      assert (m1.w = m2.w);
+      let res = ref 0 in
+      for i = 0 to m1.h -1 do 
+        for j = 0 to m1.w -1 do
+          if !res = 0
+          then 
+            res := Cmp.(match (m1.tab.(i).(j),m2.tab.(i).(j)) with
+              | Infi, Infi -> 0
+              | Infi, _    -> 1
+              | _   , Infi -> -1
+              | Zero, Zero -> 0
+              | Zero, Min1 -> 1
+              | Min1, Zero -> -1
+              | Min1, Min1 -> 0)
+        done
+      done; !res in
+    fun l1 l2 ->
+      List.sort_uniq
+        (fun (_,a) (_,b) -> compare_cmp_matrix a b) (List.append l1 l2)
+
+  let mult : t -> t -> t =
+    fun l1 l2 ->
+      List.flatten (
+        List.map (
+          fun (r1,x) ->
+            List.map (fun (r2,y) -> (r1@r2,Cmp_matrix.prod x y)) l2
+        ) l1
+      )
+end
+
+module CallGraphAdjMat = Matrix(EdgeLabel)
 
 (** Internal state of the SCT, including the representation of symbols and the call graph. *)
 type call_graph =
   {
     next_index      : index ref             ; (** The index of the next function symbol to be added *)
     symbols         : symbol IMap.t ref     ; (** A map containing every symbols studied *)
-    calls           : call list ref         ; (** The list of every call *)
+    calls           : CallGraphAdjMat.t  ref; (** The adjacence matrix of the call graph *)
   }
 
 (** Create a new graph *)
 let new_graph : unit -> call_graph =
   fun () ->
     let syms = IMap.empty in
-    { next_index = ref 0; symbols = ref syms ; calls = ref [] }
+    {
+      next_index = ref 0;
+      symbols = ref syms;
+      calls = ref (CallGraphAdjMat.new_mat 0)
+    }
 
 let find_name : call_graph -> index -> string =
   fun gr i ->
     (IMap.find i !(gr.symbols)).name
 
+type call = {caller    : index;
+             callee    : index;
+             matrix    : Cmp_matrix.t;
+             rule_name : string}
+
 (** The pretty printer for the type [call]. *)
 let pp_call : call_graph -> call printer=
-  fun gr fmt c ->
+  fun gr fmt cc ->
     let res=ref "" in
-    for i=0 to c.matrix.h -1 do
+    for i=0 to cc.matrix.h -1 do
       res:=!res^"x"^(string_of_int i)^" "
     done;
     Format.fprintf fmt "%s(%s%!) <- %s%!("
-      (find_name gr c.caller)
-      !res (find_name gr c.callee);
-    let jj=Array.length c.matrix.tab in
+      (find_name gr cc.caller)
+      !res (find_name gr cc.callee);
+    let jj=cc.matrix.h in
     if jj>0 then
-      let ii=Array.length c.matrix.tab.(0) in
+      let ii=cc.matrix.w in
       for i = 0 to ii - 1 do
         if i > 0 then Format.fprintf fmt ",";
         let some = ref false in
         for j = 0 to jj - 1 do
-          let c = c.matrix.tab.(j).(i) in
-          if c <> Infi then
+          let c = cc.matrix.tab.(j).(i) in
+          if c <> Cmp.Infi then
             begin
               let sep = if !some then " " else "" in
-              Format.fprintf fmt "%s%s" sep (cmp_to_string c);
+              Format.fprintf fmt "%s%s" sep (Cmp.cmp_to_string c);
               some := true
             end
         done
@@ -110,23 +153,64 @@ let update_result : call_graph -> index -> local_result -> unit =
     let sy = (IMap.find i tbl) in
     sy.result <- res::sy.result
 
-(** Add a new call to the call graph. *)
+(** Compute the transitive closure of a call_graph *)
+let rec trans_clos : call_graph -> unit =
+  fun gr ->
+    let m = !(gr.calls) in
+    let mm = CallGraphAdjMat.sum m (CallGraphAdjMat.prod m m) in
+    if m = mm
+    then ()
+    else (
+      gr.calls := mm;
+      trans_clos gr)
+
+(** Add a new call to the call graph.
+    We maintain the transitive closure computed at each step. *)
 let add_call : call_graph -> call -> unit =
   fun gr cc ->
     Debug.debug D_graph "New call: %a" (pp_call gr) cc;
-    gr.calls := cc :: !(gr.calls)
+    !(gr.calls).tab.(cc.caller).(cc.callee) <-
+      ([cc.rule_name],cc.matrix) :: !(gr.calls).tab.(cc.caller).(cc.callee);
+    trans_clos gr
 
 (** Add a new symb to the call graph *)
 let add_symb : call_graph -> symbol -> unit =
   fun gr sy ->
     gr.symbols := IMap.add !(gr.next_index) sy !(gr.symbols);
-    incr gr.next_index
+    incr gr.next_index;
+    let tab =
+      Array.init !(gr.next_index)
+        (fun i ->
+           Array.init !(gr.next_index)
+             (fun j ->
+                try !(gr.calls).tab.(i).(j)
+                with _ -> []
+             )
+        ) in
+    gr.calls := {h = !(gr.calls).h +1; w = !(gr.calls).w +1; tab}
 
 let graph : call_graph ref = ref (new_graph ())
 
+let initialize : unit -> unit =
+  fun () -> graph := new_graph ()
+        
+exception Success_index  of index
+
+(** [find_rule_key r] will return the key [k] which is mapped to the rule [r] *)
+let find_symbol_key : call_graph -> string ->  index
+  = fun gr s ->
+    try
+      IMap.iter
+        (
+	  fun k x -> if x.name = s then raise (Success_index k)
+        ) !(gr.symbols);
+      raise Not_found
+    with Success_index k -> k
+
 let index_and_arity_of : call_graph -> string -> index*int =
   fun gr s ->
     let symb = !(gr.symbols) in
-    let k,sym = IMap.find_first (fun k -> (IMap.find k symb).name = s) symb in
+    let k = find_symbol_key gr s in
+    let sym = IMap.find k symb in
     k, sym.arity
-    
+         

src/input.ml

@@ -6,40 +6,149 @@ module type Input = sig
   type term
   type pattern
   type typ
+  type rule_name
 
   val dig_in_rhs : term -> (string * term array) list
   val destruct_lhs : pattern -> (string * pattern array)
   val get_arity : typ -> int
-  val compare : pattern -> term -> cmp
+  val compare : pattern -> term -> Cmp.t
+  val rn_to_string : rule_name -> string
 end
 
 module StudyRules = functor (In : Input ) -> struct
 
   (** Declare a symbol to be added in the call graph *)
-  let declare : string -> In.typ -> unit =
-    fun s t ->
+  let declare : call_graph -> string -> In.typ -> unit =
+    fun gr s t ->
       let sym = { name = s; arity = In.get_arity t; result = []} in
-      add_symb !graph sym
+      add_symb gr sym
 
   (** Add the calls associated to a rule in the call graph *)
-  let add_rule : In.pattern -> In.term -> unit =
-    fun p t ->
+  let add_rule : call_graph -> In.rule_name -> In.pattern -> In.term -> unit =
+    fun gr rn p t ->
       let lhs = In.destruct_lhs p in
       let list_rhs = In.dig_in_rhs t in
       let study_call (fun_l, arg_l) (fun_r, arg_r) =
-        let ind_l, ari_l = index_and_arity_of !graph fun_l in
-        let ind_r, ari_r = index_and_arity_of !graph fun_r in
-        let mat = Array.make_matrix ari_l ari_r Infi in
-        for i=0 to min ari_l (Array.length arg_l)
+        let ind_l, h = index_and_arity_of gr fun_l in
+        let ind_r, w = index_and_arity_of gr fun_r in
+        let matrix : Cmp_matrix.t =
+          {h; w; tab = Array.make_matrix h w Cmp.Infi} in
+        for i=0 to (min h (Array.length arg_l)) -1
         do
-          for j=0 to min ari_r (Array.length arg_r)
+          for j=0 to (min w (Array.length arg_r)) -1
           do
-            mat.(i).(j) <- In.compare arg_l.(i) arg_r.(j)
+            matrix.tab.(i).(j) <- In.compare arg_l.(i) arg_r.(j)
           done
         done;
-        let matrix = {w = ari_l; h = ari_r; tab=mat} in
-        add_call !graph {caller = ind_l; callee = ind_r; matrix}
+        add_call gr {caller = ind_l; callee = ind_r; matrix;
+                     rule_name = In.rn_to_string rn }
       in
       List.iter (fun c -> study_call lhs c) list_rhs
 
 end
+
+module Dk = struct
+  type term = Term.term
+  type pattern = Rule.pattern
+  type typ = Term.term
+  type rule_name = Rule.rule_name
+
+  let string_of_name n =
+      (Basic.string_of_mident (Basic.md n))^"."^
+      (Basic.string_of_ident (Basic.id n))
+  
+  let rec dig_in_rhs : term -> (string * term array) list =
+    function
+    | Kind
+    | Type _
+    | DB (_, _, _) -> []
+    | Const (_, f) -> [string_of_name f, [||]]
+    | App (Const(_, f), t1, l) -> (string_of_name f, Array.of_list (t1 :: l)) :: List.concat (List.map dig_in_rhs (t1::l))
+    | App (t0, t1, l) ->  List.concat (List.map dig_in_rhs (t0::t1::l))
+    | Lam (_, _, None, t) -> dig_in_rhs t
+    | Lam (_, _, Some ty, t) -> (dig_in_rhs ty) @ (dig_in_rhs t)
+    | Pi (_, _, t1, t2) -> (dig_in_rhs t1) @ (dig_in_rhs t2)
+              
+  let destruct_lhs : pattern -> (string * pattern array) =
+    function
+    | Pattern (_,f,l) -> (string_of_name f, Array.of_list l)
+    | _ -> failwith "This is not a valid lhs of rule"
+                                
+  let rec get_arity : typ -> int =
+    function
+    | Pi (_, _, _, t) -> 1 + (get_arity t)
+    | _ -> 0
+
+  let compare : pattern -> term -> Cmp.t =
+    (** Compare a term and a pattern, using an int indicating under how many lambdas the comparison occurs *)
+    let rec comparison : int -> term -> pattern -> Cmp.t =
+      fun nb t p ->
+        let rec comp_list : Cmp.t -> pattern list -> term list -> Cmp.t =
+          fun cur lp lt ->
+            match lp,lt with
+            | [], _ | _, [] -> cur
+            | a::l1, b::l2  ->
+              begin
+                match (comparison nb b a), cur with
+	        | _   , Infi -> assert false
+                (* We are sure, that the current state [cur] cannot contain a Infi, else the Infi would be the result of the function and no recursive call would be needed *)
+                | Infi, _    -> Infi
+                | Min1, _    -> comp_list Min1 l1 l2
+      	        | _   , Min1 -> comp_list Min1 l1 l2
+      	        | Zero, Zero -> comp_list Zero l1 l2
+      	      end
+        in
+        match p,t with
+        | Var (_,_,n,_), DB (_,_,m) -> if n+nb=m then Zero else Infi (* Two distinct variables are uncomparable *)
+        | Var (_,_,n,_), App(DB(_,_,m),_,_) -> if n+nb=m then Zero else Infi (* A variable when applied has the same size as if it was not applied *)
+        | Lambda(_,_,Var(_,_,n,_)), DB(_,_,m) -> if n+nb=m+1 then Zero else Infi
+        | Lambda(_,_,Var(_,_,n,_)), App(DB(_,_,m),_,_) -> if n+nb=m+1 then Zero else Infi
+        | Pattern (_,f,lp), App(Const(_,g),t1,lt) when (name_eq f g) ->
+          begin
+	    comp_list Zero lp (t1::lt)
+          end
+        | Pattern (_,_,l),t -> Cmp.minus1 (Cmp.mini (List.map (comparison nb t) l))
+        | Lambda(_,_,pp),Lam(_,_,_,tt) -> comparison nb tt pp
+        | _ -> Infi
+    in fun p t -> comparison 0 t p
+
+
+  let rn_to_string : rule_name -> string =
+    function
+    | Beta -> failwith "Beta should not occur in a rule declaration"
+    | Delta n -> string_of_name n
+    | Gamma(_, n) -> string_of_name n
+end
+
+module DkRules = struct
+  include StudyRules(Dk)
+
+  let rec import : loc -> mident -> unit =
+  fun lc m ->
+      begin
+        let (deps,ctx,ext) = Signature.read_dko lc (string_of_mident m) in
+        let symb (id,_,ty,_) =
+          let cst = (string_of_mident m)^"."^(string_of_ident id) in
+          declare !graph cst ty;
+        in
+        let rule (id,_,ty,rul) =
+          List.iter
+            (fun (r : Rule.rule_infos) ->
+               add_rule !graph r.name (Pattern(dloc,r.cst,r.args)) r.rhs
+            ) rul
+        in
+        List.iter symb ctx;
+        List.iter rule ctx
+      end
+
+  and load_terms : Term.term -> unit =
+    function
+    | Term.Kind 
+    | Term.Type _
+    | Term.DB (_, _, _) -> ()
+    | Term.Const (lc, n) -> import lc (md n)
+    | Term.App (t, u, l) -> List.iter load_terms (t::u::l)
+    | Term.Lam (_, _, Some ty, te) -> load_terms ty; load_terms te
+    | Term.Lam (_, _, None, te) -> load_terms te
+    | Term.Pi (_, _, t1, t2) -> load_terms t1; load_terms t2
+end