X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcexpr2pres.ml;fp=helm%2Focaml%2Fcic_transformations%2Fcexpr2pres.ml;h=0000000000000000000000000000000000000000;hp=40f185dcdbc773ed5d2b03b08d8a97ea6074e05a;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff

diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml
deleted file mode 100644
index 40f185dcd..000000000
--- a/helm/ocaml/cic_transformations/cexpr2pres.ml
+++ /dev/null
@@ -1,398 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(**************************************************************************)
-(*                                                                        *)
-(*                           PROJECT HELM                                 *)
-(*                                                                        *)
-(*                Andrea Asperti <asperti@cs.unibo.it>                    *)
-(*                             28/6/2003                                   *)
-(*                                                                        *)
-(**************************************************************************)
-
-module P = Mpresentation;;
-
-let symbol_table = Hashtbl.create 503;;
-let symbol_table_charcount = Hashtbl.create 503;;
-
-let maxsize = 25;;
-
-let countterm current_size t =
-  let module CE = Content_expressions in
-  let rec aux current_size t =
-    if current_size > maxsize then current_size 
-    else match t with
-      CE.Symbol (_,name,None,_) -> current_size + (String.length name)
-    | CE.Symbol (_,name,Some subst,_) -> 
-        let c1 = current_size + (String.length name) in 
-        countsubst subst c1
-    | CE.LocalVar (_,name) -> current_size + (String.length name)
-    | CE.Meta (_,name) -> current_size + (String.length name)
-    | CE.Num (_,value) -> current_size + (String.length value)
-    | CE.Appl (_,l) -> 
-        List.fold_left aux current_size l
-    | CE.Binder (_, _,(n,s),body) -> 
-        let cs = aux (current_size + 2 + (String.length n)) s in
-        aux cs body
-    | CE.Letin (_,(n,s),body) ->
-        let cs = aux (current_size + 3 + (String.length n)) s in
-        aux cs body
-    | CE.Letrec (_,defs,body) ->
-        let cs = 
-          List.fold_left 
-            (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size defs in
-        aux cs body
-    | CE.Case (_,a,np) ->
-        let cs = aux (current_size + 4) a in
-        List.fold_left 
-          (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size np
-  and
-  countsubst subst current_size =
-    List.fold_left 
-      (fun current_size (uri,expr) ->
-         if (current_size > maxsize) then current_size
-         else 
-           let c1 = 
-             (current_size + (String.length (UriManager.name_of_uri uri))) in
-           (aux c1 expr)) current_size subst
-  in
-  (aux current_size t)
-;;
-
-let is_big t = 
-  ((countterm 0 t) > maxsize)
-;;
-
-let rec make_attributes l1 =
-  function
-      [] -> []
-    | None::tl -> make_attributes (List.tl l1) tl
-    | (Some s)::tl ->
-       let p,n = List.hd l1 in
-        (p,n,s)::(make_attributes (List.tl l1) tl)
-;;
-
-let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
-  let module CE = Content_expressions in
-  let module P = Mpresentation in
-  let rec aux =
-  function
-      CE.Symbol (xref,name,None,uri) -> 
-        let attr = 
-         make_attributes 
-          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
-        if tail = [] then
-          P.Mi (attr,name)
-        else P.Mrow([],P.Mi (attr,name)::tail)
-    | CE.Symbol (xref,name,Some subst,uri) ->
-        let attr = 
-         make_attributes 
-          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
-        let rec make_subst =
-          (function 
-               [] -> assert false
-             | [(uri,a)] -> 
-                 [(aux a);
-                  P.Mtext([],"/");
-                  P.Mi([],UriManager.name_of_uri uri)]
-             | (uri,a)::tl -> 
-                 (aux a)::
-                 P.Mtext([],"/")::
-                 P.Mi([],UriManager.name_of_uri uri)::
-                 P.Mtext([],"; ")::
-                 P.smallskip::
-                 (make_subst tl)) in
-        P.Mrow ([],
-          P.Mi (attr,name)::
-          P.Mtext([],"[")::
-          (make_subst subst)@
-          (P.Mtext([],"]")::tail))
-    | CE.LocalVar (xref,name) -> 
-        let attr = make_attributes [Some "helm","xref"] [xref] in
-        if tail = [] then
-          P.Mi (attr,name)
-        else P.Mrow([],P.Mi (attr,name)::tail)
-    | CE.Meta (xref,name) ->
-        let attr = make_attributes [Some "helm","xref"] [xref] in
-        if tail = [] then
-          P.Mi (attr,name)
-        else P.Mrow([],P.Mi (attr,name)::tail)
-    | CE.Num (xref,value) -> 
-        let attr = make_attributes [Some "helm","xref"] [xref] in
-        if tail = [] then
-          P.Mn (attr,value)
-        else P.Mrow([],P.Mn (attr,value)::tail)
-    | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
-        let aattr = make_attributes [Some "helm","xref"] [axref] in
-        let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
-        (try 
-          (let f = Hashtbl.find symbol_table n in
-           f tl ~priority ~assoc ~tail aattr sattr)
-        with notfound ->
-           P.Mrow(aattr,
-           P.Mo([],"(")::P.Mi(sattr,n)::(make_args tl)@(P.Mo([],")")::tail)))
-    | CE.Appl (xref,l) as t ->
-        let attr = make_attributes [Some"helm","xref"] [xref] in
-        P.Mrow(attr,
-           P.Mo([],"(")::(make_args l)@(P.Mo([],")")::tail))
-    | CE.Binder (xref, kind,(n,s),body) ->
-        let attr = make_attributes [Some "helm","xref"] [xref] in
-        let binder = 
-          if kind = "Lambda" then 
-             Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
-          else if kind = "Prod" then
-             Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
-          else if kind = "Forall" then
-             Netconversion.ustring_of_uchar `Enc_utf8 0x2200
-          else if kind = "Exists" then
-             Netconversion.ustring_of_uchar `Enc_utf8 0x2203
-          else "unknown" in
-        P.Mrow (attr, 
-           P.Mtext([None,"mathcolor","Blue"],binder)::
-           P.Mtext([],n ^ ":")::
-           (aux s)::
-           P.Mo([],".")::
-           (aux body)::tail)
-    | CE.Letin (xref,(n,s),body) ->
-        let attr = make_attributes [Some "helm","xref"] [xref] in
-        P.Mrow (attr, 
-           P.Mtext([],("let "))::
-           P.Mtext([],(n ^ "="))::
-           (aux s)::
-           P.Mtext([]," in ")::
-           (aux body)::tail)
-    | CE.Letrec (xref,defs,body) ->
-        let attr = make_attributes [Some "helm","xref"] [xref] in
-        let rec make_defs =
-          (function 
-               [] -> assert false
-             | [(n,bo)] -> 
-                 [P.Mtext([],(n ^ "="));(aux body)]
-             | (n,bo)::tl -> 
-                 P.Mtext([],(n ^ "="))::
-                 (aux body)::P.Mtext([]," and")::(make_defs tl)) in
-        P.Mrow (attr,  
-          P.Mtext([],("let rec "))::
-          (make_defs defs)@
-           (P.Mtext([]," in ")::
-           (aux body)::tail))
-    | CE.Case (xref,a,np) ->
-        let attr = make_attributes [Some "helm","xref"] [xref] in
-        let rec make_patterns =
-          (function 
-               [] -> []
-             | [(n,p)] -> 
-                 [P.Mtext([],(n ^ " -> "));(aux p)]
-             | (n,p)::tl -> 
-                 P.Mtext([],(n ^ " -> "))::
-                 (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in
-        P.Mrow (attr,  
-          P.Mtext([],("case "))::
-          (aux a)::
-          P.Mtext([],(" of "))::
-          (make_patterns np)@tail) in
-  aux t
-
-and
-
-make_args ?(priority = 0) ?(assoc = false) ?(tail = []) =
-  let module P = Mpresentation in
-  function
-      [] -> tail
-    | a::tl -> P.smallskip::(cexpr2pres a)::(make_args ~tail:tail tl)
-;;
-
-let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
-  let module P = Mpresentation in 
-  function
-    [] -> []
-  | [a] -> 
-      [P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount ~tail:tail a))])]
-  | (a::tl) as l ->
-      let c = List.fold_left countterm 0 l in
-      if c > maxsize then
-        P.Mtr([],[P.Mtd([],P.indented (cexpr2pres_charcount a))])::
-        (make_args_charcount ~tail:tail tl)
-      else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([None,"width","0.2cm"]))::(make_args ~tail:tail l)))])]
-
-(* 
-  function 
-      [] -> []
-    | a::tl -> 
-        let tlpres = 
-          let c = List.fold_left countterm 0 tl in
-          if c > maxsize then
-            P.Mtable ([("align","baseline 1");("equalrows","false");
-             ("columnalign","left")],
-              (make_args_charcount tl))
-          else 
-            P.Mrow([], make_args tl) in
-        [P.Mtr([],[P.Mtd([],(cexpr2pres_charcount a))]);
-         P.Mtr([],[P.Mtd([],P.indented tlpres)])] *)
-and  
-
-cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
-  let module CE = Content_expressions in
-  let module P = Mpresentation in
-  let rec aux =
-  function
-      CE.Symbol (xref,name,None,uri) -> 
-        let attr = 
-         make_attributes 
-          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
-        if tail = [] then
-          P.Mi (attr,name)
-        else P.Mrow ([],P.Mi (attr,name)::tail)
-    | CE.Symbol (xref,name,Some subst,uri) ->
-        let attr = 
-         make_attributes 
-          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
-        let rec make_subst =
-          (function 
-               [] -> assert false
-             | [(uri,a)] -> 
-                 [(cexpr2pres a);
-                  P.Mtext([],"/");
-                  P.Mi([],UriManager.name_of_uri uri)]
-             | (uri,a)::tl -> 
-                 (cexpr2pres a)::
-                 P.Mtext([],"/")::
-                 P.Mi([],UriManager.name_of_uri uri)::
-                 P.Mtext([],"; ")::
-                 P.smallskip::
-                 (make_subst tl)) in
-        P.Mrow ([],
-          P.Mi (attr,name)::
-          P.Mtext([],"[")::
-          (make_subst subst)@
-          (P.Mtext([],"]")::tail))
-    | CE.LocalVar (xref,name) -> 
-        let attr = make_attributes [Some "helm","xref"] [xref] in
-        if tail = [] then
-          P.Mi (attr,name)
-        else P.Mrow ([],P.Mi (attr,name)::tail)
-    | CE.Meta (xref,name) ->
-        let attr = make_attributes [Some "helm","xref"] [xref] in
-        if tail = [] then
-          P.Mi (attr,name)
-        else P.Mrow ([],P.Mi (attr,name)::tail)
-    | CE.Num (xref,value) -> 
-        let attr = make_attributes [Some "helm","xref"] [xref] in
-        if tail = [] then
-          P.Mn (attr,value)
-        else P.Mrow ([],P.Mn (attr,value)::tail)
-    | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) ->
-        let aattr = make_attributes [Some "helm","xref"] [axref] in
-        let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in
-        if (is_big t) then
-          (try 
-            (let f = Hashtbl.find symbol_table_charcount n in
-             f tl ~priority ~assoc ~tail aattr sattr)
-          with notfound ->
-            P.Mtable (aattr@P.standard_tbl_attr,
-              P.Mtr([],[P.Mtd([],P.Mrow([],
-                [P.Mtext([],"(");
-                 cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))])::
-              make_args_charcount ~tail:(P.Mtext([],")")::tail) tl))
-        else cexpr2pres t
-    | CE.Appl (xref,l) as t ->
-        let attr = make_attributes [Some "helm","xref"] [xref] in
-        if (is_big t) then
-          P.Mtable (attr@P.standard_tbl_attr,
-            P.Mtr([],[P.Mtd([],P.Mrow([],
-              [P.Mtext([],"(");
-               cexpr2pres_charcount (List.hd l)]))])::
-            make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l))
-        else cexpr2pres t
-    | CE.Binder (xref, kind,(n,s),body) as t ->
-        if (is_big t) then
-          let attr = make_attributes [Some "helm","xref"] [xref] in
-          let binder = 
-            if kind = "Lambda" then 
-              Netconversion.ustring_of_uchar `Enc_utf8 0x03bb  
-            else if kind = "Prod" then
-              Netconversion.ustring_of_uchar `Enc_utf8 0x03a0
-            else if kind = "Forall" then
-              Netconversion.ustring_of_uchar `Enc_utf8 0x2200
-            else if kind = "Exists" then
-              Netconversion.ustring_of_uchar `Enc_utf8 0x2203
-            else "unknown" in  
-          P.Mtable (attr@P.standard_tbl_attr,
-             [P.Mtr ([],[P.Mtd ([],
-               P.Mrow([],
-                [P.Mtext([None,"mathcolor","Blue"],binder);
-                 P.Mtext([],n ^ ":");
-                 cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]);
-              P.Mtr ([],[P.Mtd ([],
-               P.indented (cexpr2pres_charcount body ~tail:tail))])]) 
-        else (cexpr2pres t ~tail:tail)
-    | CE.Letin (xref,(n,s),body) as t ->
-        if (is_big t) then
-          let attr = make_attributes [Some "helm","xref"] [xref] in
-          P.Mtable (attr@P.standard_tbl_attr,
-             [P.Mtr ([],[P.Mtd ([],
-               P.Mrow([],
-                [P.Mtext([None,"mathcolor","Blue"],"let");
-                 P.smallskip;
-                 P.Mtext([],n ^ "=");
-                 cexpr2pres_charcount s;
-                 P.smallskip;
-                 P.Mtext([],"in");
-                ]))]);
-              P.Mtr ([],[P.Mtd ([],
-               P.indented (cexpr2pres_charcount body))])])
-        else (cexpr2pres t)
-    | CE.Letrec (xref,defs,body) ->
-        let attr = make_attributes [Some "helm","xref"] [xref] in
-        let rec make_defs =
-          (function 
-               [] -> assert false
-             | [(n,bo)] -> 
-                 [P.Mtext([],(n ^ "="));(aux body)]
-             | (n,bo)::tl -> 
-                 P.Mtext([],(n ^ "="))::
-                 (aux body)::P.Mtext([]," and")::(make_defs tl)) in
-        P.Mrow (attr,  
-          P.Mtext([],("let rec "))::
-          (make_defs defs)@
-          [P.Mtext([]," in ");
-           (aux body)])
-    | CE.Case (xref,a,np) ->
-        let attr = make_attributes [Some "helm","xref"] [xref] in
-        let rec make_patterns =
-          (function 
-               [] -> []
-             | [(n,p)] -> 
-                 [P.Mtext([],(n ^ " -> "));(aux p)]
-             | (n,p)::tl -> 
-                 P.Mtext([],(n ^ " -> "))::
-                 (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in
-        P.Mrow (attr,  
-          P.Mtext([],("case "))::
-          (aux a)::
-          P.Mtext([],(" of "))::
-          (make_patterns np)) in
-  aux t
-;;