Commit 36bc8e92 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

inductive (en cours)

parent 4ba2c4c3
......@@ -366,7 +366,7 @@ indcases:
;
indcase:
| uident COLON lexpr { (loc_i 1,$1,$3) }
| uident COLON lexpr { ($1,$3) }
;
primitive_type:
......
......@@ -123,8 +123,8 @@ type prop_kind =
type decl =
| TypeDecl of loc * type_decl list
| Logic of loc * logic_decl list
| Inductive_def of loc * ident * pty list * (loc * ident * lexpr) list
| Prop of loc * prop_kind * ident * lexpr
| Inductive_def of loc * ident * pty list * (ident * lexpr) list
| UseClone of loc * use * clone_subst option
| Namespace of loc * ident * decl list
......
......@@ -900,6 +900,14 @@ let add_prop k loc s f th =
with ClashSymbol _ ->
error ~loc (Clash s.id)
let add_inductive loc id tyl cl th =
let denv = create_denv th in
let pl = List.map (fun ty -> ty_of_dty (dty denv ty)) tyl in
let ps = create_psymbol (id_user id.id loc) pl in
let th' = add_decl th (create_logic [Lpredicate (ps, None)]) in
(*TODO*)
add_decl th (create_logic [Linductive (ps, [])])
let find_in_loadpath env f =
let rec find c lp = match lp, c with
| [], None ->
......@@ -994,6 +1002,8 @@ and add_decl env th = function
add_logics loc dl th
| Prop (loc, k, s, f) ->
add_prop (prop_kind k) loc s f th
| Inductive_def (loc, id, tyl, cl) ->
add_inductive loc id tyl cl th
| UseClone (loc, use, subst) ->
let t = find_theory env use.use_theory in
let use_or_clone th = match subst with
......@@ -1038,8 +1048,6 @@ and add_decl env th = function
let th = open_namespace th in
let th = add_decls env th dl in
close_namespace th id ~import:false
| Inductive_def _ ->
assert false (*TODO*)
and add_theory env pt =
let id = pt.pt_name in
......
......@@ -149,8 +149,9 @@ let print_logic_decl fmt = function
| Lpredicate (ps,Some fd) ->
fprintf fmt "@[<hov 2>logic %a :@ %a@]" print_ident ps.ls_name
print_fmla (ps_defn_axiom fd)
| Linductive _ ->
assert false (*TODO*)
| Linductive (ps, fl) ->
fprintf fmt "@[<hov 2>inductive %a ...@]" print_ident ps.ls_name
let print_decl fmt d = match d.d_node with
| Dtype tl ->
......
......@@ -6,7 +6,10 @@ theory A
type 'a list = Nil | Cons('a, 'a list)
axiom A : forall x,y:int, z:real [x+y, z=z]. x=x
inductive even_length(int list) =
| Even_nil : even_length(Nil)
| Even_cons: forall x,y:'a, l:'a list.
even_length(l) -> even_length(cons(x,cons(y,l)))
end
theory TestPrelude
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment