X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_cic_content%2Finterpretations.ml;h=794859369bbc62f593f392b80b73fcf63d6e19b7;hb=74c6905907b0bca229366d52450e2a6982b5b8be;hp=7e175193ba5493b3da527fd71c32af6490c49f37;hpb=551861bf1adbb1db5b0b9941b98ba54531157364;p=helm.git diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml index 7e175193b..794859369 100644 --- a/matita/components/ng_cic_content/interpretations.ml +++ b/matita/components/ng_cic_content/interpretations.ml @@ -58,12 +58,12 @@ type db = { Lazy.t } -let initial_db = { +let initial_db status = { counter = -1; pattern32_matrix = []; level2_patterns32 = IntMap.empty; interpretations = StringMap.empty; - compiled32 = lazy (fun _ -> assert false) + compiled32 = lazy (Ncic2astMatcher.Matcher32.compiler status []) } class type g_status = @@ -72,15 +72,17 @@ class type g_status = method interp_db: db end -class status = - object +class virtual status = + object(self) inherit NCicCoercion.status - val interp_db = initial_db - method interp_db = interp_db - method set_interp_db v = {< interp_db = v >} + val mutable interp_db = None (* mutable only to initialize it :-( *) + method interp_db = match interp_db with None -> assert false | Some x -> x + method set_interp_db v = {< interp_db = Some v >} method set_interp_status : 'status. #g_status as 'status -> 'self - = fun o -> {< interp_db = o#interp_db >}#set_coercion_status o + = fun o -> {< interp_db = Some o#interp_db >}#set_coercion_status o + initializer + interp_db <- Some (initial_db self) end let idref register_ref = @@ -105,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 @@ -144,7 +146,7 @@ let load_patterns32 status t = in status#set_interp_db {status#interp_db with - compiled32 = lazy (Ncic2astMatcher.Matcher32.compiler t) } + compiled32 = lazy (Ncic2astMatcher.Matcher32.compiler status t) } ;; let add_interpretation status dsc (symbol, args) appl_pattern = @@ -206,7 +208,7 @@ let instantiate_appl_pattern let destroy_nat = let is_nat_URI = NUri.eq (NUri.uri_of_string - "cic:/matita/ng/arithmetics/nat/nat.ind") in + "cic:/matita/arithmetics/nat/nat.ind") in let is_zero = function | NCic.Const (NReference.Ref (uri, NReference.Con (0, 1, 0))) when is_nat_URI uri -> true @@ -237,15 +239,15 @@ let nast_of_cic0 status idref (Ast.Ident (name,None)) with Failure "nth" | Invalid_argument "List.nth" -> idref (Ast.Ident ("-" ^ string_of_int (n - List.length context),None))) - | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s true r, None)) + | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s status true r, None)) | NCic.Meta (n,lc) when List.mem_assoc n subst -> let _,_,t,_ = List.assoc n subst in - k ~context (NCicSubstitution.subst_meta lc t) + k ~context (NCicSubstitution.subst_meta status lc t) | NCic.Meta (n,(s,l)) -> (* CSC: qua non dovremmo espandere *) let l = NCicUtils.expand_local_context l in idref (Ast.Meta - (n, List.map (fun x -> Some (k ~context (NCicSubstitution.lift s x))) l)) + (n, List.map (fun x -> Some (k ~context (NCicSubstitution.lift status s x))) l)) | NCic.Sort NCic.Prop -> idref (Ast.Sort `Prop) | NCic.Sort NCic.Type [] -> idref (Ast.Sort `Set) | NCic.Sort NCic.Type ((`Type,u)::_) -> @@ -265,16 +267,16 @@ 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 ty, k ~context:((n,NCic.Decl s)::context) t)) | NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst -> let _,_,t,_ = List.assoc n subst in - let hd = NCicSubstitution.subst_meta lc t in + let hd = NCicSubstitution.subst_meta status lc t in k ~context - (NCicReduction.head_beta_reduce ~upto:(List.length args) + (NCicReduction.head_beta_reduce status ~upto:(List.length args) (match hd with | NCic.Appl l -> NCic.Appl (l@args) | _ -> NCic.Appl (hd :: args))) @@ -303,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 @@ -315,13 +318,13 @@ let nast_of_cic0 status let case_indty = name, None(*CSC Some (UriManager.uri_of_string puri_str)*) in let constructors, leftno = - let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys r in + let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in let _,_,_,cl = List.nth tys n in cl,leftno 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 @@ -349,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 = @@ -388,11 +397,12 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = idref ast (*Ast.AttributedTerm (`IdRef (idref term), ast)*) ;; -let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) = +let nmap_context0 status ~idref ~metasenv ~subst context = let module K = Content in let nast_of_cic = - nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in - let context',_ = + nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst + in + fst ( List.fold_right (fun item (res,context) -> match item with @@ -418,17 +428,15 @@ let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) = K.def_term = nast_of_cic ~context t; K.def_type = nast_of_cic ~context ty })::res,item::context - ) context ([],[]) - in - ("-1",i,context',nast_of_cic ~context ty) + ) context ([],[])) ;; -let nmap_sequent status ~metasenv ~subst conjecture = +let nmap_sequent0 status ~idref ~metasenv ~subst (i,(_n,context,ty)) = let module K = Content in - let ids_to_refs = Hashtbl.create 211 in - let register_ref = Hashtbl.add ids_to_refs in - nmap_sequent0 status ~idref:(idref register_ref) ~metasenv ~subst conjecture, - ids_to_refs + let nast_of_cic = + nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in + let context' = nmap_context0 status ~idref ~metasenv ~subst context in + ("-1",i,context',nast_of_cic ~context ty) ;; let object_prefix = "obj:";; @@ -449,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 @@ -501,11 +509,8 @@ let build_decl_item seed id n s = } ;; -let nmap_obj status (uri,_,metasenv,subst,kind) = +let nmap_cobj0 status ~idref (uri,_,metasenv,subst,kind) = let module K = Content in - let ids_to_refs = Hashtbl.create 211 in - let register_ref = Hashtbl.add ids_to_refs in - let idref = idref register_ref in let nast_of_cic = nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in let seed = ref 0 in @@ -538,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 @@ -550,38 +555,100 @@ let build_fixpoint b seed = K.def_term = t; } in - let res = - match kind with - | NCic.Fixpoint (is_rec, ifl, _) -> - (gen_id object_prefix seed, conjectures, - `Joint - { K.joint_id = gen_id joint_prefix seed; - K.joint_kind = - if is_rec then - `Recursive (List.map (fun (_,_,i,_,_) -> i) ifl) - else `CoRecursive; - K.joint_defs = List.map (build_fixpoint is_rec seed) ifl - }) - | NCic.Inductive (is_ind, lno, itl, _) -> - (gen_id object_prefix seed, conjectures, - `Joint - { K.joint_id = gen_id joint_prefix seed; - K.joint_kind = - if is_ind then `Inductive lno else `CoInductive lno; - K.joint_defs = List.map (build_inductive is_ind seed) itl - }) - | NCic.Constant (_,_,Some bo,ty,_) -> - let ty = nast_of_cic ~context:[] ty in - let bo = nast_of_cic ~context:[] bo in - (gen_id object_prefix seed, conjectures, - `Def (K.Const,ty, - build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty)) - | NCic.Constant (_,_,None,ty,_) -> - let ty = nast_of_cic ~context:[] ty in - (gen_id object_prefix seed, conjectures, - `Decl (K.Const, - (*CSC: ??? get_id ty here used to be the id of the axiom! *) - build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty)) - in - res,ids_to_refs + match kind with + | NCic.Fixpoint (is_rec, ifl, _) -> + (gen_id object_prefix seed, conjectures, + `Joint + { K.joint_id = gen_id joint_prefix seed; + K.joint_kind = + if is_rec then + `Recursive (List.map (fun (_,_,i,_,_) -> i) ifl) + else `CoRecursive; + K.joint_defs = List.map (build_fixpoint is_rec seed) ifl + }) + | NCic.Inductive (is_ind, lno, itl, _) -> + (gen_id object_prefix seed, conjectures, + `Joint + { K.joint_id = gen_id joint_prefix seed; + K.joint_kind = + if is_ind then `Inductive lno else `CoInductive lno; + K.joint_defs = List.map (build_inductive is_ind seed) itl + }) + | NCic.Constant (_,_,Some bo,ty,_) -> + let ty = nast_of_cic ~context:[] ty in + let bo = nast_of_cic ~context:[] bo in + (gen_id object_prefix seed, conjectures, + `Def (K.Const,ty, + build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty)) + | NCic.Constant (_,_,None,ty,_) -> + let ty = nast_of_cic ~context:[] ty in + (gen_id object_prefix seed, conjectures, + `Decl (K.Const, + (*CSC: ??? get_id ty here used to be the id of the axiom! *) + build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty)) +;; + +let with_idrefs foo status obj = + let ids_to_refs = Hashtbl.create 211 in + let register_ref = Hashtbl.add ids_to_refs in + foo status ~idref:(idref register_ref) obj, ids_to_refs ;; + +let nmap_cobj status = with_idrefs nmap_cobj0 status + +let nmap_sequent status ~metasenv ~subst = + with_idrefs (nmap_sequent0 ~metasenv ~subst) status + +let nmap_term status ~metasenv ~subst ~context = + with_idrefs (nast_of_cic1 ~output_type:`Term ~metasenv ~subst ~context) status + +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