X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationUtil.ml;h=b426863cf613e7f77d1123bb89cf747fe4ac18cf;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=8e487ed11ed293374f4737a39bbc0e975b0165ff;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index 8e487ed11..b426863cf 100644
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -27,20 +27,28 @@
 
 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, t2) ->
-        Ast.LetIn (aux_capture_variable var, k t1, k t2)
+    | Ast.LetIn (var, t1, t3) ->
+        Ast.LetIn (aux_capture_variable var, k t1, k t3)
     | Ast.LetRec (kind, definitions, term) ->
         let definitions =
           List.map
-            (fun (var, ty, n) -> aux_capture_variable var, k ty, n)
+            (fun (params, var, ty, decrno) ->
+              List.map aux_capture_variable params, aux_capture_variable var,
+              k ty, decrno)
             definitions
         in
         Ast.LetRec (kind, definitions, k term)
@@ -54,6 +62,7 @@ let visit_ast ?(special_k = fun _ -> assert false) k =
       | Ast.Magic _
       | Ast.Variable _) as t -> special_k t
     | (Ast.Ident _
+      | Ast.NRef _
       | Ast.Implicit
       | Ast.Num _
       | Ast.Sort _
@@ -64,9 +73,12 @@ 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 ((head, hrefs, vars), term) =
-    ((head, hrefs, List.map aux_capture_variable vars), k term)
+  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, 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
   in
@@ -80,11 +92,15 @@ let visit_layout k = function
   | Ast.Over (t1, t2) -> Ast.Over (k t1, k t2)
   | Ast.Atop (t1, t2) -> Ast.Atop (k t1, k t2)
   | Ast.Frac (t1, t2) -> Ast.Frac (k t1, k t2)
+  | Ast.InfRule (t1, t2, t3) -> Ast.InfRule (k t1, k t2, k t3)
   | Ast.Sqrt t -> Ast.Sqrt (k t)
   | Ast.Root (arg, index) -> Ast.Root (k arg, k index)
   | Ast.Break -> Ast.Break
   | Ast.Box (kind, terms) -> Ast.Box (kind, List.map k terms)
   | Ast.Group terms -> Ast.Group (List.map k terms)
+  | Ast.Mstyle (l, term) -> Ast.Mstyle (l, List.map k term)
+  | Ast.Mpadded (l, term) -> Ast.Mpadded (l, List.map k term)
+  | Ast.Maction terms -> Ast.Maction (List.map k terms)
 
 let visit_magic k = function
   | Ast.List0 (t, l) -> Ast.List0 (k t, l)
@@ -131,7 +147,7 @@ let names_of_term t =
   let aux = function
     | Ast.NumVar s
     | Ast.IdentVar s
-    | Ast.TermVar s -> s
+    | Ast.TermVar (s,_) -> s
     | _ -> assert false
   in
     List.map aux (variables_of_term t)
@@ -182,9 +198,9 @@ let meta_names_of_term term =
         aux term ;
         aux_opt outty_opt ;
         List.iter aux_branch patterns
-    | Ast.LetIn (_, t1, t2) ->
+    | Ast.LetIn (_, t1, t3) ->
         aux t1 ;
-        aux t2
+        aux t3
     | Ast.LetRec (_, definitions, body) ->
         List.iter aux_definition definitions ;
         aux body
@@ -211,9 +227,12 @@ let meta_names_of_term term =
   and aux_branch (pattern, term) =
     aux_pattern pattern ;
     aux term
-  and aux_pattern (head, _, vars) = 
-    List.iter aux_capture_var vars
-  and aux_definition (var, term, i) =
+  and aux_pattern =
+   function
+      Ast.Pattern (head, _, vars) -> List.iter aux_capture_var vars
+    | Ast.Wildcard -> ()
+  and aux_definition (params, var, term, decrno) =
+    List.iter aux_capture_var params ;
     aux_capture_var var ;
     aux term
   and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
@@ -221,7 +240,7 @@ let meta_names_of_term term =
   and aux_variable = function
     | Ast.NumVar name -> add_name name
     | Ast.IdentVar name -> add_name name
-    | Ast.TermVar name -> add_name name
+    | Ast.TermVar (name,_) -> add_name name
     | Ast.FreshVar _ -> ()
     | Ast.Ascription _ -> assert false
   and aux_magic = function
@@ -308,13 +327,21 @@ let dressn ~sep:sauces =
 let find_appl_pattern_uris ap =
   let rec aux acc =
     function
-    | Ast.UriPattern uri -> uri :: acc
+    | Ast.UriPattern uri -> `Uri uri :: acc
+    | Ast.NRefPattern nref -> `NRef nref :: acc
     | Ast.ImplicitPattern
     | Ast.VarPattern _ -> acc
     | Ast.ApplPattern apl -> List.fold_left aux acc apl
   in
   let uris = aux [] ap in
-  HExtlib.list_uniq (List.fast_sort UriManager.compare uris)
+  let cmp u1 u2 =
+   match u1,u2 with
+      `Uri u1, `Uri u2 -> UriManager.compare u1 u2
+    | `NRef r1, `NRef r2 -> NReference.compare r1 r2
+    | `Uri _,`NRef _ -> -1
+    | `NRef _, `Uri _ -> 1
+  in
+  HExtlib.list_uniq (List.fast_sort cmp uris)
 
 let rec find_branch =
   function
@@ -344,7 +371,8 @@ 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 ())
+  (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
+let fresh_name () = "eta" ^ string_of_int (fresh_id ())
 
 let rec freshen_term ?(index = ref 0) term =
   let freshen_term = freshen_term ~index in
@@ -366,7 +394,10 @@ let freshen_obj obj =
   let index = ref 0 in
   let freshen_term = freshen_term ~index in
   let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in
-  let freshen_name_ty_b = List.map (fun (n, t, b) -> (n, freshen_term t, b)) in
+  let freshen_name_ty_b = List.map (fun (n,t,b,i) -> (n,freshen_term t,b,i)) in
+  let freshen_capture_variables =
+   List.map (fun (n,t) -> (freshen_term n, HExtlib.map_option freshen_term t))
+  in
   match obj with
   | CicNotationPt.Inductive (params, indtypes) ->
       let indtypes =
@@ -374,15 +405,15 @@ let freshen_obj obj =
           (fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors))
           indtypes
       in
-      CicNotationPt.Inductive (freshen_name_ty params, indtypes)
+      CicNotationPt.Inductive (freshen_capture_variables params, indtypes)
   | CicNotationPt.Theorem (flav, n, t, ty_opt) ->
       let ty_opt =
         match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
       in
       CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
   | CicNotationPt.Record (params, n, ty, fields) ->
-      CicNotationPt.Record (freshen_name_ty params, n, freshen_term ty,
-        freshen_name_ty_b fields)
+      CicNotationPt.Record (freshen_capture_variables params, n,
+        freshen_term ty, freshen_name_ty_b fields)
 
 let freshen_term = freshen_term ?index:None