X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FtermAcicContent.ml;h=681f3cd541312e8dff3e86e475cfe3e89aa0db7d;hb=b02253b371aadbbb37226a685b9bd8777a64d175;hp=622a816181ba0489fa4ee4fcdba26e63572073cd;hpb=5d010a40c726d9a7eceeb35e70e41a158eb63c70;p=helm.git diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index 622a81618..681f3cd54 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,8 +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) + (* 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 @@ -120,7 +123,7 @@ let ast_of_acic0 term_info acic k = 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)) -> + | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) as t -> let last_n n l = let rec aux = function @@ -140,14 +143,17 @@ let ast_of_acic0 term_info acic k = 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 - 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)) + (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))) + 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) -> @@ -175,10 +181,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 @@ -188,12 +196,21 @@ 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 @@ -315,11 +332,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 @@ -333,7 +351,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 @@ -349,11 +368,11 @@ 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