Commit 20dd0448 authored by POGODALLA Sylvain's avatar POGODALLA Sylvain
Browse files

Bug fixes

parent 1848f67c
......@@ -22,6 +22,7 @@ sig
val get_warnings : t -> Error.warning list
val to_string : t -> string
val term_to_string : term -> t -> string
(* val raw_to_string : term -> string*)
val type_to_string : stype -> t -> string
val convert_term : Abstract_syntax.term -> Abstract_syntax.type_def -> t -> term*stype
val convert_type : Abstract_syntax.type_def -> t -> stype
......
......@@ -74,6 +74,7 @@ sig
(** [term_to_string t sg] returns a string describing the term [t]
wrt the signature [sg]. *)
val term_to_string : term -> t -> string
(* val raw_to_string : term -> string*)
(** [type_to_string t sg] returns a string describing the term [t]
wrt the signature [sg]. *)
......
......@@ -52,7 +52,7 @@
let newline = ('\010' | '\013' | "\013\010")
let letter = ['a'-'z' 'A'-'Z']
let digit = ['0'-'9']
let string = (letter|digit|'_')*
let string = (letter|digit|'_')*'\''?
let symbol = ['!' '"' '#' '$' '%' '&' '\'' '*' '+' '-' '/' '<' '>' '?' '@' '[' '\\' ']' '^' '`' '{' '}' '~' ]
......
......@@ -276,6 +276,10 @@ struct
let get_binder_argument_functional_type _ _ = Some Abstract_syntax.Linear
let is_declared _ _ = None
let raw_to_string _ = failwith "TUTUTUT"
end
module Abstract_lex =
......
......@@ -52,6 +52,7 @@ module Lambda =
(* matching *)
let rec generate_var_name x env =
if List.exists (fun (_,s) -> x=s) env then
generate_var_name (Printf.sprintf "%s'" x) env
......@@ -209,6 +210,16 @@ module Lambda =
let rec raw_to_string_aux = function
| (Var i | LVar i) -> Printf.sprintf "(%d)" i,true
| (Const i
| DConst i)-> Printf.sprintf "[%d]" i,true
| Abs (_,t) -> Printf.sprintf "Lambda.%s" (fst (raw_to_string_aux t)),false
| LAbs (_,t) -> Printf.sprintf "lambda.%s" (fst (raw_to_string_aux t)),false
| App (t,u) -> Printf.sprintf "%s %s" (parenthesize (raw_to_string_aux t)) (parenthesize (raw_to_string_aux u)),false
| _ -> raise Not_yet_implemented
let raw_to_string t = fst (raw_to_string_aux t)
(* [is_linear tm] true if the lambda-term [tm] is such *)
......
......@@ -49,6 +49,7 @@ sig
val kind_to_string : kind -> (int -> Abstract_syntax.syntactic_behavior * string ) -> string
val type_to_string : stype -> (int -> Abstract_syntax.syntactic_behavior * string ) -> string
val term_to_string : term -> (int -> Abstract_syntax.syntactic_behavior * string) -> string
val raw_to_string : term -> string
val normalize : ?id_to_term:(int -> term) -> term -> term
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