X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_cic_content%2Finterpretations.ml;h=794859369bbc62f593f392b80b73fcf63d6e19b7;hb=3220eee6c3dd2968727c5c595d6ca78e89291b5f;hp=ee4bb9437ca5a5002f3f2587768b29a03ac2e239;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml index ee4bb9437..794859369 100644 --- a/matita/components/ng_cic_content/interpretations.ml +++ b/matita/components/ng_cic_content/interpretations.ml @@ -107,7 +107,7 @@ let add_idrefs = List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) let instantiate32 idrefs env symbol args = - let rec instantiate_arg = function + let instantiate_arg = function | Ast.IdentArg (n, name) -> let t = try List.assoc name env @@ -267,7 +267,7 @@ let nast_of_cic0 status | NCic.Lambda (n,s,t) -> idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context s)), k ~context:((n,NCic.Decl s)::context) t)) - | NCic.LetIn (n,s,ty,NCic.Rel 1) -> + | NCic.LetIn (_n,s,ty,NCic.Rel 1) -> idref (Ast.Cast (k ~context ty, k ~context s)) | NCic.LetIn (n,s,ty,t) -> idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context s)), k ~context @@ -305,6 +305,7 @@ let nast_of_cic0 status [arg] -> idref (k ~context arg) | _ -> idref (Ast.Appl (List.map (k ~context) args)))) | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) -> + (try let name = NUri.name_of_uri uri in (* CSC let uri_str = UriManager.string_of_uri uri in @@ -323,7 +324,7 @@ let nast_of_cic0 status in let rec eat_branch n ctx ty pat = match (ty, pat) with - | NCic.Prod (name, s, t), _ when n > 0 -> + | NCic.Prod (_name, _s, t), _ when n > 0 -> eat_branch (pred n) ctx t pat | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') -> let cv, rhs = eat_branch 0 ((name,NCic.Decl s)::ctx) t t' in @@ -351,6 +352,12 @@ let nast_of_cic0 status | `Term -> Some case_indty in idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns)) + with + NCicEnvironment.ObjectNotFound msg -> + idref (Ast.Case(k ~context te,Some ("NOT_FOUND: " ^ Lazy.force msg,None), + Some (k ~context outty), + (List.map (fun t -> Ast.Pattern ("????", None, []), k ~context t) + patterns)))) ;; let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = @@ -424,7 +431,7 @@ let nmap_context0 status ~idref ~metasenv ~subst context = ) context ([],[])) ;; -let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) = +let nmap_sequent0 status ~idref ~metasenv ~subst (i,(_n,context,ty)) = let module K = Content in let nast_of_cic = nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in @@ -450,7 +457,7 @@ let gen_id prefix seed = res ;; -let build_def_item seed context metasenv id n t ty = +let build_def_item seed _context _metasenv id n t ty = let module K = Content in (* try @@ -502,7 +509,7 @@ let build_decl_item seed id n s = } ;; -let nmap_obj0 status ~idref (uri,_,metasenv,subst,kind) = +let nmap_cobj0 status ~idref (uri,_,metasenv,subst,kind) = let module K = Content in let nast_of_cic = nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in @@ -536,7 +543,7 @@ let build_inductive b seed = K.inductive_constructors = build_constructors seed cl } in -let build_fixpoint b seed = +let build_fixpoint _b seed = fun (_,n,_,ty,t) -> let t = nast_of_cic ~context:[] t in let ty = nast_of_cic ~context:[] ty in @@ -587,7 +594,7 @@ let with_idrefs foo status obj = foo status ~idref:(idref register_ref) obj, ids_to_refs ;; -let nmap_obj status = with_idrefs nmap_obj0 status +let nmap_cobj status = with_idrefs nmap_cobj0 status let nmap_sequent status ~metasenv ~subst = with_idrefs (nmap_sequent0 ~metasenv ~subst) status @@ -597,3 +604,51 @@ let nmap_term status ~metasenv ~subst ~context = let nmap_context status ~metasenv ~subst = with_idrefs (nmap_context0 ~metasenv ~subst) status + +(* FG ***********************************************************************) + +let nmap_obj0 status ~idref (_, _, metasenv, subst, kind) = + let module N = NotationPt in + let nast_of_cic = + nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst + in + let rec mk_captures lno k c u = match lno, u with + | 0, _ -> k, c + | _, NCic.Prod (n, w, u) when lno > 0 -> + let cap = nast_of_cic ~context:c w, None in + let hyp = n, NCic.Decl w in + mk_captures (pred lno) (cap :: k) (hyp :: c) u + | _ -> assert false + in + let build_captures lno = function + | [] -> [], [] + | (_, _, u, _) :: _ -> mk_captures lno [] [] u + in + let rec eat_prods prods lno t = match prods, lno, t with + | _, 0, _ -> t + | true, _, NCic.Prod (_, _, t) when lno > 0 -> eat_prods prods (pred lno) t + | false, _, NCic.Lambda (_, _, t) when lno > 0 -> eat_prods prods (pred lno) t + | _ -> assert false + in + let build_constractor lno context (_, n, bo) = + let bo = nast_of_cic ~context (eat_prods false lno bo) in + n, bo + in + let build_inductive is_ind lno context (_, n, ty, cl) = + let ty = nast_of_cic ~context (eat_prods true lno ty) in + n, is_ind, ty, List.map (build_constractor lno context) cl + in + match kind with + | NCic.Constant (_, n, xbo, ty, attrs) -> + let ty = nast_of_cic ~context:[] ty in + let xbo = match xbo with + | Some bo -> Some (nast_of_cic ~context:[] bo) + | None -> None + in + N.Theorem (n, ty, xbo, attrs) + | NCic.Inductive (is_ind, lno, itl, (src, `Regular)) -> + let captures, context = build_captures lno itl in + N.Inductive (captures, List.map (build_inductive is_ind lno context) itl, src) + | _ -> assert false (* NCic.Fixpoint (is_rec, ifl, _) -> *) + +let nmap_obj status = with_idrefs nmap_obj0 status