X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FtermAcicContent.ml;h=81d0ef0a74f12211cb7a8e74ba7fd504fbf5311e;hb=c83721701dbbd44d3d547fdec6c4a5658322f424;hp=508411d2847b1b84083141efa5bbe14aed16a8fa;hpb=266fe24a5a5548c30f597ccd38578877643404d3;p=helm.git diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index 508411d28..81d0ef0a7 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -28,6 +28,7 @@ open Printf module Ast = CicNotationPt +module Obj = LibraryObjects let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () @@ -70,6 +71,21 @@ let constructor_of_inductive_type uri i j = let left_params_no_of_inductive_type uri = snd (get_types uri) +let destroy_nat annterm = + let is_zero = function + | Cic.AMutConstruct (_, uri, 0, 1, _) when Obj.is_nat_URI uri -> true + | _ -> false + in + let is_succ = function + | Cic.AMutConstruct (_, uri, 0, 2, _) when Obj.is_nat_URI uri -> true + | _ -> false + in + let rec aux acc = function + | Cic.AAppl (_, [he ; tl]) when is_succ he -> aux (acc + 1) tl + | t when is_zero t -> Some acc + | _ -> None in + aux 0 annterm + let ast_of_acic0 ~output_type term_info acic k = let k = k term_info in let id_to_uris = term_info.uri in @@ -110,7 +126,7 @@ let ast_of_acic0 ~output_type term_info acic k = let binder_kind = match sort_of_id id with | `Set | `Type _ | `NType _ -> `Pi - | `Prop | `CProp _ -> `Forall + | `Prop | `CProp _ | `NCProp _ -> `Forall in idref id (Ast.Binder (binder_kind, (CicNotationUtil.name_of_cic_name n, Some (k s)), k t)) @@ -124,7 +140,7 @@ 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 -> - (match LibraryObjects.destroy_nat t with + (match destroy_nat t with | Some n -> idref aid (Ast.Num (string_of_int n, -1)) | None -> let deannot_he = Deannotate.deannotate_term he in @@ -138,11 +154,11 @@ let ast_of_acic0 ~output_type term_info acic k = try HExtlib.split_nth (cpos+sats+1) tl with Failure _ -> [],[] in if rest = [] then - idref aid (List.nth (List.map k tl) cpos) + idref aid (k (List.nth tl cpos)) else idref aid (Ast.Appl (List.map k (List.nth tl cpos::rest))) else - idref aid (Ast.Appl (List.map k tl)) + idref aid (Ast.Appl (List.map k args)) else idref aid (Ast.Appl (List.map k args))) | Cic.AAppl (aid,args) -> @@ -290,6 +306,7 @@ let interpretations = ref (initial_interpretations ()) let compiled32 = ref None let pattern32_matrix = ref [] let counter = ref ~-1 +let find_level2_patterns32 pid = Hashtbl.find !level2_patterns32 pid;; let stack = ref [] @@ -378,17 +395,23 @@ let rec ast_of_acic1 ~output_type term_info annterm = in let _, symbol, args, _ = try - Hashtbl.find !level2_patterns32 pid + find_level2_patterns32 pid with Not_found -> assert false in let ast = instantiate32 term_info idrefs env' symbol args in Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), ast) -let load_patterns32 t = +let load_patterns32s = + let load_patterns32 t = let t = HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t in - set_compiled32 (lazy (Acic2astMatcher.Matcher32.compiler t)) + set_compiled32 (lazy (Acic2astMatcher.Matcher32.compiler t)) + in + ref [load_patterns32] +;; + +let add_load_patterns32 f = load_patterns32s := f :: !load_patterns32s;; let ast_of_acic ~output_type id_to_sort annterm = debug_print (lazy ("ast_of_acic <- " @@ -407,7 +430,7 @@ 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; + List.iter (fun f -> f !pattern32_matrix) !load_patterns32s; (try let ids = Hashtbl.find !interpretations symbol in ids := id :: !ids @@ -438,23 +461,26 @@ let set_active_interpretations ids = !pattern32_matrix in pattern32_matrix := pattern32_matrix'; - load_patterns32 !pattern32_matrix + List.iter (fun f -> f !pattern32_matrix) !load_patterns32s exception Interpretation_not_found -let lookup_interpretations symbol = +let lookup_interpretations ?(sorted=true) 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))) + let raw = + 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) + in + if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw) + else raw with Not_found -> raise Interpretation_not_found let remove_interpretation id = @@ -466,12 +492,12 @@ let remove_interpretation id = with Not_found -> raise Interpretation_not_found); pattern32_matrix := List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix; - load_patterns32 !pattern32_matrix + List.iter (fun f -> f !pattern32_matrix) !load_patterns32s -let _ = load_patterns32 [] +let init () = List.iter (fun f -> f []) !load_patterns32s let instantiate_appl_pattern - ~mk_appl ~mk_implicit ~term_of_uri env appl_pattern + ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env appl_pattern = let lookup name = try List.assoc name env @@ -481,6 +507,7 @@ let instantiate_appl_pattern in let rec aux = function | Ast.UriPattern uri -> term_of_uri uri + | Ast.NRefPattern nref -> term_of_nref nref | Ast.ImplicitPattern -> mk_implicit false | Ast.VarPattern name -> lookup name | Ast.ApplPattern terms -> mk_appl (List.map aux terms)