THESE ARE THE ADDENDA TO 
http://ls5-www.cs.uni-dortmund.de/~wirth/p/gr719/come.html

Last_update: 26.01.2000
Author: CP

------------------------------------------------------------------------------

Into LIST:

drop: nat x list -> list

drop removes the first #1 elements from #2.

prefix?: list x list -> bool

prefix? tests whether #1 is a prefix of (or equal to) #2.


------------------------------------------------------------------------------

Into FUNCTION:

rev_apply_to_set : function x set(range) -> set(domain)

rev_apply_to_set works like rev_apply but takes a whole set instead
of a single argument. Thus rev_apply(f,a)=rev_apply_to_set(f,{a}).
Thus, rev_apply_to_set applis the reverse relation of first argument
to its second argument.

domres: set(domain) x function -> function

domres restricts the domain of its second argument to its first argument.


------------------------------------------------------------------------------

Into ANCHOR:

update_location: (location -> location) x anchor -> location

update_location(f,Mkanchor(o,t,att))=Mkanchor(f(o),t,att)


------------------------------------------------------------------------------

Into LINK (resp. the new separated SPECIFIER):

val replace_uri_sp_for_anch_id 
  : uri x uri x set(anchor_id) x specifier -> specifier
(* A reference to uri #1 is replaced with uri #2, 
   provided that the anchor identifier of the specifier is in #3.           *)

replace_uri_li_for_anch_id: uri x uri x set(anchor_id) x link -> link
(* All references in specifiers of the link #4 to uri #1 
   are replaced with uri #2, provided that the anchor identifier 
   of the specifier is in #3.                                               *)


replace_uri_sp_for_anch_id(a',a'',A,s) = Mkspecifier(a'',n) 
<-- s=Mkspecifier(a,n), a=a', n\in A=true

replace_uri_sp_for_anch_id(a',a'',A,s) = s
<-- s=Mkspecifier(a,n), a=/=a'

replace_uri_sp_for_anch_id(a',a'',A,s) = s
<-- s=Mkspecifier(a,n), n\in A=false


replace_uri_li_for_anch_id(a,a',A,Mklink(S,S',t,att)) =
  Mklink(map(replace_uri_sp_for_anch_id(a,a',A),S),
         map(replace_uri_sp_for_anch_id(a,a',A),S'),
         t,
         att)


------------------------------------------------------------------------------

Into HD:

val anchor_justifies_link_as_sourced?
  : document x link x anchor -> bool
(* #3 is an anchor for the document #1 that was found in the 
   sources of the link #2. It is tested whether this anchor
   is a justification for the link being properly sourced in
   the document.                                               *)

val specifier_justifies_link_as_sourced?  
  : document x uri function(anchor_id,anchor) x link x specifier -> bool
(* #5 is a specifier that was found in the sources of the link #4.
   #1 is a document with uri #2 and anchor-tabel #3.
   It is tested whether this specifier is a justification for the
   link being properly sourced in the document. *) 

anchor_justifies_link_as_sourced? : document x link x anchor -> bool
(* #3 is an anchor for the document #1 that was found in the 
   sources of the link #2. It is tested whether this anchor
   is a justification for the link being properly sourced in
   the document.                                               *)

anchor_justifies_link_as_sourced?(d,l,c) = true 
<-- get_type(c)=type_c, type_c=/=Target, get_type(l)=Uni(Replace,act)

anchor_justifies_link_as_sourced?(d,l,c) = true 
<-- get_type(c)=type_c, type_c=/=Target, get_type(l)=Uni(New_window,act)

anchor_justifies_link_as_sourced?(d,l,c) = true
<-- get_type(c)=type_c, type_c=/=Target, get_type(l)=Uni(Embed,User),
    embed_link_ok?(location(c)) = true

anchor_justifies_link_as_sourced?(d,l,c) = true
<-- get_type(c)=type_c, type_c=/=Target, get_type(l)=Uni(Embed,Auto),
    embed_link_ok?(location(c)) = true, |get_target(l)| = 1

anchor_justifies_link_as_sourced?(d,l,c) = true
<-- get_type(c)=type_c, type_c=/=Target, get_type(l)=Bi, type_c=Label

anchor_justifies_link_as_sourced?(d,l,c) = false
<-- get_type(c)=type_c, type_c=Target  

anchor_justifies_link_as_sourced?(d,l,c) = false
<-- get_type(c)=type_c, get_type(l)=Bi, type_c=/=Label

anchor_justifies_link_as_sourced?(d,l,c) = false 
<-- get_type(c)=type_c, get_type(l)=Uni(Embed,act),
    embed_link_ok?(location(c)) = false

anchor_justifies_link_as_sourced?(d,l,c) = false
<-- get_type(c)=type_c, get_type(l)=Uni(Embed,Auto), |get_target(l)| =/= 1


specifier_justifies_link_as_sourced?(d,uri,A,l,s) 
= anchor_justifies_link_as_sourced?(d,l,get_anchor(anch_id,A))
<-- get_uri(s)=uri, get_id(s)=anch_id, anch_id\in dom(A)=true

specifier_justifies_link_as_sourced?(d,uri,A,l,s) = false
<-- get_uri(s)=/=uri

specifier_justifies_link_as_sourced?(d,uri,A,l,s) = false
<-- get_id(s)=anch_id, anch_id\in dom(A)=false


link_is_sourced?(d,uri,A,l) =
  exists(specifier_justifies_link_as_sourced?(d,uri,A,l), 
         get_source(l))


add_link(l,Mkhd(d,A,L,att,a)) = Mkhd(d,A,insert(l,L),att,a)
<-- link_is_sourced?(d,embed(a),A,l)=true



------------------------------------------------------------------------------

Into PAGE:

get_locations: page -> set(page_location)
(* Returns all locations of #1.                                             *)

get_sub_locations: nat x list(page) -> set(page_location)
(* Helps get_locations.                                                     *)

contains_at_p: page x page x page_location -> bool
(* tests whether #1 contains #2 at location #3.                             *)

contains_p: page x page -> bool
(* test whether #1 contains #2.                                             *)


get_locations p = {[]} 
<-- atomic?(p)=true

get_locations p = {[]} \cup get_sub_locations(1,get_pages(p))
<-- atomic?(p)=false

get_sub_locations(n,[]   ) = []

get_sub_locations(n,p::pl) = 
   map((fn oc => n :: oc), 
       list_locations(p))
   \cup
   list_sub_locations(n+1,pl)


contains_at?(p,p',oc) = true  <-- locate(oc,p)=p'

contains_at?(p,p',oc) = false <-- locate(oc,p)=/=p'


contains?(p,p') = exists(contains_at?(p,p'),get_locations(p))


Note that we could define contains? more efficiently as follows,
but we want to specify it via locate because this will also work
for HMD then.

contains?(p,p') = true  
<- p=p'

contains?(p,p') = false 
<- p=/=p', atomic?(p)=true

contains?(p,p') = exists((fn p'' => contains?(p'',p')),get_pages(p))
<- p=/=p', atomic?(p)=false


------------------------------------------------------------------------------

Into HMD:

empty: -> hmd

anchor_ids_below: page_location x function(anchor_id,anchor) -> set(anchor_id)
(* anchor_ids_below returns all anchor identifiers from #2 
   that refer to a location below (or equal to) #1.                         *)

locate: location x hmd x addr -> hmd 
(* Returns sub-document of the hypermediadocument #2 at location #1
   with address #3.                                                         *)

contains_at?: hmd x hmd x page_location -> bool
(* tests whether #1 contains #2 at location #3.                             *)

contains?   : hmd x hmd -> bool
(* test whether #1 contains #2.                                             *)


empty() = Mkhd(Empty_page,empty_function,{},[],[])


anchor_ids_below(o,A) =
  rev_apply_to_set(A,filter((fn c => prefix?(o,get_location(c))),
                            ran(A)))

locate(o,Mkhd(p,A,L,att,a),a') = 
  Mkhd(p',
       A',
       map(replace_uri_li_for_anch_id(uri,embed(a'),ids),
           filter(link_is_sourced?(p',uri,A'),L),
       att,
       a')
<-- locate(o,p)=p', anchor_ids_below(o,A)=ids,
    map_range(update_location(drop(|o|)),domres(ids,A))=A',
    embed(a)=uri


contains_at?(h,h',oc) = true
<-- locate(oc,h,get_addr(h'))=h'

contains_at?(h,h',oc) = false
<-- locate(oc,h,get_addr(h'))=/=h'


contains?(h,h') = exists(contains_at?(h,h'),get_locations(ll_ll(h)))

------------------------------------------------------------------------------