X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=84f4a2f7272bd5636f5fb0663ec071ea128cfad4;hb=e3369ffc8b690703cfafc7985f69db5fc140d749;hp=6b0d9d0c8595c4ade106306369efb9acc20e9389;hpb=f3f6b451707a3feb8245717e3fa7ca25df0ce8ef;p=helm.git

diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml
index 6b0d9d0c8..84f4a2f72 100644
--- a/matita/components/content_pres/termContentPres.ml
+++ b/matita/components/content_pres/termContentPres.ml
@@ -44,7 +44,7 @@ let resolve_binder = function
 
 let add_level_info prec t = Ast.AttributedTerm (`Level prec, t)
 
-let rec top_pos t = add_level_info ~-1 t
+let top_pos t = add_level_info ~-1 t
 
 let rec remove_level_info =
   function
@@ -109,7 +109,7 @@ let map_space f l =
   ~sep:[space] (List.map (fun x -> [f x]) l)
 ;;
 
-let pp_ast0 t k =
+let pp_ast0 status t k =
   let rec aux =
     function
     | Ast.Appl ts ->
@@ -143,7 +143,7 @@ let pp_ast0 t k =
         in
         let match_box =
           hvbox false false [
-           hvbox false true [
+           hvbox false false [
             hvbox false true [keyword "match"; space; break; top_pos (k what)];
             break;
             hvbox false true indty_box;
@@ -210,10 +210,11 @@ let pp_ast0 t k =
               keyword "let"; space;
               hvbox false true [
                 aux_var var; space;
-                builtin_symbol "\\def"; break; top_pos (k s) ];
-              break; space; keyword "in"; space ];
+                builtin_symbol "\\def"; break; top_pos (k s); space; keyword "in"; space ];
+              ];
             break;
             k t ])
+(*
     | Ast.LetRec (rec_kind, funs, where) ->
         let rec_op =
           match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
@@ -261,6 +262,7 @@ let pp_ast0 t k =
           ((hvbox false false
             (fst_row :: List.flatten tl_rows
              @ [ break; keyword "in"; break; k where ])))
+*)
     | Ast.Implicit `JustOne -> builtin_symbol "?"
     | Ast.Implicit `Vector -> builtin_symbol "…"
     | Ast.Meta (n, l) ->
@@ -289,7 +291,7 @@ let pp_ast0 t k =
   and special_k = function
     | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t)
     | t ->
-        prerr_endline ("unexpected special: " ^ NotationPp.pp_term t);
+        prerr_endline ("unexpected special: " ^ NotationPp.pp_term status t);
         assert false
   in
   aux t
@@ -300,14 +302,14 @@ module IntMap = Map.Make(struct type t = int let compare = compare end);;
 
 type db = {
  level1_patterns21: NotationPt.term IntMap.t;
- compiled21: ((NotationPt.term -> (NotationEnv.t * NotationPt.term list * int) option)) Lazy.t option;
+ compiled21: ((NotationPt.term -> (NotationEnv.t * NotationPt.term list * int) option)) Lazy.t;
  pattern21_matrix: (NotationPt.term * pattern_id) list;
  counter: pattern_id
 }
 
 let initial_db = {
  level1_patterns21 = IntMap.empty;
- compiled21 = None;
+ compiled21 = lazy (Content2presMatcher.Matcher21.compiler []);
  pattern21_matrix = [];
  counter = ~-1 
 }
@@ -317,8 +319,9 @@ class type g_status =
     method content_pres_db: db
   end
  
-class status =
+class virtual status =
  object
+   inherit NCic.status
    val content_pres_db = initial_db  
    method content_pres_db = content_pres_db
    method set_content_pres_db v = {< content_pres_db = v >}
@@ -328,13 +331,11 @@ class status =
  end
 
 let get_compiled21 status =
-  match status#content_pres_db.compiled21 with
-  | None -> assert false
-  | Some f -> Lazy.force f
+  Lazy.force status#content_pres_db.compiled21
 
 let set_compiled21 status f =
  status#set_content_pres_db
-  { status#content_pres_db with compiled21 = Some f }
+  { status#content_pres_db with compiled21 = f }
 
 let add_idrefs =
   List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
@@ -346,7 +347,7 @@ let instantiate21 idrefs env l1 =
         Ast.AttributedTerm (attr, subst_singleton pos env t)
     | t -> NotationUtil.group (subst pos env t)
   and subst pos env = function
-    | Ast.AttributedTerm (attr, t) ->
+    | Ast.AttributedTerm (_attr, t) ->
 (*         prerr_endline ("loosing attribute " ^ NotationPp.pp_attribute attr); *)
         subst pos env t
     | Ast.Variable var ->
@@ -377,7 +378,7 @@ let instantiate21 idrefs env l1 =
     | Ast.Literal l as t ->
         let t = add_idrefs idrefs t in
         (match l with
-        | `Keyword k -> [ add_keyword_attrs t ]
+        | `Keyword _k -> [ add_keyword_attrs t ]
         | _ -> [ t ])
     | Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ]
     | t -> [ NotationUtil.visit_ast (subst_singleton pos env) t ]
@@ -459,7 +460,7 @@ let rec pp_ast1 status term =
   let rec pp_value = function
     | NotationEnv.NumValue _ as v -> v
     | NotationEnv.StringValue _ as v -> v
-(*     | NotationEnv.TermValue t when t == term -> NotationEnv.TermValue (pp_ast0 t pp_ast1) *)
+(*     | NotationEnv.TermValue t when t == term -> NotationEnv.TermValue (pp_ast0 status t pp_ast1) *)
     | NotationEnv.TermValue t -> NotationEnv.TermValue (pp_ast1 status t)
     | NotationEnv.OptValue None as v -> v
     | NotationEnv.OptValue (Some v) -> 
@@ -476,7 +477,7 @@ let rec pp_ast1 status term =
       Ast.AttributedTerm (attrs, pp_ast1 status term')
   | _ ->
       (match get_compiled21 status term with
-      | None -> pp_ast0 term (pp_ast1 status)
+      | None -> pp_ast0 status term (pp_ast1 status)
       | Some (env, ctors, pid) ->
           let idrefs =
             List.flatten (List.map NotationUtil.get_idrefs ctors)
@@ -494,7 +495,7 @@ let load_patterns21 status t =
 let pp_ast status ast =
   debug_print (lazy "pp_ast <-");
   let ast' = pp_ast1 status ast in
-  debug_print (lazy ("pp_ast -> " ^ NotationPp.pp_term ast'));
+  debug_print (lazy ("pp_ast -> " ^ NotationPp.pp_term status ast'));
   ast'
 
 let fill_pos_info l1_pattern = l1_pattern
@@ -573,7 +574,7 @@ let tail_names names env =
   in
   aux [] env
 
-let instantiate_level2 env term =
+let instantiate_level2 status env term =
 (*   prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *)
   let fresh_env = ref [] in
   let lookup_fresh_name n =
@@ -585,9 +586,8 @@ let instantiate_level2 env term =
       new_name
   in
   let rec aux env term =
-(*    prerr_endline ("ENV " ^ NotationPp.pp_env env); *)
     match term with
-    | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term
+    | Ast.AttributedTerm (_a, term) -> (*Ast.AttributedTerm (a, *)aux env term
     | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
     | Ast.Binder (binder, var, body) ->
         Ast.Binder (binder, aux_capture_var env var, aux env body)
@@ -596,9 +596,11 @@ let instantiate_level2 env term =
           List.map (aux_branch env) patterns)
     | Ast.LetIn (var, t1, t3) ->
         Ast.LetIn (aux_capture_var env var, aux env t1, aux env t3)
+(*    
     | Ast.LetRec (kind, definitions, body) ->
         Ast.LetRec (kind, List.map (aux_definition env) definitions,
           aux env body)
+*)    
     | Ast.Uri (name, None) -> Ast.Uri (name, None)
     | Ast.Uri (name, Some substs) ->
         Ast.Uri (name, Some (aux_substs env substs))
@@ -630,18 +632,21 @@ let instantiate_level2 env term =
       Ast.Pattern (head, hrefs, vars) ->
        Ast.Pattern (head, hrefs, List.map (aux_capture_var env) vars)
     | Ast.Wildcard -> Ast.Wildcard
-  and aux_definition env (params, var, term, i) =
-    (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i)
+  (*and aux_definition env (params, var, term, i) =
+    (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i)*)
   and aux_substs env substs =
     List.map (fun (name, term) -> (name, aux env term)) substs
   and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
   and aux_variable env = function
     | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
-    | Ast.IdentVar name -> Ast.Ident (Env.lookup_string env name, None)
+    | Ast.IdentVar name ->
+       (match Env.lookup_string env name with
+           Env.Ident x -> Ast.Ident (x, None)
+         | Env.Var x -> Ast.Variable (Ast.IdentVar x))
     | Ast.TermVar (name,(Ast.Level l|Ast.Self l)) -> 
         Ast.AttributedTerm (`Level l,Env.lookup_term env name)
     | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
-    | Ast.Ascription (term, name) -> assert false
+    | Ast.Ascription (_term, _name) -> assert false
   and aux_magic env = function
     | Ast.Default (some_pattern, none_pattern) ->
         let some_pattern_names = NotationUtil.names_of_term some_pattern in
@@ -664,7 +669,7 @@ let instantiate_level2 env term =
             | _ ->
                 prerr_endline (sprintf
                   "lookup of %s in env %s did not return an optional value"
-                  name (NotationPp.pp_env env));
+                  name (NotationPp.pp_env status env));
                 assert false))
     | Ast.Fold (`Left, base_pattern, names, rec_pattern) ->
         let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
@@ -709,7 +714,7 @@ let instantiate_level2 env term =
               | _ -> assert false
             in
             instantiate_fold_right env)
-    | Ast.If (_, p_true, p_false) as t ->
+    | Ast.If (_, _p_true, _p_false) as t ->
         aux env (NotationUtil.find_branch (Ast.Magic t))
     | Ast.Fail -> assert false
     | _ -> assert false