/[mojave]/metaprl/theories/tactic/mptop.ml
ViewVC logotype

Diff of /metaprl/theories/tactic/mptop.ml

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

revision 2577 by jyh, Thu Jan 28 18:44:05 1999 UTC revision 2629 by jyh, Sun Apr 4 22:07:38 1999 UTC
# Line 123  Line 123 
123        hash        hash
124    
125  (*  (*
  * Keep a list of labeled resources for lookup  
  * by the toploop.  
  *)  
 let resources = ref []  
   
 let save data =  
    resources := data :: !resources  
   
 let get_resource name =  
    let rec search = function  
       { resource_data = Label (name', _) } as rsrc :: tl ->  
          if name' = name then  
             rsrc  
          else  
             search tl  
     | _ :: tl ->  
          search tl  
     | [] ->  
          raise Not_found  
    in  
       search !resources  
   
 (*  
126   * Wrap up the joiner.   * Wrap up the joiner.
127   *)   *)
128  let rec join_resource { resource_data = base1 } { resource_data = base2 } =  let join_resource base1 base2 =
129     { resource_data = Join (base1, base2);     Join (base1, base2)
      resource_join = join_resource;  
      resource_extract = extract_resource;  
      resource_improve = improve_resource;  
      resource_close = close_resource  
    }  
130    
131  and extract_resource { resource_data = data } =  let extract_resource data =
132     collect_table data     collect_table data
133    
134  and improve_resource { resource_data = data } (name, expr) =  let improve_resource data (name, expr) =
135     { resource_data = Expr (name, expr, data);     Expr (name, expr, data)
136       resource_join = join_resource;  
137       resource_extract = extract_resource;  let close_resource data mod_name =
138       resource_improve = improve_resource;     Label (String.capitalize mod_name, data)
      resource_close = close_resource  
    }  
   
 and close_resource { resource_data = data } mod_name =  
    let rsrc =  
       { resource_data = Label (String.capitalize mod_name, data);  
         resource_join = join_resource;  
         resource_extract = extract_resource;  
         resource_improve = improve_resource;  
         resource_close = close_resource  
       }  
    in  
       save rsrc;  
       rsrc  
139    
140  (************************************************************************  (************************************************************************
141   * COMPILING                                                            *   * COMPILING                                                            *
# Line 471  Line 429 
429              not_supported loc "while"              not_supported loc "while"
430         | MLast.ExAnt (_, e) ->         | MLast.ExAnt (_, e) ->
431              not_supported loc "ExAnt"              not_supported loc "ExAnt"
432           | MLast.ExXnd (_, _, e) ->
433                mk_expr base e
434    
435  and mk_patt base patt =  and mk_patt base patt =
436     let loc = loc_of_patt patt in     let loc = loc_of_patt patt in
# Line 507  Line 467 
467              not_supported loc "pattern uid"              not_supported loc "pattern uid"
468         | MLast.PaAnt (_, p) ->         | MLast.PaAnt (_, p) ->
469              not_supported loc "pattern PaAnt"              not_supported loc "pattern PaAnt"
470           | MLast.PaXnd _ ->
471                not_supported loc "patterm PaXnd"
472    
473  and mk_type base t =  and mk_type base t =
474     let loc = loc_of_ctyp t in     let loc = loc_of_ctyp t in
# Line 545  Line 507 
507              not_supported loc "type product"              not_supported loc "type product"
508         | (<:ctyp< $uid:s$ >>) ->         | (<:ctyp< $uid:s$ >>) ->
509              not_supported loc "type constructor var"              not_supported loc "type constructor var"
510           | MLast.TyXnd (_, _, t) ->
511                mk_type base t
512    
513  and mk_sig_item base si =  and mk_sig_item base si =
514     let loc = loc_of_sig_item si in     let loc = loc_of_sig_item si in
# Line 680  Line 644 
644        base        base
645    
646  let toploop_resource =  let toploop_resource =
647     { resource_data = add_resources Empty values;     Mp_resource.create (**)
648       resource_join = join_resource;        { resource_join = join_resource;
649       resource_extract = extract_resource;          resource_extract = extract_resource;
650       resource_improve = improve_resource;          resource_improve = improve_resource;
651       resource_close = close_resource          resource_close = close_resource
652     }        }
653          (add_resources Empty values)
654  let toploop_add  
655      { resource_data = data;  let get_resource modname =
656        resource_join = join_resource;     Mp_resource.find toploop_resource modname
       resource_extract = extract_resource;  
       resource_improve = improve_resource;  
       resource_close = close_resource  
     } values =  
    { resource_data = add_resources data values;  
      resource_join = join_resource;  
      resource_extract = extract_resource;  
      resource_improve = improve_resource;  
      resource_close = close_resource  
    }  
657    
658  let expr_of_ocaml_expr = mk_expr  let expr_of_ocaml_expr = mk_expr
659  let expr_of_ocaml_str_item = mk_str_item  let expr_of_ocaml_str_item = mk_str_item

Legend:
Removed from v.2577  
changed lines
  Added in v.2629

  ViewVC Help
Powered by ViewVC 1.1.26