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

Diff of /metaprl/library/db.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 50  Line 50 
50    
51  open Opname  open Opname
52    
53    
54    
55  let _ =  let _ =
56     show_loading "Loading Db%t"     show_loading "Loading Db%t"
57    
# Line 58  Line 60 
60  let compression_code_p          = mask_p 0x80  let compression_code_p          = mask_p 0x80
61  let compression_add_byte_p      = mask_p 0xC0  let compression_add_byte_p      = mask_p 0xC0
62    
63    let make_term_scanner = make_scanner "\\ \n\r\t()[]{}:;.," "\n\t\r "
64    
65    let myscanner = ref (make_term_scanner (Stream.of_string "lori"))
66    
67  let index_of_bytes b c = ((b land 0x0F) lsl 8) + c  let index_of_bytes b c = ((b land 0x0F) lsl 8) + c
68    
# Line 172  Line 177 
177                                  ParamList pl -> pl                                  ParamList pl -> pl
178                                   | _ -> error ["read_term"; "operator"; "nuprl-light"; "opname"] [] [])))                                   | _ -> error ["read_term"; "operator"; "nuprl-light"; "opname"] [] [])))
179                  (tl parameters))                  (tl parameters))
180       else mk_nuprl5_op ((make_param (Token opid)) :: parameters)       else Nuprl5.mk_nuprl5_op ((make_param (Token opid)) :: parameters)
181    
182    
183    
# Line 183  Line 188 
188    | CParameter -> Parameter (scan_parameter scanner)    | CParameter -> Parameter (scan_parameter scanner)
189    | COperator -> Operator (scan_operator scanner)    | COperator -> Operator (scan_operator scanner)
190    | CTerm -> Term (scan_term scanner)    | CTerm -> Term (scan_term scanner)
191    | CNumeral -> raise (Invalid_argument "Db.scan_item: CNumeral case is not implemented")    | CNumeral -> Parameter (scan_numeral_parameter scanner)
192    
193  and scan_numeral_parameter scanner =  and scan_numeral_parameter scanner =
194   let l = scan_cur_byte scanner.scanner in  
195   let mp256 = num_of_int 256 in   (*error ["break"] [] []; *)
196     let mp256 = num_of_int 256 and mp0 = num_of_int 0 and mp1 = num_of_int 1 in
197    
198     let code = scan_cur_byte scanner.scanner in
199     (*print_string " code = "; print_string (string_of_int code);*)
200    let rec aux i mpexp acc =    let rec aux i mpexp acc =
201     scan_next scanner.scanner;      
202     if i = 0     if i = 0
203        then acc        then acc
204        else aux (i - 1) (mult_num mpexp mp256)     else (scan_bump scanner.scanner;
205                 (add_num acc (mult_num mpexp (num_of_int (scan_cur_byte scanner.scanner))))           let c = scan_cur_byte scanner.scanner in
206             (
207             aux (i - 1) (mult_num mpexp mp256)
208                   (add_num acc (mult_num mpexp (num_of_int c)))))
209    
210     in    in
211      
212      let value = aux code mp1 mp0 in
213    
214    let n = aux l (num_of_int 1) (num_of_int 0) in           (* print_string " scanned numeral ";
215      scan_byte scanner.scanner icolon;           print_string (string_of_num value);
216      let ptype = (scan_string scanner.scanner) in           scan_whitespace !myscanner ;
217        match ptype with "n" -> (Number n)           scan_bump scanner.scanner;
218        | "time" -> (ParamList [(make_param (Token "time"));           scan_whitespace !myscanner ;
219                            (make_param (Number n))])           print_string " scanned bump ";*)
220        | _ -> error ["read_term"; "numeral_parameter"; "MetaPRL"; ptype] [] []  
221             scan_next scanner.scanner;
222             scan_byte scanner.scanner icolon;
223    
224              (*let c = scan_cur_byte scanner.scanner in
225              print_string " code = "; print_string (string_of_int c);
226              scan_whitespace !myscanner ;
227              if scan_at_byte_p scanner.scanner icolon then scan_bump scanner.scanner;
228             scan_whitespace !myscanner ;*)
229    
230            myscanner := scanner.scanner;
231         let ptype = scan_string scanner.scanner in
232          match ptype with "n" -> make_param (Number value)
233          | "time" -> make_param (ParamList [(make_param (Token "time"));
234                              (make_param (Number value))])
235          | "ime" -> make_param (ParamList [(make_param (Token "time"));
236                              (make_param (Number value))])
237          | _ -> error ["scan_numeral_parameter"; ptype] [] []
238    
239    
240  and scan_numeral_parameter_old scanner =  and scan_numeral_parameter_old scanner =
# Line 221  Line 251 
251    let n = aux l mp256 in    let n = aux l mp256 in
252      scan_byte scanner.scanner icolon;      scan_byte scanner.scanner icolon;
253      let ptype = (scan_string scanner.scanner) in      let ptype = (scan_string scanner.scanner) in
254        match ptype with "n" -> (Number n)        match ptype with "n" -> make_param (Number n)
255        | "time" -> (ParamList [(make_param (Token "time"));        | "time" -> make_param (ParamList [(make_param (Token "time"));
256                            (make_param (Number n))])                            (make_param (Number n))])
257        | _ -> error ["read_term"; "numeral_parameter"; "MetaPRL"; ptype] [] []        | _ -> error ["scan_numeral_parameter_old"; ptype] [] []
258    
259    
260  and scan_compressed code scanner =  and scan_compressed_new code scanner =
261   if (compression_add_byte_p code)   if (compression_add_byte_p code)
262      then let ctype = (type_of_byte code) in      then let ctype = (type_of_byte code) in
263            scan_next scanner.scanner;            scan_next scanner.scanner;
264              levels_assign scanner code (function () -> scan_item ctype scanner)
265        else (scan_bump scanner.scanner;
266             (* print_string " scan compressed index "; *)
267             let r = levels_lookup scanner
268                                   (level_of_byte code)
269                                   (index_of_bytes code (scan_cur_byte scanner.scanner)) in
270               scan_next scanner.scanner;
271               r)
272    
273    and scan_compressed code scanner =
274     if compression_add_byte_p code
275        then let ctype = type_of_byte code in
276              scan_next scanner.scanner;
277            if ctype = CNumeral            if ctype = CNumeral
278              then Parameter (make_param (scan_numeral_parameter scanner))              then (let p = Parameter (scan_numeral_parameter scanner) in p)
279              else ((* print_string " scan compressed add "; *)              else ((* print_string " scan compressed add "; *)
280                    levels_assign scanner code (function () -> scan_item ctype scanner))                    levels_assign scanner code (function () -> scan_item ctype scanner))
281      else (scan_bump scanner.scanner;      else (scan_bump scanner.scanner;
          (* print_string " scan compressed index "; *)  
282           let r = levels_lookup scanner           let r = levels_lookup scanner
283                                 (level_of_byte code)                                 (level_of_byte code)
284                                 (index_of_bytes code (scan_cur_byte scanner.scanner)) in                                 (index_of_bytes code (scan_cur_byte scanner.scanner)) in
# Line 244  Line 286 
286             r)             r)
287    
288  and scan_binding scanner =  and scan_binding scanner =
289   let code = (scan_cur_byte scanner.scanner) in   let code = scan_cur_byte scanner.scanner in
290    if compression_code_p code    if compression_code_p code
291      then match (scan_compressed code scanner) with      then match (scan_compressed code scanner) with
292              Binding sl  -> sl              Binding sl  -> sl
293            |_ -> error ["read_term"; "binding"] [] []            |_ -> error ["read_term"; "binding"] [] []
294      else (scanner.stb (scan_string scanner.scanner))      else scanner.stb (scan_string scanner.scanner)
295    
296  and scan_parameter scanner =  and scan_parameter scanner =
297   let code = (scan_cur_byte scanner.scanner) in   let code = scan_cur_byte scanner.scanner in
298    (* print_string "code  "; print_string (string_of_int code); *)    (* print_string "code = "; print_string (string_of_int code); *)
299    if compression_code_p code    if compression_code_p code
300      then match (scan_compressed code scanner) with      then match (scan_compressed code scanner) with
301              Parameter p -> p          Parameter p -> p
302          | item ->          | item ->
303    
304    ((match item with    ((match item with
# Line 265  Line 307 
307     | Term p -> print_string "Term"     | Term p -> print_string "Term"
308     | Binding p -> print_string "Binding"     | Binding p -> print_string "Binding"
309     | Opid p -> print_string p; print_string "Opid");     | Opid p -> print_string p; print_string "Opid");
310          error ["read_term"; "parameter"] [] []    
311       error ["scan_parameter"; "not"] [] []
312     )     )
313    
314      else let s = (scan_string scanner.scanner) in    else let s = scan_string scanner.scanner in
315            scan_byte scanner.scanner icolon;            scan_byte scanner.scanner icolon;
316              (*myscanner := scanner.scanner;*)
317            scanner.stp s (scan_string scanner.scanner)            scanner.stp s (scan_string scanner.scanner)
318    
319  and scan_parameters scanner =  and scan_parameters scanner =
# Line 281  Line 325 
325    
326  and scan_operator scanner =  and scan_operator scanner =
327   (* print_string " sop "; *)   (* print_string " sop "; *)
328   let code = (scan_cur_byte scanner.scanner) in   let code = scan_cur_byte scanner.scanner in
329    if compression_code_p code    if compression_code_p code
330      then match (scan_compressed code scanner) with      then match (scan_compressed code scanner) with
331              Operator op -> op              Operator op -> op
# Line 294  Line 338 
338          | Term t  -> error ["read_term"; "operator"; "term"] [] [t]          | Term t  -> error ["read_term"; "operator"; "term"] [] [t]
339          *)          *)
340    
341      else (let opid = (scan_string scanner.scanner) in      else let opid = scan_string scanner.scanner in
342            let parms = (scan_parameters scanner) in            let parms = scan_parameters scanner in
343              (make_operator opid parms))              (make_operator opid parms)
344    
345  and scan_bound_term scanner =  and scan_bound_term scanner =
346   let code = (scan_cur_byte scanner.scanner) in   let code = (scan_cur_byte scanner.scanner) in
# Line 361  Line 405 
405    
406  and scan_term scanner =  and scan_term scanner =
407   (* print_string " st "; *)   (* print_string " st "; *)
408    
409   let code = scan_cur_byte scanner.scanner in   let code = scan_cur_byte scanner.scanner in
410     if (compression_code_p code)     if compression_code_p code
411        then match (scan_compressed code scanner) with        then match (scan_compressed code scanner) with
412                Opid s ->         let op = (make_operator s (scan_parameters scanner)) in                Opid s ->         let op = (make_operator s (scan_parameters scanner)) in
413                                    mk_term op (scan_bound_terms scanner)                                    mk_term op (scan_bound_terms scanner)
414              | Operator op ->    mk_term op (scan_bound_terms scanner)              | Operator op ->    mk_term op (scan_bound_terms scanner)
415              | Term term ->      term              | Term term ->      term
416              |_ -> error ["read_term"; "term"] [] []              |_ -> error ["read_term"; "term"] [] []
417        else let op = (scan_operator scanner) in        else let op = scan_operator scanner in
418                  let bterms = (scan_bound_terms scanner) in                  let bterms = (scan_bound_terms scanner) in
419                          mk_term op bterms                          mk_term op bterms
420    
# Line 378  Line 423 
423  let read_term_aux scanner stb stp =  let read_term_aux scanner stb stp =
424   scan_term (new_lscanner scanner stb stp)   scan_term (new_lscanner scanner stb stp)
425    
 let make_term_scanner = make_scanner "\\ \n\r\t()[]{}:;.," "\n\t\r "  
426    
427  let string_to_trivial_term s stp =  let string_to_trivial_term s stp =
428    read_term_aux    read_term_aux
# Line 481  Line 525 
525    | "t" -> (Token value)    | "t" -> (Token value)
526    | "s" -> (String value)    | "s" -> (String value)
527    | "q" -> (ParamList [(make_param (Token "quote")); (make_param (Token value))])    | "q" -> (ParamList [(make_param (Token "quote")); (make_param (Token value))])
528    | "b" -> ( ParamList [ ( make_param (Token "bool"))    | "b" -> ( ParamList [ (make_param (Token "bool"))
529                          ; if stringeq value "false"     then make_param (Number (Mp_num.num_of_int 0))                          ; if (stringeq value "false") or (stringeq value "F") then
530                            else if stringeq value "true" then make_param (Number (Mp_num.num_of_int 1))                            make_param (Number (Mp_num.num_of_int 0))
531                            else error ["real_parameter_from_string"; value][][]                            else if (stringeq value "true") or (stringeq value "T") then
532                              make_param (Number (Mp_num.num_of_int 1))
533                              else error ["real_parameter_from_string"; value] [] []
534                        ])                        ])
535    | "v" -> (Var value)    | "v" -> (Var value)
536    | "l" -> let level =    | "l" -> let level = scan_level_expression (make_le_scanner (Stream.of_string value)) in
       scan_level_expression (make_le_scanner (Stream.of_string value)) in  
537      (ParamList [(make_param (Token "nuprl5_level_expression")); (make_param (MLevel level)); (make_param (String value))])      (ParamList [(make_param (Token "nuprl5_level_expression")); (make_param (MLevel level)); (make_param (String value))])
538    | "oid" -> let term = string_to_trivial_term value stp in    | "oid" -> let term = string_to_trivial_term value stp in
539      (ObId (stamp_to_object_id (term_to_stamp term)))      (ObId (stamp_to_object_id (term_to_stamp term)))
540    | t -> failwith "unknown special op-param"    | "o" -> let term = string_to_trivial_term value stp in
541        (ObId (stamp_to_object_id (term_to_stamp term)))
542      | t -> failwith (String.concat "  " ["unknown special op-param"; ptype; value])
543    
544  let mk_meta_param_from_strings value ptype =  let mk_meta_param_from_strings value ptype =
545    match ptype with "n" -> (MNumber value)    match ptype with "n" -> (MNumber value)
# Line 542  Line 589 
589    
590    
591  let rec string_to_parameter s ptype =  let rec string_to_parameter s ptype =
592      (*if s = "!stamp" then failwith "stamp";*)
593    let len = String.length s in    let len = String.length s in
594    
595      if (len < 2 or not (chareq '%' (String_util.get "Db.string_to_parameter" s 0)))      if (len < 2 or not (chareq '%' (String_util.get "Db.string_to_parameter" s 0)))
# Line 746  Line 793 
793   loaded_levels := (index, (stamp, levels)) :: !loaded_levels   loaded_levels := (index, (stamp, levels)) :: !loaded_levels
794    
795    
   
796  let rec read_levels term index =  let rec read_levels term index =
797   (* print_string "read_levels "; Mbterm.print_term term; *)   (* print_string "read_levels "; Mbterm.print_term term; *)
798   if idata_persist_term_p term   if idata_persist_term_p term
# Line 803  Line 849 
849            session_read_term scanner )            session_read_term scanner )
850    else if (scan_at_char_p scanner.scanner 't')    else if (scan_at_char_p scanner.scanner 't')
851      then (scan_char scanner.scanner 't';      then (scan_char scanner.scanner 't';
852           let t = scan_term scanner in            let t = scan_term scanner in
853               (* print_newline(); print_string " after scan term "; Mbterm.print_term t; *)
854             scan_char scanner.scanner 't';             scan_char scanner.scanner 't';
855             t)             t)
856    else error ["session"; "read_term"; Char.escaped (scan_cur_char scanner.scanner)] [][]    else error ["session"; "read_term"; Char.escaped (scan_cur_char scanner.scanner)] [][]

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

  ViewVC Help
Powered by ViewVC 1.1.26