1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jul 29 17:27:52 2010 +0200
     1.3 @@ -0,0 +1,162 @@
     1.4 +(*  Title:      HOL/Tools/Predicate_Compile/code_prolog.ML
     1.5 +    Author:     Lukas Bulwahn, TU Muenchen
     1.6 +
     1.7 +Prototype of an code generator for logic programming languages (a.k.a. Prolog)
     1.8 +*)
     1.9 +
    1.10 +signature CODE_PROLOG =
    1.11 +sig
    1.12 +  datatype term = Var of string * typ | Cons of string | AppF of string * term list;
    1.13 +  datatype prem = Conj of prem list | NotRel of string * term list | Rel of string * term list | Eq of term * term | NotEq of term * term;
    1.14 +  type clause = ((string * term list) * prem);
    1.15 +  type logic_program = clause list;
    1.16 +
    1.17 +  val generate : Proof.context -> string list -> logic_program
    1.18 +  val write_program : logic_program -> string
    1.19 +  val run : logic_program -> string -> string list -> unit
    1.20 +
    1.21 +end;
    1.22 +
    1.23 +structure Code_Prolog : CODE_PROLOG =
    1.24 +struct
    1.25 +
    1.26 +(* general string functions *)
    1.27 +
    1.28 +val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
    1.29 +val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
    1.30 +
    1.31 +(* internal program representation *)
    1.32 +
    1.33 +datatype term = Var of string * typ | Cons of string | AppF of string * term list;
    1.34 +
    1.35 +datatype prem = Conj of prem list | NotRel of string * term list | Rel of string * term list | Eq of term * term | NotEq of term * term;
    1.36 +
    1.37 +fun dest_Rel (Rel (c, ts)) = (c, ts)
    1.38 + 
    1.39 +type clause = ((string * term list) * prem);
    1.40 +
    1.41 +type logic_program = clause list;
    1.42 +
    1.43 +(* translation from introduction rules to internal representation *)
    1.44 +
    1.45 +(* assuming no clashing *)
    1.46 +fun translate_const c = Long_Name.base_name c
    1.47 +
    1.48 +fun translate_term ctxt t =
    1.49 +  case strip_comb t of
    1.50 +    (Free (v, T), []) => Var (v, T) 
    1.51 +  | (Const (c, _), []) => Cons (translate_const c)
    1.52 +  | (Const (c, _), args) => AppF (translate_const c, map (translate_term ctxt) args)
    1.53 +  | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t)
    1.54 +
    1.55 +
    1.56 +fun translate_literal ctxt t =
    1.57 +  case strip_comb t of
    1.58 +    (Const (@{const_name "op ="}, _), [l, r]) => Eq (pairself (translate_term ctxt) (l, r))
    1.59 +  | (Const (c, _), args) => Rel (translate_const c, map (translate_term ctxt) args)
    1.60 +  | _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t)
    1.61 +
    1.62 +fun NegRel_of (Rel lit) = NotRel lit
    1.63 +  | NegRel_of (Eq eq) = NotEq eq
    1.64 +  
    1.65 +fun translate_prem ctxt t =  
    1.66 +    case try HOLogic.dest_not t of
    1.67 +      SOME t => NegRel_of (translate_literal ctxt t)
    1.68 +    | NONE => translate_literal ctxt t
    1.69 +
    1.70 +fun translate_intros ctxt gr const =
    1.71 +  let
    1.72 +    val intros = Graph.get_node gr const
    1.73 +    val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
    1.74 +    fun translate_intro intro =
    1.75 +      let
    1.76 +        val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro)
    1.77 +        val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems intro) 
    1.78 +        val prems' = Conj (map (translate_prem ctxt') prems)
    1.79 +        val clause = (dest_Rel (translate_literal ctxt' head), prems')
    1.80 +      in clause end
    1.81 +  in map translate_intro intros' end
    1.82 +
    1.83 +fun generate ctxt const =
    1.84 +  let 
    1.85 +     fun strong_conn_of gr keys =
    1.86 +      Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
    1.87 +    val gr = Predicate_Compile_Core.intros_graph_of ctxt
    1.88 +    val scc = strong_conn_of gr const
    1.89 +    val _ = tracing (commas (flat scc))
    1.90 +  in
    1.91 +    maps (translate_intros ctxt gr) (flat scc)
    1.92 +  end
    1.93 +
    1.94 +(* transform logic program *)
    1.95 +
    1.96 +(** ensure groundness of terms before negation **)
    1.97 +
    1.98 +fun add_vars (Var x) vs = insert (op =) x vs
    1.99 +  | add_vars (Cons c) vs = vs
   1.100 +  | add_vars (AppF (f, args)) vs = fold add_vars args vs
   1.101 +
   1.102 +fun string_of_typ (Type (s, Ts)) = Long_Name.base_name s
   1.103 +
   1.104 +fun mk_groundness_prems ts =
   1.105 +  let
   1.106 +    val vars = fold add_vars ts []
   1.107 +    fun mk_ground (v, T) =
   1.108 +      Rel ("ground_" ^ string_of_typ T, [Var (v, T)])
   1.109 +  in
   1.110 +    map mk_ground vars
   1.111 +  end
   1.112 +
   1.113 +fun ensure_groundness_prem (NotRel (c, ts)) = Conj (mk_groundness_prems ts @ [NotRel (c, ts)]) 
   1.114 +  | ensure_groundness_prem (NotEq (l, r)) = Conj (mk_groundness_prems [l, r] @ [NotEq (l, r)])
   1.115 +  | ensure_groundness_prem (Conj ps) = Conj (map ensure_groundness_prem ps)
   1.116 +  | ensure_groundness_prem p = p
   1.117 +
   1.118 +fun ensure_groundness_before_negation p =
   1.119 +  map (apsnd ensure_groundness_prem) p
   1.120 +
   1.121 +(* code printer *)
   1.122 +
   1.123 +fun write_term (Var (v, _)) = first_upper v
   1.124 +  | write_term (Cons c) = first_lower c
   1.125 +  | write_term (AppF (f, args)) = first_lower f ^ "(" ^ space_implode ", " (map write_term args) ^ ")" 
   1.126 +
   1.127 +fun write_rel (pred, args) =
   1.128 +  pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")" 
   1.129 +
   1.130 +fun write_prem (Conj prems) = space_implode ", " (map write_prem prems)
   1.131 +  | write_prem (Rel p) = write_rel p  
   1.132 +  | write_prem (NotRel p) = "not(" ^ write_rel p ^ ")"
   1.133 +  | write_prem (Eq (l, r)) = write_term l ^ " = " ^ write_term r
   1.134 +  | write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r
   1.135 +
   1.136 +fun write_clause (head, prem) =
   1.137 +  write_rel head ^ (if prem = Conj [] then "." else " :- " ^ write_prem prem ^ ".")
   1.138 +
   1.139 +fun write_program p =
   1.140 +  cat_lines (map write_clause p) 
   1.141 +
   1.142 +fun query_first rel vnames =
   1.143 +  "eval :- once("  ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
   1.144 +  "writef('" ^ implode (map (fn v => v ^ " = %w\\n") vnames) ^"', [" ^ space_implode ", " vnames ^ "]).\n"
   1.145 +
   1.146 +val prelude =
   1.147 +  "#!/usr/bin/swipl -q -t main -f\n\n" ^
   1.148 +  ":- style_check(-singleton).\n\n" ^
   1.149 +  "main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
   1.150 +  "main :- halt(1).\n"
   1.151 +  
   1.152 +(* calling external interpreter and getting results *)
   1.153 +
   1.154 +fun run p query_rel vnames =
   1.155 +  let
   1.156 +    val cmd = Path.named_root
   1.157 +    val prog = prelude ^ query_first query_rel vnames ^ write_program p
   1.158 +    val prolog_file = File.tmp_path (Path.basic "prolog_file")
   1.159 +    val _ = File.write prolog_file prog
   1.160 +    val (solution, _) = bash_output ("/usr/bin/swipl -f " ^ File.shell_path prolog_file)
   1.161 +  in
   1.162 +    tracing ("Prolog returns result:\n" ^ solution)
   1.163 +  end
   1.164 +
   1.165 +end;