X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=b7322afd4964d1a5dd3c1667a7ab66eb38cbc466;hb=e5014674aed0dab6f3aa43773c8caeffcfe0ac32;hp=2e2d8c9d45f3699180658824d40b00939c5bb66a;hpb=bf6144a808a16d4e576e56593bbcd63b8db5fe4c;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 2e2d8c9d4..b7322afd4 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -29,13 +29,13 @@ type pattern_id = int
 type interpretation_id = pattern_id
 type pretty_printer_id = pattern_id
 
+module Ast = CicNotationPt
+
 type term_info =
-  { sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t;
+  { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
     uri: (Cic.id, string) Hashtbl.t;
   }
 
-let warning s = prerr_endline ("CicNotation WARNING: " ^ s)
-
 let get_types uri =
   let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
     match o with
@@ -61,27 +61,62 @@ let constructor_of_inductive_type uri i j =
     fst (List.nth (constructors_of_inductive_type uri i) (j-1))
   with Not_found -> assert false)
 
-module Ast = CicNotationPt
-
-let string_of_name = function
-  | Cic.Name s -> s
-  | Cic.Anonymous -> "_"
+let idref id t = Ast.AttributedTerm (`IdRef id, t)
 
-let ident_of_name n = Ast.Ident (string_of_name n, None)
+let resolve_binder = function
+  | `Lambda -> "\\lambda"
+  | `Pi -> "\\Pi"
+  | `Forall -> "\\forall"
+  | `Exists -> "\\exists"
 
-let idref id t = Ast.AttributedTerm (`IdRef id, t)
+let binder_attributes = [None, "mathcolor", "blue"]
+let atop_attributes = [None, "linethickness", "0pt"]
+let indent_attributes = [None, "indent", "1em"]
+let keyword_attributes = [None, "mathcolor", "blue"]
 
 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 binder_symbol s =
+    Ast.AttributedTerm (`XmlAttrs binder_attributes, builtin_symbol s)
+  in
+  let rec aux = function
+    | Ast.Appl ts ->
+        Ast.AttributedTerm (`Level (Ast.apply_prec, Ast.apply_assoc),
+          Ast.Layout
+	    (Ast.Box ((Ast.HOV, true, true),
+		      (CicNotationUtil.dress
+			 (Ast.Layout Ast.Break)
+			 (List.map k ts)))))
+    | Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body)
+    | Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) ->
+        Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc),
+          Ast.Layout (Ast.Box ((Ast.HV, false, true), [
+            aux_ty ty;
+	    Ast.Layout Ast.Break;			 
+            binder_symbol "\\to";
+            k body])))
+    | Ast.Binder (binder_kind, (id, ty), body) ->
+        Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc),
+          Ast.Layout (Ast.Box ((Ast.HV, false, true), [
+            binder_symbol (resolve_binder binder_kind);
+            k id;
+            builtin_symbol ":";
+            aux_ty ty;
+            Ast.Layout Ast.Break;
+            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 =
@@ -119,13 +154,15 @@ let ast_of_acic0 term_info acic k =
           | `Set | `Type -> `Pi
           | `Prop | `CProp -> `Forall
         in
-        idref id (Ast.Binder (binder_kind, (ident_of_name n, Some (k s)), k t))
-    | Cic.ACast (id,v,t) ->
-        idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); k v; k t])
+        idref id (Ast.Binder (binder_kind,
+          (CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
+    | Cic.ACast (id,v,t) -> idref id (Ast.Cast (k v, k t))
     | Cic.ALambda (id,n,s,t) ->
-        idref id (Ast.Binder (`Lambda, (ident_of_name n, Some (k s)), k t))
+        idref id (Ast.Binder (`Lambda,
+          (CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
     | Cic.ALetIn (id,n,s,t) ->
-        idref id (Ast.LetIn ((ident_of_name n, None), k s, k t))
+        idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None),
+          k s, k t))
     | Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args))
     | Cic.AConst (id,uri,substs) ->
         register_uri id (UriManager.string_of_uri uri);
@@ -151,7 +188,7 @@ let ast_of_acic0 term_info acic k =
           match (ty, pat) with
           | Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') ->
               let (cv, rhs) = eat_branch t t' in
-              (ident_of_name name, Some (k s)) :: cv, rhs
+              (CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs
           | _, _ -> [], k pat
         in
         let patterns =
@@ -198,13 +235,10 @@ let ast_of_acic0 term_info acic k =
 
 let level1_patterns21 = Hashtbl.create 211
 let level2_patterns32 = Hashtbl.create 211
+let interpretations = Hashtbl.create 211  (* symb -> id list ref *)
 
-let (compiled21: (CicNotationPt.term -> (CicNotationEnv.t * int) option)
-option ref) =
-  ref None
-let (compiled32: (Cic.annterm -> ((string * Cic.annterm) list * int) option)
-option ref) =
-  ref None
+let compiled21 = ref None
+let compiled32 = ref None
 
 let pattern21_matrix = ref []
 let pattern32_matrix = ref []
@@ -212,24 +246,20 @@ let pattern32_matrix = ref []
 let get_compiled21 () =
   match !compiled21 with
   | None -> assert false
-  | Some f -> f
+  | Some f -> Lazy.force f
 let get_compiled32 () =
   match !compiled32 with
   | None -> assert false
-  | Some f -> f
+  | Some f -> Lazy.force f
 
 let set_compiled21 f = compiled21 := Some f
 let set_compiled32 f = compiled32 := Some f
 
-let instantiate21 env pid =
-  prerr_endline "instantiate21";
-  let precedence, associativity, l1 =
-    try
-      Hashtbl.find level1_patterns21 pid
-    with Not_found -> assert false
-  in
-  let rec subst = function
-    | Ast.AttributedTerm (_, t) -> subst t
+let instantiate21 env (* precedence associativity *) l1 =
+  let rec subst_singleton env t =
+    CicNotationUtil.group (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 =
@@ -241,18 +271,67 @@ let instantiate21 env pid =
         (* 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 _ -> assert false (* TO BE IMPLEMENTED *)
-    | Ast.Literal _ as t -> t
-    | Ast.Layout l -> Ast.Layout (subst_layout l)
-    | t -> CicNotationUtil.visit_ast subst t
-  and subst_layout l = CicNotationUtil.visit_layout subst l in
-  subst l1
+        [ CicNotationEnv.term_of_value value ]
+    | Ast.Magic m -> subst_magic env m
+    | Ast.Literal (`Keyword k) as t ->
+        [ Ast.AttributedTerm (`XmlAttrs keyword_attributes, t) ]
+    | 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
+        let rec_values =
+          List.map (fun (n, _) -> CicNotationEnv.lookup_list env n) rec_decls
+        in
+        let values = CicNotationUtil.ncombine rec_values in
+        let sep =
+          match sep_opt with
+            | None -> []
+            | Some l -> [ Ast.Literal l ]
+	in
+        let rec instantiate_list acc = function
+          | [] -> List.rev acc
+	  | value_set :: [] ->
+	      let env = CicNotationEnv.combine rec_decls value_set in
+		instantiate_list (CicNotationUtil.group (subst env p) :: acc) []
+          | value_set :: tl ->
+              let env = CicNotationEnv.combine rec_decls value_set in
+		instantiate_list (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl
+        in
+        instantiate_list [] values
+    | Ast.Opt p ->
+        let opt_decls = CicNotationEnv.declarations_of_term p in
+        let env =
+          let rec build_env = function
+            | [] -> []
+            | (name, ty) :: tl ->
+                  (* assumption: if one of the value is None then all are *)
+                (match CicNotationEnv.lookup_opt env name with
+                | None -> raise Exit
+                | Some v -> (name, (ty, v)) :: build_env tl)
+          in
+          try build_env opt_decls with Exit -> []
+        in
+	  begin
+	    match env with
+	      | [] -> []
+	      | _ -> subst env p
+	  end
+    | _ -> assert false (* impossible *)
+  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_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) -> 
@@ -263,9 +342,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) -> instantiate21 (ast_env_of_env env) pid
+  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
@@ -295,18 +386,21 @@ 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)
+  set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t))
 
 let load_patterns21 t =
-  set_compiled21 (CicNotationMatcher.Matcher21.compiler t)
+  set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t))
 
 let ast_of_acic id_to_sort annterm =
   let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
@@ -321,14 +415,35 @@ let fresh_id =
     incr counter;
     !counter
 
-let add_interpretation (symbol, args) appl_pattern =
+let add_interpretation dsc (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 (dsc, symbol, args, appl_pattern, uris);
   pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix;
   load_patterns32 !pattern32_matrix;
+  (try
+    let ids = Hashtbl.find interpretations symbol in
+    ids := id :: !ids
+  with Not_found -> Hashtbl.add interpretations symbol (ref [id]));
   id
 
-let add_pretty_printer ?precedence ?associativity l2 l1 =
+exception Interpretation_not_found
+exception Pretty_printer_not_found
+
+let lookup_interpretations symbol =
+  try
+    List.map
+      (fun id ->
+        let (dsc, _, args, appl_pattern, _) =
+          try
+            Hashtbl.find level2_patterns32 id
+          with Not_found -> assert false 
+        in
+        dsc, args, appl_pattern)
+      !(Hashtbl.find interpretations symbol)
+  with Not_found -> raise Interpretation_not_found
+
+let add_pretty_printer ~precedence ~associativity l2 l1 =
   let id = fresh_id () in
   let l2' = CicNotationUtil.strip_attributes l2 in
   Hashtbl.add level1_patterns21 id (precedence, associativity, l1);
@@ -336,11 +451,11 @@ let add_pretty_printer ?precedence ?associativity l2 l1 =
   load_patterns21 !pattern21_matrix;
   id
 
-exception Interpretation_not_found
-exception Pretty_printer_not_found
-
 let remove_interpretation id =
   (try
+    let _, symbol, _, _, _ = Hashtbl.find level2_patterns32 id in
+    let ids = Hashtbl.find interpretations symbol in
+    ids := List.filter ((<>) id) !ids;
     Hashtbl.remove level2_patterns32 id;
   with Not_found -> raise Interpretation_not_found);
   pattern32_matrix := List.filter (fun (_, id') -> id <> id') !pattern32_matrix;