-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"
| 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
| 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 *)
| NumType
| OptType of value_type
| ListType of value_type
+ | NoType
(** looked up value not found in environment *)
exception Value_not_found of string
(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 =
| 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
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))
| 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)
| _ -> ""))
| 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, _
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"
| 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
| 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 "; "
INTERFACE_FILES = \
renderingAttrs.mli \
cicNotationLexer.mli \
+ interpTable.mli \
+ smallLexer.mli \
cicNotationParser.mli \
mpresentation.mli \
box.mli \
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
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
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
+
+
# </cross>
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 = "<A href=\"" uri "\">"
+let regexp hrefclose = "</A>"
+
let regexp tex_token = '\\' ident
let regexp delim_begin = "\\["
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 = "(*"
(":=", <:unicode<def>>);
]
-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 *)
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)
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"
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"
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;
}
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))
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
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)
| "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<Assign>> (* ≔ *); t = term -> (i, t)
- ] SEP SYMBOL ";";
- SYMBOL "]" ->
- substs
- ]
- ];
meta_subst: [
[ s = SYMBOL "_" -> None
| p = term -> Some p ]
| SYMBOL <:unicode<lambda>> (* λ *) -> `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
]
];
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
| _ -> failwith ("Invalid index name: " ^ blob)
]
];
+ located: [
+ [ s = SYMBOL -> loc ]
+ ];
let_defs: [
[ defs = LIST1 [
name = single_arg;
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<def>> (* ≝ *);
p1 = term; "in"; p2 = term ->
return_term loc (Ast.LetIn (var, p1, p2))
];
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))
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
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;
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))
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
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 =
| 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
(** 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
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"
| 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 =
| _ -> 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
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)
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)
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
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
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)
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
[(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 -> []
((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
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) ->
| [] -> 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)
;;
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
;;
| _ -> 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))
~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
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
(* 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
~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 =
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
-
-(*
- (* <benchmark> *)
- 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
- (* </benchmark> *)
-*)
-
- (* (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
- *)
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 *)
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
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 ->
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 ->
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 ->
((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) ->
(* $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
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 ->
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
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
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"
+;;
* 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:
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
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
]
;;
+(* XXX is this useful anymore? *)
let drop_aliases ?(minimize_instances=false) ~description_of_alias
(choices, user_asked)
=
let rec aux =
function
[] -> []
+(* now it's ALWAYS None
| (D.Symbol (s,n),ci1) as he::tl when n <> None ->
if
List.for_all
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
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));
| [] -> assert false
in
aux 1 [] passes
-;;
+;;*)
let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
~string_context_of_context ~initial_ugraph ~expty ~mk_implicit
~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
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]))
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:(
(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 ->
((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
;;
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
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 =
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 =
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 =
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 = []);
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
"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,_,_) =
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
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)
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
inherit NTacStatus.tac_status
inherit NCicLibrary.dumpable_status
inherit NCicLibrary.status
+ inherit GrafiteDisambiguate.status
inherit GrafiteParser.status
inherit TermContentPres.status
method baseuri: string
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
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
;;
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
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
(* $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 =
= 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
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
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
~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
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
;;*)
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
~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
;;
in
NUri.uri_of_string (baseuri ^ "/" ^ name)
in
- let diff, _, _, cic =
+ let ast, _, _, cic =
singleton "third"
(NCicDisambiguate.disambiguate_obj
status
~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
;;
(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 ->
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)
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 ->
#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 *
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);
(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) ->
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 "^
(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
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 =
(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
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
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) ->
| 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
| 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 _
(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
;;
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
;;
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);
| 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, [], [],
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))
| 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)))
| 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
(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'
| 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
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
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
| 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)
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)
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
| 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)
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 =
~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
;;
=
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
~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 _ =
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 *
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
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
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
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.
// 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.
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.
definition R1 ≝ eq_rect_Type0.
-(* useless stuff
+(* useless stuff *)
definition R2 :
∀T0:Type[0].
∀a0:T0.
@(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.
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 //
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 : <A href="cic:/matita/basics/pts/True.ind(1,0,0)">True</A> → eq Prop True True.
+#H %
+qed.*)
\ No newline at end of file
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) ->
) (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 =
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
*))
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;
* *)
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
(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)
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 ())
"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))
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: <A href="cic:/matita/ng/properties/relations/reflexive.def(1)">reflexive</A> ? eq_rel;
+ sym: <A href="cic:/matita/ng/properties/relations/symmetric.def(1)">symmetric</A> ? eq_rel;
+ trans: <A href="cic:/matita/ng/properties/relations/transitive.def(1)">transitive</A> ? eq_rel
}.
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: <A href="cic:/matita/ng/properties/relations1/reflexive1.def(1)">reflexive1</A> ? eq_rel1;
+ sym1: <A href="cic:/matita/ng/properties/relations1/symmetric1.def(1)">symmetric1</A> ? eq_rel1;
+ trans1: <A href="cic:/matita/ng/properties/relations1/transitive1.def(1)">transitive1</A> ? eq_rel1
}.
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: <A href="cic:/matita/ng/properties/relations2/reflexive2.def(1)">reflexive2</A> ? eq_rel2;
+ sym2: <A href="cic:/matita/ng/properties/relations2/symmetric2.def(1)">symmetric2</A> ? eq_rel2;
+ trans2: <A href="cic:/matita/ng/properties/relations2/transitive2.def(1)">transitive2</A> ? eq_rel2
}.
include "properties/relations.ma".
include "hints_declaration.ma".
-nrecord setoid : Type[1] ≝ {
+record setoid : Type[1] ≝ {
carr:> Type[0];
eq0: equivalence_relation carr
}.
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'
}.
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 ;
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
(* -------------------------------------------------------------------- *) ⊢
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.
include "sets/setoids.ma".
include "hints_declaration.ma".
-nrecord setoid1: Type[2] ≝ {
+record setoid1: Type[2] ≝ {
carr1:> Type[1];
eq1: equivalence_relation1 carr1
}.
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".
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')
}.
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)
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))
(* -------------------------------------------------------------------- *) ⊢
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.
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.*)
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
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')
}.
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".
projects / helm.git / commitdiff