From 407f120d4b6a8d829cbf8efdfe5796444dda5a73 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Tue, 15 May 2007 15:29:54 +0000 Subject: Correction du pretty-printing des big-int (la sous-fonction get_height faisait n'importe quoi). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9825 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_intsyntax.ml | 26 +++++++++----------------- 1 file changed, 9 insertions(+), 17 deletions(-) (limited to 'parsing/g_intsyntax.ml') diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml index e1cbbb7e0..0c2c870eb 100644 --- a/parsing/g_intsyntax.ml +++ b/parsing/g_intsyntax.ml @@ -14,16 +14,6 @@ open Bigint open Libnames open Rawterm -(* arnaud : plan : - - path des modules int31 et bigint dans des variables - - nom des constructeurs dans des variables - - nom des scopes dans des variables - - fonction qui cree les int31 en fonction d'un entier (ce sont des bigint de coq) - <= div2 with rest 31 fois, dans un tableau d'args preconstruit - - fonction qui cree un bigint de hauteur n (en appelant deux fois la fonction - a la hauteur n-1 (sauf dans les cas ou il y a du 0)) - /!\ attention aux nombres negatifs *) - (*** Constants for locating the int31 and bigN ***) @@ -214,18 +204,20 @@ let bigint_of_word = | RApp (_,RRef(_,c), [_;lft;rght]) when c = zn2z_WW -> let hleft = get_height lft in let hright = get_height rght in - if less_than hleft hright then - hright - else - hleft + add_1 + (if less_than hleft hright then + hright + else + hleft) | _ -> zero in let rec transform hght rc = match rc with | RApp (_,RRef(_,c),_) when c = zn2z_W0-> zero - | RApp (_,RRef(_,c), [_;lft;rght]) when c=zn2z_WW-> add (mult (rank hght) - (transform (sub_1 hght) lft)) - (transform (sub_1 hght) rght) + | RApp (_,RRef(_,c), [_;lft;rght]) when c=zn2z_WW-> let new_hght = sub_1 hght in + add (mult (rank new_hght) + (transform (new_hght) lft)) + (transform (new_hght) rght) | _ -> bigint_of_int31 rc in fun rc -> -- cgit v1.2.3