/[mojave]/metaprl/theories/mc/mp_mc_connect_base.ml
ViewVC logotype

Diff of /metaprl/theories/mc/mp_mc_connect_base.ml

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

revision 3579 by emre, Sun Mar 31 02:48:35 2002 UTC revision 3580 by emre, Fri Apr 19 08:09:21 2002 UTC
# Line 429  Line 429 
429     else     else
430        raise (RefineError ("union_type_of_term", StringTermError        raise (RefineError ("union_type_of_term", StringTermError
431              ("not a union_type", t)))              ("not a union_type", t)))
432    
433    (*
434     * Convert to and from subscripting terms.
435     *)
436    
437    let term_of_sub_block b =
438       match b with
439          BlockSub ->    blockSub_term
440        | RawDataSub ->  rawDataSub_term
441        | TupleSub ->    tupleSub_term
442        | RawTupleSub -> rawTupleSub_term
443    
444    let sub_block_of_term t =
445       if is_blockSub_term t then
446          BlockSub
447       else if is_rawDataSub_term t then
448          RawDataSub
449       else if is_tupleSub_term t then
450          TupleSub
451       else if is_rawTupleSub_term t then
452          RawTupleSub
453    
454       else
455          raise (RefineError ("sub_block_of_term", StringTermError
456                ("not a sub_block", t)))
457    
458    let term_of_sub_value v =
459       match v with
460          PolySub ->           polySub_term
461        | RawIntSub (p, s) ->  mk_rawIntSub_term (term_of_int_precision p)
462                                                 (term_of_int_signed s)
463        | RawFloatSub p ->     mk_rawFloatSub_term (term_of_float_precision p)
464        | PointerSub ->        pointerSub_term
465        | FunctionSub ->       functionSub_term
466    
467    let sub_value_of_term t =
468       if is_polySub_term t then
469          PolySub
470       else if is_rawIntSub_term t then
471          let p, s = dest_rawIntSub_term t in
472             RawIntSub   (int_precision_of_term p)
473                         (int_signed_of_term s)
474       else if is_rawFloatSub_term t then
475          RawFloatSub (float_precision_of_term (dest_rawFloatSub_term t))
476       else if is_pointerSub_term t then
477          PointerSub
478       else if is_functionSub_term t then
479          FunctionSub
480    
481       else
482          raise (RefineError ("sub_value_of_term", StringTermError
483                ("not a sub_value", t)))
484    
485    let term_of_sub_index i =
486       match i with
487          ByteIndex -> byteIndex_term
488        | WordIndex -> wordIndex_term
489    
490    let sub_index_of_term t =
491       if is_byteIndex_term t then
492          ByteIndex
493       else if is_wordIndex_term t then
494          WordIndex
495    
496       else
497          raise (RefineError ("sub_index_of_term", StringTermError
498                ("not a sub_index", t)))
499    
500    let term_of_sub_script t =
501       match t with
502          IntIndex ->             intIndex_term
503        | RawIntIndex (p, s) ->   mk_rawIntIndex_term (term_of_int_precision p)
504                                                      (term_of_int_signed s)
505    
506    let sub_script_of_term t =
507       if is_intIndex_term t then
508          IntIndex
509       else if is_rawIntIndex_term t then
510          let p, s = dest_rawIntIndex_term t in
511             RawIntIndex (int_precision_of_term p)
512                         (int_signed_of_term s)
513    
514       else
515          raise (RefineError ("sub_script_of_term", StringTermError
516                ("not a sub_script", t)))
517    
518    let term_of_subop op =
519       mk_subop_term        (term_of_sub_block op.sub_block)
520                            (term_of_sub_value op.sub_value)
521                            (term_of_sub_index op.sub_index)
522                            (term_of_sub_script op.sub_script)
523    
524    let subop_of_term t =
525       if is_subop_term t then
526          let block, value, index, script = dest_subop_term t in
527             {  sub_block = sub_block_of_term block;
528                sub_value = sub_value_of_term value;
529                sub_index = sub_index_of_term index;
530                sub_script = sub_script_of_term script
531             }
532    
533       else
534          raise (RefineError ("subop_of_term", StringTermError
535                ("not a subop", t)))

Legend:
Removed from v.3579  
changed lines
  Added in v.3580

  ViewVC Help
Powered by ViewVC 1.1.26