]> matita.cs.unibo.it Git - helm.git/commitdiff
New datatype for metasenv/subst: full fledged attributes in place of optional
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 30 Sep 2009 13:48:03 +0000 (13:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 30 Sep 2009 13:48:03 +0000 (13:48 +0000)
strings.

helm/software/components/ng_kernel/nCic.ml
helm/software/components/ng_kernel/nCicPp.ml
helm/software/components/ng_refiner/nCicMetaSubst.ml
helm/software/components/ng_refiner/nCicMetaSubst.mli
helm/software/components/ng_refiner/nCicRefiner.ml
helm/software/components/ng_refiner/nCicUnifHint.ml
helm/software/components/ng_refiner/nCicUnification.ml
helm/software/components/ng_tactics/nTacStatus.ml
helm/software/components/ng_tactics/nTacStatus.mli
helm/software/components/ng_tactics/nTactics.ml
helm/software/matita/matitaMathView.ml

index fead92210f45053b925c7acbc82aeb6f55b64cce..32b79f02a2f898a2dadd8472b7aef08a38adca36 100644 (file)
@@ -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
 
index ddecb4dfb9ba75c299211307787ce68e27363de3..33677cb422c2e22191c259376a6e2e7450cd157a 100644 (file)
@@ -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 "@[<hov 2>";
-      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;
index 52d2e45941ceb3fab8050431e82f67d655ad627a..bdd0adfe014f3acba18eab6a1270c55527d012d5 100644 (file)
@@ -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
index 92cfa0908311a30f4a4fbf5fc20779d26e480af7..4cce960956f37a9eae86922aa3b5c2f4e823254d 100644 (file)
@@ -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
index 03de06d1c6c3306613b31e77b2f24639be93ec3f..58036784f634e8e8427f3c86d4987ac0fce35d0b 100644 (file)
@@ -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] *)
index a17d7e8a670694bb6a4bfc263de475e6212f2099..a84ce0f4fba584aa8a830e4f4c31cdcc6deceece 100644 (file)
@@ -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
index 291dcabdde30c808b88db0c362bc09fbefa1e0b6..09b1f3d2e77d923b3345eba41da1aa76a6897062 100644 (file)
@@ -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
index 0bb0d846e9fedc5c3b9bc2a7da01f8b3701e66c5..83b97d4082fe6e9d895d098514b97720773efc85 100644 (file)
@@ -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
index 9279de399ab954e671faf1ee23eb59f682323508..33b01b5753e08d350b3f3a5dbeea4a1c3536882e 100644 (file)
@@ -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
index 8887175b4d95a77cf969680b8ce6e9073be9d687..1644186a1a558cca45538aa560b96387e9038e98 100644 (file)
@@ -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")
index e76c659a4cb42ab194754060e36ca392fb76192e..38c46da8c74c80b17744f5c342090ca9efbf73de 100644 (file)
@@ -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