X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=73f66771f8869695e9c90958b78a73ae88bcab79;hb=98d5d40127827a5c40e58cb0c9654066f940b0ea;hp=28edd491c84e7e32e97425176cb728e007e723e3;hpb=5a7ff7a3ce24bd14385d2295a1c77fad4b876cb8;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 28edd491c..73f66771f 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -25,12 +25,15 @@
 
 open Printf
 
+module Ast = CicNotationPt
+
+let debug = false
+let debug_print = if debug then prerr_endline else ignore
+
 type pattern_id = int
 type interpretation_id = pattern_id
 type pretty_printer_id = pattern_id
 
-module Ast = CicNotationPt
-
 type term_info =
   { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
     uri: (Cic.id, string) Hashtbl.t;
@@ -78,10 +81,13 @@ let rec remove_level_info =
   | t -> t
 
 let add_xml_attrs attrs t = Ast.AttributedTerm (`XmlAttrs attrs, t)
+
 let add_keyword_attrs =
   add_xml_attrs (RenderingAttrs.keyword_attributes `MathML)
+
 let box kind spacing indent content =
   Ast.Layout (Ast.Box ((kind, spacing, indent), content))
+
 let hbox = box Ast.H
 let vbox = box Ast.V
 let hvbox = box Ast.HV
@@ -91,12 +97,20 @@ let break = Ast.Layout Ast.Break
 let reset_href t = t
 let builtin_symbol s = reset_href (Ast.Literal (`Symbol s))
 let keyword k = reset_href (add_keyword_attrs (Ast.Literal (`Keyword k)))
+
 let number s =
   reset_href
     (add_xml_attrs (RenderingAttrs.number_attributes `MathML)
       (Ast.Literal (`Number s)))
+
 let ident i =
   add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None))
+
+let ident_w_href href i =
+  match href with
+  | None -> ident i
+  | Some href -> Ast.AttributedTerm (`Href [href], ident i)
+
 let binder_symbol s =
   add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML)
     (builtin_symbol s)
@@ -129,7 +143,7 @@ let pp_ast0 t k =
         let indty_box =
           match indty_opt with
           | None -> []
-          | Some indty -> [ keyword "in"; ident indty ]
+          | Some (indty, href) -> [ keyword "in"; ident_w_href href indty ]
         in
         let match_box =
           hvbox false true [
@@ -137,8 +151,8 @@ let pp_ast0 t k =
             hvbox false false ([ k what ] @ indty_box); break;
             keyword "with" ]
         in
-        let mk_case_pattern (head, vars) =
-          hbox true false (ident head :: List.map aux_var vars)
+        let mk_case_pattern (head, href, vars) =
+          hbox true false (ident_w_href href head :: List.map aux_var vars)
         in
         let patterns' =
           List.map
@@ -189,6 +203,7 @@ let pp_ast0 t k =
               hvbox false true [
                 aux_var var; builtin_symbol "\\def"; break; k s ];
               break; keyword "in" ];
+            break;
             k t ])
     | Ast.LetRec (rec_kind, funs, where) ->
         let rec_op =
@@ -310,9 +325,7 @@ let ast_of_acic0 term_info acic k =
     | Cic.AMutInd (id,uri,i,substs) as t ->
         let name = name_of_inductive_type uri i in
         let uri_str = UriManager.string_of_uri uri in
-        let puri_str =
-          uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")"
-        in
+        let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (i+1) in
         register_uri id puri_str;
         idref id (Ast.Ident (name, aux_substs substs))
     | Cic.AMutConstruct (id,uri,i,j,substs) ->
@@ -323,6 +336,13 @@ let ast_of_acic0 term_info acic k =
         idref id (Ast.Ident (name, aux_substs substs))
     | Cic.AMutCase (id,uri,typeno,ty,te,patterns) ->
         let name = name_of_inductive_type uri typeno in
+        let uri_str = UriManager.string_of_uri uri in
+        let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in
+        let ctor_puri j =
+          UriManager.uri_of_string
+            (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j)
+        in
+        let case_indty = name, Some (UriManager.uri_of_string puri_str) in
         let constructors = constructors_of_inductive_type uri typeno in
         let rec eat_branch ty pat =
           match (ty, pat) with
@@ -331,14 +351,16 @@ let ast_of_acic0 term_info acic k =
               (CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs
           | _, _ -> [], k pat
         in
+        let j = ref 0 in
         let patterns =
           List.map2
             (fun (name, ty) pat ->
+              incr j;
               let (capture_variables, rhs) = eat_branch ty pat in
-              ((name, capture_variables), rhs))
+              ((name, Some (ctor_puri !j), capture_variables), rhs))
             constructors patterns
         in
-        idref id (Ast.Case (k te, Some name, Some (k ty), patterns))
+        idref id (Ast.Case (k te, Some case_indty, Some (k ty), patterns))
     | Cic.AFix (id, no, funs) -> 
         let defs = 
           List.map
@@ -546,11 +568,13 @@ let load_patterns21 t =
 let ast_of_acic id_to_sort annterm =
   let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
   let ast = ast_of_acic1 term_info annterm in
+  debug_print ("ast_of_acic -> " ^ CicNotationPp.pp_term ast);
   ast, term_info.uri
 
-let pp_ast term =
-(*   prerr_endline ("pp_ast <- : " ^ CicNotationPp.pp_term term); *)
-  pp_ast1 term
+let pp_ast ast =
+  let ast' = pp_ast1 ast in
+  debug_print ("pp_ast -> " ^ CicNotationPp.pp_term ast');
+  ast'
 
 let fresh_id =
   let counter = ref ~-1 in