/[mojave]/metaprl/library/definition.ml
ViewVC logotype

Diff of /metaprl/library/definition.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 2921 by nogin, Fri Oct 22 01:07:59 1999 UTC revision 2922 by lolorigo, Thu Mar 16 19:52:02 2000 UTC
# Line 51  Line 51 
51    match dest_term t with    match dest_term t with
52      { term_op = op; term_terms = [version; purposes] }      { term_op = op; term_terms = [version; purposes] }
53      -> map_isexpr_to_list string_of_itoken_term (term_of_unbound_term purposes)      -> map_isexpr_to_list string_of_itoken_term (term_of_unbound_term purposes)
54        | { term_op = op; term_terms = [version; purposes; rest] } -> map_isexpr_to_list string_of_itoken_term (term_of_unbound_term purposes)
55      |_ -> error ["term"; "!description"; "not"] [] [t]      |_ -> error ["term"; "!description"; "not"] [] [t]
56  (*  (*
57    
# Line 245  Line 246 
246    
247    
248  let substance_import def stype data =  let substance_import def stype data =
249      print_string "subimp ";
250    match stype with    match stype with
251      Substance -> def#set_substance (new substance data#get_term); ()      Substance -> def#set_substance (new substance data#get_term); ()
252    | TermSubstance -> def#set_substance (new term_substance data#get_term); ()    | TermSubstance -> def#set_substance (new term_substance data#get_term); ()
# Line 269  Line 271 
271            match sub with None -> raise NoSubstance | Some s -> s            match sub with None -> raise NoSubstance | Some s -> s
272  end  end
273    
274    class term_dyneval (t: term) =
275     object(self)
276    
277      (*val mutable stamp = None*)
278      val term = t
279      (*val mutable flags = None
280    
281      method get_term = self#get_term*)
282    
283    end
284    
285    
286    exception NoDyneval
287    
288  class ['a] term_definition d da st =  class ['a] term_definition d da st =
289   object (self)   object (self)
290    inherit ['a] definition d da st    inherit ['a] definition d da st
291    
292      val mutable dyneval = Some (new term_dyneval ivoid_term)
293    
294      method set_dyneval s = dyneval <- Some s
295      method dyn_p = match dyneval with None -> false | Some s -> true
296      method get_dyneval = match dyneval with None -> raise NoDyneval | Some s -> s
297      
298    method set_substance (s : term_substance) = sub <- Some s    method set_substance (s : term_substance) = sub <- Some s
299    method get_term = (self#get_substance)#get_term    method get_term = (self#get_substance)#get_term
300    
# Line 281  Line 302 
302    
303  let idag_child_param = make_param (Token "!dag_child")  let idag_child_param = make_param (Token "!dag_child")
304  let idirectory_param = make_param (Token "!directory")  let idirectory_param = make_param (Token "!directory")
305    let idyneval_param = make_param (Token "!dyneval")
306    
307  let idag_cons_op = mk_nuprl5_op [make_param (Token "!dag_cons")]  let idag_cons_op = mk_nuprl5_op [make_param (Token "!dag_cons")]
308    
# Line 295  Line 317 
317          )          )
318    |_ -> false    |_ -> false
319    
320    let idyneval_term_p t =
321     match dest_term t with
322      { term_op = op; term_terms = bts}  -> (*lal make stronger test*)
323      (match dest_op op with
324          { op_name = opname; op_params =  id :: rest}
325          when Opname.eq nuprl5_opname opname & parmeq id idyneval_param -> true
326          | _ -> false
327         )
328      | _ -> false
329    
330    
331  let children_of_idirectory_term t =  let children_of_idirectory_term t =
332   match dest_term t with   match dest_term t with
# Line 354  Line 386 
386    
387    (* instantiation of values could be lazy, but seems like inconsequential space savings *)    (* instantiation of values could be lazy, but seems like inconsequential space savings *)
388    (*    (*
389    val children = children_of_idirectory_term (super#get_substance)#get_term    val children = children_of_idirectory_term (super#get_substance)#get_term (*LAL fails, not a dir term*)
390    val rootp = iroot_directory_term_p (super#get_substance)#get_term    val rootp = iroot_directory_term_p (super#get_substance)#get_term
391    val root_name = let term = (super#get_substance)#get_term in    val root_name = let term = (super#get_substance)#get_term in
392                          if (iroot_directory_term_p term)                          (print_string " n "; if (iroot_directory_term_p term)
393                             then name_of_iroot_directory_term term                             then name_of_iroot_directory_term term
394                             else ""                             else "")
395    *)    *)
396    val children = children_of_idirectory_term (term_of_isubstance_term datterm)    val children = children_of_idirectory_term (term_of_isubstance_term datterm)
397    val rootp = iroot_directory_term_p (term_of_isubstance_term    val rootp = iroot_directory_term_p (term_of_isubstance_term
398                                        datterm                                        datterm
399                                        )                                        )
400    val root_name = let term = (term_of_isubstance_term datterm) in    val root_name = let term = (term_of_isubstance_term datterm) in
401                          if (iroot_directory_term_p term)                          if (iroot_directory_term_p term) then name_of_iroot_directory_term term
                            then name_of_iroot_directory_term term  
402                             else ""                             else ""
403    
404    method get_children = children    method get_children = children
405    method rootp = rootp    method rootp = rootp
406    method get_root_name = if rootp then root_name else raise NotRootDirectory    method get_root_name = if rootp then root_name else (print_string "nonroot"; raise NotRootDirectory)
407  end  end
408    
409    
# Line 408  Line 439 
439  (* would like this to take table as arg and table contains term -> def  (* would like this to take table as arg and table contains term -> def
440     want polymorphism with definitions and tables     want polymorphism with definitions and tables
441   *)   *)
442  let import_term idef idesc =  let import_term_old idef idesc =
443    (* print_string " import_term "; Mbterm.print_term idef; *)    print_string " import_term "; Mbterm.print_term idef;
444    match dest_term idef with    match dest_term idef with
445      { term_op = op; term_terms = [idep; idata] } when opeq op idefinition_op      { term_op = op; term_terms = [idep; idata] } when opeq op idefinition_op
446        -> (let dep = term_to_dependency (term_of_unbound_term idep) in        -> (let dep = term_to_dependency (term_of_unbound_term idep) in
447            let data = term_to_data (term_of_unbound_term idata) in            let data = term_to_data (term_of_unbound_term idata) in
448    
449            (*print_string " import_term "; Mbterm.print_term (term_of_unbound_term idata); *)            print_string " import_term "; Mbterm.print_term (term_of_unbound_term idata);
450            (* if not (dag_description_p idesc) then print_string " uh oh"; *)            if not (dag_description_p idesc) then print_string " uh oh";
451    
452              if not (dag_description_p idesc)
453                 then TermDefinition (new term_definition dep data TermSubstance)
454                 else
455                      DirectoryDefinition (new directory_definition dep data Substance) (*LAL fails, subst not a dir term*)
456            )
457    
458        |_ -> error ["term"; "!definition"] [] [idef]
459    (*
460    let dest_dyneval_term t =
461      match dest_term t with
462      { term_op = op; term_terms = [cond; exp; stamp; value]} (*lal make stronger test*)
463         -> (match dest_op op with
464              { op_name = opname; op_params = id :: rest}
465                    when nuprl5_opname_p opname & parmeq id idyneval_param
466                    ->
467              | _ -> fail
468            )
469      |_ -> fail
470    *)
471    
472    let import_term idef idesc =
473      (*print_string " import_term "; Mbterm.print_term idef;*)
474      match dest_term idef with
475        { term_op = op; term_terms = [idep; idata] } when opeq op idefinition_op
476          -> (let dep = term_to_dependency (term_of_unbound_term idep) in
477              let data = term_to_data (term_of_unbound_term idata) in
478    
479              (*print_string " import_term "; Mbterm.print_term (term_of_unbound_term idata);*)
480              
481            if not (dag_description_p idesc)            if not (dag_description_p idesc)
482               then TermDefinition (new term_definition dep data TermSubstance)               then TermDefinition (new term_definition dep data TermSubstance)
483               else               else
484                  DirectoryDefinition (new directory_definition dep data Substance)                  let datterm = data#get_term in
485                    let idir = term_of_isubstance_term datterm in
486                    if idirectory_term_p idir then DirectoryDefinition (new directory_definition dep data Substance) (*LAL fails, subst not a dir term*)
487                    else TermDefinition (new term_definition dep data TermSubstance)
488    
489                    (*if (idyneval_term_p idir) then
490                    let def = new term_definition dep data TermSubstance in
491                    and [stamp, flags, term] = dest_dyneval_term idir in
492                    (def#set_dyneval (new term_dyneval idir); TermDefinition def)
493                    else error ["import"; "term"; "not"] [] [idir]*)
494                    
495          )          )
496    
497      |_ -> error ["term"; "!definition"] [] [idef]      |_ -> error ["term"; "!definition"] [] [idef]
# Line 464  Line 534 
534                  | Some s -> commit ttable s oid seq                  | Some s -> commit ttable s oid seq
535                  ) in                  ) in
536    
537    (*    
538    print_string "apply broadcast";    (*print_string "apply broadcast";
539    print_newline();    print_newline();
540    Mbterm.print_term ibcast;    Mbterm.print_term ibcast;
541    *)    print_newline();*)
542    
543    match dest_term ibcast with    match dest_term ibcast with
544      { term_op = op; term_terms = terms} ->      { term_op = op; term_terms = terms} ->
545          match dest_op op with          match dest_op op with
546            { op_name = opn; op_params = pid :: pseq :: rest } when nuprl5_opname_p opn            { op_name = opn; op_params = pid :: pseq :: rest } when nuprl5_opname_p opn
547              -> ((if parmeq pid idefinition_insert_param              -> (if parmeq pid idefinition_insert_param
548                      then let entry = (import_term (term_of_unbound_term (hd terms)) idesc) in                      then
549                        let entry = (import_term (term_of_unbound_term (hd terms)) idesc) in
550                           let oid = (oid_of_term_entry entry)                           let oid = (oid_of_term_entry entry)
551                           and seq = (dest_int_param pseq) in                           and seq = (dest_int_param pseq) in
552                            insert ttable stamp oid seq entry                            (insert ttable stamp oid seq entry;
553                            ; auto_commit oid seq                            auto_commit oid seq)
554                  else if parmeq pid idefinition_delete_param                  else if parmeq pid idefinition_delete_param
555                      then let oid = (dest_obid_param (hd rest))                      then let oid = (dest_obid_param (hd rest))
556                           and seq = (dest_int_param pseq) in                           and seq = (dest_int_param pseq) in
# Line 493  Line 564 
564                      then undo ttable stamp                      then undo ttable stamp
565                                          (dest_obid_param (hd rest))                                          (dest_obid_param (hd rest))
566                                          (dest_int_param pseq)                                          (dest_int_param pseq)
567                  else error ["term"; "broadcast"; "opid"] [] [ibcast])                  else error ["term"; "broadcast"; "opid"] [] [ibcast]
568                  )                  )              
569             |_ -> error ["term"; "broadcast"] [] [ibcast]             |_ -> error ["term"; "broadcast"] [] [ibcast]
570    
571    

Legend:
Removed from v.2921  
changed lines
  Added in v.2922

  ViewVC Help
Powered by ViewVC 1.1.26