From: Wilmer Ricciotti Date: Tue, 8 Mar 2011 13:26:37 +0000 (+0000) Subject: First commit with new (incomplete) disambiguation engine. X-Git-Tag: make_still_working~2570 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git First commit with new (incomplete) disambiguation engine. --- diff --git a/matitaB/components/METAS/meta.helm-disambiguation.src b/matitaB/components/METAS/meta.helm-disambiguation.src index 6c286ea71..5eab1b32a 100644 --- a/matitaB/components/METAS/meta.helm-disambiguation.src +++ b/matitaB/components/METAS/meta.helm-disambiguation.src @@ -1,4 +1,4 @@ -requires="helm-content" +requires="helm-content helm-grafite" version="0.0.1" archive(byte)="disambiguation.cma" archive(native)="disambiguation.cmxa" diff --git a/matitaB/components/content/notationEnv.ml b/matitaB/components/content/notationEnv.ml index be9171a8d..77ffd92f2 100644 --- a/matitaB/components/content/notationEnv.ml +++ b/matitaB/components/content/notationEnv.ml @@ -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 *) diff --git a/matitaB/components/content/notationPp.ml b/matitaB/components/content/notationPp.ml index 8828a0321..99255465d 100644 --- a/matitaB/components/content/notationPp.ml +++ b/matitaB/components/content/notationPp.ml @@ -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) diff --git a/matitaB/components/content/notationPt.ml b/matitaB/components/content/notationPt.ml index cead5e7ae..686fcd4ef 100644 --- a/matitaB/components/content/notationPt.ml +++ b/matitaB/components/content/notationPt.ml @@ -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 diff --git a/matitaB/components/content/notationUtil.ml b/matitaB/components/content/notationUtil.ml index 3d80e8fd5..eeb1cd5c6 100644 --- a/matitaB/components/content/notationUtil.ml +++ b/matitaB/components/content/notationUtil.ml @@ -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 = diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index 53c60820c..451d03a10 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -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> (* ≝ *); 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> -> return_term loc (Ast.Implicit `Vector) | PLACEHOLDER -> return_term loc Ast.UserInput diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml index 04440ffe7..305fe5794 100644 --- a/matitaB/components/content_pres/cicNotationPres.ml +++ b/matitaB/components/content_pres/cicNotationPres.ml @@ -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) [] diff --git a/matitaB/components/content_pres/content2presMatcher.ml b/matitaB/components/content_pres/content2presMatcher.ml index 8b613a524..cf5d66b6a 100644 --- a/matitaB/components/content_pres/content2presMatcher.ml +++ b/matitaB/components/content_pres/content2presMatcher.ml @@ -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 diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml index 6846c30b5..7473838ca 100644 --- a/matitaB/components/content_pres/termContentPres.ml +++ b/matitaB/components/content_pres/termContentPres.ml @@ -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) -> diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml index c83760782..62d708a7f 100644 --- a/matitaB/components/disambiguation/disambiguate.ml +++ b/matitaB/components/disambiguation/disambiguate.ml @@ -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 + *) diff --git a/matitaB/components/disambiguation/disambiguate.mli b/matitaB/components/disambiguation/disambiguate.mli index 167de714b..43fe7a717 100644 --- a/matitaB/components/disambiguation/disambiguate.mli +++ b/matitaB/components/disambiguation/disambiguate.mli @@ -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 diff --git a/matitaB/components/disambiguation/disambiguateTypes.ml b/matitaB/components/disambiguation/disambiguateTypes.ml index f6e03d098..8db0c220d 100644 --- a/matitaB/components/disambiguation/disambiguateTypes.ml +++ b/matitaB/components/disambiguation/disambiguateTypes.ml @@ -26,9 +26,16 @@ (* $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" +;; + diff --git a/matitaB/components/disambiguation/disambiguateTypes.mli b/matitaB/components/disambiguation/disambiguateTypes.mli index 1e99fd404..5ebc835cb 100644 --- a/matitaB/components/disambiguation/disambiguateTypes.mli +++ b/matitaB/components/disambiguation/disambiguateTypes.mli @@ -24,14 +24,14 @@ *) 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 diff --git a/matitaB/components/disambiguation/multiPassDisambiguator.ml b/matitaB/components/disambiguation/multiPassDisambiguator.ml index b1cf9aed0..f35b1d8d2 100644 --- a/matitaB/components/disambiguation/multiPassDisambiguator.ml +++ b/matitaB/components/disambiguation/multiPassDisambiguator.ml @@ -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 diff --git a/matitaB/components/disambiguation/multiPassDisambiguator.mli b/matitaB/components/disambiguation/multiPassDisambiguator.mli index 41b79c9b0..41e34e09c 100644 --- a/matitaB/components/disambiguation/multiPassDisambiguator.mli +++ b/matitaB/components/disambiguation/multiPassDisambiguator.mli @@ -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 * diff --git a/matitaB/components/grafite/grafiteAst.ml b/matitaB/components/grafite/grafiteAst.ml index 1175d3cc1..9d4d3490a 100644 --- a/matitaB/components/grafite/grafiteAst.ml +++ b/matitaB/components/grafite/grafiteAst.ml @@ -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 *) diff --git a/matitaB/components/grafite/grafiteAstPp.ml b/matitaB/components/grafite/grafiteAstPp.ml index 48fc8691c..c49937127 100644 --- a/matitaB/components/grafite/grafiteAstPp.ml +++ b/matitaB/components/grafite/grafiteAstPp.ml @@ -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" diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml index 7febf874e..ff9d00b81 100644 --- a/matitaB/components/grafite_engine/grafiteEngine.ml +++ b/matitaB/components/grafite_engine/grafiteEngine.ml @@ -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) diff --git a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml index f1b051d46..2693d608b 100644 --- a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml +++ b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml @@ -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 diff --git a/matitaB/components/grafite_parser/grafiteParser.ml b/matitaB/components/grafite_parser/grafiteParser.ml index 492274f97..2c9f44554 100644 --- a/matitaB/components/grafite_parser/grafiteParser.ml +++ b/matitaB/components/grafite_parser/grafiteParser.ml @@ -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: [ diff --git a/matitaB/components/ng_cic_content/interpretations.ml b/matitaB/components/ng_cic_content/interpretations.ml index ee4bb9437..5f41a1fe5 100644 --- a/matitaB/components/ng_cic_content/interpretations.ml +++ b/matitaB/components/ng_cic_content/interpretations.ml @@ -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 diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml index dbdd21313..cbe14f9d5 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml @@ -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) diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli index 1f5553e91..c75cfb3a5 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli @@ -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 -> diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml index 5c2de5caa..b34a2ec8b 100644 --- a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml @@ -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 diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli index 715be6a85..70e89dfbc 100644 --- a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli +++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli @@ -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 -> diff --git a/matitaB/components/ng_tactics/nCicElim.ml b/matitaB/components/ng_tactics/nCicElim.ml index 24fd7d8e9..0840b16a6 100644 --- a/matitaB/components/ng_tactics/nCicElim.ml +++ b/matitaB/components/ng_tactics/nCicElim.ml @@ -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 diff --git a/matitaB/components/ng_tactics/nDestructTac.ml b/matitaB/components/ng_tactics/nDestructTac.ml index 0ed800626..ef564afc6 100644 --- a/matitaB/components/ng_tactics/nDestructTac.ml +++ b/matitaB/components/ng_tactics/nDestructTac.ml @@ -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 = diff --git a/matitaB/components/ng_tactics/nInversion.ml b/matitaB/components/ng_tactics/nInversion.ml index cf4711db5..9319683ed 100644 --- a/matitaB/components/ng_tactics/nInversion.ml +++ b/matitaB/components/ng_tactics/nInversion.ml @@ -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 = diff --git a/matitaB/components/ng_tactics/nTacStatus.ml b/matitaB/components/ng_tactics/nTacStatus.ml index 9a6358baa..dc534b430 100644 --- a/matitaB/components/ng_tactics/nTacStatus.ml +++ b/matitaB/components/ng_tactics/nTacStatus.ml @@ -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 diff --git a/matitaB/components/ng_tactics/nTactics.ml b/matitaB/components/ng_tactics/nTactics.ml index dbc134319..aecc88e1f 100644 --- a/matitaB/components/ng_tactics/nTactics.ml +++ b/matitaB/components/ng_tactics/nTactics.ml @@ -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) ]) ;; diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml index 020b819c9..9ef663ee1 100644 --- a/matitaB/components/ng_tactics/nnAuto.ml +++ b/matitaB/components/ng_tactics/nnAuto.ml @@ -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 diff --git a/matitaB/matita/lib/basics/pts.ma b/matitaB/matita/lib/basics/pts.ma index 94f49fc5c..16f34ddb1 100644 --- a/matitaB/matita/lib/basics/pts.ma +++ b/matitaB/matita/lib/basics/pts.ma @@ -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. +@ diff --git a/matitaB/matita/matitaGui.ml b/matitaB/matita/matitaGui.ml index cb7c63bac..fbf9247e2 100644 --- a/matitaB/matita/matitaGui.ml +++ b/matitaB/matita/matitaGui.ml @@ -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" diff --git a/matitaB/matita/matitaScript.ml b/matitaB/matita/matitaScript.ml index af3cdf12e..8d1645858 100644 --- a/matitaB/matita/matitaScript.ml +++ b/matitaB/matita/matitaScript.ml @@ -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))