X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=49d9241b96e8290ebef312443be7fa20811de9e3;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=b9abb44183389782a7e463eaeacf0801751010f5;hpb=fb6fee82bb9172e15b1a7bc7e20641627f593fcc;p=helm.git diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml index b9abb4418..49d9241b9 100644 --- a/matita/components/content_pres/termContentPres.ml +++ b/matita/components/content_pres/termContentPres.ml @@ -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)) @@ -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,9 +574,8 @@ 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); *) -prerr_endline ("istanzio: " ^ NotationPp.pp_term term); let fresh_env = ref [] in let lookup_fresh_name n = try @@ -585,9 +585,7 @@ prerr_endline ("istanzio: " ^ NotationPp.pp_term term); fresh_env := (n, new_name) :: !fresh_env; new_name in -prerr_endline ("ENV " ^ NotationPp.pp_env env); let rec aux env term = -prerr_endline ("istanzio_deep: " ^ NotationPp.pp_term term); match term with | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms) @@ -598,9 +596,11 @@ prerr_endline ("istanzio_deep: " ^ NotationPp.pp_term 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)) @@ -669,7 +669,7 @@ prerr_endline ("istanzio_deep: " ^ NotationPp.pp_term 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 *)