util.rml

(*
    Copyright PELAB, Linkoping University

    This file is part of Open Source Modelica (OSM).

    OSM is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    OSM is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with OpenModelica; if not, write to the Free Software
    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA

*)



(**
 ** file:	 Util.rml
 ** module:      Util
 ** description: Miscellanous RML utilities
 **
 ** RCS: $Id$
 ** 
 ** This module contains various RML utilities *sigh*, mosly 
 ** related to lists.
 ** It is used pretty much everywhere. The difference between this 
 ** module and the ModUtil module is that ModUtil contains modelica 
 ** related utilities. The Util module only contains "low-level" 
 ** rml utilities, for example finding elements in lists.
 ** 
 ** This modules contains many relations that uses 'type variables' in RML.
 ** A type variable is exactly what it sounds like, a type bound to a variable.
 ** It is used for higher order functions, i.e. in RML the possibility to pass a 
 ** "pointer" to a relation into another relation. But it can also be used for 
 ** generic data types, like in  C++ templates.

 ** A type variable in RML is written as 'a
 ** For instance,
 ** relation list_fill ('a,int) => 'a list
 ** the type variable 'a is here used as a generic type for the relation list_fill, 
 ** which returns a list of n elements of a certain type.
 **)

module Util :
  relation if : (bool,'a,'a) => 'a
  relation list_fill: ('a ,int) => 'a list
  relation list_first: 'a list => 'a
  relation list_rest: 'a list => 'a list
  relation list_last: 'a list => 'a	  
  relation list_flatten : 'a list list => 'a list
  relation list_map_0 : ('a list, 'a => ()) => ()
  relation list_map : ('a list, 'a => 'b) => 'b list
  relation list_map__2 : ('a list, 'a => ('b,'c)) => ('b list,'c list)
  relation list_map_1: ('a list, ('a, 'b) => 'c, 'b) => 'c list
  relation list_map_2: ('a list, ('a, 'b,'c) => 'd, 'b,'c) => 'd list 
  relation list_map_2_2: ('a list, ('a, 'b,'c) => ('d,'e), 'b,'c) => ('d * 'e) list
  relation list_fold: ('a list, ('a,'b)=> 'b, 'b) => 'b	  
  relation list_list_map : ('a list list, 'a => 'b) => 'b list list 
  relation list_list_reverse: ('a list list) => 'a list list
  relation list_thread : ('a list, 'a list) => 'a list
  relation list_thread_map : ('a list, 'b list, ('a,'b) => 'c) => 'c list
  relation list_thread_tuple : ('a list, 'b list) => ('a * 'b) list
  relation list_list_thread_tuple : ('a list list, 'b list list) 
	  => ('a * 'b) list list
  relation list_position: (''a, ''a list)  => int
  relation list_getmember: (''a, ''a list) => ''a
  relation list_deletemember: (''a list,''a) => ''a list
  relation list_getmember_p: (''a, ''a list,(''a,''a) => bool ) => ''a
  relation list_replaceat: (''a, int, ''a list) => ''a list 
  relation list_replaceat_with_fill: (''a, int, ''a list,''a) => ''a list 
  relation list_union_elt: (''a , ''a list) => ''a list
  relation list_union_elt_p: (''a , ''a list , (''a, ''a) => bool) 
	  => ''a list 
  relation list_union:  (''a list, ''a list) => ''a list
  relation list_union_p:  (''a list, ''a list, (''a,''a) => bool) => ''a list
  relation list_list_union:  (''a list list) => ''a list 
  relation list_list_union_p:  (''a list list, (''a,''a) => bool) => ''a list 
	  
  relation list_reduce: ('a list, ('a,'a) => 'a) => 'a
	      
  relation tuple2_1 : ('a * 'b) => 'a
  relation tuple2_2 : ('a * 'b) => 'b

  relation split_tuple2_list : ('a * 'b) list => ('a list, 'b list)
  relation string_append_list : string list => string
  relation string_delimit_list : (string list, string) => string
  relation string_replace_char : (string, char, char) => string
  relation string_split_at_char : (string, char) => string list 

  relation bool_and_list: bool list => bool
  relation bool_or_list: bool list => bool
  relation bool_string: bool => string 
  relation string_equal: (string,string) => bool
  relation list_matching : ('a list, 'a => ()) => 'a list

  relation apply_option : ('a option,'a => 'b) => 'b option
  relation list_split : ('a list, int) => ('a list, 'a list)

end

(** relation: list_fill
 ** Returns a list of n elements of type 'a.
 ** For example,
 ** list_fill("foo",3) => ["foo","foo","foo"]
**)
relation list_fill: ('a ,int) => 'a list =

  axiom	list_fill (a,1) => [a]

  rule	int_sub(n,1) => n' &
	list_fill(a,n') => res
	----------------------
	list_fill (a,n) => a::res
end

(** relation: list_first 
 ** Returns the first element of a list
 ** For example,
 ** list_first([3,5,7,11,13]) => 3
 *)
relation list_first: 'a list => 'a =	

  axiom	list_first(x::_) => x
end	  

(** relation: list_rest
 ** Returns the rest of a list.
 ** For example,
 ** list_rest([3,5,7,11,13]) => [5,7,11,13]
 **)
relation list_rest: 'a list => 'a list =
	
  axiom	list_rest (_::x) => x
end

(** relation: list_last
 ** Returns the last element of a list. If the list is the empty list, the relation 
 ** fails.
 ** For example,
 ** list_last([3,5,7,11,13]) => 13
 ** list_last([]) => fail
 **)
relation list_last: 'a list => 'a =

  axiom	list_last [a] => a
	
  rule	list_last(rest) => a
	-----------------
	list_last(_::rest) => a
end

(** relation: list_flatten
 ** Takes a list of lists and flattens it out, producing one list of all 
 ** elements of the sublists.
 ** For example
 ** list_flatten([ [1,2],[3,4,5],[6],[] ]) => [1,2,3,4,5,6]
 **)
relation list_flatten : 'a list list => 'a list =

  axiom	list_flatten [] => []

  rule	list_flatten r => r' &
	list_append(f,r') => l
	-----------------------
	list_flatten f::r => l

end

(** relation: list_map
 ** Takes a list and a relation over the elements of the lists, which is applied
 ** for each element, producing a new list.
 ** For example
 ** list_map([1,2,3], int_string) => [ "1", "2", "3"]
 **)
relation list_map : ('a list, 'a => 'b) => 'b list =
	
  axiom	list_map ([],_) => []

  rule	fn f => f' &
	list_map(r,fn) => r'
	-------------------
	list_map (f::r,fn) => f'::r'
end

(** relation list_map__2
 ** Takes a list and a relation over the elements returning a tuple of two types,
 ** which is applied for each element producing two new lists.
 ** For example
 ** relation split_real_string (real) => (string,string)  returns the string value at 
 ** each side of the decimal point.
 ** list_map__2([1.5,2.01,3.1415], split_real_string) => (["1","2","3"],["5","01","1415"])
**)
relation list_map__2 : ('a list, 'a => ('b,'c)) => ('b list,'c list) =

  axiom	list_map__2 ([],_) => ([],[])

  rule	fn f => (f1',f2') &
	list_map__2(r,fn) => (r1',r2')
	-------------------
	list_map__2 (f::r,fn) => (f1'::r1',f2'::r2')
end


(** relation list_map_1
 ** Takes a list and a relation over the list plus an extra argument sent to the relation.
 ** The relation produces a new value which is used for creating a new list.
 ** For example,
 ** list_map_1([1,2,3],int_add,2) => [3,4,5]
 **)
relation list_map_1: ('a list, ('a, 'b) => 'c, 'b) => 'c list =

  axiom	list_map_1 ([],_,_) => []

  rule	fn (f,extraarg) => f' &
	list_map_1(r,fn,extraarg) => r'
	-------------------
	list_map_1(f::r,fn,extraarg) => f'::r'
end

(** relation list_map_2
 ** Takes a list and a relation and two extra arguments passed to the relation.
 ** The relation produces one new value which is used for creating a new list.
 ** For example,
 ** relation if:(bool,'a,'a) => 'a
 ** list_map_2([true,false,false],1,0,if) => [1,0,0]
 **)
relation list_map_2: ('a list, ('a, 'b,'c) => 'd, 'b,'c) => 'd list =

  axiom	list_map_2 ([],_,_,_) => []

  rule	fn (f,extraarg1,extraarg2) => f' &
	list_map_2(r,fn,extraarg1,extraarg2) => r'
	-------------------
	list_map_2(f::r,fn,extraarg1,extraarg2) => f'::r'
end

(** relation: list_map_2_2
 ** Takes a list and a relation with two extra arguments passed to the relation.
 ** The relation returns a tuple of two values which are used for creating two new lists
 ** For example,
 ** relation foo(int,string,string) => (string,string) concatenates each string with 
 ** itself n times. foo(2,"a",b") => ("aa","bb")
 ** list_map_2_2 ([2,3],foo,"a","b") => [("aa","bb"),("aa","bbb")]
**)
relation list_map_2_2: ('a list, ('a, 'b,'c) => ('d,'e), 'b,'c) => ('d * 'e) list =

  axiom	list_map_2_2 ([],_,_,_) => []

  rule	fn (f,extraarg1,extraarg2) => (f1,f2) &
	list_map_2_2(r,fn,extraarg1,extraarg2) => r'
	-------------------
	list_map_2_2(f::r,fn,extraarg1,extraarg2) => ((f1,f2)::r')
end

(** relation: list_map_0
 ** Takes a list and a relation which does not return a value
 ** The relation is probably a relation with side effects, like print.
 ** For example,
 ** list_map_0(["a","b","c"],print) => ()
 **)
relation list_map_0 : ('a list, 'a => ()) => () =

  axiom	list_map_0 ([],_) => ()

  rule	fn (f) => () &
	list_map_0(r,fn) => ()
	-------------------
	list_map_0(f::r,fn) => ()
end

(** relation: list_list_map 
 ** Takes a list of lists and a relation producing one value.
 ** The relation is applied to each element of the lists resulting
 ** in a new list of lists.
 ** For example,
 ** list_list_map([ [1,2],[3],[4]],int_string) => [ ["1","2"],["3"],["4"] ]
 **)
relation list_list_map : ('a list list, 'a => 'b) => 'b list list =
	
  axiom	list_list_map ([],_) => []

  rule	list_map(f,fn) => f' &
	list_list_map(r,fn) => r'
	-------------------
	list_list_map (f::r,fn) => f'::r'

end
(** relation: list_fold
 ** Takes a list and a relation operating on list elements having an extra argument that is 'updated'
 ** thus returned from the relation. The third argument is the startvalue for the updated value.
 ** list_fold will call the relation for each element in a sequence, updating the startvalue 
 ** For example,
 ** list_fold([1,2,3],int_add,2) =>  8
 ** int_add(1,2) => 3, int_add(2,3) => 5, int_add(3,5) => 8 
**)
relation list_fold: ('a list, ('a,'b)=> 'b, 'b) => 'b =

  axiom	list_fold([],r,b) => b
	
  rule	r(l,b) => b' &
	list_fold(lst,r,b') => b'' 
	--------------------------
	list_fold(l::lst,r,b) => b''
end

(** relation: list_list_reverse
 ** Takes a list of lists and reverses it at both levels, i.e. both the list itself
 ** and each sublist
 ** For example,
 ** list_list_reverse([[1,2],[3,4,5],[6] ]) => [ [6], [5,4,3], [2,1] ]
 **)
relation list_list_reverse: ('a list list) => 'a list list =

  rule	list_map(lsts, list_reverse) => lsts' &
	list_reverse(lsts') => lsts''
	-----------------------
	list_list_reverse(lsts) => lsts''
end

(** relation: list_thread
 ** Takes two lists of the same type and threads them togheter.
 ** For eample,
 ** list_thread([1,2,3],[4,5,6]) => [4,1,5,2,6,3]
 **)
relation list_thread : ('a list, 'a list) => 'a list =

  axiom	list_thread([],[]) => []

  rule	list_thread(ra,rb) => r' &
	let c = fb::r' &
	let d = fa::c
	------------------------
	list_thread(fa::ra,fb::rb) => d

end


(** relation: list_thread_map
 ** Takes two lists and a relation and threads and maps the elements of the two lists
 ** creating a new list.
 ** For example,
 ** list_thread_map([1,2],[3,4],int_add) => [1+3, 2+4]
 **)
relation list_thread_map : ('a list, 'b list, ('a,'b) => 'c) => 'c list =

  axiom	list_thread_map([],[],_) => []

  rule	fn(fa,fb) => fr &
	list_thread_map(ra,rb,fn) => res
	--------------------------------
	list_thread_map(fa::ra,fb::rb,fn) => fr::res
end 

(** relation: list_thread_tuple
 ** Takes two lists and threads the arguments into a list of tuples
 ** consisting of the two element types.
 ** For example,
 ** list_thread_tuple([1,2,3],[true,false,true]) => [(1,true),(2,false),(3,true)]
 **)
relation list_thread_tuple : ('a list, 'b list) => ('a * 'b) list =

  axiom	list_thread_tuple ([],[]) => []

  rule	list_thread_tuple(ra,rb) => r
	-----------------------------
	list_thread_tuple (fa::ra, fb::rb) => ((fa,fb)::r)

end


(** relation: list_list_thread_tuple
 ** Takes two list of lists as arguments and produces a list of lists of a two tuple
 ** of the element types of each list.
 ** For example,
 ** list_list_thread_tuple([[1],[2,3]],[["a"],["b","c"]]) => [ [(1,"a")],[(2,"b"),(3,"c")] ]
 **)
relation list_list_thread_tuple : ('a list list, 'b list list) 
	  => ('a * 'b) list list =

  axiom	list_list_thread_tuple ([],[]) => []

  rule	list_thread_tuple(fa,fb) => f &
	list_list_thread_tuple(ra,rb) => r
	-----------------------------
	list_list_thread_tuple (fa::ra, fb::rb) => f::r

end

(** relation: list_position
 ** Takes a value and a list of values and returns the (first) position
 ** the value has in the list. Position index start at zero, such that list_nth can
 ** be used on the resulting position directly.
 ** For example,
 ** list_position(2,[0,1,2,3]) => 2
 **)
relation list_position =
  rule	list_pos(x, ys, 0) => n
	-----------------------
	list_position(x, ys) => n
end
(** helper relation to list_position **)
relation list_pos =
  rule	x = y
	-----
	list_pos(x, y::ys, i) => i

  rule	not x = y &
	int_add(i, 1) => i' &
	list_pos(x, ys, i') => n
	------------------------
	list_pos(x, y::ys, i) => n
end

(** relation: list_getmember
 ** Takes a value and a list of values and returns the value 
 ** if present in the list. If not present, the relation will fail.
 ** For example,
 ** list_getmember(0,[1,2,3]) => fail
 ** list_getmember(1,[1,2,3]) => 1
 **)
relation list_getmember: (''a, ''a list) => ''a =

  axiom list_getmember(_,[]) => fail

  rule  x = y
	-----
	list_getmember(x,y::ys) => y 
	
  rule	not x = y & 
	list_getmember(x,ys) => res 
	----------------------
	list_getmember(x,y::ys) => res
end 

(** relation: list_deletemember
 ** Takes a list and a value and deletes the first occurence of the value in the list
 ** For example,
 ** list_deletemember([1,2,3,2],2) => [1,3,2]
 **)
relation list_deletemember: (''a list,''a) => ''a list =

  rule	list_position(elt,lst) => pos &
	list_delete(lst,pos) => lst'
	----------------------------
	list_deletemember(lst,elt) => lst'

  axiom	list_deletemember(lst,_) => lst

end

(** relation list_getmember_p
 ** Takes a value and a list of values and a comparison relation over two values.
 ** If the value is present in the list (using the comparison relation returning true)
 ** the value is returned, otherwise the relation fails.
 ** For example,
 ** relation equal_lenght(string,string) returns true if the strings are of same length
 ** list_getmember_p("a",["bb","b","ccc"],equal_length) => "b"
 **)
relation list_getmember_p: (''a, ''a list,(''a,''a) => bool) => ''a =

  axiom list_getmember_p(_,[],p) => fail

  rule  p(x, y) => true
	-----
	list_getmember_p(x,y::ys,p) => y 
	
  rule	p(x, y) => false & 
	list_getmember_p(x,ys,p) => res 
	----------------------
	list_getmember_p(x,y::ys,p) => res
end 

(** relation: list_union_elt
 ** Takes a value and a list of values and inserts the value into the list if 
 ** it is not already in the list.
 ** If it is in the list it is not inserted.
 ** For example,
 ** list_union_elt(1,[2,3]) => [1,2,3]
 ** list_union_elt(0,[0,1,2]) => [0,1,2]
**)
relation list_union_elt: (''a , ''a list) => ''a list =

  rule	list_getmember(x,lst) => _ 
	--------------------------
	list_union_elt(x,lst) => lst

  rule	not list_getmember(x,lst) => _ 
	--------------------------
	list_union_elt(x,lst) => x::lst	
end

(** relation list_union
 ** Takes two lists and returns the union of the two lists, i.e. a list of all elements combined
 ** without duplicates.
 ** For example,
 ** list_union([0,1],[2,1]) => [0,1,2]
**)
relation list_union:  (''a list, ''a list) => ''a list =
	
  axiom	list_union([],res) => res

  rule	list_union_elt(x,lst2) => r1 &
	list_union(xs,r1) => res
	-----------------------
	list_union(x::xs,lst2) => res
end

(** relation: list_list_union
 ** Takes a list of lists and returns the union of the sublists
 ** For example,
 ** list_list_union([[1],[1,2],[3,4],[5]]) => [1,2,3,4,5]
 **)
relation list_list_union:  (''a list list) => ''a list =
  
  axiom	list_list_union([]) => []

  axiom	list_list_union([x]) => x

  rule	list_union(x1,x2) => r1 &
	list_list_union(r1::rest) => res
	-----------------------
	list_list_union(x1::x2::rest) => res
end

(** relation: list_union_elt_p
 ** Takes an elemement and a list and a comparison relation over the two values.
 ** It returns the list with the element inserted if not already present in the
 ** list, according to the comparison relation.
 ** For example,
 ** list_union_elt_p(1,[2,3],int_eq) => [1,2,3]
 **)
relation list_union_elt_p: (''a , ''a list , (''a, ''a) => bool) => ''a list =

  rule	list_getmember_p(x,lst,p) => _ 
	--------------------------
	list_union_elt_p(x,lst,p) => lst

  rule	not list_getmember_p(x,lst,p) => _ 
	--------------------------
	list_union_elt_p(x,lst,p) => x::lst	
end

(** relation: list_union_p
 ** Takes two lists and a comparison relation over two elements of the list.
 ** It returns the union of the two lists, using the comparison relation passed as argument
 ** to determine identity between two elements.
 ** For example
 ** given the relation equal_lenght(string,string) returning true if the strings are of same length
 ** list_union_p(["a","aa"],["b","bbb"],equal_length) => ["a","aa","bbb"]
 **)
relation list_union_p:  (''a list, ''a list, (''a,''a) => bool) => ''a list =
	
  axiom	list_union_p([],res,p) => res

  rule	list_union_elt_p(x,lst2,p) => r1 &
	list_union_p(xs,r1,p) => res
	-----------------------
	list_union_p(x::xs,lst2,p) => res
end

(** relation: list_list_union_p
 ** Takes a list of lists and a comparison relation over two elements of the lists.
 ** It returns the union of all sublists using the comparison relation for identity.
 ** For example,
 ** list_list_union_p([[1],[1,2],[3,4]],int_eq) => [1,2,3,4]
 **)
relation list_list_union_p:  (''a list list, (''a,''a) => bool) => ''a list =
  
  axiom	list_list_union_p([],p) => []

  axiom	list_list_union_p([x],p) => x

  rule	list_union_p(x1,x2,p) => r1 &
	list_list_union_p(r1::rest,p) => res
	------------------------------------
	list_list_union_p(x1::x2::rest,p) => res
end

(** relation: list_replaceat
 ** Takes an element, a position and a list and replaces the value at the given position in 
 ** the list. Position is an integer between 0 and n-1 for a list of n elements
 ** For example,
 ** list_replaceat("A", 2, ["a","b","c"]) => ["a","b","A"]
 **)
relation list_replaceat: (''a, int, ''a list) => ''a list =

  (*axiom list_replaceat(x,-1,[]) => []*)

  axiom	 list_replaceat (x,0,y::ys) => x::ys

  rule	int_ge(n,1) => true & int_sub(n,1) => nn &
	list_replaceat(x,nn,ys) => res
	-----------------------------
	list_replaceat(x,n,y::ys) => y::res

 (* rule	print "-list_replaceat failed\n" 
	-----------------------
	list_replaceat(_,_,_) => fail*)
end

(** relation: list_replaceat_with_fill
 ** Takes 
 ** - an element, 
 ** - a position 
 ** - a list and 
 ** - a fill value 
 ** The relation replaces the value at the given position in the list, if the given position is 
 ** out of range, the fill value is used to padd the list up to that element position and then
 ** insert the value at the position
 ** 
 ** For example,
 ** list_replaceat_withfill("A", 5, ["a","b","c"],"dummy") => ["a","b","c","dummy","A"]
 **)
relation list_replaceat_with_fill: (''a, int, ''a list,''a) => ''a list =

  axiom list_replaceat_with_fill(x,0,[],fillv) => [x]
	
  axiom	list_replaceat_with_fill (x,0,y::ys,fillv) => x::ys
	
  axiom	list_replaceat_with_fill(x,1,[],fillv) => [fillv,x]
	
  rule	int_gt(numfills,1) => true &
	int_sub(numfills,1) => numfills' &
	list_fill(fillv,numfills') => res &
	list_append(res,[x]) => res'
	---------------------------------
	list_replaceat_with_fill(x,numfills,[],fillv) => res'

  rule	int_ge(n,1) => true & int_sub(n,1) => nn &
	list_replaceat_with_fill(x,nn,ys,fillv) => res
	----------------------------------------------
	list_replaceat_with_fill(x,n,y::ys,fillv) => y::res

  rule	print "-list_replaceat_with_fill failed row: " & int_string p => pos &
	print pos & print "\n" 
	----------------------
	list_replaceat_with_fill(_,p,_,_) => fail
end


(** relation: list_reduce
 ** Takes a list and a relation operating on two elements of the list.
 ** The relation performs a reduction of the lists to a single value using the relation.
 ** For example,
 ** list_reduce([1,2,3],int_add) => 6
 **)
relation list_reduce: ('a list, ('a,'a) => 'a) => 'a =
  axiom	 list_reduce([e],r) => e

  rule	r(a,b) => res
	-------------
	list_reduce([a,b],r) => res

  rule	r(a,b) => res1 &
	list_reduce(xs,r) => res2 &
	r(res1,res2) => res
	-------------------
	list_reduce(a::b::(xs as _::_),r) => res
end

(** relation: tuple2_1
 ** Takes a tuple of two values and returns the first value.
 ** For example,
 ** tuple2_1(("a",1)) => "a"
 **)
relation tuple2_1 : ('a * 'b) => 'a =
	
  axiom	tuple2_1 ((a,_)) => a

end

(** relation: tuple2_2
 ** Takes a tuple of two values and returns the second value.
 ** For example,
 ** tuple2_2(("a",1)) => 1
 **)
relation tuple2_2 : ('a * 'b) => 'b =
	
  axiom	tuple2_2 ((_,b)) => b

end

(** relation: split_tuple2_list
 ** Takes a list of two-tuples and splits it into two lists.
 ** For example,
 ** split_tuple2_list([("a",1),("b",2),("c",3)]) => (["a","b","c"], [1,2,3])
 **)
relation split_tuple2_list : ('a * 'b) list => ('a list, 'b list) =
  axiom	split_tuple2_list([]) => ([],[])

  rule	split_tuple2_list(rest) => (xs,ys)
	---------------------------------
	split_tuple2_list((x,y)::rest) => (x::xs, y::ys)
end

(** relation: if
 ** Takes a boolean and two values.
 ** Returns the first value (second argument) if the boolean value is true, otherwise 
 ** the second value (third argument) is returned.
 ** For example,
 ** if(true,"a","b") => "a"
 **)
relation if : (bool,'a,'a) => 'a =
	
  axiom	if (true,r,_) => r
  axiom	if (false,_,r) => r

end

(** relation string_append_list
 ** Takes a list of strings and appends them.
 ** For example,
 ** string_append_list(["foo", " ", "bar"]) => "foo bar"
 **)
relation string_append_list : string list => string =
	
  axiom string_append_list [] => ""

  axiom	string_append_list [f] => f

  rule	string_append_list r => r' &
	string_append(f,r') => str
	---------------------------
	string_append_list f::r => str
end

(** relation string_delimit_list
 ** Takes a list of strings and a string delimiter and appends all list elements with
 ** the string delimiter inserted between elements.
 ** For example,
 ** string_delimit_list(["x","y","z"], ", ") => "x, y, z"
 **)
relation string_delimit_list : (string list, string) => string =
	
  axiom string_delimit_list([],_) => ""

  axiom	string_delimit_list([f],delim) => f

  rule	string_delimit_list(r,delim) => str1 &
	string_append(f,delim) => str2 &
	string_append(str2,str1) => str
	---------------------------
	string_delimit_list(f::r,delim) => str
end

(** relation string_replace_char
 ** Takes a string and two chars and replaces the first char to 
 ** second char:
 ** example: string_replace_char("hej.b.c",#".",#"_") => "hej_b_c"
 **)
relation string_replace_char : (string, char, char) => string =

  rule  string_list(str) => strList &
        string_replace_char2(strList,fromChar,toChar) => resList &
        list_string(resList) => res
        -------------------------------
        string_replace_char(str, fromChar, toChar) => res

  rule  print "string_replace_char failed\n"
        ---------------------------------
        string_replace_char(strList,_,_) => strList
  
end

relation string_replace_char2 : (char list, char, char) => char list =

  rule  
        ---------------------------------
        string_replace_char2([],_,_) => []

  rule  firstChar = fromChar &
        string_replace_char2(rest,fromChar,toChar) => res
        ---------------------------------
        string_replace_char2(firstChar::rest,fromChar,toChar) => toChar::res

  rule  not firstChar = fromChar &
        string_replace_char2(rest,fromChar,toChar) => res
        ---------------------------------
        string_replace_char2(firstChar::rest,fromChar,toChar) => firstChar::res

  rule  print "string_replace_char2 failed\n"
        ---------------------------------
        string_replace_char2(strList,_,_) => strList

end

 
(** relation string_split_at_char
 ** Takes a string and a char and split the string at the char
 ** example: string_split_at_char("hej.b.c",#".") => ["hej,"b","c"]
 **)      
relation string_split_at_char : (string, char) => string list =
 
  rule  string_list(str) => chrList &
        string_split_at_char2(chrList,chr,[]) => stringList
        (*list_string(resList) => res*)
        -------------------------------
        string_split_at_char(str, chr) => stringList

  rule  print "string_split_at_char failed\n"
        ---------------------------------
        string_split_at_char(strList,_) => [strList]
end

relation string_split_at_char2 : (char list, char,char list) => string list  =

  rule  list_string(chr_rest) => res
        ---------------------------------
        string_split_at_char2([],_,chr_rest) => [res]

  rule  firstChar = chr &
        list_string(chr_rest) => res &
        string_split_at_char2(rest,chr,[]) => res_str
        ---------------------------------
        string_split_at_char2(firstChar::rest,chr,chr_rest) => res::res_str

  rule  not firstChar = chr &
        string_split_at_char2(rest,chr,firstChar::chr_rest) => res
        ---------------------------------
        string_split_at_char2(firstChar::rest,chr,chr_rest) => res

  rule  print "string_split_at_char2 failed\n"
        ---------------------------------
        string_split_at_char2(strList,_,_) => fail

end

(** relation bool_or_list
 ** Takes a list of boolean values and applies the boolean 'or' operator  to the list elements
 ** For example
 ** bool_or_list([true,false,false]) => true
 ** bool_or_list([false,false,false]) => false
 **)
relation bool_or_list: bool list => bool =

  axiom	bool_or_list([b]) => b

  rule	b = true
	---------------------
  	bool_or_list(b::rest) => true

  rule	b = false &
	bool_or_list(rest) => res
	---------------------
  	bool_or_list(b::rest) => res
end

(** relation: bool_and_list
 ** Takes a list of boolean values and applies the boolean 'and' operator on the elements
 ** For example,
 ** bool_and_list([true, true]) => true
 ** bool_and_list([false,false,true]) => false
 **)
relation bool_and_list: bool list => bool =

  axiom	bool_and_list([b]) => b

  rule	b = false
	---------------------
  	bool_and_list(b::rest) => false

  rule	b = true &
	bool_and_list(rest) => res
	---------------------
  	bool_and_list(b::rest) => res
end



(** relation: bool_string
 ** Takes a boolean value and returns a string representation of the boolean value.
 ** For example,
 ** bool_string(true) => "true"
 **)
relation bool_string: bool => string =
  axiom	bool_string true => "true"
  axiom	bool_string false => "false"
end


(** relation: string_equal
 ** Takes two strings and returns true if the strings are equal
 ** For example,
 ** string_equal("a","a") => true
 **)
relation string_equal: (string,string) => bool =
  rule	a = b
	-----
	string_equal(a,b) => true

  axiom	string_equal(_,_) => false

end

(** relation: list_matching
 ** For example,
 ** Takes a list of values and a matching relation over the values and returns a
 ** sub list of values for which the matching relation succeeds.
 ** For example,
 ** given relation is_numeric(string) => ()  which succeeds if the string is numeric.
 ** list_matching(["foo","1","bar","4"],is_numeric) => ["1","4"]
 **)
relation list_matching: ('a list, 'a => () )  => 'a list =

  axiom	list_matching ([],_) => []

  rule	cond(v) &
	list_matching (vl, cond) => vl'
	-------------------
	list_matching (v::vl, cond) => v::vl'

  rule	not cond(v) &
	list_matching (vl, cond) => vl'
	--------------------------
	list_matching (v::vl, cond) => vl'
end	

(** relation: apply_option
 ** Takes an option value and a relation over the value. It returns in another option value, resulting 
 ** from the application of the relation on the value.
 ** For example,
 ** apply_option(SOME(1), int_string) => SOME("1")
 ** apply_option(NONE, int_string) => NONE
 **)
relation apply_option : ('a option,'a => 'b) => 'b option =

  axiom	apply_option(NONE,_) => NONE 

  rule	rel(a) => b
	-----------
	apply_option( SOME(a),rel) => SOME(b)
end

(** relation: list_split
 ** Takes a list of values and an position value.
 ** The relation returns the list splitted into two lists at the position given as argument.
 ** For example,
 ** list_split([1,2,5,7],2) => ([1,2],[5,7])
 **)
relation list_split : ('a list, int) => ('a list, 'a list) =


  axiom list_split(a,0) => ([],a)
  
  rule	list_length(a) => length &
	int_gt(index,length) => true &
	print "Index out of bounds (greater than list length) in relation list_split\n"
	----------------
	list_split(a,index) => fail  

  rule	int_lt(index,0) => true &
	print "Index out of bounds (less than zero) in relation list_split\n"
	----------------
	list_split(a,index) => fail
	
  rule	int_ge(index,0) => true &
        list_length(a) => length &
	int_le(index,length) => true &	
	list_split2(a,[],index) => (b,c)
	----------------
	list_split(a,index) => (c,b) 
end

(** helper relation to list_split
 **)
relation list_split2 : ('a list, 'a list, int) => ('a list, 'a list) =
	
  rule	int_eq(index,0) => true
	------------------
	list_split2(a,b,index) => (a,b)


  rule	int_sub(index,1) => new_index &
	list_append(b,[a]) => c &
	list_split2(rest,c,new_index) =>(c,d)
	------------------
	list_split2(a::rest,b,index) => (c,d)
	
  rule	print "list_split2 failed\n"
	----------------
	list_split2(_,_,_) => fail 

end