- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)

[helm.git] / matita / components / content / notationUtil.ml

diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml
index a2ab34833cd098ea72335c56d9242c2ec60498cf..82096f80b7e89f3d3f1bfea46e2ddec7034f5788 100644 (file)
--- a/matita/components/content/notationUtil.ml
+++ b/matita/components/content/notationUtil.ml
@@ -43,15 +43,6 @@ let visit_ast ?(special_k = fun _ -> assert false)
     | 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)
-    | Ast.LetRec (kind, definitions, term) ->
-        let definitions =
-          List.map
-            (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)
     | Ast.Ident (name, Some substs) ->
         Ast.Ident (name, Some (aux_substs substs))
     | Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs substs))
@@ -202,9 +193,6 @@ let meta_names_of_term term =
     | Ast.LetIn (_, t1, t3) ->
         aux t1 ;
         aux t3
-    | Ast.LetRec (_, definitions, body) ->
-        List.iter aux_definition definitions ;
-        aux body
     | Ast.Uri (_, Some substs) -> aux_substs substs
     | Ast.Ident (_, Some substs) -> aux_substs substs
     | Ast.Meta (_, substs) -> aux_meta_substs substs
@@ -232,10 +220,6 @@ let meta_names_of_term term =
    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
   and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
   and aux_variable = function
@@ -351,7 +335,7 @@ let fresh_id () =
   !fresh_index
 
   (* TODO ensure that names generated by fresh_var do not clash with user's *)
-  (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
+  (* FG: "η" is not an identifier (it is rendered, but not parsed) *)
 let fresh_name () = "eta" ^ string_of_int (fresh_id ())
 
 let rec freshen_term ?(index = ref 0) term =
@@ -375,26 +359,49 @@ let freshen_obj obj =
   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,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
+  let freshen_capture_variable (n, t) = freshen_term n, HExtlib.map_option freshen_term t in 
+  let freshen_capture_variables = List.map freshen_capture_variable in
   match obj with
-  | NotationPt.Inductive (params, indtypes) ->
+  | NotationPt.Inductive (params, indtypes, attrs) ->
       let indtypes =
         List.map
           (fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors))
           indtypes
       in
-      NotationPt.Inductive (freshen_capture_variables params, indtypes)
-  | NotationPt.Theorem (flav, n, t, ty_opt,p) ->
+      NotationPt.Inductive (freshen_capture_variables params, indtypes, attrs)
+  | NotationPt.Theorem (n, t, ty_opt, attrs) ->
       let ty_opt =
         match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
       in
-      NotationPt.Theorem (flav, n, freshen_term t, ty_opt,p)
-  | NotationPt.Record (params, n, ty, fields) ->
+      NotationPt.Theorem (n, freshen_term t, ty_opt, attrs)
+  | NotationPt.Record (params, n, ty, fields, attrs) ->
       NotationPt.Record (freshen_capture_variables params, n,
-        freshen_term ty, freshen_name_ty_b fields)
+        freshen_term ty, freshen_name_ty_b fields, attrs)
+  | NotationPt.LetRec (kind, definitions, attrs) ->
+      let definitions =
+        List.map
+          (fun (params, var, ty, decrno) ->
+            freshen_capture_variables params, freshen_capture_variable var,
+            freshen_term ty, decrno)
+          definitions
+      in
+      NotationPt.LetRec (kind, definitions, attrs)
 
 let freshen_term = freshen_term ?index:None
 
-let refresh_uri_in_term t = assert false
+let rec refresh_uri_in_term ~refresh_uri_in_term:refresh_in_cic
+ ~refresh_uri_in_reference
+=
+ function
+    NotationPt.NRef ref -> NotationPt.NRef (refresh_uri_in_reference ref)
+  | NotationPt.NCic t -> NotationPt.NCic (refresh_in_cic t)
+  | t ->
+     visit_ast
+     (refresh_uri_in_term ~refresh_uri_in_term:refresh_in_cic
+       ~refresh_uri_in_reference) t
+      ~special_k:(fun x -> x)
+      ~map_xref_option:(function Some ref -> Some (refresh_uri_in_reference ref)
+                         | x -> x)
+      ~map_case_indty:(function (Some (s,Some ref)) -> Some (s, Some
+                        (refresh_uri_in_reference ref)) | x -> x)
+;;