src/HOL/Tools/res_clause.ML
changeset 17525 ae5bb6001afb
parent 17422 3b237822985d
child 17745 38b4d8bf2627
equal deleted inserted replaced
17524:42d56a6dec6e 17525:ae5bb6001afb
    68 
    68 
    69 val tvar_prefix = "T_";
    69 val tvar_prefix = "T_";
    70 val tfree_prefix = "t_";
    70 val tfree_prefix = "t_";
    71 
    71 
    72 val clause_prefix = "cls_"; 
    72 val clause_prefix = "cls_"; 
    73 val arclause_prefix = "arcls_" 
    73 val arclause_prefix = "clsarity_" 
    74 val clrelclause_prefix = "relcls_";
    74 val clrelclause_prefix = "clsrel_";
    75 
    75 
    76 val const_prefix = "c_";
    76 val const_prefix = "c_";
    77 val tconst_prefix = "tc_"; 
    77 val tconst_prefix = "tc_"; 
    78 
    78 
    79 val class_prefix = "class_"; 
    79 val class_prefix = "class_"; 
   122 
   122 
   123 val ascii_of = String.translate ascii_of_c;
   123 val ascii_of = String.translate ascii_of_c;
   124 
   124 
   125 end;
   125 end;
   126 
   126 
       
   127 (* convert a list of strings into one single string; surrounded by brackets *)
       
   128 fun paren_pack strings = "(" ^ commas strings ^ ")";
       
   129 
       
   130 fun bracket_pack strings = "[" ^ commas strings ^ "]";
       
   131 
       
   132 
   127 (*Remove the initial ' character from a type variable, if it is present*)
   133 (*Remove the initial ' character from a type variable, if it is present*)
   128 fun trim_type_var s =
   134 fun trim_type_var s =
   129   if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
   135   if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
   130   else error ("trim_type: Malformed type variable encountered: " ^ s);
   136   else error ("trim_type: Malformed type variable encountered: " ^ s);
   131 
   137 
   132 fun ascii_of_indexname (v,0) = ascii_of v
   138 fun ascii_of_indexname (v,0) = ascii_of v
   133   | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i;
   139   | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
   134 
   140 
   135 fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
   141 fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
   136 fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
   142 fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
   137 
   143 
   138 (*Type variables contain _H because the character ' translates to that.*)
   144 (*Type variables contain _H because the character ' translates to that.*)
   285 	  val (ts, funcslist) = ListPair.unzip ts_funcs
   291 	  val (ts, funcslist) = ListPair.unzip ts_funcs
   286 	  val ts' = ResLib.flat_noDup ts
   292 	  val ts' = ResLib.flat_noDup ts
   287 	  val funcs' = ResLib.flat_noDup funcslist
   293 	  val funcs' = ResLib.flat_noDup funcslist
   288 	  val t = make_fixed_type_const a
   294 	  val t = make_fixed_type_const a
   289       in    
   295       in    
   290 	  ((t ^ (ResLib.list_to_string folTyps)),(ts', (t, length Ts)::funcs') )
   296 	  ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs') )
   291       end
   297       end
   292   | type_of (TFree (a, s)) = 
   298   | type_of (TFree (a, s)) = 
   293       let val t = make_fixed_type_var a
   299       let val t = make_fixed_type_var a
   294       in (t, ([((FOLTFree a),s)],[(t,0)]) ) end
   300       in (t, ([((FOLTFree a),s)],[(t,0)]) ) end
   295   | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], []))
   301   | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], []))
   585 			 conclLit: arLit,
   591 			 conclLit: arLit,
   586 			 premLits: arLit list};
   592 			 premLits: arLit list};
   587 
   593 
   588 
   594 
   589 fun get_TVars 0 = []
   595 fun get_TVars 0 = []
   590   | get_TVars n = ("T_" ^ (string_of_int n)) :: get_TVars (n-1);
   596   | get_TVars n = ("T_" ^ (Int.toString n)) :: get_TVars (n-1);
   591 
   597 
   592 
   598 
   593 
   599 
   594 fun pack_sort(_,[])  = raise ARCLAUSE("Empty Sort Found") 
   600 fun pack_sort(_,[])  = raise ARCLAUSE("Empty Sort Found") 
   595   | pack_sort(tvar, [cls]) = [(make_type_class cls, tvar)] 
   601   | pack_sort(tvar, [cls]) = [(make_type_class cls, tvar)] 
   675   | string_of_term (Fun (name,typ,[])) = name
   681   | string_of_term (Fun (name,typ,[])) = name
   676   | string_of_term (Fun (name,typ,terms)) = 
   682   | string_of_term (Fun (name,typ,terms)) = 
   677       let val terms' = map string_of_term terms
   683       let val terms' = map string_of_term terms
   678       in
   684       in
   679 	  if !keep_types andalso typ<>"" 
   685 	  if !keep_types andalso typ<>"" 
   680 	  then name ^ (ResLib.list_to_string (terms' @ [typ]))
   686 	  then name ^ (paren_pack (terms' @ [typ]))
   681 	  else name ^ (ResLib.list_to_string terms')
   687 	  else name ^ (paren_pack terms')
   682       end;
   688       end;
   683 
   689 
   684 (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
   690 (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
   685 fun string_of_predicate (Predicate("equal",typ,terms)) = 
   691 fun string_of_predicate (Predicate("equal",typ,terms)) = 
   686       string_of_equality(typ,terms)
   692       string_of_equality(typ,terms)
   687   | string_of_predicate (Predicate(name,_,[])) = name 
   693   | string_of_predicate (Predicate(name,_,[])) = name 
   688   | string_of_predicate (Predicate(name,typ,terms)) = 
   694   | string_of_predicate (Predicate(name,typ,terms)) = 
   689       let val terms_as_strings = map string_of_term terms
   695       let val terms_as_strings = map string_of_term terms
   690       in
   696       in
   691 	  if !keep_types andalso typ<>""
   697 	  if !keep_types andalso typ<>""
   692 	  then name ^ (ResLib.list_to_string  (terms_as_strings @ [typ]))
   698 	  then name ^ (paren_pack (terms_as_strings @ [typ]))
   693 	  else name ^ (ResLib.list_to_string terms_as_strings) 
   699 	  else name ^ (paren_pack terms_as_strings) 
   694       end;
   700       end;
   695 
   701 
   696 
   702 
   697 fun string_of_clausename (cls_id,ax_name) = 
   703 fun string_of_clausename (cls_id,ax_name) = 
   698     clause_prefix ^ ascii_of ax_name ^ "_" ^ string_of_int cls_id;
   704     clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   699 
   705 
   700 fun string_of_type_clsname (cls_id,ax_name,idx) = 
   706 fun string_of_type_clsname (cls_id,ax_name,idx) = 
   701     string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (string_of_int idx);
   707     string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   702     
   708     
   703 
   709 
   704 (********************************)
   710 (********************************)
   705 (* Code for producing DFG files *)
   711 (* Code for producing DFG files *)
   706 (********************************)
   712 (********************************)
   794   | string_of_predicate (Predicate(name,_,[])) = name 
   800   | string_of_predicate (Predicate(name,_,[])) = name 
   795   | string_of_predicate (Predicate(name,typ,terms)) = 
   801   | string_of_predicate (Predicate(name,typ,terms)) = 
   796       let val terms_as_strings = map string_of_term terms
   802       let val terms_as_strings = map string_of_term terms
   797       in
   803       in
   798 	  if !keep_types andalso typ<>""
   804 	  if !keep_types andalso typ<>""
   799 	  then name ^ (ResLib.list_to_string  (terms_as_strings @ [typ]))
   805 	  then name ^ (paren_pack  (terms_as_strings @ [typ]))
   800 	  else name ^ (ResLib.list_to_string terms_as_strings) 
   806 	  else name ^ (paren_pack terms_as_strings) 
   801       end;
   807       end;
   802 
   808 
   803 
   809 
   804 fun concat_with sep []  = ""
   810 fun concat_with sep []  = ""
   805   | concat_with sep [x] = "(" ^ x ^ ")"
   811   | concat_with sep [x] = "(" ^ x ^ ")"
   824               (typ_clss (k+1) tfrees)
   830               (typ_clss (k+1) tfrees)
   825     in 
   831     in 
   826 	cls_str :: (typ_clss 0 tfree_lits)
   832 	cls_str :: (typ_clss 0 tfree_lits)
   827     end;
   833     end;
   828 
   834 
   829 fun string_of_arity (name, num) =  name ^ "," ^ (string_of_int num) 
   835 fun string_of_arity (name, num) =  name ^ "," ^ (Int.toString num) 
   830 
   836 
   831 fun string_of_preds preds = 
   837 fun string_of_preds preds = 
   832   "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n";
   838   "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n";
   833 
   839 
   834 fun string_of_funcs funcs =
   840 fun string_of_funcs funcs =
   922 	 clauses2dfg clss probname axioms' conjectures' funcs' preds' 
   928 	 clauses2dfg clss probname axioms' conjectures' funcs' preds' 
   923      end;
   929      end;
   924 
   930 
   925 
   931 
   926 fun string_of_arClauseID (ArityClause arcls) =
   932 fun string_of_arClauseID (ArityClause arcls) =
   927     arclause_prefix ^ string_of_int(#clause_id arcls);
   933     arclause_prefix ^ Int.toString(#clause_id arcls);
   928 
   934 
   929 fun string_of_arLit (TConsLit(b,(c,t,args))) =
   935 fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls);
   930     let val pol = if b then "++" else "--"
   936 
   931 	val arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args)
   937 (*FIXME!!! currently is TPTP format!*)
   932     in 
   938 fun dfg_of_arLit (TConsLit(b,(c,t,args))) =
   933 	pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
   939       let val pol = if b then "++" else "--"
   934     end
   940 	  val arg_strs = (case args of [] => "" | _ => paren_pack args)
   935   | string_of_arLit (TVarLit(b,(c,str))) =
   941       in 
   936     let val pol = if b then "++" else "--"
   942 	  pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
   937     in
   943       end
   938 	pol ^ c ^ "(" ^ str ^ ")"
   944   | dfg_of_arLit (TVarLit(b,(c,str))) =
   939     end;
   945       let val pol = if b then "++" else "--"
       
   946       in
       
   947 	  pol ^ c ^ "(" ^ str ^ ")"
       
   948       end;
   940     
   949     
   941 
   950 
   942 fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls);
   951 fun dfg_of_conclLit (ArityClause arcls) = dfg_of_arLit (#conclLit arcls);
   943      
   952      
   944 
   953 
   945 fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls);
   954 fun dfg_of_premLits (ArityClause arcls) = map dfg_of_arLit (#premLits arcls);
   946 		
   955 		
   947 
   956 
   948 fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls);
   957 
   949 
   958 (*FIXME: would this have variables in a forall? *)
   950 (*FIX: would this have variables in a forall? *)
       
   951 
   959 
   952 fun dfg_arity_clause arcls = 
   960 fun dfg_arity_clause arcls = 
   953     let val arcls_id = string_of_arClauseID arcls
   961   let val arcls_id = string_of_arClauseID arcls
   954 	val concl_lit = string_of_conclLit arcls
   962       val concl_lit = dfg_of_conclLit arcls
   955 	val prems_lits = strings_of_premLits arcls
   963       val prems_lits = dfg_of_premLits arcls
   956 	val knd = string_of_arKind arcls
   964       val knd = string_of_arKind arcls
   957 	val all_lits = concl_lit :: prems_lits
   965       val all_lits = concl_lit :: prems_lits
   958     in
   966   in
   959 
   967       "clause( %(" ^ knd ^ ")\n" ^  "or( " ^ (bracket_pack all_lits) ^ ")),\n" ^
   960 	"clause( %(" ^ knd ^ ")\n" ^  "or( " ^ (ResLib.list_to_string' all_lits) ^ ")),\n" ^
   968        arcls_id ^  ")."
   961 	 arcls_id ^  ")."
   969   end;
   962     end;
       
   963 
   970 
   964 
   971 
   965 (********************************)
   972 (********************************)
   966 (* code to produce TPTP files   *)
   973 (* code to produce TPTP files   *)
   967 (********************************)
   974 (********************************)
  1007     let val (lits,tfree_lits) = tptp_type_lits cls 
  1014     let val (lits,tfree_lits) = tptp_type_lits cls 
  1008             (*"lits" includes the typing assumptions (TVars)*)
  1015             (*"lits" includes the typing assumptions (TVars)*)
  1009 	val cls_id = get_clause_id cls
  1016 	val cls_id = get_clause_id cls
  1010 	val ax_name = get_axiomName cls
  1017 	val ax_name = get_axiomName cls
  1011 	val knd = string_of_kind cls
  1018 	val knd = string_of_kind cls
  1012 	val lits_str = ResLib.list_to_string' lits
  1019 	val lits_str = bracket_pack lits
  1013 	val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 			 
  1020 	val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 			 
  1014 	fun typ_clss k [] = []
  1021 	fun typ_clss k [] = []
  1015           | typ_clss k (tfree :: tfrees) = 
  1022           | typ_clss k (tfree :: tfrees) = 
  1016               gen_tptp_type_cls(cls_id,ax_name,knd,tfree,k) :: 
  1023               gen_tptp_type_cls(cls_id,ax_name,knd,tfree,k) :: 
  1017               typ_clss (k+1) tfrees
  1024               typ_clss (k+1) tfrees
  1023     let val (lits,tfree_lits) = tptp_type_lits cls 
  1030     let val (lits,tfree_lits) = tptp_type_lits cls 
  1024             (*"lits" includes the typing assumptions (TVars)*)
  1031             (*"lits" includes the typing assumptions (TVars)*)
  1025 	val cls_id = get_clause_id cls
  1032 	val cls_id = get_clause_id cls
  1026 	val ax_name = get_axiomName cls
  1033 	val ax_name = get_axiomName cls
  1027 	val knd = string_of_kind cls
  1034 	val knd = string_of_kind cls
  1028 	val lits_str = ResLib.list_to_string' lits
  1035 	val lits_str = bracket_pack lits
  1029 	val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
  1036 	val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
  1030     in
  1037     in
  1031 	(cls_str,tfree_lits) 
  1038 	(cls_str,tfree_lits) 
  1032     end;
  1039     end;
  1033 
  1040 
  1037 
  1044 
  1038 val delim = "\n";
  1045 val delim = "\n";
  1039 val tptp_clauses2str = ResLib.list2str_sep delim; 
  1046 val tptp_clauses2str = ResLib.list2str_sep delim; 
  1040      
  1047      
  1041 
  1048 
  1042 fun string_of_arClauseID (ArityClause arcls) =
  1049 fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
  1043   arclause_prefix ^ string_of_int(#clause_id arcls);
  1050       let val pol = if b then "++" else "--"
  1044 
  1051 	  val  arg_strs = (case args of [] => "" | _ => paren_pack args)
  1045 
  1052       in 
  1046 fun string_of_arLit (TConsLit(b,(c,t,args))) =
  1053 	  pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
  1047     let val pol = if b then "++" else "--"
  1054       end
  1048 	val  arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args)
  1055   | tptp_of_arLit (TVarLit(b,(c,str))) =
  1049     in 
  1056       let val pol = if b then "++" else "--"
  1050 	pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
  1057       in
  1051     end
  1058 	  pol ^ c ^ "(" ^ str ^ ")"
  1052   | string_of_arLit (TVarLit(b,(c,str))) =
  1059       end;
  1053     let val pol = if b then "++" else "--"
       
  1054     in
       
  1055 	pol ^ c ^ "(" ^ str ^ ")"
       
  1056     end;
       
  1057     
  1060     
  1058 
  1061 
  1059 fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls);
  1062 fun tptp_of_conclLit (ArityClause arcls) = tptp_of_arLit (#conclLit arcls);
  1060      
  1063      
  1061 fun strings_of_premLits (ArityClause arcls) =
  1064 fun tptp_of_premLits (ArityClause arcls) = map tptp_of_arLit (#premLits arcls);
  1062  map string_of_arLit (#premLits arcls);
       
  1063 		
  1065 		
  1064 
       
  1065 fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls);
       
  1066 
       
  1067 fun tptp_arity_clause arcls = 
  1066 fun tptp_arity_clause arcls = 
  1068     let val arcls_id = string_of_arClauseID arcls
  1067     let val arcls_id = string_of_arClauseID arcls
  1069 	val concl_lit = string_of_conclLit arcls
  1068 	val concl_lit = tptp_of_conclLit arcls
  1070 	val prems_lits = strings_of_premLits arcls
  1069 	val prems_lits = tptp_of_premLits arcls
  1071 	val knd = string_of_arKind arcls
  1070 	val knd = string_of_arKind arcls
  1072 	val all_lits = concl_lit :: prems_lits
  1071 	val all_lits = concl_lit :: prems_lits
  1073     in
  1072     in
  1074 	"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ 
  1073 	"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ 
  1075 	(ResLib.list_to_string' all_lits) ^ ")."
  1074 	(bracket_pack all_lits) ^ ")."
  1076     end;
  1075     end;
  1077 
  1076 
  1078 fun tptp_classrelLits sub sup = 
  1077 fun tptp_classrelLits sub sup = 
  1079     let val tvar = "(T)"
  1078     let val tvar = "(T)"
  1080     in 
  1079     in 
  1082 		  | (SOME supcls) =>  "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]"
  1081 		  | (SOME supcls) =>  "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]"
  1083     end;
  1082     end;
  1084 
  1083 
  1085 
  1084 
  1086 fun tptp_classrelClause (ClassrelClause cls) =
  1085 fun tptp_classrelClause (ClassrelClause cls) =
  1087     let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls)
  1086     let val relcls_id = clrelclause_prefix ^ Int.toString(#clause_id cls)
  1088 	val sub = #subclass cls
  1087 	val sub = #subclass cls
  1089 	val sup = #superclass cls
  1088 	val sup = #superclass cls
  1090 	val lits = tptp_classrelLits sub sup
  1089 	val lits = tptp_classrelLits sub sup
  1091     in
  1090     in
  1092 	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")."
  1091 	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")."