raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
in
let branches =
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with
+ if create_dummy_ids then
+ List.map
+ (function
+ Ast.Wildcard,term -> ("wildcard",None,[]), term
+ | Ast.Pattern _,_ ->
+ raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
+ ) branches
+ else
+ match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
Cic.InductiveDefinition (il,_,leftsno,_) ->
let _,_,_,cl =
try
| CicNotationPt.LetIn ((name, typ), def, body) ->
let cic_def = aux ~localize loc context def in
let cic_name = CicNotationUtil.cic_name_of_name name in
- let cic_def =
+ let cic_typ =
match typ with
- | None -> cic_def
- | Some t -> Cic.Cast (cic_def, aux ~localize loc context t)
+ | None -> Cic.Implicit (Some `Type)
+ | Some t -> aux ~localize loc context t
in
let cic_body = aux ~localize loc (cic_name :: context) body in
- Cic.LetIn (cic_name, cic_def, cic_body)
+ Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
| CicNotationPt.LetRec (kind, defs, body) ->
let context' =
List.fold_left
if localize then
match body with
CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
+ (* since we avoid the letin, the context has no
+ * recfuns in it *)
let l' = List.map (aux ~localize loc context) l in
`AvoidLetIn (n,l')
| _ -> assert false
Cic.CoFix (n,coinductiveFuns)
in
let counter = ref ~-1 in
- let build_term funs (var,_,_,_) t =
+ let build_term funs (var,_,ty,_) t =
incr counter;
- Cic.LetIn (Cic.Name var, fix_or_cofix !counter, t)
+ Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
in
(match cic_body with
`AvoidLetInNoAppl n ->
(try
match cic with
| Cic.Const (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
Cic.Const (uri, mk_subst uris)
| Cic.Var (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
Cic.Var (uri, mk_subst uris)
| Cic.MutInd (uri, i, []) ->
(try
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
Cic.MutInd (uri, i, mk_subst uris)
with
(*here the explicit_named_substituion is assumed to be of length 0 *)
Cic.MutInd (uri,i,[]))
| Cic.MutConstruct (uri, i, j, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
Cic.MutConstruct (uri, i, j, mk_subst uris)
| Cic.Meta _ | Cic.Implicit _ as t ->
| CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
| CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
| CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
- | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
+ | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
| CicNotationPt.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
| _ -> assert false (* god bless Bologna *)
CicNotationUtil.cic_name_of_name var :: context,
domain_of_term_option ~loc ~context ty @ res)
(add_defs context,[]) params))
+ @ dom
@ domain_of_term_option ~loc ~context:context' typ
@ domain_of_term ~loc ~context:context' body
) [] defs
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
let disambiguate_thing ~dbd ~context ~metasenv
- ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
+ ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
(thing_txt,thing_txt_prefix_len,thing)
=
failwith "Disambiguate: circular dependency"
let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
- ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
+ ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
(text,prefix_len,term)
=
let term =