From 2007402c996678701798d71124a1a255529061ee Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Sep 2009 13:48:03 +0000 Subject: [PATCH] New datatype for metasenv/subst: full fledged attributes in place of optional strings. --- helm/software/components/ng_kernel/nCic.ml | 6 ++- helm/software/components/ng_kernel/nCicPp.ml | 26 ++++++++--- .../components/ng_refiner/nCicMetaSubst.ml | 46 ++++++++----------- .../components/ng_refiner/nCicMetaSubst.mli | 8 ++-- .../components/ng_refiner/nCicRefiner.ml | 5 +- .../components/ng_refiner/nCicUnifHint.ml | 6 ++- .../components/ng_refiner/nCicUnification.ml | 11 ++--- .../components/ng_tactics/nTacStatus.ml | 35 +++++++------- .../components/ng_tactics/nTacStatus.mli | 2 +- .../components/ng_tactics/nTactics.ml | 13 +++--- helm/software/matita/matitaMathView.ml | 2 +- 11 files changed, 84 insertions(+), 76 deletions(-) diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index fead92210..32b79f02a 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -56,11 +56,13 @@ type hypothesis = string * context_entry (* name, entry *) type context = hypothesis list -type conjecture = string option * context * term +type meta_attrs = [`Name of string | `IsSort | `InScope | `OutScope of int] list + +type conjecture = meta_attrs * context * term type metasenv = (int * conjecture) list -type subst_entry = string option * context * term * term (* name,ctx,bo,ty *) +type subst_entry = meta_attrs * context * term * term (* name,ctx,bo,ty *) type substitution = (int * subst_entry) list diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index ddecb4dfb..33677cb42 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -208,13 +208,28 @@ let rec ppcontext ~formatter ?(sep="\n") ~subst ~metasenv = function F.fprintf formatter "%s" sep ;; +let ppmetaattrs = + function + [] -> "" + | attrs -> + "(" ^ + String.concat "," + (List.map + (function + `IsSort -> "sort" + | `Name n -> "name=" ^ n + | `InScope -> "in_scope" + | `OutScope n -> "out_scope:" ^ string_of_int n + ) attrs) ^ + ")" +;; + let rec ppmetasenv ~formatter ~subst metasenv = function | [] -> () - | (i,(name, ctx, ty)) :: tl -> + | (i,(attrs, ctx, ty)) :: tl -> F.fprintf formatter "@["; - let name = match name with Some n -> "("^n^")" | _ -> "" in ppcontext ~formatter ~sep:"; " ~subst ~metasenv ctx; - F.fprintf formatter "@;⊢@;?%d%s :@;" i name; + F.fprintf formatter "@;⊢@;?%d%s :@;" i (ppmetaattrs attrs); ppterm ~formatter ~metasenv ~subst ~context:ctx ty; F.fprintf formatter "@]@\n"; ppmetasenv ~formatter ~subst metasenv tl @@ -226,10 +241,9 @@ let ppmetasenv ~formatter ~subst metasenv = let rec ppsubst ~formatter ~subst ~metasenv = function | [] -> () - | (i,(name, ctx, t, ty)) :: tl -> - let name = match name with Some n -> "("^n^")" | _ -> "" in + | (i,(attrs, ctx, t, ty)) :: tl -> ppcontext ~formatter ~sep:"; " ~subst ~metasenv ctx; - F.fprintf formatter " ⊢ ?%d%s := " i name; + F.fprintf formatter " ⊢ ?%d%s := " i (ppmetaattrs attrs); ppterm ~formatter ~metasenv ~subst ~context:ctx t; F.fprintf formatter " : "; ppterm ~formatter ~metasenv ~subst ~context:ctx ty; diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 52d2e4594..bdd0adfe0 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -235,17 +235,10 @@ let rec flexible_arg context subst = function | _ -> false ;; -let in_scope_tag = "tag:in_scope" ;; -let out_scope_tag_prefix = "tag:out_scope:" -let out_scope_tag n = out_scope_tag_prefix ^ string_of_int n ;; -let is_out_scope_tag tag = - String.length tag > String.length out_scope_tag_prefix && - String.sub tag 0 (String.length out_scope_tag_prefix) = out_scope_tag_prefix -;; +let is_out_scope = function `OutScope _ -> true | _ -> false;; +let is_out_scope_tag = List.exists is_out_scope;; let int_of_out_scope_tag tag = - int_of_string - (String.sub tag (String.length out_scope_tag_prefix) - (String.length tag - (String.length out_scope_tag_prefix))) + match List.filter is_out_scope tag with [`OutScope n] -> n | _ -> assert false ;; @@ -259,7 +252,7 @@ let delift ~unify metasenv subst context n l t = | NCic.Meta (i,_) -> (try let tag, _, _, _ = NCicUtils.lookup_subst i subst in - tag = Some in_scope_tag + List.mem `InScope tag with NCicUtils.Subst_not_found _ -> false) | _ -> false in @@ -322,16 +315,15 @@ let delift ~unify metasenv subst context n l t = (try let tag,c,t,ty = NCicUtils.lookup_subst i subst in let in_scope, clear = - match tag with - | Some tag when tag = in_scope_tag -> 0, true - | Some tag when is_out_scope_tag tag->int_of_out_scope_tag tag,true - | _ -> in_scope, false + if List.mem `InScope tag then 0, true + else if is_out_scope_tag tag then int_of_out_scope_tag tag,true + else in_scope, false in let ms = if not clear then ms else metasenv, - (i,(None,c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst + (i,([],c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst in aux (context,k,in_scope) ms (NCicSubstitution.subst_meta l1 t) with NCicUtils.Subst_not_found _ -> @@ -462,26 +454,26 @@ let delift ~unify metasenv subst context n l t = raise (MetaSubstFailure msg) ;; -let mk_meta ?name metasenv context ty = - let tyof = function Some s -> Some ("typeof_"^s) | None -> None in - let rec mk_meta name n metasenv context = function +let mk_meta ?(attrs=[]) metasenv context ty = + let tyof = List.map (function `Name s -> `Name ("typeof_"^s) | x -> x) in + let rec mk_meta attrs n metasenv context = function | `WithType ty -> let len = List.length context in - let menv_entry = (n, (name, context, ty)) in + let menv_entry = (n, (attrs, context, ty)) in menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty | `Sort -> let ty = NCic.Implicit (`Typeof n) in - mk_meta (tyof name) n metasenv [] (`WithType ty) + mk_meta (tyof attrs) n metasenv [] (`WithType ty) | `Type -> let metasenv, _, ty, _ = - mk_meta (tyof name) (newmeta ()) metasenv context `Sort in - mk_meta name n metasenv context (`WithType ty) + mk_meta (tyof attrs) (newmeta ()) metasenv context `Sort in + mk_meta attrs n metasenv context (`WithType ty) | `Term -> let metasenv, _, ty, _ = - mk_meta (tyof name) (newmeta ()) metasenv context `Type in - mk_meta name n metasenv context (`WithType ty) + mk_meta (tyof attrs) (newmeta ()) metasenv context `Type in + mk_meta attrs n metasenv context (`WithType ty) in - mk_meta name (newmeta ()) metasenv context ty + mk_meta attrs (newmeta ()) metasenv context ty ;; let saturate ?(delta=0) metasenv subst context ty goal_arity = @@ -489,7 +481,7 @@ let saturate ?(delta=0) metasenv subst context ty goal_arity = let rec aux metasenv = function | NCic.Prod (name,s,t) as ty -> let metasenv1, _, arg,_ = - mk_meta ~name:name metasenv context (`WithType s) in + mk_meta ~attrs:[`Name name] metasenv context (`WithType s) in let t, metasenv1, args, pno = aux metasenv1 (NCicSubstitution.subst arg t) in diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index 92cfa0908..4cce96095 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -46,7 +46,7 @@ val restrict: (* bool = true if the type of the new meta is closed *) val mk_meta: - ?name:string -> + ?attrs:NCic.meta_attrs -> NCic.metasenv -> NCic.context -> [ `WithType of NCic.term | `Term | `Type | `Sort ] -> NCic.metasenv * int * NCic.term * NCic.term (* menv,metano,instance,type *) @@ -57,7 +57,5 @@ val saturate: NCic.context -> NCic.term -> int -> NCic.term * NCic.metasenv * NCic.term list -val in_scope_tag : string -val out_scope_tag : int -> string -val is_out_scope_tag : string -> bool -val int_of_out_scope_tag : string -> int +val is_out_scope_tag : NCic.meta_attrs -> bool +val int_of_out_scope_tag : NCic.meta_attrs -> int diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 03de06d1c..58036784f 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -42,7 +42,8 @@ let exp_implicit ~localise metasenv context expty t = | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term) | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type) | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term) - | `Tagged s -> NCicMetaSubst.mk_meta ~name:s metasenv context (foo `Term) + | `Tagged s -> + NCicMetaSubst.mk_meta ~attrs:[`Name s] metasenv context (foo `Term) | `Vector -> raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^ "can only be used in argument position"))) @@ -309,7 +310,7 @@ let rec typeof rdb let metasenv = List.filter (function (j,_) -> j <> metanoouttype) metasenv in let subst = - (metanoouttype,(Some "outtype",context,outtype,metaoutsort))::subst in + (metanoouttype,([`Name "outtype"],context,outtype,metaoutsort))::subst in let outtype = newouttype in (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *) diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index a17d7e8a6..a84ce0f4f 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -209,7 +209,8 @@ let saturate ?(delta=0) metasenv subst context ty goal_arity = let rec aux metasenv = function | NCic.Prod (name,s,t) as ty -> let metasenv1, _, arg,_ = - NCicMetaSubst.mk_meta ~name:name metasenv context (`WithType s) in + NCicMetaSubst.mk_meta ~attrs:[`Name name] metasenv context + (`WithType s) in let t, metasenv1, args, pno = aux metasenv1 (NCicSubstitution.subst arg t) in @@ -275,7 +276,8 @@ let look_for_hint hdb metasenv subst context t1 t2 = | NCic.Meta _ as t -> acc, t | NCic.LetIn (name,ty,bo,t) -> let m,_,i,_= - NCicMetaSubst.mk_meta ~name m context (`WithType ty)in + NCicMetaSubst.mk_meta ~attrs:[`Name name] m context + (`WithType ty)in let t = NCicSubstitution.subst i t in aux () (m, (i,bo)::l) t | t -> NCicUntrusted.map_term_fold_a (fun _ () -> ()) () aux acc t diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 291dcabdd..09b1f3d2e 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -130,7 +130,7 @@ let fix_sorts swap exc t = let is_locked n subst = try match NCicUtils.lookup_subst n subst with - | Some tag, _,_,_ when NCicMetaSubst.is_out_scope_tag tag -> true + | tag, _,_,_ when NCicMetaSubst.is_out_scope_tag tag -> true | _ -> false with NCicUtils.Subst_not_found _ -> false ;; @@ -226,7 +226,7 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = in let metasenv = remove_and_hope i in let metasenv = - (i,(None,[],NCic.Implicit (`Typeof i))):: + (i,([],[],NCic.Implicit (`Typeof i))):: List.filter (fun i',_ -> i <> i') metasenv in metasenv,subst,t @@ -427,11 +427,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = let subst = List.map (fun (i,(tag,ctx,bo,ty)) -> let tag = - match tag with - Some tag when - tag = NCicMetaSubst.in_scope_tag - || NCicMetaSubst.is_out_scope_tag tag -> None - | _ -> tag + List.filter + (function `InScope | `OutScope _ -> false | _ -> true) tag in i,(tag,ctx,bo,ty) ) subst diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 0bb0d846e..83b97d408 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -40,7 +40,7 @@ let pp_status status = prerr_endline (NCicPp.ppobj status#obj) ;; -type cic_term = NCic.conjecture (* name, context, term *) +type cic_term = NCic.conjecture (* attrs, context, term *) let ctx_of (_,c,_) = c ;; let relocate status destination (name,source,t as orig) = @@ -117,7 +117,7 @@ let disambiguate status t ty context = GrafiteDisambiguate.disambiguate_nterm expty status context metasenv subst t in let new_pstatus = uri,height,metasenv,subst,obj in - status#set_obj new_pstatus, (None, context, t) + status#set_obj new_pstatus, ([], context, t) ;; let disambiguate a b c d = wrap (disambiguate a b c) d;; @@ -125,7 +125,7 @@ let typeof status ctx t = let status, (_,_,t) = relocate status ctx t in let _,_,metasenv,subst,_ = status#obj in let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in - status, (None, ctx, ty) + status, ([], ctx, ty) ;; let typeof a b c = wrap (typeof a b) c;; @@ -163,7 +163,8 @@ let fix_sorts (name,ctx,t) = let refine status ctx term expty = let status, (nt,_,term) = relocate status ctx term in let status, ne, expty = - match expty with None -> status, None, None + match expty with + None -> status, [], None | Some e -> let status, (n,_, e) = relocate status ctx e in status, n, Some e in @@ -192,34 +193,34 @@ let instantiate status i t = status#set_obj (name,height,metasenv,subst,obj) ;; -let mk_meta status ?name ctx bo_or_ty = +let mk_meta status ?(attrs=[]) ctx bo_or_ty = match bo_or_ty with | `Decl ty -> let status, (_,_,ty) = relocate status ctx ty in let n,h,metasenv,subst,o = status#obj in let metasenv, _, instance, _ = - NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty) + NCicMetaSubst.mk_meta ~attrs metasenv ctx (`WithType ty) in let status = status#set_obj (n,h,metasenv,subst,o) in - status, (None,ctx,instance) + status, ([],ctx,instance) | `Def bo -> let status, (_,_,bo_ as bo) = relocate status ctx bo in let status, (_,_,ty) = typeof status ctx bo in let n,h,metasenv,subst,o = status#obj in let metasenv, metano, instance, _ = - NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty) in + NCicMetaSubst.mk_meta ~attrs metasenv ctx (`WithType ty) in let metasenv = List.filter (fun j,_ -> j <> metano) metasenv in - let subst = (metano, (name, ctx, bo_, ty)) :: subst in + let subst = (metano, (attrs, ctx, bo_, ty)) :: subst in let status = status#set_obj (n,h,metasenv,subst,o) in - status, (None,ctx,instance) + status, ([],ctx,instance) ;; -let mk_in_scope status t = - mk_meta status ~name:NCicMetaSubst.in_scope_tag (ctx_of t) (`Def t) +let mk_in_scope status t = + mk_meta status ~attrs:[`InScope] (ctx_of t) (`Def t) ;; let mk_out_scope n status t = - mk_meta status ~name:(NCicMetaSubst.out_scope_tag n) (ctx_of t) (`Def t) + mk_meta status ~attrs:[`OutScope n] (ctx_of t) (`Def t) ;; (* the following unification problem will be driven by @@ -237,7 +238,7 @@ let select_term = let is_found status ctx t wanted = (* we could lift wanted step-by-step *) - try true, unify status ctx (None, ctx, t) wanted + try true, unify status ctx ([], ctx, t) wanted with | Error (_, Some (NCicUnification.UnificationFailure _)) | Error (_, Some (NCicUnification.Uncertain _)) -> false, status @@ -246,7 +247,7 @@ let select_term let rec aux ctx (status,already_found) t = let b, status = is_found status ctx t wanted in if b then - let status , (_,_,t) = found status (None, ctx, t) in + let status , (_,_,t) = found status ([], ctx, t) in (status,true),t else let _,_,_,subst,_ = status#obj in @@ -313,7 +314,7 @@ let select_term let (status',found), t' = match_term status' ctx wanted t in if found then status',t' else status,t | None -> - let (status,_),t = match_term status ctx (None,ctx,t) t in + let (status,_),t = match_term status ctx ([],ctx,t) t in status,t) | NCic.Implicit _, t -> status, t | _,t -> @@ -340,7 +341,7 @@ let analyse_indty status ty = status, (ref, consno, left, right) ;; -let mk_cic_term c t = None,c,t ;; +let mk_cic_term c t = [],c,t ;; let apply_subst status ctx t = let status, (name,_,t) = relocate status ctx t in diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index 9279de399..33b01b575 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -59,7 +59,7 @@ val fix_sorts: cic_term -> cic_term val get_goalty: #pstatus -> int -> cic_term val mk_meta: - #pstatus as 'status -> ?name:string -> NCic.context -> + #pstatus as 'status -> ?attrs:NCic.meta_attrs -> NCic.context -> [ `Decl of cic_term | `Def of cic_term ] -> 'status * cic_term val instantiate: #pstatus as 'status -> int -> cic_term -> 'status diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 8887175b4..1644186a1 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -93,12 +93,13 @@ let case_tac lab status = | [] -> assert false | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s when is_fresh loc -> - let l_js = List.filter - (fun curloc -> - let _,_,metasenv,_,_ = status#obj in - match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with - Some s,_,_ when s = lab -> true - | _ -> false) ([loc] @+ g') in + let l_js = + List.filter + (fun curloc -> + let _,_,metasenv,_,_ = status#obj in + match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with + attrs,_,_ when List.mem (`Name lab) attrs -> true + | _ -> false) ([loc] @+ g') in ((l_js, t , [],`BranchTag) :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) | _ -> fail (lazy "can't use relative positioning here") diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index e76c659a4..38c46da8c 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -1476,7 +1476,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private _loadTermNCic term m s c = let d = 0 in - let m = (0,(None,c,term))::m in + let m = (0,([],c,term))::m in let status = (MatitaScript.current ())#grafite_status in mathView#nload_sequent status m s d; self#_showMath -- 2.39.2