X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_cic_content%2Finterpretations.ml;h=e2c8c76d0c53a4286b8fca9643507f00dacbcc69;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=0c78e08f999f066ec25e609e6129c20884189ae5;hpb=09c63c35520ceea6f0caaa0be856a3eaff46bb88;p=helm.git diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml index 0c78e08f9..e2c8c76d0 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 (Ncic2astMatcher.Matcher32.compiler []) + 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 = @@ -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 = @@ -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)::_) -> @@ -272,9 +274,9 @@ let nast_of_cic0 status 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,7 +318,7 @@ 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 @@ -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:";; @@ -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 @@ -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, (_, `Regular)) -> + let captures, context = build_captures lno itl in + N.Inductive (captures, List.map (build_inductive is_ind lno context) itl) + | _ -> assert false (* NCic.Fixpoint (is_rec, ifl, _) -> *) + +let nmap_obj status = with_idrefs nmap_obj0 status