* fold left/right implemented

diff --git a/helm/ocaml/cic_notation/cicNotationEnv.ml b/helm/ocaml/cic_notation/cicNotationEnv.ml
index 8d3149b98f615dd5157eafb6bd173d96cba1d885..79dfaf8be4b8dfd59da2332430add45e146f88ca 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationEnv.ml
+++ b/helm/ocaml/cic_notation/cicNotationEnv.ml
@@ -72,6 +72,31 @@ let unopt_names names env =
         | OptType ty, OptValue (Some v) -> aux ((name, (ty, v)) :: acc) tl
         | _ -> assert false)
     | _ :: tl -> aux acc tl
+      (* some pattern may contain only meta names, thus we trash all others *)
+    | [] -> acc
+  in
+  aux [] env
+
+let head_names names env =
+  let rec aux acc = function
+    | (name, (ty, v)) :: tl when List.mem name names ->
+        (match ty, v with
+        | ListType ty, ListValue (v :: _) -> aux ((name, (ty, v)) :: acc) tl
+        | _ -> assert false)
+    | _ :: tl -> aux acc tl
+      (* base pattern may contain only meta names, thus we trash all others *)
+    | [] -> acc
+  in
+  aux [] env
+
+let tail_names names env =
+  let rec aux acc = function
+    | (name, (ty, v)) :: tl when List.mem name names ->
+        (match ty, v with
+        | ListType ty, ListValue (_ :: vtl) ->
+            aux ((name, (ListType ty, ListValue vtl)) :: acc) tl
+        | _ -> assert false)
+    | binding :: tl -> aux (binding :: acc) tl
     | [] -> acc
   in
   aux [] env
@@ -147,17 +172,18 @@ let meta_names_of term =
     | FreshVar _ -> ()
     | Ascription _ -> assert false
   and aux_magic = function
+    | Default (t1, t2)
     | Fold (_, t1, _, t2) ->
         aux t1 ;
         aux t2
-    | Default (t1, t2) ->
-        aux t1 ;
-        aux t2
     | _ -> assert false
   in
   aux term ;
   !names
 
+let pp_term = ref (fun (t:CicNotationPt.term)  -> assert false; "")
+let set_pp_term f = pp_term := f
+
 let instantiate ~env term =
   let fresh_env = ref [] in
   let lookup_fresh_name n =
@@ -229,7 +255,45 @@ let instantiate ~env term =
                 aux (unopt_names names env) some_pattern
             | OptValue None -> aux env none_pattern
             | _ -> assert false))
-    | Fold _ -> failwith "not yet implemented"      (* TODO Fold *)
+    | Fold (`Left, base_pattern, names, rec_pattern) ->
+        let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
+        let meta_names =
+          List.filter ((<>) acc_name) (meta_names_of rec_pattern)
+        in
+        (match meta_names with
+        | [] -> assert false (* as above *)
+        | (name :: _) as names ->
+            let rec instantiate_fold_left acc env' =
+              prerr_endline "instantiate_fold_left";
+              match lookup_value ~env:env' name with
+              | ListValue (_ :: _) ->
+                  instantiate_fold_left 
+                    (let acc_binding = acc_name, (TermType, TermValue acc) in
+                     aux (acc_binding :: head_names names env') rec_pattern)
+                    (tail_names names env')
+              | ListValue [] -> acc
+              | _ -> assert false
+            in
+            instantiate_fold_left (aux env base_pattern) env)
+    | Fold (`Right, base_pattern, names, rec_pattern) ->
+        let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
+        let meta_names =
+          List.filter ((<>) acc_name) (meta_names_of rec_pattern)
+        in
+        (match meta_names with
+        | [] -> assert false (* as above *)
+        | (name :: _) as names ->
+            let rec instantiate_fold_right env' =
+              prerr_endline "instantiate_fold_right";
+              match lookup_value ~env:env' name with
+              | ListValue (_ :: _) ->
+                  let acc = instantiate_fold_right (tail_names names env') in
+                  let acc_binding = acc_name, (TermType, TermValue acc) in
+                  aux (acc_binding :: head_names names env') rec_pattern
+              | ListValue [] -> aux env base_pattern
+              | _ -> assert false
+            in
+            instantiate_fold_right env)
     | _ -> assert false
   in
   aux env term

diff --git a/helm/ocaml/cic_notation/cicNotationEnv.mli b/helm/ocaml/cic_notation/cicNotationEnv.mli
index 4ba9f2487ec511bc7e2ae03b0eafe68cec3e5174..a5267b04463b8493bcdf28c72989551611feb182 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationEnv.mli
+++ b/helm/ocaml/cic_notation/cicNotationEnv.mli
@@ -57,3 +57,7 @@ val list_binding_of_name: declaration -> binding  (* [] binding *)
 val opt_declaration:  declaration -> declaration  (* t -> OptType t *)
 val list_declaration: declaration -> declaration  (* t -> ListType t *)
 
+(** {2 Debugging} *)
+
+val set_pp_term: (CicNotationPt.term -> string) -> unit
+

diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml
index e4db4d503d986bd842008d5f32970fb58993d35c..bcb7e661b7e37936b993c9c0f40ddc7785171d5d 100644 (file)
--- a/helm/ocaml/cic_notation/test_parser.ml
+++ b/helm/ocaml/cic_notation/test_parser.ml
@@ -26,6 +26,7 @@
 open Printf
 
 let _ =
+  CicNotationEnv.set_pp_term CicNotationPp.pp_term;
   let module P = CicNotationPt in
   let level = ref ~-1 in
   let arg_spec = [ "-level", Arg.Set_int level, "set the notation level" ] in
@@ -85,8 +86,8 @@ let _ =
                     (fun env loc ->
                       prerr_endline "ENV";
                       prerr_endline (CicNotationPp.pp_env env);
-                      CicNotationEnv.instantiate env l2));
-                CicNotationParser.print_l2_pattern ())
+                      CicNotationEnv.instantiate env l2)))
+(*                 CicNotationParser.print_l2_pattern ()) *)
         | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream)
         | 2 ->
             let ast = CicNotationParser.parse_ast_pattern istream in