From 8917ab003a9b7f2abf8e399b5e7ad013b31a2e0e Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 20 Sep 2012 09:41:14 +0200
Subject: Imported Upstream version 0.3

---
 print.ml | 100 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 100 insertions(+)
 create mode 100644 print.ml

(limited to 'print.ml')

diff --git a/print.ml b/print.ml
new file mode 100644
index 0000000..1ceb786
--- /dev/null
+++ b/print.ml
@@ -0,0 +1,100 @@
+(***************************************************************************)
+(*  This is part of aac_tactics, it is distributed under the terms of the  *)
+(*         GNU Lesser General Public License version 3                     *)
+(*              (see file LICENSE for more details)                        *)
+(*                                                                         *)
+(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
+(***************************************************************************)
+
+(* A very basic way to interact with the envs, to choose a possible
+   solution *)
+open Pp
+open Matcher
+type named_env = (Names.name * Terms.t) list
+ 
+
+
+(** {pp_env} prints a substitution mapping names to terms, using the
+provided printer *)
+let pp_env pt  : named_env  -> Pp.std_ppcmds = fun env ->
+  List.fold_left
+    (fun acc (v,t) ->
+       begin match v with
+	 | Names.Name s -> str (Printf.sprintf "%s: " (Names.string_of_id s))
+	 | Names.Anonymous -> str ("_")
+       end
+       ++ pt t ++ str "; " ++ acc
+    ) 
+    (str "")
+    env
+   
+(** {pp_envm} prints a collection of possible environments, and number
+them. This number must remain compatible with the parameters given to
+{!aac_rewrite} *)
+let pp_envm pt : named_env Search_monad.m -> Pp.std_ppcmds = fun m ->
+  let _,s =
+    Search_monad.fold
+      (fun env (n,acc) ->
+	 n+1,  h 0 (str (Printf.sprintf "%i:\t[" n) ++pp_env pt env ++ str "]") ++ fnl () :: acc
+      ) m (0,[])
+  in
+    List.fold_left (fun acc s -> s ++ acc) (str "") (s)
+   
+let trivial_substitution envm =
+  match Search_monad.choose envm with
+    | None -> true			(* assert false *)
+    | Some l -> l=[]
+
+(** {pp_all} prints a collection of possible contexts and related
+possibles substitutions, giving a number to each. This number must
+remain compatible with the parameters of {!aac_rewrite} *)
+let pp_all pt : (int * Terms.t * named_env Search_monad.m) Search_monad.m -> Pp.std_ppcmds = fun m ->
+  let _,s = Search_monad.fold
+    (fun (size,context,envm) (n,acc) -> 
+       let s = str (Printf.sprintf "occurence %i: transitivity through " n) in
+       let s = s ++ pt context ++ str "\n" in
+       let s = if trivial_substitution envm then s else
+	 s ++ str (Printf.sprintf "%i possible(s) substitution(s)" (Search_monad.count envm) )
+	   ++ fnl () ++ pp_envm pt envm 
+       in
+	 n+1, s::acc
+    ) m (0,[]) in
+    List.fold_left (fun acc s -> s ++ str "\n" ++ acc) (str "") (s)
+
+(** The main printing function. {!print} uses the debruijn_env the
+rename the variables, and rebuilds raw Coq terms (for the context, and
+the terms in the environment). In order to do so, it requires the
+information gathered by the {!Theory.Trans} module.*)
+let print rlt ir m (context : Term.rel_context) goal =
+  if Search_monad.count m = 0
+  then
+    (
+      Tacticals.tclFAIL 0  (Pp.str "No subterm modulo AC")  goal
+    )
+  else
+    let _ = Pp.msgnl (Pp.str "All solutions:") in
+    let m = Search_monad.(>>) m
+      (fun (i,t,envm) ->
+	let envm = Search_monad.(>>) envm ( fun env ->
+	  let l = Matcher.Subst.to_list env in
+	  let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in
+	  let l =
+	    List.map (fun (v,t) ->
+	      let (name,body,types) = Term.lookup_rel  v context in
+	      (name,t)
+	    ) l
+	  in
+	  Search_monad.return l
+	) 
+	in
+	Search_monad.return (i,t,envm)
+      )
+    in
+    let m = Search_monad.sort (fun (x,_,_) (y,_,_) -> x -  y) m in
+    let _ = Pp.msgnl
+      (pp_all
+	 (fun t -> Printer.pr_constr (Theory.Trans.raw_constr_of_t ir rlt  context  t) ) m
+      )
+    in
+    Tacticals.tclIDTAC goal
+     
-- 
cgit v1.2.3