1 files changed, 510 insertions, 0 deletions

diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
new file mode 100644
index 0000000..6075b3f
--- /dev/null
+++ b/src/trace/smtForm.ml
@@ -0,0 +1,510 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+open Util
+open SmtMisc
+open CoqTerms
+open Errors
+
+module type ATOM = 
+  sig 
+
+    type t 
+    val index : t -> int
+
+    val equal : t -> t -> bool
+
+    val is_bool_type : t -> bool
+
+  end 
+
+
+type fop =
+  | Ftrue
+  | Ffalse
+  | Fand
+  | For
+  | Fxor
+  | Fimp
+  | Fiff
+  | Fite
+  | Fnot2 of int
+
+type ('a,'f) gen_pform = 
+  | Fatom of 'a
+  | Fapp of fop * 'f array
+
+
+module type FORM =
+  sig 
+    type hatom 
+    type t
+    type pform = (hatom, t) gen_pform
+
+      val pform_true : pform
+      val pform_false : pform
+
+      val equal : t -> t -> bool
+
+      val to_lit : t -> int
+      val index : t -> int
+      val pform : t -> pform
+
+      val neg : t -> t
+      val is_pos : t -> bool
+      val is_neg : t -> bool
+
+      val to_smt : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
+
+      (* Building formula from positive formula *)
+      exception NotWellTyped of pform
+      type reify 
+      val create : unit -> reify 
+      val clear : reify -> unit
+      val get : reify -> pform -> t
+      
+      (** Give a coq term, build the corresponding formula *)  
+      val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+   
+      (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
+      val flatten : reify -> t -> t
+
+      (** Producing Coq terms *) 
+
+      val to_coq : t -> Term.constr
+
+      val pform_tbl : reify -> pform array
+
+      val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
+      val interp_tbl : reify -> Term.constr * Term.constr
+      val nvars : reify -> int 
+      (** Producing a Coq term corresponding to the interpretation 
+          of a formula *)
+      (** [interp_atom] map [hatom] to coq term, it is better if it produce
+          shared terms. *)
+      val interp_to_coq : 
+	  (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t -> 
+	    t -> Term.constr
+  end
+
+module Make (Atom:ATOM) =
+  struct 
+
+    type hatom = Atom.t 
+
+    type pform = (Atom.t, t) gen_pform
+ 
+    and hpform = pform gen_hashed
+	  
+    and t = 
+      | Pos of hpform
+      | Neg of hpform 
+
+    let pform_true = Fapp (Ftrue,[||])
+    let pform_false = Fapp (Ffalse,[||])
+
+    let equal h1 h2 = 
+      match h1, h2 with
+      | Pos hp1, Pos hp2 -> hp1.index == hp2.index
+      | Neg hp1, Neg hp2 -> hp1.index == hp2.index
+      | _, _ -> false
+
+    let index = function
+      | Pos hp -> hp.index
+      | Neg hp -> hp.index
+
+    let to_lit = function
+      | Pos hp -> hp.index * 2
+      | Neg hp -> hp.index * 2 + 1
+
+    let neg = function
+      | Pos hp -> Neg hp
+      | Neg hp -> Pos hp
+	    
+    let is_pos = function
+      | Pos _ -> true
+      | _ -> false
+	    
+    let is_neg = function
+      | Neg _ -> true
+      | _ -> false
+
+    let pform = function
+      | Pos hp -> hp.hval
+      | Neg hp -> hp.hval
+
+
+    let rec to_smt atom_to_smt fmt = function
+      | Pos hp -> to_smt_pform atom_to_smt fmt hp.hval
+      | Neg hp ->
+        Format.fprintf fmt "(not ";
+        to_smt_pform atom_to_smt fmt hp.hval;
+        Format.fprintf fmt ")"
+
+    and to_smt_pform atom_to_smt fmt = function
+      | Fatom a -> atom_to_smt fmt a
+      | Fapp (op,args) -> to_smt_op atom_to_smt fmt op args
+
+    and to_smt_op atom_to_smt fmt op args =
+      let s = match op with
+        | Ftrue -> "true"
+        | Ffalse -> "false"
+        | Fand -> "and"
+        | For -> "or"
+        | Fxor -> "xor"
+        | Fimp -> "=>"
+        | Fiff -> "="
+        | Fite -> "ite"
+        | Fnot2 _ -> "" in
+      let (s1,s2) = if Array.length args = 0 then ("","") else ("(",")") in
+      Format.fprintf fmt "%s%s" s1 s;
+      Array.iter (fun h -> Format.fprintf fmt " "; to_smt atom_to_smt fmt h) args;
+      Format.fprintf fmt "%s" s2
+
+
+    module HashedForm =
+      struct 
+	
+	type t = pform
+	      
+	let equal pf1 pf2 = 
+	  match pf1, pf2 with
+	  | Fatom ha1, Fatom ha2 -> Atom.equal ha1 ha2
+	  | Fapp(op1,args1), Fapp(op2,args2) ->
+	      op1 = op2 && 
+	      Array.length args1 == Array.length args2 &&
+	      (try 
+		for i = 0 to Array.length args1 - 1 do
+		  if not (equal args1.(i) args2.(i)) then raise Not_found 
+		done;
+		true
+	      with Not_found -> false)
+	  | _, _ -> false
+
+	let hash pf = 
+	  match pf with
+	  | Fatom ha1 -> Atom.index ha1 * 2 
+	  | Fapp(op, args) -> 
+	      let hash_args =
+		match Array.length args with
+		| 0 -> 0
+		| 1 -> to_lit args.(0)
+		| 2 -> (to_lit args.(1)) lsl 2 + to_lit args.(0)
+		| _ -> 
+		    (to_lit args.(2)) lsl 4 + (to_lit args.(1)) lsl 2 +
+		      to_lit args.(0) in
+	      (hash_args * 10 + Hashtbl.hash op) * 2 + 1
+		
+      end
+
+    module HashForm = Hashtbl.Make (HashedForm)
+
+    type reify = {
+	mutable count : int;
+                tbl : t HashForm.t 
+      }  
+
+    exception NotWellTyped of pform
+   	
+    let check pf = 
+      match pf with
+      | Fatom ha ->  if not (Atom.is_bool_type ha) then raise (NotWellTyped pf)
+      | Fapp (op, args) ->
+	  match op with
+	  | Ftrue | Ffalse -> 
+	      if Array.length args <> 0 then raise (NotWellTyped pf)
+	  | Fnot2 _ -> 
+	      if Array.length args <> 1 then raise (NotWellTyped pf)
+	  | Fand | For -> ()
+	  | Fxor | Fimp | Fiff ->
+	      if Array.length args <> 2 then raise (NotWellTyped pf)
+	  | Fite ->
+	      if Array.length args <> 3 then raise (NotWellTyped pf)
+
+    let declare reify pf =
+      check pf;
+      let res = Pos {index = reify.count; hval = pf} in
+      HashForm.add reify.tbl pf res;
+      reify.count <- reify.count + 1;
+      res
+
+    let create () =
+      let reify = 
+	{ count = 0; 
+	  tbl =  HashForm.create 17 } in
+      let _ = declare reify pform_true in
+      let _ = declare reify pform_false in
+      reify
+
+    let clear r =
+      r.count <- 0;
+      HashForm.clear r.tbl;
+      let _ = declare r pform_true in
+      let _ = declare r pform_false in
+      ()
+
+    let get reify pf =
+      try HashForm.find reify.tbl pf 
+      with Not_found -> declare reify pf
+
+
+    (** Given a coq term, build the corresponding formula *)  
+    type coq_cst = 
+      | CCtrue
+      | CCfalse
+      | CCnot
+      | CCand
+      | CCor
+      | CCxor
+      | CCimp
+      | CCiff
+      | CCifb
+      | CCunknown
+
+    let op_tbl () =
+      let tbl = Hashtbl.create 29 in
+      let add (c1,c2) = Hashtbl.add tbl (Lazy.force c1) c2 in
+      List.iter add 
+	[
+	 ctrue,CCtrue; cfalse,CCfalse;
+	 candb,CCand; corb,CCor; cxorb,CCxor; cimplb,CCimp; cnegb,CCnot;
+         ceqb,CCiff; cifb,CCifb ];
+      tbl
+
+    let op_tbl = lazy (op_tbl ())
+
+    let empty_args = [||]
+
+    let of_coq atom_of_coq reify c =
+      let op_tbl = Lazy.force op_tbl in
+      let get_cst c = 
+	try Hashtbl.find op_tbl c with Not_found -> CCunknown in
+      let rec mk_hform h =
+	let c, args = Term.decompose_app h in
+	match get_cst c with
+	| CCtrue  -> get reify (Fapp(Ftrue,empty_args))
+	| CCfalse -> get reify (Fapp(Ffalse,empty_args))
+	| CCnot -> mk_fnot 1 args
+	| CCand -> mk_fand [] args
+	| CCor  -> mk_for [] args
+	| CCxor -> op2 (fun l -> Fapp(Fxor,l)) args
+	| CCiff -> op2 (fun l -> Fapp(Fiff,l)) args
+	| CCimp ->
+          (match args with
+            | [b1;b2] ->
+              let l1 = mk_hform b1 in
+              let l2 = mk_hform b2 in
+              get reify (Fapp (Fimp, [|l1;l2|]))
+            | _ -> error "SmtForm.Form.of_coq: wrong number of arguments for implb")
+	| CCifb ->
+	    (* We should also be able to syntaxify if then else *)
+	    begin match args with
+	    | [b1;b2;b3] ->
+		let l1 = mk_hform b1 in
+		let l2 = mk_hform b2 in
+		let l3 = mk_hform b3 in
+		get reify (Fapp(Fite, [|l1;l2;l3|]))
+	    | _ -> error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
+	    end
+	| _ -> 
+	    let a = atom_of_coq  h in
+            get reify (Fatom a)
+
+      and op2 f args =
+	match args with
+	| [b1;b2] ->
+	    let l1 = mk_hform b1 in
+            let l2 = mk_hform b2 in
+            get reify (f [|l1; l2|])
+	| _ ->  error "SmtForm.Form.of_coq: wrong number of arguments"
+	  
+      and mk_fnot i args =
+	match args with
+	| [t] -> 
+	    let c,args = Term.decompose_app t in
+	    if c = Lazy.force cnegb then
+              mk_fnot (i+1) args
+	    else 
+              let q,r = i lsr 1 , i land 1 in
+              let l = mk_hform t in
+              let l = if r = 0 then l else neg l in
+	      if q = 0 then l
+	      else get reify (Fapp(Fnot2 q, [|l|]))
+	| _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
+	  
+      and mk_fand acc args = 
+	match args with
+	| [t1;t2] -> 
+	    let l2 = mk_hform t2 in
+	    let c, args = Term.decompose_app t1 in
+	    if c = Lazy.force candb then
+              mk_fand (l2::acc) args
+	    else 
+	      let l1 = mk_hform t1 in
+	      get reify (Fapp(Fand, Array.of_list  (l1::l2::acc)))
+	| _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for andb" 
+
+      and mk_for acc args = 
+	match args with
+	| [t1;t2] -> 
+	    let l2 = mk_hform t2 in
+	    let c, args = Term.decompose_app t1 in
+	    if c = Lazy.force corb then
+              mk_for (l2::acc) args
+	    else 
+	      let l1 = mk_hform t1 in
+	      get reify (Fapp(For, Array.of_list (l1::l2::acc)))
+	| _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
+
+      let l = mk_hform c in
+      l
+
+    (** Flattening of Fand and For, removing of Fnot2 *)
+    let set_sign f f' =
+      if is_pos f then f' else neg f'
+
+    let rec flatten reify f = 
+      match pform f with
+      | Fatom _ -> f
+      | Fapp(Fnot2 _,args) -> set_sign f (flatten reify args.(0))
+      | Fapp(Fand, args) -> set_sign f (flatten_and reify [] (Array.to_list args))
+      | Fapp(For,args) -> set_sign f (flatten_or reify [] (Array.to_list args))
+      | Fapp(op,args) ->
+          (* TODO change Fimp into For ? *)
+	  set_sign f (get reify (Fapp(op, Array.map (flatten reify) args)))
+
+    and flatten_and reify acc args =
+      match args with
+      | [] -> get reify (Fapp(Fand, Array.of_list (List.rev acc)))
+      | a::args ->
+	  (* TODO change (not For) and (not Fimp) into Fand *)
+	  match pform a with
+	  | Fapp(Fand, args') when is_pos a ->
+	      let args = Array.fold_right (fun a args -> a::args) args' args in
+	      flatten_and reify acc args
+	  | _ -> flatten_and reify (flatten reify a :: acc) args
+
+    and flatten_or reify acc args =
+      (* TODO change Fimp and (not Fand) into For *)
+      match args with
+      | [] -> get reify (Fapp(For, Array.of_list (List.rev acc)))
+      | a::args ->
+	  match pform a with
+	  | Fapp(For, args') when is_pos a ->
+	      let args = Array.fold_right (fun a args -> a::args) args' args in
+	      flatten_or reify acc args
+	  | _ -> flatten_or reify (flatten reify a :: acc) args
+
+    (** Producing Coq terms *) 
+
+    let to_coq hf = mkInt (to_lit hf)
+
+    let args_to_coq args =
+      let cargs = Array.make (Array.length args + 1) (mkInt 0) in
+      Array.iteri (fun i hf -> cargs.(i) <- to_coq hf) args;
+      Term.mkArray (Lazy.force cint, cargs)
+	
+    let pf_to_coq = function
+      | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|]	
+      | Fapp(op,args) ->
+        match op with
+	| Ftrue -> Lazy.force cFtrue
+	| Ffalse -> Lazy.force cFfalse
+	| Fand -> mklApp cFand [| args_to_coq args|]
+	| For  -> mklApp cFor [| args_to_coq args|]
+	| Fimp -> mklApp cFimp [| args_to_coq args|]
+	| Fxor -> mklApp cFxor (Array.map to_coq args)
+	| Fiff -> mklApp cFiff (Array.map to_coq args)
+	| Fite -> mklApp cFite (Array.map to_coq args)
+	| Fnot2 i -> mklApp cFnot2 [|mkInt i; to_coq args.(0)|]
+
+    let pform_tbl reify =
+      let t = Array.make reify.count pform_true in
+      let set _ h =
+	match h with
+	| Pos hp -> t.(hp.index) <- hp.hval
+	| _ -> assert false in
+      HashForm.iter set reify.tbl;
+      t
+
+    let to_array reify dft f =
+      let t = Array.make (reify.count + 1) dft in
+      let set _ h =
+	match h with
+	| Pos hp -> t.(hp.index) <- f hp.hval
+	| _ -> assert false in
+      HashForm.iter set reify.tbl;
+      (reify.count, t)
+
+    let interp_tbl reify =
+      let (i,t) = to_array reify (Lazy.force cFtrue) pf_to_coq in
+      (mkInt i, Term.mkArray (Lazy.force cform, t))
+
+    let nvars reify = reify.count
+    (** Producing a Coq term corresponding to the interpretation of a formula *)
+    (** [interp_atom] map [Atom.t] to coq term, it is better if it produce
+	shared terms. *)
+    let interp_to_coq interp_atom form_tbl f =
+      let rec interp_form f = 
+	let l = to_lit f in
+	try Hashtbl.find form_tbl l 
+	with Not_found ->
+	  if is_neg f then 
+	    let pc = interp_form (neg f) in
+	    let nc = mklApp cnegb [|pc|] in
+	    Hashtbl.add form_tbl l nc;
+	    nc
+	  else
+	    let pc = 
+	      match pform f with
+	      | Fatom a -> interp_atom a
+	      | Fapp(op, args) ->
+		  match op with
+		  | Ftrue -> Lazy.force ctrue
+		  | Ffalse -> Lazy.force cfalse
+		  | Fand -> interp_args candb args
+		  | For -> interp_args corb args
+		  | Fxor -> interp_args cxorb args
+		  | Fimp -> 
+		      let r = ref (interp_form args.(Array.length args - 1)) in
+		      for i = Array.length args - 2 downto 0 do
+			r := mklApp cimplb [|interp_form args.(i); !r|]
+		      done;
+		      !r
+		  | Fiff -> interp_args ceqb args
+		  | Fite -> 
+		      (* TODO with if here *)
+		      mklApp cifb (Array.map interp_form args)
+		  | Fnot2 n -> 
+		      let r = ref (interp_form args.(0)) in
+		      for i = 1 to n do	r := mklApp cnegb [|!r|] done;
+		      !r in 
+	    Hashtbl.add form_tbl l pc;
+	    pc
+      and interp_args op args =
+	let r = ref (interp_form args.(0)) in
+	for i = 1 to Array.length args - 1 do
+	  r := mklApp op [|!r;interp_form args.(i)|] 
+	done;
+	!r in
+      interp_form f
+
+  end
+	
+
+	  
+
+    
+
+