(************************************************************************)
   v       *    The Coq Proof Assistant   /   The Coq Development Team     
  < O _ _ _ , , *    INRIA - CNRS - LIX - LRI - PPS - Copyright 1999 - 2014     
    \VV/   * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

  Created by   for   as part of the 
    bytecode - based reduction machine , Oct 2004
   bytecode-based reduction machine, Oct 2004 *)
  Support for native arithmetics by   , May 2007

(* This file defines the type of bytecode instructions *)

open Names
open Term

type tag = int

let id_tag = 0
let iddef_tag = 1
let ind_tag = 2
let fix_tag = 3
let switch_tag = 4
let cofix_tag = 5
let cofix_evaluated_tag = 6

type structured_constant =
  | Const_sorts of sorts
  | Const_ind of inductive
  | Const_b0 of tag
  | Const_bn of tag * structured_constant array


type reloc_table = (tag * int) array

type annot_switch =
   {ci : case_info; rtbl : reloc_table; tailcall : bool}

module Label =
  struct
    type t = int
    let no = -1
    let counter = ref no
    let create () = incr counter; !counter
    let reset_label_counter () = counter := no
  end


type instruction =
  | Klabel of Label.t
  | Kacc of int
  | Kenvacc of int
  | Koffsetclosure of int
  | Kpush
  | Kpop of int
  | Kpush_retaddr of Label.t
  | Kapply of int                       (*  number of arguments *)
  | Kappterm of int * int               (* number of arguments, slot size *)
  | Kreturn of int                      (* slot size *)
  | Kjump
  | Krestart
  | Kgrab of int                        (* number of arguments *)
  | Kgrabrec of int                     (* rec arg *)
  | Kclosure of Label.t * int           (* label, number of free variables *)
  | Kclosurerec of int * int * Label.t array * Label.t array
                   (* nb fv, init, lbl types, lbl bodies *)
  | Kclosurecofix of int * int * Label.t array * Label.t array
                   (* nb fv, init, lbl types, lbl bodies *)
  | Kgetglobal of constant
  | Kconst of structured_constant
  | Kmakeblock of int * tag             (* size, tag *)
  | Kmakeprod
  | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
  | Kswitch of Label.t array * Label.t array (* consts,blocks *)
  | Kpushfields of int
  | Kfield of int
  | Ksetfield of int
  | Kstop
  | Ksequence of bytecodes * bytecodes
(* spiwack: instructions concerning integers *)
  | Kbranch of Label.t                  (* jump to label *)
  | Kaddint31                           (* adds the int31 in the accu
                                           and the one ontop of the stack *)
  | Kaddcint31                          (* makes the sum and keeps the carry *)
  | Kaddcarrycint31                     (* sum +1, keeps the carry *)
  | Ksubint31                           (* subtraction modulo *)
  | Ksubcint31                          (* subtraction, keeps the carry *)
  | Ksubcarrycint31                      (* subtraction -1, keeps the carry *)
  | Kmulint31                           (* multiplication modulo *)
  multiplication , result in two 
					    int31 , for exact computation
					   int31, for exact computation *)
  divides a double size integer 
                                            ( represented by an int31 in the 
					    accumulator and one on the top of 
					    the stack ) by an int31 . The result 
					    is a pair of the quotient and the 
					    rest . 
					    If the divisor is 0 , it returns 
					    0 .
                                           (represented by an int31 in the
					   accumulator and one on the top of
					   the stack) by an int31. The result
					   is a pair of the quotient and the
					   rest.
					   If the divisor is 0, it returns
					   0. *)
  | Kdivint31                           (* euclidian division (returns a pair
					   quotient,rest) *)
  generic operation for shifting and 
					    cycling . Takes 3 int31 i j and s , 
					    and returns x*2^s+y/(2^(31 - s )
					   cycling. Takes 3 int31 i j and s,
					   and returns x*2^s+y/(2^(31-s) *)
  | Kcompareint31                       (* unsigned comparison of int31
					   cf COMPAREINT31 in
					   kernel/byterun/coq_interp.c
					   for more info *)
  Give the numbers of 0 in head of a in31
  Give the numbers of 0 in tail of a in31 
                                            ie low bits
                                           ie low bits *)
  | Kisconst of Label.t                 (* conditional jump *)
  | Kareconst of int*Label.t            (* conditional jump *)
  | Kcompint31                          (* dynamic compilation of int31 *)
  | Kdecompint31                        (* dynamic decompilation of int31 *)
(* /spiwack *)

and bytecodes = instruction list

type fv_elem = FVnamed of identifier | FVrel of int

type fv = fv_elem array

(* spiwack: this exception is expected to be raised by function expecting
            closed terms. *)
exception NotClosed


 : both type have been moved from  because I needed then 
   for the retroknowledge
  for the retroknowledge *)
type vm_env = {
    size : int;              (* longueur de la liste [n] *)
  [ fvn ; ... ; fv1 ]
  }


type comp_env = {
  nbre de variables sur la pile          
    in_stack : int list;         (* position dans la pile                  *)
  nbre de fonctions mutuellement         
                                 (* recursives =  nbr                      *)
    pos_rec  : instruction list; (* instruction d'acces pour les variables *)
                                 (*  de point fix ou de cofix              *)
    offset : int;
    in_env : vm_env ref
  }



(* --- Pretty print *)
open Format
let rec instruction ppf = function
  | Klabel lbl -> fprintf ppf "L%i:" lbl
  | Kacc n -> fprintf ppf "\tacc %i" n
  | Kenvacc n -> fprintf ppf "\tenvacc %i" n
  | Koffsetclosure n -> fprintf ppf "\toffsetclosure %i" n
  | Kpush -> fprintf ppf "\tpush"
  | Kpop n -> fprintf ppf "\tpop %i" n
  | Kpush_retaddr lbl -> fprintf ppf "\tpush_retaddr L%i" lbl
  | Kapply n -> fprintf ppf "\tapply %i" n
  | Kappterm(n, m) ->
      fprintf ppf "\tappterm %i, %i" n m
  | Kreturn n -> fprintf ppf "\treturn %i" n
  | Kjump -> fprintf ppf "\tjump"
  | Krestart -> fprintf ppf "\trestart"
  | Kgrab n -> fprintf ppf "\tgrab %i" n
  | Kgrabrec n -> fprintf ppf "\tgrabrec %i" n
  | Kclosure(lbl, n) ->
      fprintf ppf "\tclosure L%i, %i" lbl n
  | Kclosurerec(fv,init,lblt,lblb) ->
      fprintf ppf "\tclosurerec";
      fprintf ppf "%i , %i, " fv init;
      print_string "types = ";
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
      print_string " bodies = ";
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
  | Kclosurecofix (fv,init,lblt,lblb) ->
      fprintf ppf "\tclosurecofix";
      fprintf ppf " %i , %i, " fv init;
      print_string "types = ";
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
      print_string " bodies = ";
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
  | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
  | Kconst cst ->
      fprintf ppf "\tconst"
  | Kmakeblock(n, m) ->
      fprintf ppf "\tmakeblock %i, %i" n m
  | Kmakeprod -> fprintf ppf "\tmakeprod"
  | Kmakeswitchblock(lblt,lbls,_,sz) ->
      fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz
  | Kswitch(lblc,lblb) ->
      fprintf ppf "\tswitch";
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc;
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
  | Kpushfields n -> fprintf ppf "\tpushfields %i" n
  | Ksetfield n -> fprintf ppf "\tsetfield %i" n
  | Kfield  n -> fprintf ppf "\tgetfield %i" n
  | Kstop -> fprintf ppf "\tstop"
  | Ksequence (c1,c2) ->
      fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2
(* spiwack *)
  | Kbranch lbl -> fprintf ppf "\tbranch %i" lbl
  | Kaddint31 -> fprintf ppf "\taddint31"
  | Kaddcint31 -> fprintf ppf "\taddcint31"
  | Kaddcarrycint31 -> fprintf ppf "\taddcarrycint31"
  | Ksubint31 -> fprintf ppf "\tsubint31"
  | Ksubcint31 -> fprintf ppf "\tsubcint31"
  | Ksubcarrycint31 -> fprintf ppf "\tsubcarrycint31"
  | Kmulint31 -> fprintf ppf "\tmulint31"
  | Kmulcint31 -> fprintf ppf "\tmulcint31"
  | Kdiv21int31 -> fprintf ppf "\tdiv21int31"
  | Kdivint31 -> fprintf ppf "\tdivint31"
  | Kcompareint31 -> fprintf ppf "\tcompareint31"
  | Khead0int31 -> fprintf ppf "\thead0int31"
  | Ktail0int31 -> fprintf ppf "\ttail0int31"
  | Kaddmuldivint31 -> fprintf ppf "\taddmuldivint31"
  | Kisconst lbl -> fprintf ppf "\tisconst %i" lbl
  | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl
  | Kcompint31 -> fprintf ppf "\tcompint31"
  | Kdecompint31 -> fprintf ppf "\tdecompint"

(* /spiwack *)


and instruction_list ppf = function
    [] -> ()
  | Klabel lbl :: il ->
      fprintf ppf "L%i:%a" lbl instruction_list il
  | instr :: il ->
      fprintf ppf "%a@ %a" instruction instr instruction_list il


 : moved this type in this file   because I needed it for 
   retroknowledge which ca n't depend from 
  retroknowledge which can't depend from cbytegen *)
type block =
  | Bconstr of constr
  | Bstrconst of structured_constant
  | Bmakeblock of int * block array
  | Bconstruct_app of int * int * int * block array
                  (* tag , nparams, arity *)
  | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
                (* spiwack: compilation given by a function *)
  compilation function ( see  in 
                    retroknowledge.mli for more info ) , argument array  
                   retroknowledge.mli for more info) , argument array  *)



let draw_instr c =
  fprintf std_formatter "@[<v 0>%a@]" instruction_list c

**********************************************************************
    //   *      This file is distributed under the terms of the       
         *       GNU Lesser General Public License Version 2.1        
**********************************************************************
 This file defines the type of bytecode instructions 
  number of arguments 
 number of arguments, slot size 
 slot size 
 number of arguments 
 rec arg 
 label, number of free variables 
 nb fv, init, lbl types, lbl bodies 
 nb fv, init, lbl types, lbl bodies 
 size, tag 
 consts,blocks 
 spiwack: instructions concerning integers 
 jump to label 
 adds the int31 in the accu
                                           and the one ontop of the stack 
 makes the sum and keeps the carry 
 sum +1, keeps the carry 
 subtraction modulo 
 subtraction, keeps the carry 
 subtraction -1, keeps the carry 
 multiplication modulo 
 euclidian division (returns a pair
					   quotient,rest) 
 unsigned comparison of int31
					   cf COMPAREINT31 in
					   kernel/byterun/coq_interp.c
					   for more info 
 conditional jump 
 conditional jump 
 dynamic compilation of int31 
 dynamic decompilation of int31 
 /spiwack 
 spiwack: this exception is expected to be raised by function expecting
            closed terms. 
 longueur de la liste [n] 
 position dans la pile                  
 recursives =  nbr                      
 instruction d'acces pour les variables 
  de point fix ou de cofix              
 --- Pretty print 
 spiwack 
 /spiwack 
 tag , nparams, arity 
 spiwack: compilation given by a function 
   v       *    The Coq Proof Assistant   /   The Coq Development Team     
  < O _ _ _ , , *    INRIA - CNRS - LIX - LRI - PPS - Copyright 1999 - 2014     
    \VV/   * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  Created by   for   as part of the 
    bytecode - based reduction machine , Oct 2004
   bytecode-based reduction machine, Oct 2004 *)
  Support for native arithmetics by   , May 2007


open Names
open Term

type tag = int

let id_tag = 0
let iddef_tag = 1
let ind_tag = 2
let fix_tag = 3
let switch_tag = 4
let cofix_tag = 5
let cofix_evaluated_tag = 6

type structured_constant =
  | Const_sorts of sorts
  | Const_ind of inductive
  | Const_b0 of tag
  | Const_bn of tag * structured_constant array


type reloc_table = (tag * int) array

type annot_switch =
   {ci : case_info; rtbl : reloc_table; tailcall : bool}

module Label =
  struct
    type t = int
    let no = -1
    let counter = ref no
    let create () = incr counter; !counter
    let reset_label_counter () = counter := no
  end


type instruction =
  | Klabel of Label.t
  | Kacc of int
  | Kenvacc of int
  | Koffsetclosure of int
  | Kpush
  | Kpop of int
  | Kpush_retaddr of Label.t
  | Kjump
  | Krestart
  | Kclosurerec of int * int * Label.t array * Label.t array
  | Kclosurecofix of int * int * Label.t array * Label.t array
  | Kgetglobal of constant
  | Kconst of structured_constant
  | Kmakeprod
  | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
  | Kpushfields of int
  | Kfield of int
  | Ksetfield of int
  | Kstop
  | Ksequence of bytecodes * bytecodes
  multiplication , result in two 
					    int31 , for exact computation
					   int31, for exact computation *)
  divides a double size integer 
                                            ( represented by an int31 in the 
					    accumulator and one on the top of 
					    the stack ) by an int31 . The result 
					    is a pair of the quotient and the 
					    rest . 
					    If the divisor is 0 , it returns 
					    0 .
                                           (represented by an int31 in the
					   accumulator and one on the top of
					   the stack) by an int31. The result
					   is a pair of the quotient and the
					   rest.
					   If the divisor is 0, it returns
					   0. *)
  generic operation for shifting and 
					    cycling . Takes 3 int31 i j and s , 
					    and returns x*2^s+y/(2^(31 - s )
					   cycling. Takes 3 int31 i j and s,
					   and returns x*2^s+y/(2^(31-s) *)
  Give the numbers of 0 in head of a in31
  Give the numbers of 0 in tail of a in31 
                                            ie low bits
                                           ie low bits *)

and bytecodes = instruction list

type fv_elem = FVnamed of identifier | FVrel of int

type fv = fv_elem array

exception NotClosed


 : both type have been moved from  because I needed then 
   for the retroknowledge
  for the retroknowledge *)
type vm_env = {
  [ fvn ; ... ; fv1 ]
  }


type comp_env = {
  nbre de variables sur la pile          
  nbre de fonctions mutuellement         
    offset : int;
    in_env : vm_env ref
  }



open Format
let rec instruction ppf = function
  | Klabel lbl -> fprintf ppf "L%i:" lbl
  | Kacc n -> fprintf ppf "\tacc %i" n
  | Kenvacc n -> fprintf ppf "\tenvacc %i" n
  | Koffsetclosure n -> fprintf ppf "\toffsetclosure %i" n
  | Kpush -> fprintf ppf "\tpush"
  | Kpop n -> fprintf ppf "\tpop %i" n
  | Kpush_retaddr lbl -> fprintf ppf "\tpush_retaddr L%i" lbl
  | Kapply n -> fprintf ppf "\tapply %i" n
  | Kappterm(n, m) ->
      fprintf ppf "\tappterm %i, %i" n m
  | Kreturn n -> fprintf ppf "\treturn %i" n
  | Kjump -> fprintf ppf "\tjump"
  | Krestart -> fprintf ppf "\trestart"
  | Kgrab n -> fprintf ppf "\tgrab %i" n
  | Kgrabrec n -> fprintf ppf "\tgrabrec %i" n
  | Kclosure(lbl, n) ->
      fprintf ppf "\tclosure L%i, %i" lbl n
  | Kclosurerec(fv,init,lblt,lblb) ->
      fprintf ppf "\tclosurerec";
      fprintf ppf "%i , %i, " fv init;
      print_string "types = ";
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
      print_string " bodies = ";
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
  | Kclosurecofix (fv,init,lblt,lblb) ->
      fprintf ppf "\tclosurecofix";
      fprintf ppf " %i , %i, " fv init;
      print_string "types = ";
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
      print_string " bodies = ";
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
  | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
  | Kconst cst ->
      fprintf ppf "\tconst"
  | Kmakeblock(n, m) ->
      fprintf ppf "\tmakeblock %i, %i" n m
  | Kmakeprod -> fprintf ppf "\tmakeprod"
  | Kmakeswitchblock(lblt,lbls,_,sz) ->
      fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz
  | Kswitch(lblc,lblb) ->
      fprintf ppf "\tswitch";
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc;
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
  | Kpushfields n -> fprintf ppf "\tpushfields %i" n
  | Ksetfield n -> fprintf ppf "\tsetfield %i" n
  | Kfield  n -> fprintf ppf "\tgetfield %i" n
  | Kstop -> fprintf ppf "\tstop"
  | Ksequence (c1,c2) ->
      fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2
  | Kbranch lbl -> fprintf ppf "\tbranch %i" lbl
  | Kaddint31 -> fprintf ppf "\taddint31"
  | Kaddcint31 -> fprintf ppf "\taddcint31"
  | Kaddcarrycint31 -> fprintf ppf "\taddcarrycint31"
  | Ksubint31 -> fprintf ppf "\tsubint31"
  | Ksubcint31 -> fprintf ppf "\tsubcint31"
  | Ksubcarrycint31 -> fprintf ppf "\tsubcarrycint31"
  | Kmulint31 -> fprintf ppf "\tmulint31"
  | Kmulcint31 -> fprintf ppf "\tmulcint31"
  | Kdiv21int31 -> fprintf ppf "\tdiv21int31"
  | Kdivint31 -> fprintf ppf "\tdivint31"
  | Kcompareint31 -> fprintf ppf "\tcompareint31"
  | Khead0int31 -> fprintf ppf "\thead0int31"
  | Ktail0int31 -> fprintf ppf "\ttail0int31"
  | Kaddmuldivint31 -> fprintf ppf "\taddmuldivint31"
  | Kisconst lbl -> fprintf ppf "\tisconst %i" lbl
  | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl
  | Kcompint31 -> fprintf ppf "\tcompint31"
  | Kdecompint31 -> fprintf ppf "\tdecompint"



and instruction_list ppf = function
    [] -> ()
  | Klabel lbl :: il ->
      fprintf ppf "L%i:%a" lbl instruction_list il
  | instr :: il ->
      fprintf ppf "%a@ %a" instruction instr instruction_list il


 : moved this type in this file   because I needed it for 
   retroknowledge which ca n't depend from 
  retroknowledge which can't depend from cbytegen *)
type block =
  | Bconstr of constr
  | Bstrconst of structured_constant
  | Bmakeblock of int * block array
  | Bconstruct_app of int * int * int * block array
  | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
  compilation function ( see  in 
                    retroknowledge.mli for more info ) , argument array  
                   retroknowledge.mli for more info) , argument array  *)



let draw_instr c =
  fprintf std_formatter "@[<v 0>%a@]" instruction_list c
