]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationRew.ml
snapshot
[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml
index 79316319a7a7c42385d2f7dc4951f9ddde7d1e14..207b26a233d139773815234a62843838e115020d 100644 (file)
@@ -29,6 +29,9 @@ type pattern_id = int
 type interpretation_id = pattern_id
 type pretty_printer_id = pattern_id
 
+let default_prec = 50
+let default_assoc = Gramext.NonA
+
 type term_info =
   { sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t;
     uri: (Cic.id, string) Hashtbl.t;
@@ -62,6 +65,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,17 +75,49 @@ 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 reset_href t = Ast.AttributedTerm (`Href [], t) in
+  let builtin_symbol s = reset_href (Ast.Literal (`Symbol s)) in
+  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), [
+              builtin_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), [
+              builtin_symbol (resolve_binder binder_kind);
+              k id;
+              builtin_symbol ":";
+              aux_ty ty ]));
+            Ast.Layout (Ast.Box ((Ast.H, false, false), [
+              builtin_symbol ".";
+              k body ]))])))
+    | t -> CicNotationUtil.visit_ast ~special_k k t
+  and aux_ty = function
+    | None -> builtin_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
 
 let ast_of_acic0 term_info acic k =
-(*   prerr_endline "ast_of_acic0"; *)
   let k = k term_info in
   let register_uri id uri = Hashtbl.add term_info.uri id uri in
   let sort_of_id id =
@@ -221,10 +257,11 @@ let get_compiled32 () =
 let set_compiled21 f = compiled21 := Some f
 let set_compiled32 f = compiled32 := Some f
 
-let instantiate21 env precedence associativity l1 =
-  prerr_endline "instantiate21";
-  let rec subst last_box env = function
-    | Ast.AttributedTerm (_, t) -> subst last_box env t
+let instantiate21 env (* precedence associativity *) l1 =
+  let rec subst_singleton env t =
+    CicNotationUtil.boxify (subst env t)
+  and subst env = function
+    | Ast.AttributedTerm (_, t) -> subst env t
     | Ast.Variable var ->
         let name, expected_ty = CicNotationEnv.declaration_of_var var in
         let ty, value =
@@ -236,12 +273,12 @@ let instantiate21 env precedence associativity l1 =
         (* following assertion should be a conditional that makes this
          * instantiation fail *)
         assert (CicNotationEnv.well_typed expected_ty value);
-        CicNotationEnv.term_of_value value
-    | Ast.Magic m -> subst_magic last_box env m
-    | Ast.Literal _ as t -> t
-    | Ast.Layout l -> Ast.Layout (subst_layout last_box env l)
-    | t -> CicNotationUtil.visit_ast (subst last_box env) t
-  and subst_magic last_box env = function
+        [ CicNotationEnv.term_of_value value ]
+    | Ast.Magic m -> subst_magic env m
+    | Ast.Literal _ as t -> [ t ]
+    | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ]
+    | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ]
+  and subst_magic env = function
     | Ast.List0 (p, sep_opt)
     | Ast.List1 (p, sep_opt) ->
         let rec_decls = CicNotationEnv.declarations_of_term p in
@@ -256,12 +293,16 @@ let instantiate21 env precedence associativity l1 =
         in
         let rec instantiate_list acc = function
           | [] -> List.rev acc
+         | value_set :: [] ->
+             let env = CicNotationEnv.combine rec_decls value_set in
+               instantiate_list
+                  ((CicNotationUtil.boxify (subst env p)) :: acc) []
           | value_set :: tl ->
               let env = CicNotationEnv.combine rec_decls value_set in
-              instantiate_list ([subst last_box env p] @ sep @ acc) tl
+              instantiate_list
+                ((CicNotationUtil.boxify (subst env p @ sep)) :: acc) tl
         in
-        let children = instantiate_list [] values in
-        CicNotationPt.Layout (CicNotationPt.Box (last_box, children))
+        instantiate_list [] values
     | Ast.Opt p ->
         let opt_decls = CicNotationEnv.declarations_of_term p in
         let env =
@@ -275,23 +316,24 @@ let instantiate21 env precedence associativity l1 =
           in
           try build_env opt_decls with Exit -> []
         in
-        let children =
-          if env = [] then []
-          else [subst last_box env p]
-        in
-        CicNotationPt.Layout (CicNotationPt.Box (last_box, children))
+         begin
+           match env with
+             | [] -> []
+             | _ -> subst env p
+         end
     | _ -> assert false (* impossible *)
-  and subst_layout last_box env l =
-    CicNotationUtil.visit_layout (subst last_box env) l
-    (* TODO ZACK here we need to remember the last box traversed, but
-     * visit_layout is opaque :-((( *)
+  and subst_layout env = function
+    | Ast.Box (kind, tl) ->
+        Ast.Box (kind, List.concat (List.map (subst env) tl))
+    | l -> CicNotationUtil.visit_layout (subst_singleton env) l
   in
-  subst CicNotationPt.H env l1
+    subst_singleton env l1
 
 let rec pp_ast1 term = 
   let rec pp_value = function
     | CicNotationEnv.NumValue _ as v -> v
     | CicNotationEnv.StringValue _ as v -> v
+(*     | CicNotationEnv.TermValue t when t == term -> CicNotationEnv.TermValue (pp_ast0 t pp_ast1) *)
     | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t)
     | CicNotationEnv.OptValue None as v -> v
     | CicNotationEnv.OptValue (Some v) -> 
@@ -302,15 +344,21 @@ let rec pp_ast1 term =
   let ast_env_of_env env =
     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
   in
-  match (get_compiled21 ()) term with
-  | None -> pp_ast0 term pp_ast1
-  | Some (env, pid) ->
-      let precedence, associativity, l1 =
-        try
-          Hashtbl.find level1_patterns21 pid
-        with Not_found -> assert false
-      in
-      instantiate21 (ast_env_of_env env) precedence associativity l1
+  match term with
+  | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t)
+  | _ ->
+      begin
+       match (get_compiled21 ()) term with
+         | None -> pp_ast0 term pp_ast1
+         | Some (env, pid) ->
+              let precedence, associativity, l1 =
+               try
+                 Hashtbl.find level1_patterns21 pid
+               with Not_found -> assert false
+              in
+               Ast.AttributedTerm (`Level (precedence, associativity),
+                               (instantiate21 (ast_env_of_env env) l1))
+      end
 
 let instantiate32 term_info env symbol args =
   let rec instantiate_arg = function
@@ -340,12 +388,15 @@ let rec ast_of_acic1 term_info annterm =
       let env' =
         List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env
       in
-      let symbol, args =
+      let symbol, args, uris =
         try
           Hashtbl.find level2_patterns32 pid
         with Not_found -> assert false
       in
-      instantiate32 term_info env' symbol args
+      let ast = instantiate32 term_info env' symbol args in
+      match uris with
+      | [] -> ast
+      | _ -> Ast.AttributedTerm (`Href uris, ast)
 
 let load_patterns32 t =
   set_compiled32 (CicNotationMatcher.Matcher32.compiler t)
@@ -368,12 +419,15 @@ let fresh_id =
 
 let add_interpretation (symbol, args) appl_pattern =
   let id = fresh_id () in
-  Hashtbl.add level2_patterns32 id (symbol, args);
+  let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in
+  Hashtbl.add level2_patterns32 id (symbol, args, uris);
   pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix;
   load_patterns32 !pattern32_matrix;
   id
 
-let add_pretty_printer ?precedence ?associativity l2 l1 =
+let add_pretty_printer
+  ?(precedence = default_prec) ?(associativity = default_assoc) l2 l1
+=
   let id = fresh_id () in
   let l2' = CicNotationUtil.strip_attributes l2 in
   Hashtbl.add level1_patterns21 id (precedence, associativity, l1);