]> matita.cs.unibo.it Git - helm.git/commitdiff
First commit with new (incomplete) disambiguation engine.
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Tue, 8 Mar 2011 13:26:37 +0000 (13:26 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Tue, 8 Mar 2011 13:26:37 +0000 (13:26 +0000)
34 files changed:
matitaB/components/METAS/meta.helm-disambiguation.src
matitaB/components/content/notationEnv.ml
matitaB/components/content/notationPp.ml
matitaB/components/content/notationPt.ml
matitaB/components/content/notationUtil.ml
matitaB/components/content_pres/cicNotationParser.ml
matitaB/components/content_pres/cicNotationPres.ml
matitaB/components/content_pres/content2presMatcher.ml
matitaB/components/content_pres/termContentPres.ml
matitaB/components/disambiguation/disambiguate.ml
matitaB/components/disambiguation/disambiguate.mli
matitaB/components/disambiguation/disambiguateTypes.ml
matitaB/components/disambiguation/disambiguateTypes.mli
matitaB/components/disambiguation/multiPassDisambiguator.ml
matitaB/components/disambiguation/multiPassDisambiguator.mli
matitaB/components/grafite/grafiteAst.ml
matitaB/components/grafite/grafiteAstPp.ml
matitaB/components/grafite_engine/grafiteEngine.ml
matitaB/components/grafite_engine/nCicCoercDeclaration.ml
matitaB/components/grafite_parser/grafiteParser.ml
matitaB/components/ng_cic_content/interpretations.ml
matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
matitaB/components/ng_disambiguation/grafiteDisambiguate.mli
matitaB/components/ng_disambiguation/nCicDisambiguate.ml
matitaB/components/ng_disambiguation/nCicDisambiguate.mli
matitaB/components/ng_tactics/nCicElim.ml
matitaB/components/ng_tactics/nDestructTac.ml
matitaB/components/ng_tactics/nInversion.ml
matitaB/components/ng_tactics/nTacStatus.ml
matitaB/components/ng_tactics/nTactics.ml
matitaB/components/ng_tactics/nnAuto.ml
matitaB/matita/lib/basics/pts.ma
matitaB/matita/matitaGui.ml
matitaB/matita/matitaScript.ml

index 6c286ea713fb71e81487e1b8b51a4969a8b268d0..5eab1b32a0863fcefc7323961fa0c07e8dbf504e 100644 (file)
@@ -1,4 +1,4 @@
-requires="helm-content"
+requires="helm-content helm-grafite"
 version="0.0.1"
 archive(byte)="disambiguation.cma"
 archive(native)="disambiguation.cmxa"
index be9171a8d9318a714e16fd5ceffbc2a069099278..77ffd92f22b60e9d7fdce05d7949f85f00e1ffb5 100644 (file)
@@ -107,12 +107,12 @@ let declaration_of_var = function
 
 let value_of_term = function
   | Ast.Num (s, _) -> NumValue s
-  | Ast.Ident (s, None) -> StringValue (Var s)
+  | Ast.Ident (s, (* `Ambiguous? *) _) -> StringValue (Var s)
   | t -> TermValue t
 
 let term_of_value = function
-  | NumValue s -> Ast.Num (s, 0)
-  | StringValue (Ident s) -> Ast.Ident (s, None)
+  | NumValue s -> Ast.Num (s, None)
+  | StringValue (Ident s) -> Ast.Ident (s, `Ambiguous)
   | TermValue t -> t
   | _ -> assert false (* TO BE UNDERSTOOD *)
 
index 8828a03216bb74c64b71db833276fdd8c500d662..99255465d0fdcff99268d365ad64e274adac50b7 100644 (file)
@@ -79,6 +79,12 @@ let pp_capture_variable pp_term =
   | term, Some typ -> "(" ^ pp_term (* ~pp_parens:false *) term ^ ": " ^ pp_term typ ^ ")"
 
 let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
+  let pp_ident = function
+  | Ast.Ident (id,`Ambiguous) -> "A:" ^ id
+  | Ast.Ident (id,`Rel) -> "R:" ^ id
+  | Ast.Ident (id,`Uri u) -> ("U:(" ^ id ^ "," ^ u ^ ")")
+  | _ -> "E"
+  in
   let pp_term = pp_term status in
   let t_pp =
     match t with
@@ -88,12 +94,17 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
     | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term
     | Ast.Appl terms ->
         sprintf "%s" (String.concat " " (List.map pp_term terms))
-    | Ast.Binder (`Forall, (Ast.Ident ("_", None), typ), body)
-    | Ast.Binder (`Pi, (Ast.Ident ("_", None), typ), body) ->
+    | Ast.Binder (`Forall, (Ast.Ident ("_", `Ambiguous), typ), body)
+    | Ast.Binder (`Forall, (Ast.Ident ("_", `Rel), typ), body)
+    | Ast.Binder (`Pi, (Ast.Ident ("_", `Ambiguous), typ), body) 
+    | Ast.Binder (`Pi, (Ast.Ident ("_", `Rel), typ), body) ->
         sprintf "%s \\to %s"
           (match typ with None -> "?" | Some typ -> pp_term typ)
           (pp_term ~pp_parens:true body)
     | Ast.Binder (kind, var, body) ->
+(*
+ * sprintf "\\%s[%s] %s.%s" (pp_binder kind) (pp_ident var) (pp_capture_variable pp_term var)
+ *)
         sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable pp_term var)
           (pp_term ~pp_parens:true body)
     | Ast.Case (term, indtype, typ, patterns) ->
@@ -138,13 +149,9 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
           (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
           (String.concat " and " (List.map map definitions))
           (pp_term term)
-    | Ast.Ident (name, Some []) | Ast.Ident (name, None)
-    | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
+    | Ast.Ident (name, _ ) -> pp_ident t
     | Ast.NRef nref -> NReference.string_of_reference nref
     | Ast.NCic cic -> status#ppterm ~metasenv:[] ~context:[] ~subst:[] cic
-    | Ast.Ident (name, Some substs)
-    | Ast.Uri (name, Some substs) ->
-        sprintf "%s \\subst [%s]" name (pp_substs status substs)
     | Ast.Implicit `Vector -> "…"
     | Ast.Implicit `JustOne -> "?"
     | Ast.Implicit (`Tagged name) -> "?"^name
@@ -171,9 +178,8 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
     | true, Ast.Implicit _
     | true, Ast.UserInput
     | true, Ast.Sort _
-    | true, Ast.Ident (_, Some []) 
-    | true, Ast.Ident (_, None)    -> t_pp
-    | _                            -> sprintf "(%s)" t_pp
+    | true, Ast.Ident _    -> t_pp
+    | _                    -> sprintf "(%s)" t_pp
 
 and pp_subst status (name, term) =
  sprintf "%s \\Assign %s" name (pp_term status term)
index cead5e7ae8eda28cc6ec9d5fc8262b522ae6f3b6..686fcd4ef2ffc1fd3e1bd0b2f7f2e820b001fc0c 100644 (file)
@@ -62,7 +62,7 @@ type 'term capture_variable = 'term * 'term option
 
 (** To be increased each time the term type below changes, used for "safe"
  * marshalling *)
-let magic = 6
+let magic = 7
 
 type term =
   (* CIC AST *)
@@ -78,19 +78,24 @@ type term =
   | LetIn of term capture_variable * term * term  (* name, body, where *)
   | LetRec of induction_kind * (term capture_variable list * term capture_variable * term * int) list * term
       (* (params, name, body, decreasing arg) list, where *)
-  | Ident of string * subst list option
-      (* literal, substitutions.
-      * Some [] -> user has given an empty explicit substitution list 
-      * None -> user has given no explicit substitution list *)
+  | Ident of string * [ `Ambiguous | `Uri of string | `Rel ]
+      (* literal, disambiguation info (can be ambiguous, a disambiguated uri, 
+       * or an identifier to be converted in a Rel)
+       * case `Uri is also used for literal uris
+       * the parser fills the name of the identifier using the final part of the
+       * uri
+       *)
   | Implicit of [`Vector | `JustOne | `Tagged of string]
   | Meta of int * meta_subst list
-  | Num of string * int (* literal, instance *)
+  | Num of string * (string option * string) option 
+      (* literal, (uri, interpretation name) *)
   | Sort of sort_kind
-  | Symbol of string * int  (* canonical name, instance *)
-
+  (* XXX: symbols used to be packed with their instance number, probably for
+   * disambiguation purposes; hopefully we won't need this info any more *)
+  | Symbol of string * (string option * string) option 
+      (* canonical name, (uri, interpretation name) *)
   | UserInput (* place holder for user input, used by MatitaConsole, not to be
               used elsewhere *)
-  | Uri of string * subst list option (* as Ident, for long names *)
   | NRef of NReference.reference
 
   | NCic of NCic.term
@@ -188,6 +193,32 @@ type 'term obj =
   | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list
       (** left parameters, name, type, fields *)
 
+let map_variable f (t,u) = f t, HExtlib.map_option f u ;;
+
+let map_pattern f = function
+  | Pattern (s,h,vl) -> Pattern (s,h,List.map (map_variable f) vl)
+  | p -> p
+;;
+
+let map f = function
+  | AttributedTerm (a,u) -> AttributedTerm (a,f u)
+  | Appl tl -> Appl (List.map f tl)
+  | Binder (k,n,body) -> Binder (k,map_variable f n,f body)
+  | Case (t,ity,oty,pl) -> 
+      let pl' = List.map (fun (p,u) -> map_pattern f p, f u) pl in 
+      Case (f t,ity,HExtlib.map_option f oty,pl')
+  | Cast (u,v) -> Cast (f u,f v)
+  | LetIn (n,u,v) -> LetIn (n,f u,f v)
+  | LetRec (ik,l,t) ->
+      let l' = List.map (fun (vl,v,u,n) -> 
+                (List.map (map_variable f) vl,
+                 map_variable f v,
+                 f u,
+                 n)) l
+      in LetRec (ik,l',f t)
+  | t -> t
+;;
+
 (** {2 Standard precedences} *)
 
 let let_in_prec = 10
index 3d80e8fd51427a0d091335a95e186b1b4553d91f..eeb1cd5c6f6992b80b32004f52ed09e3e19bd96c 100644 (file)
@@ -52,9 +52,6 @@ let visit_ast ?(special_k = fun _ -> assert false)
             definitions
         in
         Ast.LetRec (kind, definitions, k term)
-    | Ast.Ident (name, Some substs) ->
-        Ast.Ident (name, Some (aux_substs substs))
-    | Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs substs))
     | Ast.Meta (index, substs) -> Ast.Meta (index, List.map aux_opt substs)
     | (Ast.AttributedTerm _
       | Ast.Layout _
@@ -68,7 +65,6 @@ let visit_ast ?(special_k = fun _ -> assert false)
       | Ast.Num _
       | Ast.Sort _
       | Ast.Symbol _
-      | Ast.Uri _
       | Ast.UserInput) as t -> t
   and aux_opt = function
     | None -> None
@@ -80,8 +76,6 @@ let visit_ast ?(special_k = fun _ -> assert false)
       Ast.Pattern (head, hrefs, vars), term ->
         Ast.Pattern (head, k_xref hrefs, List.map aux_capture_variable vars), k term
     | Ast.Wildcard, term -> Ast.Wildcard, k term
-  and aux_subst (name, term) = (name, k term)
-  and aux_substs substs = List.map aux_subst substs
   in
   aux
 
@@ -205,8 +199,6 @@ let meta_names_of_term term =
     | Ast.LetRec (_, definitions, body) ->
         List.iter aux_definition definitions ;
         aux body
-    | Ast.Uri (_, Some substs) -> aux_substs substs
-    | Ast.Ident (_, Some substs) -> aux_substs substs
     | Ast.Meta (_, substs) -> aux_meta_substs substs
 
     | Ast.Implicit _
@@ -214,7 +206,6 @@ let meta_names_of_term term =
     | Ast.Num _
     | Ast.Sort _
     | Ast.Symbol _
-    | Ast.Uri _
     | Ast.UserInput -> ()
 
     | Ast.Magic magic -> aux_magic magic
@@ -236,7 +227,6 @@ let meta_names_of_term term =
     List.iter aux_capture_var params ;
     aux_capture_var var ;
     aux term
-  and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
   and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
   and aux_variable = function
     | Ast.NumVar name -> add_name name
@@ -354,6 +344,9 @@ let fresh_id () =
   (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
 let fresh_name () = "eta" ^ string_of_int (fresh_id ())
 
+(* XXX FIXME: was used to add instance indices to symbols/numbers
+ * do we even need a similar operation? 
+ * currently an identity function! *)
 let rec freshen_term ?(index = ref 0) term =
   let freshen_term = freshen_term ~index in
   let fresh_instance () = incr index; !index in
@@ -366,8 +359,8 @@ let rec freshen_term ?(index = ref 0) term =
     | _ -> assert false
   in
   match term with
-  | Ast.Symbol (s, instance) -> Ast.Symbol (s, fresh_instance ())
-  | Ast.Num (s, instance) -> Ast.Num (s, fresh_instance ())
+  | Ast.Symbol (s, x) -> Ast.Symbol (s, x (* fresh_instance () *))
+  | Ast.Num (s, x) -> Ast.Num (s, x (* fresh_instance () *))
   | t -> visit_ast ~special_k freshen_term t
 
 let freshen_obj obj =
index 53c60820c78632bd58f3b8527d697897537c92ff..451d03a101de6273a20d566dc0e1103e06abb6e3 100644 (file)
@@ -338,7 +338,7 @@ let fold_exists terms ty body =
   List.fold_right
     (fun term body ->
       let lambda = Ast.Binder (`Lambda, (term, ty), body) in
-      Ast.Appl [ Ast.Symbol ("exists", 0); lambda ])
+      Ast.Appl [ Ast.Symbol ("exists", None); lambda ])
     terms body
 
 let fold_binder binder pt_names body =
@@ -589,12 +589,12 @@ EXTEND
     [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
         id, Some typ
     | arg = single_arg -> arg, None
-    | id = PIDENT -> Ast.Ident (id, None), None
-    | SYMBOL "_" -> Ast.Ident ("_", None), None
+    | id = PIDENT -> Ast.Ident (id, `Ambiguous), None
+    | SYMBOL "_" -> Ast.Ident ("_", `Ambiguous), None
     | LPAREN; id = PIDENT; SYMBOL ":"; typ = term; RPAREN ->
-        Ast.Ident (id, None), Some typ
+        Ast.Ident (id, `Ambiguous), Some typ
     | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
-        Ast.Ident ("_", None), Some typ
+        Ast.Ident ("_", `Ambiguous), Some typ
     ]
   ];
   match_pattern: [
@@ -615,24 +615,24 @@ EXTEND
   arg: [
     [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
       SYMBOL ":"; ty = term; RPAREN ->
-        List.map (fun n -> Ast.Ident (n, None)) names, Some ty
-    | name = IDENT -> [Ast.Ident (name, None)], None
+        List.map (fun n -> Ast.Ident (n, `Ambiguous)) names, Some ty
+    | name = IDENT -> [Ast.Ident (name, `Ambiguous)], None
     | blob = UNPARSED_META ->
         let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
         match meta with
         | Ast.Variable (Ast.FreshVar _) -> [meta], None
-        | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None
+        | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", `Ambiguous)], None
         | _ -> failwith "Invalid bound name."
    ]
   ];
   single_arg: [
-    [ name = IDENT -> Ast.Ident (name, None)
+    [ name = IDENT -> Ast.Ident (name, `Ambiguous)
     | blob = UNPARSED_META ->
         let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
         match meta with
         | Ast.Variable (Ast.FreshVar _)
         | Ast.Variable (Ast.IdentVar _) -> meta
-        | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None)
+        | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", `Ambiguous)
         | _ -> failwith "Invalid index name."
     ]
   ];
@@ -692,7 +692,7 @@ EXTEND
     [ vars = [ l =
         [ l = LIST1 single_arg SEP SYMBOL "," -> l
         | l = LIST1 [ PIDENT | SYMBOL "_" ] SEP SYMBOL "," -> 
-            List.map (fun x -> Ast.Ident(x,None)) l
+            List.map (fun x -> Ast.Ident(x,`Ambiguous)) l
       ] -> l ];
       typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
     ]
@@ -713,7 +713,7 @@ EXTEND
       [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
          id, Some typ
       | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
-         Ast.Ident(id,None), ty ];
+         Ast.Ident(id,`Ambiguous), ty ];
       SYMBOL <:unicode<def>> (* ≝ *);
       p1 = term; "in"; p2 = term ->
         return_term loc (Ast.LetIn (var, p1, p2))
@@ -745,13 +745,15 @@ EXTEND
     ];
   term: LEVEL "90"
     [
-      [ id = IDENT -> return_term loc (Ast.Ident (id, None))
-      | id = IDENT; s = explicit_subst ->
-          return_term loc (Ast.Ident (id, Some s))
-      | s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0))
-      | u = URI -> return_term loc (Ast.Uri (u, None))
+      [ id = IDENT -> return_term loc (Ast.Ident (id, `Ambiguous))
+      | id = IDENT; s = explicit_subst -> (* XXX: no more explicit subst? *)
+          assert false
+          (* return_term loc (Ast.Ident (id, Some s))*)
+      | s = CSYMBOL -> return_term loc (Ast.Symbol (s, None))
+      | u = URI -> return_term loc (Ast.Ident 
+                     (NUri.name_of_uri (NUri.uri_of_string u), `Uri u))
       | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
-      | n = NUMBER -> return_term loc (Ast.Num (n, 0))
+      | n = NUMBER -> return_term loc (Ast.Num (n, None))
       | IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
       | SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
       | PLACEHOLDER -> return_term loc Ast.UserInput
index 04440ffe7a75cefe1ce1b7d9315f2ef197928611..305fe57947edba39d50e13c0c834230b1e15a023 100644 (file)
@@ -262,32 +262,12 @@ let render status ~lookup_uri ?(prec=(-1)) =
           @ make_href xmlattrs xref
         in
         Mpres.Mo (attrs, to_unicode literal)
-    | A.Ident (literal, subst)
-    | A.Uri (literal, subst) ->
+    | A.Ident (literal, _) ->
         let attrs =
           (RenderingAttrs.ident_attributes `MathML)
           @ make_href xmlattrs xref
         in
-        let name = Mpres.Mi (attrs, to_unicode literal) in
-        (match subst with
-        | Some []
-        | None -> name
-        | Some substs ->
-            let substs' =
-              box_of mathonly (A.H, false, false) []
-                (open_brace
-                :: (NotationUtil.dress semicolon
-                    (List.map
-                      (fun (name, t) ->
-                        box_of mathonly (A.H, false, false) [] [
-                          Mpres.Mi ([], name);
-                          Mpres.Mo ([], to_unicode "\\def");
-                          aux [] mathonly xref  prec t ])
-                      substs))
-                @ [ closed_brace ])
-            in
-            let substs_maction = toggle_action [ hidden_substs; substs' ] in
-            box_of mathonly (A.H, false, false) [] [ name; substs_maction ])
+        Mpres.Mi (attrs, to_unicode literal)
     | A.Meta(n, l) ->
         let local_context l =
           box_of mathonly (A.H, false, false) []
index 8b613a524775a32bab105d8c59bc126e1d5c676a..cf5d66b6a9bd9c5f3c911d83194334efc2a248af 100644 (file)
@@ -103,7 +103,7 @@ struct
               name, (Env.TermType l, Env.TermValue t)
           | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
               name, (Env.NumType, Env.NumValue s)
-          | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
+          | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, `Ambiguous)) ->
               name, (Env.StringType, Env.StringValue (Env.Ident s))
           | _ -> assert false)
         pl tl
index 6846c30b5b9e608fe96af08fbb60b740ccf24b19..7473838ca5e6b6424e36017dc08b1c28cebe7c09 100644 (file)
@@ -75,7 +75,8 @@ let number s =
     (Ast.Literal (`Number s))
 
 let ident i =
-  add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None))
+  add_xml_attrs (RenderingAttrs.ident_attributes `MathML) 
+    (Ast.Ident (i,`Ambiguous))
 
 let ident_w_href href i =
   match href with
@@ -89,7 +90,7 @@ let binder_symbol s =
     (builtin_symbol s)
 
 let xml_of_sort x = 
-  let to_string x = Ast.Ident (x, None) in
+  let to_string x = Ast.Ident (x, `Ambiguous) in
   let identify x = 
     add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) (to_string x)
   in
@@ -271,8 +272,7 @@ let pp_ast0 status t k =
     | Ast.Sort sort -> aux_sort sort
     | Ast.Num _
     | Ast.Symbol _
-    | Ast.Ident (_, None) | Ast.Ident (_, Some [])
-    | Ast.Uri (_, None) | Ast.Uri (_, Some [])
+    | Ast.Ident _ 
     | Ast.Literal _
     | Ast.UserInput as leaf -> leaf
     | t -> NotationUtil.visit_ast ~special_k k t
@@ -599,11 +599,6 @@ let instantiate_level2 status env term =
     | Ast.LetRec (kind, definitions, body) ->
         Ast.LetRec (kind, List.map (aux_definition env) definitions,
           aux env body)
-    | Ast.Uri (name, None) -> Ast.Uri (name, None)
-    | Ast.Uri (name, Some substs) ->
-        Ast.Uri (name, Some (aux_substs env substs))
-    | Ast.Ident (name, Some substs) ->
-        Ast.Ident (name, Some (aux_substs env substs))
     | Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
 
     | Ast.Implicit _
@@ -636,14 +631,14 @@ let instantiate_level2 status env term =
     List.map (fun (name, term) -> (name, aux env term)) substs
   and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
   and aux_variable env = function
-    | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
+    | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, None)
     | Ast.IdentVar name ->
        (match Env.lookup_string env name with
-           Env.Ident x -> Ast.Ident (x, None)
+           Env.Ident x -> Ast.Ident (x, `Ambiguous)
          | Env.Var x -> Ast.Variable (Ast.IdentVar x))
     | Ast.TermVar (name,(Ast.Level l|Ast.Self l)) -> 
         Ast.AttributedTerm (`Level l,Env.lookup_term env name)
-    | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
+    | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, `Ambiguous)
     | Ast.Ascription (term, name) -> assert false
   and aux_magic env = function
     | Ast.Default (some_pattern, none_pattern) ->
index c8376078285100419e9ba228cadce6fc60170de7..62d708a7fdfcce6797bff7e0fa07926a3e128a1e 100644 (file)
@@ -124,11 +124,6 @@ let domain_size = ref 0
 let choices_avg = ref 0.
 *)
 
-let descr_of_domain_item = function
- | Id s -> s
- | Symbol (s, _) -> s
- | Num i -> string_of_int i
-
 type ('term,'metasenv,'subst,'graph) test_result =
   | Ok of 'term * 'metasenv * 'subst * 'graph
   | Ko of (Stdpp.location * string) Lazy.t
@@ -156,7 +151,7 @@ let find_in_context name context =
 
 let string_of_name =
  function
-  | Ast.Ident (n, None) -> Some n
+  | Ast.Ident (n, _) -> Some n
   | _ -> assert false
 ;;
 
@@ -165,11 +160,11 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
      domain_of_term ~loc ~context term
   | Ast.AttributedTerm (_, term) ->
       domain_of_term ~loc ~context term
-  | Ast.Symbol (symbol, instance) ->
-      [ Node ([loc], Symbol (symbol, instance), []) ]
+  | Ast.Symbol (name, attr) ->
+      [ Node ([loc], Symbol (name,attr), []) ]
       (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
-  | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
-  | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
+  | Ast.Appl (Ast.Symbol (name, attr)  as hd :: args)
+  | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (name,attr)) as hd :: args)
      ->
       let args_dom =
         List.fold_right
@@ -180,9 +175,13 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
           Ast.AttributedTerm (`Loc loc,_)  -> loc
         | _ -> loc
       in
-       [ Node ([loc], Symbol (symbol, instance), args_dom) ]
-  | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
-  | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
+       [ Node ([loc], Symbol (name,attr), args_dom) ]
+  | Ast.Appl (Ast.Ident (id,uri) as hd :: args)
+  | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (id,uri)) as hd :: args) ->
+      let uri = match uri with
+        | `Uri u -> Some u
+        | _ -> None
+      in
       let args_dom =
         List.fold_right
           (fun term acc -> domain_of_term ~loc ~context term @ acc)
@@ -194,22 +193,10 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
       in
       (try
         (* the next line can raise Not_found *)
-        ignore(find_in_context name context);
-        if subst <> None then
-          Ast.fail loc "Explicit substitutions not allowed here"
-        else
+        ignore(find_in_context id context);
           args_dom
       with Not_found ->
-        (match subst with
-        | None -> [ Node ([loc], Id name, args_dom) ]
-        | Some subst ->
-            let terms =
-              List.fold_left
-                (fun dom (_, term) ->
-                  let dom' = domain_of_term ~loc ~context term in
-                  dom @ dom')
-                [] subst in
-            [ Node ([loc], Id name, terms @ args_dom) ]))
+        [ Node ([loc], Id (id,uri), args_dom) ] )
   | Ast.Appl terms ->
       List.fold_right
         (fun term acc -> domain_of_term ~loc ~context term @ acc)
@@ -220,14 +207,17 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
         domain_of_term ~loc
           ~context:(string_of_name var :: context) body in
       (match kind with
-      | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
+      | `Exists -> [ Node ([loc], Symbol ("exists",None), (type_dom @ body_dom)) ]
       | _ -> type_dom @ body_dom)
   | Ast.Case (term, indty_ident, outtype, branches) ->
       let term_dom = domain_of_term ~loc ~context term in
       let outtype_dom = domain_of_term_option ~loc ~context outtype in
       let rec get_first_constructor = function
         | [] -> []
-        | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
+        | (Ast.Pattern (head, Some r, _), _) :: _ -> 
+             [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ]
+        | (Ast.Pattern (head, None, _), _) :: _ -> 
+             [ Node ([loc], Id (head,None), []) ]
         | _ :: tl -> get_first_constructor tl in
       let do_branch =
        function
@@ -249,7 +239,9 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
         List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
       (match indty_ident with
        | None -> get_first_constructor branches
-       | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
+       | Some (ident, None) -> [ Node ([loc], Id (ident,None) , []) ]
+       | Some (ident, Some r) -> 
+           [ Node ([loc], Id (ident,Some (NReference.string_of_reference r)), []) ])
       @ term_dom @ outtype_dom @ branches_dom
   | Ast.Cast (term, ty) ->
       let term_dom = domain_of_term ~loc ~context term in
@@ -289,15 +281,16 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
           ) [] defs
       in
       defs_dom @ where_dom
-  | Ast.Ident (name, subst) ->
+  | Ast.Ident (name, x) ->
+      let x = match x with
+        | `Uri u -> Some u
+        | _ -> None
+      in
       (try
         (* the next line can raise Not_found *)
-        ignore(find_in_context name context);
-        if subst <> None then
-          Ast.fail loc "Explicit substitutions not allowed here"
-        else
-          []
+        ignore(find_in_context name context); []
       with Not_found ->
+        (*
         (match subst with
         | None -> [ Node ([loc], Id name, []) ]
         | Some subst ->
@@ -307,8 +300,8 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
                   let dom' = domain_of_term ~loc ~context term in
                   dom @ dom')
                 [] subst in
-            [ Node ([loc], Id name, terms) ]))
-  | Ast.Uri _ -> []
+            [ Node ([loc], Id name, terms) ]))*)
+        [ Node ([loc], Id (name,x), []) ])
   | Ast.NRef _ -> []
   | Ast.NCic _ -> []
   | Ast.Implicit _ -> []
@@ -386,11 +379,11 @@ let domain_diff dom1 dom2 =
   let is_in_dom2 elt =
     List.exists
      (function
-       | Symbol (symb, 0) ->
+       | Symbol (symb,None) ->
           (match elt with
               Symbol (symb',_) when symb = symb' -> true
             | _ -> false)
-       | Num i ->
+       | Num _ ->
           (match elt with
               Num _ -> true
             | _ -> false)
@@ -407,6 +400,368 @@ let domain_diff dom1 dom2 =
 
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
+(* generic function lifting splitting from type T to type (T list) *) 
+let rec list_split item_split ctx pre post =
+  match post with
+  | [] -> []
+  | x :: post' ->
+      (item_split (fun v1 -> ctx (pre@v1::post')) x)@
+        list_split item_split ctx (pre@[x]) post'
+;;
+
+(* splits a 'term capture_variable *)
+let var_split ctx = function
+  | (_,None) -> []
+  | (v,Some ty) -> [(fun x -> ctx (v,Some x)),ty]
+;;
+
+let ity_split ctx (n,isind,ty,cl) = 
+  [(fun x -> ctx (n,isind,x,cl)),ty]@
+  list_split (fun ctx0 (v,ty) -> [(fun x -> ctx0 (v,x)),ty]) 
+    (fun x -> ctx (n,isind,ty,x)) [] cl
+;;
+
+let field_split ctx (n,ty,b,m) =
+        [(fun x -> ctx (n,x,b,m)),ty]
+;;
+
+(* splits a defn. in a mutual LetRec block *)
+let letrecaux_split ctx (args,f,bo,n) =
+        list_split var_split (fun x -> ctx (x,f,bo,n)) [] args@
+        var_split (fun x -> ctx (args,x,bo,n)) f@
+        [(fun x -> ctx (args,f,x,n)),bo]
+;;
+
+(* splits a pattern (for case analysis) *)
+let pattern_split ctx = function
+  | Ast.Wildcard -> []
+  | Ast.Pattern (s,href,pl) -> 
+     let rec auxpatt pre = function
+     | [] -> []
+     | (x,Some y as x')::post' ->
+         ((fun v -> ctx (Ast.Pattern (s,href,pre@(x,Some v)::post'))),y)
+         ::auxpatt (pre@[x']) post'
+     | (x,None as x')::post' -> auxpatt (pre@[x']) post'
+     in auxpatt [] pl
+;;
+
+  (* this function is used to get the children of a given node, together with
+   * their context 
+   * contexts are expressed in the form of functions Ast -> Ast *)
+(* split : ('term -> 'a) -> 'term -> (('term -> 'a) * 'term) list *)
+let rec split ctx = function
+  | Ast.AttributedTerm (attr,t) -> 
+     [(fun x -> ctx (Ast.AttributedTerm(attr,x))),t]
+  | Ast.Appl tl -> list_split split (fun x -> ctx (Ast.Appl x)) [] tl
+  | Ast.Binder (k,((n,None) as n'),body) -> 
+     [ (fun v -> ctx (Ast.Binder (k,n',v))),body]
+  | Ast.Binder (k,((n,Some ty) as n'),body) -> 
+     [(fun v -> ctx (Ast.Binder (k,(n,Some v),body))), ty 
+     ;(fun v -> ctx (Ast.Binder (k,n',v))),body]
+  | Ast.Case (t,ity,outty,pl) -> 
+     let outty_split = match outty with
+     | None -> []
+     | Some u -> [(fun x -> ctx (Ast.Case (t,ity,Some x,pl))),u]
+     in
+     ((fun x -> ctx (Ast.Case (x,ity,outty,pl))),t)::
+       outty_split@list_split
+         (fun ctx0 (p,x) -> 
+            ((fun y -> ctx0 (p,y)),x)::pattern_split 
+              (fun y -> ctx0 (y,x)) p) (fun x -> ctx (Ast.Case(t,ity,outty,x)))
+              [] pl
+  | Ast.Cast (u,v) -> [ (fun x -> ctx (Ast.Cast (x,v))),u
+                  ; (fun x -> ctx (Ast.Cast (u,x))),v ]
+  | Ast.LetIn ((n,None) as n',u,v) ->
+                  [ (fun x -> ctx (Ast.LetIn (n',x,v))), u
+                  ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ]
+  | Ast.LetIn ((n,Some t) as n',u,v) ->
+                  [ (fun x -> ctx (Ast.LetIn ((n,Some x),u,v))), t
+                  ; (fun x -> ctx (Ast.LetIn (n',x,v))), u
+                  ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ]
+  | Ast.LetRec (k,funs,where) -> (* we do not use where any more?? *)
+      list_split letrecaux_split (fun x -> ctx (Ast.LetRec(k,x,where))) [] funs
+  | _ -> [] (* leaves *)
+;;
+
+
+(* top_split : 'a -> ((term -> 'a) * term) list
+ * returns all the possible top-level (ctx,t) for its input *)
+let bfvisit ~pp_term top_split test t = 
+  let rec aux = function
+  | [] -> None
+  | (ctx0,t0 as hd)::tl ->
+(*      prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *)
+      prerr_endline ("t0 = " ^ pp_term t0); 
+      if test t0 then (prerr_endline "caso 1"; Some hd)
+      else 
+              let t0' = split ctx0 t0 in
+              (prerr_endline ("caso 2: length t0' = " ^ string_of_int
+              (List.length t0')); aux (tl@t0' (*split ctx0 t0*)))
+  (* in aux [(fun x -> x),t] *)
+  in aux (top_split t)
+;;
+
+let obj_split (o:Ast.term Ast.obj) = match o with
+  | Ast.Inductive (ls,itl) -> 
+      list_split var_split (fun x -> Ast.Inductive (x,itl)) [] ls@
+      list_split ity_split (fun x -> Ast.Inductive (ls,x)) [] itl 
+  | Ast.Theorem (flav,n,ty,None,p) ->
+      [(fun x -> Ast.Theorem (flav,n,x,None,p)), ty]
+  | Ast.Theorem (flav,n,ty,(Some bo as bo'),p) ->
+      [(fun x -> Ast.Theorem (flav,n,x,bo',p)), ty
+      ;(fun x -> Ast.Theorem (flav,n,ty,Some x,p)), bo]
+  | Ast.Record (ls,n,ty,fl) ->
+      list_split var_split (fun x -> Ast.Record (x,n,ty,fl)) [] ls@
+      [(fun x -> Ast.Record (ls,n,x,fl)),ty]@
+      list_split field_split (fun x -> Ast.Record (ls,n,ty,x)) [] fl 
+;;
+
+let bfvisit_obj = bfvisit obj_split;;
+
+let bfvisit = bfvisit (fun t -> [(fun x -> x),t]) ;;
+
+(*let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library t =
+  let mk_alias = function
+    | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
+    | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
+    | Ast.Num _ -> DisambiguateTypes.Num None
+    | _ -> assert false
+  in
+  let lookup_choices =
+     fun item ->
+      (*match universe with
+      | None -> 
+          lookup_in_library 
+            interactive_user_uri_choice 
+            input_or_locate_uri item
+      | Some e ->
+          (try Environment.find item e
+          with Not_found -> [])
+*)
+          (try Environment.find item universe
+          with Not_found -> [])
+   in
+   match t with
+   | Ast.Ident (_,None)
+   | Ast.Num (_,None) 
+   | Ast.Symbol (_,None) -> 
+       let choices = lookup_choices (mk_alias t) in
+       if List.length choices <> 1 then t
+       else List.hd choices
+     (* but we lose info on closedness *)
+   | t -> Ast.map (initialize_ast ~universe ~lookup_in_library) t
+;;
+*)
+
+let domain_item_of_ast = function
+  | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
+  | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
+  | Ast.Num (n,_) -> DisambiguateTypes.Num None
+  | Ast.Case(_,Some (ityname,_),_,_) -> DisambiguateTypes.Id (ityname,None)
+  | _ -> assert false
+;;
+
+let ast_of_alias_spec t alias = match (t,alias) with
+  | Ast.Ident _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri)
+  | Ast.Case (t,_,oty,pl), GrafiteAst.Ident_alias (id,uri) -> 
+      Ast.Case (t,Some (id,Some (NReference.reference_of_string uri)),oty,pl)
+  | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc))
+  | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
+  | _ -> assert false
+;;
+
+let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri 
+  ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl t =
+  try
+   let localization_tbl = mk_localization_tbl 503 in
+    let cic_thing =
+      interpretate_thing ~context ~env
+       ~uri ~is_path:false t ~localization_tbl
+    in
+    let foo () =
+           refine_thing metasenv subst context uri
+            ~use_coercions cic_thing expty ugraph ~localization_tbl
+    in match (refine_profiler.HExtlib.profile foo ()) with
+    | Ko _ -> false
+    | _ -> true
+  with
+     (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
+     | Invalid_choice loc_msg -> Ko loc_msg*)
+     | Invalid_choice _ -> false
+     | _ -> true
+;;
+
+let rec disambiguate_list
+  ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri ~interpretate_thing
+  ~refine_thing ~ugraph ~visit ~universe ~mk_localization_tbl ~pp_thing ~pp_term ts =
+  let disambiguate_list = 
+    disambiguate_list ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri
+      ~interpretate_thing ~refine_thing ~ugraph ~visit ~universe
+      ~mk_localization_tbl ~pp_thing ~pp_term
+  in
+  let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty 
+    ~env ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl
+  in
+  let find_choices item = 
+    let a2s = function
+    | GrafiteAst.Ident_alias (id,_)
+    | GrafiteAst.Symbol_alias (id,_,_) -> id
+    | GrafiteAst.Number_alias _ -> "NUM"
+    in
+    let d2s = function
+    | Id (id,_)
+    | Symbol (id,_) -> id
+    | Num _ -> "NUM"
+    in
+    let res =
+      Environment.find item universe 
+    in
+    prerr_endline (Printf.sprintf "choices for %s :\n%s"
+      (d2s item) (String.concat ", " (List.map a2s res)));
+    res
+  in
+
+  let get_instances ctx t = 
+    try 
+      let choices = find_choices (domain_item_of_ast t) in
+      List.map (fun t0 -> ctx (ast_of_alias_spec t t0)) choices
+    with
+    | Not_found -> []
+  in
+
+  match ts with
+  | [] -> None
+  | t0 :: tl ->
+      prerr_endline ("disambiguation of t0 = " ^ pp_thing t0); 
+      let is_ambiguous = function
+      | Ast.Ident (_,`Ambiguous)
+      | Ast.Num (_,None)
+      | Ast.Symbol (_,None) -> true
+      | Ast.Case (_,Some (ity,None),_,_) -> 
+          (prerr_endline ("ambiguous case" ^ ity);true)
+      | Ast.Case (_,None,_,_) -> prerr_endline "amb1";false
+      | Ast.Case (_,Some (ity,Some r),_,_) -> 
+          (prerr_endline ("amb2 " ^ NReference.string_of_reference r);false)
+      | Ast.Ident (n,`Uri u) -> 
+          (prerr_endline ("uri " ^ u ^ "inside IDENT " ^ n) ;false )
+      | _ -> false
+      in
+      let astpp = function
+              | Ast.Ident (id,_) -> "ID " ^ id
+              | Ast.Num _ -> "NUM"
+              | Ast.Symbol (sym,_) -> "SYM " ^ sym
+              | _ -> "ERROR!"
+      in
+      (* get first ambiguous subterm (or return disambiguated term) *)
+      match visit ~pp_term is_ambiguous t0 with
+      | None -> 
+          prerr_endline ("not ambiguous:\n" ^ pp_thing t0);
+          Some (t0,tl)
+      | Some (ctx, t) -> 
+        prerr_endline ("disambiguating node " ^ astpp t ^
+        "\nin " ^ pp_thing (ctx t));
+        (* get possible instantiations of t *)
+        let instances = get_instances ctx t in
+        (* perforate ambiguous subterms and test refinement *)
+        let survivors = List.filter test_interpr instances in
+        disambiguate_list (survivors@tl) 
+;;
+
+
+(*  let rec aux l =
+    match l with
+    | [] -> None
+    | (ctx,u)::vl -> 
+        if test u 
+          then (ctx,u)
+          else aux (vl@split ctx u)
+  in aux [t]
+;;*) 
+
+(* let rec instantiate_ast = function
+  | Ident (n,Some _)
+  | Symbol (s,Some _)
+  | Num (n,Some _) as t -> []
+  | Ident (n,None) -> (* output: all possible instantiations of n *)
+  | Symbol (s,None) ->
+  | Num (n,None) -> 
+
+
+  | AttributedTerm (a,u) -> AttributedTerm (a,f u)
+  | Appl tl -> Appl (List.map f tl)
+  | Binder (k,n,body) -> Binder (k,n,f body)
+  | Case (t,ity,oty,pl) -> 
+      let pl' = List.map (fun (p,u) -> p,f u) pl in 
+      Case (f t,ity,map_option f oty,pl')
+  | Cast (u,v) -> Cast (f u,f v)
+  | LetIn (n,u,v) -> LetIn (n,f u,f v)
+  | LetRec -> ada (* TODO *)
+  | t -> t
+*)
+
+let disambiguate_thing 
+  ~context ~metasenv ~subst ~use_coercions
+  ~string_context_of_context
+  ~initial_ugraph:base_univ ~expty
+  ~mk_implicit ~description_of_alias ~fix_instance
+  ~aliases ~universe ~lookup_in_library 
+  ~uri ~pp_thing ~pp_term ~domain_of_thing ~interpretate_thing ~refine_thing 
+  ~visit ~mk_localization_tbl
+  (thing_txt,thing_txt_prefix_len,thing)
+=
+(* XXX: will be thrown away *)
+  let todo_dom = domain_of_thing ~context:(string_context_of_context context) thing 
+  in
+  let rec aux_env env = function
+   | [] -> env
+   | Node (_, item, l) :: tl ->
+       let env =
+         Environment.add item
+          (mk_implicit
+            (match item with | Id _ | Num _ -> true | Symbol _ -> false))
+          env in
+       aux_env (aux_env env l) tl in
+  let env = aux_env aliases todo_dom in
+
+  let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty 
+    ~env ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl
+  in
+(* real function *)
+  let rec aux tl =
+    match disambiguate_list ~mk_localization_tbl ~context ~metasenv ~subst
+      ~interpretate_thing ~refine_thing ~ugraph:base_univ ~visit
+      ~use_coercions ~expty ~uri ~env ~universe ~pp_thing
+      ~pp_term tl with
+    | None -> []
+    | Some (t,tl') -> t::aux tl'
+  in
+
+  let refine t = 
+    let localization_tbl = mk_localization_tbl 503 in
+    match refine_thing metasenv subst context uri
+      ~use_coercions
+      (interpretate_thing ~context ~env ~uri ~is_path:false t ~localization_tbl)
+      expty base_univ ~localization_tbl with
+    | Ok (t',m',s',u') -> ([]:(Environment.key * 'f) list),m',s',t',u'
+    | Uncertain x ->
+        let _,err = Lazy.force x in
+        prerr_endline ("refinement uncertain after disambiguation: " ^ err);
+        assert false
+    | _ -> assert false
+  in
+  if not (test_interpr thing) then raise (NoWellTypedInterpretation (0,[]))
+  else
+    let res = aux [thing] in
+    let res =
+      HExtlib.filter_map (fun t -> try Some (refine t) with _ -> None) res
+    in
+    match res with
+    | [] -> raise (NoWellTypedInterpretation (0,[]))
+    | [t] -> res,false
+    | _ -> res,true
+;;
+
+(*
 let disambiguate_thing 
   ~context ~metasenv ~subst ~use_coercions
   ~string_context_of_context
@@ -702,3 +1057,4 @@ in refine_profiler.HExtlib.profile foo ()
           true
     in
      res
+     *)
index 167de714bf39b91d6338afc619530aaf47c41760..43fe7a717e039f8e51e622c4419d9fe96b9d3890 100644 (file)
@@ -86,6 +86,33 @@ val domain_of_term: context:
 val domain_of_obj: 
   context:string option list -> NotationPt.term NotationPt.obj -> domain
 
+(* val disambiguate_list :
+  context:'context ->
+  metasenv:'metasenv ->
+  subst:'subst ->
+  use_coercions:bool ->
+  expty:'refined_thing option ->
+  env:GrafiteAst.alias_spec DisambiguateTypes.Environment.t ->
+  uri:'uri ->
+  interpretate_thing:(context:'context ->
+                      env:GrafiteAst.alias_spec DisambiguateTypes.Environment.t ->
+                      uri:'uri ->
+                      is_path:bool ->
+                      'ast_thing -> localization_tbl:'cic_hash -> 'raw_thing) ->
+  refine_thing:('metasenv -> 'subst -> 'context -> 'uri ->
+                use_coercions:bool -> 'raw_thing -> 'refined_thing option ->
+                'ugraph -> localization_tbl:'cic_hash -> 
+                ('refined_thing, 'metasenv, 'subst, 'ugraph) test_result) ->
+  ugraph:'ugraph ->
+  visit:((NotationPt.term -> bool) -> 'ast_thing -> 
+        ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) ->
+  universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
+  mk_localization_tbl:(int -> 'cic_hash) ->
+  'ast_thing list -> ('ast_thing * 'ast_thing list) option
+*)
+
+(* val initialize_ast : unit *)
+
 val disambiguate_thing:
   context:'context ->
   metasenv:'metasenv ->
@@ -98,7 +125,7 @@ val disambiguate_thing:
   description_of_alias:('alias -> string) ->
   fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
-  universe:'alias list DisambiguateTypes.Environment.t option ->
+  universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
   lookup_in_library:(
     DisambiguateTypes.interactive_user_uri_choice_type ->
     DisambiguateTypes.input_or_locate_uri_type ->
@@ -106,6 +133,7 @@ val disambiguate_thing:
     'alias list) ->
   uri:'uri ->
   pp_thing:('ast_thing -> string) ->
+  pp_term:(NotationPt.term -> string) ->
   domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
   interpretate_thing:(
     context:'context ->
@@ -119,8 +147,21 @@ val disambiguate_thing:
     'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
     'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash -> 
       ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
+  visit:(pp_term:(NotationPt.term -> string) ->
+         (NotationPt.term -> bool) -> 'ast_thing -> 
+        ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) -> 
   mk_localization_tbl:(int -> 'cichash) ->
   'ast_thing disambiguator_input ->
   ((DisambiguateTypes.Environment.key * 'alias) list * 
    'metasenv * 'subst * 'refined_thing * 'ugraph)
   list * bool
+
+val bfvisit :
+  pp_term:(NotationPt.term -> string) -> 
+  (NotationPt.term -> bool) ->
+   NotationPt.term -> ((NotationPt.term -> NotationPt.term) * NotationPt.term) option
+
+val bfvisit_obj :
+  pp_term:(NotationPt.term -> string) -> 
+  (NotationPt.term -> bool) ->
+   NotationPt.term NotationPt.obj -> ((NotationPt.term -> NotationPt.term NotationPt.obj) * NotationPt.term) option
index f6e03d098ccd555de2bab69a0b4f41bb417cf4b5..8db0c220d302e46bdd9b3a210880dff6a170ae90 100644 (file)
 (* $Id$ *)
 
 type domain_item =
-  | Id of string               (* literal *)
-  | Symbol of string * int     (* literal, instance num *)
-  | Num of int                 (* instance num *)
+ | Id of (string * string option)              (* literal, opt. uri *)
+ | Symbol of string * (string option * string) option (* literal, opt. (uri,interp.) *)
+ | Num of (string option * string) option             (* opt. uri, interpretation *)
+
+(*
+type domain_item =
+ | Id of string     (* literal *)
+ | Symbol of string (* literal *)
+ | Num 
+ *)
 
 exception Invalid_choice of (Stdpp.location * string) Lazy.t
 
@@ -46,22 +53,55 @@ struct
   include Environment'
 
   let find k env =
-   match k with
-      Symbol (sym,n) ->
-       (try find k env
-        with Not_found -> find (Symbol (sym,0)) env)
-    | Num n ->
-       (try find k env
-        with Not_found -> find (Num 0) env)
-    | _ -> find k env
+    try find k env 
+    with Not_found -> 
+      match k with
+       | Symbol (sym,_) -> find (Symbol (sym,None)) env
+       | Num _ -> find (Num None) env
+       | Id (id,_) -> find (Id (id,None)) env 
 
   let cons desc_of_alias k v env =
+    let default_dom_item = function
+    | Id (s,_) -> Id (s,None)
+    | Symbol (s,_) -> Symbol (s,None)
+    | Num _ -> Num None
+    in
+    (*
     try
       let current = find k env in
       let dsc = desc_of_alias v in
-      add k (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env
+      let entry = v::(List.filter (fun x -> desc_of_alias x <> dsc) current) in
+      let id = match k with
+        | Id (id,_) -> id
+        | Symbol (sym,_) -> "SYMBOL:"^sym
+        | Num _ -> "NUM"
+      in
+      prerr_endline (Printf.sprintf "updated alias for %s with entry of length %d (was: %d)" id (List.length entry) (List.length current));
+      let res = add k entry env
+      in
+      let test = find k res in
+      prerr_endline (Printf.sprintf "so the current length of the entry is %d."
+        (List.length test));
+      res
+    with Not_found -> add k [v] env
+    *)
+    let env' =
+      try
+        let current = find k env in
+        let dsc = desc_of_alias v in
+        add k (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env
+      with Not_found ->
+        add k [v] env
+    in
+    (* we also add default aliases *)
+    let k' = default_dom_item k in
+    try
+      let current = find k' env' in
+      let dsc = desc_of_alias v in
+      add k' (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env'
     with Not_found ->
-      add k [v] env
+      add k' [v] env'
+
 end
 
 type 'term codomain_item =
@@ -82,7 +122,16 @@ type interactive_interpretation_choice_type = string -> int ->
 type input_or_locate_uri_type = 
   title:string -> ?id:string -> unit -> NReference.reference option
 
-let string_of_domain_item = function
-  | Id s -> Printf.sprintf "ID(%s)" s
-  | Symbol (s, i) -> Printf.sprintf "SYMBOL(%s,%d)" s i
-  | Num i -> Printf.sprintf "NUM(instance %d)" i
+let string_of_domain_item item =
+  let f_opt f x default =
+    match x with
+    | None -> default
+    | Some y -> f y
+  in
+  match item with
+  | Id (s,huri) -> 
+     Printf.sprintf "ID(%s,%s)" s (f_opt (fun x -> x) huri "_")
+  | Symbol (s,_) -> Printf.sprintf "SYMBOL(%s)" s
+  | Num _ -> "NUM"
+;;
+
index 1e99fd404ace0ebfad221082340ed3b98365b144..5ebc835cb4ac3ca9602ae7db3cfab7070a538aa0 100644 (file)
  *)
 
 type domain_item =
- | Id of string               (* literal *)
- | Symbol of string * int     (* literal, instance num *)
- | Num of int                 (* instance num *)
+ | Id of (string * string option)              (* literal, opt. uri *)
+ | Symbol of string * (string option * string) option (* literal, opt. (uri,interp.) *)
+ | Num of (string option * string) option             (* opt. uri, interpretation *)
 
 (* module Domain:      Set.S with type elt = domain_item *)
 module Environment:
 sig
-  include Map.S with type key = domain_item
+  include Map.S with type key = domain_item 
   val cons: ('b -> 'a) -> domain_item -> 'b -> 'b list t -> 'b list t
 end
 
index b1cf9aed0ec55f13e3317489b8e9f63e044d1ffe..f35b1d8d2e3ac5c94495330024f94194ed56bbf4 100644 (file)
@@ -73,7 +73,7 @@ let drop_aliases ?(minimize_instances=false) ~description_of_alias
    let rec aux =
     function
        [] -> []
-     | (D.Symbol (s,n),ci1) as he::tl when n > 0 ->
+     | (D.Symbol (s,n),ci1) as he::tl when n <> None ->
          if
           List.for_all
            (function
@@ -81,15 +81,15 @@ let drop_aliases ?(minimize_instances=false) ~description_of_alias
              | _ -> true
            ) d
          then
-          (D.Symbol (s,0),ci1)::(aux tl)
+          (D.Symbol (s,None),ci1)::(aux tl)
          else
           he::(aux tl)
-     | (D.Num n,ci1) as he::tl when n > 0 ->
+     | (D.Num n,ci1) as he::tl when n <> None ->
          if
           List.for_all
            (function (D.Num _,ci2) -> compare ci1 ci2 | _ -> true) d
          then
-          (D.Num 0,ci1)::(aux tl)
+          (D.Num None,ci1)::(aux tl)
          else
           he::(aux tl)
       | he::tl -> he::(aux tl)
@@ -103,12 +103,12 @@ let drop_aliases_and_clear_diff (choices, user_asked) =
   (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
   user_asked
 
-let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
+let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~visit ~f thing
 =
-  assert (universe <> None);
-  let library = false, DisambiguateTypes.Environment.empty, None in
+  let library = false, DisambiguateTypes.Environment.empty,
+                DisambiguateTypes.Environment.empty in
   let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
-  let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
+  let mono_aliases = true, aliases, DisambiguateTypes.Environment.empty in
   let passes =
     List.map
      (function (fresh_instances,env,use_coercions) ->
@@ -148,7 +148,7 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
 let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
   ~string_context_of_context ~initial_ugraph ~expty ~mk_implicit
   ~description_of_alias ~fix_instance ~aliases ~universe ~lookup_in_library
-  ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
+  ~uri ~pp_thing ~pp_term ~domain_of_thing ~interpretate_thing ~refine_thing ~visit
   ~mk_localization_tbl thing
  =
   let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
@@ -157,8 +157,8 @@ let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
       ~context ~metasenv ~subst ~use_coercions ~string_context_of_context
       ~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~fix_instance
       ~aliases ~universe ~lookup_in_library 
-      ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
-      ~mk_localization_tbl (txt,len,thing)
+      ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~visit 
+      ~mk_localization_tbl ~pp_term (txt,len,thing)
   in
   disambiguate_thing ~description_of_alias ~passes ~aliases
-   ~universe ~f thing
+   ~universe ~visit ~f thing
index 41b79c9b025b2ea73761cf5937f62be39e841396..41e34e09cff74b93c856e0998fd34adb85fe570f 100644 (file)
@@ -52,8 +52,8 @@ val disambiguate_thing:
   description_of_alias:('alias -> string) ->
   fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
-  universe:'alias list
-    DisambiguateTypes.Environment.t option ->
+  universe:GrafiteAst.alias_spec list
+    DisambiguateTypes.Environment.t ->
   lookup_in_library:(
     DisambiguateTypes.interactive_user_uri_choice_type ->
     DisambiguateTypes.input_or_locate_uri_type ->
@@ -61,6 +61,7 @@ val disambiguate_thing:
     'alias list) ->
   uri:'uri ->
   pp_thing:('ast_thing -> string) ->
+  pp_term:(NotationPt.term -> string) -> 
   domain_of_thing:
    (context: string option list -> 'ast_thing -> Disambiguate.domain) ->
   interpretate_thing:(
@@ -75,6 +76,9 @@ val disambiguate_thing:
     'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
     'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash -> 
       ('refined_thing, 'metasenv,'subst,'ugraph) Disambiguate.test_result) ->
+  visit:(pp_term:(NotationPt.term -> string) -> 
+         (NotationPt.term -> bool) -> 'ast_thing -> 
+        ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) -> 
   mk_localization_tbl:(int -> 'cichash) ->
   string * int * 'ast_thing ->
   ((DisambiguateTypes.Environment.key * 'alias) list * 
index 1175d3cc131c7fc9a6083f5ea072c59ad4c1fef4..9d4d3490a9ce7b3729b85e50484bf3790b174ad2 100644 (file)
@@ -82,15 +82,15 @@ type nmacro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 35
+let magic = 37
 
 (* composed magic: term + command magics. No need to change this value *)
 let magic = magic + 10000 * NotationPt.magic
 
 type alias_spec =
-  | Ident_alias of string * string        (* identifier, uri *)
-  | Symbol_alias of string * int * string (* name, instance no, description *)
-  | Number_alias of int * string          (* instance no, description *)
+  | Ident_alias of string * string  (* identifier, uri *)
+  | Symbol_alias of string * string option * string (* name, uri, description *)
+  | Number_alias of string option * string (* uri, description *)
 
 type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (* aka aliases *)
 
index 48fc8691c08c37b66a6425d1cd944760c0b24564..c4993712754443227cec682337fbbc64567be17f 100644 (file)
@@ -119,13 +119,11 @@ let pp_l2_pattern = NotationPp.pp_term
 
 let pp_alias = function
   | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"." id uri
-  | Symbol_alias (symb, instance, desc) ->
-      sprintf "alias symbol \"%s\" %s= \"%s\"."
-        symb
-        (if instance=0 then "" else "(instance "^ string_of_int instance ^ ") ")
-        desc
-  | Number_alias (instance,desc) ->
-      sprintf "alias num (instance %d) = \"%s\"." instance desc
+  | Symbol_alias (symb, (* uri *) _, desc) ->
+      sprintf "alias symbol \"%s\" = \"%s\"."
+        symb desc
+  | Number_alias ((* uri *) _,desc) ->
+      sprintf "alias num = \"%s\"." desc
   
 let pp_associativity = function
   | Gramext.LeftA -> "left associative"
index 7febf874e3a25ac5defb81232663ace8756a3fe2..ff9d00b819e74ae57830a8bc4f234d004636ad93 100644 (file)
@@ -54,7 +54,7 @@ let inject_unification_hint =
 ;;
 
 let eval_unification_hint status t n = 
- let metasenv,subst,status,t =
+ let newast,metasenv,subst,status,t =
   GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst status subst [] t in
@@ -81,7 +81,9 @@ let basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern
  in
  let mode = GrafiteAst.WithPreferences (*assert false*) in (* MATITA 1.0 VEDI SOTTO *)
  let diff =
-  [DisambiguateTypes.Symbol (symbol, 0), GrafiteAst.Symbol_alias (symbol,0,dsc)]
+  (* FIXME! the uri should be filled with something meaningful! *)
+  [DisambiguateTypes.Symbol (symbol, Some (None,dsc)),
+   GrafiteAst.Symbol_alias (symbol,None,dsc)]
  in
   GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
 ;;
@@ -113,6 +115,7 @@ let eval_interpretation status data=
 ;;
 
 let basic_eval_alias (mode,diff) status =
+  prerr_endline "basic_eval_alias";
   GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
 ;;
 
@@ -615,9 +618,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
             List.fold_left
              (fun status (name,cpos,arity) ->
                try
-                 let metasenv,subst,status,t =
+                 let newast,metasenv,subst,status,t =
                   GrafiteDisambiguate.disambiguate_nterm status None [] [] []
-                   ("",0,NotationPt.Ident (name,None)) in
+                   ("",0,NotationPt.Ident (name,`Ambiguous)) in
                  assert (metasenv = [] && subst = []);
                  let status, nuris = 
                    NCicCoercDeclaration.
@@ -708,8 +711,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       let metasenv,subst,status,sort = match sort with
         | None -> [],[],status,NCic.Sort NCic.Prop
         | Some s ->
-           GrafiteDisambiguate.disambiguate_nterm status None [] [] []
-            (text,prefix_len,s) 
+            let newast,metasenv,subst,status,sort = 
+              GrafiteDisambiguate.disambiguate_nterm status None [] [] []
+              (text,prefix_len,s) 
+            in metasenv,subst,status,sort
       in
       assert (metasenv = []);
       let sort = NCicReduction.whd status ~subst [] sort in
@@ -721,7 +726,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
             "ninverter: found target %s, which is not a sort"
              (status#ppterm ~metasenv ~subst ~context:[] sort))) in
       let status = status#set_ng_mode `ProofMode in
-      let metasenv,subst,status,indty =
+      let newast,metasenv,subst,status,indty =
        GrafiteDisambiguate.disambiguate_nterm status None [] [] subst
         (text,prefix_len,indty) in
       let indtyno,(_,leftno,tys,_,_) =
@@ -768,11 +773,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
              code in DisambiguatePp *)
       match spec with
       | GrafiteAst.Ident_alias (id,uri) -> 
-         [DisambiguateTypes.Id id,spec]
-      | GrafiteAst.Symbol_alias (symb, instance, desc) ->
-         [DisambiguateTypes.Symbol (symb,instance),spec]
-      | GrafiteAst.Number_alias (instance,desc) ->
-         [DisambiguateTypes.Num instance,spec]
+         [DisambiguateTypes.Id (id,Some uri),spec]
+      | GrafiteAst.Symbol_alias (symb, uri, desc) ->
+         [DisambiguateTypes.Symbol (symb, Some (uri,desc)),spec]
+      | GrafiteAst.Number_alias (uri,desc) ->
+         [DisambiguateTypes.Num (Some (uri,desc)),spec]
      in
       let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*)
        eval_alias status (mode,diff)
index f1b051d46f229915a02bdfe15daaf9f238a0a3d0..2693d608b37307140d80fa6b2b063f3447cbbd4e 100644 (file)
@@ -9,6 +9,9 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
+(* TODO: all newast's must be returned to the caller in some way
+ * e.g. modifying the status? *)
+
 (* let debug s = prerr_endline (Lazy.force s) ;;*)
 let debug _ = ();;
 
@@ -131,7 +134,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
          if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
          else
            (try 
-            let metasenv,subst,status,src =
+            let newast,metasenv,subst,status,src =
               GrafiteDisambiguate.disambiguate_nterm 
                 status None ctx [] [] ("",0,src) in
             let src = NCicUntrusted.apply_subst status subst [] src in
@@ -149,7 +152,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
       aux 0 [] ty
   in
   let status, tgt, arity = 
-    let metasenv,subst,status,tgt =
+    let newast, metasenv,subst,status,tgt =
       GrafiteDisambiguate.disambiguate_nterm 
         status None [] [] [] ("",0,tgt) in
     let tgt = NCicUntrusted.apply_subst status subst [] tgt in
@@ -316,11 +319,11 @@ let basic_eval_and_record_ncoercion_from_t_cpos_arity
 ;;
 
 let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt = 
- let metasenv,subst,status,ty =
+ let newast_ty,metasenv,subst,status,ty =
   GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
  assert (metasenv=[]);
  let ty = NCicUntrusted.apply_subst status subst [] ty in
- let metasenv,subst,status,t =
+ let newast_t,metasenv,subst,status,t =
   GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst status subst [] t in
index 492274f97ec50ff49196c271d24efdd949976bfd..2c9f44554ad00a2edce564643be7c11ab880f81c 100644 (file)
@@ -59,7 +59,7 @@ let default_associativity = Gramext.NonA
 let mk_rec_corec ind_kind defs loc = 
   let name,ty = 
     match defs with
-    | (params,(N.Ident (name, None), ty),_,_) :: _ ->
+    | (params,(N.Ident (name, `Ambiguous), ty),_,_) :: _ ->
         let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
         let ty =
          List.fold_right
@@ -69,7 +69,7 @@ let mk_rec_corec ind_kind defs loc =
          name,ty
     | _ -> assert false 
   in
-  let body = N.Ident (name,None) in
+  let body = N.Ident (name,`Ambiguous) in
    (loc, N.Theorem(`Definition, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular))
 
 let nmk_rec_corec ind_kind defs loc = 
@@ -430,6 +430,7 @@ EXTEND
         (params,name,typ,fields)
     ] ];
 
+    (* XXX: alias spec must be revised (no more instance nums) *)
     alias_spec: [
       [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
         let alpha = "[a-zA-Z]" in
@@ -455,14 +456,14 @@ EXTEND
           let instance =
             match instance with Some i -> i | None -> 0
           in
-          G.Symbol_alias (symbol, instance, dsc)
+          G.Symbol_alias (symbol, None, dsc)
       | IDENT "num";
         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
         SYMBOL "="; dsc = QSTRING ->
           let instance =
             match instance with Some i -> i | None -> 0
           in
-          G.Number_alias (instance, dsc)
+          G.Number_alias (None,dsc)
       ]
      ];
     argument: [
index ee4bb9437ca5a5002f3f2587768b29a03ac2e239..5f41a1fe56ec8b56c52b9d2abf6fb99be852598b 100644 (file)
@@ -122,15 +122,15 @@ let instantiate32 idrefs env symbol args =
         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)])
+            Ast.Binder (`Lambda, (Ast.Ident (name, `Ambiguous), None),
+              Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, `Ambiguous)])
           else
             t
         in
         add_lambda t (n - count_lambda t)
   in
   let head =
-    let symbol = Ast.Symbol (symbol, 0) in
+    let symbol = Ast.Symbol (symbol, None) in
     add_idrefs idrefs symbol
   in
   if args = [] then head
@@ -236,10 +236,11 @@ let nast_of_cic0 status
        (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))
+          idref (Ast.Ident (name,`Ambiguous))
         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 status true r, None))
+         idref (Ast.Ident ("-" ^ string_of_int (n - List.length
+         context),`Ambiguous)))
+    | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s status true r, `Ambiguous))
     | NCic.Meta (n,lc) when List.mem_assoc n subst -> 
         let _,_,t,_ = List.assoc n subst in
          k ~context (NCicSubstitution.subst_meta status lc t)
@@ -262,15 +263,15 @@ let nast_of_cic0 status
     | 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)),
+         idref (Ast.Binder (binder_kind, (Ast.Ident (n,`Ambiguous), 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)),
+        idref (Ast.Binder (`Lambda,(Ast.Ident (n,`Ambiguous), 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
+        idref (Ast.LetIn ((Ast.Ident (n,`Ambiguous), 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
@@ -282,7 +283,7 @@ let nast_of_cic0 status
            | _ -> NCic.Appl (hd :: args)))
     | NCic.Appl args as t ->
        (match destroy_nat t with
-         | Some n -> idref (Ast.Num (string_of_int n, -1))
+         | Some n -> idref (Ast.Num (string_of_int n, None))
          | None ->
             let args =
              if not !hide_coercions then args
@@ -327,7 +328,7 @@ let nast_of_cic0 status
              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
+              (Ast.Ident (name,`Ambiguous), Some (k ~context:ctx s)) :: cv, rhs
           | _, _ -> [], k ~context:ctx pat
         in
         let j = ref 0 in
@@ -366,7 +367,7 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
            idref
             ~reference:
               (match term with NCic.Const nref -> nref | _ -> assert false)
-           (NotationPt.Ident ("dummy",None))
+           (NotationPt.Ident ("dummy",`Ambiguous))
           in
            match attrterm with
               Ast.AttributedTerm (`IdRef id, _) -> id
index dbdd2131304c1ec34b4da5a0e717fa24e7743ab9..cbe14f9d5b8aaf0bcb370a70dc22d8fd86a0e494 100644 (file)
@@ -68,9 +68,11 @@ let dump_aliases out msg status =
     status#disambiguate_db.aliases
    
 let set_proof_aliases status ~implicit_aliases mode new_aliases =
+ prerr_endline "set_proof_aliases";
  if mode = GrafiteAst.WithoutPreferences then
    status
  else
+   (prerr_endline "set_proof_aliases 2";
    let aliases =
     List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
      status#disambiguate_db.aliases new_aliases in
@@ -87,7 +89,7 @@ let set_proof_aliases status ~implicit_aliases mode new_aliases =
       (if implicit_aliases then new_aliases else []) @
         status#disambiguate_db.new_aliases}
    in
-    status#set_disambiguate_db new_status
+    status#set_disambiguate_db new_status)
 
 exception BaseUriNotSetYet
 
@@ -104,7 +106,7 @@ let __Implicit = "__Implicit__"
 let __Closed_Implicit = "__Closed_Implicit__"
 
 let ncic_mk_choice status = function
-  | GrafiteAst.Symbol_alias (name, _, dsc) ->
+  | GrafiteAst.Symbol_alias (name,_, dsc) ->
      if name = __Implicit then
        dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
      else if name = __Closed_Implicit then 
@@ -118,7 +120,7 @@ let ncic_mk_choice status = function
            (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
         ~term_of_nref:(fun nref -> NCic.Const nref)
        name dsc
-  | GrafiteAst.Number_alias (_, dsc) -> 
+  | GrafiteAst.Number_alias (_,dsc) -> 
      let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
       desc, `Num_interp
        (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
@@ -133,32 +135,34 @@ let ncic_mk_choice status = function
 let mk_implicit b =
   match b with
   | false -> 
-      GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
+      GrafiteAst.Symbol_alias (__Implicit,None,"Fake Implicit")
   | true -> 
-      GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
+      GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit")
 ;;
 
 let nlookup_in_library 
   interactive_user_uri_choice input_or_locate_uri item 
 =
   match item with
-  | DisambiguateTypes.Id id -> 
+  | DisambiguateTypes.Id (id,_) -> 
      (try
        let references = NCicLibrary.resolve id in
         List.map
-         (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
+         (fun u -> 
+           GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
          ) references
       with
        NCicEnvironment.ObjectNotFound _ -> [])
   | _ -> []
 ;;
 
-let fix_instance item l =
+(* XXX TO BE REMOVED: no need to fix instances any more *)
+(*let fix_instance item l =
  match item with
     DisambiguateTypes.Symbol (_,n) ->
      List.map
       (function
-          GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d)
+          GrafiteAst.Symbol_alias (s,d) -> GrafiteAst.Symbol_alias (s,n,d)
         | _ -> assert false
       ) l
   | DisambiguateTypes.Num n ->
@@ -168,18 +172,19 @@ let fix_instance item l =
         | _ -> assert false
       ) l
   | DisambiguateTypes.Id _ -> l
-;;
+;;*)
+let fix_instance _ l = l;;
 
 
 let disambiguate_nterm status expty context metasenv subst thing
 =
-  let diff, metasenv, subst, cic =
+  let newast, diff, metasenv, subst, cic =
     singleton "first"
       (NCicDisambiguate.disambiguate_term
         status
         ~aliases:status#disambiguate_db.aliases
         ~expty 
-        ~universe:(Some status#disambiguate_db.multi_aliases)
+        ~universe:(status#disambiguate_db.multi_aliases)
         ~lookup_in_library:nlookup_in_library
         ~mk_choice:(ncic_mk_choice status)
         ~mk_implicit ~fix_instance
@@ -190,7 +195,7 @@ let disambiguate_nterm status expty context metasenv subst thing
    set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
     diff
   in
-   metasenv, subst, status, cic
+   newast, metasenv, subst, status, cic
 ;;
 
 
@@ -264,7 +269,7 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
       ~mk_choice:(ncic_mk_choice status)
       ~mk_implicit ~fix_instance ~uri
       ~aliases:status#disambiguate_db.aliases
-      ~universe:(Some status#disambiguate_db.multi_aliases) 
+      ~universe:(status#disambiguate_db.multi_aliases) 
       (text,prefix_len,obj)) in
   let status =
    set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
@@ -283,14 +288,14 @@ let disambiguate_cic_appl_pattern status args =
       (List.exists
        (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
      ->
-      let item = DisambiguateTypes.Id id in
+      let item = DisambiguateTypes.Id (id,None) in
        begin
         try
          match
           DisambiguateTypes.Environment.find item
            status#disambiguate_db.aliases
          with
-            GrafiteAst.Ident_alias (_, uri) ->
+            GrafiteAst.Ident_alias (_,uri) ->
              NotationPt.NRefPattern (NReference.reference_of_string uri)
           | _ -> assert false
         with Not_found -> 
@@ -315,6 +320,6 @@ let aliases_for_objs status refs =
        List.map
         (fun u ->
           let name = NCicPp.r2s status true u in
-           DisambiguateTypes.Id name,
+           DisambiguateTypes.Id (name, Some (NReference.string_of_reference u)),
             GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
         ) references) refs)
index 1f5553e912d31875cee67bcd654770c178b1f384..c75cfb3a53bdeee1871d9c5997420ca2dfee01e2 100644 (file)
@@ -62,7 +62,7 @@ val disambiguate_nterm :
  #status as 'status ->
  NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution ->
  NotationPt.term Disambiguate.disambiguator_input ->
-   NCic.metasenv * NCic.substitution * 'status * NCic.term
+   NotationPt.term * NCic.metasenv * NCic.substitution * 'status * NCic.term
 
 val disambiguate_nobj :
  #status as 'status -> ?baseuri:string ->
index 5c2de5caa90ba4e22758637b4feb54478d22ae35..b34a2ec8b91a65e33d35f868bd22f1be9dbac6d1 100644 (file)
@@ -22,7 +22,7 @@ let debug_print s = prerr_endline (Lazy.force s);;
 let debug_print _ = ();;
 
 let cic_name_of_name = function
-  | Ast.Ident (n, None) ->  n
+  | Ast.Ident (n,_) ->  n
   | _ -> assert false
 ;;
 
@@ -123,6 +123,8 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
         (NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)->
         aux ~localize loc context 
           (NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args)))
+    | NotationPt.Appl (NotationPt.Symbol (symb, None) :: args) ->
+        NCic.Implicit `Term
     | NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) ->
         let cic_args = List.map (aux ~localize loc context) args in
         Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
@@ -136,9 +138,9 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
         | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body)
         | `Pi
         | `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
-        | `Exists ->
-            Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0))
-              (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ]))
+        | `Exists -> assert false)
+            (*Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", None))
+              (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ])*)
     | NotationPt.Case (term, indty_ident, outtype, branches) ->
         let cic_term = aux ~localize loc context term in
         let cic_outtype = aux_option ~localize loc context `Term outtype in
@@ -175,22 +177,15 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
         else
          let indtype_ref =
           match indty_ident with
-          | Some (indty_ident, _) ->
-             (match Disambiguate.resolve ~env ~mk_choice 
-                (Id indty_ident) (`Args []) with
-              | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
-              | NCic.Implicit _ ->
-                 raise (Disambiguate.Try_again 
-                  (lazy "The type of the term to be matched is still unknown"))
-              | t ->
-                raise (DisambiguateTypes.Invalid_choice 
-                  (lazy (loc,"The type of the term to be matched "^
-                          "is not (co)inductive: " ^ status#ppterm 
-                          ~metasenv:[] ~subst:[] ~context:[] t))))
+          | Some (_,Some r) -> r
+          | Some (_, None) ->
+              raise (Disambiguate.Try_again 
+                (lazy "The type of the term to be matched is still unknown"))
           | None ->
               let rec fst_constructor =
                 function
-                   (Ast.Pattern (head, _, _), _) :: _ -> head
+                   (Ast.Pattern (head, href, _), _) :: _ -> 
+                     head, HExtlib.map_option NReference.string_of_reference href
                  | (Ast.Wildcard, _) :: tl -> fst_constructor tl
                  | [] -> raise (Invalid_choice (lazy (loc,"The type "^
                      "of the term to be matched cannot be determined "^
@@ -286,7 +281,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
                        0 -> term
                      | n ->
                         NotationPt.Binder
-                         (`Lambda, (NotationPt.Ident ("_", None), None),
+                         (`Lambda, (NotationPt.Ident ("_", `Ambiguous), None),
                            mk_lambdas (n - 1))
                    in
                     (("wildcard",None,[]),
@@ -311,18 +306,17 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
         NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
     | NotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
     | NotationPt.Ident _
-    | NotationPt.Uri _
     | NotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
-    | NotationPt.Ident (name, subst) ->
-       assert (subst = None);
-       (try
-             NCic.Rel (find_in_context name context)
-       with Not_found -> 
-         try NCic.Const (List.assoc name obj_context)
-         with Not_found ->
-            Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
-    | NotationPt.Uri (uri, subst) ->
-       assert (subst = None);
+    | NotationPt.Ident (name, `Rel) ->
+        (try NCic.Rel (find_in_context name context)
+        with Not_found -> 
+         (try NCic.Const (List.assoc name obj_context)
+          with Not_found -> assert false)) (* bug in initialize_ast *)
+    | NotationPt.Ident (name, `Ambiguous) ->
+         (try NCic.Const (List.assoc name obj_context)
+         with Not_found -> NCic.Implicit `Closed)
+            (* Disambiguate.resolve ~env ~mk_choice (Id (name,None)) (`Args [])) *)
+    | NotationPt.Ident (name, `Uri uri) ->
        (try
          NCic.Const (NReference.reference_of_string uri)
         with NRef.IllFormedReference _ ->
@@ -333,6 +327,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
     | NotationPt.Implicit `JustOne -> NCic.Implicit `Term
     | NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
     | NotationPt.UserInput -> NCic.Implicit `Hole
+    | NotationPt.Num (num, None) -> NCic.Implicit `Closed
     | NotationPt.Num (num, i) -> 
         Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
     | NotationPt.Meta (index, subst) ->
@@ -405,7 +400,7 @@ let disambiguate_path status path =
 ;;
 
 let ncic_name_of_ident = function
-  | Ast.Ident (name, None) -> name
+  | Ast.Ident (name,_) -> name
   | _ -> assert false
 ;;
 
@@ -592,10 +587,160 @@ let interpretate_obj status
      NCic.Inductive (true,leftno,tyl,attrs)
 ;;
 
+let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names t =
+  (* ast_of_alias_spec is duplicate in Disambiguate *)
+  let ast_of_alias_spec t alias = match (t,alias) with
+    | _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri) 
+    | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc))
+    | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
+    | _ -> assert false
+  in
+  let init = initialize_ast ~universe ~lookup_in_library in
+  let init_var ~local_names (n,ty) = 
+          (n,HExtlib.map_option (init ~local_names) ty)
+  in
+  let init_vars ~local_names vars =
+  (* 
+    List.fold_right (fun (n,ty) (nacc,tyacc) ->
+      (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+    ) vars (local_names,[])
+  *)
+    let a,b = List.fold_left (fun (nacc,tyacc) (n,ty) ->
+      (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+      ) (local_names,[]) vars
+    in a, List.rev b
+  in
+  let init_pattern ~local_names = function
+    | Ast.Wildcard as t -> local_names,t
+    | Ast.Pattern (c,uri,vars) -> 
+        (* XXX verificare ordine *)
+        let ln',vars' = init_vars ~local_names vars in
+        ln',Ast.Pattern (c,uri,vars')
+  in
+  let mk_alias = function
+    | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
+    | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
+    | Ast.Num _ -> DisambiguateTypes.Num None
+    | _ -> assert false
+  in
+  let lookup_choices =
+     fun item ->
+      (*match universe with
+      | None -> 
+          lookup_in_library 
+            interactive_user_uri_choice 
+            input_or_locate_uri item
+      | Some e ->
+          (try Environment.find item e
+          with Not_found -> [])
+*)
+          (try 
+             let res = Environment.find item universe in
+             let id = match item with
+               | DisambiguateTypes.Id (id,None) -> id ^ "?"
+               | DisambiguateTypes.Id (id,_) -> id ^ "!"
+               | DisambiguateTypes.Symbol _ -> "SYM"
+               | DisambiguateTypes.Num _ -> "NUM"
+             in
+             prerr_endline (Printf.sprintf "lookup_choices of %s returns length %d" id
+               (List.length res));
+             res
+          with Not_found -> [])
+   in
+   match t with
+   | Ast.Ident (id,(`Ambiguous|`Rel))
+       when List.mem id local_names -> Ast.Ident (id,`Rel)
+   | Ast.Ident (id,`Rel) -> init ~local_names (Ast.Ident (id,`Ambiguous))
+   | Ast.Ident (_,`Ambiguous)
+   | Ast.Num (_,None) 
+   | Ast.Symbol (_,None) -> 
+       let choices = lookup_choices (mk_alias t) in
+       if List.length choices <> 1 then t
+       else ast_of_alias_spec t (List.hd choices)
+   | Ast.AttributedTerm (a,u) -> Ast.AttributedTerm (a, init ~local_names u)
+   | Ast.Appl tl -> Ast.Appl (List.map (init ~local_names) tl)
+   | Ast.Binder (k,(n,ty),body) ->
+       let n' = cic_name_of_name n in
+       let ty' = HExtlib.map_option (init ~local_names) ty in
+       let body' = init ~local_names:(n'::local_names) body in
+       Ast.Binder (k,(n,ty'),body')
+   | Ast.Case (t,ity,oty,pl) -> 
+       let t' = init ~local_names t in
+       let oty' = HExtlib.map_option (init ~local_names) oty in
+       let pl' = 
+         List.map (fun (p,u) ->
+           let ns,p' = init_pattern ~local_names p in
+           p',init ~local_names:ns u) pl in
+       Ast.Case (t',ity,oty',pl')
+   | Ast.Cast (u,v) -> Ast.Cast (init ~local_names u,init ~local_names v)
+   | Ast.LetIn ((n,ty),u,v) -> 
+       let n' = cic_name_of_name n in
+       let ty' = HExtlib.map_option (init ~local_names) ty in
+       let u' = init ~local_names u in
+       let v' = init ~local_names:(n'::local_names) v in
+       Ast.LetIn ((n,ty'),u',v')
+   | Ast.LetRec (ik,l,t) ->
+       let recfuns = 
+         List.fold_right (fun (_,(n,_),_,_) acc ->
+           cic_name_of_name n::acc) l [] in
+       let l' = List.map (fun (vl,(n,ty),u,m) -> 
+         let ln',vl' = init_vars ~local_names vl in
+         let ty' = HExtlib.map_option (init ~local_names:ln') ty in
+         let ln'' = recfuns@ln' in
+         let u' = init ~local_names:ln'' u in
+         vl',(n,ty'),u',m) l in
+       let t' = init ~local_names:(recfuns@local_names) t in
+       Ast.LetRec (ik,l',t') (* XXX: t??? *)
+   | t -> t
+;;
+
+let initialize_obj ~universe ~lookup_in_library o = 
+  let init = initialize_ast ~universe ~lookup_in_library in
+  let init_var ~local_names (n,ty) = 
+          (n,HExtlib.map_option (init ~local_names) ty)
+  in
+  let init_vars ~local_names vars = 
+    let a,b = List.fold_left (fun (nacc,tyacc) (n,ty) ->
+      (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+      ) (local_names,[]) vars
+    in a, List.rev b
+    (*List.fold_right (fun (n,ty) (nacc,tyacc) ->
+      (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+    ) vars (local_names,[])*)
+  in
+
+  match o with
+  | Ast.Inductive (ls,itl) ->
+      let ln,ls' = init_vars ~local_names:[] ls in
+      let indtys = 
+         List.fold_right 
+           (fun (name,_,_,_) acc -> name::acc) itl [] in
+      let itl' = List.map
+        (fun (name,isind,ty,cl) ->
+           let ty' = init ~local_names:ln ty in
+           let cl' = 
+             List.map (fun (cname,cty) -> 
+               cname, init ~local_names:(indtys@ln) cty) cl
+           in
+           name,isind,ty',cl') itl
+      in
+      Ast.Inductive (ls',itl')
+  | Ast.Theorem (flav,n,ty,bo,p) ->
+      Ast.Theorem (flav,n,init ~local_names:[] ty,
+                   HExtlib.map_option (init ~local_names:[]) bo,p)
+  | Ast.Record (ls,n,ty,fl) ->
+      let ln,ls' = init_vars ~local_names:[] ls in
+      let ty' = init ~local_names:ln ty in
+      let fl' = List.map (fun (fn,fty,b,i) -> 
+              fn,init ~local_names:ln fty,b,i) fl in
+      Ast.Record (ls,n,ty',fl')
+;;
+
 let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst
  ~expty ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
  ~aliases ~universe ~lookup_in_library (text,prefix_len,term) 
 =
+  let local_names = List.map (fun (n,_) -> n) context in
   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
    let res,b =
     MultiPassDisambiguator.disambiguate_thing
@@ -603,16 +748,20 @@ let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst
      ~context ~metasenv ~initial_ugraph:() ~aliases
      ~mk_implicit ~description_of_alias ~fix_instance
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
-     ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status)
+     ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status)
      ~passes:(MultiPassDisambiguator.passes ())
      ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
      ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
-     ~refine_thing:(refine_term status) (text,prefix_len,term)
+     ~refine_thing:(refine_term status) 
+     (text,prefix_len,
+      (initialize_ast ~universe ~lookup_in_library ~local_names term))
+     ~visit:Disambiguate.bfvisit
      ~mk_localization_tbl ~expty ~subst
    in
-    List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
+    List.map (function (a,b,c,d,_) -> term,a,b,c,d) res, b
 ;;
 
+
 let disambiguate_obj (status: #NCicCoercion.status)
    ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
    ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) 
@@ -626,12 +775,13 @@ let disambiguate_obj (status: #NCicCoercion.status)
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
      ~universe 
      ~uri:(Some uri)
-     ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status))
+     ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status)) ~pp_term:(NotationPp.pp_term status)
      ~passes:(MultiPassDisambiguator.passes ())
      ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
      ~interpretate_thing:(interpretate_obj status ~mk_choice)
      ~refine_thing:(refine_obj status) 
-     (text,prefix_len,obj)
+     (text,prefix_len,(initialize_obj ~universe ~lookup_in_library obj))
+     ~visit:Disambiguate.bfvisit_obj
      ~mk_localization_tbl ~expty:None
    in
     List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
index 715be6a85993b5881c5d3d31f8af87ac14eb3fc4..70e89dfbc38ec888346b430899353629de5b1fa3 100644 (file)
@@ -22,14 +22,15 @@ val disambiguate_term :
   fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
   mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
-  universe:'alias list DisambiguateTypes.Environment.t option ->
+  universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
   lookup_in_library:(
     DisambiguateTypes.interactive_user_uri_choice_type ->
     DisambiguateTypes.input_or_locate_uri_type ->
     DisambiguateTypes.Environment.key ->
     'alias list) ->
   NotationPt.term Disambiguate.disambiguator_input ->
-  ((DisambiguateTypes.domain_item * 'alias) list *
+  (NotationPt.term *
+   (DisambiguateTypes.domain_item * 'alias) list *
    NCic.metasenv *                  
    NCic.substitution *
    NCic.term) list * 
@@ -42,7 +43,7 @@ val disambiguate_obj :
   fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
   mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
-  universe:'alias list DisambiguateTypes.Environment.t option ->
+  universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
   lookup_in_library:(
     DisambiguateTypes.interactive_user_uri_choice_type ->
     DisambiguateTypes.input_or_locate_uri_type ->
index 24fd7d8e9aa0eb65104e4bc7154632985f1e0d39..0840b16a65718f6bb77f71dfb2e92b02dadd9e7e 100644 (file)
@@ -20,7 +20,7 @@ let fresh_name =
 
 let mk_id id =
  let id = if id = "_" then fresh_name () else id in
-  NotationPt.Ident (id,None)
+  NotationPt.Ident (id,`Ambiguous)
 ;;
 
 (*CSC: cut&paste from nCicReduction.split_prods, but does not check that
@@ -225,9 +225,10 @@ let pp (status: #NCic.status) =
  let rec pp rels =
   function
     NCic.Rel i -> List.nth rels (i - 1)
-  | NCic.Const _ as t ->
+  | NCic.Const r as t ->
      NotationPt.Ident
-      (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t,None)
+      (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t,
+       `Uri (NReference.string_of_reference r))
   | NCic.Sort s -> NotationPt.Sort (fst (ast_of_sort s))
   | NCic.Meta _
   | NCic.Implicit _ -> assert false
@@ -280,7 +281,7 @@ let mk_projection status leftno tyname consname consty (projname,_,_) i =
      let arg = mk_id "xxx" in
      let arg_ty = mk_appl (mk_id tyname :: List.rev names) in
      let bvar = mk_id "yyy" in
-     let underscore = NotationPt.Ident ("_",None),None in
+     let underscore = NotationPt.Ident ("_",`Ambiguous),None in
      let bvars =
       HExtlib.mk_list underscore i @ [bvar,None] @
        HExtlib.mk_list underscore (argsno - i -1) in
index 0ed800626d762480895d176fefd9020e3a6b9493..ef564afc6dbe7e63823679d338313bd652b0803b 100644 (file)
@@ -41,7 +41,7 @@ let fresh_name =
 
 let mk_id id =
  let id = if id = "_" then fresh_name () else id in
-  NotationPt.Ident (id,None)
+  NotationPt.Ident (id,`Ambiguous)
 ;;
 
 let rec mk_prods l t =
index cf4711db51f25320bcd6664822399e307f0b8662..9319683ed2740fe9f32f414c953f54fee9d1fe48 100644 (file)
@@ -23,7 +23,7 @@ let fresh_name =
 
 let mk_id id =
  let id = if id = "_" then fresh_name () else id in
-  NotationPt.Ident (id,None)
+  NotationPt.Ident (id,`Ambiguous)
 ;;
 
 let rec split_arity status ~subst context te =
index 9a6358baaf3e98ee5d4de13bd12e3ee9c02e2e61..dc534b43058c04a69125cd6fdf87e4d5630512e2 100644 (file)
@@ -189,7 +189,7 @@ let disambiguate status context t ty =
        let status, (_,x) = relocate status context ty in status, Some x 
  in
  let uri,height,metasenv,subst,obj = status#obj in
- let metasenv, subst, status, t = 
+ let newast, metasenv, subst, status, t = 
    GrafiteDisambiguate.disambiguate_nterm status expty context metasenv subst t 
  in
  let new_pstatus = uri,height,metasenv,subst,obj in
index dbc134319424b94f1397903077ebc1e38e68772c..aecc88e1f5e9ff0b310487fe79122a07125a3def 100644 (file)
@@ -303,7 +303,7 @@ let assumption_tac status = distribute_tac (fun status goal ->
   let context = ctx_of gty in
   let htac = 
    first_tac
-    (List.map (fun (name,_) -> exact_tac ("",0,(Ast.Ident (name,None))))
+    (List.map (fun (name,_) -> exact_tac ("",0,(Ast.Ident (name,`Ambiguous))))
       context)
   in
     exec htac status goal) status
@@ -402,11 +402,11 @@ let select_tac ~where:((txt,txtlen,(wanted,hyps,path)) as where) ~job
   let path = 
    List.fold_left
     (fun path (name,ty) ->
-      NotationPt.Binder (`Forall, (NotationPt.Ident (name,None),Some ty),path))
+      NotationPt.Binder (`Forall, (NotationPt.Ident (name,`Ambiguous),Some ty),path))
     (match path with Some x -> x | None -> NotationPt.UserInput) (List.rev hyps)
   in
    block_tac [ 
-     generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
+     generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,`Ambiguous)) hyps);
      select0_tac ~where:(txt,txtlen,(wanted,[],Some path)) ~job;
      clear_tac (List.map fst hyps) ]
 ;;
@@ -477,7 +477,7 @@ let letin_tac ~where ~what:(_,_,w) name =
  block_tac [
   select_tac ~where ~job:(`Substexpand 1) true;
   exact_tac
-   ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit `JustOne));
+   ("",0,Ast.LetIn((Ast.Ident (name,`Ambiguous),None),w,Ast.Implicit `JustOne));
  ]
 ;;
 
@@ -538,7 +538,7 @@ let elim_tac ~what:(txt,len,what) ~where =
      in
      let eliminator = 
        let _,_,w = what in
-       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+       Ast.Appl [ Ast.Ident (name,`Ambiguous) ; Ast.Implicit `Vector ; w ]
      in
      exact_tac ("",0,eliminator) status) ]) 
 ;;
@@ -559,7 +559,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status =
    [ select_tac ~where ~job:(`Substexpand 2) true;
      exact_tac
       ("",0,
-       Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
+       Ast.Appl(Ast.Ident(name,`Ambiguous)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
         [what]))] status
 ;;
 
@@ -567,7 +567,7 @@ let intro_tac name =
  block_tac
   [ exact_tac
      ("",0,(Ast.Binder (`Lambda,
-      (Ast.Ident (name,None),None),Ast.Implicit `JustOne)));
+      (Ast.Ident (name,`Ambiguous),None),Ast.Implicit `JustOne)));
     if name = "_" then clear_tac [name] else id_tac ]
 ;;
 
@@ -619,7 +619,7 @@ let case1_tac name =
  block_tac [ intro_tac name; 
              cases_tac 
               ~where:("",0,(None,[],None)) 
-              ~what:("",0,Ast.Ident (name,None));
+              ~what:("",0,Ast.Ident (name,`Ambiguous));
              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 ;;
 
@@ -705,7 +705,7 @@ let inversion_tac ~what:(txt,len,what) ~where =
      in
      let eliminator = 
        let _,_,w = what in
-       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+       Ast.Appl [ Ast.Ident (name,`Ambiguous) ; Ast.Implicit `Vector ; w ]
      in
      exact_tac ("",0,eliminator) status) ]) 
 ;;
index 020b819c93ac8df0a5388e7de764bc75a6053b2c..9ef663ee11fe12c8ddc398f01592068fb668c060 100644 (file)
@@ -1136,7 +1136,7 @@ let applicative_case depth signature status flags gty cache =
   let candidates,smart_candidates = 
     let test x = not (is_a_fact_ast status subst metasenv context x) in
     if is_eq then 
-      Ast.Ident("refl",None) ::List.filter test candidates,
+      Ast.Ident("refl",`Ambiguous) ::List.filter test candidates,
       List.filter test smart_candidates
     else candidates,smart_candidates in 
   debug_print ~depth
@@ -1292,12 +1292,12 @@ let intros ~depth status cache =
           in 
           if head_goals status#stack = [] then 
             let status = NTactics.merge_tac status in
-            [(0,Ast.Ident("__intros",None)),status], cache
+            [(0,Ast.Ident("__intros",`Ambiguous)),status], cache
           else
             (* we reindex the equation from scratch *)
             let unit_eq = index_local_equations status#eq_cache status in
             let status = NTactics.merge_tac status in
-            [(0,Ast.Ident("__intros",None)),status], 
+            [(0,Ast.Ident("__intros",`Ambiguous)),status], 
             init_cache ~facts ~unit_eq () ~trace
       | _ -> [],cache
 ;;
@@ -1321,7 +1321,7 @@ let reduce ~whd ~depth status g =
        be empty *)
     let status = NTactics.merge_tac status in
     incr candidate_no;
-    [(!candidate_no,Ast.Ident("__whd",None)),status])
+    [(!candidate_no,Ast.Ident("__whd",`Ambiguous)),status])
 ;;
 
 let do_something signature flags status g depth gty cache =
@@ -1336,7 +1336,7 @@ let do_something signature flags status g depth gty cache =
     List.map 
       (fun s ->
          incr candidate_no;
-         ((!candidate_no,Ast.Ident("__paramod",None)),s))
+         ((!candidate_no,Ast.Ident("__paramod",`Ambiguous)),s))
       (auto_eq_check cache.unit_eq status) 
   in
   let l2 = 
@@ -1628,8 +1628,8 @@ auto_main flags signature cache depth status: unit =
              debug_print (~depth:depth) 
                (lazy ("Case: " ^ NotationPp.pp_term status t));
              let depth,cache =
-              if t=Ast.Ident("__whd",None) || 
-                  t=Ast.Ident("__intros",None
+              if t=Ast.Ident("__whd",`Ambiguous) || 
+                  t=Ast.Ident("__intros",`Ambiguous
                then depth, cache 
               else depth+1,loop_cache in 
             let cache = add_to_trace status ~depth cache t in
index 94f49fc5c33c939e0faa8366cd9ae2b9c5aacf3d..16f34ddb1d6abede235129403f80b2a337e7e880 100644 (file)
@@ -18,3 +18,23 @@ universe constraint Type[0] < Type[1].
 universe constraint Type[1] < Type[2].
 universe constraint Type[2] < Type[3].
 universe constraint Type[3] < Type[4].
+
+inductive True : Prop ≝ I : True.
+
+(*lemma fa : ∀X:Prop.X → X.
+#X #p //
+qed.
+
+(* check fa*)
+
+lemma ggr ≝ fa.*)
+
+inductive False : Prop ≝ .
+
+inductive bool : Prop ≝ True : bool | false : bool.
+
+inductive eq (A:Type[1]) (x:A) : A → Prop ≝
+    refl: eq A x x.
+
+lemma provable_True : True → eq bool True True.
+@ 
index cb7c63bac3ab49aa0d01caf02597a9578cdf3ba9..fbf9247e210f3e509fdb588f51f1577cf9869fcd 100644 (file)
@@ -377,12 +377,17 @@ let interactive_error_interp ~all_passes
                 (fun k,desc -> 
                   let alias =
                    match k with
-                   | DisambiguateTypes.Id id ->
+                   | DisambiguateTypes.Id (id,_opturi) ->
+                       (* XXX we don't have an uri to put into Ident_alias! 
+                        * then we use the description??
+                        * what does this code mean?? *)
+                       (* FIXME we are not using info from the domain_item to
+                        * fill in the alias_spec *)
                        GrafiteAst.Ident_alias (id, desc)
-                   | DisambiguateTypes.Symbol (symb, i)-> 
-                       GrafiteAst.Symbol_alias (symb, i, desc)
-                   | DisambiguateTypes.Num i ->
-                       GrafiteAst.Number_alias (i, desc)
+                   | DisambiguateTypes.Symbol (symb, _)-> 
+                       GrafiteAst.Symbol_alias (symb, None, desc)
+                   | DisambiguateTypes.Num _ ->
+                       GrafiteAst.Number_alias (None,desc)
                   in
                    GrafiteAstPp.pp_alias alias)
                 diff) ^ "\n"
index af3cdf12eb15c7a1381e3e3af84f295838974b20..8d1645858f3c5cc5a36c320d0c779848d7b22ac2 100644 (file)
@@ -119,7 +119,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
              "Many goals focused. Using the context of the first one\n";
            let _, ctx, _ = NCicUtils.lookup_meta g menv in
             ctx in
-      let m, s, status, t = 
+      let newast, m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
           status None ctx menv subst (parsed_text,parsed_text_length,
             NotationPt.Cast (t,NotationPt.Implicit `JustOne))