Commit 1e455cab authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

No commit message

No commit message
parent d780d4ed
......@@ -552,7 +552,8 @@ sig_entries :
try fst (List.hd(term_alone ~global_data:false ~local_data:(Some (Signature sg)) Data_lexer.lexer lexbuf)) with
| Dyp.Syntax_error -> raise (Error.dyp_error lexbuf "stdin") in
let () = match output with
| true -> Printf.printf "%s : %s \n%!" (E.Signature1.term_to_string abs_term sg) (E.Signature1.type_to_string abs_type sg)
| true -> let () = Printf.printf "%s : %s\n%!" (E.Signature1.term_to_string abs_term sg) (E.Signature1.type_to_string abs_type sg) in
Printf.printf "%s : %s \n%!" (E.Signature1.term_to_string (E.Signature1.unfold abs_term sg) sg) (E.Signature1.type_to_string abs_type sg)
| false -> () in
Some (abs_term,abs_type)
with
......
......@@ -271,7 +271,7 @@ let build_expectation lst =
(match k_o_t with
| (Unset|Term),(Id|Sym|Type_or_term (LPAR|DOT)) -> Sig (Sig_dec_id (Sig_dec_equal (Entry_id (Equal_def (Type_or_term_in_def (Term,a))))))
| (Unset|Term) as k,(Type_or_term RPAR) -> Sig (Sig_dec_id (Sig_dec_equal (Entry_id (Equal_def (Type_or_term_in_def (k,a))))))
| (Unset|Type),(Type_or_term ARROW) -> Sig (Sig_dec_id (Sig_dec_equal (Entry_id (Equal_def (Type_or_term_in_def (Type,a))))))
| (Unset|Type),(Type_or_term ARROW|Type_or_term LPAR) -> Sig (Sig_dec_id (Sig_dec_equal (Entry_id (Equal_def (Type_or_term_in_def (Type,a))))))
| Unset, _ -> raise (Expect [Id;Sym;Type_or_term LPAR])
| Type, _ -> raise (Expect [Type_or_term ARROW;Semi_colon])
| Term, _ -> raise (Expect [Id;Sym;Type_or_term DOT])
......
......@@ -51,6 +51,7 @@ sig
val get_binder_argument_functional_type : string -> t -> Abstract_syntax.abstraction option
val is_declared : entry -> t -> string option
val eta_long_form : term -> stype -> t -> term
val unfold : term -> t -> term
end
module type Lexicon_sig =
......
......@@ -139,6 +139,8 @@ sig
respect to the type [ty] and signature [sg]*)
val eta_long_form : term -> stype -> t -> term
val unfold : term -> t -> term
end
(** This module signature describes the interface for modules implementing lexicons *)
......
......@@ -298,6 +298,8 @@ struct
let eta_long_form _ _ _ = failwith "Not implemented: useless"
let unfold _ = failwith "Not implemented: useless"
let raw_to_string _ = failwith "TUTUTUT"
......@@ -358,6 +360,7 @@ struct
let check _ = Printf.printf "No checking of interpretations\n%!"
let compose _ _ _ = failwith "No composition\n"
end
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