(pp_term ~pp_parens:true t3)
| Ast.LetRec (kind, definitions, term) ->
let rec get_guard i = function
- | [] -> (*assert false*) Ast.Implicit
+ | [] -> (*assert false*) Ast.Implicit `JustOne
| [term, _] when i = 1 -> term
| _ :: tl -> get_guard (pred i) tl
in
let map (params, (id,typ), body, i) =
let typ =
match typ with
- None -> Ast.Implicit
+ None -> Ast.Implicit `JustOne
| Some typ -> typ
in
sprintf "%s %s on %s: %s \\def %s"
| Ast.Ident (name, Some substs)
| Ast.Uri (name, Some substs) ->
sprintf "%s \\subst [%s]" name (pp_substs substs)
- | Ast.Implicit -> "?"
+ | Ast.Implicit `Vector -> "?"
+ | Ast.Implicit `JustOne -> "..."
| Ast.Meta (index, substs) ->
sprintf "%d[%s]" index
(String.concat "; "
in
match pp_parens, t with
| false, _
- | true, Ast.Implicit
+ | true, Ast.Implicit _
| true, Ast.Sort _
| true, Ast.Ident (_, Some [])
| true, Ast.Ident (_, None) -> t_pp
(* literal, substitutions.
* Some [] -> user has given an empty explicit substitution list
* None -> user has given no explicit substitution list *)
- | Implicit
+ | Implicit of [`Vector | `JustOne]
| Meta of int * meta_subst list
| Num of string * int (* literal, instance *)
| Sort of sort_kind
| Ast.Variable _) as t -> special_k t
| (Ast.Ident _
| Ast.NRef _
- | Ast.Implicit
+ | Ast.Implicit _
| Ast.Num _
| Ast.Sort _
| Ast.Symbol _
| Ast.Ident (_, Some substs) -> aux_substs substs
| Ast.Meta (_, substs) -> aux_meta_substs substs
- | Ast.Implicit
+ | Ast.Implicit _
| Ast.Ident _
| Ast.Num _
| Ast.Sort _
| Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
| Cic.ASort (id,Cic.CProp u) -> idref id (Ast.Sort (`CProp u))
| Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput
- | Cic.AImplicit (id, _) -> idref id Ast.Implicit
+ | Cic.AImplicit (id, _) -> idref id (Ast.Implicit `JustOne)
| Cic.AProd (id,n,s,t) ->
let binder_kind =
match sort_of_id id with
| Some (s, _) -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
with Failure "nth" -> out (Printf.sprintf "%u[%i]" i (List.length c - i))
-let pp_implict out = function
+let pp_implicit out = function
| None -> out "?"
| Some `Closed -> out "?[Closed]"
| Some `Type -> out "?[Type]"
| Some `Hole -> out "?[Hole]"
+ | Some `Vector -> out "?[...]"
let pp_uri out a =
out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a))
let rec pp_term out e c = function
| C.Sort h -> pp_sort out h
| C.Rel i -> pp_rel out c i
- | C.Implicit x -> pp_implict out x
+ | C.Implicit x -> pp_implicit out x
| C.Meta (i, iss) ->
let map = function None -> out "_" | Some v -> pp_term out e c v in
out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
let cic_body =
aux ~localize loc context' (add_binders `Lambda body) in
let typ =
- match typ with Some typ -> typ | None-> CicNotationPt.Implicit in
+ match typ with
+ Some typ -> typ
+ | None-> CicNotationPt.Implicit `JustOne in
let cic_type =
aux_option ~localize loc context (Some `Type)
(Some (add_binders `Pi typ)) in
with
CicEnvironment.CircularDependency _ ->
raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
- | CicNotationPt.Implicit -> Cic.Implicit None
+ | CicNotationPt.Implicit `Vector -> assert false
+ | CicNotationPt.Implicit `JustOne -> Cic.Implicit None
| CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
| CicNotationPt.Num (num, i) ->
Disambiguate.resolve ~mk_choice ~env
(fun (context,res) (name,t) ->
let t =
match t with
- None -> CicNotationPt.Implicit
+ None -> CicNotationPt.Implicit `JustOne
| Some t -> t in
let name = CicNotationUtil.cic_name_of_name name in
name::context,(name, interpretate_term context env None false t)::res
(fun (context,res) (name,t) ->
let t =
match t with
- None -> CicNotationPt.Implicit
+ None -> CicNotationPt.Implicit `JustOne
| Some t -> t in
let name = CicNotationUtil.cic_name_of_name name in
name::context,(name, interpretate_term context env None false t)::res
let regexp qkeyword = "'" ( ident | pident ) "'"
let regexp implicit = '?'
+let regexp implicit_vector = "..."
let regexp placeholder = '%'
let regexp meta = implicit number
let s = Ulexing.utf8_lexeme lexbuf in
return lexbuf ("META", String.sub s 1 (String.length s - 1))
| implicit -> return lexbuf ("IMPLICIT", "")
+ | implicit_vector -> return lexbuf ("IMPLICITVECTOR", "")
| placeholder -> return lexbuf ("PLACEHOLDER", "")
| ident -> handle_keywords lexbuf (Hashtbl.mem !level2_ast_keywords) "IDENT"
| variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
| u = URI -> return_term loc (Ast.Uri (u, None))
| r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
| n = NUMBER -> return_term loc (Ast.Num (n, 0))
- | IMPLICIT -> return_term loc (Ast.Implicit)
+ | IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
+ | IMPLICITVECTOR -> return_term loc (Ast.Implicit `Vector)
| PLACEHOLDER -> return_term loc Ast.UserInput
| m = META -> return_term loc (Ast.Meta (int_of_string m, []))
| m = META; s = meta_substs ->
let subterms = ref [] in
let map_term t =
subterms := t :: !subterms ;
- Ast.Implicit
+ Ast.Implicit `JustOne
in
let rec aux t =
CicNotationUtil.visit_ast
((hvbox false false
(fst_row :: List.flatten tl_rows
@ [ break; keyword "in"; break; k where ])))
- | Ast.Implicit -> builtin_symbol "?"
+ | Ast.Implicit `JustOne -> builtin_symbol "?"
+ | Ast.Implicit `Vector -> builtin_symbol "..."
| Ast.Meta (n, l) ->
let local_context l =
List.map (function None -> None | Some t -> Some (k t)) l
Ast.Ident (name, Some (aux_substs env substs))
| Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
- | Ast.Implicit
+ | Ast.Implicit _
| Ast.Ident _
| Ast.Num _
| Ast.Sort _
[ Node ([loc], Id name, terms) ]))
| Ast.Uri _ -> []
| Ast.NRef _ -> []
- | Ast.Implicit -> []
+ | Ast.Implicit _ -> []
| Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
| Ast.Meta (index, local_context) ->
List.fold_left
let name,ty =
match defs with
| (params,(N.Ident (name, None), ty),_,_) :: _ ->
- let ty = match ty with Some ty -> ty | None -> N.Implicit in
+ let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
let ty =
List.fold_right
(fun var ty -> N.Binder (`Pi,var,ty)
let deannotate = function
| N.AttributedTerm (_,t) | t -> t
in match deannotate params with
- | N.Implicit -> [false]
+ | N.Implicit _ -> [false]
| N.UserInput -> [true]
| N.Appl l ->
List.map (fun x -> match deannotate x with
- | N.Implicit -> false
+ | N.Implicit _ -> false
| N.UserInput -> true
| _ -> raise (Invalid_argument "malformed target parameter list 1")) l
| _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
G.NObj (loc, N.Theorem (nflavour, name, typ, body))
| nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
body = term ->
- G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body))
+ G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body))
| IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
| NLETCOREC ; defs = let_defs ->
| flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
body = term ->
G.Obj (loc,
- N.Theorem (flavour, name, N.Implicit, Some body))
+ N.Theorem (flavour, name, N.Implicit `JustOne, Some body))
| IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
| LETCOREC ; defs = let_defs ->
F.fprintf f ")"*)
(* CSC: qua siamo grezzi *)
| NCic.Implicit `Hole -> idref (Ast.UserInput)
- | NCic.Implicit _ -> idref (Ast.Implicit)
+ | NCic.Implicit `Vector -> idref (Ast.Implicit `Vector)
+ | NCic.Implicit _ -> idref (Ast.Implicit `JustOne)
| NCic.Prod (n,s,t) ->
let n = if n.[0] = '_' then "_" else n in
let binder_kind = `Forall in
with NRef.IllFormedReference _ ->
CicNotationPt.fail loc "Ill formed reference")
| CicNotationPt.NRef nref -> NCic.Const nref
- | CicNotationPt.Implicit -> NCic.Implicit `Term
+ | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
+ | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
| CicNotationPt.UserInput -> NCic.Implicit `Hole
| CicNotationPt.Num (num, i) ->
Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
res
| Some (CicNotationPt.AttributedTerm (_, term)) ->
aux_option ~localize loc context annotation (Some term)
- | Some CicNotationPt.Implicit -> NCic.Implicit annotation
+ | Some CicNotationPt.Implicit `JustOne -> NCic.Implicit annotation
+ | Some CicNotationPt.Implicit `Vector -> assert false
| Some term -> aux ~localize loc context term
in
(fun ~context -> aux ~localize:true HExtlib.dummy_floc context),
(fun (context,res) (name,t) ->
let t =
match t with
- None -> CicNotationPt.Implicit
+ None -> CicNotationPt.Implicit `JustOne
| Some t -> t in
let name = cic_name_of_name name in
let t =
(fun (context,res) (name,t) ->
let t =
match t with
- None -> CicNotationPt.Implicit
+ None -> CicNotationPt.Implicit `JustOne
| Some t -> t in
let name = cic_name_of_name name in
let t =
type sort = Prop | Type of universe
-type implicit_annotation = [ `Closed | `Type | `Hole | `Term | `Typeof of int ]
+type implicit_annotation =
+ [ `Closed | `Type | `Hole | `Term | `Typeof of int | `Vector ]
type lc_kind = Irl of int | Ctx of term list
| `Hole -> "□"
| `Term -> "Term"
| `Typeof x -> "Ty("^string_of_int x^")"
+ | `Vector -> "..."
;;
let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t =
params @
[p_name] @
k_names @
- List.map (fun _ -> CicNotationPt.Implicit)
+ List.map (fun _ -> CicNotationPt.Implicit `JustOne)
(List.tl args) @
[mk_appl (name::abs)])))
| _ -> mk_id name,None
(function x::_ -> x | _ -> assert false) 80
(CicNotationPres.mpres_of_box boxml)));
*)
- CicNotationPt.Theorem (`Definition,srec_name,CicNotationPt.Implicit,Some res)
+ CicNotationPt.Theorem
+ (`Definition,srec_name,CicNotationPt.Implicit `JustOne,Some res)
;;
let ast_of_sort s =
(function x::_ -> x | _ -> assert false)
80 (CicNotationPres.render (fun _ -> None)
(TermContentPres.pp_ast res)));*)
- CicNotationPt.Theorem (`Definition,projname,CicNotationPt.Implicit,Some res)
+ CicNotationPt.Theorem
+ (`Definition,projname,CicNotationPt.Implicit `JustOne,Some res)
;;
let mk_projections (_,_,_,_,obj) =
let generalize0_tac args =
if args = [] then id_tac
- else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
+ else exact_tac ("",0,Ast.Appl (Ast.Implicit `JustOne :: args))
;;
let select0_tac ~where:(wanted,hyps,where) ~job =
let letin_tac ~where ~what:(_,_,w) name =
block_tac [
select_tac ~where ~job:(`Substexpand 1) true;
- exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit));
+ exact_tac
+ ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit `JustOne));
]
;;
| _ -> assert false
in
let holes =
- HExtlib.mk_list Ast.Implicit (ity.leftno+1+ ity.consno + ity.rightno) in
+ HExtlib.mk_list (Ast.Implicit `JustOne)
+ (ity.leftno+1+ ity.consno + ity.rightno) in
let eliminator =
let _,_,w = what in
Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
[ select_tac ~where ~job:(`Substexpand 1) true;
exact_tac
("",0,
- Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @
+ Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
[what]))] status
;;
block_tac
[ exact_tac
("",0,(Ast.Binder (`Lambda,
- (Ast.Ident (name,None),None),Ast.Implicit)));
+ (Ast.Ident (name,None),None),Ast.Implicit `JustOne)));
if name = "_" then clear_tac [name] else id_tac ]
;;
(fun _ ->
[GA.Executable(floc,GA.NTactic(floc,
[GA.NApply (floc,
- PT.Appl [mk_ident "ex_intro";PT.Implicit;PT.Implicit;
- PT.Implicit;PT.Implicit]);GA.NBranch floc]));
+ PT.Appl
+ [mk_ident "ex_intro";PT.Implicit `JustOne;PT.Implicit `JustOne;
+ PT.Implicit `JustOne;PT.Implicit `JustOne]);GA.NBranch floc]));
GA.Executable(floc,GA.NTactic(floc,
[GA.NPos (floc,[2])]))])
fv))
| Cic.Const _ as t ->
PT.Ident (pp_t c t, None)
| Cic.Appl l -> PT.Appl (List.map (aux c) l)
- | Cic.Implicit _ -> PT.Implicit
+ | Cic.Implicit _ -> PT.Implicit `JustOne
| Cic.Lambda (Cic.Name n, s, t) ->
PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Decl s)::c) t)
| Cic.LetIn (Cic.Name n, s, ty, t) ->
PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
- | Cic.Meta _ -> PT.Implicit
+ | Cic.Meta _ -> PT.Implicit `JustOne
| Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
| Cic.Sort Cic.Set -> PT.Sort `Set
| Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
projects / helm.git / commitdiff