From: Wilmer Ricciotti Date: Wed, 30 Mar 2011 11:52:27 +0000 (+0000) Subject: Keeping track of locations of disambiguated ids and symbols. X-Git-Tag: make_still_working~2540 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;p=helm.git Keeping track of locations of disambiguated ids and symbols. Matitac produces disambiguated files, with hyperlinks for ids and § marks for symbols. Matita is able to reparse ids with hypelinks. --- diff --git a/matitaB/components/METAS/meta.helm-content_pres.src b/matitaB/components/METAS/meta.helm-content_pres.src index f9540fa62..9687e9a02 100644 --- a/matitaB/components/METAS/meta.helm-content_pres.src +++ b/matitaB/components/METAS/meta.helm-content_pres.src @@ -1,4 +1,4 @@ -requires="helm-content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite" +requires="helm-content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite helm-disambiguation helm-grafite" version="0.0.1" archive(byte)="content_pres.cma" archive(native)="content_pres.cmxa" diff --git a/matitaB/components/content/notationEnv.ml b/matitaB/components/content/notationEnv.ml index 77ffd92f2..cca2e3799 100644 --- a/matitaB/components/content/notationEnv.ml +++ b/matitaB/components/content/notationEnv.ml @@ -32,18 +32,20 @@ type ident_or_var = | Var of string type value = - | TermValue of Ast.term + | TermValue of NotationPt.term | StringValue of ident_or_var | NumValue of string | OptValue of value option | ListValue of value list + | LocValue of Stdpp.location type value_type = - | TermType of int + | TermType of int (* the level of the expected term *) | StringType | NumType | OptType of value_type | ListType of value_type + | NoType exception Value_not_found of string exception Type_mismatch of string * value_type diff --git a/matitaB/components/content/notationEnv.mli b/matitaB/components/content/notationEnv.mli index 372bc15e8..9c83e1a83 100644 --- a/matitaB/components/content/notationEnv.mli +++ b/matitaB/components/content/notationEnv.mli @@ -35,6 +35,7 @@ type value = | NumValue of string | OptValue of value option | ListValue of value list + | LocValue of Stdpp.location type value_type = | TermType of int (* the level of the expected term *) @@ -42,6 +43,7 @@ type value_type = | NumType | OptType of value_type | ListType of value_type + | NoType (** looked up value not found in environment *) exception Value_not_found of string diff --git a/matitaB/components/content/notationPp.ml b/matitaB/components/content/notationPp.ml index 99255465d..d120fde68 100644 --- a/matitaB/components/content/notationPp.ml +++ b/matitaB/components/content/notationPp.ml @@ -70,7 +70,8 @@ let pp_attribute = (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs)) | `Level (prec) -> sprintf "L(%d)" prec | `Raw _ -> "R" - | `Loc _ -> "@" + | `Loc l -> let x,y = HExtlib.loc_of_floc l in + "@" ^ (string_of_int x) ^ "," ^ (string_of_int y) | `ChildPos p -> sprintf "P(%s)" (pp_pos p) let pp_capture_variable pp_term = @@ -79,6 +80,7 @@ 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 debug_printing = true in let pp_ident = function | Ast.Ident (id,`Ambiguous) -> "A:" ^ id | Ast.Ident (id,`Rel) -> "R:" ^ id @@ -90,7 +92,7 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t = match t with | Ast.AttributedTerm (attr, term) when debug_printing -> sprintf "%s[%s]" (pp_attribute attr) (pp_term ~pp_parens:false term) - | Ast.AttributedTerm (`Raw text, _) -> text + | Ast.AttributedTerm (`Raw text, t) -> "RAW:(" ^ (pp_term t) ^ ")" | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term | Ast.Appl terms -> sprintf "%s" (String.concat " " (List.map pp_term terms)) @@ -114,7 +116,7 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t = | None -> "" | Some (ty, href_opt) -> sprintf " in %s%s" ty - (match debug_printing, href_opt with + (match (*debug_printing*) true, href_opt with | true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri) | _ -> "")) @@ -164,14 +166,15 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t = | Ast.Sort `Prop -> "Prop" | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]" | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]" - | Ast.Symbol (name, _) -> "'" ^ name + | Ast.Symbol (name, None) -> "'" ^ name + | Ast.Symbol (name, Some (_,desc)) -> "'" ^ name ^ ":" ^ desc | Ast.UserInput -> "%" - | Ast.Literal l -> pp_literal l - | Ast.Layout l -> pp_layout status l - | Ast.Magic m -> pp_magic status m - | Ast.Variable v -> pp_variable v + | Ast.Literal l -> "literal:(" ^ (pp_literal l) ^ ")" + | Ast.Layout l -> "layout:(" ^ (pp_layout status l) ^ ")" + | Ast.Magic m -> "magic:(" ^ (pp_magic status m) ^ ")" + | Ast.Variable v -> "variable:" ^ (pp_variable v) in match pp_parens, t with | false, _ @@ -190,8 +193,9 @@ and pp_pattern status = Ast.Pattern (head, href, vars), term -> let head_pp = head ^ - (match debug_printing, href with + (match (*debug_printing*)true, href with | true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri) + | true, None -> "(i.e.ambiguous)" | _ -> "") in sprintf "%s \\Rightarrow %s" @@ -343,6 +347,7 @@ let rec pp_value (status: #NCic.status) = function | Env.OptValue (Some v) -> "Some " ^ pp_value status v | Env.OptValue None -> "None" | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map (pp_value status) l)) + | Env.LocValue l -> sprintf "#" let rec pp_value_type = function @@ -351,6 +356,7 @@ let rec pp_value_type = | Env.NumType -> "Number" | Env.OptType t -> "Maybe " ^ pp_value_type t | Env.ListType l -> "List " ^ pp_value_type l + | Env.NoType -> "NoType" let pp_env status env = String.concat "; " diff --git a/matitaB/components/content_pres/Makefile b/matitaB/components/content_pres/Makefile index 655ffbe8f..084940b4d 100644 --- a/matitaB/components/content_pres/Makefile +++ b/matitaB/components/content_pres/Makefile @@ -4,6 +4,8 @@ PREDICATES = INTERFACE_FILES = \ renderingAttrs.mli \ cicNotationLexer.mli \ + interpTable.mli \ + smallLexer.mli \ cicNotationParser.mli \ mpresentation.mli \ box.mli \ @@ -14,7 +16,12 @@ INTERFACE_FILES = \ content2pres.mli \ $(NULL) IMPLEMENTATION_FILES = \ - $(INTERFACE_FILES:%.mli=%.ml) + $(INTERFACE_FILES:%.mli=%.ml) \ + +PKGS = -package "$(MATITA_REQUIRES)" + +CMOS = $(ML:%.ml=%.cmo) +$(CMOS) : $(LIB_DEPS) cicNotationPres.cmi: OCAMLOPTIONS += -rectypes cicNotationPres.cmo: OCAMLOPTIONS += -rectypes @@ -26,10 +33,13 @@ clean: LOCAL_LINKOPTS = -package helm-content_pres -linkpkg cicNotationLexer.cmo: OCAMLC = $(OCAMLC_P4) +smallLexer.cmo: OCAMLC = $(OCAMLC_P4) cicNotationParser.cmo: OCAMLC = $(OCAMLC_P4) cicNotationLexer.cmx: OCAMLOPT = $(OCAMLOPT_P4) +smallLexer.cmx: OCAMLOPT = $(OCAMLOPT_P4) cicNotationParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) cicNotationLexer.ml.annot: OCAMLC = $(OCAMLC_P4) +smallLexer.ml.annot: OCAMLC = $(OCAMLC_P4) cicNotationParser.ml.annot: OCAMLC = $(OCAMLC_P4) include ../../Makefile.defs @@ -42,12 +52,21 @@ UTF8DIR := $(shell $(OCAMLFIND) query helm-syntax_extensions) ULEXDIR := $(shell $(OCAMLFIND) query ulex08) MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" cicNotationLexer.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +smallLexer.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) cicNotationParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) cicNotationLexer.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +smallLexer.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) cicNotationParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) cicNotationLexer.ml.annot: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +smallLexer.ml.annot: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) cicNotationParser.ml.annot: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) depend.opt: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) + +check: check.ml $(LIB_DEPS) $(CMOS) + $(H)echo " OCAMLC $<" + $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) check.ml + + # diff --git a/matitaB/components/content_pres/cicNotationLexer.ml b/matitaB/components/content_pres/cicNotationLexer.ml index eaabf61e7..524575d03 100644 --- a/matitaB/components/content_pres/cicNotationLexer.ml +++ b/matitaB/components/content_pres/cicNotationLexer.ml @@ -62,6 +62,20 @@ let regexp ident = ident_letter ident_cont* ident_decoration* let regexp variable_ident = '_' '_' number let regexp pident = '_' ident +let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+ + +let regexp uri = + ("cic:/" | "theory:/") (* schema *) +(* ident ('/' ident)* |+ path +| *) + uri_step ('/' uri_step)* (* path *) + ('.' ident)+ (* ext *) +(* ("#xpointer(" number ('/' number)+ ")")? (* xpointer *) *) + ("(" number (',' number)* ")")? (* reference spec *) + +let regexp qstring = '"' [^ '"']* '"' +let regexp hreftag = "" +let regexp hrefclose = "" + let regexp tex_token = '\\' ident let regexp delim_begin = "\\[" @@ -82,7 +96,6 @@ let regexp ast_ident = "@" ident let regexp ast_csymbol = "@" csymbol let regexp meta_ident = "$" ident let regexp meta_anonymous = "$_" -let regexp qstring = '"' [^ '"']* '"' let regexp begincomment = "(**" utf8_blank let regexp beginnote = "(*" @@ -125,15 +138,6 @@ let _ = (":=", <:unicode>); ] -let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+ - -let regexp uri = - ("cic:/" | "theory:/") (* schema *) -(* ident ('/' ident)* |+ path +| *) - uri_step ('/' uri_step)* (* path *) - ('.' ident)+ (* ext *) - ("#xpointer(" number ('/' number)+ ")")? (* xpointer *) - let regexp nreference = "cic:/" (* schema *) uri_step ('/' uri_step)* (* path *) @@ -241,9 +245,15 @@ let handle_keywords lexbuf k name = return lexbuf (name, s) ;; +let get_uri buf = + Ulexing.utf8_sub_lexeme buf 9 (Ulexing.lexeme_length buf - 11) +;; + let rec level2_meta_token = lexer | utf8_blank+ -> level2_meta_token lexbuf + | hreftag -> prerr_endline ("****** HREF : " ^ (Ulexing.utf8_lexeme lexbuf));return lexbuf ("HREF", get_uri lexbuf) + | hrefclose -> return lexbuf ("HREFEND","") | ident -> handle_keywords lexbuf (fun x -> List.mem x level2_meta_keywords) "IDENT" | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf) @@ -300,6 +310,8 @@ let rec level2_ast_token status = return lexbuf ("META", String.sub s 1 (String.length s - 1)) | implicit -> return lexbuf ("IMPLICIT", "") | placeholder -> return lexbuf ("PLACEHOLDER", "") + | hreftag -> prerr_endline ("****** HREF : " ^ (Ulexing.utf8_lexeme lexbuf));return lexbuf ("HREF", get_uri lexbuf) + | hrefclose -> return lexbuf ("HREFEND","") | ident -> handle_keywords lexbuf (fun x -> StringSet.mem x status) "IDENT" | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf) | pident -> handle_keywords lexbuf (fun x -> StringSet.mem x status) "PIDENT" @@ -335,6 +347,8 @@ and level1_pattern_token = lexer | utf8_blank+ -> ligatures_token level1_pattern_token lexbuf | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf) + | hreftag -> prerr_endline ("****** HREF : " ^ (Ulexing.utf8_lexeme lexbuf));return lexbuf ("HREF", get_uri lexbuf) + | hrefclose -> return lexbuf ("HREFEND","") | ident ->handle_keywords lexbuf (fun x -> List.mem x level1_keywords) "IDENT" | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf) | pident->handle_keywords lexbuf (fun x->List.mem x level1_keywords) "PIDENT" diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index 451d03a10..3ccd54141 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -43,6 +43,7 @@ type ('a,'b,'c,'d,'e) grammars = { term: 'b Grammar.Entry.e; ident: 'e Grammar.Entry.e; let_defs: 'c Grammar.Entry.e; + located: Stdpp.location Grammar.Entry.e; protected_binder_vars: 'd Grammar.Entry.e; level2_meta: 'b Grammar.Entry.e; } @@ -84,7 +85,10 @@ let level_of precedence = raise (Level_not_found precedence); string_of_int precedence -let gram_symbol s = Gramext.Stoken ("SYMBOL", s) +let gram_symbol s = + Gramext.srules + [ [ Gramext.Stoken ("SYMBOL",s) ], Gramext.action (fun _ loc -> loc) ] + let gram_ident status = Gramext.Snterm (Grammar.Entry.obj (status#notation_parser_db.grammars.ident : 'a Grammar.Entry.e)) @@ -110,7 +114,9 @@ let make_action action bindings = let rec aux (vl : NotationEnv.t) = function [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc) - | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl) + | NoBinding :: tl -> Gramext.action + (fun (loc: Ast.location) -> + aux (("",(Env.NoType,Env.LocValue loc))::vl) tl) (* LUCA: DEFCON 3 BEGIN *) | Binding (name, Env.TermType l) :: tl -> Gramext.action @@ -134,6 +140,7 @@ let make_action action bindings = aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl) | Env _ :: tl -> Gramext.action (fun (v:NotationEnv.t) -> aux (v @ vl) tl) + | _ (* Binding (_,NoType) *) -> assert false (* LUCA: DEFCON 3 END *) in aux [] (List.rev bindings) @@ -568,16 +575,6 @@ EXTEND | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n ] ]; - explicit_subst: [ - [ SYMBOL "\\subst "; (* to avoid catching frequent "a [1]" cases *) - SYMBOL "["; - substs = LIST1 [ - i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) - ] SEP SYMBOL ";"; - SYMBOL "]" -> - substs - ] - ]; meta_subst: [ [ s = SYMBOL "_" -> None | p = term -> Some p ] @@ -612,11 +609,18 @@ EXTEND | SYMBOL <:unicode> (* λ *) -> `Lambda ] ]; + tident: [ + [ uri = HREF; + id = IDENT; + HREFEND -> (id, `Uri uri) ]]; + gident: [ + [ fullident = tident -> fullident; + | id = IDENT -> (id, `Ambiguous) ]]; arg: [ - [ LPAREN; names = LIST1 IDENT SEP SYMBOL ","; + [ LPAREN; names = LIST1 gident SEP SYMBOL ","; SYMBOL ":"; ty = term; RPAREN -> - List.map (fun n -> Ast.Ident (n, `Ambiguous)) names, Some ty - | name = IDENT -> [Ast.Ident (name, `Ambiguous)], None + List.map (fun (n,u) -> Ast.Ident (n,u)) names, Some ty + | (name,uri) = gident -> [Ast.Ident (name,uri)], None | blob = UNPARSED_META -> let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in match meta with @@ -626,7 +630,7 @@ EXTEND ] ]; single_arg: [ - [ name = IDENT -> Ast.Ident (name, `Ambiguous) + [ (name,uri) = gident -> Ast.Ident (name,uri) | blob = UNPARSED_META -> let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in match meta with @@ -649,6 +653,9 @@ EXTEND | _ -> failwith ("Invalid index name: " ^ blob) ] ]; + located: [ + [ s = SYMBOL -> loc ] + ]; let_defs: [ [ defs = LIST1 [ name = single_arg; @@ -712,8 +719,8 @@ EXTEND var = [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN -> id, Some typ - | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] -> - Ast.Ident(id,`Ambiguous), ty ]; + | (id,uri) = gident; ty = OPT [ SYMBOL ":"; typ = term -> typ] -> + Ast.Ident (id,uri), ty ]; SYMBOL <:unicode> (* ≝ *); p1 = term; "in"; p2 = term -> return_term loc (Ast.LetIn (var, p1, p2)) @@ -745,10 +752,7 @@ EXTEND ]; term: LEVEL "90" [ - [ 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))*) + [ (id,uri) = gident -> return_term loc (Ast.Ident (id,uri)) | 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)) @@ -798,6 +802,7 @@ let initial_grammars keywords = let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast" in let term = Grammar.Entry.create level2_ast_grammar "term" in let ident = Grammar.Entry.create level2_ast_grammar "ident" in + let located = Grammar.Entry.create level2_ast_grammar "located" in let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in let protected_binder_vars = Grammar.Entry.create level2_ast_grammar "protected_binder_vars" in @@ -807,6 +812,7 @@ let initial_grammars keywords = term=term; ident=ident; let_defs=let_defs; + located=located; protected_binder_vars=protected_binder_vars; level2_meta=level2_meta; level2_ast_grammar=level2_ast_grammar; @@ -845,7 +851,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action = Some (Gramext.Level level), [ None, Some (*Gramext.NonA*) Gramext.NonA, - [ p_atoms, + [ p_atoms, (* concrete l1 syntax *) (make_action (fun (env: NotationEnv.t) (loc: Ast.location) -> (action env loc)) diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml index 7473838ca..53f0265b7 100644 --- a/matitaB/components/content_pres/termContentPres.ml +++ b/matitaB/components/content_pres/termContentPres.ml @@ -467,6 +467,7 @@ let rec pp_ast1 status term = NotationEnv.OptValue (Some (pp_value v)) | NotationEnv.ListValue vl -> NotationEnv.ListValue (List.map pp_value vl) + | NotationEnv.LocValue _ as v -> v in let ast_env_of_env env = List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env @@ -574,7 +575,7 @@ let tail_names names env = in aux [] env -let instantiate_level2 status env term = +let instantiate_level2 status env loc term = (* prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *) let fresh_env = ref [] in let lookup_fresh_name n = @@ -605,8 +606,8 @@ let instantiate_level2 status env term = | Ast.Ident _ | Ast.Num _ | Ast.Sort _ - | Ast.Symbol _ | Ast.UserInput -> term + | Ast.Symbol _ -> Ast.AttributedTerm (`Loc loc, term) | Ast.Magic magic -> aux_magic env magic | Ast.Variable var -> aux_variable env var diff --git a/matitaB/components/content_pres/termContentPres.mli b/matitaB/components/content_pres/termContentPres.mli index 9c08650c2..cd7d1ee3f 100644 --- a/matitaB/components/content_pres/termContentPres.mli +++ b/matitaB/components/content_pres/termContentPres.mli @@ -54,4 +54,4 @@ val pp_ast: #status -> NotationPt.term -> NotationPt.term (** fills a term pattern instantiating variable magics *) val instantiate_level2: - #NCic.status -> NotationEnv.t -> NotationPt.term -> NotationPt.term + #NCic.status -> NotationEnv.t -> Stdpp.location -> NotationPt.term -> NotationPt.term diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml index 62d708a7f..34cb4ee2f 100644 --- a/matitaB/components/disambiguation/disambiguate.ml +++ b/matitaB/components/disambiguation/disambiguate.ml @@ -61,14 +61,18 @@ let mono_uris_callback ~selection_mode ?ok raise Ambiguous_input let mono_interp_callback _ _ _ = raise Ambiguous_input +let mono_disamb_callback _ = raise Ambiguous_input let _choose_uris_callback = ref mono_uris_callback let _choose_interp_callback = ref mono_interp_callback +let _choose_disamb_callback = ref mono_disamb_callback let set_choose_uris_callback f = _choose_uris_callback := f let set_choose_interp_callback f = _choose_interp_callback := f +let set_choose_disamb_callback f = _choose_disamb_callback := f let interactive_user_uri_choice = !_choose_uris_callback let interactive_interpretation_choice interp = !_choose_interp_callback interp +let interactive_ast_choice interp = !_choose_disamb_callback interp let input_or_locate_uri ~(title:string) ?id () = None (* Zack: I try to avoid using this callback. I therefore assume that * the presence of an identifier that can't be resolved via "locate" @@ -129,16 +133,31 @@ type ('term,'metasenv,'subst,'graph) test_result = | Ko of (Stdpp.location * string) Lazy.t | Uncertain of (Stdpp.location * string) Lazy.t -let resolve ~env ~mk_choice (item: domain_item) arg = +let resolve ~env ~universe ~mk_choice item interpr arg = + (* let _ = (mk_choice : (GrafiteAst.alias_spec -> 'b + DisambiguateTypes.codomain_item)) in *) try - match snd (mk_choice (Environment.find item env)), arg with + let interpr = + match interpr with + | None -> InterprEnv.find item env + | Some i -> i + in + (* one, and only one interpretation is returned (or Not_found) *) + (*if (List.length interpr <> 1) + then (let strinterpr = + String.concat ", " (List.map GrafiteAst.description_of_alias interpr) in + prerr_endline (Printf.sprintf "choices for %s: %s" + (DisambiguateTypes.string_of_domain_item item) strinterpr); + assert false) + else + let interpr = List.hd interpr in*) + match snd (mk_choice interpr), arg with `Num_interp f, `Num_arg n -> f n | `Sym_interp f, `Args l -> f l | `Sym_interp f, `Num_arg n -> (* Implicit number! *) f [] | _,_ -> assert false with Not_found -> - failwith ("Domain item not found: " ^ - (DisambiguateTypes.string_of_domain_item item)) + failwith (": InterprEnv.find failed") (* TODO move it to Cic *) let find_in_context name context = @@ -155,16 +174,19 @@ let string_of_name = | _ -> assert false ;; +(* XXX: assuming the domain is composed of uninterpreted items only *) let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function | Ast.AttributedTerm (`Loc loc, term) -> domain_of_term ~loc ~context term | Ast.AttributedTerm (_, term) -> domain_of_term ~loc ~context term | Ast.Symbol (name, attr) -> - [ Node ([loc], Symbol (name,attr), []) ] + (match attr with + | None -> [ Node ([loc], Symbol name, []) ] + | _ -> []) (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *) - | Ast.Appl (Ast.Symbol (name, attr) as hd :: args) - | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (name,attr)) as hd :: args) + | Ast.Appl (Ast.Symbol (name, None) as hd :: args) + | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (name,None)) as hd :: args) -> let args_dom = List.fold_right @@ -175,13 +197,9 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function Ast.AttributedTerm (`Loc loc,_) -> loc | _ -> loc in - [ 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 + [ Node ([loc], Symbol name, args_dom) ] + | Ast.Appl (Ast.Ident (id,`Ambiguous) as hd :: args) + | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (id,`Ambiguous)) as hd :: args) -> let args_dom = List.fold_right (fun term acc -> domain_of_term ~loc ~context term @ acc) @@ -196,7 +214,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function ignore(find_in_context id context); args_dom with Not_found -> - [ Node ([loc], Id (id,uri), args_dom) ] ) + [ Node ([loc], Id id, args_dom) ] ) | Ast.Appl terms -> List.fold_right (fun term acc -> domain_of_term ~loc ~context term @ acc) @@ -207,17 +225,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",None), (type_dom @ body_dom)) ] + | `Exists -> [ Node ([loc], Symbol "exists", (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, Some r, _), _) :: _ -> - [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ] + | (Ast.Pattern (head, Some r, _), _) :: _ -> [] + (* [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ] *) | (Ast.Pattern (head, None, _), _) :: _ -> - [ Node ([loc], Id (head,None), []) ] + [ Node ([loc], Id head, []) ] | _ :: tl -> get_first_constructor tl in let do_branch = function @@ -239,9 +257,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, None) -> [ Node ([loc], Id (ident,None) , []) ] - | Some (ident, Some r) -> - [ Node ([loc], Id (ident,Some (NReference.string_of_reference r)), []) ]) + | Some (ident, None) -> [ Node ([loc], Id ident , []) ] + | 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 @@ -301,11 +319,11 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function dom @ dom') [] subst in [ Node ([loc], Id name, terms) ]))*) - [ Node ([loc], Id (name,x), []) ]) + [ Node ([loc], Id name, []) ]) | Ast.NRef _ -> [] | Ast.NCic _ -> [] | Ast.Implicit _ -> [] - | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ] + | Ast.Num (num, i) -> [ Node ([loc], Num, []) ] | Ast.Meta (index, local_context) -> List.fold_left (fun dom term -> dom @ domain_of_term_option ~loc ~context term) @@ -374,18 +392,19 @@ let domain_of_obj ~context obj = uniq_domain (domain_of_obj ~context obj) (* dom1 \ dom2 *) +(* XXX: possibly should take into account locs? *) let domain_diff dom1 dom2 = (* let domain_diff = Domain.diff *) let is_in_dom2 elt = List.exists (function - | Symbol (symb,None) -> + | Symbol symb -> (match elt with - Symbol (symb',_) when symb = symb' -> true + Symbol symb' when symb = symb' -> true | _ -> false) - | Num _ -> + | Num -> (match elt with - Num _ -> true + Num -> true | _ -> false) | item -> elt = item ) dom2 @@ -432,6 +451,11 @@ let letrecaux_split ctx (args,f,bo,n) = [(fun x -> ctx (args,f,x,n)),bo] ;; +let mk_ident s = function +| None -> Ast.Ident (s,`Ambiguous) +| Some u -> Ast.Ident (s,`Uri (NReference.string_of_reference u)) +;; + (* splits a pattern (for case analysis) *) let pattern_split ctx = function | Ast.Wildcard -> [] @@ -442,7 +466,17 @@ let pattern_split ctx = function ((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 + in + ((fun x -> + let id0, href0 = + match x with + | Ast.Ident (id,`Ambiguous) -> id, None + | Ast.Ident (id,`Uri u) -> id, Some u + | _ -> assert false + in + let href0 = HExtlib.map_option NReference.reference_of_string href0 + in ctx (Ast.Pattern (id0,href0,pl))), + mk_ident s href)::auxpatt [] pl ;; (* this function is used to get the children of a given node, together with @@ -452,7 +486,7 @@ let pattern_split ctx = function 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.Appl tl -> list_split (*split*) (fun ctx0 t0 -> [ctx0,t0]) (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) -> @@ -491,12 +525,17 @@ let bfvisit ~pp_term top_split test t = | [] -> 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) + prerr_endline ("visiting t0 = " ^ pp_term t0); + if test t0 then (prerr_endline "t0 is ambiguous"; 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*))) + (* + (prerr_endline ("splitting not ambiguous t0:"); + let t0' = split ctx0 t0 in + List.iter (fun (ctx',t') -> prerr_endline ("-- subnode " ^ + (pp_term t'))) t0'; + aux (tl@t0')) *) + let t0' = split ctx0 t0 in + aux (tl@t0') (* in aux [(fun x -> x),t] *) in aux (top_split t) ;; @@ -520,44 +559,11 @@ 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) + | Ast.Ident (id,_) -> DisambiguateTypes.Id id + | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol sym + | Ast.Num (n,_) -> DisambiguateTypes.Num + | Ast.Case(_,Some (ityname,_),_,_) -> DisambiguateTypes.Id ityname | _ -> assert false ;; @@ -570,19 +576,22 @@ let ast_of_alias_spec t alias = match (t,alias) with | _ -> assert false ;; -let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri +let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~universe ~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 + interpretate_thing ~context ~env ~universe ~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 + | Ko x -> + let _,err = Lazy.force x in + prerr_endline ("test_interpr error: " ^ err); + false | _ -> true with (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) @@ -600,18 +609,18 @@ let rec disambiguate_list ~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 + ~env ~universe ~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" + | GrafiteAst.Ident_alias (_id,uri) -> uri + | GrafiteAst.Symbol_alias (_id,_,desc) -> desc + | GrafiteAst.Number_alias (_,desc) -> desc in let d2s = function - | Id (id,_) - | Symbol (id,_) -> id - | Num _ -> "NUM" + | Id id + | Symbol id -> id + | Num -> "NUM" in let res = Environment.find item universe @@ -632,18 +641,12 @@ let rec disambiguate_list match ts with | [] -> None | t0 :: tl -> - prerr_endline ("disambiguation of t0 = " ^ pp_thing t0); + prerr_endline ("disambiguate_list: 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 ) + | Ast.Case (_,Some (ity,None),_,_) -> true | _ -> false in let astpp = function @@ -655,50 +658,24 @@ let rec disambiguate_list (* 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); + prerr_endline ("visit -- not ambiguous node:\n" ^ pp_thing t0); Some (t0,tl) | Some (ctx, t) -> - prerr_endline ("disambiguating node " ^ astpp t ^ + prerr_endline ("visit -- found ambiguous node: " ^ astpp t ^ "\nin " ^ pp_thing (ctx t)); (* get possible instantiations of t *) let instances = get_instances ctx t in + prerr_endline ("-- possible instances:"); + List.iter + (fun u0 -> prerr_endline ("-- instance: " ^ (pp_thing u0))) instances; (* perforate ambiguous subterms and test refinement *) + prerr_endline ("-- survivors:"); let survivors = List.filter test_interpr instances in + List.iter + (fun u0 -> prerr_endline ("-- survivor: " ^ (pp_thing u0))) survivors; 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 @@ -709,22 +686,10 @@ let disambiguate_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 env = aliases in let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty - ~env ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl + ~env ~universe ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl in (* real function *) let rec aux tl = @@ -738,323 +703,38 @@ let disambiguate_thing 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' + prerr_endline "before interpretate_thing"; + let t' = + interpretate_thing ~context ~env ~universe ~uri ~is_path:false t ~localization_tbl + in + prerr_endline "after interpretate_thing"; + match refine_thing metasenv subst context uri ~use_coercions t' expty + base_univ ~localization_tbl with + | Ok (t',m',s',u') -> t,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,[])) + if not (test_interpr thing) then + (prerr_endline ("preliminary test fail: " ^ pp_thing thing); + raise (NoWellTypedInterpretation (0,[]))) else let res = aux [thing] in let res = - HExtlib.filter_map (fun t -> try Some (refine t) with _ -> None) res + HExtlib.filter_map (fun t -> + try Some (refine t) + with _ -> prerr_endline ("can't interpretate/refine " ^ (pp_thing t));None) res in match res with | [] -> raise (NoWellTypedInterpretation (0,[])) | [t] -> res,false - | _ -> res,true + | _ -> + let choices = List.map (fun (t,_,_,_,_) -> pp_thing t) res in + let user_choice = interactive_ast_choice choices in + [ List.nth res user_choice ], true + (* let pp_thing (t,_,_,_,_,_) = prerr_endline ("interpretation: " ^ (pp_thing t)) in + List.iter pp_thing res; res,true *) ;; -(* -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 ~domain_of_thing ~interpretate_thing ~refine_thing - ~mk_localization_tbl - (thing_txt,thing_txt_prefix_len,thing) -= - debug_print (lazy "DISAMBIGUATE INPUT"); - debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); - let thing_dom = - domain_of_thing ~context:(string_context_of_context context) thing in - debug_print - (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom))); - let current_dom = - Environment.fold (fun item _ dom -> item :: dom) aliases [] in - let todo_dom = domain_diff thing_dom current_dom in - debug_print - (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom))); - (* (2) lookup function for any item (Id/Symbol/Num) *) - let lookup_choices = - fun item -> - match universe with - | None -> - lookup_in_library - interactive_user_uri_choice - input_or_locate_uri item - | Some e -> - (try - fix_instance item (Environment.find item e) - with Not_found -> []) - in - - (* items with 1 choice are interpreted ASAP *) - let aliases, todo_dom = - let rec aux (aliases,acc) = function - | [] -> aliases, acc - | (Node (_, item,extra) as node) :: tl -> - let choices = lookup_choices item in - if List.length choices <> 1 then aux (aliases, acc@[node]) tl - else - let tl = tl @ extra in - if Environment.mem item aliases then aux (aliases, acc) tl - else aux (Environment.add item (List.hd choices) aliases, acc) tl - in - aux (aliases,[]) todo_dom - in - -(* - (* *) - let _ = - if benchmark then begin - let per_item_choices = - List.map - (fun dom_item -> - try - let len = List.length (lookup_choices dom_item) in - debug_print (lazy (sprintf "BENCHMARK %s: %d" - (string_of_domain_item dom_item) len)); - len - with No_choices _ -> 0) - thing_dom - in - max_refinements := List.fold_left ( * ) 1 per_item_choices; - actual_refinements := 0; - domain_size := List.length thing_dom; - choices_avg := - (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size) - end - in - (* *) -*) - - (* (3) test an interpretation filling with meta uninterpreted identifiers - *) - let test_env aliases todo_dom ugraph = - try - let rec aux 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 (aux env l) tl in - let filled_env = aux aliases todo_dom in - let localization_tbl = mk_localization_tbl 503 in - let cic_thing = - interpretate_thing ~context ~env:filled_env - ~uri ~is_path:false thing ~localization_tbl - in -let foo () = - refine_thing metasenv subst context uri - ~use_coercions cic_thing expty ugraph ~localization_tbl -in refine_profiler.HExtlib.profile foo () - with - | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) - | Invalid_choice loc_msg -> Ko loc_msg - in - (* (4) build all possible interpretations *) - let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in - (* aux returns triples Ok/Uncertain/Ko *) - (* rem_dom is the concatenation of all the remainin domains *) - let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom = - debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom)); - match todo_dom with - | [] -> - assert (lookup_in_todo_dom = None); - (match test_env aliases rem_dom base_univ with - | Ok (thing, metasenv,subst,new_univ) -> - [ aliases, diff, metasenv, subst, thing, new_univ ], [], [] - | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true] - | Uncertain loc_msg -> - [],[aliases,diff,loc_msg],[]) - | Node (locs,item,inner_dom) :: remaining_dom -> - debug_print (lazy (sprintf "CHOOSED ITEM: %s" - (string_of_domain_item item))); - let choices = - match lookup_in_todo_dom with - None -> lookup_choices item - | Some choices -> choices in - match choices with - [] -> - [], [], - [aliases, diff, - (lazy (List.hd locs, - "No choices for " ^ string_of_domain_item item)), - true] -(* - | [codomain_item] -> - (* just one choice. We perform a one-step look-up and - if the next set of choices is also a singleton we - skip this refinement step *) - debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); - let new_env = Environment.add item codomain_item aliases in - let new_diff = (item,codomain_item)::diff in - let lookup_in_todo_dom,next_choice_is_single = - match remaining_dom with - [] -> None,false - | (_,he)::_ -> - let choices = lookup_choices he in - Some choices,List.length choices = 1 - in - if next_choice_is_single then - aux new_env new_diff lookup_in_todo_dom remaining_dom - base_univ - else - (match test_env new_env remaining_dom base_univ with - | Ok (thing, metasenv),new_univ -> - (match remaining_dom with - | [] -> - [ new_env, new_diff, metasenv, thing, new_univ ], [] - | _ -> - aux new_env new_diff lookup_in_todo_dom - remaining_dom new_univ) - | Uncertain (loc,msg),new_univ -> - (match remaining_dom with - | [] -> [], [new_env,new_diff,loc,msg,true] - | _ -> - aux new_env new_diff lookup_in_todo_dom - remaining_dom new_univ) - | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true]) -*) - | _::_ -> - let mark_not_significant failures = - List.map - (fun (env, diff, loc_msg, _b) -> - env, diff, loc_msg, false) - failures in - let classify_errors ((ok_l,uncertain_l,error_l) as outcome) = - if ok_l <> [] || uncertain_l <> [] then - ok_l,uncertain_l,mark_not_significant error_l - else - outcome in - let rec filter = function - | [] -> [],[],[] - | codomain_item :: tl -> - (*debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));*) - let new_env = Environment.add item codomain_item aliases in - let new_diff = (item,codomain_item)::diff in - (match - test_env new_env - (inner_dom@remaining_dom@rem_dom) base_univ - with - | Ok (thing, metasenv,subst,new_univ) -> -(* prerr_endline "OK"; *) - let res = - (match inner_dom with - | [] -> - [new_env,new_diff,metasenv,subst,thing,new_univ], - [], [] - | _ -> - aux new_env new_diff None inner_dom - (remaining_dom@rem_dom) - ) - in - res @@ filter tl - | Uncertain loc_msg -> -(* prerr_endline ("UNCERTAIN"); *) - let res = - (match inner_dom with - | [] -> [],[new_env,new_diff,loc_msg],[] - | _ -> - aux new_env new_diff None inner_dom - (remaining_dom@rem_dom) - ) - in - res @@ filter tl - | Ko loc_msg -> -(* prerr_endline "KO"; *) - let res = [],[],[new_env,new_diff,loc_msg,true] in - res @@ filter tl) - in - let ok_l,uncertain_l,error_l = - classify_errors (filter choices) - in - let res_after_ok_l = - List.fold_right - (fun (env,diff,_,_,_,_) res -> - aux env diff None remaining_dom rem_dom @@ res - ) ok_l ([],[],error_l) - in - List.fold_right - (fun (env,diff,_) res -> - aux env diff None remaining_dom rem_dom @@ res - ) uncertain_l res_after_ok_l - in - let aux' aliases diff lookup_in_todo_dom todo_dom = - if todo_dom = [] then - aux aliases diff lookup_in_todo_dom todo_dom [] - else - match test_env aliases todo_dom base_univ with - | Ok _ - | Uncertain _ -> - aux aliases diff lookup_in_todo_dom todo_dom [] - | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] - in - let res = - match aux' aliases [] None todo_dom with - | [],uncertain,errors -> - let errors = - List.map - (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true) - ) uncertain @ errors - in - let errors = - List.map - (fun (env,diff,loc_msg,significant) -> - let env' = - filter_map_domain - (fun locs domain_item -> - try - let description = - description_of_alias (Environment.find domain_item env) - in - Some (locs,descr_of_domain_item domain_item,description) - with - Not_found -> None) - thing_dom - in - let diff= List.map (fun a,b -> a,description_of_alias b) diff in - env',diff,loc_msg,significant - ) errors - in - raise (NoWellTypedInterpretation (0,errors)) - | [_,diff,metasenv,subst,t,ugraph],_,_ -> - debug_print (lazy "SINGLE INTERPRETATION"); - [diff,metasenv,subst,t,ugraph], false - | l,_,_ -> - debug_print - (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); - let choices = - List.map - (fun (env, _, _, _, _, _) -> - map_domain - (fun locs domain_item -> - let description = - description_of_alias (Environment.find domain_item env) - in - locs,descr_of_domain_item domain_item, description) - thing_dom) - l - in - let choosed = - interactive_interpretation_choice - thing_txt thing_txt_prefix_len choices - in - (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u) - choosed), - true - in - res - *) diff --git a/matitaB/components/disambiguation/disambiguate.mli b/matitaB/components/disambiguation/disambiguate.mli index 43fe7a717..bb20ff866 100644 --- a/matitaB/components/disambiguation/disambiguate.mli +++ b/matitaB/components/disambiguation/disambiguate.mli @@ -64,6 +64,9 @@ val set_choose_uris_callback: val set_choose_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type -> unit +val set_choose_disamb_callback: + DisambiguateTypes.interactive_ast_choice_type -> unit + (** @raise Ambiguous_input if called, default value for internal * choose_uris_callback if not set otherwise with set_choose_uris_callback * above *) @@ -75,9 +78,10 @@ val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type val resolve : - env:'alias DisambiguateTypes.Environment.t -> - mk_choice:('alias -> 'term DisambiguateTypes.codomain_item) -> - DisambiguateTypes.Environment.key -> + env:'alias1 DisambiguateTypes.InterprEnv.t -> + universe: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t -> + mk_choice:('alias1 -> 'term DisambiguateTypes.codomain_item) -> + DisambiguateTypes.InterprEnv.key -> 'alias1 option -> [`Num_arg of string | `Args of 'term list] -> 'term val find_in_context: string -> string option list -> int @@ -86,33 +90,6 @@ 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 -> @@ -124,7 +101,7 @@ val disambiguate_thing: mk_implicit:(bool -> 'alias) -> description_of_alias:('alias -> string) -> fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> - aliases:'alias DisambiguateTypes.Environment.t -> + aliases:'alias DisambiguateTypes.InterprEnv.t -> universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> @@ -137,7 +114,8 @@ val disambiguate_thing: domain_of_thing:(context: string option list -> 'ast_thing -> domain) -> interpretate_thing:( context:'context -> - env:'alias DisambiguateTypes.Environment.t -> + env:'alias DisambiguateTypes.InterprEnv.t -> + universe: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t -> uri:'uri -> is_path:bool -> 'ast_thing -> @@ -152,9 +130,7 @@ val disambiguate_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 + ('ast_thing * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool val bfvisit : pp_term:(NotationPt.term -> string) -> diff --git a/matitaB/components/disambiguation/disambiguateTypes.ml b/matitaB/components/disambiguation/disambiguateTypes.ml index 8db0c220d..4e74e4a3d 100644 --- a/matitaB/components/disambiguation/disambiguateTypes.ml +++ b/matitaB/components/disambiguation/disambiguateTypes.ml @@ -25,23 +25,31 @@ (* $Id$ *) +(* type domain_item = | 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 module OrderedDomain = struct type t = domain_item + (* + let compare a b = + match a,b with + | Id (x,None), Id (y,_) + | Id (x,_), Id (y,None) when x = y -> 0 + | Symbol (x,None), Symbol (y,_) + | Symbol (x,_), Symbol (y,None) when x = y -> 0 + | _ -> Pervasives.compare a b *) let compare = Pervasives.compare end @@ -54,40 +62,19 @@ struct let find k env = try find k env - with Not_found -> + 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 + *) raise Not_found 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 - 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 default_dom_item x = x in let env' = try - let current = find k env in + let current = Environment'.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 -> @@ -104,6 +91,14 @@ struct end +module InterprOD = + struct + type t = Stdpp.location + let compare = Pervasives.compare + end + +module InterprEnv = Map.Make (InterprOD) + type 'term codomain_item = string * (* description *) [`Num_interp of string -> 'term @@ -119,9 +114,12 @@ type interactive_user_uri_choice_type = type interactive_interpretation_choice_type = string -> int -> (Stdpp.location list * string * string) list list -> int list +type interactive_ast_choice_type = string list -> int + type input_or_locate_uri_type = title:string -> ?id:string -> unit -> NReference.reference option +(* let string_of_domain_item item = let f_opt f x default = match x with @@ -131,7 +129,20 @@ let string_of_domain_item item = 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 + | Symbol (s,None) -> Printf.sprintf "SYMBOL(%s)" s + | Symbol (s,Some (_,dsc)) -> Printf.sprintf "SYMBOL(%s,%s)" s dsc | Num _ -> "NUM" ;; - +*) +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 -> + Printf.sprintf "ID(%s)" s + | Symbol s -> Printf.sprintf "SYMBOL(%s)" s + | Num -> "NUM" +;; diff --git a/matitaB/components/disambiguation/disambiguateTypes.mli b/matitaB/components/disambiguation/disambiguateTypes.mli index 5ebc835cb..0f557b1ea 100644 --- a/matitaB/components/disambiguation/disambiguateTypes.mli +++ b/matitaB/components/disambiguation/disambiguateTypes.mli @@ -22,11 +22,16 @@ * For details, see the HELM World-Wide-Web page, * http://helm.cs.unibo.it/ *) - +(* type domain_item = | 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 (* module Domain: Set.S with type elt = domain_item *) module Environment: @@ -35,7 +40,12 @@ sig val cons: ('b -> 'a) -> domain_item -> 'b -> 'b list t -> 'b list t end - (** to be raised when a choice is invalid due to some given parameter (e.g. +module InterprEnv: +sig + include Map.S with type key = Stdpp.location +end + +(** to be raised when a choice is invalid due to some given parameter (e.g. * wrong number of Cic.term arguments received) *) exception Invalid_choice of (Stdpp.location * string) Lazy.t @@ -54,6 +64,8 @@ type interactive_user_uri_choice_type = type interactive_interpretation_choice_type = string -> int -> (Stdpp.location list * string * string) list list -> int list +type interactive_ast_choice_type = string list -> int + type input_or_locate_uri_type = title:string -> ?id:string -> unit -> NReference.reference option diff --git a/matitaB/components/disambiguation/multiPassDisambiguator.ml b/matitaB/components/disambiguation/multiPassDisambiguator.ml index f35b1d8d2..2edd1bd69 100644 --- a/matitaB/components/disambiguation/multiPassDisambiguator.ml +++ b/matitaB/components/disambiguation/multiPassDisambiguator.ml @@ -61,6 +61,7 @@ let passes () = (* *) ] ;; +(* XXX is this useful anymore? *) let drop_aliases ?(minimize_instances=false) ~description_of_alias (choices, user_asked) = @@ -73,6 +74,7 @@ let drop_aliases ?(minimize_instances=false) ~description_of_alias let rec aux = function [] -> [] +(* now it's ALWAYS None | (D.Symbol (s,n),ci1) as he::tl when n <> None -> if List.for_all @@ -91,23 +93,23 @@ let drop_aliases ?(minimize_instances=false) ~description_of_alias then (D.Num None,ci1)::(aux tl) else - he::(aux tl) + he::(aux tl) *) | he::tl -> he::(aux tl) in aux d in - (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices), + (List.map (fun (t, d, a, b, c, e) -> t, minimize d, a, b, c, e) choices), user_asked let drop_aliases_and_clear_diff (choices, user_asked) = - (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices), + (List.map (fun (t,_, a, b, c, d) -> t,[], a, b, c, d) choices), user_asked -let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~visit ~f thing +(*let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~visit ~f thing = - let library = false, DisambiguateTypes.Environment.empty, + let library = false, DisambiguateTypes.InterprEnv.empty, DisambiguateTypes.Environment.empty in - let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in + let multi_aliases = false, DisambiguateTypes.InterprEnv.empty, universe in let mono_aliases = true, aliases, DisambiguateTypes.Environment.empty in let passes = List.map @@ -125,7 +127,7 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~visit ~ else if user_asked then drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *) else - drop_aliases_and_clear_diff res + drop_aliases_and_clear_diff res in let rec aux i errors passes = debug_print (lazy ("Pass: " ^ string_of_int i)); @@ -143,7 +145,7 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~visit ~ | [] -> assert false in aux 1 [] passes -;; +;;*) let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst ~string_context_of_context ~initial_ugraph ~expty ~mk_implicit @@ -151,7 +153,8 @@ let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst ~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) = +(* + let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) = let thing = if fresh_instances then freshen_thing thing else thing in Disambiguate.disambiguate_thing ~context ~metasenv ~subst ~use_coercions ~string_context_of_context @@ -162,3 +165,14 @@ let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst in disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~visit ~f thing + *) + try + Disambiguate.disambiguate_thing + ~context ~metasenv ~subst ~use_coercions:true ~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 ~visit + ~mk_localization_tbl ~pp_term thing + with + | Disambiguate.NoWellTypedInterpretation (offset,newerrors) -> + raise (DisambiguationError (offset, [newerrors])) diff --git a/matitaB/components/disambiguation/multiPassDisambiguator.mli b/matitaB/components/disambiguation/multiPassDisambiguator.mli index 41e34e09c..d8e1e3d50 100644 --- a/matitaB/components/disambiguation/multiPassDisambiguator.mli +++ b/matitaB/components/disambiguation/multiPassDisambiguator.mli @@ -51,7 +51,7 @@ val disambiguate_thing: mk_implicit:(bool -> 'alias) -> description_of_alias:('alias -> string) -> fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> - aliases:'alias DisambiguateTypes.Environment.t -> + aliases:'alias DisambiguateTypes.InterprEnv.t -> universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t -> lookup_in_library:( @@ -66,7 +66,8 @@ val disambiguate_thing: (context: string option list -> 'ast_thing -> Disambiguate.domain) -> interpretate_thing:( context:'context -> - env:'alias DisambiguateTypes.Environment.t -> + env:'alias DisambiguateTypes.InterprEnv.t -> + universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t -> uri:'uri -> is_path:bool -> 'ast_thing -> @@ -81,6 +82,4 @@ val disambiguate_thing: ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) -> mk_localization_tbl:(int -> 'cichash) -> string * int * 'ast_thing -> - ((DisambiguateTypes.Environment.key * 'alias) list * - 'metasenv * 'subst * 'refined_thing * 'ugraph) - list * bool + ('ast_thing * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml index ff9d00b81..d2f12dc9d 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 newast,metasenv,subst,status,t = + let metasenv,subst,status,t = GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in assert (metasenv=[]); let t = NCicUntrusted.apply_subst status subst [] t in @@ -79,13 +79,12 @@ let basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern else status in - let mode = GrafiteAst.WithPreferences (*assert false*) in (* MATITA 1.0 VEDI SOTTO *) let diff = (* FIXME! the uri should be filled with something meaningful! *) - [DisambiguateTypes.Symbol (symbol, Some (None,dsc)), + [DisambiguateTypes.Symbol symbol, GrafiteAst.Symbol_alias (symbol,None,dsc)] in - GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff + GrafiteDisambiguate.add_to_disambiguation_univ status diff ;; let inject_interpretation = @@ -116,7 +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 + GrafiteDisambiguate.add_to_disambiguation_univ status diff ;; let inject_alias = @@ -135,8 +134,15 @@ let eval_alias status data= let basic_eval_input_notation (l1,l2) status = GrafiteParser.extend status l1 (fun env loc -> - NotationPt.AttributedTerm - (`Loc loc,TermContentPres.instantiate_level2 status env l2)) + let rec inner_loc default = function + | [] -> default + | (_,(NotationEnv.NoType,NotationEnv.LocValue l))::_ -> l + | _::tl -> inner_loc default tl + in + let inner_loc = inner_loc loc env in + let l2' = TermContentPres.instantiate_level2 status env inner_loc l2 in + prerr_endline ("new l2 ast : " ^ (NotationPp.pp_term status l2')); + NotationPt.AttributedTerm (`Loc loc,l2')) ;; let inject_input_notation = @@ -618,7 +624,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = List.fold_left (fun status (name,cpos,arity) -> try - let newast,metasenv,subst,status,t = + let metasenv,subst,status,t = GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,NotationPt.Ident (name,`Ambiguous)) in assert (metasenv = [] && subst = []); @@ -711,7 +717,7 @@ 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 -> - let newast,metasenv,subst,status,sort = + let metasenv,subst,status,sort = GrafiteDisambiguate.disambiguate_nterm status None [] [] [] (text,prefix_len,s) in metasenv,subst,status,sort @@ -726,7 +732,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 newast,metasenv,subst,status,indty = + let metasenv,subst,status,indty = GrafiteDisambiguate.disambiguate_nterm status None [] [] subst (text,prefix_len,indty) in let indtyno,(_,leftno,tys,_,_) = @@ -757,6 +763,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = in eval_interpretation status (dsc,(symbol, args),cic_appl_pattern) | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) -> + prerr_endline ("new notation: " ^ (NotationPp.pp_term status l1)); let l1 = CicNotationParser.check_l1_pattern l1 (dir = Some `RightToLeft) precedence associativity @@ -773,11 +780,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,Some uri),spec] + [DisambiguateTypes.Id id,spec] | GrafiteAst.Symbol_alias (symb, uri, desc) -> - [DisambiguateTypes.Symbol (symb, Some (uri,desc)),spec] + [DisambiguateTypes.Symbol symb,spec] | GrafiteAst.Number_alias (uri,desc) -> - [DisambiguateTypes.Num (Some (uri,desc)),spec] + [DisambiguateTypes.Num,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/grafiteTypes.ml b/matitaB/components/grafite_engine/grafiteTypes.ml index 7cb6bef0c..bfbb982c7 100644 --- a/matitaB/components/grafite_engine/grafiteTypes.ml +++ b/matitaB/components/grafite_engine/grafiteTypes.ml @@ -41,6 +41,7 @@ class virtual status = fun (b : string) -> inherit ([Continuationals.Stack.t] NTacStatus.status fake_obj (Continuationals.Stack.empty)) inherit NCicLibrary.dumpable_status inherit NCicLibrary.status + inherit GrafiteDisambiguate.status inherit GrafiteParser.status inherit TermContentPres.status val baseuri = b diff --git a/matitaB/components/grafite_engine/grafiteTypes.mli b/matitaB/components/grafite_engine/grafiteTypes.mli index 92d4cc2aa..90fdbb52e 100644 --- a/matitaB/components/grafite_engine/grafiteTypes.mli +++ b/matitaB/components/grafite_engine/grafiteTypes.mli @@ -38,6 +38,7 @@ class virtual status : inherit NTacStatus.tac_status inherit NCicLibrary.dumpable_status inherit NCicLibrary.status + inherit GrafiteDisambiguate.status inherit GrafiteParser.status inherit TermContentPres.status method baseuri: string diff --git a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml index 2693d608b..a26d5ec7c 100644 --- a/matitaB/components/grafite_engine/nCicCoercDeclaration.ml +++ b/matitaB/components/grafite_engine/nCicCoercDeclaration.ml @@ -134,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 newast,metasenv,subst,status,src = + let metasenv,subst,status,src = GrafiteDisambiguate.disambiguate_nterm status None ctx [] [] ("",0,src) in let src = NCicUntrusted.apply_subst status subst [] src in @@ -152,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 newast, metasenv,subst,status,tgt = + let metasenv,subst,status,tgt = GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,tgt) in let tgt = NCicUntrusted.apply_subst status subst [] tgt in @@ -319,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 newast_ty,metasenv,subst,status,ty = + let metasenv,subst,status,ty = GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in assert (metasenv=[]); let ty = NCicUntrusted.apply_subst status subst [] ty in - let newast_t,metasenv,subst,status,t = + let 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/library/librarian.ml b/matitaB/components/library/librarian.ml index 9ffde2b87..899a9a6a5 100644 --- a/matitaB/components/library/librarian.ml +++ b/matitaB/components/library/librarian.ml @@ -112,7 +112,8 @@ let find_root_for ~include_paths file = let mk_baseuri root extra = let chop name = assert(Filename.check_suffix name ".ma" || - Filename.check_suffix name ".mma"); + Filename.check_suffix name ".mma" || + Filename.check_suffix name ".mad"); try Filename.chop_extension name with Invalid_argument "Filename.chop_extension" -> name in diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml index cbe14f9d5..0cadc45b7 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml @@ -25,16 +25,24 @@ (* $Id$ *) +module Ast = NotationPt + type db = { - aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t; + (* maps (loc,domain_item) to alias *) + interpr: GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t; + (* the universe of possible interpretations for all symbols/ids/nums *) multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t; - new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list + (* new_aliases: ((Stdpp.location * DisambiguateTypes.domain_item) * GrafiteAst.alias_spec) list *) } +let get_interpr db = + db.interpr +;; + let initial_status = { - aliases = DisambiguateTypes.Environment.empty; + interpr = DisambiguateTypes.InterprEnv.empty; multi_aliases = DisambiguateTypes.Environment.empty; - new_aliases = [] + (* new_aliases = [] *) } class type g_status = @@ -54,28 +62,31 @@ class virtual status = = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db) end -let eval_with_new_aliases status f = +(* let eval_with_new_aliases status f = let status = status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in let res = f status in let new_aliases = status#disambiguate_db.new_aliases in new_aliases,res -;; +;;*) let dump_aliases out msg status = out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:"); - DisambiguateTypes.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x)) - status#disambiguate_db.aliases + DisambiguateTypes.InterprEnv.iter (fun _ x -> out (GrafiteAstPp.pp_alias x)) + status#disambiguate_db.interpr + +let add_to_interpr status new_aliases = + let interpr = + List.fold_left (fun acc (k,c) -> + DisambiguateTypes.InterprEnv.add k c acc) + status#disambiguate_db.interpr new_aliases + in + let new_status = + {status#disambiguate_db with interpr = interpr } + in + status#set_disambiguate_db new_status -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 +let add_to_disambiguation_univ status new_aliases = let multi_aliases = List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias @@ -83,13 +94,10 @@ let set_proof_aliases status ~implicit_aliases mode new_aliases = status#disambiguate_db.multi_aliases new_aliases in let new_status = - {multi_aliases = multi_aliases ; - aliases = aliases; - new_aliases = - (if implicit_aliases then new_aliases else []) @ - status#disambiguate_db.new_aliases} + {status#disambiguate_db with multi_aliases = multi_aliases } in - status#set_disambiguate_db new_status) + status#set_disambiguate_db new_status + exception BaseUriNotSetYet @@ -105,13 +113,18 @@ let singleton msg = function let __Implicit = "__Implicit__" let __Closed_Implicit = "__Closed_Implicit__" -let ncic_mk_choice status = function +let ncic_mk_choice status a = + prerr_endline "ncic_mk_choice"; + match a with | GrafiteAst.Symbol_alias (name,_, dsc) -> + prerr_endline ("caso 1: " ^ name ^ "; " ^ dsc); if name = __Implicit then dsc, `Sym_interp (fun _ -> NCic.Implicit `Term) else if name = __Closed_Implicit then dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed) else + (prerr_endline (Printf.sprintf "mk_choice: symbol %s, interpr %s" + name dsc); DisambiguateChoices.lookup_symbol_by_dsc status ~mk_implicit:(function | true -> NCic.Implicit `Closed @@ -119,12 +132,14 @@ let ncic_mk_choice status = function ~mk_appl:(function (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l) ~term_of_nref:(fun nref -> NCic.Const nref) - name dsc + name dsc) | GrafiteAst.Number_alias (_,dsc) -> + prerr_endline ("caso 2: " ^ 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) | GrafiteAst.Ident_alias (name, uri) -> + prerr_endline ("caso 3: " ^ name); uri, `Sym_interp (fun l->assert(l = []); let nref = NReference.reference_of_string uri in @@ -144,7 +159,7 @@ 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 @@ -175,14 +190,114 @@ let nlookup_in_library ;;*) let fix_instance _ l = l;; +let rec diff_term loc t u = match (t,u) with + | Ast.AttributedTerm (`Loc l,t'), Ast.AttributedTerm (_,u') -> diff_term l t' u' + | Ast.AttributedTerm (_,t'), Ast.AttributedTerm (_,u') -> diff_term loc t' u' + | Ast.Appl tl, Ast.Appl ul -> + List.fold_left2 (fun acc t0 u0 -> diff_term loc t0 u0@acc) [] tl ul + | Ast.Binder (_,v1,b1), Ast.Binder (_,v2,b2) -> + diff_var loc v1 v2@ diff_term loc b1 b2 + | Ast.Case (t1,ity1,outty1,pl1),Ast.Case (t2,ity2,outty2,pl2) -> + let ity_interp = match ity1,ity2 with + | Some (i,None), Some (_,Some r) -> + let uri = NReference.string_of_reference r in + [loc,GrafiteAst.Ident_alias (i,uri)] + | _ -> [] + in + let oty_interp = match outty1,outty2 with + | Some o1, Some o2 -> diff_term loc o1 o2 + | _ -> [] + in + (* pl = (case_pattern * term) list *) + let auxpatt (c1,u1) (c2,u2) acc = + let diff_cp = match c1,c2 with + | Ast.Pattern (i,href1,vars1), Ast.Pattern (_,href2,vars2) -> + let diff_i = match href1,href2 with + | None, Some r -> + let uri = NReference.string_of_reference r in + [loc,GrafiteAst.Ident_alias (i,uri)] + | _ -> [] + in + let diff_vars = + List.fold_right2 (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 [] + in + diff_i @ diff_vars + | _ -> [] + in + diff_term loc u1 u2 @ diff_cp @ acc + in + let pl_interp = List.fold_right2 auxpatt pl1 pl2 [] in + diff_term loc t1 t2 @ ity_interp @ oty_interp @ pl_interp + | Ast.Cast (u1,v1),Ast.Cast (u2,v2) -> + diff_term loc u1 u2@diff_term loc v1 v2 + | Ast.LetIn (var1,u1,v1),Ast.LetIn (var2,u2,v2) -> + diff_var loc var1 var2 @ diff_term loc u1 u2 @ diff_term loc v1 v2 + | Ast.LetRec (_,fl1,w1),Ast.LetRec (_,fl2,w2) -> + let diff_funs = + List.fold_right2 + (fun (vars1,f1,b1,_) (vars2,f2,b2,_) acc -> + let diff_vars = + List.fold_right2 + (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 [] + in + diff_vars @ diff_var loc f1 f2 @ diff_term loc b1 b2 @ acc) + fl1 fl2 [] + in + diff_funs @ diff_term loc w1 w2 + | Ast.Ident (n,`Ambiguous),Ast.Ident (_,`Uri u) -> + [loc,GrafiteAst.Ident_alias (n,u)] + | Ast.Symbol (s, None),Ast.Symbol(_,Some (uri,desc)) -> + [loc,GrafiteAst.Symbol_alias (s,uri,desc)] + | Ast.Num (_, None),Ast.Num (_,Some (uri,desc)) -> + [loc,GrafiteAst.Number_alias (uri,desc)] + | _ -> [] (* leaves *) +and diff_var loc (_,v1) (_,v2) = match v1,v2 with + | Some v1', Some v2' -> diff_term loc v1' v2' + | _ -> [] +;; + +let diff_obj loc o1 o2 = match o1,o2 with + | Ast.Inductive (ls1,itys1), Ast.Inductive (ls2,itys2) -> + let diff_ls = + List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 [] + in + let diff_itys = + List.fold_right2 + (fun (i1,_,ty1,cl1) (i2,_,ty2,cl2) acc0 -> + let diff_cl = + List.fold_right2 + (fun (_,u) (_,v) acc1 -> diff_term loc u v @ acc1) + cl1 cl2 [] + in + diff_term loc ty1 ty2 @ diff_cl @ acc0) + itys1 itys2 [] + in + diff_ls @ diff_itys + | Ast.Theorem (_,i1,b1,ty1,_), Ast.Theorem (_,i2,b2,ty2,_) -> + let diff_tys = match ty1,ty2 with + | Some ty1', Some ty2' -> diff_term loc ty1' ty2' + | _ -> [] + in + diff_term loc b1 b2 @ diff_tys + | Ast.Record (ls1,_,ty1,fl1),Ast.Record (ls2,_,ty2,fl2) -> + let diff_ls = + List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 [] + in + let diff_fl = + List.fold_right2 + (fun (_,f1,_,_) (_,f2,_,_) acc -> diff_term loc f1 f2 @ acc) fl1 fl2 [] + in + diff_ls @ diff_term loc ty1 ty2 @ diff_fl + | _ -> assert false +;; let disambiguate_nterm status expty context metasenv subst thing = - let newast, diff, metasenv, subst, cic = + let newast, metasenv, subst, cic = singleton "first" (NCicDisambiguate.disambiguate_term status - ~aliases:status#disambiguate_db.aliases + ~aliases:status#disambiguate_db.interpr ~expty ~universe:(status#disambiguate_db.multi_aliases) ~lookup_in_library:nlookup_in_library @@ -191,11 +306,11 @@ let disambiguate_nterm status expty context metasenv subst thing ~description_of_alias:GrafiteAst.description_of_alias ~context ~metasenv ~subst thing) in - let status = - set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences - diff + let _,_,thing' = thing in + let diff = diff_term Stdpp.dummy_loc thing' newast in + let status = add_to_interpr status diff in - newast, metasenv, subst, status, cic + metasenv, subst, status, cic ;; @@ -260,7 +375,7 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = in NUri.uri_of_string (baseuri ^ "/" ^ name) in - let diff, _, _, cic = + let ast, _, _, cic = singleton "third" (NCicDisambiguate.disambiguate_obj status @@ -268,12 +383,11 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = ~description_of_alias:GrafiteAst.description_of_alias ~mk_choice:(ncic_mk_choice status) ~mk_implicit ~fix_instance ~uri - ~aliases:status#disambiguate_db.aliases + ~aliases:status#disambiguate_db.interpr ~universe:(status#disambiguate_db.multi_aliases) (text,prefix_len,obj)) in - let status = - set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences - diff + let diff = diff_obj Stdpp.dummy_loc obj ast in + let status = add_to_interpr status diff in status, cic ;; @@ -288,14 +402,16 @@ let disambiguate_cic_appl_pattern status args = (List.exists (function (NotationPt.IdentArg (_,id')) -> id'=id) args) -> - let item = DisambiguateTypes.Id (id,None) in + let item = DisambiguateTypes.Id id in begin try match DisambiguateTypes.Environment.find item - status#disambiguate_db.aliases + (* status#disambiguate_db.aliases *) + status#disambiguate_db.multi_aliases with - GrafiteAst.Ident_alias (_,uri) -> + (* XXX : we only try the first match *) + GrafiteAst.Ident_alias (_,uri)::_ -> NotationPt.NRefPattern (NReference.reference_of_string uri) | _ -> assert false with Not_found -> @@ -320,6 +436,8 @@ let aliases_for_objs status refs = List.map (fun u -> let name = NCicPp.r2s status true u in - DisambiguateTypes.Id (name, Some (NReference.string_of_reference u)), + (* FIXME : we are forgetting the interpretation of the Id + * but is this useful anymore?!?!? *) + DisambiguateTypes.Id name, 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 c75cfb3a5..0babba272 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli @@ -39,15 +39,20 @@ class virtual status : method set_disambiguate_status: #g_status -> 'self end -val eval_with_new_aliases: +(* val eval_with_new_aliases: #status as 'status -> ('status -> 'a) -> - (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list * 'a + ((Stdpp.location * DisambiguateTypes.domain_item) * GrafiteAst.alias_spec) list * 'a +*) -val set_proof_aliases: +val get_interpr : db -> GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t + +val add_to_interpr: + #status as 'status -> + (Stdpp.location * GrafiteAst.alias_spec) list -> 'status + +val add_to_disambiguation_univ: #status as 'status -> - implicit_aliases:bool -> (* implicit ones are made explicit *) - GrafiteAst.inclusion_mode -> - (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status + (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status val aliases_for_objs: #NCic.status -> NUri.uri list -> @@ -62,12 +67,12 @@ val disambiguate_nterm : #status as 'status -> NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution -> NotationPt.term Disambiguate.disambiguator_input -> - NotationPt.term * NCic.metasenv * NCic.substitution * 'status * NCic.term + NCic.metasenv * NCic.substitution * 'status * NCic.term val disambiguate_nobj : #status as 'status -> ?baseuri:string -> (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input -> - 'status * NCic.obj + 'status * NCic.obj type pattern = NotationPt.term Disambiguate.disambiguator_input option * diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml index b34a2ec8b..b9ea25cfa 100644 --- a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml @@ -104,9 +104,11 @@ let find_in_context name context = aux 1 context let interpretate_term_and_interpretate_term_option (status: #NCic.status) - ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~uri ~is_path + ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~universe ~uri ~is_path ~localization_tbl = + let _ = (mk_choice : GrafiteAst.alias_spec -> NCic.term + DisambiguateTypes.codomain_item) in (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); @@ -123,11 +125,22 @@ 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) -> + | NotationPt.Appl (NotationPt.Symbol (symb, None) :: args) + | NotationPt.Appl + (NotationPt.AttributedTerm (_,NotationPt.Symbol (symb,None))::args) -> NCic.Implicit `Term - | NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) -> + | NotationPt.Appl (NotationPt.Symbol (symb, Some(uri,desc)) :: args) + | NotationPt.Appl (NotationPt.AttributedTerm + (_,NotationPt.Symbol (symb,Some (uri,desc)))::args) -> let cic_args = List.map (aux ~localize loc context) args in - Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args) + (try + prerr_endline ("interpr Appl/Sym: " ^ symb); + let interpr = Some (GrafiteAst.Symbol_alias (symb, uri, desc)) in + Disambiguate.resolve ~mk_choice ~env ~universe (loc (*, Symbol symb*)) + interpr (`Args cic_args) + with Failure err -> + prerr_endline ("resolve of " ^ symb ^ " failed: " ^ err); + assert false) | NotationPt.Appl terms -> NCic.Appl (List.map (aux ~localize loc context) terms) | NotationPt.Binder (binder_kind, (var, typ), body) -> @@ -182,11 +195,14 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) raise (Disambiguate.Try_again (lazy "The type of the term to be matched is still unknown")) | None -> - let rec fst_constructor = + let rec fst_constructor concrete_pat_found = function - (Ast.Pattern (head, href, _), _) :: _ -> - head, HExtlib.map_option NReference.string_of_reference href - | (Ast.Wildcard, _) :: tl -> fst_constructor tl + | (Ast.Pattern (_, None,_),_)::tl -> fst_constructor true tl + | (Ast.Pattern (head, Some href, _), _) :: _ -> + head, href + | (Ast.Wildcard, _) :: tl -> fst_constructor concrete_pat_found tl + | [] when concrete_pat_found -> raise (Disambiguate.Try_again + (lazy "The type of the term to be matched is still unknown")) | [] -> raise (Invalid_choice (lazy (loc,"The type "^ "of the term to be matched cannot be determined "^ "because it is an inductive type without constructors "^ @@ -199,19 +215,10 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) (DisambiguateTypes.string_of_domain_item k ^ " => " ^ description_of_alias v)) env; *) - (match Disambiguate.resolve ~env ~mk_choice - (Id (fst_constructor branches)) (`Args []) with - | NCic.Const (NReference.Ref (_,NReference.Con _) as r) -> - let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in - NReference.mk_indty b 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)))) + let kname,href = fst_constructor false branches in + let b,_,_,_,_ = NCicEnvironment.get_checked_indtys status href + in + NReference.mk_indty b href in let _,leftsno,itl,_,indtyp_no = NCicEnvironment.get_checked_indtys status indtype_ref in @@ -224,7 +231,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) NCic.Prod (_, _, t) -> 1 + (count_prod t) | _ -> 0 in - let rec sort branches cl = + let rec sort cno branches cl = match cl with [] -> let rec analyze unused unrecognized useless = @@ -259,6 +266,34 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) (lazy (loc, "Missing case: " ^ name))) | ((Ast.Wildcard, _) as branch :: _) as branches -> branch, branches + | (Ast.Pattern (name',Some href,_),_) as branch :: tl -> + prerr_endline + (Printf.sprintf "analysis of %s and %s" name name'); + (match href with + | NReference.Ref (curi, (NReference.Con (n,cno',_))) -> + (* check che la curi corrisponda alla uri del tipo induttivo *) + let this_indty = NReference.mk_indty true href in + if indtype_ref <> this_indty then + (prerr_endline "fail1"; + raise (DisambiguateTypes.Invalid_choice + (lazy (loc, Printf.sprintf + "Malformed pattern matching: the matching type is %s, but constructor %s belongs to type %s." + (NReference.string_of_reference indtype_ref) + (NReference.string_of_reference href) + (NReference.string_of_reference this_indty))))) + else + if cno = cno' then (prerr_endline "ok";branch, tl) + else + (prerr_endline (Printf.sprintf "skip %d %d" cno cno'); + let found,rest = find_and_remove tl in + found, branch::rest) + | _ -> + (prerr_endline "fail2"; + raise + (DisambiguateTypes.Invalid_choice + (lazy (loc,"Malformed pattern: found " ^ + (NReference.string_of_reference href) ^ + " which is not a type constructor."))))) | (Ast.Pattern (name',_,_),_) as branch :: tl when name = name' -> branch,tl @@ -270,7 +305,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) match branch with Ast.Pattern (name,y,args),term -> if List.length args = count_prod ty - leftsno then - ((name,y,args),term)::sort tl cltl + ((name,y,args),term)::sort (cno+1) tl cltl else raise (DisambiguateTypes.Invalid_choice @@ -285,9 +320,9 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) mk_lambdas (n - 1)) in (("wildcard",None,[]), - mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl + mk_lambdas (count_prod ty - leftsno)) :: sort (cno+1) tl cltl in - let branches = sort branches cl in + let branches = sort 1 branches cl in NCic.Match (indtype_ref, cic_outtype, cic_term, (List.map do_branch branches)) | NotationPt.Cast (t1, t2) -> @@ -327,9 +362,10 @@ 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.Num (num, i) -> + let i = HExtlib.map_option + (fun (uri,desc) -> GrafiteAst.Number_alias (uri,desc)) i in + Disambiguate.resolve ~env ~universe ~mk_choice (loc(*,Num*)) i (`Num_arg num) | NotationPt.Meta (index, subst) -> let cic_subst = List.map @@ -345,8 +381,12 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) | NotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")]) | NotationPt.Symbol (symbol, instance) -> - Disambiguate.resolve ~env ~mk_choice - (Symbol (symbol, instance)) (`Args []) + let instance = HExtlib.map_option + (fun (uri,desc) -> GrafiteAst.Symbol_alias (symbol, uri, desc)) + instance + in + Disambiguate.resolve ~env ~universe ~mk_choice + (loc (*,Symbol symbol*)) instance (`Args []) | NotationPt.Variable _ | NotationPt.Magic _ | NotationPt.Layout _ @@ -368,24 +408,24 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) (fun ~context -> aux_option ~localize:true HExtlib.dummy_floc context) ;; -let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~uri +let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~universe ~uri ~is_path ast ~obj_context ~localization_tbl ~mk_choice = let context = List.map fst context in fst (interpretate_term_and_interpretate_term_option status - ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path + ~obj_context ~mk_choice ~create_dummy_ids ~env ~universe ~uri ~is_path ~localization_tbl) ~context ast ;; -let interpretate_term_option status ?(create_dummy_ids=false) ~context ~env ~uri - ~is_path ~localization_tbl ~mk_choice ~obj_context +let interpretate_term_option status ?(create_dummy_ids=false) ~context ~env + ~universe ~uri ~is_path ~localization_tbl ~mk_choice ~obj_context = let context = List.map fst context in snd (interpretate_term_and_interpretate_term_option status - ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path + ~obj_context ~mk_choice ~create_dummy_ids ~env ~universe ~uri ~is_path ~localization_tbl) ~context ;; @@ -395,7 +435,8 @@ let disambiguate_path status path = fst (interpretate_term_and_interpretate_term_option status ~obj_context:[] ~mk_choice:(fun _ -> assert false) - ~create_dummy_ids:true ~env:DisambiguateTypes.Environment.empty + ~create_dummy_ids:true ~env:DisambiguateTypes.InterprEnv.empty + ~universe:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true ~localization_tbl) ~context:[] path ;; @@ -406,7 +447,7 @@ let ncic_name_of_ident = function let interpretate_obj status (* ?(create_dummy_ids=false) *) - ~context ~env ~uri ~is_path obj ~localization_tbl ~mk_choice + ~context ~env ~universe ~uri ~is_path obj ~localization_tbl ~mk_choice = assert (context = []); assert (is_path = false); @@ -419,7 +460,7 @@ let interpretate_obj status | NotationPt.Theorem (flavour, name, ty, bo, pragma) -> let ty' = interpretate_term status - ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty + ~obj_context:[] ~context:[] ~env ~universe ~uri:None ~is_path:false ty in let height = (* XXX calculate *) 0 in uri, height, [], [], @@ -454,13 +495,13 @@ let interpretate_obj status in let cic_body = interpretate_term status - ~obj_context ~context ~env ~uri:None ~is_path:false + ~obj_context ~context ~env ~universe ~uri:None ~is_path:false (add_binders `Lambda body) in let cic_type = interpretate_term_option status ~obj_context:[] - ~context ~env ~uri:None ~is_path:false `Type + ~context ~env ~universe ~uri:None ~is_path:false `Type (HExtlib.map_option (add_binders `Pi) typ) in ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body)) @@ -471,7 +512,7 @@ let interpretate_obj status | bo -> let bo = interpretate_term status - ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo + ~obj_context:[] ~context:[] ~env ~universe ~uri:None ~is_path:false bo in let attrs = `Provided, flavour, pragma in NCic.Constant ([],name,Some bo,ty',attrs))) @@ -486,7 +527,7 @@ let interpretate_obj status | Some t -> t in let name = cic_name_of_name name in let t = - interpretate_term status ~obj_context:[] ~context ~env ~uri:None + interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None ~is_path:false t in (name,NCic.Decl t)::context,(name,t)::res @@ -511,14 +552,14 @@ let interpretate_obj status (fun (name,_,ty,cl) -> let ty' = add_params - (interpretate_term status ~obj_context:[] ~context ~env ~uri:None + (interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None ~is_path:false ty) in let cl' = List.map (fun (name,ty) -> let ty' = add_params - (interpretate_term status ~obj_context ~context ~env ~uri:None + (interpretate_term status ~obj_context ~context ~env ~universe ~uri:None ~is_path:false ty) in let relevance = [] in relevance,name,ty' @@ -542,7 +583,7 @@ let interpretate_obj status | Some t -> t in let name = cic_name_of_name name in let t = - interpretate_term status ~obj_context:[] ~context ~env ~uri:None + interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None ~is_path:false t in (name,NCic.Decl t)::context,(name,t)::res @@ -554,7 +595,7 @@ let interpretate_obj status let leftno = List.length params in let ty' = add_params - (interpretate_term status ~obj_context:[] ~context ~env ~uri:None + (interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None ~is_path:false ty) in let nref = NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in @@ -564,7 +605,7 @@ let interpretate_obj status List.fold_left (fun (context,res) (name,ty,_coercion,_arity) -> let ty = - interpretate_term status ~obj_context ~context ~env ~uri:None + interpretate_term status ~obj_context ~context ~env ~universe ~uri:None ~is_path:false ty in let context' = (name,NCic.Decl ty)::context in context',(name,ty)::res @@ -595,6 +636,29 @@ let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc)) | _ -> 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 -> 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 let init = initialize_ast ~universe ~lookup_in_library in let init_var ~local_names (n,ty) = (n,HExtlib.map_option (init ~local_names) ty) @@ -613,40 +677,25 @@ let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names 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') + let uri' = match uri with + | Some _ -> uri + | None -> + let choices = lookup_choices (DisambiguateTypes.Id c) in + if List.length choices <> 1 then None + else (match (List.hd choices) with + | GrafiteAst.Ident_alias (_,u) -> + Some (NReference.reference_of_string u) + | _ -> assert false) + 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 + | Ast.Ident (id,_) -> DisambiguateTypes.Id id + | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol sym + | Ast.Num _ -> DisambiguateTypes.Num | _ -> 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) @@ -671,7 +720,19 @@ let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names 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') + let ity' = HExtlib.map_option + (fun (ity_id,href) -> + let href' = match href with + | None -> + let choices = lookup_choices (DisambiguateTypes.Id ity_id) in + if List.length choices <> 1 then None + else (match (List.hd choices) with + | GrafiteAst.Ident_alias (_,u) -> + Some (NReference.reference_of_string u) + | _ -> assert false) + | Some _ -> href + in (ity_id,href')) ity + 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 @@ -694,7 +755,7 @@ let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names | t -> t ;; -let initialize_obj ~universe ~lookup_in_library o = +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) @@ -726,20 +787,24 @@ let initialize_obj ~universe ~lookup_in_library o = 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) + let ty' = init ~local_names:[] ty in + let bo' = HExtlib.map_option (init ~local_names:[]) bo in + Ast.Theorem (flav,n,ty',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 _,fl' = List.fold_left (fun (ln0,fl0) (fn,fty,b,i) -> + (fn::ln0,(fn,init ~local_names:ln0 fty,b,i)::fl0)) (ln,[]) fl + in + let fl' = List.rev 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 _ = (aliases : GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t) in let local_names = List.map (fun (n,_) -> n) context in let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in let res,b = @@ -758,7 +823,7 @@ let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst ~visit:Disambiguate.bfvisit ~mk_localization_tbl ~expty ~subst in - List.map (function (a,b,c,d,_) -> term,a,b,c,d) res, b + List.map (function (t,a,b,c,_) -> t,a,b,c) res, b ;; @@ -768,6 +833,7 @@ let disambiguate_obj (status: #NCicCoercion.status) = let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in let res,b = + let obj' = initialize_obj ~universe ~lookup_in_library obj in MultiPassDisambiguator.disambiguate_thing ~freshen_thing:NotationUtil.freshen_obj ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases @@ -780,11 +846,11 @@ let disambiguate_obj (status: #NCicCoercion.status) ~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,(initialize_obj ~universe ~lookup_in_library obj)) + (text,prefix_len,obj') ~visit:Disambiguate.bfvisit_obj ~mk_localization_tbl ~expty:None in - List.map (function (a,b,c,d,_) -> a,b,c,d) res, b + List.map (function (o,a,b,c,_) -> o,a,b,c) res, b ;; (* let _ = diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli index 70e89dfbc..6f6bbd1a1 100644 --- a/matitaB/components/ng_disambiguation/nCicDisambiguate.mli +++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.mli @@ -17,20 +17,19 @@ val disambiguate_term : metasenv:NCic.metasenv -> subst:NCic.substitution -> expty:NCic.term option -> - mk_implicit: (bool -> 'alias) -> - description_of_alias:('alias -> string) -> - fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> - mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) -> - aliases:'alias DisambiguateTypes.Environment.t -> + mk_implicit: (bool -> GrafiteAst.alias_spec) -> + description_of_alias:(GrafiteAst.alias_spec -> string) -> + fix_instance:(DisambiguateTypes.domain_item -> GrafiteAst.alias_spec list -> GrafiteAst.alias_spec list) -> + mk_choice:(GrafiteAst.alias_spec -> NCic.term DisambiguateTypes.codomain_item) -> + aliases:GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t -> 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) -> + GrafiteAst.alias_spec list) -> NotationPt.term Disambiguate.disambiguator_input -> (NotationPt.term * - (DisambiguateTypes.domain_item * 'alias) list * NCic.metasenv * NCic.substitution * NCic.term) list * @@ -38,20 +37,21 @@ val disambiguate_term : val disambiguate_obj : #NCicCoercion.status -> - mk_implicit:(bool -> 'alias) -> - description_of_alias:('alias -> string) -> - fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> - mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) -> - aliases:'alias DisambiguateTypes.Environment.t -> + mk_implicit:(bool -> GrafiteAst.alias_spec) -> + description_of_alias:(GrafiteAst.alias_spec -> string) -> + fix_instance:(DisambiguateTypes.domain_item -> GrafiteAst.alias_spec list -> GrafiteAst.alias_spec list) -> + mk_choice:(GrafiteAst.alias_spec -> NCic.term DisambiguateTypes.codomain_item) -> + aliases:GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t -> 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) -> + GrafiteAst.alias_spec list) -> uri:NUri.uri -> string * int * NotationPt.term NotationPt.obj -> - ((DisambiguateTypes.Environment.key * 'alias) list * NCic.metasenv * + (NotationPt.term NotationPt.obj * + NCic.metasenv * NCic.substitution * NCic.obj) list * bool diff --git a/matitaB/components/ng_tactics/nTacStatus.ml b/matitaB/components/ng_tactics/nTacStatus.ml index dc534b430..9a6358baa 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 newast, metasenv, subst, status, t = + let 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/matita/cicMathView.ml b/matitaB/matita/cicMathView.ml index d619482de..685324580 100644 --- a/matitaB/matita/cicMathView.ml +++ b/matitaB/matita/cicMathView.ml @@ -242,7 +242,7 @@ object (self) initializer self#source_buffer#set_language (Some MatitaGtkMisc.matita_lang); self#source_buffer#set_highlight_syntax true; - self#set_editable false; + self#set_editable false; MatitaMisc.observe_font_size (fun size -> self#misc#modify_font_by_name diff --git a/matitaB/matita/lib/arithmetics/nat.ma b/matitaB/matita/lib/arithmetics/nat.ma index 6b3a1a19b..6fa6d57a8 100644 --- a/matitaB/matita/lib/arithmetics/nat.ma +++ b/matitaB/matita/lib/arithmetics/nat.ma @@ -22,7 +22,7 @@ alias num (instance 0) = "natural number". definition pred ≝ λn. match n with [ O ⇒ O | S p ⇒ p]. -theorem pred_Sn : ∀n. n = pred (S n). +theorem pred_Sn : ∀n.n = pred (S n). // qed. theorem injective_S : injective nat nat S. @@ -76,7 +76,7 @@ theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m. // qed. *) -theorem plus_n_O: ∀n:nat. n = n+O. +theorem plus_n_O: ∀n:nat. n = n+0. #n (elim n) normalize // qed. theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m. diff --git a/matitaB/matita/lib/basics/logic.ma b/matitaB/matita/lib/basics/logic.ma index 1b801a14b..fd137d662 100644 --- a/matitaB/matita/lib/basics/logic.ma +++ b/matitaB/matita/lib/basics/logic.ma @@ -19,16 +19,19 @@ inductive eq (A:Type[1]) (x:A) : A → Prop ≝ interpretation "leibnitz's equality" 'eq t x y = (eq t x y). + lemma eq_rect_r: - ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p. + ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. x = a → Type[2]. P a (refl A a) → P x p. #A #a #x #p (cases p) // qed. lemma eq_ind_r : - ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. + ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → + ∀x.∀p:eq ? x a.P x p. #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed. lemma eq_rect_Type2_r: - ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. + ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → + ∀x.∀p:eq ? x a.P x p. #A #a #P #H #x #p (generalize in match H) (generalize in match P) cases p; //; qed. @@ -141,7 +144,7 @@ definition R0 ≝ λT:Type[0].λt:T.t. definition R1 ≝ eq_rect_Type0. -(* useless stuff +(* useless stuff *) definition R2 : ∀T0:Type[0]. ∀a0:T0. @@ -216,7 +219,7 @@ definition R4 : @(eq_rect_Type0 ????? e3) @(R3 ????????? e0 ? e1 ? e2) @a4 -qed. *) +qed. (* TODO concrete definition by means of proof irrelevance *) axiom streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. diff --git a/matitaB/matita/lib/basics/pts.ma b/matitaB/matita/lib/basics/pts.ma index 16f34ddb1..1b87a2d0b 100644 --- a/matitaB/matita/lib/basics/pts.ma +++ b/matitaB/matita/lib/basics/pts.ma @@ -19,7 +19,7 @@ universe constraint Type[1] < Type[2]. universe constraint Type[2] < Type[3]. universe constraint Type[3] < Type[4]. -inductive True : Prop ≝ I : True. +(*inductive True : Prop ≝ I : True. (*lemma fa : ∀X:Prop.X → X. #X #p // @@ -32,9 +32,10 @@ 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. -@ +lemma provable_True : True → eq Prop True True. +#H % +qed.*) \ No newline at end of file diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml index 913ba87f6..68cb16c84 100644 --- a/matitaB/matita/matitaEngine.ml +++ b/matitaB/matita/matitaEngine.ml @@ -118,11 +118,17 @@ let activate_extraction baseuri fname = let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) = let baseuri = status#baseuri in + (* let new_aliases,new_status = GrafiteDisambiguate.eval_with_new_aliases status (fun status -> GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast)) in + *) + let new_status = + GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status + (text,prefix_len,ast) in + (* let _,intermediate_states = List.fold_left (fun (status,acc) (k,value) -> @@ -146,6 +152,8 @@ let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) = ) (status,[]) new_aliases (* WARNING: this must be the old status! *) in (new_status,None)::intermediate_states + *) + [new_status,None] ;; let baseuri_of_script ~include_paths fname = @@ -269,6 +277,12 @@ and compile ~compiling ~asserted ~include_paths fname = HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); pp_times fname true big_bang big_bang_u big_bang_s; + (* XXX: update script -- currently to stdout *) + let origbuf = Ulexing.from_utf8_channel (open_in fname) in + let outfile = open_out (fname ^ ".mad") in + let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in + ignore (SmallLexer.mk_small_printer interpr outfile origbuf); + close_out outfile; asserted (* MATITA 1.0: debbo fare time_travel sulla ng_library? LexiconSync.time_travel @@ -276,7 +290,7 @@ and compile ~compiling ~asserted ~include_paths fname = *)) with (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *) - | exn when not matita_debug -> + | exn when not matita_debug -> (* MATITA 1.0: debbo fare time_travel sulla ng_library? LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status; * *) diff --git a/matitaB/matita/matitaExcPp.ml b/matitaB/matita/matitaExcPp.ml index 5ecea5dc8..e3e18a415 100644 --- a/matitaB/matita/matitaExcPp.ml +++ b/matitaB/matita/matitaExcPp.ml @@ -186,7 +186,7 @@ let rec to_string = let y = y + offset in let floc = HExtlib.floc_of_loc (x,y) in Some floc - | _ -> assert false + | _ -> (* assert false *) None in let annotated_errorll = List.rev diff --git a/matitaB/matita/matitaGui.ml b/matitaB/matita/matitaGui.ml index fbf9247e2..7a05e13ff 100644 --- a/matitaB/matita/matitaGui.ml +++ b/matitaB/matita/matitaGui.ml @@ -377,16 +377,16 @@ let interactive_error_interp ~all_passes (fun k,desc -> let alias = match k with - | DisambiguateTypes.Id (id,_opturi) -> + | DisambiguateTypes.Id id -> (* 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, _)-> + | DisambiguateTypes.Symbol symb-> GrafiteAst.Symbol_alias (symb, None, desc) - | DisambiguateTypes.Num _ -> + | DisambiguateTypes.Num -> GrafiteAst.Number_alias (None,desc) in GrafiteAstPp.pp_alias alias) @@ -1255,12 +1255,29 @@ let interactive_interp_choice () text prefix_len choices = in classify example_interp [] enumerated_choices +let interactive_ast_choice () ts = + let choice = + interactive_string_choice + "" 0 ~title:"Ambiguous input" + ~msg:("Choose an interpretation") () ~id:"" [] ts + in + let choice = match choice with + | [c] -> c + | _ -> assert false + in + let rec posn x = function + | [] -> assert false + | he::tl -> if he = x then 0 else 1 + posn x tl + in + posn choice ts + let _ = (* disambiguator callbacks *) Disambiguate.set_choose_uris_callback (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg -> interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ()); Disambiguate.set_choose_interp_callback (interactive_interp_choice ()); + Disambiguate.set_choose_disamb_callback (interactive_ast_choice ()); (* gtk initialization *) GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) ignore (GMain.Main.init ()) diff --git a/matitaB/matita/matitaScript.ml b/matitaB/matita/matitaScript.ml index 8d1645858..af3cdf12e 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 newast, m, s, status, t = + let m, s, status, t = GrafiteDisambiguate.disambiguate_nterm status None ctx menv subst (parsed_text,parsed_text_length, NotationPt.Cast (t,NotationPt.Implicit `JustOne)) diff --git a/matitaB/matita/nlibrary/properties/relations.ma b/matitaB/matita/nlibrary/properties/relations.ma index 1df2e205a..334c67842 100644 --- a/matitaB/matita/nlibrary/properties/relations.ma +++ b/matitaB/matita/nlibrary/properties/relations.ma @@ -20,7 +20,7 @@ definition transitive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀z,x,y. P x z record equivalence_relation (A:Type[0]) : Type[1] ≝ { eq_rel:2> A → A → CProp[0]; - refl: reflexive ? eq_rel; - sym: symmetric ? eq_rel; - trans: transitive ? eq_rel + refl: reflexive ? eq_rel; + sym: symmetric ? eq_rel; + trans: transitive ? eq_rel }. diff --git a/matitaB/matita/nlibrary/properties/relations1.ma b/matitaB/matita/nlibrary/properties/relations1.ma index 86a6f15b7..535a11984 100644 --- a/matitaB/matita/nlibrary/properties/relations1.ma +++ b/matitaB/matita/nlibrary/properties/relations1.ma @@ -14,13 +14,13 @@ include "logic/pts.ma". -ndefinition reflexive1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀x.P x x. -ndefinition symmetric1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀x,y.P x y → P y x. -ndefinition transitive1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀z,x,y. P x z → P z y → P x y. +definition reflexive1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀x.P x x. +definition symmetric1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀x,y.P x y → P y x. +definition transitive1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀z,x,y. P x z → P z y → P x y. -nrecord equivalence_relation1 (A:Type[1]) : Type[2] ≝ +record equivalence_relation1 (A:Type[1]) : Type[2] ≝ { eq_rel1:2> A → A → CProp[1]; - refl1: reflexive1 ? eq_rel1; - sym1: symmetric1 ? eq_rel1; - trans1: transitive1 ? eq_rel1 + refl1: reflexive1 ? eq_rel1; + sym1: symmetric1 ? eq_rel1; + trans1: transitive1 ? eq_rel1 }. diff --git a/matitaB/matita/nlibrary/properties/relations2.ma b/matitaB/matita/nlibrary/properties/relations2.ma index 67d09e938..155dde75b 100644 --- a/matitaB/matita/nlibrary/properties/relations2.ma +++ b/matitaB/matita/nlibrary/properties/relations2.ma @@ -14,13 +14,13 @@ include "logic/pts.ma". -ndefinition reflexive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x.P x x. -ndefinition symmetric2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x,y.P x y → P y x. -ndefinition transitive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀z,x,y. P x z → P z y → P x y. +definition reflexive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x.P x x. +definition symmetric2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x,y.P x y → P y x. +definition transitive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀z,x,y. P x z → P z y → P x y. -nrecord equivalence_relation2 (A:Type[2]) : Type[3] ≝ +record equivalence_relation2 (A:Type[2]) : Type[3] ≝ { eq_rel2:2> A → A → CProp[2]; - refl2: reflexive2 ? eq_rel2; - sym2: symmetric2 ? eq_rel2; - trans2: transitive2 ? eq_rel2 + refl2: reflexive2 ? eq_rel2; + sym2: symmetric2 ? eq_rel2; + trans2: transitive2 ? eq_rel2 }. diff --git a/matitaB/matita/nlibrary/sets/setoids.ma b/matitaB/matita/nlibrary/sets/setoids.ma index e40dad6f6..29f4c910c 100644 --- a/matitaB/matita/nlibrary/sets/setoids.ma +++ b/matitaB/matita/nlibrary/sets/setoids.ma @@ -16,7 +16,7 @@ include "logic/connectives.ma". include "properties/relations.ma". include "hints_declaration.ma". -nrecord setoid : Type[1] ≝ { +record setoid : Type[1] ≝ { carr:> Type[0]; eq0: equivalence_relation carr }. @@ -46,7 +46,7 @@ interpretation "trans" 'trans r = (trans ????? r). notation > ".=_0 r" with precedence 50 for @{'trans_x0 $r}. interpretation "trans_x0" 'trans_x0 r = (trans ????? r). -nrecord unary_morphism (A,B: setoid) : Type[0] ≝ { +record unary_morphism (A,B: setoid) : Type[0] ≝ { fun1:1> A → B; prop1: ∀a,a'. a = a' → fun1 a = fun1 a' }. @@ -64,13 +64,13 @@ notation "┼_0 c" with precedence 89 for @{'prop1_x0 $c }. notation "l ╪_0 r" with precedence 89 for @{'prop2_x0 $l $r }. interpretation "prop1_x0" 'prop1_x0 c = (prop1 ????? c). -ndefinition unary_morph_setoid : setoid → setoid → setoid. -#S1; #S2; @ (S1 ⇒_0 S2); @; -##[ #f; #g; napply (∀x,x'. x=x' → f x = g x'); -##| #f; #x; #x'; #Hx; napply (.= †Hx); napply #; -##| #f; #g; #H; #x; #x'; #Hx; napply ((H … Hx^-1)^-1); -##| #f; #g; #h; #H1; #H2; #x; #x'; #Hx; napply (trans … (H1 …) (H2 …)); //; ##] -nqed. +definition unary_morph_setoid : setoid → setoid → setoid. +#S1 #S2 @(mk_setoid … (S1 ⇒_0 S2)) % +[ #f #g @(∀x,x'. x=x' → f x = g x') +| #f #x #x' #Hx @(.= †Hx) @# +| #f #g #H #x #x' #Hx @((H … Hx^-1)^-1) +| #f #g #h #H1 #H2 #x #x' #Hx @(trans … (H1 …) (H2 …)) // ] +qed. alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". unification hint 0 ≔ o1,o2 ; @@ -81,26 +81,27 @@ unification hint 0 ≔ o1,o2 ; interpretation "prop2" 'prop2 l r = (prop1 ? (unary_morph_setoid ??) ? ?? l ?? r). interpretation "prop2_x0" 'prop2_x0 l r = (prop1 ? (unary_morph_setoid ??) ? ?? l ?? r). -nlemma unary_morph_eq: ∀A,B.∀f,g:A ⇒_0 B. (∀x. f x = g x) → f = g. -#A B f g H x1 x2 E; napply (.= †E); napply H; nqed. +lemma unary_morph_eq: ∀A,B.∀f,g:A ⇒_0 B. (∀x. f x = g x) → f = g. +#A #B #f #g #H #x1 #x2 #E @(.= †E) @H +qed. -nlemma mk_binary_morphism: +lemma mk_binary_morphism: ∀A,B,C: setoid. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') → A ⇒_0 (unary_morph_setoid B C). - #A; #B; #C; #f; #H; @; ##[ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph_eq; #y] - /2/. -nqed. + #A #B #C #f #H % [ #x % [@(f x)|/2/] |#a #a' #Ha @unary_morph_eq #y] + /2/ +qed. -ndefinition composition ≝ +definition composition ≝ λo1,o2,o3:Type[0].λf:o2 → o3.λg: o1 → o2.λx.f (g x). interpretation "function composition" 'compose f g = (composition ??? f g). -ndefinition comp_unary_morphisms: +definition comp_unary_morphisms: ∀o1,o2,o3:setoid.o2 ⇒_0 o3 → o1 ⇒_0 o2 → o1 ⇒_0 o3. -#o1; #o2; #o3; #f; #g; @ (f ∘ g); - #a; #a'; #e; nnormalize; napply (.= †(†e)); napply #. -nqed. +#o1 #o2 #o3 #f #g % [@(f ∘ g)] + #a #a' #e normalize @(.= †(†e)) @# +qed. unification hint 0 ≔ o1,o2,o3:setoid,f:o2 ⇒_0 o3,g:o1 ⇒_0 o2; R ≟ mk_unary_morphism o1 o3 @@ -109,13 +110,13 @@ unification hint 0 ≔ o1,o2,o3:setoid,f:o2 ⇒_0 o3,g:o1 ⇒_0 o2; (* -------------------------------------------------------------------- *) ⊢ fun1 o1 o3 R ≡ composition ??? (fun1 o2 o3 f) (fun1 o1 o2 g). -ndefinition comp_binary_morphisms: +definition comp_binary_morphisms: ∀o1,o2,o3.(o2 ⇒_0 o3) ⇒_0 ((o1 ⇒_0 o2) ⇒_0 (o1 ⇒_0 o3)). -#o1; #o2; #o3; napply mk_binary_morphism - [ #f; #g; napply (comp_unary_morphisms ??? f g) +#o1 #o2 #o3 @mk_binary_morphism + [ #f #g @(comp_unary_morphisms ??? f g) (* CSC: why not ∘? GARES: because the coercion to FunClass is not triggered if there are no "extra" arguments. We could fix that in the refiner *) - | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ] -nqed. + | #a #a' #b #b' #ea #eb #x #x' #Hx normalize /3/ ] +qed. diff --git a/matitaB/matita/nlibrary/sets/setoids1.ma b/matitaB/matita/nlibrary/sets/setoids1.ma index 90be6bc94..751c238a5 100644 --- a/matitaB/matita/nlibrary/sets/setoids1.ma +++ b/matitaB/matita/nlibrary/sets/setoids1.ma @@ -16,7 +16,7 @@ include "properties/relations1.ma". include "sets/setoids.ma". include "hints_declaration.ma". -nrecord setoid1: Type[2] ≝ { +record setoid1: Type[2] ≝ { carr1:> Type[1]; eq1: equivalence_relation1 carr1 }. @@ -31,9 +31,9 @@ notation < "[\setoid1\ensp\of term 19 x]" non associative with precedence 90 f interpretation "mk_setoid1" 'mk_setoid1 x = (mk_setoid1 x ?). (* da capire se mettere come coercion *) -ndefinition setoid1_of_setoid: setoid → setoid1. - #s; @ (carr s); @ (eq0…) (refl…) (sym…) (trans…); -nqed. +definition setoid1_of_setoid: setoid → setoid1. + #s % [@(carr s)] % [@(eq0…)|@(refl…)|@(sym…)|@(trans…)] +qed. alias symbol "hint_decl" = "hint_decl_CProp2". alias symbol "hint_decl" (instance 1) = "hint_decl_Type2". @@ -66,7 +66,7 @@ interpretation "trans1" 'trans r = (trans1 ????? r). interpretation "trans" 'trans r = (trans ????? r). interpretation "trans1_x1" 'trans_x1 r = (trans1 ????? r). -nrecord unary_morphism1 (A,B: setoid1) : Type[1] ≝ { +record unary_morphism1 (A,B: setoid1) : Type[1] ≝ { fun11:1> A → B; prop11: ∀a,a'. eq1 ? a a' → eq1 ? (fun11 a) (fun11 a') }. @@ -80,13 +80,14 @@ interpretation "prop11" 'prop1 c = (prop11 ????? c). interpretation "prop11_x1" 'prop1_x1 c = (prop11 ????? c). interpretation "refl1" 'refl = (refl1 ???). -ndefinition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1. - #s; #s1; @ (s ⇒_1 s1); @ - [ #f; #g; napply (∀a,a':s. a=a' → f a = g a') - | #x; #a; #a'; #Ha; napply (.= †Ha); napply refl1 - | #x; #y; #H; #a; #a'; #Ha; napply (.= †Ha); napply sym1; /2/ - | #x; #y; #z; #H1; #H2; #a; #a'; #Ha; napply (.= †Ha); napply trans1; ##[##2: napply H1 | ##skip | napply H2]//;##] -nqed. +definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1. + #s #s1 % [@(s ⇒_1 s1)] % + [ #f #g @(∀a,a':s. a=a' → f a = g a') + | #x #a #a' #Ha @(.= †Ha) @refl1 + | #x #y #H #a #a' #Ha @(.= †Ha) @sym1 /2/ + | #x #y #z #H1 #H2 #a #a' #Ha @(.= †Ha) @trans1 + [2: @H1 | skip | @H2] // ] +qed. unification hint 0 ≔ S, T ; R ≟ (unary_morphism1_setoid1 S T) @@ -97,27 +98,29 @@ notation "l ╪_1 r" with precedence 89 for @{'prop2_x1 $l $r }. interpretation "prop21" 'prop2 l r = (prop11 ? (unary_morphism1_setoid1 ??) ? ?? l ?? r). interpretation "prop21_x1" 'prop2_x1 l r = (prop11 ? (unary_morphism1_setoid1 ??) ? ?? l ?? r). -nlemma unary_morph1_eq1: ∀A,B.∀f,g: A ⇒_1 B. (∀x. f x = g x) → f = g. -/3/. nqed. +lemma unary_morph1_eq1: ∀A,B.∀f,g: A ⇒_1 B. (∀x. f x = g x) → f = g. +/3/ +qed. -nlemma mk_binary_morphism1: +(* DISAMBIGUATION XXX: this takes some time to disambiguate *) +lemma mk_binary_morphism1: ∀A,B,C: setoid1. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') → A ⇒_1 (unary_morphism1_setoid1 B C). - #A; #B; #C; #f; #H; @ [ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph1_eq1; #y] - /2/. -nqed. + #A #B #C #f #H % [ #x % [@(f x)]] #a #a' #Ha [2: @unary_morph1_eq1 #y] + /2/ +qed. -ndefinition composition1 ≝ +definition composition1 ≝ λo1,o2,o3:Type[1].λf:o2 → o3.λg: o1 → o2.λx.f (g x). interpretation "function composition" 'compose f g = (composition ??? f g). interpretation "function composition1" 'compose f g = (composition1 ??? f g). -ndefinition comp1_unary_morphisms: +definition comp1_unary_morphisms: ∀o1,o2,o3:setoid1.o2 ⇒_1 o3 → o1 ⇒_1 o2 → o1 ⇒_1 o3. -#o1; #o2; #o3; #f; #g; @ (f ∘ g); - #a; #a'; #e; nnormalize; napply (.= †(†e)); napply #. -nqed. +#o1 #o2 #o3 #f #g % [@ (f ∘ g)] + #a #a' #e normalize @(.= †(†e)) @# +qed. unification hint 0 ≔ o1,o2,o3:setoid1,f:o2 ⇒_1 o3,g:o1 ⇒_1 o2; R ≟ (mk_unary_morphism1 ?? (composition1 ??? (fun11 ?? f) (fun11 ?? g)) @@ -125,9 +128,9 @@ unification hint 0 ≔ o1,o2,o3:setoid1,f:o2 ⇒_1 o3,g:o1 ⇒_1 o2; (* -------------------------------------------------------------------- *) ⊢ fun11 o1 o3 R ≡ composition1 ??? (fun11 ?? f) (fun11 ?? g). -ndefinition comp1_binary_morphisms: +definition comp1_binary_morphisms: ∀o1,o2,o3. (o2 ⇒_1 o3) ⇒_1 ((o1 ⇒_1 o2) ⇒_1 (o1 ⇒_1 o3)). -#o1; #o2; #o3; napply mk_binary_morphism1 - [ #f; #g; napply (comp1_unary_morphisms … f g) - | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ] -nqed. +#o1 #o2 #o3 @mk_binary_morphism1 + [ #f #g @(comp1_unary_morphisms … f g) + | #a #a' #b #b' #ea #eb #x #x' #Hx normalize /3/ ] +qed. diff --git a/matitaB/matita/nlibrary/sets/setoids2.ma b/matitaB/matita/nlibrary/sets/setoids2.ma index 34036a48b..112b19b98 100644 --- a/matitaB/matita/nlibrary/sets/setoids2.ma +++ b/matitaB/matita/nlibrary/sets/setoids2.ma @@ -15,17 +15,16 @@ include "properties/relations2.ma". include "sets/setoids1.ma". -nrecord setoid2: Type[3] ≝ +record setoid2: Type[3] ≝ { carr2:> Type[2]; eq2: equivalence_relation2 carr2 }. -ndefinition setoid2_of_setoid1: setoid1 → setoid2. - #s; @ (carr1 s); @ (carr1 s) (eq1 ?) - [ napply refl1 - | napply sym1 - | napply trans1] -nqed. +definition setoid2_of_setoid1: setoid1 → setoid2. + #s @(mk_setoid2 … (carr1 s)) + @(mk_equivalence_relation2 … (carr1 s) (eq1 ?)) + /2/ +qed. (*ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.*) @@ -33,7 +32,7 @@ nqed. interpretation "setoid2 eq" 'eq t x y = (eq_rel2 ? (eq2 t) x y). interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y). -interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y). +interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y). (* notation > "hvbox(a break =_12 b)" non associative with precedence 45 @@ -54,12 +53,12 @@ interpretation "trans2" 'trans r = (trans2 ????? r). interpretation "trans1" 'trans r = (trans1 ????? r). interpretation "trans" 'trans r = (trans ????? r). -nrecord unary_morphism2 (A,B: setoid2) : Type[2] ≝ +record unary_morphism2 (A,B: setoid2) : Type[2] ≝ { fun12:1> A → B; prop12: ∀a,a'. eq2 ? a a' → eq2 ? (fun12 a) (fun12 a') }. -nrecord binary_morphism2 (A,B,C:setoid2) : Type[2] ≝ +record binary_morphism2 (A,B,C:setoid2) : Type[2] ≝ { fun22:2> A → B → C; prop22: ∀a,a',b,b'. eq2 ? a a' → eq2 ? b b' → eq2 ? (fun22 a b) (fun22 a' b') }. diff --git a/matitaB/matita/nlibrary/sets/sets.ma b/matitaB/matita/nlibrary/sets/sets.ma index c8f303a6b..7c9bd8d07 100644 --- a/matitaB/matita/nlibrary/sets/sets.ma +++ b/matitaB/matita/nlibrary/sets/sets.ma @@ -16,46 +16,47 @@ include "logic/connectives.ma". -nrecord powerclass (A: Type[0]) : Type[1] ≝ { mem: A → CProp[0] }. +record powerclass (A: Type[0]) : Type[1] ≝ { mem: A → CProp[0] }. interpretation "mem" 'mem a S = (mem ? S a). interpretation "powerclass" 'powerset A = (powerclass A). interpretation "subset construction" 'subset \eta.x = (mk_powerclass ? x). -ndefinition subseteq ≝ λA.λU,V.∀a:A. a ∈ U → a ∈ V. +definition subseteq ≝ λA.λU,V.∀a:A. a ∈ U → a ∈ V. interpretation "subseteq" 'subseteq U V = (subseteq ? U V). -ndefinition overlaps ≝ λA.λU,V.∃x:A.x ∈ U ∧ x ∈ V. +definition overlaps ≝ λA.λU,V.∃x:A.x ∈ U ∧ x ∈ V. interpretation "overlaps" 'overlaps U V = (overlaps ? U V). -ndefinition intersect ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ x ∈ V }. +definition intersect ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ x ∈ V }. interpretation "intersect" 'intersects U V = (intersect ? U V). -ndefinition union ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∨ x ∈ V }. +definition union ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∨ x ∈ V }. interpretation "union" 'union U V = (union ? U V). -ndefinition substract ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ ¬ x ∈ V }. +definition substract ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ ¬ x ∈ V }. interpretation "substract" 'minus U V = (substract ? U V). -ndefinition big_union ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∃i. i ∈ T ∧ x ∈ f i }. +definition big_union ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∃i. i ∈ T ∧ x ∈ f i }. -ndefinition big_intersection ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∀i. i ∈ T → x ∈ f i }. +definition big_intersection ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∀i. i ∈ T → x ∈ f i }. -ndefinition full_set: ∀A. Ω^A ≝ λA.{ x | True }. +definition full_set: ∀A. Ω^A ≝ λA.{ x | True }. -nlemma subseteq_refl: ∀A.∀S: Ω^A. S ⊆ S. -//.nqed. +lemma subseteq_refl: ∀A.∀S: Ω^A. S ⊆ S. +//.qed. -nlemma subseteq_trans: ∀A.∀S,T,U: Ω^A. S ⊆ T → T ⊆ U → S ⊆ U. -/3/.nqed. +lemma subseteq_trans: ∀A.∀S,T,U: Ω^A. S ⊆ T → T ⊆ U → S ⊆ U. +/3/.qed. include "properties/relations1.ma". -ndefinition seteq: ∀A. equivalence_relation1 (Ω^A). -#A; @(λS,S'. S ⊆ S' ∧ S' ⊆ S); /2/; ##[ #A B; *; /3/] -#S T U; *; #H1 H2; *; /4/; -nqed. +definition seteq: ∀A. equivalence_relation1 (Ω^A). +#A % [@(λS,S'. S ⊆ S' ∧ S' ⊆ S)] +/2/[ #A #B * /3/] +#S #T #U * #H1 #H2 * /4/ +qed. include "sets/setoids1.ma".