Ticket #100 (closed feature: fixed)
Support zero-arity constructors (constants)
Reported by: | hritcu | Owned by: | hritcu |
---|---|---|---|
Priority: | major | Milestone: | 0.2.1 |
Component: | zk-typechecker | Keywords: | |
Cc: |
Description
Change History
comment:2 Changed 4 years ago by hritcu
This works on all old examples (without nullary constructors).
However, it doesn't work on polymorphic nullary constructors. Inference seems impossible in this case. Indeed, alg_constr in typeterm.ml raises an exception: "result type for alg_constr is not ground".
alg_constr m f = match m with
| Constr(m',_) ->
let tl, t = get_types_f m' in if List.length tl = 0 && not(well_formed f) then
(Logmanager.log "gamma:$e\n" ~environment:[f] ~loglevel:3; raise (Termtyping "zeroary constructor and gamma not well formed"))
else
let t'l = compute_input_types_f m' f in let sigma = unify t'l tl f in let result_t = apply sigma t in if is_ground result_t then
result_t
else (* XXX zeroary sufficiently solved? *)
raise (Termtyping "result type for alg_constr is not ground")
| _ -> raise (Invalid_argument "typeterm.ml(alg_constr): no constructor given")
comment:3 Changed 4 years ago by hritcu
Previous code snipped got fucked up. Here is goes again:
alg_constr m f = match m with | Constr(m',_) -> let tl, t = get_types_f m' in if List.length tl = 0 && not(well_formed f) then (Logmanager.log "gamma:$e\n" ~environment:[f] ~loglevel:3; raise (Termtyping "zeroary constructor and gamma not well formed")) else let t'l = compute_input_types_f m' f in let sigma = unify t'l tl f in let result_t = apply sigma t in if is_ground result_t then result_t else (* XXX zeroary sufficiently solved? *) raise (Termtyping "result type for alg_constr is not ground") | _ -> raise (Invalid_argument "typeterm.ml(alg_constr): no constructor given")
comment:4 Changed 4 years ago by hritcu
- Status changed from new to closed
- Resolution set to fixed
Allowing the user to annotate polymorphic nullary constructors.
Looks like this: let emptylist = nil()(*:List(Un)*) in 0
Committed a first attempt to fix this. Needs some testing.