-requires="helm-content"
+requires="helm-content helm-grafite"
version="0.0.1"
archive(byte)="disambiguation.cma"
archive(native)="disambiguation.cmxa"
let value_of_term = function
| Ast.Num (s, _) -> NumValue s
- | Ast.Ident (s, None) -> StringValue (Var s)
+ | Ast.Ident (s, (* `Ambiguous? *) _) -> StringValue (Var s)
| t -> TermValue t
let term_of_value = function
- | NumValue s -> Ast.Num (s, 0)
- | StringValue (Ident s) -> Ast.Ident (s, None)
+ | NumValue s -> Ast.Num (s, None)
+ | StringValue (Ident s) -> Ast.Ident (s, `Ambiguous)
| TermValue t -> t
| _ -> assert false (* TO BE UNDERSTOOD *)
| term, Some typ -> "(" ^ pp_term (* ~pp_parens:false *) term ^ ": " ^ pp_term typ ^ ")"
let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
+ let pp_ident = function
+ | Ast.Ident (id,`Ambiguous) -> "A:" ^ id
+ | Ast.Ident (id,`Rel) -> "R:" ^ id
+ | Ast.Ident (id,`Uri u) -> ("U:(" ^ id ^ "," ^ u ^ ")")
+ | _ -> "E"
+ in
let pp_term = pp_term status in
let t_pp =
match t with
| Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term
| Ast.Appl terms ->
sprintf "%s" (String.concat " " (List.map pp_term terms))
- | Ast.Binder (`Forall, (Ast.Ident ("_", None), typ), body)
- | Ast.Binder (`Pi, (Ast.Ident ("_", None), typ), body) ->
+ | Ast.Binder (`Forall, (Ast.Ident ("_", `Ambiguous), typ), body)
+ | Ast.Binder (`Forall, (Ast.Ident ("_", `Rel), typ), body)
+ | Ast.Binder (`Pi, (Ast.Ident ("_", `Ambiguous), typ), body)
+ | Ast.Binder (`Pi, (Ast.Ident ("_", `Rel), typ), body) ->
sprintf "%s \\to %s"
(match typ with None -> "?" | Some typ -> pp_term typ)
(pp_term ~pp_parens:true body)
| Ast.Binder (kind, var, body) ->
+(*
+ * sprintf "\\%s[%s] %s.%s" (pp_binder kind) (pp_ident var) (pp_capture_variable pp_term var)
+ *)
sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable pp_term var)
(pp_term ~pp_parens:true body)
| Ast.Case (term, indtype, typ, patterns) ->
(match kind with `Inductive -> "rec" | `CoInductive -> "corec")
(String.concat " and " (List.map map definitions))
(pp_term term)
- | Ast.Ident (name, Some []) | Ast.Ident (name, None)
- | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
+ | Ast.Ident (name, _ ) -> pp_ident t
| Ast.NRef nref -> NReference.string_of_reference nref
| Ast.NCic cic -> status#ppterm ~metasenv:[] ~context:[] ~subst:[] cic
- | Ast.Ident (name, Some substs)
- | Ast.Uri (name, Some substs) ->
- sprintf "%s \\subst [%s]" name (pp_substs status substs)
| Ast.Implicit `Vector -> "…"
| Ast.Implicit `JustOne -> "?"
| Ast.Implicit (`Tagged name) -> "?"^name
| true, Ast.Implicit _
| true, Ast.UserInput
| true, Ast.Sort _
- | true, Ast.Ident (_, Some [])
- | true, Ast.Ident (_, None) -> t_pp
- | _ -> sprintf "(%s)" t_pp
+ | true, Ast.Ident _ -> t_pp
+ | _ -> sprintf "(%s)" t_pp
and pp_subst status (name, term) =
sprintf "%s \\Assign %s" name (pp_term status term)
(** To be increased each time the term type below changes, used for "safe"
* marshalling *)
-let magic = 6
+let magic = 7
type term =
(* CIC AST *)
| LetIn of term capture_variable * term * term (* name, body, where *)
| LetRec of induction_kind * (term capture_variable list * term capture_variable * term * int) list * term
(* (params, name, body, decreasing arg) list, where *)
- | Ident of string * subst list option
- (* literal, substitutions.
- * Some [] -> user has given an empty explicit substitution list
- * None -> user has given no explicit substitution list *)
+ | Ident of string * [ `Ambiguous | `Uri of string | `Rel ]
+ (* literal, disambiguation info (can be ambiguous, a disambiguated uri,
+ * or an identifier to be converted in a Rel)
+ * case `Uri is also used for literal uris
+ * the parser fills the name of the identifier using the final part of the
+ * uri
+ *)
| Implicit of [`Vector | `JustOne | `Tagged of string]
| Meta of int * meta_subst list
- | Num of string * int (* literal, instance *)
+ | Num of string * (string option * string) option
+ (* literal, (uri, interpretation name) *)
| Sort of sort_kind
- | Symbol of string * int (* canonical name, instance *)
-
+ (* XXX: symbols used to be packed with their instance number, probably for
+ * disambiguation purposes; hopefully we won't need this info any more *)
+ | Symbol of string * (string option * string) option
+ (* canonical name, (uri, interpretation name) *)
| UserInput (* place holder for user input, used by MatitaConsole, not to be
used elsewhere *)
- | Uri of string * subst list option (* as Ident, for long names *)
| NRef of NReference.reference
| NCic of NCic.term
| Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list
(** left parameters, name, type, fields *)
+let map_variable f (t,u) = f t, HExtlib.map_option f u ;;
+
+let map_pattern f = function
+ | Pattern (s,h,vl) -> Pattern (s,h,List.map (map_variable f) vl)
+ | p -> p
+;;
+
+let map f = function
+ | AttributedTerm (a,u) -> AttributedTerm (a,f u)
+ | Appl tl -> Appl (List.map f tl)
+ | Binder (k,n,body) -> Binder (k,map_variable f n,f body)
+ | Case (t,ity,oty,pl) ->
+ let pl' = List.map (fun (p,u) -> map_pattern f p, f u) pl in
+ Case (f t,ity,HExtlib.map_option f oty,pl')
+ | Cast (u,v) -> Cast (f u,f v)
+ | LetIn (n,u,v) -> LetIn (n,f u,f v)
+ | LetRec (ik,l,t) ->
+ let l' = List.map (fun (vl,v,u,n) ->
+ (List.map (map_variable f) vl,
+ map_variable f v,
+ f u,
+ n)) l
+ in LetRec (ik,l',f t)
+ | t -> t
+;;
+
(** {2 Standard precedences} *)
let let_in_prec = 10
definitions
in
Ast.LetRec (kind, definitions, k term)
- | Ast.Ident (name, Some substs) ->
- Ast.Ident (name, Some (aux_substs substs))
- | Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs substs))
| Ast.Meta (index, substs) -> Ast.Meta (index, List.map aux_opt substs)
| (Ast.AttributedTerm _
| Ast.Layout _
| Ast.Num _
| Ast.Sort _
| Ast.Symbol _
- | Ast.Uri _
| Ast.UserInput) as t -> t
and aux_opt = function
| None -> None
Ast.Pattern (head, hrefs, vars), term ->
Ast.Pattern (head, k_xref hrefs, List.map aux_capture_variable vars), k term
| Ast.Wildcard, term -> Ast.Wildcard, k term
- and aux_subst (name, term) = (name, k term)
- and aux_substs substs = List.map aux_subst substs
in
aux
| Ast.LetRec (_, definitions, body) ->
List.iter aux_definition definitions ;
aux body
- | Ast.Uri (_, Some substs) -> aux_substs substs
- | Ast.Ident (_, Some substs) -> aux_substs substs
| Ast.Meta (_, substs) -> aux_meta_substs substs
| Ast.Implicit _
| Ast.Num _
| Ast.Sort _
| Ast.Symbol _
- | Ast.Uri _
| Ast.UserInput -> ()
| Ast.Magic magic -> aux_magic magic
List.iter aux_capture_var params ;
aux_capture_var var ;
aux term
- and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
and aux_variable = function
| Ast.NumVar name -> add_name name
(* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
let fresh_name () = "eta" ^ string_of_int (fresh_id ())
+(* XXX FIXME: was used to add instance indices to symbols/numbers
+ * do we even need a similar operation?
+ * currently an identity function! *)
let rec freshen_term ?(index = ref 0) term =
let freshen_term = freshen_term ~index in
let fresh_instance () = incr index; !index in
| _ -> assert false
in
match term with
- | Ast.Symbol (s, instance) -> Ast.Symbol (s, fresh_instance ())
- | Ast.Num (s, instance) -> Ast.Num (s, fresh_instance ())
+ | Ast.Symbol (s, x) -> Ast.Symbol (s, x (* fresh_instance () *))
+ | Ast.Num (s, x) -> Ast.Num (s, x (* fresh_instance () *))
| t -> visit_ast ~special_k freshen_term t
let freshen_obj obj =
List.fold_right
(fun term body ->
let lambda = Ast.Binder (`Lambda, (term, ty), body) in
- Ast.Appl [ Ast.Symbol ("exists", 0); lambda ])
+ Ast.Appl [ Ast.Symbol ("exists", None); lambda ])
terms body
let fold_binder binder pt_names body =
[ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
id, Some typ
| arg = single_arg -> arg, None
- | id = PIDENT -> Ast.Ident (id, None), None
- | SYMBOL "_" -> Ast.Ident ("_", None), None
+ | id = PIDENT -> Ast.Ident (id, `Ambiguous), None
+ | SYMBOL "_" -> Ast.Ident ("_", `Ambiguous), None
| LPAREN; id = PIDENT; SYMBOL ":"; typ = term; RPAREN ->
- Ast.Ident (id, None), Some typ
+ Ast.Ident (id, `Ambiguous), Some typ
| LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
- Ast.Ident ("_", None), Some typ
+ Ast.Ident ("_", `Ambiguous), Some typ
]
];
match_pattern: [
arg: [
[ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
SYMBOL ":"; ty = term; RPAREN ->
- List.map (fun n -> Ast.Ident (n, None)) names, Some ty
- | name = IDENT -> [Ast.Ident (name, None)], None
+ List.map (fun n -> Ast.Ident (n, `Ambiguous)) names, Some ty
+ | name = IDENT -> [Ast.Ident (name, `Ambiguous)], None
| blob = UNPARSED_META ->
let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
match meta with
| Ast.Variable (Ast.FreshVar _) -> [meta], None
- | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None
+ | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", `Ambiguous)], None
| _ -> failwith "Invalid bound name."
]
];
single_arg: [
- [ name = IDENT -> Ast.Ident (name, None)
+ [ name = IDENT -> Ast.Ident (name, `Ambiguous)
| blob = UNPARSED_META ->
let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
match meta with
| Ast.Variable (Ast.FreshVar _)
| Ast.Variable (Ast.IdentVar _) -> meta
- | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None)
+ | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", `Ambiguous)
| _ -> failwith "Invalid index name."
]
];
[ vars = [ l =
[ l = LIST1 single_arg SEP SYMBOL "," -> l
| l = LIST1 [ PIDENT | SYMBOL "_" ] SEP SYMBOL "," ->
- List.map (fun x -> Ast.Ident(x,None)) l
+ List.map (fun x -> Ast.Ident(x,`Ambiguous)) l
] -> l ];
typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
]
[ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
id, Some typ
| id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
- Ast.Ident(id,None), ty ];
+ Ast.Ident(id,`Ambiguous), ty ];
SYMBOL <:unicode<def>> (* ≝ *);
p1 = term; "in"; p2 = term ->
return_term loc (Ast.LetIn (var, p1, p2))
];
term: LEVEL "90"
[
- [ id = IDENT -> return_term loc (Ast.Ident (id, None))
- | id = IDENT; s = explicit_subst ->
- return_term loc (Ast.Ident (id, Some s))
- | s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0))
- | u = URI -> return_term loc (Ast.Uri (u, None))
+ [ id = IDENT -> return_term loc (Ast.Ident (id, `Ambiguous))
+ | id = IDENT; s = explicit_subst -> (* XXX: no more explicit subst? *)
+ assert false
+ (* return_term loc (Ast.Ident (id, Some s))*)
+ | s = CSYMBOL -> return_term loc (Ast.Symbol (s, None))
+ | u = URI -> return_term loc (Ast.Ident
+ (NUri.name_of_uri (NUri.uri_of_string u), `Uri u))
| r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
- | n = NUMBER -> return_term loc (Ast.Num (n, 0))
+ | n = NUMBER -> return_term loc (Ast.Num (n, None))
| IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
| SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
| PLACEHOLDER -> return_term loc Ast.UserInput
@ make_href xmlattrs xref
in
Mpres.Mo (attrs, to_unicode literal)
- | A.Ident (literal, subst)
- | A.Uri (literal, subst) ->
+ | A.Ident (literal, _) ->
let attrs =
(RenderingAttrs.ident_attributes `MathML)
@ make_href xmlattrs xref
in
- let name = Mpres.Mi (attrs, to_unicode literal) in
- (match subst with
- | Some []
- | None -> name
- | Some substs ->
- let substs' =
- box_of mathonly (A.H, false, false) []
- (open_brace
- :: (NotationUtil.dress semicolon
- (List.map
- (fun (name, t) ->
- box_of mathonly (A.H, false, false) [] [
- Mpres.Mi ([], name);
- Mpres.Mo ([], to_unicode "\\def");
- aux [] mathonly xref prec t ])
- substs))
- @ [ closed_brace ])
- in
- let substs_maction = toggle_action [ hidden_substs; substs' ] in
- box_of mathonly (A.H, false, false) [] [ name; substs_maction ])
+ Mpres.Mi (attrs, to_unicode literal)
| A.Meta(n, l) ->
let local_context l =
box_of mathonly (A.H, false, false) []
name, (Env.TermType l, Env.TermValue t)
| Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
name, (Env.NumType, Env.NumValue s)
- | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
+ | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, `Ambiguous)) ->
name, (Env.StringType, Env.StringValue (Env.Ident s))
| _ -> assert false)
pl tl
(Ast.Literal (`Number s))
let ident i =
- add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None))
+ add_xml_attrs (RenderingAttrs.ident_attributes `MathML)
+ (Ast.Ident (i,`Ambiguous))
let ident_w_href href i =
match href with
(builtin_symbol s)
let xml_of_sort x =
- let to_string x = Ast.Ident (x, None) in
+ let to_string x = Ast.Ident (x, `Ambiguous) in
let identify x =
add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) (to_string x)
in
| Ast.Sort sort -> aux_sort sort
| Ast.Num _
| Ast.Symbol _
- | Ast.Ident (_, None) | Ast.Ident (_, Some [])
- | Ast.Uri (_, None) | Ast.Uri (_, Some [])
+ | Ast.Ident _
| Ast.Literal _
| Ast.UserInput as leaf -> leaf
| t -> NotationUtil.visit_ast ~special_k k t
| Ast.LetRec (kind, definitions, body) ->
Ast.LetRec (kind, List.map (aux_definition env) definitions,
aux env body)
- | Ast.Uri (name, None) -> Ast.Uri (name, None)
- | Ast.Uri (name, Some substs) ->
- Ast.Uri (name, Some (aux_substs env substs))
- | Ast.Ident (name, Some substs) ->
- Ast.Ident (name, Some (aux_substs env substs))
| Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
| Ast.Implicit _
List.map (fun (name, term) -> (name, aux env term)) substs
and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
and aux_variable env = function
- | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
+ | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, None)
| Ast.IdentVar name ->
(match Env.lookup_string env name with
- Env.Ident x -> Ast.Ident (x, None)
+ Env.Ident x -> Ast.Ident (x, `Ambiguous)
| Env.Var x -> Ast.Variable (Ast.IdentVar x))
| Ast.TermVar (name,(Ast.Level l|Ast.Self l)) ->
Ast.AttributedTerm (`Level l,Env.lookup_term env name)
- | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
+ | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, `Ambiguous)
| Ast.Ascription (term, name) -> assert false
and aux_magic env = function
| Ast.Default (some_pattern, none_pattern) ->
let choices_avg = ref 0.
*)
-let descr_of_domain_item = function
- | Id s -> s
- | Symbol (s, _) -> s
- | Num i -> string_of_int i
-
type ('term,'metasenv,'subst,'graph) test_result =
| Ok of 'term * 'metasenv * 'subst * 'graph
| Ko of (Stdpp.location * string) Lazy.t
let string_of_name =
function
- | Ast.Ident (n, None) -> Some n
+ | Ast.Ident (n, _) -> Some n
| _ -> assert false
;;
domain_of_term ~loc ~context term
| Ast.AttributedTerm (_, term) ->
domain_of_term ~loc ~context term
- | Ast.Symbol (symbol, instance) ->
- [ Node ([loc], Symbol (symbol, instance), []) ]
+ | Ast.Symbol (name, attr) ->
+ [ Node ([loc], Symbol (name,attr), []) ]
(* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
- | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
- | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
+ | Ast.Appl (Ast.Symbol (name, attr) as hd :: args)
+ | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (name,attr)) as hd :: args)
->
let args_dom =
List.fold_right
Ast.AttributedTerm (`Loc loc,_) -> loc
| _ -> loc
in
- [ Node ([loc], Symbol (symbol, instance), args_dom) ]
- | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
- | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
+ [ Node ([loc], Symbol (name,attr), args_dom) ]
+ | Ast.Appl (Ast.Ident (id,uri) as hd :: args)
+ | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (id,uri)) as hd :: args) ->
+ let uri = match uri with
+ | `Uri u -> Some u
+ | _ -> None
+ in
let args_dom =
List.fold_right
(fun term acc -> domain_of_term ~loc ~context term @ acc)
in
(try
(* the next line can raise Not_found *)
- ignore(find_in_context name context);
- if subst <> None then
- Ast.fail loc "Explicit substitutions not allowed here"
- else
+ ignore(find_in_context id context);
args_dom
with Not_found ->
- (match subst with
- | None -> [ Node ([loc], Id name, args_dom) ]
- | Some subst ->
- let terms =
- List.fold_left
- (fun dom (_, term) ->
- let dom' = domain_of_term ~loc ~context term in
- dom @ dom')
- [] subst in
- [ Node ([loc], Id name, terms @ args_dom) ]))
+ [ Node ([loc], Id (id,uri), args_dom) ] )
| Ast.Appl terms ->
List.fold_right
(fun term acc -> domain_of_term ~loc ~context term @ acc)
domain_of_term ~loc
~context:(string_of_name var :: context) body in
(match kind with
- | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
+ | `Exists -> [ Node ([loc], Symbol ("exists",None), (type_dom @ body_dom)) ]
| _ -> type_dom @ body_dom)
| Ast.Case (term, indty_ident, outtype, branches) ->
let term_dom = domain_of_term ~loc ~context term in
let outtype_dom = domain_of_term_option ~loc ~context outtype in
let rec get_first_constructor = function
| [] -> []
- | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
+ | (Ast.Pattern (head, Some r, _), _) :: _ ->
+ [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ]
+ | (Ast.Pattern (head, None, _), _) :: _ ->
+ [ Node ([loc], Id (head,None), []) ]
| _ :: tl -> get_first_constructor tl in
let do_branch =
function
List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
(match indty_ident with
| None -> get_first_constructor branches
- | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
+ | Some (ident, None) -> [ Node ([loc], Id (ident,None) , []) ]
+ | Some (ident, Some r) ->
+ [ Node ([loc], Id (ident,Some (NReference.string_of_reference r)), []) ])
@ term_dom @ outtype_dom @ branches_dom
| Ast.Cast (term, ty) ->
let term_dom = domain_of_term ~loc ~context term in
) [] defs
in
defs_dom @ where_dom
- | Ast.Ident (name, subst) ->
+ | Ast.Ident (name, x) ->
+ let x = match x with
+ | `Uri u -> Some u
+ | _ -> None
+ in
(try
(* the next line can raise Not_found *)
- ignore(find_in_context name context);
- if subst <> None then
- Ast.fail loc "Explicit substitutions not allowed here"
- else
- []
+ ignore(find_in_context name context); []
with Not_found ->
+ (*
(match subst with
| None -> [ Node ([loc], Id name, []) ]
| Some subst ->
let dom' = domain_of_term ~loc ~context term in
dom @ dom')
[] subst in
- [ Node ([loc], Id name, terms) ]))
- | Ast.Uri _ -> []
+ [ Node ([loc], Id name, terms) ]))*)
+ [ Node ([loc], Id (name,x), []) ])
| Ast.NRef _ -> []
| Ast.NCic _ -> []
| Ast.Implicit _ -> []
let is_in_dom2 elt =
List.exists
(function
- | Symbol (symb, 0) ->
+ | Symbol (symb,None) ->
(match elt with
Symbol (symb',_) when symb = symb' -> true
| _ -> false)
- | Num i ->
+ | Num _ ->
(match elt with
Num _ -> true
| _ -> false)
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
+(* generic function lifting splitting from type T to type (T list) *)
+let rec list_split item_split ctx pre post =
+ match post with
+ | [] -> []
+ | x :: post' ->
+ (item_split (fun v1 -> ctx (pre@v1::post')) x)@
+ list_split item_split ctx (pre@[x]) post'
+;;
+
+(* splits a 'term capture_variable *)
+let var_split ctx = function
+ | (_,None) -> []
+ | (v,Some ty) -> [(fun x -> ctx (v,Some x)),ty]
+;;
+
+let ity_split ctx (n,isind,ty,cl) =
+ [(fun x -> ctx (n,isind,x,cl)),ty]@
+ list_split (fun ctx0 (v,ty) -> [(fun x -> ctx0 (v,x)),ty])
+ (fun x -> ctx (n,isind,ty,x)) [] cl
+;;
+
+let field_split ctx (n,ty,b,m) =
+ [(fun x -> ctx (n,x,b,m)),ty]
+;;
+
+(* splits a defn. in a mutual LetRec block *)
+let letrecaux_split ctx (args,f,bo,n) =
+ list_split var_split (fun x -> ctx (x,f,bo,n)) [] args@
+ var_split (fun x -> ctx (args,x,bo,n)) f@
+ [(fun x -> ctx (args,f,x,n)),bo]
+;;
+
+(* splits a pattern (for case analysis) *)
+let pattern_split ctx = function
+ | Ast.Wildcard -> []
+ | Ast.Pattern (s,href,pl) ->
+ let rec auxpatt pre = function
+ | [] -> []
+ | (x,Some y as x')::post' ->
+ ((fun v -> ctx (Ast.Pattern (s,href,pre@(x,Some v)::post'))),y)
+ ::auxpatt (pre@[x']) post'
+ | (x,None as x')::post' -> auxpatt (pre@[x']) post'
+ in auxpatt [] pl
+;;
+
+ (* this function is used to get the children of a given node, together with
+ * their context
+ * contexts are expressed in the form of functions Ast -> Ast *)
+(* split : ('term -> 'a) -> 'term -> (('term -> 'a) * 'term) list *)
+let rec split ctx = function
+ | Ast.AttributedTerm (attr,t) ->
+ [(fun x -> ctx (Ast.AttributedTerm(attr,x))),t]
+ | Ast.Appl tl -> list_split split (fun x -> ctx (Ast.Appl x)) [] tl
+ | Ast.Binder (k,((n,None) as n'),body) ->
+ [ (fun v -> ctx (Ast.Binder (k,n',v))),body]
+ | Ast.Binder (k,((n,Some ty) as n'),body) ->
+ [(fun v -> ctx (Ast.Binder (k,(n,Some v),body))), ty
+ ;(fun v -> ctx (Ast.Binder (k,n',v))),body]
+ | Ast.Case (t,ity,outty,pl) ->
+ let outty_split = match outty with
+ | None -> []
+ | Some u -> [(fun x -> ctx (Ast.Case (t,ity,Some x,pl))),u]
+ in
+ ((fun x -> ctx (Ast.Case (x,ity,outty,pl))),t)::
+ outty_split@list_split
+ (fun ctx0 (p,x) ->
+ ((fun y -> ctx0 (p,y)),x)::pattern_split
+ (fun y -> ctx0 (y,x)) p) (fun x -> ctx (Ast.Case(t,ity,outty,x)))
+ [] pl
+ | Ast.Cast (u,v) -> [ (fun x -> ctx (Ast.Cast (x,v))),u
+ ; (fun x -> ctx (Ast.Cast (u,x))),v ]
+ | Ast.LetIn ((n,None) as n',u,v) ->
+ [ (fun x -> ctx (Ast.LetIn (n',x,v))), u
+ ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ]
+ | Ast.LetIn ((n,Some t) as n',u,v) ->
+ [ (fun x -> ctx (Ast.LetIn ((n,Some x),u,v))), t
+ ; (fun x -> ctx (Ast.LetIn (n',x,v))), u
+ ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ]
+ | Ast.LetRec (k,funs,where) -> (* we do not use where any more?? *)
+ list_split letrecaux_split (fun x -> ctx (Ast.LetRec(k,x,where))) [] funs
+ | _ -> [] (* leaves *)
+;;
+
+
+(* top_split : 'a -> ((term -> 'a) * term) list
+ * returns all the possible top-level (ctx,t) for its input *)
+let bfvisit ~pp_term top_split test t =
+ let rec aux = function
+ | [] -> None
+ | (ctx0,t0 as hd)::tl ->
+(* prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *)
+ prerr_endline ("t0 = " ^ pp_term t0);
+ if test t0 then (prerr_endline "caso 1"; Some hd)
+ else
+ let t0' = split ctx0 t0 in
+ (prerr_endline ("caso 2: length t0' = " ^ string_of_int
+ (List.length t0')); aux (tl@t0' (*split ctx0 t0*)))
+ (* in aux [(fun x -> x),t] *)
+ in aux (top_split t)
+;;
+
+let obj_split (o:Ast.term Ast.obj) = match o with
+ | Ast.Inductive (ls,itl) ->
+ list_split var_split (fun x -> Ast.Inductive (x,itl)) [] ls@
+ list_split ity_split (fun x -> Ast.Inductive (ls,x)) [] itl
+ | Ast.Theorem (flav,n,ty,None,p) ->
+ [(fun x -> Ast.Theorem (flav,n,x,None,p)), ty]
+ | Ast.Theorem (flav,n,ty,(Some bo as bo'),p) ->
+ [(fun x -> Ast.Theorem (flav,n,x,bo',p)), ty
+ ;(fun x -> Ast.Theorem (flav,n,ty,Some x,p)), bo]
+ | Ast.Record (ls,n,ty,fl) ->
+ list_split var_split (fun x -> Ast.Record (x,n,ty,fl)) [] ls@
+ [(fun x -> Ast.Record (ls,n,x,fl)),ty]@
+ list_split field_split (fun x -> Ast.Record (ls,n,ty,x)) [] fl
+;;
+
+let bfvisit_obj = bfvisit obj_split;;
+
+let bfvisit = bfvisit (fun t -> [(fun x -> x),t]) ;;
+
+(*let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library t =
+ let mk_alias = function
+ | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
+ | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
+ | Ast.Num _ -> DisambiguateTypes.Num None
+ | _ -> assert false
+ in
+ let lookup_choices =
+ fun item ->
+ (*match universe with
+ | None ->
+ lookup_in_library
+ interactive_user_uri_choice
+ input_or_locate_uri item
+ | Some e ->
+ (try Environment.find item e
+ with Not_found -> [])
+*)
+ (try Environment.find item universe
+ with Not_found -> [])
+ in
+ match t with
+ | Ast.Ident (_,None)
+ | Ast.Num (_,None)
+ | Ast.Symbol (_,None) ->
+ let choices = lookup_choices (mk_alias t) in
+ if List.length choices <> 1 then t
+ else List.hd choices
+ (* but we lose info on closedness *)
+ | t -> Ast.map (initialize_ast ~universe ~lookup_in_library) t
+;;
+*)
+
+let domain_item_of_ast = function
+ | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
+ | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
+ | Ast.Num (n,_) -> DisambiguateTypes.Num None
+ | Ast.Case(_,Some (ityname,_),_,_) -> DisambiguateTypes.Id (ityname,None)
+ | _ -> assert false
+;;
+
+let ast_of_alias_spec t alias = match (t,alias) with
+ | Ast.Ident _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri)
+ | Ast.Case (t,_,oty,pl), GrafiteAst.Ident_alias (id,uri) ->
+ Ast.Case (t,Some (id,Some (NReference.reference_of_string uri)),oty,pl)
+ | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc))
+ | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
+ | _ -> assert false
+;;
+
+let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri
+ ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl t =
+ try
+ let localization_tbl = mk_localization_tbl 503 in
+ let cic_thing =
+ interpretate_thing ~context ~env
+ ~uri ~is_path:false t ~localization_tbl
+ in
+ let foo () =
+ refine_thing metasenv subst context uri
+ ~use_coercions cic_thing expty ugraph ~localization_tbl
+ in match (refine_profiler.HExtlib.profile foo ()) with
+ | Ko _ -> false
+ | _ -> true
+ with
+ (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
+ | Invalid_choice loc_msg -> Ko loc_msg*)
+ | Invalid_choice _ -> false
+ | _ -> true
+;;
+
+let rec disambiguate_list
+ ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri ~interpretate_thing
+ ~refine_thing ~ugraph ~visit ~universe ~mk_localization_tbl ~pp_thing ~pp_term ts =
+ let disambiguate_list =
+ disambiguate_list ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri
+ ~interpretate_thing ~refine_thing ~ugraph ~visit ~universe
+ ~mk_localization_tbl ~pp_thing ~pp_term
+ in
+ let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty
+ ~env ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl
+ in
+ let find_choices item =
+ let a2s = function
+ | GrafiteAst.Ident_alias (id,_)
+ | GrafiteAst.Symbol_alias (id,_,_) -> id
+ | GrafiteAst.Number_alias _ -> "NUM"
+ in
+ let d2s = function
+ | Id (id,_)
+ | Symbol (id,_) -> id
+ | Num _ -> "NUM"
+ in
+ let res =
+ Environment.find item universe
+ in
+ prerr_endline (Printf.sprintf "choices for %s :\n%s"
+ (d2s item) (String.concat ", " (List.map a2s res)));
+ res
+ in
+
+ let get_instances ctx t =
+ try
+ let choices = find_choices (domain_item_of_ast t) in
+ List.map (fun t0 -> ctx (ast_of_alias_spec t t0)) choices
+ with
+ | Not_found -> []
+ in
+
+ match ts with
+ | [] -> None
+ | t0 :: tl ->
+ prerr_endline ("disambiguation of t0 = " ^ pp_thing t0);
+ let is_ambiguous = function
+ | Ast.Ident (_,`Ambiguous)
+ | Ast.Num (_,None)
+ | Ast.Symbol (_,None) -> true
+ | Ast.Case (_,Some (ity,None),_,_) ->
+ (prerr_endline ("ambiguous case" ^ ity);true)
+ | Ast.Case (_,None,_,_) -> prerr_endline "amb1";false
+ | Ast.Case (_,Some (ity,Some r),_,_) ->
+ (prerr_endline ("amb2 " ^ NReference.string_of_reference r);false)
+ | Ast.Ident (n,`Uri u) ->
+ (prerr_endline ("uri " ^ u ^ "inside IDENT " ^ n) ;false )
+ | _ -> false
+ in
+ let astpp = function
+ | Ast.Ident (id,_) -> "ID " ^ id
+ | Ast.Num _ -> "NUM"
+ | Ast.Symbol (sym,_) -> "SYM " ^ sym
+ | _ -> "ERROR!"
+ in
+ (* get first ambiguous subterm (or return disambiguated term) *)
+ match visit ~pp_term is_ambiguous t0 with
+ | None ->
+ prerr_endline ("not ambiguous:\n" ^ pp_thing t0);
+ Some (t0,tl)
+ | Some (ctx, t) ->
+ prerr_endline ("disambiguating node " ^ astpp t ^
+ "\nin " ^ pp_thing (ctx t));
+ (* get possible instantiations of t *)
+ let instances = get_instances ctx t in
+ (* perforate ambiguous subterms and test refinement *)
+ let survivors = List.filter test_interpr instances in
+ disambiguate_list (survivors@tl)
+;;
+
+
+(* let rec aux l =
+ match l with
+ | [] -> None
+ | (ctx,u)::vl ->
+ if test u
+ then (ctx,u)
+ else aux (vl@split ctx u)
+ in aux [t]
+;;*)
+
+(* let rec instantiate_ast = function
+ | Ident (n,Some _)
+ | Symbol (s,Some _)
+ | Num (n,Some _) as t -> []
+ | Ident (n,None) -> (* output: all possible instantiations of n *)
+ | Symbol (s,None) ->
+ | Num (n,None) ->
+
+
+ | AttributedTerm (a,u) -> AttributedTerm (a,f u)
+ | Appl tl -> Appl (List.map f tl)
+ | Binder (k,n,body) -> Binder (k,n,f body)
+ | Case (t,ity,oty,pl) ->
+ let pl' = List.map (fun (p,u) -> p,f u) pl in
+ Case (f t,ity,map_option f oty,pl')
+ | Cast (u,v) -> Cast (f u,f v)
+ | LetIn (n,u,v) -> LetIn (n,f u,f v)
+ | LetRec -> ada (* TODO *)
+ | t -> t
+*)
+
+let disambiguate_thing
+ ~context ~metasenv ~subst ~use_coercions
+ ~string_context_of_context
+ ~initial_ugraph:base_univ ~expty
+ ~mk_implicit ~description_of_alias ~fix_instance
+ ~aliases ~universe ~lookup_in_library
+ ~uri ~pp_thing ~pp_term ~domain_of_thing ~interpretate_thing ~refine_thing
+ ~visit ~mk_localization_tbl
+ (thing_txt,thing_txt_prefix_len,thing)
+=
+(* XXX: will be thrown away *)
+ let todo_dom = domain_of_thing ~context:(string_context_of_context context) thing
+ in
+ let rec aux_env env = function
+ | [] -> env
+ | Node (_, item, l) :: tl ->
+ let env =
+ Environment.add item
+ (mk_implicit
+ (match item with | Id _ | Num _ -> true | Symbol _ -> false))
+ env in
+ aux_env (aux_env env l) tl in
+ let env = aux_env aliases todo_dom in
+
+ let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty
+ ~env ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl
+ in
+(* real function *)
+ let rec aux tl =
+ match disambiguate_list ~mk_localization_tbl ~context ~metasenv ~subst
+ ~interpretate_thing ~refine_thing ~ugraph:base_univ ~visit
+ ~use_coercions ~expty ~uri ~env ~universe ~pp_thing
+ ~pp_term tl with
+ | None -> []
+ | Some (t,tl') -> t::aux tl'
+ in
+
+ let refine t =
+ let localization_tbl = mk_localization_tbl 503 in
+ match refine_thing metasenv subst context uri
+ ~use_coercions
+ (interpretate_thing ~context ~env ~uri ~is_path:false t ~localization_tbl)
+ expty base_univ ~localization_tbl with
+ | Ok (t',m',s',u') -> ([]:(Environment.key * 'f) list),m',s',t',u'
+ | Uncertain x ->
+ let _,err = Lazy.force x in
+ prerr_endline ("refinement uncertain after disambiguation: " ^ err);
+ assert false
+ | _ -> assert false
+ in
+ if not (test_interpr thing) then raise (NoWellTypedInterpretation (0,[]))
+ else
+ let res = aux [thing] in
+ let res =
+ HExtlib.filter_map (fun t -> try Some (refine t) with _ -> None) res
+ in
+ match res with
+ | [] -> raise (NoWellTypedInterpretation (0,[]))
+ | [t] -> res,false
+ | _ -> res,true
+;;
+
+(*
let disambiguate_thing
~context ~metasenv ~subst ~use_coercions
~string_context_of_context
true
in
res
+ *)
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 ->
description_of_alias:('alias -> string) ->
fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
aliases:'alias DisambiguateTypes.Environment.t ->
- universe:'alias list DisambiguateTypes.Environment.t option ->
+ universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
'alias list) ->
uri:'uri ->
pp_thing:('ast_thing -> string) ->
+ pp_term:(NotationPt.term -> string) ->
domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
interpretate_thing:(
context:'context ->
'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash ->
('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
+ visit:(pp_term:(NotationPt.term -> string) ->
+ (NotationPt.term -> bool) -> 'ast_thing ->
+ ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) ->
mk_localization_tbl:(int -> 'cichash) ->
'ast_thing disambiguator_input ->
((DisambiguateTypes.Environment.key * 'alias) list *
'metasenv * 'subst * 'refined_thing * 'ugraph)
list * bool
+
+val bfvisit :
+ pp_term:(NotationPt.term -> string) ->
+ (NotationPt.term -> bool) ->
+ NotationPt.term -> ((NotationPt.term -> NotationPt.term) * NotationPt.term) option
+
+val bfvisit_obj :
+ pp_term:(NotationPt.term -> string) ->
+ (NotationPt.term -> bool) ->
+ NotationPt.term NotationPt.obj -> ((NotationPt.term -> NotationPt.term NotationPt.obj) * NotationPt.term) option
(* $Id$ *)
type domain_item =
- | Id of string (* literal *)
- | Symbol of string * int (* literal, instance num *)
- | Num of int (* instance num *)
+ | Id of (string * string option) (* literal, opt. uri *)
+ | Symbol of string * (string option * string) option (* literal, opt. (uri,interp.) *)
+ | Num of (string option * string) option (* opt. uri, interpretation *)
+
+(*
+type domain_item =
+ | Id of string (* literal *)
+ | Symbol of string (* literal *)
+ | Num
+ *)
exception Invalid_choice of (Stdpp.location * string) Lazy.t
include Environment'
let find k env =
- match k with
- Symbol (sym,n) ->
- (try find k env
- with Not_found -> find (Symbol (sym,0)) env)
- | Num n ->
- (try find k env
- with Not_found -> find (Num 0) env)
- | _ -> find k env
+ try find k env
+ with Not_found ->
+ match k with
+ | Symbol (sym,_) -> find (Symbol (sym,None)) env
+ | Num _ -> find (Num None) env
+ | Id (id,_) -> find (Id (id,None)) env
let cons desc_of_alias k v env =
+ let default_dom_item = function
+ | Id (s,_) -> Id (s,None)
+ | Symbol (s,_) -> Symbol (s,None)
+ | Num _ -> Num None
+ in
+ (*
try
let current = find k env in
let dsc = desc_of_alias v in
- add k (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env
+ let entry = v::(List.filter (fun x -> desc_of_alias x <> dsc) current) in
+ let id = match k with
+ | Id (id,_) -> id
+ | Symbol (sym,_) -> "SYMBOL:"^sym
+ | Num _ -> "NUM"
+ in
+ prerr_endline (Printf.sprintf "updated alias for %s with entry of length %d (was: %d)" id (List.length entry) (List.length current));
+ let res = add k entry env
+ in
+ let test = find k res in
+ prerr_endline (Printf.sprintf "so the current length of the entry is %d."
+ (List.length test));
+ res
+ with Not_found -> add k [v] env
+ *)
+ let env' =
+ try
+ let current = find k env in
+ let dsc = desc_of_alias v in
+ add k (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env
+ with Not_found ->
+ add k [v] env
+ in
+ (* we also add default aliases *)
+ let k' = default_dom_item k in
+ try
+ let current = find k' env' in
+ let dsc = desc_of_alias v in
+ add k' (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env'
with Not_found ->
- add k [v] env
+ add k' [v] env'
+
end
type 'term codomain_item =
type input_or_locate_uri_type =
title:string -> ?id:string -> unit -> NReference.reference option
-let string_of_domain_item = function
- | Id s -> Printf.sprintf "ID(%s)" s
- | Symbol (s, i) -> Printf.sprintf "SYMBOL(%s,%d)" s i
- | Num i -> Printf.sprintf "NUM(instance %d)" i
+let string_of_domain_item item =
+ let f_opt f x default =
+ match x with
+ | None -> default
+ | Some y -> f y
+ in
+ match item with
+ | Id (s,huri) ->
+ Printf.sprintf "ID(%s,%s)" s (f_opt (fun x -> x) huri "_")
+ | Symbol (s,_) -> Printf.sprintf "SYMBOL(%s)" s
+ | Num _ -> "NUM"
+;;
+
*)
type domain_item =
- | Id of string (* literal *)
- | Symbol of string * int (* literal, instance num *)
- | Num of int (* instance num *)
+ | Id of (string * string option) (* literal, opt. uri *)
+ | Symbol of string * (string option * string) option (* literal, opt. (uri,interp.) *)
+ | Num of (string option * string) option (* opt. uri, interpretation *)
(* module Domain: Set.S with type elt = domain_item *)
module Environment:
sig
- include Map.S with type key = domain_item
+ include Map.S with type key = domain_item
val cons: ('b -> 'a) -> domain_item -> 'b -> 'b list t -> 'b list t
end
let rec aux =
function
[] -> []
- | (D.Symbol (s,n),ci1) as he::tl when n > 0 ->
+ | (D.Symbol (s,n),ci1) as he::tl when n <> None ->
if
List.for_all
(function
| _ -> true
) d
then
- (D.Symbol (s,0),ci1)::(aux tl)
+ (D.Symbol (s,None),ci1)::(aux tl)
else
he::(aux tl)
- | (D.Num n,ci1) as he::tl when n > 0 ->
+ | (D.Num n,ci1) as he::tl when n <> None ->
if
List.for_all
(function (D.Num _,ci2) -> compare ci1 ci2 | _ -> true) d
then
- (D.Num 0,ci1)::(aux tl)
+ (D.Num None,ci1)::(aux tl)
else
he::(aux tl)
| he::tl -> he::(aux tl)
(List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
user_asked
-let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
+let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~visit ~f thing
=
- assert (universe <> None);
- let library = false, DisambiguateTypes.Environment.empty, None in
+ let library = false, DisambiguateTypes.Environment.empty,
+ DisambiguateTypes.Environment.empty in
let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
- let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
+ let mono_aliases = true, aliases, DisambiguateTypes.Environment.empty in
let passes =
List.map
(function (fresh_instances,env,use_coercions) ->
let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
~string_context_of_context ~initial_ugraph ~expty ~mk_implicit
~description_of_alias ~fix_instance ~aliases ~universe ~lookup_in_library
- ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
+ ~uri ~pp_thing ~pp_term ~domain_of_thing ~interpretate_thing ~refine_thing ~visit
~mk_localization_tbl thing
=
let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
~context ~metasenv ~subst ~use_coercions ~string_context_of_context
~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~fix_instance
~aliases ~universe ~lookup_in_library
- ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
- ~mk_localization_tbl (txt,len,thing)
+ ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~visit
+ ~mk_localization_tbl ~pp_term (txt,len,thing)
in
disambiguate_thing ~description_of_alias ~passes ~aliases
- ~universe ~f thing
+ ~universe ~visit ~f thing
description_of_alias:('alias -> string) ->
fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
aliases:'alias DisambiguateTypes.Environment.t ->
- universe:'alias list
- DisambiguateTypes.Environment.t option ->
+ universe:GrafiteAst.alias_spec list
+ DisambiguateTypes.Environment.t ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
'alias list) ->
uri:'uri ->
pp_thing:('ast_thing -> string) ->
+ pp_term:(NotationPt.term -> string) ->
domain_of_thing:
(context: string option list -> 'ast_thing -> Disambiguate.domain) ->
interpretate_thing:(
'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash ->
('refined_thing, 'metasenv,'subst,'ugraph) Disambiguate.test_result) ->
+ visit:(pp_term:(NotationPt.term -> string) ->
+ (NotationPt.term -> bool) -> 'ast_thing ->
+ ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) ->
mk_localization_tbl:(int -> 'cichash) ->
string * int * 'ast_thing ->
((DisambiguateTypes.Environment.key * 'alias) list *
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 35
+let magic = 37
(* composed magic: term + command magics. No need to change this value *)
let magic = magic + 10000 * NotationPt.magic
type alias_spec =
- | Ident_alias of string * string (* identifier, uri *)
- | Symbol_alias of string * int * string (* name, instance no, description *)
- | Number_alias of int * string (* instance no, description *)
+ | Ident_alias of string * string (* identifier, uri *)
+ | Symbol_alias of string * string option * string (* name, uri, description *)
+ | Number_alias of string option * string (* uri, description *)
type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (* aka aliases *)
let pp_alias = function
| Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"." id uri
- | Symbol_alias (symb, instance, desc) ->
- sprintf "alias symbol \"%s\" %s= \"%s\"."
- symb
- (if instance=0 then "" else "(instance "^ string_of_int instance ^ ") ")
- desc
- | Number_alias (instance,desc) ->
- sprintf "alias num (instance %d) = \"%s\"." instance desc
+ | Symbol_alias (symb, (* uri *) _, desc) ->
+ sprintf "alias symbol \"%s\" = \"%s\"."
+ symb desc
+ | Number_alias ((* uri *) _,desc) ->
+ sprintf "alias num = \"%s\"." desc
let pp_associativity = function
| Gramext.LeftA -> "left associative"
;;
let eval_unification_hint status t n =
- let metasenv,subst,status,t =
+ let newast,metasenv,subst,status,t =
GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in
assert (metasenv=[]);
let t = NCicUntrusted.apply_subst status subst [] t in
in
let mode = GrafiteAst.WithPreferences (*assert false*) in (* MATITA 1.0 VEDI SOTTO *)
let diff =
- [DisambiguateTypes.Symbol (symbol, 0), GrafiteAst.Symbol_alias (symbol,0,dsc)]
+ (* FIXME! the uri should be filled with something meaningful! *)
+ [DisambiguateTypes.Symbol (symbol, Some (None,dsc)),
+ GrafiteAst.Symbol_alias (symbol,None,dsc)]
in
GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
;;
;;
let basic_eval_alias (mode,diff) status =
+ prerr_endline "basic_eval_alias";
GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
;;
List.fold_left
(fun status (name,cpos,arity) ->
try
- let metasenv,subst,status,t =
+ let newast,metasenv,subst,status,t =
GrafiteDisambiguate.disambiguate_nterm status None [] [] []
- ("",0,NotationPt.Ident (name,None)) in
+ ("",0,NotationPt.Ident (name,`Ambiguous)) in
assert (metasenv = [] && subst = []);
let status, nuris =
NCicCoercDeclaration.
let metasenv,subst,status,sort = match sort with
| None -> [],[],status,NCic.Sort NCic.Prop
| Some s ->
- GrafiteDisambiguate.disambiguate_nterm status None [] [] []
- (text,prefix_len,s)
+ let newast,metasenv,subst,status,sort =
+ GrafiteDisambiguate.disambiguate_nterm status None [] [] []
+ (text,prefix_len,s)
+ in metasenv,subst,status,sort
in
assert (metasenv = []);
let sort = NCicReduction.whd status ~subst [] sort in
"ninverter: found target %s, which is not a sort"
(status#ppterm ~metasenv ~subst ~context:[] sort))) in
let status = status#set_ng_mode `ProofMode in
- let metasenv,subst,status,indty =
+ let newast,metasenv,subst,status,indty =
GrafiteDisambiguate.disambiguate_nterm status None [] [] subst
(text,prefix_len,indty) in
let indtyno,(_,leftno,tys,_,_) =
code in DisambiguatePp *)
match spec with
| GrafiteAst.Ident_alias (id,uri) ->
- [DisambiguateTypes.Id id,spec]
- | GrafiteAst.Symbol_alias (symb, instance, desc) ->
- [DisambiguateTypes.Symbol (symb,instance),spec]
- | GrafiteAst.Number_alias (instance,desc) ->
- [DisambiguateTypes.Num instance,spec]
+ [DisambiguateTypes.Id (id,Some uri),spec]
+ | GrafiteAst.Symbol_alias (symb, uri, desc) ->
+ [DisambiguateTypes.Symbol (symb, Some (uri,desc)),spec]
+ | GrafiteAst.Number_alias (uri,desc) ->
+ [DisambiguateTypes.Num (Some (uri,desc)),spec]
in
let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*)
eval_alias status (mode,diff)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+(* TODO: all newast's must be returned to the caller in some way
+ * e.g. modifying the status? *)
+
(* let debug s = prerr_endline (Lazy.force s) ;;*)
let debug _ = ();;
if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
else
(try
- let metasenv,subst,status,src =
+ let newast,metasenv,subst,status,src =
GrafiteDisambiguate.disambiguate_nterm
status None ctx [] [] ("",0,src) in
let src = NCicUntrusted.apply_subst status subst [] src in
aux 0 [] ty
in
let status, tgt, arity =
- let metasenv,subst,status,tgt =
+ let newast, metasenv,subst,status,tgt =
GrafiteDisambiguate.disambiguate_nterm
status None [] [] [] ("",0,tgt) in
let tgt = NCicUntrusted.apply_subst status subst [] tgt in
;;
let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt =
- let metasenv,subst,status,ty =
+ let newast_ty,metasenv,subst,status,ty =
GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
assert (metasenv=[]);
let ty = NCicUntrusted.apply_subst status subst [] ty in
- let metasenv,subst,status,t =
+ let newast_t,metasenv,subst,status,t =
GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
assert (metasenv=[]);
let t = NCicUntrusted.apply_subst status subst [] t in
let mk_rec_corec ind_kind defs loc =
let name,ty =
match defs with
- | (params,(N.Ident (name, None), ty),_,_) :: _ ->
+ | (params,(N.Ident (name, `Ambiguous), ty),_,_) :: _ ->
let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
let ty =
List.fold_right
name,ty
| _ -> assert false
in
- let body = N.Ident (name,None) in
+ let body = N.Ident (name,`Ambiguous) in
(loc, N.Theorem(`Definition, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular))
let nmk_rec_corec ind_kind defs loc =
(params,name,typ,fields)
] ];
+ (* XXX: alias spec must be revised (no more instance nums) *)
alias_spec: [
[ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
let alpha = "[a-zA-Z]" in
let instance =
match instance with Some i -> i | None -> 0
in
- G.Symbol_alias (symbol, instance, dsc)
+ G.Symbol_alias (symbol, None, dsc)
| IDENT "num";
instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
SYMBOL "="; dsc = QSTRING ->
let instance =
match instance with Some i -> i | None -> 0
in
- G.Number_alias (instance, dsc)
+ G.Number_alias (None,dsc)
]
];
argument: [
let rec add_lambda t n =
if n > 0 then
let name = NotationUtil.fresh_name () in
- Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
- Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
+ Ast.Binder (`Lambda, (Ast.Ident (name, `Ambiguous), None),
+ Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, `Ambiguous)])
else
t
in
add_lambda t (n - count_lambda t)
in
let head =
- let symbol = Ast.Symbol (symbol, 0) in
+ let symbol = Ast.Symbol (symbol, None) in
add_idrefs idrefs symbol
in
if args = [] then head
(try
let name,_ = List.nth context (n-1) in
let name = if name = "_" then "__"^string_of_int n else name in
- idref (Ast.Ident (name,None))
+ idref (Ast.Ident (name,`Ambiguous))
with Failure "nth" | Invalid_argument "List.nth" ->
- idref (Ast.Ident ("-" ^ string_of_int (n - List.length context),None)))
- | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s status true r, None))
+ idref (Ast.Ident ("-" ^ string_of_int (n - List.length
+ context),`Ambiguous)))
+ | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s status true r, `Ambiguous))
| NCic.Meta (n,lc) when List.mem_assoc n subst ->
let _,_,t,_ = List.assoc n subst in
k ~context (NCicSubstitution.subst_meta status lc t)
| NCic.Prod (n,s,t) ->
let n = if n.[0] = '_' then "_" else n in
let binder_kind = `Forall in
- idref (Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ~context s)),
+ idref (Ast.Binder (binder_kind, (Ast.Ident (n,`Ambiguous), Some (k ~context s)),
k ~context:((n,NCic.Decl s)::context) t))
| NCic.Lambda (n,s,t) ->
- idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context s)),
+ idref (Ast.Binder (`Lambda,(Ast.Ident (n,`Ambiguous), Some (k ~context s)),
k ~context:((n,NCic.Decl s)::context) t))
| NCic.LetIn (n,s,ty,NCic.Rel 1) ->
idref (Ast.Cast (k ~context ty, k ~context s))
| NCic.LetIn (n,s,ty,t) ->
- idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context s)), k ~context
+ idref (Ast.LetIn ((Ast.Ident (n,`Ambiguous), Some (k ~context s)), k ~context
ty, k ~context:((n,NCic.Decl s)::context) t))
| NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst ->
let _,_,t,_ = List.assoc n subst in
| _ -> NCic.Appl (hd :: args)))
| NCic.Appl args as t ->
(match destroy_nat t with
- | Some n -> idref (Ast.Num (string_of_int n, -1))
+ | Some n -> idref (Ast.Num (string_of_int n, None))
| None ->
let args =
if not !hide_coercions then args
eat_branch (pred n) ctx t pat
| NCic.Prod (_, _, t), NCic.Lambda (name, s, t') ->
let cv, rhs = eat_branch 0 ((name,NCic.Decl s)::ctx) t t' in
- (Ast.Ident (name,None), Some (k ~context:ctx s)) :: cv, rhs
+ (Ast.Ident (name,`Ambiguous), Some (k ~context:ctx s)) :: cv, rhs
| _, _ -> [], k ~context:ctx pat
in
let j = ref 0 in
idref
~reference:
(match term with NCic.Const nref -> nref | _ -> assert false)
- (NotationPt.Ident ("dummy",None))
+ (NotationPt.Ident ("dummy",`Ambiguous))
in
match attrterm with
Ast.AttributedTerm (`IdRef id, _) -> id
status#disambiguate_db.aliases
let set_proof_aliases status ~implicit_aliases mode new_aliases =
+ prerr_endline "set_proof_aliases";
if mode = GrafiteAst.WithoutPreferences then
status
else
+ (prerr_endline "set_proof_aliases 2";
let aliases =
List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
status#disambiguate_db.aliases new_aliases in
(if implicit_aliases then new_aliases else []) @
status#disambiguate_db.new_aliases}
in
- status#set_disambiguate_db new_status
+ status#set_disambiguate_db new_status)
exception BaseUriNotSetYet
let __Closed_Implicit = "__Closed_Implicit__"
let ncic_mk_choice status = function
- | GrafiteAst.Symbol_alias (name, _, dsc) ->
+ | GrafiteAst.Symbol_alias (name,_, dsc) ->
if name = __Implicit then
dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
else if name = __Closed_Implicit then
(NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
~term_of_nref:(fun nref -> NCic.Const nref)
name dsc
- | GrafiteAst.Number_alias (_, dsc) ->
+ | GrafiteAst.Number_alias (_,dsc) ->
let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
desc, `Num_interp
(fun num -> match f with `Num_interp f -> f num | _ -> assert false)
let mk_implicit b =
match b with
| false ->
- GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
+ GrafiteAst.Symbol_alias (__Implicit,None,"Fake Implicit")
| true ->
- GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
+ GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit")
;;
let nlookup_in_library
interactive_user_uri_choice input_or_locate_uri item
=
match item with
- | DisambiguateTypes.Id id ->
+ | DisambiguateTypes.Id (id,_) ->
(try
let references = NCicLibrary.resolve id in
List.map
- (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
+ (fun u ->
+ GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
) references
with
NCicEnvironment.ObjectNotFound _ -> [])
| _ -> []
;;
-let fix_instance item l =
+(* XXX TO BE REMOVED: no need to fix instances any more *)
+(*let fix_instance item l =
match item with
DisambiguateTypes.Symbol (_,n) ->
List.map
(function
- GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d)
+ GrafiteAst.Symbol_alias (s,d) -> GrafiteAst.Symbol_alias (s,n,d)
| _ -> assert false
) l
| DisambiguateTypes.Num n ->
| _ -> assert false
) l
| DisambiguateTypes.Id _ -> l
-;;
+;;*)
+let fix_instance _ l = l;;
let disambiguate_nterm status expty context metasenv subst thing
=
- let diff, metasenv, subst, cic =
+ let newast, diff, metasenv, subst, cic =
singleton "first"
(NCicDisambiguate.disambiguate_term
status
~aliases:status#disambiguate_db.aliases
~expty
- ~universe:(Some status#disambiguate_db.multi_aliases)
+ ~universe:(status#disambiguate_db.multi_aliases)
~lookup_in_library:nlookup_in_library
~mk_choice:(ncic_mk_choice status)
~mk_implicit ~fix_instance
set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
diff
in
- metasenv, subst, status, cic
+ newast, metasenv, subst, status, cic
;;
~mk_choice:(ncic_mk_choice status)
~mk_implicit ~fix_instance ~uri
~aliases:status#disambiguate_db.aliases
- ~universe:(Some status#disambiguate_db.multi_aliases)
+ ~universe:(status#disambiguate_db.multi_aliases)
(text,prefix_len,obj)) in
let status =
set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
(List.exists
(function (NotationPt.IdentArg (_,id')) -> id'=id) args)
->
- let item = DisambiguateTypes.Id id in
+ let item = DisambiguateTypes.Id (id,None) in
begin
try
match
DisambiguateTypes.Environment.find item
status#disambiguate_db.aliases
with
- GrafiteAst.Ident_alias (_, uri) ->
+ GrafiteAst.Ident_alias (_,uri) ->
NotationPt.NRefPattern (NReference.reference_of_string uri)
| _ -> assert false
with Not_found ->
List.map
(fun u ->
let name = NCicPp.r2s status true u in
- DisambiguateTypes.Id name,
+ DisambiguateTypes.Id (name, Some (NReference.string_of_reference u)),
GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
) references) refs)
#status as 'status ->
NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution ->
NotationPt.term Disambiguate.disambiguator_input ->
- NCic.metasenv * NCic.substitution * 'status * NCic.term
+ NotationPt.term * NCic.metasenv * NCic.substitution * 'status * NCic.term
val disambiguate_nobj :
#status as 'status -> ?baseuri:string ->
let debug_print _ = ();;
let cic_name_of_name = function
- | Ast.Ident (n, None) -> n
+ | Ast.Ident (n,_) -> n
| _ -> assert false
;;
(NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)->
aux ~localize loc context
(NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args)))
+ | NotationPt.Appl (NotationPt.Symbol (symb, None) :: args) ->
+ NCic.Implicit `Term
| NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) ->
let cic_args = List.map (aux ~localize loc context) args in
Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
| `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body)
| `Pi
| `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
- | `Exists ->
- Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0))
- (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ]))
+ | `Exists -> assert false)
+ (*Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", None))
+ (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ])*)
| NotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux ~localize loc context term in
let cic_outtype = aux_option ~localize loc context `Term outtype in
else
let indtype_ref =
match indty_ident with
- | Some (indty_ident, _) ->
- (match Disambiguate.resolve ~env ~mk_choice
- (Id indty_ident) (`Args []) with
- | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
- | NCic.Implicit _ ->
- raise (Disambiguate.Try_again
- (lazy "The type of the term to be matched is still unknown"))
- | t ->
- raise (DisambiguateTypes.Invalid_choice
- (lazy (loc,"The type of the term to be matched "^
- "is not (co)inductive: " ^ status#ppterm
- ~metasenv:[] ~subst:[] ~context:[] t))))
+ | Some (_,Some r) -> r
+ | Some (_, None) ->
+ raise (Disambiguate.Try_again
+ (lazy "The type of the term to be matched is still unknown"))
| None ->
let rec fst_constructor =
function
- (Ast.Pattern (head, _, _), _) :: _ -> head
+ (Ast.Pattern (head, href, _), _) :: _ ->
+ head, HExtlib.map_option NReference.string_of_reference href
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
| [] -> raise (Invalid_choice (lazy (loc,"The type "^
"of the term to be matched cannot be determined "^
0 -> term
| n ->
NotationPt.Binder
- (`Lambda, (NotationPt.Ident ("_", None), None),
+ (`Lambda, (NotationPt.Ident ("_", `Ambiguous), None),
mk_lambdas (n - 1))
in
(("wildcard",None,[]),
NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
| NotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
| NotationPt.Ident _
- | NotationPt.Uri _
| NotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
- | NotationPt.Ident (name, subst) ->
- assert (subst = None);
- (try
- NCic.Rel (find_in_context name context)
- with Not_found ->
- try NCic.Const (List.assoc name obj_context)
- with Not_found ->
- Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
- | NotationPt.Uri (uri, subst) ->
- assert (subst = None);
+ | NotationPt.Ident (name, `Rel) ->
+ (try NCic.Rel (find_in_context name context)
+ with Not_found ->
+ (try NCic.Const (List.assoc name obj_context)
+ with Not_found -> assert false)) (* bug in initialize_ast *)
+ | NotationPt.Ident (name, `Ambiguous) ->
+ (try NCic.Const (List.assoc name obj_context)
+ with Not_found -> NCic.Implicit `Closed)
+ (* Disambiguate.resolve ~env ~mk_choice (Id (name,None)) (`Args [])) *)
+ | NotationPt.Ident (name, `Uri uri) ->
(try
NCic.Const (NReference.reference_of_string uri)
with NRef.IllFormedReference _ ->
| NotationPt.Implicit `JustOne -> NCic.Implicit `Term
| NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
| NotationPt.UserInput -> NCic.Implicit `Hole
+ | NotationPt.Num (num, None) -> NCic.Implicit `Closed
| NotationPt.Num (num, i) ->
Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
| NotationPt.Meta (index, subst) ->
;;
let ncic_name_of_ident = function
- | Ast.Ident (name, None) -> name
+ | Ast.Ident (name,_) -> name
| _ -> assert false
;;
NCic.Inductive (true,leftno,tyl,attrs)
;;
+let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names t =
+ (* ast_of_alias_spec is duplicate in Disambiguate *)
+ let ast_of_alias_spec t alias = match (t,alias) with
+ | _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri)
+ | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc))
+ | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
+ | _ -> assert false
+ in
+ let init = initialize_ast ~universe ~lookup_in_library in
+ let init_var ~local_names (n,ty) =
+ (n,HExtlib.map_option (init ~local_names) ty)
+ in
+ let init_vars ~local_names vars =
+ (*
+ List.fold_right (fun (n,ty) (nacc,tyacc) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) vars (local_names,[])
+ *)
+ let a,b = List.fold_left (fun (nacc,tyacc) (n,ty) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) (local_names,[]) vars
+ in a, List.rev b
+ in
+ let init_pattern ~local_names = function
+ | Ast.Wildcard as t -> local_names,t
+ | Ast.Pattern (c,uri,vars) ->
+ (* XXX verificare ordine *)
+ let ln',vars' = init_vars ~local_names vars in
+ ln',Ast.Pattern (c,uri,vars')
+ in
+ let mk_alias = function
+ | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
+ | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
+ | Ast.Num _ -> DisambiguateTypes.Num None
+ | _ -> assert false
+ in
+ let lookup_choices =
+ fun item ->
+ (*match universe with
+ | None ->
+ lookup_in_library
+ interactive_user_uri_choice
+ input_or_locate_uri item
+ | Some e ->
+ (try Environment.find item e
+ with Not_found -> [])
+*)
+ (try
+ let res = Environment.find item universe in
+ let id = match item with
+ | DisambiguateTypes.Id (id,None) -> id ^ "?"
+ | DisambiguateTypes.Id (id,_) -> id ^ "!"
+ | DisambiguateTypes.Symbol _ -> "SYM"
+ | DisambiguateTypes.Num _ -> "NUM"
+ in
+ prerr_endline (Printf.sprintf "lookup_choices of %s returns length %d" id
+ (List.length res));
+ res
+ with Not_found -> [])
+ in
+ match t with
+ | Ast.Ident (id,(`Ambiguous|`Rel))
+ when List.mem id local_names -> Ast.Ident (id,`Rel)
+ | Ast.Ident (id,`Rel) -> init ~local_names (Ast.Ident (id,`Ambiguous))
+ | Ast.Ident (_,`Ambiguous)
+ | Ast.Num (_,None)
+ | Ast.Symbol (_,None) ->
+ let choices = lookup_choices (mk_alias t) in
+ if List.length choices <> 1 then t
+ else ast_of_alias_spec t (List.hd choices)
+ | Ast.AttributedTerm (a,u) -> Ast.AttributedTerm (a, init ~local_names u)
+ | Ast.Appl tl -> Ast.Appl (List.map (init ~local_names) tl)
+ | Ast.Binder (k,(n,ty),body) ->
+ let n' = cic_name_of_name n in
+ let ty' = HExtlib.map_option (init ~local_names) ty in
+ let body' = init ~local_names:(n'::local_names) body in
+ Ast.Binder (k,(n,ty'),body')
+ | Ast.Case (t,ity,oty,pl) ->
+ let t' = init ~local_names t in
+ let oty' = HExtlib.map_option (init ~local_names) oty in
+ let pl' =
+ List.map (fun (p,u) ->
+ let ns,p' = init_pattern ~local_names p in
+ p',init ~local_names:ns u) pl in
+ Ast.Case (t',ity,oty',pl')
+ | Ast.Cast (u,v) -> Ast.Cast (init ~local_names u,init ~local_names v)
+ | Ast.LetIn ((n,ty),u,v) ->
+ let n' = cic_name_of_name n in
+ let ty' = HExtlib.map_option (init ~local_names) ty in
+ let u' = init ~local_names u in
+ let v' = init ~local_names:(n'::local_names) v in
+ Ast.LetIn ((n,ty'),u',v')
+ | Ast.LetRec (ik,l,t) ->
+ let recfuns =
+ List.fold_right (fun (_,(n,_),_,_) acc ->
+ cic_name_of_name n::acc) l [] in
+ let l' = List.map (fun (vl,(n,ty),u,m) ->
+ let ln',vl' = init_vars ~local_names vl in
+ let ty' = HExtlib.map_option (init ~local_names:ln') ty in
+ let ln'' = recfuns@ln' in
+ let u' = init ~local_names:ln'' u in
+ vl',(n,ty'),u',m) l in
+ let t' = init ~local_names:(recfuns@local_names) t in
+ Ast.LetRec (ik,l',t') (* XXX: t??? *)
+ | t -> t
+;;
+
+let initialize_obj ~universe ~lookup_in_library o =
+ let init = initialize_ast ~universe ~lookup_in_library in
+ let init_var ~local_names (n,ty) =
+ (n,HExtlib.map_option (init ~local_names) ty)
+ in
+ let init_vars ~local_names vars =
+ let a,b = List.fold_left (fun (nacc,tyacc) (n,ty) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) (local_names,[]) vars
+ in a, List.rev b
+ (*List.fold_right (fun (n,ty) (nacc,tyacc) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) vars (local_names,[])*)
+ in
+
+ match o with
+ | Ast.Inductive (ls,itl) ->
+ let ln,ls' = init_vars ~local_names:[] ls in
+ let indtys =
+ List.fold_right
+ (fun (name,_,_,_) acc -> name::acc) itl [] in
+ let itl' = List.map
+ (fun (name,isind,ty,cl) ->
+ let ty' = init ~local_names:ln ty in
+ let cl' =
+ List.map (fun (cname,cty) ->
+ cname, init ~local_names:(indtys@ln) cty) cl
+ in
+ name,isind,ty',cl') itl
+ in
+ Ast.Inductive (ls',itl')
+ | Ast.Theorem (flav,n,ty,bo,p) ->
+ Ast.Theorem (flav,n,init ~local_names:[] ty,
+ HExtlib.map_option (init ~local_names:[]) bo,p)
+ | Ast.Record (ls,n,ty,fl) ->
+ let ln,ls' = init_vars ~local_names:[] ls in
+ let ty' = init ~local_names:ln ty in
+ let fl' = List.map (fun (fn,fty,b,i) ->
+ fn,init ~local_names:ln fty,b,i) fl in
+ Ast.Record (ls,n,ty',fl')
+;;
+
let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst
~expty ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
~aliases ~universe ~lookup_in_library (text,prefix_len,term)
=
+ let local_names = List.map (fun (n,_) -> n) context in
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
let res,b =
MultiPassDisambiguator.disambiguate_thing
~context ~metasenv ~initial_ugraph:() ~aliases
~mk_implicit ~description_of_alias ~fix_instance
~string_context_of_context:(List.map (fun (x,_) -> Some x))
- ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status)
+ ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status)
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
- ~refine_thing:(refine_term status) (text,prefix_len,term)
+ ~refine_thing:(refine_term status)
+ (text,prefix_len,
+ (initialize_ast ~universe ~lookup_in_library ~local_names term))
+ ~visit:Disambiguate.bfvisit
~mk_localization_tbl ~expty ~subst
in
- List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
+ List.map (function (a,b,c,d,_) -> term,a,b,c,d) res, b
;;
+
let disambiguate_obj (status: #NCicCoercion.status)
~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
~string_context_of_context:(List.map (fun (x,_) -> Some x))
~universe
~uri:(Some uri)
- ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status))
+ ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status)) ~pp_term:(NotationPp.pp_term status)
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
~interpretate_thing:(interpretate_obj status ~mk_choice)
~refine_thing:(refine_obj status)
- (text,prefix_len,obj)
+ (text,prefix_len,(initialize_obj ~universe ~lookup_in_library obj))
+ ~visit:Disambiguate.bfvisit_obj
~mk_localization_tbl ~expty:None
in
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
aliases:'alias DisambiguateTypes.Environment.t ->
- universe:'alias list DisambiguateTypes.Environment.t option ->
+ universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
DisambiguateTypes.Environment.key ->
'alias list) ->
NotationPt.term Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item * 'alias) list *
+ (NotationPt.term *
+ (DisambiguateTypes.domain_item * 'alias) list *
NCic.metasenv *
NCic.substitution *
NCic.term) list *
fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
aliases:'alias DisambiguateTypes.Environment.t ->
- universe:'alias list DisambiguateTypes.Environment.t option ->
+ universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
DisambiguateTypes.input_or_locate_uri_type ->
let mk_id id =
let id = if id = "_" then fresh_name () else id in
- NotationPt.Ident (id,None)
+ NotationPt.Ident (id,`Ambiguous)
;;
(*CSC: cut&paste from nCicReduction.split_prods, but does not check that
let rec pp rels =
function
NCic.Rel i -> List.nth rels (i - 1)
- | NCic.Const _ as t ->
+ | NCic.Const r as t ->
NotationPt.Ident
- (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t,None)
+ (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t,
+ `Uri (NReference.string_of_reference r))
| NCic.Sort s -> NotationPt.Sort (fst (ast_of_sort s))
| NCic.Meta _
| NCic.Implicit _ -> assert false
let arg = mk_id "xxx" in
let arg_ty = mk_appl (mk_id tyname :: List.rev names) in
let bvar = mk_id "yyy" in
- let underscore = NotationPt.Ident ("_",None),None in
+ let underscore = NotationPt.Ident ("_",`Ambiguous),None in
let bvars =
HExtlib.mk_list underscore i @ [bvar,None] @
HExtlib.mk_list underscore (argsno - i -1) in
let mk_id id =
let id = if id = "_" then fresh_name () else id in
- NotationPt.Ident (id,None)
+ NotationPt.Ident (id,`Ambiguous)
;;
let rec mk_prods l t =
let mk_id id =
let id = if id = "_" then fresh_name () else id in
- NotationPt.Ident (id,None)
+ NotationPt.Ident (id,`Ambiguous)
;;
let rec split_arity status ~subst context te =
let status, (_,x) = relocate status context ty in status, Some x
in
let uri,height,metasenv,subst,obj = status#obj in
- let metasenv, subst, status, t =
+ let newast, metasenv, subst, status, t =
GrafiteDisambiguate.disambiguate_nterm status expty context metasenv subst t
in
let new_pstatus = uri,height,metasenv,subst,obj in
let context = ctx_of gty in
let htac =
first_tac
- (List.map (fun (name,_) -> exact_tac ("",0,(Ast.Ident (name,None))))
+ (List.map (fun (name,_) -> exact_tac ("",0,(Ast.Ident (name,`Ambiguous))))
context)
in
exec htac status goal) status
let path =
List.fold_left
(fun path (name,ty) ->
- NotationPt.Binder (`Forall, (NotationPt.Ident (name,None),Some ty),path))
+ NotationPt.Binder (`Forall, (NotationPt.Ident (name,`Ambiguous),Some ty),path))
(match path with Some x -> x | None -> NotationPt.UserInput) (List.rev hyps)
in
block_tac [
- generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
+ generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,`Ambiguous)) hyps);
select0_tac ~where:(txt,txtlen,(wanted,[],Some path)) ~job;
clear_tac (List.map fst hyps) ]
;;
block_tac [
select_tac ~where ~job:(`Substexpand 1) true;
exact_tac
- ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit `JustOne));
+ ("",0,Ast.LetIn((Ast.Ident (name,`Ambiguous),None),w,Ast.Implicit `JustOne));
]
;;
in
let eliminator =
let _,_,w = what in
- Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+ Ast.Appl [ Ast.Ident (name,`Ambiguous) ; Ast.Implicit `Vector ; w ]
in
exact_tac ("",0,eliminator) status) ])
;;
[ select_tac ~where ~job:(`Substexpand 2) true;
exact_tac
("",0,
- Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
+ Ast.Appl(Ast.Ident(name,`Ambiguous)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
[what]))] status
;;
block_tac
[ exact_tac
("",0,(Ast.Binder (`Lambda,
- (Ast.Ident (name,None),None),Ast.Implicit `JustOne)));
+ (Ast.Ident (name,`Ambiguous),None),Ast.Implicit `JustOne)));
if name = "_" then clear_tac [name] else id_tac ]
;;
block_tac [ intro_tac name;
cases_tac
~where:("",0,(None,[],None))
- ~what:("",0,Ast.Ident (name,None));
+ ~what:("",0,Ast.Ident (name,`Ambiguous));
if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
;;
in
let eliminator =
let _,_,w = what in
- Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+ Ast.Appl [ Ast.Ident (name,`Ambiguous) ; Ast.Implicit `Vector ; w ]
in
exact_tac ("",0,eliminator) status) ])
;;
let candidates,smart_candidates =
let test x = not (is_a_fact_ast status subst metasenv context x) in
if is_eq then
- Ast.Ident("refl",None) ::List.filter test candidates,
+ Ast.Ident("refl",`Ambiguous) ::List.filter test candidates,
List.filter test smart_candidates
else candidates,smart_candidates in
debug_print ~depth
in
if head_goals status#stack = [] then
let status = NTactics.merge_tac status in
- [(0,Ast.Ident("__intros",None)),status], cache
+ [(0,Ast.Ident("__intros",`Ambiguous)),status], cache
else
(* we reindex the equation from scratch *)
let unit_eq = index_local_equations status#eq_cache status in
let status = NTactics.merge_tac status in
- [(0,Ast.Ident("__intros",None)),status],
+ [(0,Ast.Ident("__intros",`Ambiguous)),status],
init_cache ~facts ~unit_eq () ~trace
| _ -> [],cache
;;
be empty *)
let status = NTactics.merge_tac status in
incr candidate_no;
- [(!candidate_no,Ast.Ident("__whd",None)),status])
+ [(!candidate_no,Ast.Ident("__whd",`Ambiguous)),status])
;;
let do_something signature flags status g depth gty cache =
List.map
(fun s ->
incr candidate_no;
- ((!candidate_no,Ast.Ident("__paramod",None)),s))
+ ((!candidate_no,Ast.Ident("__paramod",`Ambiguous)),s))
(auto_eq_check cache.unit_eq status)
in
let l2 =
debug_print (~depth:depth)
(lazy ("Case: " ^ NotationPp.pp_term status t));
let depth,cache =
- if t=Ast.Ident("__whd",None) ||
- t=Ast.Ident("__intros",None)
+ if t=Ast.Ident("__whd",`Ambiguous) ||
+ t=Ast.Ident("__intros",`Ambiguous)
then depth, cache
else depth+1,loop_cache in
let cache = add_to_trace status ~depth cache t in
universe constraint Type[1] < Type[2].
universe constraint Type[2] < Type[3].
universe constraint Type[3] < Type[4].
+
+inductive True : Prop ≝ I : True.
+
+(*lemma fa : ∀X:Prop.X → X.
+#X #p //
+qed.
+
+(* check fa*)
+
+lemma ggr ≝ fa.*)
+
+inductive False : Prop ≝ .
+
+inductive bool : Prop ≝ True : bool | false : bool.
+
+inductive eq (A:Type[1]) (x:A) : A → Prop ≝
+ refl: eq A x x.
+
+lemma provable_True : True → eq bool True True.
+@
(fun k,desc ->
let alias =
match k with
- | DisambiguateTypes.Id id ->
+ | DisambiguateTypes.Id (id,_opturi) ->
+ (* XXX we don't have an uri to put into Ident_alias!
+ * then we use the description??
+ * what does this code mean?? *)
+ (* FIXME we are not using info from the domain_item to
+ * fill in the alias_spec *)
GrafiteAst.Ident_alias (id, desc)
- | DisambiguateTypes.Symbol (symb, i)->
- GrafiteAst.Symbol_alias (symb, i, desc)
- | DisambiguateTypes.Num i ->
- GrafiteAst.Number_alias (i, desc)
+ | DisambiguateTypes.Symbol (symb, _)->
+ GrafiteAst.Symbol_alias (symb, None, desc)
+ | DisambiguateTypes.Num _ ->
+ GrafiteAst.Number_alias (None,desc)
in
GrafiteAstPp.pp_alias alias)
diff) ^ "\n"
"Many goals focused. Using the context of the first one\n";
let _, ctx, _ = NCicUtils.lookup_meta g menv in
ctx in
- let m, s, status, t =
+ let newast, m, s, status, t =
GrafiteDisambiguate.disambiguate_nterm
status None ctx menv subst (parsed_text,parsed_text_length,
NotationPt.Cast (t,NotationPt.Implicit `JustOne))
projects / helm.git / commitdiff