X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=3d684fe39b0ff27f57fd3eb6cd23180d30042f20;hb=cfda0acfce3f5e0b843bfe2b7ba7c371e5690db0;hp=159d3451e69cdc1782f606014684795f5b6d060a;hpb=c2d62f24fdcfad145abceafa418593dfcfb4b546;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 159d3451e..3d684fe39 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -27,6 +27,9 @@ open Printf
 
 module Ast = CicNotationPt
 
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
 type pattern_id = int
 type interpretation_id = pattern_id
 type pretty_printer_id = pattern_id
@@ -78,25 +81,33 @@ 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
 let hovbox = box Ast.HOV
 let break = Ast.Layout Ast.Break
-(* let reset_href t = Ast.AttributedTerm (`Href [], t) *)
-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 builtin_symbol s = Ast.Literal (`Symbol s)
+let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k))
+
 let number s =
-  reset_href
-    (add_xml_attrs (RenderingAttrs.number_attributes `MathML)
-      (Ast.Literal (`Number s)))
+  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)
@@ -108,7 +119,8 @@ let string_of_sort_kind = function
   | `Type -> "Type"
 
 let pp_ast0 t k =
-  let rec aux = function
+  let rec aux =
+    function
     | Ast.Appl ts ->
         add_level_info Ast.apply_prec Ast.apply_assoc
           (hovbox true true (CicNotationUtil.dress break (List.map k ts)))
@@ -129,7 +141,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 +149,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
@@ -311,9 +323,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) ->
@@ -324,6 +334,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
@@ -332,14 +349,18 @@ 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 ->
-              let (capture_variables, rhs) = eat_branch ty pat in
-              ((name, capture_variables), rhs))
-            constructors patterns
+          try
+            List.map2
+              (fun (name, ty) pat ->
+                incr j;
+                let (capture_variables, rhs) = eat_branch ty pat in
+                ((name, Some (ctor_puri !j), capture_variables), rhs))
+              constructors patterns
+          with Invalid_argument _ -> assert false
         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
@@ -407,7 +428,9 @@ let instantiate21 env (* precedence associativity *) l1 =
         let ty, value =
           try
             List.assoc name env
-          with Not_found -> assert false
+          with Not_found ->
+            prerr_endline ("name " ^ name ^ " not found in environment");
+            assert false
         in
         assert (CicNotationEnv.well_typed ty value); (* INVARIANT *)
         (* following assertion should be a conditional that makes this
@@ -415,8 +438,8 @@ let instantiate21 env (* precedence associativity *) l1 =
         assert (CicNotationEnv.well_typed expected_ty value);
         [ CicNotationEnv.term_of_value value ]
     | Ast.Magic m -> subst_magic env m
-    | Ast.Literal (`Keyword k) as t -> [ (*reset_href*) (add_keyword_attrs t) ]
-    | Ast.Literal _ as t -> [ (*reset_href*) t ]
+    | Ast.Literal (`Keyword k) as t -> [ add_keyword_attrs t ]
+    | Ast.Literal _ as t -> [ t ]
     | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ]
     | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ]
   and subst_magic env = function
@@ -439,8 +462,8 @@ let instantiate21 env (* precedence associativity *) l1 =
               instantiate_list (CicNotationUtil.group (subst env p) :: acc) []
           | value_set :: tl ->
               let env = CicNotationEnv.combine rec_decls value_set in
-              instantiate_list
-                (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl
+              let terms = subst env p in
+              instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl
         in
         instantiate_list [] values
     | Ast.Opt p ->
@@ -484,24 +507,23 @@ let rec pp_ast1 term =
   let ast_env_of_env env =
     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
   in
-  match term with
-  | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t)
-  | _ ->
-      (match (get_compiled21 ()) term with
-      | None -> pp_ast0 term pp_ast1
-      | Some (env, pid) ->
-          let prec, assoc, l1 =
-            try
-              Hashtbl.find level1_patterns21 pid
-            with Not_found -> assert false
-          in
-          add_level_info prec assoc (instantiate21 (ast_env_of_env env) l1))
+(* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *)
+  (match (get_compiled21 ()) term with
+  | None -> pp_ast0 term pp_ast1
+  | Some (env, pid) ->
+      let prec, assoc, l1 =
+        try
+          Hashtbl.find level1_patterns21 pid
+        with Not_found -> assert false
+      in
+      add_level_info prec assoc (instantiate21 (ast_env_of_env env) l1))
 
 let instantiate32 term_info env symbol args =
   let rec instantiate_arg = function
     | Ast.IdentArg (n, name) ->
         let t = (try List.assoc name env with Not_found -> assert false) in
         let rec count_lambda = function
+          | Ast.AttributedTerm (_, t) -> count_lambda t
           | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
           | _ -> 0
         in
@@ -545,13 +567,18 @@ let load_patterns21 t =
   set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t))
 
 let ast_of_acic id_to_sort annterm =
+  debug_print (lazy ("ast_of_acic <- "
+    ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
   let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
   let ast = ast_of_acic1 term_info annterm in
+  debug_print (lazy ("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 =
+  debug_print (lazy "pp_ast <-");
+  let ast' = pp_ast1 ast in
+  debug_print (lazy ("pp_ast -> " ^ CicNotationPp.pp_term ast'));
+  ast'
 
 let fresh_id =
   let counter = ref ~-1 in