X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_cic_content%2FnTermCicContent.ml;h=61ff07689a83f38d8fe388941983c3d1e908a16d;hb=aab0401db0bedd941da96a32acd600af3fbe42e7;hp=b8d474cc2e260d5e9779baaf0cf002521cd4611a;hpb=5553ac7623425bce6f34eed6e17d4f0f8163e9aa;p=helm.git diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/nTermCicContent.ml index b8d474cc2..61ff07689 100644 --- a/matita/components/ng_cic_content/nTermCicContent.ml +++ b/matita/components/ng_cic_content/nTermCicContent.ml @@ -27,7 +27,7 @@ open Printf -module Ast = CicNotationPt +module Ast = NotationPt let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () @@ -36,20 +36,11 @@ type id = string let hide_coercions = ref true;; -(* -type interpretation_id = int - -type term_info = - { sort: (Cic.id, Ast.sort_kind) Hashtbl.t; - uri: (Cic.id, UriManager.uri) Hashtbl.t; - } - -let get_types uri = - let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in - match o with - | Cic.InductiveDefinition (l,_,leftno,_) -> l, leftno - | _ -> assert false -*) +class status = + object + inherit NCicCoercion.status + inherit Interpretations.status + end let idref register_ref = let id = ref 0 in @@ -89,7 +80,7 @@ let destroy_nat = (* CODICE c&p da NCicPp *) let nast_of_cic0 status ~(idref: - ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term) + ?reference:NReference.reference -> NotationPt.term -> NotationPt.term) ~output_type ~metasenv ~subst k ~context = function | NCic.Rel n -> @@ -213,44 +204,7 @@ let nast_of_cic0 status idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns)) ;; - (* persistent state *) - -(* -let initial_level2_patterns32 () = Hashtbl.create 211 -let initial_interpretations () = Hashtbl.create 211 - -let level2_patterns32 = ref (initial_level2_patterns32 ()) -(* symb -> id list ref *) -let interpretations = ref (initial_interpretations ()) -*) let compiled32 = ref None -(* -let pattern32_matrix = ref [] -let counter = ref ~-1 - -let stack = ref [] - -let push () = - stack := (!counter,!level2_patterns32,!interpretations,!compiled32,!pattern32_matrix)::!stack; - counter := ~-1; - level2_patterns32 := initial_level2_patterns32 (); - interpretations := initial_interpretations (); - compiled32 := None; - pattern32_matrix := [] -;; - -let pop () = - match !stack with - [] -> assert false - | (ocounter,olevel2_patterns32,ointerpretations,ocompiled32,opattern32_matrix)::old -> - stack := old; - counter := ocounter; - level2_patterns32 := olevel2_patterns32; - interpretations := ointerpretations; - compiled32 := ocompiled32; - pattern32_matrix := opattern32_matrix -;; -*) let get_compiled32 () = match !compiled32 with @@ -277,7 +231,7 @@ let instantiate32 idrefs env symbol args = in let rec add_lambda t n = if n > 0 then - let name = CicNotationUtil.fresh_name () in + let name = NotationUtil.fresh_name () in Ast.Binder (`Lambda, (Ast.Ident (name, None), None), Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)]) else @@ -305,7 +259,7 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = idref ~reference: (match term with NCic.Const nref -> nref | _ -> assert false) - (CicNotationPt.Ident ("dummy",None)) + (NotationPt.Ident ("dummy",None)) in match attrterm with Ast.AttributedTerm (`IdRef id, _) -> id @@ -322,7 +276,7 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = in let _, symbol, args, _ = try - Interpretations.find_level2_patterns32 pid + Interpretations.find_level2_patterns32 status pid with Not_found -> assert false in let ast = instantiate32 idrefs env symbol args in @@ -334,110 +288,8 @@ let load_patterns32 t = HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t in set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t)) -in - Interpretations.add_load_patterns32 load_patterns32; - Interpretations.init () ;; -(* -let ast_of_acic ~output_type id_to_sort annterm = - debug_print (lazy ("ast_of_acic <- " - ^ CicPp.ppterm (Deannotate.deannotate_term annterm))); - let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in - let ast = ast_of_acic1 ~output_type term_info annterm in - debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast)); - ast, term_info.uri - -let fresh_id = - fun () -> - incr counter; - !counter - -let add_interpretation dsc (symbol, args) appl_pattern = - let id = fresh_id () in - Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern); - pattern32_matrix := (true, 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 get_all_interpretations () = - List.map - (function (_, _, id) -> - let (dsc, _, _, _) = - try - Hashtbl.find !level2_patterns32 id - with Not_found -> assert false - in - (id, dsc)) - !pattern32_matrix - -let get_active_interpretations () = - HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None) - !pattern32_matrix - -let set_active_interpretations ids = - let pattern32_matrix' = - List.map - (function - | (_, ap, id) when List.mem id ids -> (true, ap, id) - | (_, ap, id) -> (false, ap, id)) - !pattern32_matrix - in - pattern32_matrix := pattern32_matrix'; - load_patterns32 !pattern32_matrix - -exception Interpretation_not_found - -let lookup_interpretations symbol = - try - HExtlib.list_uniq - (List.sort Pervasives.compare - (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 remove_interpretation id = - (try - let dsc, 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; - load_patterns32 !pattern32_matrix - -let _ = load_patterns32 [] - -let instantiate_appl_pattern - ~mk_appl ~mk_implicit ~term_of_uri env appl_pattern -= - let lookup name = - try List.assoc name env - with Not_found -> - prerr_endline (sprintf "Name %s not found" name); - assert false - in - let rec aux = function - | Ast.UriPattern uri -> term_of_uri uri - | Ast.ImplicitPattern -> mk_implicit false - | Ast.VarPattern name -> lookup name - | Ast.ApplPattern terms -> mk_appl (List.map aux terms) - in - aux appl_pattern -*) - let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) = let module K = Content in let nast_of_cic = @@ -603,7 +455,7 @@ in let res = match kind with | NCic.Fixpoint (is_rec, ifl, _) -> - (gen_id object_prefix seed, [], conjectures, + (gen_id object_prefix seed, conjectures, `Joint { K.joint_id = gen_id joint_prefix seed; K.joint_kind = @@ -613,7 +465,7 @@ in K.joint_defs = List.map (build_fixpoint is_rec seed) ifl }) | NCic.Inductive (is_ind, lno, itl, _) -> - (gen_id object_prefix seed, [], conjectures, + (gen_id object_prefix seed, conjectures, `Joint { K.joint_id = gen_id joint_prefix seed; K.joint_kind = @@ -623,15 +475,17 @@ in | NCic.Constant (_,_,Some bo,ty,_) -> let ty = nast_of_cic ~context:[] ty in let bo = nast_of_cic ~context:[] bo in - (gen_id object_prefix seed, [], conjectures, + (gen_id object_prefix seed, conjectures, `Def (K.Const,ty, build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty)) | NCic.Constant (_,_,None,ty,_) -> let ty = nast_of_cic ~context:[] ty in - (gen_id object_prefix seed, [], conjectures, + (gen_id object_prefix seed, conjectures, `Decl (K.Const, (*CSC: ??? get_id ty here used to be the id of the axiom! *) build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty)) in res,ids_to_refs ;; + +Interpretations.set_load_patterns32 load_patterns32