/[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 3278 by nogin, Wed Jun 20 00:27:36 2001 UTC revision 3292 by nogin, Sun Jun 24 10:25:49 2001 UTC
# Line 147  Line 147 
147  (*  (*
148   * The resource maps strings to values.   * The resource maps strings to values.
149   *)   *)
 type top_data =  
    Empty  
  | Label of string * top_data  
  | Expr of string * expr * top_data  
  | Join of top_data * top_data  
   
150  type top_table =  type top_table =
151     (string, string * expr) Hashtbl.t     (string, string * expr) Hashtbl.t
152    
# Line 160  Line 154 
154   * IMPLEMENTATION                                                       *   * IMPLEMENTATION                                                       *
155   ************************************************************************)   ************************************************************************)
156    
157  (*  let create () =
158   * Construct a hash table of all the values.     Hashtbl.create 201
  * As in ML, the newer values override the previous.  
  *)  
 let collect_table data =  
    let hash = Hashtbl.create 201 in  
    let rec collect mod_name labels = function  
       Empty ->  
          labels  
     | (Label (mod_name, next)) as label ->  
          if List.memq label labels then  
             labels  
          else  
             collect mod_name (label :: labels) next  
     | Expr (name, expr, next) ->  
          let labels = collect mod_name labels next in  
             Hashtbl.add hash name (mod_name, expr);  
             labels  
   
     | Join (next1, next2) ->  
          let labels = collect mod_name labels next1 in  
             collect mod_name labels next2  
    in  
    let _ = collect "." [] data in  
       hash  
159    
160  (*  let add tbl (module_name,name,expr) =
161   * Wrap up the joiner.     Hashtbl.add tbl name (module_name,expr)
  *)  
 let join_resource base1 base2 =  
    Join (base1, base2)  
162    
163  let extract_resource data =  let add_commands tbl =
164     collect_table data     List.iter (fun (name, expr) -> Hashtbl.add tbl name ("",expr))
165    
166  let improve_resource data (name, expr) =  let retr tbl = tbl
    Expr (name, expr, data)  
167    
168  let close_resource data mod_name =  (*!
169     Label (String.capitalize mod_name, data)   * @begin[doc]
170     * Toplevel values are added to the @Comment!resource[toploop_resource] resource.
171     * The argument has type @code{string * expr}, which includes
172     * the string name of the value, and it's value.
173     * @docoff
174     * @end[doc]
175     *)
176    let resource toploop = Imperative {
177       imp_create = create;
178       imp_add = add;
179       imp_retr = retr
180    }
181    
182  (************************************************************************  (************************************************************************
183   * COMPILING                                                            *   * COMPILING                                                            *
# Line 296  Line 274 
274     let lookup names v =     let lookup names v =
275        match names with        match names with
276           [modname] ->           [modname] ->
277              begin              search modname v (Hashtbl.find_all base v)
                try search modname v (Hashtbl.find_all base v) with  
                   Not_found ->  
                      Stdpp.raise_with_loc loc (**)  
                         (RefineError ("mk_proj_expr",  
                                       StringStringError ("undefined variable", modname ^ "." ^ v)))  
             end  
278         | _ ->         | _ ->
279              Stdpp.raise_with_loc loc (**)              Stdpp.raise_with_loc loc (**)
280                 (RefineError ("mk_proj_expr", StringError "nested modules are not implemented"))                 (RefineError ("mk_proj_expr", StringError "nested modules are not implemented"))
# Line 701  Line 673 
673                  | _ ->                  | _ ->
674                       raise (RefineError ("cons_expr", StringError "type mismatch"))))                       raise (RefineError ("cons_expr", StringError "type mismatch"))))
675    
676  let values =  let resource toploop +=
677     ["+",                int_int_fun_int_expr ( + );     ["Pervasives", "+",     int_int_fun_int_expr ( + );
678      "-",                int_int_fun_int_expr ( - );      "Pervasives", "-",     int_int_fun_int_expr ( - );
679      "*",                int_int_fun_int_expr ( * );      "Pervasives", "*",     int_int_fun_int_expr ( * );
680      "/",                int_int_fun_int_expr ( / );      "Pervasives", "/",     int_int_fun_int_expr ( / );
681      "::",               cons_expr;      "Pervasives", "::",    cons_expr;
682      "()",               UnitExpr ();      "Pervasives", "()",    UnitExpr ();
683      "[]",               ListExpr [];      "Pervasives", "[]",    ListExpr [];
684      "True",             BoolExpr true;      "Pervasives", "True",  BoolExpr true;
685      "False",            BoolExpr false]      "Pervasives", "False", BoolExpr false]
   
   
 let rec add_resources base = function  
    (name, expr) :: tl ->  
       add_resources (Expr (name, expr, base)) tl  
  | [] ->  
       base  
   
 (*!  
  * @begin[doc]  
  * Toplevel values are added to the @Comment!resource[toploop_resource] resource.  
  * The argument has type @code{string * expr}, which includes  
  * the string name of the value, and it's value.  
  * @docoff  
  * @end[doc]  
  *)  
 let resource toploop = {  
    resource_empty = add_resources Empty values;  
    resource_join = join_resource;  
    resource_extract = extract_resource;  
    resource_improve = improve_resource;  
    resource_improve_arg = Mp_resource.improve_arg_fail "toploop_resource";  
    resource_close = close_resource  
 }  
   
 let get_resource modname =  
    Mp_resource.find toploop_resource modname  
686    
687  let expr_of_ocaml_expr = mk_expr  let expr_of_ocaml_expr = mk_expr
688  let expr_of_ocaml_str_item = mk_str_item  let expr_of_ocaml_str_item = mk_str_item

Legend:
Removed from v.3278  
changed lines
  Added in v.3292

  ViewVC Help
Powered by ViewVC 1.1.26