X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FtermAcicContent.ml;h=eaa53259021821dc3dc4b053f6eeffbfa160915d;hb=47988107f44566d53fd5a71fd64a015bbf24a380;hp=7948f2654ac51aa29cc79d13f12bbb3dd6a71534;hpb=bdf989481462c1185c9cbbfdd4b31d13aa4352b3;p=helm.git diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index 7948f2654..eaa532590 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -44,17 +44,17 @@ type term_info = let get_types uri = let o,_ = CicEnvironment.get_obj CicUniv.empty_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,6 +66,9 @@ let constructor_of_inductive_type uri i j = fst (List.nth (constructors_of_inductive_type uri i) (j-1)) with Not_found -> assert false) + (* 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 k = k term_info in @@ -121,16 +124,31 @@ let ast_of_acic0 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)) -> - if CoercGraph.is_a_coercion (Deannotate.deannotate_term he) && - !Acic2content.hide_coercions + 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 + let deannot_he = Deannotate.deannotate_term he in + if CoercDb.is_a_coercion' deannot_he && !Acic2content.hide_coercions then - let rec last = - function - [] -> assert false - | [t] -> t - | _::tl -> last tl - in - idref aid (k (last tl)) + 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)) else idref aid (Ast.Appl (List.map k args)) | Cic.AAppl (aid,args) -> @@ -160,10 +178,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 @@ -173,7 +193,7 @@ 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 + let (capture_variables, rhs) = eat_branch lpsno ty pat in ((name, Some (ctor_puri !j), capture_variables), rhs)) constructors patterns with Invalid_argument _ -> assert false @@ -183,28 +203,72 @@ let ast_of_acic0 term_info acic k = 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