Anubis / Anubis

   /**************************************************************************************
   
   
                     _____              ___.   .__         ________  
                    /  _  \   ____  __ _\_ |__ |__| ______ \_____  \ 
                   /  /_\  \ /    \|  |  \ __ \|  |/  ___/  /  ____/ 
                  /    |    \   |  \  |  / \_\ \  |\___ \  /       \ 
                  \____|__  /___|  /____/|___  /__/____  > \_______ \
                          \/ The \/  Anubis  \/    2   \/  Project \/
   
   
   Name of this file:           memory_1.anubis
   
   Purpose of this file:        Managing the knowledge base. 
   
   

   Authors (Name [initials]):   Alain Proute'   [AP]
   
   Updates ([initials] (date) comment): 
      [AP] (2007 jun 29) Creation of this file.
   
   
   **************************************************************************************/

read tools/basis.anubis   
read tools/streams.anubis   
read common.anubis
read dictionary_1.anubis   
read src_files_1.anubis   

   
   ----------------------------------- Table of Contents ---------------------------------

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

   
   *** (1) Entries in dictionaries. 
   
   Each dictionary has its own type of entries. 
   
   
      *** (1.1) Dictionary of modules. 
   
public type ModuleEntry:
   predefined,                      // the special module containing all predefinitions
   src_file
     (
       List(Int32)   depends,       // ids of modules it depends on (not including itself)
       String        absolute_path, // non ambiguous (absolute) path of source file
       Int32         last_compiled  // date at which the module has been last compiled
     ). 

   Alternatives may be added if there are other kinds of modules.    
   
public define String
   absolute_path
     (
       ModuleEntry   entry
     ) =
   if entry is 
     {
       predefined            then "/predefined", 
       src_file(_,path,_)    then path
     }.
      
   
   
      *** (1.2) Dictionary of types. 
   
public type EntryAlternative:
   singleton  (String name),
   product    (List((StrongType,String))  components). 
   
public type TypeEntry:
   type
     (
       List(Int32)              depends,        // ids of modules it depends on
       Int32                    module_id,      // id of module within which this type is defined
       String                   name,           // name of this type (or type schema)
       List(Position)           positions,      // positions of all paragraphs defining this type
       List(String)             parameters,     // list of names of parameters
       List(EntryAlternative)   alternatives,   // list of alternatives
       TypeCompletion           completion      // flag indicating if type is complete or not
     ).
   

   
   
      *** (1.3) Dictionary of data. 
   
public type DatumEntry:
   datum
     (
       List(Int32)              depends,        // ids of modules it depends on
       Int32                    module_id,
       String                   name, 
       Position                 position,
       List(String)             parameters, 
       Signature                signature, 
       String                   sign, 
       StrongTerm               value
     ). 
   
   
   
      *** (1.4) Dictionary of theorems. 
   
public type ThmEntry:
   thm
     (
       List(Int32)              depends,        // ids of modules it depends on
       Int32                    datum_id,
       StrongTerm               pattern
     ).
   
   
   
    
   
   
   *** (2) Compiler states. 
   
   The compiler  needs to manage several  directories, which make  together its 'knowledge
   base'.   These directories  are  saved into  files  between compilations,  so that  non
   modified  modules are  not recompiled.   During the  compilation, the  dictionaries are
   accessible through the following structure:
   
public type Dictionaries:
   dictionaries
     (
       Dictionary1(ModuleEntry,  String),
       Dictionary1(TypeEntry,    String),
       Dictionary1(DatumEntry,   String),
       Dictionary1(ThmEntry,     StrongTerm)
     ).

   
public type OpenModule:
   src_file
     (
       Stream          stream,
       Int32           module_id
     ).
   
   The compiler has an internal state of the following type: 
   
public type State:
   cstate
     (
       List(Option)           options, 
       Dictionaries           dictionaries,
       Var(List(OpenModule))  read_stack,
       List(List(String))     read_paths
     ). 
   
   
   
   The next tool, used once at the  beginning of each compilation, enables to retrieve the
   dictionaries of the previous compilation. Obsolete entries are discarded automatically.
   If a file does'nt exists or is corrupted, an empty dictionary is created.
   
public define State
   recover_compiler_state
     (
       List(Option) options        // all options found on the command line
     ). 
   
   
   The next  tool, used  once at  the end of  each compilation,  saves all  directories to
   files.

public define One
   save_compiler_state
     (
       State  state
     ). 
   
   
   
   
   
   --- That's all for the public part ! --------------------------------------------------
   
   
   
   ----------------------------------- Table of Contents ---------------------------------

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

   
   
   *** [1] Naming the dictionaries. 
   
define String     mod_dict_name =     "modules".
define String     typ_dict_name =     "types".  
define String     dat_dict_name =     "data". 
define String     thm_dict_name =     "theorems".
   
   
   
   
   
   
   *** [2] Updating ids in strong items. 

   When the directories are retrieved from files, entries must be updated. This amounts to
   replace old ids  by new ids.  For each  kind of id we have a  'Renumbering' object (see
   dictionary_1.anubis).

   
   
   
      *** [2.1] Tools for applying a function which may fail to lists or pairs.  
   
   We  use operations which  may fail.  This is  why we  need the  following tools.   In a
   compound operation, the whole operation fails as soon as at least one of the operations
   fails.
   
   The following tool applies 'f' to each  element of the list 'l' the result is 'failure'
   as soon as 'f' fails on at least one element of 'l'.
   
define Maybe(List($T))
   map_discard
     (
       $U -> Maybe($T)      f,     // the operation which may fail
       List($U)             l      // the list the elements it is applied to
     ) =
   if l is 
     {
       [ ] then success([ ]), 
       [h . t] then if f(h) is 
         {
           failure then failure, 
           success(h1) then 
             if map_discard(f,t) is 
               {
                 failure then failure, 
                 success(t1) then success([h1 . t1])
               }
         }
     }.
   
   
   
   The same one for a pair of data.
   
define Maybe(($T,$T))
   map_discard
     (
       $U -> Maybe($T)      f, 
       $U                   a, 
       $U                   b
     ) =
   if f(a) is 
     {
       failure then failure, 
       success(a1) then if f(b) is 
         {
           failure then failure,
           success(b1) then success((a1,b1))
         }
     }.
     
   
   
   
      *** [2.1] Updating the type ids and the data (term) ids. 
   
   The two functions are cross recursive. 
   
define StrongTerm
   update_ids 
     ( 
       Renumbering(TypeEntry)     typ_renum, 
       Renumbering(DatumEntry)    dat_renum,
       StrongTerm                 sterm
     ).
   
   
define StrongType
   update_ids 
     ( 
       Renumbering(TypeEntry)     typ_renum, 
       Renumbering(DatumEntry)    dat_renum,
       StrongType                 stype
     ) =
   if stype is 
     {
       _Parameter(name) then 
         stype, 
   
       _Defined(type_id,operands) then 
         _Defined(new_id(typ_renum,type_id),
                  map((StrongType st) |-> update_ids(typ_renum,dat_renum,st),operands)), 
   
       _Product(l) then 
         _Product(map((StrongType st) |-> update_ids(typ_renum,dat_renum,st),l)), 
   
       _Functional(source,target) then 
         _Functional(update_ids(typ_renum,dat_renum,source),
                     update_ids(typ_renum,dat_renum,target)),
   
       _Omega then 
         _Omega,
   
       _Witness(statement) then 
         _Witness(update_ids(typ_renum,dat_renum,statement)), 
   
       _Quantified(_X,_T) then 
         _Quantified(_X,update_ids(typ_renum,dat_renum,_T))
     }. 
   
   
define StrongTerm
   update_ids 
     ( 
       Renumbering(TypeEntry)     typ_renum, 
       Renumbering(DatumEntry)    dat_renum,
       StrongTerm                 sterm
     ) =
   if sterm is 
     {
       global(id) then 
         global(new_id(dat_renum,id)), 
   
       symbol(depth) then
         sterm, 
   
       tuple(l) then
         tuple(map((StrongTerm st) |-> update_ids(typ_renum,dat_renum,st),l)), 
      
       proj(i,st) then 
         proj(i,update_ids(typ_renum,dat_renum,st)), 
   
       incl(_T,i,st) then
         incl(update_ids(typ_renum,dat_renum,_T),i,update_ids(typ_renum,dat_renum,st)),
   
       cond(_T,test,cases) then
         cond(update_ids(typ_renum,dat_renum,_T),
              update_ids(typ_renum,dat_renum,test),
              map((StrongTerm st) |-> update_ids(typ_renum,dat_renum,st),
                                  cases)),
   
       lambda(_T,_E) then 
         lambda(update_ids(typ_renum,dat_renum,_T),
                update_ids(typ_renum,dat_renum,_E)),
   
       app(f,a) then 
         app(update_ids(typ_renum,dat_renum,f),
             update_ids(typ_renum,dat_renum,a)),
            
       forall(_T,_E) then 
         forall(update_ids(typ_renum,dat_renum,_T),
                update_ids(typ_renum,dat_renum,_E)),
   
       description(p) then 
         description(update_ids(typ_renum,dat_renum,p)),
   
       property(p) then 
         property(update_ids(typ_renum,dat_renum,p)),
   
       choice(p) then 
         choice(update_ids(typ_renum,dat_renum,p)),
      
       parametric(_X,st) then 
         parametric(_X,update_ids(typ_renum,dat_renum,st)),
   
       parametric_app(st,_T) then 
         parametric_app(update_ids(typ_renum,dat_renum,st),
                        update_ids(typ_renum,dat_renum,_T)),
  }. 
   
   
   
   

   
   *** [3] Saving the dictionaries. 
   
define One
   save
     (
       Dictionaries   dicts
     ) =
   if dicts is dictionaries(mod_d,typ_d,dat_d,thm_d) then 
   save(mod_d);
   save(typ_d);
   save(dat_d);
   save(thm_d).
   
   
   
   
   
   *** [4] Retrieving all dictionaries. 
   
   This  must be  done in  a specific  order because  of cross  references by  ids between
   dictionaries, which may change during the retrieving. 
   
   We will need the following tool testing if two list have an element in common:
   
define Bool   
   intersect
     (
       List($T)   l1, 
       List($T)   l2
     ) =
   if l1 is 
     {
       [ ] then false, 
       [h . t] then 
         if member(l2,h)
         then true
         else intersect(t,l2)
     }.
   
   

      *** [4.1] The modules dictionary. 
   
   
         *** [4.1.1] Getting the date of last modification of a file. 
   
define Maybe(Int32)
   file_date
     (
       String path
     ) =
   if get_file_times(path) is 
     {
       failure then failure, 
       success(t) then if t is times(d,_) then success(d)
     }. 
   
   
   
         *** [4.1.2] The function for discarding a module. 
   
   If the date of the file cannot be found (the file may have been erased for example) the
   module is discarded. Otherwise, the module (i.e. the result of the previous compilation
   of this module) is  discarded if and only if the date of  last modification of the file
   is newer than the recorded date of compilation of the module.
   
define KeepOrDiscard
   discard_module
     (
       ModuleEntry   entry
     ) =
   if entry is 
     {
       predefined then keep,
       src_file(dep,abs_path,last_compiled) then 
         if file_date(abs_path) is 
           {
             failure then discard, 
             success(new_date) then 
               if new_date >= last_compiled
               then discard
               else keep
           }
     }.
   
   
   
   
   
   
      *** [4.2] The types dictionary. 
   
   
         *** [] Discarding a type. 
   
define TypeEntry -> KeepOrDiscard
   discard_type
     (
       List(Int32)   to_be_recompiled 
     ) =
   (TypeEntry te) |-> if te is type(dep,_,_,_,_,_,_) then 
   if intersect(to_be_recompiled,dep)
   then discard
   else keep. 
   
     
   
      *** [4.3] The data dictionary.
   
         *** [4.3.1] Discarding a datum. 
   
define DatumEntry -> KeepOrDiscard
   discard_datum
     (
       List(Int32)   to_be_recompiled
     ) =
   (DatumEntry de) |-> if de is datum(dep,_,_,_,_,_,_,_) then 
   if intersect(to_be_recompiled,dep)
   then discard
   else keep. 
   
   
   
   
      *** [4.4] The theorems dictionary. 
   
define ThmEntry -> KeepOrDiscard
   discard_thm
     (
       List(Int32)   to_be_recompiled
     ) =
   (ThmEntry te) |-> if te is thm(dep,_,_) then 
   if intersect(to_be_recompiled,dep)
   then discard
   else keep. 
   
   
   
   *** [5] Saving the compiler's state. 
   
public define One
   save_compiler_state
     (
       State  state
     ) = 
   if state is cstate(options,dictionaries,read_stack,read_paths) then 
   save(dictionaries). 
   

   
   
   *** [6] Recovering the compiler state. 

   
   Getting the old ids of all modules which must be recompiled. 
   
define List(Int32)
   get_to_be_recompiled
     (
       Renumbering(ModuleEntry)   renum,
       List(Int32)                so_far,
       Int32                      i             // decreasing
     ) =
   if i < 0 then so_far else 
   if maybe_new_id(renum,i) is 
     {
       failure     then get_to_be_recompiled(renum, [i . so_far], i-1),
       success(_)  then get_to_be_recompiled(renum, so_far      , i-1)
     }. 
   
define List(Int32)
   get_to_be_recompiled
     (
       Renumbering(ModuleEntry)   renum
     ) =
   get_to_be_recompiled(renum,[],size(renum)-1). 
   
   
   Create an 'empty' state:
   
define List(List(String))
   get_read_paths
     =
   [
      split_path(get_current_directory),
      split_path(my_anubis_directory),
      split_path(anubis_directory)
   ]. 
   
   
define State
   new_state
     (
       List(Option)  options
     ) =
   cstate(options,
          dictionaries
            (
              create_dictionary(8,  mod_dict_name,absolute_path),
              create_dictionary(10, typ_dict_name,name),
              create_dictionary(12, dat_dict_name,name),
              create_dictionary(12, thm_dict_name,pattern)
            ),
          var([]),
          get_read_paths
         ). 
   
   
   
   A type used locally:
   
type RetDicts:   
   dicts
     (
       Dictionary1(ModuleEntry,String),
       Renumbering(ModuleEntry), 
       Dictionary1(TypeEntry,String),
       Renumbering(TypeEntry), 
       Dictionary1(DatumEntry,String),
       Renumbering(DatumEntry), 
       Dictionary1(ThmEntry,StrongTerm),
       Renumbering(ThmEntry)
     ). 
   
define Maybe(RetDicts)
   retrieve_dictionaries
     =
   if retrieve_dictionary(8,mod_dict_name,absolute_path,discard_module) is 
     {
     failure then failure, 
     success(p) then if p is (mod_dict,mod_renum) then 
       with to_be_recompiled = get_to_be_recompiled(mod_renum), 
       if retrieve_dictionary(10,typ_dict_name,name,discard_type(to_be_recompiled)) is 
       {
       failure then failure, 
       success(p) then if p is (typ_dict,typ_renum) then
         if retrieve_dictionary(12,dat_dict_name,name,discard_datum(to_be_recompiled)) is
         {
         failure then failure, 
         success(p) then if p is (dat_dict,dat_renum) then 
           if retrieve_dictionary(12,thm_dict_name,pattern,discard_thm(to_be_recompiled)) is 
           {
           failure then failure, 
           success(p) then if p is (thm_dict,thm_renum) then 
             success(dicts
                       (
                         mod_dict,mod_renum,
                         typ_dict,typ_renum,
                         dat_dict,dat_renum,
                         thm_dict,thm_renum
                       )
                    )
           }
         }
       }
     }. 
     
   
   

      *** [] Updating the modules dictionary. 
   
   Only the  list of  dependancies must be  updated. Ids  of discarded (to  be recompiled)
   modules  are discarded  from the  list.  They are  regenerated when  these modules  are
   recompiled.

   Of course, the list of dependancies of the special module 'predefined' is empty. 
   
define ModuleEntry -> ModuleEntry
   update_mod_entry
     (
       Renumbering(ModuleEntry) renum
     ) =
   (ModuleEntry e) |-> 
   if e is 
     {
       predefined then e, 
       src_file(dep,ap,lc) then 
         src_file(map((Int32 old_id) |-> new_id(renum,old_id),dep),ap,lc)
     }.
   
   
define One
   update_mod_dictionary
     (
       Dictionary1(ModuleEntry,String)     mod_dict,
       Renumbering(ModuleEntry)            mod_renum
     ) =
   update_all_entries(mod_dict,update_mod_entry(mod_renum)). 
   
   
   
   
   
      *** [] Updating the types dictionary. 
   
   We must update:
     - the list of dependancies,
     - the module id, 
     - the list of alternatives. 
     
   
define EntryAlternative -> EntryAlternative
   update_alternative
     (
       Renumbering(TypeEntry)     typ_renum, 
       Renumbering(DatumEntry)    dat_renum
     ) =
   (EntryAlternative ea) |->
     if ea is 
       {
         singleton(name)  then ea, 
         product(comps)   then product(map(((StrongType,String) p) |-> 
                                              if p is (t,n) then 
                                                (update_ids(typ_renum,dat_renum,t),n),
                                           comps))
       }.
   
   
define TypeEntry -> TypeEntry
   update_typ_entry
     (
       Renumbering(ModuleEntry)       mod_renum, 
       Renumbering(TypeEntry)         typ_renum, 
       Renumbering(DatumEntry)        dat_renum
     ) =
   (TypeEntry te) |-> 
   if te is type(dep,mod_id,name,pos,parms,alts,comp) then 
   type(map((Int32 old_id) |-> new_id(mod_renum,old_id),dep),
        new_id(mod_renum,mod_id),
        name,
        pos,
        parms, 
        map(update_alternative(typ_renum,dat_renum),alts),
        comp). 
   
define One 
   update_typ_dictionary
     (
       Dictionary1(TypeEntry,String)        typ_dict, 
       Renumbering(ModuleEntry)             mod_renum,
       Renumbering(TypeEntry)               typ_renum,
       Renumbering(DatumEntry)              dat_renum     
     ) =
   update_all_entries(typ_dict,update_typ_entry(mod_renum,typ_renum,dat_renum)). 
   
   
   
   
   
      *** [] Updating the data dictionary. 
   
   We must update:
     - the list of dependancies, 
     - the id of the module, 
     - the signature,
     - the value
   
   
define Signature -> Signature
   update_signature
     (
       Renumbering(TypeEntry)         typ_renum, 
       Renumbering(DatumEntry)        dat_renum
     ) =
   (Signature s) |->   
      if s is 
        {  
          nullary(_T) then
            nullary(update_ids(typ_renum,dat_renum,_T)),
   
          unary(src,trgt) then
            unary(update_ids(typ_renum,dat_renum,src),
                  update_ids(typ_renum,dat_renum,trgt)),
   
          binary(src1,src2,trgt) then
            binary(update_ids(typ_renum,dat_renum,src1),
                   update_ids(typ_renum,dat_renum,src2),
                   update_ids(typ_renum,dat_renum,trgt)),
   
          declarative(dom,bt,trgt) then
            declarative(update_ids(typ_renum,dat_renum,dom),
                        update_ids(typ_renum,dat_renum,bt),
                        update_ids(typ_renum,dat_renum,trgt))
        }. 
   
   
define DatumEntry -> DatumEntry
   update_dat_entry
     (
       Renumbering(ModuleEntry)       mod_renum, 
       Renumbering(TypeEntry)         typ_renum, 
       Renumbering(DatumEntry)        dat_renum
     ) =
   (DatumEntry de) |-> 
   if de is datum(dep,m_id,name,pos,parms,signature,sign,value) then
   datum(map((Int32 old_id) |-> new_id(mod_renum,old_id),dep),
         new_id(mod_renum,m_id),
         name,
         pos,
         parms,
         update_signature(typ_renum,dat_renum)(signature), 
         sign,
         update_ids(typ_renum,dat_renum,value)). 
   
define One 
   update_dat_dictionary
     (
       Dictionary1(DatumEntry,String)       dat_dict, 
       Renumbering(ModuleEntry)             mod_renum,
       Renumbering(TypeEntry)               typ_renum,
       Renumbering(DatumEntry)              dat_renum     
     ) =
   update_all_entries(dat_dict,update_dat_entry(mod_renum,typ_renum,dat_renum)). 
   
   
   
   
      *** [] Updating the theorems dictionary. 
   
   We must update:
     - the list of dependancies, 
     - the datum id,
     - the pattern. 
   
define ThmEntry -> ThmEntry
   update_thm_entry
     (
       Renumbering(ModuleEntry)       mod_renum, 
       Renumbering(TypeEntry)         typ_renum, 
       Renumbering(DatumEntry)        dat_renum
     ) =
   (ThmEntry te) |-> 
   if te is thm(dep,d_id,pattern) then 
   thm(map((Int32 old_id) |-> new_id(mod_renum,old_id),dep),
       new_id(dat_renum,d_id), 
       update_ids(typ_renum,dat_renum,pattern)). 
   
   
define One 
   update_thm_dictionary
     (
       Dictionary1(ThmEntry,StrongTerm)     thm_dict, 
       Renumbering(ModuleEntry)             mod_renum,
       Renumbering(TypeEntry)               typ_renum,
       Renumbering(DatumEntry)              dat_renum     
     ) =
   update_all_entries(thm_dict,update_thm_entry(mod_renum,typ_renum,dat_renum)). 
   
   
   
   *** [] Recovering the whole compiler's state. 
   
public define State
   recover_compiler_state
     (
       List(Option) options
     ) = 
   if retrieve_dictionaries is
     {
       failure then new_state(options), 
       success(r) then if r is 
         dicts(mod_dict,mod_renum,
               typ_dict,typ_renum,
               dat_dict,dat_renum,
               thm_dict,thm_renum) then 
         update_mod_dictionary(mod_dict,mod_renum);
         update_typ_dictionary(typ_dict,mod_renum,typ_renum,dat_renum);
         update_dat_dictionary(dat_dict,mod_renum,typ_renum,dat_renum);
         update_thm_dictionary(thm_dict,mod_renum,typ_renum,dat_renum);
         cstate(options,
                dictionaries(mod_dict,typ_dict,dat_dict,thm_dict),
                var([]),
                get_read_paths)
     }.