version 0.7.1

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

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 529353daa3e492e0d7ff12c3bc55795c368731d9..2f95a56350f5af1b5fa492c36d2310fa18debb18 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -62,6 +62,7 @@ let constructor_of_inductive_type uri i j =
   with Not_found -> assert false)
 
 module Ast = CicNotationPt
+module Parser = CicNotationParser
 
 let string_of_name = function
   | Cic.Name s -> s
@@ -71,11 +72,41 @@ let ident_of_name n = Ast.Ident (string_of_name n, None)
 
 let idref id t = Ast.AttributedTerm (`IdRef id, t)
 
+let resolve_binder = function
+  | `Lambda -> "\\lambda"
+  | `Pi -> "\\Pi"
+  | `Forall -> "\\forall"
+  | `Exists -> "\\exists"
+
 let pp_ast0 t k =
-  prerr_endline "pp_ast0";
-  let rec aux t = CicNotationUtil.visit_ast ~special_k k t
+  let rec aux = function
+    | Ast.Appl ts ->
+        Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc),
+          Ast.Layout (Ast.Box ((Ast.HOV, true, true), List.map k ts)))
+    | Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body)
+    | Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) ->
+        Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
+          Ast.Layout (Ast.Box ((Ast.HV, false, true), [
+            aux_ty ty;
+            Ast.Layout (Ast.Box ((Ast.H, false, false), [
+              Ast.Literal (`Symbol "\\to"); k body]))])))
+    | Ast.Binder (binder_kind, (id, ty), body) ->
+        Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
+          Ast.Layout (Ast.Box ((Ast.HV, false, true), [
+            Ast.Layout (Ast.Box ((Ast.H, false, false), [
+              Ast.Literal (`Symbol (resolve_binder binder_kind));
+              k id;
+              Ast.Literal (`Symbol ":");
+              aux_ty ty ]));
+            Ast.Layout (Ast.Box ((Ast.H, false, false), [
+              Ast.Literal (`Symbol ".");
+              k body ]))])))
+    | t -> CicNotationUtil.visit_ast ~special_k k t
+  and aux_ty = function
+    | None -> Ast.Literal (`Symbol "?")
+    | Some ty -> k ty
   and special_k = function
-    | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, aux t)
+    | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t)
     | _ -> assert false
   in
   aux t
@@ -222,13 +253,8 @@ let set_compiled21 f = compiled21 := Some f
 let set_compiled32 f = compiled32 := Some f
 
 let instantiate21 env precedence associativity l1 =
-  prerr_endline "instantiate21";
-  let boxify = function
-    | [t] -> t
-    | tl -> Ast.Layout (Ast.Box (Ast.H, tl))
-  in
   let rec subst_singleton env t =
-    boxify (subst env t)
+    CicNotationUtil.boxify (subst env t)
   and subst env = function
     | Ast.AttributedTerm (_, t) -> subst env t
     | Ast.Variable var ->
@@ -264,12 +290,14 @@ let instantiate21 env precedence associativity l1 =
           | [] -> List.rev acc
          | value_set :: [] ->
              let env = CicNotationEnv.combine rec_decls value_set in
-               instantiate_list ((boxify (subst env p)) :: acc) []
+               instantiate_list
+                  ((CicNotationUtil.boxify (subst env p)) :: acc) []
           | value_set :: tl ->
               let env = CicNotationEnv.combine rec_decls value_set in
-              instantiate_list ((boxify (subst env p @ sep)) :: acc) tl
+              instantiate_list
+                ((CicNotationUtil.boxify (subst env p @ sep)) :: acc) tl
         in
-        instantiate_list [] (List.rev values)
+        instantiate_list [] values
     | Ast.Opt p ->
         let opt_decls = CicNotationEnv.declarations_of_term p in
         let env =