pattern matching over Ast.Case simplified:

- it is not possible to match the `in intype` foo part
- it is not possible to match the outtype
eta expansion still done on Ast (hard to do it in Cic. The abstracted variable
does not have a type :-( thus you may have to double your notations. Name for fresh variables changed to \etaX instead of freshX (much shorter in terms of screen pixels)

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index 8997a924f46916b3739ac66e9b7dd719573cadaf..1ddd5c9c3b1572c74034fb70b4f2563867ee6786 100644 (file)
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -27,13 +27,19 @@
 
 module Ast = CicNotationPt
 
-let visit_ast ?(special_k = fun _ -> assert false) k =
+let visit_ast ?(special_k = fun _ -> assert false) 
+  ?(map_xref_option= fun x -> x) ?(map_case_indty= fun x -> x) 
+  ?(map_case_outtype=
+      fun k x -> match x with None -> None | Some x -> Some (k x)) 
+  k 
+=
   let rec aux = function
     | Ast.Appl terms -> Ast.Appl (List.map k terms)
     | Ast.Binder (kind, var, body) ->
         Ast.Binder (kind, aux_capture_variable var, k body) 
     | Ast.Case (term, indtype, typ, patterns) ->
-        Ast.Case (k term, indtype, aux_opt typ, aux_patterns patterns)
+        Ast.Case (k term, map_case_indty indtype, map_case_outtype k typ,
+          aux_patterns map_xref_option patterns)
     | Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2)
     | Ast.LetIn (var, t1, t3) ->
         Ast.LetIn (aux_capture_variable var, k t1, k t3)
@@ -66,11 +72,11 @@ let visit_ast ?(special_k = fun _ -> assert false) k =
     | None -> None
     | Some term -> Some (k term)
   and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
-  and aux_patterns patterns = List.map aux_pattern patterns
-  and aux_pattern =
+  and aux_patterns k_xref patterns = List.map (aux_pattern k_xref) patterns
+  and aux_pattern k_xref =
    function
       Ast.Pattern (head, hrefs, vars), term ->
-        Ast.Pattern (head, hrefs, List.map aux_capture_variable vars), k term
+        Ast.Pattern (head, k_xref hrefs, List.map aux_capture_variable vars), k term
     | Ast.Wildcard, term -> Ast.Wildcard, k term
   and aux_subst (name, term) = (name, k term)
   and aux_substs substs = List.map aux_subst substs
@@ -355,7 +361,7 @@ let fresh_id () =
   !fresh_index
 
   (* TODO ensure that names generated by fresh_var do not clash with user's *)
-let fresh_name () = "fresh" ^ string_of_int (fresh_id ())
+let fresh_name () = "η" ^ string_of_int (fresh_id ())
 
 let rec freshen_term ?(index = ref 0) term =
   let freshen_term = freshen_term ~index in

diff --git a/helm/software/components/acic_content/cicNotationUtil.mli b/helm/software/components/acic_content/cicNotationUtil.mli
index 2ead321f69f52badc233f21753c8e62bb15e668c..5a4e1c536f4bdb5f82023a0ac362e690019498f2 100644 (file)
--- a/helm/software/components/acic_content/cicNotationUtil.mli
+++ b/helm/software/components/acic_content/cicNotationUtil.mli
@@ -33,6 +33,12 @@ val keywords_of_term: CicNotationPt.term -> string list
 
 val visit_ast:
   ?special_k:(CicNotationPt.term -> CicNotationPt.term) ->
+  ?map_xref_option:(CicNotationPt.href option -> CicNotationPt.href option) ->
+  ?map_case_indty:(CicNotationPt.case_indtype option ->
+          CicNotationPt.case_indtype option) ->
+  ?map_case_outtype:((CicNotationPt.term -> CicNotationPt.term) -> 
+                     CicNotationPt.term option -> CicNotationPt.term
+  option) ->
   (CicNotationPt.term -> CicNotationPt.term) ->
   CicNotationPt.term ->
     CicNotationPt.term

diff --git a/helm/software/components/content_pres/content2presMatcher.ml b/helm/software/components/content_pres/content2presMatcher.ml
index 3c6a61a6fb169958176aef607d6a359ffd879753..0e85618896833b254b52e12970ff81f6a3f96b72 100644 (file)
--- a/helm/software/components/content_pres/content2presMatcher.ml
+++ b/helm/software/components/content_pres/content2presMatcher.ml
@@ -38,7 +38,12 @@ let get_tag term0 =
     subterms := t :: !subterms ; 
     Ast.Implicit
   in
-  let rec aux t = CicNotationUtil.visit_ast ~special_k map_term t
+  let rec aux t = 
+    CicNotationUtil.visit_ast 
+      ~map_xref_option:(fun _ -> None)
+      ~map_case_indty:(fun _ -> None)
+      ~map_case_outtype:(fun _ _ -> None)
+      ~special_k map_term t
   and special_k = function
     | Ast.AttributedTerm (_, t) -> aux t
     | _ -> assert false