snapshot (first working implementation of parttern matching from level 2

[helm.git] / helm / ocaml / cic_notation / cicNotationUtil.ml

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index ff0b7fc73757abf0f1d9218e491ee789b203347f..271b0df2155dee1cab6b98b0d79178b06752b9b1 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationUtil.ml
+++ b/helm/ocaml/cic_notation/cicNotationUtil.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+open CicNotationPt
+
   (* TODO ensure that names generated by fresh_var do not clash with user's *)
 let fresh_name =
   let index = ref ~-1 in
@@ -30,3 +32,86 @@ let fresh_name =
     incr index;
     "fresh" ^ string_of_int !index
 
+let visit_ast ?(special_k = fun _ -> assert false) k =
+  let rec aux = function
+
+    | Appl terms -> Appl (List.map k terms)
+    | Binder (kind, var, body) ->
+        Binder (kind, aux_capture_variable var, k body) 
+    | Case (term, indtype, typ, patterns) ->
+        Case (k term, indtype, aux_opt typ, aux_patterns patterns)
+    | LetIn (var, t1, t2) -> LetIn (aux_capture_variable var, k t1, k t2)
+    | LetRec (kind, definitions, term) ->
+        let definitions =
+          List.map
+            (fun (var, ty, n) -> aux_capture_variable var, k ty, n)
+            definitions
+        in
+        LetRec (kind, definitions, k term)
+    | Ident (name, Some substs) -> Ident (name, Some (aux_substs substs))
+    | Uri (name, Some substs) -> Uri (name, Some (aux_substs substs))
+    | Meta (index, substs) -> Meta (index, List.map aux_opt substs)
+
+    | (AttributedTerm _
+      | Layout _
+      | Literal _
+      | Magic _
+      | Variable _) as t -> special_k t
+
+    | (Ident _
+      | Implicit
+      | Num _
+      | Sort _
+      | Symbol _
+      | Uri _
+      | UserInput) as t -> t
+
+  and aux_opt = function
+    | 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, vars), term) =
+    ((head, List.map aux_capture_variable vars), k term)
+
+  and aux_subst (name, term) = (name, k term)
+
+  and aux_substs substs = List.map aux_subst substs
+
+  in
+
+  aux
+
+let visit_layout k = function
+  | Sub (t1, t2) -> Sub (k t1, k t2)
+  | Sup (t1, t2) -> Sup (k t1, k t2)
+  | Below (t1, t2) -> Below (k t1, k t2)
+  | Above (t1, t2) -> Above (k t1, k t2)
+  | Over (t1, t2) -> Over (k t1, k t2)
+  | Atop (t1, t2) -> Atop (k t1, k t2)
+  | Frac (t1, t2) -> Frac (k t1, k t2)
+  | Sqrt t -> Sqrt (k t)
+  | Root (arg, index) -> Root (k arg, k index)
+  | Break -> Break
+  | Box (kind, terms) -> Box (kind, List.map k terms)
+
+let visit_magic k = function
+  | List0 (t, l) -> List0 (k t, l)
+  | List1 (t, l) -> List1 (k t, l )
+  | Opt t -> Opt (k t)
+  | Fold (kind, t1, names, t2) -> Fold (kind, k t1, names, k t2)
+  | Default (t1, t2) -> Default (k t1, k t2)
+
+let rec strip_attributes t =
+  prerr_endline "strip_attributes";
+  let special_k = function
+    | AttributedTerm (_, term) -> strip_attributes term
+    | Magic m -> Magic (visit_magic strip_attributes m)
+    | Variable _ as t -> t
+    | t -> assert false
+  in
+  visit_ast ~special_k strip_attributes t
+