X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcexpr2pres.ml;h=5210840c88c83321d9ccaf469f94a9678532222a;hb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;hp=841ccf3da57e3f58d4c69070b889ef89b2e22b2f;hpb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml
index 841ccf3da..5210840c8 100644
--- a/helm/ocaml/cic_transformations/cexpr2pres.ml
+++ b/helm/ocaml/cic_transformations/cexpr2pres.ml
@@ -33,52 +33,56 @@
 (**************************************************************************)
 
 module P = Mpresentation;;
+module CE = Content_expressions;;
 
 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
+let rec countterm 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,l) ->
+     List.fold_left
+      (fun i t ->
+        match t with
+           None -> i
+         | Some t' -> countterm i t'
+      ) (current_size + String.length name) l
+  | CE.Num (_,value) -> current_size + (String.length value)
+  | CE.Appl (_,l) -> 
+      List.fold_left countterm current_size l
+  | CE.Binder (_, _,(n,s),body) -> 
+      let cs = countterm (current_size + 2 + (String.length n)) s in
+      countterm cs body
+  | CE.Letin (_,(n,s),body) ->
+      let cs = countterm (current_size + 3 + (String.length n)) s in
+      countterm cs body
+  | CE.Letrec (_,defs,body) ->
+      let cs = 
         List.fold_left 
-          (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size np
-  and
-  countsubst subst current_size =
+          (fun c (n,bo) -> countterm (c+(String.length n)) bo) current_size defs in
+      countterm cs body
+  | CE.Case (_,a,np) ->
+      let cs = countterm (current_size + 4) a in
+      List.fold_left 
+        (fun c (n,bo) -> countterm (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)
+           (countterm c1 expr)) current_size subst
 ;;
 
 let is_big t = 
@@ -89,7 +93,9 @@ let rec make_attributes l1 =
   function
       [] -> []
     | None::tl -> make_attributes (List.tl l1) tl
-    | (Some s)::tl -> (List.hd l1,s)::(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 =
@@ -100,14 +106,14 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
       CE.Symbol (xref,name,None,uri) -> 
         let attr = 
          make_attributes 
-          ["helm:xref";"xlink:href"] [xref;uri] in
+          [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 
-          ["helm:xref";"xlink:href"] [xref;uri] in
+          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
         let rec make_subst =
           (function 
                [] -> assert false
@@ -128,23 +134,32 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
           (make_subst subst)@
           (P.Mtext([],"]")::tail))
     | CE.LocalVar (xref,name) -> 
-        let attr = make_attributes ["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 ["helm:xref"] [xref] in
+        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,l) ->
+        let attr = make_attributes [Some "helm","xref"] [xref] in
+        let l' =
+         List.map
+          (function
+              None -> P.Mo([],"_")
+            | Some t -> cexpr2pres t
+          ) l
+        in
+         if tail = [] then
+           P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
+         else
+           P.Mrow
+            ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
     | CE.Num (xref,value) -> 
-        let attr = make_attributes ["helm:xref"] [xref] in
+        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 ["helm:xref"] [axref] in
-        let sattr = make_attributes ["helm:xref";"xlink:href"] [sxref;uri] in
+        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)
@@ -152,11 +167,11 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
            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 ["helm:xref"] [xref] in
+        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 ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         let binder = 
           if kind = "Lambda" then 
              Netconversion.ustring_of_uchar `Enc_utf8 0x03bb
@@ -168,13 +183,13 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
              Netconversion.ustring_of_uchar `Enc_utf8 0x2203
           else "unknown" in
         P.Mrow (attr, 
-           P.Mtext([("mathcolor","Blue")],binder)::
+           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 ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         P.Mrow (attr, 
            P.Mtext([],("let "))::
            P.Mtext([],(n ^ "="))::
@@ -182,7 +197,7 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
            P.Mtext([]," in ")::
            (aux body)::tail)
     | CE.Letrec (xref,defs,body) ->
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         let rec make_defs =
           (function 
                [] -> assert false
@@ -197,20 +212,33 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t =
            (P.Mtext([]," in ")::
            (aux body)::tail))
     | CE.Case (xref,a,np) ->
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         let rec make_patterns =
           (function 
                [] -> []
-             | [(n,p)] -> 
-                 [P.Mtext([],(n ^ " -> "));(aux p)]
+             | [(n,p)] -> make_pattern n p
              | (n,p)::tl -> 
-                 P.Mtext([],(n ^ " -> "))::
-                 (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in
+                 (make_pattern n p)@(P.smallskip::
+                 P.Mtext([],"|")::P.smallskip::(make_patterns tl)))
+        and make_pattern n p =           
+          let rec get_vars_and_body = 
+            (function
+                CE.Binder (_, "Lambda",(n,_),body) ->
+                  let v,b = get_vars_and_body body in
+                  n::v,b 
+              | t -> [],t) in
+          let vars,body = get_vars_and_body p in
+          let lhs = 
+            match vars with 
+	        [] -> n ^ " -> "
+              | l -> "(" ^ n ^" "^(String.concat " " l) ^ ")" ^ " -> " in
+          [P.Mtext([],lhs);P.smallskip;aux body] in
         P.Mrow (attr,  
-          P.Mtext([],("case "))::
-          (aux a)::
-          P.Mtext([],(" of "))::
-          (make_patterns np)@tail) in
+          P.Mtext([],"match")::P.smallskip::
+          (aux a)::P.smallskip::
+          P.Mtext([],"with")::P.smallskip::
+          P.Mtext([],"[")::P.smallskip::
+          (make_patterns np)@(P.smallskip::P.Mtext([],("]"))::tail))  in
   aux t
 
 and
@@ -233,7 +261,7 @@ let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
       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([("width","0.2cm")]))::(make_args ~tail:tail l)))])]
+      else [P.Mtr([],[P.Mtd([],P.Mrow([],(P.Mspace([None,"width","0.2cm"]))::(make_args ~tail:tail l)))])]
 
 (* 
   function 
@@ -252,21 +280,20 @@ let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) =
 and  
 
 cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
-  let module CE = Content_expressions in
-  let module P = Mpresentation in
-  let rec aux =
-  function
+  if not(is_big t) then (cexpr2pres ~priority ~assoc ~tail t) 
+  else let aux = cexpr2pres_charcount in
+  match t with
       CE.Symbol (xref,name,None,uri) -> 
         let attr = 
          make_attributes 
-          ["helm:xref";"xlink:href"] [xref;uri] in
+          [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 
-          ["helm:xref";"xlink:href"] [xref;uri] in
+          [Some "helm","xref";Some "xlink","href"] [xref;uri] in
         let rec make_subst =
           (function 
                [] -> assert false
@@ -287,83 +314,84 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
           (make_subst subst)@
           (P.Mtext([],"]")::tail))
     | CE.LocalVar (xref,name) -> 
-        let attr = make_attributes ["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 ["helm:xref"] [xref] in
+        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,l) ->
+        let attr = make_attributes [Some "helm","xref"] [xref] in
+        let l' =
+         List.map
+          (function
+              None -> P.Mo([],"_")
+            | Some t -> cexpr2pres t
+          ) l
+        in
+         if tail = [] then
+           P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")])
+         else
+           P.Mrow
+            ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail)
     | CE.Num (xref,value) -> 
-        let attr = make_attributes ["helm:xref"] [xref] in
+        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 ["helm:xref"] [axref] in
-        let sattr = make_attributes ["helm:xref";"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 ["helm:xref"] [xref] in
-        if (is_big t) then
-          P.Mtable (attr@P.standard_tbl_attr,
+        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_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_charcount (List.hd l)]))])::
-            make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l))
-        else cexpr2pres t
+               cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))])::
+            make_args_charcount ~tail:(P.Mtext([],")")::tail) tl))
+    | CE.Appl (xref,l) as t ->
+        let attr = make_attributes [Some "helm","xref"] [xref] in
+        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))
     | CE.Binder (xref, kind,(n,s),body) as t ->
-        if (is_big t) then
-          let attr = make_attributes ["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([("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)
+        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))])]) 
     | CE.Letin (xref,(n,s),body) as t ->
-        if (is_big t) then
-          let attr = make_attributes ["helm:xref"] [xref] in
-          P.Mtable (attr@P.standard_tbl_attr,
-             [P.Mtr ([],[P.Mtd ([],
-               P.Mrow([],
-                [P.Mtext([("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)
+        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))])])
     | CE.Letrec (xref,defs,body) ->
-        let attr = make_attributes ["helm:xref"] [xref] in
+        let attr = make_attributes [Some "helm","xref"] [xref] in
         let rec make_defs =
           (function 
                [] -> assert false
@@ -378,19 +406,55 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t =
           [P.Mtext([]," in ");
            (aux body)])
     | CE.Case (xref,a,np) ->
-        let attr = make_attributes ["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
+        let attr = make_attributes [Some "helm","xref"] [xref] in
+        let arg = 
+          if (is_big a) then
+            let tail = P.Mtext([],(" with"))::tail in
+            [P.Mtr ([],[P.Mtd ([],P.Mtext([],("match ")))]);
+             P.Mtr ([],[P.Mtd ([],aux a ~tail:tail)])]
+          else 
+            [P.Mtr ([],[P.Mtd ([],P.Mrow([],[P.Mtext([],("match"));P.smallskip;aux a ~tail:tail; P.smallskip;P.Mtext([],("with"))]))])] in
+        let rec make_patterns is_first ~tail =
+          function 
+              [] -> []
+            | [(n,p)] ->
+                let sep = 
+                  if is_first then "[ " else "| " in
+                [P.Mtr ([],
+                  [P.Mtd ([],
+                     make_pattern sep ~tail n p)])]
+            | (n,p)::tl -> 
+                let sep = 
+                  if is_first then "[ " else "| " in
+                P.Mtr ([],
+                  [P.Mtd ([],
+                    make_pattern sep [] n p)])
+                ::(make_patterns false ~tail  tl)
+        and make_pattern sep ~tail n p =
+          let rec get_vars_and_body = 
+            function
+                CE.Binder (_, "Lambda",(n,_),body) ->
+                  let v,b = get_vars_and_body body in
+                  n::v,b 
+              | t -> [],t in
+          let vars,body = get_vars_and_body p in
+          let lhs = 
+            match vars with 
+	        [] -> sep ^ n ^ " -> "
+              | l -> sep ^"(" ^n^" "^(String.concat " " l) ^ ")" ^ " -> " in
+          if (is_big body) then
+            P.Mtable (P.standard_tbl_attr,
+              [P.Mtr ([],
+                [P.Mtd ([],P.Mtext([],lhs))]);
+               P.Mtr ([],
+                [P.Mtd ([],P.indented (aux ~tail body ))])])
+          else
+            P.Mrow([],[P.Mtext([],lhs);aux ~tail body]) in
+        let patterns =
+          make_patterns true np ~tail:(P.Mtext([],"]")::tail) in 
+        P.Mtable (attr@P.standard_tbl_attr,
+          arg@patterns)
 ;;
+
+
+