X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=6340d88a15db67f3dddc364540bfddfb702dac02;hb=ed7711935c7377ea8785a9f3b85984785b92030e;hp=b5d3d271dbd798880fa947b15b4652c660be9fed;hpb=e80eed78f048a235b44d2fd266c4b5a4dd951632;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index b5d3d271d..6340d88a1 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 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
 
-module Ast = CicNotationPt
-
 type term_info =
   { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
     uri: (Cic.id, string) Hashtbl.t;
@@ -78,24 +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 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)
@@ -104,10 +116,11 @@ let string_of_sort_kind = function
   | `Prop -> "Prop"
   | `Set -> "Set"
   | `CProp -> "CProp"
-  | `Type -> "Type"
+  | `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)))
@@ -128,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 [
@@ -136,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
@@ -188,6 +201,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 =
@@ -259,7 +273,9 @@ let ast_of_acic0 term_info acic k =
   let sort_of_id id =
     try
       Hashtbl.find term_info.sort id
-    with Not_found -> assert false
+    with Not_found ->
+      prerr_endline (sprintf "warning: sort of id %s not found, using Type" id);
+      `Type (CicUniv.fresh ())
   in
   let aux_substs substs =
     Some
@@ -282,13 +298,13 @@ let ast_of_acic0 term_info acic k =
     | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context l))
     | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
     | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
-    | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type)
+    | Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
     | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
     | Cic.AImplicit _ -> assert false
     | Cic.AProd (id,n,s,t) ->
         let binder_kind =
           match sort_of_id id with
-          | `Set | `Type -> `Pi
+          | `Set | `Type _ -> `Pi
           | `Prop | `CProp -> `Forall
         in
         idref id (Ast.Binder (binder_kind,
@@ -307,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) ->
@@ -320,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
@@ -328,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
@@ -393,17 +418,19 @@ let get_compiled32 () =
 let set_compiled21 f = compiled21 := Some f
 let set_compiled32 f = compiled32 := Some f
 
-let instantiate21 env (* precedence associativity *) l1 =
+let instantiate21 env l1 =
   let rec subst_singleton env t =
     CicNotationUtil.group (subst env t)
   and subst env = function
-    | Ast.AttributedTerm (_, t) -> subst env t
+    | Ast.AttributedTerm (attr, t) -> subst env t
     | Ast.Variable var ->
         let name, expected_ty = CicNotationEnv.declaration_of_var var in
         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
@@ -411,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
@@ -435,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 ->
@@ -480,8 +507,9 @@ let rec pp_ast1 term =
   let ast_env_of_env env =
     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
   in
+(* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *)
   match term with
-  | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t)
+  | Ast.AttributedTerm (attrs, term) -> Ast.AttributedTerm (attrs, pp_ast1 term)
   | _ ->
       (match (get_compiled21 ()) term with
       | None -> pp_ast0 term pp_ast1
@@ -498,6 +526,7 @@ let instantiate32 term_info env symbol args =
     | 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
@@ -541,13 +570,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