From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- kernel/byterun/coq_fix_code.c | 30 +- kernel/byterun/coq_instruct.h | 14 +- kernel/byterun/coq_interp.c | 356 +++++++++++++------- kernel/byterun/coq_memory.c | 7 +- kernel/byterun/coq_memory.h | 1 - kernel/byterun/coq_values.c | 3 +- kernel/byterun/coq_values.h | 14 +- kernel/cbytecodes.ml | 31 +- kernel/cbytecodes.mli | 18 +- kernel/cbytegen.ml | 347 +++++++++++++------ kernel/cemitcodes.ml | 21 +- kernel/closure.ml | 21 +- kernel/closure.mli | 7 +- kernel/cooking.ml | 12 +- kernel/cooking.mli | 4 +- kernel/declarations.ml | 26 +- kernel/declarations.mli | 20 +- kernel/environ.ml | 27 +- kernel/environ.mli | 5 +- kernel/indtypes.ml | 14 +- kernel/inductive.ml | 119 +++---- kernel/inductive.mli | 11 +- kernel/mod_typing.ml | 6 +- kernel/modops.ml | 77 +++-- kernel/reduction.ml | 12 +- kernel/safe_typing.ml | 36 +- kernel/sign.ml | 5 +- kernel/sign.mli | 8 +- kernel/subtyping.ml | 35 +- kernel/term.ml | 12 +- kernel/term.mli | 10 +- kernel/term_typing.ml | 34 +- kernel/term_typing.mli | 11 +- kernel/typeops.ml | 68 +++- kernel/typeops.mli | 17 +- kernel/univ.ml | 6 +- kernel/vconv.ml | 360 ++------------------ kernel/vconv.mli | 25 +- kernel/vm.ml | 749 +++++++++++++++++++++--------------------- kernel/vm.mli | 65 ++-- 40 files changed, 1405 insertions(+), 1239 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 4616580d..70648b44 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -27,31 +27,31 @@ void init_arity () { /* instruction with zero operand */ arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]= arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]= - arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]=arity[PUSHACC6]= - arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]=arity[ENVACC4]= - arity[PUSHENVACC1]=arity[PUSHENVACC2]=arity[PUSHENVACC3]=arity[PUSHENVACC4]= - arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]= + arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]= + arity[PUSHACC6]=arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]= + arity[ENVACC3]=arity[ENVACC4]=arity[PUSHENVACC1]=arity[PUSHENVACC2]= + arity[PUSHENVACC3]=arity[PUSHENVACC4]=arity[APPLY1]=arity[APPLY2]= + arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]= arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]= arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]= + arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]= arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= - arity[ACCUMULATE]=arity[STOP]=arity[FORCE]=arity[MAKEPROD]= 0; + arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= 0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= - arity[PUSH_RETADDR]= - arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=arity[APPTERM3]=arity[RETURN]= - arity[GRAB]=arity[COGRAB]= - arity[OFFSETCLOSURE]=arity[PUSHOFFSETCLOSURE]= - arity[GETGLOBAL]=arity[PUSHGETGLOBAL]= - arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEACCU]= - arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=arity[PUSHFIELD]= - arity[ACCUMULATECOND]= 1; + arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]= + arity[APPTERM3]=arity[RETURN]=arity[GRAB]=arity[OFFSETCLOSURE]= + arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]= + arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]= + arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]= + arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=arity[ACCUMULATECOND]= 1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=2; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; /* instruction with arbitrary operands */ - arity[CLOSUREREC]=arity[SWITCH]=0; + arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0; } #endif /* THREADED_CODE */ @@ -150,7 +150,7 @@ value coq_tcode_of_code (value code, value size) { block_size = sizes >> 16; sizes = const_size + block_size; for(i=0; i 0) { coq_extra_args--; @@ -485,30 +504,6 @@ value coq_interprete Next; } - Instruct(COGRAB){ - int required = *pc++; - print_instr("COGRAB"); - if(forcable == Val_true) { - print_instr("true"); - /* L'instruction précédante est FORCE */ - if (coq_extra_args > 0) coq_extra_args--; - pc++; - forcable = Val_false; - } else { /* L'instruction précédante est APPLY */ - mlsize_t num_args, i; - num_args = 1 + coq_extra_args; /* arg1 + extra args */ - Alloc_small(accu, num_args + 2, Closure_tag); - Field(accu, 1) = coq_env; - for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i]; - Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */ - sp += num_args; - pc = (code_t)(sp[0]); - coq_env = sp[1]; - coq_extra_args = Long_val(sp[2]); - sp += 3; - } - Next; - } Instruct(GRABREC) { int rec_pos = *pc++; /* commence a zero */ print_instr("GRABREC"); @@ -607,7 +602,59 @@ value coq_interprete accu = accu + 2 * start * sizeof(value); Next; } - + + Instruct(CLOSURECOFIX){ + int nfunc = *pc++; + int nvars = *pc++; + int start = *pc++; + int i, j , size; + value * p; + print_instr("CLOSURECOFIX"); + if (nvars > 0) *--sp = accu; + /* construction du vecteur de type */ + Alloc_small(accu, nfunc, 0); + for(i = 0; i < nfunc; i++) { + Field(accu,i) = (value)(pc+pc[i]); + } + pc += nfunc; + *--sp=accu; + + /* Creation des blocks accumulate */ + for(i=0; i < nfunc; i++) { + Alloc_small(accu, 2, Accu_tag); + Code_val(accu) = accumulate; + Field(accu,1) = Val_int(1); + *--sp=accu; + } + /* creation des fonction cofix */ + + p = sp; + size = nfunc + nvars + 2; + for (i=0; i < nfunc; i++) { + + Alloc_small(accu, size, Closure_tag); + Code_val(accu) = pc+pc[i]; + for (j = 0; j < nfunc; j++) Field(accu, j+1) = p[j]; + Field(accu, size - 1) = p[nfunc]; + for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = p[j]; + *--sp = accu; + /* creation du block contenant le cofix */ + + Alloc_small(accu,1, ATOM_COFIX_TAG); + Field(accu, 0) = sp[0]; + *sp = accu; + /* mise a jour du block accumulate */ + CAML_MODIFY(&Field(p[i], 1),*sp); + sp++; + } + pc += nfunc; + accu = p[start]; + sp = p + nfunc + 1 + nvars; + print_instr("ici4"); + Next; + } + + Instruct(PUSHOFFSETCLOSURE) { print_instr("PUSHOFFSETCLOSURE"); *--sp = accu; @@ -644,7 +691,7 @@ value coq_interprete /* Access to global variables */ Instruct(PUSHGETGLOBAL) { - print_instr("PUSHGETGLOBAL"); + print_instr("PUSH"); *--sp = accu; } /* Fallthrough */ @@ -703,38 +750,27 @@ value coq_interprete accu = block; Next; } + Instruct(MAKEBLOCK4) { + tag_t tag = *pc++; + value block; + print_instr("MAKEBLOCK4"); + Alloc_small(block, 4, tag); + Field(block, 0) = accu; + Field(block, 1) = sp[0]; + Field(block, 2) = sp[1]; + Field(block, 3) = sp[2]; + sp += 3; + accu = block; + Next; + } /* Access to components of blocks */ - -/* Branches and conditional branches */ - Instruct(FORCE) { - print_instr("FORCE"); - if (Is_block(accu) && Tag_val(accu) == Closure_tag) { - forcable = Val_true; - /* On pousse l'addresse de retour et l'argument */ - sp -= 3; - sp[0] = (value) (pc - 1); - sp[1] = coq_env; - sp[2] = Val_long(coq_extra_args); - /* On evalue le cofix */ - coq_extra_args = 0; - pc = Code_val(accu); - coq_env = accu; - goto check_stacks; - } else { - if (Is_block(accu)) print_int(Tag_val(accu)); - else print_instr("Not a block"); - } - Next; - } - - Instruct(SWITCH) { uint32 sizes = *pc++; print_instr("SWITCH"); - print_int(sizes); + print_int(sizes & 0xFFFF); if (Is_block(accu)) { long index = Tag_val(accu); print_instr("block"); @@ -748,68 +784,79 @@ value coq_interprete } Next; } - Instruct(PUSHFIELD){ + + Instruct(PUSHFIELDS){ int i; int size = *pc++; - print_instr("PUSHFIELD"); + print_instr("PUSHFIELDS"); sp -= size; for(i=0;i fprintf ppf "\trestart" | Kgrab n -> fprintf ppf "\tgrab %i" n | Kgrabrec n -> fprintf ppf "\tgrabrec %i" n - | Kcograb n -> fprintf ppf "\tcograb %i" n | Kclosure(lbl, n) -> fprintf ppf "\tclosure L%i, %i" lbl n | Kclosurerec(fv,init,lblt,lblb) -> @@ -89,7 +98,13 @@ let rec instruction ppf = function Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt; print_string " bodies = "; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; - (* nb fv, init, lbl types, lbl bodies *) + | 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" @@ -98,13 +113,13 @@ let rec instruction ppf = function | Kmakeprod -> fprintf ppf "\tmakeprod" | Kmakeswitchblock(lblt,lbls,_,sz) -> fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz - | Kforce -> fprintf ppf "\tforce" | Kswitch(lblc,lblb) -> fprintf ppf "\tswitch"; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; - | Kpushfield n -> - fprintf ppf "\tpushfield %i" n + | 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 diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index a996f750..215b6ad4 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -3,6 +3,14 @@ open Term type tag = int +val id_tag : tag +val iddef_tag : tag +val ind_tag : tag +val fix_tag : tag +val switch_tag : tag +val cofix_tag : tag +val cofix_evaluated_tag : tag + type structured_constant = | Const_sorts of sorts | Const_ind of inductive @@ -37,21 +45,24 @@ type instruction = | Krestart | Kgrab of int (* number of arguments *) | Kgrabrec of int (* rec arg *) - | Kcograb of int (* number of arguments *) | 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 - | Kforce | Kswitch of Label.t array * Label.t array (* consts,blocks *) - | Kpushfield of int + | Kpushfields of int + | Kfield of int + | Ksetfield of int | Kstop | Ksequence of bytecodes * bytecodes + and bytecodes = instruction list type fv_elem = FVnamed of identifier | FVrel of int @@ -59,3 +70,4 @@ type fv_elem = FVnamed of identifier | FVrel of int type fv = fv_elem array val draw_instr : bytecodes -> unit + diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 041e0795..e1f89fad 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -6,35 +6,161 @@ open Term open Declarations open Pre_env -(*i Compilation des variables + calcul des variables libres *) -(* Representation des environnements machines : *) -(*[t0|C0| ... |tc|Cc| ... |t(nbr-1)|C(nbr-1)| fv1 | fv1 | .... | fvn] *) -(* ^<----------offset---------> *) - - -type fv = fv_elem list - -type vm_env = {size : int; fv_rev : fv} - (* size = n; fv_rev = [fvn; ... ;fv1] *) - -type t = { - nb_stack : int; (* nbre de variables sur la pile *) - in_stack : int list; (* position dans la pile *) - nb_rec : int; (* nbre de fonctions mutuellement recursives = - nbr *) - pos_rec : int; (* position de la fonction courante = c *) - offset : int; - in_env : vm_env ref - } - -let empty_fv = {size= 0; fv_rev = []} +(* Compilation des variables + calcul des variables libres *) + +(* Dans la machine virtuel il n'y a pas de difference entre les *) +(* fonctions et leur environnement *) + +(* Representation de l'environnements des fonctions : *) +(* [clos_t | code | fv1 | fv2 | ... | fvn ] *) +(* ^ *) +(* l'offset pour l'acces au variable libre est 1 (il faut passer le *) +(* pointeur de code). *) +(* Lors de la compilation, les variables libres sont stock'ees dans *) +(* [in_env] dans l'ordre inverse de la representation machine, ceci *) +(* permet de rajouter des nouvelles variables dans l'environnememt *) +(* facilement. *) +(* Les arguments de la fonction arrive sur la pile dans l'ordre de *) +(* l'application : f arg1 ... argn *) +(* - la pile est alors : *) +(* arg1 : ... argn : extra args : return addr : ... *) +(* Dans le corps de la fonction [arg1] est repr'esent'e par le de Bruijn *) +(* [n], [argn] par le de Bruijn [1] *) + +(* Representation des environnements des points fix mutuels : *) +(* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *) +(* ^<----------offset---------> *) +(* type = [Ct1 | .... | Ctn] *) +(* Ci est le code correspondant au corps du ieme point fix *) +(* Lors de l'evaluation d'un point fix l'environnement est un pointeur *) +(* sur la position correspondante a son code. *) +(* Dans le corps de chaque point fix le de Bruijn [nbr] represente, *) +(* le 1er point fix de la declaration mutuelle, le de Bruijn [1] le *) +(* nbr-ieme. *) +(* L'acces a ces variables se fait par l'instruction [Koffsetclosure] *) +(* (decalage de l'environnement) *) + +(* Ceci permet de representer tout les point fix mutuels en un seul bloc *) +(* [Ct1 | ... | Ctn] est un tableau contant le code d'evaluation des *) +(* types des points fixes, ils sont utilises pour tester la conversion *) +(* Leur environnement d'execution est celui du dernier point fix : *) +(* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *) +(* ^ *) + + +(* Representation des cofix mutuels : *) +(* a1 = [A_t | accumulate | [Cfx_t | fcofix1 ] ] *) +(* ... *) +(* anbr = [A_t | accumulate | [Cfx_t | fcofixnbr ] ] *) +(* *) +(* fcofix1 = [clos_t | code1 | a1 |...| anbr | fv1 |...| fvn | type] *) +(* ^ *) +(* ... *) +(* fcofixnbr = [clos_t | codenbr | a1 |...| anbr | fv1 |...| fvn | type] *) +(* ^ *) +(* Les block [ai] sont des fonctions qui accumulent leurs arguments : *) +(* ai arg1 argp ---> *) +(* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *) +(* Si un tel bloc arrive sur un [match] il faut forcer l'evaluation, *) +(* la fonction [fcofixi] est alors appliqu'ee a [ai'] [arg1] ... [argp] *) +(* A la fin de l'evaluation [ai'] est mis a jour avec le resultat de *) +(* l'evaluation : *) +(* ai' <-- *) +(* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *) +(* L'avantage de cette representation est qu'elle permet d'evaluer qu'une *) +(* fois l'application d'un cofix (evaluation lazy) *) +(* De plus elle permet de creer facilement des cycles quand les cofix ne *) +(* n'ont pas d'aruments, ex: *) +(* cofix one := cons 1 one *) +(* a1 = [A_t | accumulate | [Cfx_t|fcofix1] ] *) +(* fcofix1 = [clos_t | code | a1] *) +(* Quand on force l'evaluation de [a1] le resultat est *) +(* [cons_t | 1 | a1] *) +(* [a1] est mis a jour : *) +(* a1 = [A_t | accumulate | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ] *) +(* Le cycle est cree ... *) + +(* On conserve la fct de cofix pour la conversion *) + +type vm_env = { + size : int; (* longueur de la liste [n] *) + fv_rev : fv_elem list (* [fvn; ... ;fv1] *) + } + +let empty_fv = { size= 0; fv_rev = [] } + +type comp_env = { + nb_stack : int; (* nbre de variables sur la pile *) + in_stack : int list; (* position dans la pile *) + nb_rec : int; (* 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 + } let fv r = !(r.in_env) + +let empty_comp_env ()= + { nb_stack = 0; + in_stack = []; + nb_rec = 0; + pos_rec = []; + offset = 0; + in_env = ref empty_fv; + } + +(*i Creation functions for comp_env *) -(* [add_param n] rend la liste [sz+1;sz+2;...;sz+n] *) let rec add_param n sz l = if n = 0 then l else add_param (n - 1) sz (n+sz::l) + +let comp_env_fun arity = + { nb_stack = arity; + in_stack = add_param arity 0 []; + nb_rec = 0; + pos_rec = []; + offset = 1; + in_env = ref empty_fv + } + + +let comp_env_type rfv = + { nb_stack = 0; + in_stack = []; + nb_rec = 0; + pos_rec = []; + offset = 1; + in_env = rfv + } + +let comp_env_fix ndef curr_pos arity rfv = + let prec = ref [] in + for i = ndef downto 1 do + prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec + done; + { nb_stack = arity; + in_stack = add_param arity 0 []; + nb_rec = ndef; + pos_rec = !prec; + offset = 2 * (ndef - curr_pos - 1)+1; + in_env = rfv + } + +let comp_env_cofix ndef arity rfv = + let prec = ref [] in + for i = 1 to ndef do + prec := Kenvacc i :: !prec + done; + { nb_stack = arity; + in_stack = add_param arity 0 []; + nb_rec = ndef; + pos_rec = !prec; + offset = ndef+1; + in_env = rfv + } (* [push_param ] ajoute les parametres de fonction dans la pile *) let push_param n sz r = @@ -42,33 +168,16 @@ let push_param n sz r = nb_stack = r.nb_stack + n; in_stack = add_param n sz r.in_stack } -(* [push_local e sz] ajoute une nouvelle variable dans la pile a la position *) +(* [push_local e sz] ajoute une nouvelle variable dans la pile a la *) +(* position [sz] *) let push_local sz r = { r with nb_stack = r.nb_stack + 1; in_stack = (sz + 1) :: r.in_stack } -(* Table de relocation initiale *) -let empty () = - { nb_stack = 0; in_stack = []; - nb_rec = 0;pos_rec = 0; - offset = 0; in_env = ref empty_fv } -let init_fun arity = - { nb_stack = arity; in_stack = add_param arity 0 []; - nb_rec = 0; pos_rec = 0; - offset = 1; in_env = ref empty_fv } - -let init_type ndef rfv = - { nb_stack = 0; in_stack = []; - nb_rec = 0; pos_rec = 0; - offset = 2*(ndef-1)+1; in_env = rfv } - -let init_fix ndef pos_rec arity rfv = - { nb_stack = arity; in_stack = add_param arity 0 []; - nb_rec = ndef; pos_rec = pos_rec; - offset = 2 * (ndef - pos_rec - 1)+1; in_env = rfv} +(*i Compilation of variables *) let find_at el l = let rec aux n = function | [] -> raise Not_found @@ -87,24 +196,27 @@ let pos_named id r = let pos_rel i r sz = if i <= r.nb_stack then Kacc(sz - (List.nth r.in_stack (i-1))) - else if i <= r.nb_stack + r.nb_rec - then Koffsetclosure (2 * (r.nb_rec + r.nb_stack - r.pos_rec - i)) - else - let db = FVrel(i - r.nb_stack - r.nb_rec) in - let env = !(r.in_env) in - try Kenvacc(r.offset + env.size - (find_at db env.fv_rev)) - with Not_found -> - let pos = env.size in - r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; - Kenvacc(r.offset + pos) - + else + let i = i - r.nb_stack in + if i <= r.nb_rec then + try List.nth r.pos_rec (i-1) + with _ -> assert false + else + let i = i - r.nb_rec in + let db = FVrel(i) in + let env = !(r.in_env) in + try Kenvacc(r.offset + env.size - (find_at db env.fv_rev)) + with Not_found -> + let pos = env.size in + r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; + Kenvacc(r.offset + pos) (*i Examination of the continuation *) -(* Discard all instructions up to the next label. - This function is to be applied to the continuation before adding a - non-terminating instruction (branch, raise, return, appterm) - in front of it. *) +(* Discard all instructions up to the next label. *) +(* This function is to be applied to the continuation before adding a *) +(* non-terminating instruction (branch, raise, return, appterm) *) +(* in front of it. *) let rec discard_dead_code cont = cont (*function @@ -113,9 +225,9 @@ let rec discard_dead_code cont = cont | _ :: cont -> discard_dead_code cont *) -(* Return a label to the beginning of the given continuation. - If the sequence starts with a branch, use the target of that branch - as the label, thus avoiding a jump to a jump. *) +(* Return a label to the beginning of the given continuation. *) +(* If the sequence starts with a branch, use the target of that branch *) +(* as the label, thus avoiding a jump to a jump. *) let label_code = function | Klabel lbl :: _ as cont -> (lbl, cont) @@ -138,7 +250,7 @@ let rec is_tailcall = function | Klabel _ :: c -> is_tailcall c | _ -> None -(* Extention of the continuation ****) +(* Extention of the continuation *) (* Add a Kpop n instruction in front of a continuation *) let rec add_pop n = function @@ -150,15 +262,41 @@ let add_grab arity lbl cont = if arity = 1 then Klabel lbl :: cont else Krestart :: Klabel lbl :: Kgrab (arity - 1) :: cont - -(* Environnement global *****) +let add_grabrec rec_arg arity lbl cont = + if arity = 1 then + Klabel lbl :: Kgrabrec 0 :: Krestart :: cont + else + Krestart :: Klabel lbl :: Kgrabrec rec_arg :: + Krestart :: Kgrab (arity - 1) :: cont + +(* continuation of a cofix *) + +let cont_cofix arity = + (* accu = res *) + (* stk = ai::args::ra::... *) + (* ai = [At|accumulate|[Cfx_t|fcofix]|args] *) + [ Kpush; + Kpush; (* stk = res::res::ai::args::ra::... *) + Kacc 2; + Kfield 1; + Kfield 0; + Kmakeblock(2, cofix_evaluated_tag); + Kpush; (* stk = [Cfxe_t|fcofix|res]::res::ai::args::ra::...*) + Kacc 2; + Ksetfield 1; (* ai = [At|accumulate|[Cfxe_t|fcofix|res]|args] *) + (* stk = res::ai::args::ra::... *) + Kacc 0; (* accu = res *) + Kreturn (arity+2) ] + + +(*i Global environment global *) let global_env = ref empty_env let set_global_env env = global_env := env -(* Code des fermetures ****) +(* Code des fermetures *) let fun_code = ref [] let init_fun_code () = fun_code := [] @@ -259,6 +397,14 @@ let compile_fv_elem reloc fv sz cont = | FVrel i -> pos_rel i reloc sz :: cont | FVnamed id -> pos_named id reloc :: cont +let rec compile_fv reloc l sz cont = + match l with + | [] -> cont + | [fvn] -> compile_fv_elem reloc fvn sz cont + | fvn :: tl -> + compile_fv_elem reloc fvn sz + (Kpush :: compile_fv reloc tl (sz + 1) cont) + (* compilation des constantes *) let rec get_allias env kn = @@ -271,8 +417,8 @@ let rec get_allias env kn = let rec compile_constr reloc c sz cont = match kind_of_term c with - | Meta _ -> raise (Invalid_argument "Cbytegen.gen_lam : Meta") - | Evar _ -> raise (Invalid_argument "Cbytegen.gen_lam : Evar") + | Meta _ -> raise (Invalid_argument "Cbytegen.compile_constr : Meta") + | Evar _ -> raise (Invalid_argument "Cbytegen.compile_constr : Evar") | Cast(c,_,_) -> compile_constr reloc c sz cont @@ -294,7 +440,7 @@ let rec compile_constr reloc c sz cont = | Lambda _ -> let params, body = decompose_lam c in let arity = List.length params in - let r_fun = init_fun arity in + let r_fun = comp_env_fun arity in let lbl_fun = Label.create() in let cont_fun = compile_constr r_fun body arity [Kreturn arity] in @@ -314,11 +460,11 @@ let rec compile_constr reloc c sz cont = let lbl_types = Array.create ndef Label.no in let lbl_bodies = Array.create ndef Label.no in (* Compilation des types *) - let rtype = init_type ndef rfv in + let env_type = comp_env_type rfv in for i = 0 to ndef - 1 do let lbl,fcode = label_code - (compile_constr rtype type_bodies.(i) 0 [Kstop]) in + (compile_constr env_type type_bodies.(i) 0 [Kstop]) in lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; @@ -326,18 +472,12 @@ let rec compile_constr reloc c sz cont = for i = 0 to ndef - 1 do let params,body = decompose_lam rec_bodies.(i) in let arity = List.length params in - let rbody = init_fix ndef i arity rfv in + let env_body = comp_env_fix ndef i arity rfv in let cont1 = - compile_constr rbody body arity [Kreturn arity] in + compile_constr env_body body arity [Kreturn arity] in let lbl = Label.create () in lbl_bodies.(i) <- lbl; - let fcode = - if arity = 1 then - Klabel lbl :: Kgrabrec 0 :: Krestart :: cont1 - else - Krestart :: Klabel lbl :: Kgrabrec rec_args.(i) :: - Krestart :: Kgrab (arity - 1) :: cont1 - in + let fcode = add_grabrec rec_args.(i) arity lbl cont1 in fun_code := [Ksequence(fcode,!fun_code)] done; let fv = !rfv in @@ -346,15 +486,15 @@ let rec compile_constr reloc c sz cont = | CoFix(init,(_,type_bodies,rec_bodies)) -> let ndef = Array.length type_bodies in - let rfv = ref empty_fv in let lbl_types = Array.create ndef Label.no in let lbl_bodies = Array.create ndef Label.no in (* Compilation des types *) - let rtype = init_type ndef rfv in + let rfv = ref empty_fv in + let env_type = comp_env_type rfv in for i = 0 to ndef - 1 do let lbl,fcode = label_code - (compile_constr rtype type_bodies.(i) 0 [Kstop]) in + (compile_constr env_type type_bodies.(i) 0 [Kstop]) in lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; @@ -362,21 +502,18 @@ let rec compile_constr reloc c sz cont = for i = 0 to ndef - 1 do let params,body = decompose_lam rec_bodies.(i) in let arity = List.length params in - let rbody = init_fix ndef i arity rfv in + let env_body = comp_env_cofix ndef arity rfv in let lbl = Label.create () in - let cont1 = - compile_constr rbody body arity [Kreturn(arity)] in + compile_constr env_body body (arity+1) (cont_cofix arity) in let cont2 = - if arity <= 1 then cont1 else Kgrab (arity - 1) :: cont1 in - let cont3 = - Krestart :: Klabel lbl :: Kcograb arity :: Krestart :: cont2 in - fun_code := [Ksequence(cont3,!fun_code)]; - lbl_bodies.(i) <- lbl + add_grab (arity+1) lbl cont1 in + lbl_bodies.(i) <- lbl; + fun_code := [Ksequence(cont2,!fun_code)]; done; let fv = !rfv in compile_fv reloc fv.fv_rev sz - (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont) + (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) | Case(ci,t,a,branchs) -> let ind = ci.ci_ind in @@ -418,12 +555,12 @@ let rec compile_constr reloc c sz cont = let lbl_b,code_b = label_code( if nargs = arity then - Kpushfield arity :: + Kpushfields arity :: compile_constr (push_param arity sz_b reloc) body (sz_b+arity) (add_pop arity (branch :: !c)) else let sz_appterm = if is_tailcall then sz_b + arity else arity in - Kpushfield arity :: + Kpushfields arity :: compile_constr reloc branchs.(i) (sz_b+arity) (Kappterm(arity,sz_appterm) :: !c)) in @@ -436,17 +573,8 @@ let rec compile_constr reloc c sz cont = | Klabel lbl -> Kpush_retaddr lbl :: !c | _ -> !c in - let cont_a = if mib.mind_finite then code_sw else Kforce :: code_sw in - compile_constr reloc a sz cont_a - -and compile_fv reloc l sz cont = - match l with - | [] -> cont - | [fvn] -> compile_fv_elem reloc fvn sz cont - | fvn :: tl -> - compile_fv_elem reloc fvn sz - (Kpush :: compile_fv reloc tl (sz + 1) cont) - + compile_constr reloc a sz code_sw + and compile_str_cst reloc sc sz cont = match sc with | Bconstr c -> compile_constr reloc c sz cont @@ -465,9 +593,18 @@ let compile env c = set_global_env env; init_fun_code (); Label.reset_label_counter (); - let reloc = empty () in + let reloc = empty_comp_env () in let init_code = compile_constr reloc c 0 [Kstop] in let fv = List.rev (!(reloc.in_env).fv_rev) in +(* draw_instr init_code; + draw_instr !fun_code; + Format.print_string "fv = "; + List.iter (fun v -> + match v with + | FVnamed id -> Format.print_string ((string_of_id id)^"; ") + | FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv; Format + .print_string "\n"; + Format.print_flush(); *) init_code,!fun_code, Array.of_list fv let compile_constant_body env body opaque boxed = diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index cccb1844..71a9aa0e 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -149,8 +149,6 @@ let emit_instr = function out opGRAB; out_int n | Kgrabrec(rec_arg) -> out opGRABREC; out_int rec_arg - | Kcograb n -> - out opCOGRAB; out_int n | Kclosure(lbl, n) -> out opCLOSURE; out_int n; out_label lbl | Kclosurerec(nfv,init,lbl_types,lbl_bodies) -> @@ -160,6 +158,13 @@ let emit_instr = function Array.iter (out_label_with_orig org) lbl_types; let org = !out_position in Array.iter (out_label_with_orig org) lbl_bodies + | Kclosurecofix(nfv,init,lbl_types,lbl_bodies) -> + out opCLOSURECOFIX;out_int (Array.length lbl_bodies); + out_int nfv; out_int init; + let org = !out_position in + Array.iter (out_label_with_orig org) lbl_types; + let org = !out_position in + Array.iter (out_label_with_orig org) lbl_bodies | Kgetglobal q -> out opGETGLOBAL; slot_for_getglobal q | Kconst((Const_b0 i)) -> @@ -178,16 +183,20 @@ let emit_instr = function out opMAKESWITCHBLOCK; out_label typlbl; out_label swlbl; slot_for_annot annot;out_int sz - | Kforce -> - out opFORCE | Kswitch (tbl_const, tbl_block) -> out opSWITCH; out_int (Array.length tbl_const + (Array.length tbl_block lsl 16)); let org = !out_position in Array.iter (out_label_with_orig org) tbl_const; Array.iter (out_label_with_orig org) tbl_block - | Kpushfield n -> - out opPUSHFIELD;out_int n + | Kpushfields n -> + out opPUSHFIELDS;out_int n + | Kfield n -> + if n <= 1 then out (opGETFIELD0+n) + else (out opGETFIELD;out_int n) + | Ksetfield n -> + if n <= 1 then out (opSETFIELD0+n) + else (out opSETFIELD;out_int n) | Kstop -> out opSTOP | Ksequence _ -> raise (Invalid_argument "Cemitcodes.emit_instr") diff --git a/kernel/closure.ml b/kernel/closure.ml index 617611bf..41fe8750 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: closure.ml 8802 2006-05-10 20:47:28Z barras $ *) +(* $Id: closure.ml 9215 2006-10-05 15:40:31Z herbelin $ *) open Util open Pp @@ -375,14 +375,17 @@ let defined_rels flags env = (rel_context env) ~init:(0,[]) (* else (0,[])*) - -let rec mind_equiv info kn1 kn2 = - kn1 = kn2 || - match (lookup_mind kn1 info.i_env).mind_equiv with - Some kn1' -> mind_equiv info kn2 kn1' - | None -> match (lookup_mind kn2 info.i_env).mind_equiv with - Some kn2' -> mind_equiv info kn2' kn1 - | None -> false +let rec mind_equiv env (kn1,i1) (kn2,i2) = + let rec equiv kn1 kn2 = + kn1 = kn2 || + match (lookup_mind kn1 env).mind_equiv with + Some kn1' -> equiv kn2 kn1' + | None -> match (lookup_mind kn2 env).mind_equiv with + Some kn2' -> equiv kn2' kn1 + | None -> false in + i1 = i2 && equiv kn1 kn2 + +let mind_equiv_infos info = mind_equiv info.i_env let create mk_cl flgs env = { i_flags = flgs; diff --git a/kernel/closure.mli b/kernel/closure.mli index feec8395..924da0a5 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: closure.mli 8793 2006-05-05 17:41:41Z barras $ i*) +(*i $Id: closure.mli 9215 2006-10-05 15:40:31Z herbelin $ i*) (*i*) open Pp @@ -179,8 +179,9 @@ val whd_stack : (* [unfold_reference] unfolds references in a [fconstr] *) val unfold_reference : clos_infos -> table_key -> fconstr option -(* [mind_equiv] checks whether two mutual inductives are intentionally equal *) -val mind_equiv : clos_infos -> mutual_inductive -> mutual_inductive -> bool +(* [mind_equiv] checks whether two inductive types are intentionally equal *) +val mind_equiv : env -> inductive -> inductive -> bool +val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool (************************************************************************) (*i This is for lazy debug *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 58c21d9f..6b2a6245 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cooking.ml 8752 2006-04-27 19:37:33Z herbelin $ i*) +(*i $Id: cooking.ml 9320 2006-10-30 16:53:43Z barras $ i*) open Pp open Util @@ -122,7 +122,13 @@ let cook_constant env r = on_body (fun c -> abstract_constant_body (expmod_constr r.d_modlist c) hyps) cb.const_body in - let typ = - abstract_constant_type (expmod_constr r.d_modlist cb.const_type) hyps in + let typ = match cb.const_type with + | NonPolymorphicType t -> + let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in + NonPolymorphicType typ + | PolymorphicArity (ctx,s) -> + let t = mkArity (ctx,Type s.poly_level) in + let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in + Typeops.make_polymorphic_if_arity env typ in let boxed = Cemitcodes.is_boxed cb.const_body_code in (body, typ, cb.const_constraints, cb.const_opaque, boxed) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7b51ac0c..93c2ccc9 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cooking.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id: cooking.mli 9310 2006-10-28 19:35:09Z herbelin $ i*) open Names open Term @@ -25,7 +25,7 @@ type recipe = { val cook_constant : env -> recipe -> - constr_substituted option * constr * constraints * bool * bool + constr_substituted option * constant_type * constraints * bool * bool (*s Utility functions used in module [Discharge]. *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index c52b5c48..e5e05eb3 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declarations.ml 8845 2006-05-23 07:41:58Z herbelin $ i*) +(*i $Id: declarations.ml 9310 2006-10-28 19:35:09Z herbelin $ i*) (*i*) open Util @@ -25,6 +25,15 @@ type engagement = ImpredicativeSet (*s Constants (internal representation) (Definition/Axiom) *) +type polymorphic_arity = { + poly_param_levels : universe option list; + poly_level : universe; +} + +type constant_type = + | NonPolymorphicType of types + | PolymorphicArity of rel_context * polymorphic_arity + type constr_substituted = constr substituted let from_val = from_val @@ -36,7 +45,7 @@ let subst_constr_subst = subst_substituted type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) const_body : constr_substituted option; - const_type : types; + const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted; (* const_type_code : Cemitcodes.to_patch; *) const_constraints : constraints; @@ -90,11 +99,6 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn *) -type polymorphic_inductive_arity = { - mind_param_levels : universe option list; - mind_level : universe; -} - type monomorphic_inductive_arity = { mind_user_arity : constr; mind_sort : sorts; @@ -102,7 +106,7 @@ type monomorphic_inductive_arity = { type inductive_arity = | Monomorphic of monomorphic_inductive_arity -| Polymorphic of polymorphic_inductive_arity +| Polymorphic of polymorphic_arity type one_inductive_body = { @@ -186,11 +190,15 @@ type mutual_inductive_body = { mind_equiv : kernel_name option } +let subst_arity sub = function +| NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) +| PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) + (* TODO: should be changed to non-coping after Term.subst_mps *) let subst_const_body sub cb = { const_hyps = (assert (cb.const_hyps=[]); []); const_body = option_map (subst_constr_subst sub) cb.const_body; - const_type = subst_mps sub cb.const_type; + const_type = subst_arity sub cb.const_type; const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) const_constraints = cb.const_constraints; diff --git a/kernel/declarations.mli b/kernel/declarations.mli index c96d2131..1eaeecb9 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declarations.mli 8845 2006-05-23 07:41:58Z herbelin $ i*) +(*i $Id: declarations.mli 9310 2006-10-28 19:35:09Z herbelin $ i*) (*i*) open Names @@ -26,6 +26,15 @@ type engagement = ImpredicativeSet (**********************************************************************) (*s Representation of constants (Definition/Axiom) *) +type polymorphic_arity = { + poly_param_levels : universe option list; + poly_level : universe; +} + +type constant_type = + | NonPolymorphicType of types + | PolymorphicArity of rel_context * polymorphic_arity + type constr_substituted val from_val : constr -> constr_substituted @@ -34,7 +43,7 @@ val force : constr_substituted -> constr type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) const_body : constr_substituted option; - const_type : types; + const_type : constant_type; const_body_code : to_patch_substituted; (*i const_type_code : to_patch;i*) const_constraints : constraints; @@ -70,11 +79,6 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths \end{verbatim} *) -type polymorphic_inductive_arity = { - mind_param_levels : universe option list; - mind_level : universe; -} - type monomorphic_inductive_arity = { mind_user_arity : constr; mind_sort : sorts; @@ -82,7 +86,7 @@ type monomorphic_inductive_arity = { type inductive_arity = | Monomorphic of monomorphic_inductive_arity -| Polymorphic of polymorphic_inductive_arity +| Polymorphic of polymorphic_arity type one_inductive_body = { diff --git a/kernel/environ.ml b/kernel/environ.ml index a1e19815..e73f5848 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: environ.ml 8810 2006-05-12 18:50:21Z barras $ *) +(* $Id: environ.ml 9201 2006-10-03 16:47:40Z notin $ *) open Util open Names @@ -245,6 +245,31 @@ let global_vars_set env constr = in filtrec Idset.empty constr +(* like [global_vars] but don't get through evars *) +let global_vars_set_drop_evar env constr = + let fold_constr_drop_evar f acc c = match kind_of_term c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> acc + | Cast (c,_,t) -> f (f acc c) t + | Prod (_,t,c) -> f (f acc t) c + | Lambda (_,t,c) -> f (f acc t) c + | LetIn (_,b,t,c) -> f (f (f acc b) t) c + | App (c,l) -> Array.fold_left f (f acc c) l + | Evar (_,l) -> acc + | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl + | Fix (_,(lna,tl,bl)) -> + let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in + Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd + | CoFix (_,(lna,tl,bl)) -> + let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in + Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd in + let rec filtrec acc c = + let vl = vars_of_global env c in + let acc = List.fold_right Idset.add vl acc in + fold_constr_drop_evar filtrec acc c + in + filtrec Idset.empty constr + (* [keep_hyps env ids] keeps the part of the section context of [env] which contains the variables of the set [ids], and recursively the variables contained in the types of the needed variables. *) diff --git a/kernel/environ.mli b/kernel/environ.mli index cfc23651..3728eea3 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: environ.mli 8810 2006-05-12 18:50:21Z barras $ i*) +(*i $Id: environ.mli 9310 2006-10-28 19:35:09Z herbelin $ i*) (*i*) open Names @@ -129,7 +129,7 @@ type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result val constant_value : env -> constant -> constr -val constant_type : env -> constant -> types +val constant_type : env -> constant -> constant_type val constant_opt_value : env -> constant -> constr option (************************************************************************) @@ -165,6 +165,7 @@ val set_engagement : engagement -> env -> env (* [global_vars_set env c] returns the list of [id]'s occurring as [VAR id] in [c] *) val global_vars_set : env -> constr -> Idset.t +val global_vars_set_drop_evar : env -> constr -> Idset.t (* the constr must be an atomic construction *) val vars_of_global : env -> constr -> identifier list diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e7dc09ee..1520e009 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indtypes.ml 8871 2006-05-28 16:46:48Z herbelin $ *) +(* $Id: indtypes.ml 9310 2006-10-28 19:35:09Z herbelin $ *) open Util open Names @@ -163,9 +163,13 @@ let small_unit constrsinfos = w1,w2,w3 <= u3 *) +let extract_level (_,_,_,lc,lev) = + (* Enforce that the level is not in Prop if more than two constructors *) + if Array.length lc >= 2 then sup base_univ lev else lev + let inductive_levels arities inds = let levels = Array.map pi3 arities in - let cstrs_levels = Array.map (fun (_,_,_,_,lev) -> lev) inds in + let cstrs_levels = Array.map extract_level inds in (* Take the transitive closure of the system of constructors *) (* level constraints and remove the recursive dependencies *) solve_constraints_system levels cstrs_levels @@ -388,7 +392,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = let specif = lookup_mind_specif env mi in let env' = push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive specif) lpar) env in + hnf_prod_applist env (type_of_inductive env specif) lpar) env in let ra_env' = (Imbr mi,Rtree.mk_param 0) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in @@ -597,8 +601,8 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = let arkind,kelim = match ar_kind with | Inr (param_levels,lev) -> Polymorphic { - mind_param_levels = param_levels; - mind_level = lev; + poly_param_levels = param_levels; + poly_level = lev; }, all_sorts | Inl ((issmall,isunit),ar,s) -> let isunit = isunit && ntypes = 1 && not (is_recursive recargs.(0)) in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 76553237..b7265e8c 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductive.ml 8972 2006-06-22 22:17:43Z herbelin $ *) +(* $Id: inductive.ml 9323 2006-10-30 23:05:29Z herbelin $ *) open Util open Names @@ -30,8 +30,8 @@ let lookup_mind_specif env (kn,tyi) = let find_rectype env c = let (t, l) = decompose_app (whd_betadeltaiota env c) in match kind_of_term t with - | Ind ind -> (ind, l) - | _ -> raise Not_found + | Ind ind -> (ind, l) + | _ -> raise Not_found let find_inductive env c = let (t, l) = decompose_app (whd_betadeltaiota env c) in @@ -122,14 +122,6 @@ where Remark: Set (predicative) is encoded as Type(0) *) -let set_inductive_level env s t = - let sign,s' = dest_prod_assum env t in - if family_of_sort s <> family_of_sort (destSort s') then - (* This induces reductions if user_arity <> nf_arity *) - mkArity (sign,s) - else - t - let sort_as_univ = function | Type u -> u | Prop Null -> neutral_univ @@ -139,44 +131,71 @@ let cons_subst u su subst = try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst with Not_found -> (u, su) :: subst -let rec make_subst env exp act = - match exp, act with - (* Bind expected levels of parameters to actual levels *) - | None :: exp, _ :: act -> - make_subst env exp act - | Some u :: exp, t :: act -> - let su = sort_as_univ (snd (dest_arity env t)) in - cons_subst u su (make_subst env exp act) - (* Not enough parameters, create a fresh univ *) - | Some u :: exp, [] -> - let su = fresh_local_univ () in - cons_subst u su (make_subst env exp []) - | None :: exp, [] -> - make_subst env exp [] - (* Uniform parameters are exhausted *) - | [], _ -> [] - -let sort_of_instantiated_universe mip subst level = - let level = subst_large_constraints subst level in - let nci = number_of_constructors mip in - if nci = 0 then mk_Prop - else - if is_empty_univ level then if nci = 1 then mk_Prop else mk_Set - else if is_base_univ level then mk_Set - else Type level - -let instantiate_inductive_with_param_levels env ar mip paramtyps = - let args = Array.to_list paramtyps in - let subst = make_subst env ar.mind_param_levels args in - sort_of_instantiated_universe mip subst ar.mind_level +let actualize_decl_level env lev t = + let sign,s = dest_arity env t in + mkArity (sign,lev) + +let polymorphism_on_non_applied_parameters = false + +(* Bind expected levels of parameters to actual levels *) +(* Propagate the new levels in the signature *) +let rec make_subst env = function + | (_,Some _,_ as t)::sign, exp, args -> + let ctx,subst = make_subst env (sign, exp, args) in + t::ctx, subst + | d::sign, None::exp, args -> + let args = match args with _::args -> args | [] -> [] in + let ctx,subst = make_subst env (sign, exp, args) in + d::ctx, subst + | d::sign, Some u::exp, a::args -> + (* We recover the level of the argument, but we don't change the *) + (* level in the corresponding type in the arity; this level in the *) + (* arity is a global level which, at typing time, will be enforce *) + (* to be greater than the level of the argument; this is probably *) + (* a useless extra constraint *) + let s = sort_as_univ (snd (dest_arity env a)) in + let ctx,subst = make_subst env (sign, exp, args) in + d::ctx, cons_subst u s subst + | (na,None,t as d)::sign, Some u::exp, [] -> + (* No more argument here: we instantiate the type with a fresh level *) + (* which is first propagated to the corresponding premise in the arity *) + (* (actualize_decl_level), then to the conclusion of the arity (via *) + (* the substitution) *) + let ctx,subst = make_subst env (sign, exp, []) in + if polymorphism_on_non_applied_parameters then + let s = fresh_local_univ () in + let t = actualize_decl_level env (Type s) t in + (na,None,t)::ctx, cons_subst u s subst + else + d::ctx, subst + | sign, [], _ -> + (* Uniform parameters are exhausted *) + sign,[] + | [], _, _ -> + assert false + +let instantiate_universes env ctx ar argsorts = + let args = Array.to_list argsorts in + let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in + let level = subst_large_constraints subst ar.poly_level in + ctx, + if is_empty_univ level then mk_Prop + else if is_base_univ level then mk_Set + else Type level let type_of_inductive_knowing_parameters env mip paramtyps = match mip.mind_arity with | Monomorphic s -> s.mind_user_arity | Polymorphic ar -> - let s = instantiate_inductive_with_param_levels env ar mip paramtyps in - mkArity (mip.mind_arity_ctxt,s) + let ctx = List.rev mip.mind_arity_ctxt in + let ctx,s = instantiate_universes env ctx ar paramtyps in + mkArity (List.rev ctx,s) + +(* Type of a (non applied) inductive type *) + +let type_of_inductive env (_,mip) = + type_of_inductive_knowing_parameters env mip [||] (* The max of an array of universes *) @@ -188,18 +207,6 @@ let cumulate_constructor_univ u = function let max_inductive_sort = Array.fold_left cumulate_constructor_univ neutral_univ -(* Type of a (non applied) inductive type *) - -let type_of_inductive (_,mip) = - match mip.mind_arity with - | Monomorphic s -> s.mind_user_arity - | Polymorphic s -> - let subst = map_succeed (function - | Some u -> (u, fresh_local_univ ()) - | None -> failwith "") s.mind_param_levels in - let s = mkSort (sort_of_instantiated_universe mip subst s.mind_level) in - it_mkProd_or_LetIn s mip.mind_arity_ctxt - (************************************************************************) (* Type of a constructor *) @@ -364,7 +371,7 @@ let inductive_equiv env (kn1,i1) (kn2,i2) = let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if - (indsp <> ci.ci_ind) or + not (Closure.mind_equiv env indsp ci.ci_ind) or (mib.mind_nparams <> ci.ci_npar) or (mip.mind_consnrealdecls <> ci.ci_cstr_nargs) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index d81904cc..b9d0f984 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: inductive.mli 8871 2006-05-28 16:46:48Z herbelin $ i*) +(*i $Id: inductive.mli 9314 2006-10-29 20:11:08Z herbelin $ i*) (*i*) open Names @@ -35,8 +35,9 @@ type mind_specif = mutual_inductive_body * one_inductive_body val lookup_mind_specif : env -> inductive -> mind_specif (*s Functions to build standard types related to inductive *) +val ind_subst : mutual_inductive -> mutual_inductive_body -> constr list -val type_of_inductive : mind_specif -> types +val type_of_inductive : env -> mind_specif -> types val elim_sorts : mind_specif -> sorts_family list @@ -49,6 +50,7 @@ val arities_of_constructors : inductive -> mind_specif -> types array (* Transforms inductive specification into types (in nf) *) val arities_of_specif : mutual_inductive -> mind_specif -> types array + (* [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression:

Cases (c :: (I args)) of b1..bn end @@ -78,10 +80,11 @@ val check_cofix : env -> cofixpoint -> unit val type_of_inductive_knowing_parameters : env -> one_inductive_body -> types array -> types -val set_inductive_level : env -> sorts -> types -> types - val max_inductive_sort : sorts array -> universe +val instantiate_universes : env -> Sign.rel_context -> + polymorphic_arity -> types array -> Sign.rel_context * sorts + (***************************************************************) (* Debug *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index a8aff184..663434ec 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mod_typing.ml 7639 2005-12-02 10:01:15Z gregoire $ i*) +(*i $Id: mod_typing.ml 9310 2006-10-28 19:35:09Z herbelin $ i*) open Util open Names @@ -87,8 +87,8 @@ and merge_with env mtb with_decl = match cb.const_body with | None -> let (j,cst1) = Typeops.infer env' c in - let cst2 = - Reduction.conv_leq env' j.uj_type cb.const_type in + let typ = Typeops.type_of_constant_type env' cb.const_type in + let cst2 = Reduction.conv_leq env' j.uj_type typ in let cst = Constraint.union (Constraint.union cb.const_constraints cst1) diff --git a/kernel/modops.ml b/kernel/modops.ml index b2f02a5f..5cc2a84d 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modops.ml 8879 2006-05-30 21:32:10Z letouzey $ i*) +(*i $Id: modops.ml 9138 2006-09-14 15:20:45Z jforest $ i*) (*i*) open Util @@ -170,34 +170,6 @@ and subst_module sub mb = let subst_signature_msid msid mp = subst_signature (map_msid msid mp) -let rec constants_of_specification env mp sign = - let aux res (l,elem) = - match elem with - | SPBconst cb -> ((make_con mp empty_dirpath l),cb)::res - | SPBmind _ -> res - | SPBmodule mb -> - (constants_of_modtype env (MPdot (mp,l)) - (module_body_of_spec mb).mod_type) @ res - | SPBmodtype mtb -> res (* ???? *) - in - List.fold_left aux [] sign - -and constants_of_modtype env mp modtype = - match scrape_modtype env modtype with - MTBident _ -> anomaly "scrape_modtype does not work!" - | MTBsig (msid,sign) -> - constants_of_specification env mp - (subst_signature_msid msid mp sign) - | MTBfunsig _ -> [] - -(* returns a resolver for kn that maps mbid to mp *) -(* Nota: Some delta-expansions used to happen here. - Browse SVN if you want to know more. *) -let resolver_of_environment mbid modtype mp env = - let constants = constants_of_modtype env (MPbound mbid) modtype in - let resolve = List.map (fun (con,_) -> con,None) constants in - Mod_subst.make_resolver resolve - (* we assume that the substitution of "mp" into "msid" is already done (or unnecessary) *) let rec add_signature mp sign env = @@ -224,6 +196,53 @@ and add_module mp mb env = | MTBfunsig _ -> env +let rec constants_of_specification env mp sign = + let aux (env,res) (l,elem) = + match elem with + | SPBconst cb -> env,((make_con mp empty_dirpath l),cb)::res + | SPBmind _ -> env,res + | SPBmodule mb -> + let new_env = add_module (MPdot (mp,l)) (module_body_of_spec mb) env in + new_env,(constants_of_modtype env (MPdot (mp,l)) + (module_body_of_spec mb).mod_type) @ res + | SPBmodtype mtb -> + (* module type dans un module type. + Il faut au moins mettre mtb dans l'environnement (avec le bon + kn pour pouvoir continuer aller deplier les modules utilisant ce + mtb + ex: + Module Type T1. + Module Type T2. + .... + End T2. + ..... + Declare Module M : T2. + End T2 + si on ne rajoute pas T2 dans l'environement de typage + on va exploser au moment du Declare Module + *) + let new_env = Environ.add_modtype (make_kn mp empty_dirpath l) mtb env in + new_env, constants_of_modtype env (MPdot(mp,l)) mtb @ res + in + snd (List.fold_left aux (env,[]) sign) + +and constants_of_modtype env mp modtype = + match scrape_modtype env modtype with + MTBident _ -> anomaly "scrape_modtype does not work!" + | MTBsig (msid,sign) -> + constants_of_specification env mp + (subst_signature_msid msid mp sign) + | MTBfunsig _ -> [] + +(* returns a resolver for kn that maps mbid to mp *) +(* Nota: Some delta-expansions used to happen here. + Browse SVN if you want to know more. *) +let resolver_of_environment mbid modtype mp env = + let constants = constants_of_modtype env (MPbound mbid) modtype in + let resolve = List.map (fun (con,_) -> con,None) constants in + Mod_subst.make_resolver resolve + + let strengthen_const env mp l cb = match cb.const_opaque, cb.const_body with | false, Some _ -> cb diff --git a/kernel/reduction.ml b/kernel/reduction.ml index bd849dad..701020d0 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: reduction.ml 8845 2006-05-23 07:41:58Z herbelin $ *) +(* $Id: reduction.ml 9215 2006-10-05 15:40:31Z herbelin $ *) open Util open Names @@ -257,14 +257,14 @@ and eqappr cv_pb infos appr1 appr2 cuniv = (* Inductive types: MutInd MutConstruct Fix Cofix *) - | (FInd (kn1,i1), FInd (kn2,i2)) -> - if i1 = i2 && mind_equiv infos kn1 kn2 + | (FInd ind1, FInd ind2) -> + if mind_equiv_infos infos ind1 ind2 then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible - | (FConstruct ((kn1,i1),j1), FConstruct ((kn2,i2),j2)) -> - if i1 = i2 && j1 = j2 && mind_equiv infos kn1 kn2 + | (FConstruct (ind1,j1), FConstruct (ind2,j2)) -> + if j1 = j2 && mind_equiv_infos infos ind1 ind2 then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible @@ -317,7 +317,7 @@ and eqappr cv_pb infos appr1 appr2 cuniv = and convert_stacks infos lft1 lft2 stk1 stk2 cuniv = compare_stacks (fun (l1,t1) (l2,t2) c -> ccnv CONV infos l1 l2 t1 t2 c) - (fun (mind1,i1) (mind2,i2) -> i1=i2 && mind_equiv infos mind1 mind2) + (mind_equiv_infos infos) lft1 stk1 lft2 stk2 cuniv and convert_vect infos lft1 lft2 v1 v2 cuniv = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 95092814..c4d9c991 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: safe_typing.ml 8898 2006-06-05 23:15:51Z letouzey $ *) +(* $Id: safe_typing.ml 9310 2006-10-28 19:35:09Z herbelin $ *) open Util open Names @@ -119,6 +119,12 @@ type global_declaration = | ConstantEntry of constant_entry | GlobalRecipe of Cooking.recipe +let hcons_constant_type = function + | NonPolymorphicType t -> + NonPolymorphicType (hcons1_constr t) + | PolymorphicArity (ctx,s) -> + PolymorphicArity (map_rel_context hcons1_constr ctx,s) + let hcons_constant_body cb = let body = match cb.const_body with None -> None @@ -127,28 +133,28 @@ let hcons_constant_body cb = in { cb with const_body = body; - const_type = hcons1_constr cb.const_type } + const_type = hcons_constant_type cb.const_type } let add_constant dir l decl senv = check_label l senv.labset; - let kn = make_con senv.modinfo.modpath dir l in + let kn = make_con senv.modinfo.modpath dir l in let cb = match decl with - | ConstantEntry ce -> translate_constant senv.env kn ce - | GlobalRecipe r -> - let cb = translate_recipe senv.env kn r in - if dir = empty_dirpath then hcons_constant_body cb else cb + | ConstantEntry ce -> translate_constant senv.env kn ce + | GlobalRecipe r -> + let cb = translate_recipe senv.env kn r in + if dir = empty_dirpath then hcons_constant_body cb else cb in let env' = Environ.add_constraints cb.const_constraints senv.env in let env'' = Environ.add_constant kn cb env' in - kn, { old = senv.old; - env = env''; - modinfo = senv.modinfo; - labset = Labset.add l senv.labset; - revsign = (l,SPBconst cb)::senv.revsign; - revstruct = (l,SEBconst cb)::senv.revstruct; - imports = senv.imports; - loads = senv.loads } + kn, { old = senv.old; + env = env''; + modinfo = senv.modinfo; + labset = Labset.add l senv.labset; + revsign = (l,SPBconst cb)::senv.revsign; + revstruct = (l,SEBconst cb)::senv.revstruct; + imports = senv.imports; + loads = senv.loads } (* Insertion of inductive types. *) diff --git a/kernel/sign.ml b/kernel/sign.ml index 75342f2c..b42ca581 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: sign.ml 8845 2006-05-23 07:41:58Z herbelin $ *) +(* $Id: sign.ml 9103 2006-09-01 11:02:52Z herbelin $ *) open Names open Util @@ -83,6 +83,9 @@ let map_context f l = let map_rel_context = map_context let map_named_context = map_context +let iter_rel_context f = List.iter (fun (_,b,t) -> f t; option_iter f b) +let iter_named_context f = List.iter (fun (_,b,t) -> f t; option_iter f b) + (* Push named declarations on top of a rel context *) (* Bizarre. Should be avoided. *) let push_named_to_rel_context hyps ctxt = diff --git a/kernel/sign.mli b/kernel/sign.mli index 4a90302b..88e9dbf0 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: sign.mli 6737 2005-02-18 20:49:43Z herbelin $ i*) +(*i $Id: sign.mli 9103 2006-09-01 11:02:52Z herbelin $ i*) (*i*) open Names @@ -65,6 +65,12 @@ val map_rel_context : (constr -> constr) -> rel_context -> rel_context (*s Map function of [named_context] *) val map_named_context : (constr -> constr) -> named_context -> named_context +(*s Map function of [rel_context] *) +val iter_rel_context : (constr -> unit) -> rel_context -> unit + +(*s Map function of [named_context] *) +val iter_named_context : (constr -> unit) -> named_context -> unit + (*s Term constructors *) val it_mkLambda_or_LetIn : constr -> rel_context -> constr diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index bbc89e39..9a8de5a9 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtyping.ml 8845 2006-05-23 07:41:58Z herbelin $ i*) +(*i $Id: subtyping.ml 9310 2006-10-28 19:35:09Z herbelin $ i*) (*i*) open Util @@ -94,9 +94,9 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = (* listrec ignored *) (* finite done *) (* nparams done *) - (* params_ctxt done *) + (* params_ctxt done because part of the inductive types *) (* Don't check the sort of the type if polymorphic *) - let cst = check_conv cst conv env (type_of_inductive (mib1,p1)) (type_of_inductive (mib2,p2)) + let cst = check_conv cst conv env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2)) in cst in @@ -114,9 +114,12 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = assert (Array.length mib1.mind_packets >= 1 && Array.length mib2.mind_packets >= 1); - (* TODO: we should allow renaming of parameters at least ! *) + (* Check that the expected numbers of uniform parameters are the same *) + (* No need to check the contexts of parameters: it is checked *) + (* at the time of checking the inductive arities in check_packet. *) + (* Notice that we don't expect the local definitions to match: only *) + (* the inductive types and constructors types have to be convertible *) check (fun mib -> mib.mind_nparams); - check (fun mib -> mib.mind_params_ctxt); begin match mib2.mind_equiv with @@ -161,7 +164,9 @@ let check_constant cst env msid1 l info1 cb2 spec2 = | Constant cb1 -> assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; (*Start by checking types*) - let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in + let typ1 = Typeops.type_of_constant_type env cb1.const_type in + let typ2 = Typeops.type_of_constant_type env cb2.const_type in + let cst = check_conv cst conv_leq env typ1 typ2 in let con = make_con (MPself msid1) empty_dirpath l in let cst = match cb2.const_body with @@ -176,23 +181,27 @@ let check_constant cst env msid1 l info1 cb2 spec2 = in cst | IndType ((kn,i),mind1) -> - Util.error ("The kernel does not recognize yet that a parameter can be " ^ + ignore (Util.error ( + "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ - "name.") ; + "name.")); assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; if cb2.const_body <> None then error () ; - let arity1 = type_of_inductive (mind1,mind1.mind_packets.(i)) in - check_conv cst conv_leq env arity1 cb2.const_type + let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in + let typ2 = Typeops.type_of_constant_type env cb2.const_type in + check_conv cst conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - Util.error ("The kernel does not recognize yet that a parameter can be " ^ + ignore (Util.error ( + "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ - "name.") ; + "name.")); assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; if cb2.const_body <> None then error () ; let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in - check_conv cst conv env ty1 cb2.const_type + let ty2 = Typeops.type_of_constant_type env cb2.const_type in + check_conv cst conv env ty1 ty2 | _ -> error () let rec check_modules cst env msid1 l msb1 msb2 = diff --git a/kernel/term.ml b/kernel/term.ml index 228ae48a..456a29e4 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: term.ml 8850 2006-05-23 16:11:31Z herbelin $ *) +(* $Id: term.ml 9303 2006-10-27 21:50:17Z herbelin $ *) (* This module instantiates the structure of generic deBruijn terms to Coq *) @@ -646,6 +646,9 @@ type rel_declaration = name * constr option * types let map_named_declaration f (id, v, ty) = (id, option_map f v, f ty) let map_rel_declaration = map_named_declaration +let fold_named_declaration f (_, v, ty) a = f ty (option_fold_right f v a) +let fold_rel_declaration = fold_named_declaration + (****************************************************************************) (* Functions for dealing with constr terms *) (****************************************************************************) @@ -659,17 +662,16 @@ exception LocalOccur (* (closedn n M) raises FreeVar if a variable of height greater than n occurs in M, returns () otherwise *) -let closedn = +let closedn n c = let rec closed_rec n c = match kind_of_term c with | Rel m -> if m>n then raise LocalOccur | _ -> iter_constr_with_binders succ closed_rec n c in - closed_rec + try closed_rec n c; true with LocalOccur -> false (* [closed0 M] is true iff [M] is a (deBruijn) closed term *) -let closed0 term = - try closedn 0 term; true with LocalOccur -> false +let closed0 = closedn 0 (* (noccurn n M) returns true iff (Rel n) does NOT occur in term M *) diff --git a/kernel/term.mli b/kernel/term.mli index 8d72e0d8..d6244f5b 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: term.mli 8850 2006-05-23 16:11:31Z herbelin $ i*) +(*i $Id: term.mli 9303 2006-10-27 21:50:17Z herbelin $ i*) (*i*) open Names @@ -327,6 +327,11 @@ val map_named_declaration : val map_rel_declaration : (constr -> constr) -> rel_declaration -> rel_declaration +val fold_named_declaration : + (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a +val fold_rel_declaration : + (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a + (* Constructs either [(x:t)c] or [[x=b:t]c] *) val mkProd_or_LetIn : rel_declaration -> types -> types val mkNamedProd_or_LetIn : named_declaration -> types -> types @@ -426,6 +431,9 @@ val under_outer_cast : (constr -> constr) -> constr -> constr (*s Occur checks *) +(* [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *) +val closedn : int -> constr -> bool + (* [closed0 M] is true iff [M] is a (deBruijn) closed term *) val closed0 : constr -> bool diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index fde5fa25..575330a4 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: term_typing.ml 7639 2005-12-02 10:01:15Z gregoire $ *) +(* $Id: term_typing.ml 9323 2006-10-30 23:05:29Z herbelin $ *) open Util open Names @@ -23,7 +23,20 @@ open Indtypes open Typeops let constrain_type env j cst1 = function - | None -> j.uj_type, cst1 + | None -> +(* To have definitions in Type polymorphic + make_polymorphic_if_arity env j.uj_type, cst1 +*) + NonPolymorphicType j.uj_type, cst1 + | Some t -> + let (tj,cst2) = infer_type env t in + let (_,cst3) = judge_of_cast env j DEFAULTcast tj in + assert (t = tj.utj_val); + NonPolymorphicType t, Constraint.union (Constraint.union cst1 cst2) cst3 + +let local_constrain_type env j cst1 = function + | None -> + j.uj_type, cst1 | Some t -> let (tj,cst2) = infer_type env t in let (_,cst3) = judge_of_cast env j DEFAULTcast tj in @@ -32,7 +45,7 @@ let constrain_type env j cst1 = function let translate_local_def env (b,topt) = let (j,cst) = infer env b in - let (typ,cst) = constrain_type env j cst topt in + let (typ,cst) = local_constrain_type env j cst topt in (j.uj_val,typ,cst) let translate_local_assum env t = @@ -83,16 +96,25 @@ let infer_declaration env dcl = c.const_entry_opaque, c.const_entry_boxed | ParameterEntry t -> let (j,cst) = infer env t in - None, Typeops.assumption_of_judgment env j, cst, false, false + None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst, + false, false + +let global_vars_set_constant_type env = function + | NonPolymorphicType t -> global_vars_set env t + | PolymorphicArity (ctx,_) -> + Sign.fold_rel_context + (fold_rel_declaration + (fun t c -> Idset.union (global_vars_set env t) c)) + ctx ~init:Idset.empty let build_constant_declaration env kn (body,typ,cst,op,boxed) = let ids = match body with - | None -> global_vars_set env typ + | None -> global_vars_set_constant_type env typ | Some b -> Idset.union (global_vars_set env (Declarations.force b)) - (global_vars_set env typ) + (global_vars_set_constant_type env typ) in let tps = Cemitcodes.from_val (compile_constant_body env body op boxed) in let hyps = keep_hyps env ids in diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index cf111b6b..c102d01b 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: term_typing.mli 6245 2004-10-20 13:50:08Z barras $ i*) +(*i $Id: term_typing.mli 9310 2006-10-28 19:35:09Z herbelin $ i*) (*i*) open Names @@ -24,7 +24,14 @@ val translate_local_def : env -> constr * types option -> val translate_local_assum : env -> types -> types * Univ.constraints - + +val infer_declaration : env -> constant_entry -> + constr_substituted option * constant_type * constraints * bool * bool + +val build_constant_declaration : env -> 'a -> + constr_substituted option * constant_type * constraints * bool * bool -> + constant_body + val translate_constant : env -> constant -> constant_entry -> constant_body val translate_mind : diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 8299a3c9..2a0dd526 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: typeops.ml 8871 2006-05-28 16:46:48Z herbelin $ *) +(* $Id: typeops.ml 9314 2006-10-29 20:11:08Z herbelin $ *) open Util open Names @@ -49,8 +49,6 @@ let assumption_of_judgment env j = let sort_judgment env j = (type_judgment env j).utj_type -let on_judgment_type f j = { j with uj_type = f j.uj_type } - (************************************************) (* Incremental typing rules: builds a typing judgement given the *) (* judgements for the subterms. *) @@ -127,13 +125,52 @@ let check_hyps id env hyps = *) (* Instantiation of terms on real arguments. *) +(* Make a type polymorphic if an arity *) + +let extract_level env p = + let _,c = dest_prod_assum env p in + match kind_of_term c with Sort (Type u) -> Some u | _ -> None + +let extract_context_levels env = + List.fold_left + (fun l (_,b,p) -> if b=None then extract_level env p::l else l) [] + +let make_polymorphic_if_arity env t = + let params, ccl = dest_prod_assum env t in + match kind_of_term ccl with + | Sort (Type u) -> + let param_ccls = extract_context_levels env params in + let s = { poly_param_levels = param_ccls; poly_level = u} in + PolymorphicArity (params,s) + | _ -> + NonPolymorphicType t + (* Type of constants *) + +let type_of_constant_knowing_parameters env t paramtyps = + match t with + | NonPolymorphicType t -> t + | PolymorphicArity (sign,ar) -> + let ctx = List.rev sign in + let ctx,s = instantiate_universes env ctx ar paramtyps in + mkArity (List.rev ctx,s) + +let type_of_constant_type env t = + type_of_constant_knowing_parameters env t [||] + +let type_of_constant env cst = + type_of_constant_type env (constant_type env cst) + +let judge_of_constant_knowing_parameters env cst jl = + let c = mkConst cst in + let cb = lookup_constant cst env in + let _ = check_args env c cb.const_hyps in + let paramstyp = Array.map (fun j -> j.uj_type) jl in + let t = type_of_constant_knowing_parameters env cb.const_type paramstyp in + make_judge c t + let judge_of_constant env cst = - let constr = mkConst cst in - let _ = - let ce = lookup_constant cst env in - check_args env constr ce.const_hyps in - make_judge constr (constant_type env cst) + judge_of_constant_knowing_parameters env cst [||] (* Type of a lambda-abstraction. *) @@ -350,11 +387,16 @@ let rec execute env cstr cu = | App (f,args) -> let (jl,cu1) = execute_array env args cu in let (j,cu2) = - if isInd f then - (* Sort-polymorphism of inductive types *) - judge_of_inductive_knowing_parameters env (destInd f) jl, cu1 - else - execute env f cu1 + match kind_of_term f with + | Ind ind -> + (* Sort-polymorphism of inductive types *) + judge_of_inductive_knowing_parameters env ind jl, cu1 + | Const cst -> + (* Sort-polymorphism of constant *) + judge_of_constant_knowing_parameters env cst jl, cu1 + | _ -> + (* No sort-polymorphism *) + execute env f cu1 in univ_combinator cu2 (judge_of_apply env j jl) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 86a795b5..64a2f650 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: typeops.mli 8871 2006-05-28 16:46:48Z herbelin $ i*) +(*i $Id: typeops.mli 9314 2006-10-29 20:11:08Z herbelin $ i*) (*i*) open Names @@ -14,6 +14,7 @@ open Univ open Term open Environ open Entries +open Declarations (*i*) (*s Typing functions (not yet tagged as safe) *) @@ -33,8 +34,6 @@ val infer_local_decls : val assumption_of_judgment : env -> unsafe_judgment -> types val type_judgment : env -> unsafe_judgment -> unsafe_type_judgment -val on_judgment_type : - (types -> types) -> unsafe_judgment -> unsafe_judgment (*s Type of sorts. *) val judge_of_prop_contents : contents -> unsafe_judgment @@ -49,6 +48,9 @@ val judge_of_variable : env -> variable -> unsafe_judgment (*s type of a constant *) val judge_of_constant : env -> constant -> unsafe_judgment +val judge_of_constant_knowing_parameters : + env -> constant -> unsafe_judgment array -> unsafe_judgment + (*s Type of application. *) val judge_of_apply : env -> unsafe_judgment -> unsafe_judgment array @@ -95,3 +97,12 @@ val type_fixpoint : env -> name array -> types array (* Kernel safe typing but applicable to partial proofs *) val typing : env -> constr -> unsafe_judgment +val type_of_constant : env -> constant -> types + +val type_of_constant_type : env -> constant_type -> types + +val type_of_constant_knowing_parameters : + env -> constant_type -> constr array -> types + +(* Make a type polymorphic if an arity *) +val make_polymorphic_if_arity : env -> types -> constant_type diff --git a/kernel/univ.ml b/kernel/univ.ml index e76b7b02..775e505f 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: univ.ml 8845 2006-05-23 07:41:58Z herbelin $ *) +(* $Id: univ.ml 9314 2006-10-29 20:11:08Z herbelin $ *) (* Initial Caml version originates from CoC 4.8 [Dec 1988] *) (* Extension with algebraic universes by HH [Sep 2001] *) @@ -63,8 +63,8 @@ let pr_uni_level u = str (string_of_univ_level u) let pr_uni = function | Atom u -> pr_uni_level u - | Max ([],[Base]) -> - int 1 + | Max ([],[u]) -> + str "(" ++ pr_uni_level u ++ str ")+1" | Max (gel,gtl) -> str "max(" ++ hov 0 (prlist_with_sep pr_coma pr_uni_level gel ++ diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 653f8978..7c515735 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -17,7 +17,7 @@ let val_of_constr env c = let compare_zipper z1 z2 = match z1, z2 with | Zapp args1, Zapp args2 -> nargs args1 = nargs args2 - | Zfix _, Zfix _ -> true + | Zfix(f1,args1), Zfix(f2,args2) -> nargs args1 = nargs args2 | Zswitch _, Zswitch _ -> true | _ , _ -> false @@ -42,8 +42,9 @@ let conv_vect fconv vect1 vect2 cu = let infos = ref (create_clos_infos betaiotazeta Environ.empty_env) -let rec conv_val pb k v1 v2 cu = - if v1 == v2 then cu else conv_whd pb k (whd_val v1) (whd_val v2) cu +let rec conv_val pb k v1 v2 cu = + if v1 == v2 then cu + else conv_whd pb k (whd_val v1) (whd_val v2) cu and conv_whd pb k whd1 whd2 cu = match whd1, whd2 with @@ -52,21 +53,14 @@ and conv_whd pb k whd1 whd2 cu = let cu = conv_val CONV k (dom p1) (dom p2) cu in conv_fun pb k (codom p1) (codom p2) cu | Vfun f1, Vfun f2 -> conv_fun CONV k f1 f2 cu - | Vfix f1, Vfix f2 -> conv_fix k f1 f2 cu - | Vfix_app fa1, Vfix_app fa2 -> - let f1 = fix fa1 in - let args1 = args_of_fix fa1 in - let f2 = fix fa2 in - let args2 = args_of_fix fa2 in - conv_arguments k args1 args2 (conv_fix k f1 f2 cu) - | Vcofix cf1, Vcofix cf2 -> - conv_cofix k cf1 cf2 cu - | Vcofix_app cfa1, Vcofix_app cfa2 -> - let cf1 = cofix cfa1 in - let args1 = args_of_cofix cfa1 in - let cf2 = cofix cfa2 in - let args2 = args_of_cofix cfa2 in - conv_arguments k args1 args2 (conv_cofix k cf1 cf2 cu) + | Vfix (f1,None), Vfix (f2,None) -> conv_fix k f1 f2 cu + | Vfix (f1,Some args1), Vfix(f2,Some args2) -> + if nargs args1 <> nargs args2 then raise NotConvertible + else conv_arguments k args1 args2 (conv_fix k f1 f2 cu) + | Vcofix (cf1,_,None), Vcofix (cf2,_,None) -> conv_cofix k cf1 cf2 cu + | Vcofix (cf1,_,Some args1), Vcofix (cf2,_,Some args2) -> + if nargs args1 <> nargs args2 then raise NotConvertible + else conv_arguments k args1 args2 (conv_cofix k cf1 cf2 cu) | Vconstr_const i1, Vconstr_const i2 -> if i1 = i2 then cu else raise NotConvertible | Vconstr_block b1, Vconstr_block b2 -> @@ -89,7 +83,8 @@ and conv_whd pb k whd1 whd2 cu = and conv_atom pb k a1 stk1 a2 stk2 cu = match a1, a2 with | Aind (kn1,i1), Aind(kn2,i2) -> - if i1 = i2 && mind_equiv !infos kn1 kn2 && compare_stack stk1 stk2 then + if mind_equiv_infos !infos (kn1,i1) (kn2,i2) && compare_stack stk1 stk2 + then conv_stack k stk1 stk2 cu else raise NotConvertible | Aid ik1, Aid ik2 -> @@ -111,8 +106,6 @@ and conv_atom pb k a1 stk1 a2 stk2 cu = conv_whd pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu | _, Aiddef(ik2,v2) -> conv_whd pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu - | Afix_app _, _ | _, Afix_app _ | Aswitch _, _ | _, Aswitch _ -> - Util.anomaly "Vconv.conv_atom : Vm.whd_val doesn't work" | _, _ -> raise NotConvertible and conv_stack k stk1 stk2 cu = @@ -120,22 +113,17 @@ and conv_stack k stk1 stk2 cu = | [], [] -> cu | Zapp args1 :: stk1, Zapp args2 :: stk2 -> conv_stack k stk1 stk2 (conv_arguments k args1 args2 cu) - | Zfix fa1 :: stk1, Zfix fa2 :: stk2 -> - let f1 = fix fa1 in - let args1 = args_of_fix fa1 in - let f2 = fix fa2 in - let args2 = args_of_fix fa2 in + | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 -> conv_stack k stk1 stk2 (conv_arguments k args1 args2 (conv_fix k f1 f2 cu)) | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 -> - if eq_tbl sw1 sw2 then + if check_switch sw1 sw2 then let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in let rcu = ref (conv_val CONV k vt1 vt2 cu) in let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in for i = 0 to Array.length b1 - 1 do rcu := - conv_val CONV (k + fst b1.(i)) - (snd b1.(i)) (snd b2.(i)) !rcu + conv_val CONV (k + fst b1.(i)) (snd b1.(i)) (snd b2.(i)) !rcu done; conv_stack k stk1 stk2 !rcu else raise NotConvertible @@ -151,24 +139,20 @@ and conv_fix k f1 f2 cu = if f1 == f2 then cu else if check_fix f1 f2 then - let tf1 = types_of_fix f1 in - let tf2 = types_of_fix f2 in + let bf1, tf1 = reduce_fix k f1 in + let bf2, tf2 = reduce_fix k f2 in let cu = conv_vect (conv_val CONV k) tf1 tf2 cu in - let bf1 = bodies_of_fix k f1 in - let bf2 = bodies_of_fix k f2 in - conv_vect (conv_fun CONV (k + (fix_ndef f1))) bf1 bf2 cu + conv_vect (conv_fun CONV (k + Array.length tf1)) bf1 bf2 cu else raise NotConvertible and conv_cofix k cf1 cf2 cu = if cf1 == cf2 then cu else if check_cofix cf1 cf2 then - let tcf1 = types_of_cofix cf1 in - let tcf2 = types_of_cofix cf2 in + let bcf1, tcf1 = reduce_cofix k cf1 in + let bcf2, tcf2 = reduce_cofix k cf2 in let cu = conv_vect (conv_val CONV k) tcf1 tcf2 cu in - let bcf1 = bodies_of_cofix k cf1 in - let bcf2 = bodies_of_cofix k cf2 in - conv_vect (conv_val CONV (k + (cofix_ndef cf1))) bcf1 bcf2 cu + conv_vect (conv_val CONV (k + Array.length tcf1)) bcf1 bcf2 cu else raise NotConvertible and conv_arguments k args1 args2 cu = @@ -255,302 +239,4 @@ let set_use_vm b = let use_vm _ = !use_vm -(*******************************************) -(* Calcul de la forme normal d'un terme *) -(*******************************************) - -let crazy_type = mkSet - -let decompose_prod env t = - let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in - if name = Anonymous then (Name (id_of_string "x"),dom,codom) - else res - -exception Find_at of int - -(* rend le numero du constructeur correspondant au tag [tag], - [cst] = true si c'est un constructeur constant *) - -let invert_tag cst tag reloc_tbl = - try - for j = 0 to Array.length reloc_tbl - 1 do - let tagj,arity = reloc_tbl.(j) in - if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then - raise (Find_at j) - else () - done;raise Not_found - with Find_at j -> (j+1) - (* Argggg, ces constructeurs de ... qui commencent a 1*) - -(* Build the substitution that replaces Rels by the appropriate - inductives *) -let ind_subst mind mib = - let ntypes = mib.mind_ntypes in - let make_Ik k = mkInd (mind,ntypes-k-1) in - Util.list_tabulate make_Ik ntypes - -(* Instantiate inductives and parameters in constructor type - in normal form *) -let constructor_instantiate mind mib params ctyp = - let si = ind_subst mind mib in - let ctyp1 = substl si ctyp in - let nparams = Array.length params in - if nparams = 0 then ctyp1 - else - let _,ctyp2 = decompose_prod_n nparams ctyp1 in - let sp = List.rev (Array.to_list params) in substl sp ctyp2 - -let destApplication t = - try destApp t - with _ -> t,[||] - -let construct_of_constr_const env tag typ = - let cind,params = destApplication (whd_betadeltaiota env typ) in - let ind = destInd cind in - let (_,mip) = Inductive.lookup_mind_specif env ind in - let rtbl = mip.mind_reloc_tbl in - let i = invert_tag true tag rtbl in - mkApp(mkConstruct(ind,i), params) - -let find_rectype typ = - let cind,args = destApplication typ in - let ind = destInd cind in - ind, args - -let construct_of_constr_block env tag typ = - let (mind,_ as ind),allargs = find_rectype (whd_betadeltaiota env typ) in - let (mib,mip) = Inductive.lookup_mind_specif env ind in - let nparams = mib.mind_nparams in - let rtbl = mip.mind_reloc_tbl in - let i = invert_tag false tag rtbl in - let params = Array.sub allargs 0 nparams in - let specif = mip.mind_nf_lc in - let ctyp = constructor_instantiate mind mib params specif.(i-1) in - (mkApp(mkConstruct(ind,i), params), ctyp) - -let constr_type_of_idkey env idkey = - match idkey with - | ConstKey cst -> - let ty = (lookup_constant cst env).const_type in - mkConst cst, ty - | VarKey id -> - let (_,_,ty) = lookup_named id env in - mkVar id, ty - | RelKey i -> - let n = (nb_rel env - i) in - let (_,_,ty) = lookup_rel n env in - mkRel n, lift n ty - -let type_of_ind env ind = - let specif = Inductive.lookup_mind_specif env ind in - Inductive.type_of_inductive specif - -let build_branches_type (mind,_ as _ind) mib mip params dep p rtbl = - (* [build_one_branch i cty] construit le type de la ieme branche (commence - a 0) et les lambda correspondant aux realargs *) - let build_one_branch i cty = - let typi = constructor_instantiate mind mib params cty in - let decl,indapp = Term.decompose_prod typi in - let ind,cargs = find_rectype indapp in - let nparams = Array.length params in - let carity = snd (rtbl.(i)) in - let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in - let codom = - let papp = mkApp(p,crealargs) in - if dep then - let cstr = ith_constructor_of_inductive ind (i+1) in - let relargs = Array.init carity (fun i -> mkRel (carity-i)) in - let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in - mkApp(papp,[|dep_cstr|]) - else papp - in - decl, codom - in Array.mapi build_one_branch mip.mind_nf_lc - -(* La fonction de normalisation *) - -let rec nf_val env v t = nf_whd env (whd_val v) t - -and nf_whd env whd typ = - match whd with - | Vsort s -> mkSort s - | Vprod p -> - let dom = nf_val env (dom p) crazy_type in - let name = Name (id_of_string "x") in - let vc = body_of_vfun (nb_rel env) (codom p) in - let codom = nf_val (push_rel (name,None,dom) env) vc crazy_type in - mkProd(name,dom,codom) - | Vfun f -> nf_fun env f typ - | Vfix f -> nf_fix env f - | Vfix_app fa -> - let f = fix fa in - let vargs = args_of_fix fa in - let fd = nf_fix env f in - let (_,i),(_,ta,_) = destFix fd in - let t = ta.(i) in - let _, args = nf_args env vargs t in - mkApp(fd,args) - | Vcofix cf -> nf_cofix env cf - | Vcofix_app cfa -> - let cf = cofix cfa in - let vargs = args_of_cofix cfa in - let cfd = nf_cofix env cf in - let i,(_,ta,_) = destCoFix cfd in - let t = ta.(i) in - let _, args = nf_args env vargs t in - mkApp(cfd,args) - | Vconstr_const n -> construct_of_constr_const env n typ - | Vconstr_block b -> - let capp,ctyp = construct_of_constr_block env (btag b) typ in - let args = nf_bargs env b ctyp in - mkApp(capp,args) - | Vatom_stk(Aid idkey, stk) -> - let c,typ = constr_type_of_idkey env idkey in - nf_stk env c typ stk - | Vatom_stk(Aiddef(idkey,v), stk) -> - nf_whd env (whd_stack v stk) typ - | Vatom_stk(Aind ind, stk) -> - nf_stk env (mkInd ind) (type_of_ind env ind) stk - | Vatom_stk(_,stk) -> assert false - -and nf_stk env c t stk = - match stk with - | [] -> c - | Zapp vargs :: stk -> - let t, args = nf_args env vargs t in - nf_stk env (mkApp(c,args)) t stk - | Zfix fa :: stk -> - let f = fix fa in - let vargs = args_of_fix fa in - let fd = nf_fix env f in - let (_,i),(_,ta,_) = destFix fd in - let tf = ta.(i) in - let typ, args = nf_args env vargs tf in - let _,_,codom = decompose_prod env typ in - nf_stk env (mkApp(mkApp(fd,args),[|c|])) (subst1 c codom) stk - | Zswitch sw :: stk -> - let (mind,_ as ind),allargs = find_rectype (whd_betadeltaiota env t) in - let (mib,mip) = Inductive.lookup_mind_specif env ind in - let nparams = mib.mind_nparams in - let params,realargs = Util.array_chop nparams allargs in - (* calcul du predicat du case, - [dep] indique si c'est un case dependant *) - let dep,p = - let dep = ref false in - let rec nf_predicate env v pT = - match whd_val v, kind_of_term pT with - | Vfun f, Prod _ -> - let k = nb_rel env in - let vb = body_of_vfun k f in - let name,dom,codom = decompose_prod env pT in - let body = - nf_predicate (push_rel (name,None,dom) env) vb codom in - mkLambda(name,dom,body) - | Vfun f, _ -> - dep := true; - let k = nb_rel env in - let vb = body_of_vfun k f in - let name = Name (id_of_string "c") in - let n = mip.mind_nrealargs in - let rargs = Array.init n (fun i -> mkRel (n-i)) in - let dom = mkApp(mkApp(mkInd ind,params),rargs) in - let body = - nf_val (push_rel (name,None,dom) env) vb crazy_type in - mkLambda(name,dom,body) - | _, _ -> nf_val env v crazy_type - in - let aux = - nf_predicate env (type_of_switch sw) - (hnf_prod_applist env (type_of_ind env ind) (Array.to_list params)) - in - !dep,aux in - (* Calcul du type des branches *) - let btypes = - build_branches_type ind mib mip params dep p mip.mind_reloc_tbl in - (* calcul des branches *) - let bsw = branch_of_switch (nb_rel env) sw in - let mkbranch i (n,v) = - let decl,codom = btypes.(i) in - let env = - List.fold_right - (fun (name,t) env -> push_rel (name,None,t) env) decl env in - let b = nf_val env v codom in - compose_lam decl b - in - let branchs = Array.mapi mkbranch bsw in - let tcase = - if dep then mkApp(mkApp(p, params), [|c|]) - else mkApp(p, params) - in - let ci = case_info sw in - nf_stk env (mkCase(ci, p, c, branchs)) tcase stk - -and nf_args env vargs t = - let t = ref t in - let len = nargs vargs in - let targs = - Array.init len - (fun i -> - let _,dom,codom = decompose_prod env !t in - let c = nf_val env (arg vargs i) dom in - t := subst1 c codom; c) in - !t,targs - -and nf_bargs env b t = - let t = ref t in - let len = bsize b in - let args = Array.create len crazy_type in - for i = 0 to len - 1 do - let _,dom,codom = decompose_prod env !t in - let c = nf_val env (bfield b i) dom in - args.(i) <- c; - t := subst1 c codom - done; - args -(* Array.init len - (fun i -> - let _,dom,codom = decompose_prod env !t in - let c = nf_val env (bfield b i) dom in - t := subst1 c codom; c) *) - -and nf_fun env f typ = - let k = nb_rel env in - let vb = body_of_vfun k f in - let name,dom,codom = decompose_prod env typ in - let body = nf_val (push_rel (name,None,dom) env) vb codom in - mkLambda(name,dom,body) - -and nf_fix env f = - let init = fix_init f in - let rec_args = rec_args f in - let ndef = fix_ndef f in - let vt = types_of_fix f in - let ft = Array.map (fun v -> nf_val env v crazy_type) vt in - let name = Array.init ndef (fun _ -> (Name (id_of_string "Ffix"))) in - let k = nb_rel env in - let vb = bodies_of_fix k f in - let env = push_rec_types (name,ft,ft) env in - let fb = Util.array_map2 (fun v t -> nf_fun env v t) vb ft in - mkFix ((rec_args,init),(name,ft,fb)) - -and nf_cofix env cf = - let init = cofix_init cf in - let ndef = cofix_ndef cf in - let vt = types_of_cofix cf in - let cft = Array.map (fun v -> nf_val env v crazy_type) vt in - let name = Array.init ndef (fun _ -> (Name (id_of_string "Fcofix"))) in - let k = nb_rel env in - let vb = bodies_of_cofix k cf in - let env = push_rec_types (name,cft,cft) env in - let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in - mkCoFix (init,(name,cft,cfb)) - -let cbv_vm env c t = - let transp = transp_values () in - if not transp then set_transp_values true; - let v = val_of_constr env c in - let c = nf_val env v t in - if not transp then set_transp_values false; - c - diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 4aed5d05..551615aa 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -19,28 +19,5 @@ val use_vm : unit -> bool val set_use_vm : bool -> unit val vconv : conv_pb -> types conversion_function -(***********************************************************************) -(*s Reduction functions *) -val cbv_vm : env -> constr -> types -> constr - - - - - -val nf_val : env -> values -> types -> constr - -val nf_whd : env -> Vm.whd -> types -> constr - -val nf_stk : env -> constr -> types -> Vm.stack -> constr - -val nf_args : env -> Vm.arguments -> types -> types * constr array - -val nf_bargs : env -> Vm.vblock -> types -> constr array - -val nf_fun : env -> Vm.vfun -> types -> constr - -val nf_fix : env -> Vm.vfix -> constr - -val nf_cofix : env -> Vm.vcofix -> constr +val val_of_constr : env -> constr -> values - diff --git a/kernel/vm.ml b/kernel/vm.ml index c8be979e..de9bd753 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -1,20 +1,16 @@ -open Obj open Names open Term open Conv_oracle open Cbytecodes - external set_drawinstr : unit -> unit = "coq_set_drawinstr" (******************************************) (* Fonctions en plus du module Obj ********) (******************************************) -external offset_closure : t -> int -> t = "coq_offset_closure" -external offset : t -> int = "coq_offset" -let first o = (offset_closure o (offset o)) -let last o = (field o (size o - 1)) +external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" +external offset : Obj.t -> int = "coq_offset" let accu_tag = 0 @@ -34,8 +30,10 @@ external set_transp_values : bool -> unit = "coq_set_transp_value" (*******************************************) type tcode -let tcode_of_obj v = ((obj v):tcode) -let fun_code v = tcode_of_obj (field (repr v) 0) +let tcode_of_obj v = ((Obj.obj v):tcode) +let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) + + external mkAccuCode : int -> tcode = "coq_makeaccu" external mkPopStopCode : int -> tcode = "coq_pushpop" @@ -63,155 +61,26 @@ let popstop_code i = end let stop = popstop_code 0 - + (******************************************************) (* Types de donnees abstraites et fonctions associees *) (******************************************************) (* Values of the abstract machine *) -let val_of_obj v = ((obj v):values) -let crasy_val = (val_of_obj (repr 0)) - - -(* Functions *) -type vfun -(* v = [Tc | c | fv1 | ... | fvn ] *) -(* ^ *) -(* [Tc | (Restart : c) | v | a1 | ... an] *) -(* ^ *) +let val_of_obj v = ((Obj.obj v):values) +let crasy_val = (val_of_obj (Obj.repr 0)) -(* Products *) +(* Abstract data *) type vprod -(* [0 | dom : codom] *) -(* ^ *) -let dom : vprod -> values = fun p -> val_of_obj (field (repr p) 0) -let codom : vprod -> vfun = fun p -> (obj (field (repr p) 1)) - -(* Arguments *) -type arguments -(* arguments = [_ | _ | _ | a1 | ... | an] *) -(* ^ *) -let nargs : arguments -> int = fun args -> (size (repr args)) - 2 - -let unsafe_arg : arguments -> int -> values = - fun args i -> val_of_obj (field (repr args) (i+2)) - -let arg args i = - if 0 <= i && i < (nargs args) then unsafe_arg args i - else raise (Invalid_argument - ("Vm.arg size = "^(string_of_int (nargs args))^ - " acces "^(string_of_int i))) - -(* Fixpoints *) +type vfun type vfix +type vcofix +type vblock +type arguments -(* [Tc|c0|Ti|c1|...|Ti|cn|fv1|...|fvn| [ct0|...|ctn]] *) -(* ^ *) -type vfix_block - -let fix_init : vfix -> int = fun vf -> (offset (repr vf)/2) - -let block_of_fix : vfix -> vfix_block = fun vf -> obj (first (repr vf)) - -let fix_block_type : vfix_block -> tcode array = - fun fb -> (obj (last (repr fb))) - -let fix_block_ndef : vfix_block -> int = - fun fb -> size (last (repr fb)) - -let fix_ndef vf = fix_block_ndef (block_of_fix vf) - -let unsafe_fb_code : vfix_block -> int -> tcode = - fun fb i -> tcode_of_obj (field (repr fb) (2 * i)) - -let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 - -let rec_args vf = - let fb = block_of_fix vf in - let size = fix_block_ndef fb in - Array.init size (unsafe_rec_arg fb) - -exception FALSE - -let check_fix f1 f2 = - let i1, i2 = fix_init f1, fix_init f2 in - (* Verification du point de depart *) - if i1 = i2 then - let fb1,fb2 = block_of_fix f1, block_of_fix f2 in - let n = fix_block_ndef fb1 in - (* Verification du nombre de definition *) - if n = fix_block_ndef fb2 then - (* Verification des arguments recursifs *) - try - for i = 0 to n - 1 do - if not (unsafe_rec_arg fb1 i = unsafe_rec_arg fb2 i) then - raise FALSE - done; - true - with FALSE -> false - else false - else false - -(* Partials applications of Fixpoints *) -type vfix_app -let fix : vfix_app -> vfix = - fun vfa -> ((obj (field (repr vfa) 1)):vfix) -let args_of_fix : vfix_app -> arguments = - fun vfa -> ((magic vfa) : arguments) - -(* CoFixpoints *) -type vcofix -type vcofix_block -let cofix_init : vcofix -> int = fun vcf -> (offset (repr vcf)/2) - -let block_of_cofix : vcofix -> vcofix_block = fun vcf -> obj (first (repr vcf)) - -let cofix_block_ndef : vcofix_block -> int = - fun fb -> size (last (repr fb)) - -let cofix_ndef vcf= cofix_block_ndef (block_of_cofix vcf) - -let cofix_block_type : vcofix_block -> tcode array = - fun cfb -> (obj (last (repr cfb))) - -let check_cofix cf1 cf2 = - cofix_init cf1 = cofix_init cf2 && - cofix_ndef cf1 = cofix_ndef cf2 - -let cofix_arity c = int_tcode c 1 - -let unsafe_cfb_code : vcofix_block -> int -> tcode = - fun cfb i -> tcode_of_obj (field (repr cfb) (2 * i)) - -(* Partials applications of CoFixpoints *) -type vcofix_app -let cofix : vcofix_app -> vcofix = - fun vcfa -> ((obj (field (repr vcfa) 1)):vcofix) -let args_of_cofix : vcofix_app -> arguments = - fun vcfa -> ((magic vcfa) : arguments) - -(* Blocks *) -type vblock (* la representation Ocaml *) -let btag : vblock -> int = fun b -> tag (repr b) -let bsize : vblock -> int = fun b -> size (repr b) -let bfield b i = - if 0 <= i && i < (bsize b) then - val_of_obj (field (repr b) i) - else raise (Invalid_argument "Vm.bfield") - -(* Accumulators and atoms *) - -type accumulator -(* [Ta | accumulate | at | a1 | ... | an ] *) - -type inv_rel_key = int - -type id_key = inv_rel_key tableKey - +type vm_env type vstack = values array -type vm_env - type vswitch = { sw_type_code : tcode; sw_code : tcode; @@ -220,138 +89,148 @@ type vswitch = { sw_env : vm_env } -(* Ne pas changer ce type sans modifier le code C *) +(* Representation des types abstraits: *) +(* + Les produits : *) +(* - vprod = 0_[ dom | codom] *) +(* dom : values, codom : vfun *) +(* *) +(* + Les fonctions ont deux representations possibles : *) +(* - fonction non applique : vf = Ct_[ C | fv1 | ... | fvn] *) +(* C:tcode, fvi : values *) +(* Remarque : il n'y a pas de difference entre la fct et son *) +(* environnement. *) +(* - Application partielle : Ct_[Restart:C| vf | arg1 | ... argn] *) +(* *) +(* + Les points fixes : *) +(* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *) +(* Remarque il n'y a qu'un seul block pour representer tout les *) +(* points fixes d'une declaration mutuelle, chaque point fixe *) +(* pointe sur la position de son code dans le block. *) +(* - L'application partielle d'un point fixe suit le meme schema *) +(* que celui des fonctions *) +(* Remarque seul les points fixes qui n'ont pas encore recu leur *) +(* argument recursif sont encode de cette maniere (si l'argument *) +(* recursif etait un constructeur le point fixe se serait reduit *) +(* sinon il est represente par un accumulateur) *) +(* *) +(* + Les cofix sont expliques dans cbytegen.ml *) +(* *) +(* + Les vblock encodent les constructeurs (non constant) de caml, *) +(* la difference est que leur tag commence a 1 (0 est reserve pour les *) +(* accumulateurs : accu_tag) *) +(* *) +(* + vm_env est le type des environnement machine (une fct ou un pt fixe) *) +(* *) +(* + Les accumulateurs : At_[accumulate| accu | arg1 | ... | argn ] *) +(* - representation des [accu] : tag_[....] *) +(* -- tag <= 2 : encodage du type atom *) +(* -- 3_[accu|fix_app] : un point fixe bloque par un accu *) +(* -- 4_[accu|vswitch] : un case bloque par un accu *) +(* -- 5_[fcofix] : une fonction de cofix *) +(* -- 6_[fcofix|val] : une fonction de cofix, val represente *) +(* la valeur de la reduction de la fct applique a arg1 ... argn *) +(* Le type [arguments] est utiliser de maniere abstraite comme un *) +(* tableau, il represente la structure de donnee suivante : *) +(* tag[ _ | _ |v1|... | vn] *) +(* Generalement le 1er champs est un pointeur de code *) + +(* Ne pas changer ce type sans modifier le code C, *) +(* en particulier le fichier "coq_values.h" *) type atom = | Aid of id_key | Aiddef of id_key * values | Aind of inductive - | Afix_app of accumulator * vfix_app - | Aswitch of accumulator * vswitch - -let atom_of_accu : accumulator -> atom = - fun a -> ((obj (field (repr a) 1)) : atom) - -let args_of_accu : accumulator -> arguments = - fun a -> ((magic a) : arguments) - -let nargs_of_accu a = nargs (args_of_accu a) (* Les zippers *) type zipper = | Zapp of arguments - | Zfix of vfix_app + | Zfix of vfix*arguments (* Peut-etre vide *) | Zswitch of vswitch type stack = zipper list +type to_up = values + type whd = | Vsort of sorts | Vprod of vprod | Vfun of vfun - | Vfix of vfix - | Vfix_app of vfix_app - | Vcofix of vcofix - | Vcofix_app of vcofix_app + | Vfix of vfix * arguments option + | Vcofix of vcofix * to_up * arguments option | Vconstr_const of int | Vconstr_block of vblock | Vatom_stk of atom * stack -(* Les atomes sont forcement Aid Aiddef Aind *) - -(**********************************************) -(* Constructeurs ******************************) -(**********************************************) -(* obj_of_atom : atom -> t *) -let obj_of_atom : atom -> t = - fun a -> - let res = Obj.new_block accu_tag 2 in - set_field res 0 (repr accumulate); - set_field res 1 (repr a); - res - -(* obj_of_str_const : structured_constant -> t *) -let rec obj_of_str_const str = - match str with - | Const_sorts s -> repr (Vsort s) - | Const_ind ind -> obj_of_atom (Aind ind) - | Const_b0 tag -> repr tag - | Const_bn(tag, args) -> - let len = Array.length args in - let res = new_block tag len in - for i = 0 to len - 1 do - set_field res i (obj_of_str_const args.(i)) - done; - res - -let val_of_obj o = ((obj o) : values) - -let val_of_str_const str = val_of_obj (obj_of_str_const str) - -let val_of_atom a = val_of_obj (obj_of_atom a) - -let idkey_tbl = Hashtbl.create 31 - -let val_of_idkey key = - try Hashtbl.find idkey_tbl key - with Not_found -> - let v = val_of_atom (Aid key) in - Hashtbl.add idkey_tbl key v; - v - -let val_of_rel k = val_of_idkey (RelKey k) -let val_of_rel_def k v = val_of_atom(Aiddef(RelKey k, v)) - -let val_of_named id = val_of_idkey (VarKey id) -let val_of_named_def id v = val_of_atom(Aiddef(VarKey id, v)) - -let val_of_constant c = val_of_idkey (ConstKey c) -let val_of_constant_def n c v = - let res = Obj.new_block accu_tag 2 in - set_field res 0 (repr (mkAccuCond n)); - set_field res 1 (repr (Aiddef(ConstKey c, v))); - val_of_obj res - - (*************************************************) (* Destructors ***********************************) (*************************************************) - let rec whd_accu a stk = let stk = - if nargs_of_accu a = 0 then stk - else Zapp (args_of_accu a) :: stk in - let at = atom_of_accu a in - match at with - | Aid _ | Aiddef _ | Aind _ -> Vatom_stk(at, stk) - | Afix_app(a,fa) -> whd_accu a (Zfix fa :: stk) - | Aswitch(a,sw) -> whd_accu a (Zswitch sw :: stk) + if Obj.size a = 2 then stk + else Zapp (Obj.obj a) :: stk in + let at = Obj.field a 1 in + match Obj.tag at with + | i when i <= 2 -> + Vatom_stk(Obj.magic at, stk) + | 3 (* fix_app tag *) -> + let fa = Obj.field at 1 in + let zfix = + Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in + whd_accu (Obj.field at 0) (zfix :: stk) + | 4 (* switch tag *) -> + let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in + whd_accu (Obj.field at 0) (zswitch :: stk) + | 5 (* cofix_tag *) -> + begin match stk with + | [] -> + let vcfx = Obj.obj (Obj.field at 0) in + let to_up = Obj.obj a in + Vcofix(vcfx, to_up, None) + | [Zapp args] -> + let vcfx = Obj.obj (Obj.field at 0) in + let to_up = Obj.obj a in + Vcofix(vcfx, to_up, Some args) + | _ -> assert false + end + | 6 (* cofix_evaluated_tag *) -> + begin match stk with + | [] -> + let vcofix = Obj.obj (Obj.field at 0) in + let res = Obj.obj a in + Vcofix(vcofix, res, None) + | [Zapp args] -> + let vcofix = Obj.obj (Obj.field at 0) in + let res = Obj.obj a in + Vcofix(vcofix, res, Some args) + | _ -> assert false + end + | _ -> assert false -external kind_of_closure : t -> int = "coq_kind_of_closure" +external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" let whd_val : values -> whd = fun v -> - let o = repr v in - if is_int o then Vconstr_const (obj o) + let o = Obj.repr v in + if Obj.is_int o then Vconstr_const (Obj.obj o) else - let tag = tag o in + let tag = Obj.tag o in if tag = accu_tag then - if is_accumulate (fun_code o) then whd_accu (obj o) [] + ( + if Obj.size o = 1 then Obj.obj o (* sort *) else - if size o = 1 then Vsort(obj (field o 0)) - else Vprod(obj o) + if is_accumulate (fun_code o) then whd_accu o [] + else (Vprod(Obj.obj o))) else - if tag = closure_tag || tag = infix_tag then - match kind_of_closure o with - | 0 -> Vfun(obj o) - | 1 -> Vfix(obj o) - | 2 -> Vfix_app(obj o) - | 3 -> Vcofix(obj o) - | 4 -> Vcofix_app(obj o) - | 5 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> Util.anomaly "Vm.whd : kind_of_closure does not work" - else Vconstr_block(obj o) + if tag = Obj.closure_tag || tag = Obj.infix_tag then + ( match kind_of_closure o with + | 0 -> Vfun(Obj.obj o) + | 1 -> Vfix(Obj.obj o, None) + | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) + | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) + | _ -> Util.anomaly "Vm.whd : kind_of_closure does not work") + else Vconstr_block(Obj.obj o) @@ -359,7 +238,6 @@ let whd_val : values -> whd = (* La machine abstraite *************************) (************************************************) - (* gestion de la pile *) external push_ra : tcode -> unit = "coq_push_ra" external push_val : values -> unit = "coq_push_val" @@ -371,6 +249,17 @@ external push_vstack : vstack -> unit = "coq_push_vstack" external interprete : tcode -> values -> vm_env -> int -> values = "coq_interprete_ml" + + +(* Functions over arguments *) +let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 +let arg args i = + if 0 <= i && i < (nargs args) then + val_of_obj (Obj.field (Obj.repr args) (i+2)) + else raise (Invalid_argument + ("Vm.arg size = "^(string_of_int (nargs args))^ + " acces "^(string_of_int i))) + let apply_arguments vf vargs = let n = nargs vargs in if n = 0 then vf @@ -378,7 +267,7 @@ let apply_arguments vf vargs = begin push_ra stop; push_arguments vargs; - interprete (fun_code vf) vf (magic vf) (n - 1) + interprete (fun_code vf) vf (Obj.magic vf) (n - 1) end let apply_vstack vf vstk = @@ -388,80 +277,130 @@ let apply_vstack vf vstk = begin push_ra stop; push_vstack vstk; - interprete (fun_code vf) vf (magic vf) (n - 1) + interprete (fun_code vf) vf (Obj.magic vf) (n - 1) end -let apply_fix_app vfa arg = - let vf = fix vfa in - let vargs = args_of_fix vfa in - push_ra stop; - push_val arg; - push_arguments vargs; - interprete (fun_code vf) (magic vf) (magic vf) (nargs vargs) - -external set_forcable : unit -> unit = "coq_set_forcable" -let force_cofix v = - match whd_val v with - | Vcofix _ | Vcofix_app _ -> - push_ra stop; - set_forcable (); - interprete (fun_code v) (magic v) (magic v) 0 - | _ -> v - -let apply_switch sw arg = - let arg = force_cofix arg in - let tc = sw.sw_annot.tailcall in - if tc then - (push_ra stop;push_vstack sw.sw_stk) - else - (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk))); - interprete sw.sw_code arg sw.sw_env 0 +(**********************************************) +(* Constructeurs ******************************) +(**********************************************) -let is_accu v = - is_block (repr v) && tag (repr v) = accu_tag && - fun_code v == accumulate +let obj_of_atom : atom -> Obj.t = + fun a -> + let res = Obj.new_block accu_tag 2 in + Obj.set_field res 0 (Obj.repr accumulate); + Obj.set_field res 1 (Obj.repr a); + res -let rec whd_stack v stk = - match stk with - | [] -> whd_val v - | Zapp a :: stkt -> whd_stack (apply_arguments v a) stkt - | Zfix fa :: stkt -> - if is_accu v then whd_accu (magic v) stk - else whd_stack (apply_fix_app fa v) stkt - | Zswitch sw :: stkt -> - if is_accu v then whd_accu (magic v) stk - else whd_stack (apply_switch sw v) stkt +(* obj_of_str_const : structured_constant -> Obj.t *) +let rec obj_of_str_const str = + match str with + | Const_sorts s -> Obj.repr (Vsort s) + | Const_ind ind -> obj_of_atom (Aind ind) + | Const_b0 tag -> Obj.repr tag + | Const_bn(tag, args) -> + let len = Array.length args in + let res = Obj.new_block tag len in + for i = 0 to len - 1 do + Obj.set_field res i (obj_of_str_const args.(i)) + done; + res -let rec force_whd v stk = - match whd_stack v stk with - | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk - | res -> res +let val_of_obj o = ((Obj.obj o) : values) - +let val_of_str_const str = val_of_obj (obj_of_str_const str) -(* Function *) -external closure_arity : vfun -> int = "coq_closure_arity" +let val_of_atom a = val_of_obj (obj_of_atom a) + +let idkey_tbl = Hashtbl.create 31 + +let val_of_idkey key = + try Hashtbl.find idkey_tbl key + with Not_found -> + let v = val_of_atom (Aid key) in + Hashtbl.add idkey_tbl key v; + v + +let val_of_rel k = val_of_idkey (RelKey k) +let val_of_rel_def k v = val_of_atom(Aiddef(RelKey k, v)) + +let val_of_named id = val_of_idkey (VarKey id) +let val_of_named_def id v = val_of_atom(Aiddef(VarKey id, v)) + +let val_of_constant c = val_of_idkey (ConstKey c) +let val_of_constant_def n c v = + let res = Obj.new_block accu_tag 2 in + Obj.set_field res 0 (Obj.repr (mkAccuCond n)); + Obj.set_field res 1 (Obj.repr (Aiddef(ConstKey c, v))); + val_of_obj res -(* [apply_rel v k arity] applique la valeurs [v] aux arguments - [k],[k+1], ... , [k+arity-1] *) let mkrel_vstack k arity = let max = k + arity - 1 in Array.init arity (fun i -> val_of_rel (max - i)) +(*************************************************) +(** Operations pour la manipulation des donnees **) +(*************************************************) + + +(* Functions over products *) + +let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) +let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1)) + +(* Functions over vfun *) + +external closure_arity : vfun -> int = "coq_closure_arity" + let body_of_vfun k vf = let vargs = mkrel_vstack k 1 in - apply_vstack (magic vf) vargs + apply_vstack (Obj.magic vf) vargs let decompose_vfun2 k vf1 vf2 = let arity = min (closure_arity vf1) (closure_arity vf2) in - assert (0 <= arity && arity < Sys.max_array_length); + assert (0 < arity && arity < Sys.max_array_length); let vargs = mkrel_vstack k arity in - let v1 = apply_vstack (magic vf1) vargs in - let v2 = apply_vstack (magic vf2) vargs in + let v1 = apply_vstack (Obj.magic vf1) vargs in + let v2 = apply_vstack (Obj.magic vf2) vargs in arity, v1, v2 - + +(* Functions over fixpoint *) + +let first o = (offset_closure o (offset o)) +let last o = (Obj.field o (Obj.size o - 1)) + +let current_fix vf = - (offset (Obj.repr vf) / 2) + +let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) + +let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 -(* Fix *) +let rec_args vf = + let fb = first (Obj.repr vf) in + let size = Obj.size (last fb) in + Array.init size (unsafe_rec_arg fb) + +exception FALSE + +let check_fix f1 f2 = + let i1, i2 = current_fix f1, current_fix f2 in + (* Verification du point de depart *) + if i1 = i2 then + let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in + let n = Obj.size (last fb1) in + (* Verification du nombre de definition *) + if n = Obj.size (last fb2) then + (* Verification des arguments recursifs *) + try + for i = 0 to n - 1 do + if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i + then raise FALSE + done; + true + with FALSE -> false + else false + else false + +(* Functions over vfix *) external atom_rel : unit -> atom array = "get_coq_atom_tbl" external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl" @@ -486,69 +425,89 @@ let relaccu_code i = !relaccu_tbl.(i) end -let jump_grabrec c = offset_tcode c 2 -let jump_grabrecrestart c = offset_tcode c 3 - -let bodies_of_fix k vf = - let fb = block_of_fix vf in - let ndef = fix_block_ndef fb in +let reduce_fix k vf = + let fb = first (Obj.repr vf) in + (* calcul des types *) + let fc_typ = ((Obj.obj (last fb)) : tcode array) in + let ndef = Array.length fc_typ in + let et = offset_closure fb (2*(ndef - 1)) in + let ftyp = + Array.map + (fun c -> interprete c crasy_val (Obj.magic et) 0) fc_typ in (* Construction de l' environnement des corps des points fixes *) - let e = dup (repr fb) in + let e = Obj.dup fb in for i = 0 to ndef - 1 do - set_field e (2 * i) (repr (relaccu_code (k + i))) + Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) done; let fix_body i = + let jump_grabrec c = offset_tcode c 2 in let c = jump_grabrec (unsafe_fb_code fb i) in - let res = Obj.new_block closure_tag 2 in - set_field res 0 (repr c); - set_field res 1 (offset_closure e (2*i)); - ((obj res) : vfun) - in Array.init ndef fix_body - -let types_of_fix vf = - let fb = block_of_fix vf in - let type_code = fix_block_type fb in - let type_val c = interprete c crasy_val (magic fb) 0 in - Array.map type_val type_code - + let res = Obj.new_block Obj.closure_tag 2 in + Obj.set_field res 0 (Obj.repr c); + Obj.set_field res 1 (offset_closure e (2*i)); + ((Obj.obj res) : vfun) in + (Array.init ndef fix_body, ftyp) -(* CoFix *) -let jump_cograb c = offset_tcode c 2 -let jump_cograbrestart c = offset_tcode c 3 - -let bodies_of_cofix k vcf = - let cfb = block_of_cofix vcf in - let ndef = cofix_block_ndef cfb in - (* Construction de l' environnement des corps des cofix *) - let e = dup (repr cfb) in +(* Functions over vcofix *) + +let get_fcofix vcf i = + match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with + | Vcofix(vcfi, _, _) -> vcfi + | _ -> assert false + +let current_cofix vcf = + let ndef = Obj.size (last (Obj.repr vcf)) in + let rec find_cofix pos = + if pos < ndef then + if get_fcofix vcf pos == vcf then pos + else find_cofix (pos+1) + else raise Not_found in + try find_cofix 0 + with _ -> assert false + +let check_cofix vcf1 vcf2 = + (current_cofix vcf1 = current_cofix vcf2) && + (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2))) + +external print_point : Obj.t -> unit = "coq_print_pointer" + +let reduce_cofix k vcf = + let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in + let ndef = Array.length fc_typ in + let ftyp = + Array.map (fun c -> interprete c crasy_val (Obj.magic vcf) 0) fc_typ in + (* Construction de l'environnement des corps des cofix *) + + let max = k + ndef - 1 in + let e = Obj.dup (Obj.repr vcf) in for i = 0 to ndef - 1 do - set_field e (2 * i) (repr (relaccu_code (k + i))) + Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) done; + let cofix_body i = - let c = unsafe_cfb_code cfb i in - let arity = int_tcode c 1 in - if arity = 0 then - begin - push_ra stop; - interprete (jump_cograbrestart c) crasy_val - (obj (offset_closure e (2*i))) 0 - end - else - let res = Obj.new_block closure_tag 2 in - set_field res 0 (repr (jump_cograb c)); - set_field res 1 (offset_closure e (2*i)); - ((obj res) : values) - in Array.init ndef cofix_body - -let types_of_cofix vcf = - let cfb = block_of_cofix vcf in - let type_code = cofix_block_type cfb in - let type_val c = interprete c crasy_val (magic cfb) 0 in - Array.map type_val type_code - -(* Switch *) - -let eq_tbl sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl + let vcfi = get_fcofix vcf i in + let c = Obj.field (Obj.repr vcfi) 0 in + Obj.set_field e 0 c; + let atom = Obj.new_block cofix_tag 1 in + let self = Obj.new_block accu_tag 2 in + Obj.set_field self 0 (Obj.repr accumulate); + Obj.set_field self 1 (Obj.repr atom); + apply_vstack (Obj.obj e) [|Obj.obj self|] in + (Array.init ndef cofix_body, ftyp) + + +(* Functions over vblock *) + +let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b) +let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b) +let bfield b i = + if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i) + else raise (Invalid_argument "Vm.bfield") + + +(* Functions over vswitch *) + +let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl let case_info sw = sw.sw_annot.ci @@ -557,15 +516,22 @@ let type_of_switch sw = interprete sw.sw_type_code crasy_val sw.sw_env 0 let branch_arg k (tag,arity) = - if arity = 0 then ((magic tag):values) + if arity = 0 then ((Obj.magic tag):values) else - let b = new_block tag arity in + let b = Obj.new_block tag arity in for i = 0 to arity - 1 do - set_field b i (repr (val_of_rel (k+i))) + Obj.set_field b i (Obj.repr (val_of_rel (k+i))) done; val_of_obj b - - + +let apply_switch sw arg = + let tc = sw.sw_annot.tailcall in + if tc then + (push_ra stop;push_vstack sw.sw_stk) + else + (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk))); + interprete sw.sw_code arg sw.sw_env 0 + let branch_of_switch k sw = let eval_branch (_,arity as ta) = let arg = branch_arg k ta in @@ -573,27 +539,62 @@ let branch_of_switch k sw = (arity, v) in Array.map eval_branch sw.sw_annot.rtbl - - - - - - - - - - - - - - - - + +(* Evaluation *) +let is_accu v = + let o = Obj.repr v in + Obj.is_block o && Obj.tag o = accu_tag && + fun_code v == accumulate && Obj.tag (Obj.field o 1) < cofix_tag +let rec whd_stack v stk = + match stk with + | [] -> whd_val v + | Zapp args :: stkt -> whd_stack (apply_arguments v args) stkt + | Zfix (f,args) :: stkt -> + let o = Obj.repr v in + if Obj.is_block o && Obj.tag o = accu_tag then + whd_accu (Obj.repr v) stk + else + let v', stkt = + match stkt with + | Zapp args' :: stkt -> + push_ra stop; + push_arguments args'; + push_val v; + push_arguments args; + let v' = + interprete (fun_code f) (Obj.magic f) (Obj.magic f) + (nargs args+ nargs args') in + v', stkt + | _ -> + push_ra stop; + push_val v; + push_arguments args; + let v' = + interprete (fun_code f) (Obj.magic f) (Obj.magic f) + (nargs args) in + v', stkt + in + whd_stack v' stkt + | Zswitch sw :: stkt -> + let o = Obj.repr v in + if Obj.is_block o && Obj.tag o = accu_tag then + if Obj.tag (Obj.field o 1) < cofix_tag then whd_accu (Obj.repr v) stk + else + let to_up = + match whd_accu (Obj.repr v) [] with + | Vcofix (_, to_up, _) -> to_up + | _ -> assert false in + whd_stack (apply_switch sw to_up) stkt + else whd_stack (apply_switch sw v) stkt +let rec force_whd v stk = + match whd_stack v stk with + | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk + | res -> res diff --git a/kernel/vm.mli b/kernel/vm.mli index b5fd9b9d..279ac937 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -13,45 +13,41 @@ type tcode (* Les valeurs ***********) -type accumulator type vprod type vfun type vfix -type vfix_app type vcofix -type vcofix_app type vblock type vswitch type arguments +type atom = + | Aid of id_key + | Aiddef of id_key * values + | Aind of inductive + +(* Les zippers *) + type zipper = | Zapp of arguments - | Zfix of vfix_app + | Zfix of vfix*arguments (* Peut-etre vide *) | Zswitch of vswitch type stack = zipper list - -type atom = - | Aid of id_key - | Aiddef of id_key * values - | Aind of inductive - | Afix_app of accumulator * vfix_app - | Aswitch of accumulator * vswitch +type to_up type whd = | Vsort of sorts | Vprod of vprod | Vfun of vfun - | Vfix of vfix - | Vfix_app of vfix_app - | Vcofix of vcofix - | Vcofix_app of vcofix_app + | Vfix of vfix * arguments option + | Vcofix of vcofix * to_up * arguments option | Vconstr_const of int | Vconstr_block of vblock | Vatom_stk of atom * stack - -(* Constructors *) + +(** Constructors *) val val_of_str_const : structured_constant -> values val val_of_rel : int -> values @@ -63,44 +59,43 @@ val val_of_named_def : identifier -> values -> values val val_of_constant : constant -> values val val_of_constant_def : int -> constant -> values -> values -(* Destructors *) +(** Destructors *) val whd_val : values -> whd +(* Arguments *) +val nargs : arguments -> int +val arg : arguments -> int -> values + (* Product *) val dom : vprod -> values val codom : vprod -> vfun + (* Function *) val body_of_vfun : int -> vfun -> values val decompose_vfun2 : int -> vfun -> vfun -> int * values * values + (* Fix *) -val fix : vfix_app -> vfix -val args_of_fix : vfix_app -> arguments -val fix_init : vfix -> int -val fix_ndef : vfix -> int -val rec_args : vfix -> int array +val current_fix : vfix -> int val check_fix : vfix -> vfix -> bool -val bodies_of_fix : int -> vfix -> vfun array -val types_of_fix : vfix -> values array +val rec_args : vfix -> int array +val reduce_fix : int -> vfix -> vfun array * values array + (* bodies , types *) + (* CoFix *) -val cofix : vcofix_app -> vcofix -val args_of_cofix : vcofix_app -> arguments -val cofix_init : vcofix -> int -val cofix_ndef : vcofix -> int +val current_cofix : vcofix -> int val check_cofix : vcofix -> vcofix -> bool -val bodies_of_cofix : int -> vcofix -> values array -val types_of_cofix : vcofix -> values array +val reduce_cofix : int -> vcofix -> values array * values array + (* bodies , types *) (* Block *) val btag : vblock -> int val bsize : vblock -> int val bfield : vblock -> int -> values + (* Switch *) -val eq_tbl : vswitch -> vswitch -> bool +val check_switch : vswitch -> vswitch -> bool val case_info : vswitch -> case_info val type_of_switch : vswitch -> values val branch_of_switch : int -> vswitch -> (int * values) array -(* Arguments *) -val nargs : arguments -> int -val arg : arguments -> int -> values (* Evaluation *) val whd_stack : values -> stack -> whd -- cgit v1.2.3