From 5149063488e3771fb55c198e0ecef5fb5aaaab67 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 27 May 2009 08:49:30 +0000 Subject: [PATCH] Basic support for interpretations for NG: 1) only interpretations for old objects are used (i.e. no way yet to declare a new interpretation on a new object) 2) only interpretations for constants (no inductive definitions/constructors) since we have no faithful embedding of new references into old URIs 3) no support for backtracking (I think) --- .../acic_content/termAcicContent.ml | 21 ++- .../acic_content/termAcicContent.mli | 10 ++ .../components/ng_cic_content/.depend | 8 +- .../components/ng_cic_content/.depend.opt | 8 +- .../components/ng_cic_content/Makefile | 1 + .../ng_cic_content/nTermCicContent.ml | 161 ++++++++++-------- .../ng_cic_content/ncic2astMatcher.ml | 109 ++++++++++++ .../ng_cic_content/ncic2astMatcher.mli | 34 ++++ 8 files changed, 267 insertions(+), 85 deletions(-) create mode 100644 helm/software/components/ng_cic_content/ncic2astMatcher.ml create mode 100644 helm/software/components/ng_cic_content/ncic2astMatcher.mli diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index c02c5892d..9176a8b56 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -306,6 +306,7 @@ let interpretations = ref (initial_interpretations ()) let compiled32 = ref None let pattern32_matrix = ref [] let counter = ref ~-1 +let find_level2_patterns32 pid = Hashtbl.find !level2_patterns32 pid;; let stack = ref [] @@ -394,17 +395,23 @@ let rec ast_of_acic1 ~output_type term_info annterm = in let _, symbol, args, _ = try - Hashtbl.find !level2_patterns32 pid + find_level2_patterns32 pid with Not_found -> assert false in let ast = instantiate32 term_info idrefs env' symbol args in Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), ast) -let load_patterns32 t = +let load_patterns32s = + let load_patterns32 t = let t = HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t in - set_compiled32 (lazy (Acic2astMatcher.Matcher32.compiler t)) + set_compiled32 (lazy (Acic2astMatcher.Matcher32.compiler t)) + in + ref [load_patterns32] +;; + +let add_load_patterns32 f = load_patterns32s := f :: !load_patterns32s;; let ast_of_acic ~output_type id_to_sort annterm = debug_print (lazy ("ast_of_acic <- " @@ -423,7 +430,7 @@ let add_interpretation dsc (symbol, args) appl_pattern = let id = fresh_id () in Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern); pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix; - load_patterns32 !pattern32_matrix; + List.iter (fun f -> f !pattern32_matrix) !load_patterns32s; (try let ids = Hashtbl.find !interpretations symbol in ids := id :: !ids @@ -454,7 +461,7 @@ let set_active_interpretations ids = !pattern32_matrix in pattern32_matrix := pattern32_matrix'; - load_patterns32 !pattern32_matrix + List.iter (fun f -> f !pattern32_matrix) !load_patterns32s exception Interpretation_not_found @@ -485,9 +492,9 @@ let remove_interpretation id = with Not_found -> raise Interpretation_not_found); pattern32_matrix := List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix; - load_patterns32 !pattern32_matrix + List.iter (fun f -> f !pattern32_matrix) !load_patterns32s -let _ = load_patterns32 [] +let init () = List.iter (fun f -> f []) !load_patterns32s let instantiate_appl_pattern ~mk_appl ~mk_implicit ~term_of_uri env appl_pattern diff --git a/helm/software/components/acic_content/termAcicContent.mli b/helm/software/components/acic_content/termAcicContent.mli index 605a8f5ca..3ba6caefc 100644 --- a/helm/software/components/acic_content/termAcicContent.mli +++ b/helm/software/components/acic_content/termAcicContent.mli @@ -73,3 +73,13 @@ val instantiate_appl_pattern: val push: unit -> unit val pop: unit -> unit + +(* for Matita NG *) +val find_level2_patterns32: + int -> + string * string * + CicNotationPt.argument_pattern list * CicNotationPt.cic_appl_pattern + +val add_load_patterns32: + ((bool * CicNotationPt.cic_appl_pattern * int) list -> unit) -> unit +val init: unit -> unit diff --git a/helm/software/components/ng_cic_content/.depend b/helm/software/components/ng_cic_content/.depend index 23dc61522..1316c8eab 100644 --- a/helm/software/components/ng_cic_content/.depend +++ b/helm/software/components/ng_cic_content/.depend @@ -1,2 +1,6 @@ -nTermCicContent.cmo: nTermCicContent.cmi -nTermCicContent.cmx: nTermCicContent.cmi +ncic2astMatcher.cmi: +nTermCicContent.cmi: +ncic2astMatcher.cmo: ncic2astMatcher.cmi +ncic2astMatcher.cmx: ncic2astMatcher.cmi +nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi +nTermCicContent.cmx: ncic2astMatcher.cmx nTermCicContent.cmi diff --git a/helm/software/components/ng_cic_content/.depend.opt b/helm/software/components/ng_cic_content/.depend.opt index 23dc61522..1316c8eab 100644 --- a/helm/software/components/ng_cic_content/.depend.opt +++ b/helm/software/components/ng_cic_content/.depend.opt @@ -1,2 +1,6 @@ -nTermCicContent.cmo: nTermCicContent.cmi -nTermCicContent.cmx: nTermCicContent.cmi +ncic2astMatcher.cmi: +nTermCicContent.cmi: +ncic2astMatcher.cmo: ncic2astMatcher.cmi +ncic2astMatcher.cmx: ncic2astMatcher.cmi +nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi +nTermCicContent.cmx: ncic2astMatcher.cmx nTermCicContent.cmi diff --git a/helm/software/components/ng_cic_content/Makefile b/helm/software/components/ng_cic_content/Makefile index e899d62bd..c501a09e1 100644 --- a/helm/software/components/ng_cic_content/Makefile +++ b/helm/software/components/ng_cic_content/Makefile @@ -1,6 +1,7 @@ PACKAGE = ng_cic_content INTERFACE_FILES = \ + ncic2astMatcher.mli \ nTermCicContent.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index 95ce44b64..2022797a2 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -55,24 +55,24 @@ let idref () = ;; (* CODICE c&p da NCicPp *) -let nast_of_cic ~idref ~output_type ~subst ~context = - let rec k ctx = function +let nast_of_cic0 ~idref ~output_type ~subst k ~context = + function | NCic.Rel n -> (try - let name,_ = List.nth ctx (n-1) in + 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 ctx),None))) + idref (Ast.Ident ("-" ^ string_of_int (n - List.length context),None))) | NCic.Const r -> idref (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 ctx (NCicSubstitution.subst_meta lc t) + 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 ctx (NCicSubstitution.lift s x))) l)) + (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) (* CSC: | C.Sort (C.Type []) -> F.fprintf f "Type0" @@ -90,23 +90,23 @@ let nast_of_cic ~idref ~output_type ~subst ~context = | 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 ctx s)), - k ((n,NCic.Decl s)::ctx) t)) + 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 ctx s)), - k ((n,NCic.Decl s)::ctx) 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,t) -> - idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ctx ty)), k ctx s, - k ((n,NCic.Decl s)::ctx) t)) + idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context ty)), k ~context s, + 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 ctx + 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 -> idref (Ast.Appl (List.map (k ctx) args)) + | NCic.Appl args -> 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 @@ -130,8 +130,8 @@ let nast_of_cic ~idref ~output_type ~subst ~context = eat_branch (pred n) ((name,NCic.Decl s)::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 ctx s)) :: cv, rhs - | _, _ -> [], k ctx pat + (Ast.Ident (name,None), Some (k ~context s)) :: cv, rhs + | _, _ -> [], k ~context pat in let j = ref 0 in let patterns = @@ -141,8 +141,8 @@ let nast_of_cic ~idref ~output_type ~subst ~context = incr j; let name,(capture_variables,rhs) = match output_type with - `Term -> name, eat_branch leftno ctx ty pat - | `Pattern -> "_", ([], k ctx pat) + `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 @@ -153,55 +153,21 @@ let nast_of_cic ~idref ~output_type ~subst ~context = `Pattern -> None | `Term -> Some case_indty in - idref (Ast.Case (k ctx te, indty, Some (k ctx outty), patterns)) - in - k context + idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns)) ;; -let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) = - let module K = Content in - let nast_of_cic = nast_of_cic ~idref:(idref ()) ~output_type:`Term ~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 -;; - -(* (* persistent state *) +(* let initial_level2_patterns32 () = Hashtbl.create 211 let initial_interpretations () = Hashtbl.create 211 let level2_patterns32 = ref (initial_level2_patterns32 ()) (* symb -> id list ref *) let interpretations = ref (initial_interpretations ()) +*) let compiled32 = ref None +(* let pattern32_matrix = ref [] let counter = ref ~-1 @@ -227,6 +193,7 @@ let pop () = compiled32 := ocompiled32; pattern32_matrix := opattern32_matrix ;; +*) let get_compiled32 () = match !compiled32 with @@ -238,7 +205,7 @@ let set_compiled32 f = compiled32 := Some f let add_idrefs = List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) -let instantiate32 term_info idrefs env symbol args = +let instantiate32 idrefs env symbol args = let rec instantiate_arg = function | Ast.IdentArg (n, name) -> let t = @@ -268,42 +235,53 @@ 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 ~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 +let rec nast_of_cic1 ~idref ~output_type ~subst ~context term = +(* + let register_uri id uri = assert false in +*) + match (get_compiled32 ()) term with | None -> - ast_of_acic0 ~output_type term_info annterm (ast_of_acic1 ~output_type) + nast_of_cic0 ~idref ~output_type ~subst + (nast_of_cic1 ~idref ~output_type ~subst) ~context term | Some (env, ctors, pid) -> let idrefs = +(* List.map - (fun annterm -> - let idref = CicUtil.id_of_annterm annterm in + (fun term -> + let idref = idref term in (try register_uri idref - (CicUtil.uri_of_term (Deannotate.deannotate_term annterm)) + (CicUtil.uri_of_term (Deannotate.deannotate_term term)) with Invalid_argument _ -> ()); idref) ctors +*) [] in - let env' = + let env = List.map - (fun (name, term) -> name, ast_of_acic1 ~output_type term_info term) env + (fun (name, term) -> + name, nast_of_cic1 ~idref ~output_type ~subst ~context term) env in let _, symbol, args, _ = try - Hashtbl.find !level2_patterns32 pid + TermAcicContent.find_level2_patterns32 pid with Not_found -> assert false in - let ast = instantiate32 term_info idrefs env' symbol args in - Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), ast) + 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 (Acic2astMatcher.Matcher32.compiler t)) + let t = + HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t + in + set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t)) +in + TermAcicContent.add_load_patterns32 load_patterns32; + TermAcicContent.init () +;; +(* let ast_of_acic ~output_type id_to_sort annterm = debug_print (lazy ("ast_of_acic <- " ^ CicPp.ppterm (Deannotate.deannotate_term annterm))); @@ -401,3 +379,38 @@ let instantiate_appl_pattern in aux appl_pattern *) + +let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) = + let module K = Content in + let nast_of_cic = nast_of_cic1 ~idref:(idref ()) ~output_type:`Term ~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 +;; + diff --git a/helm/software/components/ng_cic_content/ncic2astMatcher.ml b/helm/software/components/ng_cic_content/ncic2astMatcher.ml new file mode 100644 index 000000000..099e0b26a --- /dev/null +++ b/helm/software/components/ng_cic_content/ncic2astMatcher.ml @@ -0,0 +1,109 @@ +(* 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: acic2astMatcher.ml 9271 2008-11-28 18:28:58Z fguidi $ *) + +module Ast = CicNotationPt +module Util = CicNotationUtil + +module Matcher32 = +struct + module Pattern32 = + struct + type cic_mask_t = + Blob + | Uri of UriManager.uri + | Appl of cic_mask_t list + + let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) + + let mask_of_cic = function + | NCic.Appl tl -> Appl (List.map (fun _ -> Blob) tl), tl + | NCic.Const nref -> Uri (NCic2OCic.ouri_of_reference nref), [] + | _ -> Blob, [] + + let tag_of_term t = + let mask, tl = mask_of_cic t in + Hashtbl.hash mask, tl + + let mask_of_appl_pattern = function + | Ast.UriPattern uri -> Uri uri, [] + | Ast.ImplicitPattern + | Ast.VarPattern _ -> Blob, [] + | Ast.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl + + let tag_of_pattern p = + let mask, pl = mask_of_appl_pattern p in + Hashtbl.hash mask, pl + + type pattern_t = Ast.cic_appl_pattern + type term_t = NCic.term + + let string_of_pattern = CicNotationPp.pp_cic_appl_pattern + let string_of_term t = + (*CSC: ??? *) + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t + + let classify = function + | Ast.ImplicitPattern + | Ast.VarPattern _ -> PatternMatcher.Variable + | Ast.UriPattern _ + | Ast.ApplPattern _ -> PatternMatcher.Constructor + end + + module M = PatternMatcher.Matcher (Pattern32) + + let compiler rows = + let match_cb rows matched_terms constructors = + HExtlib.list_findopt + (fun (pl,pid) _ -> + let env = + try + List.map2 + (fun p t -> + match p with + | Ast.ImplicitPattern -> Util.fresh_name (), t + | Ast.VarPattern name -> name, t + | _ -> assert false) + pl matched_terms + with Invalid_argument _ -> assert false in + let rec check_non_linear_patterns = + function + [] -> true + | (name,t)::tl -> + List.for_all + (fun (name',t') -> + name <> name' || NCicReduction.alpha_eq [] [] [] t t' + ) tl && check_non_linear_patterns tl + in + if check_non_linear_patterns env then + Some (env, constructors, pid) + else + None + ) rows + in + M.compiler rows match_cb (fun () -> None) +end + diff --git a/helm/software/components/ng_cic_content/ncic2astMatcher.mli b/helm/software/components/ng_cic_content/ncic2astMatcher.mli new file mode 100644 index 000000000..14e59e002 --- /dev/null +++ b/helm/software/components/ng_cic_content/ncic2astMatcher.mli @@ -0,0 +1,34 @@ +(* 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/ + *) + +module Matcher32: +sig + (** @param l3_patterns level 3 (CIC) patterns (AKA cic_appl_pattern) *) + val compiler : + (CicNotationPt.cic_appl_pattern * int) list -> + (NCic.term -> + ((string * NCic.term) list * NCic.term list * int) option) +end + -- 2.39.2