- bugfix: eta abstractions ignores attributed node while counting lambdas

- permit pattern matching on attributed asts (since attributes are transparent to pattern matching)
- wrapped with assert false some unsafe function invocations (e.g. List.map2)
- removed reset_href (no longer needed)

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 73f66771f8869695e9c90958b78a73ae88bcab79..d65eb0a5047724e1c49e2b8ee8408523e1a4c7bb 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -93,15 +93,12 @@ 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))
@@ -122,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)))
@@ -353,12 +351,14 @@ let ast_of_acic0 term_info acic k =
         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, Some (ctor_puri !j), 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 case_indty, Some (k ty), patterns))
     | Cic.AFix (id, no, funs) -> 
@@ -428,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
@@ -436,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
@@ -460,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 ->
@@ -505,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
@@ -566,12 +567,15 @@ let load_patterns21 t =
   set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t))
 
 let ast_of_acic id_to_sort annterm =
+  debug_print ("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 ("ast_of_acic -> " ^ CicNotationPp.pp_term ast);
   ast, term_info.uri
 
 let pp_ast ast =
+  debug_print "pp_ast <-";
   let ast' = pp_ast1 ast in
   debug_print ("pp_ast -> " ^ CicNotationPp.pp_term ast');
   ast'