some more renamings for Multivariate (#159)

Deducteam · Jan 6, 2025 · 6cf9448 · 6cf9448
1 parent b0293b4
commit 6cf9448
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 5 deletions.
diff --git a/README.md b/README.md
@@ -228,9 +228,10 @@ Performances
 
 On a machine with 32 processors i9-13950HX, 64 Gb RAM, Hol2dk master, HOL-Light 3.0.0, OCaml 5.2.1, Camlp5 8.03.01, Lambdapi c24b28e2 and Coq 8.20.0:
 
-| HOL-Light file | dump  | size | steps | thms | lp  | v   | size | vo     |
-|----------------|-------|------|-------|------|-----|-----|------|--------|
-| hol.ml         | 3m58s | 3 Gb | 3 M   | 5687 | 40s | 37s | 1 Gb | 52m21s |
+| HOL-Light file               | dump  | size   | steps | thms  | lp  | v   | size  | vo      |
+|------------------------------|-------|--------|-------|-------|-----|-----|-------|---------|
+| hol.ml                       | 3m58s | 3 Gb   | 3 M   | 5687  | 40s | 37s | 1 Gb  | 52m21s  |
+| Multivariate/make_complex.ml | 3h    | 135 Gb | 85 M  | 40728 | 48m | 31m | 91 Gb | >23h47m |
 
 Translating HOL-Light proofs to Dedukti
 ---------------------------------------

diff --git a/main.ml b/main.ml
@@ -136,7 +136,7 @@ hol2dk env
 hol2dk nbp $base
   print the number of useful proof steps in $base.prf
 
-hol2dk proof $base $x $y
+hol2dk proof $base $x [$y]
   print proof steps between theorem indexes $x and $y
 
 hol2dk print use $base $x

diff --git a/renaming.lp b/renaming.lp
@@ -96,3 +96,5 @@ builtin "dollardollar" ≔ ﹩﹩;
 builtin "dollardollar_def" ≔ ﹩﹩_def;
 builtin "longarrow" ≔ ⭬;
 builtin "longarrow_def" ≔ ⭬_def;
+builtin "Z'" ≔ Z;
+builtin "Z''" ≔ Z';
diff --git a/xlp.ml b/xlp.ml
@@ -68,7 +68,7 @@ let string_of_typ_name n =
   match n with
   | "" -> assert false
   (* type names used also as constant names are capitalized *)
-  |"sum"|"topology"|"metric"|"multiset"|"group"|"multivector"|"real" ->
+  |"sum"|"topology"|"metric"|"multiset"|"group"|"multivector"|"real"|"matroid" ->
     String.capitalize_ascii n
   | _ ->
     if n.[0] = '?' then "_" ^ String.sub n 1 (String.length n - 1) else n