X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FtermAcicContent.ml;h=61e77c6fe12047b9efbe5939a362df8b088333fb;hb=987627a48b2a3c2345d1af2c2a6b1ab78aa90b58;hp=da5aa49609fab082c97661faa97e6f7a150fe8f7;hpb=04c4835d193b96b7a01bc725abd9f3282c91a9ed;p=helm.git diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index da5aa4960..61e77c6fe 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -124,34 +124,25 @@ let ast_of_acic0 ~output_type term_info acic k = | Cic.AAppl (aid,(Cic.AConst _ as he::tl as args)) | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args)) | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) as t -> - let last_n n l = - let rec aux = - function - [] -> assert false - | [_] as l -> l,1 - | he::tl -> - let (res,len) as res' = aux tl in - if len < n then - he::res,len + 1 - else - res' - in - match fst (aux l) with - [] -> assert false - | [t] -> t - | Ast.AttributedTerm (_,(Ast.Appl l))::tl -> - idref aid (Ast.Appl (l@tl)) - | l -> idref aid (Ast.Appl l) - in (match LibraryObjects.destroy_nat t with | Some n -> idref aid (Ast.Num (string_of_int n, -1)) | None -> let deannot_he = Deannotate.deannotate_term he in - if CoercDb.is_a_coercion' deannot_he && !Acic2content.hide_coercions - then - (match CoercDb.is_a_coercion_to_funclass deannot_he with - | None -> idref aid (last_n 1 (List.map k tl)) - | Some i -> idref aid (last_n (i+1) (List.map k tl))) + let coercion_info = CoercDb.is_a_coercion deannot_he in + if coercion_info <> None && !Acic2content.hide_coercions then + match coercion_info with + | None -> assert false + | Some (_,_,_,sats,cpos) -> + if cpos < List.length tl then + let _,rest = + try HExtlib.split_nth (cpos+sats+1) tl with Failure _ -> [],[] + in + if rest = [] then + idref aid (List.nth (List.map k tl) cpos) + else + idref aid (Ast.Appl (List.map k (List.nth tl cpos::rest))) + else + idref aid (Ast.Appl (List.map k tl)) else idref aid (Ast.Appl (List.map k args))) | Cic.AAppl (aid,args) -> @@ -290,11 +281,38 @@ let ast_of_acic0 ~output_type term_info acic k = (* persistent state *) -let level2_patterns32 = Hashtbl.create 211 -let interpretations = Hashtbl.create 211 (* symb -> id list ref *) +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 @@ -360,7 +378,7 @@ let rec ast_of_acic1 ~output_type term_info annterm = in let _, symbol, args, _ = try - Hashtbl.find level2_patterns32 pid + Hashtbl.find !level2_patterns32 pid with Not_found -> assert false in let ast = instantiate32 term_info idrefs env' symbol args in @@ -380,8 +398,6 @@ let ast_of_acic ~output_type id_to_sort annterm = debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast)); ast, term_info.uri -let counter = ref ~-1 -let reset () = counter := ~-1;; let fresh_id = fun () -> incr counter; @@ -389,13 +405,13 @@ let fresh_id = let add_interpretation dsc (symbol, args) appl_pattern = let id = fresh_id () in - Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern); + 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 + let ids = Hashtbl.find !interpretations symbol in ids := id :: !ids - with Not_found -> Hashtbl.add interpretations symbol (ref [id])); + with Not_found -> Hashtbl.add !interpretations symbol (ref [id])); id let get_all_interpretations () = @@ -403,7 +419,7 @@ let get_all_interpretations () = (function (_, _, id) -> let (dsc, _, _, _) = try - Hashtbl.find level2_patterns32 id + Hashtbl.find !level2_patterns32 id with Not_found -> assert false in (id, dsc)) @@ -434,19 +450,19 @@ let lookup_interpretations symbol = (fun id -> let (dsc, _, args, appl_pattern) = try - Hashtbl.find level2_patterns32 id + Hashtbl.find !level2_patterns32 id with Not_found -> assert false in dsc, args, appl_pattern) - !(Hashtbl.find interpretations symbol))) + !(Hashtbl.find !interpretations symbol))) with Not_found -> raise Interpretation_not_found let remove_interpretation id = (try - let _, symbol, _, _ = Hashtbl.find level2_patterns32 id in - let ids = Hashtbl.find interpretations symbol in + 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; + Hashtbl.remove !level2_patterns32 id; with Not_found -> raise Interpretation_not_found); pattern32_matrix := List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix; @@ -454,7 +470,9 @@ let remove_interpretation id = let _ = load_patterns32 [] -let instantiate_appl_pattern env appl_pattern = +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 -> @@ -462,10 +480,10 @@ let instantiate_appl_pattern env appl_pattern = assert false in let rec aux = function - | Ast.UriPattern uri -> CicUtil.term_of_uri uri - | Ast.ImplicitPattern -> Cic.Implicit None + | Ast.UriPattern uri -> term_of_uri uri + | Ast.ImplicitPattern -> mk_implicit false | Ast.VarPattern name -> lookup name - | Ast.ApplPattern terms -> Cic.Appl (List.map aux terms) + | Ast.ApplPattern terms -> mk_appl (List.map aux terms) in aux appl_pattern