From: Claudio Sacerdoti Coen Date: Thu, 4 Nov 2010 20:26:10 +0000 (+0000) Subject: - content/interpretations.ml and ng_cic_content/nTermCicContent.ml where X-Git-Tag: make_still_working~2734 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=551861bf1adbb1db5b0b9941b98ba54531157364;hp=01b29f47d0d3e6c131fbdcc7a4180d428c8c97b9;p=helm.git - content/interpretations.ml and ng_cic_content/nTermCicContent.ml where mutually recursive and part of the status was kept imperatively; the two files have been merged together into ng_cic_content/interpretations.ml --- diff --git a/matita/components/METAS/meta.helm-ng_disambiguation.src b/matita/components/METAS/meta.helm-ng_disambiguation.src index 84eeab3fe..97a3c1346 100644 --- a/matita/components/METAS/meta.helm-ng_disambiguation.src +++ b/matita/components/METAS/meta.helm-ng_disambiguation.src @@ -1,4 +1,4 @@ -requires="helm-content helm-ng_refiner helm-disambiguation" +requires="helm-ng_cic_content helm-ng_refiner helm-disambiguation" version="0.0.1" archive(byte)="ng_disambiguation.cma" archive(native)="ng_disambiguation.cmxa" diff --git a/matita/components/Makefile b/matita/components/Makefile index 7d463f88c..b1485c5cf 100644 --- a/matita/components/Makefile +++ b/matita/components/Makefile @@ -15,12 +15,12 @@ MODULES = \ ng_kernel \ getter \ library \ - content \ + content \ grafite \ - disambiguation \ ng_refiner \ - ng_disambiguation \ ng_cic_content \ + disambiguation \ + ng_disambiguation \ ng_paramodulation \ ng_library \ content_pres \ diff --git a/matita/components/content/.depend b/matita/components/content/.depend index d5941b8ef..f4b4f3037 100644 --- a/matita/components/content/.depend +++ b/matita/components/content/.depend @@ -2,7 +2,6 @@ content.cmi: notationUtil.cmi: notationPt.cmo notationEnv.cmi: notationPt.cmo notationPp.cmi: notationPt.cmo notationEnv.cmi -interpretations.cmi: notationPt.cmo notationPt.cmo: notationPt.cmx: content.cmo: content.cmi @@ -13,5 +12,3 @@ notationEnv.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi notationPp.cmo: notationPt.cmo notationEnv.cmi notationPp.cmi notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi -interpretations.cmo: notationUtil.cmi notationPt.cmo interpretations.cmi -interpretations.cmx: notationUtil.cmx notationPt.cmx interpretations.cmi diff --git a/matita/components/content/Makefile b/matita/components/content/Makefile index 5ea3ee796..8ea1cd33c 100644 --- a/matita/components/content/Makefile +++ b/matita/components/content/Makefile @@ -6,7 +6,6 @@ INTERFACE_FILES = \ notationUtil.mli \ notationEnv.mli \ notationPp.mli \ - interpretations.mli \ $(NULL) IMPLEMENTATION_FILES = \ notationPt.ml \ diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml deleted file mode 100644 index 28957074f..000000000 --- a/matita/components/content/interpretations.ml +++ /dev/null @@ -1,177 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -open Printf - -module Ast = NotationPt - -let debug = false -let debug_print s = if debug then prerr_endline (Lazy.force s) else () - -let load_patterns32 = ref (fun _ -> assert false);; -let set_load_patterns32 f = load_patterns32 := f;; - -let idref id t = Ast.AttributedTerm (`IdRef id, t) - -type cic_id = string - -type term_info = - { sort: (cic_id, Ast.sort_kind) Hashtbl.t; - uri: (cic_id, NReference.reference) Hashtbl.t; - } - -module IntMap = Map.Make(struct type t = int let compare = compare end);; -module StringMap = Map.Make(String);; - -type db = { - counter: int; - pattern32_matrix: (bool * NotationPt.cic_appl_pattern * int) list; - level2_patterns32: - (string * string * NotationPt.argument_pattern list * - NotationPt.cic_appl_pattern) IntMap.t; - interpretations: int list StringMap.t; (* symb -> id list *) -} - -let initial_db = { - counter = -1; - pattern32_matrix = []; - level2_patterns32 = IntMap.empty; - interpretations = StringMap.empty -} - -class type g_status = - object - method interp_db: db - end - -class status = - object - val interp_db = initial_db - method interp_db = interp_db - method set_interp_db v = {< interp_db = v >} - method set_interp_status - : 'status. #g_status as 'status -> 'self - = fun o -> {< interp_db = o#interp_db >} - end - -let find_level2_patterns32 status pid = - IntMap.find pid status#interp_db.level2_patterns32 - -let add_idrefs = - List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) - -let instantiate32 term_info idrefs env symbol args = - let rec instantiate_arg = function - | Ast.IdentArg (n, name) -> - let t = - try List.assoc name env - with Not_found -> prerr_endline ("name not found in env: "^name); - assert false - in - let rec count_lambda = function - | Ast.AttributedTerm (_, t) -> count_lambda t - | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body - | _ -> 0 - in - let rec add_lambda t n = - if n > 0 then - let name = NotationUtil.fresh_name () in - Ast.Binder (`Lambda, (Ast.Ident (name, None), None), - Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)]) - else - t - in - add_lambda t (n - count_lambda t) - in - let head = - let symbol = Ast.Symbol (symbol, 0) in - add_idrefs idrefs symbol - in - if args = [] then head - else Ast.Appl (head :: List.map instantiate_arg args) - -let fresh_id status = - let counter = status#interp_db.counter+1 in - status#set_interp_db ({ status#interp_db with counter = counter }), counter - -let add_interpretation (status : #status) dsc (symbol, args) appl_pattern = - let status,id = fresh_id status in - let ids = - try - id::StringMap.find symbol status#interp_db.interpretations - with Not_found -> [id] in - let status = - status#set_interp_db { status#interp_db with - level2_patterns32 = - IntMap.add id (dsc, symbol, args, appl_pattern) - status#interp_db.level2_patterns32; - pattern32_matrix = (true,appl_pattern,id)::status#interp_db.pattern32_matrix; - interpretations = StringMap.add symbol ids status#interp_db.interpretations - } - in - !load_patterns32 status#interp_db.pattern32_matrix; - status - -let toggle_active_interpretations status b = - status#set_interp_db { status#interp_db with - pattern32_matrix = - List.map (fun (_,ap,id) -> b,ap,id) status#interp_db.pattern32_matrix } - -exception Interpretation_not_found - -let lookup_interpretations status ?(sorted=true) symbol = - try - let raw = - List.map ( - fun id -> - let (dsc, _, args, appl_pattern) = - try IntMap.find id status#interp_db.level2_patterns32 - with Not_found -> assert false - in - dsc, args, appl_pattern - ) (StringMap.find symbol status#interp_db.interpretations) - in - if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw) - else raw - with Not_found -> raise Interpretation_not_found - -let instantiate_appl_pattern - ~mk_appl ~mk_implicit ~term_of_nref env appl_pattern -= - let lookup name = - try List.assoc name env - with Not_found -> - prerr_endline (sprintf "Name %s not found" name); - assert false - in - let rec aux = function - | Ast.NRefPattern nref -> term_of_nref nref - | Ast.ImplicitPattern -> mk_implicit false - | Ast.VarPattern name -> lookup name - | Ast.ApplPattern terms -> mk_appl (List.map aux terms) - in - aux appl_pattern diff --git a/matita/components/content/interpretations.mli b/matita/components/content/interpretations.mli deleted file mode 100644 index 8ee3fc01f..000000000 --- a/matita/components/content/interpretations.mli +++ /dev/null @@ -1,82 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - - - (** {2 State handling} *) - -type db - -class type g_status = - object - method interp_db: db - end - -class status : - object ('self) - method interp_db: db - method set_interp_db: db -> 'self - method set_interp_status: #g_status -> 'self - end - -type cic_id = string - -val add_interpretation: - #status as 'status -> - string -> (* id / description *) - string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *) - NotationPt.cic_appl_pattern -> (* level 3 pattern *) - 'status - -val set_load_patterns32: - ((bool * NotationPt.cic_appl_pattern * int) list -> unit) -> unit - -exception Interpretation_not_found - - (** @raise Interpretation_not_found *) -val lookup_interpretations: - #status -> - ?sorted:bool -> string -> (* symbol *) - (string * NotationPt.argument_pattern list * - NotationPt.cic_appl_pattern) list - - (** {3 Interpretations toggling} *) - -val toggle_active_interpretations: #status as 'status -> bool -> 'status - - (** {2 content -> cic} *) - - (** @param env environment from argument_pattern to cic terms - * @param pat cic_appl_pattern *) -val instantiate_appl_pattern: - mk_appl:('term list -> 'term) -> - mk_implicit:(bool -> 'term) -> - term_of_nref : (NReference.reference -> 'term) -> - (string * 'term) list -> NotationPt.cic_appl_pattern -> - 'term - -val find_level2_patterns32: - #status -> int -> - string * string * NotationPt.argument_pattern list * - NotationPt.cic_appl_pattern diff --git a/matita/components/content_pres/content2pres.mli b/matita/components/content_pres/content2pres.mli index 1c5b410b2..87843815f 100644 --- a/matita/components/content_pres/content2pres.mli +++ b/matita/components/content_pres/content2pres.mli @@ -35,6 +35,6 @@ val ncontent2pres: #TermContentPres.status -> ?skip_initial_lambdas:int -> ?skip_thm_and_qed:bool -> - ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t -> + ids_to_nrefs:(Interpretations.id, NReference.reference) Hashtbl.t -> NotationPt.term Content.cobj -> CicNotationPres.boxml_markup diff --git a/matita/components/content_pres/sequent2pres.mli b/matita/components/content_pres/sequent2pres.mli index cc3f27457..ae1051490 100644 --- a/matita/components/content_pres/sequent2pres.mli +++ b/matita/components/content_pres/sequent2pres.mli @@ -34,6 +34,6 @@ val nsequent2pres : #TermContentPres.status -> - ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t -> + ids_to_nrefs:(Interpretations.id, NReference.reference) Hashtbl.t -> subst:NCic.substitution -> NotationPt.term Content.conjecture -> CicNotationPres.boxml_markup diff --git a/matita/components/ng_cic_content/.depend b/matita/components/ng_cic_content/.depend index 1316c8eab..dd8940e5a 100644 --- a/matita/components/ng_cic_content/.depend +++ b/matita/components/ng_cic_content/.depend @@ -1,6 +1,8 @@ ncic2astMatcher.cmi: -nTermCicContent.cmi: +interpretations.cmi: ncic2astMatcher.cmo: ncic2astMatcher.cmi ncic2astMatcher.cmx: ncic2astMatcher.cmi -nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi -nTermCicContent.cmx: ncic2astMatcher.cmx nTermCicContent.cmi +interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi \ + interpretations.cmi +interpretations.cmx: ncic2astMatcher.cmx interpretations.cmx \ + interpretations.cmi diff --git a/matita/components/ng_cic_content/Makefile b/matita/components/ng_cic_content/Makefile index c501a09e1..ac40a66f1 100644 --- a/matita/components/ng_cic_content/Makefile +++ b/matita/components/ng_cic_content/Makefile @@ -2,7 +2,7 @@ PACKAGE = ng_cic_content INTERFACE_FILES = \ ncic2astMatcher.mli \ - nTermCicContent.mli + interpretations.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml new file mode 100644 index 000000000..7e175193b --- /dev/null +++ b/matita/components/ng_cic_content/interpretations.ml @@ -0,0 +1,587 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id$ *) + +open Printf + +module Ast = NotationPt + + +let debug = false +let debug_print s = if debug then prerr_endline (Lazy.force s) else () + +type id = string +let hide_coercions = ref true;; + +type cic_id = string + +type term_info = + { sort: (cic_id, Ast.sort_kind) Hashtbl.t; + uri: (cic_id, NReference.reference) Hashtbl.t; + } + +module IntMap = Map.Make(struct type t = int let compare = compare end);; +module StringMap = Map.Make(String);; + +type db = { + counter: int; + pattern32_matrix: (bool * NotationPt.cic_appl_pattern * int) list; + level2_patterns32: + (string * string * NotationPt.argument_pattern list * + NotationPt.cic_appl_pattern) IntMap.t; + interpretations: int list StringMap.t; (* symb -> id list *) + compiled32: + (NCic.term -> ((string * NCic.term) list * NCic.term list * int) option) + Lazy.t +} + +let initial_db = { + counter = -1; + pattern32_matrix = []; + level2_patterns32 = IntMap.empty; + interpretations = StringMap.empty; + compiled32 = lazy (fun _ -> assert false) +} + +class type g_status = + object + inherit NCicCoercion.g_status + method interp_db: db + end + +class status = + object + inherit NCicCoercion.status + val interp_db = initial_db + method interp_db = interp_db + method set_interp_db v = {< interp_db = v >} + method set_interp_status + : 'status. #g_status as 'status -> 'self + = fun o -> {< interp_db = o#interp_db >}#set_coercion_status o + end + +let idref register_ref = + let id = ref 0 in + fun ?reference t -> + incr id; + let id = "i" ^ string_of_int !id in + (match reference with None -> () | Some r -> register_ref id r); + Ast.AttributedTerm (`IdRef id, t) +;; + +let level_of_uri u = + let name = NUri.name_of_uri u in + assert(String.length name > String.length "Type"); + String.sub name 4 (String.length name - 4) +;; + +let find_level2_patterns32 status pid = + IntMap.find pid status#interp_db.level2_patterns32 + +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 + | Ast.IdentArg (n, name) -> + let t = + try List.assoc name env + with Not_found -> prerr_endline ("name not found in env: "^name); + assert false + in + let rec count_lambda = function + | Ast.AttributedTerm (_, t) -> count_lambda t + | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body + | _ -> 0 + in + let rec add_lambda t n = + if n > 0 then + let name = NotationUtil.fresh_name () in + Ast.Binder (`Lambda, (Ast.Ident (name, None), None), + Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)]) + else + t + in + add_lambda t (n - count_lambda t) + in + let head = + let symbol = Ast.Symbol (symbol, 0) in + add_idrefs idrefs symbol + in + if args = [] then head + else Ast.Appl (head :: List.map instantiate_arg args) + +let fresh_id status = + let counter = status#interp_db.counter+1 in + status#set_interp_db ({ status#interp_db with counter = counter }), counter + +let load_patterns32 status t = + let t = + HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t + in + status#set_interp_db + {status#interp_db with + compiled32 = lazy (Ncic2astMatcher.Matcher32.compiler t) } +;; + +let add_interpretation status dsc (symbol, args) appl_pattern = + let status,id = fresh_id status in + let ids = + try + id::StringMap.find symbol status#interp_db.interpretations + with Not_found -> [id] in + let status = + status#set_interp_db { status#interp_db with + level2_patterns32 = + IntMap.add id (dsc, symbol, args, appl_pattern) + status#interp_db.level2_patterns32; + pattern32_matrix = (true,appl_pattern,id)::status#interp_db.pattern32_matrix; + interpretations = StringMap.add symbol ids status#interp_db.interpretations + } + in + load_patterns32 status status#interp_db.pattern32_matrix + +let toggle_active_interpretations status b = + status#set_interp_db { status#interp_db with + pattern32_matrix = + List.map (fun (_,ap,id) -> b,ap,id) status#interp_db.pattern32_matrix } + +exception Interpretation_not_found + +let lookup_interpretations status ?(sorted=true) symbol = + try + let raw = + List.map ( + fun id -> + let (dsc, _, args, appl_pattern) = + try IntMap.find id status#interp_db.level2_patterns32 + with Not_found -> assert false + in + dsc, args, appl_pattern + ) (StringMap.find symbol status#interp_db.interpretations) + in + if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw) + else raw + with Not_found -> raise Interpretation_not_found + +let instantiate_appl_pattern + ~mk_appl ~mk_implicit ~term_of_nref env appl_pattern += + let lookup name = + try List.assoc name env + with Not_found -> + prerr_endline (sprintf "Name %s not found" name); + assert false + in + let rec aux = function + | Ast.NRefPattern nref -> term_of_nref nref + | Ast.ImplicitPattern -> mk_implicit false + | Ast.VarPattern name -> lookup name + | Ast.ApplPattern terms -> mk_appl (List.map aux terms) + in + aux appl_pattern + +let destroy_nat = + let is_nat_URI = NUri.eq (NUri.uri_of_string + "cic:/matita/ng/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 + | _ -> false + in + let is_succ = function + | NCic.Const (NReference.Ref (uri, NReference.Con (0, 2, 0))) when + is_nat_URI uri -> true + | _ -> false + in + let rec aux acc = function + | NCic.Appl [he ; tl] when is_succ he -> aux (acc + 1) tl + | t when is_zero t -> Some acc + | _ -> None + in + aux 0 + +(* CODICE c&p da NCicPp *) +let nast_of_cic0 status + ~(idref: + ?reference:NReference.reference -> NotationPt.term -> NotationPt.term) + ~output_type ~metasenv ~subst k ~context = + function + | NCic.Rel n -> + (try + let name,_ = List.nth context (n-1) in + let name = if name = "_" then "__"^string_of_int n else name in + 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.Meta (n,lc) when List.mem_assoc n subst -> + let _,_,t,_ = List.assoc n subst in + k ~context (NCicSubstitution.subst_meta 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)) + | NCic.Sort NCic.Prop -> idref (Ast.Sort `Prop) + | NCic.Sort NCic.Type [] -> idref (Ast.Sort `Set) + | NCic.Sort NCic.Type ((`Type,u)::_) -> + idref(Ast.Sort (`NType (level_of_uri u))) + | NCic.Sort NCic.Type ((`CProp,u)::_) -> + idref(Ast.Sort (`NCProp (level_of_uri u))) + | NCic.Sort NCic.Type ((`Succ,u)::_) -> + idref(Ast.Sort (`NType (level_of_uri u ^ "+1"))) + | NCic.Implicit `Hole -> idref (Ast.UserInput) + | NCic.Implicit `Vector -> idref (Ast.Implicit `Vector) + | NCic.Implicit _ -> idref (Ast.Implicit `JustOne) + | NCic.Prod (n,s,t) -> + let n = if n.[0] = '_' then "_" else n in + let binder_kind = `Forall in + idref (Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ~context s)), + k ~context:((n,NCic.Decl s)::context) t)) + | 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) -> + 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 + k ~context + (NCicReduction.head_beta_reduce ~upto:(List.length args) + (match hd with + | NCic.Appl l -> NCic.Appl (l@args) + | _ -> NCic.Appl (hd :: args))) + | NCic.Appl args as t -> + (match destroy_nat t with + | Some n -> idref (Ast.Num (string_of_int n, -1)) + | None -> + let args = + if not !hide_coercions then args + else + match + NCicCoercion.match_coercion status ~metasenv ~context ~subst t + with + | None -> args + | Some (_,sats,cpos) -> +(* CSC: sats e' il numero di pi, ma non so cosa farmene! voglio il numero di + argomenti da saltare, come prima! *) + if cpos < List.length args - 1 then + List.nth args (cpos + 1) :: + try snd (HExtlib.split_nth (cpos+sats+2) args) + with Failure _->[] + else + args + in + (match args with + [arg] -> idref (k ~context arg) + | _ -> idref (Ast.Appl (List.map (k ~context) args)))) + | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) -> + let name = NUri.name_of_uri uri in +(* CSC + let uri_str = UriManager.string_of_uri uri in + let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in + let ctor_puri j = + UriManager.uri_of_string + (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j) + in +*) + 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 _,_,_,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 -> + 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 + (Ast.Ident (name,None), Some (k ~context:ctx s)) :: cv, rhs + | _, _ -> [], k ~context:ctx pat + in + let j = ref 0 in + let patterns = + try + List.map2 + (fun (_, name, ty) pat -> + incr j; + let name,(capture_variables,rhs) = + match output_type with + `Term -> name, eat_branch leftno context ty pat + | `Pattern -> "_", ([], k ~context pat) + in + Ast.Pattern (name, None(*CSC Some (ctor_puri !j)*), capture_variables), rhs + ) constructors patterns + with Invalid_argument _ -> assert false + in + let indty = + match output_type with + `Pattern -> None + | `Term -> Some case_indty + in + idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns)) +;; + +let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = + match Lazy.force status#interp_db.compiled32 term with + | None -> + nast_of_cic0 status ~idref ~output_type ~metasenv ~subst + (nast_of_cic1 status ~idref ~output_type ~metasenv ~subst) ~context term + | Some (env, ctors, pid) -> + let idrefs = + List.map + (fun term -> + let attrterm = + idref + ~reference: + (match term with NCic.Const nref -> nref | _ -> assert false) + (NotationPt.Ident ("dummy",None)) + in + match attrterm with + Ast.AttributedTerm (`IdRef id, _) -> id + | _ -> assert false + ) ctors + in + let env = + List.map + (fun (name, term) -> + name, + nast_of_cic1 status ~idref ~output_type ~subst ~metasenv ~context + term + ) env + in + let _, symbol, args, _ = + try + find_level2_patterns32 status pid + with Not_found -> assert false + in + let ast = instantiate32 idrefs env symbol args in + idref ast (*Ast.AttributedTerm (`IdRef (idref term), ast)*) +;; + +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 + let context',_ = + List.fold_right + (fun item (res,context) -> + match item with + | name,NCic.Decl t -> + Some + (* We should call build_decl_item, but we have not computed *) + (* the inner-types ==> we always produce a declaration *) + (`Declaration + { K.dec_name = (Some name); + K.dec_id = "-1"; + K.dec_inductive = false; + K.dec_aref = "-1"; + K.dec_type = nast_of_cic ~context t + })::res,item::context + | name,NCic.Def (t,ty) -> + Some + (* We should call build_def_item, but we have not computed *) + (* the inner-types ==> we always produce a declaration *) + (`Definition + { K.def_name = (Some name); + K.def_id = "-1"; + K.def_aref = "-1"; + 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) +;; + +let nmap_sequent status ~metasenv ~subst conjecture = + 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 object_prefix = "obj:";; +let declaration_prefix = "decl:";; +let definition_prefix = "def:";; +let inductive_prefix = "ind:";; +let joint_prefix = "joint:";; + +let get_id = + function + Ast.AttributedTerm (`IdRef id, _) -> id + | _ -> assert false +;; + +let gen_id prefix seed = + let res = prefix ^ string_of_int !seed in + incr seed ; + res +;; + +let build_def_item seed context metasenv id n t ty = + let module K = Content in +(* + try + let sort = Hashtbl.find ids_to_inner_sorts id in + if sort = `Prop then + (let p = + (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) + in + `Proof p;) + else +*) + `Definition + { K.def_name = Some n; + K.def_id = gen_id definition_prefix seed; + K.def_aref = id; + K.def_term = t; + K.def_type = ty + } +(* + with + Not_found -> assert false +*) + +let build_decl_item seed id n s = + let module K = Content in +(* + let sort = + try + Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)) + with Not_found -> None + in + match sort with + | Some `Prop -> + `Hypothesis + { K.dec_name = name_of n; + K.dec_id = gen_id declaration_prefix seed; + K.dec_inductive = false; + K.dec_aref = id; + K.dec_type = s + } + | _ -> +*) + `Declaration + { K.dec_name = Some n; + K.dec_id = gen_id declaration_prefix seed; + K.dec_inductive = false; + K.dec_aref = id; + K.dec_type = s + } +;; + +let nmap_obj status (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 + let conjectures = + match metasenv with + [] -> None + | _ -> (*Some (List.map (map_conjectures seed) metasenv)*) + (*CSC: used to be the previous line, that uses seed *) + Some (List.map (nmap_sequent0 status ~idref ~metasenv ~subst) metasenv) + in +let build_constructors seed l = + List.map + (fun (_,n,ty) -> + let ty = nast_of_cic ~context:[] ty in + { K.dec_name = Some n; + K.dec_id = gen_id declaration_prefix seed; + K.dec_inductive = false; + K.dec_aref = ""; + K.dec_type = ty + }) l +in +let build_inductive b seed = + fun (_,n,ty,cl) -> + let ty = nast_of_cic ~context:[] ty in + `Inductive + { K.inductive_id = gen_id inductive_prefix seed; + K.inductive_name = n; + K.inductive_kind = b; + K.inductive_type = ty; + K.inductive_constructors = build_constructors seed cl + } +in +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 + `Definition + { K.def_id = gen_id inductive_prefix seed; + K.def_name = Some n; + K.def_aref = ""; + K.def_type = ty; + 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 +;; diff --git a/matita/components/ng_cic_content/interpretations.mli b/matita/components/ng_cic_content/interpretations.mli new file mode 100644 index 000000000..a4a3fb9c0 --- /dev/null +++ b/matita/components/ng_cic_content/interpretations.mli @@ -0,0 +1,91 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + + + (** {2 State handling} *) + +type id = string + +val hide_coercions: bool ref + +type db + +class type g_status = + object + inherit NCicCoercion.g_status + method interp_db: db + end + +class status : + object ('self) + inherit NCicCoercion.status + method interp_db: db + method set_interp_db: db -> 'self + method set_interp_status: #g_status -> 'self + end + +type cic_id = string + +val add_interpretation: + #status as 'status -> + string -> (* id / description *) + string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *) + NotationPt.cic_appl_pattern -> (* level 3 pattern *) + 'status + +exception Interpretation_not_found + + (** @raise Interpretation_not_found *) +val lookup_interpretations: + #status -> + ?sorted:bool -> string -> (* symbol *) + (string * NotationPt.argument_pattern list * + NotationPt.cic_appl_pattern) list + + (** {3 Interpretations toggling} *) + +val toggle_active_interpretations: #status as 'status -> bool -> 'status + + (** {2 content -> cic} *) + + (** @param env environment from argument_pattern to cic terms + * @param pat cic_appl_pattern *) +val instantiate_appl_pattern: + mk_appl:('term list -> 'term) -> + mk_implicit:(bool -> 'term) -> + term_of_nref : (NReference.reference -> 'term) -> + (string * 'term) list -> NotationPt.cic_appl_pattern -> + 'term + +val nmap_sequent: + #status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> + int * NCic.conjecture -> + NotationPt.term Content.conjecture * + (id, NReference.reference) Hashtbl.t (* id -> reference *) + +val nmap_obj: + #status -> NCic.obj -> + NotationPt.term Content.cobj * + (id, NReference.reference) Hashtbl.t (* id -> reference *) diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/nTermCicContent.ml deleted file mode 100644 index 61ff07689..000000000 --- a/matita/components/ng_cic_content/nTermCicContent.ml +++ /dev/null @@ -1,491 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id: termAcicContent.ml 9304 2008-12-05 23:12:39Z sacerdot $ *) - -open Printf - -module Ast = NotationPt - -let debug = false -let debug_print s = if debug then prerr_endline (Lazy.force s) else () - -type id = string - -let hide_coercions = ref true;; - -class status = - object - inherit NCicCoercion.status - inherit Interpretations.status - end - -let idref register_ref = - let id = ref 0 in - fun ?reference t -> - incr id; - let id = "i" ^ string_of_int !id in - (match reference with None -> () | Some r -> register_ref id r); - Ast.AttributedTerm (`IdRef id, t) -;; - -let level_of_uri u = - let name = NUri.name_of_uri u in - assert(String.length name > String.length "Type"); - String.sub name 4 (String.length name - 4) -;; - -let destroy_nat = - let is_nat_URI = NUri.eq (NUri.uri_of_string - "cic:/matita/ng/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 - | _ -> false - in - let is_succ = function - | NCic.Const (NReference.Ref (uri, NReference.Con (0, 2, 0))) when - is_nat_URI uri -> true - | _ -> false - in - let rec aux acc = function - | NCic.Appl [he ; tl] when is_succ he -> aux (acc + 1) tl - | t when is_zero t -> Some acc - | _ -> None - in - aux 0 - -(* CODICE c&p da NCicPp *) -let nast_of_cic0 status - ~(idref: - ?reference:NReference.reference -> NotationPt.term -> NotationPt.term) - ~output_type ~metasenv ~subst k ~context = - function - | NCic.Rel n -> - (try - let name,_ = List.nth context (n-1) in - let name = if name = "_" then "__"^string_of_int n else name in - 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.Meta (n,lc) when List.mem_assoc n subst -> - let _,_,t,_ = List.assoc n subst in - k ~context (NCicSubstitution.subst_meta 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)) - | NCic.Sort NCic.Prop -> idref (Ast.Sort `Prop) - | NCic.Sort NCic.Type [] -> idref (Ast.Sort `Set) - | NCic.Sort NCic.Type ((`Type,u)::_) -> - idref(Ast.Sort (`NType (level_of_uri u))) - | NCic.Sort NCic.Type ((`CProp,u)::_) -> - idref(Ast.Sort (`NCProp (level_of_uri u))) - | NCic.Sort NCic.Type ((`Succ,u)::_) -> - idref(Ast.Sort (`NType (level_of_uri u ^ "+1"))) - | NCic.Implicit `Hole -> idref (Ast.UserInput) - | NCic.Implicit `Vector -> idref (Ast.Implicit `Vector) - | NCic.Implicit _ -> idref (Ast.Implicit `JustOne) - | NCic.Prod (n,s,t) -> - let n = if n.[0] = '_' then "_" else n in - let binder_kind = `Forall in - idref (Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ~context s)), - k ~context:((n,NCic.Decl s)::context) t)) - | 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) -> - 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 - k ~context - (NCicReduction.head_beta_reduce ~upto:(List.length args) - (match hd with - | NCic.Appl l -> NCic.Appl (l@args) - | _ -> NCic.Appl (hd :: args))) - | NCic.Appl args as t -> - (match destroy_nat t with - | Some n -> idref (Ast.Num (string_of_int n, -1)) - | None -> - let args = - if not !hide_coercions then args - else - match - NCicCoercion.match_coercion status ~metasenv ~context ~subst t - with - | None -> args - | Some (_,sats,cpos) -> -(* CSC: sats e' il numero di pi, ma non so cosa farmene! voglio il numero di - argomenti da saltare, come prima! *) - if cpos < List.length args - 1 then - List.nth args (cpos + 1) :: - try snd (HExtlib.split_nth (cpos+sats+2) args) - with Failure _->[] - else - args - in - (match args with - [arg] -> idref (k ~context arg) - | _ -> idref (Ast.Appl (List.map (k ~context) args)))) - | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) -> - let name = NUri.name_of_uri uri in -(* CSC - let uri_str = UriManager.string_of_uri uri in - let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in - let ctor_puri j = - UriManager.uri_of_string - (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j) - in -*) - 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 _,_,_,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 -> - 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 - (Ast.Ident (name,None), Some (k ~context:ctx s)) :: cv, rhs - | _, _ -> [], k ~context:ctx pat - in - let j = ref 0 in - let patterns = - try - List.map2 - (fun (_, name, ty) pat -> - incr j; - let name,(capture_variables,rhs) = - match output_type with - `Term -> name, eat_branch leftno context ty pat - | `Pattern -> "_", ([], k ~context pat) - in - Ast.Pattern (name, None(*CSC Some (ctor_puri !j)*), capture_variables), rhs - ) constructors patterns - with Invalid_argument _ -> assert false - in - let indty = - match output_type with - `Pattern -> None - | `Term -> Some case_indty - in - idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns)) -;; - -let compiled32 = ref None - -let get_compiled32 () = - match !compiled32 with - | None -> assert false - | Some f -> Lazy.force f - -let set_compiled32 f = compiled32 := Some f - -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 - | Ast.IdentArg (n, name) -> - let t = - try List.assoc name env - with Not_found -> prerr_endline ("name not found in env: "^name); - assert false - in - let rec count_lambda = function - | Ast.AttributedTerm (_, t) -> count_lambda t - | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body - | _ -> 0 - in - let rec add_lambda t n = - if n > 0 then - let name = NotationUtil.fresh_name () in - Ast.Binder (`Lambda, (Ast.Ident (name, None), None), - Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)]) - else - t - in - add_lambda t (n - count_lambda t) - in - let head = - let symbol = Ast.Symbol (symbol, 0) in - add_idrefs idrefs symbol - in - if args = [] then head - else Ast.Appl (head :: List.map instantiate_arg args) - -let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = - match (get_compiled32 ()) term with - | None -> - nast_of_cic0 status ~idref ~output_type ~metasenv ~subst - (nast_of_cic1 status ~idref ~output_type ~metasenv ~subst) ~context term - | Some (env, ctors, pid) -> - let idrefs = - List.map - (fun term -> - let attrterm = - idref - ~reference: - (match term with NCic.Const nref -> nref | _ -> assert false) - (NotationPt.Ident ("dummy",None)) - in - match attrterm with - Ast.AttributedTerm (`IdRef id, _) -> id - | _ -> assert false - ) ctors - in - let env = - List.map - (fun (name, term) -> - name, - nast_of_cic1 status ~idref ~output_type ~subst ~metasenv ~context - term - ) env - in - let _, symbol, args, _ = - try - Interpretations.find_level2_patterns32 status pid - with Not_found -> assert false - in - let ast = instantiate32 idrefs env symbol args in - idref ast (*Ast.AttributedTerm (`IdRef (idref term), ast)*) -;; - -let load_patterns32 t = - let t = - HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t - in - set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t)) -;; - -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 - let context',_ = - List.fold_right - (fun item (res,context) -> - match item with - | name,NCic.Decl t -> - Some - (* We should call build_decl_item, but we have not computed *) - (* the inner-types ==> we always produce a declaration *) - (`Declaration - { K.dec_name = (Some name); - K.dec_id = "-1"; - K.dec_inductive = false; - K.dec_aref = "-1"; - K.dec_type = nast_of_cic ~context t - })::res,item::context - | name,NCic.Def (t,ty) -> - Some - (* We should call build_def_item, but we have not computed *) - (* the inner-types ==> we always produce a declaration *) - (`Definition - { K.def_name = (Some name); - K.def_id = "-1"; - K.def_aref = "-1"; - 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) -;; - -let nmap_sequent status ~metasenv ~subst conjecture = - 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 object_prefix = "obj:";; -let declaration_prefix = "decl:";; -let definition_prefix = "def:";; -let inductive_prefix = "ind:";; -let joint_prefix = "joint:";; - -let get_id = - function - Ast.AttributedTerm (`IdRef id, _) -> id - | _ -> assert false -;; - -let gen_id prefix seed = - let res = prefix ^ string_of_int !seed in - incr seed ; - res -;; - -let build_def_item seed context metasenv id n t ty = - let module K = Content in -(* - try - let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = `Prop then - (let p = - (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) - in - `Proof p;) - else -*) - `Definition - { K.def_name = Some n; - K.def_id = gen_id definition_prefix seed; - K.def_aref = id; - K.def_term = t; - K.def_type = ty - } -(* - with - Not_found -> assert false -*) - -let build_decl_item seed id n s = - let module K = Content in -(* - let sort = - try - Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)) - with Not_found -> None - in - match sort with - | Some `Prop -> - `Hypothesis - { K.dec_name = name_of n; - K.dec_id = gen_id declaration_prefix seed; - K.dec_inductive = false; - K.dec_aref = id; - K.dec_type = s - } - | _ -> -*) - `Declaration - { K.dec_name = Some n; - K.dec_id = gen_id declaration_prefix seed; - K.dec_inductive = false; - K.dec_aref = id; - K.dec_type = s - } -;; - -let nmap_obj status (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 - let conjectures = - match metasenv with - [] -> None - | _ -> (*Some (List.map (map_conjectures seed) metasenv)*) - (*CSC: used to be the previous line, that uses seed *) - Some (List.map (nmap_sequent0 status ~idref ~metasenv ~subst) metasenv) - in -let build_constructors seed l = - List.map - (fun (_,n,ty) -> - let ty = nast_of_cic ~context:[] ty in - { K.dec_name = Some n; - K.dec_id = gen_id declaration_prefix seed; - K.dec_inductive = false; - K.dec_aref = ""; - K.dec_type = ty - }) l -in -let build_inductive b seed = - fun (_,n,ty,cl) -> - let ty = nast_of_cic ~context:[] ty in - `Inductive - { K.inductive_id = gen_id inductive_prefix seed; - K.inductive_name = n; - K.inductive_kind = b; - K.inductive_type = ty; - K.inductive_constructors = build_constructors seed cl - } -in -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 - `Definition - { K.def_id = gen_id inductive_prefix seed; - K.def_name = Some n; - K.def_aref = ""; - K.def_type = ty; - 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 -;; - -Interpretations.set_load_patterns32 load_patterns32 diff --git a/matita/components/ng_cic_content/nTermCicContent.mli b/matita/components/ng_cic_content/nTermCicContent.mli deleted file mode 100644 index 4a13a8956..000000000 --- a/matita/components/ng_cic_content/nTermCicContent.mli +++ /dev/null @@ -1,45 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -type id = string - -val hide_coercions: bool ref - -class status : - object ('self) - inherit NCicCoercion.status - inherit Interpretations.status - end - -val nmap_sequent: - #status as 'a -> metasenv:NCic.metasenv -> subst:NCic.substitution -> - int * NCic.conjecture -> - NotationPt.term Content.conjecture * - (id, NReference.reference) Hashtbl.t (* id -> reference *) - -val nmap_obj: - #status -> NCic.obj -> - NotationPt.term Content.cobj * - (id, NReference.reference) Hashtbl.t (* id -> reference *) diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt index e2be9b49b..104a90938 100644 --- a/matita/components/statuses.txt +++ b/matita/components/statuses.txt @@ -7,8 +7,10 @@ grafitetypes -> tac -> auto + eq + (grafitedisambiguate = lexicon+nciccoercion) |-> notation_parser -ntermciccontent = nciccoercion+interpretation - | - unif_hint - -applytransformation = ntermciccontent+termcontentpres +applytransformation + | + |-> ntermciccontent = nciccoercion+interpretation + | | + | unif_hint + | + |-> termcontentpres diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml index 8e09d9db4..442a7eb3c 100644 --- a/matita/matita/applyTransformation.ml +++ b/matita/matita/applyTransformation.ml @@ -37,7 +37,7 @@ class status = object - inherit NTermCicContent.status + inherit Interpretations.status inherit TermContentPres.status end @@ -47,7 +47,7 @@ let mpres_document pres_box = let ntxt_of_cic_sequent ~map_unicode_to_tex size status metasenv subst sequent = let content_sequent,ids_to_refs = - NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in + Interpretations.nmap_sequent status ~metasenv ~subst sequent in let pres_sequent = Sequent2pres.nsequent2pres status ids_to_refs subst content_sequent in let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in @@ -55,7 +55,7 @@ let ntxt_of_cic_sequent ~map_unicode_to_tex size status metasenv subst sequent = (function x::_ -> x | _ -> assert false) size pres_sequent let ntxt_of_cic_object ~map_unicode_to_tex size status obj = - let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in + let cobj,ids_to_nrefs = Interpretations.nmap_obj status obj in let pres_sequent = Content2pres.ncontent2pres status ~ids_to_nrefs cobj in let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in BoxPp.render_to_string ~map_unicode_to_tex diff --git a/matita/matita/applyTransformation.mli b/matita/matita/applyTransformation.mli index 6d3e40810..4b95e5370 100644 --- a/matita/matita/applyTransformation.mli +++ b/matita/matita/applyTransformation.mli @@ -35,13 +35,12 @@ class status : object ('self) - inherit NTermCicContent.status + inherit Interpretations.status inherit TermContentPres.status end val ntxt_of_cic_sequent: - map_unicode_to_tex:bool -> int -> - #status -> + map_unicode_to_tex:bool -> int -> #status -> NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *) int * NCic.conjecture -> (* sequent *) string (* text *) diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index a42500bd6..d963cf6a2 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -859,7 +859,7 @@ class gui () = s#set_grafite_status status*) ); MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem - ~callback:(fun enabled -> NTermCicContent.hide_coercions := enabled); + ~callback:(fun enabled -> Interpretations.hide_coercions := enabled); MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem ~callback:(fun enabled -> Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);