X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FtermAcicContent.ml;h=edb22c9442c5aaa53c9e43c7ea8b7a54b728c2e1;hb=910c252965fe17d6b5af92e4658e7d02bac82d58;hp=a25730e4d1fa0aed8e2279694d2d60d3a7d7deb7;hpb=7815a9150b5581f60e49ad6520f46ac287e073fa;p=helm.git diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index a25730e4d..edb22c944 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -42,19 +42,19 @@ type term_info = } let get_types uri = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with - | Cic.InductiveDefinition (l,_,_,_) -> l + | Cic.InductiveDefinition (l,_,lpsno,_) -> l, lpsno | _ -> assert false let name_of_inductive_type uri i = - let types = get_types uri in + let types, _ = get_types uri in let (name, _, _, _) = try List.nth types i with Not_found -> assert false in name (* returns pairs *) let constructors_of_inductive_type uri i = - let types = get_types uri in + let types, _ = get_types uri in let (_, _, _, constructors) = try List.nth types i with Not_found -> assert false in @@ -66,9 +66,11 @@ let constructor_of_inductive_type uri i j = fst (List.nth (constructors_of_inductive_type uri i) (j-1)) with Not_found -> assert false) -let hide_coercions = ref true;; + (* returns the number of left parameters *) +let left_params_no_of_inductive_type uri = + snd (get_types uri) -let ast_of_acic0 term_info acic k = +let ast_of_acic0 ~output_type term_info acic k = let k = k term_info in let id_to_uris = term_info.uri in let register_uri id uri = Hashtbl.add id_to_uris id uri in @@ -101,14 +103,14 @@ let ast_of_acic0 term_info acic k = | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop) | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set) | Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u)) - | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp) + | Cic.ASort (id,Cic.CProp u) -> idref id (Ast.Sort (`CProp u)) | Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput | Cic.AImplicit (id, _) -> idref id Ast.Implicit | Cic.AProd (id,n,s,t) -> let binder_kind = match sort_of_id id with | `Set | `Type _ -> `Pi - | `Prop | `CProp -> `Forall + | `Prop | `CProp _ -> `Forall in idref id (Ast.Binder (binder_kind, (CicNotationUtil.name_of_cic_name n, Some (k s)), k t)) @@ -116,24 +118,33 @@ let ast_of_acic0 term_info acic k = | Cic.ALambda (id,n,s,t) -> idref id (Ast.Binder (`Lambda, (CicNotationUtil.name_of_cic_name n, Some (k s)), k t)) - | Cic.ALetIn (id,n,s,t) -> - idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None), + | Cic.ALetIn (id,n,s,ty,t) -> + idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, Some (k ty)), k s, k t)) | 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)) -> - if CoercGraph.is_a_coercion (Deannotate.deannotate_term he) && - !hide_coercions - then - let rec last = - function - [] -> assert false - | [t] -> t - | _::tl -> last tl - in - idref aid (k (last tl)) - else - idref aid (Ast.Appl (List.map k args)) + | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) as t -> + (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 + 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) -> idref aid (Ast.Appl (List.map k args)) | Cic.AConst (id,uri,substs) -> @@ -161,10 +172,12 @@ let ast_of_acic0 term_info acic k = in let case_indty = name, Some (UriManager.uri_of_string puri_str) in let constructors = constructors_of_inductive_type uri typeno in - let rec eat_branch ty pat = + let lpsno = left_params_no_of_inductive_type uri in + let rec eat_branch n ty pat = match (ty, pat) with + | Cic.Prod (_, _, t), _ when n > 0 -> eat_branch (pred n) t pat | Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') -> - let (cv, rhs) = eat_branch t t' in + let (cv, rhs) = eat_branch 0 t t' in (CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs | _, _ -> [], k pat in @@ -174,38 +187,91 @@ let ast_of_acic0 term_info acic k = List.map2 (fun (name, ty) pat -> incr j; - let (capture_variables, rhs) = eat_branch ty pat in - ((name, Some (ctor_puri !j), capture_variables), rhs)) - constructors patterns + let name,(capture_variables,rhs) = + match output_type with + `Term -> name, eat_branch lpsno ty pat + | `Pattern -> "_", ([], k pat) + in + Ast.Pattern (name, Some (ctor_puri !j), capture_variables), rhs + ) constructors patterns with Invalid_argument _ -> assert false in - idref id (Ast.Case (k te, Some case_indty, Some (k ty), patterns)) + let indty = + match output_type with + `Pattern -> None + | `Term -> Some case_indty + in + idref id (Ast.Case (k te, indty, Some (k ty), patterns)) | Cic.AFix (id, no, funs) -> let defs = List.map (fun (_, n, decr_idx, ty, bo) -> - ((Ast.Ident (n, None), Some (k ty)), k bo, decr_idx)) + let params,bo = + let rec aux = + function + Cic.ALambda (_,name,so,ta) -> + let params,rest = aux ta in + (CicNotationUtil.name_of_cic_name name,Some (k so)):: + params, rest + | t -> [],t + in + aux bo + in + let ty = + let rec eat_pis = + function + 0,ty -> ty + | n,Cic.AProd (_,_,_,ta) -> eat_pis (n - 1,ta) + | n,ty -> + (* I should do a whd here, but I have no context *) + assert false + in + eat_pis ((List.length params),ty) + in + (params,(Ast.Ident (n, None), Some (k ty)), k bo, decr_idx)) funs in let name = try (match List.nth defs no with - | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n + | _, (Ast.Ident (n, _), _), _, _ when n <> "_" -> n | _ -> assert false) with Not_found -> assert false in - idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None))) + idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None))) | Cic.ACoFix (id, no, funs) -> let defs = List.map (fun (_, n, ty, bo) -> - ((Ast.Ident (n, None), Some (k ty)), k bo, 0)) + let params,bo = + let rec aux = + function + Cic.ALambda (_,name,so,ta) -> + let params,rest = aux ta in + (CicNotationUtil.name_of_cic_name name,Some (k so)):: + params, rest + | t -> [],t + in + aux bo + in + let ty = + let rec eat_pis = + function + 0,ty -> ty + | n,Cic.AProd (_,_,_,ta) -> eat_pis (n - 1,ta) + | n,ty -> + (* I should do a whd here, but I have no context *) + assert false + in + eat_pis ((List.length params),ty) + in + (params,(Ast.Ident (n, None), Some (k ty)), k bo, 0)) funs in let name = try (match List.nth defs no with - | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n + | _, (Ast.Ident (n, _), _), _, _ when n <> "_" -> n | _ -> assert false) with Not_found -> assert false in @@ -234,7 +300,11 @@ let add_idrefs = let instantiate32 term_info idrefs env symbol args = let rec instantiate_arg = function | Ast.IdentArg (n, name) -> - let t = (try List.assoc name env with Not_found -> assert false) in + let t = + try List.assoc name env + with Not_found -> prerr_endline ("name not found in env: "^name); + assert false + in let rec count_lambda = function | Ast.AttributedTerm (_, t) -> count_lambda t | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body @@ -257,11 +327,12 @@ let instantiate32 term_info idrefs env symbol args = if args = [] then head else Ast.Appl (head :: List.map instantiate_arg args) -let rec ast_of_acic1 term_info annterm = +let rec ast_of_acic1 ~output_type term_info annterm = let id_to_uris = term_info.uri in let register_uri id uri = Hashtbl.add id_to_uris id uri in match (get_compiled32 ()) annterm with - | None -> ast_of_acic0 term_info annterm ast_of_acic1 + | None -> + ast_of_acic0 ~output_type term_info annterm (ast_of_acic1 ~output_type) | Some (env, ctors, pid) -> let idrefs = List.map @@ -275,7 +346,8 @@ let rec ast_of_acic1 term_info annterm = ctors in let env' = - List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env + List.map + (fun (name, term) -> name, ast_of_acic1 ~output_type term_info term) env in let _, symbol, args, _ = try @@ -291,16 +363,21 @@ let load_patterns32 t = in set_compiled32 (lazy (Acic2astMatcher.Matcher32.compiler t)) -let ast_of_acic id_to_sort annterm = +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 term_info annterm 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 counter = ref ~-1 +let reset () = + counter := ~-1; + Hashtbl.clear level2_patterns32; + Hashtbl.clear interpretations +;; let fresh_id = - let counter = ref ~-1 in fun () -> incr counter; !counter @@ -361,7 +438,7 @@ let lookup_interpretations symbol = let remove_interpretation id = (try - let _, symbol, _, _ = Hashtbl.find level2_patterns32 id 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;